Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / dimension.ml @ 6afa892a

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

    
356
let rec expr_replace_var fvar e = 
357
 { e with dim_desc = expr_replace_desc fvar e.dim_desc }
358
and expr_replace_desc fvar e =
359
  let re = expr_replace_var fvar in
360
  match e with
361
  | Dvar
362
  | Dunivar
363
  | Dbool _
364
  | Dint _ -> e
365
  | Dident v -> Dident (fvar v)
366
  | Dappl (id, el) -> Dappl (id, List.map re el)
367
  | Dite (g,t,e) -> Dite (re g, re t, re e)
368
  | Dlink e -> Dlink (re e)