# HG changeset patch
# User Adam Chlipala <adamc@hcoop.net>
# Date 1253024336 14400
# Node ID 37dd42935dadc4f5f51eda5ed2a05b0ea80248c7
# Parent  6966d98c80b5e8de91ef89a8e4def0b5b695cdf3
Summary row with aggregates

diff -r 6966d98c80b5 -r 37dd42935dad demo/more/dbgrid.ur
--- a/demo/more/dbgrid.ur	Tue Sep 15 09:45:46 2009 -0400
+++ b/demo/more/dbgrid.ur	Tue Sep 15 10:18:56 2009 -0400
@@ -251,6 +251,7 @@
 
                  con aggregates :: {Type}
                  val aggregates : $(map (aggregateMeta (key ++ row)) aggregates)
+                 val aggFolder : folder aggregates
              end) = struct
     open Grid.Make(struct
                        fun keyOf r = r --- M.row
@@ -297,5 +298,7 @@
                        val folder = M.colsFolder
 
                        val aggregates = M.aggregates
+
+                       val aggFolder = M.aggFolder
                    end)
 end
diff -r 6966d98c80b5 -r 37dd42935dad demo/more/dbgrid.urs
--- a/demo/more/dbgrid.urs	Tue Sep 15 09:45:46 2009 -0400
+++ b/demo/more/dbgrid.urs	Tue Sep 15 10:18:56 2009 -0400
@@ -103,6 +103,7 @@
 
                  con aggregates :: {Type}
                  val aggregates : $(map (aggregateMeta (key ++ row)) aggregates)
+                 val aggFolder : folder aggregates
              end) : sig
     type grid
 
diff -r 6966d98c80b5 -r 37dd42935dad demo/more/dlist.ur
--- a/demo/more/dlist.ur	Tue Sep 15 09:45:46 2009 -0400
+++ b/demo/more/dlist.ur	Tue Sep 15 10:18:56 2009 -0400
@@ -86,3 +86,22 @@
     case dl' of
         Empty => return []
       | Nonempty {Head = hd, ...} => elements' hd
+
+fun foldl [t] [acc] (f : t -> acc -> signal acc) =
+    let
+        fun foldl'' (i : acc) (dl : dlist'' t) : signal acc =
+            case dl of
+                Nil => return i
+              | Cons (v, dl') =>
+                dl' <- signal dl';
+                i' <- f v i;
+                foldl'' i' dl'
+
+        fun foldl' (i : acc) (dl : dlist t) : signal acc =
+            dl <- signal dl;
+            case dl of
+                Empty => return i
+              | Nonempty {Head = dl, ...} => foldl'' i dl
+    in
+        foldl'
+    end
diff -r 6966d98c80b5 -r 37dd42935dad demo/more/dlist.urs
--- a/demo/more/dlist.urs	Tue Sep 15 09:45:46 2009 -0400
+++ b/demo/more/dlist.urs	Tue Sep 15 10:18:56 2009 -0400
@@ -6,6 +6,7 @@
 val append : t ::: Type -> dlist t -> t -> transaction position
 val delete : position -> transaction unit
 val elements : t ::: Type -> dlist t -> signal (list t)
+val foldl : t ::: Type -> acc ::: Type -> (t -> acc -> signal acc) -> acc -> dlist t -> signal acc
 
 val render : ctx ::: {Unit} -> [ctx ~ body] => t ::: Type
              -> (t -> position -> xml (ctx ++ body) [] [])
diff -r 6966d98c80b5 -r 37dd42935dad demo/more/grid.ur
--- a/demo/more/grid.ur	Tue Sep 15 09:45:46 2009 -0400
+++ b/demo/more/grid.ur	Tue Sep 15 10:18:56 2009 -0400
@@ -32,11 +32,13 @@
 
                  con aggregates :: {Type}
                  val aggregates : $(map (aggregateMeta row) aggregates)
+                 val aggFolder : folder aggregates
              end) = struct
     style tabl
     style tr
     style th
     style td
