Automata minimization.
This commit is contained in:
Adrien Guatto
parent
a4c3d9e856
commit
4044d8a0a2
|
|
@ -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;
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
||||
|
|
|
|||
|
|
@ -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. *)
|
||||
|
||||
|
|
|
|||
|
|
@ -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))
|
||||
|
|
|
|||
66
compiler/minils/transformations/checkpass.ml
Normal file
66
compiler/minils/transformations/checkpass.ml
Normal file
|
|
@ -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 []; }
|
||||
66
compiler/minils/transformations/elimtuples.ml
Normal file
66
compiler/minils/transformations/elimtuples.ml
Normal file
|
|
@ -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; }
|
||||
105
compiler/minils/transformations/introvars.ml
Normal file
105
compiler/minils/transformations/introvars.ml
Normal file
|
|
@ -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; }
|
||||
167
compiler/minils/transformations/singletonvars.ml
Normal file
167
compiler/minils/transformations/singletonvars.ml
Normal file
|
|
@ -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
|
||||
509
compiler/minils/transformations/tomato.ml
Normal file
509
compiler/minils/transformations/tomato.ml
Normal file
|
|
@ -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
|
||||
" @[<v 2>%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 "@[<v 2>%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
|
||||
|
|
@ -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 = "<node>\t\tInsert run-time assertions for boolean node <node>"
|
||||
and doc_inline = "<node>\t\tInline node <node>"
|
||||
and doc_itfusion = "\t\tEnable iterator fusion."
|
||||
and doc_tomato = "\t\tEnable automata minimization."
|
||||
|
|
|
|||
Loading…
Reference in a new issue