Coq: generalise dependent pair handling a little

1. for monadic values (not in a terribly useful way, though)
2. for more types

2 files changed, 11 insertions, 1 deletions

diff --git a/lib/coq/Sail2_prompt.v b/lib/coq/Sail2_prompt.v
index c98e2926..0b3a2cd8 100644
--- a/lib/coq/Sail2_prompt.v
+++ b/lib/coq/Sail2_prompt.v
@@ -115,3 +115,13 @@ let rec untilM vars cond body =
   write_reg r1 r1_v >> write_reg r2 r2_v*)
 
 *)
+
+(* If we need to build an existential after a monadic operation, assume that
+   we can do it entirely from the type. *)
+
+Definition build_ex_m {rv e} {T:Type} (x:monad rv T e) {P:T -> Prop} `{H:forall x, ArithFact (P x)} : monad rv {x : T & ArithFact (P x)} e :=
+  x >>= fun y => returnm (existT _ y (H y)).
+
+Definition projT1_m {rv e} {P:Z -> Prop} (x: monad rv {x : Z & P x} e) : monad rv Z e :=
+  x >>= fun y => returnm (projT1 y).
+
diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v
index 41414c96..acd11b45 100644
--- a/lib/coq/Sail2_values.v
+++ b/lib/coq/Sail2_values.v
@@ -21,7 +21,7 @@ Lemma use_ArithFact {P} `(ArithFact P) : P.
 apply fact.
 Defined.
 
-Definition build_ex (n:Z) {P:Z -> Prop} `{H:ArithFact (P n)} : {x : Z & ArithFact (P x)} :=
+Definition build_ex {T:Type} (n:T) {P:T -> Prop} `{H:ArithFact (P n)} : {x : T & ArithFact (P x)} :=
   existT _ n H.
 
 Definition generic_eq {T:Type} (x y:T) `{Decidable (x = y)} := Decidable_witness.