|
|
|
@ -68,6 +68,7 @@ open Hept_parsetree
|
|
|
|
|
%token ENFORCE
|
|
|
|
|
%token REACHABLE
|
|
|
|
|
%token ATTRACTIVE
|
|
|
|
|
%token ASYNC
|
|
|
|
|
%token WITH
|
|
|
|
|
%token WHEN WHENOT MERGE ON ONOT
|
|
|
|
|
%token INLINED
|
|
|
|
@ -525,6 +526,14 @@ 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 }
|
|
|
|
|
|
|
|
|
|
async_clock_args:
|
|
|
|
|
| const opt_comma {[$1]}
|
|
|
|
|
| const COMMA async_clock_args {$1 :: $3}
|
|
|
|
|
|
|
|
|
|
async_clock:
|
|
|
|
|
| n=IDENT LPAREN args=async_clock_args RPAREN
|
|
|
|
|
{ mk_ack n args }
|
|
|
|
|
|
|
|
|
|
merge_handlers:
|
|
|
|
|
| hs=nonempty_list(merge_handler) { hs }
|
|
|
|
|
| e1=simple_exp e2=simple_exp { [(Q Initial.ptrue, e1);(Q Initial.pfalse, e2)] }
|
|
|
|
@ -542,6 +551,9 @@ _exp:
|
|
|
|
|
/* node call*/
|
|
|
|
|
| n=node_name LPAREN args=exps RPAREN
|
|
|
|
|
{ Eapp(n, args) }
|
|
|
|
|
/* async node call */
|
|
|
|
|
| ASYNC q=qualname c=call_params LPAREN args=exps RPAREN ON ack=async_clock
|
|
|
|
|
{ Eapp(mk_app (Easync (q, ack)) c false, args) }
|
|
|
|
|
| SPLIT n=ident LPAREN e=exp RPAREN
|
|
|
|
|
{ Esplit(n, e) }
|
|
|
|
|
| REINIT LPAREN e1=exp COMMA e2=exp RPAREN
|
|
|
|
|