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