lustrec / src / dimension.ml @ 8f1c7e91
History | View | Annotate | Download (11.5 KB)
1 |
(* ---------------------------------------------------------------------------- |
---|---|
2 |
* SchedMCore - A MultiCore Scheduling Framework |
3 |
* Copyright (C) 2009-2013, ONERA, Toulouse, FRANCE - LIFL, Lille, FRANCE |
4 |
* Copyright (C) 2012-2013, INPT, Toulouse, FRANCE |
5 |
* |
6 |
* This file is part of Prelude |
7 |
* |
8 |
* Prelude is free software; you can redistribute it and/or |
9 |
* modify it under the terms of the GNU Lesser General Public License |
10 |
* as published by the Free Software Foundation ; either version 2 of |
11 |
* the License, or (at your option) any later version. |
12 |
* |
13 |
* Prelude is distributed in the hope that it will be useful, but |
14 |
* WITHOUT ANY WARRANTY ; without even the implied warranty of |
15 |
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU |
16 |
* Lesser General Public License for more details. |
17 |
* |
18 |
* You should have received a copy of the GNU Lesser General Public |
19 |
* License along with this program ; if not, write to the Free Software |
20 |
* Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 |
21 |
* USA |
22 |
*---------------------------------------------------------------------------- *) |
23 |
|
24 |
(* This module is used for the lustre to C compiler *) |
25 |
|
26 |
open Format |
27 |
|
28 |
type dim_expr = |
29 |
{mutable dim_desc: dim_desc; |
30 |
dim_loc: Location.t; |
31 |
dim_id: int} |
32 |
|
33 |
and dim_desc = |
34 |
| Dbool of bool |
35 |
| Dint of int |
36 |
| Dident of Utils.ident |
37 |
| Dappl of Utils.ident * dim_expr list |
38 |
| Dite of dim_expr * dim_expr * dim_expr |
39 |
| Dlink of dim_expr |
40 |
| Dvar |
41 |
| Dunivar |
42 |
|
43 |
exception Unify of dim_expr * dim_expr |
44 |
exception InvalidDimension |
45 |
|
46 |
let new_id = ref (-1) |
47 |
|
48 |
let mkdim loc dim = |
49 |
incr new_id; |
50 |
{ dim_loc = loc; |
51 |
dim_id = !new_id; |
52 |
dim_desc = dim;} |
53 |
|
54 |
let mkdim_var () = |
55 |
incr new_id; |
56 |
{ dim_loc = Location.dummy_loc; |
57 |
dim_id = !new_id; |
58 |
dim_desc = Dvar;} |
59 |
|
60 |
let mkdim_ident loc id = |
61 |
incr new_id; |
62 |
{ dim_loc = loc; |
63 |
dim_id = !new_id; |
64 |
dim_desc = Dident id;} |
65 |
|
66 |
let mkdim_bool loc b = |
67 |
incr new_id; |
68 |
{ dim_loc = loc; |
69 |
dim_id = !new_id; |
70 |
dim_desc = Dbool b;} |
71 |
|
72 |
let mkdim_int loc i = |
73 |
incr new_id; |
74 |
{ dim_loc = loc; |
75 |
dim_id = !new_id; |
76 |
dim_desc = Dint i;} |
77 |
|
78 |
let mkdim_appl loc f args = |
79 |
incr new_id; |
80 |
{ dim_loc = loc; |
81 |
dim_id = !new_id; |
82 |
dim_desc = Dappl (f, args);} |
83 |
|
84 |
let mkdim_ite loc i t e = |
85 |
incr new_id; |
86 |
{ dim_loc = loc; |
87 |
dim_id = !new_id; |
88 |
dim_desc = Dite (i, t, e);} |
89 |
|
90 |
let rec pp_dimension fmt dim = |
91 |
(*fprintf fmt "<%d>" (Obj.magic dim: int);*) |
92 |
match dim.dim_desc with |
93 |
| Dident id -> |
94 |
fprintf fmt "%s" id |
95 |
| Dint i -> |
96 |
fprintf fmt "%d" i |
97 |
| Dbool b -> |
98 |
fprintf fmt "%B" b |
99 |
| Dite (i, t, e) -> |
100 |
fprintf fmt "if %a then %a else %a" |
101 |
pp_dimension i pp_dimension t pp_dimension e |
102 |
| Dappl (f, [arg]) -> |
103 |
fprintf fmt "(%s%a)" f pp_dimension arg |
104 |
| Dappl (f, [arg1; arg2]) -> |
105 |
fprintf fmt "(%a%s%a)" pp_dimension arg1 f pp_dimension arg2 |
106 |
| Dappl (_, _) -> assert false |
107 |
| Dlink dim' -> fprintf fmt "%a" pp_dimension dim' |
108 |
| Dvar -> fprintf fmt "_%s" (Utils.name_of_dimension dim.dim_id) |
109 |
| Dunivar -> fprintf fmt "'%s" (Utils.name_of_dimension dim.dim_id) |
110 |
|
111 |
let rec multi_dimension_product loc dim_list = |
112 |
match dim_list with |
113 |
| [] -> mkdim_int loc 1 |
114 |
| [d] -> d |
115 |
| d::q -> mkdim_appl loc "*" [d; multi_dimension_product loc q] |
116 |
|
117 |
(* Builds a dimension expr representing 0<=d *) |
118 |
let check_bound loc d = |
119 |
mkdim_appl loc "<=" [mkdim_int loc 0; d] |
120 |
|
121 |
(* Builds a dimension expr representing 0<=i<d *) |
122 |
let check_access loc d i = |
123 |
mkdim_appl loc "&&" |
124 |
[mkdim_appl loc "<=" [mkdim_int loc 0; i]; |
125 |
mkdim_appl loc "<" [i; d]] |
126 |
|
127 |
let rec repr dim = |
128 |
match dim.dim_desc with |
129 |
| Dlink dim' -> repr dim' |
130 |
| _ -> dim |
131 |
|
132 |
let rec is_eq_dimension d1 d2 = |
133 |
let d1 = repr d1 in |
134 |
let d2 = repr d2 in |
135 |
d1.dim_id = d2.dim_id || |
136 |
match d1.dim_desc, d2.dim_desc with |
137 |
| Dappl (f1, args1), Dappl (f2, args2) -> |
138 |
f1 = f2 && List.length args1 = List.length args2 && List.for_all2 is_eq_dimension args1 args2 |
139 |
| Dite (c1, t1, e1), Dite (c2, t2, e2) -> |
140 |
is_eq_dimension c1 c2 && is_eq_dimension t1 t2 && is_eq_dimension e1 e2 |
141 |
| Dvar, _ |
142 |
| _, Dvar |
143 |
| Dunivar, _ |
144 |
| _, Dunivar -> false |
145 |
| _ -> d1 = d2 |
146 |
|
147 |
let is_dimension_const dim = |
148 |
match (repr dim).dim_desc with |
149 |
| Dint _ |
150 |
| Dbool _ -> true |
151 |
| _ -> false |
152 |
|
153 |
let size_const_dimension dim = |
154 |
match (repr dim).dim_desc with |
155 |
| Dint i -> i |
156 |
| Dbool b -> if b then 1 else 0 |
157 |
| _ -> (Format.eprintf "internal error: size_const_dimension %a@." pp_dimension dim; assert false) |
158 |
|
159 |
let rec is_polymorphic dim = |
160 |
match dim.dim_desc with |
161 |
| Dident _ |
162 |
| Dint _ |
163 |
| Dbool _ |
164 |
| Dvar -> false |
165 |
| Dite (i, t, e) -> |
166 |
is_polymorphic i || is_polymorphic t || is_polymorphic e |
167 |
| Dappl (_, args) -> List.exists is_polymorphic args |
168 |
| Dlink dim' -> is_polymorphic dim' |
169 |
| Dunivar -> true |
170 |
|
171 |
(* Normalizes a dimension expression, i.e. canonicalize all polynomial |
172 |
sub-expressions, where unsupported operations (eg. '/') are treated |
173 |
as variables. |
174 |
*) |
175 |
|
176 |
let rec factors dim = |
177 |
match dim.dim_desc with |
178 |
| Dappl (f, args) when f = "*" -> List.flatten (List.map factors args) |
179 |
| _ -> [dim] |
180 |
|
181 |
let rec factors_constant fs = |
182 |
match fs with |
183 |
| [] -> 1 |
184 |
| f::q -> |
185 |
match f.dim_desc with |
186 |
| Dint i -> i * (factors_constant q) |
187 |
| _ -> factors_constant q |
188 |
|
189 |
let norm_factors fs = |
190 |
let k = factors_constant fs in |
191 |
let nk = List.filter (fun d -> not (is_dimension_const d)) fs in |
192 |
(k, List.sort Pervasives.compare nk) |
193 |
|
194 |
let rec terms dim = |
195 |
match dim.dim_desc with |
196 |
| Dappl (f, args) when f = "+" -> List.flatten (List.map terms args) |
197 |
| _ -> [dim] |
198 |
|
199 |
let rec normalize dim = |
200 |
dim |
201 |
(* |
202 |
let rec unnormalize loc l = |
203 |
let l = List.sort (fun (k, l) (k', l') -> compare l l') (List.map (fun (k, l) -> (k, List.sort compare l)) l) in |
204 |
match l with |
205 |
| [] -> mkdim_int loc 0 |
206 |
| t::q -> |
207 |
List.fold_left (fun res (k, l) -> mkdim_appl loc "+" res (mkdim_appl loc "*" (mkdim_int loc k) l)) t q |
208 |
*) |
209 |
let copy copy_dim_vars dim = |
210 |
let rec cp dim = |
211 |
match dim.dim_desc with |
212 |
| Dbool _ |
213 |
| Dint _ -> dim |
214 |
| Dident id -> mkdim_ident dim.dim_loc id |
215 |
| Dite (c, t, e) -> mkdim_ite dim.dim_loc (cp c) (cp t) (cp e) |
216 |
| Dappl (id, args) -> mkdim_appl dim.dim_loc id (List.map cp args) |
217 |
| Dlink dim' -> cp dim' |
218 |
| Dunivar -> assert false |
219 |
| Dvar -> |
220 |
try |
221 |
List.assoc dim.dim_id !copy_dim_vars |
222 |
with Not_found -> |
223 |
let var = mkdim dim.dim_loc Dvar in |
224 |
copy_dim_vars := (dim.dim_id, var)::!copy_dim_vars; |
225 |
var |
226 |
in cp dim |
227 |
|
228 |
(* Partially evaluates a 'simple' dimension expr [dim], i.e. an expr containing only int and bool |
229 |
constructs, with conditionals. [eval_const] is a typing environment for static values. [eval_op] is an evaluation env for basic operators. The argument [dim] is modified in-place. |
230 |
*) |
231 |
let rec eval eval_op eval_const dim = |
232 |
match dim.dim_desc with |
233 |
| Dbool _ |
234 |
| Dint _ -> () |
235 |
| Dident id -> |
236 |
(match eval_const id with |
237 |
| Some val_dim -> dim.dim_desc <- Dlink val_dim |
238 |
| None -> raise InvalidDimension) |
239 |
| Dite (c, t, e) -> |
240 |
begin |
241 |
eval eval_op eval_const c; |
242 |
eval eval_op eval_const t; |
243 |
eval eval_op eval_const e; |
244 |
match (repr c).dim_desc with |
245 |
| Dbool b -> dim.dim_desc <- Dlink (if b then t else e) |
246 |
| _ -> () |
247 |
end |
248 |
| Dappl (id, args) -> |
249 |
begin |
250 |
List.iter (eval eval_op eval_const) args; |
251 |
if List.for_all is_dimension_const args |
252 |
then dim.dim_desc <- Env.lookup_value eval_op id (List.map (fun d -> (repr d).dim_desc) args) |
253 |
end |
254 |
| Dlink dim' -> |
255 |
begin |
256 |
eval eval_op eval_const dim'; |
257 |
dim.dim_desc <- Dlink (repr dim') |
258 |
end |
259 |
| Dvar -> () |
260 |
| Dunivar -> assert false |
261 |
|
262 |
let uneval const univar = |
263 |
let univar = repr univar in |
264 |
match univar.dim_desc with |
265 |
| Dunivar -> univar.dim_desc <- Dident const |
266 |
| _ -> assert false |
267 |
|
268 |
(** [occurs dvar dim] returns true if the dimension variable [dvar] occurs in |
269 |
dimension expression [dim]. False otherwise. *) |
270 |
let rec occurs dvar dim = |
271 |
let dim = repr dim in |
272 |
match dim.dim_desc with |
273 |
| Dvar -> dim.dim_id = dvar.dim_id |
274 |
| Dident _ |
275 |
| Dint _ |
276 |
| Dbool _ |
277 |
| Dunivar -> false |
278 |
| Dite (i, t, e) -> |
279 |
occurs dvar i || occurs dvar t || occurs dvar e |
280 |
| Dappl (_, args) -> List.exists (occurs dvar) args |
281 |
| Dlink _ -> assert false |
282 |
|
283 |
(* Promote monomorphic dimension variables to polymorphic variables. |
284 |
Generalize by side-effects *) |
285 |
let rec generalize dim = |
286 |
match dim.dim_desc with |
287 |
| Dvar -> dim.dim_desc <- Dunivar |
288 |
| Dident _ |
289 |
| Dint _ |
290 |
| Dbool _ |
291 |
| Dunivar -> () |
292 |
| Dite (i, t, e) -> |
293 |
generalize i; generalize t; generalize e |
294 |
| Dappl (_, args) -> List.iter generalize args |
295 |
| Dlink dim' -> generalize dim' |
296 |
|
297 |
(* Instantiate polymorphic dimension variables to monomorphic variables. |
298 |
Also duplicates the whole term structure (but the constant sub-terms). |
299 |
*) |
300 |
let rec instantiate inst_dim_vars dim = |
301 |
let dim = repr dim in |
302 |
match dim.dim_desc with |
303 |
| Dvar _ |
304 |
| Dident _ |
305 |
| Dint _ |
306 |
| Dbool _ -> dim |
307 |
| Dite (i, t, e) -> |
308 |
mkdim_ite dim.dim_loc |
309 |
(instantiate inst_dim_vars i) |
310 |
(instantiate inst_dim_vars t) |
311 |
(instantiate inst_dim_vars e) |
312 |
| Dappl (f, args) -> mkdim_appl dim.dim_loc f (List.map (instantiate inst_dim_vars) args) |
313 |
| Dlink dim' -> assert false (*mkdim dim.dim_loc (Dlink (instantiate inst_dim_vars dim'))*) |
314 |
| Dunivar -> |
315 |
try |
316 |
List.assoc dim.dim_id !inst_dim_vars |
317 |
with Not_found -> |
318 |
let var = mkdim dim.dim_loc Dvar in |
319 |
inst_dim_vars := (dim.dim_id, var)::!inst_dim_vars; |
320 |
var |
321 |
|
322 |
let rec unify dim1 dim2 = |
323 |
let dim1 = repr dim1 in |
324 |
let dim2 = repr dim2 in |
325 |
if dim1.dim_id = dim2.dim_id then () else |
326 |
match dim1.dim_desc, dim2.dim_desc with |
327 |
| Dunivar, _ |
328 |
| _ , Dunivar -> assert false |
329 |
| Dvar , Dvar -> |
330 |
if dim1.dim_id < dim2.dim_id |
331 |
then dim2.dim_desc <- Dlink dim1 |
332 |
else dim1.dim_desc <- Dlink dim2 |
333 |
| Dvar , _ when not (occurs dim1 dim2) -> |
334 |
dim1.dim_desc <- Dlink dim2 |
335 |
| _ , Dvar when not (occurs dim2 dim1) -> |
336 |
dim2.dim_desc <- Dlink dim1 |
337 |
| Dite(i1, t1, e1), Dite(i2, t2, e2) -> |
338 |
begin |
339 |
unify i1 i2; |
340 |
unify t1 t2; |
341 |
unify e1 e2 |
342 |
end |
343 |
| Dappl(f1, args1), Dappl(f2, args2) when f1 = f2 && List.length args1 = List.length args2 -> |
344 |
List.iter2 unify args1 args2 |
345 |
| Dbool b1, Dbool b2 when b1 = b2 -> () |
346 |
| Dint i1 , Dint i2 when i1 = i2 -> () |
347 |
| Dident id1, Dident id2 when id1 = id2 -> () |
348 |
| _ -> raise (Unify (dim1, dim2)) |
349 |
|
350 |
(* unification with the constraint that dim1 is an instance of dim2 *) |
351 |
let rec semi_unify dim1 dim2 = |
352 |
let dim1 = repr dim1 in |
353 |
let dim2 = repr dim2 in |
354 |
if dim1.dim_id = dim2.dim_id then () else |
355 |
match dim1.dim_desc, dim2.dim_desc with |
356 |
| Dunivar, _ |
357 |
| _ , Dunivar -> assert false |
358 |
| Dvar , Dvar -> |
359 |
if dim1.dim_id < dim2.dim_id |
360 |
then dim2.dim_desc <- Dlink dim1 |
361 |
else dim1.dim_desc <- Dlink dim2 |
362 |
| Dvar , _ -> raise (Unify (dim1, dim2)) |
363 |
| _ , Dvar when not (occurs dim2 dim1) -> |
364 |
dim2.dim_desc <- Dlink dim1 |
365 |
| Dite(i1, t1, e1), Dite(i2, t2, e2) -> |
366 |
begin |
367 |
semi_unify i1 i2; |
368 |
semi_unify t1 t2; |
369 |
semi_unify e1 e2 |
370 |
end |
371 |
| Dappl(f1, args1), Dappl(f2, args2) when f1 = f2 && List.length args1 = List.length args2 -> |
372 |
List.iter2 semi_unify args1 args2 |
373 |
| Dbool b1, Dbool b2 when b1 = b2 -> () |
374 |
| Dint i1 , Dint i2 when i1 = i2 -> () |
375 |
| Dident id1, Dident id2 when id1 = id2 -> () |
376 |
| _ -> raise (Unify (dim1, dim2)) |
377 |
|
378 |
let rec expr_replace_var fvar e = |
379 |
{ e with dim_desc = expr_replace_desc fvar e.dim_desc } |
380 |
and expr_replace_desc fvar e = |
381 |
let re = expr_replace_var fvar in |
382 |
match e with |
383 |
| Dvar |
384 |
| Dunivar |
385 |
| Dbool _ |
386 |
| Dint _ -> e |
387 |
| Dident v -> Dident (fvar v) |
388 |
| Dappl (id, el) -> Dappl (id, List.map re el) |
389 |
| Dite (g,t,e) -> Dite (re g, re t, re e) |
390 |
| Dlink e -> Dlink (re e) |