git.iko.soy/Idris-dev
on master help sign in
Merge branch 'master' of github.com:edwinb/Idris-dev
commit02f8b53411cf37b9be3539ab06dd26bfbf533e3f authorEdwin Brady <ecb10@st-andrews.ac.uk> dateMon 5 Aug 2013, 15:57 (13 years ago) parentecc30827506102
10 files changed+109−81
compare with master
unifiedsplit
lib/Language/Reflection.idr+21−11 lib/Prelude.idr+15 lib/Prelude/Applicative.idr−15 lib/Prelude/Foldable.idr+38 lib/Prelude/Heap.idr+1−1 lib/Prelude/List.idr+6−29 lib/Prelude/Maybe.idr+5 lib/Prelude/Traversable.idr+16 lib/Prelude/Vect.idr+5−24 lib/base.ipkg+2−1
lib/Language/Reflection.idr+21−11
@@ -98,17 +98,27 @@ instance Functor Binder where
9898 map f (PVar x) = PVar (f x)
9999 map f (PVTy x) = PVTy (f x)
100100
101−total
102−traverse : (Applicative f) => (a -> f b) -> Binder a -> f (Binder b)
103−traverse f (Lam x) = [| Lam (f x) |]
104−traverse f (Pi x) = [| Pi (f x) |]
105−traverse f (Let x y) = [| Let (f x) (f y) |]
106−traverse f (NLet x y) = [| NLet (f x) (f y) |]
107−traverse f (Hole x) = [| Hole (f x) |]
108−traverse f (GHole x) = [| GHole (f x) |]
109−traverse f (Guess x y) = [| Guess (f x) (f y) |]
110−traverse f (PVar x) = [| PVar (f x) |]
111−traverse f (PVTy x) = [| PVTy (f x) |]
101+instance Foldable Binder where
102+ foldr f z (Lam x) = f x z
103+ foldr f z (Pi x) = f x z
104+ foldr f z (Let x y) = f x (f y z)
105+ foldr f z (NLet x y) = f x (f y z)
106+ foldr f z (Hole x) = f x z
107+ foldr f z (GHole x) = f x z
108+ foldr f z (Guess x y) = f x (f y z)
109+ foldr f z (PVar x) = f x z
110+ foldr f z (PVTy x) = f x z
111+
112+instance Traversable Binder where
113+ traverse f (Lam x) = [| Lam (f x) |]
114+ traverse f (Pi x) = [| Pi (f x) |]
115+ traverse f (Let x y) = [| Let (f x) (f y) |]
116+ traverse f (NLet x y) = [| NLet (f x) (f y) |]
117+ traverse f (Hole x) = [| Hole (f x) |]
118+ traverse f (GHole x) = [| GHole (f x) |]
119+ traverse f (Guess x y) = [| Guess (f x) (f y) |]
120+ traverse f (PVar x) = [| PVar (f x) |]
121+ traverse f (PVTy x) = [| PVTy (f x) |]
112122
113123
114124-- | Reflection of the well typed core language
lib/Prelude.idr+15
@@ -15,6 +15,7 @@ import Prelude.Either
1515import Prelude.Vect
1616import Prelude.Strings
1717import Prelude.Chars
18+import Prelude.Traversable
1819
1920%access public
2021%default total
@@ -253,6 +254,20 @@ instance Monad List where
253254instance Monad (Vect n) where
254255 m >>= f = diag (map f m)
255256
257+---- Traversable instances
258+
259+instance Traversable Maybe where
260+ traverse f Nothing = pure Nothing
261+ traverse f (Just x) = [| Just (f x) |]
262+
263+instance Traversable List where
264+ traverse f [] = pure List.Nil
265+ traverse f (x::xs) = [| List.(::) (f x) (traverse f xs) |]
266+
267+instance Traversable (Vect n) where
268+ traverse f [] = pure Vect.Nil
269+ traverse f (x::xs) = [| Vect.(::) (f x) (traverse f xs) |]
270+
256271---- some mathematical operations
257272
258273%include C "math.h"
lib/Prelude/Applicative.idr−15
@@ -29,18 +29,3 @@ guard a = if a then pure () else empty
2929
3030when : Applicative f => Bool -> f () -> f ()
3131when a f = if a then f else pure ()
32−
33−sequence : Applicative f => List (f a) -> f (List a)
34−sequence [] = pure []
35−sequence (x :: xs) = map (::) x <$> sequence xs
36−
37−sequence_ : Applicative f => List (f a) -> f ()
38−sequence_ [] = pure ()
39−sequence_ (x :: xs) = x $> sequence_ xs
40−
41−traverse : Applicative f => (a -> f b) -> List a -> f (List b)
42−traverse f xs = sequence (map f xs)
43−
44−traverse_ : Applicative f => (a -> f b) -> List a -> f ()
45−traverse_ f (x :: xs) = f x $> traverse_ f xs
46−traverse_ f [] = pure ()
lib/Prelude/Foldable.idrnew file+38
@@ -0,0 +1,38 @@
1+module Prelude.Foldable
2+
3+import Builtins
4+import Prelude.Algebra
5+
6+%access public
7+%default total
8+
9+class Foldable (t : Type -> Type) where
10+ foldr : (elt -> acc -> acc) -> acc -> t elt -> acc
11+
12+foldl : Foldable t => (acc -> elt -> acc) -> acc -> t elt -> acc
13+foldl f z t = foldr (flip (.) . flip f) id t z
14+
15+concat : (Foldable t, Monoid a) => t a -> a
16+concat = foldr (<+>) neutral
17+
18+concatMap : (Foldable t, Monoid m) => (a -> m) -> t a -> m
19+concatMap f = foldr ((<+>) . f) neutral
20+
21+and : Foldable t => t Bool -> Bool
22+and = foldr (&&) True
23+
24+or : Foldable t => t Bool -> Bool
25+or = foldr (||) False
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+
33+sum : (Foldable t, Num a) => t a -> a
34+sum = foldr (+) 0
35+
36+product : (Foldable t, Num a) => t a -> a
37+product = foldr (*) 1
38+
lib/Prelude/Heap.idr+1−1
@@ -106,7 +106,7 @@ toList (Node s l e r) = toList' (Node s l e r) refl
106106 where
107107 %assert_total -- relies on deleteMinimum making heap smaller
108108 toList' : Ord a => (h : MaxiphobicHeap a) -> (isEmpty h = False) -> List a
109− toList' heap p = findMinimum heap p :: (toList (deleteMinimum heap p))
109+ toList' heap p = findMinimum heap p :: (Heap.toList (deleteMinimum heap p))
110110
111111fromList : Ord a => List a -> MaxiphobicHeap a
112112fromList = foldr insert empty
lib/Prelude/List.idr+6−29
@@ -3,6 +3,7 @@ module Prelude.List
33import Builtins
44
55import Prelude.Algebra
6+import Prelude.Foldable
67import Prelude.Functor
78import Prelude.Maybe
89import Prelude.Nat
@@ -217,40 +218,16 @@ mapMaybe f (x::xs) =
217218-- Folds
218219--------------------------------------------------------------------------------
219220
220−foldl : (a -> b -> a) -> a -> List b -> a
221−foldl f e [] = e
222−foldl f e (x::xs) = foldl f (f e x) xs
223−
224−foldr : (a -> b -> b) -> b -> List a -> b
225−foldr f e [] = e
226−foldr f e (x::xs) = f x (foldr f e xs)
221+instance Foldable List where
222+ foldr f e [] = e
223+ foldr f e (x::xs) = f x (foldr f e xs)
227224
228225--------------------------------------------------------------------------------
229226-- Special folds
230227--------------------------------------------------------------------------------
231228
232−mconcat : Monoid a => List a -> a
233−mconcat = foldr (<+>) neutral
234−
235−concat : List (List a) -> List a
236−concat [] = []
237−concat (x::xs) = x ++ concat xs
238−
239−concatMap : (a -> List b) -> List a -> List b
240−concatMap f [] = []
241−concatMap f (x::xs) = f x ++ concatMap f xs
242−
243−and : List Bool -> Bool
244−and = foldr (&&) True
245−
246−or : List Bool -> Bool
247−or = foldr (||) False
248−
249−any : (a -> Bool) -> List a -> Bool
250−any p = or . map p
251−
252−all : (a -> Bool) -> List a -> Bool
253−all p = and . map p
229+toList : Foldable t => t a -> List a
230+toList = foldr (::) []
254231
255232--------------------------------------------------------------------------------
256233-- Transformations
lib/Prelude/Maybe.idr+5
@@ -3,6 +3,7 @@ module Prelude.Maybe
33import Builtins
44import Prelude.Algebra
55import Prelude.Cast
6+import Prelude.Foldable
67
78%access public
89%default total
@@ -81,3 +82,7 @@ instance (Monoid a, Eq a) => Cast a (Maybe a) where
8182
8283instance (Monoid a) => Cast (Maybe a) a where
8384 cast = lowerMaybe
85+
86+instance Foldable Maybe where
87+ foldr _ z Nothing = z
88+ foldr f z (Just x) = f x z
lib/Prelude/Traversable.idrnew file+16
@@ -0,0 +1,16 @@
1+module Prelude.Traversable
2+
3+import Prelude.Applicative
4+import Prelude.Foldable
5+
6+traverse_ : (Foldable t, Applicative f) => (a -> f b) -> t a -> f ()
7+traverse_ f = foldr (($>) . f) (pure ())
8+
9+sequence_ : (Foldable t, Applicative f) => t (f a) -> f ()
10+sequence_ = foldr ($>) (pure ())
11+
12+class (Functor t, Foldable t) => Traversable (t : Type -> Type) where
13+ traverse : Applicative f => (a -> f b) -> t a -> f (t b)
14+
15+sequence : (Traversable t, Applicative f) => t (f a) -> f (t a)
16+sequence = traverse id
lib/Prelude/Vect.idr+5−24
@@ -1,6 +1,7 @@
11module Prelude.Vect
22
33import Prelude.Fin
4+import Prelude.Foldable
45import Prelude.Functor
56import Prelude.List
67import Prelude.Nat
@@ -62,13 +63,9 @@ drop (fS k) [] impossible
6263drop (fS k) (x::xs) = drop k xs
6364
6465--------------------------------------------------------------------------------
65−-- Conversions to and from list
66+-- Conversion from list (toList is provided by Foldable)
6667--------------------------------------------------------------------------------
6768
68−toList : Vect n a -> List a
69−toList [] = []
70−toList (x::xs) = x :: toList xs
71−
7269fromList : (l : List a) -> Vect (length l) a
7370fromList [] = []
7471fromList (x::xs) = x :: fromList xs
@@ -123,13 +120,9 @@ instance Functor (Vect n) where
123120-- Folds
124121--------------------------------------------------------------------------------
125122
126−total foldl : (a -> b -> a) -> a -> Vect m b -> a
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
132−foldr f e (x::xs) = f x (foldr f e xs)
123+instance Foldable (Vect n) where
124+ foldr f e [] = e
125+ foldr f e (x::xs) = f x (foldr f e xs)
133126
134127--------------------------------------------------------------------------------
135128-- Special folds
@@ -139,18 +132,6 @@ concat : Vect m (Vect n a) -> Vect (m * n) a
139132concat [] = []
140133concat (v::vs) = v ++ concat vs
141134
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−
154135--------------------------------------------------------------------------------
155136-- Transformations
156137--------------------------------------------------------------------------------
lib/base.ipkg+2−1
@@ -6,7 +6,8 @@ modules = Builtins, Prelude, IO, System,
66 Prelude.Algebra, Prelude.Cast, Prelude.Nat, Prelude.Fin,
77 Prelude.List, Prelude.Maybe, Prelude.Monad, Prelude.Applicative,
88 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+ Prelude.Traversable,
1011
1112 Network.Cgi,
1213 Debug.Trace,