git.iko.soy/Idris-dev
on master help sign in
Merge pull request #1838 from L8D/master
2e55414David Christiansen
libs/base/Control/Monad/Reader.idr+4
compare with master
unifiedsplit
@@ -2,6 +2,7 @@ module Control.Monad.Reader
2
2
3import Builtins
3import Builtins
4import Control.Monad.Identity
4import Control.Monad.Identity
5+import Control.Monad.Trans
5
6
6%access public
7%access public
7
8
@@ -41,6 +42,9 @@ instance Monad m => MonadReader r (ReaderT r m) where
41 ask = RD return
42 ask = RD return
42 local f (RD m) = RD $ m . f
43 local f (RD m) = RD $ m . f
43
44
45+instance MonadTrans (ReaderT r) where
46+ lift x = RD (const x)
47+
44||| Evaluate a function in the context of a Reader monad
48||| Evaluate a function in the context of a Reader monad
45asks : MonadReader r m => (r -> a) -> m a
49asks : MonadReader r m => (r -> a) -> m a
46asks f = do r <- ask
50asks f = do r <- ask
libs/base/Control/Monad/State.idr+5
@@ -1,6 +1,7 @@
1module Control.Monad.State
1module Control.Monad.State
2
2
3import Control.Monad.Identity
3import Control.Monad.Identity
4+import Control.Monad.Trans
4
5
5%access public
6%access public
6
7
@@ -37,6 +38,10 @@ instance Monad m => MonadState s (StateT s m) where
37 get = ST (\x => return (x, x))
38 get = ST (\x => return (x, x))
38 put x = ST (\y => return ((), x))
39 put x = ST (\y => return ((), x))
39
40
41+instance MonadTrans (StateT s) where
42+ lift x = ST (\st => do r <- x
43+ return (r, st))
44+
40||| Apply a function to modify the context of this computation
45||| Apply a function to modify the context of this computation
41modify : MonadState s m => (s -> s) -> m ()
46modify : MonadState s m => (s -> s) -> m ()
42modify f = do s <- get
47modify f = do s <- get
libs/base/Control/Monad/Trans.idrnew file+4
@@ -0,0 +1,4 @@
1+module Control.Monad.Trans
2+
3+class MonadTrans (t : (Type -> Type) -> Type -> Type) where
4+ lift : Monad m => m a -> t m a
libs/base/Control/Monad/Writer.idr+5
@@ -2,6 +2,7 @@ module Control.Monad.Writer
2
2
3import Builtins
3import Builtins
4import Control.Monad.Identity
4import Control.Monad.Identity
5+import Control.Monad.Trans
5
6
6%access public
7%access public
7
8
@@ -44,6 +45,10 @@ instance (Monoid w, Monad m) => MonadWriter w (WriterT w m) where
44 pass (WR m) = WR $ do ((a, f), w) <- m
45 pass (WR m) = WR $ do ((a, f), w) <- m
45 return (a, f w)
46 return (a, f w)
46
47
48+instance Monoid w => MonadTrans (WriterT w) where
49+ lift x = WR $ do r <- x
50+ return (r, neutral)
51+
47||| Run an action in the Writer monad and transform the written output
52||| Run an action in the Writer monad and transform the written output
48listens : MonadWriter w m => (w -> b) -> m a -> m (a, b)
53listens : MonadWriter w m => (w -> b) -> m a -> m (a, b)
49listens f m = listens' f (listen m) where
54listens f m = listens' f (listen m) where