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.
This commit is contained in:
parent
0ef0ac5529
commit
cae38d0e60
3 changed files with 17 additions and 3 deletions
|
@ -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 }
|
||||
;
|
||||
|
||||
%%
|
||||
|
|
|
@ -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
|
||||
|
|
|
@ -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)
|
||||
|
|
Loading…
Reference in a new issue