Mercurial > urweb

changeset 18:9a578171de9e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Unification wildcards
author Adam Chlipala <adamc@hcoop.net>
date Sun, 08 Jun 2008 14:25:27 -0400
parents 9bd8669d53c2
children e634ae817a8e
files src/elaborate.sml src/lacweb.grm src/lacweb.lex src/source.sml src/source_print.sml tests/impl.lac
diffstat 6 files changed, 33 insertions(+), 8 deletions(-) [+]
line wrap: on
line diff
--- a/src/elaborate.sml	Sun Jun 08 14:10:51 2008 -0400
+++ b/src/elaborate.sml	Sun Jun 08 14:25:27 2008 -0400
@@ -36,13 +36,6 @@
 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 @@
 
 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 @@
             ((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
--- a/src/lacweb.grm	Sun Jun 08 14:10:51 2008 -0400
+++ b/src/lacweb.grm	Sun Jun 08 14:25:27 2008 -0400
@@ -39,7 +39,7 @@
  | 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 @@
        | 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 @@
 
        | 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 @@
        | 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)])
--- a/src/lacweb.lex	Sun Jun 08 14:10:51 2008 -0400
+++ b/src/lacweb.lex	Sun Jun 08 14:25:27 2008 -0400
@@ -120,6 +120,8 @@
 <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));
--- a/src/source.sml	Sun Jun 08 14:10:51 2008 -0400
+++ b/src/source.sml	Sun Jun 08 14:25:27 2008 -0400
@@ -34,6 +34,7 @@
        | KArrow of kind * kind
        | KName
        | KRecord of kind
+       | KWild
 
 withtype kind = kind' located
 
@@ -57,6 +58,8 @@
        | CRecord of (con * con) list
        | CConcat of con * con
 
+       | CWild of kind
+
 withtype con = con' located
 
 datatype exp' =
--- a/src/source_print.sml	Sun Jun 08 14:10:51 2008 -0400
+++ b/src/source_print.sml	Sun Jun 08 14:25:27 2008 -0400
@@ -44,6 +44,7 @@
                                              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 @@
                                               string "++",
                                               space,
                                               p_con c2])
+      | CWild k => box [string "(_",
+                        space,
+                        string "::",
+                        space,
+                        p_kind k]
         
 and p_con c = p_con' false c
 
--- a/tests/impl.lac	Sun Jun 08 14:10:51 2008 -0400
+++ b/tests/impl.lac	Sun Jun 08 14:25:27 2008 -0400
@@ -7,6 +7,8 @@
 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}