02f8b53 · Idris-dev · git.iko.soy

lib/Language/Reflection.idr+21−11

compare with master

unifiedsplit

@@ -98,17 +98,27 @@ instance Functor Binder where

98 map f (PVar x) = PVar (f x)

99 map f (PVTy x) = PVTy (f x)

100

101−total

101+instance Foldable Binder where

102−traverse : (Applicative f) => (a -> f b) -> Binder a -> f (Binder b)

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

103−traverse f (Lam x) = [| Lam (f x) |]

113+ traverse f (Lam x) = [| Lam (f x) |]

104−traverse f (Pi x) = [| Pi (f x) |]

114+ traverse f (Pi x) = [| Pi (f x) |]

105−traverse f (Let x y) = [| Let (f x) (f y) |]

115+ traverse f (Let x y) = [| Let (f x) (f y) |]

106−traverse f (NLet x y) = [| NLet (f x) (f y) |]

116+ traverse f (NLet x y) = [| NLet (f x) (f y) |]

107−traverse f (Hole x) = [| Hole (f x) |]

117+ traverse f (Hole x) = [| Hole (f x) |]

108−traverse f (GHole x) = [| GHole (f x) |]

118+ traverse f (GHole x) = [| GHole (f x) |]

109−traverse f (Guess x y) = [| Guess (f x) (f y) |]

119+ traverse f (Guess x y) = [| Guess (f x) (f y) |]

110−traverse f (PVar x) = [| PVar (f x) |]

120+ traverse f (PVar x) = [| PVar (f x) |]

111−traverse f (PVTy x) = [| PVTy (f x) |]

121+ traverse f (PVTy x) = [| PVTy (f x) |]

112

122

113

123

114-- | Reflection of the well typed core language

124-- | Reflection of the well typed core language

lib/Prelude.idr+15

@@ -15,6 +15,7 @@ import Prelude.Either

15import Prelude.Vect

16import Prelude.Strings

17import Prelude.Chars

18+import Prelude.Traversable

18

19

19%access public

20%access public

20%default total

21%default total

@@ -253,6 +254,20 @@ instance Monad List where

253instance Monad (Vect n) where

254instance Monad (Vect n) where

254 m >>= f = diag (map f m)

255 m >>= f = diag (map f m)

255

256

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+

256---- some mathematical operations

271---- some mathematical operations

257

272

258%include C "math.h"

273%include C "math.h"

lib/Prelude/Applicative.idr−15

@@ -29,18 +29,3 @@ guard a = if a then pure () else empty

29

30when : Applicative f => Bool -> f () -> f ()

31when 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

106 where

107 %assert_total -- relies on deleteMinimum making heap smaller

108 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))

110

111fromList : Ord a => List a -> MaxiphobicHeap a

112fromList = foldr insert empty

lib/Prelude/List.idr+6−29

@@ -3,6 +3,7 @@ module Prelude.List

3import Builtins

4

5import Prelude.Algebra

6+import Prelude.Foldable

6import Prelude.Functor

7import Prelude.Functor

7import Prelude.Maybe

8import Prelude.Maybe

8import Prelude.Nat

9import Prelude.Nat

@@ -217,40 +218,16 @@ mapMaybe f (x::xs) =

217-- Folds

218-- Folds

218--------------------------------------------------------------------------------

219--------------------------------------------------------------------------------

219

220

220−foldl : (a -> b -> a) -> a -> List b -> a

221+instance Foldable List where

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

222+ foldr f e [] = e

225−foldr f e [] = e

226−foldr f e (x::xs) = f x (foldr f e xs)

223+ foldr f e (x::xs) = f x (foldr f e xs)

227

224

228--------------------------------------------------------------------------------

225--------------------------------------------------------------------------------

229-- Special folds

226-- Special folds

230--------------------------------------------------------------------------------

227--------------------------------------------------------------------------------

231

228

232−mconcat : Monoid a => List a -> a

229+toList : Foldable t => t a -> List a

233−mconcat = foldr (<+>) neutral

230+toList = foldr (::) []

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

254

231

255--------------------------------------------------------------------------------

232--------------------------------------------------------------------------------

256-- Transformations

233-- Transformations

lib/Prelude/Maybe.idr+5

@@ -3,6 +3,7 @@ module Prelude.Maybe

3import Builtins

4import Prelude.Algebra

5import Prelude.Cast

6+import Prelude.Foldable

6

7

7%access public

8%access public

8%default total

9%default total

@@ -81,3 +82,7 @@ instance (Monoid a, Eq a) => Cast a (Maybe a) where

81

82

82instance (Monoid a) => Cast (Maybe a) a where

83instance (Monoid a) => Cast (Maybe a) a where

83 cast = lowerMaybe

84 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 @@

1module Prelude.Vect

2

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+2−1

@@ -6,7 +6,8 @@ modules = Builtins, Prelude, IO, System,

6 Prelude.Algebra, Prelude.Cast, Prelude.Nat, Prelude.Fin,

7 Prelude.List, Prelude.Maybe, Prelude.Monad, Prelude.Applicative,

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+ Prelude.Traversable,

10

11

11 Network.Cgi,

12 Network.Cgi,

12 Debug.Trace,

13 Debug.Trace,