Commit 557aa6ef authored by Andrei Paskevich's avatar Andrei Paskevich

whyml: remove "anonymous" regions from effects in psymbols

parent 92ad3c64
......@@ -53,7 +53,7 @@ let ps_equal : psymbol -> psymbol -> bool = (==)
let create_psymbol id vta vars = {
ps_name = id_register id;
ps_vta = vta;
ps_vta = vta_filter vars vta;
ps_vars = vars;
ps_subst = vars_freeze vars;
}
......
......@@ -588,6 +588,26 @@ let eff_full_inst s e =
eff_resets = Mreg.fold add_mreg e.eff_resets Mreg.empty;
}
let eff_filter vars e =
let rec check r vars =
Sreg.exists (occurs r) vars.vars_reg
and occurs r r' =
reg_equal r r' || check r r'.reg_ity.ity_vars
in
let check r = check r vars in
let reset r = function
| _ when not (check r) -> None
| Some u as v when check u -> Some v
| _ -> Some None
in
{ e with
eff_reads = Sreg.filter check e.eff_reads;
eff_writes = Sreg.filter check e.eff_writes;
eff_ghostr = Sreg.filter check e.eff_ghostr;
eff_ghostw = Sreg.filter check e.eff_ghostw;
eff_resets = Mreg.mapi_filter reset e.eff_resets;
}
(* program types *)
type vty_value = {
......@@ -690,6 +710,17 @@ and vty_full_inst s = function
| VTvalue vtv -> VTvalue (vtv_full_inst s vtv)
| VTarrow vta -> VTarrow (vta_full_inst s vta)
let vta_filter vars vta =
let vars = vars_union vars vta.vta_vars in
let rec filter a =
let vty = match a.vta_result with
| VTarrow a -> VTarrow (filter a)
| v -> v in
let effect = eff_filter vars a.vta_effect in
vty_arrow ~ghost:a.vta_ghost ~effect a.vta_arg vty
in
filter vta
(** THE FOLLOWING CODE MIGHT BE USEFUL LATER FOR WPgen *)
(*
(* program variables *)
......
......@@ -210,6 +210,8 @@ val eff_remove_raise : effect -> xsymbol -> effect
val eff_full_inst : ity_subst -> effect -> effect
val eff_filter : varset -> effect -> effect
(** program types *)
(* type of function arguments and values *)
......@@ -252,6 +254,10 @@ val vty_ghostify : vty -> vty
but also every type variable and every region in vta_effect *)
val vta_full_inst : ity_subst -> vty_arrow -> vty_arrow
(* remove from the given arrow every effect that is covered
neither by the arrow's vta_vars nor by the given varset *)
val vta_filter : varset -> vty_arrow -> vty_arrow
(** THE FOLLOWING CODE MIGHT BE USEFUL LATER FOR WPgen *)
(*
(* program variables *)
......
......@@ -31,7 +31,7 @@ module N
let u = {| f1 = z; f2 = Node x Nil |} in
let r = {| contents = {| u with f2 = Node one Nil |} |} in
x.contents <- one;
r (* zero *)
zero
end
(*
......
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