Library FSetWeakDecide
This file implements a decision procedure for a certain
class of propositions involving finite sets.
Require Import FSetWeak.
Module Decide (Import M : S).
Overview
This functor defines the tacticfsetdec
, which will
solve any valid goal of the form
forall s1 ... sn, forall x1 ... xm, P1 -> ... -> Pk -> P
where
P
's are defined by the grammar:
P ::= | Q | Empty F | Subset F F' | Equal F F' Q ::= | E.eq X X' | In X F | Q /\ Q' | Q \/ Q' | Q -> Q' | Q <-> Q' | ~ Q | True | False F ::= | S | empty | singleton X | add X F | remove X F | union F F' | inter F F' | diff F F' X ::= x1 | ... | xm S ::= s1 | ... | sn
The tactic will also work on some goals that vary slightly from the above form:
- The variables and hypotheses may be mixed in any order and may have already been introduced into the context. Moreover, there may be additional, unrelated hypotheses mixed in (these will be ignored).
- A conjunction of hypotheses will be handled as easily as
separate hypotheses, i.e.,
P1 /\ P2 -> P
can be solved iffP1 -> P2 -> P
can be solved. -
fsetdec
should solve any goal if the FSet-related hypotheses are contradictory. -
fsetdec
will first perform any necessary zeta and beta reductions and will invokesubst
to eliminate any Coq equalities between finite sets or their elements. - If
E.eq
is convertible with Coq's equality, it will not matter which one is used in the hypotheses or conclusion. - The tactic can solve goals where the finite sets or set
elements are expressed by Coq terms that are more complicated
than variables. However, non-local definitions are not
expanded, and Coq equalities between non-variable terms are
not used. For example, this goal will be solved:
forall (f : t -> t), forall (g : elt -> elt), forall (s1 s2 : t), forall (x1 x2 : elt), Equal s1 (f s2) -> E.eq x1 (g (g x2)) -> In x1 s1 -> In (g (g x2)) (f s2)
This one will not be solved:
forall (f : t -> t), forall (g : elt -> elt), forall (s1 s2 : t), forall (x1 x2 : elt), Equal s1 (f s2) -> E.eq x1 (g x2) -> In x1 s1 -> g x2 = g (g x2) -> In (g (g x2)) (f s2)
Facts and Tactics for Propositional Logic
These lemmas and tactics are in a module so that they do not affect the namespace if you import the enclosing moduleDecide
.
Module FSetLogicalFacts.
Require Export Decidable.
Require Export Setoid.
Lemmas and Tactics About Decidable Propositions
XXX: The lemmadec_iff
should have been included in
Decidable.v
. Some form of the solve_decidable
tactics below would also make sense in Decidable.v
.
Lemma dec_iff : forall P Q : Prop,
decidable P ->
decidable Q ->
decidable (P <-> Q).
With this hint database, we can leverage
auto
to check
decidability of propositions.
Hint Resolve
dec_True dec_False dec_or dec_and dec_imp dec_not dec_iff
: decidable_prop.
solve_decidable using lib
will solve goals about the
decidability of a proposition, assisted by an auxiliary
database of lemmas. The database is intended to contain
lemmas stating the decidability of base propositions,
(e.g., the decidability of equality on a particular
inductive type).
Tactic Notation "solve_decidable" "using" ident(db) :=
match goal with
| |- decidable ?P =>
solve [ auto 100 with decidable_prop db ]
end.
Tactic Notation "solve_decidable" :=
solve_decidable using core.
Propositional Equivalences Involving Negation
These are all written with the unfolded form of negation, since I am not sure if setoid rewriting will always perform conversion.
Eliminating Negations
We begin with lemmas that, when read from left to right, can be understood as ways to eliminate uses ofnot
.
Lemma not_true_iff :
(True -> False) <-> False.
Lemma not_false_iff :
(False -> False) <-> True.
Lemma not_not_iff : forall P : Prop,
decidable P ->
(((P -> False) -> False) <-> P).
Lemma contrapositive : forall P Q : Prop,
decidable P ->
(((P -> False) -> (Q -> False)) <-> (Q -> P)).
Lemma or_not_l_iff_1 : forall P Q : Prop,
decidable P ->
((P -> False) \/ Q <-> (P -> Q)).
Lemma or_not_l_iff_2 : forall P Q : Prop,
decidable Q ->
((P -> False) \/ Q <-> (P -> Q)).
Lemma or_not_r_iff_1 : forall P Q : Prop,
decidable P ->
(P \/ (Q -> False) <-> (Q -> P)).
Lemma or_not_r_iff_2 : forall P Q : Prop,
decidable Q ->
(P \/ (Q -> False) <-> (Q -> P)).
Lemma imp_not_l : forall P Q : Prop,
decidable P ->
(((P -> False) -> Q) <-> (P \/ Q)).
Moving Negations Around
We have four lemmas that, when read from left to right, describe how to push negations toward the leaves of a proposition and, when read from right to left, describe how to pull negations toward the top of a proposition.
Lemma not_or_iff : forall P Q : Prop,
(P \/ Q -> False) <-> (P -> False) /\ (Q -> False).
Lemma not_and_iff : forall P Q : Prop,
(P /\ Q -> False) <-> (P -> Q -> False).
Lemma not_imp_iff : forall P Q : Prop,
decidable P ->
(((P -> Q) -> False) <-> P /\ (Q -> False)).
Lemma not_imp_rev_iff : forall P Q : Prop,
decidable P ->
(((P -> Q) -> False) <-> (Q -> False) /\ P).
Tactic Notation "fold" "any" "not" :=
repeat (
match goal with
| H: context [?P -> False] |- _ =>
fold (~ P) in H
| |- context [?P -> False] =>
fold (~ P)
end).
push not using db
will pushes all negations to the
leaves of propositions in the goal, using the lemmas in
db
to assist in checking the decidability of the
propositions involved. If using db
is omitted, then
core
will be used. Additional versions are provided
to manipulate the hypotheses or the hypotheses and goal
together.
XXX: This tactic and the similar subsequent ones should have been defined using
autorewrite
. However, there
is a bug in the order that Coq generates subgoals when
rewriting using a setoid. In order to work around this
bug, these tactics had to be written out in an explicit
way. When the bug is fixed these tactics will break!!
Tactic Notation "push" "not" "using" ident(db) :=
unfold not, iff;
repeat (
match goal with
(** simplification by not_true_iff *)
| |- context [True -> False] =>
rewrite not_true_iff
(** simplification by not_false_iff *)
| |- context [False -> False] =>
rewrite not_false_iff
(** simplification by not_not_iff *)
| |- context [(?P -> False) -> False] =>
rewrite (not_not_iff P);
[ solve_decidable using db | ]
(** simplification by contrapositive *)
| |- context [(?P -> False) -> (?Q -> False)] =>
rewrite (contrapositive P Q);
[ solve_decidable using db | ]
(** simplification by or_not_l_iff_1/_2 *)
| |- context [(?P -> False) \/ ?Q] =>
(rewrite (or_not_l_iff_1 P Q);
[ solve_decidable using db | ]) ||
(rewrite (or_not_l_iff_2 P Q);
[ solve_decidable using db | ])
(** simplification by or_not_r_iff_1/_2 *)
| |- context [?P \/ (?Q -> False)] =>
(rewrite (or_not_r_iff_1 P Q);
[ solve_decidable using db | ]) ||
(rewrite (or_not_r_iff_2 P Q);
[ solve_decidable using db | ])
(** simplification by imp_not_l *)
| |- context [(?P -> False) -> ?Q] =>
rewrite (imp_not_l P Q);
[ solve_decidable using db | ]
(** rewriting by not_or_iff *)
| |- context [?P \/ ?Q -> False] =>
rewrite (not_or_iff P Q)
(** rewriting by not_and_iff *)
| |- context [?P /\ ?Q -> False] =>
rewrite (not_and_iff P Q)
(** rewriting by not_imp_iff *)
| |- context [(?P -> ?Q) -> False] =>
rewrite (not_imp_iff P Q);
[ solve_decidable using db | ]
end);
fold any not.
Tactic Notation "push" "not" :=
push not using core.
Tactic Notation
"push" "not" "in" "*" "|-" "using" ident(db) :=
unfold not, iff in * |-;
repeat (
match goal with
(** simplification by not_true_iff *)
| H: context [True -> False] |- _ =>
rewrite not_true_iff in H
(** simplification by not_false_iff *)
| H: context [False -> False] |- _ =>
rewrite not_false_iff in H
(** simplification by not_not_iff *)
| H: context [(?P -> False) -> False] |- _ =>
rewrite (not_not_iff P) in H;
[ | solve_decidable using db ]
(** simplification by contrapositive *)
| H: context [(?P -> False) -> (?Q -> False)] |- _ =>
rewrite (contrapositive P Q) in H;
[ | solve_decidable using db ]
(** simplification by or_not_l_iff_1/_2 *)
| H: context [(?P -> False) \/ ?Q] |- _ =>
(rewrite (or_not_l_iff_1 P Q) in H;
[ | solve_decidable using db ]) ||
(rewrite (or_not_l_iff_2 P Q) in H;
[ | solve_decidable using db ])
(** simplification by or_not_r_iff_1/_2 *)
| H: context [?P \/ (?Q -> False)] |- _ =>
(rewrite (or_not_r_iff_1 P Q) in H;
[ | solve_decidable using db ]) ||
(rewrite (or_not_r_iff_2 P Q) in H;
[ | solve_decidable using db ])
(** simplification by imp_not_l *)
| H: context [(?P -> False) -> ?Q] |- _ =>
rewrite (imp_not_l P Q) in H;
[ | solve_decidable using db ]
(** rewriting by not_or_iff *)
| H: context [?P \/ ?Q -> False] |- _ =>
rewrite (not_or_iff P Q) in H
(** rewriting by not_and_iff *)
| H: context [?P /\ ?Q -> False] |- _ =>
rewrite (not_and_iff P Q) in H
(** rewriting by not_imp_iff *)
| H: context [(?P -> ?Q) -> False] |- _ =>
rewrite (not_imp_iff P Q) in H;
[ | solve_decidable using db ]
end);
fold any not.
Tactic Notation "push" "not" "in" "*" "|-" :=
push not in * |- using core.
Tactic Notation "push" "not" "in" "*" "using" ident(db) :=
push not using db; push not in * |- using db.
Tactic Notation "push" "not" "in" "*" :=
push not in * using core.
pull not using db
will pull as many negations as
possible toward the top of the propositions in the goal,
using the lemmas in db
to assist in checking the
decidability of the propositions involved. If using
db
is omitted, then core
will be used. Additional
versions are provided to manipulate the hypotheses or
the hypotheses and goal together.
Tactic Notation "pull" "not" "using" ident(db) :=
unfold not, iff;
repeat (
match goal with
(** simplification by not_true_iff *)
| |- context [True -> False] =>
rewrite not_true_iff
(** simplification by not_false_iff *)
| |- context [False -> False] =>
rewrite not_false_iff
(** simplification by not_not_iff *)
| |- context [(?P -> False) -> False] =>
rewrite (not_not_iff P);
[ solve_decidable using db | ]
(** simplification by contrapositive *)
| |- context [(?P -> False) -> (?Q -> False)] =>
rewrite (contrapositive P Q);
[ solve_decidable using db | ]
(** simplification by or_not_l_iff_1/_2 *)
| |- context [(?P -> False) \/ ?Q] =>
(rewrite (or_not_l_iff_1 P Q);
[ solve_decidable using db | ]) ||
(rewrite (or_not_l_iff_2 P Q);
[ solve_decidable using db | ])
(** simplification by or_not_r_iff_1/_2 *)
| |- context [?P \/ (?Q -> False)] =>
(rewrite (or_not_r_iff_1 P Q);
[ solve_decidable using db | ]) ||
(rewrite (or_not_r_iff_2 P Q);
[ solve_decidable using db | ])
(** simplification by imp_not_l *)
| |- context [(?P -> False) -> ?Q] =>
rewrite (imp_not_l P Q);
[ solve_decidable using db | ]
(** rewriting by not_or_iff *)
| |- context [(?P -> False) /\ (?Q -> False)] =>
rewrite <- (not_or_iff P Q)
(** rewriting by not_and_iff *)
| |- context [?P -> ?Q -> False] =>
rewrite <- (not_and_iff P Q)
(** rewriting by not_imp_iff *)
| |- context [?P /\ (?Q -> False)] =>
rewrite <- (not_imp_iff P Q);
[ solve_decidable using db | ]
(** rewriting by not_imp_rev_iff *)
| |- context [(?Q -> False) /\ ?P] =>
rewrite <- (not_imp_rev_iff P Q);
[ solve_decidable using db | ]
end);
fold any not.
Tactic Notation "pull" "not" :=
pull not using core.
Tactic Notation
"pull" "not" "in" "*" "|-" "using" ident(db) :=
unfold not, iff in * |-;
repeat (
match goal with
(** simplification by not_true_iff *)
| H: context [True -> False] |- _ =>
rewrite not_true_iff in H
(** simplification by not_false_iff *)
| H: context [False -> False] |- _ =>
rewrite not_false_iff in H
(** simplification by not_not_iff *)
| H: context [(?P -> False) -> False] |- _ =>
rewrite (not_not_iff P) in H;
[ | solve_decidable using db ]
(** simplification by contrapositive *)
| H: context [(?P -> False) -> (?Q -> False)] |- _ =>
rewrite (contrapositive P Q) in H;
[ | solve_decidable using db ]
(** simplification by or_not_l_iff_1/_2 *)
| H: context [(?P -> False) \/ ?Q] |- _ =>
(rewrite (or_not_l_iff_1 P Q) in H;
[ | solve_decidable using db ]) ||
(rewrite (or_not_l_iff_2 P Q) in H;
[ | solve_decidable using db ])
(** simplification by or_not_r_iff_1/_2 *)
| H: context [?P \/ (?Q -> False)] |- _ =>
(rewrite (or_not_r_iff_1 P Q) in H;
[ | solve_decidable using db ]) ||
(rewrite (or_not_r_iff_2 P Q) in H;
[ | solve_decidable using db ])
(** simplification by imp_not_l *)
| H: context [(?P -> False) -> ?Q] |- _ =>
rewrite (imp_not_l P Q) in H;
[ | solve_decidable using db ]
(** rewriting by not_or_iff *)
| H: context [(?P -> False) /\ (?Q -> False)] |- _ =>
rewrite <- (not_or_iff P Q) in H
(** rewriting by not_and_iff *)
| H: context [?P -> ?Q -> False] |- _ =>
rewrite <- (not_and_iff P Q) in H
(** rewriting by not_imp_iff *)
| H: context [?P /\ (?Q -> False)] |- _ =>
rewrite <- (not_imp_iff P Q) in H;
[ | solve_decidable using db ]
(** rewriting by not_imp_rev_iff *)
| H: context [(?Q -> False) /\ ?P] |- _ =>
rewrite <- (not_imp_rev_iff P Q) in H;
[ | solve_decidable using db ]
end);
fold any not.
Tactic Notation "pull" "not" "in" "*" "|-" :=
pull not in * |- using core.
Tactic Notation "pull" "not" "in" "*" "using" ident(db) :=
pull not using db; pull not in * |- using db.
Tactic Notation "pull" "not" "in" "*" :=
pull not in * using core.
End FSetLogicalFacts.
Import FSetLogicalFacts.
Auxiliary Tactics
Again, these lemmas and tactics are in a module so that they do not affect the namespace if you import the enclosing moduleDecide
.
Module FSetDecideAuxiliary.
if t then t1 else t2
executes t
and, if it does not
fail, then t1
will be applied to all subgoals
produced. If t
fails, then t2
is executed.
Tactic Notation
"if" tactic(t)
"then" tactic(t1)
"else" tactic(t2) :=
first [ t; first [ t1 | fail 2 ] | t2 ].
prop P holds by t
succeeds (but does not modify the
goal or context) if the proposition P
can be proved by
t
in the current context. Otherwise, the tactic
fails.
Tactic Notation "prop" constr(P) "holds" "by" tactic(t) :=
let H := fresh in
assert P as H by t;
clear H.
This tactic acts just like
assert ... by ...
but will
fail if the context already contains the proposition.
Tactic Notation "assert" "new" constr(e) "by" tactic(t) :=
match goal with
| H: e |- _ => fail 1
| _ => assert e by t
end.
subst++
is similar to subst
except that
- it never fails (as
subst
does on recursive equations), - it substitutes locally defined variable for their definitions,
- it performs beta reductions everywhere, which may arise after substituting a locally defined function for its definition.
Tactic Notation "subst" "++" :=
repeat (
match goal with
| x : _ |- _ => subst x
end);
cbv zeta beta in *.
If you have a negated goal and
H
is a negated
hypothesis, then contra H
exchanges your goal and H
,
removing the negations. (Just like swap
but reuses
the same name.
Ltac contra H :=
let J := fresh in
unfold not;
unfold not in H;
intros J;
apply H;
clear H;
rename J into H.
decompose records
calls decompose record H
on every
relevant hypothesis H
.
Tactic Notation "decompose" "records" :=
repeat (
match goal with
| H: _ |- _ => progress (decompose record H); clear H
end).
Discarding Irrelevant Hypotheses
We will want to clear the context of any non-FSet-related hypotheses in order to increase the speed of the tactic. To do this, we will need to be able to decide which are relevant. We do this by making a simple inductive definition classifying the propositions of interest.
Inductive FSet_elt_Prop : Prop -> Prop :=
| eq_Prop : forall (S : Set) (x y : S),
FSet_elt_Prop (x = y)
| eq_elt_prop : forall x y,
FSet_elt_Prop (E.eq x y)
| In_elt_prop : forall x s,
FSet_elt_Prop (In x s)
| True_elt_prop :
FSet_elt_Prop True
| False_elt_prop :
FSet_elt_Prop False
| conj_elt_prop : forall P Q,
FSet_elt_Prop P ->
FSet_elt_Prop Q ->
FSet_elt_Prop (P /\ Q)
| disj_elt_prop : forall P Q,
FSet_elt_Prop P ->
FSet_elt_Prop Q ->
FSet_elt_Prop (P \/ Q)
| impl_elt_prop : forall P Q,
FSet_elt_Prop P ->
FSet_elt_Prop Q ->
FSet_elt_Prop (P -> Q)
| not_elt_prop : forall P,
FSet_elt_Prop P ->
FSet_elt_Prop (~ P).
Inductive FSet_Prop : Prop -> Prop :=
| elt_FSet_Prop : forall P,
FSet_elt_Prop P ->
FSet_Prop P
| Empty_FSet_Prop : forall s,
FSet_Prop (Empty s)
| Subset_FSet_Prop : forall s1 s2,
FSet_Prop (Subset s1 s2)
| Equal_FSet_Prop : forall s1 s2,
FSet_Prop (Equal s1 s2).
Here is the tactic that will throw away hypotheses that
are not useful (for the intended scope of the
fsetdec
tactic).
Hint Constructors FSet_elt_Prop FSet_Prop : FSet_Prop.
Ltac discard_nonFSet :=
decompose records;
repeat (
match goal with
| H : ?P |- _ =>
if prop (FSet_Prop P) holds by
(auto 100 with FSet_Prop)
then fail
else clear H
end).
Turning Set Operators into Propositional Connectives
The lemmas will be used to break down set operations into propositional formulas built over the predicatesIn
and E.eq
applied only to variables. We are going
to use them with autorewrite
. (There were copied from
the Facts
functor to break that module dependency.)
Section Iff.
Variables s s' : t.
Variables x y : elt.
Lemma empty_iff : In x empty <-> False.
Lemma singleton_iff : In y (singleton x) <-> E.eq x y.
Lemma add_iff : In y (add x s) <-> E.eq x y \/ In y s.
Lemma remove_iff :
In y (remove x s) <-> In y s /\ ~ E.eq x y.
Lemma union_iff :
In x (union s s') <-> In x s \/ In x s'.
Lemma inter_iff :
In x (inter s s') <-> In x s /\ In x s'.
Lemma diff_iff :
In x (diff s s') <-> In x s /\ ~ In x s'.
End Iff.
Hint Rewrite
empty_iff singleton_iff add_iff remove_iff union_iff
inter_iff diff_iff
: set_simpl.
In
is decidable.
Lemma dec_In : forall x s,
decidable (In x s).
E.eq
is decidable.
Lemma dec_eq : forall (x y : E.t),
decidable (E.eq x y).
The hint database
FSet_decidability
will be given to
the push_neg
tactic from the module Negation
.
Hint Resolve dec_In dec_eq : FSet_decidability.
Normalizing Propositions About Equality
We have to deal with the fact thatE.eq
may be
convertible with Coq's equality. Thus, we will find the
following tactics useful to replace one form with the
other everywhere.
The next tactic,
Logic_eq_to_E_eq
, mentions the term
E.t
; thus, we must ensure that E.t
is used in favor
of any other convertible but syntactically distinct
term.
Ltac change_to_E_t :=
repeat (
match goal with
| H : ?T |- _ =>
progress (change T with E.t in H);
repeat (
match goal with
| J : _ |- _ => progress (change T with E.t in J)
| |- _ => progress (change T with E.t)
end )
| H : forall x : ?T, _ |- _ =>
progress (change T with E.t in H);
repeat (
match goal with
| J : _ |- _ => progress (change T with E.t in J)
| |- _ => progress (change T with E.t)
end )
end).
These two tactics take us from Coq's built-in equality
to
E.eq
(and vice versa) when possible.
Ltac Logic_eq_to_E_eq :=
repeat (
match goal with
| H: _ |- _ =>
progress (change (@Logic.eq E.t) with E.eq in H)
| |- _ =>
progress (change (@Logic.eq E.t) with E.eq)
end).
Ltac E_eq_to_Logic_eq :=
repeat (
match goal with
| H: _ |- _ =>
progress (change E.eq with (@Logic.eq E.t) in H)
| |- _ =>
progress (change E.eq with (@Logic.eq E.t))
end).
We are going to write a tactic that works like the
built-in tactic
subst
, but at the level of set element
equality (which may or may not be the convertible with
Coq's equality).
Section RewriteWithEq.
Variables x y z : E.t.
Variables s : t.
Lemma rewr_eq_l :
E.eq x y -> (E.eq x z <-> E.eq y z).
Lemma rewr_eq_r :
E.eq x y -> (E.eq z x <-> E.eq z y).
Lemma rewr_In :
E.eq x y -> (In x s <-> In y s).
End RewriteWithEq.
Ltac substFSetElt x :=
match goal with
| eq1: E.eq x ?y |- _ =>
if prop (E.eq x y) holds by apply E.eq_refl
then fail
else (
repeat (progress (match goal with
| |- context [E.eq x ?z] =>
rewrite -> (rewr_eq_l x y z eq1)
| |- context [E.eq ?z x] =>
rewrite -> (rewr_eq_r x y z eq1)
| |- context [In x ?s] =>
rewrite -> (rewr_In x y s eq1)
| eq2: context [E.eq x ?z] |- _ =>
if prop (E.eq y z) holds by apply E.eq_refl
then fail
else rewrite -> (rewr_eq_l x y z eq1) in eq2
| eq2: context [E.eq ?z x] |- _ =>
rewrite -> (rewr_eq_r x y z eq1) in eq2
| H: context [In x ?s] |- _ =>
rewrite -> (rewr_In x y s eq1) in H
end));
match goal with
| H : context [x] |- _ => clear H
end;
clear x)
| eq1: E.eq ?y x |- _ =>
if prop (E.eq x y) holds by apply E.eq_refl
then fail
else (
apply E.eq_sym in eq1;
repeat (progress (match goal with
| |- context [E.eq x ?z] =>
rewrite -> (rewr_eq_l x y z eq1)
| |- context [E.eq ?z x] =>
rewrite -> (rewr_eq_r x y z eq1)
| |- context [In x ?s] =>
rewrite -> (rewr_In x y s eq1)
| eq2: context [E.eq x ?z] |- _ =>
if prop (E.eq y z) holds by apply E.eq_refl
then fail
else rewrite -> (rewr_eq_l x y z eq1) in eq2
| eq2: context [E.eq ?z x] |- _ =>
rewrite -> (rewr_eq_r x y z eq1) in eq2
| H: context [In x ?s] |- _ =>
rewrite -> (rewr_In x y s eq1) in H
end));
match goal with
| H : context [x] |- _ => clear H
end;
clear x)
end.
Ltac substFSet :=
repeat (progress (
match goal with
| x : E.t |- _ => substFSetElt x
end)).
Considering Decidability of Base Propositions
This tactic adds assertions about the decidability ofE.eq
and In
to the context. This is necessary for
the completeness of the fsetdec
tactic. However, in
order to minimize the cost of proof search, we should be
careful to not add more than we need. Once negations
have been pushed to the leaves of the propositions, we
only need to worry about decidability for those base
propositions that appear in a negated form.
Ltac assert_decidability :=
(** We actually don't want these rules to fire if the
syntactic context in the patterns below is trivially
empty, but we'll just do some clean-up at the
afterward.
Handling Empty
, Subset
, and Equal
This tactic instantiates universally quantified
hypotheses (which arise from the unfolding of Empty
,
Subset
, and Equal
) for each of the set element
expressions that is involved in some membership or
equality fact. Then it throws away those hypotheses,
which should no longer be needed.
Ltac inst_FSet_hypotheses :=
repeat (
match goal with
| H : forall a : E.t, _,
_ : context [ In ?x _ ] |- _ =>
let P := type of (H x) in
assert new P by (exact (H x))
| H : forall a : E.t, _
|- context [ In ?x _ ] =>
let P := type of (H x) in
assert new P by (exact (H x))
| H : forall a : E.t, _,
_ : context [ E.eq ?x _ ] |- _ =>
let P := type of (H x) in
assert new P by (exact (H x))
| H : forall a : E.t, _
|- context [ E.eq ?x _ ] =>
let P := type of (H x) in
assert new P by (exact (H x))
| H : forall a : E.t, _,
_ : context [ E.eq _ ?x ] |- _ =>
let P := type of (H x) in
assert new P by (exact (H x))
| H : forall a : E.t, _
|- context [ E.eq _ ?x ] =>
let P := type of (H x) in
assert new P by (exact (H x))
end);
repeat (
match goal with
| H : forall a : E.t, _ |- _ =>
clear H
end).
Here is the crux of the proof search. Recursion through
intuition
! (This will terminate if I correctly
understand the behavior of intuition
.)
Ltac fsetdec_rec :=
try (match goal with
| H: E.eq ?x ?x -> False |- _ => destruct H
end);
try apply E.eq_refl;
try contradiction;
progress substFSet;
intuition fsetdec_rec.
If we add
unfold Empty, Subset, Equal in *; intros;
to
the beginning of this tactic, it will satisfy the same
specification as the fsetdec
tactic; however, it will
be much slower than necessary without the pre-processing
done by the wrapper tactic fsetdec
.
Ltac fsetdec_body :=
inst_FSet_hypotheses;
autorewrite with set_simpl in *;
push not in * using FSet_decidability;
assert_decidability;
substFSet;
assert (forall x : E.t, E.eq x x) by exact E.eq_refl;
auto;
(intuition fsetdec_rec) ||
fail 1
"because the goal is beyond the scope of this tactic".
End FSetDecideAuxiliary.
Import FSetDecideAuxiliary.
The fsetdec
Tactic
Here is the top-level tactic (the only one intended for
clients of this library). It's specification is given at
the top of the file.
Ltac fsetdec :=
(** We first unfold any occurrences of [iff].
Module FSetDecideTestCases.
Lemma test_eq_trans_1 : forall x y z s,
E.eq x y ->
~ ~ E.eq z y ->
In x s ->
In z s.
Lemma test_eq_trans_2 : forall x y z r s,
In x (singleton y) ->
~ In z r ->
~ ~ In z (add y r) ->
In x s ->
In z s.
Lemma test_eq_neq_trans_1 : forall w x y z s,
E.eq x w ->
~ ~ E.eq x y ->
~ E.eq y z ->
In w s ->
In w (remove z s).
Lemma test_eq_neq_trans_2 : forall w x y z r1 r2 s,
In x (singleton w) ->
~ In x r1 ->
In x (add y r1) ->
In y r2 ->
In y (remove z r2) ->
In w s ->
In w (remove z s).
Lemma test_In_singleton : forall x,
In x (singleton x).
Lemma test_add_In : forall x y s,
In x (add y s) ->
~ E.eq x y ->
In x s.
Lemma test_Subset_add_remove : forall x s,
s [<=] (add x (remove x s)).
Lemma test_eq_disjunction : forall w x y z,
In w (add x (add y (singleton z))) ->
E.eq w x \/ E.eq w y \/ E.eq w z.
Lemma test_not_In_disj : forall x y s1 s2 s3 s4,
~ In x (union s1 (union s2 (union s3 (add y s4)))) ->
~ (In x s1 \/ In x s4 \/ E.eq y x).
Lemma test_not_In_conj : forall x y s1 s2 s3 s4,
~ In x (union s1 (union s2 (union s3 (add y s4)))) ->
~ In x s1 /\ ~ In x s4 /\ ~ E.eq y x.
Lemma test_iff_conj : forall a x s s',
(In a s' <-> E.eq x a \/ In a s) ->
(In a s' <-> In a (add x s)).
Lemma test_set_ops_1 : forall x q r s,
(singleton x) [<=] s ->
Empty (union q r) ->
Empty (inter (diff s q) (diff s r)) ->
~ In x s.
Lemma eq_chain_test : forall x1 x2 x3 x4 s1 s2 s3 s4,
Empty s1 ->
In x2 (add x1 s1) ->
In x3 s2 ->
~ In x3 (remove x2 s2) ->
~ In x4 s3 ->
In x4 (add x3 s3) ->
In x1 s4 ->
Subset (add x4 s4) s4.
Lemma test_too_complex : forall x y z r s,
E.eq x y ->
(In x (singleton y) -> r [<=] s) ->
In z r ->
In z s.
fsetdec
is not intended to solve this directly.
Lemma function_test_1 :
forall (f : t -> t),
forall (g : elt -> elt),
forall (s1 s2 : t),
forall (x1 x2 : elt),
Equal s1 (f s2) ->
E.eq x1 (g (g x2)) ->
In x1 s1 ->
In (g (g x2)) (f s2).
Lemma function_test_2 :
forall (f : t -> t),
forall (g : elt -> elt),
forall (s1 s2 : t),
forall (x1 x2 : elt),
Equal s1 (f s2) ->
E.eq x1 (g x2) ->
In x1 s1 ->
g x2 = g (g x2) ->
In (g (g x2)) (f s2).
fsetdec
is not intended to solve this directly.
Lemma test :
forall (f : t -> t),
forall (s : t),
forall (x y : elt),
In x (add y (f s)) ->
~ E.eq x y ->
In x (f s).
End FSetDecideTestCases.
End Decide.
This page has been generated by coqdoc


Event Location:
Office Floor II, 1700 Sofia, Bulgaria
110 B, Simeonovsko Shosse Bul.
Sofia, , Bulgaria
Abstract:
Cloud computing is already a fact, which nobody doubts. Moreover, with cloud technologies, organizations can focus on their main activities. In the cloud each user has access to the highest quality services. Along with the various positive effects, vendors face a number of problems and undeveloped areas. Preparation of the stakeholders is crucial for each project. More or less the technologies are the same, but the way we use them is not the same in the cloud. Former flaws are today’s advantages, former fundamentals for developers are no longer available in the cloud. Are we ready to forget all that we know and start over again to learn and how sustainable is the new knowledge – these are the open questions that stakeholders raise today.
Speaker(s): Miroslav Lessev,
Abstract:
If you’ve ever worked with SSIS packages there’s no doubt you’ve been in a situation where all of the sudden the package does not behave in the way you'd expect it to and you need to quickly turn around with figuring out the cause and get the package running again. For simple packages, the task might be trivial, but as we work with more and more data and build complex ETLs using SSIS, it is necessary to have a detailed outlook into your package's execution and progress. In this lecture we will go over the different approaches and best practices for logging for SSIS packages. We will also talk about the Integration Services Catalog in SSIS 2012, specifically its capabilities for tracing package execution. Finally we will cover the built-in reports in SSMS 2012.
Speaker(s): Nikolay Nyagolov,
Abstract:
SQL Server Reporting Services provides data-driven subscriptions to render reports based on information in a database table. This is a very nice feature but the down side is that you are required to purchase an Enterprise license (or BI license in SQL 2012) of SQL Server in order to use this feature. Customers like this feature but don't want to pay for the Enterprise license so I searched for an alternative with standard licenses. In this session I will show the alternative where the end user can still create his own subscription in SharePoint. Step-by-step I will create an SQL Server Integration Services package that renders reports to a SharePoint library on values stored in the database.
Speaker(s): David Smeets,
Abstract:
Data Mining is all about data really. But what kind of data do you need? How much data do you need and how to measure data quantity? Finally, how to deal with missing data? Those questions will be answered during this session.
Speaker(s): Marcin Szeliga,
Abstract:
Everybody knows that use of stored procedures offers a number of benefits over issuing T-SQL code directly from an application. In this demo heavy session I am going to explain to you: 1. Why plan caching and reuse is a good thing. 2. How to avoid unnecessary recompilations for plan stability-related reasons. 3. How to avoid unnecessary recompilations for plan optimality-related reasons. 4. When plan reusing is not a good thing and how you can deal with this “Parameter Sniffing” problem. 5. Why you should evade conditional logic inside stored procedures that do data access.
Speaker(s): Marcin Szeliga,
Abstract:
The session is dedicated to Windows Azure Storage - queues, blobs and tables. We'll go through areas of applications, good and bad scenarios, and specifics of working with it.We'll also talk about how it works internally (data partitioning, moving from one partition server to another), and why it should be taken into consideration when implementing software.
Speaker(s): Anton Vidishchev,
Abstract:
The Hadoop ecosystem is a valuable tool for Business Intelligence and Data Visualisation practitioners. It allows you to mashup unstructured data from Hadoop with structured data from more traditional relational and multi-dimensional sources. For Business Intelligence practitioners, this is an excellent tool to gain new business insights, and overcome data silos that come from within the organisation, whilst freeing you to make use of external data sources too. Join us at this session in order to see how your Big Data can empower your business users via familiar Business Intelligence tools such as Excel and Power View.
Speaker(s): Jen Stirrup,
Abstract:
SQL Server performance troubleshooting is one of the most complex things you will have to do around your SQL instances. And it is always difficult to pinpoint the root-cause, especially for professionals which primary role is not a database administrator. This session will provide you the basic concept for performance troubleshooting and what tools you can use so you can quickly head in the right direction and fix the problem.
Speaker(s): Ivan Donev,
Abstract:
This presentation introduces the decision-making ability possible with the free Excel add-ins for PowerPivot and SQL Server Data Mining. The data mining is a service hosted in Microsoft SQL Server Analysis Services 2012, but the Excel add-in exposes the enterprise-strength server technology to analysts and executives. This talk introduces some functions from the "Analyze" and “Data Mining” tabs, including data mining model creation from Excel data. Having seen this presentation some had thought it was all Excel since the functions seem so seamless. The Excel interface provides a familiar way for professionals to make actionable decisions.
Speaker(s): Boriana Petrova,
Abstract:
Description: SQL Server Reporting Services 2012 was released with some core feature redesigns and new functionalities. Come and join me in this sessions where I will cover the setup, report deployment, RS configuration and managing of the RS engine in Sharepoint mode. We will also talk about Data Alerts - the new custom alerting solution of Microsoft that enable you to receive reports as soon as the source data changes
Speaker(s): Ivan Donev,
Abstract:
This session describes how SQL Server internally stores table data. Although you can use SQL without understanding the internals of data storage, a deep knowledge of how data is stored will improve the development of efficient applications. This session explores the basic of metadata that keeps track of data and index storage information.
Speaker(s): Bruno Basto,
Abstract:
In-Memory features is the most perspective trend in the area of high performance. Columnstore Indexes is one of such features, and even with their restrictions, they can accelerate your queries at times! How to get more from this feature? In which situations should we use them? Which internal mechanisms help to achive that? You can get answers on these questions on this session.
Speaker(s): Denis Reznik,
Abstract:
SQL Server 2014 receives a very new important feature - Clustered Columnstore Indexes. Using a xVelocity compression and a batch processing mode this type of indexes which was introduced in SQL Server 2012 is greatly enhanced by making it a Clustered and making it a default recommend solution for the DataWarehouse solutions. Join to discover the Clustered Columnstore Indexes by understanding on which principles they are built and what should you do get the best out of them. This new feature is targeted at the OLAP installations and it is already available for the PDW (Parallel DataWarehouse) v2.
Speaker(s): Niko Neugebauer,
Abstract:
Power BI tools within Excel are available in the cloud with Office 365, allowing customers to access and share BI reports and models across the desktop and web, and all within a managed environment. Power BI for Office 365 includes Power Pivot and Power View, and two new Excel capabilities have been added to allow the over one billion Office 365 users the ability to do more with their data! These two new features are Power Query which was formerly Project Codename “Data Explorer”, and Power Map formerly Project Codename “Geoflow”.
Speaker(s): Mihail Mateev,
Abstract:
So you already know and understand Row Groups, Delta Stores and Compression Methods, but let me show you how Clustered Columnstore Indexes work when locking blocking, when using different compression methods and technics. Let us dive deep into the Dictionaries creation and different methods for the ETL processes.
Speaker(s): Niko Neugebauer,
Abstract:
Have you ever wanted to replay your application workload be that because you upgraded to a new hardware, added new indexes or something else? Now there's a feature for that! It's called Distributed Replay and in this session you will learn how this new feature in SQL Server 2012 can help you resolve that problem!
Speaker(s): Boris Hristov,
Abstract:
We are going to examine a variety of oopsies MANY developers fall prey too - some obvious, some pretty subtle and some down right sneaky! Lots of code examples with the bad AND good code presented. I GUARANTEE that you will find things here that will either prevent you from getting bad data, throwing unwanted errors or vastly improving your database application's performance. I have given this talk over FORTY times now and it is always very highly rated!
Speaker(s): Kevin Boles,
Abstract:
The AlwaysOn Availability Groups feature is a high-availability and disaster-recovery solution that provides an enterprise-level alternative to database mirroring. Introduced in SQL Server 2014 CTP1, AlwaysOn Availability Groups maximizes the availability of a set of user databases for an enterprise. In this session we will talk about what’s coming with Always On, and how does it help to improve high availability and disaster recovery solutions.
Speaker(s): Turgay Sahtiyan,
Abstract:
This talk is about how to deploy a report server project to Windows Azure SQL Reporting report server, and provide initial information for application developers who integrate reports hosted by Windows Azure SQL Reporting in their applications, as well as develop management tools against SQL Reporting report servers.
Speaker(s): Mihail Mateev,
Abstract:
We will talk about how SQL Server produces query plans using estimates and statistics and why are they so important. I will share my experience of managing statistics and show you cases where wrong estimates guessing by optimizer can lead to performance issues. The session will be useful for both administrators and developers.
Speaker(s): Sergey Olontsev,
Abstract:
The fact of the matter is that SQL injection is still a problem at the end of 2013. Web sites are still being hacked by using SQL Injection on a regular basis. Are you ready to learn as to protect your systems?
Speaker(s): Andrey Korshikov,
Abstract:
Some geeky thinks, some tips and tricks, some internals and some little known query processor details. Shortly – come and take a deep dive tour into query optimizer with me! Get inside switch the light!
Speaker(s): Margarita Naumova,
Abstract:
In this session we will walk through the world of Extended Events and their power in monitoring SQL server instances. We will explore some real-world scenarios and see how we can benefit from Xevents in solving them. You will be able to see how to track a specific application behavior and how to troubleshoot connectivity issues
Speaker(s): Miroslav Dimitrov,
Abstract:
SQL Server 2014 introduces memory-optimized database technology for optimizing the performance of OLTP workloads or In-Memory OLTP. In particular, it introduces memory-optimized tables for efficient, contention-free data access, and natively compiled stored procedures for efficient execution of business logic. How fast is the fastest? How cool are the coolest? What are those new technologies coming directly from Microsoft Research into the next version Engine? The session drills down into In_Memory OLTP as the most exciting feature of SQL Server 2014. Of course we will see some other surprises of the new version.
Speaker(s): Margarita Naumova,
Abstract:
We will talk about those tiny blocks which form query plan and I will show you some of them in details. There are plenty of properties each operator have and some of them contain more valuable information than others. Knowing this details can help you better understand query plan and find causes of performance issues.
Speaker(s): Sergey Olontsev,
Abstract:
So what is the real-world difference between regular covering indexes and covering indexes with included columns?
Speaker(s): Oleksii Kovalov,
Abstract:
Are you familiar with SQL Server Dynamic Management Objects (DMOs)? Do you know what kind of data you can collect from them? Are you aware of the standard tools available to analyze data from them? In this session you will learn how to use some of the SQL Server Dynamic Management Objects to collect performance data. The session will have some demos on how to collect and analyze SQL Server Performance information with DMOs. By the end of the session you will know how to collect and analyze SQL Server performance data using data gathered with DMOs.
Speaker(s): Ignacio Salom Rangel,
Abstract:
MS SQL parameter sniffing (or "Bind Variable Peeking" in Oracle) is designed for good. Following some common best practices developers create procedures, analyze actual execution plan, test performance with various sets of data and it is then that they deploy. How about when the same good procedure that used to run less than 100ms starts to timeout...in production? Then you may have become a victim of bad query plan due to parameter sniffing. This may sound as a sci-fi scenario but is rather a real life use case which anyone may encounter. Join this session to get practical ideas of how to identify the cause, avoid typical mistakes and perform a fix.
Speaker(s): Ivelin Andreev,
Abstract:
"Deadlock" is a terrible word, isn't it? Is it as scary as it sounds? Why do they occur and how can they affect an application? Significantly important question is how to solve "Deadlock" issues? The answers to these questions can be found in my session, which is completely dedicated to the fundamental principles of locking and isolation levels.
Speaker(s): Denis Reznik,
Abstract:
The breadth and depth of improvements in TSQL coming out with SQL Server 2012 represent the most significant changes in, well, probably ever! This fast and furious overview will touch on a large range of these goodies, with plenty of sample code for you to take home and review at your leisure!
Speaker(s): Kevin Boles,
This is a list of speakers from the XML Guidebook records. The details and URLs were valid at the time of the event.
LinkedIn: http://bg.linkedin.com/pub/margarita-naumova/9/965/206
Contact: www.maginaumova.com; http://blogs.technet.com/b/magi/
Magi Naumova is SQL Server Architect and Consultant, speaker and trainer, Microsoft Certified Master, MVP Data Platform, MCT, Founder of SQL Master Academy, founder and leader of the Bulgarian SQL User group. She has more than 15 years SQL Server training and consulting experience. Magi is a former member of Microsoft Services Worldwide Technical Leadership Team, а Microsoft Women worth watching http://zd.net/1lwNYKH Currently she speaks, writes, trains and consults people on SQL Server technology. She runs a Data Platform consulting company part of which is SQL Master Academy training program. It helps hundreds of specialists to feel knowledgeable in their daily work or to find an inspirational career path in the world of SQL Server.
LinkedIn: http://pt.linkedin.com/in/webcaravela/
Contact: http://www.nikoport.com
Niko Neugebauer is a Data Platform Consultant. A SQL Server MVP with over 20 years of experience in IT, he is passionate about the Microsoft Data Platform and community. Founder of the Portuguese SQL Server User Group and the main organizer of the first SQLSaturday event outside of North America (#78 Portugal), Niko speaks regularly at events such as PASS Summit, SQLRally, SQLBits, and SQLSaturday events around the world. Niko loves sharing information and knowledge and has authored over 130 blog posts on Columnstore Indexes, and regularly contributes to the open-sourced CISL library focused on Columnstore Indexes.
LinkedIn: http://bg.linkedin.com/pub/margarita-naumova/9/965/206
Contact: www.maginaumova.com; http://blogs.technet.com/b/magi/
Magi Naumova is SQL Server Architect and Consultant, speaker and trainer, Microsoft Certified Master, MVP Data Platform, MCT, Founder of SQL Master Academy, founder and leader of the Bulgarian SQL User group. She has more than 15 years SQL Server training and consulting experience. Magi is a former member of Microsoft Services Worldwide Technical Leadership Team, а Microsoft Women worth watching http://zd.net/1lwNYKH Currently she speaks, writes, trains and consults people on SQL Server technology. She runs a Data Platform consulting company part of which is SQL Master Academy training program. It helps hundreds of specialists to feel knowledgeable in their daily work or to find an inspirational career path in the world of SQL Server.
LinkedIn: http://pt.linkedin.com/in/webcaravela/
Contact: http://www.nikoport.com
Niko Neugebauer is a Data Platform Consultant. A SQL Server MVP with over 20 years of experience in IT, he is passionate about the Microsoft Data Platform and community. Founder of the Portuguese SQL Server User Group and the main organizer of the first SQLSaturday event outside of North America (#78 Portugal), Niko speaks regularly at events such as PASS Summit, SQLRally, SQLBits, and SQLSaturday events around the world. Niko loves sharing information and knowledge and has authored over 130 blog posts on Columnstore Indexes, and regularly contributes to the open-sourced CISL library focused on Columnstore Indexes.
LinkedIn: http://linkedin.com/in/sergeyolontsev
Contact: http://SergeyOlontsev.com/
I have been working with SQL Server since SQL Server 2000 version as a database administrator, developer, consultant and trainer, focusing on high availability and disaster recovery solutions, ETL, troubleshooting and performance tuning, developing high performance solutions . I'm a regular speaker at SQL Server user group meetings, SQLSaturday events and other conferences. An owner of MCM certification and MVP award on SQL Server.
LinkedIn: https://bg.linkedin.com/pub/miroslav-lessev/62/238/34
I am a PhD candidate at Faculty of Economics and Business Administration, University of Sofia quot;St. Kliment Ohridskiquot; in Implementation of modern computer engineering in economic studies at. I have study on cloud computing and its effect on economics and people. I have more than 20 years of experience in designing, developing, implementing and supporting databases. At the moment I#39;m a Big Data Developer in DataCore Software.
LinkedIn: http://www.linkedin.com/pub/denis-reznik/3/502/234
Contact: http://reznik.uneta.com.ua
Denis Reznik is a Data Architect at Intapp, Inc. He has more than ten years experience in software development, database design, and performance tuning for cloud and on-premises solutions. In 2010 Denis became Microsoft Data Platform MVP and maintains MVP status today. Apart from his professional career, Denis actively participates in the development of the Ukrainian Data Community.
LinkedIn: http://linkedin.com/in/sergeyolontsev
Contact: http://SergeyOlontsev.com/
I have been working with SQL Server since SQL Server 2000 version as a database administrator, developer, consultant and trainer, focusing on high availability and disaster recovery solutions, ETL, troubleshooting and performance tuning, developing high performance solutions . I'm a regular speaker at SQL Server user group meetings, SQLSaturday events and other conferences. An owner of MCM certification and MVP award on SQL Server.
LinkedIn: https://bg.linkedin.com/in/ivelin
Contact: https://www.slideshare.net/ivoandreev
Ivelin is a Microsoft Azure MVP and software architect in one of the leading and highly innovative Bulgarian IT brands - Interconsult Bulgaria Ltd. He is an external ICT expert in the European Commission, Eurostars-Eureka programme and Innovation Fund Denmark, Microsoft professional developer, senior project manager and Data Platform specialist. With 17+ years of strong experience in design and development of web systems, SOA, enterprise integration, machine learning, web security and data management, he is a practical man who always tries to balance between risk and flexibility. Never scared of work he has turned the weighing of pros and cons into own marked style that urges to make conscious decisions.
LinkedIn: http://www.linkedin.com/pub/denis-reznik/3/502/234
Contact: http://reznik.uneta.com.ua
Denis Reznik is a Data Architect at Intapp, Inc. He has more than ten years experience in software development, database design, and performance tuning for cloud and on-premises solutions. In 2010 Denis became Microsoft Data Platform MVP and maintains MVP status today. Apart from his professional career, Denis actively participates in the development of the Ukrainian Data Community.
Contact: http://www.jenstirrup.com
Jen is a database strategist, small business owner, SQLFamily and community advocate, public speaker and blogger. Jen was elected Director-At-Large (elect) for the Professional Association of SQL Server, responsible for the EMEA regions plus the Virtual Chapter portfolio. Jen is passionate about all things data and business intelligence, helping leaders derive value from their Microsoft SQL Server, SharePoint and Office365 investments.
LinkedIn: http://www.linkedin.com/in/thesqlguru
Kevin Boles is a SQL Server expert, working exclusively with the product since v6.5. With over 25 years of database experience and over 45,000 man hours of SQL Server engine experience, he holds many related certifications, is an MCT and was a SQL Server MVP from 2007 to 2012. Kevin has been a very successful independent consultant for over 20 years. His passion is the relational engine, especially designing, building, analyzing and tuning high-performance database applications.
LinkedIn: https://www.linkedin.com/in/borianapetrova/
Contact: http://itraining.bg/category/itraining-blog/
Microsoft Certified Trainer with over 10 years experience as an IT instructor and Consultant. She has many qualifications and professional certifications, including: Excel MVP, MCT, MCITP, MCTS, MOS Master. In 2008 she is among the TOP 25 of the best instructors in Microsoft World Company business evaluation and measurement - Knowledge Advisors.
LinkedIn: http://www.linkedin.com/in/thesqlguru
Kevin Boles is a SQL Server expert, working exclusively with the product since v6.5. With over 25 years of database experience and over 45,000 man hours of SQL Server engine experience, he holds many related certifications, is an MCT and was a SQL Server MVP from 2007 to 2012. Kevin has been a very successful independent consultant for over 20 years. His passion is the relational engine, especially designing, building, analyzing and tuning high-performance database applications.
LinkedIn: https://www.linkedin.com/in/ignaciosalomrangel
Contact: http://ignaciosalom.com/
Ignacio Salom is a Senior SQL Server DBA and the CEO of Cenlinea Online Education He has over 15 years of experience in IT and in 2006 he turned his focus to SQL Server. Ignacio holds MCITP Database Administrator certifications for SQL Server 2005 and SQL Server 2008. His online presence includes: - Writing for Confio Software’s LogicalRead - His blog - The SQL Server Central forums - MSDN forums - Linkedin - Twitter(@iasalom)
Contact: http://smeetsd.wordpress.com/
David Smeets has been active as A BI professional for 10 years now. Currently he is working as a SharePoint BI Consultant at CTG Belgium where he has completed several SharePoint BI projects and assisted clients in improving their BI environment. In 2012 he was a speaker for the Belgium BIWUG and active as a speaker for Sharepoint Europe. In 2012 he also won the Belgium Microsoft contest: So you think you can demo (BI track) with a HealthCare BI solution.
Работать с SQL Server начал в 2003 году. Довелось работать и сдавать сертификационные экзамены по версиям SQL Server от 2000 до 2012. Участник конференций SQLSaturday, Платформа, DevCon и TechEd. География выступлений от Тампы до Красноярска, от Санкт-Петербурга до Тбилиси. Основатель сообществ Krasnodar SQLamp;BI Usergroup и Global Russian Virtual Chapter. На данный момент являюсь PASS Regional Mentor for Central Eastern Europe.
LinkedIn: https://pl.linkedin.com/in/marcinszeliga
Data Philosopher. Since 2006 invariably awarded Microsoft Most Valuable Professional title in the Data Platform category. A speaker at numerous conferences across Europe, as well as at user groups meetings. The author of many books and articles devoted to Microsoft Data Platform. An independent consultant, database-centric application practitioner and architect totally focused on SQL Server and Azure. Huge fan of Data Science and Machine Learning.
Contact: http://cloudytimes.azurewebsites.net
Anton is a Windows Azure MVP, and one of the active speakers participating at many conferences in Ukraine and Russia. One of the leaders of Odessa .NET community. Team Leader at RR Donnelley. Author of http://cloudytimes.azurewebsites.net.
LinkedIn: http://tr.linkedin.com/pub/turgay-sahtiyan/15/b46/682
Contact: http://www.turgaysahtiyan.com/
Turgay Sahtiyan has been working in IT industry over a decade and he currently works as a PMC (Premier Mission Critical) Solution Engineer at Microsoft.He is based in Turkey and primarily giving proactive and reactive services with solution based approach to top enterprise customer in the MEA region.Before joined to Microsoft, he was one of the SQL Server MVP in Turkey,in addition he is founder and former president of SQLPass Turkey Chapter.(Detailed BIO http://www.turgaysahtiyan.com/about.aspx)
Nikolay Georgiev Nyagolov is a Senior Business Intelligence Developer at MentorMate Bulgaria. He has 7 years experience in Databases, in particular MS SQL Server and works as a BI for more than 4 years. He is also specialized in the development of SSIS packages and integrated BI solutions.
Bruno Basto, senior consultant #160;and senior trainer #160;at Rumos. SQL certified since 6.5 version (1998). Work with MSFT tools and infrastructure since 1992 in the financial, banking and insurance areas. Responsible for several training projects for software solutions with MSFT infrastructure. Speaker at several MSFT and SQLPass events.
LinkedIn: https://bg.linkedin.com/in/dimitrovmiroslav
Contact: http://www.sqlshack.com/author/miroslav-dimitrov/
Miroslav Dimitrov is a Senior Big Data and Analytics Engineer at DXC Technology, regular speaker at various events and Microsoft Certified Trainer. He is MCSE: Data Platform for SQL Server and MCITP on SQL 2008. In the last years he had worked on great variety of customers' environments and involved in complex transitions and transformation projects as well as developing private and public cloud solutions. Miroslav is also leading database courses at Sofia University.
LinkedIn: https://www.linkedin.com/in/ivandonev/
I am a Data platform MVP with more than 10 years of real-life experience with SQL Server and its stack of services. Besides the support and project work, I am also a trainer, conference speaker and user group organizer (and volunteer).
LinkedIn: http://www.linkedin.com/pub/mihail-mateev/1/6b3/4b1
Contact: https://mmateev.wordpress.com/
Mihail Mateev is a technical consultant, community enthusiast, PASS Regional Mentor for CEE, chapter lead, Microsoft Azure MVP, Microsoft Regional Director. He works as a Senior Solutions Architect at EPAM Systems, focused on Data Platform, IoT and cloud related solutions. He also worked many years like a Technical evangelist in the Infragistics. Last years Mihail was focused on various areas related to technology Microsoft: Data Platform, Visual Studio, ASP.Net, Windows client apps, Data Platform, and Microsoft Azure. Michael also has a PhD in cloud computing area. He is a university lecturer on Smart Homes and Smart Energy IoT Solutions.
LinkedIn: https://pl.linkedin.com/in/marcinszeliga
Data Philosopher. Since 2006 invariably awarded Microsoft Most Valuable Professional title in the Data Platform category. A speaker at numerous conferences across Europe, as well as at user groups meetings. The author of many books and articles devoted to Microsoft Data Platform. An independent consultant, database-centric application practitioner and architect totally focused on SQL Server and Azure. Huge fan of Data Science and Machine Learning.
LinkedIn: http://bg.linkedin.com/in/borishristov
Contact: http://borishristov.com/blog/
Boris is a SQL Server Consultant, but also an Author for Pluralsight and a SQL Server MVP. He is frequently speaking at conferences all accross Europe and is heavily involved in training students and organizations in what he calls quot;The Art of SQL Serverquot;. Boris is frequently blogging and is the host of SQLHangouts.
DBA and DB developer with more than 10 year expirience. SQLSat/SSUG speaker. MCTS, MCITP. Author of pet-projects ExpressProfiler and SQL Code Guard
LinkedIn: https://www.linkedin.com/in/ivandonev/
I am a Data platform MVP with more than 10 years of real-life experience with SQL Server and its stack of services. Besides the support and project work, I am also a trainer, conference speaker and user group organizer (and volunteer).
LinkedIn: http://www.linkedin.com/pub/mihail-mateev/1/6b3/4b1
Contact: https://mmateev.wordpress.com/
Mihail Mateev is a technical consultant, community enthusiast, PASS Regional Mentor for CEE, chapter lead, Microsoft Azure MVP, Microsoft Regional Director. He works as a Senior Solutions Architect at EPAM Systems, focused on Data Platform, IoT and cloud related solutions. He also worked many years like a Technical evangelist in the Infragistics. Last years Mihail was focused on various areas related to technology Microsoft: Data Platform, Visual Studio, ASP.Net, Windows client apps, Data Platform, and Microsoft Azure. Michael also has a PhD in cloud computing area. He is a university lecturer on Smart Homes and Smart Energy IoT Solutions.
The following is a list of sponsors that helped fund the event.


---
layout: default
---
Class objectives:
- How to apply instructional design models to develop online learning experiences
- How to collaborate with a subject matter expert
- How to create a design document to guide the online course development process
Assignments
After reading about the classic ADDIE model, we were asked to visually map out what the model and its components mean to us.
For this assignment, we were asked to create a brief podcast explaining the stages of the Dick and Carey model.
This exercise helped us think more about desired results and evidence before developing learning materials.
This assignment acknowledged the fast-paced world a lot of designers work in.
This exercise helped prepare us for the signature assignment by distinguishing between then developing educational goals and objectives.
We were asked to put together a presentation proposing the creation of a new instructional model to various stakeholders. This video is accompanied by supporting documentation that explains the need for the module, objectives, and more.


The Ninth Gate ***
Rated on a 4-star scale Screening venue: Odeon (Bromborough) Released in the UK by UIP on June 2, 2000; certificate 15; 133 minutes; countries of origin France/Spain/USA; aspect ratio 2.35:1
Directed by Roman Polanski; produced by Mark Allan, Antonio Cardenal, Inaki Nunez, Roman Polanski, Alain Vannier. Written by John Brownjohn, Roman Polanski, Enrique Urbizu; based on the novel "El Club Dumas" by Aturo Pérez-Reverte. Photographed by Darius Kondjhi; edited by Hervé de Luze.
CAST..... Johnny Depp..... Dean Corso Emmanuelle Seigner..... The Girl Frank Langella..... Boris Balkan Lena Olin..... Liana Telfer Barbara Jefford..... Baroness Kessler Jack Taylor..... Victor Fargas James Russo..... Bernie
Chandeliers are grand, ornate and thoroughly ridiculous, and sometimes fall down on people. Roman Polanski's "The Ninth Gate" is like that -- a supernatural thriller and detective movie that begins by playing tricks with its genre and ends up playing one on the audience. It deliberately leaves us unsatisfied, but is silly and goofy and a whole lot of fun.
Johnny Depp stars as Dean Corso, a rare book dealer hired by a strange collector (Frank Langella) to track down a book entitled "The Nine Gates of the Kingdom of Shadows". Legend has it that its illustrations, when used in satanic ritual, can summon up Lucifer himself. Corso, in trying to find it, runs into one strange person after another, and we are reminded of such films as "The Big Sleep" and "Angel Heart", although "The Ninth Gate" is goofier, and the structure and details of the plot make it extremely predictable.
Until, that is, the last act, when the fire-and-brimstone conclusion we've been expecting doesn't happen, and there is a confusing final shot that leaves us wondering whether Corso has lost power over his soul, sold it, or gone to battle.
Polanski, the director, is manipulating us. He knows how to make a serious detective movie ("Chinatown"), tale of witchcraft ("Macbeth"), or movie about the Devil ("Rosemary's Baby") -- but he's decided to forget about that and have a little fun. The early scenes involve us with a subtle, odd sense of humour: they undermine the seriousness of the plot by focusing on ridiculous images like a light fixture a guy hung himself on; and by letting Depp skulk through the movie with an eyebrow raised, as he did in "Sleepy Hollow". Then the anti-climactic nature of the ending reveals that Polanski's chuckles extend to us, because he's toying with us just as surely as he is with the film noir genre. Odd, but not uninteresting.
COPYRIGHT(c) 2000 Ian Waldron-Mantgani Please visit, and encourage others to visit, the UK Critic's website at http://members.aol.com/ukcritic
The review above was posted to the
rec.arts.movies.reviews newsgroup (de.rec.film.kritiken for German reviews).
The Internet Movie Database accepts no responsibility for the contents of the
review and has no editorial control. Unless stated otherwise, the copyright
belongs to the author.
Please direct comments/criticisms of the review to relevant newsgroups.
Broken URLs inthe reviews are the responsibility of the author.
The formatting of the review is likely to differ from the original due
to ASCII to HTML conversion.
Related links: index of all rec.arts.movies.reviews reviews


Dave Burton
http://ioccc.snox.net
make
./prog < any-file
./prog < prog
./prog < prog.c
One line, one array, one loop and one statement but it prints many bytes. It won.
Feed this anything on stdin.
The included script may be used as a driver program for this entry. It adds several nice-to-have features, and allows salt-to-taste customizability.
This code has been compiled and tested on:
This started life as a personal challenge: write the shortest hex dump utility in C.
The self-imposed ground rules in the hunt for shortest: the code has to output correctly, no extraneous newlines, the code must be portable, and without bypassing the solution using execve(2), or functions built upon it (system(3), popen(3), etc). E.g:
main(){system("hd");} // it's turtles all the way down!
is not acceptable. And, “output correctly” is the output format of this entry. QED.
Early attempts ended up at a reasonably short 157 characters. This was too long for a one-liner, so it had to be formatted as something more interesting. This solution is pleasing, but a true one-liner was the hoped-for goal. Here is the 157 character version in it’s entirety:
char O,o[ 20];L(O){
putchar ( O+ 48+39 *(9<
O));} I(O) {L(~ 15);
O|| puts(o);} main (l){
for(;~(l=getchar()) ;I(O
&=15 ))o[ O++ ]=4<
(4^l >>5) ?l: 46,L
(l>> 4),L (l&15);O&&
I(o[ O]=0 );}//157c
While thinking about this in the shower (you are not the only one that does this!) came the idea which reduced the code to just 119 chars. This dramatic reduction started to feel close to minimal, and the hunt resumed. The progression to the present size is interesting, and it is interesting that the same algorithm can be expressed so differently by slight rearrangement of its parts.
// 119
char O,o[20];main(l){for(;~(l=getchar());O||puts(o))o[O++]=isprint(l)?l:46,O&=15,printf("%02x ",l);O[o]=0;O&&puts(o);}
// 116
char O,o[20];main(l){for(;O++[o]=~(l=getchar())?4<(4^l>>5)?l:46:0;(O&=15)||puts(o))printf("%02x ",l);O>1&&puts(o);}
// 115
char O,o[20];main(l){for(;O[o]=~(l=getchar())?4<(4^l>>5)?l:46:0;(O=-~O&15)||puts(o))printf("%02x ",l);O&&puts(o);}
// 113
char O,o[20];main(l){for(;~l;(O=~l?printf("%02x ",l),-~O&15:!O)||puts(o))O[o]=~(l=getchar())?4<(4^l>>5)?l:46:0;}
// 112
char O,o[20];main(l){for(;~l;(O=~l?-~O&printf("%02x ",l)*5:!O)||puts(o))O[o]=~(l=getchar())?4<(4^l>>5)?l:46:0;}
// 111
char O,o[20];main(l){for(;~l;O||puts(o))O=(O[o]=~(l=getchar())?4<(4^l>>5)?l:46:0)?-~O&printf("%02x ",l)*5:!O;}
// 110
char O,o[0];main(l){for(;~l;O||puts(o))O=(O[o]=~(l=getchar())?4<(4^l>>5)?l:46:0)?-~O&printf("%02x ",l)*5:!O;}
// 109
char O,o[];main(l){for(;~l;O||puts(o))O=(O[o]=~(l=getchar())?4<(4^l>>5)?l:46:0)?-~O&printf("%02x ",l)*5:!O;}
There are solutions without the ASCII sidebar that are significantly shorter. These do not compete in the same category, since their output is materially different. They are derived from the solutions above, but are still fascinating as concise utilities, so here is their progression, for the curious:
// 102
I;O(O){putchar(O+48+39*(9<O));}main(l){for(;~(l=getchar());O(++I&15?~15:~37))O(l>>4),O(l&15);O(-38);}
// 80
O;main(l){while(~(l=getchar()))printf("%02x%c",l,++O&15?32:10);O&15&&puts("");}
// 78
O;main(l){for(;~l;(O=~(l=getchar())?printf("%02x ",l),-~O&15:!O)||puts(""));}
// 77
O;main(l){for(;~l;(O=~(l=getchar())?-~O&printf("%02x ",l)*5:!O)||puts(""));}
// 76
O;main(l){for(;~l;O||puts(&O))O=~(l=getchar())?-~O&printf("%02x ",l)*5:!O;}
It is possible to reduce the size of each of these by one by eliding the trailing newline. This was not reported above since the newline kept getting appended by processing software, and it is more interesting to remove characters by changing code than by filtering:
$ tr -d '\012' < 109.c | wc -c
108
$ tr -d '\012' < 76.c | wc -c
75
$ tr -d '\012' < 109.c | cc -o 108 -xc -
$ verify 108
$
An obfuscated hex dump has been done before: 1986/bright/bright.c is similar in function, but it uses more characters in just setting up its obfuscation than this entire solution!
If you are unhappy with the way DEL (character 127) is handled,
replace the cryptic expression 4<(4^l>>5)?l:46
with 32>l|l>126?46:l
.
Both take the same number of characters, but the former is a bit more interesting.
Bonus question: how does the first expression work?
Technically, char o[0];
is illegal (SS <IP_ADDRESS>) according to ISO (N1570).
And char o[];
is a conditionally supported feature (SS <IP_ADDRESS>, <IP_ADDRESS>).
However, it works in modern C implementations as an extension,
including GCC, Clang and TCC, for X86 and ARM,
on multiple operating systems (Linux, OSX, FreeBSD), so it is functionally correct.
MicroSoft Visual C++ does not allow char o[]
or char o[0]
,
and implements its close relative char o[1]
such that writing more than a single char will cause a fault, which is technically correct.
But how does this work at all, even as an extension?
o[]
allocates one(!) byte in a zero-filled data area (formerly BSS).
The UNIX-derived systems this code was run upon all place the
storage of O
and o
into a zero-filled VM page with nothing following:
thus, there are plenty of available and unused zero bytes following O
, addressed via o
,
and this code only needs 17.
This is undefined behavior, but as shown, it is widely available.
The 1979 Seventh Edition UNIX (v7) system pre-dates the IOCCC by several years,
and the source code to sh
(1) was a significant inspiration for this contest.
There are two C compilers present: cc
written by Dennis Ritchie, and pcc
written by Steven Johnson.
The nested conditional expressions in 116 and smaller are too complex for cc
(“Illegal conditional”)
but pcc
handles them correctly, and neither compiler accepts char o[]
or char o[0]
nor puts the bytes in
a zero-filled page (as a paged VM was not yet written for UNIX).
More significant is that v7 printf
(3) does not report the number of characters written,
and therefore 111 compiles but does not work correctly;
113 is the shortest code that compiles and runs correctly in Ancient UNIX.
Interesting digression: v7
printf
(_doprnt
) was written in PDP-11 assembler. It pre-datesvarargs.h
, and assembly was the only way to gain access to the variable argument types. The first edition The C Programming Language, 1978, page 71, remarks:By the way, there is no entirely satisfactory way to write a portable function that accepts a variable number of arguments, because there is no portable way for the called function to determine how many arguments where actually passed to it in a given call. …
printf
, the most common C function with a variable number of arguments, … is also non-portable and must be modified for different environments.It is fascinating to explore the roots of C through the history of the operating system it was birthed within. C is often criticized as a difficult, inscrutable language, but as this contest demonstrates, this is in parody. Shell-gol is one of those instances where someone preferred a different language, and (ab)used the preprocessor to re-mold C into something they found comfortable. Most of the rest of the system, especially in the kernel, are models of clarity and efficient expression.
So which version is the shortest, portable hex dump?
Clearly, the smallest possible program violates modern best practice. It is not even possible to compile cleanly, but it will compile correctly.
Included is prog.nowarn.c
, a modern C implementation that is – perhaps – the smallest,
clean-compiling version using clang
or gcc
with -Wall -pedantic
.
Note that while this is larger than all but the original attempt,
it will not work with the original Ritchie PDP-11 C compiler,
since the expression within the ternary remains too complex.
Try
cat prog.c prog.nowarn.c
to compare the differences (diff
is not helpful on a one-liner).
© Copyright 1984-2018,
Leo Broukhis, Simon Cooper, Landon Curt Noll
- All rights reserved |


19:00- Pre-conference sauna and social hanging around @ Restaurant Villi Wäinö. There will be a sauna with towels provided by the house. Map. The second floor is booked for pythonistas.
8:30 Registration Opens
9:00 - 9:30 Welcome and quick introduction of all talks
9:30 - 10:00 Pragmatic Testing
10:00 - 10:30 Coffee / mingling
10:30 - 11:30 Keynote: Solid data structures in Python with logs
11:30 - 12:30 [Track 1] How to become enterprise-friendly with free software [Track 2] Building a marketplace (30 min) [Track 2] Weaving a Search Engine around User's Workflow (30 min)
12:30 - 13:30 Lunch (om nom)
13:30 - 14:30 [Track 1] Hunting Malware with Python [Track 2] Introducing the Asphalt framework
14:30 - 15:30 [Track 1] Welcome to async/await era [Track 2] Plug in with Python
15:30 - 16:00 Coffee / mingling
16:00 - 17:00 [Track 1] Bug forecasting by visualizing code evolution [Track 2] Nix for Python developers
17:00 - 18:00 Lightning talks
18:xx - 18:30 Stroll to dinner venue
18:30 - Late at night Dinner at restaurant Dylan Milk (Porkkalankatu 5).


A CSS/Sass style for simple HTML documents. It has mainly been tested on Org-mode exports. Contributions welcome.
Except for a few classes specific to Org-mode exports, elements are styled directly. It uses the Solarized colour scheme, and includes both light and dark versions. There are some media queries. Google Fonts is used, but you might prefer to provide your own - the files are included for convenience.
You can include generic-css.js
to insert theme-selecting buttons at the
top of the page (as seen on the styled README page). It expects your stylesheet
links to have IDs generic-css-dark
and generic-css-light
, as in the below snippet:
<link id="generic-css-dark" rel="stylesheet" type="text/css" href="https://mattduck.github.io/generic-css/css/generic-dark.min.css"/>
<link id="generic-css-light" rel="stylesheet" type="text/css" href="https://mattduck.github.io/generic-css/css/generic-light.min.css"/>
<script type="text/javascript" src="https://mattduck.github.io/generic-css/js/generic-css.min.js"></script>
To try without downloading, use (light):
<link href="https://mattduck.github.io/generic-css/css/generic-light.min.css" rel="stylesheet" type="text/css"/>
or (dark):
<link href="https://mattduck.github.io/generic-css/css/generic-dark.min.css" rel="stylesheet" type="text/css"/>
Run build.sh
to compile the Sass files to ./css
, compress the Javascript and
export README.md
to index.html
:
cd $repository_root
./build.sh
This requires:
sass
kramdown
uglifyjs
.html
and .org
files.


one (
0
)
two (
0
)
Question:
Loading ...
Thema:
Loading ...
Time (in sec.):
0
A) Loading ...
B) Loading ...
C) Loading ...
D) Loading ...
three (
0
)
four (
0
)


The DisplayEntity is the basic 3D graphical object in JaamSim. All JaamSim objects that have graphics are subclasses of DisplayEntity.
All objects intended for visualization in a model display window in JaamSim have a set of basic graphics keywords used to define their appearance. These are found in the Graphics tab of the Input Editor when the object is selected. For polyline type objects the inputs for Position, Alignment, Size, and Orientation are replaced by those for Points and CurveType.
DisplayEntity Inputs
|
Keyword |
Description |
|
Normal Objects |
|
|
Position |
The location of the object in {x, y, z} coordinates. |
|
Alignment |
The point within the object that is located at the coordinates of its Position input. Expressed with respect to a unit box centered about { 0 0 0 }. |
|
Size |
The size of the object in {x, y, z} coordinates. If only the x- and y-dimensions are given then the z-dimension is assumed to be zero. |
|
Orientation |
Euler angles defining the rotation of the object. |
|
Polyline Type Objects |
|
|
Points |
A list of points in {x, y, z} coordinates that define a polyline. When only two coordinates are given it is assumed that z = 0. |
|
CurveType |
The type of curve interpolation used for line type entities. |
|
All Objects |
|
|
Region |
If a Region is specified, the Position and Orientation inputs for the present object are relative to the Position and Orientation of the specified Region. If the specified Region is moved or rotated, the present object is moved to maintain its relative position and orientation. |
|
RelativeEntity |
If an object is specified, the Position input for the present object is relative to the Position for the specified object. If the specified object is moved, the present object is moved to maintain its relative position. |
|
DisplayModel |
The graphic representation of the object. If a list of DisplayModels is entered, each one is displayed provided that its DrawRange input is satisfied. This feature allows the object's appearance to change with its distance from the View window's camera. |
|
Show |
If TRUE, the object is shown in the View windows. |
|
Movable |
If TRUE, the object will respond to mouse clicks and can be positioned by dragging with the mouse. |
|
VisibleViews |
The view windows on which this entity will be visible. |
|
DrawRange |
The minimum and maximum distance from the camera for which this entity is displayed. |
DisplayEntity Outputs
|
Output Name |
Description |
|
Name |
The unique input name for this entity. |
|
ObjectType |
The class of objects that this entity belongs to. |
|
SimTime |
The present simulation time. |
|
Parent |
The parent entity for this entity. |
|
User-defined attributes and custom outputs |
The present values for each of the attributes and custom outputs that were defined for the DisplayEntity. |
|
Position |
The present {x, y, z} coordinates of the DisplayEntity in its Region. |
|
Size |
The present {x, y, z} components of the DisplayEntity's size. |
|
Orientation |
The present {x, y, z} Euler angles of the DisplayEntity's rotation. |
|
Alignment |
The present {x, y, z} coordinates of a point on the DisplayEntity that aligns direction with the position output. Each component should be in the range [-0.5, 0.5]. |
|
GraphicalLength |
Polyline type objects: the length of the polyline determined by its Points and CurveType inputs. Non-polyline type objects: the largest of the Size inputs. |
|
ObserverList |
The observers that are monitoring the state of this entity. |
|
NextList |
The entities that are immediately downstream from this entity. |
|
PreviousList |
The entities that are immediately upstream from this entity. |


{% extends "layouts/layout.html" %} {% block header %}
Upload an image and the algorithm will tell you what it is!


文言, or
wenyan, is an esoteric programming language that closely follows the grammar and tone of classical Chinese literature. Moreover, the alphabet of
wenyan contains only traditional Chinese characters and
「」
quotes, so it is guaranteed to be readable by ancient Chinese people. You too can try it out on the
online editor,
download a compiler, or view the
source code.
Syntax
Syntax of
wenyan is just like that of its namesake, classical Chinese:
天地，好在否！/ HELLO WORLD ▶
The code above is editable, go ahead customize the greeting and hit ▶! Another slightly more sophisticated example, using the sieve of Erathosthenes to find prime numbers:
埃氏筛 / SIEVE OF ERATOSTHENES ▶
You can find many more examples such as a Universal Turing Machine, a Mandelbrot set plotter, a Tower of Hanoi solver, and so on on the
online IDE.
Compilation
wenyan currently compiles to JavaScript, Python, or Ruby, and will support more languages (e.g. C) in the future. The Hello World example (or whatever you edited it to be) above translates to:
Get
WIKI
GITHUB
ONLINE EDITOR
LANGUAGE SPEC
REFERENCE


---
title: Sunglasses
year: 2013
description: Stained pine, brass hardware, floral cardstock.
---
{% include resimg.html src="sunglasses/closed.jpg" class="with-viewer" %}
{% include resimg.html src="sunglasses/from-behind.jpg" class="with-viewer" %}
{% include resimg.html src="sunglasses/half-open.jpg" class="with-viewer" %}
{% include resimg.html src="sunglasses/table.jpg" class="with-viewer" %}


@GuardedBy
annotations on instance fields or methods
in which the guard is a static
field. Guarding a non-static by a static may result in excessive lock contention,
as access to each locked field in any object instance will prevent simultaneous access to that field in every object instance.
Example:
private static ReadWriteLock lock = new ReentrantReadWriteLock(); //static guarding field
private Object state;
@GuardedBy("lock")
public void bar() {
state = new Object();
}
Supported @GuardedBy
annotations are:
net.jcip.annotations.GuardedBy
javax.annotation.concurrent.GuardedBy
org.apache.http.annotation.GuardedBy
com.android.annotations.concurrency.GuardedBy
androidx.annotation.GuardedBy
com.google.errorprone.annotations.concurrent.GuardedBy


Haystack comes with some default, simple views & forms to help you get started and to cover the common cases. Included is a way to provide:
- Basic, query-only search.
- Search by models.
- Search with basic highlighted results.
- Faceted search.
- Search by models with basic highlighted results.
Most processing is done by the forms provided by Haystack via the search method. As a result, all but the faceted types (see Faceting) use the standard SearchView.
There is very little coupling between the forms & the views (other than relying on the existence of a search method on the form), so you may interchangeably use forms and/or views anywhere within your own code.
The most basic of the form types, this form consists of a single field, the q field (for query). Upon searching, the form will take the cleaned contents of the q field and perform an auto_query on either the custom SearchQuerySet you provide or off a default SearchQuerySet.
To customize the SearchQuerySet the form will use, pass it a searchqueryset parameter to the constructor with the SearchQuerySet you’d like to use. If using this form in conjunction with a SearchView, the form will receive whatever SearchQuerySet you provide to the view with no additional work needed.
The SearchForm also accepts a load_all parameter (True or False), which determines how the database is queried when iterating through the results. This also is received automatically from the SearchView.
All other forms in Haystack inherit (either directly or indirectly) from this form.
Identical to the SearchForm except that it tags the highlight method on to the end of the SearchQuerySet to enable highlighted results.
This form adds new fields to form. It iterates through all registered models for the current SearchSite and provides a checkbox for each one. If no models are selected, all types will show up in the results.
Identical to the ModelSearchForm except that it tags the highlight method on to the end of the SearchQuerySet to enable highlighted results on the selected models.
Identical to the SearchForm except that it adds a hidden selected_facets field onto the form, allowing the form to narrow the results based on the facets chosen by the user.
The simplest way to go about creating your own form is to inherit from SearchForm (or the desired parent) and extend the search method. By doing this, you save yourself most of the work of handling data correctly and stay API compatible with the SearchView.
For example, let’s say you’re providing search with a user-selectable date range associated with it. You might create a form that looked as follows:
from django import forms
from haystack.forms import SearchForm
class DateRangeSearchForm(SearchForm):
start_date = forms.DateField(required=False)
end_date = forms.DateField(required=False)
def search(self):
# First, store the SearchQuerySet received from other processing.
sqs = super(DateRangeSearchForm, self).search()
# Check to see if a start_date was chosen.
if self.cleaned_data['start_date']:
sqs = sqs.filter(pub_date__gte=self.cleaned_data['start_date'])
# Check to see if an end_date was chosen.
if self.cleaned_data['end_date']:
sqs = sqs.filter(pub_date__lte=self.cleaned_data['end_date'])
return sqs
This form adds two new fields for (optionally) choosing the start and end dates. Within the search method, we grab the results from the parent form’s processing. Then, if a user has selected a start and/or end date, we apply that filtering. Finally, we simply return the SearchQuerySet.
Haystack comes bundled with three views, the class-based views (SearchView & FacetedSearchView) and a traditional functional view (basic_search).
The class-based views provide for easy extension should you need to alter the way a view works. Except in the case of faceting (again, see Faceting), the SearchView works interchangeably with all other forms provided by Haystack.
The functional view provides an example of how Haystack can be used in more traditional settings or as an example of how to write a more complex custom view. It is also thread-safe.
The SearchView is designed to be easy/flexible enough to override common changes as well as being internally abstracted so that only altering a specific portion of the code should be easy to do.
Without touching any of the internals of the SearchView, you can modify which template is used, which form class should be instantiated to search with, what SearchQuerySet to use in the event you wish to pre-filter the results. what Context-style object to use in the response and the load_all performance optimization to reduce hits on the database. These options can (and generally should) be overridden at the URLconf level. For example, to have a custom search limited to the ‘John’ author, displaying all models to search by and specifying a custom template (my/special/path/john_search.html), your URLconf should look something like:
from django.conf.urls.defaults import *
from haystack.forms import ModelSearchForm
from haystack.query import SearchQuerySet
from haystack.views import SearchView
sqs = SearchQuerySet().filter(author='john')
# Without threading...
urlpatterns = patterns('haystack.views',
url(r'^$', SearchView(
template='my/special/path/john_search.html',
searchqueryset=sqs,
form_class=SearchForm
), name='haystack_search'),
)
# With threading...
from haystack.views import SearchView, search_view_factory
urlpatterns = patterns('haystack.views',
url(r'^$', search_view_factory(
view_class=SearchView,
template='my/special/path/john_search.html',
searchqueryset=sqs,
form_class=ModelSearchForm
), name='haystack_search'),
)
Warning
The standard SearchView is not thread-safe. Use the search_view_factory function, which returns thread-safe instances of SearchView.
By default, if you don’t specify a form_class, the view will use the haystack.forms.ModelSearchForm form.
Beyond this customizations, you can create your own SearchView and extend/override the following methods to change the functionality.
Generates the actual response to the search.
Relies on internal, overridable methods to construct the response. You generally should avoid altering this method unless you need to change the flow of the methods or to add a new method into the processing.
Instantiates the form the class should use to process the search query.
Optionally accepts a dictionary of parameters that are passed on to the form’s __init__. You can use this to lightly customize the form.
You should override this if you write a custom form that needs special parameters for instantiation.
Returns the query provided by the user.
Returns an empty string if the query is invalid. This pulls the cleaned query from the form, via the q field, for use elsewhere within the SearchView. This is used to populate the query context variable.
Fetches the results via the form.
Returns an empty list if there’s no query to search with. This method relies on the form to do the heavy lifting as much as possible.
Paginates the results appropriately.
In case someone does not want to use Django’s built-in pagination, it should be a simple matter to override this method to do what they would like.
Allows the addition of more context variables as needed. Must return a dictionary whose contents will add to or overwrite the other variables in the context.
Generates the actual HttpResponse to send back to the user. It builds the page, creates the context and renders the response for all the aforementioned processing.
The basic_search tries to provide most of the same functionality as the class-based views but resembles a more traditional generic view. It’s both a working view if you prefer not to use the class-based views as well as a good starting point for writing highly custom views.
Since it is all one function, the only means of extension are passing in kwargs, similar to the way generic views work.
As with the forms, inheritance is likely your best bet. In this case, the FacetedSearchView is a perfect example of how to extend the existing SearchView. The complete code for the FacetedSearchView looks like:
class FacetedSearchView(SearchView):
def __name__(self):
return "FacetedSearchView"
def extra_context(self):
extra = super(FacetedSearchView, self).extra_context()
if self.results == []:
extra['facets'] = self.form.search().facet_counts()
else:
extra['facets'] = self.results.facet_counts()
return extra
It updates the name of the class (generally for documentation purposes) and adds the facets from the SearchQuerySet to the context as the facets variable. As with the custom form example above, it relies on the parent class to handle most of the processing and extends that only where needed.


2013 - September: Our blog hits the web to semantically correct reviews!
2014 - January: Business plan is completed.
August: British developer Terrance Tech is hired. Expansion of our IT space continues.
2015 - January: Marketing department hosts gala open house showcasing our newly renovated offices.
September 28: Our website goes live!
2016 - May: Announcement of Vancouver and Montreal offices to open in 2017!
Our blog was developed as a result of founder Dr. Doctype’s belief that he could make people more aware of beautifully crafted code. In August 2013, he left his position as Senior Developer at the Coding Network and dedicated himself to turning his vision into reality.


{% extends 'modal_base.html' %} {% block modal_title %}Delete{% endblock %} {% block modal_body %}Are you sure you want to delete the "{{ command.command }}" command?{% endblock %} {% block modal_footer %}


Msg object
A msg
object represents a line of text delivered from the connected Twitch server. It is formatted to be easier to use than a raw line of text from chat would normally be. But it's still a generic format.
Many are easy to understand and consistent such as the JOIN Twitch command, some can also be a little bit more difficult.  Examples of what raw messages look like can be found on the Twitch IRC guide.
| param | description |
|---|---|
raw |
The full message in raw form |
tags |
Object containing all tags |
prefix |
Object containing prefix information |
prefix.full |
Full prefix (Ie<EMAIL_ADDRESS>) |
prefix.host |
Host (Ie. 'ronni.tmi.twitch.tv' ) |
prefix.user |
User (Ie. 'ronni' ) |
command |
The Twitch command (Ie. 'PRIVMSG' ) |
params |
Array of parameters that follow the command (Ie. ['#channel', 'Hi everyone!'] ) |
channel |
Taken from params if detected or null (Ie. '#channel' ) |
message |
Taken from params if detected or null (Ie. 'Hi everyone!' ) |
extended |
Object containing special extended information (Ie. {} ) |
Tags
Tags are converted into an object with keys that are in camelCase. If you are looking for a tag named 'display-name'
for example it can be found in the msg object at msg.tags.displayName
. When the value is a number it is converted into a number otherwise all tags resolve a string.
A few of the tags returned have special rendering.
badges
Badges are split by ','
so that they are an array, for example ['subscriber/0', 'premium/1']
.
emotes
Emotes denote where in the message an emote was used and is rendered as an array containing objects with id
, start
, end
, and length
attributes. For example [{ id: 25, start: 27, end: 31, length: 4 }]
emoteSets
Emote sets are split by ','
and turned into numbers for example [0]
.
Params
The first parameter is commonly the channel, therefore very often when you want to know what channel the command is related to you could use msg.params[0]
. This isn't true for all commands but is good general rule to keep in mind.
A msg.channel
attribute is available, if what looks like a channel is found in msg.params
and it isn't the message. A msg.message
attribute is available, if the last parameter in msg.params
uses the :
long form notation.
Furthermore params are emitted as the remaining parameters of events in the format (msg, ...params)
so they are easy access in event handlers.


importance: 5
Write the function sortByAge(users)
that gets an array of objects with the age
property and sorts them by age
.
For instance:
```js no-beautify let john = { name: “John”, age: 25 }; let pete = { name: “Pete”, age: 30 }; let mary = { name: “Mary”, age: 28 };
let arr = [ pete, john, mary ];
sortByAge(arr);
// now: [john, mary, pete] alert(arr[0].name); // John alert(arr[1].name); // Mary alert(arr[2].name); // Pete ```


Topic Area:
Enter your solution:
Submit
Correct!
Next
Wrong
Please try again
More Options
Delete Card


Bay Seeker Island Package
Change SearchIncluded in this booking:
- Same day return ferry ticket
- Rottnest Island admission ticket
- Morning tea at Hillarys Boat Harbour
- Full-day tour host
- 2 hour island tour includes all of Rottnest’s must see locations, including Wadjemup Lighthouse, Henrietta Rocks, the majestic look-out point at the rugged Cathedral Rocks and Cape Vlamingh
- and any selected extras
Review your Booking
Please review your booking thoroughly.
Booking Details
Bay Seeker Island Package
| Rottnest Island Admission Fee | |||
| Adult (x1) | $19.50 | ||
| Kid (x1) | $7.00 | ||
| Subtotal | $26.50 | ||
| Hillarys to Rottnest Ferry Ticket | |||
| Sun, 03 Jan 2021 - 7:30am | |||
| Package Fare | |||
| Adult (x1) | $112.00 | ||
| Child (x1) | $68.00 | ||
| Subtotal | $180.00 | ||
| Rottnest to Hillarys Ferry Ticket | |||
| Sun, 03 Jan 2021 - 4:30pm | |||
| Package Fare | |||
| Adult (x1) | $0.00 | ||
| Child (x1) | $0.00 | ||
| Subtotal | $0.00 | ||
| Bus Pickup | |||
| Great Southern Hotel - 6:25am | |||
| Adult (x1) | $0.00 | ||
| Child (x1) | $0.00 | ||
| Subtotal | $0.00 | ||
| Extras | |||
| No Item Selected | |||
| Snorkel Set (x2) (x1 days) | $30.00 | ||
|
|
|||
|
|
|||
| Subtotal | $30.00 | ||
| Mobility Items | |||
| No Item Selected | |||
| Subtotal | $0.00 | ||
| Coupon Discount | |||
|
|||
| Total | $ 212.85 | ||
| Credit card Surcharge (1.5%) | $ 3.19 | ||
| Final Price | $ 212.85 |
Passenger Details
1 Adult & 1 Child
Grace Kaspe - Adult
- Email Address<EMAIL_ADDRESS>- Addreess: 459 Stirling Highway, Cottesloe 6107 Western Australia, Australia
- Date of Birth: 14/08/1996
Little Grace - Child
Payment
All transactions are secure and encrypted. You will receive an email confirmation containing your booking details, which needs to be presented on the day of your trip.
Credit Card
Merchant Reference: 355753
Final price to pay:$212.85


ChiTown Speedzone Trains
From Chitown to Wherever We Go
Train Scheduled
Train Name
Destination
Frequency (min.)
Next Arrival
Minutes Away
Delete
Train Name
Train Name
Train Destination
First Train Time (hh:mm - military time)
Frequency
Submit


A controllable logging module.
Base class for HTTP abstraction.
This class provides the basic functionality (get/post/delete/request), as well as utilities to construct uniform responses.
Base classes should only override makeRequest
and parseJSON
Various utility functions for the Splunk SDK
Utilities for Async control flow and collection handling
Abstraction over the Splunk HTTP-wire protocol
This class provides the basic functionality for communicating with a Splunk instance over HTTP. It will handle authentication and authorization, and formatting HTTP requests (GET/POST/DELETE) in the format Splunk expects.
Root access point to the Splunk REST API
This Service
class provides "typed" access to Splunk concepts such as searches, indexes, apps and more, as well as providing convenience methods to authenticate and get more specialized instances of the service.
Base definition for a Splunk endpoint (specific service + path combination).
This Endpoint
class provides convenience methods for the three HTTP verbs used in splunkjs. It will automatically prepare the path correctly, and allows for relative calls.
Base definition for a Splunk "resource" (e.g. index, jobs, etc)
This Resource
class provides basic methods for handling Splunk resources, such as validation, property accessor, etc. This class should not be used directly, as most methods are meant to be overridden.
Base class for a Splunk "entity", which is a well defined construct with certain operations (like "properties", "update", "delete").
This Entity
class provides basic methods for handling Splunk entities, such as fetching them, updating, etc.
Base class for a Splunk "collection", which is a well defined construct with certain operations (like "list", "create", etc).
This Collection
class provides basic methods for handling Splunk entity collection, such as creating an entity, listing entities, etc.
Represents a specific Splunk saved search. You can update, remove and perform various operations on this saved search.
Represents the Splunk collection of saved searches. You can create and list saved searches using this container, or get a specific one.
Represents a specific Splunk application. You can update, remove and perform various operations on this application.
Represents the Splunk collection of applications. You can create and list applications using this container, or get a specific one.
Represents the server info
Represents a specific Splunk user. You can update, remove and perform various operations on this user.
Represents the Splunk collection of users. You can create and list users using this container, or get a specific one.
Represents a specific Splunk view. You can update, remove and perform various operations on this view.
Represents the Splunk collection of views. You can create and list views using this container, or get a specific one.
Represents a specific Splunk index. You can update and submit events to this index.
Represents the Splunk collection of indexes. You can create and list indexes using this container, or get a specific one.
Represents a specific Splunk stanza. You can update and remove this stanza.
Represents the Splunk collection of stanzas for a specific property file. You can create and list stanzas using this container, or get a specific one.
Represents the Splunk collection of configuration files. You can create and list files using this container, or get a specific one.
Represents a specific Splunk search job. You can perform various operations on this job, such as reading its status, cancelling it, getting results and so on.
Represents the Splunk collection of jobs. You can create and list search jobs using this container, or get a specific one.


DISCLAIMER
This tool must not be relied upon, content could be false, outdated, inaccurate or misleading.
You must not use the information on this site for anything when the safety of yourself or others is a concern.


Upcoming Events
August 4
NYSL Fundraiser
August 16
Season Kick-off: Meet the teams
September 1
First Game of the Season (Check Game Schedule for details)
NYSL Fundraiser
Season Kick-off: Meet the teams
First Game of the Season (Check Game Schedule for details)


VSL // In Defense Of Breakfast
* Pixie queen and budding style icon Tavi Gevinson takes our favorite cereal box mascots and gives them the Rookie treatment
today’s Very Short List:
food 28 Mar 2014
A native New Yorker and self-proclaimed foodie, Sonia J. Lessuck is an Account Executive at Susan Magrino Agency. When she’s not eating or working she enjoys yoga, dancing, and reading. Twitter
Subscribe
* Turns out saturated fats may not be that bad for you. TakePart
* Still haven’t tried Dominique Ansel’s infamous Cronut? In last week’s Front Burner, Florence Fabricant offers an alternative
http://link.nyobserver.com/516ca68465217dc6e1b9a3a61hzpu.bl0/UQvKZm-oa4SYFKEqC9f1d very short list is a
delightful e-mail that shares
cultural gems from a
different curator every day.
If you have any problems reading this e-mail, click here
http://link.nyobserver.com/516ca68465217dc6e1b9a3a61hzpu.bl0/Tyk4O_EdCBvgSTIZCa36d
Subscribe
Forward
My Account
Unsubscribe
culture 26 Mar 2014
Carly Ayres uncovers some hidden artistic details.
tech 24 Mar 2014
Celine Semaan Vernon on the comeback of science.
style 21 Mar 2014
Jac Cameron and Maggie Winter on the allure of denim.
Editorial Policy
Privacy Policy
Contact Us
Press
Terms + Conditions
very fine print: ©2014
Observer VSL LLC.
321 West 44th Street, 6th Floor
New York, NY 10036 USA
All rights reserved.
Questions?<PHONE_NUMBER>.
This message was intended for<EMAIL_ADDRESS>If you believe this has been sent to you in error, please safely unsubscribe


Dear Firefox User,
You are seeing this message instead of whatever page you're expecting to see because of a recent decision made by the Mozilla corporation. On March 24, 2014, Brendan Eich was promoted to the CEO of Mozilla. In 2008, Eich made a $1,000 donation in support of California's Proposition 8. As you probably know, Prop 8 was a (thankfully failed) attempt at destroying marriage equality in California.
In 2012, when it was discovered that he made this donation, Eich wrote a non-apologetic apology and another one in 2013, shortly after the firestorm of controversy erupted around his promotion to CEO. His actions clearly indicate that he does not value the civil rights of LGBT individuals.
Sadly, this is not all. In the 90's and early 2000's, Eich has made several donations to Pat Buchanan, Ron Paul, and Tea Party representative Thomas McClintock (R-CA) (source).
Brendan Eich is standing on the wrong side of history, and is doubling down. Since Eich is the CEO of Mozilla, it follows that Mozilla is standing on the wrong side of history.
Please consider accessing this site with another browser:If you insist on viewing this page with Firefox, please add the following to the end of the URL: ?firefox_bypass=1


5 Things I Learned from the Accessibility Community
@MarcySutton / #CMEmpathy
#a11y
- Listen and learn
- Know your craft
- Design for low vision
- Don’t be vague
- Be positive
Spending time with people with disabilities
Making waves, on my birthday.
Raising awareness and empathy
I'm not disabled, but I could be. So could you.
A lot of legacy to take in as a newcomer (i.e. longdesc)
I am dying to do user testing, particularly with people with disabilities.
Embrace flexibility.
Limit the marketing speak.
Provide captions.
Be positive.
Look for the beauty in things.
Don’t let perfect be the enemy of good.
Accessibility Wins
“It’s not unique to them.”
“Don’t sweat the medium stuff.”