Add 'block' to Heptagon.

compiler/heptagon/analysis/causality.ml

@@ -166,6 +166,8 @@ and typing_eq eq =
         typing_present handlers b
     | Ereset(b, e) ->
         cseq (typing e) (typing_block b)
+    | Eblock b ->
+        typing_block b
     | Eeq(pat, e) ->
         cseq (typing e) (typing_pat pat)
 

compiler/heptagon/analysis/initialization.ml

@@ -300,6 +300,8 @@ and typing_eq h eq =
         typing_present h handlers b
     | Ereset(b, e) ->
         initialized_exp h e; ignore (typing_block h b)
+    | Eblock b ->
+        ignore (typing_block h b)
     | Eeq(pat, e) ->
         let ty_pat = typing_pat h pat in
         expect h e ty_pat

compiler/heptagon/analysis/typing.ml

@@ -869,6 +869,10 @@ let rec typing_eq const_env h acc eq =
         let typed_b, def_names, _ = typing_block const_env h b in
         Ereset(typed_b, typed_e),
         Env.union def_names acc
+    | Eblock b ->
+        let typed_b, def_names, _ = typing_block const_env h b in
+        Eblock typed_b,
+        Env.union def_names acc
     | Eeq(pat, e) ->
         let acc, ty_pat = typing_pat h acc pat in
         let typed_e = expect const_env h ty_pat e in

compiler/heptagon/hept_mapfold.ml

@@ -188,6 +188,9 @@ and eqdesc funs acc eqd = match eqd with
       let b, acc = block_it funs acc b in
       let e, acc = exp_it funs acc e in
       Ereset (b, e), acc
+  | Eblock b ->
+      let b, acc = block_it funs acc b in
+      Eblock b, acc
   | Eeq (p, e) ->
       let p, acc = pat_it funs acc p in
       let e, acc = exp_it funs acc e in

compiler/heptagon/hept_printer.ml

@@ -193,14 +193,16 @@ let rec print_eq ff eq =
         print_default b
     | Ereset(b, e) ->
       fprintf ff "@[<v>@[<hv 2>reset @ %a@]@,every %a@]"
-        print_block b   print_exp e
+        (print_block "in") b   print_exp e
+    | Eblock b ->
+      fprintf ff "@[<v>do@[<v>@ @[%a@]@]@ done@]" (print_block "in") b
 
 and print_state_handler_list ff tag_act_list =
   print_list
     (fun ff sh ->
        fprintf ff "@[<v 2>state %a:@ %a%a%a@]"
          print_name sh.s_state
-         print_block sh.s_block
+         (print_block "do") sh.s_block
          (print_escape_list "until") sh.s_until
          (print_escape_list "unless") sh.s_unless)
     "" "" "" ff tag_act_list
@@ -221,7 +223,7 @@ and print_switch_handler_list ff tag_act_list =
     (fun ff sh ->
        fprintf ff "@[<v 2>| %a:@ %a@]"
          print_qualname sh.w_name
-         print_block sh.w_block)
+         (print_block "do") sh.w_block)
     "" "" "" ff tag_act_list
 
 and print_present_handler_list ff present_act_list =
@@ -229,20 +231,24 @@ and print_present_handler_list ff present_act_list =
     (fun ff ph ->
        fprintf ff "@[<v 2>| %a:@ %a@]"
          print_exp ph.p_cond
-         print_block ph.p_block)
+         (print_block "do") ph.p_block)
     "" "" "" ff present_act_list
 
 and print_default ff b =
   match b.b_equs with
     | [] -> ()
-    | _ -> fprintf ff "@[<v 2>default@,%a@]" print_block b
+    | _ -> fprintf ff "@[<v 2>default@,%a@]" (print_block "do") b
 
 and print_eq_list ff = function
   | [] -> ()
   | l -> print_list_r print_eq """;""" ff l
 
-and print_block ff { b_local = v_list; b_equs = eqs } =
-  fprintf ff "%a@[<v2>do@ %a@]" print_local_vars v_list  print_eq_list eqs
+and print_block s ff { b_local = v_list; b_equs = eqs } =
+  fprintf ff "%a@[<v2>%s@ %a@]" print_local_vars v_list s print_eq_list eqs
+
+
+let print_inblock = print_block "in"
+
 
 let rec print_type_def ff { t_name = name; t_desc = tdesc } =
   let print_type_desc ff = function
