Project

General

Profile

« Previous | Next » 

Revision ca7ff3f7

Added by LĂ©lio Brun 7 months ago

reformatting

View differences:

src/utils/dimension.ml
11 11

  
12 12
open Format
13 13

  
14
type dim_expr =
15
  {mutable dim_desc: dim_desc;
16
   dim_loc: Location.t;
17
   dim_id: int}
14
type dim_expr = {
15
  mutable dim_desc : dim_desc;
16
  dim_loc : Location.t;
17
  dim_id : int;
18
}
18 19

  
19 20
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
21
  | Dbool of bool
22
  | Dint of int
23
  | Dident of Utils.ident
24
  | Dappl of Utils.ident * dim_expr list
25
  | Dite of dim_expr * dim_expr * dim_expr
26
  | Dlink of dim_expr
27
  | Dvar
28
  | Dunivar
28 29

  
29 30
exception Unify of dim_expr * dim_expr
31

  
30 32
exception InvalidDimension
31 33

  
32 34
let new_id = ref (-1)
33 35

  
34 36
let mkdim loc dim =
35 37
  incr new_id;
36
  { dim_loc = loc;
37
    dim_id = !new_id;
38
    dim_desc = dim;}
38
  { dim_loc = loc; dim_id = !new_id; dim_desc = dim }
39 39

  
40 40
let mkdim_var () =
41 41
  incr new_id;
42
  { dim_loc = Location.dummy_loc;
43
    dim_id = !new_id;
44
    dim_desc = Dvar;}
42
  { dim_loc = Location.dummy_loc; dim_id = !new_id; dim_desc = Dvar }
45 43

  
46 44
let mkdim_ident loc id =
47 45
  incr new_id;
48
  { dim_loc = loc;
49
    dim_id = !new_id;
50
    dim_desc = Dident id;}
46
  { dim_loc = loc; dim_id = !new_id; dim_desc = Dident id }
51 47

  
52 48
let mkdim_bool loc b =
53 49
  incr new_id;
54
  { dim_loc = loc;
55
    dim_id = !new_id;
56
    dim_desc = Dbool b;}
50
  { dim_loc = loc; dim_id = !new_id; dim_desc = Dbool b }
57 51

  
58 52
let mkdim_int loc i =
59 53
  incr new_id;
60
  { dim_loc = loc;
61
    dim_id = !new_id;
62
    dim_desc = Dint i;}
54
  { dim_loc = loc; dim_id = !new_id; dim_desc = Dint i }
63 55

  
64 56
let mkdim_appl loc f args =
65 57
  incr new_id;
66
  { dim_loc = loc;
67
    dim_id = !new_id;
68
    dim_desc = Dappl (f, args);}
58
  { dim_loc = loc; dim_id = !new_id; dim_desc = Dappl (f, args) }
69 59

  
70 60
let mkdim_ite loc i t e =
71 61
  incr new_id;
72
  { dim_loc = loc;
73
    dim_id = !new_id;
74
    dim_desc = Dite (i, t, e);}
62
  { dim_loc = loc; dim_id = !new_id; dim_desc = Dite (i, t, e) }
75 63

  
76 64
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)
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_dimension i pp_dimension t
75
      pp_dimension e
76
  | Dappl (f, [ arg ]) ->
77
    fprintf fmt "(%s%a)" f pp_dimension arg
78
  | Dappl (f, [ arg1; arg2 ]) ->
79
    fprintf fmt "(%a%s%a)" pp_dimension arg1 f pp_dimension arg2
80
  | Dappl (_, _) ->
81
    assert false
82
  | Dlink dim' ->
83
    fprintf fmt "%a" pp_dimension 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)
96 88

  
97 89
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]
90
  match dim_list with
91
  | [] ->
92
    mkdim_int loc 1
93
  | [ d ] ->
94
    d
95
  | d :: q ->
96
    mkdim_appl loc "*" [ d; multi_dimension_product loc q ]
102 97

  
103 98
(* Builds a dimension expr representing 0<=d *)
104
let check_bound loc d =
105
 mkdim_appl loc "<=" [mkdim_int loc 0; d]
99
let check_bound loc d = mkdim_appl loc "<=" [ mkdim_int loc 0; d ]
106 100

  
107 101
(* Builds a dimension expr representing 0<=i<d *)
108 102
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]]
103
  mkdim_appl loc "&&"
104
    [ mkdim_appl loc "<=" [ mkdim_int loc 0; i ]; mkdim_appl loc "<" [ i; d ] ]
112 105

  
113
let rec repr dim =
114
 match dim.dim_desc with
115
 | Dlink dim' -> repr dim'
116
 | _          -> dim
106
let rec repr dim = match dim.dim_desc with Dlink dim' -> repr dim' | _ -> dim
117 107

  
118 108
let rec is_eq_dimension d1 d2 =
119 109
  let d1 = repr d1 in
120 110
  let d2 = repr d2 in
121
  d1.dim_id = d2.dim_id ||
111
  d1.dim_id = d2.dim_id
112
  ||
122 113
  match d1.dim_desc, d2.dim_desc with
123 114
  | Dappl (f1, args1), Dappl (f2, args2) ->
124
    f1 = f2 && List.length args1 = List.length args2 && List.for_all2 is_eq_dimension args1 args2
115
    f1 = f2
116
    && List.length args1 = List.length args2
117
    && List.for_all2 is_eq_dimension args1 args2
125 118
  | Dite (c1, t1, e1), Dite (c2, t2, e2) ->
