Added 'when', 'merge' to the parsing and scoping.

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 }

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 <Hept_parsetree.program> 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

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; }
 

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

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,

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 }