From 830f8e4bfa3e6502d8a9381be645993579fc58fc Mon Sep 17 00:00:00 2001
From: Tom Barthe <tom.barthe@ens-paris-saclay.fr>
Date: Sun, 20 Dec 2020 14:51:19 +0100
Subject: [PATCH] Add async call syntax to the parser

Warning: The code doesn't compile at this stage.
---
 compiler/heptagon/heptagon.ml               |  3 +++
 compiler/heptagon/parsing/hept_lexer.mll    |  1 +
 compiler/heptagon/parsing/hept_parser.mly   | 12 ++++++++++++
 compiler/heptagon/parsing/hept_parsetree.ml |  6 ++++++
 compiler/heptagon/parsing/hept_scoping.ml   |  1 +
 5 files changed, 23 insertions(+)

diff --git a/compiler/heptagon/heptagon.ml b/compiler/heptagon/heptagon.ml
index 4a1332e..4498b66 100644
--- a/compiler/heptagon/heptagon.ml
+++ b/compiler/heptagon/heptagon.ml
@@ -79,6 +79,7 @@ and op =
   | Etuple
   | Efun of fun_name
   | Enode of fun_name
+  | Easync of fun_name * ack
   | Eifthenelse
   | Earrow
   | Efield
@@ -93,6 +94,8 @@ and op =
   | Econcat
   | Ereinit
 
+and ack = { ack_name : string; ack_params : static_exp list }
+
 and pat =
   | Etuplepat of pat list
   | Evarpat of var_ident
diff --git a/compiler/heptagon/parsing/hept_lexer.mll b/compiler/heptagon/parsing/hept_lexer.mll
index c80c00e..24dd846 100644
--- a/compiler/heptagon/parsing/hept_lexer.mll
+++ b/compiler/heptagon/parsing/hept_lexer.mll
@@ -42,6 +42,7 @@ let keyword_table = ((Hashtbl.create 149) : (string, token) Hashtbl.t);;
 
 List.iter (fun (str,tok) -> Hashtbl.add keyword_table str tok) [
  "node", NODE;
+ "async", ASYNC;
  "fun", FUN;
  "returns", RETURNS;
  "var", VAR;
diff --git a/compiler/heptagon/parsing/hept_parser.mly b/compiler/heptagon/parsing/hept_parser.mly
index 8a936a6..8c4699a 100644
--- a/compiler/heptagon/parsing/hept_parser.mly
+++ b/compiler/heptagon/parsing/hept_parser.mly
@@ -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
diff --git a/compiler/heptagon/parsing/hept_parsetree.ml b/compiler/heptagon/parsing/hept_parsetree.ml
index 917205e..d492af3 100644
--- a/compiler/heptagon/parsing/hept_parsetree.ml
+++ b/compiler/heptagon/parsing/hept_parsetree.ml
@@ -113,6 +113,7 @@ and app = { a_op: op; a_params: exp list; a_inlined: bool }
 and op =
   | Etuple
   | Enode of qualname
+  | Easync of qualname * ack
   | Efun of qualname
   | Eifthenelse
   | Earrow
@@ -128,6 +129,8 @@ and op =
   | Econcat
   | Ereinit
 
+and ack = { ack_name: string; ack_params: static_exp list }
+
 and pat =
   | Etuplepat of pat list
   | Evarpat of var_name
@@ -271,6 +274,9 @@ let mk_exp desc ?(ct_annot = None) loc =
 let mk_app op params inlined =
   { a_op = op; a_params = params; a_inlined = inlined }
 
+let mk_ack name params =
+  { ack_name = name; ack_params = params }
+
 let mk_call ?(params=[]) ?(inlined=false) op exps =
   Eapp (mk_app op params inlined, exps)
 
diff --git a/compiler/heptagon/parsing/hept_scoping.ml b/compiler/heptagon/parsing/hept_scoping.ml
index ac66065..4f5705d 100644
--- a/compiler/heptagon/parsing/hept_scoping.ml
+++ b/compiler/heptagon/parsing/hept_scoping.ml
@@ -366,6 +366,7 @@ and translate_op = function
   | Eselect_trunc -> Heptagon.Eselect_trunc
   | Efun ln -> Heptagon.Efun (qualify_value ln)
   | Enode ln -> Heptagon.Enode (qualify_value ln)
+  | Easync (ln, ack) -> Heptagon.Easync (qualify_value ln, ack)
   | Ereinit -> Heptagon.Ereinit
 
 and translate_pat loc env = function