Mercurial > urweb

comparison src/elaborate.sml @ 1303:c7b9a33c26c8

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Hopeful fix for the Great Unification Bug
author Adam Chlipala <adam@chlipala.net>
date Sun, 10 Oct 2010 14:41:03 -0400
parents d008c4c43a0a
children f0afe61a6f8b
comparison
equal deleted inserted replaced
1302:d008c4c43a0a 1303:c7b9a33c26c8
205 str (chr (ord #"A" + n)) 205 str (chr (ord #"A" + n))
206 else 206 else
207 "U" ^ Int.toString (n - 26) 207 "U" ^ Int.toString (n - 26)
208 in 208 in
209 count := n + 1; 209 count := n + 1;
210 (L'.CUnif (loc, k, s, ref NONE), loc) 210 (L'.CUnif (0, loc, k, s, ref NONE), loc)
211 end 211 end
212 212
213 end 213 end
214 214
215 fun elabKind env (k, loc) = 215 fun elabKind env (k, loc) =
493 L'.KUnif (_, _, ref NONE) => true 493 L'.KUnif (_, _, ref NONE) => true
494 | L'.KTupleUnif (_, _, ref NONE) => true 494 | L'.KTupleUnif (_, _, ref NONE) => true
495 | _ => false 495 | _ => false
496 fun cunifsRemain c = 496 fun cunifsRemain c =
497 case c of 497 case c of
498 L'.CUnif (loc, _, _, ref NONE) => SOME loc 498 L'.CUnif (_, loc, _, _, ref NONE) => SOME loc
499 | _ => NONE 499 | _ => NONE
500 500
501 val kunifsInDecl = U.Decl.exists {kind = kunifsRemain, 501 val kunifsInDecl = U.Decl.exists {kind = kunifsRemain,
502 con = fn _ => false, 502 con = fn _ => false,
503 exp = fn _ => false, 503 exp = fn _ => false,
514 str = fn _ => NONE, 514 str = fn _ => NONE,
515 decl = fn _ => NONE} 515 decl = fn _ => NONE}
516 516
517 fun occursCon r = 517 fun occursCon r =
518 U.Con.exists {kind = fn _ => false, 518 U.Con.exists {kind = fn _ => false,
519 con = fn L'.CUnif (_, _, _, r') => r = r' 519 con = fn L'.CUnif (_, _, _, _, r') => r = r'
520 | _ => false} 520 | _ => false}
521 521
522 exception CUnify' of cunify_error 522 exception CUnify' of cunify_error
523
524 exception SynUnif = E.SynUnif
525 523
526 type record_summary = { 524 type record_summary = {
527 fields : (L'.con * L'.con) list, 525 fields : (L'.con * L'.con) list,
528 unifs : (L'.con * L'.con option ref) list, 526 unifs : (L'.con * L'.con option ref) list,
529 others : L'.con list 527 others : L'.con list
586 (case hnormKind (kindof env c) of 584 (case hnormKind (kindof env c) of
587 (L'.KTuple ks, _) => List.nth (ks, n - 1) 585 (L'.KTuple ks, _) => List.nth (ks, n - 1)
588 | k => raise CUnify' (CKindof (k, c, "tuple"))) 586 | k => raise CUnify' (CKindof (k, c, "tuple")))
589 587
590 | L'.CError => kerror 588 | L'.CError => kerror
591 | L'.CUnif (_, k, _, _) => k 589 | L'.CUnif (_, _, k, _, _) => k
592 590
593 | L'.CKAbs (x, c) => (L'.KFun (x, kindof (E.pushKRel env x) c), loc) 591 | L'.CKAbs (x, c) => (L'.KFun (x, kindof (E.pushKRel env x) c), loc)
594 | L'.CKApp (c, k) => 592 | L'.CKApp (c, k) =>
595 (case hnormKind (kindof env c) of 593 (case hnormKind (kindof env c) of
596 (L'.KFun (_, k'), _) => subKindInKind (0, k) k' 594 (L'.KFun (_, k'), _) => subKindInKind (0, k) k'
642 (*(case hnormKind (kindof env c) of 640 (*(case hnormKind (kindof env c) of
643 (L'.KTuple ks, _) => #1 (List.nth (ks, n - 1)) = L'.KUnit 641 (L'.KTuple ks, _) => #1 (List.nth (ks, n - 1)) = L'.KUnit
644 | k => raise CUnify' (CKindof (k, c, "tuple")))*) 642 | k => raise CUnify' (CKindof (k, c, "tuple")))*)
645 643
646 | L'.CError => false 644 | L'.CError => false
647 | L'.CUnif (_, k, _, _) => #1 k = L'.KUnit 645 | L'.CUnif (_, _, k, _, _) => #1 k = L'.KUnit
648 646
649 | L'.CKAbs _ => false 647 | L'.CKAbs _ => false
650 | L'.CKApp _ => false 648 | L'.CKApp _ => false
651 | L'.TKFun _ => false 649 | L'.TKFun _ => false
652 650
699 in 697 in
700 {fields = #fields s1 @ #fields s2, 698 {fields = #fields s1 @ #fields s2,
701 unifs = #unifs s1 @ #unifs s2, 699 unifs = #unifs s1 @ #unifs s2,
702 others = #others s1 @ #others s2} 700 others = #others s1 @ #others s2}
703 end 701 end
704 | (L'.CUnif (_, _, _, ref (SOME c)), _) => recordSummary env c 702 | (L'.CUnif (nl, _, _, _, ref (SOME c)), _) => recordSummary env (E.mliftConInCon nl c)
705 | c' as (L'.CUnif (_, _, _, r), _) => {fields = [], unifs = [(c', r)], others = []} 703 | c' as (L'.CUnif (0, _, _, _, r), _) => {fields = [], unifs = [(c', r)], others = []}
706 | c' => {fields = [], unifs = [], others = [c']} 704 | c' => {fields = [], unifs = [], others = [c']}
707 in 705 in
708 sum 706 sum
709 end 707 end
710 708
733 | _ => false 731 | _ => false
734 732
735 and unifySummaries env (loc, k, s1 : record_summary, s2 : record_summary) = 733 and unifySummaries env (loc, k, s1 : record_summary, s2 : record_summary) =
736 let 734 let
737 (*val () = eprefaces "Summaries" [("loc", PD.string (ErrorMsg.spanToString loc)), 735 (*val () = eprefaces "Summaries" [("loc", PD.string (ErrorMsg.spanToString loc)),
738 ("#1", p_summary env s1), 736 ("#1", p_summary env s1),
739 ("#2", p_summary env s2)]*) 737 ("#2", p_summary env s2)]*)
740 738
741 fun eatMatching p (ls1, ls2) = 739 fun eatMatching p (ls1, ls2) =
742 let 740 let
743 fun em (ls1, ls2, passed1) = 741 fun em (ls1, ls2, passed1) =
744 case ls1 of 742 case ls1 of
920 in 918 in
921 unfold (r1, c1'); 919 unfold (r1, c1');
922 unfold (r2, c2'); 920 unfold (r2, c2');
923 unifyCons env loc r (L'.CConcat (r1, r2), loc) 921 unifyCons env loc r (L'.CConcat (r1, r2), loc)
924 end 922 end
925 | L'.CUnif (_, _, _, ur) => 923 | L'.CUnif (0, _, _, _, ur) =>
926 ur := SOME (L'.CApp ((L'.CApp ((L'.CMap (dom, ran), loc), f), loc), r), loc) 924 ur := SOME (L'.CApp ((L'.CApp ((L'.CMap (dom, ran), loc), f), loc), r), loc)
927 | _ => raise ex 925 | _ => raise ex
928 in 926 in
929 unfold (r, c) 927 unfold (r, c)
930 end 928 end
968 unifyCons' env loc c1 c2 966 unifyCons' env loc c1 c2
969 else 967 else
970 onFail () 968 onFail ()
971 in 969 in
972 case #1 (hnormCon env c2) of 970 case #1 (hnormCon env c2) of
973 L'.CUnif (_, k, _, r) => 971 L'.CUnif (0, _, k, _, r) =>
974 (case #1 (hnormKind k) of 972 (case #1 (hnormKind k) of
975 L'.KTuple ks => 973 L'.KTuple ks =>
976 let 974 let
977 val loc = #2 c2 975 val loc = #2 c2
978 val us = map (fn k => cunif (loc, k)) ks 976 val us = map (fn k => cunif (loc, k)) ks
984 | _ => tryNormal () 982 | _ => tryNormal ()
985 end 983 end
986 | _ => onFail () 984 | _ => onFail ()
987 in 985 in
988 case #1 (hnormCon env c1) of 986 case #1 (hnormCon env c1) of
989 L'.CUnif (_, k, _, r) => 987 L'.CUnif (0, _, k, _, r) =>
990 (case #1 (hnormKind k) of 988 (case #1 (hnormKind k) of
991 L'.KTuple ks => 989 L'.KTuple ks =>
992 let 990 let
993 val loc = #2 c1 991 val loc = #2 c1
994 val us = map (fn k => cunif (loc, k)) ks 992 val us = map (fn k => cunif (loc, k)) ks
1000 | _ => trySnd () 998 | _ => trySnd ()
1001 end 999 end
1002 1000
1003 fun projSpecial2 (c2, n2, onFail) = 1001 fun projSpecial2 (c2, n2, onFail) =
1004 case #1 (hnormCon env c2) of 1002 case #1 (hnormCon env c2) of
1005 L'.CUnif (_, k, _, r) => 1003 L'.CUnif (0, _, k, _, r) =>
1006 (case #1 (hnormKind k) of 1004 (case #1 (hnormKind k) of
1007 L'.KTuple ks => 1005 L'.KTuple ks =>
1008 let 1006 let
1009 val loc = #2 c2 1007 val loc = #2 c2
1010 val us = map (fn k => cunif (loc, k)) ks 1008 val us = map (fn k => cunif (loc, k)) ks
1033 | (L'.CRecord _, _) => isRecord () 1031 | (L'.CRecord _, _) => isRecord ()
1034 | (_, L'.CRecord _) => isRecord () 1032 | (_, L'.CRecord _) => isRecord ()
1035 | (L'.CConcat _, _) => isRecord () 1033 | (L'.CConcat _, _) => isRecord ()
1036 | (_, L'.CConcat _) => isRecord () 1034 | (_, L'.CConcat _) => isRecord ()
1037 1035
1038 | (L'.CUnif (_, k1, _, r1), L'.CUnif (_, k2, _, r2)) => 1036 | (L'.CUnif (nl1, loc1, k1, _, r1), L'.CUnif (nl2, loc2, k2, _, r2)) =>
1039 if r1 = r2 then 1037 if r1 = r2 andalso nl1 = nl2 then
1040 () 1038 ()
1041 else 1039 else if nl1 = 0 then
1042 (unifyKinds env k1 k2; 1040 (unifyKinds env k1 k2;
1043 r1 := SOME c2All) 1041 r1 := SOME c2All)
1044 1042 else if nl2 = 0 then
1045 | (L'.CUnif (_, _, _, r), _) => 1043 (unifyKinds env k1 k2;
1044 r2 := SOME c2All)
1045 else
1046 err (fn _ => TooLifty (loc1, loc2))
1047
1048 | (L'.CUnif (0, _, _, _, r), _) =>
1046 if occursCon r c2All then 1049 if occursCon r c2All then
1047 err COccursCheckFailed 1050 err COccursCheckFailed
1048 else 1051 else
1049 r := SOME c2All 1052 r := SOME c2All
1050 | (_, L'.CUnif (_, _, _, r)) => 1053 | (_, L'.CUnif (0, _, _, _, r)) =>
1051 if occursCon r c1All then 1054 if occursCon r c1All then
1052 err COccursCheckFailed 1055 err COccursCheckFailed
1053 else 1056 else
1054 r := SOME c1All 1057 r := SOME c1All
1055 1058
1165 (case hnormCon env cl of 1168 (case hnormCon env cl of
1166 (L'.CModProj (top_n, [], "folder"), _) => top_n = !top_r 1169 (L'.CModProj (top_n, [], "folder"), _) => top_n = !top_r
1167 | _ => false) 1170 | _ => false)
1168 | _ => false 1171 | _ => false
1169 1172
1173 fun subConInCon env x y =
1174 ElabOps.subConInCon x y
1175 handle SubUnif => (cunifyError env (TooUnify (#2 x, y));
1176 cerror)
1177
1170 fun elabHead (env, denv) infer (e as (_, loc)) t = 1178 fun elabHead (env, denv) infer (e as (_, loc)) t =
1171 let 1179 let
1172 fun unravelKind (t, e) = 1180 fun unravelKind (t, e) =
1173 case hnormCon env t of 1181 case hnormCon env t of
1174 (L'.TKFun (x, t'), _) => 1182 (L'.TKFun (x, t'), _) =>
1193 end 1201 end
1194 | (L'.TCFun (L'.Implicit, x, k, t'), _) => 1202 | (L'.TCFun (L'.Implicit, x, k, t'), _) =>
1195 let 1203 let
1196 val u = cunif (loc, k) 1204 val u = cunif (loc, k)
1197 1205
1198 val t'' = subConInCon (0, u) t' 1206 val t'' = subConInCon env (0, u) t'
1199 in 1207 in
1200 unravel (t'', (L'.ECApp (e, u), loc)) 1208 unravel (t'', (L'.ECApp (e, u), loc))
1201 end 1209 end
1202 | (L'.TFun (dom, ran), _) => 1210 | (L'.TFun (dom, ran), _) =>
1203 let 1211 let
1280 val ((p', pt), (env, bound)) = elabPat (p, (env, bound)) 1288 val ((p', pt), (env, bound)) = elabPat (p, (env, bound))
1281 1289
1282 val k = (L'.KType, loc) 1290 val k = (L'.KType, loc)
1283 val unifs = map (fn _ => cunif (loc, k)) xs 1291 val unifs = map (fn _ => cunif (loc, k)) xs
1284 val nxs = length unifs - 1 1292 val nxs = length unifs - 1
1285 val t = ListUtil.foldli (fn (i, u, t) => subConInCon (nxs - i, u) t) t unifs 1293 val t = ListUtil.foldli (fn (i, u, t) => subConInCon env (nxs - i, u) t) t unifs
1286 val dn = foldl (fn (u, dn) => (L'.CApp (dn, u), loc)) dn unifs 1294 val dn = foldl (fn (u, dn) => (L'.CApp (dn, u), loc)) dn unifs
1287 in 1295 in
1288 ignore (checkPatCon env p' pt t); 1296 ignore (checkPatCon env p' pt t);
1289 (((L'.PCon (dk, pc, unifs, SOME p'), loc), dn), 1297 (((L'.PCon (dk, pc, unifs, SOME p'), loc), dn),
1290 (env, bound)) 1298 (env, bound))
1467 L'.CApp (t, arg) => unapp (t, arg :: acc) 1475 L'.CApp (t, arg) => unapp (t, arg :: acc)
1468 | _ => (t, rev acc) 1476 | _ => (t, rev acc)
1469 1477
1470 val (t1, args) = unapp (hnormCon env q1, []) 1478 val (t1, args) = unapp (hnormCon env q1, [])
1471 val t1 = hnormCon env t1 1479 val t1 = hnormCon env t1
1472 fun doSub t = foldl (fn (arg, t) => subConInCon (0, arg) t) t args 1480 fun doSub t = foldl (fn (arg, t) => subConInCon env (0, arg) t) t args
1473 1481
1474 fun dtype (dtO, names) = 1482 fun dtype (dtO, names) =
1475 let 1483 let
1476 val nameSet = IS.addList (IS.empty, names) 1484 val nameSet = IS.addList (IS.empty, names)
1477 val nameSet = foldl (fn (ps, nameSet) => 1485 val nameSet = foldl (fn (ps, nameSet) =>
1651 val c2 = normClassConstraint env c2 1659 val c2 = normClassConstraint env c2
1652 in 1660 in
1653 (L'.TFun (c1, c2), loc) 1661 (L'.TFun (c1, c2), loc)
1654 end 1662 end
1655 | L'.TCFun (expl, x, k, c1) => (L'.TCFun (expl, x, k, normClassConstraint env c1), loc) 1663 | L'.TCFun (expl, x, k, c1) => (L'.TCFun (expl, x, k, normClassConstraint env c1), loc)
1656 | L'.CUnif (_, _, _, ref (SOME c)) => normClassConstraint env c 1664 | L'.CUnif (nl, _, _, _, ref (SOME c)) => normClassConstraint env (E.mliftConInCon nl c)
1657 | _ => unmodCon env (c, loc) 1665 | _ => unmodCon env (c, loc)
1658 1666
1659 fun findHead e e' = 1667 fun findHead e e' =
1660 let 1668 let
1661 fun findHead (e, _) = 1669 fun findHead (e, _) =
1861 case et' of 1869 case et' of
1862 L'.CError => (eerror, cerror, []) 1870 L'.CError => (eerror, cerror, [])
1863 | L'.TCFun (_, x, k, eb) => 1871 | L'.TCFun (_, x, k, eb) =>
1864 let 1872 let
1865 val () = checkKind env c' ck k 1873 val () = checkKind env c' ck k
1866 val eb' = subConInCon (0, c') eb 1874 val eb' = subConInCon env (0, c') eb
1867 handle SynUnif => (expError env (Unif ("substitution", loc, eb));
1868 cerror)
1869 1875
1870 val ef = (L'.ECApp (e', c'), loc) 1876 val ef = (L'.ECApp (e', c'), loc)
1871 val (ef, eb', gs3) = 1877 val (ef, eb', gs3) =
1872 case findHead e e' of 1878 case findHead e e' of
1873 NONE => (ef, eb', []) 1879 NONE => (ef, eb', [])
3301 | L'.CConcat (c1, c2) => 3307 | L'.CConcat (c1, c2) =>
3302 (case (decompileCon env c1, decompileCon env c2) of 3308 (case (decompileCon env c1, decompileCon env c2) of
3303 (SOME c1, SOME c2) => SOME (L.CConcat (c1, c2), loc) 3309 (SOME c1, SOME c2) => SOME (L.CConcat (c1, c2), loc)
3304 | _ => NONE) 3310 | _ => NONE)
3305 | L'.CUnit => SOME (L.CUnit, loc) 3311 | L'.CUnit => SOME (L.CUnit, loc)
3306 | L'.CUnif (_, _, _, ref (SOME c)) => decompileCon env c 3312 | L'.CUnif (nl, _, _, _, ref (SOME c)) => decompileCon env (E.mliftConInCon nl c)
3307 3313
3308 | _ => NONE 3314 | _ => NONE
3309 3315
3310 fun buildNeeded env sgis = 3316 fun buildNeeded env sgis =
3311 #1 (foldl (fn ((sgi, loc), (nd, env')) => 3317 #1 (foldl (fn ((sgi, loc), (nd, env')) =>