diff --git a/compiler/heptagon/main/hept_compiler.ml b/compiler/heptagon/main/hept_compiler.ml index 1484d9a..7894ef2 100644 --- a/compiler/heptagon/main/hept_compiler.ml +++ b/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 diff --git a/compiler/heptagon/transformations/inline.ml b/compiler/heptagon/transformations/inline.ml index ba49b28..1a6857f 100644 --- a/compiler/heptagon/transformations/inline.ml +++ b/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 = diff --git a/compiler/main/heptc.ml b/compiler/main/heptc.ml index a063f94..77c65a6 100644 --- a/compiler/main/heptc.ml +++ b/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; diff --git a/compiler/utilities/global/compiler_utils.ml b/compiler/utilities/global/compiler_utils.ml index d377458..f358c70 100644 --- a/compiler/utilities/global/compiler_utils.ml +++ b/compiler/utilities/global/compiler_utils.ml @@ -75,6 +75,7 @@ and doc_object_file = "\t\tOnly generate a .epo object file" and doc_sim = "\t\tCreate simulation for 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 = "\tGenerate code in language \n\t\t\t(with =c," ^ " java or z3z)" diff --git a/compiler/utilities/misc.ml b/compiler/utilities/misc.ml index b5f4886..b191a77 100644 --- a/compiler/utilities/misc.ml +++ b/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";; diff --git a/compiler/utilities/misc.mli b/compiler/utilities/misc.mli index b5c08ff..909558b 100644 --- a/compiler/utilities/misc.mli +++ b/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