# HG changeset patch
# User Adam Chlipala <adamc@hcoop.net>
# Date 1253385756 14400
# Node ID e9c5992bc9bcab8c6239e270f1ef1f87c3577b40
# Parent  fbc3a0eef45ac4acc955f32d58a3aa8abdec6728
Progress on sorting + filtering

diff -r fbc3a0eef45a -r e9c5992bc9bc demo/more/dlist.ur
--- 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 =
diff -r fbc3a0eef45a -r e9c5992bc9bc demo/more/dlist.urs
--- 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
diff -r fbc3a0eef45a -r e9c5992bc9bc demo/more/grid.ur
--- 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