(** Time-stamp: <modified the 13/05/2009 (at 16:35) 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
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 = id, 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])
*)
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
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];
clk = arg.clk
}
in
narg
)
args
in
let nrhs = { rhs with core =
CallByPosEff({ src = lxm_ve ; it = (CALL node)}, OperEff args) }
in
let eq = { src = lxm_eq ; it = (lhs, nrhs) } in
(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])
*)
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
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
let type_exp,clock_exp =
List.hd (acc_in.typ),
List.hd (acc_in.clk)
in
let (acc_vars : var_info list) =
let rec f i acc =
if i = 0 then acc else
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::(
List.map
(fun vi ->
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];
clk = [snd vi.var_clock_eff];
core = CallByPosEff(op_flg, OperEff []) }
in
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];
clk=[clock_exp];
}
in
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
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;
clk = List.map snd cl;
core = CallByPosEff({src=lxm_ve;it = (CALL node)}, OperEff args) }
in
let eq = { 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])
*)
let clk = rhs.clk 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) ];
clk = clk;
core = CallByPosEff({src=lxm_ve;it= ARRAY args}, OperEff [])} in
let rhs = {
typ = [Bool_type_eff];
clk = clk;
core = CallByPosEff({src=lxm_ve;it=boolred_op}, OperEff [arg]) }
in
let eq = { src = lxm_eq ; it = (lhs, rhs) } in
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])
*)
let clk = rhs.clk 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) ];
clk = clk;
core = CallByPosEff({src=lxm_ve;it=ARRAY args}, OperEff []) }
in
let rhs = {
typ = [Bool_type_eff];
clk = clk;
core = CallByPosEff({src=lxm_ve;it=boolred_op}, OperEff [arg]) }
in
let eq = { src = lxm_eq ; it = (lhs, rhs) } in
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;
*)
let rhs_clk = rhs.clk 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 (snd 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 = { clk=rhs_clk; typ = [Int_type_eff]; core = CallByPosEff(i_op, OperEff []) }
and j_eff = { clk=rhs_clk; typ = [Int_type_eff]; core = CallByPosEff(j_op, OperEff [])}
and cpt_eff = { clk=rhs_clk; typ = [Int_type_eff]; core = CallByPosEff(cpt_op, OperEff []) }
in
let i_inf_cpt = { clk=rhs_clk; typ = [Bool_type_eff];
core = CallByPosEff(inf_op,OperEff[i_eff;cpt_eff]) }
and cpt_if_j = { clk=rhs_clk; typ = [Bool_type_eff];
core = CallByPosEff(inf_op,OperEff[cpt_eff;j_eff]) }
in
{ clk=rhs_clk; typ = [Bool_type_eff];
core = CallByPosEff(and_op, OperEff [i_inf_cpt; cpt_if_j]) }
in
let eq =
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 = {
clk = rhs_clk; typ = [Int_type_eff];
core = CallByPosEff({it=Predef(id_of_int 0,[]);src=lxm_ve},OperEff[])}
and one = {
clk = rhs_clk;
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 =
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 = { clk = rhs_clk; typ = [type_elt];
core = CallByPosEff(a_op, OperEff [array]) }
in
let nve = {
clk=rhs_clk; typ = [Int_type_eff];
core = CallByPosEff(ite_op, OperEff [a_i;one;zero]) }
in
nve
in
let rhs =
List.fold_left
(fun acc i ->
let nve = {
clk=rhs_clk; typ = [Int_type_eff];
core = CallByPosEff(plus_op, OperEff [acc; make_ite i]) }
in
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
in
let nb = { b with eqs_eff = List.rev neqs } in
let res =
{ n with
loclist_eff = Some nv;
def_eff = BodyEff nb
}
in
res