Commit 22780e82 authored by Andrei Paskevich's avatar Andrei Paskevich

Vc: asymmetric "and" for chains of pre-/post-/invariant goals

parent 78270aaf
......@@ -333,7 +333,7 @@ let add_var kn pins vl v =
Mls.add (ls_of_rs f) (v, down ty) m, mv in
let pjs, mv = List.fold_left add_field
(Mls.empty, Mvs.empty) d.itd_fields in
let inv = t_ty_subst sbs mv (t_and_l d.itd_invariant) in
let inv = t_ty_subst sbs mv (t_and_asym_l d.itd_invariant) in
let pin = {p_vars = pjs; p_inv = inv} in
let n = new_index () in
rp := Mint.add n pin !rp;
......@@ -260,14 +260,14 @@ let renew_oldies o2v =
(* convert user specifications into goals (wp) and premises (sp) *)
let wp_of_inv loc lab expl pl =
t_and_l ( (vc_expl loc lab expl) pl)
t_and_asym_l ( (vc_expl loc lab expl) pl)
let wp_of_pre loc lab pl = wp_of_inv loc lab expl_pre pl
let wp_of_post expl ity ql =
let v = res_of_post ity ql in let t = t_var v.pv_vs in
let make q = vc_expl None Slab.empty expl (open_post_with t q) in
v, t_and_l ( make ql)
v, t_and_asym_l ( make ql)
let push_stop loc lab expl f =
let rec push f = match f.t_node with
Markdown is supported
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment