diff options
author | Adam Chlipala <adamc@hcoop.net> | 2009-09-19 14:42:36 -0400 |
---|---|---|
committer | Adam Chlipala <adamc@hcoop.net> | 2009-09-19 14:42:36 -0400 |
commit | 3bf0f6b7a465e3f24eff57633ee8aa3bbe41422a (patch) | |
tree | c66699a201ad33330f7547289548ce1fdf714f0f /demo/more | |
parent | 142e0b28763660019a6fc0fc4a9383fb43b77407 (diff) |
Progress on sorting + filtering
Diffstat (limited to 'demo/more')
-rw-r--r-- | demo/more/dlist.ur | 15 | ||||
-rw-r--r-- | demo/more/dlist.urs | 1 | ||||
-rw-r--r-- | demo/more/grid.ur | 36 |
3 files changed, 39 insertions, 13 deletions
diff --git a/demo/more/dlist.ur b/demo/more/dlist.ur index fe0cdd07..277f1219 100644 --- a/demo/more/dlist.ur +++ b/demo/more/dlist.ur @@ -260,6 +260,21 @@ fun size [t] (dl : dlist t) = 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 = diff --git a/demo/more/dlist.urs b/demo/more/dlist.urs index 6918fdc8..3509ef2d 100644 --- a/demo/more/dlist.urs +++ b/demo/more/dlist.urs @@ -9,6 +9,7 @@ val replace : t ::: Type -> dlist t -> list t -> transaction unit 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 diff --git a/demo/more/grid.ur b/demo/more/grid.ur index d63a1424..f2b9681c 100644 --- a/demo/more/grid.ur +++ b/demo/more/grid.ur @@ -107,6 +107,18 @@ functor Make(M : sig 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 @@ functor Make(M : sig [_] 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 @@ functor Make(M : sig {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 |