From e2170d73e8d43842996910a6b512df89e20be389 Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adamc@hcoop.net>
Date: Thu, 17 Sep 2009 14:27:00 -0400
Subject: Make filter argument to render, not create

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

(limited to 'demo')

diff --git a/demo/more/dlist.ur b/demo/more/dlist.ur
index d4a255ee..a99244ec 100644
--- a/demo/more/dlist.ur
+++ b/demo/more/dlist.ur
@@ -6,19 +6,18 @@ datatype dlist' t =
          Empty
        | Nonempty of { Head : dlist'' t, Tail : source (source (dlist'' t)) }
 
-con dlist t = {Filter: t -> signal bool,
-               Elements : source (dlist' t)}
+con dlist t = source (dlist' t)
 
 type position = transaction unit
 
 fun headPos [t] (dl : dlist t) =
-    dl' <- get dl.Elements;
+    dl' <- get dl;
     case dl' of
         Nonempty { Head = Cons (_, tl), Tail = tl' } =>
         cur <- get tl;
-        set dl.Elements (case cur of
-                             Nil => Empty
-                           | _ => Nonempty {Head = cur, Tail = tl'})
+        set dl (case cur of
+                    Nil => Empty
+                  | _ => Nonempty {Head = cur, Tail = tl'})
       | _ => return ()
 
 fun tailPos [t] (cur : source (dlist'' t)) new tail =
@@ -29,20 +28,17 @@ fun tailPos [t] (cur : source (dlist'' t)) new tail =
         Nil => set tail cur
       | _ => return ()
 
-fun create [t] r =
-    s <- source Empty;
-    return {Filter = r.Filter,
-            Elements = s}
+val create [t] = source Empty
 
-fun clear [t] (s : dlist t) = set s.Elements Empty
+fun clear [t] (s : dlist t) = set s Empty
 
 fun append [t] dl v =
-    dl' <- get dl.Elements;
+    dl' <- get dl;
     case dl' of
         Empty =>
         tl <- source Nil;
         tl' <- source tl;
-        set dl.Elements (Nonempty {Head = Cons (v, tl), Tail = tl'});
+        set dl (Nonempty {Head = Cons (v, tl), Tail = tl'});
         return (headPos dl)
                 
       | Nonempty {Tail = tl, ...} =>
@@ -52,8 +48,8 @@ fun append [t] dl v =
         set tl new;
         return (tailPos cur new tl)
 
-fun render [ctx] [ctx ~ body] [t] f dl = <xml>
-  <dyn signal={dl' <- signal dl.Elements;
+fun render [ctx] [ctx ~ body] [t] f {Filter = filter, ...} dl = <xml>
+  <dyn signal={dl' <- signal dl;
                return (case dl' of
                            Empty => <xml/>
                          | Nonempty {Head = hd, Tail = tlTop} => 
@@ -67,7 +63,7 @@ fun render [ctx] [ctx ~ body] [t] f dl = <xml>
                                                          None => headPos dl
                                                        | Some prev => tailPos prev tl tlTop
                                        in
-                                           <xml><dyn signal={b <- dl.Filter v;
+                                           <xml><dyn signal={b <- filter v;
                                                              return (if b then
                                                                          f v pos
                                                                      else
@@ -91,7 +87,7 @@ fun elements' [t] (dl'' : dlist'' t) =
         return (x :: tl)
 
 fun elements [t] (dl : dlist t) =
-    dl' <- signal dl.Elements;
+    dl' <- signal dl;
     case dl' of
         Empty => return []
       | Nonempty {Head = hd, ...} => elements' hd
@@ -107,7 +103,7 @@ fun foldl [t] [acc] (f : t -> acc -> signal acc) =
                 foldl'' i' dl'
 
         fun foldl' (i : acc) (dl : dlist t) : signal acc =
-            dl <- signal dl.Elements;
+            dl <- signal dl;
             case dl of
                 Empty => return i
               | Nonempty {Head = dl, ...} => foldl'' i dl
diff --git a/demo/more/dlist.urs b/demo/more/dlist.urs
index a55a1774..a775113e 100644
--- a/demo/more/dlist.urs
+++ b/demo/more/dlist.urs
@@ -1,7 +1,7 @@
 con dlist :: Type -> Type
 type position
 
-val create : t ::: Type -> {Filter : t -> signal bool} -> transaction (dlist t)
+val create : t ::: Type -> transaction (dlist t)
 val clear : t ::: Type -> dlist t -> transaction unit
 val append : t ::: Type -> dlist t -> t -> transaction position
 val delete : position -> transaction unit
@@ -10,5 +10,6 @@ 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}
              -> dlist t
              -> xml (ctx ++ body) [] []
diff --git a/demo/more/grid.ur b/demo/more/grid.ur
index 424c3b6f..6dd0543a 100644
--- a/demo/more/grid.ur
+++ b/demo/more/grid.ur
@@ -80,19 +80,13 @@ functor Make(M : sig
                                    (meta.Handlers state).CreateFilter)
                                [_] M.folder M.cols cols;
 
-        rows <- Dlist.create {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 cols filters row};
+        rows <- Dlist.create;
         sel <- source False;
-        return {Cols = cols, Rows = rows, Selection = sel, Filters = filters}
+
+        return {Cols = cols,
+                Rows = rows,
+                Selection = sel,
+                Filters = filters}
 
     fun sync {Cols = cols, Rows = rows, ...} =
         Dlist.clear rows;
@@ -207,7 +201,19 @@ functor Make(M : sig
                                                                  </td></xml>)
                                                              [_] M.folder grid.Cols M.cols cols)}/>
                                 </tr></xml>
-                          end) grid.Rows}
+                          end)
+                      {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}
+                      grid.Rows}
 
             <dyn signal={rows <- Dlist.foldl (fn row => Monad.mapR2 [aggregateMeta M.row] [id] [id]
                                                                     (fn [nm :: Name] [t :: Type] meta acc =>
-- 
cgit v1.2.3