Merge branch 'sail2' of https://github.com/rems-project/sail into sail2

2 files changed, 36 insertions, 25 deletions

diff --git a/lib/coq/Sail2_prompt.v b/lib/coq/Sail2_prompt.v
index bd0d7750..bae8381e 100644
--- a/lib/coq/Sail2_prompt.v
+++ b/lib/coq/Sail2_prompt.v
@@ -57,9 +57,37 @@ Definition foreach_ZM_down {rv e Vars} from to step vars body `{ArithFact (0 < s
 Definition and_boolM {rv E} (l : monad rv bool E) (r : monad rv bool E) : monad rv bool E :=
  l >>= (fun l => if l then r else returnm false).
 
+Definition and_boolMP {rv E} {P Q R:bool->Prop} (x : monad rv {b:bool & ArithFact (P b)} E) (y : monad rv {b:bool & ArithFact (Q b)} E)
+  `{H:ArithFact (forall l r, P l -> (l = true -> Q r) -> R (andb l r))}
+  : monad rv {b:bool & ArithFact (R b)} E.
+refine (
+  x >>= fun '(existT _ x (Build_ArithFact _ p)) => (if x return P x -> _ then
+    fun p => y >>= fun '(existT _ y _) => returnm (existT _ y _)
+  else fun p => returnm (existT _ false _)) p
+).
+* constructor. destruct H. destruct a0. change y with (andb true y). auto.
+* constructor. destruct H. change false with (andb false false). apply fact.
+  assumption.
+  congruence.
+Defined.
+
 (*val or_boolM : forall 'rv 'e. monad 'rv bool 'e -> monad 'rv bool 'e -> monad 'rv bool 'e*)
 Definition or_boolM {rv E} (l : monad rv bool E) (r : monad rv bool E) : monad rv bool E :=
  l >>= (fun l => if l then returnm true else r).
+Definition or_boolMP {rv E} {P Q R:bool -> Prop} (l : monad rv {b : bool & ArithFact (P b)} E) (r : monad rv {b : bool & ArithFact (Q b)} E)
+ `{ArithFact (forall l r, P l -> (l = false -> Q r) -> R (orb l r))}
+ : monad rv {b : bool & ArithFact (R b)} E.
+refine (
+ l >>= fun '(existT _ l (Build_ArithFact _ p)) =>
+  (if l return P l -> _ then fun p => returnm (existT _ true _)
+   else fun p => r >>= fun '(existT _ r _) => returnm (existT _ r _)) p
+).
+* constructor. destruct H. change true with (orb true true). apply fact. assumption. congruence.
+* constructor. destruct H. destruct a0. change r with (orb false r). auto.
+Defined.
+
+Definition build_trivial_ex {rv E} {T:Type} (x:monad rv T E) : monad rv {x : T & ArithFact True} E :=
+  x >>= fun x => returnm (existT _ x (Build_ArithFact _ I)).
 
 (*val bool_of_bitU_fail : forall 'rv 'e. bitU -> monad 'rv bool 'e*)
 Definition bool_of_bitU_fail {rv E} (b : bitU) : monad rv bool E :=
diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v
index 943d850a..e6c5e786 100644
--- a/lib/coq/Sail2_values.v
+++ b/lib/coq/Sail2_values.v
@@ -45,25 +45,6 @@ End Morphism.
 Definition build_ex {T:Type} (n:T) {P:T -> Prop} `{H:ArithFact (P n)} : {x : T & ArithFact (P x)} :=
   existT _ n H.
 
-(* The informative boolean type. *)
-
-Definition Bool (P : Prop) : Type := {P} + {~P}.
-
-Definition build_Bool {P:Prop} (b:bool) `{ArithFact (b = true <-> P)} : Bool P.
-refine (if sumbool_of_bool b then left _ else right _);
-destruct H; subst;
-intuition.
-Defined.
-
-Definition projBool {P:Prop} (b:Bool P) : bool := if b then true else false.
-
-Lemma projBool_true {P:Prop} {b:Bool P} : projBool b = true <-> P.
-destruct b; simpl; intuition.
-Qed.
-Lemma projBool_false {P:Prop} {b:Bool P} : projBool b = false <-> ~P.
-destruct b; simpl; intuition.
-Qed.
-
 
 Definition generic_eq {T:Type} (x y:T) `{Decidable (x = y)} := Decidable_witness.
 Definition generic_neq {T:Type} (x y:T) `{Decidable (x = y)} := negb Decidable_witness.
@@ -1113,11 +1094,6 @@ Ltac extract_properties :=
     let Hx := fresh "Hx" in
     destruct X as [x Hx] in *;
     change (projT1 (existT _ x Hx)) with x in * end.
-(* We could also destruct any remaining Bools, if necessary. *)
-Ltac extract_Bool_props :=
-  repeat match goal with
-  | H:projBool _ = true |- _ => rewrite projBool_true in H
-  | H:projBool _ = false |- _ => rewrite projBool_false in H end.
 (* TODO: hyps, too? *)
 Ltac reduce_list_lengths :=
   repeat match goal with |- context [length_list ?X] => 
@@ -1183,7 +1159,6 @@ Ltac prepare_for_solver :=
  autounfold with sail in * |- *; (* You can add Hint Unfold ... : sail to let omega see through fns *)
  split_cases;
  extract_properties;
- extract_Bool_props;
  repeat match goal with w:mword ?n |- _ => apply ArithFact_mword in w end;
  unwrap_ArithFacts;
  destruct_exists;
@@ -1233,6 +1208,14 @@ prepare_for_solver;
  | constructor; eauto 3 with zarith sail
    (* The datatypes hints give us some list handling, esp In *)
  | constructor; drop_exists; eauto 3 with datatypes zarith sail
+   (* Booleans - and_boolMP *)
+ | match goal with |- ArithFact (forall l r:bool, _ -> _ -> exists _, _) => 
+     constructor; intros l r H1 H2;
+     solve [exists l; destruct l; intuition | exists r; destruct l; intuition]
+   end
+ | match goal with |- context [@eq _ _ _] =>
+     constructor; intuition
+   end
  | constructor; idtac "Unable to solve constraint"; dump_context; fail
  ].
 (* Add an indirection so that you can redefine run_solver to fail to get