{-|
This is a very strict Writer monad, as a wrapper on "Agda.Utils.StrictState".
-}

module Agda.Utils.StrictWriter where

import Agda.Utils.StrictState

newtype Writer w a = Writer {forall w a. Writer w a -> State w a
unWriter :: State w a}
  deriving ((forall a b. (a -> b) -> Writer w a -> Writer w b)
-> (forall a b. a -> Writer w b -> Writer w a)
-> Functor (Writer w)
forall a b. a -> Writer w b -> Writer w a
forall a b. (a -> b) -> Writer w a -> Writer w b
forall w a b. a -> Writer w b -> Writer w a
forall w a b. (a -> b) -> Writer w a -> Writer w b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall w a b. (a -> b) -> Writer w a -> Writer w b
fmap :: forall a b. (a -> b) -> Writer w a -> Writer w b
$c<$ :: forall w a b. a -> Writer w b -> Writer w a
<$ :: forall a b. a -> Writer w b -> Writer w a
Functor, Functor (Writer w)
Functor (Writer w) =>
(forall a. a -> Writer w a)
-> (forall a b. Writer w (a -> b) -> Writer w a -> Writer w b)
-> (forall a b c.
    (a -> b -> c) -> Writer w a -> Writer w b -> Writer w c)
-> (forall a b. Writer w a -> Writer w b -> Writer w b)
-> (forall a b. Writer w a -> Writer w b -> Writer w a)
-> Applicative (Writer w)
forall w. Functor (Writer w)
forall a. a -> Writer w a
forall w a. a -> Writer w a
forall a b. Writer w a -> Writer w b -> Writer w a
forall a b. Writer w a -> Writer w b -> Writer w b
forall a b. Writer w (a -> b) -> Writer w a -> Writer w b
forall w a b. Writer w a -> Writer w b -> Writer w a
forall w a b. Writer w a -> Writer w b -> Writer w b
forall w a b. Writer w (a -> b) -> Writer w a -> Writer w b
forall a b c.
(a -> b -> c) -> Writer w a -> Writer w b -> Writer w c
forall w a b c.
(a -> b -> c) -> Writer w a -> Writer w b -> Writer w c
forall (f :: * -> *).
Functor f =>
(forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
$cpure :: forall w a. a -> Writer w a
pure :: forall a. a -> Writer w a
$c<*> :: forall w a b. Writer w (a -> b) -> Writer w a -> Writer w b
<*> :: forall a b. Writer w (a -> b) -> Writer w a -> Writer w b
$cliftA2 :: forall w a b c.
(a -> b -> c) -> Writer w a -> Writer w b -> Writer w c
liftA2 :: forall a b c.
(a -> b -> c) -> Writer w a -> Writer w b -> Writer w c
$c*> :: forall w a b. Writer w a -> Writer w b -> Writer w b
*> :: forall a b. Writer w a -> Writer w b -> Writer w b
$c<* :: forall w a b. Writer w a -> Writer w b -> Writer w a
<* :: forall a b. Writer w a -> Writer w b -> Writer w a
Applicative, Applicative (Writer w)
Applicative (Writer w) =>
(forall a b. Writer w a -> (a -> Writer w b) -> Writer w b)
-> (forall a b. Writer w a -> Writer w b -> Writer w b)
-> (forall a. a -> Writer w a)
-> Monad (Writer w)
forall w. Applicative (Writer w)
forall a. a -> Writer w a
forall w a. a -> Writer w a
forall a b. Writer w a -> Writer w b -> Writer w b
forall a b. Writer w a -> (a -> Writer w b) -> Writer w b
forall w a b. Writer w a -> Writer w b -> Writer w b
forall w a b. Writer w a -> (a -> Writer w b) -> Writer w b
forall (m :: * -> *).
Applicative m =>
(forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
$c>>= :: forall w a b. Writer w a -> (a -> Writer w b) -> Writer w b
>>= :: forall a b. Writer w a -> (a -> Writer w b) -> Writer w b
$c>> :: forall w a b. Writer w a -> Writer w b -> Writer w b
>> :: forall a b. Writer w a -> Writer w b -> Writer w b
$creturn :: forall w a. a -> Writer w a
return :: forall a. a -> Writer w a
Monad)

{-# INLINE tell #-}
tell :: Monoid w => w -> Writer w ()
tell :: forall w. Monoid w => w -> Writer w ()
tell !w
w = State w () -> Writer w ()
forall w a. State w a -> Writer w a
Writer ((w -> w) -> State w ()
forall s. (s -> s) -> State s ()
modify (w -> w -> w
forall a. Semigroup a => a -> a -> a
<> w
w))

{-# INLINE listen #-}
listen :: Monoid w => Writer w a -> Writer w (a, w)
listen :: forall w a. Monoid w => Writer w a -> Writer w (a, w)
listen (Writer State w a
act) = State w (a, w) -> Writer w (a, w)
forall w a. State w a -> Writer w a
Writer do
  old <- State w w
forall s. State s s
get
  put mempty
  a <- act
  diff <- get
  put (old <> diff)
  pure (a, diff)

{-# INLINE writer #-}
writer :: Monoid w => (a, w) -> Writer w a
writer :: forall w a. Monoid w => (a, w) -> Writer w a
writer (!a
a, !w
w) = do
  w -> Writer w ()
forall w. Monoid w => w -> Writer w ()
tell w
w
  a -> Writer w a
forall a. a -> Writer w a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
a

{-# INLINE censor #-}
censor :: Monoid w => (w -> w) -> Writer w a -> Writer w a
censor :: forall w a. Monoid w => (w -> w) -> Writer w a -> Writer w a
censor w -> w
f (Writer State w a
act) = State w a -> Writer w a
forall w a. State w a -> Writer w a
Writer do
  old <- State w w
forall s. State s s
get
  put mempty
  a <- act
  diff <- get
  let !diff' = w -> w
f w
diff
  put (old <> diff')
  pure a

{-# INLINE runWriter #-}
runWriter :: Monoid w => Writer w a -> (a, w)
runWriter :: forall w a. Monoid w => Writer w a -> (a, w)
runWriter (Writer State w a
act) = State w a -> w -> (a, w)
forall s a. State s a -> s -> (a, s)
runState State w a
act w
forall a. Monoid a => a
mempty

{-# INLINE execWriter #-}
execWriter :: Monoid w => Writer w a -> w
execWriter :: forall w a. Monoid w => Writer w a -> w
execWriter (Writer State w a
act) = State w a -> w -> w
forall s a. State s a -> s -> s
execState State w a
act w
forall a. Monoid a => a
mempty