Mercurial > urweb

comparison src/elaborate.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
645 let 645 let
646 fun rkindof c = 646 fun rkindof c =
647 case hnormKind (kindof env c) of 647 case hnormKind (kindof env c) of
648 (L'.KRecord k, _) => k 648 (L'.KRecord k, _) => k
649 | (L'.KError, _) => kerror 649 | (L'.KError, _) => kerror
650 | (L'.KUnif (_, _, r), _) =>
651 let
652 val k = kunif (#2 c)
653 in
654 r := SOME (L'.KRecord k, #2 c);
655 k
656 end
650 | k => raise CUnify' (CKindof (k, c, "record")) 657 | k => raise CUnify' (CKindof (k, c, "record"))
651 658
652 val k1 = rkindof c1 659 val k1 = rkindof c1
653 val k2 = rkindof c2 660 val k2 = rkindof c2
654 661
784 | orig => orig 791 | orig => orig
785 792
786 (*val () = eprefaces "Summaries4" [("#1", p_summary env {fields = fs1, unifs = unifs1, others = others1}), 793 (*val () = eprefaces "Summaries4" [("#1", p_summary env {fields = fs1, unifs = unifs1, others = others1}),
787 ("#2", p_summary env {fields = fs2, unifs = unifs2, others = others2})]*) 794 ("#2", p_summary env {fields = fs2, unifs = unifs2, others = others2})]*)
788 795
789 fun isGuessable (other, fs) = 796 fun isGuessable (other, fs, unifs) =
790 (guessMap env (other, (L'.CRecord (k, fs), loc), GuessFailure); 797 let
791 true) 798 val c = (L'.CRecord (k, fs), loc)
792 handle GuessFailure => false 799 val c = foldl (fn ((c', _), c) => (L'.CConcat (c', c), loc)) c unifs
800 in
801 (guessMap env (other, c, GuessFailure);
802 true)
803 handle GuessFailure => false
804 end
793 805
794 val (fs1, fs2, others1, others2) = 806 val (fs1, fs2, others1, others2) =
795 case (fs1, fs2, others1, others2) of 807 case (fs1, fs2, others1, others2, unifs1, unifs2) of
796 ([], _, [other1], []) => 808 ([], _, [other1], [], [], _) =>
797 if isGuessable (other1, fs2) then 809 if isGuessable (other1, fs2, unifs2) then
798 ([], [], [], []) 810 ([], [], [], [])
799 else 811 else
800 (fs1, fs2, others1, others2) 812 (fs1, fs2, others1, others2)
801 | (_, [], [], [other2]) => 813 | (_, [], [], [other2], _, []) =>
802 if isGuessable (other2, fs1) then 814 if isGuessable (other2, fs1, unifs1) then
803 ([], [], [], []) 815 ([], [], [], [])
804 else 816 else
805 (fs1, fs2, others1, others2) 817 (fs1, fs2, others1, others2)
806 | _ => (fs1, fs2, others1, others2) 818 | _ => (fs1, fs2, others1, others2)
807 819
863 val r2 = cunif (loc, (L'.KRecord dom, loc)) 875 val r2 = cunif (loc, (L'.KRecord dom, loc))
864 in 876 in
865 unfold (r1, c1'); 877 unfold (r1, c1');
866 unfold (r2, c2'); 878 unfold (r2, c2');
867 unifyCons env r (L'.CConcat (r1, r2), loc) 879 unifyCons env r (L'.CConcat (r1, r2), loc)
880 end
881 | L'.CUnif (_, _, _, ref (SOME c)) => unfold (r, c)
882 | L'.CUnif (_, _, _, ur as ref NONE) =>
883 let
884 val ur' = cunif (loc, (L'.KRecord dom, loc))
885 in
886 ur := SOME (L'.CApp ((L'.CApp ((L'.CMap (dom, ran), loc), f), loc), ur'), loc)
868 end 887 end
869 | _ => raise ex 888 | _ => raise ex
870 in 889 in
871 unfold (r, c) 890 unfold (r, c)
872 end 891 end
1142 end 1161 end
1143 else 1162 else
1144 default () 1163 default ()
1145 1164
1146 fun hasInstance c = 1165 fun hasInstance c =
1147 case #1 (hnormCon env c) of 1166 case hnormCon env c of
1148 L'.CApp (cl, x) => 1167 (L'.TRecord c, _) => U.Con.exists {kind = fn _ => false,
1168 con = fn c =>
1169 E.isClass env (hnormCon env (c, loc))} c
1170 | c =>
1149 let 1171 let
1150 val cl = hnormCon env cl 1172 fun findHead c =
1173 case #1 c of
1174 L'.CApp (f, _) => findHead f
1175 | _ => c
1176
1177 val cl = hnormCon env (findHead c)
1151 in 1178 in
1152 isClassOrFolder env cl 1179 isClassOrFolder env cl
1153 end 1180 end
1154 | L'.TRecord c => U.Con.exists {kind = fn _ => false,
1155 con = fn c =>
1156 E.isClass env (hnormCon env (c, loc))} c
1157 | _ => false
1158 in 1181 in
1159 if hasInstance dom then 1182 if hasInstance dom then
1160 isInstance () 1183 isInstance ()
1161 else 1184 else
1162 default () 1185 default ()
3645 raise Fail "Unresolved constraint in top.ur")) 3668 raise Fail "Unresolved constraint in top.ur"))
3646 | TypeClass (env, c, r, loc) => 3669 | TypeClass (env, c, r, loc) =>
3647 let 3670 let
3648 val c = normClassKey env c 3671 val c = normClassKey env c
3649 in 3672 in
3650 case E.resolveClass (hnormCon env) env c of 3673 case E.resolveClass (hnormCon env) (consEq env) env c of
3651 SOME e => r := SOME e 3674 SOME e => r := SOME e
3652 | NONE => expError env (Unresolvable (loc, c)) 3675 | NONE => expError env (Unresolvable (loc, c))
3653 end) gs 3676 end) gs
3654 3677
3655 val () = subSgn env' topSgn' topSgn 3678 val () = subSgn env' topSgn' topSgn
3682 3705
3683 (ds, (env, gs)) 3706 (ds, (env, gs))
3684 end 3707 end
3685 3708
3686 val (file, (_, gs)) = ListUtil.foldlMapConcat elabDecl' (env', []) file 3709 val (file, (_, gs)) = ListUtil.foldlMapConcat elabDecl' (env', []) file
3710
3711 val delayed = !delayedUnifs
3687 in 3712 in
3713 delayedUnifs := [];
3714 app (fn (env, k, s1, s2) =>
3715 unifySummaries env (k, normalizeRecordSummary env s1, normalizeRecordSummary env s2))
3716 delayed;
3717
3718 if ErrorMsg.anyErrors () then
3719 ()
3720 else
3721 let
3722 fun solver gs =
3723 let
3724 val (gs, solved) =
3725 ListUtil.foldlMapPartial
3726 (fn (g, solved) =>
3727 case g of
3728 Disjoint (loc, env, denv, c1, c2) =>
3729 (case D.prove env denv (c1, c2, loc) of
3730 [] => (NONE, true)
3731 | _ => (SOME g, solved))
3732 | TypeClass (env, c, r, loc) =>
3733 let
3734 fun default () = (SOME g, solved)
3735
3736 val c = normClassKey env c
3737 in
3738 case E.resolveClass (hnormCon env) (consEq env) env c of
3739 SOME e => (r := SOME e;
3740 (NONE, true))
3741 | NONE =>
3742 case #1 (hnormCon env c) of
3743 L'.CApp (f, x) =>
3744 (case (#1 (hnormCon env f), #1 (hnormCon env x)) of
3745 (L'.CKApp (f, _), L'.CRecord (k, xcs)) =>
3746 (case #1 (hnormCon env f) of
3747 L'.CModProj (top_n', [], "folder") =>
3748 if top_n' = top_n then
3749 let
3750 val e = (L'.EModProj (top_n, ["Folder"], "nil"), loc)
3751 val e = (L'.EKApp (e, k), loc)
3752
3753 val (folder, _) = foldr (fn ((x, c), (folder, xcs)) =>
3754 let
3755 val e = (L'.EModProj (top_n, ["Folder"],
3756 "cons"), loc)
3757 val e = (L'.EKApp (e, k), loc)
3758 val e = (L'.ECApp (e,
3759 (L'.CRecord (k, xcs),
3760 loc)), loc)
3761 val e = (L'.ECApp (e, x), loc)
3762 val e = (L'.ECApp (e, c), loc)
3763 val e = (L'.EApp (e, folder), loc)
3764 in
3765 (e, (x, c) :: xcs)
3766 end)
3767 (e, []) xcs
3768 in
3769 (r := SOME folder;
3770 (NONE, true))
3771 end
3772 else
3773 default ()
3774 | _ => default ())
3775 | _ => default ())
3776 | _ => default ()
3777 end)
3778 false gs
3779 in
3780 case (gs, solved) of
3781 ([], _) => ()
3782 | (_, true) => solver gs
3783 | _ =>
3784 app (fn Disjoint (loc, env, denv, c1, c2) =>
3785 ((ErrorMsg.errorAt loc "Couldn't prove field name disjointness";
3786 eprefaces' [("Con 1", p_con env c1),
3787 ("Con 2", p_con env c2),
3788 ("Hnormed 1", p_con env (ElabOps.hnormCon env c1)),
3789 ("Hnormed 2", p_con env (ElabOps.hnormCon env c2))]))
3790 | TypeClass (env, c, r, loc) =>
3791 expError env (Unresolvable (loc, c)))
3792 gs
3793 end
3794 in
3795 solver gs
3796 end;
3797
3688 mayDelay := false; 3798 mayDelay := false;
3689 3799
3690 app (fn (env, k, s1, s2) => 3800 app (fn (env, k, s1, s2) =>
3691 unifySummaries env (k, normalizeRecordSummary env s1, normalizeRecordSummary env s2) 3801 unifySummaries env (k, normalizeRecordSummary env s1, normalizeRecordSummary env s2)
3692 handle CUnify' err => (ErrorMsg.errorAt (#2 k) "Error in final record unification"; 3802 handle CUnify' err => (ErrorMsg.errorAt (#2 k) "Error in final record unification";
3695 delayedUnifs := []; 3805 delayedUnifs := [];
3696 3806
3697 if ErrorMsg.anyErrors () then 3807 if ErrorMsg.anyErrors () then
3698 () 3808 ()
3699 else 3809 else
3700 app (fn Disjoint (loc, env, denv, c1, c2) =>
3701 (case D.prove env denv (c1, c2, loc) of
3702 [] => ()
3703 | _ =>
3704 (ErrorMsg.errorAt loc "Couldn't prove field name disjointness";
3705 eprefaces' [("Con 1", p_con env c1),
3706 ("Con 2", p_con env c2),
3707 ("Hnormed 1", p_con env (ElabOps.hnormCon env c1)),
3708 ("Hnormed 2", p_con env (ElabOps.hnormCon env c2))]))
3709 | TypeClass (env, c, r, loc) =>
3710 let
3711 fun default () = expError env (Unresolvable (loc, c))
3712
3713 val c = normClassKey env c
3714 in
3715 case E.resolveClass (hnormCon env) env c of
3716 SOME e => r := SOME e
3717 | NONE =>
3718 case #1 (hnormCon env c) of
3719 L'.CApp (f, x) =>
3720 (case (#1 (hnormCon env f), #1 (hnormCon env x)) of
3721 (L'.CKApp (f, _), L'.CRecord (k, xcs)) =>
3722 (case #1 (hnormCon env f) of
3723 L'.CModProj (top_n', [], "folder") =>
3724 if top_n' = top_n then
3725 let
3726 val e = (L'.EModProj (top_n, ["Folder"], "nil"), loc)
3727 val e = (L'.EKApp (e, k), loc)
3728
3729 val (folder, _) = foldr (fn ((x, c), (folder, xcs)) =>
3730 let
3731 val e = (L'.EModProj (top_n, ["Folder"],
3732 "cons"), loc)
3733 val e = (L'.EKApp (e, k), loc)
3734 val e = (L'.ECApp (e,
3735 (L'.CRecord (k, xcs),
3736 loc)), loc)
3737 val e = (L'.ECApp (e, x), loc)
3738 val e = (L'.ECApp (e, c), loc)
3739 val e = (L'.EApp (e, folder), loc)
3740 in
3741 (e, (x, c) :: xcs)
3742 end)
3743 (e, []) xcs
3744 in
3745 r := SOME folder
3746 end
3747 else
3748 default ()
3749 | _ => default ())
3750 | _ => default ())
3751 | _ => default ()
3752 end) gs;
3753
3754 if ErrorMsg.anyErrors () then
3755 ()
3756 else
3757 app (fn f => f ()) (!checks); 3810 app (fn f => f ()) (!checks);
3758 3811
3759 (L'.DFfiStr ("Basis", basis_n, sgn), ErrorMsg.dummySpan) 3812 (L'.DFfiStr ("Basis", basis_n, sgn), ErrorMsg.dummySpan)
3760 :: ds 3813 :: ds
3761 @ (L'.DStr ("Top", top_n, topSgn, topStr), ErrorMsg.dummySpan) 3814 @ (L'.DStr ("Top", top_n, topSgn, topStr), ErrorMsg.dummySpan)