Mercurial > urweb
changeset 1302:d008c4c43a0a
Flex kinds for type-level tuples; ::_ notation
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Sun, 10 Oct 2010 13:07:38 -0400 |
| parents | 4359e185d3af |
| children | c7b9a33c26c8 |
| files | demo/batchFun.ur demo/crud.ur demo/metaform.ur doc/manual.tex src/elab.sml src/elab_print.sml src/elab_util.sml src/elaborate.sml src/explify.sml src/urweb.grm src/urweb.lex tests/ktuple.ur tests/ktuple.urp |
| diffstat | 13 files changed, 125 insertions(+), 56 deletions(-) [+] |
line wrap: on
line diff
--- 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 @@ <tr> <td>{[r.Id]}</td> {@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 => <xml><td>{m.Show v}</td></xml>) M.fl M.cols (r -- #Id)} {if withDel then @@ -89,8 +86,7 @@ <tr> <th>Id</th> {@mapX [colMeta] [_] - (fn [nm :: Name] [p :: (Type * Type)] [rest :: {(Type * Type)}] - [[nm] ~ rest] m => + (fn [nm :: Name] [p ::_] [rest ::_] [[nm] ~ rest] m => <xml><th>{[m.Nam]}</th></xml>) M.fl M.cols} </tr> @@ -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 @@ <table> <tr> <th>Id:</th> <td><ctextbox source={id}/></td> </tr> {@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 => <xml><tr> <th>{[m.Nam]}:</th> <td>{m.Widget s}</td> </tr></xml>) M.fl M.cols inps} <tr> <th/> <td><button value="Batch it" onclick={add ()}/></td> </tr>
--- 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 @@ <tr> <td>{[fs.T.Id]}</td> {@mapX2 [fst] [colMeta] [tr] - (fn [nm :: Name] [t :: (Type * Type)] [rest :: {(Type * Type)}] - [[nm] ~ rest] v col => <xml> - <td>{col.Show v}</td> - </xml>) + (fn [nm :: Name] [t ::_] [rest ::_] [[nm] ~ rest] v col => <xml> + <td>{col.Show v}</td> + </xml>) M.fl (fs.T -- #Id) M.cols} <td> <a link={upd fs.T.Id}>[Update]</a> @@ -67,10 +66,9 @@ <tr> <th>ID</th> {@mapX [colMeta] [tr] - (fn [nm :: Name] [t :: (Type * Type)] [rest :: {(Type * Type)}] - [[nm] ~ rest] col => <xml> - <th>{cdata col.Nam}</th> - </xml>) + (fn [nm :: Name] [t ::_] [rest ::_] [[nm] ~ rest] col => <xml> + <th>{cdata col.Nam}</th> + </xml>) M.fl M.cols} </tr> {rows} @@ -79,12 +77,11 @@ <br/><hr/><br/> <form> - {@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)) => <xml> - <li> {cdata col.Nam}: {col.Widget [nm]}</li> - {useMore acc} - </xml>) + {@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)) => <xml> + <li> {cdata col.Nam}: {col.Widget [nm]}</li> + {useMore acc} + </xml>) <xml/> 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 <xml><body>Not found!</body></xml> | Some fs => return <xml><body><form> - {@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)) => <xml> <li> {cdata col.Nam}: {col.WidgetPopulated [nm] v}</li>
--- 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 <xml><body> {@mapUX2 [string] [string] [body] - (fn [nm :: Name] [rest :: {Unit}] [[nm] ~ rest] name value => <xml> + (fn [nm :: Name] [rest ::_] [[nm] ~ rest] name value => <xml> <li> {[name]} = {[value]}</li> </xml>) M.fl M.names values} @@ -14,8 +14,8 @@ fun main () = return <xml><body> <form> - {@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)) => <xml> <li> {[name]}: <textbox{nm}/></li> {useMore acc}
--- 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.
--- 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
--- 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 "<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)
--- 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' =>
--- 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
--- 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)
--- 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)
--- 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 @@ <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));