Mercurial > urweb

comparison src/elaborate.sml @ 34:44b5405e74c7

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Elaborating module projection
author Adam Chlipala <adamc@hcoop.net>
date Tue, 17 Jun 2008 16:38:54 -0400
parents 535c324f0b35
children 1dfbd9e3e790
comparison
equal deleted inserted replaced
33:535c324f0b35 34:44b5405e74c7
106 unifyKinds' k1 k2 106 unifyKinds' k1 k2
107 handle KUnify' err => raise KUnify (k1, k2, err) 107 handle KUnify' err => raise KUnify (k1, k2, err)
108 108
109 datatype con_error = 109 datatype con_error =
110 UnboundCon of ErrorMsg.span * string 110 UnboundCon of ErrorMsg.span * string
111 | UnboundStrInCon of ErrorMsg.span * string
111 | WrongKind of L'.con * L'.kind * L'.kind * kunify_error 112 | WrongKind of L'.con * L'.kind * L'.kind * kunify_error
112 113
113 fun conError env err = 114 fun conError env err =
114 case err of 115 case err of
115 UnboundCon (loc, s) => 116 UnboundCon (loc, s) =>
116 ErrorMsg.errorAt loc ("Unbound constructor variable " ^ s) 117 ErrorMsg.errorAt loc ("Unbound constructor variable " ^ s)
118 | UnboundStrInCon (loc, s) =>
119 ErrorMsg.errorAt loc ("Unbound structure " ^ s)
117 | WrongKind (c, k1, k2, kerr) => 120 | WrongKind (c, k1, k2, kerr) =>
118 (ErrorMsg.errorAt (#2 c) "Wrong kind"; 121 (ErrorMsg.errorAt (#2 c) "Wrong kind";
119 eprefaces' [("Constructor", p_con env c), 122 eprefaces' [("Constructor", p_con env c),
120 ("Have kind", p_kind k1), 123 ("Have kind", p_kind k1),
121 ("Need kind", p_kind k2)]; 124 ("Need kind", p_kind k2)];
223 in 226 in
224 checkKind env c' ck k; 227 checkKind env c' ck k;
225 ((L'.TRecord c', loc), ktype) 228 ((L'.TRecord c', loc), ktype)
226 end 229 end
227 230
228 | L.CVar s => 231 | L.CVar ([], s) =>
229 (case E.lookupC env s of 232 (case E.lookupC env s of
230 E.NotBound => 233 E.NotBound =>
231 (conError env (UnboundCon (loc, s)); 234 (conError env (UnboundCon (loc, s));
232 (cerror, kerror)) 235 (cerror, kerror))
233 | E.Rel (n, k) => 236 | E.Rel (n, k) =>
234 ((L'.CRel n, loc), k) 237 ((L'.CRel n, loc), k)
235 | E.Named (n, k) => 238 | E.Named (n, k) =>
236 ((L'.CNamed n, loc), k)) 239 ((L'.CNamed n, loc), k))
240 | L.CVar (m1 :: ms, s) =>
241 (case E.lookupStr env m1 of
242 NONE => (conError env (UnboundStrInCon (loc, s));
243 (cerror, kerror))
244 | SOME (n, sgn) =>
245 let
246 val (str, sgn) = foldl (fn (m, (str, sgn)) =>
247 case E.projectStr env {sgn = sgn, str = str, field = m} of
248 NONE => (conError env (UnboundStrInCon (loc, m));
249 (strerror, sgnerror))
250 | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
251 ((L'.StrVar n, loc), sgn) ms
252
253 val k = case E.projectCon env {sgn = sgn, str = str, field = s} of
254 NONE => (conError env (UnboundCon (loc, s));
255 kerror)
256 | SOME (k, _) => k
257 in
258 ((L'.CModProj (n, ms, s), loc), k)
259 end)
260
237 | L.CApp (c1, c2) => 261 | L.CApp (c1, c2) =>
238 let 262 let
239 val (c1', k1) = elabCon env c1 263 val (c1', k1) = elabCon env c1
240 val (c2', k2) = elabCon env c2 264 val (c2', k2) = elabCon env c2
241 val dom = kunif () 265 val dom = kunif ()
402 | L'.TCFun _ => ktype 426 | L'.TCFun _ => ktype
403 | L'.TRecord _ => ktype 427 | L'.TRecord _ => ktype
404 428
405 | L'.CRel xn => #2 (E.lookupCRel env xn) 429 | L'.CRel xn => #2 (E.lookupCRel env xn)
406 | L'.CNamed xn => #2 (E.lookupCNamed env xn) 430 | L'.CNamed xn => #2 (E.lookupCNamed env xn)
431 | L'.CModProj (n, ms, x) =>
432 let
433 val (_, sgn) = E.lookupStrNamed env n
434 val (str, sgn) = foldl (fn (m, (str, sgn)) =>
435 case E.projectStr env {sgn = sgn, str = str, field = m} of
436 NONE => raise Fail "kindof: Unknown substructure"
437 | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
438 ((L'.StrVar n, loc), sgn) ms
439 in
440 case E.projectCon env {sgn = sgn, str = str, field = x} of
441 NONE => raise Fail "kindof: Unknown con in structure"
442 | SOME (k, _) => k
443 end
444
407 | L'.CApp (c, _) => 445 | L'.CApp (c, _) =>
408 (case #1 (hnormKind (kindof env c)) of 446 (case #1 (hnormKind (kindof env c)) of
409 L'.KArrow (_, k) => k 447 L'.KArrow (_, k) => k
410 | L'.KError => kerror 448 | L'.KError => kerror
411 | _ => raise CUnify' (CKindof c)) 449 | _ => raise CUnify' (CKindof c))
539 pairOffUnifs (rest1, rest2)) 577 pairOffUnifs (rest1, rest2))
540 in 578 in
541 pairOffUnifs (unifs1, unifs2) 579 pairOffUnifs (unifs1, unifs2)
542 end 580 end
543 581
544 and hnormCon env (cAll as (c, _)) = 582 and hnormCon env (cAll as (c, loc)) =
545 case c of 583 case c of
546 L'.CUnif (_, _, ref (SOME c)) => hnormCon env c 584 L'.CUnif (_, _, ref (SOME c)) => hnormCon env c
547 585
548 | L'.CNamed xn => 586 | L'.CNamed xn =>
549 (case E.lookupCNamed env xn of 587 (case E.lookupCNamed env xn of
550 (_, _, SOME c') => hnormCon env c' 588 (_, _, SOME c') => hnormCon env c'
551 | _ => cAll) 589 | _ => cAll)
590
591 | L'.CModProj (n, ms, x) =>
592 let
593 val (_, sgn) = E.lookupStrNamed env n
594 val (str, sgn) = foldl (fn (m, (str, sgn)) =>
595 case E.projectStr env {sgn = sgn, str = str, field = m} of
596 NONE => raise Fail "hnormCon: Unknown substructure"
597 | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
598 ((L'.StrVar n, loc), sgn) ms
599 in
600 case E.projectCon env {sgn = sgn, str = str, field = x} of
601 NONE => raise Fail "kindof: Unknown con in structure"
602 | SOME (_, NONE) => cAll
603 | SOME (_, SOME c) => hnormCon env c
604 end
552 605
553 | L'.CApp (c1, c2) => 606 | L'.CApp (c1, c2) =>
554 (case hnormCon env c1 of 607 (case hnormCon env c1 of
555 (L'.CAbs (_, _, cb), _) => 608 (L'.CAbs (_, _, cb), _) =>
556 ((hnormCon env (subConInCon (0, c2) cb)) 609 ((hnormCon env (subConInCon (0, c2) cb))
608 if n1 = n2 then 661 if n1 = n2 then
609 () 662 ()
610 else 663 else
611 err CIncompatible 664 err CIncompatible
612 665
666 | (L'.CModProj (n1, ms1, x1), L'.CModProj (n2, ms2, x2)) =>
667 if n1 = n2 andalso ms1 = ms2 andalso x1 = x2 then
668 ()
669 else
670 err CIncompatible
671
613 | (L'.CError, _) => () 672 | (L'.CError, _) => ()
614 | (_, L'.CError) => () 673 | (_, L'.CError) => ()
615 674
616 | (L'.CUnif (_, _, ref (SOME c1All)), _) => unifyCons' env c1All c2All 675 | (L'.CUnif (_, _, ref (SOME c1All)), _) => unifyCons' env c1All c2All
617 | (_, L'.CUnif (_, _, ref (SOME c2All))) => unifyCons' env c1All c2All 676 | (_, L'.CUnif (_, _, ref (SOME c2All))) => unifyCons' env c1All c2All
647 handle CUnify' err => raise CUnify (c1, c2, err) 706 handle CUnify' err => raise CUnify (c1, c2, err)
648 | KUnify args => raise CUnify (c1, c2, CKind args) 707 | KUnify args => raise CUnify (c1, c2, CKind args)
649 708
650 datatype exp_error = 709 datatype exp_error =
651 UnboundExp of ErrorMsg.span * string 710 UnboundExp of ErrorMsg.span * string
711 | UnboundStrInExp of ErrorMsg.span * string
652 | Unify of L'.exp * L'.con * L'.con * cunify_error 712 | Unify of L'.exp * L'.con * L'.con * cunify_error
653 | Unif of string * L'.con 713 | Unif of string * L'.con
654 | WrongForm of string * L'.exp * L'.con 714 | WrongForm of string * L'.exp * L'.con
655 715
656 fun expError env err = 716 fun expError env err =
657 case err of 717 case err of
658 UnboundExp (loc, s) => 718 UnboundExp (loc, s) =>
659 ErrorMsg.errorAt loc ("Unbound expression variable " ^ s) 719 ErrorMsg.errorAt loc ("Unbound expression variable " ^ s)
720 | UnboundStrInExp (loc, s) =>
721 ErrorMsg.errorAt loc ("Unbound structure " ^ s)
660 | Unify (e, c1, c2, uerr) => 722 | Unify (e, c1, c2, uerr) =>
661 (ErrorMsg.errorAt (#2 e) "Unification failure"; 723 (ErrorMsg.errorAt (#2 e) "Unification failure";
662 eprefaces' [("Expression", p_exp env e), 724 eprefaces' [("Expression", p_exp env e),
663 ("Have con", p_con env c1), 725 ("Have con", p_con env c1),
664 ("Need con", p_con env c2)]; 726 ("Need con", p_con env c2)];
693 fun typeof env (e, loc) = 755 fun typeof env (e, loc) =
694 case e of 756 case e of
695 L'.EPrim p => (primType env p, loc) 757 L'.EPrim p => (primType env p, loc)
696 | L'.ERel n => #2 (E.lookupERel env n) 758 | L'.ERel n => #2 (E.lookupERel env n)
697 | L'.ENamed n => #2 (E.lookupENamed env n) 759 | L'.ENamed n => #2 (E.lookupENamed env n)
760 | L'.EModProj (n, ms, x) =>
761 let
762 val (_, sgn) = E.lookupStrNamed env n
763 val (str, sgn) = foldl (fn (m, (str, sgn)) =>
764 case E.projectStr env {sgn = sgn, str = str, field = m} of
765 NONE => raise Fail "kindof: Unknown substructure"
766 | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
767 ((L'.StrVar n, loc), sgn) ms
768 in
769 case E.projectVal env {sgn = sgn, str = str, field = x} of
770 NONE => raise Fail "typeof: Unknown val in structure"
771 | SOME t => t
772 end
773
698 | L'.EApp (e1, _) => 774 | L'.EApp (e1, _) =>
699 (case #1 (typeof env e1) of 775 (case #1 (typeof env e1) of
700 L'.TFun (_, c) => c 776 L'.TFun (_, c) => c
701 | _ => raise Fail "typeof: Bad EApp") 777 | _ => raise Fail "typeof: Bad EApp")
702 | L'.EAbs (_, _, ran, _) => ran 778 | L'.EAbs (_, _, ran, _) => ran
737 checkCon env e' et t'; 813 checkCon env e' et t';
738 (e', t') 814 (e', t')
739 end 815 end
740 816
741 | L.EPrim p => ((L'.EPrim p, loc), (primType env p, loc)) 817 | L.EPrim p => ((L'.EPrim p, loc), (primType env p, loc))
742 | L.EVar s => 818 | L.EVar ([], s) =>
743 (case E.lookupE env s of 819 (case E.lookupE env s of
744 E.NotBound => 820 E.NotBound =>
745 (expError env (UnboundExp (loc, s)); 821 (expError env (UnboundExp (loc, s));
746 (eerror, cerror)) 822 (eerror, cerror))
747 | E.Rel (n, t) => ((L'.ERel n, loc), t) 823 | E.Rel (n, t) => ((L'.ERel n, loc), t)
748 | E.Named (n, t) => ((L'.ENamed n, loc), t)) 824 | E.Named (n, t) => ((L'.ENamed n, loc), t))
825 | L.EVar (m1 :: ms, s) =>
826 (case E.lookupStr env m1 of
827 NONE => (expError env (UnboundStrInExp (loc, s));
828 (eerror, cerror))
829 | SOME (n, sgn) =>
830 let
831 val (str, sgn) = foldl (fn (m, (str, sgn)) =>
832 case E.projectStr env {sgn = sgn, str = str, field = m} of
833 NONE => (conError env (UnboundStrInCon (loc, m));
834 (strerror, sgnerror))
835 | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
836 ((L'.StrVar n, loc), sgn) ms
837
838 val t = case E.projectVal env {sgn = sgn, str = str, field = s} of
839 NONE => (expError env (UnboundExp (loc, s));
840 cerror)
841 | SOME t => t
842 in
843 ((L'.EModProj (n, ms, s), loc), t)
844 end)
845
749 | L.EApp (e1, e2) => 846 | L.EApp (e1, e2) =>
750 let 847 let
751 val (e1', t1) = elabExp env e1 848 val (e1', t1) = elabExp env e1
752 val (e1', t1) = elabHead env e1' t1 849 val (e1', t1) = elabHead env e1' t1
753 val (e2', t2) = elabExp env e2 850 val (e2', t2) = elabExp env e2
1207 (case E.lookupStr env x of 1304 (case E.lookupStr env x of
1208 NONE => 1305 NONE =>
1209 (strError env (UnboundStr (loc, x)); 1306 (strError env (UnboundStr (loc, x));
1210 (strerror, sgnerror)) 1307 (strerror, sgnerror))
1211 | SOME (n, sgn) => ((L'.StrVar n, loc), sgn)) 1308 | SOME (n, sgn) => ((L'.StrVar n, loc), sgn))
1309 | L.StrProj (str, x) =>
1310 let
1311 val (str', sgn) = elabStr env str
1312 in
1313 case E.projectStr env {str = str', sgn = sgn, field = x} of
1314 NONE => (strError env (UnboundStr (loc, x));
1315 (strerror, sgnerror))
1316 | SOME sgn => ((L'.StrProj (str', x), loc), sgn)
1317 end
1212 1318
1213 val elabFile = ListUtil.foldlMap elabDecl 1319 val elabFile = ListUtil.foldlMap elabDecl
1214 1320
1215 end 1321 end