Impure: improved iandb + struct_eq

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.