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

All-new and fresh tomato!

Browse source 
Not working ATM:
  * tuples
  * when
This commit is contained in:
Adrien Guatto 2011-06-30 17:41:25 +02:00
parent 0518ecafe6
commit 891174d73c
7 changed files with 303 additions and 788 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
compiler/global/idents.mli
View file

@ -3,7 +3,7 @@ open Names
(** This modules manages unique identifiers,
/!\ To be effective, [enter_node] has to be called when entering a node
[gen_fresh] generates an identifier
[gen_var] generates a variable identifier
[name] returns a unique name (inside its node) from an identifier. *)
(** The (abstract) type of identifiers*)
@ -36,7 +36,7 @@ val ident_of_name : ?reset:bool -> string -> ident
val is_reset : ident -> bool
(** /!\ This function should be called every time we enter a node *)
(** /!\ [enter_node qualname] should be called every time we enter a node with name [qualname]. *)
val enter_node : Names.qualname -> unit
(** Maps taking an identifier as a key. *)

10
compiler/minils/mls_compare.ml
View file

@ -44,7 +44,7 @@ let rec exp_compare e1 e2 =
let cr = type_compare e1.e_ty e2.e_ty in
if cr <> 0 then cr
else
let cr = clock_compare e1.e_ck e2.e_ck in
let cr = clock_compare e1.e_base_ck e2.e_base_ck in
if cr <> 0 then cr
else
match e1.e_desc, e2.e_desc with
@ -58,6 +58,11 @@ let rec exp_compare e1 e2 =
if cr <> 0 then cr
else let cr = list_compare extvalue_compare el1 el2 in
if cr <> 0 then cr else option_compare ident_compare vio1 vio2
| Ewhen (e1, cn1, id1), Ewhen (e2, cn2, id2) ->
let cr = compare cn1 cn2 in
if cr <> 0 then cr
else let cr = ident_compare id1 id2 in
if cr <> 0 then cr else exp_compare e1 e2
| Emerge (vi1, cnel1), Emerge (vi2, cnel2) ->
let compare_cne (cn1, e1) (cn2, e2) =
let cr = compare cn1 cn2 in
@ -90,6 +95,9 @@ let rec exp_compare e1 e2 =
| Eapp _, (Eextvalue _ | Efby _) -> -1
| Eapp _, _ -> 1
| Ewhen _, (Eextvalue _ | Efby _ | Eapp _) -> -1
| Ewhen _, _ -> 1
| Emerge _, (Estruct _ | Eiterator _) -> 1
| Emerge _, _ -> -1

131
compiler/minils/transformations/introvars.ml
View file

