diff --git a/compiler/heptagon/main/hept_compiler.ml b/compiler/heptagon/main/hept_compiler.ml index a773a80..1484d9a 100644 --- a/compiler/heptagon/main/hept_compiler.ml +++ b/compiler/heptagon/main/hept_compiler.ml @@ -49,6 +49,8 @@ let compile_impl pp p = (* Completion of partial definitions *) let p = do_pass Completion.program "Completion" p pp true in + let p = do_pass Inline.program "Inlining" p pp (List.length !inline > 0) in + (* Automata *) let p = do_pass Automata.program "Automata" p pp true in diff --git a/compiler/heptagon/transformations/inline.ml b/compiler/heptagon/transformations/inline.ml new file mode 100644 index 0000000..ba49b28 --- /dev/null +++ b/compiler/heptagon/transformations/inline.ml @@ -0,0 +1,114 @@ +(**************************************************************************) +(* *) +(* Heptagon *) +(* *) +(* Author : Marc Pouzet *) +(* Organization : Demons, LRI, University of Paris-Sud, Orsay *) +(* *) +(**************************************************************************) + +open Misc +open Ident +open Signature +open Types +open Names +open Heptagon +open Hept_mapfold + +let to_be_inlined s = List.mem s !Misc.inline + +let mk_unique_node nd = + let mk_bind vd = + let id = Ident.fresh (Ident.sourcename vd.v_ident) in + (vd.v_ident, { vd with v_ident = id; }) in + let subst = List.map mk_bind (nd.n_local @ nd.n_input @ nd.n_output) in + + let subst_var_dec funs () vd = + ({ vd with v_ident = (List.assoc vd.v_ident subst).v_ident; }, ()) in + let subst_edesc funs () ed = match ed with + | Evar vn -> (Evar (List.assoc vn subst).v_ident, ()) + | _ -> raise Fallback in + let subst_eqdesc funs () eqd = + let (eqd, ()) = Hept_mapfold.eqdesc funs () eqd in + match eqd with + | Eeq (pat, e) -> + let rec subst_pat pat = match pat with + | Evarpat vn -> Evarpat (try (List.assoc vn subst).v_ident + with Not_found -> vn) + | Etuplepat patl -> Etuplepat (List.map subst_pat patl) in + (Eeq (subst_pat pat, e), ()) + | _ -> raise Fallback in + + let funs = { defaults with + var_dec = subst_var_dec; + eqdesc = subst_eqdesc; + edesc = subst_edesc; } in + fst (Hept_mapfold.node_dec funs () nd) + +let exp funs (env, newvars, newequs) exp = match exp.e_desc with + | Eapp ({ a_op = Enode nn; } as op, argl, rso) when to_be_inlined nn -> + let add_reset eq = match rso with + | None -> eq + | Some x -> mk_equation ~statefull:false (Ereset ([eq], x)) in + + let ni = mk_unique_node (env nn) in + + let static_subst = + List.combine (List.map (fun p -> Name p.p_name) ni.n_params) + op.a_params in + + (* Perform [static_exp] substitution. *) + let ni = + let apply_sexp_subst_sexp funs () sexp = match sexp.se_desc with + | Svar s -> ((try List.assoc s static_subst + with Not_found -> sexp), ()) + | _ -> Global_mapfold.static_exp funs () sexp in + + let funs = + { defaults with global_funs = + { Global_mapfold.defaults with Global_mapfold.static_exp = + apply_sexp_subst_sexp; }; } in + + fst (Hept_mapfold.node_dec funs () ni) in + + let mk_input_equ vd e = + mk_equation ~statefull:false (Eeq (Evarpat vd.v_ident, e)) in + let mk_output_exp vd = mk_exp (Evar vd.v_ident) vd.v_type in + + let newvars = ni.n_input @ ni.n_local @ ni.n_output @ newvars + and newequs = + List.map2 mk_input_equ ni.n_input argl + @ List.map add_reset ni.n_equs + @ newequs in + + (* For clocking reason we cannot create 1-tuples. *) + let res_e = match ni.n_output with + | [o] -> mk_output_exp o + | _ -> + mk_exp (Eapp ({ op with a_op = Etuple; }, + List.map mk_output_exp ni.n_output, None)) exp.e_ty in + (res_e, (env, newvars, newequs)) + | _ -> Hept_mapfold.exp funs (env, newvars, newequs) exp + +let block funs (env, newvars, newequs) blk = + let (block, (env, newvars, newequs)) = + Hept_mapfold.block funs (env, newvars, newequs) blk in + ({ blk with b_local = newvars @ blk.b_local; b_equs = newequs @ blk.b_equs; }, + (env, [], [])) + +let node_dec funs (env, newvars, newequs) nd = + let nd, (env, newvars, newequs) = + Hept_mapfold.node_dec funs (env, newvars, newequs) nd in + ({ nd with n_local = newvars @ nd.n_local; n_equs = newequs @ nd.n_equs; }, + (env, [], [])) + +let program p = + let env n = + let mk_ln s = Modname { qual = p.p_modname; id = s; } in + List.find (fun nd -> mk_ln nd.n_name = n) p.p_nodes in + let funs = + { defaults with exp = exp; block = block; node_dec = node_dec; eq = eq; } in + let (p, (_, newvars, newequs)) = Hept_mapfold.program funs (env, [], []) p in + assert (newvars = []); + assert (newequs = []); + p diff --git a/compiler/main/hept2mls.ml b/compiler/main/hept2mls.ml index 90f2a80..d21393f 100644 --- a/compiler/main/hept2mls.ml +++ b/compiler/main/hept2mls.ml @@ -64,7 +64,7 @@ struct let con env x e = let rec conrec env = match env with - | Eempty -> Format.printf "%s\n" (name x); assert false + | Eempty -> Printf.eprintf "%s\n" (name x); assert false | Eon(env, tag, name) -> let e, ck = conrec env in let ck_tag_name = Con(ck, tag, name) in diff --git a/compiler/main/heptc.ml b/compiler/main/heptc.ml index b37ba08..a063f94 100644 --- a/compiler/main/heptc.ml +++ b/compiler/main/heptc.ml @@ -80,6 +80,7 @@ let main () = "-stdlib", Arg.String set_stdlib, doc_stdlib; "-c", Arg.Set create_object_file, doc_object_file; "-s", Arg.String set_simulation_node, doc_sim; + "-inline", Arg.String add_inlined_node, doc_inline; "-assert", Arg.String add_assert, doc_assert; "-nopervasives", Arg.Unit set_no_pervasives, doc_no_pervasives; "-target", Arg.String add_target_language, doc_target; diff --git a/compiler/utilities/global/compiler_utils.ml b/compiler/utilities/global/compiler_utils.ml index 3ff7bc4..d377458 100644 --- a/compiler/utilities/global/compiler_utils.ml +++ b/compiler/utilities/global/compiler_utils.ml @@ -84,6 +84,7 @@ and doc_target_path = ^ " cleaned)" and doc_noinit = "\t\tDisable initialization analysis" and doc_assert = "\t\tInsert run-time assertions for boolean node " +and doc_inline = "\t\tInline node " let errmsg = "Options are:" diff --git a/compiler/utilities/misc.ml b/compiler/utilities/misc.ml index 1c53e99..b5f4886 100644 --- a/compiler/utilities/misc.ml +++ b/compiler/utilities/misc.ml @@ -81,6 +81,10 @@ let cse = ref false let tomato = ref false +let inline = ref [] + +let add_inlined_node s = inline := Names.mk_longname s :: !inline + (* Backward compatibility *) let set_sigali () = add_target_language "z3z";; diff --git a/compiler/utilities/misc.mli b/compiler/utilities/misc.mli index 379c1c5..b5c08ff 100644 --- a/compiler/utilities/misc.mli +++ b/compiler/utilities/misc.mli @@ -83,6 +83,12 @@ val cse : bool ref (* Automata minimization *) val tomato : bool ref +(* List of nodes to inline *) +val inline : Names.longname list ref + +(* Add a new node name to the list of nodes to inline. *) +val add_inlined_node : string -> unit + (* Z/3Z back-end mode *) val set_sigali : unit -> unit