From bfeac162a328dba937a28e747e4fc4006fac500c Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adam@chlipala.net>
Date: Sun, 10 Oct 2010 13:07:38 -0400
Subject: Flex kinds for type-level tuples; ::_ notation

---
 src/elab_util.sml | 12 +++++++++++-
 1 file changed, 11 insertions(+), 1 deletion(-)

(limited to 'src/elab_util.sml')

diff --git a/src/elab_util.sml b/src/elab_util.sml
index ccfb86a3..33ed599c 100644
--- a/src/elab_util.sml
+++ b/src/elab_util.sml
@@ -78,6 +78,16 @@ fun mapfoldB {kind, bind} =
               | KUnif (_, _, ref (SOME k)) => mfk' ctx k
               | KUnif _ => S.return2 kAll
 
+              | KTupleUnif (_, _, ref (SOME k)) => mfk' ctx k
+              | KTupleUnif (loc, nks, r) =>
+                S.map2 (ListUtil.mapfold (fn (n, k) =>
+                                             S.map2 (mfk ctx k,
+                                                  fn k' =>
+                                                     (n, k'))) nks,
+                     fn nks' =>
+                        (KTupleUnif (loc, nks', r), loc))
+
+
               | KRel _ => S.return2 kAll
               | KFun (x, k) =>
                 S.map2 (mfk (bind (ctx, x)) k,
@@ -207,7 +217,7 @@ fun mapfoldB {kind = fk, con = fc, bind} =
               | CError => S.return2 cAll
               | CUnif (_, _, _, ref (SOME c)) => mfc' ctx c
               | CUnif _ => S.return2 cAll
-
+                        
               | CKAbs (x, c) =>
                 S.map2 (mfc (bind (ctx, RelK x)) c,
                         fn c' =>
-- 
cgit v1.2.3