Keyword "inlined" for nodes

Added a keyword "inlined": "inlined f(x)" is intended to
inline only this application. (not effective yet)

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)

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;

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

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 }

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) ->