From cae38d0e60ce54dfba8aa16b62511189c8c2d50c Mon Sep 17 00:00:00 2001
From: Timothy Bourke <tim@tbrk.org>
Date: Mon, 23 Jan 2017 14:59:09 +0100
Subject: [PATCH] Accept when-syntax for declaring clocks

The parameter or local declaration:
    x : bool :: . on y

Can now be made using the 'standard' Lustre syntax:
    x : bool when y

In this case, the translation gives x the clock:
    'a on y

and relies on the (MiniLS) Clocking pass to instantiate the fresh clock
variables.
---
 compiler/heptagon/parsing/hept_parser.mly   | 17 ++++++++++++++---
 compiler/heptagon/parsing/hept_parsetree.ml |  1 +
 compiler/heptagon/parsing/hept_scoping.ml   |  2 ++
 3 files changed, 17 insertions(+), 3 deletions(-)

diff --git a/compiler/heptagon/parsing/hept_parser.mly b/compiler/heptagon/parsing/hept_parser.mly
index 45e3679..2d85423 100644
--- a/compiler/heptagon/parsing/hept_parser.mly
+++ b/compiler/heptagon/parsing/hept_parser.mly
@@ -350,6 +350,12 @@ ck_annot:
   | /*empty */        { None }
   | COLONCOLON ck=ck
   | ON ck=on_ck       { Some ck }
+  | WHEN ck=when_ck   { Some ck }
+
+sig_ck_annot:
+  | /*empty */        { None }
+  | COLONCOLON ck=ck
+  | ON ck=on_ck       { Some ck }
 
 ck:
   | DOT                  { Cbase }
@@ -363,6 +369,11 @@ on_ck:
   | b=ck ONOT x=IDENT                                      { Con(b,Q Initial.pfalse,x) }
   | b=ck ON c=constructor_or_bool LPAREN x=IDENT RPAREN    { Con(b,c,x) }
 
+when_ck:
+  | x=IDENT                                                { Cwhen(Q Initial.ptrue,x) }
+  | c=constructor_or_bool LPAREN x=IDENT RPAREN            { Cwhen(c,x) }
+  | b=ck x=IDENT                                           { Cwhen(Q Initial.ptrue,x) }
+  | b=ck NOT x=IDENT                                       { Cwhen(Q Initial.pfalse,x) }
 
 equs:
   | /* empty */                      { [] }
@@ -750,9 +761,9 @@ nonmt_params_signature:
 ;
 
 param_signature:
-  | IDENT COLON located_ty_ident ck=ck_annot { mk_arg (Some $1) $3 ck }
-  | located_ty_ident ck=ck_annot { mk_arg None $1 ck }
-  | THREE_DOTS ck=ck_annot { mk_arg None (Tinvalid, Linearity.Ltop) ck }
+  | IDENT COLON located_ty_ident ck=sig_ck_annot { mk_arg (Some $1) $3 ck }
+  | located_ty_ident ck=sig_ck_annot { mk_arg None $1 ck }
+  | THREE_DOTS ck=sig_ck_annot { mk_arg None (Tinvalid, Linearity.Ltop) ck }
 ;
 
 %%
diff --git a/compiler/heptagon/parsing/hept_parsetree.ml b/compiler/heptagon/parsing/hept_parsetree.ml
index 39a66ff..917205e 100644
--- a/compiler/heptagon/parsing/hept_parsetree.ml
+++ b/compiler/heptagon/parsing/hept_parsetree.ml
@@ -84,6 +84,7 @@ type ty =
 and ck =
   | Cbase
   | Con of ck * constructor_name * var_name
+  | Cwhen of constructor_name * var_name
 
 and ct =
   | Ck of ck
diff --git a/compiler/heptagon/parsing/hept_scoping.ml b/compiler/heptagon/parsing/hept_scoping.ml
index d4c5302..ac66065 100644
--- a/compiler/heptagon/parsing/hept_scoping.ml
+++ b/compiler/heptagon/parsing/hept_scoping.ml
@@ -285,6 +285,7 @@ let rec translate_some_clock loc env ck = match ck with
 and translate_clock loc env ck = match ck with
   | Cbase -> Clocks.Cbase
   | Con(ck,c,x) -> Clocks.Con(translate_clock loc env ck, qualify_constrs c, Rename.var loc env x)
+  | Cwhen(c, x) -> Clocks.Con(Clocks.fresh_clock(), qualify_constrs c, Rename.var loc env x)
 
 let rec translate_ct loc env ct = match ct with
   | Ck ck -> Clocks.Ck (translate_clock loc env ck)
@@ -585,6 +586,7 @@ let translate_signature s =
   and translate_clock ck = match ck with
     | Cbase -> Signature.Cbase
     | Con(ck,c,x) -> Signature.Con(translate_clock ck, qualify_constrs c, x)
+    | Cwhen _ -> assert false (* not permitted by sig_ck_annot parser rule *)
   and translate_arg a =
     Signature.mk_arg a.a_name (translate_type s.sig_loc a.a_type)
       a.a_linearity (translate_some_clock a.a_clock)