Coq: Clean up rich boolean handling in backend

Now generates something vaguely sensible for RISC-V, although the solver
needs a little work.
Adds type annotations around effectful, rich and/or expressions.

1 files changed, 12 insertions, 12 deletions

diff --git a/lib/coq/Sail2_prompt.v b/lib/coq/Sail2_prompt.v
index f5d277e1..741fa921 100644
--- a/lib/coq/Sail2_prompt.v
+++ b/lib/coq/Sail2_prompt.v
@@ -57,16 +57,16 @@ 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 & P b} E) (y : monad rv {b:bool & Q b} E)
+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 & R b} E.
+  : monad rv {b:bool & ArithFact (R b)} E.
 refine (
-  x >>= fun '(existT _ x p) => (if x return P x -> _ then
+  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
 ).
-* destruct H. change y with (andb true y). auto.
-* destruct H. change false with (andb false false). apply fact.
+* 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.
@@ -74,20 +74,20 @@ 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 & P b} E) (r : monad rv {b : bool & Q b} E)
+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 & R b} E.
+ : monad rv {b : bool & ArithFact (R b)} E.
 refine (
- l >>= fun '(existT _ l p) =>
+ 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
 ).
-* destruct H. change true with (orb true true). apply fact. assumption. congruence.
-* destruct H. change r with (orb false r). auto.
+* 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 & True} E :=
-  x >>= fun x => returnm (existT _ x I).
+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)).
 
 Definition and_boolBM {rv E P Q} (l : monad rv (Bool P) E) (r : monad rv (Bool Q) E) : monad rv (Bool (P /\ Q)) E.
 refine (