f3ce933 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Some prelude shuffling

commitf3ce933e789449ae60707a62ce4712d86a4db594 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateSun 8 Jan 2012, 20:30 (15 years ago) parent2ce525e

8 files changed+76−39

compare with master

unifiedsplit

lib/checkall.idr+2−2 lib/prelude.idr+10−24 lib/prelude/applicative.idr+13 lib/prelude/cast.idr+2−2 lib/prelude/monad.idr+44 src/Idris/Parser.hs+3−3 test/test007/test007.idr−6 tutorial/interp.tex+2−2

lib/checkall.idr+2−2

@@ -13,6 +13,8 @@ import prelude.nat

1313import prelude.fin

1414import prelude.list

1515import prelude.maybe

16+import prelude.monad

17+import prelude.applicative

1618import prelude.either

1719import prelude.vect

1820import prelude.strings

@@ -20,5 +22,3 @@ import prelude.char

2022

2123import network.cgi

2224

23−private dummy : Int

24−dummy = 42

lib/prelude.idr+10−24

@@ -8,6 +8,8 @@ import prelude.nat

88import prelude.fin

99import prelude.list

1010import prelude.maybe

11+import prelude.monad

12+import prelude.applicative

1113import prelude.either

1214import prelude.vect

1315import prelude.strings

@@ -64,17 +66,7 @@ instance Show a => Show (Maybe a) where

6466 show Nothing = "Nothing"

6567 show (Just x) = "Just " ++ show x

6668

67−---- Monad and instances

68−

69−infixl 5 >>=

70−

71−class Monad (m : Set -> Set) where

72− return : a -> m a

73− (>>=) : m a -> (a -> m b) -> m b

74−

75−class Monad m => MonadPlus (m : Set -> Set) where

76− mplus : m a -> m a -> m a

77− mzero : m a

69+---- Monad instances

7870

7971instance Monad IO where

8072 return t = io_return t

@@ -101,14 +93,7 @@ instance MonadPlus List where

10193 mzero = []

10294 mplus = app

10395

104−guard : MonadPlus m => Bool -> m ()

105−guard True = return ()

106−guard False = mzero

107−

108−---- Functors

109−

110−class Functor (f : Set -> Set) where

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

96+---- Functor instances

11297

11398instance Functor Maybe where

11499 fmap f (Just x) = Just (f x)

@@ -117,13 +102,14 @@ instance Functor Maybe where

117102instance Functor List where

118103 fmap = map

119104

120−---- Applicative functors/Idioms

105+---- Applicative instances

106+

107+instance Applicative Maybe where

108+ pure = Just

121109

122−infixl 2 <$>

110+ (Just f) <$> (Just a) = Just (f a)

111+ Nothing <$> Nothing = Nothing

123112

124−class Functor f => Applicative (f : Set -> Set) where

125− pure : a -> f a

126− (<$>) : f (a -> b) -> f a -> f b

127113

128114---- some mathematical operations

129115

lib/prelude/applicative.idrnew file+13

@@ -0,0 +1,13 @@

1+module prelude.applicative

3+import builtins

5+---- Applicative functors/Idioms

7+infixl 2 <$>

9+class Applicative (f : Set -> Set) where

10+ pure : a -> f a

11+ (<$>) : f (a -> b) -> f a -> f b

12+

13+

lib/prelude/cast.idr+2−2

@@ -1,7 +1,7 @@

11module prelude.cast

3−class Cast a b where

4− cast : a -> b

3+class Cast from to where

4+ cast : from -> to

66-- String casts

lib/prelude/monad.idrnew file+44

@@ -0,0 +1,44 @@

1+module prelude.monad

3+-- Monads and Functors

5+import builtins

7+%access public

9+infixl 5 >>=

10+

11+class Monad (m : Set -> Set) where

12+ return : a -> m a

13+ (>>=) : m a -> (a -> m b) -> m b

14+

15+class Functor (f : Set -> Set) where

16+ fmap : (a -> b) -> f a -> f b

17+

18+class Monad m => MonadPlus (m : Set -> Set) where

19+ mplus : m a -> m a -> m a

20+ mzero : m a

21+

22+guard : MonadPlus m => Bool -> m ()

23+guard True = return ()

24+guard False = mzero

25+

26+when : Monad m => Bool -> m () -> m ()

27+when True f = f

28+when False _ = return ()

29+

30+sequence : Monad m => List (m a) -> m (List a)

31+sequence [] = return []

32+sequence (x :: xs) = [ x' :: xs' | x' <- x, xs' <- sequence xs ]

33+

34+sequence_ : Monad m => List (m a) -> m ()

35+sequence_ [] = return ()

36+sequence_ (x :: xs) = do x; sequence_ xs

37+

38+mapM : Monad m => (a -> m b) -> List a -> m (List b)

39+mapM f xs = sequence (map f xs)

40+

41+mapM_ : Monad m => (a -> m b) -> List a -> m ()

42+mapM_ f xs = sequence_ (map f xs)

43+

44+

src/Idris/Parser.hs+3−3

@@ -256,7 +256,7 @@ parseProg syn fname input pos

256256 = do i <- get

257257 case (runParser (do setPosition pos

258258 whiteSpace

259− ps <- many1 (pDecl syn)

259+ ps <- many (pDecl syn)

260260 eof

261261 i' <- getState

262262 return (concat ps, i')) i fname input) of

@@ -812,9 +812,9 @@ pComprehension syn

812812 = do lchar '['; fc <- pfc; pat <- pExpr syn; lchar '|';

813813 qs <- sepBy1 (pDo syn) (lchar ','); lchar ']';

814814 return (PDoBlock (map addGuard qs ++

815− [DoExp fc (PApp fc (PRef fc (NS (UN "return") ["prelude"]))

815+ [DoExp fc (PApp fc (PRef fc (UN "return"))

816816 [pexp pat])]))

817− where addGuard (DoExp fc e) = DoExp fc (PApp fc (PRef fc (NS (UN "guard") ["prelude"]))

817+ where addGuard (DoExp fc e) = DoExp fc (PApp fc (PRef fc (UN "guard"))

818818 [pexp e])

819819 addGuard x = x

820820

test/test007/test007.idr−6

@@ -1,11 +1,5 @@

11module main

3−instance Applicative Maybe where

4− (Just f) <$> (Just a) = Just (f a)

5− Nothing <$> Nothing = Nothing

6−

7− pure x = Just x

8−

93data Expr = Var String

104 | Val Int

115 | Add Expr Expr

tutorial/interp.tex+2−2

@@ -358,8 +358,8 @@ types:

358358

359359\begin{SaveVerbatim}{castclass}

360360

361−class Cast a b where

362− cast : a -> b

361+class Cast from to where

362+ cast : from -> to

363363

364364\end{SaveVerbatim}

365365\useverb{castclass}