From 13c0b591dccb95622174628fa6899385e37b3156 Mon Sep 17 00:00:00 2001 From: Raphael Rieu-Helft Date: Mon, 8 Oct 2018 14:47:35 +0200 Subject: [PATCH] Extraction: inline more proxy variables --- src/mlw/cakeml_printer.ml | 4 ++-- src/mlw/compile.ml | 25 +++++++++++++++++++++---- src/mlw/cprinter.ml | 5 +++-- src/mlw/mlinterp.ml | 4 ++-- src/mlw/mltree.ml | 2 +- src/mlw/ocaml_printer.ml | 4 ++-- 6 files changed, 31 insertions(+), 13 deletions(-) diff --git a/src/mlw/cakeml_printer.ml b/src/mlw/cakeml_printer.ml index c3ad49ad4..c0c233edf 100644 --- a/src/mlw/cakeml_printer.ml +++ b/src/mlw/cakeml_printer.ml @@ -268,10 +268,10 @@ module Print = struct (print_expr info) e (print_list_next newline (print_branch info)) bl (print_list_next newline (print_xbranch true info)) xl | Eassign al -> - let assign fmt (rho, rs, pv) = + let assign fmt (rho, rs, e) = fprintf fmt "@[%a.%a <-@ %a@]" (print_lident info) (pv_name rho) (print_lident info) rs.rs_name - (print_lident info) (pv_name pv) in + (print_expr info) e in begin match al with | [] -> assert false | [a] -> assign fmt a | al -> fprintf fmt "@[(%a)]" (print_list semi assign) al end diff --git a/src/mlw/compile.ml b/src/mlw/compile.ml index a92f8f778..b90c4bbe4 100644 --- a/src/mlw/compile.ml +++ b/src/mlw/compile.ml @@ -408,6 +408,8 @@ module Translate = struct | Eassign al -> let rm_ghost (_, rs, _) = not (rs_ghost rs) in let al = List.filter rm_ghost al in + let e_of_var pv = ML.e_var pv (ML.I pv.pv_ity) MaskVisible eff attrs in + let al = List.map (fun (pv1, rs, pv2) -> (pv1, rs, e_of_var pv2)) al in ML.e_assign al (ML.I e.e_ity) mask eff attrs | Ematch (e1, bl, xl) when e_ghost e1 -> assert (Mxs.is_empty xl); (* Expr ensures this for the time being *) @@ -616,6 +618,15 @@ module Transform = struct * Spv.for_all is_not_write spv *) Spv.is_empty (pvs_affected spv_mreg spv) + let rec can_inline ({e_effect = eff1} as e1) ({e_effect = eff2} as e2) = + match e2.e_node with + | Evar _ | Eapp _ | Eassign _ | Econst _ -> true + | Eblock el -> List.for_all (fun e -> can_inline e1 e) el + | Elet (Lvar (_, {e_effect = eff1'}), e2') -> + no_reads_writes_conflict eff1.eff_reads eff1'.eff_writes + && can_inline e1 e2' + | _ -> no_reads_writes_conflict eff1.eff_reads eff2.eff_writes + let mk_list_eb ebl f = let mk_acc e (e_acc, s_acc) = let e, s = f e in e::e_acc, Spv.union s s_acc in @@ -627,10 +638,10 @@ module Transform = struct match e.e_node with | 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)) + | Elet (Lvar (pv, ({e_effect = eff1} as e1)), e2) when Sattr.mem Expr.proxy_attr pv.pv_vs.vs_name.id_attrs && eff_pure eff1 && - no_reads_writes_conflict eff1.eff_reads eff2.eff_writes -> + can_inline e1 e2 -> 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 @@ -690,8 +701,14 @@ module Transform = struct | Eraise (exn, Some e) -> let e, spv = expr info subst e in mk (Eraise (exn, Some e)), spv - | Eassign _al -> - e, Spv.empty + | Eassign al -> + let al, s = + List.fold_left + (fun (accl, spv) (pv,rs,e) -> + let e, s = expr info subst e in + ((pv, rs, e)::accl, Spv.union spv s)) + ([], Spv.empty) al in + mk (Eassign (List.rev al)), s | Econst _ | Eabsurd | Ehole | Eany _ -> e, Spv.empty | Eignore e -> let e, spv = expr info subst e in diff --git a/src/mlw/cprinter.ml b/src/mlw/cprinter.ml index 51d464e7b..2fb8c1477 100644 --- a/src/mlw/cprinter.ml +++ b/src/mlw/cprinter.ml @@ -1028,7 +1028,7 @@ module MLToC = struct d@defs, C.(Sseq(Sseq(s,assigns), Sblock b)) | Ematch _ -> raise (Unsupported "pattern matching") | Eabsurd -> assert false - | Eassign ([pv, ({rs_field = Some _} as rs), v]) -> + | Eassign ([pv, ({rs_field = Some _} as rs), e2]) -> let t = match query_syntax info.syntax rs.rs_name with | Some s -> @@ -1047,7 +1047,8 @@ module MLToC = struct in C.Esyntax(s,ty_of_ty info rty, rtyargs, params) | None -> raise (Unsupported ("assign not in driver")) in - [], C.(Sexpr(Ebinop(Bassign, t, C.Evar v.pv_vs.vs_name))) + let v = expr info env e2 in + [], C.(Sexpr(Ebinop(Bassign, t, simplify_expr v))) | Eassign _ -> raise (Unsupported "assign") | Ehole | Eany _ -> assert false | Eexn (_,_,e) -> expr info env e diff --git a/src/mlw/mlinterp.ml b/src/mlw/mlinterp.ml index 9ec87b1d2..7419c9917 100644 --- a/src/mlw/mlinterp.ml +++ b/src/mlw/mlinterp.ml @@ -696,9 +696,9 @@ let rec interp_expr info (e:Mltree.expr) : value = end | Eassign l -> List.iter - (fun (pvs, rs, v) -> + (fun (pvs, rs, e) -> let fld = fd_of_rs rs in - let value = get v info in + let value = interp_expr info e in match get pvs info with | Vconstr(c, args) -> let rec aux cargs args = diff --git a/src/mlw/mltree.ml b/src/mlw/mltree.ml index 3c5dc72a4..6c72d0c8b 100644 --- a/src/mlw/mltree.ml +++ b/src/mlw/mltree.ml @@ -54,7 +54,7 @@ and expr_node = | Efun of var list * expr | Elet of let_def * expr | Eif of expr * expr * expr - | Eassign of (pvsymbol * rsymbol * pvsymbol) list + | Eassign of (pvsymbol * rsymbol * expr) list | Ematch of expr * reg_branch list * exn_branch list | Eblock of expr list | Ewhile of expr * expr diff --git a/src/mlw/ocaml_printer.ml b/src/mlw/ocaml_printer.ml index 7f983c2a1..94534c7bb 100644 --- a/src/mlw/ocaml_printer.ml +++ b/src/mlw/ocaml_printer.ml @@ -461,10 +461,10 @@ module Print = struct (protect_on paren "begin match @[%a@] with@\n@[%a@]@\nend") (print_expr info) e (print_list newline (print_branch info)) pl | Eassign al -> - let assign fmt (rho, rs, pv) = + let assign fmt (rho, rs, e) = fprintf fmt "@[%a.%a <-@ %a@]" (print_lident info) (pv_name rho) (print_lident info) rs.rs_name - (print_lident info) (pv_name pv) in + (print_expr info) e in begin match al with | [] -> assert false | [a] -> assign fmt a | al -> fprintf fmt "@[begin %a end@]" (print_list semi assign) al end -- GitLab