# HG changeset patch # User Adam Chlipala # Date 1286730458 14400 # Node ID d008c4c43a0a8aae3983a208e3cff5480c40c69b # Parent 4359e185d3af3d33352284dd5069bff1bdaab44c Flex kinds for type-level tuples; ::_ notation diff -r 4359e185d3af -r d008c4c43a0a demo/batchFun.ur --- a/demo/batchFun.ur Thu Sep 30 18:29:59 2010 -0400 +++ b/demo/batchFun.ur Sun Oct 10 13:07:38 2010 -0400 @@ -6,7 +6,7 @@ NewState : transaction state, Widget : state -> xbody, ReadState : state -> transaction db} -con colsMeta = fn cols :: {(Type * Type)} => $(map colMeta cols) +con colsMeta = fn cols => $(map colMeta cols) fun default [t] (sh : show t) (rd : read t) (inj : sql_injectable t) name : colMeta (t, source string) = @@ -46,10 +46,8 @@ fun add r = dml (insert t (@foldR2 [fst] [colMeta] - [fn cols => $(map (fn t :: (Type * Type) => - sql_exp [] [] [] t.1) cols)] - (fn [nm :: Name] [t :: (Type * Type)] [rest :: {(Type * Type)}] - [[nm] ~ rest] input col acc => + [fn cols => $(map (fn t => sql_exp [] [] [] t.1) cols)] + (fn [nm :: Name] [t ::_] [rest ::_] [[nm] ~ rest] input col acc => acc ++ {nm = @sql_inject col.Inject input}) {} M.fl (r -- #Id) M.cols ++ {Id = (SQL {[r.Id]})})) @@ -73,8 +71,7 @@ {[r.Id]} {@mapX2 [colMeta] [fst] [_] - (fn [nm :: Name] [p :: (Type * Type)] [rest :: {(Type * Type)}] - [[nm] ~ rest] m v => + (fn [nm :: Name] [p ::_] [rest ::_] [[nm] ~ rest] m v => {m.Show v}) M.fl M.cols (r -- #Id)} {if withDel then @@ -89,8 +86,7 @@ Id {@mapX [colMeta] [_] - (fn [nm :: Name] [p :: (Type * Type)] [rest :: {(Type * Type)}] - [[nm] ~ rest] m => + (fn [nm :: Name] [p ::_] [rest ::_] [[nm] ~ rest] m => {[m.Nam]}) M.fl M.cols} @@ -104,7 +100,7 @@ id <- source ""; inps <- @foldR [colMeta] [fn r => transaction ($(map snd r))] - (fn [nm :: Name] [p :: (Type * Type)] [rest :: {(Type * Type)}] [[nm] ~ rest] m acc => + (fn [nm :: Name] [p ::_] [rest ::_] [[nm] ~ rest] m acc => s <- m.NewState; r <- acc; return ({nm = s} ++ r)) @@ -115,8 +111,7 @@ fun add () = id <- get id; vs <- @foldR2 [colMeta] [snd] [fn r => transaction ($(map fst r))] - (fn [nm :: Name] [p :: (Type * Type)] [rest :: {(Type * Type)}] - [[nm] ~ rest] m s acc => + (fn [nm :: Name] [p ::_] [rest ::_] [[nm] ~ rest] m s acc => v <- m.ReadState s; r <- acc; return ({nm = v} ++ r)) @@ -145,8 +140,7 @@ {@mapX2 [colMeta] [snd] [_] - (fn [nm :: Name] [p :: (Type * Type)] [rest :: {(Type * Type)}] - [[nm] ~ rest] m s => + (fn [nm :: Name] [p ::_] [rest ::_] [[nm] ~ rest] m s => ) M.fl M.cols inps} diff -r 4359e185d3af -r d008c4c43a0a demo/crud.ur --- a/demo/crud.ur Thu Sep 30 18:29:59 2010 -0400 +++ b/demo/crud.ur Sun Oct 10 13:07:38 2010 -0400 @@ -5,7 +5,7 @@ WidgetPopulated : nm :: Name -> db -> xml form [] [nm = widget], Parse : widget -> db, Inject : sql_injectable db} -con colsMeta = fn cols :: {(Type * Type)} => $(map colMeta cols) +con colsMeta = fn cols => $(map colMeta cols) fun default [t] (sh : show t) (rd : read t) (inj : sql_injectable t) name : colMeta (t, string) = @@ -51,10 +51,9 @@ {@mapX2 [fst] [colMeta] [tr] - (fn [nm :: Name] [t :: (Type * Type)] [rest :: {(Type * Type)}] - [[nm] ~ rest] v col => - - ) + (fn [nm :: Name] [t ::_] [rest ::_] [[nm] ~ rest] v col => + + ) M.fl (fs.T -- #Id) M.cols} {@mapX [colMeta] [tr] - (fn [nm :: Name] [t :: (Type * Type)] [rest :: {(Type * Type)}] - [[nm] ~ rest] col => - - ) + (fn [nm :: Name] [t ::_] [rest ::_] [[nm] ~ rest] col => + + ) M.fl M.cols} {rows} @@ -79,12 +77,11 @@


