diff --git a/compiler/heptagon/main/hept_compiler.ml b/compiler/heptagon/main/hept_compiler.ml index 3f45d1a..c5fd40b 100644 --- a/compiler/heptagon/main/hept_compiler.ml +++ b/compiler/heptagon/main/hept_compiler.ml @@ -30,9 +30,7 @@ let compile_program p = let p = pass "Completion" true Completion.program p pp in (* Inlining *) - let p = - let call_inline_pass = (List.length !inline > 0) || !flatten in - pass "Inlining" call_inline_pass Inline.program p pp in + let p = pass "Inlining" true Inline.program p pp in (* Automata *) let p = pass "Automata" true Automata.program p pp in diff --git a/compiler/heptagon/parsing/hept_parser.mly b/compiler/heptagon/parsing/hept_parser.mly index 517e1df..d726cd7 100644 --- a/compiler/heptagon/parsing/hept_parser.mly +++ b/compiler/heptagon/parsing/hept_parser.mly @@ -463,6 +463,7 @@ node_name: merge_handlers: | hs=nonempty_list(merge_handler) { hs } + | e1=simple_exp e2=simple_exp { [(Q Initial.ptrue, e1);(Q Initial.pfalse, e2)] } merge_handler: | LPAREN c=constructor_or_bool ARROW e=exp RPAREN { (c,e) } diff --git a/compiler/heptagon/transformations/inline.ml b/compiler/heptagon/transformations/inline.ml index 1bd0949..994ee7d 100644 --- a/compiler/heptagon/transformations/inline.ml +++ b/compiler/heptagon/transformations/inline.ml @@ -58,7 +58,9 @@ let exp funs (env, newvars, newequs) exp = (Hept_printer.iterator_to_string it) (fullname nn); (exp, (env, newvars, newequs)) - | Eapp ({ a_op = (Enode nn | Efun nn); } as op, argl, rso) when to_be_inlined nn -> + | Eapp ({ a_op = (Enode nn | Efun nn); + a_unsafe = false; (* Unsafe can't be inlined *) + a_inlined = inlined } as op, argl, rso) when inlined || to_be_inlined nn -> begin try let add_reset eq = match rso with | None -> eq