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

git.iko.soy/Idris-dev

Merge pull request #394 from Melvar/fmap-to-map

rename fmap to map

commit7105d7997617654976bca4975804ca75da6ff123 authorEdwin Brady <edwin.brady@gmail.com> dateTue 16 Jul 2013, 05:11 (13 years ago) parentc2623f4 ee06705

17 files changed+48−50

compare with master

unifiedsplit

contribs/lib/SQLite3/Sqlite3.idr+3−3 contribs/lib/SimpleParser/SimpleParser.idr+6−6 lib/Control/IOExcept.idr+1−1 lib/Control/Monad/Identity.idr+1−1 lib/Control/Monad/State.idr+1−1 lib/Data/Morphisms.idr+1−1 lib/Data/SortedMap.idr+5−5 lib/Language/Reflection.idr+9−9 lib/Network/Cgi.idr+2−2 lib/Prelude.idr+6−9 lib/Prelude/Applicative.idr+3−3 lib/Prelude/Functor.idr+1−1 lib/Prelude/List.idr+5−4 lib/System/Concurrency/Process.idr+1−1 test/reg001/reg001.idr+1−1 test/test007/test007.idr+1−1 tutorial/examples/idiom.idr+1−1

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

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

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

4242

4343instance Functor DB where

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

45− return (fmap f res))

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

45+ return (map f res))

4646

4747

4848instance Applicative DB where

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

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

5151 case f' of

5252 Left err => return (Left err)

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

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

5454

5555

5656instance Monad DB where

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

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

2424parse (P p) inp = p inp

2525

2626instance 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

2828 Left err => Left err

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

3030

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

9090char x = sat (== x)

9191

9292string : String -> Parser String

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

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

9494

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

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

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

110110 pure False

111111

112112ident : Parser String

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

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

114114

115115nat : Parser Int

116116nat = do xs <- many digit

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

148148symbol xs = token (string xs)

149149

150150strToken : Parser String

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

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

152152

153153

154154--------------------------------------------------------------------------------

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

160160term : Parser Int

161161

162162expr = do t <- term

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

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

164164

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

166166

167167term = do f <- factor

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

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

169169

170170eval : String -> Maybe Int

171171eval xs = case (parse expr xs) of

lib/Control/IOExcept.idr+1−1

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

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

1010instance Functor (IOExcept e) where

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

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

1212

1313instance Applicative (IOExcept e) where

1414 pure x = ioM (pure (pure x))

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

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

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

1010instance Functor Identity where

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

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

1212

1313instance Applicative Identity where

1414 pure x = Id x

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

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

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

1616

1717instance 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

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

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

2121

lib/Data/Morphisms.idr+1−1

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

2323applyEndo (Endo f) a = f a

2424

2525instance Functor (Morphism r) where

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

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

2727

2828instance Applicative (Morphism r) where

2929 pure a = Mor $ const a

lib/Data/SortedMap.idr+5−5

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

226226toList (M _ t) = treeToList t

227227

228228instance Functor (Tree n k) where

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

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

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

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

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

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

232232

233233instance Functor (SortedMap k) where

234− fmap _ Empty = Empty

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

234+ map _ Empty = Empty

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

8888

8989

9090instance Functor Binder where

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

100100

101101total

102102traverse : (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)

2828getAction (MkCGI act) = act

2929

3030instance Functor CGI where

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

32− return (f a, i))

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

32+ return (f a, i))

3333

3434instance Applicative CGI where

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

lib/Prelude.idr+6−9

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

181181---- Functor instances

182182

183183instance Functor IO where

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

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

185185

186186instance Functor Maybe where

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

188− fmap f Nothing = Nothing

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

188+ map f Nothing = Nothing

189189

190190instance Functor (Either e) where

191− fmap f (Left l) = Left l

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

193−

194−instance Functor List where

195− fmap = map

191+ map f (Left l) = Left l

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

196193

197194---- Applicative instances

198195

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

376373

377374partial

378375getChar : IO Char

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

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

380377

381378---- some basic file handling

382379

lib/Prelude/Applicative.idr+3−3

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

1313

1414infixl 2 <$

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

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

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

1717

1818infixl 2 $>

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

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

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

2121

2222infixl 3 <|>

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

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

3232

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

3434sequence [] = pure []

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

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

3636

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

3838sequence_ [] = pure ()

lib/Prelude/Functor.idr+1−1

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

11module Prelude.Functor

33class 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

33import Builtins

55import Prelude.Algebra

6+import Prelude.Functor

67import Prelude.Maybe

78import Prelude.Nat

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

163164-- instance VerifiedSemigroup (List a) where

164165-- semigroupOpIsAssociative = appendAssociative

165166

167+instance Functor List where

168+ map f [] = []

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

170+

166171--------------------------------------------------------------------------------

167172-- Zips and unzips

168173--------------------------------------------------------------------------------

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

201206-- Maps

202207--------------------------------------------------------------------------------

203208

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

205−map f [] = []

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

207−

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

209210mapMaybe f [] = []

210211mapMaybe f (x::xs) =

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

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

1616 lift : IO a -> Process msg a

1717

1818instance Functor (Process msg) where

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

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

2020

2121instance Applicative (Process msg) where

2222 pure = lift . return

test/reg001/reg001.idr+1−1

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

22apply f x = f x

44class 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

77data Imp : Type where

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

test/test007/test007.idr+1−1

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

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

1515

1616instance 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))

1818

1919instance Applicative Eval where

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

tutorial/examples/idiom.idr+1−1