Mercurial > urweb
comparison src/elaborate.sml @ 2044:42ae25a354f8
Retweak the last tweak to allow type inference to succeed in a strict superset of the places where it used to succeed
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Tue, 29 Jul 2014 14:46:06 -0400 |
parents | e762c96fffb7 |
children | 459ccbf8cd08 |
comparison
equal
deleted
inserted
replaced
2043:e762c96fffb7 | 2044:42ae25a354f8 |
---|---|
1 (* Copyright (c) 2008-2013, Adam Chlipala | 1 (* Copyright (c) 2008-2014, Adam Chlipala |
2 * All rights reserved. | 2 * All rights reserved. |
3 * | 3 * |
4 * Redistribution and use in source and binary forms, with or without | 4 * Redistribution and use in source and binary forms, with or without |
5 * modification, are permitted provided that the following conditions are met: | 5 * modification, are permitted provided that the following conditions are met: |
6 * | 6 * |
1189 fun isRecord () = | 1189 fun isRecord () = |
1190 case (c1, c2) of | 1190 case (c1, c2) of |
1191 (L'.CProj (c1, n1), _) => projSpecial1 (c1, n1, isRecord') | 1191 (L'.CProj (c1, n1), _) => projSpecial1 (c1, n1, isRecord') |
1192 | (_, L'.CProj (c2, n2)) => projSpecial2 (c2, n2, isRecord') | 1192 | (_, L'.CProj (c2, n2)) => projSpecial2 (c2, n2, isRecord') |
1193 | _ => isRecord' () | 1193 | _ => isRecord' () |
1194 | |
1195 fun maybeIsRecord c = | |
1196 case c of | |
1197 L'.CRecord _ => isRecord () | |
1198 | L'.CConcat _ => isRecord () | |
1199 | _ => err COccursCheckFailed | |
1194 in | 1200 in |
1195 (*eprefaces "unifyCons''" [("c1", p_con env c1All), | 1201 (*eprefaces "unifyCons''" [("c1", p_con env c1All), |
1196 ("c2", p_con env c2All)];*) | 1202 ("c2", p_con env c2All)];*) |
1197 | 1203 |
1198 (case (c1, c2) of | 1204 (case (c1, c2) of |
1218 else | 1224 else |
1219 err CScope) | 1225 err CScope) |
1220 else | 1226 else |
1221 err (fn _ => TooLifty (loc1, loc2)) | 1227 err (fn _ => TooLifty (loc1, loc2)) |
1222 | 1228 |
1223 | (L'.CRecord _, _) => isRecord () | |
1224 | (_, L'.CRecord _) => isRecord () | |
1225 | (L'.CConcat _, _) => isRecord () | |
1226 | (_, L'.CConcat _) => isRecord () | |
1227 | |
1228 | (L'.CUnif (0, _, _, _, r as ref (L'.Unknown f)), _) => | 1229 | (L'.CUnif (0, _, _, _, r as ref (L'.Unknown f)), _) => |
1229 if occursCon r c2All then | 1230 if occursCon r c2All then |
1230 err COccursCheckFailed | 1231 maybeIsRecord c2 |
1231 else if f c2All then | 1232 else if f c2All then |
1232 r := L'.Known c2All | 1233 r := L'.Known c2All |
1233 else | 1234 else |
1234 err CScope | 1235 err CScope |
1235 | (_, L'.CUnif (0, _, _, _, r as ref (L'.Unknown f))) => | 1236 | (_, L'.CUnif (0, _, _, _, r as ref (L'.Unknown f))) => |
1236 if occursCon r c1All then | 1237 if occursCon r c1All then |
1237 err COccursCheckFailed | 1238 maybeIsRecord c1 |
1238 else if f c1All then | 1239 else if f c1All then |
1239 r := L'.Known c1All | 1240 r := L'.Known c1All |
1240 else | 1241 else |
1241 err CScope | 1242 err CScope |
1242 | 1243 |
1243 | (L'.CUnif (nl, _, _, _, r as ref (L'.Unknown f)), _) => | 1244 | (L'.CUnif (nl, _, _, _, r as ref (L'.Unknown f)), _) => |
1244 if occursCon r c2All then | 1245 if occursCon r c2All then |
1245 err COccursCheckFailed | 1246 maybeIsRecord c2 |
1246 else | 1247 else |
1247 (let | 1248 (let |
1248 val sq = squish nl c2All | 1249 val sq = squish nl c2All |
1249 in | 1250 in |
1250 if f sq then | 1251 if f sq then |
1253 err CScope | 1254 err CScope |
1254 end | 1255 end |
1255 handle CantSquish => err (fn _ => TooDeep)) | 1256 handle CantSquish => err (fn _ => TooDeep)) |
1256 | (_, L'.CUnif (nl, _, _, _, r as ref (L'.Unknown f))) => | 1257 | (_, L'.CUnif (nl, _, _, _, r as ref (L'.Unknown f))) => |
1257 if occursCon r c1All then | 1258 if occursCon r c1All then |
1258 err COccursCheckFailed | 1259 maybeIsRecord c1 |
1259 else | 1260 else |
1260 (let | 1261 (let |
1261 val sq = squish nl c1All | 1262 val sq = squish nl c1All |
1262 in | 1263 in |
1263 if f sq then | 1264 if f sq then |
1264 r := L'.Known sq | 1265 r := L'.Known sq |
1265 else | 1266 else |
1266 err CScope | 1267 err CScope |
1267 end | 1268 end |
1268 handle CantSquish => err (fn _ => TooDeep)) | 1269 handle CantSquish => err (fn _ => TooDeep)) |
1270 | |
1271 | (L'.CRecord _, _) => isRecord () | |
1272 | (_, L'.CRecord _) => isRecord () | |
1273 | (L'.CConcat _, _) => isRecord () | |
1274 | (_, L'.CConcat _) => isRecord () | |
1269 | 1275 |
1270 | 1276 |
1271 | (L'.CUnit, L'.CUnit) => () | 1277 | (L'.CUnit, L'.CUnit) => () |
1272 | 1278 |
1273 | (L'.TFun (d1, r1), L'.TFun (d2, r2)) => | 1279 | (L'.TFun (d1, r1), L'.TFun (d2, r2)) => |