Mercurial > urweb

comparison src/elab_env.sml @ 904:6d9538ce94d8

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Fix type class resolution infinite loop, discovered while meeting with Ezra
author Adam Chlipala <adamc@hcoop.net>
date Thu, 06 Aug 2009 15:23:04 -0400
parents e571fb150a9f
children 86b831978b8d
comparison
equal deleted inserted replaced
903:63114a2e5075 904:6d9538ce94d8
498 | (_, KUnif (_, _, ref (SOME k2))) => unifyKinds (k1, k2) 498 | (_, KUnif (_, _, ref (SOME k2))) => unifyKinds (k1, k2)
499 | (KRel n1, KRel n2) => if n1 = n2 then () else raise Unify 499 | (KRel n1, KRel n2) => if n1 = n2 then () else raise Unify
500 | (KFun (_, k1), KFun (_, k2)) => unifyKinds (k1, k2) 500 | (KFun (_, k1), KFun (_, k2)) => unifyKinds (k1, k2)
501 | _ => raise Unify 501 | _ => raise Unify
502 502
503 fun eqCons (c1, c2) =
504 case (#1 c1, #1 c2) of
505 (CUnif (_, _, _, ref (SOME c1)), _) => eqCons (c1, c2)
506 | (_, CUnif (_, _, _, ref (SOME c2))) => eqCons (c1, c2)
507
508 | (CRel n1, CRel n2) => if n1 = n2 then () else raise Unify
509
510 | (TFun (d1, r1), TFun (d2, r2)) => (eqCons (d1, d2); eqCons (r1, r2))
511 | (TCFun (_, _, k1, r1), TCFun (_, _, k2, r2)) => (unifyKinds (k1, k2); eqCons (r1, r2))
512 | (TRecord c1, TRecord c2) => eqCons (c1, c2)
513 | (TDisjoint (a1, b1, c1), TDisjoint (a2, b2, c2)) =>
514 (eqCons (a1, a2); eqCons (b1, b2); eqCons (c1, c2))
515
516 | (CNamed n1, CNamed n2) => if n1 = n2 then () else raise Unify
517 | (CModProj (n1, ms1, x1), CModProj (n2, ms2, x2)) =>
518 if n1 = n2 andalso ms1 = ms2 andalso x1 = x2 then () else raise Unify
519 | (CApp (f1, x1), CApp (f2, x2)) => (eqCons (f1, f2); eqCons (x1, x2))
520 | (CAbs (_, k1, b1), CAbs (_, k2, b2)) => (unifyKinds (k1, k2); eqCons (b1, b2))
521
522 | (CKAbs (_, b1), CKAbs (_, b2)) => eqCons (b1, b2)
523 | (CKApp (c1, k1), CKApp (c2, k2)) => (eqCons (c1, c2); unifyKinds (k1, k2))
524 | (TKFun (_, c1), TKFun (_, c2)) => eqCons (c1, c2)
525
526 | (CName s1, CName s2) => if s1 = s2 then () else raise Unify
527
528 | (CRecord (k1, xcs1), CRecord (k2, xcs2)) =>
529 (unifyKinds (k1, k2);
530 ListPair.appEq (fn ((x1, c1), (x2, c2)) => (eqCons (x1, x2); eqCons (c1, c2))) (xcs1, xcs2)
531 handle ListPair.UnequalLengths => raise Unify)
532 | (CConcat (f1, x1), CConcat (f2, x2)) => (eqCons (f1, f2); eqCons (x1, x2))
533 | (CMap (d1, r1), CMap (d2, r2)) => (unifyKinds (d1, d2); unifyKinds (r1, r2))
534
535 | (CUnit, CUnit) => ()
536
537 | (CTuple cs1, CTuple cs2) => (ListPair.appEq (eqCons) (cs1, cs2)
538 handle ListPair.UnequalLengths => raise Unify)
539 | (CProj (c1, n1), CProj (c2, n2)) => (eqCons (c1, c2);
540 if n1 = n2 then () else raise Unify)
541
542 | _ => raise Unify
543
503 fun unifyCons rs = 544 fun unifyCons rs =
504 let 545 let
505 fun unify d (c1, c2) = 546 fun unify d (c1, c2) =
506 case (#1 c1, #1 c2) of 547 case (#1 c1, #1 c2) of
507 (CUnif (_, _, _, ref (SOME c1)), _) => unify d (c1, c2) 548 (CUnif (_, _, _, ref (SOME c1)), _) => unify d (c1, c2)
522 let 563 let
523 val r = List.nth (rs, n2 - d) 564 val r = List.nth (rs, n2 - d)
524 in 565 in
525 case !r of 566 case !r of
526 NONE => r := SOME c1 567 NONE => r := SOME c1
527 | SOME c2 => unify d (c1, c2) 568 | SOME c2 => eqCons (c1, c2)
528 end 569 end
529 570
530 | (TFun (d1, r1), TFun (d2, r2)) => (unify d (d1, d2); unify d (r1, r2)) 571 | (TFun (d1, r1), TFun (d2, r2)) => (unify d (d1, d2); unify d (r1, r2))
531 | (TCFun (_, _, k1, r1), TCFun (_, _, k2, r2)) => (unifyKinds (k1, k2); unify (d + 1) (r1, r2)) 572 | (TCFun (_, _, k1, r1), TCFun (_, _, k2, r2)) => (unifyKinds (k1, k2); unify (d + 1) (r1, r2))
532 | (TRecord c1, TRecord c2) => unify d (c1, c2) 573 | (TRecord c1, TRecord c2) => unify d (c1, c2)