Skip to content

Commit

Permalink
Update - first step of copy.ml
Browse files Browse the repository at this point in the history
  • Loading branch information
@marcpouzet
marcpouzet committed Oct 27, 2024
1 parent aeb9eaa commit 09d1947
Show file tree
Hide file tree
Showing 4 changed files with 83 additions and 342 deletions.
50 changes: 23 additions & 27 deletions src/compiler/rewrite/aform.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -31,13 +31,17 @@ type acc =

let empty = { renaming = Env.empty; subst = Env.empty }

(* matching. Translate [(p1,...,pn) = (e1,...,en)] into *)
(* [p1 = e1 and ... and pn = en] *)
let rec matching eq_list ({ pat_desc } as p) ({ e_desc } as e) =
match pat_desc, e_desc with
| Etuplepat(p_list), Etuple(e_list) ->
List.fold_left2 matching eq_list p_list e_list
| _ -> (Aux.eq_make p e) :: eq_list

let find { renaming; subst } id =
try Env.find id renaming with | Not_found -> assert false

let last_ident global_funs acc id = find acc id, acc
let init_ident global_funs acc id = find acc id, acc
let der_ident global_funs acc id = find acc id, acc

let rec make_pat t =
match t with
| Leaf(id) -> Aux.varpat id
Expand All @@ -53,6 +57,8 @@ let rec names acc t =
| Leaf(id) -> id :: acc
| Lpar(t_list) -> List.fold_left names acc t_list

let var_ident global_funs acc id = find acc id, acc

(* Build an accumulator from an environment *)
let build global_funs ({ renaming; subst } as acc) env =
let rec buildrec n ({ t_tys = { typ_body }; t_sort; t_path } as entry)
Expand All @@ -79,41 +85,31 @@ let build global_funs ({ renaming; subst } as acc) env =
let env, acc = Env.fold buildrec env (Env.empty, acc) in
env, acc

(* matching. Translate [(p1,...,pn) = (e1,...,en)] into *)
(* [p1 = e1 and ... and pn = en] *)
let rec matching eq_list ({ pat_desc } as p) ({ e_desc } as e) =
match pat_desc, e_desc with
| Etuplepat(p_list), Etuple(e_list) ->
List.fold_left2 matching eq_list p_list e_list
| _ -> (Aux.eq_make p e) :: eq_list

let pattern funs { renaming; subst } ({ pat_desc } as p) =
let pattern funs ({ renaming; subst } as acc) ({ pat_desc } as p) =
match pat_desc with
| Evarpat(x) ->
begin try
{ p with pat_desc = Evarpat(Env.find x renaming) }
let p =
try { p with pat_desc = Evarpat(Env.find x renaming) }
with
| Not_found ->
try
make_pat (Env.find x subst)
with | Not_found -> assert false
end
with | Not_found -> assert false in
p, acc
| _ -> raise Mapfold.Fallback

let expression funs acc e =
let ({ e_desc } as e), ({ renaming; subst } as acc) =
Mapfold.expression_it funs acc e in
let expression funs ({ renaming; subst } as acc) ({ e_desc } as e) =
match e_desc with
| Evar(x) ->
begin try
{ e with e_desc = Evar(Env.find x renaming) }
let e =
try { e with e_desc = Evar(Env.find x renaming) }
with
| Not_found ->
try
make_exp (Env.find x subst)
with | Not_found -> assert false
end
| _ -> e
with | Not_found -> assert false in
e, acc
| _ -> raise Mapfold.Fallback

let equation funs acc eq =
let ({ eq_desc } as eq), acc = Mapfold.equation_it funs acc eq in
Expand All @@ -138,10 +134,10 @@ let set_index funs acc n =
let get_index funs acc n = Ident.get (), acc

