module LinearScan.State0 where
import Debug.Trace (trace, traceShow, traceShowId)
import qualified Prelude
import qualified Data.IntMap
import qualified Data.IntSet
import qualified Data.List
import qualified Data.Ord
import qualified Data.Functor.Identity
import qualified Hask.Utils
import qualified LinearScan.Applicative as Applicative
import qualified LinearScan.Class as Class
import qualified LinearScan.Functor as Functor
import qualified LinearScan.Monad as Monad
import qualified LinearScan.Prelude0 as Prelude0
import qualified LinearScan.State as State
import qualified LinearScan.Tuple as Tuple
#ifdef __GLASGOW_HASKELL__
import qualified GHC.Base as GHC.Base
import qualified GHC.Prim as GHC.Prim
#else
import qualified LinearScan.IOExts as IOExts
#endif
#ifdef __GLASGOW_HASKELL__
type Any = GHC.Prim.Any
#else
type Any = ()
#endif
type StateT s m a = s -> m
getT :: (Applicative.Applicative a1) -> StateT a2 a1 a2
getT h i =
Applicative.pure h ((,) i i)
putT :: (Applicative.Applicative a1) -> a2 -> StateT a2 a1 ()
putT h x x0 =
Applicative.pure h ((,) () x)
modifyT :: (Applicative.Applicative a1) -> (a2 -> a2) -> StateT a2 a1 ()
modifyT h f i =
Applicative.pure h ((,) () (f i))
coq_StateT_Functor :: (Functor.Functor a2) -> Functor.Functor
(StateT a1 a2 Any)
coq_StateT_Functor h _ _ f x st =
Functor.fmap h (Tuple.first f) (x st)
coq_StateT_ap :: (Monad.Monad a1) -> (StateT a2 a1 (a3 -> a4)) -> (StateT
a2 a1 a3) -> StateT a2 a1 a4
coq_StateT_ap h f x st =
Monad.join h
(Functor.fmap (Applicative.is_functor (Monad.is_applicative h)) (\z ->
case z of {
(,) f' st' ->
Functor.fmap (Applicative.is_functor (Monad.is_applicative h))
(Tuple.first f') (x st')}) (f st))
coq_StateT_Applicative :: (Monad.Monad a1) -> Applicative.Applicative
(StateT a2 a1 Any)
coq_StateT_Applicative h =
Applicative.Build_Applicative
(coq_StateT_Functor (Applicative.is_functor (Monad.is_applicative h)))
(\_ x st -> Applicative.pure (Monad.is_applicative h) ((,) x st))
(\_ _ -> coq_StateT_ap h)
coq_StateT_join :: (Monad.Monad a1) -> (StateT a2 a1 (StateT a2 a1 a3)) ->
StateT a2 a1 a3
coq_StateT_join h x =
(Prelude..)
((Prelude..) (Monad.join h)
(Functor.fmap (Applicative.is_functor (Monad.is_applicative h))
(Tuple.curry Prelude0.apply))) x
coq_StateT_Monad :: (Monad.Monad a1) -> Monad.Monad (StateT a2 a1 Any)
coq_StateT_Monad h =
Monad.Build_Monad (coq_StateT_Applicative h) (\_ -> coq_StateT_join h)
coq_StateT_MonadTrans :: Class.MonadTrans (StateT a1 Any Any)
coq_StateT_MonadTrans _ h h0 _ x s =
Functor.fmap (Applicative.is_functor (Monad.is_applicative h)) (\k -> (,) k
s) x
liftStateT :: (Monad.Monad a1) -> (State.State a2 a3) -> StateT a2 a1 a3
liftStateT h x =
Monad.bind (coq_StateT_Monad h) (\st ->
case x st of {
(,) a st' ->
Monad.bind (coq_StateT_Monad h) (\x0 ->
Applicative.pure (coq_StateT_Applicative h) a)
(putT (Monad.is_applicative h) st')}) (getT (Monad.is_applicative h))