idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-11-28 11:05:17 +03:00
Code Issues Projects Releases Wiki Activity

removed MonadWriter functions from RWS.CPS.idr

Browse Source
This commit is contained in:
stefan-hoeck 2021-01-20 05:48:43 +01:00
parent 6f2e358f1b
commit e8f2f56768
2 changed files with 11 additions and 52 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

46
libs/base/Control/Monad/RWS/CPS.idr
View File

@ -136,52 +136,6 @@ HasIO m => HasIO (RWST r w s m) where
-- Writer Operations
--------------------------------------------------------------------------------
||| Construct a writer computation from a (result, output) pair.
public export %inline
writer : (Semigroup w, Applicative m) => (a, w) -> RWST r w s m a
writer (a,w') = MkRWST \_,s,w => pure (a,s,w <+> w')
||| `tell w` is an action that produces the output `w`.
public export %inline
tell : (Semigroup w, Applicative m) => w -> RWST r w s m ()
tell w' = writer ((), w')
||| `listens f m` is an action that executes the action `m` and adds
||| the result of applying `f` to the output to the value of the computation.
public export %inline
listens : (Monoid w, Functor m)
=> (w -> b) -> RWST r w s m a -> RWST r w s m (a, b)
listens f m = MkRWST \r,s,w =>
(\(a,s',w') => ((a,f w'),s',w <+> w')) <$> runRWST m r s
||| `listen m` is an action that executes the action `m` and adds its
||| output to the value of the computation.
public export %inline
listen : (Monoid w, Functor m)
=> RWST r w s m a -> RWST r w s m (a, w)
listen = listens id
||| `pass m` is an action that executes the action `m`, which returns
||| a value and a function, and returns the value, applying the function
||| to the output.
public export %inline
pass : (Monoid w, Semigroup w', Functor m)
=> RWST r w s m (a, w -> w') -> RWST r w' s m a
pass m = MkRWST \r,s,w =>
(\((a,f),s',w') => (a,s',w <+> f w')) <$> runRWST m r s
||| `censor f m` is an action that executes the action `m` and
||| applies the function `f` to its output, leaving the return value
||| unchanged.
public export %inline
censor : (Monoid w, Functor m) => (w -> w) -> RWST r w s m a -> RWST r w s m a
censor f m = MkRWST \r,s,w =>
(\(a,s',w') => (a,s',w <+> f w')) <$> runRWST m r s
--------------------------------------------------------------------------------
-- Writer Operations
--------------------------------------------------------------------------------
||| Construct a state monad computation from a state transformer function.
public export %inline
state : Applicative m => (s -> (s, a)) -> RWST r w s m a

17
libs/base/Control/Monad/Writer/Interface.idr
View File

@ -4,9 +4,9 @@ import Control.Monad.Maybe
import Control.Monad.Error.Either
import Control.Monad.Reader.Reader
import Control.Monad.State.State
import Control.Monad.RWS.CPS as RWS
import Control.Monad.RWS.CPS
import Control.Monad.Trans
import Control.Monad.Writer.CPS as Writer
import Control.Monad.Writer.CPS
||| MonadWriter interface
|||
@ -68,10 +68,15 @@ public export %inline
public export %inline
(Monoid w, Monad m) => MonadWriter w (RWST r w s m) where
writer = RWS.writer
tell = RWS.tell
listen = RWS.listen
pass = RWS.pass
writer (a,w') = MkRWST \_,s,w => pure (a,s,w <+> w')
tell w' = writer ((), w')
listen m = MkRWST \r,s,w =>
(\(a,s',w') => ((a,w'),s',w <+> w')) <$> runRWST m r s
pass m = MkRWST \r,s,w =>
(\((a,f),s',w') => (a,s',w <+> f w')) <$> runRWST m r s
public export %inline
MonadWriter w m => MonadWriter w (EitherT e m) where