diff options
author | 2010-10-19 10:13:24 -0400 | |
---|---|---|
committer | 2010-10-19 10:13:24 -0400 | |
commit | 0d52aedbd9ecc04c0540ad7d7d7ff2b5051dcaa5 (patch) | |
tree | 1cded183f95d276e9d76bdcf8eb0af157eaa1763 /src | |
parent | 25838bc2eb221b82151c648473b3528e3a4e4e9d (diff) |
Smarter handling of unification variables for 'kindof' on projections
Diffstat (limited to 'src')
-rw-r--r-- | src/elab.sml | 2 | ||||
-rw-r--r-- | src/elaborate.sml | 19 |
2 files changed, 20 insertions, 1 deletions
diff --git a/src/elab.sml b/src/elab.sml index 97acec31..c042d916 100644 --- a/src/elab.sml +++ b/src/elab.sml @@ -1,4 +1,4 @@ -(* Copyright (c) 2008, Adam Chlipala +(* Copyright (c) 2008-2010, Adam Chlipala * All rights reserved. * * Redistribution and use in source and binary forms, with or without diff --git a/src/elaborate.sml b/src/elaborate.sml index dcae4650..3346fc37 100644 --- a/src/elaborate.sml +++ b/src/elaborate.sml @@ -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 |