# HG changeset patch
# User Adam Chlipala <adamc@hcoop.net>
# Date 1253382937 14400
# Node ID 6f9d1565de56027a19fda69bc31c093c41f56306
# Parent  7e7edfb6fe8248a406eb13cb9480bfa787a971ea
Testing Dlist MaxLength with constant value

diff -r 7e7edfb6fe82 -r 6f9d1565de56 demo/more/dlist.ur
--- a/demo/more/dlist.ur	Sat Sep 19 13:44:12 2009 -0400
+++ b/demo/more/dlist.ur	Sat Sep 19 13:55:37 2009 -0400
@@ -66,29 +66,33 @@
             set dl (Nonempty {Head = Cons (x, hd), Tail = tlS})
         end
 
-fun renderDyn [ctx] [ctx ~ body] [t] (f : t -> position -> xml (ctx ++ body) [] []) filter pos dl = <xml>
+fun renderDyn [ctx] [ctx ~ body] [t] (f : t -> position -> xml (ctx ++ body) [] []) filter pos len dl = <xml>
   <dyn signal={dl' <- signal dl;
                case dl' of
                    Empty => return <xml/>
                  | Nonempty {Head = hd, Tail = tlTop} => 
                    let
-                       fun render' prev dl'' =
-                           case dl'' of
-                               Nil => <xml/>
-                             | Cons (v, tl) =>
-                               let
-                                   val pos = case prev of
-                                                 None => headPos dl
-                                               | Some prev => tailPos prev tl tlTop
-                               in
-                                   <xml><dyn signal={b <- filter v;
-                                                     return (if b then
-                                                                 f v pos
-                                                             else
-                                                                 <xml/>)}/>
-                                     <dyn signal={tl' <- signal tl;
-                                                  return (render' (Some tl) tl')}/></xml>
-                               end
+                       fun render' prev dl'' len =
+                           case len of
+                               Some 0 => <xml/>
+                             | _ =>
+                               case dl'' of
+                                   Nil => <xml/>
+                                 | Cons (v, tl) =>
+                                   let
+                                       val pos = case prev of
+                                                     None => headPos dl
+                                                   | Some prev => tailPos prev tl tlTop
+                                       val len = Option.mp (fn n => n - 1) len
+                                   in
+                                       <xml><dyn signal={b <- filter v;
+                                                         return (if b then
+                                                                     f v pos
+                                                                 else
+                                                                     <xml/>)}/>
+                                         <dyn signal={tl' <- signal tl;
+                                                      return (render' (Some tl) tl' len)}/></xml>
+                                   end
 
                        fun skip pos hd =
                            case pos of
@@ -101,15 +105,33 @@
                                    skip (pos-1) tl'
                    in
                        case pos of
-                           None => return (render' None hd)
+                           None => return (render' None hd len)
                          | Some pos =>
                            hd <- skip pos hd;
-                           return (render' None hd)
+                           return (render' None hd len)
                    end}/>
 </xml>
 
-fun renderFlat [ctx] [ctx ~ body] [t] (f : t -> position -> xml (ctx ++ body) [] []) filter ls =
-    List.mapX (fn p => f p.1 p.2) ls
+fun renderFlat [ctx] [ctx ~ body] [t] (f : t -> position -> xml (ctx ++ body) [] []) filter =
+    let
+        fun renderFlat' len ls =
+            case len of
+                Some 0 => <xml/>
+              | _ =>
+                case ls of
+                    [] => <xml/>
+                  | p :: ls =>
+                    let
+                        val len =
+                            case len of
+                                None => None
+                              | Some n => Some (n - 1)
+                    in
+                        <xml>{f p.1 p.2}{renderFlat' len ls}</xml>
+                    end
+    in
+        renderFlat'
+    end
 
 val split [t] =
     let
@@ -158,11 +180,14 @@
 
 fun render [ctx] [ctx ~ body] [t] f (r : {Filter : t -> signal bool,
                                           Sort : signal (option (t -> t -> signal bool)),
-                                          StartPosition : signal (option int)}) dl = <xml>
-    <dyn signal={cmp <- r.Sort;
+                                          StartPosition : signal (option int),
+                                          MaxLength : signal (option int)}) dl = <xml>
+    <dyn signal={len <- r.MaxLength;
+                 cmp <- r.Sort;
                  pos <- r.StartPosition;
+
                  case cmp of
-                     None => return (renderDyn f r.Filter pos dl)
+                     None => return (renderDyn f r.Filter pos len dl)
                    | Some cmp =>
                      dl' <- signal dl;
                      elems <- (case dl' of
@@ -201,7 +226,7 @@
                                  None => elems
                                | Some pos => skip pos elems
                      in
-                         return (renderFlat f r.Filter elems)
+                         return (renderFlat f r.Filter len elems)
                      end}/>
 </xml>
 
diff -r 7e7edfb6fe82 -r 6f9d1565de56 demo/more/dlist.urs
--- a/demo/more/dlist.urs	Sat Sep 19 13:44:12 2009 -0400
+++ b/demo/more/dlist.urs	Sat Sep 19 13:55:37 2009 -0400
@@ -13,6 +13,7 @@
 val render : ctx ::: {Unit} -> [ctx ~ body] => t ::: Type
              -> (t -> position -> xml (ctx ++ body) [] [])
              -> {StartPosition : signal (option int),
+                 MaxLength : signal (option int),
                  Filter : t -> signal bool,
                  Sort : signal (option (t -> t -> signal bool)) (* <= *)}
              -> dlist t
diff -r 7e7edfb6fe82 -r 6f9d1565de56 demo/more/grid.ur
--- a/demo/more/grid.ur	Sat Sep 19 13:44:12 2009 -0400
+++ b/demo/more/grid.ur	Sat Sep 19 13:55:37 2009 -0400
@@ -217,6 +217,7 @@
                                 </tr></xml>
                           end)
                       {StartPosition = return (Some 1),
+                       MaxLength = return (Some 2),
                        Filter = fn all =>
                                    row <- signal all.Row;
                                    foldR3 [colMeta M.row] [fst3] [thd3] [fn _ => M.row -> signal bool]