Mercurial > urweb

comparison src/elaborate.sml @ 2211:ef766ef6e242

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Merge.
author Ziv Scully <ziv@mit.edu>
date Sat, 13 Sep 2014 19:16:07 -0400
parents 459ccbf8cd08
children 834b438d57f3
comparison
equal deleted inserted replaced
2210:69c0f36255cb 2211:ef766ef6e242
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'.CUnif (0, _, _, _, r as ref (L'.Unknown f)), _) => 1229 | (L'.CUnif (0, _, k1, _, r as ref (L'.Unknown f)), _) =>
1230 (unifyKinds env k1 (kindof env c2All);
1231 if occursCon r c2All then
1232 maybeIsRecord c2
1233 else if f c2All then
1234 r := L'.Known c2All
1235 else
1236 err CScope)
1237 | (_, L'.CUnif (0, _, k2, _, r as ref (L'.Unknown f))) =>
1238 (unifyKinds env (kindof env c1All) k2;
1239 if occursCon r c1All then
1240 maybeIsRecord c1
1241 else if f c1All then
1242 r := L'.Known c1All
1243 else
1244 err CScope)
1245
1246 | (L'.CUnif (nl, _, k1, _, r as ref (L'.Unknown f)), _) =>
1224 if occursCon r c2All then 1247 if occursCon r c2All then
1225 err COccursCheckFailed 1248 maybeIsRecord c2
1226 else if f c2All then
1227 r := L'.Known c2All
1228 else 1249 else
1229 err CScope 1250 (unifyKinds env k1 (kindof env c2All);
1230 | (_, L'.CUnif (0, _, _, _, r as ref (L'.Unknown f))) => 1251 let
1231 if occursCon r c1All then
1232 err COccursCheckFailed
1233 else if f c1All then
1234 r := L'.Known c1All
1235 else
1236 err CScope
1237
1238 | (L'.CUnif (nl, _, _, _, r as ref (L'.Unknown f)), _) =>
1239 if occursCon r c2All then
1240 err COccursCheckFailed
1241 else
1242 (let
1243 val sq = squish nl c2All 1252 val sq = squish nl c2All
1244 in 1253 in
1245 if f sq then 1254 if f sq then
1246 r := L'.Known sq 1255 r := L'.Known sq
1247 else 1256 else
1248 err CScope 1257 err CScope
1249 end 1258 end
1250 handle CantSquish => err (fn _ => TooDeep)) 1259 handle CantSquish => err (fn _ => TooDeep))
1251 | (_, L'.CUnif (nl, _, _, _, r as ref (L'.Unknown f))) => 1260 | (_, L'.CUnif (nl, _, k2, _, r as ref (L'.Unknown f))) =>
1252 if occursCon r c1All then 1261 if occursCon r c1All then
1253 err COccursCheckFailed 1262 maybeIsRecord c1
1254 else 1263 else
1255 (let 1264 (unifyKinds env (kindof env c1All) k2;
1265 let
1256 val sq = squish nl c1All 1266 val sq = squish nl c1All
1257 in 1267 in
1258 if f sq then 1268 if f sq then
1259 r := L'.Known sq 1269 r := L'.Known sq
1260 else 1270 else