Mercurial > urweb

comparison src/elaborate.sml @ 1719:0bafdfae2ac7

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Saving proper environments, to use in displaying nested error messages
author Adam Chlipala <adam@chlipala.net>
date Sat, 21 Apr 2012 14:57:00 -0400
parents 16ee7ff7f119
children 5ecf67553da8
comparison
equal deleted inserted replaced
1718:dd12d6d9e9a7 1719:0bafdfae2ac7
84 true) 84 true)
85 handle _ => false 85 handle _ => false
86 86
87 and validateKind env k = validateCon env (L'.CRecord (k, []), ErrorMsg.dummySpan) 87 and validateKind env k = validateCon env (L'.CRecord (k, []), ErrorMsg.dummySpan)
88 88
89 exception KUnify' of kunify_error 89 exception KUnify' of E.env * kunify_error
90 90
91 fun unifyKinds' env (k1All as (k1, _)) (k2All as (k2, _)) = 91 fun unifyKinds' env (k1All as (k1, _)) (k2All as (k2, _)) =
92 let 92 let
93 fun err f = raise KUnify' (f (k1All, k2All)) 93 fun err f = raise KUnify' (env, f (k1All, k2All))
94 in 94 in
95 case (k1, k2) of 95 case (k1, k2) of
96 (L'.KType, L'.KType) => () 96 (L'.KType, L'.KType) => ()
97 | (L'.KUnit, L'.KUnit) => () 97 | (L'.KUnit, L'.KUnit) => ()
98 98
177 end 177 end
178 178
179 | _ => err KIncompatible 179 | _ => err KIncompatible
180 end 180 end
181 181
182 exception KUnify of L'.kind * L'.kind * kunify_error 182 exception KUnify of L'.kind * L'.kind * E.env * kunify_error
183 183
184 fun unifyKinds env k1 k2 = 184 fun unifyKinds env k1 k2 =
185 unifyKinds' env k1 k2 185 unifyKinds' env k1 k2
186 handle KUnify' err => raise KUnify (k1, k2, err) 186 handle KUnify' (env', err) => raise KUnify (k1, k2, env', err)
187 187
188 fun checkKind env c k1 k2 = 188 fun checkKind env c k1 k2 =
189 unifyKinds env k1 k2 189 unifyKinds env k1 k2
190 handle KUnify (k1, k2, err) => 190 handle KUnify (k1, k2, env', err) =>
191 conError env (WrongKind (c, k1, k2, err)) 191 conError env (WrongKind (c, k1, k2, env', err))
192 192
193 val dummy = ErrorMsg.dummySpan 193 val dummy = ErrorMsg.dummySpan
194 194
195 val ktype = (L'.KType, dummy) 195 val ktype = (L'.KType, dummy)
196 val kname = (L'.KName, dummy) 196 val kname = (L'.KName, dummy)
561 fun occursCon r = 561 fun occursCon r =
562 U.Con.exists {kind = fn _ => false, 562 U.Con.exists {kind = fn _ => false,
563 con = fn L'.CUnif (_, _, _, _, r') => r = r' 563 con = fn L'.CUnif (_, _, _, _, r') => r = r'
564 | _ => false} 564 | _ => false}
565 565
566 exception CUnify' of cunify_error 566 exception CUnify' of E.env * cunify_error
567 567
568 type record_summary = { 568 type record_summary = {
569 fields : (L'.con * L'.con) list, 569 fields : (L'.con * L'.con) list,
570 unifs : (L'.con * L'.cunif ref) list, 570 unifs : (L'.con * L'.cunif ref) list,
571 others : L'.con list 571 others : L'.con list
587 concat ((L'.CRecord (ktype, fields), dummy), c) 587 concat ((L'.CRecord (ktype, fields), dummy), c)
588 end 588 end
589 589
590 fun p_summary env s = p_con env (summaryToCon s) 590 fun p_summary env s = p_con env (summaryToCon s)
591 591
592 exception CUnify of L'.con * L'.con * cunify_error 592 exception CUnify of L'.con * L'.con * E.env * cunify_error
593 593
594 fun kindof env (c, loc) = 594 fun kindof env (c, loc) =
595 case c of 595 case c of
596 L'.TFun _ => ktype 596 L'.TFun _ => ktype
597 | L'.TCFun _ => ktype 597 | L'.TCFun _ => ktype
616 616
617 | L'.CApp (c, _) => 617 | L'.CApp (c, _) =>
618 (case hnormKind (kindof env c) of 618 (case hnormKind (kindof env c) of
619 (L'.KArrow (_, k), _) => k 619 (L'.KArrow (_, k), _) => k
620 | (L'.KError, _) => kerror 620 | (L'.KError, _) => kerror
621 | k => raise CUnify' (CKindof (k, c, "arrow"))) 621 | k => raise CUnify' (env, CKindof (k, c, "arrow")))
622 | L'.CAbs (x, k, c) => (L'.KArrow (k, kindof (E.pushCRel env x k) c), loc) 622 | L'.CAbs (x, k, c) => (L'.KArrow (k, kindof (E.pushCRel env x k) c), loc)
623 623
624 624
625 | L'.CName _ => kname 625 | L'.CName _ => kname
626 626
651 val k = (L'.KTupleUnif (loc, ((n, ku) :: nks), r), loc) 651 val k = (L'.KTupleUnif (loc, ((n, ku) :: nks), r), loc)
652 in 652 in
653 r := L'.KKnown k; 653 r := L'.KKnown k;
654 k 654 k
655 end) 655 end)
656 | k => raise CUnify' (CKindof (k, c, "tuple"))) 656 | k => raise CUnify' (env, CKindof (k, c, "tuple")))
657 657
658 | L'.CError => kerror 658 | L'.CError => kerror
659 | L'.CUnif (_, _, k, _, _) => k 659 | L'.CUnif (_, _, k, _, _) => k
660 660
661 | L'.CKAbs (x, c) => (L'.KFun (x, kindof (E.pushKRel env x) c), loc) 661 | L'.CKAbs (x, c) => (L'.KFun (x, kindof (E.pushKRel env x) c), loc)
662 | L'.CKApp (c, k) => 662 | L'.CKApp (c, k) =>
663 (case hnormKind (kindof env c) of 663 (case hnormKind (kindof env c) of
664 (L'.KFun (_, k'), _) => subKindInKind (0, k) k' 664 (L'.KFun (_, k'), _) => subKindInKind (0, k) k'
665 | k => raise CUnify' (CKindof (k, c, "kapp"))) 665 | k => raise CUnify' (env, CKindof (k, c, "kapp")))
666 | L'.TKFun _ => ktype 666 | L'.TKFun _ => ktype
667 667
668 exception GuessFailure 668 exception GuessFailure
669 669
670 fun isUnitCon env (c, loc) = 670 fun isUnitCon env (c, loc) =
756 val k = kunif' f (#2 c) 756 val k = kunif' f (#2 c)
757 in 757 in
758 r := L'.KKnown (L'.KRecord k, #2 c); 758 r := L'.KKnown (L'.KRecord k, #2 c);
759 k 759 k
760 end 760 end
761 | k => raise CUnify' (CKindof (k, c, "record")) 761 | k => raise CUnify' (env, CKindof (k, c, "record"))
762 762
763 val k1 = rkindof c1 763 val k1 = rkindof c1
764 val k2 = rkindof c2 764 val k2 = rkindof c2
765 765
766 val r1 = recordSummary env c1 766 val r1 = recordSummary env c1
985 | SOME (_, c2) => 985 | SOME (_, c2) =>
986 if consEq env loc (c1, c2) then 986 if consEq env loc (c1, c2) then
987 findPointwise fs1 987 findPointwise fs1
988 else 988 else
989 SOME (nm1, c1, c2, (unifyCons env loc c1 c2; NONE) 989 SOME (nm1, c1, c2, (unifyCons env loc c1 c2; NONE)
990 handle CUnify (_, _, err) => (reducedSummaries := NONE; 990 handle CUnify (_, _, env', err) => (reducedSummaries := NONE;
991 SOME err)) 991 SOME (env', err)))
992 in 992 in
993 raise CUnify' (CRecordFailure (unsummarize s1, unsummarize s2, findPointwise (#fields s1))) 993 raise CUnify' (env, CRecordFailure (unsummarize s1, unsummarize s2, findPointwise (#fields s1)))
994 end 994 end
995 995
996 fun default () = if !mayDelay then 996 fun default () = if !mayDelay then
997 delayedUnifs := (loc, env, k, s1, s2) :: !delayedUnifs 997 delayedUnifs := (loc, env, k, s1, s2) :: !delayedUnifs
998 else 998 else
1007 let 1007 let
1008 val c = summaryToCon {fields = fs1, unifs = unifs1, others = others1} 1008 val c = summaryToCon {fields = fs1, unifs = unifs1, others = others1}
1009 in 1009 in
1010 if occursCon r c then 1010 if occursCon r c then
1011 (reducedSummaries := NONE; 1011 (reducedSummaries := NONE;
1012 raise CUnify' (COccursCheckFailed (cr, c))) 1012 raise CUnify' (env, COccursCheckFailed (cr, c)))
1013 else 1013 else
1014 let 1014 let
1015 val sq = squish nl c 1015 val sq = squish nl c
1016 in 1016 in
1017 if not (f sq) then 1017 if not (f sq) then
1025 let 1025 let
1026 val c = summaryToCon {fields = fs2, unifs = unifs2, others = others2} 1026 val c = summaryToCon {fields = fs2, unifs = unifs2, others = others2}
1027 in 1027 in
1028 if occursCon r c then 1028 if occursCon r c then
1029 (reducedSummaries := NONE; 1029 (reducedSummaries := NONE;
1030 raise CUnify' (COccursCheckFailed (cr, c))) 1030 raise CUnify' (env, COccursCheckFailed (cr, c)))
1031 else 1031 else
1032 let 1032 let
1033 val sq = squish nl c 1033 val sq = squish nl c
1034 in 1034 in
1035 if not (f sq) then 1035 if not (f sq) then
1117 handle ex => guessMap env loc (c1, c2, ex) 1117 handle ex => guessMap env loc (c1, c2, ex)
1118 end 1118 end
1119 1119
1120 and unifyCons'' env loc (c1All as (c1, _)) (c2All as (c2, _)) = 1120 and unifyCons'' env loc (c1All as (c1, _)) (c2All as (c2, _)) =
1121 let 1121 let
1122 fun err f = raise CUnify' (f (c1All, c2All)) 1122 fun err f = raise CUnify' (env, f (c1All, c2All))
1123 1123
1124 fun projSpecial1 (c1, n1, onFail) = 1124 fun projSpecial1 (c1, n1, onFail) =
1125 let 1125 let
1126 fun trySnd () = 1126 fun trySnd () =
1127 case #1 (hnormCon env c2All) of 1127 case #1 (hnormCon env c2All) of
1342 ("c2", p_con env c2All)]*) 1342 ("c2", p_con env c2All)]*)
1343 end 1343 end
1344 1344
1345 and unifyCons env loc c1 c2 = 1345 and unifyCons env loc c1 c2 =
1346 unifyCons' env loc c1 c2 1346 unifyCons' env loc c1 c2
1347 handle CUnify' err => raise CUnify (c1, c2, err) 1347 handle CUnify' (env', err) => raise CUnify (c1, c2, env', err)
1348 | KUnify args => raise CUnify (c1, c2, CKind args) 1348 | KUnify (arg as {3 = env', ...}) => raise CUnify (c1, c2, env', CKind arg)
1349 1349
1350 fun checkCon env e c1 c2 = 1350 fun checkCon env e c1 c2 =
1351 unifyCons env (#2 e) c1 c2 1351 unifyCons env (#2 e) c1 c2
1352 handle CUnify (c1, c2, err) => 1352 handle CUnify (c1, c2, env', err) =>
1353 expError env (Unify (e, c1, c2, err)) 1353 expError env (Unify (e, c1, c2, env', err))
1354 1354
1355 fun checkPatCon env p c1 c2 = 1355 fun checkPatCon env p c1 c2 =
1356 unifyCons env (#2 p) c1 c2 1356 unifyCons env (#2 p) c1 c2
1357 handle CUnify (c1, c2, err) => 1357 handle CUnify (c1, c2, env', err) =>
1358 expError env (PatUnify (p, c1, c2, err)) 1358 expError env (PatUnify (p, c1, c2, env', err))
1359 1359
1360 fun primType env p = 1360 fun primType env p =
1361 case p of 1361 case p of
1362 P.Int _ => !int 1362 P.Int _ => !int
1363 | P.Float _ => !float 1363 | P.Float _ => !float
2577 val old = c' 2577 val old = c'
2578 val c' = normClassConstraint env c' 2578 val c' = normClassConstraint env c'
2579 val (env', n) = E.pushENamed env x c' 2579 val (env', n) = E.pushENamed env x c'
2580 in 2580 in
2581 (unifyKinds env ck ktype 2581 (unifyKinds env ck ktype
2582 handle KUnify ue => strError env (NotType (loc, ck, ue))); 2582 handle KUnify arg => strError env (NotType (loc, ck, arg)));
2583 2583
2584 ([(L'.SgiVal (x, n, c'), loc)], (env', denv, gs' @ gs)) 2584 ([(L'.SgiVal (x, n, c'), loc)], (env', denv, gs' @ gs))
2585 end 2585 end
2586 2586
2587 | L.SgiTable (x, c, pe, ce) => 2587 | L.SgiTable (x, c, pe, ce) =>
3054 let 3054 let
3055 fun found (x', n1, k1, co1) = 3055 fun found (x', n1, k1, co1) =
3056 if x = x' then 3056 if x = x' then
3057 let 3057 let
3058 val () = unifyKinds env k1 k2 3058 val () = unifyKinds env k1 k2
3059 handle KUnify (k1, k2, err) => 3059 handle KUnify (k1, k2, env', err) =>
3060 sgnError env (SgiWrongKind (loc, sgi1All, k1, 3060 sgnError env (SgiWrongKind (loc, sgi1All, k1,
3061 sgi2All, k2, err)) 3061 sgi2All, k2, env', err))
3062 val env = E.pushCNamedAs env x n1 k1 co1 3062 val env = E.pushCNamedAs env x n1 k1 co1
3063 in 3063 in
3064 SOME (if n1 = n2 then 3064 SOME (if n1 = n2 then
3065 env 3065 env
3066 else 3066 else
3123 SOME env 3123 SOME env
3124 end 3124 end
3125 in 3125 in
3126 (unifyCons env loc c1 c2; 3126 (unifyCons env loc c1 c2;
3127 good ()) 3127 good ())
3128 handle CUnify (c1, c2, err) => 3128 handle CUnify (c1, c2, env', err) =>
3129 (sgnError env (SgiWrongCon (loc, sgi1All, c1, 3129 (sgnError env (SgiWrongCon (loc, sgi1All, c1,
3130 sgi2All, c2, err)); 3130 sgi2All, c2, env', err));
3131 good ()) 3131 good ())
3132 end 3132 end
3133 else 3133 else
3134 NONE 3134 NONE
3135 in 3135 in
3249 SOME env 3249 SOME env
3250 end 3250 end
3251 in 3251 in
3252 (unifyCons env loc t1 t2; 3252 (unifyCons env loc t1 t2;
3253 good ()) 3253 good ())
3254 handle CUnify (c1, c2, err) => 3254 handle CUnify (c1, c2, env', err) =>
3255 (sgnError env (SgiWrongCon (loc, sgi1All, c1, sgi2All, c2, err)); 3255 (sgnError env (SgiWrongCon (loc, sgi1All, c1, sgi2All, c2, env', err));
3256 good ()) 3256 good ())
3257 end 3257 end
3258 else 3258 else
3259 NONE 3259 NONE
3260 3260
3270 ("c1", p_con env c1), 3270 ("c1", p_con env c1),
3271 ("c2", p_con env c2), 3271 ("c2", p_con env c2),
3272 ("c2'", p_con env (sub2 c2))];*) 3272 ("c2'", p_con env (sub2 c2))];*)
3273 unifyCons env loc c1 (sub2 c2); 3273 unifyCons env loc c1 (sub2 c2);
3274 SOME env) 3274 SOME env)
3275 handle CUnify (c1, c2, err) => 3275 handle CUnify (c1, c2, env', err) =>
3276 (sgnError env (SgiWrongCon (loc, sgi1All, c1, sgi2All, c2, err)); 3276 (sgnError env (SgiWrongCon (loc, sgi1All, c1, sgi2All, c2, env', err));
3277 SOME env) 3277 SOME env)
3278 else 3278 else
3279 NONE 3279 NONE
3280 | _ => NONE) 3280 | _ => NONE)
3281 3281
3338 let 3338 let
3339 fun found (x', n1, k1, co) = 3339 fun found (x', n1, k1, co) =
3340 if x = x' then 3340 if x = x' then
3341 let 3341 let
3342 val () = unifyKinds env k1 k2 3342 val () = unifyKinds env k1 k2
3343 handle KUnify (k1, k2, err) => 3343 handle KUnify (k1, k2, env', err) =>
3344 sgnError env (SgiWrongKind (loc, sgi1All, k1, 3344 sgnError env (SgiWrongKind (loc, sgi1All, k1,
3345 sgi2All, k2, err)) 3345 sgi2All, k2, env', err))
3346 3346
3347 val env = E.pushCNamedAs env x n1 k1 co 3347 val env = E.pushCNamedAs env x n1 k1 co
3348 in 3348 in
3349 SOME (if n1 = n2 then 3349 SOME (if n1 = n2 then
3350 env 3350 env
3365 let 3365 let
3366 fun found (x', n1, k1, c1) = 3366 fun found (x', n1, k1, c1) =
3367 if x = x' then 3367 if x = x' then
3368 let 3368 let
3369 val () = unifyKinds env k1 k2 3369 val () = unifyKinds env k1 k2
3370 handle KUnify (k1, k2, err) => 3370 handle KUnify (k1, k2, env', err) =>
3371 sgnError env (SgiWrongKind (loc, sgi1All, k1, 3371 sgnError env (SgiWrongKind (loc, sgi1All, k1,
3372 sgi2All, k2, err)) 3372 sgi2All, k2, env', err))
3373 3373
3374 val c2 = sub2 c2 3374 val c2 = sub2 c2
3375 3375
3376 fun good () = 3376 fun good () =
3377 let 3377 let
3385 SOME env 3385 SOME env
3386 end 3386 end
3387 in 3387 in
3388 (unifyCons env loc c1 c2; 3388 (unifyCons env loc c1 c2;
3389 good ()) 3389 good ())
3390 handle CUnify (c1, c2, err) => 3390 handle CUnify (c1, c2, env', err) =>
3391 (sgnError env (SgiWrongCon (loc, sgi1All, c1, 3391 (sgnError env (SgiWrongCon (loc, sgi1All, c1,
3392 sgi2All, c2, err)); 3392 sgi2All, c2, env', err));
3393 good ()) 3393 good ())
3394 end 3394 end
3395 else 3395 else
3396 NONE 3396 NONE
3397 in 3397 in
4628 if ErrorMsg.anyErrors () then 4628 if ErrorMsg.anyErrors () then
4629 () 4629 ()
4630 else 4630 else
4631 (app (fn (loc, env, k, s1, s2) => 4631 (app (fn (loc, env, k, s1, s2) =>
4632 unifySummaries env (loc, k, normalizeRecordSummary env s1, normalizeRecordSummary env s2) 4632 unifySummaries env (loc, k, normalizeRecordSummary env s1, normalizeRecordSummary env s2)
4633 handle CUnify' err => (ErrorMsg.errorAt loc "Error in final record unification"; 4633 handle CUnify' (env', err) => (ErrorMsg.errorAt loc "Error in final record unification";
4634 cunifyError env err; 4634 cunifyError env' err;
4635 case !reducedSummaries of 4635 case !reducedSummaries of
4636 NONE => () 4636 NONE => ()
4637 | SOME (s1, s2) => 4637 | SOME (s1, s2) =>
4638 (ErrorMsg.errorAt loc "Stuck unifying these records after canceling matching pieces:"; 4638 (ErrorMsg.errorAt loc "Stuck unifying these records after canceling matching pieces:";
4639 eprefaces' [("Have", s1), 4639 eprefaces' [("Have", s1),
4640 ("Need", s2)]))) 4640 ("Need", s2)])))
4641 (!delayedUnifs); 4641 (!delayedUnifs);
4642 delayedUnifs := []); 4642 delayedUnifs := []);
4643 4643
4644 if ErrorMsg.anyErrors () then 4644 if ErrorMsg.anyErrors () then
4645 () 4645 ()