Mercurial > urweb

diff src/elab_util.sml @ 1302:d008c4c43a0a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Flex kinds for type-level tuples; ::_ notation
author Adam Chlipala <adam@chlipala.net>
date Sun, 10 Oct 2010 13:07:38 -0400
parents b4480a56cab7
children c7b9a33c26c8
line wrap: on
line diff
--- a/src/elab_util.sml	Thu Sep 30 18:29:59 2010 -0400
+++ b/src/elab_util.sml	Sun Oct 10 13:07:38 2010 -0400
@@ -78,6 +78,16 @@
               | 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 @@
               | 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' =>