From e39a0484ffbc98392b0bb18827e6d93ea5f14ed9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9onard=20G=C3=A9rard?= Date: Fri, 10 Dec 2010 00:35:31 +0100 Subject: [PATCH] Add 'block' to Heptagon. --- compiler/heptagon/analysis/causality.ml | 2 ++ compiler/heptagon/analysis/initialization.ml | 2 ++ compiler/heptagon/analysis/typing.ml | 4 ++++ compiler/heptagon/hept_mapfold.ml | 3 +++ compiler/heptagon/hept_printer.ml | 22 ++++++++++++------- compiler/heptagon/heptagon.ml | 1 + compiler/heptagon/main/hept_compiler.ml | 3 +++ compiler/heptagon/parsing/hept_lexer.mll | 2 ++ compiler/heptagon/parsing/hept_parser.mly | 6 +++-- compiler/heptagon/parsing/hept_parsetree.ml | 1 + .../parsing/hept_parsetree_mapfold.ml | 3 +++ compiler/heptagon/parsing/hept_scoping.ml | 3 +++ compiler/main/hept2mls.ml | 1 + 13 files changed, 43 insertions(+), 10 deletions(-) diff --git a/compiler/heptagon/analysis/causality.ml b/compiler/heptagon/analysis/causality.ml index 5e07a51..24eb9b4 100644 --- a/compiler/heptagon/analysis/causality.ml +++ b/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) diff --git a/compiler/heptagon/analysis/initialization.ml b/compiler/heptagon/analysis/initialization.ml index 637e73d..d35c89c 100644 --- a/compiler/heptagon/analysis/initialization.ml +++ b/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 diff --git a/compiler/heptagon/analysis/typing.ml b/compiler/heptagon/analysis/typing.ml index d1bff1c..f01c393 100644 --- a/compiler/heptagon/analysis/typing.ml +++ b/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 diff --git a/compiler/heptagon/hept_mapfold.ml b/compiler/heptagon/hept_mapfold.ml index c09078f..d2a5484 100644 --- a/compiler/heptagon/hept_mapfold.ml +++ b/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 diff --git a/compiler/heptagon/hept_printer.ml b/compiler/heptagon/hept_printer.ml index ee9e0ab..346464a 100644 --- a/compiler/heptagon/hept_printer.ml +++ b/compiler/heptagon/hept_printer.ml @@ -193,14 +193,16 @@ let rec print_eq ff eq = print_default b | Ereset(b, e) -> fprintf ff "@[@[reset @ %a@]@,every %a@]" - print_block b print_exp e + (print_block "in") b print_exp e + | Eblock b -> + fprintf ff "@[do@[@ @[%a@]@]@ done@]" (print_block "in") b and print_state_handler_list ff tag_act_list = print_list (fun ff sh -> fprintf ff "@[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 "@[| %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 "@[| %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 "@[default@,%a@]" print_block b + | _ -> fprintf ff "@[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@[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@[%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 "@[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 diff --git a/compiler/heptagon/heptagon.ml b/compiler/heptagon/heptagon.ml index b959840..e1cb533 100644 --- a/compiler/heptagon/heptagon.ml +++ b/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 = { diff --git a/compiler/heptagon/main/hept_compiler.ml b/compiler/heptagon/main/hept_compiler.ml index 19aa693..605a3e3 100644 --- a/compiler/heptagon/main/hept_compiler.ml +++ b/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 diff --git a/compiler/heptagon/parsing/hept_lexer.mll b/compiler/heptagon/parsing/hept_lexer.mll index ef7284f..9f035a9 100644 --- a/compiler/heptagon/parsing/hept_lexer.mll +++ b/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; diff --git a/compiler/heptagon/parsing/hept_parser.mly b/compiler/heptagon/parsing/hept_parser.mly index 816384a..52d5a44 100644 --- a/compiler/heptagon/parsing/hept_parser.mly +++ b/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: diff --git a/compiler/heptagon/parsing/hept_parsetree.ml b/compiler/heptagon/parsing/hept_parsetree.ml index 854fca2..106a044 100644 --- a/compiler/heptagon/parsing/hept_parsetree.ml +++ b/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 = diff --git a/compiler/heptagon/parsing/hept_parsetree_mapfold.ml b/compiler/heptagon/parsing/hept_parsetree_mapfold.ml index 10789ad..1caaaa6 100644 --- a/compiler/heptagon/parsing/hept_parsetree_mapfold.ml +++ b/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 diff --git a/compiler/heptagon/parsing/hept_scoping.ml b/compiler/heptagon/parsing/hept_scoping.ml index 31dcf69..71dee7d 100644 --- a/compiler/heptagon/parsing/hept_scoping.ml +++ b/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 diff --git a/compiler/main/hept2mls.ml b/compiler/main/hept2mls.ml index 543093e..3403f1b 100644 --- a/compiler/main/hept2mls.ml +++ b/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