Project

General

Profile

Revision 59294251 src/dimension.ml

View differences:

src/dimension.ml
319 319
	inst_dim_vars := (dim.dim_id, var)::!inst_dim_vars;
320 320
	var
321 321

  
322
let rec unify dim1 dim2 =
323
  let dim1 = repr dim1 in
324
  let dim2 = repr dim2 in
325
  if dim1.dim_id = dim2.dim_id then () else
326
  match dim1.dim_desc, dim2.dim_desc with
327
  | Dunivar, _
328
  | _      , Dunivar -> assert false
329
  | Dvar   , Dvar    ->
330
      if dim1.dim_id < dim2.dim_id
331
      then dim2.dim_desc <- Dlink dim1
332
      else dim1.dim_desc <- Dlink dim2
333
  | Dvar   , _ when not (occurs dim1 dim2) ->
334
      dim1.dim_desc <- Dlink dim2
335
  | _      , Dvar when not (occurs dim2 dim1) ->
336
      dim2.dim_desc <- Dlink dim1
337
  | Dite(i1, t1, e1), Dite(i2, t2, e2) ->
338
      begin
339
        unify i1 i2;
340
	unify t1 t2;
341
	unify e1 e2
342
      end
343
  | Dappl(f1, args1), Dappl(f2, args2) when f1 = f2 && List.length args1 = List.length args2 ->
344
      List.iter2 unify args1 args2
345
  | Dbool b1, Dbool b2 when b1 = b2 -> ()
346
  | Dint i1 , Dint i2 when i1 = i2 -> ()
347
  | Dident id1, Dident id2 when id1 = id2 -> ()
348
  | _ -> raise (Unify (dim1, dim2))
349

  
350
(* unification with the constraint that dim1 is an instance of dim2 *)
351
let rec semi_unify dim1 dim2 =
352
  let dim1 = repr dim1 in
353
  let dim2 = repr dim2 in
354
  if dim1.dim_id = dim2.dim_id then () else
355
  match dim1.dim_desc, dim2.dim_desc with
356
  | Dunivar, _
357
  | _      , Dunivar -> assert false
358
  | Dvar   , Dvar    ->
359
      if dim1.dim_id < dim2.dim_id
360
      then dim2.dim_desc <- Dlink dim1
361
      else dim1.dim_desc <- Dlink dim2
362
  | Dvar   , _  -> raise (Unify (dim1, dim2))
363
  | _      , Dvar when not (occurs dim2 dim1) ->
364
      dim2.dim_desc <- Dlink dim1
365
  | Dite(i1, t1, e1), Dite(i2, t2, e2) ->
366
      begin
367
        semi_unify i1 i2;
368
	semi_unify t1 t2;
369
	semi_unify e1 e2
370
      end
371
  | Dappl(f1, args1), Dappl(f2, args2) when f1 = f2 && List.length args1 = List.length args2 ->
372
      List.iter2 semi_unify args1 args2
373
  | Dbool b1, Dbool b2 when b1 = b2 -> ()
374
  | Dint i1 , Dint i2 when i1 = i2 -> ()
375
  | Dident id1, Dident id2 when id1 = id2 -> ()
376
  | _ -> raise (Unify (dim1, dim2))
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
377 355

  
378 356
let rec expr_replace_var fvar e = 
379 357
 { e with dim_desc = expr_replace_desc fvar e.dim_desc }

Also available in: Unified diff