summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2015-11-27 15:28:12 -0500
committerGravatar Adam Chlipala <adam@chlipala.net>2015-11-27 15:28:12 -0500
commit4635acd2d4e4404b2b1a89909cd765ac310d62c5 (patch)
tree3a5805f65fb9c84460ab85f8c09f40e49dc9f4d9 /src
parent9e392faf0f78cb6b96708d96ed9c5fb6f9dd26dd (diff)
Fix tricky case of functor signature subsumption
Diffstat (limited to 'src')
-rw-r--r--src/elab_env.sig2
-rw-r--r--src/elab_env.sml4
-rw-r--r--src/elaborate.sml9
3 files changed, 13 insertions, 2 deletions
diff --git a/src/elab_env.sig b/src/elab_env.sig
index e0c589c4..cbc85cdd 100644
--- a/src/elab_env.sig
+++ b/src/elab_env.sig
@@ -37,6 +37,8 @@ signature ELAB_ENV = sig
type env
+ val dump : env -> unit
+
val empty : env
exception UnboundRel of int
diff --git a/src/elab_env.sml b/src/elab_env.sml
index 9c9cd14f..3523b576 100644
--- a/src/elab_env.sml
+++ b/src/elab_env.sml
@@ -239,6 +239,10 @@ type env = {
str : (string * sgn) IM.map
}
+fun dump (env : env) =
+ (print "NamedC:\n";
+ IM.appi (fn (n, (x, k, co)) => print (x ^ " [" ^ Int.toString n ^ "]\n")) (#namedC env))
+
val namedCounter = ref 0
fun newNamed () =
diff --git a/src/elaborate.sml b/src/elaborate.sml
index 7671f597..25cce6bd 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -1359,7 +1359,9 @@
end
and unifyCons env loc c1 c2 =
- unifyCons' env loc c1 c2
+ ((*Print.prefaces "uc" [("c1", p_con env c1),
+ ("c2", p_con env c2)];*)
+ unifyCons' env loc c1 c2)
handle CUnify' (env', err) => raise CUnify (c1, c2, env', err)
| KUnify (arg as {3 = env', ...}) => raise CUnify (c1, c2, env', CKind arg)
@@ -3079,6 +3081,8 @@ and subSgn' counterparts env strLoc sgn1 (sgn2 as (_, loc2)) =
fun cpart n = IM.find (!counterparts, n)
fun cparts (n2, n1) = counterparts := IM.insert (!counterparts, n2, n1)
+ fun uncparts n2 = (counterparts := #1 (IM.remove (!counterparts, n2)))
+ handle NotFound => ()
val sub2 = U.Con.map {kind = fn k => k,
con = fn c =>
@@ -3107,7 +3111,8 @@ and subSgn' counterparts env strLoc sgn1 (sgn2 as (_, loc2)) =
if E.checkENamed env n then
env
else
- E.pushCNamedAs env x n k (SOME c)
+ (uncparts n;
+ E.pushCNamedAs env x n k (SOME c))
| L'.SgiConAbs (x, n, k) =>
if E.checkENamed env n then
env