diff --git a/compiler/heptagon/parsing/hept_lexer.mll b/compiler/heptagon/parsing/hept_lexer.mll index b2a3b43..ef7284f 100644 --- a/compiler/heptagon/parsing/hept_lexer.mll +++ b/compiler/heptagon/parsing/hept_lexer.mll @@ -51,6 +51,8 @@ List.iter (fun (str,tok) -> Hashtbl.add keyword_table str tok) [ "assume", ASSUME; "enforce", ENFORCE; "with", WITH; + "when", WHEN; + "merge", MERGE; "map", MAP; "fold", FOLD; "foldi", FOLDI; @@ -146,10 +148,10 @@ rule token = parse | (['A'-'Z' 'a'-'z']('_' ? ['A'-'Z' 'a'-'z' ''' '0'-'9']) * as id) { let s = Lexing.lexeme lexbuf in begin try - Hashtbl.find keyword_table s + Hashtbl.find keyword_table s with - Not_found -> IDENT id - end + Not_found -> IDENT id + end } | ['0'-'9']+ | '0' ['x' 'X'] ['0'-'9' 'A'-'F' 'a'-'f']+ @@ -160,14 +162,14 @@ rule token = parse { FLOAT (float_of_string(Lexing.lexeme lexbuf)) } | "(*@ " (['A'-'Z' 'a'-'z']('_' ? ['A'-'Z' 'a'-'z' ''' '0'-'9']) * as id) { - reset_string_buffer(); + reset_string_buffer(); let l1 = lexbuf.lex_curr_p in - begin try - pragma lexbuf - with Lexical_error(Unterminated_comment, Loc(_, l2)) -> - raise(Lexical_error(Unterminated_comment, Loc (l1, l2))) - end; - PRAGMA(id,get_stored_string()) + begin try + pragma lexbuf + with Lexical_error(Unterminated_comment, Loc(_, l2)) -> + raise(Lexical_error(Unterminated_comment, Loc (l1, l2))) + end; + PRAGMA(id,get_stored_string()) } | "(*" { let comment_start = lexbuf.lex_curr_p in @@ -181,32 +183,32 @@ rule token = parse token lexbuf } | ['!' '?' '~'] ['!' '$' '%' '&' '*' '+' '-' '.' '/' ':' - '<' '=' '>' '?' '@' '^' '|' '~'] * + '<' '=' '>' '?' '@' '^' '|' '~'] * { PREFIX(Lexing.lexeme lexbuf) } | ['=' '<' '>' '&' '|' '&' '$'] ['!' '$' '%' '&' '*' '+' '-' '.' '/' ':' '<' '=' '>' - '?' '@' '^' '|' '~'] * + '?' '@' '^' '|' '~'] * { INFIX0(Lexing.lexeme lexbuf) } | ['@' '^'] ['!' '$' '%' '&' '*' '+' '-' '.' '/' ':' '<' '=' '>' - '?' '@' '^' '|' '~'] * + '?' '@' '^' '|' '~'] * { INFIX1(Lexing.lexeme lexbuf) } | ['+' '-'] ['!' '$' '%' '&' '*' '+' '-' '.' '/' ':' '<' '=' '>' - '?' '@' '^' '|' '~'] * + '?' '@' '^' '|' '~'] * { INFIX2(Lexing.lexeme lexbuf) } | "**" ['!' '$' '%' '&' '*' '+' '-' '.' '/' ':' '<' '=' '>' - '?' '@' '^' '|' '~'] * + '?' '@' '^' '|' '~'] * { INFIX4(Lexing.lexeme lexbuf) } | ['*' '/' '%'] ['!' '$' '%' '&' '*' '+' '-' '.' '/' ':' '<' '=' '>' - '?' '@' '^' '|' '~'] * + '?' '@' '^' '|' '~'] * { INFIX3(Lexing.lexeme lexbuf) } | eof {EOF} | _ {raise (Lexical_error (Illegal_character, - Loc (Lexing.lexeme_start_p lexbuf, - Lexing.lexeme_end_p lexbuf)))} + Loc (Lexing.lexeme_start_p lexbuf, + Lexing.lexeme_end_p lexbuf)))} and pragma = parse | newline { new_line lexbuf; pragma lexbuf } @@ -228,7 +230,7 @@ and pragma = parse | _ { store_string_char(Lexing.lexeme_char lexbuf 0); - pragma lexbuf } + pragma lexbuf } and comment = parse | newline { new_line lexbuf; comment lexbuf } diff --git a/compiler/heptagon/parsing/hept_parser.mly b/compiler/heptagon/parsing/hept_parser.mly index b82e9ec..3d9ada7 100644 --- a/compiler/heptagon/parsing/hept_parser.mly +++ b/compiler/heptagon/parsing/hept_parser.mly @@ -39,6 +39,7 @@ open Hept_parsetree %token ASSUME %token ENFORCE %token WITH +%token WHEN MERGE %token POWER %token LBRACKET %token RBRACKET @@ -65,6 +66,7 @@ open Hept_parsetree %left AMPERSAND %left INFIX0 EQUAL LESS_GREATER %right INFIX1 +%right WHEN %left INFIX2 SUBTRACTIVE %left STAR INFIX3 %left INFIX4 @@ -76,6 +78,7 @@ open Hept_parsetree %right PREFIX %left DOT + %start program %type program @@ -84,14 +87,22 @@ open Hept_parsetree %% +/** Tools **/ +%inline slist(S, x) : l=separated_list(S, x) {l} +%inline snlist(S, x) : l=separated_nonempty_list(S, x) {l} +%inline tuple(x) : LPAREN h=x COMMA t=snlist(COMMA,x) RPAREN { h::t } +%inline soption(P,x): + |/* empty */ { None } + | P v=x { Some(v) } + program: | pragma_headers open_modules const_decs type_decs node_decs EOF {{ p_modname = ""; p_pragmas = $1; - p_opened = List.rev $2; + p_opened = List.rev $2; p_types = $4; p_nodes = $5; - p_consts = $3; }} + p_consts = $3; }} ; pragma_headers: @@ -159,13 +170,13 @@ node_dec: RETURNS LPAREN out_params RPAREN contract b=block(LET) TEL {{ n_name = $2; - n_statefull = $1; - n_input = $5; - n_output = $9; - n_contract = $11; - n_block = b; - n_params = $3; - n_loc = (Loc($startpos,$endpos)) }} + n_statefull = $1; + n_input = $5; + n_output = $9; + n_contract = $11; + n_block = b; + n_params = $3; + n_loc = (Loc($startpos,$endpos)) }} ; node_or_fun: @@ -211,8 +222,8 @@ contract: | /* empty */ {None} | CONTRACT b=block(LET) TEL? opt_assume enforce { Some{ c_block = b; - c_assume = $4; - c_enforce = $5 } } + c_assume = $4; + c_enforce = $5 } } ; opt_assume: @@ -402,6 +413,10 @@ _simple_exp: node_name: | qualname call_params { mk_app (Enode $1) $2 } +merge_handlers: + | hs=nonempty_list(merge_handler) { hs } +merge_handler: + | LPAREN c=constructor_or_bool ARROW e=exp RPAREN { (c,e) } exp: | e=simple_exp { e } @@ -421,6 +436,10 @@ _exp: { mk_op_call $2 [$1; $3] } | exp INFIX2 exp { mk_op_call $2 [$1; $3] } + | e=exp WHEN c=constructor_or_bool LPAREN n=IDENT RPAREN + { Ewhen (e, c, n) } + | MERGE n=IDENT hs=merge_handlers + { Emerge (n, hs) } | exp INFIX1 exp { mk_op_call $2 [$1; $3] } | exp INFIX0 exp diff --git a/compiler/heptagon/parsing/hept_parsetree.ml b/compiler/heptagon/parsing/hept_parsetree.ml index 29900ba..3149d1f 100644 --- a/compiler/heptagon/parsing/hept_parsetree.ml +++ b/compiler/heptagon/parsing/hept_parsetree.ml @@ -63,13 +63,15 @@ and exp = and edesc = | Econst of static_exp - | Evar of var_name + | Evar of var_name (* can be a constant_name *) | Elast of var_name | Epre of exp option * exp | Efby of exp * exp | Estruct of (qualname * exp) list | Eapp of app * exp list | Eiterator of iterator_type * app * exp * exp list + | Ewhen of exp * constructor_name * var_name + | Emerge of var_name * (constructor_name * exp) list and app = { a_op: op; a_params: exp list; } diff --git a/compiler/heptagon/parsing/hept_scoping.ml b/compiler/heptagon/parsing/hept_scoping.ml index 7e99da4..d0dbc48 100644 --- a/compiler/heptagon/parsing/hept_scoping.ml +++ b/compiler/heptagon/parsing/hept_scoping.ml @@ -285,6 +285,20 @@ and translate_desc loc local_const env = function let app = Heptagon.mk_op ~params:params (translate_op op) in Heptagon.Eiterator (translate_iterator_type it, app, n, e_list, None) + | Ewhen (e, c, n) -> + let e = translate_exp local_const env e in + let c = qualify_constrs c in + let n = Rename.var loc env n in + Heptagon.Ewhen (e, c, n) + | Emerge (n, c_e_list) -> + let n = Rename.var loc env n in + let c_e_list = + let fun_c_e (c, e) = + let e = translate_exp local_const env e in + let c = qualify_constrs c in + (c, e) in + List.map fun_c_e c_e_list in + Heptagon.Emerge (n, c_e_list) and translate_op = function | Eequal -> Heptagon.Eequal diff --git a/compiler/minils/parsing/mls_lexer.mll b/compiler/minils/parsing/mls_lexer.mll index ab43dea..8aea017 100644 --- a/compiler/minils/parsing/mls_lexer.mll +++ b/compiler/minils/parsing/mls_lexer.mll @@ -149,7 +149,7 @@ rule token = parse { FLOAT (float_of_string(Lexing.lexeme lexbuf)) } (* | "(*@ " (['A'-'Z' 'a'-'z']('_' ? ['A'-'Z' 'a'-'z' ''' '0'-'9']) * as id) { - reset_string_buffer(); + reset_string_buffer(); let l1 = lexbuf.lex_curr_p in begin try pragma lexbuf @@ -170,27 +170,27 @@ rule token = parse token lexbuf } | ['!' '?' '~'] ['!' '$' '%' '&' '*' '+' '-' '.' '/' ':' - '<' '=' '>' '?' '@' '^' '|' '~'] * + '<' '=' '>' '?' '@' '^' '|' '~'] * { PREFIX(Lexing.lexeme lexbuf) } | ['=' '<' '>' '&' '|' '&' '$'] ['!' '$' '%' '&' '*' '+' '-' '.' '/' ':' '<' '=' '>' - '?' '@' '^' '|' '~'] * + '?' '@' '^' '|' '~'] * { INFIX0(Lexing.lexeme lexbuf) } | ['@' '^'] ['!' '$' '%' '&' '*' '+' '-' '.' '/' ':' '<' '=' '>' - '?' '@' '^' '|' '~'] * + '?' '@' '^' '|' '~'] * { INFIX1(Lexing.lexeme lexbuf) } | ['+' '-'] ['!' '$' '%' '&' '*' '+' '-' '.' '/' ':' '<' '=' '>' - '?' '@' '^' '|' '~'] * + '?' '@' '^' '|' '~'] * { INFIX2(Lexing.lexeme lexbuf) } | "**" ['!' '$' '%' '&' '*' '+' '-' '.' '/' ':' '<' '=' '>' - '?' '@' '^' '|' '~'] * + '?' '@' '^' '|' '~'] * { INFIX4(Lexing.lexeme lexbuf) } | ['*' '/' '%'] ['!' '$' '%' '&' '*' '+' '-' '.' '/' ':' '<' '=' '>' - '?' '@' '^' '|' '~'] * + '?' '@' '^' '|' '~'] * { INFIX3(Lexing.lexeme lexbuf) } | eof {EOF} | _ {raise (Lexical_error (Illegal_character, diff --git a/compiler/minils/parsing/mls_parser.mly b/compiler/minils/parsing/mls_parser.mly index 9831568..5eb9285 100644 --- a/compiler/minils/parsing/mls_parser.mly +++ b/compiler/minils/parsing/mls_parser.mly @@ -69,21 +69,21 @@ open Mls_utils %% /** Tools **/ -%inline slist(S, x) : l=separated_list(S, x) {l} +%inline slist(S, x) : l=separated_list(S, x) {l} %inline snlist(S, x) : l=separated_nonempty_list(S, x) {l} %inline tuple(x) : LPAREN h=x COMMA t=snlist(COMMA,x) RPAREN { h::t } %inline option(P,x): - |/* empty */ { None } + |/* empty */ { None } | P v=x { Some(v) } qualified(x) : | n=x { Modules.qualname n } | m=CONSTRUCTOR DOT n=x { { qual = m; name = n } } - + structure(field): LBRACE s=snlist(SEMICOL,field) RBRACE {s} localize(x): y=x { y, (Loc($startpos(y),$endpos(y))) } - + program: | o=open_modules c=const_decs t=type_decs n=node_decs EOF @@ -118,10 +118,10 @@ node_dec: NODE n=qualname p=params(n_param) LPAREN args=args RPAREN RETURNS LPAREN out=args RPAREN vars=loc_vars eqs=equs { mk_node p args out vars eqs ~loc:(Loc ($startpos,$endpos)) n } - + args_t: SEMICOL p=args {p} -args: +args: | /* empty */ { [] } | h=var t=loption(args_t) {h@t} @@ -155,7 +155,7 @@ pat: | LPAREN p=snlist(COMMA, pat) RPAREN {Etuplepat p} longname: l=qualified(name) {l} - + constructor: /* of type longname */ | ln=qualified(CONSTRUCTOR) { ln } | b=BOOL { if b then Initial.ptrue else Initial.pfalse }