diff --git a/compiler/heptagon/transformations/reset_mapfold.ml b/compiler/heptagon/transformations/reset_mapfold.ml new file mode 100644 index 0000000..a3b399a --- /dev/null +++ b/compiler/heptagon/transformations/reset_mapfold.ml @@ -0,0 +1,218 @@ +(**************************************************************************) +(* *) +(* Heptagon *) +(* *) +(* Author : Marc Pouzet *) +(* Organization : Demons, LRI, University of Paris-Sud, Orsay *) +(* *) +(**************************************************************************) +(* removing reset statements *) + + +open Misc +open Ident +open Heptagon +open Hept_mapfold +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_op_app Eifthenelse [init e3; e2; e3] + | _ -> (* a reset occurs *) + mk_op_app Eifthenelse [exp_of_res res; e2; e3] + +(* add an equation *) +let equation v acc_eq_list e = + let n = Ident.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 mk_local_equation i k m lm = + (* m_i = false; m_j = l_mj *) + if i = k then + mk_simple_equation (Evarpat m) dfalse + else + mk_simple_equation (Evarpat m) (mk_bool_var lm) + +let mk_global_equation res m lm = + (* [ l_m1 = if res then true else true fby m1;...; + l_mn = if res then true else true fby mn ] *) + let e = + (match res with + | Rfalse -> pre_true (mk_bool_var m) + | _ -> mk_exp (ifres res dtrue (pre_true (mk_bool_var m))) + (Tid Initial.pbool) + ) in + mk_simple_equation (Evarpat lm) e + +let statefull eq_list = List.exists (fun eq -> eq.eq_statefull) eq_list + + +let edesc funs (res, v, acc_eq_list) ed = + let ed, _ = Hept_mapfold.edesc funs (res, v, acc_eq_list) ed in + let ed = match ed with + | Efby (e1, e2) -> + (match res, e1 with + | Rfalse, { e_desc = Econst c } -> + (* no reset *) + Epre(Some c, e2) + | _ -> + ifres res e1 + { e2 with e_desc = Epre(default e1, e2) } + ) + | Eapp({ a_op = Earrow }, [e1;e2], _) -> + ifres res e1 e2 + + (* add reset to the current reset exp. *) + | Eapp({ a_op = Enode _ } as op, e_list, Some re) -> + 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) -> + if true_reset res then + Eapp(op, e_list, Some (exp_of_res res)) + else + Eapp(op, e_list, None) + (* add reset to the current reset exp. *) + | Eiterator(it, ({ a_op = Enode _ } as op), n, e_list, Some re) -> + 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) -> + if true_reset res then + Eiterator(it, op, n, e_list, Some (exp_of_res res)) + else + Eiterator(it, op, n, e_list, None) + | _ -> ed + in + ed, (res, v, acc_eq_list) + +let switch_handlers funs (res, v, acc_eq_list) switch_handlers = + (* introduce a reset bit for each branch *) + let m_list = List.map (fun _ -> Ident.fresh "r") switch_handlers in + let lm_list = List.map (fun _ -> Ident.fresh "r") switch_handlers in + + let body i ({ w_block = b } as sh) m lm = + let defnames = List.fold_left (fun acc m -> + Env.add m (Tid Initial.pbool) acc) b.b_defnames m_list in + let _, (_, v, acc_eq_list) = + mapfold (eq_it funs) (rvar lm, b.b_local, []) b.b_equs in + let added_eqs = mapi2 (mk_local_equation i) m_list lm_list in + { sh with w_block = { b with b_local = v; b_defnames = defnames; + b_equs = added_eqs @ acc_eq_list } } in + + let v = (List.map mk_bool_param m_list)@ + (List.map mk_bool_param lm_list)@v in + let switch_handlers = mapi3 body switch_handlers m_list lm_list in + let added_eqs = List.map2 (mk_global_equation res) m_list lm_list in + + v, switch_handlers, acc_eq_list @ added_eqs + +let eq funs (res, v, acc_eq_list) equ = + match equ.eq_desc with + | Eswitch(e, sh) -> + let e, _ = exp_it funs (res, v, acc_eq_list) e in + let v, sh, acc_eq_list = + 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) -> + let e, _ = exp_it funs (res, v, acc_eq_list) e in + let v, acc_eq_list, res = + if statefull eq_list then + orthen v acc_eq_list res e + else + let _, v, acc_eq_list = equation v acc_eq_list e in + v, acc_eq_list, res + in + let _, (res, v, acc_eq_list) = + mapfold (eq_it funs) (res, v, acc_eq_list) eq_list in + equ, (res, v, acc_eq_list) + + | _ -> + let equ, (res, v, acc_eq_list) = eq funs (res, v, acc_eq_list) equ in + equ, (res, v, equ::acc_eq_list) + + +let node funs _ n = + let n, (_, v, eq_list) = Hept_mapfold.node_dec funs (rfalse, [], []) n in + { n with n_local = v @ n.n_local; n_equs = eq_list; }, (rfalse, [], []) + +let program p = + let funs = { Hept_mapfold.hept_funs_default with + eq = eq; node_dec = node; edesc = edesc } in + let p, _ = program_it funs (rfalse, [], []) p in + p + diff --git a/compiler/utilities/misc.ml b/compiler/utilities/misc.ml index 1711454..b5b2389 100644 --- a/compiler/utilities/misc.ml +++ b/compiler/utilities/misc.ml @@ -207,3 +207,31 @@ let mapfold f acc l = ([],acc) l in List.rev l, acc +let mapi f l = + let rec aux i = function + | [] -> [] + | v::l -> (f i v)::(aux (i+1) l) + in + aux 0 l + +let mapi2 f l1 l2 = + let rec aux i l1 l2 = + match l1, l2 with + | [], [] -> [] + | [], _ -> invalid_arg "" + | _, [] -> invalid_arg "" + | v1::l1, v2::l2 -> (f i v1 v2)::(aux (i+1) l1 l2) + in + aux 0 l1 l2 + +let mapi3 f l1 l2 l3 = + let rec aux i l1 l2 l3 = + match l1, l2, l3 with + | [], [], [] -> [] + | [], _, _ -> invalid_arg "" + | _, [], _ -> invalid_arg "" + | _, _, [] -> invalid_arg "" + | v1::l1, v2::l2, v3::l3 -> + (f i v1 v2 v3)::(aux (i+1) l1 l2 l3) + in + aux 0 l1 l2 l3 diff --git a/compiler/utilities/misc.mli b/compiler/utilities/misc.mli index dc7691c..da9734e 100644 --- a/compiler/utilities/misc.mli +++ b/compiler/utilities/misc.mli @@ -161,4 +161,11 @@ exception Fallback (** Mapfold *) -val mapfold: ('a -> 'b -> 'c * 'a) -> 'a -> 'b list -> 'c list * 'a \ No newline at end of file +val mapfold: ('a -> 'b -> 'c * 'a) -> 'a -> 'b list -> 'c list * 'a + +(** Mapi *) +val mapi: (int -> 'a -> 'b) -> 'a list -> 'b list +val mapi2: (int -> 'a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list +val mapi3: (int -> 'a -> 'b -> 'c -> 'd) -> + 'a list -> 'b list -> 'c list -> 'd list +