aboutsummaryrefslogtreecommitdiffhomepage
path: root/demo
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2009-09-19 14:42:36 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2009-09-19 14:42:36 -0400
commit3bf0f6b7a465e3f24eff57633ee8aa3bbe41422a (patch)
treec66699a201ad33330f7547289548ce1fdf714f0f /demo
parent142e0b28763660019a6fc0fc4a9383fb43b77407 (diff)
Progress on sorting + filtering
Diffstat (limited to 'demo')
-rw-r--r--demo/more/dlist.ur15
-rw-r--r--demo/more/dlist.urs1
-rw-r--r--demo/more/grid.ur36
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