From c9c3eaa4c489077ef0199eacc16674b328348734 Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adamc@hcoop.net>
Date: Sat, 19 Sep 2009 13:55:37 -0400
Subject: Testing Dlist MaxLength with constant value

---
 demo/more/dlist.ur  | 77 +++++++++++++++++++++++++++++++++++------------------
 demo/more/dlist.urs |  1 +
 demo/more/grid.ur   |  1 +
 3 files changed, 53 insertions(+), 26 deletions(-)

(limited to 'demo')

diff --git a/demo/more/dlist.ur b/demo/more/dlist.ur
index 3bec8077..1a5be7e3 100644
--- a/demo/more/dlist.ur
+++ b/demo/more/dlist.ur
@@ -66,29 +66,33 @@ fun replace [t] dl ls =
             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 @@ fun renderDyn [ctx] [ctx ~ body] [t] (f : t -> position -> xml (ctx ++ body) []
                                    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 sort [t] (cmp : t -> t -> signal bool) =
 
 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 @@ fun render [ctx] [ctx ~ body] [t] f (r : {Filter : t -> signal bool,
                                  None => elems
                                | Some pos => skip pos elems
                      in
-                         return (renderFlat f r.Filter elems)
+                         return (renderFlat f r.Filter len elems)
                      end}/>
 </xml>
 
diff --git a/demo/more/dlist.urs b/demo/more/dlist.urs
index cd42f9ee..4da61863 100644
--- a/demo/more/dlist.urs
+++ b/demo/more/dlist.urs
@@ -13,6 +13,7 @@ val foldl : t ::: Type -> acc ::: Type -> (t -> acc -> signal acc) -> acc -> dli
 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 --git a/demo/more/grid.ur b/demo/more/grid.ur
index dbaca7db..560ff146 100644
--- a/demo/more/grid.ur
+++ b/demo/more/grid.ur
@@ -217,6 +217,7 @@ functor Make(M : sig
                                 </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]
-- 
cgit v1.2.3