diff --git a/src/compiler/rewrite/aform.ml b/src/compiler/rewrite/aform.ml new file mode 100644 index 00000000..0b699485 --- /dev/null +++ b/src/compiler/rewrite/aform.ml @@ -0,0 +1,268 @@ +(***********************************************************************) +(* *) +(* *) +(* Zelus, a synchronous language for hybrid systems *) +(* *) +(* (c) 2024 Inria Paris (see the AUTHORS file) *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed under *) +(* the terms of the INRIA Non-Commercial License Agreement (see the *) +(* LICENSE file). *) +(* *) +(* *********************************************************************) + +(* A-normal form: distribution of tuples *) +(* for any variable [x: t1 *...* t2n, introduce fresh names *) +(* [x1:t1,...,xn:tn] so that [x = (x1,...,xn)] *) +(* distribute pattern matchings [(p1,...,pn) = (e1,...,en)] into *) +(* p1 = e1 and ... pn = en] *) +open Ident +open Zelus +open Deftypes + +(* the type of the accumulator *) +type acc = + { renaming: Ident.t Env.t; (* renaming environment *) + env: (Typinfo.pattern * Typinfo.exp) Env.t; + } + +(* Build a renaming from an environment *) +let build global_funs ({ renaming } as acc) env = + let buildrec n entry (env, renaming) = + let m = Ident.fresh (Ident.source n) in + Env.add m entry env, + Env.add n m renaming in + let env, renaming = Env.fold buildrec env (Env.empty, renaming) in + env, { acc with renaming } + +(* associate a pattern and an expression to a variable according to its type *) +(* [intro t_env subst = subst', t_env'] *) +let build global_funs ({ renaming; env } as acc) env = + (* returns a pair [spat, se] with [spat] a pattern, [se] an expression *) + let result { source } entry acc ty = + let id = Ident.fresh source in + (Aux.varpat id, Aux.var id), + Env.add id { entry with t_tys = Deftypes.scheme ty } acc in + let rec value id entry acc ({ t_desc } as ty) = + match t_desc with + | Tvar | Tarrow _ | Tvec _ | Tconstr _ -> result id entry acc ty + | Tproduct(ty_list) -> + let p_e_list, acc = Util.mapfold (value id entry) acc ty_list in + let p_list, e_list = List.split p_e_list in + (Aux.tuplepat p_list, Aux.tuple e_list), acc + | Tlink(ty_link) -> value id entry acc ty_link in + let add id ({ t_tys = { typ_body }; t_sort; t_path } as entry) + (subst_acc, env_acc) = + match t_sort with + | Sort_val | Sort_var -> + let r, env_acc = value id entry env_acc typ_body in + Env.add id r subst_acc, env_acc + | _ -> + (* state variables are not splitted but renamed *) + let r, env_acc = result id entry env_acc typ_body in + Env.add id r subst_acc, env_acc in + let buildrec n entry (env, renaming) = + let m = Ident.fresh (Ident.source n) in + Env.add m entry env, + Env.add n m renaming in + let env, renaming = Env.fold buildrec env (Env.empty, renaming) in + env, { acc with renaming }Env.fold add t_env (subst, Env.empty) + +(* matching. Translate [(p1,...,pn) = (e1,...,en)] into the set of *) +(* equations [p1 = e1 and ... and pn = en] *) +(* [compose] defines the type of equation: [init p = e] or [p = e] *) +let rec matching compose eq_list ({ pat_desc } as p) ({ e_desc } as e) = + match pat_desc, e_desc with + | Etuplepat(p_list), Etuple(e_list) -> + matching_list compose eq_list p_list e_list + | _ -> (compose p e) :: eq_list + +and matching_list compose eq_list p_list e_list = + List.fold_left2 (matching compose) eq_list p_list e_list + +(* Functions which traverse the ast *) +(** expressions *) +let rec expression subst ({ e_desc = desc } as e) = + match desc with + | Econst _ | Econstr0 _ | Eglobal _ -> e + | Elast(x) -> { e with e_desc = Elast(name_of_name x subst) } + | Elocal(x) -> + let ename = exp_of_name x subst in + { e with e_desc = ename.e_desc } + | Etuple(e_list) -> + { e with e_desc = Etuple(List.map (expression subst) e_list) } + | Econstr1(c, e_list) -> + { e with e_desc = Econstr1(c, List.map (expression subst) e_list) } + | Erecord(n_e_list) -> + { e with e_desc = + Erecord(List.map (fun (ln, e) -> + (ln, expression subst e)) n_e_list) } + | Erecord_access(e_record, ln) -> + { e with e_desc = Erecord_access(expression subst e_record, ln) } + | Erecord_with(e_record, n_e_list) -> + { e with e_desc = + Erecord_with(expression subst e_record, + List.map (fun (ln, e) -> + (ln, expression subst e)) n_e_list) } + | Eop(op, e_list) -> + { e with e_desc = Eop(op, List.map (expression subst) e_list) } + | Eapp(app, e_op, e_list) -> + let e_op = expression subst e_op in + let e_list = List.map (expression subst) e_list in + { e with e_desc = Eapp(app, e_op, e_list) } + | Etypeconstraint(e1, ty) -> + { e with e_desc = Etypeconstraint(expression subst e1, ty) } + | Eseq(e1, e2) -> + { e with e_desc = Eseq(expression subst e1, expression subst e2) } + | Elet(l, e_let) -> + let subst, l = local subst l in + { e with e_desc = Elet(l, expression subst e_let) } + | Eperiod _ | Epresent _ | Ematch _ | Eblock _ -> assert false + +(** Local declarations *) +and local subst ({ l_eq = eq_list; l_env = l_env } as l) = + let subst, l_env = build l_env subst in + let eq_list = equation_list subst eq_list in + subst, { l with l_eq = eq_list; l_env = l_env } + +and pattern subst p = + match p.p_desc with + | Ewildpat | Econstpat _ | Econstr0pat _ -> p + | Etuplepat(p_list) -> + { p with p_desc = Etuplepat(List.map (pattern subst) p_list) } + | Econstr1pat(c, p_list) -> + { p with p_desc = Econstr1pat(c, List.map (pattern subst) p_list) } + | Evarpat(x) -> + let pname = pat_of_name x subst in + { p with p_desc = pname.p_desc } + | Ealiaspat(p1, n) -> + { p with p_desc = Ealiaspat(pattern subst p1, name_of_name n subst) } + | Eorpat(p1, p2) -> + { p with p_desc = Eorpat(pattern subst p1, pattern subst p2) } + | Erecordpat(l_p_list) -> + let l_p_list = + List.map (fun (l, p) -> (l, pattern subst p)) l_p_list in + { p with p_desc = Erecordpat(l_p_list) } + | Etypeconstraintpat(p1, ty) -> + { p with p_desc = Etypeconstraintpat(pattern subst p1, ty) } + +and equation subst eq_list ({ eq_desc = desc } as eq) = + let returns eq eq_desc eq_list = + { eq with eq_desc = eq_desc; eq_write = Deftypes.empty } :: eq_list in + match desc with + | EQeq(p, e) -> + let p = pattern subst p in + let e = expression subst e in + matching (fun p e -> Zaux.eqmake (EQeq(p, e))) eq_list p e + | EQder(x, e, e_opt, []) -> + returns eq (EQder(name_of_name x subst, expression subst e, + Zmisc.optional_map (expression subst) e_opt, [])) eq_list + | EQinit(x, e) -> + (* [x] should not be renamed as it is a state variable *) + returns eq (EQinit(name_of_name x subst, + expression subst e)) eq_list + | EQnext(x, e, e_opt) -> + (* [x] should not be renamed as it is a state variable *) + returns eq (EQnext(name_of_name x subst, expression subst e, + Zmisc.optional_map (expression subst) e_opt)) eq_list + | EQpluseq(x, e) -> + (* [x] should not be renamed as it is a multi-write variable *) + returns eq (EQpluseq(name_of_name x subst, + expression subst e)) eq_list + | EQreset(reset_eq_list, e) -> + returns eq (EQreset(equation_list subst reset_eq_list, + expression subst e)) eq_list + | EQmatch(total, e, m_h_list) -> + returns eq (EQmatch(total, expression subst e, + List.map (handler subst) m_h_list)) eq_list + | EQblock(b) -> + returns eq (EQblock(block subst b)) eq_list + | EQand(and_eq_list) -> + returns eq (EQand(equation_list subst and_eq_list)) eq_list + | EQbefore(before_eq_list) -> + returns eq (EQbefore(equation_list subst before_eq_list)) eq_list + | EQforall ({ for_index = i_list; for_init = init_list; + for_body = b_eq_list; + for_in_env = fi_env; for_out_env = fo_env } as b) -> + let subst, fi_env = build fi_env subst in + let subst, fo_env = build fo_env subst in + let index ({ desc = desc } as ind) = + let desc = match desc with + | Einput(i, e) -> Einput(name_of_name i subst, expression subst e) + | Eoutput(oi, o) -> + Eoutput(name_of_name oi subst, name_of_name o subst) + | Eindex(i, e1, e2) -> + Eindex(name_of_name i subst, + expression subst e1, expression subst e2) in + { ind with desc = desc } in + let init ({ desc = desc } as ini) = + let desc = match desc with + | Einit_last(i, e) -> + Einit_last(name_of_name i subst, expression subst e) in + { ini with desc = desc } in + let i_list = List.map index i_list in + let init_list = List.map init init_list in + let b_eq_list = block subst b_eq_list in + returns eq + (EQforall + { b with for_index = i_list; for_init = init_list; + for_body = b_eq_list; for_in_env = fi_env; + for_out_env = fo_env }) eq_list + | EQautomaton _ | EQpresent _ | EQder _ | EQemit _ -> assert false + +and equation_list subst eq_list = + let eq_list = List.fold_left (equation subst) [] eq_list in List.rev eq_list + +and handler subst ({ m_pat = p; m_body = b; m_env = m_env } as m_h) = + let subst, m_env = build m_env subst in + let p = pattern subst p in + { m_h with m_pat = p; m_body = block subst b; m_env = m_env } + + +and block subst ({ b_vars = v_list; b_body = eq_list; b_env = b_env } as b) = + (* the field [b.b_locals] must be [] as this compilation step is done *) + (* after normalisation *) + let vardec_list subst v_list = + (* Warning. if [n] is a state variable or associated with a *) + (* default value of combine function, it is not split into a tuple *) + (* but a single name. The code below makes this assumption. *) + let vardec acc ({ vardec_name = n} as v) = + let p = pat_of_name n subst in + let nset = Vars.fv_pat S.empty S.empty p in + S.fold (fun n acc -> { v with vardec_name = n } :: acc) nset acc in + List.fold_left vardec [] v_list in + + let subst, b_env = build b_env subst in + let v_list = vardec_list subst v_list in + { b with b_vars = v_list; b_body = equation_list subst eq_list; + b_env = b_env; b_write = Deftypes.empty } + +let implementation impl = + match impl.desc with + | Eopen _ | Etypedecl _ -> impl + | Econstdecl(n, is_static, e) -> + { impl with desc = Econstdecl(n, is_static, expression Env.empty e) } + | Efundecl(n, ({ f_body = e; f_env = f_env; f_args = p_list } as body)) -> + let subst, f_env = build f_env Env.empty in + let p_list = List.map (pattern subst) p_list in + let e = expression subst e in + { impl with desc = + Efundecl(n, { body with f_body = e; + f_env = f_env; f_args = p_list }) } + +let implementation_list impl_list = Zmisc.iter implementation impl_list + +let set_index funs acc n = + let _ = Ident.set n in n, acc +let get_index funs acc n = Ident.get (), acc + +let program genv p = + let global_funs = { Mapfold.default_global_funs with build; var_ident } in + let funs = + { Mapfold.defaults with + expression; global_funs; set_index; get_index; implementation; + open_t } in + let p, _ = Mapfold.program_it funs { empty with genv } p in + p + diff --git a/src/compiler/rewrite/copy.ml b/src/compiler/rewrite/copy.ml new file mode 100644 index 00000000..461c0774 --- /dev/null +++ b/src/compiler/rewrite/copy.ml @@ -0,0 +1,201 @@ +(***********************************************************************) +(* *) +(* *) +(* Zelus, a synchronous language for hybrid systems *) +(* *) +(* (c) 2020 Inria Paris (see the AUTHORS file) *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed under *) +(* the terms of the INRIA Non-Commercial License Agreement (see the *) +(* LICENSE file). *) +(* *) +(* *********************************************************************) + +(* Elimination of atomic values copy variables [x = y], constants, globals *) +(* The transformation is applied after static scheduling and before *) +(* translation into sequential code *) + +open Zmisc +open Zident +open Zelus +open Deftypes + +(** atomic expressions - either immediate constants or variables *) +type value = | Vlocal of Zident.t | Vlast of Zident.t | Vconst of Zelus.desc + +type renaming = + { rel: value Env.t; (* the substitution *) + defs: S.t; (* names after which the substitution cannot be applied *) + } + +let empty = { rel = Env.empty; defs = S.empty } + +(** Append a renaming with a new relation *) +let append new_rel ({ rel = rel } as renaming) = + { renaming with rel = Env.append new_rel rel } + +(** Apply the renaming recursively. If [rel = [n\n1, n1\n2]], then *) +(** [rename n rel] = n2 *) +(** A substitution [n\last m] is not performed when [m] belongs to [defs] *) +let rename n { rel = rel; defs = defs } = + let rec rename n = + try + let m = Env.find n rel in + begin + match m with + | Vlocal m -> rename m + | Vlast m -> if S.mem m defs then raise Not_found else Elast m + | Vconst(edesc) -> edesc + end + with Not_found -> Elocal n in + rename n + +let rec size ({ rel = rel } as renaming) ({ desc = desc } as s) = + try + let s = + match desc with + | Sconst _ | Sglobal _ -> s + | Sname(n) -> + let n = Env.find n rel in + begin match n with + | Vlocal n -> { s with desc = Sname(n) } + | _ -> raise Not_found + end + | Sop(op, s1, s2) -> + { s with desc = Sop(op, size renaming s1, size renaming s2) } in + s + with + Not_found -> s + +let operator renaming op = + match op with + | Efby | Eunarypre | Eifthenelse + | Eminusgreater | Eup | Einitial | Edisc + | Ehorizon | Etest | Eaccess | Eupdate | Econcat | Eatomic -> op + | Eslice(s1, s2) -> Eslice(size renaming s1, size renaming s2) + +(** Build a substitution [x1\v1,...,xn\vn]. *) +let rec build rel { eq_desc = desc } = + match desc with + | EQeq({ p_desc = Evarpat(x) }, { e_desc = desc }) -> + let rel = + match desc with + | Elocal m -> Env.add x (Vlocal(m)) rel + | Eglobal _ | Econst _ -> Env.add x (Vconst(desc)) rel + | Elast m -> Env.add x (Vlast(m)) rel + | _ -> rel in + rel + | EQreset(eq_list, _) + | EQand(eq_list) + | EQbefore(eq_list) -> List.fold_left build rel eq_list + | EQeq _ | EQpluseq _ | EQnext _ | EQinit _ | EQmatch _ + | EQder(_, _, None, []) + | EQforall _ | EQblock _ -> rel + | EQautomaton _ | EQpresent _ | EQemit _ | EQder _ -> assert false + +(** Expressions. Apply [renaming] to every sub-expression *) +let rec expression renaming ({ e_desc = desc } as e) = + match desc with + | Econst _ | Econstr0 _ | Eglobal _ | Elast _ -> e + | Elocal(x) -> { e with e_desc = rename x renaming } + | Etuple(e_list) -> + { e with e_desc = Etuple(List.map (expression renaming) e_list) } + | Econstr1(c, e_list) -> + { e with e_desc = Econstr1(c, List.map (expression renaming) e_list) } + | Erecord(n_e_list) -> + { e with e_desc = + Erecord(List.map (fun (ln, e) -> + (ln, expression renaming e)) n_e_list) } + | Erecord_access(e_record, ln) -> + { e with e_desc = Erecord_access(expression renaming e_record, ln) } + | Erecord_with(e_record, n_e_list) -> + { e with e_desc = + Erecord_with(expression renaming e_record, + List.map (fun (ln, e) -> + (ln, expression renaming e)) n_e_list) } + | Eop(op, e_list) -> + { e with e_desc = Eop(operator renaming op, + List.map (expression renaming) e_list) } + | Eapp(app, e_op, e_list) -> + let e_op = expression renaming e_op in + let e_list = List.map (expression renaming) e_list in + { e with e_desc = Eapp(app, e_op, e_list) } + | Etypeconstraint(e1, ty) -> + { e with e_desc = Etypeconstraint(expression renaming e1, ty) } + | Eseq(e1, e2) -> + { e with e_desc = Eseq(expression renaming e1, expression renaming e2) } + | Elet(l, e_let) -> + let renaming, l = local renaming l in + { e with e_desc = Elet(l, expression renaming e_let) } + | Eperiod _ | Epresent _ | Ematch _ | Eblock _ -> assert false + +(** Local declarations *) +and local renaming ({ l_eq = eq_list } as l) = + let rel = List.fold_left build Env.empty eq_list in + let renaming = append rel renaming in + let renaming, eq_list = equation_list renaming eq_list in + renaming, { l with l_eq = eq_list } + +(** renaming of equations *) +and equation ({ defs = defs } as renaming, eq_list) + ({ eq_desc = desc; eq_write = w } as eq) = + let desc = match desc with + | EQeq(p, e) -> EQeq(p, expression renaming e) + | EQpluseq(x, e) -> EQpluseq(x, expression renaming e) + | EQinit(x, e0) -> EQinit(x, expression renaming e0) + | EQmatch(total, e, m_b_list) -> + let rename ({ m_body = b } as m_h) = + { m_h with m_body = block renaming b } in + EQmatch(total, expression renaming e, List.map rename m_b_list) + | EQder(x, e, None, []) -> + EQder(x, expression renaming e, None, []) + | EQreset(res_eq_list, e) -> + let e = expression renaming e in + let _, eq_list = equation_list renaming res_eq_list in + EQreset(eq_list, e) + | EQforall ({ for_index = i_list; for_init = init_list; + for_body = b_eq_list } as b) -> + let index ({ desc = desc } as ind) = + let desc = match desc with + | Einput(i, e) -> Einput(i, expression renaming e) + | Eoutput _ -> desc + | Eindex(i, e1, e2) -> + Eindex(i, expression renaming e1, expression renaming e2) in + { ind with desc = desc } in + let init ({ desc = desc } as i) = + let desc = match desc with + | Einit_last(i, e) -> Einit_last(i, expression renaming e) in + { i with desc = desc } in + let i_list = List.map index i_list in + let init_list = List.map init init_list in + let b_eq_list = block renaming b_eq_list in + EQforall { b with for_index = i_list; for_init = init_list; + for_body = b_eq_list } + | EQbefore(before_eq_list) -> + let _, before_eq_list = equation_list renaming before_eq_list in + EQbefore(before_eq_list) + | EQand _ | EQblock _ | EQautomaton _ | EQpresent _ + | EQemit _ | EQder _ | EQnext _ -> assert false in + { renaming with defs = Deftypes.cur_names defs w }, + { eq with eq_desc = desc } :: eq_list + +and equation_list renaming eq_list = + let renaming, eq_list = List.fold_left equation (renaming, []) eq_list in + renaming, List.rev eq_list + +and block renaming ({ b_body = eq_list } as b) = + let rel = List.fold_left build Env.empty eq_list in + let renaming = append rel renaming in + let _, eq_list = equation_list renaming eq_list in + { b with b_body = eq_list } + +let implementation impl = + match impl.desc with + | Efundecl(f, ({ f_body = e } as body)) -> + let e = expression empty e in + let body = { body with f_body = e } in + { impl with desc = Efundecl(f, body) } + | _ -> impl + +let implementation_list impl_list = Zmisc.iter implementation impl_list diff --git a/src/compiler/rewrite/cse.ml b/src/compiler/rewrite/cse.ml new file mode 100644 index 00000000..304c5ec4 --- /dev/null +++ b/src/compiler/rewrite/cse.ml @@ -0,0 +1,169 @@ +(***********************************************************************) +(* *) +(* *) +(* Zelus, a synchronous language for hybrid systems *) +(* *) +(* (c) 2020 Inria Paris (see the AUTHORS file) *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed under *) +(* the terms of the INRIA Non-Commercial License Agreement (see the *) +(* LICENSE file). *) +(* *) +(* *********************************************************************) + +(* common sub-expression for registers. Very simple things. *) +(* For the moment, only equations of the form *) +(* [init x = e0 ... x = e] are shared *) + +open Zmisc +open Zident +open Zelus + +(** Build the association table [pre(n) -> x] and substitution [x\y] *) +(** every time some equation [y = pre(n)] already exists *) +let build_table subst eq_list = + let rec equation (table, subst, eq_list) eq = + match eq.eq_desc with + | EQeq({ p_desc = Evarpat(x) } as p, + ({ e_desc = Eop(Eunarypre, [{ e_desc = Elocal(n) }]) } as e)) -> + begin try + let y = Env.find n table in + table, + (* extends the substitution *) + Env.add x y subst, + { eq with eq_desc = EQeq(p, { e with e_desc = Elocal(y) }) } + :: eq_list + with + | Not_found -> + (* build [pre(n) -> x] if it does not exist already *) + Env.add n x table, subst, eq :: eq_list + end + | EQand(and_eq_list) -> + let table, subst, and_eq_list = equation_list table subst and_eq_list in + table, subst, { eq with eq_desc = EQand(and_eq_list) } :: eq_list + | EQbefore(and_eq_list) -> + let table, subst, and_eq_list = equation_list table subst and_eq_list in + table, subst, { eq with eq_desc = EQbefore(and_eq_list) } :: eq_list + | EQeq _ | EQpluseq _ | EQinit _ | EQnext _ + | EQmatch _ | EQreset _ | EQder _ | EQblock _ | EQforall _ -> + table, subst, eq :: eq_list + | EQemit _ | EQautomaton _ | EQpresent _ -> assert false + and equation_list table subst eq_list = + let table, subst, eq_list = + List.fold_left equation (table, subst, []) eq_list in + table, subst, List.rev eq_list in + let table, subst, eq_list = equation_list Env.empty subst eq_list in + subst, eq_list + +(* substitution *) +let rec exp subst e = + match e.e_desc with + | Econst _ | Econstr0 _ | Eglobal _ | Elast _ -> e + | Elocal(n) -> + begin try { e with e_desc = Elocal(Env.find n subst) } + with Not_found -> e end + | Etuple(e_list) -> + { e with e_desc = Etuple(List.map (exp subst) e_list) } + | Econstr1(c, e_list) -> + { e with e_desc = Econstr1(c, List.map (exp subst) e_list) } + | Eop(op, e_list) -> + let e_list = List.map (exp subst) e_list in + { e with e_desc = Eop(op, e_list) } + | Eapp(app, e_op, e_list) -> + { e with e_desc = + Eapp(app, exp subst e_op, List.map (exp subst) e_list) } + | Erecord(label_e_list) -> + { e with e_desc = + Erecord(List.map (fun (l, e) -> l, exp subst e) label_e_list) } + | Erecord_access(e_record, longname) -> + { e with e_desc = Erecord_access(exp subst e_record, longname) } + | Erecord_with(e_record,label_e_list) -> + { e with e_desc = + Erecord_with(exp subst e_record, + List.map + (fun (l, e) -> l, exp subst e) label_e_list) } + | Etypeconstraint(e1, ty) -> + { e with e_desc = Etypeconstraint(exp subst e1, ty) } + | Eseq(e1, e2) -> + { e with e_desc = Eseq(exp subst e1, exp subst e2) } + | Eperiod _ | Epresent _ | Ematch _ | Elet _ | Eblock _ -> assert false + +(* [equation subst eq = eq'] apply a substitution to eq. *) +and equation subst eq = + match eq.eq_desc with + | EQeq(pat, e) -> { eq with eq_desc = EQeq(pat, exp subst e) } + | EQpluseq(n, e) -> { eq with eq_desc = EQpluseq(n, exp subst e) } + | EQinit(n, e0) -> + { eq with eq_desc = EQinit(n, exp subst e0) } + | EQnext(n, e, e_opt) -> + { eq with eq_desc = EQnext(n, exp subst e, + Zmisc.optional_map (exp subst) e_opt) } + | EQmatch(total, e, m_h_list) -> + let e = exp subst e in + let m_h_list = + List.map + (fun ({ m_body = b} as h) -> { h with m_body = block subst b }) + m_h_list in + { eq with eq_desc = EQmatch(total, e, m_h_list) } + | EQreset(res_eq_list, e) -> + { eq with eq_desc = + EQreset(List.map (equation subst) res_eq_list, + exp subst e) } + | EQand(and_eq_list) -> + { eq with eq_desc = EQand(List.map (equation subst) and_eq_list) } + | EQbefore(before_eq_list) -> + { eq with eq_desc = EQbefore(List.map (equation subst) before_eq_list) } + | EQder(n, e, None, []) -> + { eq with eq_desc = EQder(n, exp subst e, None, []) } + | EQblock(b) -> { eq with eq_desc= EQblock(block subst b) } + | EQforall ({ for_index = i_list; for_init = init_list; + for_body = b_eq_list } as body) -> + let index ({ desc = desc } as ind) = + let desc = match desc with + | Einput(x, e) -> Einput(x, exp subst e) + | Eoutput _ -> desc + | Eindex(x, e1, e2) -> Eindex(x, exp subst e1, exp subst e2) in + { ind with desc = desc } in + let init ({ desc = desc } as ini) = + let desc = match desc with + | Einit_last(x, e) -> Einit_last(x, exp subst e) in + { ini with desc = desc } in + let i_list = List.map index i_list in + let init_list = List.map init init_list in + let b_eq_list = block subst b_eq_list in + { eq with eq_desc = + EQforall { body with for_index = i_list; + for_init = init_list; + for_body = b_eq_list } } + | EQder _ | EQemit _ | EQautomaton _ | EQpresent _ -> assert false + +and local subst ({ l_eq = eq_list } as l) = + (* extends the association table *) + let subst, eq_list = build_table subst eq_list in + (* apply the substitution *) + let eq_list = List.map (equation subst) eq_list in + { l with l_eq = eq_list } + +and block subst ({ b_body = eq_list } as b) = + let subst, eq_list = build_table subst eq_list in + let eq_list = List.map (equation subst) eq_list in + { b with b_body = eq_list } + +(** the main entry for expressions. Warning: [e] must be in normal form *) +let exp subst e = + match e.e_desc with + | Elet(l, e1) -> + let l = local subst l in + let e1 = exp subst e1 in + { e with e_desc = Elet(l, e1) } + | _ -> exp subst e + +let implementation impl = + match impl.desc with + | Eopen _ | Etypedecl _ | Econstdecl _ -> impl + | Efundecl(n, ({ f_body = e } as body)) -> + { impl with desc = + Efundecl(n, { body with f_body = exp Env.empty e }) } + +let implementation_list impl_list = Zmisc.iter implementation impl_list diff --git a/src/compiler/rewrite/deadcode.ml b/src/compiler/rewrite/deadcode.ml new file mode 100644 index 00000000..490c6229 --- /dev/null +++ b/src/compiler/rewrite/deadcode.ml @@ -0,0 +1,344 @@ +(***********************************************************************) +(* *) +(* *) +(* Zelus, a synchronous language for hybrid systems *) +(* *) +(* (c) 2020 Inria Paris (see the AUTHORS file) *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed under *) +(* the terms of the INRIA Non-Commercial License Agreement (see the *) +(* LICENSE file). *) +(* *) +(* *********************************************************************) + +(* dead-code removal. *) +(* this is applied to normalized code *) + +open Zmisc +open Zident +open Vars +open Zelus +open Deftypes + +(** Dead-code removal. First build a table [yn -> {x1,...,xk}] wich associate *) +(** the list of read variables used to produce yn *) +(** then recursively mark all useful variable according to *) +(** read-in dependences *) +(** An equation [eq] is marked useful when it may be unsafe, that *) +(** is, it has side effets and/or is non total *) +(** For the moment, only combinatorial functions *) +(** are considered safe. *) +(** finally, only keep equations and name defs. for useful variables *) +(** horizons are considered to be useful *) +type table = cont Env.t + and cont = + { mutable c_vars: S.t; (* set of variables *) + mutable c_useful: bool; (* is-it a useful variable? *) + mutable c_visited: bool; (* has it been visited already? *) } + +(** Useful function. For debugging purpose. *) +let print ff table = + let names ff l = + Pp_tools.print_list_r Printer.name "{" "," "}" ff (S.elements l) in + let entry x { c_vars = l; c_useful = u } = + Format.fprintf ff "@[%a -> {c_vars = %a; c_useful = %s}@]@ " + Printer.name x + names l (if u then "true" else "false") in + Env.iter entry table + +(* Add the entries [x_j <- x1; ...; x_j <- xn] in the table. *) +(* for any variable [x_j in w] *) +(* if [x_j] already, extends the set of variables on which it depends. *) +(* Otherwise, add the new entry *) +(* when [is_useful = true], mark all read and write variables to be useful *) +let add is_useful w r table = + (* mark all names in [set] to be useful *) + let mark_useful set table = + let mark x table = + try + let { c_useful = u } as cont = Env.find x table in + cont.c_useful <- true; + table + with + | Not_found -> + Env.add x + { c_vars = S.empty; c_useful = true; + c_visited = false } table in + S.fold mark set table in + + let add x table = + try + let { c_vars = l; c_useful = u } as cont = Env.find x table in + cont.c_vars <- S.union r l; + cont.c_useful <- u || is_useful; + table + with + | Not_found -> + Env.add x + { c_vars = r; c_useful = is_useful; c_visited = false } table in + (* mark all vars. in [r] to be useful *) + let table = if is_useful then mark_useful r table else table in + (* add dependences *) + S.fold add w table + + +(** Extend [table] where every entry [y -> {x1,...,xn}] *) +(** is marked to also depend on names in [names] *) +let extend table names = + Env.map + (fun ({ c_vars = l } as cont) -> { cont with c_vars = S.union l names }) + table + +(** Fusion of two tables *) +let merge table1 table2 = + let add x ({ c_vars = l1; c_useful = u1 } as cont1) table = + try + let ({ c_vars = l2; c_useful = u2 } as cont2) = Env.find x table in + cont2.c_vars <- S.union l1 l2; cont2.c_useful <- u1 || u2; + table + with + | Not_found -> Env.add x cont1 table in + Env.fold add table2 table1 + +(** Build the association table [yk -> { x1,..., xn}] *) +let rec build_equation table { eq_desc = desc } = + match desc with + | EQeq(p, e) -> + let w = fv_pat S.empty S.empty p in + (* for every [x in w], add the link [x -> {x1, ..., xn }] to table *) + let r = fve S.empty e in + add (Unsafe.exp e) w r table + | EQpluseq(n, e) | EQinit(n, e) + | EQder(n, e, None, []) -> + let r = fve S.empty e in + add (Unsafe.exp e) (S.singleton n) r table + | EQmatch(_, e, m_h_list) -> + let r = fve S.empty e in + let u = Unsafe.exp e in + (* mark read variables to be useful when [e] is potentially unsafe *) + let table = add u S.empty r table in + let table_b = + List.fold_left + (fun table { m_body = b } -> build_block table b) + Env.empty m_h_list in + merge table (extend table_b r) + | EQreset(res_eq_list, e) -> + let r = fve S.empty e in + let u = Unsafe.exp e in + (* mark read variables to be useful when [e] is potentially unsafe *) + let table = add u S.empty r table in + let table_res = build_equation_list Env.empty res_eq_list in + merge table (extend table_res r) + | EQforall { for_index = i_list; for_init = init_list; + for_body = b_eq_list } -> + let index table { desc = desc } = + match desc with + | Einput(i, e) -> + add (Unsafe.exp e) (S.singleton i) (fve S.empty e) table + | Eoutput(i, j) -> + add false (S.singleton j) (S.singleton i) table + | Eindex(i, e1, e2) -> + add ((Unsafe.exp e1) || (Unsafe.exp e2)) + (S.singleton i) (fve (fve S.empty e1) e2) table in + let init table { desc = desc } = + match desc with + | Einit_last(i, e) -> + add (Unsafe.exp e) (S.singleton i) (fve S.empty e) table in + let table = List.fold_left index table i_list in + let table = List.fold_left init table init_list in + build_block table b_eq_list + | EQand(eq_list) | EQbefore(eq_list) -> build_equation_list table eq_list + | EQblock _ | EQder _ | EQnext _ | EQautomaton _ + | EQpresent _ | EQemit _ -> assert false + +and build_block table { b_body = eq_list } = build_equation_list table eq_list + +and build_local table { l_eq = eq_list } = build_equation_list table eq_list + +and build_equation_list table eq_list = + List.fold_left build_equation table eq_list + +(** Visit the table: recursively mark all useful variables *) +(** returns the set of useful variables *) +(** [read] is a set of variables *) +let visit read table = + let useful = ref S.empty in + (* recursively mark visited nodes which are useful *) + let rec visit x ({ c_vars = l; c_useful = u; c_visited = v } as entry) = + if not v then + begin + entry.c_visited <- true; + entry.c_useful <- true; + useful := S.add x !useful; + S.iter visit_fathers l + end + and visit_fathers x = + useful := S.add x !useful; + try + let entry = Env.find x table in + visit x entry + with + Not_found -> () + (* look for an entry in the table that is not marked but useful *) + and visit_table x ({ c_useful = u; c_visited = v } as entry) = + if not v && u then visit x entry in + (* recursively mark nodes and their predecessors *) + S.iter visit_fathers read; + Env.iter visit_table table; + !useful + +(** Empty block *) +let is_empty_block { b_locals = l; b_body = eq_list } = + (l = []) && (eq_list = []) + +(** remove useless names in write names *) +let writes useful { dv = dv; di = di; der = der; nv = nv; mv = mv } = + let filter set = S.filter (fun x -> S.mem x useful) set in + { dv = filter dv; di = filter di; der = filter der; + nv = filter nv; mv = filter mv } + +(* remove useless names in a pattern *) +let rec pattern useful ({ p_desc = desc } as p) = + match desc with + | Ewildpat | Econstpat _ | Econstr0pat _ -> p + | Etuplepat(p_list) -> + { p with p_desc = Etuplepat(List.map (pattern useful) p_list) } + | Econstr1pat(c, p_list) -> + { p with p_desc = Econstr1pat(c, List.map (pattern useful) p_list) } + | Evarpat(x) -> if S.mem x useful then p else { p with p_desc = Ewildpat } + | Ealiaspat(p_alias, x) -> + let p_alias = pattern useful p_alias in + if S.mem x useful then { p with p_desc = Ealiaspat(p_alias, x) } + else p_alias + | Eorpat(p1, p2) -> + { p with p_desc = Eorpat(pattern useful p1, pattern useful p2) } + | Erecordpat(ln_pat_list) -> + { p with p_desc = + Erecordpat(List.map (fun (ln, p) -> + (ln, pattern useful p)) ln_pat_list) } + | Etypeconstraintpat(p, ty_exp) -> + let p = pattern useful p in + { p with p_desc = Etypeconstraintpat(p, ty_exp) } + +(** Remove useless equations. [useful] is the set of useful names *) +let rec remove_equation useful + ({ eq_desc = desc; eq_write = w } as eq) eq_list = + match desc with + | EQeq(p, e) -> + let w = fv_pat S.empty S.empty p in + if Unsafe.exp e || S.exists (fun x -> S.mem x useful) w + then (* the equation is useful *) + { eq with eq_desc = EQeq(pattern useful p, e) } :: eq_list else eq_list + | EQpluseq(n, e) | EQder(n, e, None, []) + | EQinit(n, e) -> + if Unsafe.exp e || S.mem n useful then eq :: eq_list else eq_list + | EQmatch(total, e, m_h_list) -> + let m_h_list = + List.map + (fun ({ m_body = b } as m_h) -> + { m_h with m_body = remove_block useful b }) m_h_list in + (* remove the equation if all handlers are empty *) + if not (Unsafe.exp e) + && List.for_all (fun { m_body = b} -> is_empty_block b) m_h_list + then eq_list + else { eq with eq_desc = EQmatch(total, e, m_h_list); + eq_write = writes useful w } :: eq_list + | EQreset(res_eq_list, e) -> + let res_eq_list = remove_equation_list useful res_eq_list in + (* remove the equation if the body is empty *) + if not (Unsafe.exp e) && res_eq_list = [] then eq_list + else { eq with eq_desc = EQreset(res_eq_list, e); + eq_write = writes useful w } :: eq_list + | EQforall({ for_index = i_list; for_init = init_list; for_body = b_eq_list; + for_in_env = in_env; for_out_env = out_env } as f_body) -> + let index acc ({ desc = desc } as ind) = + match desc with + | Einput(i, e) -> + if (Unsafe.exp e) || (S.mem i useful) then ind :: acc else acc + | Eoutput(xo, o) -> + if (S.mem xo useful) || (S.mem o useful) then ind :: acc else acc + | Eindex _ -> + (* the index i in [e1 .. e2] is kept *) + ind :: acc in + let init acc ({ desc = desc } as ini) = + match desc with + | Einit_last(i, e) -> + if (Unsafe.exp e) || (S.mem i useful) then ini :: acc else acc in + let i_list = List.fold_left index [] i_list in + let init_list = List.fold_left init [] init_list in + let b_eq_list = remove_block useful b_eq_list in + let in_env = Env.filter (fun x entry -> S.mem x useful) in_env in + let out_env = Env.filter (fun x entry -> S.mem x useful) out_env in + if is_empty_block b_eq_list then eq_list + else { eq with eq_desc = + EQforall { f_body with + for_index = i_list; + for_init = init_list; + for_body = b_eq_list; + for_in_env = in_env; + for_out_env = out_env } } :: eq_list + | EQbefore(before_eq_list) -> + let before_eq_list = remove_equation_list useful before_eq_list in + (* remove the equation if the body is empty *) + if before_eq_list = [] then eq_list + else (Zaux.before before_eq_list) :: eq_list + | EQand(and_eq_list) -> + let and_eq_list = remove_equation_list useful and_eq_list in + (* remove the equation if the body is empty *) + if and_eq_list = [] then eq_list + else (Zaux.par and_eq_list) :: eq_list + | EQnext _ | EQder _ | EQautomaton _ | EQblock _ + | EQpresent _ | EQemit _ -> assert false + +and remove_equation_list useful eq_list = + List.fold_right (remove_equation useful) eq_list [] + +and remove_block useful + ({ b_vars = n_list; b_locals = l_list; + b_body = eq_list; + b_write = ({ dv = w } as defnames); + b_env = n_env } as b) = + let l_list = List.map (remove_local useful) l_list in + let eq_list = remove_equation_list useful eq_list in + let n_list = + List.filter (fun { vardec_name = x } -> S.mem x useful) n_list in + let n_env = Env.filter (fun x entry -> S.mem x useful) n_env in + let w = S.filter (fun x -> S.mem x useful) w in + { b with b_vars = n_list; b_locals = l_list; b_body = eq_list; + b_write = { defnames with dv = w }; b_env = n_env } + +and remove_local useful ({ l_eq = eq_list; l_env = l_env } as l) = + let eq_list = remove_equation_list useful eq_list in + let l_env = Env.filter (fun x entry -> S.mem x useful) l_env in + { l with l_eq = eq_list; l_env = l_env } + +(** Compute the set of horizons *) +let horizon read { l_env = l_env } = + let take h { t_sort = sort } acc = + match sort with + | Smem { m_kind = Some(Horizon) } -> S.add h acc | _ -> acc in + Env.fold take l_env read + +(** the main entry for expressions. Warning: [e] must be in normal form *) +let exp ({ e_desc = desc } as e) = + match desc with + | Elet(l, e_let) -> + let read = fve S.empty e_let in + (* horizons are considered as outputs *) + let read = horizon read l in + let table = build_local Env.empty l in + (* Format.printf "%a@.@." print table; *) + let useful = visit read table in + (* Format.printf "%a@." print table; flush stdout; *) + let { l_eq = eq_list } as l = remove_local useful l in + if eq_list = [] then e_let else { e with e_desc = Elet(l, e_let) } + | _ -> e + +let implementation impl = + match impl.desc with + | Eopen _ | Etypedecl _ | Econstdecl _ -> impl + | Efundecl(n, ({ f_body = e } as body)) -> + { impl with desc = Efundecl(n, { body with f_body = exp e }) } + +let implementation_list impl_list = Zmisc.iter implementation impl_list diff --git a/src/compiler/rewrite/rewrite.ml b/src/compiler/rewrite/rewrite.ml index 15841b12..a3a5a98d 100644 --- a/src/compiler/rewrite/rewrite.ml +++ b/src/compiler/rewrite/rewrite.ml @@ -24,18 +24,17 @@ let hybrid_list = "disc", "Translation of disc done. See below:", Disc.program] -(* let optim_list = - ["horizon", - "Gather all horizons into a single one per function. See below:", - Horizon.program; - "aform", "A-normal form. See below:", + ["aform", "A-normal form. See below:", Aform.program; "deadcode", "Dead-code removal. See below:", Deadcode.program; - "copy", "Remove of copy variables. See below:", - Copy.program] -*) + "cse", "Common sub-expression elimination. See below:", + Cse.program; + "copy", "Remove of copy variables. See below:", + Copy.program; + "zopt", "Sharing of zero-crossings. See below:", + Zopt.program] let default_list = ["static", "Static reduction done. See below:", @@ -55,8 +54,8 @@ let default_list = "shared", "Normalise equations to shared variables in [x = ...]. See below:", Shared.program; - (* "encore", "Add an extra discrete step for weak transitions. See below:", - Encore.program; *) + "encore", "Add an extra discrete step for weak transitions. See below:", + Encore.program; "lastinpatterns", "Replace [last x] by [last* m] when [x] is an input variable.\n\ See below:", @@ -66,7 +65,7 @@ let default_list = is a local variable. See below:", Copylast.program; "letin", "Un-nesting of let/in and blocks. See below:", - Letin.program; + Letin.program] @ optim_list @ [ "schedule", "Static scheduling. See below:", Schedule.program ] diff --git a/src/compiler/rewrite/zopt.ml b/src/compiler/rewrite/zopt.ml new file mode 100644 index 00000000..d86de31a --- /dev/null +++ b/src/compiler/rewrite/zopt.ml @@ -0,0 +1,235 @@ +(***********************************************************************) +(* *) +(* *) +(* Zelus, a synchronous language for hybrid systems *) +(* *) +(* (c) 2020 Inria Paris (see the AUTHORS file) *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed under *) +(* the terms of the INRIA Non-Commercial License Agreement (see the *) +(* LICENSE file). *) +(* *) +(* *********************************************************************) + +(* sharing of zero-crossings *) +(* Zero-crossing that appear in exclusive control branches are shared *) +(* This transformation is applied to normalized equations and expressions *) +(* [z1 = up(e1) # z2 = up(e2)] becomes [z1 = up(e1) # z1 = up(e2)] *) +(* Two phases algorithm: + * one phase computes zero-crossing variables and a substitution; + * the second one applies the subsitution *) +open Zident +open Zelus +open Deftypes + +(* an environment { env, size, subst } + * env: the environment of zero-crossings; + * ren: Zident.t -> Zident.t defines the renaming of zero-crossings + * size: number of entries in env *) +type zenv = { env: Deftypes.tentry Env.t; ren: Zident.t Env.t; size: int } + +let zempty = { env = Env.empty; ren = Env.empty; size = 0 } + +(* Partition an environment into an environment of zero-crossing variables *) +(* and its complement *) +let zero_from_env env = + let select key { t_sort = s } = + match s with + | Smem { m_kind = Some(Zero) } -> true | _ -> false in + Env.partition select env + +let vars_of_env vars env = + List.filter (fun { vardec_name = x } -> Env.mem x env) vars + +(* Make a renaming from two environment *) +(* [make env2 env1 = ren] where + * ren = [x1\y1,..., xn\yn] with [x1,...,xn] = Dom(env2) + * and [y1,...,yn] in Dom(env1) *) +let make env2 env1 = + (* [one key entry (l, acc) = acc + [key \ key'], l'] + * renames key into key' if [l = [key', entry'].l'] *) + let one key _ (l, acc) = + match l with + | [] -> assert false (* env1 is supposed to be bigger than env2 *) + | (key', _) :: l -> l, Env.add key key' acc in + let l1 = Env.bindings env1 in + let _, ren = Env.fold one env2 (l1, Env.empty) in + ren + +(* Compose two renamings. *) +(* [compose r2_by_1 r2 = r] returns an environment [r] such that: + * r(x) = r2_by_1 (r2(x)) *) +let compose r2_by_1 r2 = + Env.map (fun n2 -> try Env.find n2 r2_by_1 with Not_found -> assert false) r2 + +(* Composition of two environment *) +let parallel + { env = env1; ren = r1; size = s1 } { env = env2; ren = r2; size = s2 } = + { env = Env.append env1 env2; ren = Env.append r1 r2; size = s1 + s2 } + +let sharp + { env = env1; ren = r1; size = s1 } { env = env2; ren = r2; size = s2 } = + (* all names of env2 are renamed by those from env1 if s1 >= s2 *) + if s1 >= s2 + then let r2_by_1 = make env2 env1 in + let r = Env.append r1 (Env.append r2_by_1 (compose r2_by_1 r2)) in + { env = env1; ren = r; size = s1 } + else let r1_by_2 = make env1 env2 in + let r = Env.append r2 (Env.append r1_by_2 (compose r1_by_2 r1)) in + { env = env2; ren = r; size = s2 } + +(* [equation eq = eq', zenv] where + * eq': the new equation in which zero-crossing variables have been removed + * zenv.env: the set of zero-crossing variables defined in eq + * zenv.rename: Zident.t -> Zident.t, the substitution of zero-crossing variables *) +let rec equation ({ eq_desc = desc } as eq) = + match desc with + | EQeq _ | EQpluseq _ | EQder _ | EQinit _ -> eq, zempty + | EQmatch(total, e, m_h_list) -> + let m_h_list, zenv = + Zmisc.map_fold (fun acc ({ m_body = b } as m_h) -> + let b, zenv = block b in + { m_h with m_body = b }, + sharp acc zenv) + zempty m_h_list in + { eq with eq_desc = EQmatch(total, e, m_h_list) }, zenv + | EQreset(eq_list, e) -> + let eq_list, zenv = equation_list eq_list in + { eq with eq_desc = EQreset(eq_list, e) }, zenv + | EQand(and_eq_list) -> + let and_eq_list, zenv = equation_list and_eq_list in + { eq with eq_desc = EQand(and_eq_list) }, zenv + | EQbefore(before_eq_list) -> + let before_eq_list, zenv = equation_list before_eq_list in + { eq with eq_desc = EQbefore(before_eq_list) }, zenv + | EQforall _ -> eq, zempty + | EQblock _ | EQpresent _ | EQautomaton _ | EQnext _ | EQemit _ -> + assert false + +and equation_list eq_list = + Zmisc.map_fold (fun acc eq -> let eq, zenv = equation eq in + eq, parallel acc zenv) + zempty eq_list + +and block ({ b_vars = vars; b_env = b_env; b_body = eq_list } as b) = + let zero_env, b_env = zero_from_env b_env in + let eq_list, zenv = equation_list eq_list in + { b with b_vars = vars_of_env vars b_env; b_env = b_env; b_body = eq_list }, + parallel { env = zero_env; ren = Env.empty; size = Env.cardinal zero_env } zenv + +(* renaming *) +let rec rename_expression ren ({ e_desc = desc } as e) = + match desc with + | Econst _ | Econstr0 _ | Eglobal _ -> e + | Elocal(x) -> { e with e_desc = Elocal(apply x ren) } + | Elast(x) -> { e with e_desc = Elast(apply x ren) } + | Etuple(e_list) -> + { e with e_desc = Etuple(List.map (rename_expression ren) e_list) } + | Econstr1(c, e_list) -> + { e with e_desc = Econstr1(c, List.map (rename_expression ren) e_list) } + | Erecord(n_e_list) -> + { e with e_desc = + Erecord(List.map (fun (ln, e) -> + (ln, rename_expression ren e)) n_e_list) } + | Erecord_access(e_record, ln) -> + { e with e_desc = Erecord_access(rename_expression ren e_record, ln) } + | Erecord_with(e_record, n_e_list) -> + { e with e_desc = + Erecord_with(rename_expression ren e_record, + List.map + (fun (ln, e) -> + (ln, rename_expression ren e)) n_e_list) } + | Eop(op, e_list) -> + { e with e_desc = Eop(op, List.map (rename_expression ren) e_list) } + | Eapp(app, e_op, e_list) -> + let e_op = rename_expression ren e_op in + let e_list = List.map (rename_expression ren) e_list in + { e with e_desc = Eapp(app, e_op, e_list) } + | Etypeconstraint(e1, ty) -> + { e with e_desc = Etypeconstraint(rename_expression ren e1, ty) } + | Eseq(e1, e2) -> + { e with e_desc = Eseq(rename_expression ren e1, rename_expression ren e2) } + | Eperiod _ | Epresent _ | Ematch _ | Elet _ | Eblock _ -> assert false + +and rename_local ren ({ l_eq = eq_list } as l) = + let eq_list = rename_equation_list ren eq_list in + { l with l_eq = eq_list } + +and rename_equation ren ({ eq_desc = desc } as eq) = + let desc = match desc with + (* zero-crossing definitions must be of the form [x = up(e)] *) + | EQeq({ p_desc = Evarpat(x) } as p, e) -> + EQeq( { p with p_desc = Evarpat(apply x ren) }, rename_expression ren e) + | EQeq(p, e) -> EQeq(p, rename_expression ren e) + | EQpluseq(x, e) -> EQpluseq(apply x ren, rename_expression ren e) + | EQinit(x, e0) -> EQinit(apply x ren, rename_expression ren e0) + | EQmatch(total, e, m_h_list) -> + let m_h_list = + List.map + (fun ({ m_body = b } as m_h) -> + { m_h with m_body = rename_block ren b }) + m_h_list in + EQmatch(total, rename_expression ren e, m_h_list) + | EQder(x, e, None, []) -> EQder(x, rename_expression ren e, None, []) + | EQreset(res_eq_list, e) -> + let e = rename_expression ren e in + let res_eq_list = rename_equation_list ren res_eq_list in + EQreset(res_eq_list, e) + | EQand(and_eq_list) -> + EQand(rename_equation_list ren and_eq_list) + | EQbefore(before_eq_list) -> + EQbefore(rename_equation_list ren before_eq_list) + | EQforall ({ for_index = i_list; for_init = init_list; + for_body = b_eq_list } as body) -> + let index ({ desc = desc } as ind) = + let desc = match desc with + | Einput(x, e) -> Einput(x, rename_expression ren e) + | Eoutput _ -> desc + | Eindex(x, e1, e2) -> Eindex(x, rename_expression ren e1, + rename_expression ren e2) in + { ind with desc = desc } in + let init ({ desc = desc } as ini) = + let desc = match desc with + | Einit_last(x, e) -> Einit_last(x, rename_expression ren e) in + { ini with desc = desc } in + let i_list = List.map index i_list in + let init_list = List.map init init_list in + let b_eq_list = rename_block ren b_eq_list in + EQforall { body with for_index = i_list; for_init = init_list; + for_body = b_eq_list } + | EQblock _ | EQautomaton _ | EQpresent _ + | EQemit _ | EQder _ | EQnext _ -> assert false in + { eq with eq_desc = desc } + +and rename_equation_list ren eq_list = List.map (rename_equation ren) eq_list + +and rename_block ren ({ b_body = eq_list } as b) = + let eq_list = rename_equation_list ren eq_list in + { b with b_body = eq_list } + +and apply x ren = + try Env.find x ren with | Not_found -> x + +(* The main functions *) +let local ({ l_eq = eq_list; l_env = l_env } as l) = + let eq_list, { env = env; ren = ren } = equation_list eq_list in + let eq_list = rename_equation_list ren eq_list in + { l with l_eq = eq_list; l_env = Env.append env l_env } + +let expression ({ e_desc = desc } as e) = + let desc = + match desc with + | Elet(l, e) -> Elet(local l, e) + | _ -> desc in + { e with e_desc = desc } + +let implementation impl = + match impl.desc with + | Econstdecl(n, is_static, e) -> + { impl with desc = Econstdecl(n, is_static, expression e) } + | Efundecl(n, ({ f_body = e } as body)) -> + { impl with desc = Efundecl(n, { body with f_body = expression e }) } + | _ -> impl + +let implementation_list impl_list = Zmisc.iter implementation impl_list diff --git a/src/dune b/src/dune index dc70f906..761bee43 100644 --- a/src/dune +++ b/src/dune @@ -169,7 +169,11 @@ complete ; complete equations with [der x = 0.0] shared ; normalise equations to shared variables into [x = ...] letin ; un-nesting of let/in and blocks - ; deadcode ; deadcode removal + aform ; A-normal form + zopt ; sharing of zero-crossings + copy ; remove of copy variables + cse ; common sub-expression elimination + deadcode ; deadcode removal vars ; read variables dependences ; data-dependences between equations control ; fusion of control dependences diff --git a/src/zrun/coiteration.ml b/src/zrun/coiteration.ml index e6ac8ef4..605d91e6 100644 --- a/src/zrun/coiteration.ml +++ b/src/zrun/coiteration.ml @@ -1602,12 +1602,10 @@ and seq genv env { eq_desc; eq_write; eq_loc } s = is_bool b |> Opt.to_result ~none:{ kind = Etype; loc = e.e_loc } in if v then let* env_true, s_eq_true = seq genv env eq_true s_eq_true in - let l1 = Env.to_list env_true in (* complete the output environment with default *) (* or last values from all variables defined in [eq_write] but *) (* not in [env1] *) let* env_true = Fix.by eq_loc env env_true (names eq_write) in - let l2 = Env.to_list env_true in return (env_true, [s_eq_true; s_eq_false]) else let* env_false, s_eq_false = seq genv env eq_false s_eq_false in @@ -1935,17 +1933,12 @@ and sblock_with_reset genv env b_eq s_eq r = (* for[ward|each] [resume] (n)[i](...) returns (acc_env) local x1,...,xm do eq [[while|until|unless] c] *) and sforblock genv env acc_env b for_exit s_b = - let l0 = Env.to_list env in - let l1 = Env.to_list acc_env in (* the semantics for a block [local x1,...,xn do eq] *) let sbody genv env b s_b acc_env = let sem s_b env_in = let* env, env_eq_not_x, s_b = sblock genv (Env.append env_in env) b s_b in - let l1 = Env.to_list env in - let l2 = Env.to_list env_eq_not_x in let new_env_in = Fix.complete env_in env_eq_not_x in - let l3 = Env.to_list new_env_in in return ((env, new_env_in), s_b) in let* _, (env, new_acc_env), s_b = Fix.fixpoint b.b_loc (Env.cardinal acc_env + 1) Fix.stop sem s_b acc_env @@ -1966,8 +1959,6 @@ and sforblock genv env acc_env b for_exit s_b = match for_exit with | None -> let* env, new_acc_env, s_b = sbody genv env b s_b acc_env in - let l1 = Env.to_list env in - let l2 = Env.to_list new_acc_env in return (false, new_acc_env, s_b) | Some { for_exit; for_exit_kind } -> match for_exit_kind with diff --git a/src/zrun/forloop.ml b/src/zrun/forloop.ml index fbe6db7a..e47df525 100644 --- a/src/zrun/forloop.ml +++ b/src/zrun/forloop.ml @@ -203,13 +203,10 @@ let step loc sbody env i_env i acc_env s = Debug.print_state "For loop: state before step = " s; let* env_0 = geti_env loc i_env i in let env = Env.append env_0 env in - let l1 = Env.to_list env in Debug.print_ienv "For loop: acc_env = " acc_env; let* is_exit, local_env, s = sbody env acc_env s in (* every entry [x\v] from [acc_env] becomes [x \ { cur = bot; last = v }] *) - let l2 = Env.to_list local_env in let acc_env = x_to_lastx acc_env local_env in - let l3 = Env.to_list acc_env in Debug.print_ienv "For loop: local_env = " local_env; Debug.print_ienv "For loop: acc_env = " acc_env; Debug.print_state "For loop: state after step = " s;