f3ce933 · Idris-dev · git.iko.soy

lib/checkall.idr+2−2

compare with master

unifiedsplit

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

13import prelude.fin

14import prelude.list

15import prelude.maybe

16+import prelude.monad

17+import prelude.applicative

16import prelude.either

18import prelude.either

17import prelude.vect

19import prelude.vect

18import prelude.strings

20import prelude.strings

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

20

22

21import network.cgi

23import network.cgi

22

24

23−private dummy : Int

24−dummy = 42

lib/prelude.idr+10−24

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

8import prelude.fin

9import prelude.list

10import prelude.maybe

11+import prelude.monad

12+import prelude.applicative

11import prelude.either

13import prelude.either

12import prelude.vect

14import prelude.vect

13import prelude.strings

15import prelude.strings

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

64 show Nothing = "Nothing"

66 show Nothing = "Nothing"

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

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

66

68

67−---- Monad and instances

69+---- Monad 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

78

70

79instance Monad IO where

71instance Monad IO where

80 return t = io_return t

72 return t = io_return t

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

101 mzero = []

93 mzero = []

102 mplus = app

94 mplus = app

103

95

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

96+---- Functor instances

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

112

97

113instance Functor Maybe where

98instance Functor Maybe where

114 fmap f (Just x) = Just (f x)

99 fmap f (Just x) = Just (f x)

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

117instance Functor List where

102instance Functor List where

118 fmap = map

103 fmap = map

119

104

120−---- Applicative functors/Idioms

105+---- Applicative instances

106+

107+instance Applicative Maybe where

108+ pure = Just

121

109

122−infixl 2 <$>

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

111+ Nothing <$> Nothing = Nothing

123

112

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

125− pure : a -> f a

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

127

113

128---- some mathematical operations

114---- some mathematical operations

129

115

lib/prelude/applicative.idrnew file+13

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

1+module prelude.applicative

2+

3+import builtins

4+

5+---- Applicative functors/Idioms

6+

7+infixl 2 <$>

8+

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

1module prelude.cast

2

3−class Cast a b where

3+class Cast from to where

4− cast : a -> b

4+ cast : from -> to

5

6-- String casts

7

lib/prelude/monad.idrnew file+44

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

1+module prelude.monad

2+

3+-- Monads and Functors

4+

5+import builtins

6+

7+%access public

8+

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

256 = do i <- get

257 case (runParser (do setPosition pos

258 whiteSpace

259− ps <- many1 (pDecl syn)

259+ ps <- many (pDecl syn)

260 eof

261 i' <- getState

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

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

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

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

814 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"))

816 [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"))

818 [pexp e])

819 addGuard x = x

820

test/test007/test007.idr−6

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

1module main

2

3−instance Applicative Maybe where

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

5− Nothing <$> Nothing = Nothing

6−

7− pure x = Just x

8−

9data Expr = Var String

3data Expr = Var String

10 | Val Int

4 | Val Int

11 | Add Expr Expr

5 | Add Expr Expr

tutorial/interp.tex+2−2

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

358

359\begin{SaveVerbatim}{castclass}

360

361−class Cast a b where

361+class Cast from to where

362− cast : a -> b

362+ cast : from -> to

363

364\end{SaveVerbatim}

365\useverb{castclass}