@@ -258,7 +264,7 @@ let print_contract ff { c_block = b;
                         c_assume = e_a; c_enforce = e_g;
 			c_controllables = c} =
   fprintf ff "@[<v2>contract@\n%a@ assume %a@ enforce %a@ with (%a)@]"
-    print_block b
+    (print_block "let") b
     print_exp e_a
     print_exp e_g
     print_vd_tuple c

compiler/heptagon/heptagon.ml

@@ -82,6 +82,7 @@ and eqdesc =
   | Eswitch of exp * switch_handler list
   | Epresent of present_handler list * block
   | Ereset of block * exp
+  | Eblock of block
   | Eeq of pat * exp
 
 and block = {

compiler/heptagon/main/hept_compiler.ml

@@ -70,6 +70,9 @@ let compile_impl pp p =
   (* Every *)
   let p = pass "Every" true Every.program p pp in
 
+  (* Block flatten *)
+  let p = pass "Block" true Block.program p pp in
+
   (* Return the transformed AST *)
   p
 

compiler/heptagon/parsing/hept_lexer.mll

@@ -47,6 +47,8 @@ List.iter (fun (str,tok) -> Hashtbl.add keyword_table str tok) [
  "default", DEFAULT;
  "continue", CONTINUE;
  "do", DO;
+ "done", DONE;
+ "in", IN;
  "contract", CONTRACT;
  "assume", ASSUME;
  "enforce", ENFORCE;

compiler/heptagon/parsing/hept_parser.mly

@@ -33,7 +33,7 @@ open Hept_parsetree
 %token THEN
 %token ELSE
 %token DEFAULT
-%token DO
+%token DO DONE IN
 %token CONTINUE
 %token CONTRACT
 %token ASSUME
@@ -313,8 +313,10 @@ _equ:
       { Eswitch($2,
                    [{ w_name = ptrue; w_block = tb };
                     { w_name = pfalse; w_block = fb }]) }
-  | RESET equs EVERY exp
+  | RESET equs EVERY exp (* LG TODO real blocks(IN)*)
       { Ereset(mk_block [] $2 (Loc($startpos,$endpos)), $4) }
+  | DO b=block(IN) DONE
+      { Eblock b }
 ;
 
 automaton_handler:

compiler/heptagon/parsing/hept_parsetree.ml

@@ -106,6 +106,7 @@ and eqdesc =
   | Eswitch of exp * switch_handler list
   | Epresent of present_handler list * block
   | Ereset of block * exp
+  | Eblock of block
   | Eeq of pat * exp
 
 and block =

compiler/heptagon/parsing/hept_parsetree_mapfold.ml

@@ -188,6 +188,9 @@ and eqdesc funs acc eqd = match eqd with
       let b, acc = block_it funs acc b in
       let e, acc = exp_it funs acc e in
       Ereset (b, e), acc
+  | Eblock b ->
+      let b, acc = block_it funs acc b in
+      Eblock b, acc
   | Eeq (p, e) ->
       let p, acc = pat_it funs acc p in
       let e, acc = exp_it funs acc e in

compiler/heptagon/parsing/hept_scoping.ml

@@ -313,6 +313,9 @@ and translate_eq_desc loc env = function
   | Ereset (b, e) ->
       let b, _ = translate_block env b in
       Heptagon.Ereset (b, translate_exp env e)
+  | Eblock b ->
+      let b, _ = translate_block env b in
+      Heptagon.Eblock b
 
 and translate_block env b =
   let env = Rename.append env b.b_local in

compiler/main/hept2mls.ml

@@ -300,6 +300,7 @@ let rec translate_eq env ni (locals, l_eqs, s_eqs)
         locals,
         (mk_equation ~loc:loc p' (translate env e)) :: l_eqs,
         s_eqs
+    | Heptagon.Eblock _
     | Heptagon.Epresent _ | Heptagon.Eautomaton _ | Heptagon.Ereset _ ->
         Error.message loc Error.Eunsupported_language_construct