diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/elaborate.sml | 22 | ||||
| -rw-r--r-- | src/lacweb.grm | 6 | ||||
| -rw-r--r-- | src/lacweb.lex | 2 | ||||
| -rw-r--r-- | src/source.sml | 3 | ||||
| -rw-r--r-- | src/source_print.sml | 6 |
5 files changed, 31 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 |