diff --git a/compiler/heptagon/parsing/hept_lexer.mll b/compiler/heptagon/parsing/hept_lexer.mll index e9891e6..629d426 100644 --- a/compiler/heptagon/parsing/hept_lexer.mll +++ b/compiler/heptagon/parsing/hept_lexer.mll @@ -57,6 +57,7 @@ List.iter (fun (str,tok) -> Hashtbl.add keyword_table str tok) [ "whenot", WHENOT; "merge", MERGE; "on", ON; + "onot", ONOT; "map", MAP; "mapi", MAPI; "fold", FOLD; diff --git a/compiler/heptagon/parsing/hept_parser.mly b/compiler/heptagon/parsing/hept_parser.mly index c90ca7c..73a1a0e 100644 --- a/compiler/heptagon/parsing/hept_parser.mly +++ b/compiler/heptagon/parsing/hept_parser.mly @@ -39,7 +39,7 @@ open Hept_parsetree %token ASSUME %token ENFORCE %token WITH -%token WHEN WHENOT MERGE ON +%token WHEN WHENOT MERGE ON ONOT %token POWER %token LBRACKET LBRACKETGREATER %token RBRACKET LESSRBRACKET @@ -285,8 +285,11 @@ ck: on_ck: - | c=constructor_or_bool LPAREN x=IDENT RPAREN { Con(Cbase,c,x) } - | b=ck ON c=constructor_or_bool LPAREN x=IDENT RPAREN { Con(b,c,x) } + | x=IDENT { Con(Cbase,Q Initial.ptrue,x) } + | c=constructor_or_bool LPAREN x=IDENT RPAREN { Con(Cbase,c,x) } + | b=ck ON x=IDENT { Con(b,Q Initial.ptrue,x) } + | 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) } equs: diff --git a/test/good/auto.ept b/test/good/auto.ept index 3d42889..ab579f4 100644 --- a/test/good/auto.ept +++ b/test/good/auto.ept @@ -3,14 +3,19 @@ let o = 0 fby (o + 1); tel -node main() returns (c : bool) +node f() returns(x,y : bool) +let + (x,y) = (true,false) +tel + +node main() returns (c,c1 : bool) let automaton state One - do c = true; + do (c,c1) = f() until count() = 5 then Two state Two - do c = false + do (c,c1) = f() until count() = 3 then One end tel