Commit 3a6a512c authored by Andrei Paskevich's avatar Andrei Paskevich

rename Mlw_ty.ity_inv to ity_has_inv

parent 44e81c0a
......@@ -255,9 +255,9 @@ let ity_subst_unsafe mv mr ity =
let ity_closed ity = Stv.is_empty ity.ity_vars.vars_tv
let ity_pure ity = Sreg.is_empty ity.ity_vars.vars_reg
let rec ity_inv ity = match ity.ity_node with
| Ityapp (its,_,_) -> its.its_inv || ity_any ity_inv ity
| _ -> ity_any ity_inv ity
let rec ity_has_inv ity = match ity.ity_node with
| Ityapp (its,_,_) -> its.its_inv || ity_any ity_has_inv ity
| _ -> ity_any ity_has_inv ity
let rec reg_fold fn vars acc =
let on_reg r acc = reg_fold fn r.reg_ity.ity_vars (fn r acc) in
......
......@@ -121,7 +121,7 @@ val its_clone : Theory.symbol_map -> itysymbol Mits.t * region Mreg.t
val ity_closed : ity -> bool
val ity_pure : ity -> bool
val ity_inv : ity -> bool
val ity_has_inv : ity -> bool
(* these functions attend the sub-regions *)
......
......@@ -1425,7 +1425,7 @@ let add_types ~wp uc tdl =
let mk_proj (regs,inv) (id,pty) =
let ity = parse pty in
let vtv = vty_value ity in
let inv = inv || ity_inv ity in
let inv = inv || ity_has_inv ity in
match id with
| None ->
let pv = create_pvsymbol (id_fresh "pj") vtv in
......@@ -1455,7 +1455,7 @@ let add_types ~wp uc tdl =
let mk_field (regs,inv) f =
let ghost = f.f_ghost in
let ity = parse f.f_pty in
let inv = inv || ity_inv ity in
let inv = inv || ity_has_inv ity in
let fid = Denv.create_user_id f.f_ident in
let regs,mut = if f.f_mutable then
let r = create_region fid ity in
......
......@@ -370,7 +370,7 @@ let ps_inv = Term.create_psymbol (id_fresh "inv")
let full_invariant lkm km vs ity =
let rec update vs { vtv_ity = ity } =
if not (ity_inv ity) then t_true else
if not (ity_has_inv ity) then t_true else
(* what is our current invariant? *)
let f = match ity.ity_node with
| Ityapp (its,_,_) when its.its_inv ->
......
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