Mercurial > urweb
changeset 965:e9c5992bc9bc
Progress on sorting + filtering
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Sat, 19 Sep 2009 14:42:36 -0400 |
parents | fbc3a0eef45a |
children | c2fe1dbaceb9 |
files | demo/more/dlist.ur demo/more/dlist.urs demo/more/grid.ur |
diffstat | 3 files changed, 39 insertions(+), 13 deletions(-) [+] |
line wrap: on
line diff
--- a/demo/more/dlist.ur Sat Sep 19 14:21:25 2009 -0400 +++ b/demo/more/dlist.ur Sat Sep 19 14:42:36 2009 -0400 @@ -260,6 +260,21 @@ Empty => return 0 | Nonempty {Head = hd, ...} => size' hd +fun numPassing' [t] (f : t -> signal bool) (dl'' : dlist'' t) = + case dl'' of + Nil => return 0 + | Cons (x, dl'') => + b <- f x; + dl'' <- signal dl''; + n <- numPassing' f dl''; + return (if b then n + 1 else n) + +fun numPassing [t] (f : t -> signal bool) (dl : dlist t) = + dl' <- signal dl; + case dl' of + Empty => return 0 + | Nonempty {Head = hd, ...} => numPassing' f hd + fun foldl [t] [acc] (f : t -> acc -> signal acc) = let fun foldl'' (i : acc) (dl : dlist'' t) : signal acc =
--- a/demo/more/dlist.urs Sat Sep 19 14:21:25 2009 -0400 +++ b/demo/more/dlist.urs Sat Sep 19 14:42:36 2009 -0400 @@ -9,6 +9,7 @@ val delete : position -> transaction unit val elements : t ::: Type -> dlist t -> signal (list t) val size : t ::: Type -> dlist t -> signal int +val numPassing : t ::: Type -> (t -> signal bool) -> dlist t -> signal int val foldl : t ::: Type -> acc ::: Type -> (t -> acc -> signal acc) -> acc -> dlist t -> signal acc val render : ctx ::: {Unit} -> [ctx ~ body] => t ::: Type
--- a/demo/more/grid.ur Sat Sep 19 14:21:25 2009 -0400 +++ b/demo/more/grid.ur Sat Sep 19 14:42:36 2009 -0400 @@ -107,6 +107,18 @@ rs <- List.mapM (newRow cols) init; Dlist.replace rows rs + 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 + fun render (grid : grid) = <xml> <table class={tabl}> <tr class={tr}> @@ -221,19 +233,17 @@ [_] M.folder grid.Cols M.cols cols)}/> </tr></xml> end) - {StartPosition = Monad.mp Some (signal grid.Position), + {StartPosition = case M.pageLength of + None => return None + | Some len => + avail <- Dlist.numPassing (myFilter grid) grid.Rows; + pos <- signal grid.Position; + return (Some (if pos >= avail then + 0 + else + pos)), MaxLength = return M.pageLength, - 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 grid.Cols grid.Filters row, + Filter = myFilter grid, Sort = f <- signal grid.Sort; return (Option.mp (fn f r1 r2 => r1 <- signal r1.Row; r2 <- signal r2.Row; @@ -267,7 +277,7 @@ {case M.pageLength of None => <xml/> | Some plen => <xml> - <dyn signal={avail <- Dlist.size grid.Rows; + <dyn signal={avail <- Dlist.numPassing (myFilter grid) grid.Rows; return (if avail <= plen then <xml/> else