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)