diff options
| -rw-r--r-- | lib/coq/Sail2_prompt.v | 10 | ||||
| -rw-r--r-- | lib/coq/Sail2_values.v | 2 | ||||
| -rw-r--r-- | src/pretty_print_coq.ml | 9 |
3 files changed, 17 insertions, 4 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. diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index 93a24f4e..dff68092 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -1133,10 +1133,13 @@ let doc_exp_lem, doc_let_lem = | _ -> false in unpack,build_ex,autocast in - let autocast_id = if effectful eff then "autocast_m" else "autocast" in - let epp = if unpack then string "projT1" ^^ space ^^ parens epp else epp in + let autocast_id, proj_id, build_id = + if effectful eff + then "autocast_m", "projT1_m", "build_ex_m" + else "autocast", "projT1", "build_ex" in + let epp = if unpack then string proj_id ^^ space ^^ parens epp else epp in let epp = if autocast then string autocast_id ^^ space ^^ parens epp else epp in - let epp = if build_ex then string "build_ex" ^^ space ^^ parens epp else epp in + let epp = if build_ex then string build_id ^^ space ^^ parens epp else epp in liftR (if aexp_needed then parens (align epp) else epp) end | E_vector_access (v,e) -> |