diff demo/more/dlist.ur @ 937:37dd42935dad

Summary row with aggregates
author Adam Chlipala <adamc@hcoop.net>
date Tue, 15 Sep 2009 10:18:56 -0400
parents 5e8b6fa5b48f
children da3ec6014d2f
line wrap: on
line diff
--- 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