From 2ace64baba707b2e76778c74789735263eb50823 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/grid.ur | 170 +++++++++++++++++++++++++++--------------------------- 1 file changed, 85 insertions(+), 85 deletions(-) (limited to 'demo/more/grid.ur') 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}
-- cgit v1.2.3