summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--src/elab.sml2
-rw-r--r--src/elaborate.sml19
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