diff options
Diffstat (limited to 'mppa_k1c/abstractbb/Impure/ImpPrelude.v')
| -rw-r--r-- | mppa_k1c/abstractbb/Impure/ImpPrelude.v | 32 |
1 files changed, 17 insertions, 15 deletions
diff --git a/mppa_k1c/abstractbb/Impure/ImpPrelude.v b/mppa_k1c/abstractbb/Impure/ImpPrelude.v index 8d904be6..0efa042c 100644 --- a/mppa_k1c/abstractbb/Impure/ImpPrelude.v +++ b/mppa_k1c/abstractbb/Impure/ImpPrelude.v @@ -6,10 +6,23 @@ Require Import BinNums. Require Export ImpCore. Require Export PArith. + +Import Notations. +Local Open Scope impure. + +(** 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 ! *) + +(** Strings for pretty-printing *) + Axiom caml_string: Type. Extract Constant caml_string => "string". -(** New line *) +(* New line *) Definition nl: string := String (ascii_of_pos 10%positive) EmptyString. Inductive pstring: Type := @@ -25,9 +38,6 @@ Notation "x +; y" := (Concat x y) (** Coq references *) -Import Notations. -Local Open Scope impure. - Record cref {A} := { set: A -> ?? unit; get: unit -> ?? A @@ -52,20 +62,15 @@ Extract Constant count_logger => "(fun () -> let count = ref 0 in { log_insert = (** Axioms of Physical equality *) -Module Type PhysEq. - Axiom phys_eq: forall {A}, A -> A -> ?? bool. Axiom phys_eq_correct: forall A (x y:A), WHEN phys_eq x y ~> b THEN b=true -> x=y. -End PhysEq. - - (* We only check here that above axioms are not trivially inconsistent... (but this does not prove the correctness of the extraction directive below). *) -Module PhysEqModel: PhysEq. +Module PhysEqModel. Definition phys_eq {A} (x y: A) := ret false. @@ -76,16 +81,13 @@ Qed. End PhysEqModel. - -Export PhysEqModel. - -Extract Constant phys_eq => "(==)". +Extract Inlined 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 if b then x=y else x<>y. -Extract Constant struct_eq => "(=)". +Extract Inlined Constant struct_eq => "(=)". Hint Resolve struct_eq_correct: wlp. |