Flex kinds for type-level tuples; ::_ notation

7 files changed, 91 insertions, 11 deletions

diff --git a/src/elab.sml b/src/elab.sml
index 6d405af6..dcb15502 100644
--- a/src/elab.sml
+++ b/src/elab.sml
@@ -39,6 +39,7 @@ datatype kind' =
 
        | KError
        | KUnif of ErrorMsg.span * string * kind option ref
+       | KTupleUnif of ErrorMsg.span * (int * kind) list * kind option ref
 
        | KRel of int
        | KFun of string * kind
diff --git a/src/elab_print.sml b/src/elab_print.sml
index 4fb7ee73..279c7231 100644
--- a/src/elab_print.sml
+++ b/src/elab_print.sml
@@ -56,6 +56,16 @@ fun p_kind' par env (k, _) =
       | KError => string "<ERROR>"
       | KUnif (_, _, ref (SOME k)) => p_kind' par env k
       | KUnif (_, s, _) => string ("<UNIF:" ^ s ^ ">")
+      | KTupleUnif (_, _, ref (SOME k)) => p_kind' par env k
+      | KTupleUnif (_, nks, _) => box [string "(",
+                                       p_list_sep (box [space, string "*", space])
+                                                  (fn (n, k) => box [string (Int.toString n ^ ":"),
+                                                                     space,
+                                                                     p_kind env k]) nks,
+                                       space,
+                                       string "*",
+                                       space,
+                                       string "...)"]
 
       | KRel n => ((if !debug then
                          string (E.lookupKRel env n ^ "_" ^ Int.toString n)
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' =>
diff --git a/src/elaborate.sml b/src/elaborate.sml
index e3f42c19..2cc01eda 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -94,6 +94,9 @@
            | (L'.KUnif (_, _, ref (SOME k1All)), _) => unifyKinds' env k1All k2All
            | (_, L'.KUnif (_, _, ref (SOME k2All))) => unifyKinds' env k1All k2All
 
+           | (L'.KTupleUnif (_, _, ref (SOME k)), _) => unifyKinds' env k k2All
+           | (_, L'.KTupleUnif (_, _, ref (SOME k))) => unifyKinds' env k1All k
+
            | (L'.KUnif (_, _, r1), L'.KUnif (_, _, r2)) =>
              if r1 = r2 then
                  ()
@@ -111,6 +114,32 @@
              else
                  r := SOME k1All
 
+           | (L'.KTupleUnif (_, nks, r), L'.KTuple ks) =>
+             ((app (fn (n, k) => unifyKinds' env k (List.nth (ks, n-1))) nks;
+               r := SOME k2All)
+              handle Subscript => err KIncompatible)
+           | (L'.KTuple ks, L'.KTupleUnif (_, nks, r)) =>
+             ((app (fn (n, k) => unifyKinds' env (List.nth (ks, n-1)) k) nks;
+               r := SOME k1All)
+              handle Subscript => err KIncompatible)
+           | (L'.KTupleUnif (loc, nks1, r1), L'.KTupleUnif (_, nks2, r2)) =>
+             let
+                 val nks = foldl (fn (p as (n, k1), nks) =>
+                                     case ListUtil.search (fn (n', k2) =>
+                                                              if n' = n then
+                                                                  SOME k2
+                                                              else
+                                                                  NONE) nks2 of
+                                         NONE => p :: nks
+                                       | SOME k2 => (unifyKinds' env k1 k2;
+                                                     nks)) nks2 nks1
+
+                 val k = (L'.KTupleUnif (loc, nks, ref NONE), loc)
+             in
+                 r1 := SOME k;
+                 r2 := SOME k
+             end
+
            | _ => err KIncompatible
      end
 
@@ -441,16 +470,15 @@
        | L.CProj (c, n) =>
          let
              val (c', k, gs) = elabCon (env, denv) c
+
+             val k' = kunif loc
          in
-             case hnormKind k of
-                 (L'.KTuple ks, _) =>
-                 if n <= 0 orelse n > length ks then
-                     (conError env (ProjBounds (c', n));
-                      (cerror, kerror, []))
-                 else
-                     ((L'.CProj (c', n), loc), List.nth (ks, n - 1), gs)
-               | k => (conError env (ProjMismatch (c', k));
-                       (cerror, kerror, []))
+             if n <= 0 then
+                 (conError env (ProjBounds (c', n));
+                  (cerror, kerror, []))
+             else
+                 (checkKind env c' k (L'.KTupleUnif (loc, [(n, k')], ref NONE), loc);
+                  ((L'.CProj (c', n), loc), k', gs))
          end
 
        | L.CWild k =>
@@ -463,6 +491,7 @@
  fun kunifsRemain k =
      case k of
          L'.KUnif (_, _, ref NONE) => true
+       | L'.KTupleUnif (_, _, ref NONE) => true
        | _ => false
  fun cunifsRemain c =
      case c of
@@ -3229,6 +3258,8 @@ and wildifyStr env (str, sgn) =
                        | L'.KError => NONE
                        | L'.KUnif (_, _, ref (SOME k)) => decompileKind k
                        | L'.KUnif _ => NONE
+                       | L'.KTupleUnif (_, _, ref (SOME k)) => decompileKind k
+                       | L'.KTupleUnif _ => NONE
 
                        | L'.KRel _ => NONE
                        | L'.KFun _ => NONE
diff --git a/src/explify.sml b/src/explify.sml
index 4f4f83e1..cf6c491c 100644
--- a/src/explify.sml
+++ b/src/explify.sml
@@ -44,6 +44,8 @@ fun explifyKind (k, loc) =
       | L.KError => raise Fail ("explifyKind: KError at " ^ EM.spanToString loc)
       | L.KUnif (_, _, ref (SOME k)) => explifyKind k
       | L.KUnif _ => raise Fail ("explifyKind: KUnif at " ^ EM.spanToString loc)
+      | L.KTupleUnif (loc, _, ref (SOME k)) => explifyKind k
+      | L.KTupleUnif _ => raise Fail ("explifyKind: KTupleUnif at " ^ EM.spanToString loc)
 
       | L.KRel n => (L'.KRel n, loc)
       | L.KFun (x, k) => (L'.KFun (x, explifyKind k), loc)
diff --git a/src/urweb.grm b/src/urweb.grm
index dfc22112..0c85ad7f 100644
--- a/src/urweb.grm
+++ b/src/urweb.grm
@@ -212,7 +212,7 @@ fun tnamesOf (e, _) =
  | STRING of string | INT of Int64.int | FLOAT of Real64.real | CHAR of char
  | SYMBOL of string | CSYMBOL of string
  | LPAREN | RPAREN | LBRACK | RBRACK | LBRACE | RBRACE
- | EQ | COMMA | COLON | DCOLON | TCOLON | DOT | HASH | UNDER | UNDERUNDER | BAR
+ | EQ | COMMA | COLON | DCOLON | DCOLONWILD | TCOLON | DOT | HASH | UNDER | UNDERUNDER | BAR
  | PLUS | MINUS | DIVIDE | DOTDOTDOT | MOD | AT
  | CON | LTYPE | VAL | REC | AND | FUN | MAP | UNIT | KUNIT | CLASS
  | DATATYPE | OF
@@ -510,6 +510,7 @@ dtypes : dtype                          ([dtype])
 
 kopt   :                                (NONE)
        | DCOLON kind                    (SOME kind)
+       | DCOLONWILD                     (SOME (KWild, s (DCOLONWILDleft, DCOLONWILDright)))
 
 dargs  :                                ([])
        | SYMBOL dargs                   (SYMBOL :: dargs)
@@ -853,6 +854,22 @@ carg   : SYMBOL DCOLON kind             (fn (c, k) =>
                                                 ((CAbs ("_", SOME kind, c), loc),
                                                  (KArrow (kind, k), loc))
                                             end)
+       | SYMBOL DCOLONWILD              (fn (c, k) =>
+                                            let
+                                                val loc = s (SYMBOLleft, DCOLONWILDright)
+                                                val kind = (KWild, loc)
+                                            in
+                                                ((CAbs (SYMBOL, NONE, c), loc),
+                                                 (KArrow (kind, k), loc))
+                                            end)
+       | UNDER DCOLONWILD               (fn (c, k) =>
+                                            let
+                                                val loc = s (UNDERleft, DCOLONWILDright)
+                                                val kind = (KWild, loc)
+                                            in
+                                                ((CAbs ("_", NONE, c), loc),
+                                                 (KArrow (kind, k), loc))
+                                            end)
        | cargp                          (cargp)
 
 cargp  : SYMBOL                         (fn (c, k) =>
@@ -1079,6 +1096,14 @@ earga  : LBRACK SYMBOL RBRACK            (fn (e, t) =>
                                                  ((ECAbs (Implicit, SYMBOL, kind, e), loc),
                                                   (TCFun (Implicit, SYMBOL, kind, t), loc))
                                              end)
+       | LBRACK SYMBOL DCOLONWILD RBRACK (fn (e, t) =>
+                                             let
+                                                 val loc = s (LBRACKleft, RBRACKright)
+                                                 val kind = (KWild, loc)
+                                             in
+                                                 ((ECAbs (Explicit, SYMBOL, kind, e), loc),
+                                                  (TCFun (Explicit, SYMBOL, kind, t), loc))
+                                             end)
        | LBRACK SYMBOL kcolon kind RBRACK(fn (e, t) =>
                                              let
                                                  val loc = s (LBRACKleft, RBRACKright)
diff --git a/src/urweb.lex b/src/urweb.lex
index 0ee09cad..a6df5f1b 100644
--- a/src/urweb.lex
+++ b/src/urweb.lex
@@ -372,6 +372,7 @@ xint = x[0-9a-fA-F][0-9a-fA-F];
 <INITIAL> ">="        => (Tokens.GE (pos yypos, pos yypos + size yytext));
 <INITIAL> ","         => (Tokens.COMMA (pos yypos, pos yypos + size yytext));
 <INITIAL> ":::"       => (Tokens.TCOLON (pos yypos, pos yypos + size yytext));
+<INITIAL> "::_"       => (Tokens.DCOLONWILD (pos yypos, pos yypos + size yytext));
 <INITIAL> "::"        => (Tokens.DCOLON (pos yypos, pos yypos + size yytext));
 <INITIAL> ":"         => (Tokens.COLON (pos yypos, pos yypos + size yytext));
 <INITIAL> "..."       => (Tokens.DOTDOTDOT (pos yypos, pos yypos + size yytext));