diff options
Diffstat (limited to 'mppa_k1c/abstractbb/Impure/ImpCore.v')
| -rw-r--r-- | mppa_k1c/abstractbb/Impure/ImpCore.v | 196 |
1 files changed, 196 insertions, 0 deletions
diff --git a/mppa_k1c/abstractbb/Impure/ImpCore.v b/mppa_k1c/abstractbb/Impure/ImpCore.v new file mode 100644 index 00000000..f1abaf7a --- /dev/null +++ b/mppa_k1c/abstractbb/Impure/ImpCore.v @@ -0,0 +1,196 @@ +(** 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).
\ No newline at end of file |