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

Make the file more readable

Browse source 
Use let in and meaningfull names 
to show the structure of the functions 
(which shows that it is more simple that it 
appeared before)
This commit is contained in:
Cédric Pasteur 2010-06-22 14:30:22 +02:00 committed by Léonard Gérard
parent 30338a3f38
commit 7984917b0e
1 changed files with 65 additions and 51 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

116
compiler/heptagon/transformations/automata.ml
View file

@ -58,17 +58,18 @@ let rec translate_eq (v, eq_list) eq =
Eautomaton(state_handlers) ->
translate_automaton v eq_list state_handlers
| Eswitch(e, switch_handlers) ->
v,
{ eq with eq_desc =
Eswitch(e, translate_switch_handlers switch_handlers) }
:: eq_list
let eq = { eq with eq_desc =
Eswitch(e, translate_switch_handlers switch_handlers) } in
v, eq::eq_list
| Epresent(present_handlers, block) ->
v, { eq with eq_desc =
let eq = { eq with eq_desc =
Epresent(translate_present_handlers present_handlers,
translate_block block) } :: eq_list
translate_block block) } in
v, eq::eq_list
| Ereset(r_eq_list, e) ->
let v, r_eq_list = translate_eqs v r_eq_list in
v, { eq with eq_desc = Ereset(r_eq_list, e) } :: eq_list
let eq = { eq with eq_desc = Ereset(r_eq_list, e) } in
v, eq::eq_list
| Eeq _ -> v, eq :: eq_list
and translate_eqs v eq_list = List.fold_left translate_eq (v, []) eq_list
@ -112,30 +113,35 @@ and translate_automaton v eq_list handlers =
let escapes n s rcont =
let escape { e_cond = e; e_reset = r; e_next_state = n } cont =
mk_ifthenelse e (mk_pair (state n) (if r then dtrue else dfalse)) cont in
List.fold_right escape s (mk_pair (state n) rcont) in
mk_ifthenelse e (mk_pair (state n) (if r then dtrue else dfalse)) cont
in
List.fold_right escape s (mk_pair (state n) rcont)
in
let strong { s_state = n; s_unless = su } =
mk_block
(Env.add statename tstatetype
(Env.add resetname (Tid Initial.pbool) Env.empty))
([mk_reset_equation (
[mk_simple_equation (Etuplepat[Evarpat(statename);Evarpat(resetname)])
(escapes n su (boolvar pre_next_resetname))])
(boolvar pre_next_resetname)]) in
let defnames = Env.add resetname (Tid Initial.pbool) Env.empty in
let defnames = Env.add statename tstatetype defnames in
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)]
in
let weak { s_state = n; s_block = b; s_until = su } =
let b = translate_block b in
{ b with b_equs =
[mk_reset_equation ((mk_simple_equation (Etuplepat[Evarpat(next_statename);
Evarpat(next_resetname)])
(escapes n su dfalse)) :: b.b_equs)
(boolvar resetname)];
let defnames = Env.add next_resetname (Tid Initial.pbool) b.b_defnames in
let defnames = Env.add next_statename tstatetype defnames in
let ns_eq = mk_simple_equation
(Etuplepat[Evarpat(next_statename); Evarpat(next_resetname)])
(escapes n su dfalse) in
{ b with b_equs =
[mk_reset_equation (ns_eq::b.b_equs) (boolvar resetname)];
(* (or_op (boolvar pre_next_resetname) (boolvar resetname))]; *)
b_defnames =
Env.add next_statename tstatetype
(Env.add next_resetname (Tid Initial.pbool)
b.b_defnames)
} in
b_defnames = defnames;
}
in
let v =
(mk_var_dec next_statename (Tid(statetype))) ::
(mk_var_dec resetname (Tid Initial.pbool)) ::
@ -145,32 +151,40 @@ and translate_automaton v eq_list handlers =
(* or only weak automaton *)
match has_until, has_unless with
| true, false ->
(* a Moore automaton with only weak transitions *)
v, (mk_switch_equation (mk_exp_fby_state initial (statevar next_statename))
(List.map
(fun ({ s_state = n } as case) ->
{ w_name = name n; w_block = weak case })
handlers)) ::
(mk_simple_equation (Evarpat pre_next_resetname)
(mk_exp_fby_false (boolvar (next_resetname)))) ::
(mk_simple_equation (Evarpat resetname) (boolvar pre_next_resetname)) :: eq_list
let switch_e = mk_exp_fby_state initial (statevar next_statename) in
let switch_handlers = (List.map
(fun ({ s_state = n } as case) ->
{ w_name = name n; w_block = weak case })
handlers) in
let switch_eq = mk_switch_equation switch_e switch_handlers in
let nr_eq = mk_simple_equation (Evarpat pre_next_resetname)
(mk_exp_fby_false (boolvar (next_resetname))) in
let pnr_eq = mk_simple_equation (Evarpat resetname)
(boolvar pre_next_resetname) in
(* a Moore automaton with only weak transitions *)
v, switch_eq :: nr_eq :: pnr_eq :: eq_list
| _ ->
(* the general case; two switch to generate,
statename variable used and defined *)
(mk_var_dec statename (Tid statetype)) :: v,
(mk_switch_equation (mk_exp_fby_state initial (statevar next_statename))
(List.map
(fun ({ s_state = n } as case) ->
{ w_name = name n; w_block = strong case })
handlers)) ::
(mk_switch_equation (statevar statename)
(List.map
(fun ({ s_state = n } as case) ->
{ w_name = name n; w_block = weak case })
handlers)) ::
(mk_simple_equation (Evarpat pre_next_resetname)
(mk_exp_fby_false (boolvar (next_resetname)))) ::
eq_list
(* the general case; two switch to generate,
statename variable used and defined *)
let v = (mk_var_dec statename (Tid statetype)) :: v in
let ns_switch_e = mk_exp_fby_state initial (statevar next_statename) in
let ns_switch_handlers = List.map
(fun ({ s_state = n } as case) ->
{ w_name = name n; w_block = strong case })
handlers in
let ns_switch_eq = mk_switch_equation ns_switch_e ns_switch_handlers in
let switch_e = statevar statename in
let switch_handlers = List.map
(fun ({ s_state = n } as case) ->
{ w_name = name n; w_block = weak case })
handlers in
let switch_eq = mk_switch_equation switch_e switch_handlers in
let pnr_eq = mk_simple_equation (Evarpat pre_next_resetname)
(mk_exp_fby_false (boolvar (next_resetname))) in
v, ns_switch_eq :: switch_eq :: pnr_eq :: eq_list
let translate_contract ({ c_local = v; c_eq = eq_list} as c) =
let v, eq_list = translate_eqs v eq_list in