@@ -6,64 +6,64 @@ import public Control.Monad.Trans
66%access public export
77
88||| A computation which runs in a context and produces an output
9−interface Monad m => MonadState s (m : Type -> Type) | m where
9+interface Monad m => MonadState stateType (m : Type -> Type) | m where
1010 ||| Get the context
11− get : m s
11+ get : m stateType
1212 ||| Write a new context/output
13− put : s -> m ()
13+ put : stateType -> m ()
1414
1515||| The transformer on which the State monad is based
16−record StateT (s : Type) (m : Type -> Type) (a : Type) where
16+record StateT (stateType : Type) (m : Type -> Type) (a : Type) where
1717 constructor ST
18− runStateT : s -> m (a, s)
18+ runStateT : stateType -> m (a, stateType)
1919
20−implementation Functor f => Functor (StateT s f) where
20+implementation Functor f => Functor (StateT stateType f) where
2121 map f (ST g) = ST (\st => map (mapFst f) (g st)) where
2222 mapFst : (a -> x) -> (a, s) -> (x, s)
2323 mapFst fn (a, b) = (fn a, b)
2424
25−implementation Monad f => Applicative (StateT s f) where
25+implementation Monad f => Applicative (StateT stateType f) where
2626 pure x = ST (\st => pure (x, st))
2727
2828 (ST f) <*> (ST a) = ST (\st => do (g, r) <- f st
2929 (b, t) <- a r
3030 return (g b, t))
3131
32−implementation Monad m => Monad (StateT s m) where
32+implementation Monad m => Monad (StateT stateType m) where
3333 (ST f) >>= k = ST (\st => do (v, st') <- f st
3434 let ST kv = k v
3535 kv st')
3636
37−implementation Monad m => MonadState s (StateT s m) where
37+implementation Monad m => MonadState stateType (StateT stateType m) where
3838 get = ST (\x => return (x, x))
3939 put x = ST (\y => return ((), x))
4040
41−implementation MonadTrans (StateT s) where
41+implementation MonadTrans (StateT stateType) where
4242 lift x = ST (\st => do r <- x
4343 return (r, st))
4444
4545||| Apply a function to modify the context of this computation
46−modify : MonadState s m => (s -> s) -> m ()
46+modify : MonadState stateType m => (stateType -> stateType) -> m ()
4747modify f = do s <- get
4848 put (f s)
4949
5050||| Evaluate a function in the context held by this computation
51−gets : MonadState s m => (s -> a) -> m a
51+gets : MonadState stateType m => (stateType -> a) -> m a
5252gets f = do s <- get
5353 return (f s)
5454
5555||| The State monad. See the MonadState interface
56−State : Type -> Type -> Type
56+State : (stateType : Type) -> (ty : Type) -> Type
5757State = \s, a => StateT s Identity a
5858
5959||| Unwrap a State monad computation.
60−runState : StateT s Identity a -> s -> (a, s)
60+runState : StateT stateType Identity a -> stateType -> (a, stateType)
6161runState act = runIdentity . runStateT act
6262
6363||| Unwrap a State monad computation, but discard the final state.
64−evalState : State s a -> s -> a
64+evalState : State stateType a -> stateType -> a
6565evalState m = fst . runState m
6666
6767||| Unwrap a State monad computation, but discard the resulting value.
68−execState : State s a -> s -> s
68+execState : State stateType a -> stateType -> stateType
6969execState m = snd . runState m