let program genv p =
let global_funs = { Mapfold.default_global_funs with build } in
let global_funs = { Mapfold.default_global_funs with build; var_ident } in
let funs =
{ Mapfold.defaults with
equation; vardec_list;
pattern; expression; equation; vardec_list;
set_index; get_index; global_funs } in
let p, _ = Mapfold.program_it funs empty p in
p
Expand Down
204 changes: 59 additions & 145 deletions src/compiler/rewrite/copy.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@
(* *)
(* Zelus, a synchronous language for hybrid systems *)
(* *)
(* (c) 2020 Inria Paris (see the AUTHORS file) *)
(* (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 *)
Expand All @@ -16,186 +16,100 @@
(* The transformation is applied after static scheduling and before *)
(* translation into sequential code *)

open Zmisc
open Zident
open Misc
open Ident
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 'a value = | Vvar of Ident.t | Vlast of Zelus.last | Vconst of 'a

type renaming =
{ rel: value Env.t; (* the substitution *)
defs: S.t; (* names after which the substitution cannot be applied *)
type 'a renaming =
{ rel: 'a Env.t; (* the substitution *)
defs: S.t; (* names for 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) =
let append new_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 } =
(* 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; 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
| Vvar m -> rename m
| Vlast({ id } as l) ->
if S.mem id defs then raise Not_found else Elast l
| Vconst(v) -> v
end
with Not_found -> Elocal n in
with Not_found -> Evar n in
rename n

let rec size ({ rel = rel } as renaming) ({ desc = desc } as s) =
let rec size ({ rel } as renaming) ({ desc } as s) =
try
let s =
match desc with
| Sconst _ | Sglobal _ -> s
| Sname(n) ->
| Size_int _ -> s
| Size_var(n) ->
let n = Env.find n rel in
begin match n with
| Vlocal n -> { s with desc = Sname(n) }
| Vvar n -> { s with desc = Size_var(n) }
| _ -> raise Not_found
end
| Sop(op, s1, s2) ->
{ s with desc = Sop(op, size renaming s1, size renaming s2) } in
| Size_op(op, s1, s2) ->
{ s with desc = Size_op(op, size renaming s1, size renaming s2) }
| Size_frac({ num } as f) ->
{ s with desc = Size_frac({ f with num = size renaming num }) } 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 }) ->
(* Build a substitution [x1\v1,...,xn\vn] *)
let rec build rel { eq_desc } =
match eq_desc with
| EQeq({ pat_desc = Evarpat(x) }, { e_desc }) ->
let rel =
match desc with
| Elocal m -> Env.add x (Vlocal(m)) rel
| Eglobal _ | Econst _ -> Env.add x (Vconst(desc)) rel
match e_desc with
| Evar m -> Env.add x (Vvar(m)) rel
| Eglobal _ | Econst _ -> Env.add x (Vconst(e_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
| EQreset(eq, _) -> build rel eq
| EQand { eq_list } -> List.fold_left build rel eq_list
| _ -> rel

(** 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
(* Function to traverse the ast *)
(* Apply [renaming] to every sub-expression *)
let expression funs renaming ({ e_desc } as e) =
match e_desc with
| Evar(id) -> { e with e_desc = rename id renaming }, renaming
| _ -> raise Mapfold.Fallback

(** 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 }
(* Local declarations *)
let leq_t funs renaming ({ l_eq } as l) =
let rel = build Env.empty l_eq in
let new_renaming = append rel renaming in
let l_eq, renaming = Mapfold.equation_it funs new_renaming l_eq in
{ l with l_eq }, renaming

(** 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
let block funs renaming ({ b_body } as b) =
let rel = build Env.empty b_body in
let new_renaming = append rel renaming in
let b_body, renaming = Mapfold.equation_it funs new_renaming b_body in
{ b with b_body }, renaming

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
let program genv p =
let global_funs = Mapfold.default_global_funs in
let funs =
{ Mapfold.defaults with
expression; leq_t; block; global_funs } in
let p, _ = Mapfold.program_it funs empty p in
p
Loading

0 comments on commit 09d1947

Please sign in to comment.