Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / dimension.ml @ 01d48bb0

History | View | Annotate | Download (11 KB)

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 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
  | Dint i1   , Dint i2    -> i1 = i2
128
  | Dbool b1  , Dbool b2   -> b1 = b2
129
  | Dident id1, Dident id2 -> id1 = id2
130
  | _                      -> false
131

    
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
(*
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
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         -> (Format.eprintf "invalid %a@." pp_dimension dim; 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
in
248
begin
249
  Format.eprintf "Dimension.eval %a = " pp_dimension dim; 
250
  eval eval_op eval_const dim;
251
  Format.eprintf "%a@." pp_dimension dim
252
end
253
*)
254
let uneval const univar =
255
  let univar = repr univar in
256
  match univar.dim_desc with
257
  | Dunivar -> univar.dim_desc <- Dident const
258
  | _       -> assert false
259

    
260
(** [occurs dvar dim] returns true if the dimension variable [dvar] occurs in
261
    dimension expression [dim]. False otherwise. *)
262
let rec occurs dvar dim =
263
  let dim = repr dim in
264
  match dim.dim_desc with
265
  | Dvar  -> dim.dim_id = dvar.dim_id
266
  | Dident _
267
  | Dint _
268
  | Dbool _
269
  | Dunivar          -> false
270
  | Dite (i, t, e)   ->
271
      occurs dvar i || occurs dvar t || occurs dvar e
272
  | Dappl (_, args) -> List.exists (occurs dvar) args
273
  | Dlink _ -> assert false
274

    
275
(* Promote monomorphic dimension variables to polymorphic variables.
276
   Generalize by side-effects *)
277
let rec generalize dim =
278
  match dim.dim_desc with
279
  | Dvar -> dim.dim_desc <- Dunivar
280
  | Dident _
281
  | Dint _
282
  | Dbool _
283
  | Dunivar          -> ()
284
  | Dite (i, t, e)   ->
285
      generalize i; generalize t; generalize e
286
  | Dappl (_, args) -> List.iter generalize args
287
  | Dlink dim' -> generalize dim'
288

    
289
(* Instantiate polymorphic dimension variables to monomorphic variables.
290
   Also duplicates the whole term structure (but the constant sub-terms).
291
*)
292
let rec instantiate inst_dim_vars dim =
293
  let dim = repr dim in
294
  match dim.dim_desc with
295
  | Dvar
296
  | Dident _
297
  | Dint _
298
  | Dbool _ -> dim
299
  | Dite (i, t, e)   ->
300
      mkdim_ite dim.dim_loc
301
	(instantiate inst_dim_vars i)
302
	(instantiate inst_dim_vars t)
303
	(instantiate inst_dim_vars e)
304
  | Dappl (f, args) -> mkdim_appl dim.dim_loc f (List.map (instantiate inst_dim_vars) args)
305
  | Dlink dim' -> assert false (*mkdim dim.dim_loc (Dlink (instantiate inst_dim_vars dim'))*)
306
  | Dunivar ->
307
      try
308
        List.assoc dim.dim_id !inst_dim_vars
309
      with Not_found ->
310
        let var = mkdim dim.dim_loc Dvar in
311
	inst_dim_vars := (dim.dim_id, var)::!inst_dim_vars;
312
	var
313

    
314
(** destructive unification of [dim1] and [dim2].
315
   Raises [Unify (t1,t2)] if the types are not unifiable.
316
   if [semi] unification is required,
317
   [dim1] should furthermore be an instance of [dim2] *)
318
let unify ?(semi=false) dim1 dim2 =
319
  let rec unif dim1 dim2 =
320
    let dim1 = repr dim1 in
321
    let dim2 = repr dim2 in
322
    if dim1.dim_id = dim2.dim_id then () else
323
      match dim1.dim_desc, dim2.dim_desc with
324
      | Dunivar, _
325
      | _      , Dunivar -> assert false
326
      | Dvar   , Dvar    ->
327
	if dim1.dim_id < dim2.dim_id
328
	then dim2.dim_desc <- Dlink dim1
329
	else dim1.dim_desc <- Dlink dim2
330
      | Dvar   , _ when (not semi) && not (occurs dim1 dim2) ->
331
	dim1.dim_desc <- Dlink dim2
332
      | _      , Dvar when not (occurs dim2 dim1) ->
333
	dim2.dim_desc <- Dlink dim1
334
      | Dite(i1, t1, e1), Dite(i2, t2, e2) ->
335
	begin
336
          unif i1 i2;
337
	  unif t1 t2;
338
	  unif e1 e2
339
	end
340
      | Dappl(f1, args1), Dappl(f2, args2) when f1 = f2 && List.length args1 = List.length args2 ->
341
	List.iter2 unif args1 args2
342
      | Dbool b1, Dbool b2 when b1 = b2 -> ()
343
      | Dint i1 , Dint i2 when i1 = i2 -> ()
344
      | Dident id1, Dident id2 when id1 = id2 -> ()
345
      | _ -> raise (Unify (dim1, dim2))
346
  in unif dim1 dim2
347

    
348
let rec expr_replace_var fvar e = 
349
 { e with dim_desc = expr_replace_var_desc fvar e.dim_desc }
350
and expr_replace_var_desc fvar e =
351
  let re = expr_replace_var fvar in
352
  match e with
353
  | Dvar
354
  | Dunivar
355
  | Dbool _
356
  | Dint _ -> e
357
  | Dident v -> Dident (fvar v)
358
  | Dappl (id, el) -> Dappl (id, List.map re el)
359
  | Dite (g,t,e) -> Dite (re g, re t, re e)
360
  | Dlink e -> Dlink (re e)
361

    
362
let rec expr_replace_expr fvar e = 
363
 { e with dim_desc = expr_replace_expr_desc fvar e.dim_desc }
364
and expr_replace_expr_desc fvar e =
365
  let re = expr_replace_expr fvar in
366
  match e with
367
  | Dvar
368
  | Dunivar
369
  | Dbool _
370
  | Dint _ -> e
371
  | Dident v -> (fvar v).dim_desc
372
  | Dappl (id, el) -> Dappl (id, List.map re el)
373
  | Dite (g,t,e) -> Dite (re g, re t, re e)
374
  | Dlink e -> Dlink (re e)