diff --git a/compiler/heptagon/heptagon.ml b/compiler/heptagon/heptagon.ml index 4cd3924..7f5bc0d 100644 --- a/compiler/heptagon/heptagon.ml +++ b/compiler/heptagon/heptagon.ml @@ -52,7 +52,8 @@ and desc = and app = { a_op : op; a_params : static_exp list; - a_unsafe : bool } + a_unsafe : bool; + a_inlined : bool } and op = | Eequal @@ -194,8 +195,8 @@ let mk_exp desc ?(ct_annot = Clocks.invalid_clock) ?(loc = no_location) ty = { e_desc = desc; e_ty = ty; e_ct_annot = ct_annot; e_base_ck = Cbase; e_loc = loc; } -let mk_app ?(params=[]) ?(unsafe=false) op = - { a_op = op; a_params = params; a_unsafe = unsafe } +let mk_app ?(params=[]) ?(unsafe=false) ?(inlined=false) op = + { a_op = op; a_params = params; a_unsafe = unsafe; a_inlined = inlined } let mk_op_app ?(params=[]) ?(unsafe=false) ?(reset=None) op args = Eapp(mk_app ~params:params ~unsafe:unsafe op, args, reset) diff --git a/compiler/heptagon/parsing/hept_lexer.mll b/compiler/heptagon/parsing/hept_lexer.mll index e370f0d..7ad7845 100644 --- a/compiler/heptagon/parsing/hept_lexer.mll +++ b/compiler/heptagon/parsing/hept_lexer.mll @@ -53,6 +53,7 @@ List.iter (fun (str,tok) -> Hashtbl.add keyword_table str tok) [ "assume", ASSUME; "enforce", ENFORCE; "with", WITH; + "inlined",INLINED; "when", WHEN; "merge", MERGE; "map", MAP; diff --git a/compiler/heptagon/parsing/hept_parser.mly b/compiler/heptagon/parsing/hept_parser.mly index e3ad86f..6ffcb93 100644 --- a/compiler/heptagon/parsing/hept_parser.mly +++ b/compiler/heptagon/parsing/hept_parser.mly @@ -39,6 +39,7 @@ open Hept_parsetree %token ASSUME %token ENFORCE %token WITH +%token INLINED %token WHEN MERGE %token POWER %token LBRACKET LBRACKETGREATER @@ -411,6 +412,9 @@ _simple_exp: /* TODO : conflict with Eselect_dyn and or const*/ ; +node_name: + | q=qualname c=call_params { mk_app (Enode q) c false } + | INLINED q=qualname c=call_params { mk_app (Enode q) c true } merge_handlers: | hs=nonempty_list(merge_handler) { hs } @@ -426,8 +430,8 @@ _exp: | PRE exp { Epre (None, $2) } /* node call*/ - | n=qualname p=call_params LPAREN args=exps RPAREN - { Eapp(mk_app (Enode n) p , args) } + | n=node_name LPAREN args=exps RPAREN + { Eapp(n, args) } | NOT exp { mk_op_call "not" [$2] } | exp INFIX4 exp diff --git a/compiler/heptagon/parsing/hept_parsetree.ml b/compiler/heptagon/parsing/hept_parsetree.ml index f567ddb..afeab5a 100644 --- a/compiler/heptagon/parsing/hept_parsetree.ml +++ b/compiler/heptagon/parsing/hept_parsetree.ml @@ -77,7 +77,7 @@ and edesc = | Ewhen of exp * constructor_name * var_name | Emerge of var_name * (constructor_name * exp) list -and app = { a_op: op; a_params: exp list; } +and app = { a_op: op; a_params: exp list; a_inlined: bool } and op = | Eequal @@ -219,17 +219,17 @@ and interface_desc = let mk_exp desc ?(ct_annot = Clocks.invalid_clock) loc = { e_desc = desc; e_ct_annot = ct_annot; e_loc = loc } -let mk_app op params = - { a_op = op; a_params = params; } +let mk_app op params inlined = + { a_op = op; a_params = params; a_inlined = inlined } -let mk_call ?(params=[]) op exps = - Eapp (mk_app op params, exps) +let mk_call ?(params=[]) ?(inlined=false) op exps = + Eapp (mk_app op params inlined, exps) let mk_op_call ?(params=[]) s exps = mk_call ~params:params (Efun (Q (Names.pervasives_qn s))) exps let mk_iterator_call it ln params n pexps exps = - Eiterator (it, mk_app (Enode ln) params, n, pexps, exps) + Eiterator (it, mk_app (Enode ln) params false, n, pexps, exps) let mk_static_exp desc loc = { se_desc = desc; se_loc = loc } diff --git a/compiler/heptagon/parsing/hept_scoping.ml b/compiler/heptagon/parsing/hept_scoping.ml index 61ad4e6..1f5b56c 100644 --- a/compiler/heptagon/parsing/hept_scoping.ml +++ b/compiler/heptagon/parsing/hept_scoping.ml @@ -244,10 +244,10 @@ and translate_desc loc env = function List.map (fun (f,e) -> qualify_field f, translate_exp env e) f_e_list in Heptagon.Estruct f_e_list - | Eapp ({ a_op = op; a_params = params; }, e_list) -> + | Eapp ({ a_op = op; a_params = params; a_inlined = inl }, e_list) -> let e_list = List.map (translate_exp env) e_list in let params = List.map (expect_static_exp) params in - let app = Heptagon.mk_app ~params:params (translate_op op) in + let app = Heptagon.mk_op ~params:params ~inlined:inl (translate_op op) in Heptagon.Eapp (app, e_list, None) | Eiterator (it, { a_op = op; a_params = params }, n, pe_list, e_list) ->