Mercurial > urweb

comparison src/elaborate.sml @ 1304:f0afe61a6f8b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Tweaking unification fix to apply to demo/more
author Adam Chlipala <adam@chlipala.net>
date Sun, 10 Oct 2010 15:37:14 -0400
parents c7b9a33c26c8
children a6fc03d28170
comparison
equal deleted inserted replaced
1303:c7b9a33c26c8 1304:f0afe61a6f8b
652 652
653 val mayDelay = ref false 653 val mayDelay = ref false
654 val delayedUnifs = ref ([] : (ErrorMsg.span * E.env * L'.kind * record_summary * record_summary) list) 654 val delayedUnifs = ref ([] : (ErrorMsg.span * E.env * L'.kind * record_summary * record_summary) list)
655 655
656 val delayedExhaustives = ref ([] : (E.env * L'.con * L'.pat list * ErrorMsg.span) list) 656 val delayedExhaustives = ref ([] : (E.env * L'.con * L'.pat list * ErrorMsg.span) list)
657
658 exception CantSquish
659
660 fun squish by =
661 U.Con.mapB {kind = fn _ => fn k => k,
662 con = fn bound => fn c =>
663 case c of
664 L'.CRel xn =>
665 if xn < bound then
666 c
667 else if bound <= xn andalso xn < bound + by then
668 raise CantSquish
669 else
670 L'.CRel (xn - by)
671 | L'.CUnif _ => raise CantSquish
672 | _ => c,
673 bind = fn (bound, U.Con.RelC _) => bound + 1
674 | (bound, _) => bound} 0
657 675
658 fun unifyRecordCons env (loc, c1, c2) = 676 fun unifyRecordCons env (loc, c1, c2) =
659 let 677 let
660 fun rkindof c = 678 fun rkindof c =
661 case hnormKind (kindof env c) of 679 case hnormKind (kindof env c) of
1054 if occursCon r c1All then 1072 if occursCon r c1All then
1055 err COccursCheckFailed 1073 err COccursCheckFailed
1056 else 1074 else
1057 r := SOME c1All 1075 r := SOME c1All
1058 1076
1077 | (L'.CUnif (nl, _, _, _, r), _) =>
1078 if occursCon r c2All then
1079 err COccursCheckFailed
1080 else
1081 (r := SOME (squish nl c2All)
1082 handle CantSquish => err CIncompatible)
1083 | (_, L'.CUnif (nl, _, _, _, r)) =>
1084 if occursCon r c1All then
1085 err COccursCheckFailed
1086 else
1087 (r := SOME (squish nl c1All)
1088 handle CantSquish => err CIncompatible)
1089
1059 | (L'.CUnit, L'.CUnit) => () 1090 | (L'.CUnit, L'.CUnit) => ()
1060 1091
1061 | (L'.TFun (d1, r1), L'.TFun (d2, r2)) => 1092 | (L'.TFun (d1, r1), L'.TFun (d2, r2)) =>
1062 (unifyCons' env loc d1 d2; 1093 (unifyCons' env loc d1 d2;
1063 unifyCons' env loc r1 r2) 1094 unifyCons' env loc r1 r2)
1288 val ((p', pt), (env, bound)) = elabPat (p, (env, bound)) 1319 val ((p', pt), (env, bound)) = elabPat (p, (env, bound))
1289 1320
1290 val k = (L'.KType, loc) 1321 val k = (L'.KType, loc)
1291 val unifs = map (fn _ => cunif (loc, k)) xs 1322 val unifs = map (fn _ => cunif (loc, k)) xs
1292 val nxs = length unifs - 1 1323 val nxs = length unifs - 1
1293 val t = ListUtil.foldli (fn (i, u, t) => subConInCon env (nxs - i, u) t) t unifs 1324 val t = ListUtil.foldli (fn (i, u, t) => subConInCon env (nxs - i,
1325 E.mliftConInCon (nxs - i) u) t) t unifs
1294 val dn = foldl (fn (u, dn) => (L'.CApp (dn, u), loc)) dn unifs 1326 val dn = foldl (fn (u, dn) => (L'.CApp (dn, u), loc)) dn unifs
1295 in 1327 in
1296 ignore (checkPatCon env p' pt t); 1328 ignore (checkPatCon env p' pt t);
1297 (((L'.PCon (dk, pc, unifs, SOME p'), loc), dn), 1329 (((L'.PCon (dk, pc, unifs, SOME p'), loc), dn),
1298 (env, bound)) 1330 (env, bound))