Added an option for global inlining (-flatten).

compiler/heptagon/main/hept_compiler.ml

@@ -49,7 +49,9 @@ 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
+  let p =
+    let call_inline_pass = (List.length !inline > 0) || !Misc.flatten in
+    do_pass Inline.program "Inlining" p pp call_inline_pass in
 
   (* Automata *)
   let p = do_pass Automata.program "Automata" p pp true in

compiler/heptagon/transformations/inline.ml

@@ -15,7 +15,7 @@ open Names
 open Heptagon
 open Hept_mapfold
 
-let to_be_inlined s = List.mem s !Misc.inline
+let to_be_inlined s = !Misc.flatten || (List.mem s !Misc.inline)
 
 let mk_unique_node nd =
   let mk_bind vd =

compiler/main/heptc.ml

@@ -81,6 +81,7 @@ let main () =
         "-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;
+        "-flatten", Arg.Set flatten, doc_flatten;
         "-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

@@ -75,6 +75,7 @@ and doc_object_file = "\t\tOnly generate a .epo object file"
 and doc_sim = "<node>\t\tCreate simulation for node <node>"
 and doc_locate_stdlib = "\t\tLocate standard libray"
 and doc_no_pervasives = "\tDo not load the pervasives module"
+and doc_flatten = "\t\tInline everything."
 and doc_target =
   "<lang>\tGenerate code in language <lang>\n\t\t\t(with <lang>=c,"
   ^ " java or z3z)"

compiler/utilities/misc.ml

@@ -85,6 +85,8 @@ let inline = ref []
 
 let add_inlined_node s = inline := Names.mk_longname s :: !inline
 
+let flatten = ref false
+
 (* Backward compatibility *)
 let set_sigali () = add_target_language "z3z";;
 

compiler/utilities/misc.mli

@@ -85,9 +85,10 @@ 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
+(* Inline every node. *)
+val flatten : bool ref
 
 (* Z/3Z back-end mode *)
 val set_sigali : unit -> unit