Commit 2ea64b0a authored by Mário Pereira's avatar Mário Pereira Committed by Guillaume Melquiond
Browse files

Extraction:

 . Moved [ity_affected], [pv_affected], and [pvs_affected] from src/mlw/vc.ml to
   src/mlw/ity.ml. These are also declared in src/mlw/ity.mli;

 . the test for conflicting reads and writes effects now uses the [pvs_affected]
   function.
parent 41fe3f5a
......@@ -610,10 +610,11 @@ module Transform = struct
open Mltree
let no_reads_writes_conflict spv spv_mreg =
let is_not_write {pv_ity = ity} = match ity.ity_node with
| Ityreg rho -> not (Mreg.mem rho spv_mreg)
| _ -> true in
Spv.for_all is_not_write spv
(* let is_not_write {pv_ity = ity} = match ity.ity_node with
* | Ityreg rho -> not (Mreg.mem rho spv_mreg)
* | _ -> true in
* Spv.for_all is_not_write spv *)
Spv.is_empty (pvs_affected spv_mreg spv)
let mk_list_eb ebl f =
let mk_acc e (e_acc, s_acc) =
......
......@@ -1231,6 +1231,17 @@ let eff_escape eff ity =
Spv.fold add_fd fs esc in
Mreg.fold add_write eff.eff_writes esc
(* affected program variables by some writes effect *)
let ity_affected wr ity =
Util.any ity_rch_fold (Mreg.contains wr) ity
let pv_affected wr v = ity_affected wr v.pv_ity
let pvs_affected wr pvs =
if Mreg.is_empty wr then Spv.empty
else Spv.filter (pv_affected wr) pvs
(** specification *)
type pre = term (* precondition: pre_fmla *)
......
......@@ -399,6 +399,18 @@ val mask_adjust : effect -> ity -> mask -> mask
val eff_escape : effect -> ity -> Sity.t
val ity_affected : 'a Mreg.t -> ity -> bool
(** [ity_affected wr ity] returns [true] if the regions of [ity] are contained
in the effect described by [wr]. *)
val pv_affected : 'a Mreg.t -> pvsymbol -> bool
(** [pv_affected wr pv] returns [true] if the regions of [pv] are contained in
the effect described by [wr]. *)
val pvs_affected : 'a Mreg.t -> Spv.t -> Spv.t
(** [pvs_affected wr pvs] returns the set of pvsymbols from [pvs] whose regions
are contained in the effect described by [wr]. *)
(** {2 Computation types (higher-order types with effects)} *)
type pre = term (** precondition: pre_fmla *)
......
......@@ -228,17 +228,6 @@ let sp_let v t sp rd =
if Spv.mem v rd then sp_and (t_equ (t_var v.pv_vs) t) sp else
t_let_close_simp v.pv_vs t sp
(* affected program variables *)
let ity_affected wr ity =
Util.any ity_rch_fold (Mreg.contains wr) ity
let pv_affected wr v = ity_affected wr v.pv_ity
let pvs_affected wr pvs =
if Mreg.is_empty wr then Spv.empty
else Spv.filter (pv_affected wr) pvs
(* variant decrease preconditions *)
let decrease_alg env loc old_t t =
......
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