summaryrefslogtreecommitdiff
path: root/demo/more/dlist.ur
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2009-09-15 10:18:56 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2009-09-15 10:18:56 -0400
commit62c16c0eed4b755ffcc4379455971a4c0125a3a8 (patch)
treeb81fba316b6a552d9b1cf527831175d0926da43f /demo/more/dlist.ur
parent93594385adcba919b2e61785b5a60779e2be20db (diff)
Summary row with aggregates
Diffstat (limited to 'demo/more/dlist.ur')
-rw-r--r--demo/more/dlist.ur19
1 files changed, 19 insertions, 0 deletions
diff --git a/demo/more/dlist.ur b/demo/more/dlist.ur
index f8aca1e2..850836b0 100644
--- a/demo/more/dlist.ur
+++ b/demo/more/dlist.ur
@@ -86,3 +86,22 @@ fun elements [t] (dl : dlist t) =
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