Mercurial > urweb

comparison src/elab_env.sml @ 753:d484df4e841a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Preparing to allow views in SELECT FROM clauses
author Adam Chlipala <adamc@hcoop.net>
date Tue, 28 Apr 2009 14:02:23 -0400
parents 059074c8d2fc
children 8688e01ae469
comparison
equal deleted inserted replaced
752:bc5cfd6cb30f 753:d484df4e841a
587 | _ => c, 587 | _ => c,
588 bind = fn (d, U.Con.RelC _) => d + 1 588 bind = fn (d, U.Con.RelC _) => d + 1
589 | (d, _) => d} 589 | (d, _) => d}
590 0 590 0
591 591
592 fun postUnify x = 592 exception Bad of con * con
593 let 593
594 fun unify (c1, c2) = 594 fun resolveClass (hnorm : con -> con) (consEq : con * con -> bool) (env : env) =
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) =
642 let 595 let
643 fun resolve c = 596 fun resolve c =
644 let 597 let
645 fun doHead f = 598 fun doHead f =
646 case CM.find (#classes env, f) of 599 case CM.find (#classes env, f) of
647 NONE => NONE 600 NONE => NONE
648 | SOME class => 601 | SOME class =>
649 let 602 let
650 val loc = #2 c 603 val loc = #2 c
604
605 fun generalize (c as (_, loc)) =
606 case #1 c of
607 CApp (f, x) =>
608 let
609 val (f, equate) = generalize f
610
611 fun isRecord () =
612 let
613 val rk = ref NONE
614 val k = (KUnif (loc, "k", rk), loc)
615 val r = ref NONE
616 val rc = (CUnif (loc, k, "x", r), loc)
617 in
618 ((CApp (f, rc), loc),
619 fn () => (if consEq (rc, x) then
620 true
621 else
622 (raise Bad (rc, x);
623 false))
624 andalso equate ())
625 end
626 in
627 case #1 x of
628 CConcat _ => isRecord ()
629 | CRecord _ => isRecord ()
630 | _ => ((CApp (f, x), loc), equate)
631 end
632 | _ => (c, fn () => true)
633
634 val (c, equate) = generalize c
651 635
652 fun tryRules rules = 636 fun tryRules rules =
653 case rules of 637 case rules of
654 [] => NONE 638 [] => NONE
655 | (nRs, cs, c', e) :: rules' => 639 | (nRs, cs, c', e) :: rules' =>
658 | SOME rs => 642 | SOME rs =>
659 let 643 let
660 val eos = map (resolve o unifySubst rs) cs 644 val eos = map (resolve o unifySubst rs) cs
661 in 645 in
662 if List.exists (not o Option.isSome) eos 646 if List.exists (not o Option.isSome) eos
663 orelse not (postUnifies (c, unifySubst rs c')) then 647 orelse not (equate ())
648 orelse not (consEq (c, unifySubst rs c')) then
664 tryRules rules' 649 tryRules rules'
665 else 650 else
666 let 651 let
667 val es = List.mapPartial (fn x => x) eos 652 val es = List.mapPartial (fn x => x) eos
668 653