summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2010-10-10 13:07:38 -0400
committerGravatar Adam Chlipala <adam@chlipala.net>2010-10-10 13:07:38 -0400
commitbfeac162a328dba937a28e747e4fc4006fac500c (patch)
tree1d0f355dec824a81d80e9e838e0cae8845f8e179
parent81934ea4c2cf2260b6000e9be4d13e328204929a (diff)
Flex kinds for type-level tuples; ::_ notation
-rw-r--r--demo/batchFun.ur22
-rw-r--r--demo/crud.ur46
-rw-r--r--demo/metaform.ur6
-rw-r--r--doc/manual.tex2
-rw-r--r--src/elab.sml1
-rw-r--r--src/elab_print.sml10
-rw-r--r--src/elab_util.sml12
-rw-r--r--src/elaborate.sml49
-rw-r--r--src/explify.sml2
-rw-r--r--src/urweb.grm27
-rw-r--r--src/urweb.lex1
-rw-r--r--tests/ktuple.ur2
-rw-r--r--tests/ktuple.urp1
13 files changed, 125 insertions, 56 deletions
diff --git a/demo/batchFun.ur b/demo/batchFun.ur
index f665b132..ca48c7dc 100644
--- a/demo/batchFun.ur
+++ b/demo/batchFun.ur
@@ -6,7 +6,7 @@ con colMeta = fn (db :: Type, state :: Type) =>
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 @@ functor Make(M : sig
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 @@ functor Make(M : sig
<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 @@ functor Make(M : sig
<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 @@ functor Make(M : sig
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 @@ functor Make(M : sig
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 @@ functor Make(M : sig
<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>
diff --git a/demo/crud.ur b/demo/crud.ur
index 82739772..2fc82c1b 100644
--- a/demo/crud.ur
+++ b/demo/crud.ur
@@ -5,7 +5,7 @@ con colMeta = fn (db :: Type, widget :: Type) =>
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 @@ functor Make(M : sig
<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 @@ functor Make(M : sig
<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 @@ functor Make(M : sig
<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 @@ functor Make(M : sig
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 @@ functor Make(M : sig
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 @@ functor Make(M : sig
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>
diff --git a/demo/metaform.ur b/demo/metaform.ur
index 0a664005..729b7d08 100644
--- a/demo/metaform.ur
+++ b/demo/metaform.ur
@@ -6,7 +6,7 @@ functor Make (M : sig
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 @@ functor Make (M : sig
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}
diff --git a/doc/manual.tex b/doc/manual.tex
index 98b3b63c..9dbdb505 100644
--- a/doc/manual.tex
+++ b/doc/manual.tex
@@ -495,6 +495,8 @@ A tuple type $(\tau_1, \ldots, \tau_n)$ expands to a record type $\{1 = \tau_1,
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 --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));
diff --git a/tests/ktuple.ur b/tests/ktuple.ur
new file mode 100644
index 00000000..040578e0
--- /dev/null
+++ b/tests/ktuple.ur
@@ -0,0 +1,2 @@
+type q = (fn p => p.1) (int, float)
+type q = (fn p => p.1 * $p.3) (int, float, [])
diff --git a/tests/ktuple.urp b/tests/ktuple.urp
new file mode 100644
index 00000000..c466588c
--- /dev/null
+++ b/tests/ktuple.urp
@@ -0,0 +1 @@
+ktuple