diff options
author | Adam Chlipala <adam@chlipala.net> | 2010-10-10 13:07:38 -0400 |
---|---|---|
committer | Adam Chlipala <adam@chlipala.net> | 2010-10-10 13:07:38 -0400 |
commit | d8bc26c9647d2b45009f6538bc2a69508c983449 (patch) | |
tree | 1d0f355dec824a81d80e9e838e0cae8845f8e179 /src | |
parent | 975b1f43784dfc1769ec93dd5dd408434791464e (diff) |
Flex kinds for type-level tuples; ::_ notation
Diffstat (limited to 'src')
-rw-r--r-- | src/elab.sml | 1 | ||||
-rw-r--r-- | src/elab_print.sml | 10 | ||||
-rw-r--r-- | src/elab_util.sml | 12 | ||||
-rw-r--r-- | src/elaborate.sml | 49 | ||||
-rw-r--r-- | src/explify.sml | 2 | ||||
-rw-r--r-- | src/urweb.grm | 27 | ||||
-rw-r--r-- | src/urweb.lex | 1 |
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)); |