@ -1,131 +0,0 @@
(**************************************************************************)
(* *)
(* Heptagon *)
(* *)
(* Author : Marc Pouzet *)
(* Organization : Demons, LRI, University of Paris-Sud, Orsay *)
(* *)
(**************************************************************************)
(* This module recursively introduces intermediate variables for each equation
of a node. The resulting node's equations bodies are no deeper than 1 level
in terms of expression depth.
x = 1 + (2 + 3);
->
x = _1 + _2;
_1 = 1;
_2 = _3 + _4;
_3 = 2;
_4 = 3;
Note that the identifiers of the introduced should begin with a specific
prefix that is not usable by user variables; this information is used by the
automata minimization pass to distinguish variables introduced here from
original ones.
*)
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 prefix = "_t"
let was_generated s =
let ivars_re = Str.regexp_string prefix in
try Str.search_forward ivars_re s 0 = 0
with Not_found -> 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, pe_list, e_list, vio) ->
let (e_list, eq_list, var_list) =
intro_vars e_list (eq_list, var_list) in
let (pe_list, eq_list, var_list) =
intro_vars pe_list (eq_list, var_list) in
Eiterator (it, app, se, pe_list, 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.gen_var "introvars" prefix 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 (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
View file

@ -1,167 +0,0 @@
(**************************************************************************)
(* *)
(* 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
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 Eextvalue { w_desc = Wconst _ } -> 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
| Eextvalue { w_desc = Wvar vi } -> add_var_use vi use_counts
| Emerge (vi, _) -> add_clock_use vi use_counts
| Eextvalue { w_desc = Wwhen (_, _, 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_it 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
| Eextvalue { w_desc = Wvar 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_it 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
(* do not inline tuple patterns *)
| Etuplepat _, _ -> (eq :: eq_list, subst)
| _ ->
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 (mk_app ~unsafe:unsafe Etuple, 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

767
compiler/minils/transformations/tomato.ml
View file

@ -20,545 +20,340 @@ open Clocks
open Pp_tools
open Mls_compare
(** TODO: remove all references to Introvars *)
(* Data-flow minimization on MiniLS:
let debug_do = Introvars.debug_do
1. Put each equation into a big map. It maps variable names to triples (class_id * truncated
expression * class_id list). Initially, each local variable is in the same class.
module IntMap = Map.Make(struct
type t = int
let compare = Pervasives.compare
end)
2. Compute the new class_id of each equation: two equations are in the same class if they are
equal and have the same child equations.
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.gen_var "tomato" name in
Hashtbl.add ht i new_ident;
new_ident
3. If anything has changed: go to 2
type cl_id =
| Input of ident
| Var of int
| Pattern of pat * int list
4. Reconstruct: one equation for one equivalence class.
*)
let print_cl_id fmt cl_id = match cl_id with
| Input ident -> Format.fprintf fmt "in %a" print_ident ident
| Var i -> Format.fprintf fmt "%d" i
| Pattern (pat, il) ->
Format.fprintf fmt "%a: %a"
print_pat pat
(print_list_r (fun fmt d -> Format.fprintf fmt "%d" d) "" "," "") il
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
(* An environment used for automata minimization: holds both a pattern environment mapping patterns to equivalence
classes, and a [(pat * int list) Env.t] that maps variable [x] to a [(pat, pth)] tuple where [pat] is the pattern
holding [x] at path [pth] *)
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 =
module OrderedInts =
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_it funs subst nd)
type t = int
let compare = Pervasives.compare
end
let empty_var = Idents.gen_var "tomato" "EMPTY"
let dummy_exp = mk_exp Types.Tinvalid (Evar empty_var)
module IntSet = Set.Make(OrderedInts)
module IntMap = Map.Make(OrderedInts)
let exp_of_ident ~ty vi = mk_exp ~ty:ty (Evar vi)
and ident_of_exp { e_desc = e_d; } = match e_d with
| Evar vi -> vi
| _ -> invalid_arg "ident_of_exp"
module TomEnv =
struct
let behead e =
(* We have to add rst as a sub-expression for finer equivalence classes
computation for Eapps and Eiterators:
module PatMap = Map.Make(struct
type t = pat
let compare = pat_compare
end)
x = f() every m;
y = f() every n;
type class_ref =
| Cr_plain of ident
| Cr_input of extvalue (* we record the full expression for convenience *)
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:
type eq_repr =
{
mutable er_class : int;
er_pattern : pat;
er_head : exp;
er_children : class_ref list;
}
x = {f() every $empty_var}, m
y = {f() every $empty_var}, n
*)
type tom_env = eq_repr PatMap.t
let encode_reset rst = match rst with
| None -> (None, [])
| Some x -> (Some empty_var, [exp_of_ident ~ty:(Tid Initial.pbool) x]) in
open Mls_printer
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 ~ty:(Modules.find_constrs cstr) 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
let ty = lne_list |> List.hd |> fun (c,_) -> c |> Modules.find_constrs in
(Emerge (empty_var, lne_list), exp_of_ident ~ty:ty 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, pe_list, e_list, rst) ->
let (rst, l) = encode_reset rst in
(* count is the number of partial arguments *)
let count = mk_exp ~ty:Initial.tint
(Econst (Initial.mk_static_int (List.length pe_list))) in
(Eiterator (it, op, s, [], [], rst), count :: (pe_list @ l @ e_list)) in
({ e with e_desc = e_desc; }, children)
let print_class_ref fmt cr = match cr with
| Cr_plain id -> print_ident fmt id
| Cr_input w -> print_extvalue fmt w
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 ()
let debug_tenv fmt tenv =
let debug pat repr =
Format.fprintf fmt "%a => @[class %d,@ pattern %a,@ head { %a },@ children %a@]@."
print_pat pat
repr.er_class
print_pat repr.er_pattern
print_exp repr.er_head
(print_list_r print_class_ref "[" ";" "]") repr.er_children
in
PatMap.iter debug tenv
end
module ClassMap = Map.Make(
open TomEnv
let gen_var = Idents.gen_var ~reset:false "tomato"
let dummy_extvalue = mk_extvalue ~ty:Initial.tint (Wvar (gen_var "dummy"))
let initial_class = 0
let concat_idents id1 id2 = gen_var (Idents.name id1 ^ "_" ^ Idents.name id2)
let symbol_for_int i =
if i > 25
then "a" ^ string_of_int i
else String.make 1 (Char.chr (Char.code 'a' + i))
(*******************************************************************)
(* Construct an initial minimization environment *)
(*******************************************************************)
let rec add_equation is_input (tenv : tom_env) eq =
let add_clause (cn, w) class_id_list =
let class_id_list, w = extvalue is_input w class_id_list in
class_id_list, (cn, w) in
let ed, class_id_list = match eq.eq_rhs.e_desc with
| Eextvalue w ->
let class_id_list, w = extvalue is_input w [] in
Eextvalue w, class_id_list
| Eapp (app, w_list, rst) ->
let class_id_list, w_list = mapfold_right (extvalue is_input) w_list [] in
Eapp (app, w_list, rst), class_id_list
| Efby (seo, w) ->
let class_id_list, w = extvalue is_input w [] in
Efby (seo, w), class_id_list
| Ewhen _ -> assert false (* TODO *)
| Emerge (vi, clause_list) ->
let class_id_list, clause_list = mapfold_right add_clause clause_list [] in
Emerge (vi, clause_list), class_id_list
| Eiterator (it, app, se, partial_w_list, w_list, rst) ->
let class_id_list, partial_w_list = mapfold_right (extvalue is_input) partial_w_list [] in
let class_id_list, w_list = mapfold_right (extvalue is_input) w_list class_id_list in
Eiterator (it, app, se, partial_w_list, w_list, rst), class_id_list
| Estruct field_val_list ->
let class_id_list, field_val_list = mapfold_right add_clause field_val_list [] in
Estruct field_val_list, class_id_list
in
let eq_repr =
{
er_class = initial_class;
er_pattern = eq.eq_lhs;
er_head = { eq.eq_rhs with e_desc = ed; };
er_children = class_id_list;
}
in
PatMap.add eq.eq_lhs eq_repr tenv
and extvalue is_input w class_id_list = match w.w_desc with
| Wvar v ->
(if is_input v then Cr_input w else Cr_plain v)
:: class_id_list, dummy_extvalue
| _ -> class_id_list, w
(***********************************************************************)
(* Compute the next equivalence classes for a minimization environment *)
(***********************************************************************)
module EqClasses = 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
)
type t = exp * int option list
let bindings_of_env env =
let compare (_, (_, e1, _)) (_, (_, e2, _)) = exp_compare e1 e2 in
let unsafe { e_desc = ed; _ } = match ed with
| Eapp (app, _, _) | Eiterator (_, app, _, _, _, _) -> app.a_unsafe
| _ -> false
let add pat info l = (pat, info) :: l in
List.sort compare (PatEnv.fold add env [])
let compare (e1, cr_list1) (e2, cr_list2) =
let cr = Mls_compare.exp_compare e1 e2 in
if cr <> 0 then cr
else
if unsafe e1 then 1
else
(if unsafe e2 then -1 else list_compare Pervasives.compare cr_list1 cr_list2)
end)
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 compute_new_class tenv =
let fresh_id, get_id = let id = ref 0 in ((fun () -> incr id; !id), (fun () -> !id)) in
let equivalent env1 env2 = (normalize_classes env1) = (normalize_classes env2)
let add_eq_repr _ eqr classes =
let map_class_ref cref = match cref with
| Cr_input _ -> None
| Cr_plain v ->
let er = PatMap.find (Evarpat v) tenv in
Some er.er_class in
let children = List.map map_class_ref eqr.er_children in
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 key = (eqr.er_head, children) in
let id = try EqClasses.find key classes with Not_found -> fresh_id () in
eqr.er_class <- id;
EqClasses.add (eqr.er_head, children) id classes
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
in
let env = fst (PatEnv.add eq.eq_lhs (1, e, children) env) in
(env, penv)
let classes = PatMap.fold add_eq_repr tenv EqClasses.empty in
(* Idea: we put the classes in a big map, grouped by class_id = description x
children ids. *)
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
(get_id (), tenv)
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 rec separate_classes tenv =
let rec fix (id, tenv) =
Format.eprintf "New tenv %d:\n%a@." id debug_tenv tenv;
let new_id, tenv = compute_new_class tenv in
if new_id = id then tenv else fix (new_id, tenv)
in
fix (compute_new_class tenv)
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
(*******************************************************************)
(* Regroup classes from a minimization environment *)
(*******************************************************************)
let (env' : PatEnv.t) = (penv', snd env) in
let rec compute_classes tenv =
let rec add_eq_repr _ repr cenv =
let repr_list = try IntMap.find repr.er_class cenv with Not_found -> [] in
IntMap.add repr.er_class (repr :: repr_list) cenv in
PatMap.fold add_eq_repr tenv IntMap.empty
debug_do (fun _ ->
Format.printf "New environment:@\n%a@\n" PatEnv.print env');
(********************************************************************)
(* Reconstruct a list of equation from a set of equivalence classes *)
(********************************************************************)
if equivalent env env' then env' else compute_classes env'
let rec reconstruct (((tenv : tom_env), cenv) as env) =
let reconstruct_class id eq_repr_list eq_list =
assert (List.length eq_repr_list > 0);
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_pattern = (* TODO: O(n2) *)
let gather pat (cl_id', _, _) pat_list =
if cl_id = cl_id' then pat :: pat_list else pat_list in
let repr = List.hd eq_repr_list in
let rec filter_pattern pat acc = match pat with
| Evarpat id ->
if Introvars.was_generated (Idents.name id)
then acc else pat :: acc
| Etuplepat pat_list ->
(match filter_patterns pat_list with
| [] -> acc
| pat_list -> Etuplepat pat_list :: acc)
let e =
let ed = reconstruct_exp_desc (tenv, cenv) repr.er_head.e_desc repr.er_children in
let ck = reconstruct_clock env repr.er_head.e_base_ck in
let level_ck =
reconstruct_clock env repr.er_head.e_level_ck in (* not strictly needed, done for
consistency reasons *)
let ct = reconstruct_clock_type env repr.er_head.e_ct in
{ repr.er_head with e_desc = ed; e_base_ck = ck; e_level_ck = level_ck; e_ct = ct; } in
and filter_patterns pat_list =
List.fold_right filter_pattern pat_list [] in
let pat = pattern_name_for_id env repr.er_head.e_ty id in
match filter_patterns (PatEnv.fold gather env []) with
| [] -> Evarpat (ident_of_int "tom" cl_id)
| [pat] -> pat
| pat_list ->
let concat pat prefix =
let pn = pat_name pat in
if Introvars.was_generated pn
then prefix
else pn ^ "_" ^ prefix in
let prefix = List.fold_right concat pat_list "" in
let prefix = (* chops trailing _ if needed *)
if prefix = ""
then "tom"
else String.sub prefix 0 (String.length prefix - 1) in
Evarpat (ident_of_int prefix cl_id) in
(PatEnv.P.add ident new_pattern subst,
IntMap.add cl_id ident classes) in
PatEnv.fold add_to_env env (PatEnv.P.empty, IntMap.empty) in
mk_equation pat e :: eq_list in
IntMap.fold reconstruct_class cenv []
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' ->
Format.printf "Remapping %a to %a@."
print_ident ident
print_ident 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
and reconstruct_exp_desc ((tenv : tom_env), (cenv : eq_repr list IntMap.t) as env) headd children =
let reconstruct_clauses clause_list =
let (qn_list, w_list) = List.split clause_list in
let w_list = reconstruct_extvalues env w_list children in
List.combine qn_list w_list in
((IntMap.fold create_var_for_class classes PatEnv.P.empty, snd env), subst)
match headd with
| Eextvalue w ->
let w = assert_1 (reconstruct_extvalues env [w] children) in
Eextvalue w
| Efby (ini, w) ->
let w = assert_1 (reconstruct_extvalues env [w] children) in
Efby (ini, w)
| Eapp (app, w_list, rst) ->
Eapp (app, reconstruct_extvalues env w_list children, optional (new_ident_for env) rst)
| Ewhen _ -> assert false (* TODO *)
| Emerge (ck_x, clause_list) ->
Emerge (new_ident_for env ck_x, reconstruct_clauses clause_list)
| Estruct field_val_list ->
let field_val_list = reconstruct_clauses field_val_list in
Estruct field_val_list
| Eiterator (it, app, se, partial_w_list, w_list, rst) ->
let total_w_list = reconstruct_extvalues env (partial_w_list @ w_list) children in
let partial_w_list, w_list = split_at (List.length partial_w_list) total_w_list in
Eiterator (it, app, se, partial_w_list, w_list, optional (new_ident_for env) rst)
let rec reconstruct input_type (env : PatEnv.t) =
let find_head ident =
try let (_, head, _) = PatEnv.find (Evarpat ident) env in head
and reconstruct_extvalues (tenv, cenv) w_list children =
let consume w (children, result_w_list) =
if extvalue_compare w dummy_extvalue = 0
then (List.tl children, reconstruct_class_ref (tenv, cenv) (List.hd children) :: result_w_list)
else (children, w :: result_w_list) in
let (children, w_list) = List.fold_right consume w_list (children, []) in
assert (children = []); (* There should be no more children than dummy_exps! *)
w_list
and reconstruct_class_ref (tenv, cenv) cr = match cr with
| Cr_input w -> w
| Cr_plain w ->
let er = PatMap.find (Evarpat w) tenv in
mk_extvalue ~ty:er.er_head.e_ty (Wvar (ident_for_class cenv er.er_class))
and reconstruct_clock env ck = match ck_repr ck with
| Con (ck, c, x) -> Con (reconstruct_clock env ck, c, new_ident_for env x)
| _ -> ck
and reconstruct_clock_type env ct = match ct with
| Cprod ct_list -> Cprod (List.map (reconstruct_clock_type env) ct_list)
| Ck ck -> Ck (reconstruct_clock env ck)
and new_ident_for ((tenv : tom_env), (cenv : eq_repr list IntMap.t)) x =
let class_id = (PatMap.find (Evarpat x) tenv).er_class in
ident_for_class cenv class_id
and ident_for_class =
let ht = Hashtbl.create 100 in
fun (cenv : eq_repr list IntMap.t) class_id ->
try Hashtbl.find ht class_id
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 id =
let repr_list = IntMap.find class_id cenv
and make_ident { er_pattern = pat; } =
Misc.fold_right_1 concat_idents (ident_list_of_pat pat) in
Misc.fold_right_1 concat_idents (List.map make_ident repr_list) in
Hashtbl.add ht class_id id;
id
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
and pattern_name_for_id ((tenv, cenv) as env) ty id = pattern_name env ty (ident_for_class cenv id)
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 [], Tunit -> var_list
| Etuplepat _, (Tarray _ | Tid _ | Tunit | Tmutable _) -> assert false (* ill-typed *) in
and pattern_name env ty name = match ty with
| Tprod ty_list ->
let component_name i ty =
pattern_name env ty (concat_idents (gen_var (symbol_for_int i)) name) in
Etuplepat (mapi component_name ty_list)
| _ -> Evarpat name
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
(********************************************************************)
(* Top-level functions: plug everything together to minimize a node *)
(********************************************************************)
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 ->
(* the first element is the number of partial arguments *)
let count, e_list = assert_1min e_list in
let c = (match count.e_desc with
| Econst { se_desc = Sint c } -> c
| _ -> assert false)
in
let pe_list, e_list = Misc.split_at c e_list in
let rst, e_list = rst_of_e_list rst e_list in
Eiterator (it, app, se, pe_list, e_list, rst)
let rec fix_local_var_dec ((tenv, cenv) as env) vd (seen, vd_list) =
let class_id = (PatMap.find (Evarpat vd.v_ident) tenv).er_class in
if IntSet.mem class_id seen then (seen, vd_list)
else
(IntSet.add class_id seen,
{ vd with
v_ident = new_ident_for env vd.v_ident;
v_clock = reconstruct_clock env vd.v_clock; } :: vd_list)
| (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 ([], [])
and fix_local_var_decs tenv vd_list =
snd (List.fold_right (fix_local_var_dec tenv) vd_list (IntSet.empty, []))
(* We may have fused together distinct outputs during minimization, e.g.
let rec fix_output_var_dec ((tenv, cenv) as env) vd vd_list =
let class_id = (PatMap.find (Evarpat vd.v_ident) tenv).er_class in
{ vd with
v_ident = new_ident_for env vd.v_ident;
v_clock = reconstruct_clock env vd.v_clock; } :: vd_list
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.gen_var "tomato" (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; }
and fix_output_var_decs tenv vd_list = List.fold_right (fix_output_var_dec tenv) vd_list []
let node nd =
debug_do (fun _ -> Format.printf "Original node:@\n%a@\n" print_node nd);
Idents.enter_node nd.n_name;
let nd = Introvars.node nd in
(* Initial environment *)
let tenv =
let is_input id = List.exists (fun vd -> ident_compare vd.v_ident id = 0) nd.n_input in
List.fold_left (add_equation is_input) PatMap.empty nd.n_equs in
let orig_eq_count = List.length nd.n_equs in
(* Compute fix-point of [compute_new_class] *)
let tenv = separate_classes tenv in
debug_do (fun _ ->
Format.printf "Node with vars introduced:@\n%a@\n" print_node nd);
(* Regroup equivalence classes *)
let cenv = compute_classes tenv in
let env = List.fold_left compute_initial_env PatEnv.empty nd.n_equs in
(* Reconstruct equation list from grouped equivalence classes *)
let eq_list = reconstruct (tenv, cenv) in
debug_do (fun _ ->
Format.printf "Initial environment:@\n%a@\n" PatEnv.print env);
let local = fix_local_var_decs (tenv, cenv) nd.n_local in
let output = fix_output_var_decs (tenv, cenv) nd.n_output in
let env = compute_classes env in
{ nd with n_equs = eq_list; n_output = output; n_local = local; }
debug_do (fun _ ->
Format.printf "Env with classes:@\n%a@\n" PatEnv.print env);
let program_desc pd pd_list = match pd with
| Pnode nd -> Pnode (node nd) :: pd_list
| _ -> pd :: pd_list
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 input type for %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
*)
let program p = { p with p_desc = List.fold_right program_desc p.p_desc []; }

5
compiler/utilities/misc.ml
View file

@ -163,6 +163,11 @@ let mapfold_right f l acc =
List.fold_right (fun e (acc, l) -> let acc, e = f e acc in (acc, e :: l))
l (acc, [])
let rec fold_right_1 f l = match l with
| [] -> invalid_arg "fold_right_1: empty list"
| [x] -> x
| x :: l -> f x (fold_right_1 f l)
let mapi f l =
let rec aux i = function
| [] -> []

7
compiler/utilities/misc.mli
View file

@ -46,7 +46,7 @@ val split_last : 'a list -> ('a list * 'a)
val split_nlast : int -> 'a list -> ('a list * 'a list)
exception List_too_short
(** [split_at n l] splits [l] in two after the [n]th value.
(** [split_at n l] splits [l] in two after the [n]th value (starting at 0).
Raises List_too_short exception if the list is too short. *)
val split_at : int -> 'a list -> 'a list * 'a list
@ -78,6 +78,11 @@ val mapfold: ('acc -> 'b -> 'c * 'acc) -> 'acc -> 'b list -> 'c list * 'acc
val mapfold_right
: ('a -> 'acc -> 'acc * 'b) -> 'a list -> 'acc -> 'acc * 'b list
(** [fold_right_1 f [x1; x2; ...; xn]] = f x1 (f x2 (f ... xn)). The list should
have at least one element! *)
val fold_right_1 :
('a -> 'a -> 'a) -> 'a list -> 'a
(** Mapi *)
val mapi: (int -> 'a -> 'b) -> 'a list -> 'b list
val mapi2: (int -> 'a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list