Commit 78270aaf authored by Andrei Paskevich's avatar Andrei Paskevich

Pdecl: add triggers to the invariant axiom

Let's see if this helps our provers to instantiate the axiom.
parent 12bb1ee3
......@@ -306,14 +306,16 @@ let mk_decl = mk_decl_meta []
let axiom_of_invariant itd =
let ts = itd.itd_its.its_ts in
let inv = t_and_simp_l itd.itd_invariant in
let ty = ty_app ts (List.map ty_var ts.ts_args) in
let u = create_vsymbol (id_fresh "self") ty in
let tl = [t_var u] in
let add_fd sbs s = let pj = ls_of_rs s in
Mvs.add (fd_of_rs s).pv_vs (t_app pj tl pj.ls_value) sbs in
let sbs = List.fold_left add_fd Mvs.empty itd.itd_fields in
let inv = t_subst sbs (t_and_simp_l itd.itd_invariant) in
t_forall_close [u] [] inv
let sbs = Mvs.set_inter sbs (t_freevars Mvs.empty inv) in
let trl = Mvs.fold (fun _ t trl -> [t] :: trl) sbs [] in
t_forall_close [u] trl (t_subst sbs inv)
let create_type_decl dl =
if dl = [] then invalid_arg "Pdecl.create_type_decl";
......
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