From b85f9ab456adbdf3facbb8b4813ffb6c2b377790 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?C=C3=A9dric=20Pasteur?= Date: Fri, 23 Jul 2010 10:56:25 +0200 Subject: [PATCH] Use a block in reset (instead of a list of eqs) - Most transformation passes expect that list of equations are always nested inside a block. This fixes a problem with a duplication of equations in Automata_mapfold. --- compiler/heptagon/analysis/causality.ml | 4 ++-- compiler/heptagon/analysis/initialization.ml | 4 ++-- compiler/heptagon/analysis/typing.ml | 7 ++++--- compiler/heptagon/hept_mapfold.ml | 6 +++--- compiler/heptagon/hept_printer.ml | 4 ++-- compiler/heptagon/heptagon.ml | 4 ++-- compiler/heptagon/parsing/hept_parser.mly | 10 +++++----- compiler/heptagon/parsing/hept_parsetree.ml | 2 +- compiler/heptagon/parsing/hept_scoping.ml | 6 +++--- compiler/heptagon/transformations/automata_mapfold.ml | 6 +++--- compiler/heptagon/transformations/inline.ml | 3 ++- compiler/heptagon/transformations/present_mapfold.ml | 2 +- compiler/heptagon/transformations/reset_mapfold.ml | 4 ++-- 13 files changed, 32 insertions(+), 30 deletions(-) diff --git a/compiler/heptagon/analysis/causality.ml b/compiler/heptagon/analysis/causality.ml index 633d743..6e83018 100644 --- a/compiler/heptagon/analysis/causality.ml +++ b/compiler/heptagon/analysis/causality.ml @@ -149,8 +149,8 @@ and typing_eq eq = cseq (typing e) (typing_switch handlers) | Epresent(handlers, b) -> typing_present handlers b - | Ereset(eq_list, e) -> - cseq (typing e) (typing_eqs eq_list) + | Ereset(b, e) -> + cseq (typing e) (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 dc326fb..6740842 100644 --- a/compiler/heptagon/analysis/initialization.ml +++ b/compiler/heptagon/analysis/initialization.ml @@ -263,8 +263,8 @@ and typing_eq h eq = typing_switch h handlers | Epresent(handlers, b) -> typing_present h handlers b - | Ereset(eq_list, e) -> - initialized_exp h e; typing_eqs h eq_list + | Ereset(b, e) -> + initialized_exp h e; 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 ca6311d..f5e3059 100644 --- a/compiler/heptagon/analysis/typing.ml +++ b/compiler/heptagon/analysis/typing.ml @@ -878,11 +878,12 @@ let rec typing_eq statefull const_env h acc eq = acc def_names present_handlers in Epresent(typed_ph,typed_b), acc - | Ereset(eq_list, e) -> + | Ereset(b, e) -> let typed_e = expect statefull const_env h (Tid Initial.pbool) e in let typed_eq_list, acc = typing_eq_list statefull - const_env h acc eq_list in - Ereset(typed_eq_list,typed_e), + const_env h acc b.b_equs in + let typed_b = { b with b_equs = typed_eq_list } in + Ereset(typed_b, typed_e), acc | Eeq(pat, e) -> let acc, ty_pat = typing_pat h acc pat in diff --git a/compiler/heptagon/hept_mapfold.ml b/compiler/heptagon/hept_mapfold.ml index 809883a..7376274 100644 --- a/compiler/heptagon/hept_mapfold.ml +++ b/compiler/heptagon/hept_mapfold.ml @@ -173,10 +173,10 @@ and eqdesc funs acc eqd = match eqd with let p_h_l, acc = mapfold (present_handler_it funs) acc p_h_l in let b, acc = block_it funs acc b in Epresent (p_h_l, b), acc - | Ereset (eq_l, e) -> - let eq_l, acc = mapfold (eq_it funs) acc eq_l in + | Ereset (b, e) -> + let b, acc = block_it funs acc b in let e, acc = exp_it funs acc e in - Ereset (eq_l, e), acc + Ereset (b, e), 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 0d5f6e6..5083074 100644 --- a/compiler/heptagon/hept_printer.ml +++ b/compiler/heptagon/hept_printer.ml @@ -190,10 +190,10 @@ let rec print_eq ff eq = fprintf ff "@]" end; fprintf ff "@,end@]" - | Ereset(eq_list, e) -> + | Ereset(b, e) -> fprintf ff "@[reset@,"; fprintf ff " @["; - print_eq_list ff eq_list; + print_block ff b; fprintf ff "@]"; fprintf ff "@,every "; print_exp ff e; diff --git a/compiler/heptagon/heptagon.ml b/compiler/heptagon/heptagon.ml index 5fe6072..85bf781 100644 --- a/compiler/heptagon/heptagon.ml +++ b/compiler/heptagon/heptagon.ml @@ -62,7 +62,7 @@ and eqdesc = | Eautomaton of state_handler list | Eswitch of exp * switch_handler list | Epresent of present_handler list * block - | Ereset of eq list * exp + | Ereset of block * exp | Eeq of pat * exp and block = { @@ -165,7 +165,7 @@ let mk_var_dec ?(last = Var) name ty = { v_ident = name; v_type = ty; v_last = last; v_loc = no_location } -let mk_block ?(statefull = true) defnames eqs = +let mk_block ?(statefull = true) ?(defnames = Env.empty) eqs = { b_local = []; b_equs = eqs; b_defnames = defnames; b_statefull = statefull; b_loc = no_location } diff --git a/compiler/heptagon/parsing/hept_parser.mly b/compiler/heptagon/parsing/hept_parser.mly index 506209e..f67bca6 100644 --- a/compiler/heptagon/parsing/hept_parser.mly +++ b/compiler/heptagon/parsing/hept_parser.mly @@ -119,11 +119,11 @@ type_decs: ; type_dec: - | TYPE IDENT + | TYPE IDENT { mk_type_dec $2 Type_abs (Loc($startpos,$endpos)) } - | TYPE IDENT EQUAL enum_ty_desc + | TYPE IDENT EQUAL enum_ty_desc { mk_type_dec $2 (Type_enum ($4)) (Loc($startpos,$endpos)) } - | TYPE IDENT EQUAL struct_ty_desc + | TYPE IDENT EQUAL struct_ty_desc { mk_type_dec $2 (Type_struct ($4)) (Loc($startpos,$endpos)) } ; @@ -232,7 +232,7 @@ loc_params: | var_last SEMICOL loc_params { $1 @ $3 } ; - + var_last: | ident_list COLON ty_ident { List.map (fun id -> mk_var_dec id $3 Var (Loc($startpos,$endpos))) $1 } @@ -294,7 +294,7 @@ _equ: [{ w_name = Name("true"); w_block = tb }; { w_name = Name("false"); w_block = fb }]) } | RESET equs EVERY exp - { Ereset($2, $4) } + { Ereset(mk_block [] $2 (Loc($startpos,$endpos)), $4) } ; automaton_handler: diff --git a/compiler/heptagon/parsing/hept_parsetree.ml b/compiler/heptagon/parsing/hept_parsetree.ml index 58313c7..8d62aa4 100644 --- a/compiler/heptagon/parsing/hept_parsetree.ml +++ b/compiler/heptagon/parsing/hept_parsetree.ml @@ -67,7 +67,7 @@ and eqdesc = | Eautomaton of state_handler list | Eswitch of exp * switch_handler list | Epresent of present_handler list * block - | Ereset of eq list * exp + | Ereset of block * exp | Eeq of pat * exp and block = diff --git a/compiler/heptagon/parsing/hept_scoping.ml b/compiler/heptagon/parsing/hept_scoping.ml index a066da3..28772f4 100644 --- a/compiler/heptagon/parsing/hept_scoping.ml +++ b/compiler/heptagon/parsing/hept_scoping.ml @@ -226,9 +226,9 @@ and translate_eq_desc loc const_env env = function | Eautomaton state_handlers -> Heptagon.Eautomaton (List.map (translate_state_handler const_env env) state_handlers) - | Ereset (eq_list, e) -> - Heptagon.Ereset (List.map (translate_eq const_env env) eq_list, - translate_exp const_env env e) + | Ereset (b, e) -> + let b, _ = translate_block const_env env b in + Heptagon.Ereset (b, translate_exp const_env env e) and translate_block const_env env b = let env = build_vd_list env b.b_local in diff --git a/compiler/heptagon/transformations/automata_mapfold.ml b/compiler/heptagon/transformations/automata_mapfold.ml index 0ca91f5..90d942e 100644 --- a/compiler/heptagon/transformations/automata_mapfold.ml +++ b/compiler/heptagon/transformations/automata_mapfold.ml @@ -22,7 +22,7 @@ let mk_pair e1 e2 = mk_exp (mk_op_app Etuple [e1;e2]) (Tprod [e1.e_ty; e2.e_ty]) let mk_reset_equation eq_list e = - mk_equation (Ereset (eq_list, e)) + mk_equation (Ereset (mk_block eq_list, e)) let mk_switch_equation e l = mk_equation (Eswitch (e, l)) @@ -89,8 +89,8 @@ let translate_automaton v eq_list handlers = let st_eq = mk_simple_equation (Etuplepat[Evarpat(statename); Evarpat(resetname)]) (escapes n su (boolvar pre_next_resetname)) in - mk_block defnames [mk_reset_equation [st_eq] - (boolvar pre_next_resetname)] + mk_block ~defnames:defnames [mk_reset_equation [st_eq] + (boolvar pre_next_resetname)] in let weak { s_state = n; s_block = b; s_until = su } = diff --git a/compiler/heptagon/transformations/inline.ml b/compiler/heptagon/transformations/inline.ml index e0d3be6..3502821 100644 --- a/compiler/heptagon/transformations/inline.ml +++ b/compiler/heptagon/transformations/inline.ml @@ -56,7 +56,8 @@ let exp funs (env, newvars, newequs) exp = match exp.e_desc with | Eapp ({ a_op = Enode nn; } as op, argl, rso) when to_be_inlined nn -> let add_reset eq = match rso with | None -> eq - | Some x -> mk_equation ~statefull:false (Ereset ([eq], x)) in + | Some x -> mk_equation ~statefull:false + (Ereset (mk_block [eq], x)) in let ni = mk_unique_node (env nn) in diff --git a/compiler/heptagon/transformations/present_mapfold.ml b/compiler/heptagon/transformations/present_mapfold.ml index cb9935b..1223a56 100644 --- a/compiler/heptagon/transformations/present_mapfold.ml +++ b/compiler/heptagon/transformations/present_mapfold.ml @@ -13,7 +13,7 @@ open Hept_mapfold let translate_present_handlers handlers cont = let translate_present_handler { p_cond = e; p_block = b } cont = let statefull = b.b_statefull or cont.b_statefull in - mk_block ~statefull:statefull b.b_defnames + mk_block ~statefull:statefull ~defnames:b.b_defnames [mk_switch_equation ~statefull:statefull e [{ w_name = Initial.ptrue; w_block = b }; diff --git a/compiler/heptagon/transformations/reset_mapfold.ml b/compiler/heptagon/transformations/reset_mapfold.ml index 34b325b..6b9aaf5 100644 --- a/compiler/heptagon/transformations/reset_mapfold.ml +++ b/compiler/heptagon/transformations/reset_mapfold.ml @@ -162,7 +162,7 @@ let eq funs (res, v, acc_eq_list) equ = switch_handlers funs (res, v, acc_eq_list) sh in equ, (res, v, { equ with eq_desc = Eswitch(e, sh) } :: acc_eq_list) - | Ereset(eq_list, e) -> + | Ereset(b, e) -> let e, _ = exp_it funs (res, v, acc_eq_list) e in let res, v, acc_eq_list = (* if statefull eq_list then*) @@ -172,7 +172,7 @@ let eq funs (res, v, acc_eq_list) equ = res, v, acc_eq_list*) in let _, (res, v, acc_eq_list) = - mapfold (eq_it funs) (res, v, acc_eq_list) eq_list in + mapfold (eq_it funs) (res, v, acc_eq_list) b.b_equs in equ, (res, v, acc_eq_list) | _ ->