Newer
Older
(** Time-stamp: <modified the 12/03/2009 (at 10:23) by Erwan Jahier> *)
open Lxm
open Eff
(********************************************************************************)
(* stuff to create fresh var names. *)
let new_var str node_env type_eff clock_eff =
let id = Ident.of_string (Name.new_local_var str) in
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
let var =
{
var_name_eff = id;
var_nature_eff = SyntaxTreeCore.VarLocal;
var_number_eff = -1; (* this field is used only for i/o.
Should i rather put something sensible there ? *)
var_type_eff = type_eff;
var_clock_eff = clock_eff;
}
in
Hashtbl.add node_env.lenv_vars id var;
var
(********************************************************************************)
(* A small util function followed by a quick unit test. *)
let rec fill i size = if i >= size then [] else i::(fill (i+1) size)
let _ = assert (fill 0 5 = [0;1;2;3;4])
let (elt_type_of_array : Eff.type_ list -> Eff.type_) =
function
| [Array_type_eff(t, _)] -> t
| _ -> assert false (* it ougth to be an array... *)
let rec (list_map3:
('a -> 'b -> 'c -> 'd) -> 'a list -> 'b list -> 'c list -> 'd list) =
fun f l1 l2 l3 ->
match (l1, l2, l3) with
| ([], [], []) -> []
| (e1::t1, e2::t2, e3::t3) -> (f e1 e2 e3)::(list_map3 f t1 t2 t3)
| _ -> (* should not occur *)
print_string "*** list_map3 called with lists of different size.\n";
flush stdout;
assert false
let (check_clock_and_type :
Eff.id_solver -> Lxm.t -> val_exp -> Eff.type_ -> Eff.id_clock -> unit) =
fun id_solver lxm rhs exp_type (_,exp_clock) ->
(* Let's be paranoiac and check types and clocks of the expression
this function generates.
Moreover, this fills some tables that may be used by
the call to Split.eq below....*)
let rhs, rhs_tl = EvalType.f id_solver rhs in
if (rhs_tl <> [exp_type]) then assert false;
try ignore(EvalClock.f lxm id_solver UnifyClock.empty_subst rhs [exp_clock])
with _ -> assert false
(********************************************************************************)
(* The functions below accumulate
(1) the new equations
(2) the fresh variables.
*)
type inline_acc = (Eff.eq_info srcflagged) list * Eff.var_info list
let rec (inline_eq: Eff.local_env ->
Eff.id_solver -> inline_acc -> Eff.eq_info srcflagged -> inline_acc) =
fun node_env id_solver (eqs, locs) eq ->
let { src = lxm_eq ; it = (lhs, rhs) } = eq in
match rhs.core with
| CallByPosEff(
{src=lxm_ve;it=CALL ({it = {node_key_eff = (("Lustre", "map"),sargs)}})},
OperEff args)
| CallByPosEff({src=lxm_ve;it=Eff.Predef(Predef.Map, sargs)}, OperEff args)
->
(* Given
- a node n of type: tau_1 * ... * tau_n -> teta_1 * ... * teta_l
- and an integer c
The profile of map<<node,c>> is:
tau_1^c * ... * tau_n^c -> teta_1^c * ... * teta_l^c
and
Y1, ... ,Yl = map<<node; c>>(X1,...,Xk)
<=>
for all i = 0, ..., c-1; (Y1[i], ... ,Yl[i]) = N(X_1[i], ... ,X_k[i])
*)
Erwan Jahier
committed
let ((node,inlist,outlist),c) = match sargs with
| [ConstStaticArgEff(_,Int_const_eff(c)) ; NodeStaticArgEff(_,node)]
| [NodeStaticArgEff(_,node) ; ConstStaticArgEff(_,Int_const_eff(c))] ->
node, c
| _ -> assert false (* todo: issue an error *)
in
Erwan Jahier
committed
let node = id_solver.id2node (Ident.idref_of_long node) [] lxm_ve in
let node = flagit node lxm_ve in
let index_list = fill 0 c in
List.fold_left
(fun (eqs,locs) i ->
let lhs = List.map
(fun lp ->
let t_elt = elt_type_of_array [type_of_left lp] in
LeftArrayEff(lp, i, t_elt))
lhs
in
let args =
List.map
(fun arg ->
let targ = arg.typ in
let t_elt = elt_type_of_array targ in
let op_flg = { src = lxm_ve ; it = ARRAY_ACCES(i) } in
let narg = {
core = CallByPosEff(op_flg, OperEff [arg]);
typ = [t_elt]
}
in
Erwan Jahier
committed
EvalClock.copy narg arg;
narg
)
let nrhs = { rhs with core =
CallByPosEff({ src = lxm_ve ; it = (CALL node)}, OperEff args) }
Erwan Jahier
committed
let eq = { src = lxm_eq ; it = (lhs, nrhs) } in
EvalClock.copy nrhs rhs;
(eq::eqs,locs)
)
(eqs,locs)
index_list
| CallByPosEff(
{src=lxm_ve;it=CALL ({it = {node_key_eff = (("Lustre", "red"),sargs)}})},
OperEff args)
| CallByPosEff(
{src=lxm_ve;it=CALL ({it = {node_key_eff = (("Lustre", "fill"),sargs)}})},
OperEff args)
| CallByPosEff(
{src=lxm_ve;it=CALL ({it = {node_key_eff = (("Lustre", "fillred"),sargs)}})},
OperEff args)
| CallByPosEff({src=lxm_ve;it=Eff.Predef(Predef.Fill, sargs)}, OperEff args)
| CallByPosEff({src=lxm_ve;it=Eff.Predef(Predef.Red, sargs)}, OperEff args)
| CallByPosEff({src=lxm_ve;it=Eff.Predef(Predef.FillRed,sargs)}, OperEff args)
->
(* Given
- a node n of type
tau * tau_1 * ... * tau_n -> tau * teta_1 * ... * teta_l
- a integer c
the fillred expression has the profile:
tau * tau_1^c * ... * tau_n^c -> tau * teta_1^c * ... * teta_l^c
acc_out, Y1, ... ,Yl = fillred<<node; c>>(acc_in,X1,...,Xk)
<=>
exists acc_0, ..., acc_c-1, where acc_o=acc_in, and acc_c-1=acc_out
such that, for all i = 0, ..., c-1;
(acc_i+1, Y1[i], ... ,Yl[i]) = N(acc_i,X_1[i], ... ,X_k[i])
*)
Erwan Jahier
committed
let ((node,_,_),c) = match sargs with
| [ConstStaticArgEff(_,Int_const_eff(c)) ; NodeStaticArgEff(_,node)]
| [NodeStaticArgEff(_,node) ; ConstStaticArgEff(_,Int_const_eff(c))] ->
node, c
| _ -> assert false (* todo: issue an error *)
in
Erwan Jahier
committed
let node = id_solver.id2node (Ident.idref_of_long node) [] lxm_ve in
let node = flagit node lxm_ve in
let index_list = fill 0 c in
(* Retreive acc_in and acc_out *)
let acc_out = List.hd lhs in
let lhs = List.tl lhs in
let acc_in = List.hd args in
let args = List.tl args in
List.hd (acc_in.typ),
Erwan Jahier
committed
List.hd (EvalClock.lookup acc_in)
let rec f i acc =
f (i-1) ((new_var "acc" node_env type_exp clock_exp)::acc)
in
(* coquetry: reverse the list to have the name in a nice order *)
List.rev(f (c-1) [])
in
let (acc_left_list : left list) =
(List.map (fun vi -> LeftVarEff(vi,lxm_ve)) acc_vars)@[acc_out]
in
let (acc_rigth_list : val_exp list) =
acc_in::(
let id = Ident.to_idref vi.var_name_eff in
let op_flg = { src = lxm_ve ; it = IDENT id } in
let ve = {
typ = [vi.var_type_eff];
core = CallByPosEff(op_flg, OperEff []) }
in
Erwan Jahier
committed
EvalClock.add ve [vi.var_clock_eff];
ve
)
acc_vars)
in
let neqs =
list_map3
(fun i acc_left acc_rigth ->
let args =
List.map
(fun arg ->
let t_elt = elt_type_of_array arg.typ in
let op_flg = {src = lxm_ve ; it = ARRAY_ACCES(i)} in
let new_arg =
{ core = CallByPosEff(op_flg, OperEff [arg]); typ=[t_elt] }
in
Erwan Jahier
committed
EvalClock.add new_arg [clock_exp];
new_arg
)
args
in
let args = acc_rigth::args in
let lhs =
List.map
(fun lp ->
let t_elt = elt_type_of_array [type_of_left lp] in
LeftArrayEff(lp,i,t_elt))
lhs
in
let lhs = acc_left::lhs in
Erwan Jahier
committed
let tl = List.map Eff.type_of_left lhs in
let cl = List.map
(fun l -> (Eff.var_info_of_left l).var_clock_eff) lhs
in
let rhs = {
typ = tl;
core = CallByPosEff({src=lxm_ve;it = (CALL node)}, OperEff args) }
Erwan Jahier
committed
let eq =
EvalClock.add rhs cl;
{ src = lxm_eq ; it = (lhs, rhs) }
in
eq
)
index_list
acc_left_list
acc_rigth_list
in
(List.rev_append neqs eqs, List.append acc_vars locs)
| CallByPosEff(
{src=lxm_ve;it=CALL ({it = {node_key_eff = (("Lustre", "diese"),_)}})},
OperEff args)
| CallByPosEff({src=lxm_ve;it=Eff.Predef(Predef.DIESE_n,_)}, OperEff args) ->
(* a diese is a particular kind of boolred:
#(A,...,an) = boolred(1,1,n)([a1,...,an])
*)
Erwan Jahier
committed
let clk = EvalClock.lookup rhs in
let n = List.length args in
let sargs = [ConstStaticArgEff(Ident.of_string "i",Int_const_eff 1);
ConstStaticArgEff(Ident.of_string "j",Int_const_eff 1);
ConstStaticArgEff(Ident.of_string "k",Int_const_eff n)
]
in
let boolred_op = Eff.Predef(Predef.BoolRed,sargs) in
let arg = {
typ = [Array_type_eff(Bool_type_eff,n) ];
core = CallByPosEff({src=lxm_ve;it= ARRAY args}, OperEff [])} in
let rhs = {
typ = [Bool_type_eff];
core = CallByPosEff({src=lxm_ve;it=boolred_op}, OperEff [arg]) }
in
let eq = { src = lxm_eq ; it = (lhs, rhs) } in
Erwan Jahier
committed
EvalClock.add arg clk;
EvalClock.add rhs clk;
inline_eq node_env id_solver (eqs, locs) eq
| CallByPosEff(
{src=lxm_ve;it=CALL ({it = {node_key_eff = (("Lustre", "nor"),_)}})},
OperEff args)
| CallByPosEff({src=lxm_ve;it=Eff.Predef(Predef.NOR_n,_)}, OperEff args) ->
(* a nor is a particular kind of boolred too:
#(A,...,an) = boolred(0,0,n)([a1,...,an])
*)
Erwan Jahier
committed
let clk = EvalClock.lookup rhs in
let n = List.length args in
let sargs = [ConstStaticArgEff(Ident.of_string "i",Int_const_eff 0);
ConstStaticArgEff(Ident.of_string "j",Int_const_eff 0);
ConstStaticArgEff(Ident.of_string "k",Int_const_eff n)
]
in
let boolred_op = Eff.Predef(Predef.BoolRed,sargs) in
let arg = {
typ = [Array_type_eff(Bool_type_eff,n) ];
core = CallByPosEff({src=lxm_ve;it=ARRAY args}, OperEff []) }
in
let rhs = {
typ = [Bool_type_eff];
core = CallByPosEff({src=lxm_ve;it=boolred_op}, OperEff [arg]) }
in
Erwan Jahier
committed
let eq = { src = lxm_eq ; it = (lhs, rhs) } in
EvalClock.add arg clk;
EvalClock.add rhs clk;
inline_eq node_env id_solver (eqs, locs) eq
| CallByPosEff({src=lxm_ve;it=CALL (
{it = {node_key_eff = (("Lustre", "boolred"),sargs)}})},
OperEff args)
| CallByPosEff({src=lxm_ve;it=Eff.Predef(Predef.BoolRed,sargs)}, OperEff args) ->
(* Given
- 3 integers i, j, k
boolref<<i,j,k>> has the profile: bool^n -> bool
and
res = boolred<<i,j,k>>(A);
<=>
cpt = (if A[0] then 1 else 0) + ... + (if A[k-1] then 1 else 0);
res = i <= cpt && cpt <= j;
*)
Erwan Jahier
committed
let rhs_clk = EvalClock.lookup rhs in
let (i,j,k) =
match sargs with
| [ConstStaticArgEff(_,Int_const_eff i);
ConstStaticArgEff(_,Int_const_eff j);
ConstStaticArgEff(_,Int_const_eff k)
] ->
(i,j,k)
| _ -> assert false
in
let index_list = fill 0 k in
let lp = try List.hd lhs with Not_found -> assert false in
let res_clock = (Eff.var_info_of_left lp).var_clock_eff in
let cpt = new_var "cpt" node_env Int_type_eff res_clock in
let id_of_int i = Predef.ICONST_n(Ident.of_string (string_of_int i)) in
let rhs = (* i <= cpt && cpt <= j; *)
let i_op = { it = Predef(id_of_int i,[]) ; src = lxm_ve }
and j_op = { it = Predef(id_of_int j,[]) ; src = lxm_ve }
and cpt_op = { it = IDENT (Ident.to_idref cpt.var_name_eff);src=lxm_ve }
and and_op = { it = Predef(Predef.AND_n,[]) ; src = lxm_ve }
and inf_op = { it = Predef(Predef.LTE_n,[]) ; src = lxm_ve } in
let i_eff = { typ = [Int_type_eff]; core = CallByPosEff(i_op, OperEff []) }
and j_eff = { typ = [Int_type_eff]; core = CallByPosEff(j_op, OperEff [])}
and cpt_eff = { typ = [Int_type_eff]; core = CallByPosEff(cpt_op, OperEff []) }
in
let i_inf_cpt = { typ = [Bool_type_eff];
core = CallByPosEff(inf_op,OperEff[i_eff;cpt_eff]) }
and cpt_if_j = { typ = [Bool_type_eff];
core = CallByPosEff(inf_op,OperEff[cpt_eff;j_eff]) }
in
Erwan Jahier
committed
EvalClock.add i_inf_cpt rhs_clk;
EvalClock.add cpt_if_j rhs_clk;
{ typ = [Bool_type_eff];
core = CallByPosEff(and_op, OperEff [i_inf_cpt; cpt_if_j]) }
in
let eq =
Erwan Jahier
committed
EvalClock.add rhs rhs_clk;
check_clock_and_type id_solver lxm_eq rhs Bool_type_eff res_clock;
{ src = lxm_eq ; it = (lhs, rhs) }
in
let eq_cpt =
let lhs = [LeftVarEff(cpt,lxm_ve)] in
(* (if A[0] then 1 else 0) + ... + (if A[k-1] then 1 else 0) *)
let zero = {
typ = [Int_type_eff];
core = CallByPosEff({it=Predef(id_of_int 0,[]);src=lxm_ve},OperEff[])}
and one = {
typ = [Int_type_eff];
core = CallByPosEff({it=Predef(id_of_int 1,[]);src=lxm_ve},OperEff[]) }
and plus_op = { it = Predef(Predef.IPLUS_n,[]) ; src = lxm_ve }
and ite_op = { it = Predef(Predef.IF_n,[]) ; src = lxm_ve }
in
let array, type_elt =
Erwan Jahier
committed
EvalClock.add zero rhs_clk;
EvalClock.add one rhs_clk;
match args with
| [arg] -> arg,elt_type_of_array arg.typ
| _ -> assert false
in
let make_ite i = (* returns '(if A[i] then 1 else 0)' *)
let a_op = { it = ARRAY_ACCES(i) ; src = lxm_ve } in
let a_i = { typ = [type_elt];
core = CallByPosEff(a_op, OperEff [array]) }
in
let nve = {
typ = [Int_type_eff];
core = CallByPosEff(ite_op, OperEff [a_i;one;zero]) }
in
Erwan Jahier
committed
EvalClock.add a_i rhs_clk;
EvalClock.add nve rhs_clk;
nve
in
let rhs =
List.fold_left
Erwan Jahier
committed
(fun acc i ->
let nve = {
typ = [Int_type_eff];
core = CallByPosEff(plus_op, OperEff [acc; make_ite i]) }
in
Erwan Jahier
committed
EvalClock.add nve rhs_clk;
nve
)
(make_ite (List.hd index_list))
(List.tl index_list)
in
check_clock_and_type id_solver lxm_eq rhs Int_type_eff res_clock;
{ src = lxm_eq ; it = (lhs, rhs) }
in
if !Global.one_op_per_equation then
let eqs_res, vars_res = Split.eq node_env eq in
let eqs_cpt, vars_cpt = Split.eq node_env eq_cpt in
let eqs = List.rev_append (eqs_res@eqs_cpt) eqs
and locs = cpt::(List.append vars_res (List.append vars_cpt locs))
in
(eqs, locs)
else
(eq::eq_cpt::eqs, cpt::locs)
(* All the other operators *)
| _ ->
(eq::eqs, locs)
(* exported *)
and (iterators : Eff.local_env -> Eff.id_solver -> Eff.node_exp -> Eff.node_exp) =
fun node_env id_solver n ->
match n.def_eff with
| ExternEff
| AbstractEff None -> n
| AbstractEff (Some pn) ->
{ n with def_eff = AbstractEff (Some (iterators node_env id_solver pn)) }
| BodyEff b ->
Name.reset_local_var_prefix "acc";
Name.reset_local_var_prefix "cpt";
let nv = match n.loclist_eff with None -> [] | Some l -> l in
let (neqs, nv) =
List.fold_left (inline_eq node_env id_solver) ([], nv) b.eqs_eff