Mercurial > urweb

comparison src/elaborate.sml @ 2196:100352dbae36

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Fix tricky case of functor signature subsumption
author Adam Chlipala <adam@chlipala.net>
date Fri, 27 Nov 2015 15:28:12 -0500
parents fb113569519e
children
comparison
equal deleted inserted replaced
2195:18e6fb487880 2196:100352dbae36
1357 eprefaces "/unifyCons''" [("c1", p_con env c1All), 1357 eprefaces "/unifyCons''" [("c1", p_con env c1All),
1358 ("c2", p_con env c2All)]*) 1358 ("c2", p_con env c2All)]*)
1359 end 1359 end
1360 1360
1361 and unifyCons env loc c1 c2 = 1361 and unifyCons env loc c1 c2 =
1362 unifyCons' env loc c1 c2 1362 ((*Print.prefaces "uc" [("c1", p_con env c1),
1363 ("c2", p_con env c2)];*)
1364 unifyCons' env loc c1 c2)
1363 handle CUnify' (env', err) => raise CUnify (c1, c2, env', err) 1365 handle CUnify' (env', err) => raise CUnify (c1, c2, env', err)
1364 | KUnify (arg as {3 = env', ...}) => raise CUnify (c1, c2, env', CKind arg) 1366 | KUnify (arg as {3 = env', ...}) => raise CUnify (c1, c2, env', CKind arg)
1365 1367
1366 fun checkCon env e c1 c2 = 1368 fun checkCon env e c1 c2 =
1367 unifyCons env (#2 e) c1 c2 1369 unifyCons env (#2 e) c1 c2
3077 ("sgis1", p_sgn env (L'.SgnConst sgis1, loc2)), 3079 ("sgis1", p_sgn env (L'.SgnConst sgis1, loc2)),
3078 ("sgis2", p_sgn env (L'.SgnConst sgis2, loc2))]*) 3080 ("sgis2", p_sgn env (L'.SgnConst sgis2, loc2))]*)
3079 3081
3080 fun cpart n = IM.find (!counterparts, n) 3082 fun cpart n = IM.find (!counterparts, n)
3081 fun cparts (n2, n1) = counterparts := IM.insert (!counterparts, n2, n1) 3083 fun cparts (n2, n1) = counterparts := IM.insert (!counterparts, n2, n1)
3084 fun uncparts n2 = (counterparts := #1 (IM.remove (!counterparts, n2)))
3085 handle NotFound => ()
3082 3086
3083 val sub2 = U.Con.map {kind = fn k => k, 3087 val sub2 = U.Con.map {kind = fn k => k,
3084 con = fn c => 3088 con = fn c =>
3085 case c of 3089 case c of
3086 L'.CNamed n2 => 3090 L'.CNamed n2 =>
3105 val env = case #1 h of 3109 val env = case #1 h of
3106 L'.SgiCon (x, n, k, c) => 3110 L'.SgiCon (x, n, k, c) =>
3107 if E.checkENamed env n then 3111 if E.checkENamed env n then
3108 env 3112 env
3109 else 3113 else
3110 E.pushCNamedAs env x n k (SOME c) 3114 (uncparts n;
3115 E.pushCNamedAs env x n k (SOME c))
3111 | L'.SgiConAbs (x, n, k) => 3116 | L'.SgiConAbs (x, n, k) =>
3112 if E.checkENamed env n then 3117 if E.checkENamed env n then
3113 env 3118 env
3114 else 3119 else
3115 E.pushCNamedAs env x n k NONE 3120 E.pushCNamedAs env x n k NONE