diff --git a/compiler/global/idents.mli b/compiler/global/idents.mli index 7130fd7..ee0ac0f 100644 --- a/compiler/global/idents.mli +++ b/compiler/global/idents.mli @@ -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. *) diff --git a/compiler/minils/mls_compare.ml b/compiler/minils/mls_compare.ml index 04fd632..dd8e55b 100644 --- a/compiler/minils/mls_compare.ml +++ b/compiler/minils/mls_compare.ml @@ -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 diff --git a/compiler/minils/transformations/introvars.ml b/compiler/minils/transformations/introvars.ml deleted file mode 100644 index e06f815..0000000 --- a/compiler/minils/transformations/introvars.ml +++ /dev/null @@ -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; } diff --git a/compiler/minils/transformations/singletonvars.ml b/compiler/minils/transformations/singletonvars.ml deleted file mode 100644 index 474a5dc..0000000 --- a/compiler/minils/transformations/singletonvars.ml +++ /dev/null @@ -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 diff --git a/compiler/minils/transformations/tomato.ml b/compiler/minils/transformations/tomato.ml index 2f9d489..90b177d 100644 --- a/compiler/minils/transformations/tomato.ml +++ b/compiler/minils/transformations/tomato.ml @@ -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 - " @[%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 = +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 []; } diff --git a/compiler/utilities/misc.ml b/compiler/utilities/misc.ml index 8b5c977..935ce2a 100644 --- a/compiler/utilities/misc.ml +++ b/compiler/utilities/misc.ml @@ -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 | [] -> [] diff --git a/compiler/utilities/misc.mli b/compiler/utilities/misc.mli index 7fdfc64..e5c8836 100644 --- a/compiler/utilities/misc.mli +++ b/compiler/utilities/misc.mli @@ -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