Commit 2f75633a authored by Mário Pereira's avatar Mário Pereira

Pmodule: minor

parent e5dc233b
......@@ -577,7 +577,7 @@ let cl_save_rs cl s s' =
| RLnone, RLnone -> ()
| _ -> assert false
(* Mário: recovered this commented function *)
(* Mário: commented out this function *)
let ls_of_rs rs = match rs.rs_logic with
| RLls ls -> ls
| _ -> assert false
......@@ -777,7 +777,7 @@ let clone_cty cl sm ?(drop_decr=false) cty =
let reads = Spv.fold add_read (cty_reads cty) Spv.empty in
let reads = List.fold_right add_read cty.cty_args reads in
let reads = Spv.union reads (Mpv.domain olds) in
let add_write reg fs m =
let add_write reg fs m = (* add new mutable fields to functions effect *)
let add_fd fd s = Spv.add (Mpv.find_def fd fd cl.fd_table) s in
let reg' = Mreg.find_def reg reg cl.rn_table in
let smf_reg' = Spv.of_list reg'.reg_its.its_mfields in
......@@ -786,9 +786,6 @@ let clone_cty cl sm ?(drop_decr=false) cty =
let fs = Spv.fold add_fd fs Spv.empty in
Mreg.add (clone_reg cl reg) (Spv.union fs smf_diff) m in
let writes = Mreg.fold add_write cty.cty_effect.eff_writes Mreg.empty in
(* Mreg.iter (fun rho spv -> Format.eprintf "rho:%a@." print_reg rho; *)
(* Spv.iter (fun pv -> Format.eprintf "pv:%a@." print_pv pv) spv) *)
(* writes; *)
let add_reset reg s = Sreg.add (clone_reg cl reg) s in
let resets = Sreg.fold add_reset cty.cty_effect.eff_resets Sreg.empty in
let eff = eff_reset (eff_write reads writes) resets in
......
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