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 MonadState functions from RWS.CPS.idr

Browse Source
This commit is contained in:
stefan-hoeck 2021-01-20 05:51:39 +01:00
parent e8f2f56768
commit e906b28cae
2 changed files with 4 additions and 35 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -131,34 +131,3 @@ MonadTrans (RWST r w s) where
public export %inline
HasIO m => HasIO (RWST r w s m) where
liftIO = lift . liftIO
--------------------------------------------------------------------------------
-- 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
state f = MkRWST \_,s,w => let (s',a) = f s in pure (a,s',w)
||| Get a specific component of the state, using a projection function
||| supplied.
public export %inline
gets : Applicative m =>(s -> a) -> RWST r w s m a
gets f = MkRWST \_,s,w => pure (f s,s,w)
||| Fetch the current value of the state within the monad.
public export %inline
get : Applicative m =>RWST r w s m s
get = gets id
||| `put s` sets the state within the monad to `s`.
public export %inline
put : Applicative m => s -> RWST r w s m ()
put s = MkRWST \_,_,w => pure ((),s,w)
||| `modify f` is an action that updates the state to the result of
||| applying `f` to the current state.
public export %inline
modify : Applicative m =>(s -> s) -> RWST r w s m ()
modify f = MkRWST \_,s,w => pure ((),f s,w)

8
libs/base/Control/Monad/State/Interface.idr
View File

@ -4,7 +4,7 @@ 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
@ -61,9 +61,9 @@ MonadState s m => MonadState s (MaybeT m) where
public export %inline
Monad m => MonadState s (RWST r w s m) where
get = RWS.get
put = RWS.put
state = RWS.state
get = MkRWST \_,s,w => pure (s,s,w)
put s = MkRWST \_,_,w => pure ((),s,w)
state f = MkRWST \_,s,w => let (s',a) = f s in pure (a,s',w)
public export %inline
MonadState s m => MonadState s (ReaderT r m) where