Mercurial > urweb
changeset 1093:8d3aa6c7cee0
Make summary unification more conservative; infer implicit arguments after applications
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Sat, 26 Dec 2009 11:56:40 -0500 |
| parents | 6f4b05fc4361 |
| children | db52c32dbe42 |
| files | CHANGELOG demo/batchFun.ur demo/crud.ur demo/metaform.ur demo/more/dbgrid.ur demo/more/grid.ur demo/more/grid1.ur demo/more/orm.ur demo/more/orm1.ur demo/more/versioned.ur demo/sum.ur demo/tcSum.ur lib/ur/monad.ur lib/ur/monad.urs lib/ur/top.ur lib/ur/top.urs src/elaborate.sml src/urweb.grm tests/impl.ur tests/impl.urp |
| diffstat | 20 files changed, 429 insertions(+), 381 deletions(-) [+] |
line wrap: on
line diff
--- a/CHANGELOG Fri Dec 25 10:48:02 2009 -0500 +++ b/CHANGELOG Sat Dec 26 11:56:40 2009 -0500 @@ -2,6 +2,7 @@ Next ======== +- Automatic insertion of implicit arguments in more positions - Reifying expressions as URLs and redirecting to them explicitly - More syntactic sugar for SQL - Typing of SQL queries no longer exposes which tables were used in joins but
--- a/demo/batchFun.ur Fri Dec 25 10:48:02 2009 -0500 +++ b/demo/batchFun.ur Sat Dec 26 11:56:40 2009 -0500 @@ -45,14 +45,14 @@ 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 => - acc ++ {nm = @sql_inject col.Inject input}) - {} [M.cols] M.fl (r -- #Id) M.cols - ++ {Id = (SQL {[r.Id]})})) + (@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 => + acc ++ {nm = @sql_inject col.Inject input}) + {} M.fl (r -- #Id) M.cols + ++ {Id = (SQL {[r.Id]})})) fun doBatch ls = case ls of @@ -72,11 +72,11 @@ | Cons (r, ls) => <xml> <tr> <td>{[r.Id]}</td> - {foldRX2 [colMeta] [fst] [_] - (fn [nm :: Name] [p :: (Type * Type)] [rest :: {(Type * Type)}] - [[nm] ~ rest] m v => - <xml><td>{m.Show v}</td></xml>) - [M.cols] M.fl M.cols (r -- #Id)} + {@foldRX2 [colMeta] [fst] [_] + (fn [nm :: Name] [p :: (Type * Type)] [rest :: {(Type * Type)}] + [[nm] ~ rest] m v => + <xml><td>{m.Show v}</td></xml>) + M.fl M.cols (r -- #Id)} {if withDel then <xml><td><button value="Delete" onclick={rpc (del r.Id)}/></td></xml> else @@ -88,11 +88,11 @@ <xml><dyn signal={ls <- signal lss; return <xml><table> <tr> <th>Id</th> - {foldRX [colMeta] [_] - (fn [nm :: Name] [p :: (Type * Type)] [rest :: {(Type * Type)}] - [[nm] ~ rest] m => - <xml><th>{[m.Nam]}</th></xml>) - [M.cols] M.fl M.cols} + {@foldRX [colMeta] [_] + (fn [nm :: Name] [p :: (Type * Type)] [rest :: {(Type * Type)}] + [[nm] ~ rest] m => + <xml><th>{[m.Nam]}</th></xml>) + M.fl M.cols} </tr> {show' ls} </table></xml>}/></xml> @@ -103,25 +103,25 @@ batched <- source Nil; id <- source ""; - inps <- foldR [colMeta] [fn r => transaction ($(map snd r))] - (fn [nm :: Name] [p :: (Type * Type)] [rest :: {(Type * Type)}] [[nm] ~ rest] m acc => - s <- m.NewState; - r <- acc; - return ({nm = s} ++ r)) - (return {}) - [M.cols] M.fl M.cols; - + inps <- @foldR [colMeta] [fn r => transaction ($(map snd r))] + (fn [nm :: Name] [p :: (Type * Type)] [rest :: {(Type * Type)}] [[nm] ~ rest] m acc => + s <- m.NewState; + r <- acc; + return ({nm = s} ++ r)) + (return {}) + M.fl M.cols; + let 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 => - v <- m.ReadState s; - r <- acc; - return ({nm = v} ++ r)) - (return {}) - [M.cols] M.fl M.cols inps; + vs <- @foldR2 [colMeta] [snd] [fn r => transaction ($(map fst r))] + (fn [nm :: Name] [p :: (Type * Type)] [rest :: {(Type * Type)}] + [[nm] ~ rest] m s acc => + v <- m.ReadState s; + r <- acc; + return ({nm = v} ++ r)) + (return {}) + M.fl M.cols inps; ls <- get batched; set batched (Cons ({Id = readError id} ++ vs, ls)) @@ -144,11 +144,11 @@ <table> <tr> <th>Id:</th> <td><ctextbox source={id}/></td> </tr> - {foldRX2 [colMeta] [snd] [_] - (fn [nm :: Name] [p :: (Type * Type)] [rest :: {(Type * Type)}] - [[nm] ~ rest] m s => - <xml><tr> <th>{[m.Nam]}:</th> <td>{m.Widget s}</td> </tr></xml>) - [M.cols] M.fl M.cols inps} + {@foldRX2 [colMeta] [snd] [_] + (fn [nm :: Name] [p :: (Type * Type)] [rest :: {(Type * Type)}] + [[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> </table>
--- a/demo/crud.ur Fri Dec 25 10:48:02 2009 -0500 +++ b/demo/crud.ur Sat Dec 26 11:56:40 2009 -0500 @@ -50,12 +50,12 @@ (fn (fs : {T : $([Id = int] ++ map fst M.cols)}) => <xml> <tr> <td>{[fs.T.Id]}</td> - {foldRX2 [fst] [colMeta] [tr] - (fn [nm :: Name] [t :: (Type * Type)] [rest :: {(Type * Type)}] - [[nm] ~ rest] v col => <xml> - <td>{col.Show v}</td> - </xml>) - [M.cols] M.fl (fs.T -- #Id) M.cols} + {@foldRX2 [fst] [colMeta] [tr] + (fn [nm :: Name] [t :: (Type * Type)] [rest :: {(Type * Type)}] + [[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> <a link={confirm fs.T.Id}>[Delete]</a> @@ -66,12 +66,12 @@ <table border={1}> <tr> <th>ID</th> - {foldRX [colMeta] [tr] - (fn [nm :: Name] [t :: (Type * Type)] [rest :: {(Type * Type)}] - [[nm] ~ rest] col => <xml> - <th>{cdata col.Nam}</th> - </xml>) - [M.cols] M.fl M.cols} + {@foldRX [colMeta] [tr] + (fn [nm :: Name] [t :: (Type * Type)] [rest :: {(Type * Type)}] + [[nm] ~ rest] col => <xml> + <th>{cdata col.Nam}</th> + </xml>) + M.fl M.cols} </tr> {rows} </table> @@ -79,14 +79,14 @@ <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>) - <xml/> - [M.cols] M.fl M.cols} + {@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>) + <xml/> + M.fl M.cols} <submit action={create}/> </form> @@ -95,13 +95,13 @@ and create (inputs : $(map snd M.cols)) = 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 input col acc => acc ++ {nm = @sql_inject col.Inject (col.Parse input)}) - {} [M.cols] M.fl inputs M.cols + (@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 input col acc => acc ++ {nm = @sql_inject col.Inject (col.Parse input)}) + {} M.fl inputs M.cols ++ {Id = (SQL {[id]})})); ls <- list (); return <xml><body> @@ -113,17 +113,17 @@ and upd (id : int) = let 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 input col acc => acc ++ {nm = - @sql_inject col.Inject (col.Parse input)}) - {} [M.cols] M.fl inputs 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 input col acc => acc ++ {nm = + @sql_inject col.Inject (col.Parse input)}) + {} M.fl inputs M.cols) tab (WHERE T.Id = {[id]})); ls <- list (); return <xml><body> @@ -136,16 +136,16 @@ 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) - (acc : xml form [] (map snd rest)) => - <xml> - <li> {cdata col.Nam}: {col.WidgetPopulated [nm] v}</li> - {useMore acc} - </xml>) - <xml/> - [M.cols] M.fl fs.Tab M.cols} + {@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) + (acc : xml form [] (map snd rest)) => + <xml> + <li> {cdata col.Nam}: {col.WidgetPopulated [nm] v}</li> + {useMore acc} + </xml>) + <xml/> + M.fl fs.Tab M.cols} <submit action={save}/> </form></body></xml>
--- a/demo/metaform.ur Fri Dec 25 10:48:02 2009 -0500 +++ b/demo/metaform.ur Sat Dec 26 11:56:40 2009 -0500 @@ -5,23 +5,23 @@ end) = struct fun handler values = return <xml><body> - {foldURX2 [string] [string] [body] - (fn [nm :: Name] [rest :: {Unit}] [[nm] ~ rest] name value => <xml> - <li> {[name]} = {[value]}</li> - </xml>) - [M.fs] M.fl M.names values} + {@foldURX2 [string] [string] [body] + (fn [nm :: Name] [rest :: {Unit}] [[nm] ~ rest] name value => <xml> + <li> {[name]} = {[value]}</li> + </xml>) + M.fl M.names values} </body></xml> fun main () = return <xml><body> <form> - {foldUR [string] [fn cols :: {Unit} => xml form [] (mapU string cols)] - (fn [nm :: Name] [rest :: {Unit}] [[nm] ~ rest] name - (acc : xml form [] (mapU string rest)) => <xml> - <li> {[name]}: <textbox{nm}/></li> - {useMore acc} - </xml>) - <xml/> - [M.fs] M.fl M.names} + {@foldUR [string] [fn cols :: {Unit} => xml form [] (mapU string cols)] + (fn [nm :: Name] [rest :: {Unit}] [[nm] ~ rest] name + (acc : xml form [] (mapU string rest)) => <xml> + <li> {[name]}: <textbox{nm}/></li> + {useMore acc} + </xml>) + <xml/> + M.fl M.names} <submit action={handler}/> </form> </body></xml>
--- a/demo/more/dbgrid.ur Fri Dec 25 10:48:02 2009 -0500 +++ b/demo/more/dbgrid.ur Sat Dec 26 11:56:40 2009 -0500 @@ -384,31 +384,31 @@ val wholeRow = @Folder.concat ! M.keyFolder M.rowFolder fun ensql [env] (r : $(M.key ++ M.row)) = - map2 [rawMeta] [id] [sql_exp env [] []] - (fn [t] meta v => @sql_inject meta.Inj v) - [_] wholeRow M.raw r + @map2 [rawMeta] [id] [sql_exp env [] []] + (fn [t] meta v => @sql_inject meta.Inj v) + wholeRow M.raw r val new = - row <- Monad.mapR [rawMeta] [id] - (fn [nm :: Name] [t :: Type] meta => meta.New) - [_] wholeRow M.raw; + row <- @Monad.mapR _ [rawMeta] [id] + (fn [nm :: Name] [t :: Type] meta => meta.New) + wholeRow M.raw; dml (insert M.tab (ensql row)); return row fun selector (r : $M.key) : sql_exp [T = M.key ++ M.row] [] [] bool = - foldR2 [rawMeta] [id] - [fn key => rest :: {Type} -> [rest ~ key] => sql_exp [T = key ++ rest] [] [] bool] - (fn [nm :: Name] [t :: Type] [key :: {Type}] [[nm] ~ key] - (meta : rawMeta t) (v : t) - (exp : rest :: {Type} -> [rest ~ key] => sql_exp [T = key ++ rest] [] [] bool) - [rest :: {Type}] [rest ~ [nm = t] ++ key] => - (WHERE T.{nm} = {@sql_inject meta.Inj v} AND {exp [[nm = t] ++ rest] !})) - (fn [rest :: {Type}] [rest ~ []] => (WHERE TRUE)) - [_] M.keyFolder (M.raw --- map rawMeta M.row) r - [_] ! + @foldR2 [rawMeta] [id] + [fn key => rest :: {Type} -> [rest ~ key] => sql_exp [T = key ++ rest] [] [] bool] + (fn [nm :: Name] [t :: Type] [key :: {Type}] [[nm] ~ key] + (meta : rawMeta t) (v : t) + (exp : rest :: {Type} -> [rest ~ key] => sql_exp [T = key ++ rest] [] [] bool) + [rest :: {Type}] [rest ~ [nm = t] ++ key] => + (WHERE T.{nm} = {@sql_inject meta.Inj v} AND {exp [[nm = t] ++ rest] !})) + (fn [rest :: {Type}] [rest ~ []] => (WHERE TRUE)) + M.keyFolder (M.raw --- map rawMeta M.row) r + [_] ! fun save key row = - dml (update [M.key ++ M.row] ! + dml (update [M.key ++ M.row] (ensql row) M.tab (selector key))
--- a/demo/more/grid.ur Fri Dec 25 10:48:02 2009 -0500 +++ b/demo/more/grid.ur Sat Dec 26 11:56:40 2009 -0500 @@ -49,9 +49,9 @@ fun make (row : M.row) [input] [filter] (m : colMeta' M.row input filter) : transaction input = m.Project row fun makeAll cols row = @@Monad.exec [transaction] _ [map snd3 M.cols] - (map2 [fst3] [colMeta M.row] [fn p => transaction (snd3 p)] - (fn [p] data meta => make row [_] [_] (meta.Handlers data)) - [_] M.folder cols M.cols) + (@map2 [fst3] [colMeta M.row] [fn p => transaction (snd3 p)] + (fn [p] data meta => make row(meta.Handlers data)) + M.folder cols M.cols) (@@Folder.mp [_] [_] M.folder) type grid = {Cols : $(map fst3 M.cols), @@ -80,14 +80,14 @@ Monad.ignore (Dlist.append rows r) val grid = - cols <- Monad.mapR [colMeta M.row] [fst3] - (fn [nm :: Name] [p :: (Type * Type * Type)] meta => meta.Initialize) - [_] M.folder M.cols; + cols <- @Monad.mapR _ [colMeta M.row] [fst3] + (fn [nm :: Name] [p :: (Type * Type * Type)] meta => meta.Initialize) + M.folder M.cols; - filters <- Monad.mapR2 [colMeta M.row] [fst3] [thd3] - (fn [nm :: Name] [p :: (Type * Type * Type)] meta state => - (meta.Handlers state).CreateFilter) - [_] M.folder M.cols cols; + filters <- @Monad.mapR2 _ [colMeta M.row] [fst3] [thd3] + (fn [nm :: Name] [p :: (Type * Type * Type)] meta state => + (meta.Handlers state).CreateFilter) + M.folder M.cols cols; rows <- Dlist.create; sel <- source False; @@ -109,30 +109,30 @@ fun myFilter grid all = row <- signal all.Row; - foldR3 [colMeta M.row] [fst3] [thd3] [fn _ => M.row -> signal bool] - (fn [nm :: Name] [p :: (Type * Type * Type)] - [rest :: {(Type * Type * Type)}] [[nm] ~ rest] - meta state filter combinedFilter row => - previous <- combinedFilter row; - this <- (meta.Handlers state).Filter filter row; - return (previous && this)) - (fn _ => return True) - [_] M.folder M.cols grid.Cols grid.Filters row + @foldR3 [colMeta M.row] [fst3] [thd3] [fn _ => M.row -> signal bool] + (fn [nm :: Name] [p :: (Type * Type * Type)] + [rest :: {(Type * Type * Type)}] [[nm] ~ rest] + meta state filter combinedFilter row => + previous <- combinedFilter row; + this <- (meta.Handlers state).Filter filter row; + return (previous && this)) + (fn _ => return True) + M.folder M.cols grid.Cols grid.Filters row fun render (grid : grid) = <xml> <table class={tabl}> <tr class={tr}> <th/> <th/> <th><button value="No sort" onclick={set grid.Sort None}/></th> - {foldRX2 [fst3] [colMeta M.row] [_] - (fn [nm :: Name] [p :: (Type * Type * Type)] [rest :: {(Type * Type * Type)}] [[nm] ~ rest] - data (meta : colMeta M.row p) => - <xml><th class={th}> - {case (meta.Handlers data).Sort of - None => txt (meta.Handlers data).Header - | sort => <xml><button value={(meta.Handlers data).Header} - onclick={set grid.Sort sort}/></xml>} - </th></xml>) - [_] M.folder grid.Cols M.cols} + {@foldRX2 [fst3] [colMeta M.row] [_] + (fn [nm :: Name] [p :: (Type * Type * Type)] [rest :: {(Type * Type * Type)}] [[nm] ~ rest] + data (meta : colMeta M.row p) => + <xml><th class={th}> + {case (meta.Handlers data).Sort of + None => txt (meta.Handlers data).Header + | sort => <xml><button value={(meta.Handlers data).Header} + onclick={set grid.Sort sort}/></xml>} + </th></xml>) + M.folder grid.Cols M.cols} </tr> {Dlist.render (fn {Row = rowS, Cols = colsS, Updating = ud, Selected = sd} pos => @@ -152,18 +152,18 @@ val save = cols <- get colsS; - errors <- Monad.foldR3 [fst3] [colMeta M.row] [snd3] [fn _ => option string] - (fn [nm :: Name] [p :: (Type * Type * Type)] [rest :: {(Type * Type * Type)}] - [[nm] ~ rest] data meta v errors => - b <- current ((meta.Handlers data).Validate v); - return (if b then - errors - else - case errors of - None => Some ((meta.Handlers data).Header) - | Some s => Some ((meta.Handlers data).Header - ^ ", " ^ s))) - None [_] M.folder grid.Cols M.cols cols; + errors <- @Monad.foldR3 _ [fst3] [colMeta M.row] [snd3] [fn _ => option string] + (fn [nm :: Name] [p :: (Type * Type * Type)] [rest :: {(Type * Type * Type)}] + [[nm] ~ rest] data meta v errors => + b <- current ((meta.Handlers data).Validate v); + return (if b then + errors + else + case errors of + None => Some ((meta.Handlers data).Header) + | Some s => Some ((meta.Handlers data).Header + ^ ", " ^ s))) + None M.folder grid.Cols M.cols cols; case errors of Some s => alert ("Can't save because the following columns have invalid values:\n" @@ -171,12 +171,12 @@ | None => set ud False; row <- get rowS; - row' <- Monad.foldR3 [fst3] [colMeta M.row] [snd3] [fn _ => M.row] - (fn [nm :: Name] [t :: (Type * Type * Type)] - [rest :: {(Type * Type * Type)}] - [[nm] ~ rest] data meta v row' => - (meta.Handlers data).Update row' v) - row [_] M.folder grid.Cols M.cols cols; + row' <- @Monad.foldR3 _ [fst3] [colMeta M.row] [snd3] [fn _ => M.row] + (fn [nm :: Name] [t :: (Type * Type * Type)] + [rest :: {(Type * Type * Type)}] + [[nm] ~ rest] data meta v row' => + (meta.Handlers data).Update row' v) + row M.folder grid.Cols M.cols cols; rpc (M.save (M.keyOf row) row'); set rowS row'; @@ -208,29 +208,29 @@ </td> <dyn signal={cols <- signal colsS; - return (foldRX3 [fst3] [colMeta M.row] [snd3] [_] - (fn [nm :: Name] [t :: (Type * Type * Type)] - [rest :: {(Type * Type * Type)}] - [[nm] ~ rest] data meta v => - <xml><td class={td}> - <dyn signal={b <- signal ud; - return (if b then - (meta.Handlers data).Edit v - else - (meta.Handlers data).Display - v)}/> - <dyn signal={b <- signal ud; - if b then - valid <- - (meta.Handlers data).Validate v; - return (if valid then - <xml/> - else - <xml>!</xml>) - else - return <xml/>}/> - </td></xml>) - [_] M.folder grid.Cols M.cols cols)}/> + return (@foldRX3 [fst3] [colMeta M.row] [snd3] [_] + (fn [nm :: Name] [t :: (Type * Type * Type)] + [rest :: {(Type * Type * Type)}] + [[nm] ~ rest] data meta v => + <xml><td class={td}> + <dyn signal={b <- signal ud; + return (if b then + (meta.Handlers data).Edit v + else + (meta.Handlers data).Display + v)}/> + <dyn signal={b <- signal ud; + if b then + valid <- + (meta.Handlers data).Validate v; + return (if valid then + <xml/> + else + <xml>!</xml>) + else + return <xml/>}/> + </td></xml>) + M.folder grid.Cols M.cols cols)}/> </tr></xml> end) {StartPosition = case M.pageLength of @@ -250,27 +250,27 @@ return (f r1 r2)) f)} grid.Rows} - <dyn signal={rows <- Dlist.foldl (fn row => Monad.mapR2 [aggregateMeta M.row] [id] [id] - (fn [nm :: Name] [t :: Type] meta acc => - Monad.mp (fn v => meta.Step v acc) - (signal row.Row)) - [_] M.aggFolder M.aggregates) - (mp [aggregateMeta M.row] [id] + <dyn signal={rows <- Dlist.foldl (fn row => @Monad.mapR2 _ [aggregateMeta M.row] [id] [id] + (fn [nm :: Name] [t :: Type] meta acc => + Monad.mp (fn v => meta.Step v acc) + (signal row.Row)) + M.aggFolder M.aggregates) + (@mp [aggregateMeta M.row] [id] (fn [t] meta => meta.Initial) - [_] M.aggFolder M.aggregates) grid.Rows; + M.aggFolder M.aggregates) grid.Rows; return <xml><tr> <th colspan={3}>Aggregates</th> - {foldRX2 [aggregateMeta M.row] [id] [_] - (fn [nm :: Name] [t :: Type] [rest :: {Type}] [[nm] ~ rest] meta acc => - <xml><td class={agg}>{meta.Display acc}</td></xml>) - [_] M.aggFolder M.aggregates rows} + {@foldRX2 [aggregateMeta M.row] [id] [_] + (fn [nm :: Name] [t :: Type] [rest :: {Type}] [[nm] ~ rest] meta acc => + <xml><td class={agg}>{meta.Display acc}</td></xml>) + M.aggFolder M.aggregates rows} </tr></xml>}/> <tr><th colspan={3}>Filters</th> - {foldRX3 [colMeta M.row] [fst3] [thd3] [_] - (fn [nm :: Name] [p :: (Type * Type * Type)] [rest :: {(Type * Type * Type)}] [[nm] ~ rest] - meta state filter => <xml><td>{(meta.Handlers state).DisplayFilter filter}</td></xml>) - [_] M.folder M.cols grid.Cols grid.Filters} + {@foldRX3 [colMeta M.row] [fst3] [thd3] [_] + (fn [nm :: Name] [p :: (Type * Type * Type)] [rest :: {(Type * Type * Type)}] [[nm] ~ rest] + meta state filter => <xml><td>{(meta.Handlers state).DisplayFilter filter}</td></xml>) + M.folder M.cols grid.Cols grid.Filters} </tr> </table>
--- a/demo/more/grid1.ur Fri Dec 25 10:48:02 2009 -0500 +++ b/demo/more/grid1.ur Sat Dec 26 11:56:40 2009 -0500 @@ -35,13 +35,13 @@ fun render r = r.A end) - val cols = {Id = Direct.readOnly [#Id] ! "Id" Direct.int, - A = Direct.editable [#A] ! "A" Direct.int, - B = Direct.editable [#B] ! "B" Direct.string, - C = Direct.editable [#C] ! "C" Direct.bool, - D = Direct.editable [#D] ! "D" F.meta, - E = Direct.editable [#E] ! "E" (Direct.nullable Direct.int), - F = Direct.editable [#F] ! "F" (Direct.nullable F.meta), + val cols = {Id = Direct.readOnly [#Id] "Id" Direct.int, + A = Direct.editable [#A] "A" Direct.int, + B = Direct.editable [#B] "B" Direct.string, + C = Direct.editable [#C] "C" Direct.bool, + D = Direct.editable [#D] "D" F.meta, + E = Direct.editable [#E] "E" (Direct.nullable Direct.int), + F = Direct.editable [#F] "F" (Direct.nullable F.meta), DA = computed "2A" (fn r => 2 * r.A), Link = computedHtml "Link" (fn r => <xml><a link={page (r.A, r.B)}>Go</a></xml>)}
--- a/demo/more/orm.ur Fri Dec 25 10:48:02 2009 -0500 +++ b/demo/more/orm.ur Sat Dec 26 11:56:40 2009 -0500 @@ -32,9 +32,9 @@ Inj = inj} fun ensql [avail] (r : row') : $(map (sql_exp avail [] []) fs') = - map2 [meta] [fst] [fn ts :: (Type * Type) => sql_exp avail [] [] ts.1] - (fn [ts] meta v => @sql_inject meta.Inj v) - [_] M.folder M.cols r + @map2 [meta] [fst] [fn ts :: (Type * Type) => sql_exp avail [] [] ts.1] + (fn [ts] meta v => @sql_inject meta.Inj v) + M.folder M.cols r fun create (r : row') = id <- nextval s; @@ -43,7 +43,7 @@ fun delete r = dml (DELETE FROM t WHERE t.Id = {[r.Id]}) - fun save r = dml (update [fs'] ! (ensql (r -- #Id)) t (WHERE T.Id = {[r.Id]})) + fun save r = dml (update [fs'] (ensql (r -- #Id)) t (WHERE T.Id = {[r.Id]})) fun lookup id = ro <- oneOrNoRows (SELECT * FROM t WHERE t.Id = {[id]}); @@ -59,20 +59,20 @@ {Col : {Exp : sql_exp [T = fs] [] [] col, Inj : sql_injectable col}, Parent : $fs -> transaction (option parent)} - val cols = foldR [meta] [fn before => after :: {(Type * Type)} -> [before ~ after] => - $(map (meta' (map fst (before ++ after))) before)] - (fn [nm :: Name] [ts :: (Type * Type)] [before :: {(Type * Type)}] - [[nm] ~ before] (meta : meta ts) - (acc : after :: {(Type * Type)} -> [before ~ after] => - $(map (meta' (map fst (before ++ after))) before)) - [after :: {(Type * Type)}] [[nm = ts] ++ before ~ after] => - {nm = {Col = {Exp = sql_field [#T] [nm], - Inj = meta.Inj}, - Parent = fn r => meta.Link r.nm}} - ++ acc [[nm = ts] ++ after] !) - (fn [after :: {(Type * Type)}] [[] ~ after] => {}) - [_] M.folder M.cols - [[Id = (id, row)]] ! + val cols = @foldR [meta] [fn before => after :: {(Type * Type)} -> [before ~ after] => + $(map (meta' (map fst (before ++ after))) before)] + (fn [nm :: Name] [ts :: (Type * Type)] [before :: {(Type * Type)}] + [[nm] ~ before] (meta : meta ts) + (acc : after :: {(Type * Type)} -> [before ~ after] => + $(map (meta' (map fst (before ++ after))) before)) + [after :: {(Type * Type)}] [[nm = ts] ++ before ~ after] => + {nm = {Col = {Exp = sql_field [#T] [nm], + Inj = meta.Inj}, + Parent = fn r => meta.Link r.nm}} + ++ acc [[nm = ts] ++ after] !) + (fn [after :: {(Type * Type)}] [[] ~ after] => {}) + M.folder M.cols + [[Id = (id, row)]] ! type filter = sql_exp [T = fs] [] [] bool fun find (f : filter) = resultOut (SELECT * FROM t WHERE {f}) @@ -80,12 +80,12 @@ fun bin (b : t ::: Type -> sql_binary t t bool) [t] (c : col t) (v : t) = sql_binary b c.Exp (@sql_inject c.Inj v) - val eq = bin @@sql_eq - val ne = bin @@sql_ne - val lt = bin @@sql_lt - val le = bin @@sql_le - val gt = bin @@sql_gt - val ge = bin @@sql_ge + val eq = @@bin @@sql_eq + val ne = @@bin @@sql_ne + val lt = @@bin @@sql_lt + val le = @@bin @@sql_le + val gt = @@bin @@sql_gt + val ge = @@bin @@sql_ge fun bb (b : sql_binary bool bool bool) (f1 : filter) (f2 : filter) = sql_binary b f1 f2
--- a/demo/more/orm1.ur Fri Dec 25 10:48:02 2009 -0500 +++ b/demo/more/orm1.ur Sat Dec 26 11:56:40 2009 -0500 @@ -1,13 +1,13 @@ open Orm structure T = Table(struct - val cols = {A = local [int] _, - B = local [string] _} + val cols = {A = local [int], + B = local [string]} end) structure S = Table(struct val cols = {C = T.id, - D = local [float] _} + D = local [float]} end) fun action () =
--- a/demo/more/versioned.ur Fri Dec 25 10:48:02 2009 -0500 +++ b/demo/more/versioned.ur Sat Dec 26 11:56:40 2009 -0500 @@ -24,33 +24,33 @@ Eq : eq t} fun keyRecd (r : $(M.key ++ M.data)) = - map2 [sql_injectable] [id] [sql_exp [] [] []] - (fn [t] => @sql_inject) - [_] M.keyFolder M.key (r --- M.data) + @map2 [sql_injectable] [id] [sql_exp [] [] []] + (fn [t] => @sql_inject) + M.keyFolder M.key (r --- M.data) fun insert r = vr <- nextval s; dml (Basis.insert t ({Version = (SQL {[vr]}), When = (SQL CURRENT_TIMESTAMP)} ++ keyRecd r - ++ map2 [dmeta] [id] + ++ @map2 [dmeta] [id] [fn t => sql_exp [] [] [] (option t)] (fn [t] x v => @sql_inject (@sql_option_prim x.Inj) (Some v)) - [_] M.dataFolder M.data (r --- M.key))) + M.dataFolder M.data (r --- M.key))) fun keyExp (r : $M.key) : sql_exp [T = all] [] [] bool = - foldR2 [sql_injectable] [id] [fn before => after :: {Type} -> [before ~ after] - => sql_exp [T = before ++ after] [] [] bool] - (fn [nm :: Name] [t :: Type] [before :: {Type}] [[nm] ~ before] - (inj : sql_injectable t) (v : t) - (e : after :: {Type} -> [before ~ after] - => sql_exp [T = before ++ after] [] [] bool) - [after :: {Type}] [[nm = t] ++ before ~ after] => - (SQL t.{nm} = {[v]} AND {e [[nm = t] ++ after] !})) - (fn [after :: {Type}] [[] ~ after] => (SQL TRUE)) - [_] M.keyFolder M.key r - [_] ! + @foldR2 [sql_injectable] [id] [fn before => after :: {Type} -> [before ~ after] + => sql_exp [T = before ++ after] [] [] bool] + (fn [nm :: Name] [t :: Type] [before :: {Type}] [[nm] ~ before] + (inj : sql_injectable t) (v : t) + (e : after :: {Type} -> [before ~ after] + => sql_exp [T = before ++ after] [] [] bool) + [after :: {Type}] [[nm = t] ++ before ~ after] => + (SQL t.{nm} = {[v]} AND {e [[nm = t] ++ after] !})) + (fn [after :: {Type}] [[] ~ after] => (SQL TRUE)) + M.keyFolder M.key r + [_] ! datatype bound = NoBound @@ -61,13 +61,13 @@ let fun current' vro r = let - val complete = foldR [option] [fn ts => option $ts] - (fn [nm :: Name] [v :: Type] [r :: {Type}] [[nm] ~ r] - v r => - case (v, r) of - (Some v, Some r) => Some ({nm = v} ++ r) - | _ => None) - (Some {}) [_] M.dataFolder r + val complete = @foldR [option] [fn ts => option $ts] + (fn [nm :: Name] [v :: Type] [r :: {Type}] [[nm] ~ r] + v r => + case (v, r) of + (Some v, Some r) => Some ({nm = v} ++ r) + | _ => None) + (Some {}) M.dataFolder r in case complete of Some r => return (Some r) @@ -88,19 +88,19 @@ None => return None | Some r' => let - val r = map2 [option] [option] [option] - (fn [t ::: Type] old new => - case old of - None => new - | Some _ => old) - [_] M.dataFolder r (r'.T -- #Version) + val r = @map2 [option] [option] [option] + (fn [t ::: Type] old new => + case old of + None => new + | Some _ => old) + M.dataFolder r (r'.T -- #Version) in current' (Lt r'.T.Version) r end end end in - current' vro (map0 [option] (fn [t :: Type] => None : option t) [_] M.dataFolder) + current' vro (@map0 [option] (fn [t :: Type] => None : option t) M.dataFolder) end val current = seek NoBound @@ -113,14 +113,14 @@ | Some cur => vr <- nextval s; let - val r' = map3 [dmeta] [id] [id] [fn t => sql_exp [] [] [] (option t)] - (fn [t] (meta : dmeta t) old new => - @sql_inject (@sql_option_prim meta.Inj) - (if @@eq [_] meta.Eq old new then - None - else - Some new)) - [_] M.dataFolder M.data cur (r --- M.key) + val r' = @map3 [dmeta] [id] [id] [fn t => sql_exp [] [] [] (option t)] + (fn [t] (meta : dmeta t) old new => + @sql_inject (@sql_option_prim meta.Inj) + (if @@eq [_] meta.Eq old new then + None + else + Some new)) + M.dataFolder M.data cur (r --- M.key) val r' = {Version = (SQL {[vr]}), When = (SQL CURRENT_TIMESTAMP)} ++ keyRecd r ++ r'
--- a/demo/sum.ur Fri Dec 25 10:48:02 2009 -0500 +++ b/demo/sum.ur Sat Dec 26 11:56:40 2009 -0500 @@ -1,7 +1,7 @@ fun sum [fs ::: {Unit}] (fl : folder fs) (x : $(mapU int fs)) = - foldUR [int] [fn _ => int] - (fn [nm :: Name] [rest :: {Unit}] [[nm] ~ rest] n acc => n + acc) - 0 [fs] fl x + @foldUR [int] [fn _ => int] + (fn [nm :: Name] [rest :: {Unit}] [[nm] ~ rest] n acc => n + acc) + 0 fl x fun main () = return <xml><body> {[sum {}]}<br/>
--- a/demo/tcSum.ur Fri Dec 25 10:48:02 2009 -0500 +++ b/demo/tcSum.ur Sat Dec 26 11:56:40 2009 -0500 @@ -1,7 +1,7 @@ fun sum [t] (_ : num t) [fs ::: {Unit}] (fl : folder fs) (x : $(mapU t fs)) = - foldUR [t] [fn _ => t] - (fn [nm :: Name] [rest :: {Unit}] [[nm] ~ rest] n acc => n + acc) - zero [fs] fl x + @foldUR [t] [fn _ => t] + (fn [nm :: Name] [rest :: {Unit}] [[nm] ~ rest] n acc => n + acc) + zero fl x fun main () = return <xml><body> {[sum {A = 0, B = 1}]}<br/>
--- a/lib/ur/monad.ur Fri Dec 25 10:48:02 2009 -0500 +++ b/lib/ur/monad.ur Sat Dec 26 11:56:40 2009 -0500 @@ -1,10 +1,10 @@ fun exec [m ::: Type -> Type] (_ : monad m) [ts ::: {Type}] r (fd : folder ts) = - foldR [m] [fn ts => m $ts] - (fn [nm :: Name] [v :: Type] [rest :: {Type}] [[nm] ~ rest] action acc => - this <- action; - others <- acc; - return ({nm = this} ++ others)) - (return {}) [ts] fd r + @foldR [m] [fn ts => m $ts] + (fn [nm :: Name] [v :: Type] [rest :: {Type}] [[nm] ~ rest] action acc => + this <- action; + others <- acc; + return ({nm = this} ++ others)) + (return {}) fd r fun ignore [m ::: Type -> Type] (_ : monad m) [t] (v : m t) = x <- v; return () @@ -16,40 +16,40 @@ (f : nm :: Name -> t :: K -> rest :: {K} -> [[nm] ~ rest] => tf t -> tr rest -> m (tr ([nm = t] ++ rest))) - (i : tr []) [r :: {K}] (fl : folder r) = - Top.fold [fn r :: {K} => $(map tf r) -> m (tr r)] - (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] - (acc : _ -> m (tr rest)) r => - acc' <- acc (r -- nm); - f [nm] [t] [rest] ! r.nm acc') - (fn _ => return i) - [_] fl + (i : tr []) [r ::: {K}] (fl : folder r) = + @Top.fold [fn r :: {K} => $(map tf r) -> m (tr r)] + (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] + (acc : _ -> m (tr rest)) r => + acc' <- acc (r -- nm); + f [nm] [t] [rest] ! r.nm acc') + (fn _ => return i) + fl fun foldR2 [K] [m] (_ : monad m) [tf1 :: K -> Type] [tf2 :: K -> Type] [tr :: {K} -> Type] (f : nm :: Name -> t :: K -> rest :: {K} -> [[nm] ~ rest] => tf1 t -> tf2 t -> tr rest -> m (tr ([nm = t] ++ rest))) - (i : tr []) [r :: {K}] (fl : folder r) = - Top.fold [fn r :: {K} => $(map tf1 r) -> $(map tf2 r) -> m (tr r)] - (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] - (acc : _ -> _ -> m (tr rest)) r1 r2 => - acc' <- acc (r1 -- nm) (r2 -- nm); - f [nm] [t] [rest] ! r1.nm r2.nm acc') - (fn _ _ => return i) - [_] fl + (i : tr []) [r ::: {K}] (fl : folder r) = + @Top.fold [fn r :: {K} => $(map tf1 r) -> $(map tf2 r) -> m (tr r)] + (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] + (acc : _ -> _ -> m (tr rest)) r1 r2 => + acc' <- acc (r1 -- nm) (r2 -- nm); + f [nm] [t] [rest] ! r1.nm r2.nm acc') + (fn _ _ => return i) + fl fun foldR3 [K] [m] (_ : monad m) [tf1 :: K -> Type] [tf2 :: K -> Type] [tf3 :: K -> Type] [tr :: {K} -> Type] (f : nm :: Name -> t :: K -> rest :: {K} -> [[nm] ~ rest] => tf1 t -> tf2 t -> tf3 t -> tr rest -> m (tr ([nm = t] ++ rest))) - (i : tr []) [r :: {K}] (fl : folder r) = - Top.fold [fn r :: {K} => $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> m (tr r)] - (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] - (acc : _ -> _ -> _ -> m (tr rest)) r1 r2 r3 => - acc' <- acc (r1 -- nm) (r2 -- nm) (r3 -- nm); - f [nm] [t] [rest] ! r1.nm r2.nm r3.nm acc') - (fn _ _ _ => return i) - [_] fl + (i : tr []) [r ::: {K}] (fl : folder r) = + @Top.fold [fn r :: {K} => $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> m (tr r)] + (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] + (acc : _ -> _ -> _ -> m (tr rest)) r1 r2 r3 => + acc' <- acc (r1 -- nm) (r2 -- nm) (r3 -- nm); + f [nm] [t] [rest] ! r1.nm r2.nm r3.nm acc') + (fn _ _ _ => return i) + fl fun mapR [K] [m] (_ : monad m) [tf :: K -> Type] [tr :: K -> Type] (f : nm :: Name -> t :: K -> tf t -> m (tr t)) =
--- a/lib/ur/monad.urs Fri Dec 25 10:48:02 2009 -0500 +++ b/lib/ur/monad.urs Sat Dec 26 11:56:40 2009 -0500 @@ -14,7 +14,7 @@ -> [[nm] ~ rest] => tf t -> tr rest -> m (tr ([nm = t] ++ rest))) -> tr [] - -> r :: {K} -> folder r -> $(map tf r) -> m (tr r) + -> r ::: {K} -> folder r -> $(map tf r) -> m (tr r) val foldR2 : K --> m ::: (Type -> Type) -> monad m -> tf1 :: (K -> Type) -> tf2 :: (K -> Type) @@ -23,7 +23,7 @@ -> [[nm] ~ rest] => tf1 t -> tf2 t -> tr rest -> m (tr ([nm = t] ++ rest))) -> tr [] - -> r :: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> m (tr r) + -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> m (tr r) val foldR3 : K --> m ::: (Type -> Type) -> monad m -> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> tf3 :: (K -> Type) @@ -32,16 +32,16 @@ -> [[nm] ~ rest] => tf1 t -> tf2 t -> tf3 t -> tr rest -> m (tr ([nm = t] ++ rest))) -> tr [] - -> r :: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> m (tr r) + -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> m (tr r) val mapR : K --> m ::: (Type -> Type) -> monad m -> tf :: (K -> Type) -> tr :: (K -> Type) -> (nm :: Name -> t :: K -> tf t -> m (tr t)) - -> r :: {K} -> folder r -> $(map tf r) -> m ($(map tr r)) + -> r ::: {K} -> folder r -> $(map tf r) -> m ($(map tr r)) val mapR2 : K --> m ::: (Type -> Type) -> monad m -> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> tr :: (K -> Type) -> (nm :: Name -> t :: K -> tf1 t -> tf2 t -> m (tr t)) - -> r :: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> m ($(map tr r)) + -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> m ($(map tr r))
--- a/lib/ur/top.ur Fri Dec 25 10:48:02 2009 -0500 +++ b/lib/ur/top.ur Sat Dec 26 11:56:40 2009 -0500 @@ -9,7 +9,7 @@ fun fold [K] [tf :: {K} -> Type] (f : (nm :: Name -> v :: K -> r :: {K} -> [[nm] ~ r] => tf r -> tf ([nm = v] ++ r))) - (i : tf []) [r :: {K}] (fl : folder r) = fl [tf] f i + (i : tf []) [r ::: {K}] (fl : folder r) = fl [tf] f i structure Folder = struct fun nil [K] [tf :: {K} -> Type] @@ -92,27 +92,27 @@ fun txt [t] [ctx ::: {Unit}] [use ::: {Type}] (_ : show t) (v : t) = cdata (show v) -fun map0 [K] [tf :: K -> Type] (f : t :: K -> tf t) [r :: {K}] (fl : folder r) = +fun map0 [K] [tf :: K -> Type] (f : t :: K -> tf t) [r ::: {K}] (fl : folder r) = fl [fn r :: {K} => $(map tf r)] (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] acc => acc ++ {nm = f [t]}) {} -fun mp [K] [tf1 :: K -> Type] [tf2 :: K -> Type] (f : t ::: K -> tf1 t -> tf2 t) [r :: {K}] (fl : folder r) = +fun mp [K] [tf1 :: K -> Type] [tf2 :: K -> Type] (f : t ::: K -> tf1 t -> tf2 t) [r ::: {K}] (fl : folder r) = fl [fn r :: {K} => $(map tf1 r) -> $(map tf2 r)] (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] acc r => acc (r -- nm) ++ {nm = f r.nm}) (fn _ => {}) fun map2 [K] [tf1 :: K -> Type] [tf2 :: K -> Type] [tf3 :: K -> Type] - (f : t ::: K -> tf1 t -> tf2 t -> tf3 t) [r :: {K}] (fl : folder r) = + (f : t ::: K -> tf1 t -> tf2 t -> tf3 t) [r ::: {K}] (fl : folder r) = fl [fn r :: {K} => $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r)] (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] acc r1 r2 => acc (r1 -- nm) (r2 -- nm) ++ {nm = f r1.nm r2.nm}) (fn _ _ => {}) fun map3 [K] [tf1 :: K -> Type] [tf2 :: K -> Type] [tf3 :: K -> Type] [tf :: K -> Type] - (f : t ::: K -> tf1 t -> tf2 t -> tf3 t -> tf t) [r :: {K}] (fl : folder r) = + (f : t ::: K -> tf1 t -> tf2 t -> tf3 t -> tf t) [r ::: {K}] (fl : folder r) = fl [fn r :: {K} => $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> $(map tf r)] (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] acc r1 r2 r3 => acc (r1 -- nm) (r2 -- nm) (r3 -- nm) ++ {nm = f r1.nm r2.nm r3.nm}) @@ -122,7 +122,7 @@ (f : nm :: Name -> rest :: {Unit} -> [[nm] ~ rest] => tf -> tr rest -> tr ([nm] ++ rest)) - (i : tr []) [r :: {Unit}] (fl : folder r) = + (i : tr []) [r ::: {Unit}] (fl : folder r) = fl [fn r :: {Unit} => $(mapU tf r) -> tr r] (fn [nm :: Name] [t :: Unit] [rest :: {Unit}] [[nm] ~ rest] acc r => f [nm] [rest] ! r.nm (acc (r -- nm))) @@ -132,7 +132,7 @@ (f : nm :: Name -> rest :: {Unit} -> [[nm] ~ rest] => tf1 -> tf2 -> tr rest -> tr ([nm] ++ rest)) - (i : tr []) [r :: {Unit}] (fl : folder r) = + (i : tr []) [r ::: {Unit}] (fl : folder r) = fl [fn r :: {Unit} => $(mapU tf1 r) -> $(mapU tf2 r) -> tr r] (fn [nm :: Name] [t :: Unit] [rest :: {Unit}] [[nm] ~ rest] acc r1 r2 => f [nm] [rest] ! r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm))) @@ -142,16 +142,16 @@ (f : nm :: Name -> rest :: {Unit} -> [[nm] ~ rest] => tf1 -> tf2 -> xml ctx [] []) = - foldUR2 [tf1] [tf2] [fn _ => xml ctx [] []] - (fn [nm :: Name] [rest :: {Unit}] [[nm] ~ rest] v1 v2 acc => - <xml>{f [nm] [rest] ! v1 v2}{acc}</xml>) - <xml/> + @@foldUR2 [tf1] [tf2] [fn _ => xml ctx [] []] + (fn [nm :: Name] [rest :: {Unit}] [[nm] ~ rest] v1 v2 acc => + <xml>{f [nm] [rest] ! v1 v2}{acc}</xml>) + <xml/> fun foldR [K] [tf :: K -> Type] [tr :: {K} -> Type] (f : nm :: Name -> t :: K -> rest :: {K} -> [[nm] ~ rest] => tf t -> tr rest -> tr ([nm = t] ++ rest)) - (i : tr []) [r :: {K}] (fl : folder r) = + (i : tr []) [r ::: {K}] (fl : folder r) = fl [fn r :: {K} => $(map tf r) -> tr r] (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] (acc : _ -> tr rest) r => f [nm] [t] [rest] ! r.nm (acc (r -- nm))) @@ -161,7 +161,7 @@ (f : nm :: Name -> t :: K -> rest :: {K} -> [[nm] ~ rest] => tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest)) - (i : tr []) [r :: {K}] (fl : folder r) = + (i : tr []) [r ::: {K}] (fl : folder r) = fl [fn r :: {K} => $(map tf1 r) -> $(map tf2 r) -> tr r] (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] (acc : _ -> _ -> tr rest) r1 r2 => @@ -172,7 +172,7 @@ (f : nm :: Name -> t :: K -> rest :: {K} -> [[nm] ~ rest] => tf1 t -> tf2 t -> tf3 t -> tr rest -> tr ([nm = t] ++ rest)) - (i : tr []) [r :: {K}] (fl : folder r) = + (i : tr []) [r ::: {K}] (fl : folder r) = fl [fn r :: {K} => $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> tr r] (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] (acc : _ -> _ -> _ -> tr rest) r1 r2 r3 => @@ -183,30 +183,30 @@ (f : nm :: Name -> t :: K -> rest :: {K} -> [[nm] ~ rest] => tf t -> xml ctx [] []) = - foldR [tf] [fn _ => xml ctx [] []] - (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] r acc => - <xml>{f [nm] [t] [rest] ! r}{acc}</xml>) - <xml/> + @@foldR [tf] [fn _ => xml ctx [] []] + (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] r acc => + <xml>{f [nm] [t] [rest] ! r}{acc}</xml>) + <xml/> fun foldRX2 [K] [tf1 :: K -> Type] [tf2 :: K -> Type] [ctx :: {Unit}] (f : nm :: Name -> t :: K -> rest :: {K} -> [[nm] ~ rest] => tf1 t -> tf2 t -> xml ctx [] []) = - foldR2 [tf1] [tf2] [fn _ => xml ctx [] []] - (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] - r1 r2 acc => - <xml>{f [nm] [t] [rest] ! r1 r2}{acc}</xml>) - <xml/> + @@foldR2 [tf1] [tf2] [fn _ => xml ctx [] []] + (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] + r1 r2 acc => + <xml>{f [nm] [t] [rest] ! r1 r2}{acc}</xml>) + <xml/> fun foldRX3 [K] [tf1 :: K -> Type] [tf2 :: K -> Type] [tf3 :: K -> Type] [ctx :: {Unit}] (f : nm :: Name -> t :: K -> rest :: {K} -> [[nm] ~ rest] => tf1 t -> tf2 t -> tf3 t -> xml ctx [] []) = - foldR3 [tf1] [tf2] [tf3] [fn _ => xml ctx [] []] - (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] - r1 r2 r3 acc => - <xml>{f [nm] [t] [rest] ! r1 r2 r3}{acc}</xml>) - <xml/> + @@foldR3 [tf1] [tf2] [tf3] [fn _ => xml ctx [] []] + (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] + r1 r2 r3 acc => + <xml>{f [nm] [t] [rest] ! r1 r2 r3}{acc}</xml>) + <xml/> fun queryL [tables] [exps] [tables ~ exps] (q : sql_query tables exps) = query q
--- a/lib/ur/top.urs Fri Dec 25 10:48:02 2009 -0500 +++ b/lib/ur/top.urs Sat Dec 26 11:56:40 2009 -0500 @@ -6,7 +6,7 @@ -> (nm :: Name -> v :: K -> r :: {K} -> [[nm] ~ r] => tf r -> tf ([nm = v] ++ r)) -> tf [] - -> r :: {K} -> folder r -> tf r + -> r ::: {K} -> folder r -> tf r structure Folder : sig val nil : K --> folder (([]) :: {K}) @@ -47,40 +47,40 @@ val map0 : K --> tf :: (K -> Type) -> (t :: K -> tf t) - -> r :: {K} -> folder r -> $(map tf r) + -> r ::: {K} -> folder r -> $(map tf r) val mp : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> (t ::: K -> tf1 t -> tf2 t) - -> r :: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) + -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) val map2 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> tf :: (K -> Type) -> (t ::: K -> tf1 t -> tf2 t -> tf t) - -> r :: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> $(map tf r) + -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> $(map tf r) val map3 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> tf3 :: (K -> Type) -> tf :: (K -> Type) -> (t ::: K -> tf1 t -> tf2 t -> tf3 t -> tf t) - -> r :: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> $(map tf r) + -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> $(map tf r) val foldUR : tf :: Type -> tr :: ({Unit} -> Type) -> (nm :: Name -> rest :: {Unit} -> [[nm] ~ rest] => tf -> tr rest -> tr ([nm] ++ rest)) - -> tr [] -> r :: {Unit} -> folder r -> $(mapU tf r) -> tr r + -> tr [] -> r ::: {Unit} -> folder r -> $(mapU tf r) -> tr r val foldUR2 : tf1 :: Type -> tf2 :: Type -> tr :: ({Unit} -> Type) -> (nm :: Name -> rest :: {Unit} -> [[nm] ~ rest] => tf1 -> tf2 -> tr rest -> tr ([nm] ++ rest)) - -> tr [] -> r :: {Unit} -> folder r -> $(mapU tf1 r) -> $(mapU tf2 r) -> tr r + -> tr [] -> r ::: {Unit} -> folder r -> $(mapU tf1 r) -> $(mapU tf2 r) -> tr r val foldURX2: tf1 :: Type -> tf2 :: Type -> ctx :: {Unit} -> (nm :: Name -> rest :: {Unit} -> [[nm] ~ rest] => tf1 -> tf2 -> xml ctx [] []) - -> r :: {Unit} -> folder r -> $(mapU tf1 r) -> $(mapU tf2 r) -> xml ctx [] [] + -> r ::: {Unit} -> folder r -> $(mapU tf1 r) -> $(mapU tf2 r) -> xml ctx [] [] val foldR : K --> tf :: (K -> Type) -> tr :: ({K} -> Type) -> (nm :: Name -> t :: K -> rest :: {K} -> [[nm] ~ rest] => tf t -> tr rest -> tr ([nm = t] ++ rest)) - -> tr [] -> r :: {K} -> folder r -> $(map tf r) -> tr r + -> tr [] -> r ::: {K} -> folder r -> $(map tf r) -> tr r val foldR2 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> tr :: ({K} -> Type) @@ -88,7 +88,7 @@ -> [[nm] ~ rest] => tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest)) -> tr [] - -> r :: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> tr r + -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> tr r val foldR3 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> tf3 :: (K -> Type) -> tr :: ({K} -> Type) @@ -96,26 +96,26 @@ -> [[nm] ~ rest] => tf1 t -> tf2 t -> tf3 t -> tr rest -> tr ([nm = t] ++ rest)) -> tr [] - -> r :: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> tr r + -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> tr r val foldRX : K --> tf :: (K -> Type) -> ctx :: {Unit} -> (nm :: Name -> t :: K -> rest :: {K} -> [[nm] ~ rest] => tf t -> xml ctx [] []) - -> r :: {K} -> folder r -> $(map tf r) -> xml ctx [] [] + -> r ::: {K} -> folder r -> $(map tf r) -> xml ctx [] [] val foldRX2 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> ctx :: {Unit} -> (nm :: Name -> t :: K -> rest :: {K} -> [[nm] ~ rest] => tf1 t -> tf2 t -> xml ctx [] []) - -> r :: {K} -> folder r + -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> xml ctx [] [] val foldRX3 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> tf3 :: (K -> Type) -> ctx :: {Unit} -> (nm :: Name -> t :: K -> rest :: {K} -> [[nm] ~ rest] => tf1 t -> tf2 t -> tf3 t -> xml ctx [] []) - -> r :: {K} -> folder r + -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> xml ctx [] [] val queryL : tables ::: {{Type}} -> exps ::: {Type}
--- a/src/elaborate.sml Fri Dec 25 10:48:02 2009 -0500 +++ b/src/elaborate.sml Sat Dec 26 11:56:40 2009 -0500 @@ -693,6 +693,13 @@ and consNeq env (c1, c2) = case (#1 (hnormCon env c1), #1 (hnormCon env c2)) of (L'.CName x1, L'.CName x2) => x1 <> x2 + | (L'.CName _, L'.CRel _) => true + | (L'.CRel _, L'.CName _) => true + | (L'.CRel n1, L'.CRel n2) => n1 <> n2 + | (L'.CRel _, L'.CNamed _) => true + | (L'.CNamed _, L'.CRel _) => true + | (L'.CRel _, L'.CModProj _) => true + | (L'.CModProj _, L'.CRel _) => true | _ => false and unifySummaries env (loc, k, s1 : record_summary, s2 : record_summary) = @@ -1619,6 +1626,34 @@ | L'.CUnif (_, _, _, ref (SOME c)) => normClassConstraint env c | _ => unmodCon env (c, loc) +fun findHead e e' = + let + fun findHead (e, _) = + case e of + L.EVar (_, _, infer) => + let + fun findHead' (e, _) = + case e of + L'.ENamed _ => true + | L'.EModProj _ => true + | L'.EApp (e, _) => findHead' e + | L'.ECApp (e, _) => findHead' e + | L'.EKApp (e, _) => findHead' e + | _ => false + in + if findHead' e' then + SOME infer + else + NONE + end + | L.EApp (e, _) => findHead e + | L.ECApp (e, _) => findHead e + | L.EDisjointApp e => findHead e + | _ => NONE + in + findHead e + end + fun elabExp (env, denv) (eAll as (e, loc)) = let (*val () = eprefaces "elabExp" [("eAll", SourcePrint.p_exp eAll)]*) @@ -1674,15 +1709,23 @@ | L.EApp (e1, e2) => let val (e1', t1, gs1) = elabExp (env, denv) e1 + val (e2', t2, gs2) = elabExp (env, denv) e2 val dom = cunif (loc, ktype) val ran = cunif (loc, ktype) val t = (L'.TFun (dom, ran), loc) + + val () = checkCon env e1' t1 t + val () = checkCon env e2' t2 dom + + val ef = (L'.EApp (e1', e2'), loc) + val (ef, et, gs3) = + case findHead e1 e1' of + NONE => (ef, ran, []) + | SOME infer => elabHead (env, denv) infer ef ran in - checkCon env e1' t1 t; - checkCon env e2' t2 dom; - ((L'.EApp (e1', e2'), loc), ran, gs1 @ gs2) + (ef, et, gs1 @ gs2 @ gs3) end | L.EAbs (x, to, e) => let @@ -1705,6 +1748,7 @@ | L.ECApp (e, c) => let val (e', et, gs1) = elabExp (env, denv) e + val oldEt = et val (c', ck, gs2) = elabCon (env, denv) c val (et', _) = hnormCon env et @@ -1717,6 +1761,12 @@ val eb' = subConInCon (0, c') eb handle SynUnif => (expError env (Unif ("substitution", loc, eb)); cerror) + + val ef = (L'.ECApp (e', c'), loc) + val (ef, eb', gs3) = + case findHead e e' of + NONE => (ef, eb', []) + | SOME infer => elabHead (env, denv) infer ef eb' in (*prefaces "Elab ECApp" [("e", SourcePrint.p_exp eAll), ("et", p_con env oldEt), @@ -1724,7 +1774,7 @@ ("eb", p_con (E.pushCRel env x k) eb), ("c", p_con env c'), ("eb'", p_con env eb')];*) - ((L'.ECApp (e', c'), loc), eb', gs1 @ enD gs2) + (ef, eb', gs1 @ enD gs2 @ gs3) end | _ =>
--- a/src/urweb.grm Fri Dec 25 10:48:02 2009 -0500 +++ b/src/urweb.grm Sat Dec 26 11:56:40 2009 -0500 @@ -540,9 +540,8 @@ val e = (EVar (["Basis"], "unique", Infer), loc) val e = (ECApp (e, #1 (#1 tnames)), loc) val e = (ECApp (e, (CRecord (#2 tnames), loc)), loc) - val e = (EDisjointApp e, loc) in - (EDisjointApp e, loc) + e end) | CHECK sqlexp (let @@ -562,9 +561,6 @@ val e = (EVar (["Basis"], "mat_cons", Infer), loc) val e = (ECApp (e, nm1), loc) val e = (ECApp (e, nm2), loc) - val e = (EDisjointApp e, loc) - val e = (EDisjointApp e, loc) - val e = (EApp (e, (EWild, loc)), loc) in (EApp (e, mat), loc) end) @@ -634,7 +630,7 @@ | PRIMARY KEY tnames (let val loc = s (PRIMARYleft, tnamesright) - val e = (EVar (["Basis"], "primary_key", Infer), loc) + val e = (EVar (["Basis"], "primary_key", TypesOnly), loc) val e = (ECApp (e, #1 (#1 tnames)), loc) val e = (ECApp (e, (CRecord (#2 tnames), loc)), loc) val e = (EDisjointApp e, loc) @@ -1192,7 +1188,6 @@ val e = (EVar (["Basis"], "update", Infer), loc) val e = (ECApp (e, (CWild (KRecord (KType, loc), loc), loc)), loc) - val e = (EDisjointApp e, loc) val e = (EApp (e, (ERecord fsets, loc)), loc) val e = (EApp (e, texp), loc) in @@ -1335,11 +1330,8 @@ if et = "form" then (EApp ((EVar (["Basis"], "form", Infer), pos), xmlOpt), pos) - else if et = "subform" then - (EApp ((EDisjointApp (#2 (#1 tag)), pos), - xmlOpt), pos) - else if et = "subforms" then - (EApp ((EDisjointApp (#2 (#1 tag)), pos), + else if et = "subform" orelse et = "subforms" then + (EApp (#2 (#1 tag), xmlOpt), pos) else if et = "entry" then (EApp ((EVar (["Basis"], "entry", Infer), pos), @@ -1504,7 +1496,6 @@ val e = (EVar (["Basis"], "sql_query1", Infer), loc) val e = (ECApp (e, (CRecord (map (fn nm => (nm, (CUnit, loc))) empties), loc)), loc) - val e = (EDisjointApp e, loc) val re = (ERecord [((CName "Distinct", loc), dopt), ((CName "From", loc),
--- a/tests/impl.ur Fri Dec 25 10:48:02 2009 -0500 +++ b/tests/impl.ur Sat Dec 26 11:56:40 2009 -0500 @@ -1,15 +1,18 @@ -val id = fn t :: Type => fn x : t => x +fun id [t :: Type] (x : t) = x val id_self = id [t :: Type -> t -> t] id -val idi = fn t ::: Type => fn x : t => x -val idi_self = idi idi +fun idi [t ::: Type] (x : t) = x +val idi_self = idi @@idi -val picker = fn na :: Name => fn a ::: Type => fn nb :: Name => fn b ::: Type => fn fs ::: {Type} => - fn r : $([na = a, nb = b] ++ fs) => {na = r.na, nb = r.nb} +fun picker [na :: Name] [a ::: Type] [nb :: Name] [b ::: Type] [fs ::: {Type}] [[na] ~ [nb]] [[na, nb] ~ fs] + (r : $([na = a, nb = b] ++ fs)) = {na = r.na, nb = r.nb} val getem = picker [#A] [#C] {A = 0, B = 1.0, C = "hi", D = {}} val getem2 = picker [#A] [_] {A = 0, B = 1.0, C = "hi", D = {}} val getem3 = picker [#A] [_::Name] {A = 0, B = 1.0, C = "hi", D = {}} -val picker_ohmy = fn na ::: Name => fn a ::: Type => fn nb ::: Name => fn b ::: Type => fn fs ::: {Type} => - fn r : $([na = a, nb = b] ++ fs) => {na = r.na, nb = r.nb} +fun picker_ohmy [na ::: Name] [a ::: Type] [nb ::: Name] [b ::: Type] [fs ::: {Type}] [[na] ~ [nb]] [[na, nb] ~ fs] + (r : $([na = a, nb = b] ++ fs)) = {na = r.na, nb = r.nb} val getem_ohmy = picker_ohmy {A = 0, B = 1.0, C = "hi", D = {}} + +fun proj [fs] [t] [nm :: Name] [[nm] ~ fs] (r : $([nm = t] ++ fs)) = r.nm +val one = proj [#A] {A = 1, B = True}