Mercurial > urweb
changeset 944:da3ec6014d2f
Filters implementation type-checking
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Tue, 15 Sep 2009 15:48:53 -0400 |
| parents | e2194a6793ae |
| children | 7710f65935b6 |
| files | demo/more/dbgrid.ur demo/more/dbgrid.urs demo/more/dlist.ur demo/more/dlist.urs demo/more/grid.ur demo/more/grid.urp demo/more/grid.urs lib/ur/option.ur lib/ur/option.urs |
| diffstat | 9 files changed, 300 insertions(+), 147 deletions(-) [+] |
line wrap: on
line diff
--- a/demo/more/dbgrid.ur Tue Sep 15 13:07:57 2009 -0400 +++ b/demo/more/dbgrid.ur Tue Sep 15 15:48:53 2009 -0400 @@ -2,17 +2,20 @@ {New : transaction t, Inj : sql_injectable t} -con colMeta' = fn (row :: {Type}) (t :: Type) => +con colMeta' = fn (row :: {Type}) (input :: Type) (filter :: Type) => {Header : string, - Project : $row -> transaction t, - Update : $row -> t -> transaction ($row), - Display : t -> xbody, - Edit : t -> xbody, - Validate : t -> signal bool} + Project : $row -> transaction input, + Update : $row -> input -> transaction ($row), + Display : input -> xbody, + Edit : input -> xbody, + Validate : input -> signal bool, + CreateFilter : transaction filter, + DisplayFilter : filter -> xbody, + Filter : filter -> $row -> signal bool} -con colMeta = fn (row :: {Type}) (global_t :: (Type * Type)) => - {Initialize : transaction global_t.1, - Handlers : global_t.1 -> colMeta' row global_t.2} +con colMeta = fn (row :: {Type}) (global_input_filter :: (Type * Type * Type)) => + {Initialize : transaction global_input_filter.1, + Handlers : global_input_filter.1 -> colMeta' row global_input_filter.2 global_input_filter.3} con aggregateMeta = fn (row :: {Type}) (acc :: Type) => {Initial : acc, @@ -20,22 +23,26 @@ Display : acc -> xbody} structure Direct = struct - con metaBase = fn actual_input :: (Type * Type) => - {Display : actual_input.2 -> xbody, - Edit : actual_input.2 -> xbody, - Initialize : actual_input.1 -> transaction actual_input.2, - Parse : actual_input.2 -> signal (option actual_input.1)} + con metaBase = fn actual_input_filter :: (Type * Type * Type) => + {Display : actual_input_filter.2 -> xbody, + Edit : actual_input_filter.2 -> xbody, + Initialize : actual_input_filter.1 -> transaction actual_input_filter.2, + Parse : actual_input_filter.2 -> signal (option actual_input_filter.1), + CreateFilter : transaction actual_input_filter.3, + DisplayFilter : actual_input_filter.3 -> xbody, + Filter : actual_input_filter.3 -> actual_input_filter.1 -> signal bool} - datatype metaBoth actual input = - NonNull of metaBase (actual, input) * metaBase (option actual, input) - | Nullable of metaBase (actual, input) + datatype metaBoth actual input filter = + NonNull of metaBase (actual, input, filter) * metaBase (option actual, input, filter) + | Nullable of metaBase (actual, input, filter) - con meta = fn global_actual_input :: (Type * Type * Type) => - {Initialize : transaction global_actual_input.1, - Handlers : global_actual_input.1 - -> metaBoth global_actual_input.2 global_actual_input.3} + con meta = fn global_actual_input_filter :: (Type * Type * Type * Type) => + {Initialize : transaction global_actual_input_filter.1, + Handlers : global_actual_input_filter.1 + -> metaBoth global_actual_input_filter.2 global_actual_input_filter.3 + global_actual_input_filter.4} - con editableState (ts :: (Type * Type * Type)) = (ts.1, ts.3) + con editableState (ts :: (Type * Type * Type * Type)) = (ts.1, ts.3, ts.4) fun editable [ts] [rest] [nm :: Name] [[nm] ~ rest] name (m : meta ts) : colMeta ([nm = ts.2] ++ rest) (editableState ts) = let @@ -48,7 +55,10 @@ | Some v => r -- nm ++ {nm = v}), Display = mr.Display, Edit = mr.Edit, - Validate = fn s => vo <- mr.Parse s; return (Option.isSome vo)} + Validate = fn s => vo <- mr.Parse s; return (Option.isSome vo), + CreateFilter = mr.CreateFilter, + DisplayFilter = mr.DisplayFilter, + Filter = fn i r => mr.Filter i r.nm} in {Initialize = m.Initialize, Handlers = fn data => case m.Handlers data of @@ -56,7 +66,7 @@ | Nullable mr => doMr mr} end - con readOnlyState (ts :: (Type * Type * Type)) = (ts.1, ts.3) + con readOnlyState (ts :: (Type * Type * Type * Type)) = (ts.1, ts.3, ts.4) fun readOnly [ts] [rest] [nm :: Name] [[nm] ~ rest] name (m : meta ts) : colMeta ([nm = ts.2] ++ rest) (readOnlyState ts) = let @@ -65,7 +75,10 @@ Update = fn r _ => return r, Display = mr.Display, Edit = mr.Display, - Validate = fn _ => return True} + Validate = fn _ => return True, + CreateFilter = mr.CreateFilter, + DisplayFilter = mr.DisplayFilter, + Filter = fn i r => mr.Filter i r.nm} in {Initialize = m.Initialize, Handlers = fn data => case m.Handlers data of @@ -73,22 +86,30 @@ | Nullable mr => doMr mr} end - con metaBasic = fn actual_input :: (Type * Type) => - {Display : actual_input.2 -> xbody, - Edit : source actual_input.2 -> xbody, - Initialize : actual_input.1 -> actual_input.2, - InitializeNull : actual_input.2, - IsNull : actual_input.2 -> bool, - Parse : actual_input.2 -> option actual_input.1} + con metaBasic = fn actual_input_filter :: (Type * Type * Type) => + {Display : actual_input_filter.2 -> xbody, + Edit : source actual_input_filter.2 -> xbody, + Initialize : actual_input_filter.1 -> actual_input_filter.2, + InitializeNull : actual_input_filter.2, + IsNull : actual_input_filter.2 -> bool, + Parse : actual_input_filter.2 -> option actual_input_filter.1, + CreateFilter : actual_input_filter.3, + DisplayFilter : source actual_input_filter.3 -> xbody, + Filter : actual_input_filter.3 -> actual_input_filter.1 -> bool, + FilterIsNull : actual_input_filter.3 -> bool} con basicState = source - fun basic [ts ::: (Type * Type)] (m : metaBasic ts) : meta (unit, ts.1, basicState ts.2) = + con basicFilter = source + fun basic [ts ::: (Type * Type * Type)] (m : metaBasic ts) : meta (unit, ts.1, basicState ts.2, basicFilter ts.3) = {Initialize = return (), Handlers = fn () => NonNull ( {Display = fn s => <xml><dyn signal={v <- signal s; return (m.Display v)}/></xml>, Edit = m.Edit, Initialize = fn v => source (m.Initialize v), - Parse = fn s => v <- signal s; return (m.Parse v)}, + Parse = fn s => v <- signal s; return (m.Parse v), + CreateFilter = source m.CreateFilter, + DisplayFilter = m.DisplayFilter, + Filter = fn f v => f <- signal f; return (m.Filter f v)}, {Display = fn s => <xml><dyn signal={v <- signal s; return (m.Display v)}/></xml>, Edit = m.Edit, Initialize = fn v => source (case v of @@ -100,9 +121,18 @@ else case m.Parse v of None => None - | Some v' => Some (Some v'))})} + | Some v' => Some (Some v')), + CreateFilter = source m.CreateFilter, + DisplayFilter = m.DisplayFilter, + Filter = fn f v => f <- signal f; + return (if m.FilterIsNull f then + Option.isNone v + else + case v of + None => False + | Some v => m.Filter f v) : signal bool})} - fun nullable [global] [actual] [input] (m : meta (global, actual, input)) = + fun nullable [global] [actual] [input] [filter] (m : meta (global, actual, input, filter)) = {Initialize = m.Initialize, Handlers = fn d => case m.Handlers d of Nullable _ => error <xml>Don't stack calls to Direct.nullable!</xml> @@ -110,33 +140,62 @@ type intGlobal = unit type intInput = basicState string - val int : meta (intGlobal, int, intInput) = + type intFilter = basicFilter string + val int : meta (intGlobal, int, intInput, intFilter) = basic {Display = fn s => <xml>{[s]}</xml>, Edit = fn s => <xml><ctextbox source={s}/></xml>, Initialize = fn n => show n, InitializeNull = "", IsNull = eq "", - Parse = fn v => read v} + Parse = fn v => read v, + CreateFilter = "", + DisplayFilter = fn s => <xml><ctextbox source={s}/></xml> : xbody, + Filter = fn s n => + case read s of + None => True + | Some n' => n' = n, + FilterIsNull = eq ""} type stringGlobal = unit type stringInput = basicState string - val string : meta (stringGlobal, string, stringInput) = + type stringFilter = basicFilter string + val string : meta (stringGlobal, string, stringInput, stringFilter) = basic {Display = fn s => <xml>{[s]}</xml>, Edit = fn s => <xml><ctextbox source={s}/></xml>, Initialize = fn s => s, InitializeNull = "", IsNull = eq "", - Parse = fn s => Some s} + Parse = fn s => Some s, + CreateFilter = "", + DisplayFilter = fn s => <xml><ctextbox source={s}/></xml> : xbody, + Filter = fn s n => + case read s of + None => True + | Some n' => n' = n, + FilterIsNull = eq ""} type boolGlobal = unit type boolInput = basicState bool - val bool : meta (boolGlobal, bool, boolInput) = + type boolFilter = basicFilter string + val bool : meta (boolGlobal, bool, boolInput, boolFilter) = basic {Display = fn b => <xml>{[b]}</xml>, Edit = fn s => <xml><ccheckbox source={s}/></xml>, Initialize = fn b => b, InitializeNull = False, IsNull = fn _ => False, - Parse = fn b => Some b} + Parse = fn b => Some b, + CreateFilter = "", + DisplayFilter = fn s => <xml><cselect source={s}> + <coption/> + <coption value="0">False</coption> + <coption value="1">True</coption> + </cselect></xml> : xbody, + Filter = fn s b => + case s of + "0" => b = False + | "1" => b = True + | _ => True, + FilterIsNull = eq ""} functor Foreign (M : sig con row :: {Type} @@ -152,8 +211,9 @@ end) = struct open M - con global = list (t * string) - con input = source string * option (t * $row) + type global = list (t * string) + type input = source string * option (t * $row) + type filter = source string val getChoices = List.mapQuery (SELECT * FROM tab AS T) (fn r => (r.T.nm, render r.T)) @@ -162,7 +222,7 @@ r <- oneRow (SELECT T.{{row}} FROM tab AS T WHERE T.{nm} = {[k]}); return r.T - val meta : meta (global, M.t, input) = + val meta : meta (global, M.t, input, filter) = {Initialize = getChoices, Handlers = fn choices => NonNull ( @@ -182,7 +242,19 @@ Initialize = fn k => s <- source (show k); r <- rpc (getChoice k); return (s, Some (k, r)), - Parse = fn (s, _) => k <- signal s; return (read k : option t)}, + Parse = fn (s, _) => k <- signal s; return (read k : option t), + CreateFilter = source "", + DisplayFilter = fn s => + <xml><cselect source={s}> + <coption/> + {List.mapX (fn (k, rend) => + <xml><coption value={show k}>{[rend]}</coption></xml>) + choices} + </cselect></xml> : xbody, + Filter = fn s k => s <- signal s; + return (case read s : option t of + None => True + | Some k' => k' = k)}, {Display = fn (_, kr) => case kr of None => <xml>NULL</xml> | Some (k, r) => <xml>{[render ({nm = k} ++ r)]}</xml>, @@ -212,11 +284,31 @@ "" => Some None | _ => case read ks : option t of None => None - | Some k => Some (Some k))})} + | Some k => Some (Some k)), + CreateFilter = source "", + DisplayFilter = fn s => + <xml><cselect source={s}> + <coption/> + <coption value="0">NULL</coption> + {List.mapX (fn (k, rend) => + <xml><coption value={"1" ^ show k}>{[rend]}</coption> + </xml>) + choices} + </cselect></xml> : xbody, + Filter = fn s ko => s <- signal s; + return (case s of + "" => True + | "0" => ko = None + | _ => + case read (String.substring s {Start = 1, + Len = String.length s - 1}) + : option t of + None => True + | Some k => ko = Some k)})} end end -con computedState = (unit, xbody) +con computedState = (unit, xbody, unit) fun computed [row] [t] (_ : show t) name (f : $row -> t) : colMeta row computedState = {Initialize = return (), Handlers = fn () => {Header = name, @@ -224,7 +316,10 @@ Update = fn r _ => return r, Display = fn x => x, Edit = fn _ => <xml>...</xml>, - Validate = fn _ => return True}} + Validate = fn _ => return True, + CreateFilter = return (), + DisplayFilter = fn _ => <xml/>, + Filter = fn _ _ => return True}} fun computedHtml [row] name (f : $row -> xbody) : colMeta row computedState = {Initialize = return (), Handlers = fn () => {Header = name, @@ -232,7 +327,10 @@ Update = fn r _ => return r, Display = fn x => x, Edit = fn _ => <xml>...</xml>, - Validate = fn _ => return True}} + Validate = fn _ => return True, + CreateFilter = return (), + DisplayFilter = fn _ => <xml/>, + Filter = fn _ _ => return True}} functor Make(M : sig con key :: {Type} @@ -242,7 +340,7 @@ val raw : $(map rawMeta (key ++ row)) - con cols :: {(Type * Type)} + con cols :: {(Type * Type * Type)} val cols : $(map (colMeta (key ++ row)) cols) val keyFolder : folder key
--- a/demo/more/dbgrid.urs Tue Sep 15 13:07:57 2009 -0400 +++ b/demo/more/dbgrid.urs Tue Sep 15 15:48:53 2009 -0400 @@ -2,17 +2,20 @@ {New : transaction t, Inj : sql_injectable t} -con colMeta' = fn (row :: {Type}) (t :: Type) => +con colMeta' = fn (row :: {Type}) (input :: Type) (filter :: Type) => {Header : string, - Project : $row -> transaction t, - Update : $row -> t -> transaction ($row), - Display : t -> xbody, - Edit : t -> xbody, - Validate : t -> signal bool} + Project : $row -> transaction input, + Update : $row -> input -> transaction ($row), + Display : input -> xbody, + Edit : input -> xbody, + Validate : input -> signal bool, + CreateFilter : transaction filter, + DisplayFilter : filter -> xbody, + Filter : filter -> $row -> signal bool} -con colMeta = fn (row :: {Type}) (global_t :: (Type * Type)) => - {Initialize : transaction global_t.1, - Handlers : global_t.1 -> colMeta' row global_t.2} +con colMeta = fn (row :: {Type}) (global_input_filter :: (Type * Type * Type)) => + {Initialize : transaction global_input_filter.1, + Handlers : global_input_filter.1 -> colMeta' row global_input_filter.2 global_input_filter.3} con aggregateMeta = fn (row :: {Type}) (acc :: Type) => {Initial : acc, @@ -20,48 +23,55 @@ Display : acc -> xbody} structure Direct : sig - con metaBase = fn actual_input :: (Type * Type) => - {Display : actual_input.2 -> xbody, - Edit : actual_input.2 -> xbody, - Initialize : actual_input.1 -> transaction actual_input.2, - Parse : actual_input.2 -> signal (option actual_input.1)} + con metaBase = fn actual_input_filter :: (Type * Type * Type) => + {Display : actual_input_filter.2 -> xbody, + Edit : actual_input_filter.2 -> xbody, + Initialize : actual_input_filter.1 -> transaction actual_input_filter.2, + Parse : actual_input_filter.2 -> signal (option actual_input_filter.1), + CreateFilter : transaction actual_input_filter.3, + DisplayFilter : actual_input_filter.3 -> xbody, + Filter : actual_input_filter.3 -> actual_input_filter.1 -> signal bool} - datatype metaBoth actual input = - NonNull of metaBase (actual, input) * metaBase (option actual, input) - | Nullable of metaBase (actual, input) + datatype metaBoth actual input filter = + NonNull of metaBase (actual, input, filter) * metaBase (option actual, input, filter) + | Nullable of metaBase (actual, input, filter) - con meta = fn global_actual_input :: (Type * Type * Type) => - {Initialize : transaction global_actual_input.1, - Handlers : global_actual_input.1 - -> metaBoth global_actual_input.2 global_actual_input.3} + con meta = fn global_actual_input_filter :: (Type * Type * Type * Type) => + {Initialize : transaction global_actual_input_filter.1, + Handlers : global_actual_input_filter.1 + -> metaBoth global_actual_input_filter.2 global_actual_input_filter.3 + global_actual_input_filter.4} - con editableState :: (Type * Type * Type) -> (Type * Type) - val editable : ts ::: (Type * Type * Type) -> rest ::: {Type} + con editableState :: (Type * Type * Type * Type) -> (Type * Type * Type) + val editable : ts ::: (Type * Type * Type * Type) -> rest ::: {Type} -> nm :: Name -> [[nm] ~ rest] => string -> meta ts -> colMeta ([nm = ts.2] ++ rest) (editableState ts) - con readOnlyState :: (Type * Type * Type) -> (Type * Type) - val readOnly : ts ::: (Type * Type * Type) -> rest ::: {Type} + con readOnlyState :: (Type * Type * Type * Type) -> (Type * Type * Type) + val readOnly : ts ::: (Type * Type * Type * Type) -> rest ::: {Type} -> nm :: Name -> [[nm] ~ rest] => string -> meta ts -> colMeta ([nm = ts.2] ++ rest) (readOnlyState ts) - val nullable : global ::: Type -> actual ::: Type -> input ::: Type - -> meta (global, actual, input) - -> meta (global, option actual, input) + val nullable : global ::: Type -> actual ::: Type -> input ::: Type -> filter ::: Type + -> meta (global, actual, input, filter) + -> meta (global, option actual, input, filter) type intGlobal type intInput - val int : meta (intGlobal, int, intInput) + type intFilter + val int : meta (intGlobal, int, intInput, intFilter) type stringGlobal type stringInput - val string : meta (stringGlobal, string, stringInput) + type stringFilter + val string : meta (stringGlobal, string, stringInput, stringFilter) type boolGlobal type boolInput - val bool : meta (boolGlobal, bool, boolInput) + type boolFilter + val bool : meta (boolGlobal, bool, boolInput, boolFilter) functor Foreign (M : sig con row :: {Type} @@ -75,13 +85,14 @@ table tab : ([nm = t] ++ row) val render : $([nm = t] ++ row) -> string end) : sig - con global :: Type - con input :: Type - val meta : meta (global, M.t, input) + type global + type input + type filter + val meta : meta (global, M.t, input, filter) end end -con computedState :: (Type * Type) +con computedState :: (Type * Type * Type) val computed : row ::: {Type} -> t ::: Type -> show t -> string -> ($row -> t) -> colMeta row computedState val computedHtml : row ::: {Type} -> string -> ($row -> xbody) -> colMeta row computedState @@ -94,7 +105,7 @@ val raw : $(map rawMeta (key ++ row)) - con cols :: {(Type * Type)} + con cols :: {(Type * Type * Type)} val cols : $(map (colMeta (key ++ row)) cols) val keyFolder : folder key
--- a/demo/more/dlist.ur Tue Sep 15 13:07:57 2009 -0400 +++ b/demo/more/dlist.ur Tue Sep 15 15:48:53 2009 -0400 @@ -6,18 +6,19 @@ Empty | Nonempty of { Head : dlist'' t, Tail : source (source (dlist'' t)) } -con dlist t = source (dlist' t) +con dlist t = {Filter: t -> signal bool, + Elements : source (dlist' t)} type position = transaction unit fun headPos [t] (dl : dlist t) = - dl' <- get dl; + dl' <- get dl.Elements; case dl' of Nonempty { Head = Cons (_, tl), Tail = tl' } => cur <- get tl; - set dl (case cur of - Nil => Empty - | _ => Nonempty {Head = cur, Tail = tl'}) + set dl.Elements (case cur of + Nil => Empty + | _ => Nonempty {Head = cur, Tail = tl'}) | _ => return () fun tailPos [t] (cur : source (dlist'' t)) new tail = @@ -28,17 +29,20 @@ Nil => set tail cur | _ => return () -val create = fn [t] => source Empty +fun create [t] r = + s <- source Empty; + return {Filter = r.Filter, + Elements = s} -fun clear [t] (s : dlist t) = set s Empty +fun clear [t] (s : dlist t) = set s.Elements Empty fun append [t] dl v = - dl' <- get dl; + dl' <- get dl.Elements; case dl' of Empty => tl <- source Nil; tl' <- source tl; - set dl (Nonempty {Head = Cons (v, tl), Tail = tl'}); + set dl.Elements (Nonempty {Head = Cons (v, tl), Tail = tl'}); return (headPos dl) | Nonempty {Tail = tl, ...} => @@ -49,7 +53,7 @@ return (tailPos cur new tl) fun render [ctx] [ctx ~ body] [t] f dl = <xml> - <dyn signal={dl' <- signal dl; + <dyn signal={dl' <- signal dl.Elements; return (case dl' of Empty => <xml/> | Nonempty {Head = hd, Tail = tlTop} => @@ -63,8 +67,13 @@ None => headPos dl | Some prev => tailPos prev tl tlTop in - <xml>{f v pos}<dyn signal={tl' <- signal tl; - return (render' (Some tl) tl')}/></xml> + <xml><dyn signal={b <- dl.Filter v; + return (if b then + f v pos + else + <xml/>)}/> + <dyn signal={tl' <- signal tl; + return (render' (Some tl) tl')}/></xml> end in render' None hd @@ -82,7 +91,7 @@ return (x :: tl) fun elements [t] (dl : dlist t) = - dl' <- signal dl; + dl' <- signal dl.Elements; case dl' of Empty => return [] | Nonempty {Head = hd, ...} => elements' hd @@ -98,7 +107,7 @@ foldl'' i' dl' fun foldl' (i : acc) (dl : dlist t) : signal acc = - dl <- signal dl; + dl <- signal dl.Elements; case dl of Empty => return i | Nonempty {Head = dl, ...} => foldl'' i dl
--- a/demo/more/dlist.urs Tue Sep 15 13:07:57 2009 -0400 +++ b/demo/more/dlist.urs Tue Sep 15 15:48:53 2009 -0400 @@ -1,7 +1,7 @@ con dlist :: Type -> Type type position -val create : t ::: Type -> transaction (dlist t) +val create : t ::: Type -> {Filter : t -> signal bool} -> transaction (dlist t) val clear : t ::: Type -> dlist t -> transaction unit val append : t ::: Type -> dlist t -> t -> transaction position val delete : position -> transaction unit
--- a/demo/more/grid.ur Tue Sep 15 13:07:57 2009 -0400 +++ b/demo/more/grid.ur Tue Sep 15 15:48:53 2009 -0400 @@ -1,14 +1,17 @@ -con colMeta' = fn (row :: Type) (t :: Type) => +con colMeta' = fn (row :: Type) (input :: Type) (filter :: Type) => {Header : string, - Project : row -> transaction t, - Update : row -> t -> transaction row, - Display : t -> xbody, - Edit : t -> xbody, - Validate : t -> signal bool} - -con colMeta = fn (row :: Type) (global_t :: (Type * Type)) => - {Initialize : transaction global_t.1, - Handlers : global_t.1 -> colMeta' row global_t.2} + Project : row -> transaction input, + Update : row -> input -> transaction row, + Display : input -> xbody, + Edit : input -> xbody, + Validate : input -> signal bool, + CreateFilter : transaction filter, + DisplayFilter : filter -> xbody, + Filter : filter -> row -> signal bool} + +con colMeta = fn (row :: Type) (global_input_filter :: (Type * Type * Type)) => + {Initialize : transaction global_input_filter.1, + Handlers : global_input_filter.1 -> colMeta' row global_input_filter.2 global_input_filter.3} con aggregateMeta = fn (row :: Type) (acc :: Type) => {Initial : acc, @@ -25,7 +28,7 @@ val save : key -> row -> transaction unit val delete : key -> transaction unit - con cols :: {(Type * Type)} + con cols :: {(Type * Type * Type)} val cols : $(map (colMeta row) cols) val folder : folder cols @@ -40,20 +43,21 @@ style td style agg - fun make (row : M.row) [t] (m : colMeta' M.row t) : transaction t = m.Project row + 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 snd M.cols] - (map2 [fst] [colMeta M.row] [fn p :: (Type * Type) => transaction p.2] - (fn [p] data meta => make row [_] (meta.Handlers data)) + 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) (@@Folder.mp [_] [_] M.folder) - type grid = {Cols : $(map fst M.cols), + type grid = {Cols : $(map fst3 M.cols), Rows : Dlist.dlist {Row : source M.row, - Cols : source ($(map snd M.cols)), + Cols : source ($(map snd3 M.cols)), Updating : source bool, Selected : source bool}, - Selection : source bool} + Selection : source bool, + Filters : $(map thd3 M.cols)} fun addRow cols rows row = rowS <- source row; @@ -66,15 +70,29 @@ Updating = ud, Selected = sd}) - val createMetas = Monad.mapR [colMeta M.row] [fst] - (fn [nm :: Name] [p :: (Type * Type)] meta => meta.Initialize) - [_] M.folder M.cols + val grid = + cols <- Monad.mapR [colMeta M.row] [fst3] + (fn [nm :: Name] [p :: (Type * Type * Type)] meta => meta.Initialize) + [_] M.folder M.cols; - val grid = - cols <- createMetas; - rows <- Dlist.create; + 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 {Filter = fn 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 cols filters row}; sel <- source False; - return {Cols = cols, Rows = rows, Selection = sel} + return {Cols = cols, Rows = rows, Selection = sel, Filters = filters} fun sync {Cols = cols, Rows = rows, ...} = Dlist.clear rows; @@ -85,8 +103,8 @@ <table class={tabl}> <tr class={tr}> <th/> <th/> <th/> - {foldRX2 [fst] [colMeta M.row] [_] - (fn [nm :: Name] [p :: (Type * Type)] [rest :: {(Type * Type)}] [[nm] ~ rest] + {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}>{[(meta.Handlers data).Header]}</th></xml>) [_] M.folder grid.Cols M.cols} @@ -109,8 +127,8 @@ val save = cols <- get colsS; - errors <- Monad.foldR3 [fst] [colMeta M.row] [snd] [fn _ => option string] - (fn [nm :: Name] [p :: (Type * Type)] [rest :: {(Type * Type)}] + 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 @@ -128,9 +146,9 @@ | None => set ud False; row <- get rowS; - row' <- Monad.foldR3 [fst] [colMeta M.row] [snd] [fn _ => M.row] - (fn [nm :: Name] [t :: (Type * Type)] - [rest :: {(Type * Type)}] + 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; @@ -165,9 +183,9 @@ </td> <dyn signal={cols <- signal colsS; - return (foldRX3 [fst] [colMeta M.row] [snd] [_] - (fn [nm :: Name] [t :: (Type * Type)] - [rest :: {(Type * Type)}] + 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; @@ -206,6 +224,13 @@ <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} + </tr> </table> <button value="New row" onclick={row <- rpc M.new;
--- a/demo/more/grid.urp Tue Sep 15 13:07:57 2009 -0400 +++ b/demo/more/grid.urp Tue Sep 15 15:48:53 2009 -0400 @@ -2,6 +2,7 @@ $/option $/monad $/list +$/string dlist grid dbgrid
--- a/demo/more/grid.urs Tue Sep 15 13:07:57 2009 -0400 +++ b/demo/more/grid.urs Tue Sep 15 15:48:53 2009 -0400 @@ -1,14 +1,17 @@ -con colMeta' = fn (row :: Type) (t :: Type) => +con colMeta' = fn (row :: Type) (input :: Type) (filter :: Type) => {Header : string, - Project : row -> transaction t, - Update : row -> t -> transaction row, - Display : t -> xbody, - Edit : t -> xbody, - Validate : t -> signal bool} + Project : row -> transaction input, + Update : row -> input -> transaction row, + Display : input -> xbody, + Edit : input -> xbody, + Validate : input -> signal bool, + CreateFilter : transaction filter, + DisplayFilter : filter -> xbody, + Filter : filter -> row -> signal bool} -con colMeta = fn (row :: Type) (global_t :: (Type * Type)) => - {Initialize : transaction global_t.1, - Handlers : global_t.1 -> colMeta' row global_t.2} +con colMeta = fn (row :: Type) (global_input_filter :: (Type * Type * Type)) => + {Initialize : transaction global_input_filter.1, + Handlers : global_input_filter.1 -> colMeta' row global_input_filter.2 global_input_filter.3} con aggregateMeta = fn (row :: Type) (acc :: Type) => {Initial : acc, @@ -25,7 +28,7 @@ val save : key -> row -> transaction unit val delete : key -> transaction unit - con cols :: {(Type * Type)} + con cols :: {(Type * Type * Type)} val cols : $(map (colMeta row) cols) val folder : folder cols
--- a/lib/ur/option.ur Tue Sep 15 13:07:57 2009 -0400 +++ b/lib/ur/option.ur Tue Sep 15 15:48:53 2009 -0400 @@ -7,6 +7,11 @@ | (Some x, Some y) => x = y | _ => False) +fun isNone [a] x = + case x of + None => True + | Some _ => False + fun isSome [a] x = case x of None => False
--- a/lib/ur/option.urs Tue Sep 15 13:07:57 2009 -0400 +++ b/lib/ur/option.urs Tue Sep 15 15:48:53 2009 -0400 @@ -2,6 +2,7 @@ val eq : a ::: Type -> eq a -> eq (t a) +val isNone : a ::: Type -> t a -> bool val isSome : a ::: Type -> t a -> bool val mp : a ::: Type -> b ::: Type -> (a -> b) -> t a -> t b