git.iko.soy/Idris-dev
on master help sign in
Add more folds and a Foldable instance for (Vect n)
d4f173dMelvar Chen
lib/Prelude/Foldable.idr+13−4
compare with master
unifiedsplit
@@ -15,15 +15,24 @@ foldl f z t = foldr (flip (.) . flip f) id t z
15concat : (Foldable t, Monoid a) => t a -> a
15concat : (Foldable t, Monoid a) => t a -> a
16concat = foldr (<+>) neutral
16concat = foldr (<+>) neutral
17
17
18+concatMap : (Foldable t, Monoid m) => (a -> m) -> t a -> m
19+concatMap f = foldr ((<+>) . f) neutral
20+
18and : Foldable t => t Bool -> Bool
21and : Foldable t => t Bool -> Bool
19and = foldr (&&) True
22and = foldr (&&) True
20
23
21or : Foldable t => t Bool -> Bool
24or : Foldable t => t Bool -> Bool
22or = foldr (||) False
25or = foldr (||) False
23
26
27+any : Foldable t => (a -> Bool) -> t a -> Bool
28+any p = foldr ((||) . p) False
29+
30+all : Foldable t => (a -> Bool) -> t a -> Bool
31+all p = foldr ((&&) . p) True
32+
24−any : (Foldable t, Functor t) => (a -> Bool) -> t a -> Bool
33+sum : (Foldable t, Num a) => t a -> a
25−any p = Foldable.or . fmap p
34+sum = foldr (+) 0
26
35
27−all : (Foldable t, Functor t) => (a -> Bool) -> t a -> Bool
36+product : (Foldable t, Num a) => t a -> a
28−all p = Foldable.and . fmap p
37+product = foldr (*) 1
29
38
lib/Prelude/List.idr−4
@@ -226,10 +226,6 @@ instance Foldable List where
226-- Special folds
226-- Special folds
227--------------------------------------------------------------------------------
227--------------------------------------------------------------------------------
228
228
229−concatMap : (a -> List b) -> List a -> List b
230−concatMap f [] = []
231−concatMap f (x::xs) = f x ++ concatMap f xs
232−
233--------------------------------------------------------------------------------
229--------------------------------------------------------------------------------
234-- Transformations
230-- Transformations
235--------------------------------------------------------------------------------
231--------------------------------------------------------------------------------
lib/Prelude/Vect.idr+5−24
@@ -1,6 +1,7 @@
1module Prelude.Vect
1module Prelude.Vect
2
2
3import Prelude.Fin
3import Prelude.Fin
4+import Prelude.Foldable
4import Prelude.Functor
5import Prelude.Functor
5import Prelude.List
6import Prelude.List
6import Prelude.Nat
7import Prelude.Nat
@@ -62,13 +63,9 @@ drop (fS k) [] impossible
62drop (fS k) (x::xs) = drop k xs
63drop (fS k) (x::xs) = drop k xs
63
64
64--------------------------------------------------------------------------------
65--------------------------------------------------------------------------------
65−-- Conversions to and from list
66+-- Conversion from list (toList is provided by Foldable)
66--------------------------------------------------------------------------------
67--------------------------------------------------------------------------------
67
68
68−toList : Vect n a -> List a
69−toList [] = []
70−toList (x::xs) = x :: toList xs
71−
72fromList : (l : List a) -> Vect (length l) a
69fromList : (l : List a) -> Vect (length l) a
73fromList [] = []
70fromList [] = []
74fromList (x::xs) = x :: fromList xs
71fromList (x::xs) = x :: fromList xs
@@ -123,13 +120,9 @@ instance Functor (Vect n) where
123-- Folds
120-- Folds
124--------------------------------------------------------------------------------
121--------------------------------------------------------------------------------
125
122
126−total foldl : (a -> b -> a) -> a -> Vect m b -> a
123+instance Foldable (Vect n) where
127−foldl f e [] = e
128−foldl f e (x::xs) = foldl f (f e x) xs
129−
130−total foldr : (a -> b -> b) -> b -> Vect m a -> b
131−foldr f e [] = e
124+ foldr f e [] = e
132−foldr f e (x::xs) = f x (foldr f e xs)
125+ foldr f e (x::xs) = f x (foldr f e xs)
133
126
134--------------------------------------------------------------------------------
127--------------------------------------------------------------------------------
135-- Special folds
128-- Special folds
@@ -139,18 +132,6 @@ concat : Vect m (Vect n a) -> Vect (m * n) a
139concat [] = []
132concat [] = []
140concat (v::vs) = v ++ concat vs
133concat (v::vs) = v ++ concat vs
141
134
142−total and : Vect m Bool -> Bool
143−and = foldr (&&) True
144−
145−total or : Vect m Bool -> Bool
146−or = foldr (||) False
147−
148−total any : (a -> Bool) -> Vect m a -> Bool
149−any p = Vect.or . map p
150−
151−total all : (a -> Bool) -> Vect m a -> Bool
152−all p = Vect.and . map p
153−
154--------------------------------------------------------------------------------
135--------------------------------------------------------------------------------
155-- Transformations
136-- Transformations
156--------------------------------------------------------------------------------
137--------------------------------------------------------------------------------
lib/base.ipkg+1−1
@@ -6,7 +6,7 @@ modules = Builtins, Prelude, IO, System,
6 Prelude.Algebra, Prelude.Cast, Prelude.Nat, Prelude.Fin,
6 Prelude.Algebra, Prelude.Cast, Prelude.Nat, Prelude.Fin,
7 Prelude.List, Prelude.Maybe, Prelude.Monad, Prelude.Applicative,
7 Prelude.List, Prelude.Maybe, Prelude.Monad, Prelude.Applicative,
8 Prelude.Either, Prelude.Vect, Prelude.Strings, Prelude.Chars,
8 Prelude.Either, Prelude.Vect, Prelude.Strings, Prelude.Chars,
9− Prelude.Heap, Prelude.Complex, Prelude.Functor,
9+ Prelude.Heap, Prelude.Complex, Prelude.Functor, Prelude.Foldable,
10
10
11 Network.Cgi,
11 Network.Cgi,
12 Debug.Trace,
12 Debug.Trace,