From 5619eec808bdb9066c5e26b41956fc4534e103fa Mon Sep 17 00:00:00 2001
From: Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr>
Date: Mon, 8 Apr 2019 17:39:28 +0200
Subject: moving iandb from ImpCore to ImpPrelude

---
 mppa_k1c/abstractbb/Impure/ImpCore.v    |  9 +--------
 mppa_k1c/abstractbb/Impure/ImpPrelude.v | 32 +++++++++++++++++---------------
 2 files changed, 18 insertions(+), 23 deletions(-)

(limited to 'mppa_k1c/abstractbb')

diff --git a/mppa_k1c/abstractbb/Impure/ImpCore.v b/mppa_k1c/abstractbb/Impure/ImpCore.v
index 9745e35c..55e67608 100644
--- a/mppa_k1c/abstractbb/Impure/ImpCore.v
+++ b/mppa_k1c/abstractbb/Impure/ImpCore.v
@@ -185,11 +185,4 @@ Ltac wlp_xsimplify hint :=
 
 Create HintDb wlp discriminated.
 
-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
+Ltac wlp_simplify := wlp_xsimplify ltac:(intuition eauto with wlp).
\ No newline at end of file
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.
 
 
-- 
cgit