+    style agg
 
     fun make (row : M.row) [t] (m : colMeta' M.row t) : transaction t = m.Project row
 
@@ -77,101 +79,118 @@
         <tr class={tr}>
           <th/> <th/>
           {foldRX2 [fst] [colMeta M.row] [_]
-                  (fn [nm :: Name] [p :: (Type * Type)] [rest :: {(Type * Type)}] [[nm] ~ rest]
-                                   data (meta : colMeta M.row p) =>
-                      <xml><th class={th}>{[(meta.Handlers data).Header]}</th></xml>)
-                  [_] M.folder grid.Cols M.cols}
-          </tr>
+                   (fn [nm :: Name] [p :: (Type * Type)] [rest :: {(Type * Type)}] [[nm] ~ rest]
+                                    data (meta : colMeta M.row p) =>
+                       <xml><th class={th}>{[(meta.Handlers data).Header]}</th></xml>)
+                   [_] M.folder grid.Cols M.cols}
+        </tr>
 
-          {Dlist.render (fn {Row = rowS, Cols = colsS, Updating = ud} pos =>
-                            let
-                                val delete =
-                                    Dlist.delete pos;
-                                    row <- get rowS;
-                                    rpc (M.delete (M.keyOf row))
+        {Dlist.render (fn {Row = rowS, Cols = colsS, Updating = ud} pos =>
+                          let
+                              val delete =
+                                  Dlist.delete pos;
+                                  row <- get rowS;
+                                  rpc (M.delete (M.keyOf row))
 
-                                val update = set ud True
+                              val update = set ud True
 
-                                val cancel =
-                                    set ud False;
-                                    row <- get rowS;
-                                    cols <- makeAll grid.Cols row;
-                                    set colsS cols
-                                    
-                                val save =
-                                    cols <- get colsS;
-                                    errors <- Monad.foldR3 [fst] [colMeta M.row] [snd] [fn _ => option string]
-                                                           (fn [nm :: Name] [p :: (Type * Type)] [rest :: {(Type * Type)}]
-                                                                            [[nm] ~ rest] data meta v errors =>
-                                                               b <- current ((meta.Handlers data).Validate v);
-                                                               return (if b then
-                                                                           errors
-                                                                       else
-                                                                           case errors of
-                                                                               None => Some ((meta.Handlers data).Header)
-                                                                             | Some s => Some ((meta.Handlers data).Header
-                                                                                               ^ ", " ^ s)))
-                                                           None [_] M.folder grid.Cols M.cols cols;
+                              val cancel =
+                                  set ud False;
+                                  row <- get rowS;
+                                  cols <- makeAll grid.Cols row;
+                                  set colsS cols
+                                  
+                              val save =
+                                  cols <- get colsS;
+                                  errors <- Monad.foldR3 [fst] [colMeta M.row] [snd] [fn _ => option string]
+                                                         (fn [nm :: Name] [p :: (Type * Type)] [rest :: {(Type * Type)}]
+                                                                          [[nm] ~ rest] data meta v errors =>
+                                                             b <- current ((meta.Handlers data).Validate v);
+                                                             return (if b then
+                                                                         errors
+                                                                     else
+                                                                         case errors of
+                                                                             None => Some ((meta.Handlers data).Header)
+                                                                           | Some s => Some ((meta.Handlers data).Header
+                                                                                             ^ ", " ^ s)))
+                                                         None [_] M.folder grid.Cols M.cols cols;
 
-                                    case errors of
-                                        Some s => alert ("Can't save because the following columns have invalid values:\n"
-                                                         ^ s)
-                                      | None =>
-                                        set ud False;
-                                        row <- get rowS;
-                                        row' <- Monad.foldR3 [fst] [colMeta M.row] [snd] [fn _ => M.row]
+                                  case errors of
+                                      Some s => alert ("Can't save because the following columns have invalid values:\n"
+                                                       ^ s)
+                                    | None =>
+                                      set ud False;
+                                      row <- get rowS;
+                                      row' <- Monad.foldR3 [fst] [colMeta M.row] [snd] [fn _ => M.row]
+                                                           (fn [nm :: Name] [t :: (Type * Type)]
+                                                                            [rest :: {(Type * Type)}]
+                                                                            [[nm] ~ rest] data meta v row' =>
+                                                               (meta.Handlers data).Update row' v)
+                                                           row [_] M.folder grid.Cols M.cols cols;
+                                      rpc (M.save (M.keyOf row) row');
+                                      set rowS row';
+
+                                      cols <- makeAll grid.Cols row';
+                                      set colsS cols
+                          in
+                              <xml><tr class={tr}>
+                                <td>
+                                  <dyn signal={b <- signal ud;
+                                               return (if b then
+                                                           <xml><button value="Save" onclick={save}/></xml>
+                                                       else
+                                                           <xml><button value="Update" onclick={update}/></xml>)}/>
+                                </td>
+
+                                <td><dyn signal={b <- signal ud;
+                                                 return (if b then
+                                                             <xml><button value="Cancel" onclick={cancel}/></xml>
+                                                         else
+                                                             <xml><button value="Delete" onclick={delete}/></xml>)}/>
+                                </td>
+
+                                <dyn signal={cols <- signal colsS;
+                                             return (foldRX3 [fst] [colMeta M.row] [snd] [_]
                                                              (fn [nm :: Name] [t :: (Type * Type)]
                                                                               [rest :: {(Type * Type)}]
-                                                                              [[nm] ~ rest] data meta v row' =>
-                                                                 (meta.Handlers data).Update row' v)
-                                                             row [_] M.folder grid.Cols M.cols cols;
-                                        rpc (M.save (M.keyOf row) row');
-                                        set rowS row';
+                                                                              [[nm] ~ rest] data meta v =>
+                                                                 <xml><td class={td}>
+                                                                   <dyn signal={b <- signal ud;
+                                                                                return (if b then
+                                                                                            (meta.Handlers data).Edit v
+                                                                                        else
+                                                                                            (meta.Handlers data).Display
+                                                                                                                v)}/>
+                                                                   <dyn signal={b <- signal ud;
+                                                                                if b then
+                                                                                    valid <-
+                                                                                    (meta.Handlers data).Validate v;
+                                                                                    return (if valid then
+                                                                                                <xml/>
+                                                                                            else
+                                                                                                <xml>!</xml>)
+                                                                                else
+                                                                                    return <xml/>}/>
+                                                                 </td></xml>)
+                                                             [_] M.folder grid.Cols M.cols cols)}/>
+                                </tr></xml>
+                          end) grid.Rows}
 
-                                        cols <- makeAll grid.Cols row';
-                                        set colsS cols
-                            in
-                                <xml><tr class={tr}>
-                                  <td>
-                                    <dyn signal={b <- signal ud;
-                                                 return (if b then
-                                                             <xml><button value="Save" onclick={save}/></xml>
-                                                         else
-                                                             <xml><button value="Update" onclick={update}/></xml>)}/>
-                                  </td>
-                                  <td><dyn signal={b <- signal ud;
-                                                   return (if b then
-                                                               <xml><button value="Cancel" onclick={cancel}/></xml>
-                                                           else
-                                                               <xml><button value="Delete" onclick={delete}/></xml>)}/>
-                                  </td>
-
-                                  <dyn signal={cols <- signal colsS;
-                                               return (foldRX3 [fst] [colMeta M.row] [snd] [_]
-                                                               (fn [nm :: Name] [t :: (Type * Type)]
-                                                                                [rest :: {(Type * Type)}]
-                                                                                [[nm] ~ rest] data meta v =>
-                                                                   <xml><td class={td}>
-                                                                     <dyn signal={b <- signal ud;
-                                                                                  return (if b then
-                                                                                              (meta.Handlers data).Edit v
-                                                                                          else
-                                                                                              (meta.Handlers data).Display
-                                                                                                                  v)}/>
-                                                                     <dyn signal={b <- signal ud;
-                                                                                  if b then
-                                                                                      valid <-
-                                                                                      (meta.Handlers data).Validate v;
-                                                                                      return (if valid then
-                                                                                                  <xml/>
-                                                                                              else
-                                                                                                  <xml>!</xml>)
-                                                                                  else
-                                                                                      return <xml/>}/>
-                                                                   </td></xml>)
-                                                               [_] M.folder grid.Cols M.cols cols)}/>
-                                  </tr></xml>
-                            end) grid.Rows}
+            <dyn signal={rows <- Dlist.foldl (fn row => Monad.mapR2 [aggregateMeta M.row] [id] [id]
+                                                                    (fn [nm :: Name] [t :: Type] meta acc =>
+                                                                        Monad.mp (fn v => meta.Step v acc)
+                                                                                 (signal row.Row))
+                                                                    [_] M.aggFolder M.aggregates)
+                                 (mp [aggregateMeta M.row] [id]
+                                  (fn [t] meta => meta.Initial)
+                                  [_] M.aggFolder M.aggregates) grid.Rows;
+                         return <xml><tr>
+                           <td/><td/>
+                           {foldRX2 [aggregateMeta M.row] [id] [_]
+                                    (fn [nm :: Name] [t :: Type] [rest :: {Type}] [[nm] ~ rest] meta acc =>
+                                        <xml><td class={agg}>{meta.Display acc}</td></xml>)
+                                    [_] M.aggFolder M.aggregates rows}
+                         </tr></xml>}/>
           </table>
           
           <button value="New row" onclick={row <- rpc M.new;
diff -r 6966d98c80b5 -r 37dd42935dad demo/more/grid.urs
--- a/demo/more/grid.urs	Tue Sep 15 09:45:46 2009 -0400
+++ b/demo/more/grid.urs	Tue Sep 15 10:18:56 2009 -0400
@@ -32,6 +32,7 @@
 
                  con aggregates :: {Type}
                  val aggregates : $(map (aggregateMeta row) aggregates)
+                 val aggFolder : folder aggregates
              end) : sig
     type grid
 
diff -r 6966d98c80b5 -r 37dd42935dad demo/more/grid1.ur
--- a/demo/more/grid1.ur	Tue Sep 15 09:45:46 2009 -0400
+++ b/demo/more/grid1.ur	Tue Sep 15 10:18:56 2009 -0400
@@ -45,7 +45,18 @@
                           DA = computed "2A" (fn r => 2 * r.A),
                           Link = computedHtml "Link" (fn r => <xml><a link={page (r.A, r.B)}>Go</a></xml>)}
 
-              val aggregates = {}
+              val aggregates = {Dummy1 = {Initial = (),
+                                          Step = fn _ _ => (),
+                                          Display = fn _ => <xml/>},
+                                Sum = {Initial = 0,
+                                       Step = fn r n => r.A + n,
+                                       Display = txt},
+                                Dummy2 = {Initial = (),
+                                          Step = fn _ _ => (),
+                                          Display = fn _ => <xml>-</xml>},
+                                And = {Initial = True,
+                                       Step = fn r b => r.C && b,
+                                       Display = txt}}
           end)
 
 fun main () =
diff -r 6966d98c80b5 -r 37dd42935dad demo/more/out/grid.css
--- a/demo/more/out/grid.css	Tue Sep 15 09:45:46 2009 -0400
+++ b/demo/more/out/grid.css	Tue Sep 15 10:18:56 2009 -0400
@@ -13,3 +13,7 @@
 .Grid1_td {
         border-style: solid
 }
+
+.Grid1_agg {
+        border-style: solid
+}
\ No newline at end of file
diff -r 6966d98c80b5 -r 37dd42935dad lib/ur/monad.ur
--- a/lib/ur/monad.ur	Tue Sep 15 09:45:46 2009 -0400
+++ b/lib/ur/monad.ur	Tue Sep 15 10:18:56 2009 -0400
@@ -59,3 +59,12 @@
         v' <- f [nm] [t] v;
         return (acc ++ {nm = v'}))
     {}
+
+fun mapR2 [K] [m] (_ : monad m) [tf1 :: K -> Type] [tf2 :: K -> Type] [tr :: K -> Type]
+         (f : nm :: Name -> t :: K -> tf1 t -> tf2 t -> m (tr t)) =
+    @@foldR2 [m] _ [tf1] [tf2] [fn r => $(map tr r)]
+    (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] (v1 : tf1 t) (v2 : tf2 t)
+                     (acc : $(map tr rest)) =>
+        v' <- f [nm] [t] v1 v2;
+        return (acc ++ {nm = v'}))
+    {}
diff -r 6966d98c80b5 -r 37dd42935dad lib/ur/monad.urs
--- a/lib/ur/monad.urs	Tue Sep 15 09:45:46 2009 -0400
+++ b/lib/ur/monad.urs	Tue Sep 15 10:18:56 2009 -0400
@@ -39,3 +39,9 @@
            -> tr :: (K -> Type)
            -> (nm :: Name -> t :: K -> tf t -> m (tr t))
            -> r :: {K} -> folder r -> $(map tf r) -> m ($(map tr r))
+
+val mapR2 : K --> m ::: (Type -> Type) -> monad m
+            -> tf1 :: (K -> Type) -> tf2 :: (K -> Type)
+            -> tr :: (K -> Type)
+            -> (nm :: Name -> t :: K -> tf1 t -> tf2 t -> m (tr t))
+            -> r :: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> m ($(map tr r))
diff -r 6966d98c80b5 -r 37dd42935dad lib/ur/top.ur
--- a/lib/ur/top.ur	Tue Sep 15 09:45:46 2009 -0400
+++ b/lib/ur/top.ur	Tue Sep 15 10:18:56 2009 -0400
@@ -105,6 +105,13 @@
         acc (r1 -- nm) (r2 -- nm) ++ {nm = f r1.nm r2.nm})
     (fn _ _ => {})
 
+fun map3 [K] [tf1 :: K -> Type] [tf2 :: K -> Type] [tf3 :: K -> Type] [tf :: K -> Type]
+         (f : t ::: K -> tf1 t -> tf2 t -> tf3 t -> tf t) [r :: {K}] (fl : folder r) =
+    fl [fn r :: {K} => $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> $(map tf r)]
+    (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] acc r1 r2 r3 =>
+        acc (r1 -- nm) (r2 -- nm) (r3 -- nm) ++ {nm = f r1.nm r2.nm r3.nm})
+    (fn _ _ _ => {})
+
 fun foldUR [tf :: Type] [tr :: {Unit} -> Type]
            (f : nm :: Name -> rest :: {Unit}
                 -> [[nm] ~ rest] =>
diff -r 6966d98c80b5 -r 37dd42935dad lib/ur/top.urs
--- a/lib/ur/top.urs	Tue Sep 15 09:45:46 2009 -0400
+++ b/lib/ur/top.urs	Tue Sep 15 10:18:56 2009 -0400
@@ -48,9 +48,12 @@
 val mp : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type)
          -> (t ::: K -> tf1 t -> tf2 t)
          -> r :: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r)
-val map2 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> tf3 :: (K -> Type)
-           -> (t ::: K -> tf1 t -> tf2 t -> tf3 t)
-           -> r :: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r)
+val map2 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> tf :: (K -> Type)
+           -> (t ::: K -> tf1 t -> tf2 t -> tf t)
+           -> r :: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> $(map tf r)
+val map3 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> tf3 :: (K -> Type) -> tf :: (K -> Type)
+           -> (t ::: K -> tf1 t -> tf2 t -> tf3 t -> tf t)
+           -> r :: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> $(map tf r)
 
 val foldUR : tf :: Type -> tr :: ({Unit} -> Type)
              -> (nm :: Name -> rest :: {Unit}