diff options
| author |  Adam Chlipala <adam@chlipala.net> | 2015-11-27 15:28:12 -0500 |
|---|---|---|
| committer | Adam Chlipala <adam@chlipala.net> | 2015-11-27 15:28:12 -0500 |
| commit | 4635acd2d4e4404b2b1a89909cd765ac310d62c5 (patch) | |
| tree | 3a5805f65fb9c84460ab85f8c09f40e49dc9f4d9 /src | |
| parent | 9e392faf0f78cb6b96708d96ed9c5fb6f9dd26dd (diff) | |
Fix tricky case of functor signature subsumption
Diffstat (limited to 'src')
| -rw-r--r-- | src/elab_env.sig | 2 | ||||
| -rw-r--r-- | src/elab_env.sml | 4 | ||||
| -rw-r--r-- | src/elaborate.sml | 9 |
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 |