From db87f2d9dd9ef6ea5a9471e13fce81515900e4dc Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adamc@hcoop.net>
Date: Thu, 17 Sep 2009 14:42:02 -0400
Subject: Insert dummy Sort parameter

---
 demo/more/dlist.ur  | 35 ++++++++++++++++++++++++++++++++++-
 demo/more/dlist.urs |  3 ++-
 demo/more/grid.ur   |  3 ++-
 3 files changed, 38 insertions(+), 3 deletions(-)

(limited to 'demo')

diff --git a/demo/more/dlist.ur b/demo/more/dlist.ur
index a99244ec..244c54a7 100644
--- a/demo/more/dlist.ur
+++ b/demo/more/dlist.ur
@@ -48,7 +48,7 @@ fun append [t] dl v =
         set tl new;
         return (tailPos cur new tl)
 
-fun render [ctx] [ctx ~ body] [t] f {Filter = filter, ...} dl = <xml>
+fun renderDyn [ctx] [ctx ~ body] [t] (f : t -> position -> xml (ctx ++ body) [] []) filter dl = <xml>
   <dyn signal={dl' <- signal dl;
                return (case dl' of
                            Empty => <xml/>
@@ -76,6 +76,39 @@ fun render [ctx] [ctx ~ body] [t] f {Filter = filter, ...} dl = <xml>
                            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 render [ctx] [ctx ~ body] [t] f r dl = <xml>
+    <dyn signal={sort <- r.Sort;
+                 case sort of
+                     None => return (renderDyn f r.Filter dl)
+                   | Some sort =>
+                     dl' <- signal dl;
+                     elems <- (case dl' of
+                                   Empty => return []
+                                 | Nonempty {Head = hd, Tail = tlTop} =>
+                                   let
+                                       fun listOut prev dl'' acc =
+                                           case dl'' of
+                                               Nil => return acc
+                                             | Cons (v, tl) =>
+                                               let
+                                                   val pos = case prev of
+                                                                 None => headPos dl
+                                                               | Some prev => tailPos prev tl tlTop
+                                               in
+                                                   tl' <- signal tl;
+                                                   listOut (Some tl) tl' ((v, pos) :: acc)
+                                               end
+                                   in
+                                       listOut None hd []
+                                   end);
+                     return (renderFlat f r.Filter elems)}/>
+</xml>
+                             
+        
+
 fun delete pos = pos
 
 fun elements' [t] (dl'' : dlist'' t) =
diff --git a/demo/more/dlist.urs b/demo/more/dlist.urs
index a775113e..b912139e 100644
--- a/demo/more/dlist.urs
+++ b/demo/more/dlist.urs
@@ -10,6 +10,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) [] [])
-             -> {Filter : t -> signal bool}
+             -> {Filter : t -> signal bool,
+                 Sort : signal (option (t -> t -> signal bool)) (* <= *)}
              -> dlist t
              -> xml (ctx ++ body) [] []
diff --git a/demo/more/grid.ur b/demo/more/grid.ur
index 6dd0543a..a59e1082 100644
--- a/demo/more/grid.ur
+++ b/demo/more/grid.ur
@@ -212,7 +212,8 @@ functor Make(M : sig
                                               this <- (meta.Handlers state).Filter filter row;
                                               return (previous && this))
                                           (fn _ => return True)
-                                          [_] M.folder M.cols grid.Cols grid.Filters row}
+                                          [_] M.folder M.cols grid.Cols grid.Filters row,
+                       Sort = return None}
                       grid.Rows}
 
             <dyn signal={rows <- Dlist.foldl (fn row => Monad.mapR2 [aggregateMeta M.row] [id] [id]
-- 
cgit v1.2.3