From c4120c8ddaa5340efad5f835ce4565f2a8ae2cbf Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Sat, 26 Dec 2009 11:56:40 -0500 Subject: Make summary unification more conservative; infer implicit arguments after applications --- demo/more/dbgrid.ur | 34 +++++----- demo/more/grid.ur | 170 ++++++++++++++++++++++++------------------------- demo/more/grid1.ur | 14 ++-- demo/more/orm.ur | 48 +++++++------- demo/more/orm1.ur | 6 +- demo/more/versioned.ur | 76 +++++++++++----------- 6 files changed, 174 insertions(+), 174 deletions(-) (limited to 'demo/more') diff --git a/demo/more/dbgrid.ur b/demo/more/dbgrid.ur index fe77f21b..b6cd94ae 100644 --- a/demo/more/dbgrid.ur +++ b/demo/more/dbgrid.ur @@ -384,31 +384,31 @@ functor Make(M : sig 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)) diff --git a/demo/more/grid.ur b/demo/more/grid.ur index 170c6f2c..7540ca27 100644 --- a/demo/more/grid.ur +++ b/demo/more/grid.ur @@ -49,9 +49,9 @@ functor Make(M : sig 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 @@ functor Make(M : sig 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 @@ functor Make(M : sig 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) = - {foldRX2 [fst3] [colMeta M.row] [_] - (fn [nm :: Name] [p :: (Type * Type * Type)] [rest :: {(Type * Type * Type)}] [[nm] ~ rest] - data (meta : colMeta M.row p) => - ) - [_] 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) => + ) + M.folder grid.Cols M.cols} {Dlist.render (fn {Row = rowS, Cols = colsS, Updating = ud, Selected = sd} pos => @@ -152,18 +152,18 @@ functor Make(M : sig 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 @@ functor Make(M : sig | 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 @@ functor Make(M : sig - ) - [_] 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 => + ) + M.folder grid.Cols M.cols cols)}/> end) {StartPosition = case M.pageLength of @@ -250,27 +250,27 @@ functor Make(M : sig return (f r1 r2)) f)} grid.Rows} - 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] + @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 - {foldRX2 [aggregateMeta M.row] [id] [_] - (fn [nm :: Name] [t :: Type] [rest :: {Type}] [[nm] ~ rest] meta acc => - ) - [_] M.aggFolder M.aggregates rows} + {@foldRX2 [aggregateMeta M.row] [id] [_] + (fn [nm :: Name] [t :: Type] [rest :: {Type}] [[nm] ~ rest] meta acc => + ) + M.aggFolder M.aggregates rows} }/> - {foldRX3 [colMeta M.row] [fst3] [thd3] [_] - (fn [nm :: Name] [p :: (Type * Type * Type)] [rest :: {(Type * Type * Type)}] [[nm] ~ rest] - meta state filter => ) - [_] 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 => ) + M.folder M.cols grid.Cols grid.Filters}
- {case (meta.Handlers data).Sort of - None => txt (meta.Handlers data).Header - | sort => + {case (meta.Handlers data).Sort of + None => txt (meta.Handlers data).Header + | sort =>
- - - else - !) - else - return }/> - + + + else + !) + else + return }/> +
Aggregates{meta.Display acc}{meta.Display acc}
Filters{(meta.Handlers state).DisplayFilter filter}{(meta.Handlers state).DisplayFilter filter}
diff --git a/demo/more/grid1.ur b/demo/more/grid1.ur index 1eb5e596..2e58bdb7 100644 --- a/demo/more/grid1.ur +++ b/demo/more/grid1.ur @@ -35,13 +35,13 @@ open Make(struct 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 => Go)} diff --git a/demo/more/orm.ur b/demo/more/orm.ur index 620db9ad..d9f57f3b 100644 --- a/demo/more/orm.ur +++ b/demo/more/orm.ur @@ -32,9 +32,9 @@ functor Table(M : sig 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 @@ functor Table(M : sig 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 @@ functor Table(M : sig {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 @@ functor Table(M : sig 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 diff --git a/demo/more/orm1.ur b/demo/more/orm1.ur index bbbe2b00..b5ba29ac 100644 --- a/demo/more/orm1.ur +++ b/demo/more/orm1.ur @@ -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 () = diff --git a/demo/more/versioned.ur b/demo/more/versioned.ur index bc9911e3..8579559e 100644 --- a/demo/more/versioned.ur +++ b/demo/more/versioned.ur @@ -24,33 +24,33 @@ functor Make(M : sig 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 @@ functor Make(M : sig 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 @@ functor Make(M : sig 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 @@ functor Make(M : sig | 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' -- cgit v1.2.3