7105d79 · Idris-dev · git.iko.soy

contribs/lib/SQLite3/Sqlite3.idr+3−3

compare with master

unifiedsplit

@@ -41,8 +41,8 @@ forM xs f = (sequence (map f xs))

41data DB a = MkDB (IO (Either String a))

42

43instance Functor DB where

44− fmap f (MkDB action) = MkDB (do res <- action

44+ map f (MkDB action) = MkDB (do res <- action

45− return (fmap f res))

45+ return (map f res))

46

47

48instance Applicative DB where

@@ -50,7 +50,7 @@ instance Applicative DB where

50 (MkDB f) <$> (MkDB x) = MkDB (do f' <- f

51 case f' of

52 Left err => return (Left err)

53− Right op => x >>= (return . fmap op))

53+ Right op => x >>= (return . map op))

54

55

56instance Monad DB where

contribs/lib/SimpleParser/SimpleParser.idr+6−6

@@ -24,7 +24,7 @@ parse : Parser a -> String -> Either String (a, String)

24parse (P p) inp = p inp

25

26instance Functor Parser where

27− fmap f p = P (\inp => case parse p inp of

27+ map f p = P (\inp => case parse p inp of

28 Left err => Left err

29 Right (v, rest) => Right ((f v), rest))

30

@@ -90,7 +90,7 @@ char : Char -> Parser Char

90char x = sat (== x)

91

92string : String -> Parser String

93−string s = fmap pack (traverse char (unpack s))

93+string s = map pack (traverse char (unpack s))

94

95many1 : Parser a -> Parser (List a)

96many : Parser a -> Parser (List a)

@@ -110,7 +110,7 @@ bool = parseTrue <|> parseFalse

110 pure False

111

112ident : Parser String

113−ident = fmap pack [| letter :: many1 alphanum |]

113+ident = map pack [| letter :: many1 alphanum |]

114

115nat : Parser Int

116nat = do xs <- many digit

@@ -148,7 +148,7 @@ symbol : String -> Parser String

148symbol xs = token (string xs)

149

150strToken : Parser String

151−strToken = fmap pack (token (many1 alphanum))

151+strToken = map pack (token (many1 alphanum))

152

153

154--------------------------------------------------------------------------------

@@ -160,12 +160,12 @@ factor : Parser Int

160term : Parser Int

161

162expr = do t <- term

163− fmap (t+) (symbol "+" $> expr) <|> pure t

163+ map (t+) (symbol "+" $> expr) <|> pure t

164

165factor = (symbol "(" $> expr <$ symbol ")") <|> natural

166

167term = do f <- factor

168− fmap (f*) (symbol "*" $> term) <|> pure f

168+ map (f*) (symbol "*" $> term) <|> pure f

169

170eval : String -> Maybe Int

171eval xs = case (parse expr xs) of

lib/Control/IOExcept.idr+1−1

@@ -8,7 +8,7 @@ data IOExcept : Type -> Type -> Type where

8 ioM : IO (Either err a) -> IOExcept err a

9

10instance Functor (IOExcept e) where

11− fmap f (ioM fn) = ioM (fmap (fmap f) fn)

11+ map f (ioM fn) = ioM (map (map f) fn)

12

13instance Applicative (IOExcept e) where

14 pure x = ioM (pure (pure x))

lib/Control/Monad/Identity.idr+1−1

@@ -8,7 +8,7 @@ public record Identity : Type -> Type where

8 Id : (runIdentity : a) -> Identity a

9

10instance Functor Identity where

11− fmap fn (Id a) = Id (fn a)

11+ map fn (Id a) = Id (fn a)

12

13instance Applicative Identity where

14 pure x = Id x

lib/Control/Monad/State.idr+1−1

@@ -15,7 +15,7 @@ record StateT : Type -> (Type -> Type) -> Type -> Type where

15 (runStateT : s -> m (a, s)) -> StateT s m a

16

17instance Functor f => Functor (StateT s f) where

18− fmap f (ST g) = ST (\st => fmap (mapFst f) (g st)) where

18+ map f (ST g) = ST (\st => map (mapFst f) (g st)) where

19 mapFst : (a -> x) -> (a, b) -> (x, b)

20 mapFst fn (a, b) = (fn a, b)

21

lib/Data/Morphisms.idr+1−1

@@ -23,7 +23,7 @@ applyEndo : Endomorphism a -> a -> a

23applyEndo (Endo f) a = f a

24

25instance Functor (Morphism r) where

26− fmap f (Mor a) = Mor (f . a)

26+ map f (Mor a) = Mor (f . a)

27

28instance Applicative (Morphism r) where

29 pure a = Mor $ const a

lib/Data/SortedMap.idr+5−5

@@ -226,10 +226,10 @@ toList Empty = []

226toList (M _ t) = treeToList t

227

228instance Functor (Tree n k) where

229− fmap f (Leaf k v) = Leaf k (f v)

229+ map f (Leaf k v) = Leaf k (f v)

230− fmap f (Branch2 t1 k t2) = Branch2 (fmap f t1) k (fmap f t2)

230+ map f (Branch2 t1 k t2) = Branch2 (map f t1) k (map f t2)

231− fmap f (Branch3 t1 k1 t2 k2 t3) = Branch3 (fmap f t1) k1 (fmap f t2) k2 (fmap f t3)

231+ map f (Branch3 t1 k1 t2 k2 t3) = Branch3 (map f t1) k1 (map f t2) k2 (map f t3)

232

233instance Functor (SortedMap k) where

234− fmap _ Empty = Empty

234+ map _ Empty = Empty

235− fmap f (M n t) = M _ (fmap f t)

235+ map f (M n t) = M _ (map f t)

lib/Language/Reflection.idr+9−9

@@ -88,15 +88,15 @@ data Binder a = Lam a

88

89

90instance Functor Binder where

91− fmap f (Lam x) = Lam (f x)

91+ map f (Lam x) = Lam (f x)

92− fmap f (Pi x) = Pi (f x)

92+ map f (Pi x) = Pi (f x)

93− fmap f (Let x y) = Let (f x) (f y)

93+ map f (Let x y) = Let (f x) (f y)

94− fmap f (NLet x y) = NLet (f x) (f y)

94+ map f (NLet x y) = NLet (f x) (f y)

95− fmap f (Hole x) = Hole (f x)

95+ map f (Hole x) = Hole (f x)

96− fmap f (GHole x) = GHole (f x)

96+ map f (GHole x) = GHole (f x)

97− fmap f (Guess x y) = Guess (f x) (f y)

97+ map f (Guess x y) = Guess (f x) (f y)

98− fmap f (PVar x) = PVar (f x)

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

99− fmap f (PVTy x) = PVTy (f x)

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

100

101total

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

lib/Network/Cgi.idr+2−2

@@ -28,8 +28,8 @@ getAction : CGI a -> CGIInfo -> IO (a, CGIInfo)

28getAction (MkCGI act) = act

29

30instance Functor CGI where

31− fmap f (MkCGI c) = MkCGI (\s => do (a, i) <- c s

31+ map f (MkCGI c) = MkCGI (\s => do (a, i) <- c s

32− return (f a, i))

32+ return (f a, i))

33

34instance Applicative CGI where

35 pure v = MkCGI (\s => return (v, s))

lib/Prelude.idr+6−9

@@ -181,18 +181,15 @@ instance Show a => Show (Maybe a) where

181---- Functor instances

182

183instance Functor IO where

184− fmap f io = io_bind io (io_return . f)

184+ map f io = io_bind io (io_return . f)

185

186instance Functor Maybe where

187− fmap f (Just x) = Just (f x)

187+ map f (Just x) = Just (f x)

188− fmap f Nothing = Nothing

188+ map f Nothing = Nothing

189

190instance Functor (Either e) where

191− fmap f (Left l) = Left l

191+ map f (Left l) = Left l

192− fmap f (Right r) = Right (f r)

192+ map f (Right r) = Right (f r)

193−

194−instance Functor List where

195− fmap = map

196

193

197---- Applicative instances

194---- Applicative instances

198

195

@@ -376,7 +373,7 @@ putChar c = mkForeign (FFun "putchar" [FInt] FUnit) (cast c)

376

373

377partial

374partial

378getChar : IO Char

375getChar : IO Char

379−getChar = fmap cast $ mkForeign (FFun "getchar" [] FInt)

376+getChar = map cast $ mkForeign (FFun "getchar" [] FInt)

380

377

381---- some basic file handling

378---- some basic file handling

382

379

lib/Prelude/Applicative.idr+3−3

@@ -13,11 +13,11 @@ class Functor f => Applicative (f : Type -> Type) where

13

14infixl 2 <$

15(<$) : Applicative f => f a -> f b -> f a

16−a <$ b = fmap const a <$> b

16+a <$ b = map const a <$> b

17

18infixl 2 $>

19($>) : Applicative f => f a -> f b -> f b

20−a $> b = fmap (const id) a <$> b

20+a $> b = map (const id) a <$> b

21

22infixl 3 <|>

23class Applicative f => Alternative (f : Type -> Type) where

@@ -32,7 +32,7 @@ when a f = if a then f else pure ()

32

33sequence : Applicative f => List (f a) -> f (List a)

34sequence [] = pure []

35−sequence (x :: xs) = fmap (::) x <$> sequence xs

35+sequence (x :: xs) = map (::) x <$> sequence xs

36

37sequence_ : Applicative f => List (f a) -> f ()

38sequence_ [] = pure ()

lib/Prelude/Functor.idr+1−1

@@ -1,4 +1,4 @@

1module Prelude.Functor

2

3class Functor (f : Type -> Type) where

4− fmap : (a -> b) -> f a -> f b

4+ map : (a -> b) -> f a -> f b

lib/Prelude/List.idr+5−4

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

3import Builtins

4

5import Prelude.Algebra

6+import Prelude.Functor

6import Prelude.Maybe

7import Prelude.Maybe

7import Prelude.Nat

8import Prelude.Nat

8

9

@@ -163,6 +164,10 @@ instance Monoid (List a) where

163-- instance VerifiedSemigroup (List a) where

164-- instance VerifiedSemigroup (List a) where

164-- semigroupOpIsAssociative = appendAssociative

165-- semigroupOpIsAssociative = appendAssociative

165

166

167+instance Functor List where

168+ map f [] = []

169+ map f (x::xs) = f x :: map f xs

170+

166--------------------------------------------------------------------------------

171--------------------------------------------------------------------------------

167-- Zips and unzips

172-- Zips and unzips

168--------------------------------------------------------------------------------

173--------------------------------------------------------------------------------

@@ -201,10 +206,6 @@ unzip3 ((l, c, r)::xs) with (unzip3 xs)

201-- Maps

206-- Maps

202--------------------------------------------------------------------------------

207--------------------------------------------------------------------------------

203

208

204−map : (a -> b) -> List a -> List b

205−map f [] = []

206−map f (x::xs) = f x :: map f xs

207−

208mapMaybe : (a -> Maybe b) -> List a -> List b

209mapMaybe : (a -> Maybe b) -> List a -> List b

209mapMaybe f [] = []

210mapMaybe f [] = []

210mapMaybe f (x::xs) =

211mapMaybe f (x::xs) =

lib/System/Concurrency/Process.idr+1−1

@@ -16,7 +16,7 @@ data Process : (msgType : Type) -> Type -> Type where

16 lift : IO a -> Process msg a

17

18instance Functor (Process msg) where

19− fmap f (lift a) = lift (fmap f a)

19+ map f (lift a) = lift (map f a)

20

21instance Applicative (Process msg) where

22 pure = lift . return

test/reg001/reg001.idr+1−1

@@ -2,7 +2,7 @@ apply : (a -> b) -> a -> b

2apply f x = f x

3

4class Functor f => VerifiedFunctor (f : Type -> Type) where

5− identity : (fa : f a) -> fmap id fa = fa

5+ identity : (fa : f a) -> map id fa = fa

6

7data Imp : Type where

8 MkImp : {any : Type} -> any -> Imp

test/test007/test007.idr+1−1

@@ -14,7 +14,7 @@ fetch x = MkEval (\e => fetchVal e) where

14 fetchVal ((v, val) :: xs) = if (x == v) then (Just val) else (fetchVal xs)

15

16instance Functor Eval where

17− fmap f (MkEval g) = MkEval (\e => fmap f (g e))

17+ map f (MkEval g) = MkEval (\e => map f (g e))

18

19instance Applicative Eval where

20 pure x = MkEval (\e => Just x)

tutorial/examples/idiom.idr+1−1