Unification wildcards

6 files changed, 33 insertions, 8 deletions

diff --git a/src/elaborate.sml b/src/elaborate.sml
index 9e457499..9e63ecea 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -36,13 +36,6 @@ structure U = ElabUtil
 open Print
 open ElabPrint
 
-fun elabKind (k, loc) =
-    case k of
-        L.KType => (L'.KType, loc)
-      | L.KArrow (k1, k2) => (L'.KArrow (elabKind k1, elabKind k2), loc)
-      | L.KName => (L'.KName, loc)
-      | L.KRecord k => (L'.KRecord (elabKind k), loc)
-
 fun elabExplicitness e =
     case e of
         L.Explicit => L'.Explicit
@@ -183,6 +176,14 @@ fun cunif k =
 
 end
 
+fun elabKind (k, loc) =
+    case k of
+        L.KType => (L'.KType, loc)
+      | L.KArrow (k1, k2) => (L'.KArrow (elabKind k1, elabKind k2), loc)
+      | L.KName => (L'.KName, loc)
+      | L.KRecord k => (L'.KRecord (elabKind k), loc)
+      | L.KWild => kunif ()
+
 fun elabCon env (c, loc) =
     case c of
         L.CAnnot (c, k) =>
@@ -283,6 +284,13 @@ fun elabCon env (c, loc) =
             ((L'.CConcat (c1', c2'), loc), k)
         end
 
+      | L.CWild k =>
+        let
+            val k' = elabKind k
+        in
+            (cunif k', k')
+        end
+
 fun kunifsRemain k =
     case k of
         L'.KUnif (_, ref NONE) => true
diff --git a/src/lacweb.grm b/src/lacweb.grm
index 12cc0378..0c491bc3 100644
--- a/src/lacweb.grm
+++ b/src/lacweb.grm
@@ -39,7 +39,7 @@ val s = ErrorMsg.spanOf
  | STRING of string | INT of Int64.int | FLOAT of Real64.real
  | SYMBOL of string | CSYMBOL of string
  | LPAREN | RPAREN | LBRACK | RBRACK | LBRACE | RBRACE
- | EQ | COMMA | COLON | DCOLON | TCOLON | DOT | HASH
+ | EQ | COMMA | COLON | DCOLON | TCOLON | DOT | HASH | UNDER | UNDERUNDER
  | CON | LTYPE | VAL
  | TYPE | NAME
  | ARROW | LARROW | DARROW
@@ -102,6 +102,7 @@ kind   : TYPE                           (KType, s (TYPEleft, TYPEright))
        | LBRACE kind RBRACE             (KRecord kind, s (LBRACEleft, RBRACEright))
        | kind ARROW kind                (KArrow (kind1, kind2), s (kind1left, kind2right))
        | LPAREN kind RPAREN             (#1 kind, s (LPARENleft, RPARENright))
+       | UNDERUNDER                     (KWild, s (UNDERUNDERleft, UNDERUNDERright))
 
 capps  : cterm                          (cterm)
        | capps cterm                    (CApp (capps, cterm), s (cappsleft, ctermright))
@@ -116,6 +117,8 @@ cexp   : capps                          (capps)
 
        | LPAREN cexp RPAREN DCOLON kind (CAnnot (cexp, kind), s (LPARENleft, kindright))
 
+       | UNDER DCOLON kind              (CWild kind, s (UNDERleft, UNDERright))
+
 kcolon : DCOLON                         (Explicit)
        | TCOLON                         (Implicit)
 
@@ -127,6 +130,7 @@ cterm  : LPAREN cexp RPAREN             (#1 cexp, s (LPARENleft, RPARENright))
        | HASH CSYMBOL                   (CName CSYMBOL, s (HASHleft, CSYMBOLright))
 
        | SYMBOL                         (CVar SYMBOL, s (SYMBOLleft, SYMBOLright))
+       | UNDER                          (CWild (KWild, s (UNDERleft, UNDERright)), s (UNDERleft, UNDERright))
 
 rcon   :                                ([])
        | ident EQ cexp                  ([(ident, cexp)])
diff --git a/src/lacweb.lex b/src/lacweb.lex
index af2ed464..3fb3d95e 100644
--- a/src/lacweb.lex
+++ b/src/lacweb.lex
@@ -120,6 +120,8 @@ realconst = [0-9]+\.[0-9]*;
 <INITIAL> "."         => (Tokens.DOT (yypos, yypos + size yytext));
 <INITIAL> "$"         => (Tokens.DOLLAR (yypos, yypos + size yytext));
 <INITIAL> "#"         => (Tokens.HASH (yypos, yypos + size yytext));
+<INITIAL> "__"        => (Tokens.UNDERUNDER (yypos, yypos + size yytext));
+<INITIAL> "_"         => (Tokens.UNDER (yypos, yypos + size yytext));
 
 <INITIAL> "con"       => (Tokens.CON (yypos, yypos + size yytext));
 <INITIAL> "type"      => (Tokens.LTYPE (yypos, yypos + size yytext));
diff --git a/src/source.sml b/src/source.sml
index 9b0e2a07..c76ebf0b 100644
--- a/src/source.sml
+++ b/src/source.sml
@@ -34,6 +34,7 @@ datatype kind' =
        | KArrow of kind * kind
        | KName
        | KRecord of kind
+       | KWild
 
 withtype kind = kind' located
 
@@ -57,6 +58,8 @@ datatype con' =
        | CRecord of (con * con) list
        | CConcat of con * con
 
+       | CWild of kind
+
 withtype con = con' located
 
 datatype exp' =
diff --git a/src/source_print.sml b/src/source_print.sml
index 3db15ec6..90524241 100644
--- a/src/source_print.sml
+++ b/src/source_print.sml
@@ -44,6 +44,7 @@ fun p_kind' par (k, _) =
                                              p_kind k2])
       | KName => string "Name"
       | KRecord k => box [string "{", p_kind k, string "}"]
+      | KWild => string "_"
 
 and p_kind k = p_kind' false k
 
@@ -118,6 +119,11 @@ fun p_con' par (c, _) =
                                               string "++",
                                               space,
                                               p_con c2])
+      | CWild k => box [string "(_",
+                        space,
+                        string "::",
+                        space,
+                        p_kind k]
         
 and p_con c = p_con' false c
 
diff --git a/tests/impl.lac b/tests/impl.lac
index b647b96e..5304598c 100644
--- a/tests/impl.lac
+++ b/tests/impl.lac
@@ -7,6 +7,8 @@ val idi_self = idi idi
 val picker = fn na :: Name => fn a ::: Type => fn nb :: Name => fn b ::: Type => fn fs ::: {Type} =>
         fn r : $([na = a, nb = b] ++ fs) => {na = r.na, nb = r.nb}
 val getem = picker [#A] [#C] {A = 0, B = 1.0, C = "hi", D = {}}
+val getem2 = picker [#A] [_] {A = 0, B = 1.0, C = "hi", D = {}}
+val getem3 = picker [#A] [_::Name] {A = 0, B = 1.0, C = "hi", D = {}}
 
 val picker_ohmy = fn na ::: Name => fn a ::: Type => fn nb ::: Name => fn b ::: Type => fn fs ::: {Type} =>
         fn r : $([na = a, nb = b] ++ fs) => {na = r.na, nb = r.nb}