-
Erwan Jahier authoredErwan Jahier authored
inline.ml 13.02 KiB
(** Time-stamp: <modified the 21/11/2008 (at 17:16) by Erwan Jahier> *)
open Lxm
open Eff
(********************************************************************************)
(* stuff to create fresh var names. *)
let var_cpt = ref 0
let new_var str node_env type_eff clock_eff =
incr var_cpt;
let id = Ident.of_string (str ^ (string_of_int !var_cpt)) 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 = clock_eff;
}
in
Hashtbl.add node_env.lenv_vars id var;
var
let init_var () =
var_cpt := 0
(********************************************************************************)
(* 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....*)
if (EvalType.f id_solver rhs <> [exp_type]) then assert false;
try
let (clock, subst) =
EvalClock.f id_solver UnifyClock.empty_subst rhs
in
ignore(UnifyClock.f lxm subst (List.hd clock) 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 with
| 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,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 = { it = node ; src = 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 t_elt = elt_type_of_array (EvalType.f id_solver arg) in
let op_flg = { src = lxm_ve ; it = ARRAY_ACCES(i,t_elt) } in
CallByPosEff(op_flg, OperEff [arg]))
args
in
let rhs =
CallByPosEff({ src = lxm_ve ; it = (CALL node)}, OperEff args)
in
let eq = { src = lxm_eq ; it = (lhs, rhs) } in
(eq::eqs,locs)
)
(eqs,locs)
index_list
| 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 = { it = node ; src = 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 (EvalType.f id_solver acc_in),
(ignore (EvalClock.f id_solver UnifyClock.empty_subst acc_in);
List.hd (EvalClock.get_val_exp_eff acc_in))
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
CallByPosEff(op_flg, OperEff []))
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 (EvalType.f id_solver arg) in
let op_flg = {src = lxm_ve ; it = ARRAY_ACCES(i,t_elt)} in
CallByPosEff(op_flg, OperEff [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 rhs =
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=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 (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 = CallByPosEff(i_op, OperEff [])
and j_eff = CallByPosEff(j_op, OperEff [])
and cpt_eff = CallByPosEff(cpt_op, OperEff []) in
let i_inf_cpt = CallByPosEff(inf_op,OperEff[i_eff;cpt_eff])
and cpt_if_j = CallByPosEff(inf_op,OperEff[cpt_eff;j_eff])in
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 = CallByPosEff({it=Predef(id_of_int 0,[]);src=lxm_ve},OperEff[])
and one = 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 (EvalType.f id_solver arg)
| _ -> assert false
in
let make_ite i = (* returns '(if A[i] then 1 else 0)' *)
let a_op = { it = ARRAY_ACCES(i,type_elt) ; src = lxm_ve } in
let a_i = CallByPosEff(a_op, OperEff [array]) in
CallByPosEff(ite_op, OperEff [a_i;one;zero])
in
let rhs =
List.fold_left
(fun acc i -> CallByPosEff(plus_op, OperEff [acc; make_ite i]))
(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 *)
let (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 -> n
| BodyEff b ->
init_var ();
let loc = match n.loclist_eff with None -> [] | Some l -> l in
let (neqs, nv) =
List.fold_left (inline_eq node_env id_solver) ([], loc) 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