- {@foldR [colMeta] [fn cols :: {(Type * Type)} => xml form [] (map snd cols)] - (fn [nm :: Name] [t :: (Type * Type)] [rest :: {(Type * Type)}] - [[nm] ~ rest] (col : colMeta t) (acc : xml form [] (map snd rest)) => -
  • {cdata col.Nam}: {col.Widget [nm]}
  • - {useMore acc} -
    ) + {@foldR [colMeta] [fn cols => xml form [] (map snd cols)] + (fn [nm :: Name] [t ::_] [rest ::_] [[nm] ~ rest] (col : colMeta t) (acc : xml form [] (map snd rest)) => +
  • {cdata col.Nam}: {col.Widget [nm]}
  • + {useMore acc} +
    ) M.fl M.cols} @@ -96,10 +93,8 @@ id <- nextval seq; dml (insert tab (@foldR2 [snd] [colMeta] - [fn cols => $(map (fn t :: (Type * Type) => - sql_exp [] [] [] t.1) cols)] - (fn [nm :: Name] [t :: (Type * Type)] [rest :: {(Type * Type)}] - [[nm] ~ rest] => + [fn cols => $(map (fn t => sql_exp [] [] [] t.1) cols)] + (fn [nm :: Name] [t ::_] [rest ::_] [[nm] ~ rest] => fn input col acc => acc ++ {nm = @sql_inject col.Inject (col.Parse input)}) {} M.fl inputs M.cols ++ {Id = (SQL {[id]})})); @@ -115,12 +110,8 @@ fun save (inputs : $(map snd M.cols)) = dml (update [map fst M.cols] (@foldR2 [snd] [colMeta] - [fn cols => $(map (fn t :: (Type * Type) => - sql_exp [T = [Id = int] - ++ map fst M.cols] - [] [] t.1) cols)] - (fn [nm :: Name] [t :: (Type * Type)] [rest :: {(Type * Type)}] - [[nm] ~ rest] => + [fn cols => $(map (fn t => sql_exp [T = [Id = int] ++ map fst M.cols] [] [] t.1) cols)] + (fn [nm :: Name] [t ::_] [rest ::_] [[nm] ~ rest] => fn input col acc => acc ++ {nm = @sql_inject col.Inject (col.Parse input)}) {} M.fl inputs M.cols) @@ -136,9 +127,8 @@ case fso : (Basis.option {Tab : $(map fst M.cols)}) of None => return Not found! | Some fs => return - {@foldR2 [fst] [colMeta] [fn cols :: {(Type * Type)} => xml form [] (map snd cols)] - (fn [nm :: Name] [t :: (Type * Type)] [rest :: {(Type * Type)}] - [[nm] ~ rest] (v : t.1) (col : colMeta t) + {@foldR2 [fst] [colMeta] [fn cols => xml form [] (map snd cols)] + (fn [nm :: Name] [t ::_] [rest ::_] [[nm] ~ rest] (v : t.1) (col : colMeta t) (acc : xml form [] (map snd rest)) =>
  • {cdata col.Nam}: {col.WidgetPopulated [nm] v}
  • diff -r 4359e185d3af -r d008c4c43a0a demo/metaform.ur --- a/demo/metaform.ur Thu Sep 30 18:29:59 2010 -0400 +++ b/demo/metaform.ur Sun Oct 10 13:07:38 2010 -0400 @@ -6,7 +6,7 @@ fun handler values = return {@mapUX2 [string] [string] [body] - (fn [nm :: Name] [rest :: {Unit}] [[nm] ~ rest] name value => + (fn [nm :: Name] [rest ::_] [[nm] ~ rest] name value =>
  • {[name]} = {[value]}
  • ) M.fl M.names values} @@ -14,8 +14,8 @@ fun main () = return - {@foldUR [string] [fn cols :: {Unit} => xml form [] (mapU string cols)] - (fn [nm :: Name] [rest :: {Unit}] [[nm] ~ rest] name + {@foldUR [string] [fn cols => xml form [] (mapU string cols)] + (fn [nm :: Name] [rest ::_] [[nm] ~ rest] name (acc : xml form [] (mapU string rest)) =>
  • {[name]}:
  • {useMore acc} diff -r 4359e185d3af -r d008c4c43a0a doc/manual.tex --- a/doc/manual.tex Thu Sep 30 18:29:59 2010 -0400 +++ b/doc/manual.tex Sun Oct 10 13:07:38 2010 -0400 @@ -495,6 +495,8 @@ In general, several adjacent $\lambda$ forms may be combined into one, and kind and type annotations may be omitted, in which case they are implicitly included as wildcards. More formally, for constructor-level abstractions, we can define a new non-terminal $b ::= x \mid (x :: \kappa) \mid X$ and allow composite abstractions of the form $\lambda b^+ \Rightarrow c$, elaborating into the obvious sequence of one core $\lambda$ per element of $b^+$. +In some contexts, the parser isn't happy with token sequences like $x :: \_$, to indicate a constructor variable of wildcard kind. In such cases, write the second two tokens as $::\hspace{-.05in}\_$, with no intervening spaces. + For any signature item or declaration that defines some entity to be equal to $A$ with classification annotation $B$ (e.g., $\mt{val} \; x : B = A$), $B$ and the preceding colon (or similar punctuation) may be omitted, in which case it is filled in as a wildcard. A signature item or declaration $\mt{type} \; x$ or $\mt{type} \; x = \tau$ is elaborated into $\mt{con} \; x :: \mt{Type}$ or $\mt{con} \; x :: \mt{Type} = \tau$, respectively. diff -r 4359e185d3af -r d008c4c43a0a src/elab.sml --- a/src/elab.sml Thu Sep 30 18:29:59 2010 -0400 +++ b/src/elab.sml Sun Oct 10 13:07:38 2010 -0400 @@ -39,6 +39,7 @@ | 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 -r 4359e185d3af -r d008c4c43a0a src/elab_print.sml --- a/src/elab_print.sml Thu Sep 30 18:29:59 2010 -0400 +++ b/src/elab_print.sml Sun Oct 10 13:07:38 2010 -0400 @@ -56,6 +56,16 @@ | KError => string "" | KUnif (_, _, ref (SOME k)) => p_kind' par env k | KUnif (_, s, _) => string ("") + | 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 -r 4359e185d3af -r d008c4c43a0a src/elab_util.sml --- a/src/elab_util.sml Thu Sep 30 18:29:59 2010 -0400 +++ b/src/elab_util.sml Sun Oct 10 13:07:38 2010 -0400 @@ -78,6 +78,16 @@ | 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 @@ | 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 -r 4359e185d3af -r d008c4c43a0a src/elaborate.sml --- a/src/elaborate.sml Thu Sep 30 18:29:59 2010 -0400 +++ b/src/elaborate.sml Sun Oct 10 13:07:38 2010 -0400 @@ -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 @@ | 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 -r 4359e185d3af -r d008c4c43a0a src/explify.sml --- a/src/explify.sml Thu Sep 30 18:29:59 2010 -0400 +++ b/src/explify.sml Sun Oct 10 13:07:38 2010 -0400 @@ -44,6 +44,8 @@ | 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 -r 4359e185d3af -r d008c4c43a0a src/urweb.grm --- a/src/urweb.grm Thu Sep 30 18:29:59 2010 -0400 +++ b/src/urweb.grm Sun Oct 10 13:07:38 2010 -0400 @@ -212,7 +212,7 @@ | 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 @@ kopt : (NONE) | DCOLON kind (SOME kind) + | DCOLONWILD (SOME (KWild, s (DCOLONWILDleft, DCOLONWILDright))) dargs : ([]) | SYMBOL dargs (SYMBOL :: dargs) @@ -853,6 +854,22 @@ ((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 @@ ((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 -r 4359e185d3af -r d008c4c43a0a src/urweb.lex --- a/src/urweb.lex Thu Sep 30 18:29:59 2010 -0400 +++ b/src/urweb.lex Sun Oct 10 13:07:38 2010 -0400 @@ -372,6 +372,7 @@ ">=" => (Tokens.GE (pos yypos, pos yypos + size yytext)); "," => (Tokens.COMMA (pos yypos, pos yypos + size yytext)); ":::" => (Tokens.TCOLON (pos yypos, pos yypos + size yytext)); + "::_" => (Tokens.DCOLONWILD (pos yypos, pos yypos + size yytext)); "::" => (Tokens.DCOLON (pos yypos, pos yypos + size yytext)); ":" => (Tokens.COLON (pos yypos, pos yypos + size yytext)); "..." => (Tokens.DOTDOTDOT (pos yypos, pos yypos + size yytext)); diff -r 4359e185d3af -r d008c4c43a0a tests/ktuple.ur --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/tests/ktuple.ur Sun Oct 10 13:07:38 2010 -0400 @@ -0,0 +1,2 @@ +type q = (fn p => p.1) (int, float) +type q = (fn p => p.1 * $p.3) (int, float, []) diff -r 4359e185d3af -r d008c4c43a0a tests/ktuple.urp --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/tests/ktuple.urp Sun Oct 10 13:07:38 2010 -0400 @@ -0,0 +1,1 @@ +ktuple
    Id:
    {[m.Nam]}: {m.Widget s}
    {[fs.T.Id]}{col.Show v}{col.Show v} [Update] @@ -67,10 +66,9 @@
    ID{cdata col.Nam}{cdata col.Nam}