jeltz/heptagon
1
0
Fork 0
Code Issues Pull requests Releases Activity

Use a block in reset (instead of a list of eqs)

Browse source 
- 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.
This commit is contained in:
Cédric Pasteur 2010-07-23 10:56:25 +02:00
parent 89ceb8df76
commit b85f9ab456
13 changed files with 32 additions and 30 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
compiler/heptagon/analysis/causality.ml
View file

@ -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)

4
compiler/heptagon/analysis/initialization.ml
View file

@ -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

7
compiler/heptagon/analysis/typing.ml
View file

@ -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

6
compiler/heptagon/hept_mapfold.ml
View file

@ -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

4
compiler/heptagon/hept_printer.ml
View file

@ -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 "@[<v>reset@,";
fprintf ff " @[<v>";
print_eq_list ff eq_list;
print_block ff b;
fprintf ff "@]";
fprintf ff "@,every ";
print_exp ff e;

4
compiler/heptagon/heptagon.ml
View file

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

10
compiler/heptagon/parsing/hept_parser.mly
View file

@ -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:

2
compiler/heptagon/parsing/hept_parsetree.ml
View file

@ -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 =

6
compiler/heptagon/parsing/hept_scoping.ml
View file

@ -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

6
compiler/heptagon/transformations/automata_mapfold.ml
View file

@ -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 } =

3
compiler/heptagon/transformations/inline.ml
View file

@ -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

2
compiler/heptagon/transformations/present_mapfold.ml
View file

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

4
compiler/heptagon/transformations/reset_mapfold.ml
View file

@ -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)
| _ ->