Commit bd9acd41 authored by Andrei Paskevich's avatar Andrei Paskevich

whyml: make preliminary checks on VCs before calling eval_match

eval_match expects a well-formed formula, consistent with the known_map
parent 4902c129
......@@ -347,10 +347,10 @@ exception TooLateInvariant
let add_invariant uc its p =
let rec add = function
| { pd_node = PDtype _ } as d :: dl ->
let nd, dl = add dl in nd, d :: dl
| d :: dl when Mid.mem its.its_pure.ts_name d.pd_news ->
let d = Mlw_decl.add_invariant d its p in d, d :: dl
| { pd_node = PDtype _ } as d :: dl ->
let nd, dl = add dl in nd, d :: dl
| _ -> raise TooLateInvariant in
let decl, decls = add uc.muc_decls in
let kn = Mid.map (Util.const decl) decl.pd_news in
......
......@@ -89,10 +89,7 @@ val add_meta : module_uc -> meta -> meta_arg list -> module_uc
val add_pdecl : wp:bool -> module_uc -> pdecl -> module_uc
(** [add_pdecl ~wp m d] adds declaration [d] in module [m].
It may raise [Not_found] if [d] contains objects that are not visible
within the current module.
parameter [w] : TODO
*)
If [wp] is [true], VC is computed and added to [m]. *)
exception TooLateInvariant
......
......@@ -898,6 +898,8 @@ let add_wp_decl km name f uc =
let f = if Debug.test_flag no_track then f else track_values lkm km f in
(* simplify f *)
let f = if Debug.test_flag no_eval then f else
(* do preliminary checks on f to spare eval_match any surprises *)
let _lkm = Decl.known_add_decl lkm (create_prop_decl Pgoal pr f) in
Eval_match.eval_match ~inline:Eval_match.inline_nonrec_linear lkm f in
(* printf "wp: f=%a@." print_term f; *)
let d = create_prop_decl Pgoal pr f in
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment