Mercurial > urweb

comparison src/elaborate.sml @ 92:1a4c51fa615c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
XML tags with contents
author Adam Chlipala <adamc@hcoop.net>
date Thu, 03 Jul 2008 17:02:42 -0400
parents 4327abd52997
children 94afff1ff7f6
comparison
equal deleted inserted replaced
91:4327abd52997 92:1a4c51fa615c
546 546
547 val hnormCon = D.hnormCon 547 val hnormCon = D.hnormCon
548 548
549 fun unifyRecordCons (env, denv) (c1, c2) = 549 fun unifyRecordCons (env, denv) (c1, c2) =
550 let 550 let
551 val k1 = kindof env c1 551 fun rkindof c =
552 val k2 = kindof env c2 552 case kindof env c of
553 (L'.KRecord k, _) => k
554 | _ => raise CUnify' (CKindof c)
555
556 val k1 = rkindof c1
557 val k2 = rkindof c2
553 558
554 val (r1, gs1) = recordSummary (env, denv) c1 559 val (r1, gs1) = recordSummary (env, denv) c1
555 val (r2, gs2) = recordSummary (env, denv) c2 560 val (r2, gs2) = recordSummary (env, denv) c2
556 in 561 in
557 unifyKinds k1 k2; 562 unifyKinds k1 k2;
695 let 700 let
696 fun err f = raise CUnify' (f (c1All, c2All)) 701 fun err f = raise CUnify' (f (c1All, c2All))
697 702
698 fun isRecord () = unifyRecordCons (env, denv) (c1All, c2All) 703 fun isRecord () = unifyRecordCons (env, denv) (c1All, c2All)
699 in 704 in
705 (*eprefaces "unifyCons''" [("c1All", p_con env c1All),
706 ("c2All", p_con env c2All)];*)
707
700 case (c1, c2) of 708 case (c1, c2) of
701 (L'.CUnit, L'.CUnit) => [] 709 (L'.CUnit, L'.CUnit) => []
702 710
703 | (L'.TFun (d1, r1), L'.TFun (d2, r2)) => 711 | (L'.TFun (d1, r1), L'.TFun (d2, r2)) =>
704 unifyCons' (env, denv) d1 d2 712 unifyCons' (env, denv) d1 d2
742 err CIncompatible 750 err CIncompatible
743 751
744 | (L'.CError, _) => [] 752 | (L'.CError, _) => []
745 | (_, L'.CError) => [] 753 | (_, L'.CError) => []
746 754
747 | (L'.CUnif (_, _, _, ref (SOME c1All)), _) => unifyCons' (env, denv) c1All c2All 755 | (L'.CRecord _, _) => isRecord ()
748 | (_, L'.CUnif (_, _, _, ref (SOME c2All))) => unifyCons' (env, denv) c1All c2All 756 | (_, L'.CRecord _) => isRecord ()
757 | (L'.CConcat _, _) => isRecord ()
758 | (_, L'.CConcat _) => isRecord ()
759 (*| (L'.CUnif (_, (L'.KRecord _, _), _, _), _) => isRecord ()
760 | (_, L'.CUnif (_, (L'.KRecord _, _), _, _)) => isRecord ()*)
749 761
750 | (L'.CUnif (_, k1, _, r1), L'.CUnif (_, k2, _, r2)) => 762 | (L'.CUnif (_, k1, _, r1), L'.CUnif (_, k2, _, r2)) =>
751 if r1 = r2 then 763 if r1 = r2 then
752 [] 764 []
753 else 765 else
766 err COccursCheckFailed 778 err COccursCheckFailed
767 else 779 else
768 (r := SOME c1All; 780 (r := SOME c1All;
769 []) 781 [])
770 782
771 | (L'.CRecord _, _) => isRecord ()
772 | (_, L'.CRecord _) => isRecord ()
773 | (L'.CConcat _, _) => isRecord ()
774 | (_, L'.CConcat _) => isRecord ()
775 783
776 | (L'.CFold (dom1, ran1), L'.CFold (dom2, ran2)) => 784 | (L'.CFold (dom1, ran1), L'.CFold (dom2, ran2)) =>
777 (unifyKinds dom1 dom2; 785 (unifyKinds dom1 dom2;
778 unifyKinds ran1 ran2; 786 unifyKinds ran1 ran2;
779 []) 787 [])
790 UnboundExp of ErrorMsg.span * string 798 UnboundExp of ErrorMsg.span * string
791 | UnboundStrInExp of ErrorMsg.span * string 799 | UnboundStrInExp of ErrorMsg.span * string
792 | Unify of L'.exp * L'.con * L'.con * cunify_error 800 | Unify of L'.exp * L'.con * L'.con * cunify_error
793 | Unif of string * L'.con 801 | Unif of string * L'.con
794 | WrongForm of string * L'.exp * L'.con 802 | WrongForm of string * L'.exp * L'.con
803 | IncompatibleCons of L'.con * L'.con
795 804
796 fun expError env err = 805 fun expError env err =
797 case err of 806 case err of
798 UnboundExp (loc, s) => 807 UnboundExp (loc, s) =>
799 ErrorMsg.errorAt loc ("Unbound expression variable " ^ s) 808 ErrorMsg.errorAt loc ("Unbound expression variable " ^ s)
810 eprefaces' [("Con", p_con env c)]) 819 eprefaces' [("Con", p_con env c)])
811 | WrongForm (variety, e, t) => 820 | WrongForm (variety, e, t) =>
812 (ErrorMsg.errorAt (#2 e) ("Expression is not a " ^ variety); 821 (ErrorMsg.errorAt (#2 e) ("Expression is not a " ^ variety);
813 eprefaces' [("Expression", p_exp env e), 822 eprefaces' [("Expression", p_exp env e),
814 ("Type", p_con env t)]) 823 ("Type", p_con env t)])
824 | IncompatibleCons (c1, c2) =>
825 (ErrorMsg.errorAt (#2 c1) "Incompatible constructors";
826 eprefaces' [("Con 1", p_con env c1),
827 ("Con 2", p_con env c2)])
815 828
816 fun checkCon (env, denv) e c1 c2 = 829 fun checkCon (env, denv) e c1 c2 =
817 unifyCons (env, denv) c1 c2 830 unifyCons (env, denv) c1 c2
818 handle CUnify (c1, c2, err) => 831 handle CUnify (c1, c2, err) =>
819 (expError env (Unify (e, c1, c2, err)); 832 (expError env (Unify (e, c1, c2, err));
903 end 916 end
904 in 917 in
905 unravel (t, e) 918 unravel (t, e)
906 end 919 end
907 920
908 fun elabExp (env, denv) (e, loc) = 921 fun elabExp (env, denv) (eAll as (e, loc)) =
909 let 922 let
910 fun doApp (e1, e2) = 923
911 let
912 val (e1', t1, gs1) = elabExp (env, denv) e1
913 val (e1', t1, gs2) = elabHead (env, denv) e1' t1
914 val (e2', t2, gs3) = elabExp (env, denv) e2
915
916 val dom = cunif (loc, ktype)
917 val ran = cunif (loc, ktype)
918 val t = (L'.TFun (dom, ran), dummy)
919
920 val gs4 = checkCon (env, denv) e1' t1 t
921 val gs5 = checkCon (env, denv) e2' t2 dom
922 in
923 ((L'.EApp (e1', e2'), loc), ran, gs1 @ gs2 @ gs3 @ gs4 @ gs5)
924 end
925 in 924 in
925 (*eprefaces "elabExp" [("eAll", SourcePrint.p_exp eAll)];*)
926
926 case e of 927 case e of
927 L.EAnnot (e, t) => 928 L.EAnnot (e, t) =>
928 let 929 let
929 val (e', et, gs1) = elabExp (env, denv) e 930 val (e', et, gs1) = elabExp (env, denv) e
930 val (t', _, gs2) = elabCon (env, denv) t 931 val (t', _, gs2) = elabCon (env, denv) t
1038 val gs1 = unifyCons (env, denv) ns ns' 1039 val gs1 = unifyCons (env, denv) ns ns'
1039 val gs2 = setEmpty ns' 1040 val gs2 = setEmpty ns'
1040 val gs3 = unifyCons (env, denv) ns ns' 1041 val gs3 = unifyCons (env, denv) ns ns'
1041 in 1042 in
1042 gs1 @ gs2 @ gs3 1043 gs1 @ gs2 @ gs3
1043 end 1044 end handle CUnify _ => (expError env (IncompatibleCons (ns, ns'));
1045 [])
1044 1046
1045 val gs7 = doUnify (ns1, ns1') 1047 val gs7 = doUnify (ns1, ns1')
1046 val gs8 = doUnify (ns2, ns2') 1048 val gs8 = doUnify (ns2, ns2')
1047 in 1049 in
1048 (e, t, (loc, env, denv, shared, ctx1) 1050 (e, t, (loc, env, denv, shared, ctx1)