From a81dd0b2b4299ec2c3e5ca582697f19c717ec456 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?C=C3=A9dric=20Pasteur?= Date: Mon, 26 Jul 2010 14:12:37 +0200 Subject: [PATCH] Remove old version of files --- compiler/heptagon/transformations/automata.ml | 219 -------------- .../heptagon/transformations/completion.ml | 80 ------ .../transformations/completion_mapfold.ml | 58 ---- compiler/heptagon/transformations/every.ml | 131 --------- compiler/heptagon/transformations/last.ml | 102 ------- compiler/heptagon/transformations/present.ml | 68 ----- compiler/heptagon/transformations/reset.ml | 271 ------------------ 7 files changed, 929 deletions(-) delete mode 100644 compiler/heptagon/transformations/automata.ml delete mode 100644 compiler/heptagon/transformations/completion.ml delete mode 100644 compiler/heptagon/transformations/completion_mapfold.ml delete mode 100644 compiler/heptagon/transformations/every.ml delete mode 100644 compiler/heptagon/transformations/last.ml delete mode 100644 compiler/heptagon/transformations/present.ml delete mode 100644 compiler/heptagon/transformations/reset.ml diff --git a/compiler/heptagon/transformations/automata.ml b/compiler/heptagon/transformations/automata.ml deleted file mode 100644 index af0ddc5..0000000 --- a/compiler/heptagon/transformations/automata.ml +++ /dev/null @@ -1,219 +0,0 @@ -(**************************************************************************) -(* *) -(* Heptagon *) -(* *) -(* Author : Marc Pouzet *) -(* Organization : Demons, LRI, University of Paris-Sud, Orsay *) -(* *) -(**************************************************************************) -(* removing automata statements *) - -(* $Id$ *) - -open Misc -open Names -open Idents -open Heptagon -open Types - -let mk_var_exp n ty = - mk_exp (Evar n) ty - -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)) - -let mk_switch_equation e l = - mk_equation (Eswitch (e, l)) - -let mk_exp_fby_false e = - mk_exp (Epre (Some (mk_static_exp (Sconstructor Initial.pfalse)), e)) - (Tid Initial.pbool) - -let mk_exp_fby_state initial e = - { e with e_desc = Epre (Some (mk_static_exp (Sconstructor initial)), e) } - -(* the list of enumerated types introduced to represent states *) -let state_type_dec_list = ref [] - -let intro_type states = - let list env = NamesEnv.fold (fun _ state l -> state :: l) env [] in - let n = gen_symbol () in - let state_type = "st" ^ n in - state_type_dec_list := - (mk_type_dec state_type (Type_enum (list states))) :: !state_type_dec_list; - Name(state_type) - -(* an automaton may be a Moore automaton, i.e., with only weak transitions; *) -(* a Mealy one, i.e., with only strong transition or mixed *) -let moore_mealy state_handlers = - let handler (moore, mealy) { s_until = l1; s_unless = l2 } = - (moore or (l1 <> []), mealy or (l2 <> [])) in - List.fold_left handler (false, false) state_handlers - -let rec translate_eq (v, eq_list) eq = - match eq.eq_desc with - Eautomaton(state_handlers) -> - translate_automaton v eq_list state_handlers - | Eswitch(e, switch_handlers) -> - let eq = { eq with eq_desc = - Eswitch(e, translate_switch_handlers switch_handlers) } in - v, eq::eq_list - | Epresent(present_handlers, block) -> - let eq = { eq with eq_desc = - Epresent(translate_present_handlers present_handlers, - 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 - 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 - -and translate_block ({ b_local = v; b_equs = eq_list } as b) = - let v, eq_list = translate_eqs v eq_list in - { b with b_local = v; b_equs = eq_list } - -and translate_switch_handlers handlers = - let translate_switch_handler { w_name = n; w_block = b } = - { w_name = n; w_block = translate_block b } in - List.map translate_switch_handler handlers - -and translate_present_handlers handlers = - let translate_present_handler { p_cond = e; p_block = b } = - { p_cond = e; p_block = translate_block b } in - List.map translate_present_handler handlers - -and translate_automaton v eq_list handlers = - let has_until, has_unless = moore_mealy handlers in - let states = - let suffix = gen_symbol () in - List.fold_left - (fun env { s_state = n } -> NamesEnv.add n (n ^ suffix) env) - NamesEnv.empty handlers in - - let statetype = intro_type states in - let tstatetype = Tid statetype in - let initial = Name(NamesEnv.find (List.hd handlers).s_state states) in - - let statename = Idents.fresh "s" in - let next_statename = Idents.fresh "ns" in - let resetname = Idents.fresh "r" in - let next_resetname = Idents.fresh "nr" in - let pre_next_resetname = Idents.fresh "pnr" in - - let name n = Name(NamesEnv.find n states) in - let state n = mk_exp (Econst (mk_static_exp - (Sconstructor (name n)))) tstatetype in - let statevar n = mk_var_exp n tstatetype in - let boolvar n = mk_var_exp n (Tid Initial.pbool) in - - 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 - - let strong { s_state = n; s_unless = su } = - 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 - 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 = defnames; - } - in - - let v = - (mk_var_dec next_statename (Tid(statetype))) :: - (mk_var_dec resetname (Tid Initial.pbool)) :: - (mk_var_dec next_resetname (Tid Initial.pbool)) :: - (mk_var_dec pre_next_resetname (Tid Initial.pbool)) :: v in - (* we optimise the case of an only strong automaton *) - (* or only weak automaton *) - match has_until, has_unless with - | true, false -> - 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 *) - 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 - { c with c_local = v; c_eq = eq_list } - -let node ({ n_local = v; n_equs = eq_list; n_contract = contract } as n) = - let v, eq_list = translate_eqs v eq_list in - let contract = optional translate_contract contract in - { n with n_local = v; n_equs = eq_list; n_contract = contract } - -let program ({ p_types = pt_list; p_nodes = n_list } as p) = - let n_list = List.map node n_list in - { p with p_types = !state_type_dec_list @ pt_list; - p_nodes = n_list } - -(* - A -> do ... unless c1 then A1 ... until c'1 then A'1 ... - - match A fby next_state with - A -> resA = pre_next_res or (if c1 then ... else .. - - match state with - A -> reset - next_res = if c'1 then true else ... else false - every resA - - if faut donc: - une memoire pour pre(next_res) + n memoires (pre(resA),...) - - merge state - (A -> reset ... when A(state) every pre_next_res or res) -*) diff --git a/compiler/heptagon/transformations/completion.ml b/compiler/heptagon/transformations/completion.ml deleted file mode 100644 index 74c4336..0000000 --- a/compiler/heptagon/transformations/completion.ml +++ /dev/null @@ -1,80 +0,0 @@ -(**************************************************************************) -(* *) -(* Heptagon *) -(* *) -(* Author : Marc Pouzet *) -(* Organization : Demons, LRI, University of Paris-Sud, Orsay *) -(* *) -(**************************************************************************) -(* complete partial definitions with [x = last(x)] *) - -open Misc -open Heptagon -open Idents - -(* adds an equation [x = last(x)] for every partially defined variable *) -(* in a control structure *) -let complete_with_last defined_names local_defined_names eq_list = - let last n ty = mk_exp (Elast n) ty in - let equation n ty eq_list = - (mk_equation (Eeq(Evarpat n, last n ty)))::eq_list - in - let d = Env.diff defined_names local_defined_names in - Env.fold equation d eq_list - -let rec translate_eq eq = - match eq.eq_desc with - | Ereset(eq_list, e) -> - { eq with eq_desc = Ereset(translate_eqs eq_list, e) } - | Eeq(pat, e) -> - { eq with eq_desc = Eeq(pat, e) } - | Eswitch(e, switch_handlers) -> - let defnames = - List.fold_left - (fun acc { w_block = { b_defnames = d } } -> Env.union acc d) - Env.empty switch_handlers in - let switch_handlers = - List.map (fun ({ w_block = b } as handler) -> - { handler with w_block = translate_block defnames b }) - switch_handlers in - { eq with eq_desc = Eswitch(e, switch_handlers) } - | Epresent(present_handlers, b) -> - let defnames = - List.fold_left - (fun acc { p_block = { b_defnames = d } } -> Env.union acc d) - b.b_defnames present_handlers in - let present_handlers = - List.map (fun ({ p_block = b } as handler) -> - { handler with p_block = translate_block defnames b }) - present_handlers in - let b = translate_block defnames b in - {eq with eq_desc = Epresent(present_handlers, b)} - | Eautomaton(state_handlers) -> - let defnames = - List.fold_left - (fun acc { s_block = { b_defnames = d } } -> Env.union acc d) - Env.empty state_handlers in - let state_handlers = - List.map (fun ({ s_block = b } as handler) -> - { handler with s_block = translate_block defnames b }) - state_handlers in - { eq with eq_desc = Eautomaton(state_handlers) } - -and translate_eqs eq_list = List.map translate_eq eq_list - -and translate_block defnames - ({ b_defnames = bdefnames; b_equs = eq_list } as b) = - let eq_list = translate_eqs eq_list in - let eq_list = complete_with_last defnames bdefnames eq_list in - { b with b_equs = eq_list; b_defnames = defnames } - -let translate_contract ({ c_eq = eqs } as c) = - { c with c_eq = translate_eqs eqs } - -let node ({ n_equs = eq_list; n_contract = contract } as n) = - { n with - n_equs = translate_eqs eq_list; - n_contract = optional translate_contract contract } - -let program ({ p_types = pt_list; p_nodes = n_list } as p) = - { p with p_types = pt_list; p_nodes = List.map node n_list } diff --git a/compiler/heptagon/transformations/completion_mapfold.ml b/compiler/heptagon/transformations/completion_mapfold.ml deleted file mode 100644 index fbacfaa..0000000 --- a/compiler/heptagon/transformations/completion_mapfold.ml +++ /dev/null @@ -1,58 +0,0 @@ -(**************************************************************************) -(* *) -(* Heptagon *) -(* *) -(* Author : Marc Pouzet *) -(* Organization : Demons, LRI, University of Paris-Sud, Orsay *) -(* *) -(**************************************************************************) -(* complete partial definitions with [x = last(x)] *) - -open Misc -open Heptagon -open Global_mapfold -open Hept_mapfold -open Idents - -(* adds an equation [x = last(x)] for every partially defined variable *) -(* in a control structure *) -let complete_with_last defined_names local_defined_names eq_list = - let last n ty = mk_exp (Elast n) ty in - let equation n ty eq_list = - (mk_equation (Eeq(Evarpat n, last n ty)))::eq_list - in - let d = Env.diff defined_names local_defined_names in - Env.fold equation d eq_list - -let block funs (defnames,collect) b = - if collect then - b, (b.b_defnames, collect) - else - let b, _ = Hept_mapfold.block funs (Env.empty, false) b in - let added_eq = complete_with_last defnames b.b_defnames [] in - { b with b_equs = b.b_equs @ added_eq; b_defnames = defnames }, - (Env.empty, false) - -let eqdesc funs _ ed = - match ed with - | Epresent _ | Eautomaton _ | Eswitch _ -> - (* collect defined names *) - let ed, (defnames, _) = Hept_mapfold.eqdesc funs (Env.empty, true) ed in - (* add missing defnames *) - Hept_mapfold.eqdesc funs (defnames, false) ed - - | _ -> raise Misc.Fallback - -let gather (acc, collect) (local_acc, collect) = - Env.union local_acc acc, collect - -let program p = - let funs = - { Hept_mapfold.defaults - with eqdesc = eqdesc; block = block; - switch_handler = it_gather gather Hept_mapfold.switch_handler; - present_handler = it_gather gather Hept_mapfold.present_handler; - state_handler = it_gather gather Hept_mapfold.state_handler; } in - let p, _ = program_it funs (Env.empty, false) p in - p - diff --git a/compiler/heptagon/transformations/every.ml b/compiler/heptagon/transformations/every.ml deleted file mode 100644 index b3401d3..0000000 --- a/compiler/heptagon/transformations/every.ml +++ /dev/null @@ -1,131 +0,0 @@ -(**************************************************************************) -(* *) -(* Heptagon *) -(* *) -(* Author : Marc Pouzet *) -(* Organization : Demons, LRI, University of Paris-Sud, Orsay *) -(* *) -(**************************************************************************) - -(* removing complex reset expressions : - equations - x = (f every e) e' - --> - r = e; - x = (f every r) e' -*) - -open Misc -open Idents -open Heptagon -open Reset - -(* - let defnames m n d = - let rec loop acc k = if k < n then loop (S.add m.(k) acc) (k+1) else acc in - loop d 0 -*) - -let statefull eq_list = List.exists (fun eq -> eq.eq_statefull) eq_list - -let is_var = function - | { e_desc = Evar _ } -> true - | _ -> false - -let rec translate_eq v acc_eq_list eq = - match eq.eq_desc with - | Eeq(pat, e) -> - let v,acc_eq_list,e = translate v acc_eq_list e in - v, { eq with eq_desc = Eeq(pat, e) } :: acc_eq_list - | Eswitch(e, tag_block_list) -> - let v,acc_eq_list,e = translate v acc_eq_list e in - let tag_block_list, acc_eq_list = - translate_switch acc_eq_list tag_block_list in - v, { eq with eq_desc = Eswitch(e, tag_block_list) } :: acc_eq_list - | Ereset _ | Epresent _ | Eautomaton _ -> assert false - -and translate_eqs v acc_eq_list eq_list = - List.fold_left - (fun (v,acc_eq_list) eq -> - translate_eq v acc_eq_list eq) (v,acc_eq_list) eq_list - -and translate_switch acc_eq_list switch_handlers = - - let body {w_name = c; - w_block = ({ b_local = lv; b_defnames = d; b_equs = eqs } as b)} = - let lv,eqs = translate_eqs lv [] eqs in - { w_name = c; - w_block = { b with b_local = lv; b_defnames = d; b_equs = eqs } } in - - let rec loop switch_handlers = - match switch_handlers with - [] -> [] - | handler :: switch_handlers -> - (body handler) :: (loop switch_handlers) in - - loop switch_handlers, acc_eq_list - -and translate v acc_eq_list e = - match e.e_desc with - Econst _ | Evar _ | Elast _ | Efby _ | Epre _ -> v,acc_eq_list,e - | Eapp (op, e_list, Some re) when not (is_var re) -> - let v, acc_eq_list,re = translate v acc_eq_list re in - let n, v, acc_eq_list = equation v acc_eq_list re in - let v, acc_eq_list, e_list = translate_list v acc_eq_list e_list in - let re = { re with e_desc = Evar(n) } in - v,acc_eq_list, - { e with e_desc = Eapp (op, e_list, Some re) } - | Eiterator(it, op, n, e_list, Some re) when not (is_var re) -> - let v, acc_eq_list,re = translate v acc_eq_list re in - let x, v, acc_eq_list = equation v acc_eq_list re in - let v, acc_eq_list, e_list = translate_list v acc_eq_list e_list in - let re = { re with e_desc = Evar x } in - v,acc_eq_list, - { e with e_desc = Eiterator(it, op, n, e_list, Some re) } - | Eapp(op, e_list, r) -> - let v, acc_eq_list, e_list = translate_list v acc_eq_list e_list in - v, acc_eq_list, - { e with e_desc = Eapp(op, e_list, r) } - | Eiterator(it, op, n, e_list, r) -> - let v, acc_eq_list, e_list = translate_list v acc_eq_list e_list in - v, acc_eq_list, - { e with e_desc = Eiterator(it, op, n, e_list, r) } - | Estruct(e_f_list) -> - let v,acc_eq_list,e_f_list = - List.fold_left - (fun (v,acc_eq_list,acc_e_f) (f,e) -> - let v,acc_eq_list,e = translate v acc_eq_list e in - (v,acc_eq_list,(f,e)::acc_e_f)) - (v,acc_eq_list,[]) e_f_list in - v,acc_eq_list, - { e with e_desc = Estruct(List.rev e_f_list) } - -and translate_list v acc_eq_list e_list = - let v,acc_eq_list,acc_e = - List.fold_left - (fun (v,acc_eq_list,acc_e) e -> - let v,acc_eq_list,e = translate v acc_eq_list e in - (v,acc_eq_list,e::acc_e)) - (v,acc_eq_list,[]) e_list in - v,acc_eq_list,List.rev acc_e - -let translate_contract ({ c_local = v; - c_eq = eq_list; - c_assume = e_a; - c_enforce = e_g } as c) = - let v,acc_eq,e_a = translate v [] e_a in - let v,acc_eq,e_g = translate v acc_eq e_g in - let v, eq_list = translate_eqs v acc_eq eq_list in - { c with - c_local = v; - c_eq = eq_list; - c_assume = e_a; - c_enforce = e_g } - -let node ({ n_local = v; n_equs = eq_list; n_contract = contract } as n) = - let contract = optional translate_contract contract in - let v, eq_list = translate_eqs v [] eq_list in - { n with n_local = v; n_equs = eq_list; n_contract = contract } - -let program ({ p_types = pt_list; p_nodes = n_list } as p) = - { p with p_types = pt_list; p_nodes = List.map node n_list } diff --git a/compiler/heptagon/transformations/last.ml b/compiler/heptagon/transformations/last.ml deleted file mode 100644 index baad46a..0000000 --- a/compiler/heptagon/transformations/last.ml +++ /dev/null @@ -1,102 +0,0 @@ -(**************************************************************************) -(* *) -(* Heptagon *) -(* *) -(* Author : Marc Pouzet *) -(* Organization : Demons, LRI, University of Paris-Sud, Orsay *) -(* *) -(**************************************************************************) -(* removing accessed to shared variables (last x) *) - -open Misc -open Heptagon -open Idents - -(* introduce a fresh equation [last_x = pre(x)] for every *) -(* variable declared with a last *) -let last (eq_list, env, v) { v_ident = n; v_type = t; v_last = last } = - match last with - | Var -> (eq_list, env, v) - | Last(default) -> - let lastn = Idents.fresh ("last" ^ (sourcename n)) in - let eq = mk_equation (Eeq (Evarpat lastn, - mk_exp (Epre (default, - mk_exp (Evar n) t)) t)) in - eq:: eq_list, - Env.add n lastn env, - (mk_var_dec lastn t) :: v - -let extend_env env v = List.fold_left last ([], env, []) v - -let rec translate_eq env eq = - match eq.eq_desc with - | Ereset(eq_list, e) -> - { eq with eq_desc = Ereset(translate_eqs env eq_list, translate env e) } - | Eeq(pat, e) -> - { eq with eq_desc = Eeq(pat, translate env e) } - | Eswitch(e, handler_list) -> - let handler_list = - List.map (fun ({ w_block = b } as handler) -> - { handler with w_block = translate_block env b }) - handler_list in - { eq with eq_desc = Eswitch(translate env e, handler_list) } - | Epresent _ | Eautomaton _ -> assert false - -and translate_eqs env eq_list = List.map (translate_eq env) eq_list - -and translate_block env ({ b_local = v; b_equs = eq_list } as b) = - let eq_lastn_n_list, env, last_v = extend_env env v in - let eq_list = translate_eqs env eq_list in - { b with b_local = v @ last_v; b_equs = eq_lastn_n_list @ eq_list } - -and translate env e = - match e.e_desc with - | Econst _ | Evar _ -> e - | Elast(x) -> - let lx = Env.find x env in { e with e_desc = Evar(lx) } - | Epre(c, e) -> - { e with e_desc = Epre(c, translate env e) } - | Efby (e1, e2) -> - { e with e_desc = Efby(translate env e1, translate env e2) } - | Eapp(op, e_list, r) -> - { e with e_desc = Eapp(op, List.map (translate env) e_list, r) } - | Estruct(e_f_list) -> - { e with e_desc = - Estruct(List.map (fun (f, e) -> (f, translate env e)) e_f_list) } - | Eiterator(it, app, n, e_list, r) -> - { e with e_desc = Eiterator(it, app, n, - List.map (translate env) e_list, r) } - -let translate_contract env contract = - match contract with - | None -> None, env - | Some { c_local = v; - c_eq = eq_list; - c_assume = e_a; - c_enforce = e_g } -> - let eq_lastn_n_list, env', last_v = extend_env env v in - let eq_list = translate_eqs env' eq_list in - let e_a = translate env' e_a in - let e_g = translate env' e_g in - Some { c_local = v @ last_v; - c_eq = eq_lastn_n_list @ eq_list; - c_assume = e_a; - c_enforce = e_g }, - env - -let node ({ n_input = i; n_local = v; n_output = o; - n_equs = eq_list; n_contract = contract } as n) = - let _, env, _ = extend_env Env.empty i in - let eq_lasto_list, env, last_o = extend_env env o in - let contract, env = translate_contract env contract in - let eq_lastn_n_list, env, last_v = extend_env env v in - let eq_list = translate_eqs env eq_list in - { n with - n_input = i; - n_output = o; - n_local = v @ last_o @ last_v; - n_contract = contract; - n_equs = eq_lasto_list @ eq_lastn_n_list @ eq_list } - -let program ({ p_types = pt_list; p_nodes = n_list } as p) = - { p with p_types = pt_list; p_nodes = List.map node n_list } diff --git a/compiler/heptagon/transformations/present.ml b/compiler/heptagon/transformations/present.ml deleted file mode 100644 index 28fb0c0..0000000 --- a/compiler/heptagon/transformations/present.ml +++ /dev/null @@ -1,68 +0,0 @@ -(**************************************************************************) -(* *) -(* Heptagon *) -(* *) -(* Author : Marc Pouzet *) -(* Organization : Demons, LRI, University of Paris-Sud, Orsay *) -(* *) -(**************************************************************************) -(* removing present statements *) - -(* $Id$ *) - -open Misc -open Location -open Heptagon -open Initial - -let rec translate_eq v eq = - match eq.eq_desc with - | Eswitch(e, switch_handlers) -> - v, { eq with eq_desc = - Eswitch(e, translate_switch_handlers switch_handlers) } - | Epresent(present_handlers, block) -> - v, - translate_present_handlers present_handlers (translate_block block) - | Ereset(eq_list, e) -> - let v, eq_list = translate_eqs v eq_list in - v, { eq with eq_desc = Ereset(eq_list, e) } - | Eeq _ -> v, eq - | Eautomaton _ -> assert false - -and translate_eqs v eq_list = - List.fold_left - (fun (v, eq_list) eq -> - let v, eq = translate_eq v eq in v, eq :: eq_list) - (v, []) eq_list - -and translate_block ({ b_local = v; b_equs = eq_list } as b) = - let v, eq_list = translate_eqs v eq_list in - { b with b_local = v; b_equs = eq_list } - -and translate_switch_handlers handlers = - let translate_switch_handler { w_name = n; w_block = b } = - { w_name = n; w_block = translate_block b } in - List.map translate_switch_handler handlers - -and 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_switch_equation - ~statefull:statefull e - [{ w_name = ptrue; w_block = b }; - { w_name = pfalse; w_block = cont }]] in - let b = List.fold_right translate_present_handler handlers cont in - List.hd (b.b_equs) - -let translate_contract ({ c_local = v; c_eq = eq_list} as c) = - let v, eq_list = translate_eqs v eq_list in - { c with c_local = v; c_eq = eq_list } - -let node ({ n_local = v; n_equs = eq_list; n_contract = contract } as n) = - let v, eq_list = translate_eqs v eq_list in - let contract = optional translate_contract contract in - { n with n_local = v; n_equs = eq_list; n_contract = contract } - -let program ({ p_types = pt_list; p_nodes = n_list } as p) = - { p with p_types = pt_list; p_nodes = List.map node n_list } diff --git a/compiler/heptagon/transformations/reset.ml b/compiler/heptagon/transformations/reset.ml deleted file mode 100644 index cf06102..0000000 --- a/compiler/heptagon/transformations/reset.ml +++ /dev/null @@ -1,271 +0,0 @@ -(**************************************************************************) -(* *) -(* Heptagon *) -(* *) -(* Author : Marc Pouzet *) -(* Organization : Demons, LRI, University of Paris-Sud, Orsay *) -(* *) -(**************************************************************************) -(* removing reset statements *) - - -open Misc -open Idents -open Heptagon -open Types - -(* We introduce an initialization variable for each block *) -(* Using an asynchronous reset would allow to produce *) -(* better code avoiding to introduce n local variables and *) -(* n state variables *) -(* reset - switch e with - case C1 do ... - | case C2 do ... - | case C3 do ... - end - every r - - switch e with - case C1 do ... (* l_m1 *) - m1 = false; m2 = l_m2; m3 = l_m3 - | case C2 do ... (* l_m2 *) - m1 = l_m1; m2 = false; m3 = l_m3 - | case C3 do ... (* l_m3 *) - m1 = l_m1; m2 = l_m2; m3 = false - end; - l_m1 = if res then true else true fby m1;...; - l_m3 = if res then true else true fby m3 - - e1 -> e2 is translated into if (true fby false) then e1 else e2 -*) - -let mk_bool_var n = - mk_exp (Evar n) (Tid Initial.pbool) -let mk_bool_param n = - mk_var_dec n (Tid Initial.pbool) - -let or_op_call = mk_op (Efun Initial.por) - -let pre_true e = - { e with e_desc = Epre (Some (mk_static_exp ~ty:(Tid Initial.pbool) - (Sconstructor Initial.ptrue)), e) } -let init e = pre_true { dfalse with e_loc = e.e_loc } - -(* the boolean condition for a structural reset *) -type reset = - | Rfalse - | Rorthen of reset * ident - -let rfalse = Rfalse -let rvar n = Rorthen(Rfalse, n) - -let true_reset = function - | Rfalse -> false - | _ -> true - -let rec or_op res e = - match res with - | Rfalse -> e - | Rorthen(res, n) -> - or_op res { e with e_desc = Eapp(or_op_call, [mk_bool_var n; e], None) } - -let default e = - match e.e_desc with - | Econst c -> Some c - | _ -> None - -let exp_of_res res = - match res with - | Rfalse -> dfalse - | Rorthen(res, n) -> or_op res (mk_bool_var n) - -let ifres res e2 e3 = - match res with - | Rfalse -> mk_ifthenelse (init e3) e2 e3 - | _ -> (* a reset occurs *) - mk_ifthenelse (exp_of_res res) e2 e3 - -(* add an equation *) -let equation v acc_eq_list e = - let n = Idents.fresh "r" in - n, - (mk_bool_param n) :: v, - (mk_equation (Eeq(Evarpat n, e))) ::acc_eq_list - -let orthen v acc_eq_list res e = - match e.e_desc with - | Evar(n) -> v, acc_eq_list, Rorthen(res, n) - | _ -> - let n, v, acc_eq_list = equation v acc_eq_list e in - v, acc_eq_list, Rorthen(res, n) - -let add_locals m n locals = - let rec loop locals i n = - if i < n then - loop ((mk_bool_param m.(i)) :: locals) (i+1) n - else locals in - loop locals 0 n - -let add_local_equations i n m lm acc = - (* [mi = false;...; m1 = l_m1;...; mn = l_mn] *) - let rec loop acc k = - if k < n then - if k = i - then loop ((mk_simple_equation (Evarpat (m.(k))) dfalse) :: acc) (k+1) - else - loop - ((mk_simple_equation (Evarpat (m.(k))) (mk_bool_var lm.(k))) :: acc) - (k+1) - else acc - in loop acc 0 - -let add_global_equations n m lm res acc = - (* [ l_m1 = if res then true else true fby m1;...; - l_mn = if res then true else true fby mn ] *) - let rec loop acc k = - if k < n then - let exp = - (match res with - | Rfalse -> pre_true (mk_bool_var m.(k)) - | _ -> ifres res dtrue (pre_true (mk_bool_var m.(k))) - ) in - loop - ((mk_equation (Eeq (Evarpat (lm.(k)), exp))) :: acc) (k+1) - else acc in - loop acc 0 - -let defnames m n d = - let rec loop acc k = - if k < n - then loop (Env.add m.(k) (Tid Initial.pbool) acc) (k+1) - else acc in - loop d 0 - -let statefull eq_list = List.exists (fun eq -> eq.eq_statefull) eq_list - -let rec translate_eq res v acc_eq_list eq = - match eq.eq_desc with - | Ereset(eq_list, e) -> - let e = translate res e in - if statefull eq_list then - let v, acc_eq_list, res = orthen v acc_eq_list res e in - translate_eqs res v acc_eq_list eq_list - else - let _, v, acc_eq_list = equation v acc_eq_list e in - translate_eqs res v acc_eq_list eq_list - | Eeq(pat, e) -> - v, { eq with eq_desc = Eeq(pat, translate res e) } :: acc_eq_list - | Eswitch(e, tag_block_list) -> - let e = translate res e in - let v, tag_block_list, acc_eq_list = - translate_switch res v acc_eq_list tag_block_list in - v, { eq with eq_desc = Eswitch(e, tag_block_list) } :: acc_eq_list - | Epresent _ | Eautomaton _ -> assert false - -and translate_eqs res v acc_eq_list eq_list = - List.fold_left - (fun (v, acc_eq_list) eq -> - translate_eq res v acc_eq_list eq) (v, acc_eq_list) eq_list - -and translate_switch res locals acc_eq_list switch_handlers = - (* introduce a reset bit for each branch *) - let tab_of_vars n = Array.init n (fun _ -> Idents.fresh "r") in - let n = List.length switch_handlers in - let m = tab_of_vars n in - let lm = tab_of_vars n in - - let locals = add_locals m n locals in - let locals = add_locals lm n locals in - - let body i {w_name = ci; - w_block = ({ b_local = li; b_defnames = d; b_equs = eqi } as b)} = - let d = defnames m n d in - let li, eqi = translate_eqs (rvar (lm.(i))) li [] eqi in - let eqi = add_local_equations i n m lm eqi in - { w_name = ci; - w_block = { b with b_local = li; b_defnames = d; b_equs = eqi } } in - - let rec loop i switch_handlers = - match switch_handlers with - [] -> [] - | handler :: switch_handlers -> - (body i handler) :: (loop (i+1) switch_handlers) in - - let acc_eq_list = add_global_equations n m lm res acc_eq_list in - - locals, loop 0 switch_handlers, acc_eq_list - -and translate res e = - match e.e_desc with - | Econst _ | Evar _ | Elast _ -> e - | Efby (e1, e2) -> - let e1 = translate res e1 in - let e2 = translate res e2 in - begin - match res, e1 with - | Rfalse, { e_desc = Econst c } -> - (* no reset *) - { e with e_desc = Epre(Some c, e2) } - | _ -> - ifres res e1 - { e with e_desc = Epre(default e1, e2) } - end - | Eapp({ a_op = Earrow }, [e1;e2], _) -> - let e1 = translate res e1 in - let e2 = translate res e2 in - ifres res e1 e2 - | Epre (c, e1) -> - { e with e_desc = Epre (c, translate res e1)} - - (* add reset to the current reset exp. *) - | Eapp({ a_op = Enode _ } as op, e_list, Some re) -> - let re = translate res re in - let e_list = List.map (translate res) e_list in - { e with e_desc = Eapp(op, e_list, Some (or_op res re)) } - (* create a new reset exp if necessary *) - | Eapp({ a_op = Enode _ } as op, e_list, None) -> - let e_list = List.map (translate res) e_list in - if true_reset res then - { e with e_desc = Eapp(op, e_list, Some (exp_of_res res)) } - else - { e with e_desc = Eapp(op, e_list, None) } - (* add reset to the current reset exp. *) - | Eiterator(it, ({ a_op = Enode _ } as op), n, e_list, Some re) -> - let re = translate res re in - let e_list = List.map (translate res) e_list in - { e with e_desc = Eiterator(it, op, n, e_list, Some (or_op res re)) } - (* create a new reset exp if necessary *) - | Eiterator(it, ({ a_op = Enode _ } as op), n, e_list, None) -> - let e_list = List.map (translate res) e_list in - if true_reset res then - { e - with e_desc = Eiterator(it, op, n, e_list, Some (exp_of_res res)) } - else - { e with e_desc = Eiterator(it, op, n, e_list, None) } - | Eiterator(it, op, n, e_list, r) -> - let e_list = List.map (translate res) e_list in - { e with e_desc = Eiterator(it, op, n, e_list, None) } - - | Eapp(op, e_list, _) -> - { e with e_desc = Eapp(op, List.map (translate res) e_list, None) } - | Estruct(e_f_list) -> - { e with e_desc = - Estruct(List.map (fun (f, e) -> (f, translate res e)) e_f_list) } - -let translate_contract ({ c_local = v; - c_eq = eq_list; - c_assume = e_a; - c_enforce = e_g } as c) = - let v, eq_list = translate_eqs rfalse v [] eq_list in - let e_a = translate rfalse e_a in - let e_g = translate rfalse e_g in - { c with c_local = v; c_eq = eq_list; c_assume = e_a; c_enforce = e_g } - -let node n = - let c = optional translate_contract n.n_contract in - let var, eqs = translate_eqs rfalse n.n_local [] n.n_equs in - { n with n_local = var; n_equs = eqs; n_contract = c } - -let program p = - { p with p_nodes = List.map node p.p_nodes }