Inlining pass added. Use with -inline.

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
 

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

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

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;

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 = "<node>\t\tInsert run-time assertions for boolean node <node>"
+and doc_inline = "<node>\t\tInline node <node>"
 
 let errmsg = "Options are:"
 

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";;
 

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