diff options
Diffstat (limited to 'mppa_k1c/abstractbb')
| -rw-r--r-- | mppa_k1c/abstractbb/Impure/ImpCore.v | 10 | ||||
| -rw-r--r-- | mppa_k1c/abstractbb/Impure/ImpPrelude.v | 4 |
2 files changed, 11 insertions, 3 deletions
diff --git a/mppa_k1c/abstractbb/Impure/ImpCore.v b/mppa_k1c/abstractbb/Impure/ImpCore.v index 6eb0c5af..9745e35c 100644 --- a/mppa_k1c/abstractbb/Impure/ImpCore.v +++ b/mppa_k1c/abstractbb/Impure/ImpCore.v @@ -132,6 +132,7 @@ Proof. destruct x; simpl; auto. Qed. + (* Tactics MAIN tactics: @@ -184,4 +185,11 @@ Ltac wlp_xsimplify hint := Create HintDb wlp discriminated. -Ltac wlp_simplify := wlp_xsimplify ltac:(intuition eauto with wlp).
\ No newline at end of file +Ltac wlp_simplify := wlp_xsimplify ltac:(intuition eauto with wlp). + +(* impure lazy andb of booleans *) +Definition iandb (k1 k2: ??bool): ?? bool := + DO r1 <~ k1 ;; + if r1 then k2 else RET false. + +Extraction Inline iandb. (* Juste pour l'efficacité à l'extraction ! *)
\ No newline at end of file diff --git a/mppa_k1c/abstractbb/Impure/ImpPrelude.v b/mppa_k1c/abstractbb/Impure/ImpPrelude.v index e7c7a9fb..8d904be6 100644 --- a/mppa_k1c/abstractbb/Impure/ImpPrelude.v +++ b/mppa_k1c/abstractbb/Impure/ImpPrelude.v @@ -77,14 +77,14 @@ Qed. End PhysEqModel. - Export PhysEqModel. Extract Constant phys_eq => "(==)". Hint Resolve phys_eq_correct: wlp. + Axiom struct_eq: forall {A}, A -> A -> ?? bool. -Axiom struct_eq_correct: forall A (x y:A), WHEN struct_eq x y ~> b THEN b=true -> x=y. +Axiom struct_eq_correct: forall A (x y:A), WHEN struct_eq x y ~> b THEN if b then x=y else x<>y. Extract Constant struct_eq => "(=)". Hint Resolve struct_eq_correct: wlp. |