{-# LANGUAGE MagicHash, UnboxedTuples, Strict #-} {-# OPTIONS_GHC -Wno-redundant-bang-patterns #-} {-# OPTIONS_GHC -ddump-simpl -ddump-to-file -dsuppress-all -dno-suppress-type-signatures #-} module Agda.Utils.StrictState2 where import GHC.Exts (oneShot) newtype State s t a = State {forall s t a. State s t a -> s -> t -> (# a, s, t #) runState# :: s -> t -> (# a, s, t #)} instance Functor (State s t) where {-# INLINE fmap #-} fmap :: forall a b. (a -> b) -> State s t a -> State s t b fmap a -> b f (State s -> t -> (# a, s, t #) g) = (s -> t -> (# b, s, t #)) -> State s t b forall s t a. (s -> t -> (# a, s, t #)) -> State s t a State ((s -> t -> (# b, s, t #)) -> s -> t -> (# b, s, t #) forall a b. (a -> b) -> a -> b oneShot \s s t t -> case s -> t -> (# a, s, t #) g s s t t of (# a a, !s s, !t t #) -> let b :: b b = a -> b f a a in (# b b, s s, t t #)) {-# INLINE (<$) #-} <$ :: forall a b. a -> State s t b -> State s t a (<$) a a State s t b m = (\b _ -> a a) (b -> a) -> State s t b -> State s t a forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> State s t b m instance Applicative (State s t) where {-# INLINE pure #-} pure :: forall a. a -> State s t a pure ~a a = (s -> t -> (# a, s, t #)) -> State s t a forall s t a. (s -> t -> (# a, s, t #)) -> State s t a State ((s -> t -> (# a, s, t #)) -> s -> t -> (# a, s, t #) forall a b. (a -> b) -> a -> b oneShot \s s t t -> (# a a, s s, t t #)) {-# INLINE (<*>) #-} State s -> t -> (# a -> b, s, t #) mf <*> :: forall a b. State s t (a -> b) -> State s t a -> State s t b <*> State s -> t -> (# a, s, t #) ma = (s -> t -> (# b, s, t #)) -> State s t b forall s t a. (s -> t -> (# a, s, t #)) -> State s t a State ((s -> t -> (# b, s, t #)) -> s -> t -> (# b, s, t #) forall a b. (a -> b) -> a -> b oneShot \s s t t -> case s -> t -> (# a -> b, s, t #) mf s s t t of (# a -> b f, s s, t t #) -> case s -> t -> (# a, s, t #) ma s s t t of (# a a, !s s, !t t #) -> let b :: b b = a -> b f a a in (# b b, s s, t t #)) {-# INLINE (*>) #-} State s -> t -> (# a, s, t #) ma *> :: forall a b. State s t a -> State s t b -> State s t b *> State s -> t -> (# b, s, t #) mb = (s -> t -> (# b, s, t #)) -> State s t b forall s t a. (s -> t -> (# a, s, t #)) -> State s t a State ((s -> t -> (# b, s, t #)) -> s -> t -> (# b, s, t #) forall a b. (a -> b) -> a -> b oneShot \s s t t -> case s -> t -> (# a, s, t #) ma s s t t of (# a _, s s, t t #) -> s -> t -> (# b, s, t #) mb s s t t) {-# INLINE (<*) #-} State s -> t -> (# a, s, t #) ma <* :: forall a b. State s t a -> State s t b -> State s t a <* State s -> t -> (# b, s, t #) mb = (s -> t -> (# a, s, t #)) -> State s t a forall s t a. (s -> t -> (# a, s, t #)) -> State s t a State ((s -> t -> (# a, s, t #)) -> s -> t -> (# a, s, t #) forall a b. (a -> b) -> a -> b oneShot \s s t t -> case s -> t -> (# a, s, t #) ma s s t t of (# a a, s s, t t #) -> case s -> t -> (# b, s, t #) mb s s t t of (# b _, s s, t t #) -> (# a a, s s, t t #)) instance Monad (State s t) where {-# INLINE return #-} return :: forall a. a -> State s t a return = a -> State s t a forall a. a -> State s t a forall (f :: * -> *) a. Applicative f => a -> f a pure {-# INLINE (>>=) #-} State s -> t -> (# a, s, t #) ma >>= :: forall a b. State s t a -> (a -> State s t b) -> State s t b >>= a -> State s t b f = (s -> t -> (# b, s, t #)) -> State s t b forall s t a. (s -> t -> (# a, s, t #)) -> State s t a State ((s -> t -> (# b, s, t #)) -> s -> t -> (# b, s, t #) forall a b. (a -> b) -> a -> b oneShot \s s t t -> case s -> t -> (# a, s, t #) ma s s t t of (# a a, s s, t t #) -> State s t b -> s -> t -> (# b, s, t #) forall s t a. State s t a -> s -> t -> (# a, s, t #) runState# (a -> State s t b f a a) s s t t) {-# INLINE (>>) #-} >> :: forall a b. State s t a -> State s t b -> State s t b (>>) = State s t a -> State s t b -> State s t b forall a b. State s t a -> State s t b -> State s t b forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b (*>) {-# INLINE put #-} put :: s -> t -> State s t () put :: forall s t. s -> t -> State s t () put s s t t = (s -> t -> (# (), s, t #)) -> State s t () forall s t a. (s -> t -> (# a, s, t #)) -> State s t a State ((s -> t -> (# (), s, t #)) -> s -> t -> (# (), s, t #) forall a b. (a -> b) -> a -> b oneShot \s _ t _ -> (# (), s s, t t #)) {-# INLINE put1 #-} put1 :: s -> State s t () put1 :: forall s t. s -> State s t () put1 s s = (s -> t -> (# (), s, t #)) -> State s t () forall s t a. (s -> t -> (# a, s, t #)) -> State s t a State \s _ t t -> (# (), s s, t t #) {-# INLINE put2 #-} put2 :: t -> State s t () put2 :: forall t s. t -> State s t () put2 t t = (s -> t -> (# (), s, t #)) -> State s t () forall s t a. (s -> t -> (# a, s, t #)) -> State s t a State \s s t _ -> (# (), s s, t t #) {-# INLINE get #-} get :: State s t (s, t) get :: forall s t. State s t (s, t) get = (s -> t -> (# (s, t), s, t #)) -> State s t (s, t) forall s t a. (s -> t -> (# a, s, t #)) -> State s t a State \s s t t -> (# (s s, t t), s s, t t #) {-# INLINE get1 #-} get1 :: State s t s get1 :: forall s t. State s t s get1 = (s -> t -> (# s, s, t #)) -> State s t s forall s t a. (s -> t -> (# a, s, t #)) -> State s t a State \s s t t -> (# s s, s s, t t #) {-# INLINE get2 #-} get2 :: State s t t get2 :: forall s t. State s t t get2 = (s -> t -> (# t, s, t #)) -> State s t t forall s t a. (s -> t -> (# a, s, t #)) -> State s t a State \s s t t -> (# t t, s s, t t #) {-# INLINE gets #-} gets :: ((s, t) -> a) -> State s t a gets :: forall s t a. ((s, t) -> a) -> State s t a gets (s, t) -> a f = (s, t) -> a f ((s, t) -> a) -> State s t (s, t) -> State s t a forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> State s t (s, t) forall s t. State s t (s, t) get {-# INLINE modify #-} modify :: ((s,t) -> (s,t)) -> State s t () modify :: forall s t. ((s, t) -> (s, t)) -> State s t () modify (s, t) -> (s, t) f = (s -> t -> (# (), s, t #)) -> State s t () forall s t a. (s -> t -> (# a, s, t #)) -> State s t a State \s s t t -> let (!s s', !t t') = (s, t) -> (s, t) f (s s, t t) in (# (), s s', t t' #) {-# INLINE modify1 #-} modify1 :: (s -> s) -> State s t () modify1 :: forall s t. (s -> s) -> State s t () modify1 s -> s f = (s -> t -> (# (), s, t #)) -> State s t () forall s t a. (s -> t -> (# a, s, t #)) -> State s t a State \s s t t -> let !s' :: s s' = s -> s f s s in (# (), s s', t t #) {-# INLINE modify2 #-} modify2 :: (t -> t) -> State s t () modify2 :: forall t s. (t -> t) -> State s t () modify2 t -> t f = (s -> t -> (# (), s, t #)) -> State s t () forall s t a. (s -> t -> (# a, s, t #)) -> State s t a State \s s t t -> let !t' :: t t' = t -> t f t t in (# (), s s, t t' #) {-# INLINE execState #-} execState :: State s t a -> (s, t) -> (s, t) execState :: forall s t a. State s t a -> (s, t) -> (s, t) execState (State s -> t -> (# a, s, t #) f) (s s, t t) = case s -> t -> (# a, s, t #) f s s t t of (# a _, s s, t t #) -> (s s, t t) {-# INLINE runState #-} runState :: State s t a -> (s, t) -> (a, (s, t)) runState :: forall s t a. State s t a -> (s, t) -> (a, (s, t)) runState (State s -> t -> (# a, s, t #) f) (s s, t t) = case s -> t -> (# a, s, t #) f s s t t of (# !a a, !s s, !t t #) -> (a a, (s s, t t)) {-# INLINE evalState #-} evalState :: State s t a -> (s, t) -> a evalState :: forall s t a. State s t a -> (s, t) -> a evalState (State s -> t -> (# a, s, t #) f) (s s, t t) = case s -> t -> (# a, s, t #) f s s t t of (# a a, s _, t _ #) -> a a