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