Newer
Older
(** 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 =
let id = Ident.of_string (str ^ (string_of_int !var_cpt)) in
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
46
47
48
49
50
51
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
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
(********************************************************************************)
(* 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)
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
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)
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
| 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 *)
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
| _ ->
(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