126 119
    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
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
131 128

  
132 129
let is_dimension_const dim =
133
 match (repr dim).dim_desc with
134
 | Dint _
135
 | Dbool _ -> true
136
 | _       -> false
130
  match (repr dim).dim_desc with Dint _ | Dbool _ -> true | _ -> false
137 131

  
138 132
let size_const_dimension dim =
139 133
  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)
134
  | Dint i ->
135
    i
136
  | Dbool b ->
137
    if b then 1 else 0
138
  | _ ->
139
    Format.eprintf "internal error: size_const_dimension %a@." pp_dimension dim;
140
    assert false
143 141

  
144 142
let rec is_polymorphic dim =
145 143
  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
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
155 154

  
156 155
(* Normalizes a dimension expression, i.e. canonicalize all polynomial
157
   sub-expressions, where unsupported operations (eg. '/') are treated
158
   as variables.
159
*)
156
   sub-expressions, where unsupported operations (eg. '/') are treated as
157
   variables. *)
160 158

  
161 159
let rec factors dim =
162 160
  match dim.dim_desc with
163
  | Dappl (f, args) when f = "*" -> List.flatten (List.map factors args)
164
  | _                            -> [dim]
161
  | Dappl (f, args) when f = "*" ->
162
    List.flatten (List.map factors args)
163
  | _ ->
164
    [ dim ]
165 165

  
166 166
let rec factors_constant fs =
167 167
  match fs with
168
  | []   -> 1
169
  | f::q ->
168
  | [] ->
169
    1
170
  | f :: q -> (
170 171
    match f.dim_desc with
171
    | Dint i -> i * (factors_constant q)
172
    | _      -> factors_constant q
172
    | Dint i ->
173
      i * factors_constant q
174
    | _ ->
175
      factors_constant q)
173 176

  
174 177
let norm_factors fs =
175 178
  let k = factors_constant fs in
176 179
  let nk = List.filter (fun d -> not (is_dimension_const d)) fs in
177
  (k, List.sort compare nk)
180
  k, List.sort compare nk
178 181

  
179 182
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 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 183
  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
184
  | Dappl (f, args) when f = "+" ->
185
    List.flatten (List.map terms args)
186
  | _ ->
187
    [ dim ]
188

  
189
let normalize dim = dim
212 190

  
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
*)
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. *)
216 223
let rec eval eval_op eval_const dim =
217 224
  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
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_dimension 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
      ())
233 243
  | 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
244
    List.iter (eval eval_op eval_const) args;
245
    if List.for_all is_dimension_const args then
246
      dim.dim_desc <-
247
        Env.lookup_value eval_op id (List.map (fun d -> (repr d).dim_desc) args)
239 248
  | 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
249
    eval eval_op eval_const dim';
250
    dim.dim_desc <- Dlink (repr dim')
251
  | Dvar ->
252
    ()
253
  | Dunivar ->
254
    assert false
246 255

  
247 256
let uneval const univar =
248 257
  let univar = repr univar in
249 258
  match univar.dim_desc with
250
  | Dunivar -> univar.dim_desc <- Dident const
251
  | _       -> assert false
259
  | Dunivar ->
260
    univar.dim_desc <- Dident const
261
  | _ ->
262
    assert false
252 263

  
253 264
(** [occurs dvar dim] returns true if the dimension variable [dvar] occurs in
254 265
    dimension expression [dim]. False otherwise. *)
255 266
let rec occurs dvar dim =
256 267
  let dim = repr dim in
257 268
  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 *)
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 *)
270 282
let rec generalize dim =
271 283
  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
*)
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). *)
285 299
let rec instantiate inst_dim_vars dim =
286 300
  let dim = repr dim in
287 301
  match dim.dim_desc with
288
  | Dvar
289
  | 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 _ -> 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
(** 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 =
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 =
312 324
  let rec unif dim1 dim2 =
313 325
    let dim1 = repr dim1 in
314 326
    let dim2 = repr dim2 in
315
    if dim1.dim_id = dim2.dim_id then () else
327
    if dim1.dim_id = dim2.dim_id then ()
328
    else
316 329
      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

  
341
let rec rename fnode fvar e = 
342
 { e with dim_desc = expr_replace_var_desc fnode fvar e.dim_desc }
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

  
343 360
and expr_replace_var_desc fnode fvar e =
344 361
  let re = rename fnode fvar in
345 362
  match e with
346
  | Dvar
347
  | Dunivar
348
  | Dbool _
349
  | Dint _ -> e
350
  | Dident v -> Dident (fvar v)
351
  | Dappl (id, el) -> Dappl (fnode id, List.map re el)
352
  | Dite (g,t,e) -> Dite (re g, re t, re e)
353
  | Dlink e -> Dlink (re e)
354

  
355
let rec expr_replace_expr fvar e = 
356
 { e with dim_desc = expr_replace_expr_desc fvar e.dim_desc }
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

  
357 377
and expr_replace_expr_desc fvar e =
358 378
  let re = expr_replace_expr fvar in
359 379
  match e with
360
  | Dvar
361
  | Dunivar
362
  | Dbool _
363
  | Dint _ -> e
364
  | Dident v -> (fvar v).dim_desc
365
  | Dappl (id, el) -> Dappl (id, List.map re el)
366
  | Dite (g,t,e) -> Dite (re g, re t, re e)
367
  | Dlink e -> Dlink (re e)
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)

Also available in: Unified diff