Mercurial > urweb

comparison src/elaborate.sml @ 1668:64c1e65c2365

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Prevent horrifying loops in unification variable graph
author Adam Chlipala <adam@chlipala.net>
date Mon, 09 Jan 2012 16:20:10 -0500
parents edf86cef0dba
children 1584fd8d16dd
comparison
equal deleted inserted replaced
1667:833402503855 1668:64c1e65c2365
1186 case (c1, c2) of 1186 case (c1, c2) of
1187 (L'.CProj (c1, n1), _) => projSpecial1 (c1, n1, isRecord') 1187 (L'.CProj (c1, n1), _) => projSpecial1 (c1, n1, isRecord')
1188 | (_, L'.CProj (c2, n2)) => projSpecial2 (c2, n2, isRecord') 1188 | (_, L'.CProj (c2, n2)) => projSpecial2 (c2, n2, isRecord')
1189 | _ => isRecord' () 1189 | _ => isRecord' ()
1190 in 1190 in
1191 (*eprefaces "unifyCons''" [("c1All", p_con env c1All), 1191 (*eprefaces "unifyCons''" [("c1", p_con env c1All),
1192 ("c2All", p_con env c2All)];*) 1192 ("c2", p_con env c2All)];*)
1193 1193
1194 case (c1, c2) of 1194 (case (c1, c2) of
1195 (L'.CError, _) => () 1195 (L'.CError, _) => ()
1196 | (_, L'.CError) => () 1196 | (_, L'.CError) => ()
1197 1197
1198 | (L'.CUnif (nl1, loc1, k1, _, r1 as ref (L'.Unknown f1)), L'.CUnif (nl2, loc2, k2, _, r2 as ref (L'.Unknown f2))) => 1198 | (L'.CUnif (nl1, loc1, k1, _, r1 as ref (L'.Unknown f1)), L'.CUnif (nl2, loc2, k2, _, r2 as ref (L'.Unknown f2))) =>
1199 if r1 = r2 andalso nl1 = nl2 then 1199 if r1 = r2 then
1200 () 1200 if nl1 = nl2 then
1201 ()
1202 else
1203 err (fn _ => TooLifty (loc1, loc2))
1201 else if nl1 = 0 then 1204 else if nl1 = 0 then
1202 (unifyKinds env k1 k2; 1205 (unifyKinds env k1 k2;
1203 if f1 c2All then 1206 if f1 c2All then
1204 r1 := L'.Known c2All 1207 r1 := L'.Known c2All
1205 else 1208 else
1333 (unifyKinds env k1 k2; 1336 (unifyKinds env k1 k2;
1334 unifyCons' env loc c1 c2) 1337 unifyCons' env loc c1 c2)
1335 | (L'.TKFun (x, c1), L'.TKFun (_, c2)) => 1338 | (L'.TKFun (x, c1), L'.TKFun (_, c2)) =>
1336 unifyCons' (E.pushKRel env x) loc c1 c2 1339 unifyCons' (E.pushKRel env x) loc c1 c2
1337 1340
1338 | _ => err CIncompatible 1341 | _ => err CIncompatible)(*;
1342 eprefaces "/unifyCons''" [("c1", p_con env c1All),
1343 ("c2", p_con env c2All)]*)
1339 end 1344 end
1340 1345
1341 and unifyCons env loc c1 c2 = 1346 and unifyCons env loc c1 c2 =
1342 unifyCons' env loc c1 c2 1347 unifyCons' env loc c1 c2
1343 handle CUnify' err => raise CUnify (c1, c2, err) 1348 handle CUnify' err => raise CUnify (c1, c2, err)
3008 | SOME n1 => L'.CNamed n1) 3013 | SOME n1 => L'.CNamed n1)
3009 | _ => c} 3014 | _ => c}
3010 3015
3011 fun folder (sgi2All as (sgi, loc), env) = 3016 fun folder (sgi2All as (sgi, loc), env) =
3012 let 3017 let
3013 (*val () = prefaces "folder" [("sgis1", p_sgn env (L'.SgnConst sgis1, loc2))]*) 3018 (*val () = prefaces "folder" [("sgi2", p_sgn_item env sgi2All)]*)
3014 3019
3015 fun seek' f p = 3020 fun seek' f p =
3016 let 3021 let
3017 fun seek env ls = 3022 fun seek env ls =
3018 case ls of 3023 case ls of
4494 let 4499 let
4495 val () = resetKunif () 4500 val () = resetKunif ()
4496 val () = resetCunif () 4501 val () = resetCunif ()
4497 val (ds, (env', _, gs)) = elabDecl (d, (env, D.empty, gs)) 4502 val (ds, (env', _, gs)) = elabDecl (d, (env, D.empty, gs))
4498 in 4503 in
4499 (**)
4500 (ds, (env', gs)) 4504 (ds, (env', gs))
4501 end 4505 end
4502 4506
4503 val (file, (env'', gs)) = ListUtil.foldlMapConcat elabDecl' (env', []) file 4507 val (file, (env'', gs)) = ListUtil.foldlMapConcat elabDecl' (env', []) file
4504 4508