# HG changeset patch
# User Adam Chlipala <adamc@hcoop.net>
# Date 1218913385 14400
# Node ID 766b5475477fcee93b0769f3223672d3a22f0e6f
# Parent  0343557355fcfdd030b7bad02a34424fbac24558
Corifying con-tuples

diff -r 0343557355fc -r 766b5475477f src/core.sml
--- a/src/core.sml	Sat Aug 16 14:45:23 2008 -0400
+++ b/src/core.sml	Sat Aug 16 15:03:05 2008 -0400
@@ -35,6 +35,7 @@
        | KName
        | KRecord of kind
        | KUnit
+       | KTuple of kind list
 
 withtype kind = kind' located
 
@@ -57,6 +58,9 @@
 
        | CUnit
 
+       | CTuple of con list
+       | CProj of con * int
+
 withtype con = con' located
 
 datatype datatype_kind = datatype Elab.datatype_kind
diff -r 0343557355fc -r 766b5475477f src/core_print.sml
--- a/src/core_print.sml	Sat Aug 16 14:45:23 2008 -0400
+++ b/src/core_print.sml	Sat Aug 16 15:03:05 2008 -0400
@@ -49,6 +49,9 @@
       | KName => string "Name"
       | KRecord k => box [string "{", p_kind k, string "}"]
       | KUnit => string "Unit"
+      | KTuple ks => box [string "(",
+                          p_list_sep (box [space, string "*", space]) p_kind ks,
+                          string ")"]
 
 and p_kind k = p_kind' false k
 
@@ -137,6 +140,13 @@
                                               p_con env c2])
       | CFold _ => string "fold"
       | CUnit => string "()"
+
+      | CTuple cs => box [string "(",
+                          p_list (p_con env) cs,
+                          string ")"]
+      | CProj (c, n) => box [p_con env c,
+                             string ".",
+                             string (Int.toString n)]
         
 and p_con env = p_con' false env
 
diff -r 0343557355fc -r 766b5475477f src/core_util.sml
--- a/src/core_util.sml	Sat Aug 16 14:45:23 2008 -0400
+++ b/src/core_util.sml	Sat Aug 16 15:03:05 2008 -0400
@@ -54,6 +54,10 @@
       | (_, KRecord _) => GREATER
 
       | (KUnit, KUnit) => EQUAL
+      | (KUnit, _) => LESS
+      | (_, KUnit) => GREATER
+
+      | (KTuple ks1, KTuple ks2) => joinL compare (ks1, ks2)
 
 fun mapfold f =
     let
@@ -79,6 +83,11 @@
                            (KRecord k', loc))
 
               | KUnit => S.return2 kAll
+
+              | KTuple ks =>
+                S.map2 (ListUtil.mapfold mfk ks,
+                        fn ks' =>
+                           (KTuple ks', loc))
     in
         mfk
     end
@@ -170,6 +179,15 @@
       | (_, CFold _) => GREATER
 
       | (CUnit, CUnit) => EQUAL
+      | (CUnit, _) => LESS
+      | (_, CUnit) => GREATER
+
+      | (CTuple cs1, CTuple cs2) => joinL compare (cs1, cs2)
+      | (CTuple _, _) => LESS
+      | (_, CTuple _) => GREATER
+
+      | (CProj (c1, n1), CProj (c2, n2)) => join (Int.compare (n1, n2),
+                                                  fn () => compare (c1, c2))
 
 datatype binder =
          Rel of string * kind
@@ -245,6 +263,16 @@
                                        (CFold (k1', k2'), loc)))
 
               | CUnit => S.return2 cAll
+
+              | CTuple cs =>
+                S.map2 (ListUtil.mapfold (mfc ctx) cs,
+                        fn cs' =>
+                           (CTuple cs', loc))
+
+              | CProj (c, n) =>
+                S.map2 (mfc ctx c,
+                        fn c' =>
+                           (CProj (c', n), loc))
     in
         mfc
     end
diff -r 0343557355fc -r 766b5475477f src/corify.sml
--- a/src/corify.sml	Sat Aug 16 14:45:23 2008 -0400
+++ b/src/corify.sml	Sat Aug 16 15:03:05 2008 -0400
@@ -380,7 +380,7 @@
        | L.KName => (L'.KName, loc)
        | L.KRecord k => (L'.KRecord (corifyKind k), loc)
        | L.KUnit => (L'.KUnit, loc)
-       | L.KTuple _ => raise Fail "Corify KTuple"
+       | L.KTuple ks => (L'.KTuple (map corifyKind ks), loc)
 
  fun corifyCon st (c, loc) =
      case c of
@@ -414,8 +414,8 @@
        | L.CFold (k1, k2) => (L'.CFold (corifyKind k1, corifyKind k2), loc)
        | L.CUnit => (L'.CUnit, loc)
 
-       | L.CTuple _ => raise Fail "Corify CTuple"
-       | L.CProj _ => raise Fail "Corify CProj"
+       | L.CTuple cs => (L'.CTuple (map (corifyCon st) cs), loc)
+       | L.CProj (c, n) => (L'.CProj (corifyCon st c, n), loc)
 
  fun corifyPatCon st pc =
      case pc of
diff -r 0343557355fc -r 766b5475477f src/monoize.sml
--- a/src/monoize.sml	Sat Aug 16 14:45:23 2008 -0400
+++ b/src/monoize.sml	Sat Aug 16 15:03:05 2008 -0400
@@ -98,6 +98,9 @@
                   | L.CConcat _ => poly ()
                   | L.CFold _ => poly ()
                   | L.CUnit => poly ()
+
+                  | L.CTuple _ => poly ()
+                  | L.CProj _ => poly ()
             end
     in
         mt env IM.empty