Mercurial > urweb

comparison src/elaborate.sml @ 2049:459ccbf8cd08

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
When unifying constructor-level unification variables, also unify their kinds
author Adam Chlipala <adam@chlipala.net>
date Fri, 01 Aug 2014 16:11:36 -0400
parents 42ae25a354f8
children 834b438d57f3
comparison
equal deleted inserted replaced
2048:4d64af730e35 2049:459ccbf8cd08
1224 else 1224 else
1225 err CScope) 1225 err CScope)
1226 else 1226 else
1227 err (fn _ => TooLifty (loc1, loc2)) 1227 err (fn _ => TooLifty (loc1, loc2))
1228 1228
1229 | (L'.CUnif (0, _, _, _, r as ref (L'.Unknown f)), _) => 1229 | (L'.CUnif (0, _, k1, _, r as ref (L'.Unknown f)), _) =>
1230 if occursCon r c2All then 1230 (unifyKinds env k1 (kindof env c2All);
1231 maybeIsRecord c2 1231 if occursCon r c2All then
1232 else if f c2All then 1232 maybeIsRecord c2
1233 r := L'.Known c2All 1233 else if f c2All then
1234 else 1234 r := L'.Known c2All
1235 err CScope 1235 else
1236 | (_, L'.CUnif (0, _, _, _, r as ref (L'.Unknown f))) => 1236 err CScope)
1237 if occursCon r c1All then 1237 | (_, L'.CUnif (0, _, k2, _, r as ref (L'.Unknown f))) =>
1238 maybeIsRecord c1 1238 (unifyKinds env (kindof env c1All) k2;
1239 else if f c1All then 1239 if occursCon r c1All then
1240 r := L'.Known c1All 1240 maybeIsRecord c1
1241 else 1241 else if f c1All then
1242 err CScope 1242 r := L'.Known c1All
1243 1243 else
1244 | (L'.CUnif (nl, _, _, _, r as ref (L'.Unknown f)), _) => 1244 err CScope)
1245
1246 | (L'.CUnif (nl, _, k1, _, r as ref (L'.Unknown f)), _) =>
1245 if occursCon r c2All then 1247 if occursCon r c2All then
1246 maybeIsRecord c2 1248 maybeIsRecord c2
1247 else 1249 else
1248 (let 1250 (unifyKinds env k1 (kindof env c2All);
1251 let
1249 val sq = squish nl c2All 1252 val sq = squish nl c2All
1250 in 1253 in
1251 if f sq then 1254 if f sq then
1252 r := L'.Known sq 1255 r := L'.Known sq
1253 else 1256 else
1254 err CScope 1257 err CScope
1255 end 1258 end
1256 handle CantSquish => err (fn _ => TooDeep)) 1259 handle CantSquish => err (fn _ => TooDeep))
1257 | (_, L'.CUnif (nl, _, _, _, r as ref (L'.Unknown f))) => 1260 | (_, L'.CUnif (nl, _, k2, _, r as ref (L'.Unknown f))) =>
1258 if occursCon r c1All then 1261 if occursCon r c1All then
1259 maybeIsRecord c1 1262 maybeIsRecord c1
1260 else 1263 else
1261 (let 1264 (unifyKinds env (kindof env c1All) k2;
1265 let
1262 val sq = squish nl c1All 1266 val sq = squish nl c1All
1263 in 1267 in
1264 if f sq then 1268 if f sq then
1265 r := L'.Known sq 1269 r := L'.Known sq
1266 else 1270 else