Mercurial > urweb

comparison src/elab_env.sml @ 750:059074c8d2fc

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
LEFT JOIN
author Adam Chlipala <adamc@hcoop.net>
date Tue, 28 Apr 2009 11:05:28 -0400
parents 9864b64b1700
children d484df4e841a
comparison
equal deleted inserted replaced
749:16bfd9e244cd 750:059074c8d2fc
505 fun unify d (c1, c2) = 505 fun unify d (c1, c2) =
506 case (#1 c1, #1 c2) of 506 case (#1 c1, #1 c2) of
507 (CUnif (_, _, _, ref (SOME c1)), _) => unify d (c1, c2) 507 (CUnif (_, _, _, ref (SOME c1)), _) => unify d (c1, c2)
508 | (_, CUnif (_, _, _, ref (SOME c2))) => unify d (c1, c2) 508 | (_, CUnif (_, _, _, ref (SOME c2))) => unify d (c1, c2)
509 509
510 | (CUnif _, _) => ()
511
510 | (c1', CRel n2) => 512 | (c1', CRel n2) =>
511 if n2 < d then 513 if n2 < d then
512 case c1' of 514 case c1' of
513 CRel n1 => if n1 = n2 then () else raise Unify 515 CRel n1 => if n1 = n2 then () else raise Unify
514 | _ => raise Unify 516 | _ => raise Unify
585 | _ => c, 587 | _ => c,
586 bind = fn (d, U.Con.RelC _) => d + 1 588 bind = fn (d, U.Con.RelC _) => d + 1
587 | (d, _) => d} 589 | (d, _) => d}
588 0 590 0
589 591
590 fun resolveClass (env : env) = 592 fun postUnify x =
593 let
594 fun unify (c1, c2) =
595 case (#1 c1, #1 c2) of
596 (CUnif (_, _, _, ref (SOME c1)), _) => unify (c1, c2)
597 | (_, CUnif (_, _, _, ref (SOME c2))) => unify (c1, c2)
598
599 | (CUnif (_, _, _, r), _) => r := SOME c2
600
601 | (TFun (d1, r1), TFun (d2, r2)) => (unify (d1, d2); unify (r1, r2))
602 | (TCFun (_, _, k1, r1), TCFun (_, _, k2, r2)) => (unifyKinds (k1, k2); unify (r1, r2))
603 | (TRecord c1, TRecord c2) => unify (c1, c2)
604 | (TDisjoint (a1, b1, c1), TDisjoint (a2, b2, c2)) =>
605 (unify (a1, a2); unify (b1, b2); unify (c1, c2))
606
607 | (CRel n1, CRel n2) => if n1 = n2 then () else raise Unify
608 | (CNamed n1, CNamed n2) => if n1 = n2 then () else raise Unify
609 | (CModProj (n1, ms1, x1), CModProj (n2, ms2, x2)) =>
610 if n1 = n2 andalso ms1 = ms2 andalso x1 = x2 then () else raise Unify
611 | (CApp (f1, x1), CApp (f2, x2)) => (unify (f1, f2); unify (x1, x2))
612 | (CAbs (_, k1, b1), CAbs (_, k2, b2)) => (unifyKinds (k1, k2); unify (b1, b2))
613
614 | (CKAbs (_, b1), CKAbs (_, b2)) => unify (b1, b2)
615 | (CKApp (c1, k1), CKApp (c2, k2)) => (unify (c1, c2); unifyKinds (k1, k2))
616 | (TKFun (_, c1), TKFun (_, c2)) => unify (c1, c2)
617
618 | (CName s1, CName s2) => if s1 = s2 then () else raise Unify
619
620 | (CRecord (k1, xcs1), CRecord (k2, xcs2)) =>
621 (unifyKinds (k1, k2);
622 ListPair.appEq (fn ((x1, c1), (x2, c2)) => (unify (x1, x2); unify (c1, c2))) (xcs1, xcs2)
623 handle ListPair.UnequalLengths => raise Unify)
624 | (CConcat (f1, x1), CConcat (f2, x2)) => (unify (f1, f2); unify (x1, x2))
625 | (CMap (d1, r1), CMap (d2, r2)) => (unifyKinds (d1, d2); unifyKinds (r1, r2))
626
627 | (CUnit, CUnit) => ()
628
629 | (CTuple cs1, CTuple cs2) => (ListPair.appEq unify (cs1, cs2)
630 handle ListPair.UnequalLengths => raise Unify)
631 | (CProj (c1, n1), CProj (c2, n2)) => (unify (c1, c2);
632 if n1 = n2 then () else raise Unify)
633
634 | _ => raise Unify
635 in
636 unify x
637 end
638
639 fun postUnifies x = (postUnify x; true) handle Unify => false
640
641 fun resolveClass (hnorm : con -> con) (env : env) =
591 let 642 let
592 fun resolve c = 643 fun resolve c =
593 let 644 let
594 fun doHead f = 645 fun doHead f =
595 case CM.find (#classes env, f) of 646 case CM.find (#classes env, f) of
606 NONE => tryRules rules' 657 NONE => tryRules rules'
607 | SOME rs => 658 | SOME rs =>
608 let 659 let
609 val eos = map (resolve o unifySubst rs) cs 660 val eos = map (resolve o unifySubst rs) cs
610 in 661 in
611 if List.exists (not o Option.isSome) eos then 662 if List.exists (not o Option.isSome) eos
663 orelse not (postUnifies (c, unifySubst rs c')) then
612 tryRules rules' 664 tryRules rules'
613 else 665 else
614 let 666 let
615 val es = List.mapPartial (fn x => x) eos 667 val es = List.mapPartial (fn x => x) eos
616 668
632 | SOME _ => SOME e 684 | SOME _ => SOME e
633 in 685 in
634 tryGrounds (#ground class) 686 tryGrounds (#ground class)
635 end 687 end
636 in 688 in
637 case class_head_in c of 689 case #1 c of
638 SOME f => doHead f 690 TRecord c =>
639 | _ => NONE 691 (case #1 (hnorm c) of
692 CRecord (_, xts) =>
693 let
694 fun resolver (xts, acc) =
695 case xts of
696 [] => SOME (ERecord acc, #2 c)
697 | (x, t) :: xts =>
698 let
699 val t = hnorm t
700
701 val t = case t of
702 (CApp (f, x), loc) => (CApp (hnorm f, hnorm x), loc)
703 | _ => t
704 in
705 case resolve t of
706 NONE => NONE
707 | SOME e => resolver (xts, (x, e, t) :: acc)
708 end
709 in
710 resolver (xts, [])
711 end
712 | _ => NONE)
713 | _ =>
714 case class_head_in c of
715 SOME f => doHead f
716 | _ => NONE
640 end 717 end
641 in 718 in
642 resolve 719 resolve
643 end 720 end
644 721