Mercurial > urweb
diff src/elaborate.sml @ 1311:5337adf33a4a
Smarter handling of unification variables for 'kindof' on projections
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Tue, 19 Oct 2010 10:13:24 -0400 |
parents | 3a845f2ce9e9 |
children | df7bfb30dcc3 |
line wrap: on
line diff
--- a/src/elaborate.sml Sun Oct 17 13:26:11 2010 -0400 +++ b/src/elaborate.sml Tue Oct 19 10:13:24 2010 -0400 @@ -583,6 +583,25 @@ | L'.CProj (c, n) => (case hnormKind (kindof env c) of (L'.KTuple ks, _) => List.nth (ks, n - 1) + | (L'.KUnif (_, _, r), _) => + let + val ku = kunif loc + val k = (L'.KTupleUnif (loc, [(n, ku)], ref NONE), loc) + in + r := SOME k; + k + end + | (L'.KTupleUnif (_, nks, r), _) => + (case ListUtil.search (fn (n', k) => if n' = n then SOME k else NONE) nks of + SOME k => k + | NONE => + let + val ku = kunif loc + val k = (L'.KTupleUnif (loc, ((n, ku) :: nks), ref NONE), loc) + in + r := SOME k; + k + end) | k => raise CUnify' (CKindof (k, c, "tuple"))) | L'.CError => kerror