diff options
| author | Brian Campbell | 2019-04-16 14:38:35 +0100 |
|---|---|---|
| committer | Brian Campbell | 2019-04-16 17:47:36 +0100 |
| commit | 70c1ab20b8b5539f4efedff84bea68f7683d1aec (patch) | |
| tree | 4aef88e8c3abbd159ed5ae7fd34d50c1896c5c4e /src | |
| parent | 23f39ad36659e7d46a3c1799e217bab22eca7869 (diff) | |
Coq: don't record assertions in the context if Sail doesn't
This can massively reduce Coq's typechecking time on assertion heavy code,
such as the builtins tests.
Diffstat (limited to 'src')
| -rw-r--r-- | src/pretty_print_coq.ml | 11 | ||||
| -rw-r--r-- | src/type_check.mli | 2 |
2 files changed, 10 insertions, 3 deletions
diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index ae0e1561..07f70c42 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -1994,9 +1994,14 @@ let doc_exp, doc_let = match pat, e1, e2 with | (P_aux (P_wild,_) | P_aux (P_typ (_, P_aux (P_wild, _)), _)), (E_aux (E_assert (assert_e1,assert_e2),_)), _ -> - let epp = liftR (separate space [string "assert_exp'"; expY assert_e1; expY assert_e2]) in - let epp = infix 0 1 (string ">>= fun _ =>") epp (top_exp new_ctxt false e2) in - if aexp_needed then parens (align epp) else align epp + let assert_fn, mid = + match assert_constraint outer_env true assert_e1 with + | Some _ -> "assert_exp'", ">>= fun _ =>" + | None -> "assert_exp", ">>" + in + let epp = liftR (separate space [string assert_fn; expY assert_e1; expY assert_e2]) in + let epp = infix 0 1 (string mid) epp (top_exp new_ctxt false e2) in + if aexp_needed then parens (align epp) else align epp | _ -> let epp = let middle = diff --git a/src/type_check.mli b/src/type_check.mli index 2a413238..dcedcc90 100644 --- a/src/type_check.mli +++ b/src/type_check.mli @@ -319,6 +319,8 @@ val check_fundef : Env.t -> 'a fundef -> tannot def list * Env.t val check_val_spec : Env.t -> 'a val_spec -> tannot def list * Env.t +val assert_constraint : Env.t -> bool -> tannot exp -> n_constraint option + (** Attempt to prove a constraint using z3. Returns true if z3 can prove that the constraint is true, returns false if z3 cannot prove the constraint true. Note that this does not guarantee that the |