starting to move common files

1 files changed, 0 insertions, 196 deletions

diff --git a/kvx/abstractbb/Impure/ImpCore.v b/kvx/abstractbb/Impure/ImpCore.v
deleted file mode 100644
index 508b3f19..00000000
--- a/kvx/abstractbb/Impure/ImpCore.v
+++ /dev/null
@@ -1,196 +0,0 @@
-(** Impure monad for interface with impure code
-
-*)
-
-Require Export Program.
-Require Export ImpConfig.
-
-(* Theory: bind + embed => dbind 
-
-Program Definition dbind {A B} (k1: t A) (k2: forall (a:A), (mayRet k1 a) -> t B) : t B
-  := bind (mk_annot k1) (fun a => k2 a _).
-
-Lemma mayRet_dbind: forall (A B:Type) k1 k2 (b:B),
-     mayRet (dbind k1 k2) b -> exists a:A, exists H: (mayRet k1 a), mayRet (k2 a H) b.
-Proof.
-  intros A B k1 k2 b H; decompose [ex and] (mayRet_bind _ _ _ _ _ H).
-  eapply ex_intro.
-  eapply ex_intro.
-  eauto.
-Qed.
-
-*)
-
-Definition wlp {A:Type} (k: t A) (P: A -> Prop): Prop
-  := forall a, mayRet k a -> P a.
-
-(* Notations *)
-
-(* Print Grammar constr. *)
-
-Module Notations.
-
-  Bind Scope impure_scope with t.
-  Delimit Scope impure_scope with impure.
-
-  Notation "?? A" := (t A) (at level 0, A at level 95): impure_scope.
-
-  Notation "k '~~>' a" := (mayRet k a) (at level 75, no associativity): impure_scope. 
-
-  Notation "'RET' a" := (ret a) (at level 0): impure_scope.
-
-  Notation "'DO' x '<~' k1 ';;' k2" := (bind k1 (fun x => k2))
-    (at level 55, k1 at level 53, x at level 99, right associativity): impure_scope.
-
-  Notation "k1 ';;'  k2" := (bind k1 (fun _ => k2))
-    (at level 55, right associativity): impure_scope.
-
-  Notation "'WHEN' k '~>' a 'THEN' R" := (wlp k (fun a => R))
-    (at level 73, R at level 100, right associativity): impure_scope.
-
-  Notation "'ASSERT' P" := (ret (A:=P) _) (at level 0, only parsing): impure_scope.
-
-End Notations.
-
-Import Notations.
-Local Open Scope impure.
-
-Goal ((?? list nat * ??nat -> nat) = ((?? ((list nat) * ?? nat) -> nat)))%type.
-Proof.
-  apply refl_equal.
-Qed.
-
-
-(* wlp lemmas for tactics *)
-
-Lemma wlp_unfold A (k:??A)(P: A -> Prop):
-   (forall a, k ~~> a -> P a)
-    -> wlp k P.
-Proof.
-  auto.
-Qed.
-
-Lemma wlp_monotone A (k:?? A) (P1 P2: A -> Prop):
-    wlp k P1
-    -> (forall a, k ~~> a -> P1 a -> P2 a)
-    -> wlp k P2.
-Proof.
-  unfold wlp; eauto.
-Qed.
-
-Lemma wlp_forall A B (k:?? A) (P: B -> A -> Prop):
-   (forall x, wlp k (P x))
-    -> wlp k (fun a => forall x, P x a).
-Proof.
-  unfold wlp; auto.
-Qed.
-
-Lemma wlp_ret A (P: A -> Prop) a:
-   P a -> wlp (ret a) P.
-Proof.
-    unfold wlp.
-    intros H b H0.
-    rewrite <- (mayRet_ret _ a b H0).
-    auto.
-Qed.
-
-Lemma wlp_bind A B (k1:??A) (k2: A -> ??B) (P: B -> Prop):
-  wlp k1 (fun a => wlp (k2 a) P) -> wlp (bind k1 k2) P.
-Proof.
-    unfold wlp.
-    intros H a H0.
-    case (mayRet_bind _ _ _ _ _ H0); clear H0.
-    intuition eauto.
-Qed.
-
-Lemma wlp_ifbool A (cond: bool) (k1 k2: ?? A) (P: A -> Prop):
- (cond=true -> wlp k1 P) -> (cond=false -> wlp k2 P) -> wlp (if cond then k1 else k2) P.
-Proof.
-  destruct cond; auto.
-Qed.
-
-Lemma wlp_letprod (A B C: Type) (p: A*B) (k: A -> B -> ??C) (P: C -> Prop):
-  (wlp (k (fst p) (snd p)) P)
-    -> (wlp (let (x,y):=p in (k x y)) P).
-Proof.
-  destruct p; simpl; auto.
-Qed.
-
-Lemma wlp_sum (A B C: Type) (x: A+B) (k1: A -> ??C) (k2: B -> ??C)  (P: C -> Prop):
-  (forall a, x=inl a -> wlp (k1 a) P) -> 
-  (forall b, x=inr b -> wlp (k2 b) P) -> 
-     (wlp (match x with inl a => k1 a | inr b => k2 b end) P).
-Proof.
-  destruct x; simpl; auto.
-Qed.
-
-Lemma wlp_sumbool (A B:Prop) (C: Type) (x: {A}+{B}) (k1: A -> ??C) (k2: B -> ??C)  (P: C -> Prop):
-  (forall a, x=left a -> wlp (k1 a) P) -> 
-  (forall b, x=right b -> wlp (k2 b) P) -> 
-     (wlp (match x with left a => k1 a | right b => k2 b end) P).
-Proof.
-  destruct x; simpl; auto.
-Qed.
-
-Lemma wlp_option (A B: Type) (x: option A) (k1: A -> ??B) (k2: ??B)  (P: B -> Prop):
-  (forall a, x=Some a -> wlp (k1 a) P) -> 
-  (x=None -> wlp k2 P) -> 
-     (wlp (match x with Some a => k1 a | None => k2 end) P).
-Proof.
-  destruct x; simpl; auto.
-Qed.
-
-(* Tactics 
-
-MAIN tactics:  
-  - xtsimplify "base": simplification using from hints in "base" database (in particular "wlp" lemmas).
-  - xtstep "base": only one step of simplification.
-
-For good performance, it is recommanded to have several databases.
-
-*)
-
-Ltac introcomp :=
-  let a:= fresh "exta" in
-  let H:= fresh "Hexta" in
-  intros a H.
-
-(* decompose the current wlp goal using "introduction" rules *)
-Ltac wlp_decompose :=
-    apply wlp_ret
- || apply wlp_bind
- || apply wlp_ifbool
- || apply wlp_letprod
- || apply wlp_sum
- || apply wlp_sumbool
- || apply wlp_option
- .
-
-(* this tactic simplifies the current "wlp" goal using any hint found via tactic "hint". *) 
-Ltac apply_wlp_hint hint :=
-    eapply wlp_monotone;
-      [ hint; fail | idtac ] ;
-      simpl; introcomp.
-
-(* one step of wlp_xsimplify 
-*)
-Ltac wlp_step hint :=
-    match goal with
-      | |- (wlp _ _) => 
-        wlp_decompose
-        || apply_wlp_hint hint
-        || (apply wlp_unfold; introcomp)
-    end.
-
-(* main general tactic 
-WARNING: for the good behavior of "wlp_xsimplify", "hint" must at least perform a "eauto".
-
-Example of use:
-  wlp_xsimplify (intuition eauto with base).
-*)
-Ltac wlp_xsimplify hint := 
-    repeat (intros; subst; wlp_step hint; simpl; (tauto || hint)).
-
-Create HintDb wlp discriminated.
-
-Ltac wlp_simplify := wlp_xsimplify ltac:(intuition eauto with wlp).