diff --git a/compiler/main/heptc.ml b/compiler/main/heptc.ml index ec22e06..0e46c04 100644 --- a/compiler/main/heptc.ml +++ b/compiler/main/heptc.ml @@ -78,6 +78,9 @@ let main () = "-stdlib", Arg.String set_stdlib, doc_stdlib; "-c", Arg.Set create_object_file, doc_object_file; "-s", read_qualname set_simulation_node, doc_sim; + "-tomato", Arg.Set tomato, doc_tomato; + "-tomanode", read_qualname add_tomato_node, doc_tomato; + "-tomacheck", read_qualname add_tomato_check, ""; "-inline", read_qualname add_inlined_node, doc_inline; "-flatten", Arg.Set flatten, doc_flatten; "-assert", read_qualname add_assert, doc_assert; diff --git a/compiler/minils/main/mls_compiler.ml b/compiler/minils/main/mls_compiler.ml index ce8d45f..cd2d32b 100644 --- a/compiler/minils/main/mls_compiler.ml +++ b/compiler/minils/main/mls_compiler.ml @@ -39,6 +39,14 @@ let compile pp p = (* Iterator fusion *) let p = pass "Iterator fusion" !do_iterator_fusion Itfusion.program p pp in + (* Automata minimization *) + let p = + let call_tomato = !tomato or (List.length !tomato_nodes > 0) in + pass "Automata minimization" call_tomato Tomato.program p pp in + + let p = + pass "Automata minimization checks" true Tomato.tomato_checks p pp in + (* Normalization to maximize opportunities *) let p = pass "Normalization" true Normalize.program p pp in diff --git a/compiler/minils/mls_mapfold.ml b/compiler/minils/mls_mapfold.ml index e9ef4d3..07fb58a 100644 --- a/compiler/minils/mls_mapfold.ml +++ b/compiler/minils/mls_mapfold.ml @@ -12,7 +12,7 @@ open Errors open Global_mapfold open Minils -(* /!\ do never, never put in your funs record one +(* /!\ do not ever, NEVER put in your funs record one of the generic iterator function (_it), either yours either the default version named according to the type. *) diff --git a/compiler/minils/mls_utils.ml b/compiler/minils/mls_utils.ml index dfbee6a..c7ab4b7 100644 --- a/compiler/minils/mls_utils.ml +++ b/compiler/minils/mls_utils.ml @@ -56,7 +56,6 @@ let is_record_type ty = match ty with let is_op = function | { qual = "Pervasives"; name = _ } -> true | _ -> false - let exp_list_of_static_exp_list se_list = let mk_one_const se = Minils.mk_exp ~ty:se.se_ty (Minils.Econst se) @@ -164,3 +163,5 @@ module AllDep = Dep.Make let def = Vars.def let antidep _ = false end) + +let eq_find id = List.find (fun eq -> List.mem id (Vars.def [] eq)) diff --git a/compiler/minils/transformations/checkpass.ml b/compiler/minils/transformations/checkpass.ml new file mode 100644 index 0000000..4ba1c96 --- /dev/null +++ b/compiler/minils/transformations/checkpass.ml @@ -0,0 +1,66 @@ +(**************************************************************************) +(* *) +(* Heptagon *) +(* *) +(* Author : Marc Pouzet *) +(* Organization : Demons, LRI, University of Paris-Sud, Orsay *) +(* *) +(**************************************************************************) + +open Misc +open Names +open Idents +open Signature +open Minils +open Mls_utils +open Mls_printer +open Global_printer +open Types +open Clocks + +let add_check prefix pass nd nd_list = + if nd.n_input <> [] + then (Format.eprintf "Cannot generate check for node %a with inputs" + print_qualname nd.n_name; assert false) + else + let nd'_name = { nd.n_name with name = prefix ^ "_" ^ nd.n_name.name; } in + let nd' = pass nd in + let nd' = { nd' with n_name = nd'_name; } in + let output = Idents.fresh "o" in + + let echeck = + let ty_r = match nd.n_output with + | [out] -> out.v_type + | _ -> Tprod (List.map (fun vd -> vd.v_type) nd.n_output) in + let mk_call nn = + mk_exp ~ty:ty_r + (Eapp ({ a_op = Enode nn; a_params = []; a_unsafe = false; }, + [], None)) in + mk_exp ~ty:(Tid Initial.pbool) + (Eapp ({ a_op = Eequal; a_params = []; a_unsafe = false; }, + [mk_call nd.n_name; mk_call nd'.n_name], None)) in + + let nd_check = + mk_node + ~output:[mk_var_dec output (Tid Initial.pbool)] + ~eq:[mk_equation (Evarpat output) echeck] + { nd.n_name with name = prefix ^ "_check_" ^ nd.n_name.name; } in + + let sign = Modules.find_value nd.n_name in + Modules.add_value nd'.n_name sign; + Modules.add_value nd_check.n_name + { node_inputs = []; + node_outputs = [{ a_name = None; a_type = Tid Initial.pbool; }]; + node_statefull = true; + node_params = []; + node_params_constraints = [] }; + + Compiler_options.add_assert nd_check.n_name; + nd :: nd' :: nd_check :: nd_list + +let add_checks pass prefix nnl p = + let add nd nd_list = + if List.mem nd.n_name nnl + then add_check pass prefix nd nd_list + else nd :: nd_list in + { p with p_nodes = List.fold_right add p.p_nodes []; } diff --git a/compiler/minils/transformations/elimtuples.ml b/compiler/minils/transformations/elimtuples.ml new file mode 100644 index 0000000..20dc371 --- /dev/null +++ b/compiler/minils/transformations/elimtuples.ml @@ -0,0 +1,66 @@ +(**************************************************************************) +(* *) +(* Heptagon *) +(* *) +(* Author : Marc Pouzet *) +(* Organization : Demons, LRI, University of Paris-Sud, Orsay *) +(* *) +(**************************************************************************) + +(* This module removes tuple-patterns when possible. + + (x, y) = if b then (1, 2) else (3, 4); + -> + x = if b then 1 else 3; + y = if b then 2 else 4; + + However, if f() is a function/node returning multiple values, the following + equation stay the same: + + (x, y) = if b then (1, 2) else f(arg); +*) + +open Misc +open Names +open Idents +open Signature +open Minils +open Mls_utils +open Mls_printer +open Types +open Clocks +open Pp_tools + +(* raised when a multi-valued call is found *) +exception Call + +(* never leaves the scope of a precise pattern, i.e. [e_list] never changes type + during subsequent recursive calls. *) +let rec control e_list = + let exp e e_list = match e.e_desc with + | Eapp ({ a_op = Efun _ | Enode _; }, _, _) -> raise Call + | Eapp ({ a_op = Etuple; }, arg_list, _) -> arg_list @ e_list + | Econst { se_desc = Stuple arg_list; } -> + List.map (fun se -> mk_exp ~ty:se.se_ty (Econst se)) arg_list + | Eapp ({ a_op = Eifthenelse; } as op, [c; t; e], rst) -> + let t_children = control [t] + and e_children = control [e] in + let add_condition t e = + mk_exp ~ty:t.e_ty (Eapp (op, [c; t; e], rst)) in + List.map2 add_condition t_children e_children + | _ -> e :: e_list in + List.fold_right exp e_list [] + +let rec eq equ eq_list = match equ.eq_lhs with + | Evarpat _ -> equ :: eq_list + | Etuplepat pat_list -> + try + let new_eqs = List.map2 mk_equation pat_list (control [equ.eq_rhs]) in + List.fold_right eq new_eqs eq_list + with Call -> equ :: eq_list + +let node nd = + let eq_list = List.fold_right eq nd.n_equs [] in + { nd with n_equs = eq_list; } + +let program p = { p with p_nodes = List.map node p.p_nodes; } diff --git a/compiler/minils/transformations/introvars.ml b/compiler/minils/transformations/introvars.ml new file mode 100644 index 0000000..2239c91 --- /dev/null +++ b/compiler/minils/transformations/introvars.ml @@ -0,0 +1,105 @@ +(**************************************************************************) +(* *) +(* Heptagon *) +(* *) +(* Author : Marc Pouzet *) +(* Organization : Demons, LRI, University of Paris-Sud, Orsay *) +(* *) +(**************************************************************************) + +open Misc +open Names +open Idents +open Signature +open Minils +open Mls_utils +open Mls_printer +open Types +open Clocks +open Pp_tools + +let debug_tomato = false + +let debug_do f = if debug_tomato then f () else () + +let rec exp e (eq_list, var_list) = match e.e_desc with + | Evar _ | Econst _ -> (e, eq_list, var_list) + | _ -> + let (e_desc, eq_list, var_list) = match e.e_desc with + | Evar _ | Econst _ -> assert false (* handled above *) + | Efby (seo, e) -> + let (e, eq_list, var_list) = intro_var e (eq_list, var_list) in + Efby (seo, e), eq_list, var_list + | Eapp (app, e_list, vi) -> + let (e_list, eq_list, var_list) = + intro_vars e_list (eq_list, var_list) in + Eapp (app, e_list, vi), eq_list, var_list + | Ewhen (e, cn, vi) -> + let (e, eq_list, var_list) = intro_var e (eq_list, var_list) in + Ewhen (e, cn, vi), eq_list, var_list + | Emerge (vi, cnel) -> + let e_list = List.map snd cnel in + let e_list, eq_list, var_list = + intro_vars e_list (eq_list, var_list) in + let cnel = List.combine (List.map fst cnel) e_list in + Emerge (vi, cnel), eq_list, var_list + | Estruct fnel -> + let e_list = List.map snd fnel in + let e_list, eq_list, var_list = + intro_vars e_list (eq_list, var_list) in + let fnel = List.combine (List.map fst fnel) e_list in + Estruct fnel, eq_list, var_list + | Eiterator (it, app, se, e_list, vio) -> + let (e_list, eq_list, var_list) = + intro_vars e_list (eq_list, var_list) in + Eiterator (it, app, se, e_list, vio), eq_list, var_list in + ({ e with e_desc = e_desc; }, eq_list, var_list) + +and intro_vars e_list (eq_list, var_list) = + let acc e (e_list, eq_list, var_list) = + let (e, eq_list, var_list) = intro_var e (eq_list, var_list) in + (e :: e_list, eq_list, var_list) in + List.fold_right acc e_list ([], eq_list, var_list) + +and intro_var e (eq_list, var_list) = + let (e, eq_list, var_list) = exp e (eq_list, var_list) in + match e.e_desc with + | Evar _ -> (e, eq_list, var_list) + | _ -> + let id = Idents.fresh "t" in + let new_eq = mk_equation (Evarpat id) e + and var_dc = mk_var_dec id e.e_ty in + (mk_exp ~ty:e.e_ty (Evar id), new_eq :: eq_list, var_dc :: var_list) + +let rec intro_vars_pat pat e (eq_list, var_list) = match pat, e.e_desc with + | _, Eapp ({ a_op = Efun _ | Enode _; }, _, _) -> + let (e, eq_list, var_list) = exp e (eq_list, var_list) in + (mk_equation pat e :: eq_list, var_list) + | Etuplepat pat, Econst { se_desc = Stuple se_list; se_ty = Tprod ty_list } -> + let e_list = + let mk se ty = mk_exp ~ty:ty (Econst se) in + List.map2 mk se_list ty_list in + List.fold_right2 intro_vars_pat pat e_list (eq_list, var_list) + | Etuplepat pat_list, Eapp ({ a_op = Etuple; }, e_list, _) -> + List.fold_right2 intro_vars_pat pat_list e_list (eq_list, var_list) + | pat, _ -> + let (e, eq_list, var_list) = exp e (eq_list, var_list) in + (mk_equation pat e :: eq_list, var_list) + +and mk_var_decs pat ty var_list = match pat, ty with + | Evarpat ident, _ -> mk_var_dec ident ty :: var_list + | Etuplepat pat_list, Tprod ty_list -> + List.fold_right2 mk_var_decs pat_list ty_list var_list + | _ -> assert false (* ill-typed *) + +let eq eq (eq_list, var_list) = + intro_vars_pat eq.eq_lhs eq.eq_rhs (eq_list, var_list) + +let node nd = + let nd = Elimtuples.node nd in + debug_do (fun _ -> + Format.printf "Detuplized node:@\n%a@." print_node nd); + let (eq_list, var_list) = List.fold_right eq nd.n_equs ([], nd.n_local) in + { nd with n_equs = eq_list; n_local = var_list; } + +let program p = { p with p_nodes = List.map node p.p_nodes; } diff --git a/compiler/minils/transformations/singletonvars.ml b/compiler/minils/transformations/singletonvars.ml new file mode 100644 index 0000000..7e21ef3 --- /dev/null +++ b/compiler/minils/transformations/singletonvars.ml @@ -0,0 +1,167 @@ +(**************************************************************************) +(* *) +(* Heptagon *) +(* *) +(* Author : Marc Pouzet *) +(* Organization : Demons, LRI, University of Paris-Sud, Orsay *) +(* *) +(**************************************************************************) + +open Misc +open Names +open Idents +open Signature +open Minils +open Mls_utils +open Mls_printer +open Types +open Clocks +open Pp_tools + +module UseCounts = +struct + type use = + | Clock + | Reset + | Var of int + + let find_uses ident use_counts = + try Env.find ident use_counts + with Not_found -> Var 0 + + let add_var_use ident use_counts = + let use = match find_uses ident use_counts with + | Var x -> Var (x + 1) + | use -> use in + Env.add ident use use_counts + + let add_clock_use ident use_counts = Env.add ident Clock use_counts + + let add_reset_use ident use_counts = Env.add ident Reset use_counts + + let factorable ident e use_count = + let uses = find_uses ident use_count in + match uses with + | Clock | Reset -> false + | Var i -> i < 2 || (match e.e_desc with Econst _ -> true | _ -> false) + + let edesc funs use_counts edesc = + let (edesc, use_counts) = Mls_mapfold.edesc funs use_counts edesc in + let use_counts = match edesc with + | Evar vi -> add_var_use vi use_counts + | Emerge (vi, _) -> add_clock_use vi use_counts + | Ewhen (_, _, vi) -> add_clock_use vi use_counts + | Eapp (_, _, Some vi) | Eiterator (_, _, _, _, Some vi) -> + add_reset_use vi use_counts + | _ -> use_counts in + (edesc, use_counts) + + let node nd = + let funs = { Mls_mapfold.defaults with Mls_mapfold.edesc = edesc; } in + snd (Mls_mapfold.node_dec funs Env.empty nd) +end + +module InlineSingletons = +struct + let exp funs subst exp = + let (exp, subst) = Mls_mapfold.exp funs subst exp in + match exp.e_desc with + | Evar vi -> (try Env.find vi subst with Not_found -> exp), subst + | _ -> (exp, subst) + + let inline_node subst nd = + let funs = { Mls_mapfold.defaults with Mls_mapfold.exp = exp; } in + fst (Mls_mapfold.node_dec funs subst nd) + + let inline_exp subst e = + let funs = { Mls_mapfold.defaults with + Mls_mapfold.exp = exp; } in + fst (Mls_mapfold.exp_it funs subst e) +end + +let debug_subst subst = + Env.iter + (fun id e -> Format.printf "%a -> @[%a@]@." print_ident id print_exp e) + subst + +let rec close_subst subst = + let close_binding id e subst = + let e = InlineSingletons.inline_exp subst e in + let s = Env.add id e Env.empty in + let inline id e subst = + Env.add id (InlineSingletons.inline_exp s e) subst in + Env.fold inline subst Env.empty in + Env.fold close_binding subst subst + +let node nd = + (* Removes unused var_decs from a node *) + let filter_var_decs nd = + let add eq iset = List.fold_right IdentSet.add (Vars.def [] eq) iset in + let iset = List.fold_right add nd.n_equs IdentSet.empty in + let add_if_useful vd local = + if IdentSet.mem vd.v_ident iset then vd :: local else local in + { nd with n_local = List.fold_right add_if_useful nd.n_local [] } in + + let use_counts = UseCounts.node nd in + + let add_reset rst e = e in + + let is_output id = List.exists (fun vd -> vd.v_ident = id) nd.n_output in + + let (eq_list, subst) = + let add_to_subst eq (eq_list, subst) = + match (eq.eq_lhs, eq.eq_rhs.e_desc) with + | Etuplepat _, Eapp ({ a_op = (Efun _ | Enode _); }, _, _) -> + (eq :: eq_list, subst) (* cannot factor out multi-ret fun calls *) + | _ -> + let id_list = Vars.def [] eq in + let e_list, rst, unsafe = match eq.eq_rhs.e_desc with + | Eapp ({ a_op = Etuple; a_unsafe = unsafe; }, e_list, rst) -> + e_list, rst, unsafe + | _ -> [eq.eq_rhs], None, false in + + (* Walk over variables/exps couples of eq, gathering equations to + be inlined. + POSTCOND: id_list and e_list only contains non-singleton vars, + subst is enriched with singleton vars encountered. *) + let (id_list, e_list, subst) = + let add_if_needed id e (id_list, e_list, subst) = + if UseCounts.factorable id e use_counts && not (is_output id) + then (id_list, e_list, Env.add id e subst) (* to be expanded *) + else (id :: id_list, e :: e_list, subst) in + List.fold_right2 add_if_needed id_list e_list ([], [], subst) in + + assert (List.length id_list = List.length e_list); + + match id_list, e_list with + | [], [] -> (eq_list, subst) + | [id], [e] -> + (mk_equation (Evarpat id) (add_reset rst e) :: eq_list, subst) + | _ -> + let pat = + Etuplepat (List.map (fun id -> Evarpat id) id_list) in + + let eq = + mk_equation pat + { eq.eq_rhs with e_desc = + Eapp ({ a_op = Etuple; + a_params = []; + a_unsafe = unsafe; }, e_list, rst); } in + (eq :: eq_list, subst) in + List.fold_right add_to_subst nd.n_equs ([], Env.empty) in + + let nd = { nd with n_equs = eq_list; } in + + (* Format.printf "Node:@\n%a@\n" print_node nd; *) + + let subst = close_subst subst in + + (* debug_subst subst; *) + + let nd = InlineSingletons.inline_node subst nd in + + (* Format.printf "Node:@\n%a@\n" print_node nd; *) + + let nd = filter_var_decs nd in + + nd diff --git a/compiler/minils/transformations/tomato.ml b/compiler/minils/transformations/tomato.ml new file mode 100644 index 0000000..fc456c4 --- /dev/null +++ b/compiler/minils/transformations/tomato.ml @@ -0,0 +1,509 @@ +(**************************************************************************) +(* *) +(* Heptagon *) +(* *) +(* Author : Marc Pouzet *) +(* Organization : Demons, LRI, University of Paris-Sud, Orsay *) +(* *) +(**************************************************************************) + +open Misc +open Names +open Idents +open Signature +open Minils +open Mls_utils +open Mls_printer +open Types +open Clocks +open Pp_tools +open Mls_compare + +let debug_do = Introvars.debug_do + +module IntMap = Map.Make(struct + type t = int + let compare = Pervasives.compare + end) + +let ident_of_int = + let ht = Hashtbl.create 300 in + fun (name : string) (i : int) -> + try Hashtbl.find ht i + with Not_found -> + let new_ident = Idents.fresh name in + Hashtbl.add ht i new_ident; + new_ident + +type cl_id = + | Input of ident + | Var of int + | Pattern of pat * int list + +let cl_id_compare id1 id2 = match id1, id2 with + | Input id1, Input id2 -> ident_compare id1 id2 + | Var i1, Var i2 -> compare i1 i2 + | Pattern (p1, i1), Pattern (p2, i2) -> + let cr = pat_compare p1 p2 in + if cr <> 0 then cr else Pervasives.compare i1 i2 + | (Input _ | Var _), _ -> -1 + | Pattern _, _ -> 1 + +module PatEnv = + struct + module P = Map.Make(struct + type t = pat + let compare = pat_compare + end) + + type penv_t = (int * exp * ident list) P.t + + type t = penv_t * (pat * int list) Env.t + + let empty = (P.empty, Env.empty) + + let find ident (penv, _) = P.find ident penv + + let fold f (penv, _) acc = P.fold f penv acc + + let find_class_id (penv, env) ident = + try let (cl_id, _, _) = P.find (Evarpat ident) penv in Var cl_id + with Not_found -> + (try let pat, i = Env.find ident env in Pattern (pat, i) + with Not_found -> Input ident) + + let find_id ident (penv, env) = + try P.find (Evarpat ident) penv + with Not_found -> + let rec consume (pat, i_list) = match pat, i_list with + | Evarpat ident, [] -> Evarpat ident + | Etuplepat pat_list, x :: i_list -> + consume (List.nth pat_list x, i_list) + | Etuplepat _, [] | Evarpat _, _ :: _ -> assert false in + P.find (consume (Env.find ident env)) penv + + let print fmt (penv, env) = + let print_binding pat (cl_num, head, children) = + Format.fprintf fmt + " @[%a => class %d, head = @[%a@], children = @[%a@]@]@\n" + print_pat pat + cl_num + print_exp head + (print_list_l print_ident "" "," "") children + + and print_pat_link ident (pat, i) = + Format.fprintf fmt "@[%a => %a, %a@]@\n" + print_ident ident + print_pat pat + (print_list_r (fun fmt i -> Format.fprintf fmt "%d" i) "" "," "") i in + P.iter print_binding penv; + Env.iter print_pat_link env + + let add ident info (penv, env) = (P.add ident info penv, env) + + let add_pat_link (penv, env) pat = + let rec add path pat env = match pat with + | Evarpat ident -> Env.add ident path env + | Etuplepat pat_list -> + let rec call pat (i, env) = (i + 1, add (i :: path) pat env) in + snd (List.fold_right call pat_list (0, env)) in + (penv, add [] pat env) + end + +module SubstNode = +struct + let apply_subst subst ident = + try match PatEnv.find_id ident subst with + | Evarpat ident -> ident + | pat -> + debug_do (fun _ -> + Format.printf "apply_subst (...) %a => %a@." + print_ident ident + print_pat pat); + assert false + with Not_found -> ident + + let rec apply_subst_clock subst ck = match ck with + | Cbase -> Cbase + | Con (ck, cstr, x) -> + Con (apply_subst_clock subst ck, cstr, apply_subst subst x) + | Cvar { contents = Clink ck; } -> apply_subst_clock subst ck + | Cvar { contents = Cindex _; } -> ck + + + let exp funs subst e = + let (e, subst) = Mls_mapfold.exp funs subst e in + ({ e with e_ck = apply_subst_clock subst e.e_ck; }, subst) + + let var_dec _ subst vd = + ({ vd with v_ident = apply_subst subst vd.v_ident; }, subst) + + let subst_node subst nd = + let funs = { Mls_mapfold.defaults with + Mls_mapfold.exp = exp; + Mls_mapfold.var_dec = var_dec; } in + fst (Mls_mapfold.node_dec funs subst nd) +end + +let empty_var = Idents.fresh "EMPTY" +let dummy_exp = mk_exp (Evar empty_var) + +let exp_of_ident vi = mk_exp (Evar vi) +and ident_of_exp { e_desc = e_d; } = match e_d with + | Evar vi -> vi + | _ -> invalid_arg "ident_of_exp" + +let behead e = + (* We have to add rst as a sub-expression for finer equivalence classes + computation for Eapps and Eiterators: + + x = f() every m; + y = f() every n; + + should be equivalent iff m and n are. Thus, when beheading e, we have to + somehow record whether it held a reset field or not. We choose to do + so by adding an [empty_var] as a reset. In our example, x and y + become: + + x = {f() every $empty_var}, m + y = {f() every $empty_var}, n + *) + + let encode_reset rst = match rst with + | None -> (None, []) + | Some x -> (Some empty_var, [exp_of_ident x]) in + + let (e_desc, children) = match e.e_desc with + | Econst _ -> (e.e_desc, []) + | Evar _ -> (e.e_desc, []) + | Efby (c, e) -> (Efby (c, dummy_exp), [e]) + | Eapp (op, e_list, rst) -> + let (rst, l) = encode_reset rst in + (* the pretty-printer dies when handling certain kinds of apps with + an empty argument list. *) + (Eapp (op, repeat_list dummy_exp (List.length e_list), rst), l @ e_list) + | Ewhen (e, cstr, x) -> + (Ewhen (dummy_exp, cstr, empty_var), [exp_of_ident x; e]) + | Emerge (x, lne_list) -> + let (lne_list, e_list) = + List.split + (List.map (fun (ln, e) -> ((ln, dummy_exp), e)) lne_list) in + (Emerge (empty_var, lne_list), exp_of_ident x :: e_list) + | Estruct lne_list -> + let (lne_list, e_list) = + List.split + (List.map (fun (ln, e) -> ((ln, dummy_exp), e)) lne_list) in + (Estruct lne_list, e_list) + | Eiterator (it, op, s, e_list, rst) -> + let (rst, l) = encode_reset rst in + (Eiterator (it, op, s, [], rst), l @ e_list) in + ({ e with e_desc = e_desc; }, children) + +let pat_name pat = + let rec acc fmt pat = match pat with + | Evarpat ident -> print_ident fmt ident + | Etuplepat pat_list -> print_list acc "" "x" "" fmt pat_list in + ignore (Format.flush_str_formatter ()); + acc Format.str_formatter pat; + Format.flush_str_formatter () + +module ClassMap = Map.Make( + struct + (* class id 0 will be for inputs, which are implicitly never in the + same class *) + type t = (Minils.exp * cl_id list) + let compare (e1, id1_list) (e2, id2_list) = + let e_c = exp_compare e1 e2 in + if e_c <> 0 then e_c else list_compare cl_id_compare id1_list id2_list + end +) + +let bindings_of_env env = + let compare (_, (_, e1, _)) (_, (_, e2, _)) = exp_compare e1 e2 in + + let add pat info l = (pat, info) :: l in + List.sort compare (PatEnv.fold add env []) + +let normalize_classes env = + let l = bindings_of_env env in (* key property: l is sorted by exp *) + let _, _, l = + let add (pat, (cl_num, e, children)) (subst, i, l) = + try (subst, i, (pat, (IntMap.find cl_num subst, e, children)) :: l) + with Not_found -> + let vi = Var i in + (IntMap.add cl_num vi subst, i + 1, (pat, (vi, e, children)) :: l) in + List.fold_right add l (IntMap.empty, 1, []) in + let add (key, info) env = PatEnv.P.add key info env in + List.fold_right add l PatEnv.P.empty + +let equivalent env1 env2 = (normalize_classes env1) = (normalize_classes env2) + +let compute_initial_env env eq = + let penv = match eq.eq_lhs with + | Etuplepat _ -> + let rec add pat i_list penv = match pat with + | Evarpat id -> Env.add id (eq.eq_lhs, i_list) penv + | Etuplepat pat_list -> + fold_righti (fun i pat -> add pat (i :: i_list)) pat_list penv in + add eq.eq_lhs [] (snd env) + | Evarpat _ -> snd env in + + let (e, children) = behead eq.eq_rhs in + let (e, children) = match e.e_desc, children with + | Evar _, [] -> (dummy_exp, [e]) + | _ -> (e, children) in + let children = + let add e = match e.e_desc with + | Evar id -> id + | _ -> + Format.printf "Unexpected: @[%a@]@." print_exp e; + assert false in + List.map add children in + + let env = fst (PatEnv.add eq.eq_lhs (1, e, children) env) in + (env, penv) + +let rec compute_classes (env : PatEnv.t) = + (* Perform potential optimization, e.g. replace + x = merge ... (true -> y) (false -> y); + by + x = y; + *) + let transform ((head, child_id_list) as cl_key) = match head.e_desc with + | Emerge _ -> + (* skip ident in front of the list *) + let child_id_list = List.tl child_id_list in + let first_elem = List.hd child_id_list in + let all_the_same = + List.filter (fun x -> x <> first_elem) child_id_list = [] in + if all_the_same then (dummy_exp, [first_elem]) else cl_key + | Eapp ({ a_op = Eifthenelse; }, _, None) -> + (match child_id_list with + | [_; t; e] -> if t = e then (dummy_exp, [t]) else cl_key + | _ -> assert false) + | _ -> cl_key in + + let clmap = + let add_to_classmap pat ((_, head, children) as info) clmap = + let cl_key = (head, List.map (PatEnv.find_class_id env) children) in + let cl_key = transform cl_key in (* apply potential optimization *) + let cl = try ClassMap.find cl_key clmap with Not_found -> [] in + ClassMap.add cl_key ((pat, info) :: cl) clmap in + PatEnv.fold add_to_classmap env ClassMap.empty in + + let (_, penv') = + let add_class_to_env _ ninfo_list (i, env) = + let add_ninfo_to_env env (pat, (_, head, children)) = + PatEnv.P.add pat (i, head, children) env in + (i + 1, List.fold_left add_ninfo_to_env env ninfo_list) in + ClassMap.fold add_class_to_env clmap (1, PatEnv.P.empty) in + + let (env' : PatEnv.t) = (penv', snd env) in + + debug_do (fun _ -> + Format.printf "New environment:@\n%a@\n" PatEnv.print env'); + + if equivalent env env' then env' else compute_classes env' + +let factor_classes (env : PatEnv.t) = + let (subst, classes) = + let add_to_env ident (cl_id, _, _) (subst, classes) = + (* New identifier for [pat] : either the concatenation of the + equivalence class patterns with a unique number appended OR *) + let new_ident = (* TODO: O(n2) *) + let gather pat (cl_id', _, _) pat_list = + if cl_id = cl_id' then pat :: pat_list else pat_list in + match PatEnv.fold gather env [] with + | [pat] -> pat + | pat_list -> + let concat pat prefix = (pat_name pat) ^ "_" ^ prefix in + let prefix = List.fold_right concat pat_list "" in + let prefix = String.sub prefix 0 (String.length prefix - 1) in + Evarpat (ident_of_int prefix cl_id) in + (PatEnv.P.add ident new_ident subst, + IntMap.add cl_id ident classes) in + PatEnv.fold add_to_env env (PatEnv.P.empty, IntMap.empty) in + + let create_var_for_class _ pat (penv' : PatEnv.penv_t) = + let (cl_id, head, children) = PatEnv.find pat env in + let children = (* remap children to new idents according to subst *) + let remap ident = + (* Inputs won't be present in env *) + try match PatEnv.P.find (Evarpat ident) subst with + | Evarpat ident -> ident + | Etuplepat _ -> assert false + with Not_found -> ident in + List.map remap children in + PatEnv.P.add (PatEnv.P.find pat subst) (cl_id, head, children) penv' in + + ((IntMap.fold create_var_for_class classes PatEnv.P.empty, snd env), subst) + +let rec reconstruct input_type (env : PatEnv.t) = + let find_head ident = + try let (_, head, _) = PatEnv.find (Evarpat ident) env in head + with Not_found -> + (try + debug_do (fun _ -> + Format.printf "find_head %a@." print_ident ident; + Env.iter + (fun id (p, _) -> + Format.printf "%a => %a@." print_ident id print_pat p) + (snd env)); + + let (pat, _) = Env.find ident (snd env) in + debug_do (fun _ -> + Format.printf "find_head %a => %a@." + print_ident ident + print_pat pat); + let (_, head, _) = PatEnv.find pat env in head + with Not_found -> mk_exp ~ty:(input_type ident) (Evar ident)) in + + let rec mk_var_decs pat ty var_list = match pat, ty with + | Evarpat ident, _ -> mk_var_dec ident ty :: var_list + | Etuplepat pat_list, Tprod ty_list -> + List.fold_right2 mk_var_decs pat_list ty_list var_list + | Etuplepat _, (Tarray _ | Tid _) -> assert false (* ill-typed *) in + + let add_to_lists pat (_, head, children) (eq_list, var_list) = + (* Remember the encoding of resets given above. *) + let rst_of_e_list rst e_list = match rst, e_list with + | None, _ -> (None, e_list) + | Some empty, x :: e_list when empty == empty_var -> + (Some (ident_of_exp x), e_list) + | _ -> assert false in + + let make_exp child = { (find_head child) with e_desc = Evar child; }; in + let e_desc = match head.e_desc, List.map make_exp children with + | Econst _, [] -> head.e_desc + | Evar _, [e] -> e.e_desc (* ILL-TYPED *) + | Efby (seo, _), [e] -> Efby (seo, e) + | Eapp (app, _, rst), e_list -> + let rst, e_list = rst_of_e_list rst e_list in Eapp (app, e_list, rst) + | Ewhen (_, cn, _), [x; e] -> Ewhen (e, cn, ident_of_exp x) + | Emerge (_, cnel), e_list -> + Emerge (ident_of_exp (List.hd e_list), + List.combine (List.map fst cnel) (List.tl e_list)) + | Estruct fnel, e_list -> + Estruct (List.combine (List.map fst fnel) e_list) + | Eiterator (it, app, se, [], rst), e_list -> + let rst, e_list = rst_of_e_list rst e_list in + Eiterator (it, app, se, e_list, rst) + + | (Eiterator (_, _, _, _ :: _, _) | Ewhen _ | Efby _ | Evar _ | Econst _) + , _ -> assert false (* invariant *) in + (mk_equation pat { head with e_desc = e_desc; } :: eq_list, + mk_var_decs pat head.e_ty var_list) in + PatEnv.fold add_to_lists env ([], []) + +(* We may have fused together distinct outputs during minimization, e.g. + + node f(x : int) returns (o, o2 : int) + let + o = 4 + x; + o2 = 4 + x; + tel + + becomes + + node f(x : int) returns (o_o2_42, o_o2_42 : int) + let + o_o2_42 = 4 + x; + tel + + which is ill-formed. The following function reintroduces needed copies for + duplicated outputs. In our example, f() will become: + + node f(x : int) returns (o_o2_42, o_o2_42_43 : int) + let + o_o2_42 = 4 + x; + o_o2_42_43 = o_o2_42; + tel + *) +let introduce_copies_for_outputs nd = + let var_dec vd (iset, vd_list, eq_list) = + if IdentSet.mem vd.v_ident iset + then (* introduce copy, change vd *) + let fresh = Idents.fresh (Idents.name vd.v_ident) in + let new_eq = + let e = mk_exp ~ty:vd.v_type (Evar vd.v_ident) in + mk_equation (Evarpat fresh) e in + (iset, { vd with v_ident = fresh; } :: vd_list, new_eq :: eq_list) + else + (IdentSet.add vd.v_ident iset, vd :: vd_list, eq_list) in + let (_, vd_list, eq_list) = + List.fold_right var_dec nd.n_output (IdentSet.empty, [], []) in + { nd with n_output = vd_list; n_equs = eq_list @ nd.n_equs; } + +let node nd = + debug_do (fun _ -> Format.printf "Original node:@\n%a@\n" print_node nd); + + let nd = Introvars.node nd in + + let orig_eq_count = List.length nd.n_equs in + + debug_do (fun _ -> + Format.printf "Node with vars introduced:@\n%a@\n" print_node nd); + + let env = List.fold_left compute_initial_env PatEnv.empty nd.n_equs in + + debug_do (fun _ -> + Format.printf "Initial environment:@\n%a@\n" PatEnv.print env); + + let env = compute_classes env in + + debug_do (fun _ -> + Format.printf "Env with classes:@\n%a@\n" PatEnv.print env); + + let ((env : PatEnv.t), subst) = factor_classes env in + + debug_do (fun _ -> + Format.printf "Env with factored classes:@\n%a@\n" + PatEnv.print env); + + let eq_list, var_list = + let input_type id = + try + (List.find (fun vd -> vd.v_ident = id) nd.n_input).v_type + with Not_found -> + Format.printf "Could not find %a@." print_ident id; + assert false in + reconstruct input_type env in + let var_list = + let is_not_output vd = + not (List.exists + (fun out -> ident_compare vd.v_ident out.v_ident = 0) + nd.n_output) in + List.filter is_not_output var_list in + + let nd = { nd with n_equs = eq_list; n_local = var_list; } in + let nd = SubstNode.subst_node (subst, snd env) nd in + + debug_do (fun _ -> + Format.printf "TOMATOed node:@\n%a@\n" print_node nd); + + if !Compiler_options.verbose then + Format.printf + "TOMATO: factored out %d expressions.@." + (orig_eq_count - List.length nd.n_equs); + + let nd = Singletonvars.node nd in + + debug_do (fun _ -> + Format.printf "Factored node:@\n%a@\n" print_node nd); + + let nd = introduce_copies_for_outputs nd in + + debug_do (fun _ -> + Format.printf "Final node:@\n%a@\n" print_node nd); + + nd + +let node nd = + let to_be_tomatoized s = s = nd.n_name in + if List.exists to_be_tomatoized !Compiler_options.tomato_nodes + || !Compiler_options.tomato then node nd else nd + +let program p = { p with p_nodes = List.map node p.p_nodes; } + +let tomato_checks p = + Checkpass.add_checks "tomato" node !Compiler_options.tomato_check p diff --git a/compiler/utilities/global/compiler_options.ml b/compiler/utilities/global/compiler_options.ml index 281a116..276f20a 100644 --- a/compiler/utilities/global/compiler_options.ml +++ b/compiler/utilities/global/compiler_options.ml @@ -82,6 +82,15 @@ let add_inlined_node s = inline := s :: !inline let flatten = ref false +let tomato = ref false + +let tomato_nodes : qualname list ref = ref [] + +let add_tomato_node s = tomato_nodes := s :: !tomato_nodes + +let tomato_check : qualname list ref = ref [] + +let add_tomato_check s = tomato_check := s :: !tomato_check let do_iterator_fusion = ref false @@ -106,3 +115,4 @@ and doc_noinit = "\t\tDisable initialization analysis" and doc_assert = "\t\tInsert run-time assertions for boolean node " and doc_inline = "\t\tInline node " and doc_itfusion = "\t\tEnable iterator fusion." +and doc_tomato = "\t\tEnable automata minimization."