@@ -6,64 +6,64 @@ import public Control.Monad.Trans
6%access public export
6%access public export
8||| A computation which runs in a context and produces an output
8||| 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
10 ||| Get the context
10 ||| Get the context
11− get : m s
11+ get : m stateType
12 ||| Write a new context/output
12 ||| Write a new context/output
13− put : s -> m ()
13+ put : stateType -> m ()
15||| The transformer on which the State monad is based
15||| 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
17 constructor ST
17 constructor ST
18− runStateT : s -> m (a, s)
18+ runStateT : stateType -> m (a, stateType)
20−implementation Functor f => Functor (StateT s f) where
20+implementation Functor f => Functor (StateT stateType f) where
21 map f (ST g) = ST (\st => map (mapFst f) (g st)) where
21 map f (ST g) = ST (\st => map (mapFst f) (g st)) where
22 mapFst : (a -> x) -> (a, s) -> (x, s)
22 mapFst : (a -> x) -> (a, s) -> (x, s)
23 mapFst fn (a, b) = (fn a, b)
23 mapFst fn (a, b) = (fn a, b)
25−implementation Monad f => Applicative (StateT s f) where
25+implementation Monad f => Applicative (StateT stateType f) where
26 pure x = ST (\st => pure (x, st))
26 pure x = ST (\st => pure (x, st))
28 (ST f) <*> (ST a) = ST (\st => do (g, r) <- f st
28 (ST f) <*> (ST a) = ST (\st => do (g, r) <- f st
29 (b, t) <- a r
29 (b, t) <- a r
30 return (g b, t))
30 return (g b, t))
32−implementation Monad m => Monad (StateT s m) where
32+implementation Monad m => Monad (StateT stateType m) where
33 (ST f) >>= k = ST (\st => do (v, st') <- f st
33 (ST f) >>= k = ST (\st => do (v, st') <- f st
34 let ST kv = k v
34 let ST kv = k v
37−implementation Monad m => MonadState s (StateT s m) where
37+implementation Monad m => MonadState stateType (StateT stateType m) where
38 get = ST (\x => return (x, x))
38 get = ST (\x => return (x, x))
39 put x = ST (\y => return ((), x))
39 put x = ST (\y => return ((), x))
41−implementation MonadTrans (StateT s) where
41+implementation MonadTrans (StateT stateType) where
42 lift x = ST (\st => do r <- x
42 lift x = ST (\st => do r <- x
43 return (r, st))
43 return (r, st))
45||| Apply a function to modify the context of this computation
45||| 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 ()
47modify f = do s <- get
47modify f = do s <- get
50||| Evaluate a function in the context held by this computation
50||| 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
52gets f = do s <- get
52gets f = do s <- get
53 return (f s)
53 return (f s)
55||| The State monad. See the MonadState interface
55||| The State monad. See the MonadState interface
56−State : Type -> Type -> Type
56+State : (stateType : Type) -> (ty : Type) -> Type
57State = \s, a => StateT s Identity a
57State = \s, a => StateT s Identity a
59||| Unwrap a State monad computation.
59||| Unwrap a State monad computation.
60−runState : StateT s Identity a -> s -> (a, s)
60+runState : StateT stateType Identity a -> stateType -> (a, stateType)
61runState act = runIdentity . runStateT act
61runState act = runIdentity . runStateT act
63||| Unwrap a State monad computation, but discard the final state.
63||| Unwrap a State monad computation, but discard the final state.
64−evalState : State s a -> s -> a
64+evalState : State stateType a -> stateType -> a
65evalState m = fst . runState m
65evalState m = fst . runState m
67||| Unwrap a State monad computation, but discard the resulting value.
67||| Unwrap a State monad computation, but discard the resulting value.
68−execState : State s a -> s -> s
68+execState : State stateType a -> stateType -> stateType
69execState m = snd . runState m
69execState m = snd . runState m