comparison 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
comparison
equal deleted inserted replaced
936:6966d98c80b5 937:37dd42935dad
84 fun elements [t] (dl : dlist t) = 84 fun elements [t] (dl : dlist t) =
85 dl' <- signal dl; 85 dl' <- signal dl;
86 case dl' of 86 case dl' of
87 Empty => return [] 87 Empty => return []
88 | Nonempty {Head = hd, ...} => elements' hd 88 | Nonempty {Head = hd, ...} => elements' hd
89
90 fun foldl [t] [acc] (f : t -> acc -> signal acc) =
91 let
92 fun foldl'' (i : acc) (dl : dlist'' t) : signal acc =
93 case dl of
94 Nil => return i
95 | Cons (v, dl') =>
96 dl' <- signal dl';
97 i' <- f v i;
98 foldl'' i' dl'
99
100 fun foldl' (i : acc) (dl : dlist t) : signal acc =
101 dl <- signal dl;
102 case dl of
103 Empty => return i
104 | Nonempty {Head = dl, ...} => foldl'' i dl
105 in
106 foldl'
107 end