Commit 4ead4697 authored by Mário Pereira's avatar Mário Pereira

Code extraction

Avoid inlining proxy variables whenever there are conflicting effects
parent 7b218458
......@@ -834,8 +834,11 @@ module Transform = struct
open ML
let conflict_reads_writes spv spv_mreg =
Mreg.exists (fun _ v -> not (Spv.is_empty (Spv.diff v spv))) spv_mreg
let no_reads_writes_conflict spv spv_mreg =
let is_reg {pv_ity = ity} = match ity.ity_node with
| Ityreg rho -> not (Mreg.mem rho spv_mreg)
| _ -> true in
Spv.for_all is_reg spv
type subst = expr Mpv.t
......@@ -848,12 +851,12 @@ module Transform = struct
let mk e_node = { e with e_node = e_node } in
let add_subst pv e1 e2 = expr info (Mpv.add pv e1 subst) e2 in
match e.e_node with
| Evar pv ->
(try Mpv.find pv subst, Spv.singleton pv with Not_found -> e, Spv.empty)
| Evar pv -> begin try Mpv.find pv subst, Spv.singleton pv
with Not_found -> e, Spv.empty end
| Elet (Lvar (pv, ({e_effect = eff1} as e1)), ({e_effect = eff2} as e2))
when Slab.mem Expr.proxy_label pv.pv_vs.vs_name.id_label &&
eff_pure eff1 &&
not (conflict_reads_writes eff1.eff_reads eff2.eff_writes) ->
no_reads_writes_conflict eff1.eff_reads eff2.eff_writes ->
let e1, s1 = expr info subst e1 in
let e2, s2 = add_subst pv e1 e2 in
let s_union = Spv.union s1 s2 in
......@@ -868,10 +871,17 @@ module Transform = struct
let e_app, spv = mk_list_eb el (expr info subst) in
mk (Eapp (rs, e_app)), spv
| Efun (vl, e) ->
(* We begin the inlining of proxy variables in an [Efun]
with the empty substituion. This keeps A-normal lets,
preventing undiserable capture of variables insinde. *)
let e, spv = expr info Mpv.empty e in
(* For now, we accept to inline constants and constructors
with zero arguments inside a [Efun]. *)
let p _k e = match e.e_node with
| Econst _ -> true
| Eapp (rs, []) when Translate.isconstructor info rs -> true
| _ -> false in
let restrict_subst = Mpv.filter p subst in
(* We begin the inlining of proxy variables in an [Efun] with a
restricted substituion. This keeps some proxy lets, preventing
undiserable captures inside the [Efun] expression. *)
let e, spv = expr info restrict_subst e in
mk (Efun (vl, e)), spv
| Eif (e1, e2, e3) ->
let e1, s1 = expr info subst e1 in
......@@ -939,8 +949,7 @@ module Transform = struct
let pdecl info = function
| Dtype _ | Dexn _ | Dclone _ as d -> d
| Dlet def ->
(* for top-level symbols we can forget
the set of inlined variables *)
(* for top-level symbols we can forget the set of inlined variables *)
let e, _ = let_def info Mpv.empty def in
Dlet e
......
......@@ -581,6 +581,11 @@ let ls_of_rs rs = match rs.rs_logic with
| _ -> assert false
*)
let clone_type_record cl s s' =
(* check if fields from former type are also declared in the new type *)
cl.ts_table <- Mts.add s.its_ts s' cl.ts_table
let clone_type_decl inst cl tdl =
let def =
List.fold_left (fun m d -> Mits.add d.itd_its d m) Mits.empty tdl in
......@@ -614,12 +619,12 @@ let clone_type_decl inst cl tdl =
raise (BadInstance id);
if not (its_pure s && its_pure s') then raise (BadInstance id);
(* TODO: accept refinement of private records *)
cl.ts_table <- Mts.add s.its_ts s' cl.ts_table
clone_type_record cl s s'
| None -> begin match Mts.find_opt ts inst.mi_ty with
| Some ity ->
let stv = Stv.of_list ts.ts_args in
if not (Stv.subset (ity_freevars Stv.empty ity) stv &&
its_pure s && ity_immutable ity) then raise (BadInstance id);
its_pure s && ity_immutable ity) then raise (BadInstance id);
cl.ty_table <- Mts.add ts ity cl.ty_table
| None -> assert false end end;
Hits.add htd s None;
......@@ -892,6 +897,7 @@ let clone_pdecl inst cl uc d = match d.pd_node with
if tdl = [] then List.fold_left add_vc uc vcl else
add_pdecl ~vc:false uc (create_type_decl tdl)
| PDlet (LDsym (rs, c)) when Mrs.mem rs inst.mi_rs ->
(* only refine [val] symbols *)
if c.c_node <> Cany then raise (BadInstance rs.rs_name);
let kind = match rs.rs_logic with
| RLnone -> RKnone
......
......@@ -6,8 +6,8 @@ open Test
let (=) = Z.equal
let b42 = Z.of_int 42
let () = assert (test_int () = b42)
let () = assert (test_int63 () = b42)
let () = assert (test_int () = b42)
let () = assert (test_int63 () = b42)
let () = assert (test_ref () = b42)
let () = assert (test_array () = b42)
......
......@@ -244,9 +244,29 @@ module TestExtraction
let test2 () raises { AssertFailure }
= ocaml_assert (of_int 1 + of_int 1 = of_int 2)
(* testing proxy-variables inlining mechanism inside a lambda *)
let test3 () raises { AssertFailure }
= let i = ref (of_int 42) in
let c = Cons !i in
i := (of_int 0);
let c = c Nil in
ocaml_assert (match c with Cons x _ -> x = of_int 42 | _ -> true end)
(* testing proxy-variables inlining with conflicting effects *)
let test4 () raises { AssertFailure }
= let f (x y: int63) raises { AssertFailure }
= ocaml_assert (y = of_int 42);
x + y in
let i = ref (of_int 42) in
let res = f (i := of_int 0; !i) !i in
ocaml_assert (!i = of_int 0);
ocaml_assert (res = of_int 42)
let main () raises { AssertFailure } =
test1 ();
test2 ();
test3 ();
test4 ();
test_parallel_assign ()
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