Mercurial > urweb

comparison src/elaborate.sml @ 2044:42ae25a354f8

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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)) =>