{-# LANGUAGE MagicHash #-}
{-# LANGUAGE UnboxedTuples #-}
{-# LANGUAGE Strict #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-redundant-bang-patterns #-}
{-|
This is a very strict Writer monad, as a wrapper on "Agda.Utils.StrictState".
-}

module Agda.Utils.StrictWriter (
    MonadWriter(..)
  , censor
  , module Agda.Utils.StrictWriter )
  where

import Control.Monad.Reader (MonadReader(..))
import Control.Monad.Except (MonadError(..))
import Control.Monad.State (MonadState(..))
import Control.Monad.Trans (MonadTrans(..))
import Control.Monad.IO.Class (MonadIO(..))
import Control.Monad.Trans.Control (MonadTransControl(..))
import Control.Monad.Writer (MonadWriter(..), censor)
import Data.Strict.Tuple
import GHC.Exts (oneShot)
import Agda.Utils.StrictState
import Agda.Utils.ExpandCase

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)

deriving instance ExpandCase (State w a) => ExpandCase (Writer w 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

instance Monoid w => MonadWriter w (Writer w) where
  {-# INLINE tell #-}
  tell :: 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 (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (w -> w -> w
forall a. Semigroup a => a -> a -> a
<> w
w))

  pass :: forall a. Writer w (a, w -> w) -> Writer w a
pass (Writer (State w -> (# (a, w -> w), w #)
m)) = State w a -> Writer w a
forall w a. State w a -> Writer w a
Writer ((w -> (# a, w #)) -> State w a
forall s a. (s -> (# a, s #)) -> State s a
State ((w -> (# a, w #)) -> w -> (# a, w #)
forall a b. (a -> b) -> a -> b
oneShot \w
w -> case w -> (# (a, w -> w), w #)
m w
w of
    (# (!a
a, !w -> w
f), w
w' #) -> let wt :: w
wt = w
w w -> w -> w
forall a. Semigroup a => a -> a -> a
<> w -> w
f w
w' in (# a
a, w
wt #)))

  {-# INLINE listen #-}
  listen :: forall a. 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 (m :: * -> *). MonadState s m => m s
get
    put mempty
    a <- act
    diff <- get
    put (old <> diff)
    pure (a, diff)

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

newtype WriterT w m a = WriterT {forall w (m :: * -> *) a. WriterT w m a -> StateT w m a
unWriterT :: StateT w m a}
  deriving ((forall a b. (a -> b) -> WriterT w m a -> WriterT w m b)
-> (forall a b. a -> WriterT w m b -> WriterT w m a)
-> Functor (WriterT w m)
forall a b. a -> WriterT w m b -> WriterT w m a
forall a b. (a -> b) -> WriterT w m a -> WriterT w m b
forall w (m :: * -> *) a b.
Functor m =>
a -> WriterT w m b -> WriterT w m a
forall w (m :: * -> *) a b.
Functor m =>
(a -> b) -> WriterT w m a -> WriterT w m 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 (m :: * -> *) a b.
Functor m =>
(a -> b) -> WriterT w m a -> WriterT w m b
fmap :: forall a b. (a -> b) -> WriterT w m a -> WriterT w m b
$c<$ :: forall w (m :: * -> *) a b.
Functor m =>
a -> WriterT w m b -> WriterT w m a
<$ :: forall a b. a -> WriterT w m b -> WriterT w m a
Functor, Functor (WriterT w m)
Functor (WriterT w m) =>
(forall a. a -> WriterT w m a)
-> (forall a b.
    WriterT w m (a -> b) -> WriterT w m a -> WriterT w m b)
-> (forall a b c.
    (a -> b -> c) -> WriterT w m a -> WriterT w m b -> WriterT w m c)
-> (forall a b. WriterT w m a -> WriterT w m b -> WriterT w m b)
-> (forall a b. WriterT w m a -> WriterT w m b -> WriterT w m a)
-> Applicative (WriterT w m)
forall a. a -> WriterT w m a
forall a b. WriterT w m a -> WriterT w m b -> WriterT w m a
forall a b. WriterT w m a -> WriterT w m b -> WriterT w m b
forall a b. WriterT w m (a -> b) -> WriterT w m a -> WriterT w m b
forall a b c.
(a -> b -> c) -> WriterT w m a -> WriterT w m b -> WriterT w m c
forall w (m :: * -> *). Monad m => Functor (WriterT w m)
forall w (m :: * -> *) a. Monad m => a -> WriterT w m a
forall w (m :: * -> *) a b.
Monad m =>
WriterT w m a -> WriterT w m b -> WriterT w m a
forall w (m :: * -> *) a b.
Monad m =>
WriterT w m a -> WriterT w m b -> WriterT w m b
forall w (m :: * -> *) a b.
Monad m =>
WriterT w m (a -> b) -> WriterT w m a -> WriterT w m b
forall w (m :: * -> *) a b c.
Monad m =>
(a -> b -> c) -> WriterT w m a -> WriterT w m b -> WriterT w m 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 (m :: * -> *) a. Monad m => a -> WriterT w m a
pure :: forall a. a -> WriterT w m a
$c<*> :: forall w (m :: * -> *) a b.
Monad m =>
WriterT w m (a -> b) -> WriterT w m a -> WriterT w m b
<*> :: forall a b. WriterT w m (a -> b) -> WriterT w m a -> WriterT w m b
$cliftA2 :: forall w (m :: * -> *) a b c.
Monad m =>
(a -> b -> c) -> WriterT w m a -> WriterT w m b -> WriterT w m c
liftA2 :: forall a b c.
(a -> b -> c) -> WriterT w m a -> WriterT w m b -> WriterT w m c
$c*> :: forall w (m :: * -> *) a b.
Monad m =>
WriterT w m a -> WriterT w m b -> WriterT w m b
*> :: forall a b. WriterT w m a -> WriterT w m b -> WriterT w m b
$c<* :: forall w (m :: * -> *) a b.
Monad m =>
WriterT w m a -> WriterT w m b -> WriterT w m a
<* :: forall a b. WriterT w m a -> WriterT w m b -> WriterT w m a
Applicative, Applicative (WriterT w m)
Applicative (WriterT w m) =>
(forall a b.
 WriterT w m a -> (a -> WriterT w m b) -> WriterT w m b)
-> (forall a b. WriterT w m a -> WriterT w m b -> WriterT w m b)
-> (forall a. a -> WriterT w m a)
-> Monad (WriterT w m)
forall a. a -> WriterT w m a
forall a b. WriterT w m a -> WriterT w m b -> WriterT w m b
forall a b. WriterT w m a -> (a -> WriterT w m b) -> WriterT w m b
forall w (m :: * -> *). Monad m => Applicative (WriterT w m)
forall w (m :: * -> *) a. Monad m => a -> WriterT w m a
forall w (m :: * -> *) a b.
Monad m =>
WriterT w m a -> WriterT w m b -> WriterT w m b
forall w (m :: * -> *) a b.
Monad m =>
WriterT w m a -> (a -> WriterT w m b) -> WriterT w m 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 (m :: * -> *) a b.
Monad m =>
WriterT w m a -> (a -> WriterT w m b) -> WriterT w m b
>>= :: forall a b. WriterT w m a -> (a -> WriterT w m b) -> WriterT w m b
$c>> :: forall w (m :: * -> *) a b.
Monad m =>
WriterT w m a -> WriterT w m b -> WriterT w m b
>> :: forall a b. WriterT w m a -> WriterT w m b -> WriterT w m b
$creturn :: forall w (m :: * -> *) a. Monad m => a -> WriterT w m a
return :: forall a. a -> WriterT w m a
Monad, (forall (m :: * -> *). Monad m => Monad (WriterT w m)) =>
(forall (m :: * -> *) a. Monad m => m a -> WriterT w m a)
-> MonadTrans (WriterT w)
forall w (m :: * -> *). Monad m => Monad (WriterT w m)
forall w (m :: * -> *) a. Monad m => m a -> WriterT w m a
forall (m :: * -> *). Monad m => Monad (WriterT w m)
forall (m :: * -> *) a. Monad m => m a -> WriterT w m a
forall (t :: (* -> *) -> * -> *).
(forall (m :: * -> *). Monad m => Monad (t m)) =>
(forall (m :: * -> *) a. Monad m => m a -> t m a) -> MonadTrans t
$clift :: forall w (m :: * -> *) a. Monad m => m a -> WriterT w m a
lift :: forall (m :: * -> *) a. Monad m => m a -> WriterT w m a
MonadTrans, Monad (WriterT w m)
Monad (WriterT w m) =>
(forall a. IO a -> WriterT w m a) -> MonadIO (WriterT w m)
forall a. IO a -> WriterT w m a
forall w (m :: * -> *). MonadIO m => Monad (WriterT w m)
forall w (m :: * -> *) a. MonadIO m => IO a -> WriterT w m a
forall (m :: * -> *).
Monad m =>
(forall a. IO a -> m a) -> MonadIO m
$cliftIO :: forall w (m :: * -> *) a. MonadIO m => IO a -> WriterT w m a
liftIO :: forall a. IO a -> WriterT w m a
MonadIO, MonadTrans (WriterT w)
MonadTrans (WriterT w) =>
(forall (m :: * -> *) a.
 Monad m =>
 (Run (WriterT w) -> m a) -> WriterT w m a)
-> (forall (m :: * -> *) a.
    Monad m =>
    m (StT (WriterT w) a) -> WriterT w m a)
-> MonadTransControl (WriterT w)
forall w. MonadTrans (WriterT w)
forall w (m :: * -> *) a.
Monad m =>
m (StT (WriterT w) a) -> WriterT w m a
forall w (m :: * -> *) a.
Monad m =>
(Run (WriterT w) -> m a) -> WriterT w m a
forall (m :: * -> *) a.
Monad m =>
m (StT (WriterT w) a) -> WriterT w m a
forall (m :: * -> *) a.
Monad m =>
(Run (WriterT w) -> m a) -> WriterT w m a
forall (t :: (* -> *) -> * -> *).
MonadTrans t =>
(forall (m :: * -> *) a. Monad m => (Run t -> m a) -> t m a)
-> (forall (m :: * -> *) a. Monad m => m (StT t a) -> t m a)
-> MonadTransControl t
$cliftWith :: forall w (m :: * -> *) a.
Monad m =>
(Run (WriterT w) -> m a) -> WriterT w m a
liftWith :: forall (m :: * -> *) a.
Monad m =>
(Run (WriterT w) -> m a) -> WriterT w m a
$crestoreT :: forall w (m :: * -> *) a.
Monad m =>
m (StT (WriterT w) a) -> WriterT w m a
restoreT :: forall (m :: * -> *) a.
Monad m =>
m (StT (WriterT w) a) -> WriterT w m a
MonadTransControl)

deriving instance ExpandCase (m (Pair a w)) => ExpandCase (WriterT w m a)
deriving instance (Monad m, MonadError e (StateT w m)) => MonadError e (WriterT w m)
deriving instance (Monad m, MonadReader r (StateT w m)) => MonadReader r (WriterT w m)
deriving instance (Monad m, MonadState s (StateT w m)) => MonadState s (WriterT w m)


instance (Monoid w, Monad m) => MonadWriter w (WriterT w m) where
  {-# INLINE tell #-}
  tell :: w -> WriterT w m ()
tell w
w = StateT w m () -> WriterT w m ()
forall w (m :: * -> *) a. StateT w m a -> WriterT w m a
WriterT ((w -> w) -> StateT w m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (w -> w -> w
forall a. Semigroup a => a -> a -> a
<> w
w))

  {-# INLINE pass #-}
  pass :: forall a. WriterT w m (a, w -> w) -> WriterT w m a
pass (WriterT (StateT w -> m (Pair (a, w -> w) w)
m)) = StateT w m a -> WriterT w m a
forall w (m :: * -> *) a. StateT w m a -> WriterT w m a
WriterT ((w -> m (Pair a w)) -> StateT w m a
forall s (m :: * -> *) a. (s -> m (Pair a s)) -> StateT s m a
StateT ((w -> m (Pair a w)) -> w -> m (Pair a w)
forall a b. (a -> b) -> a -> b
oneShot \w
w -> do
    (!a, !f) :!: w' <- w -> m (Pair (a, w -> w) w)
m w
w
    let wt = w
w w -> w -> w
forall a. Semigroup a => a -> a -> a
<> w -> w
f w
w'
    pure (a :!: wt)))

  {-# INLINE listen #-}
  listen :: forall a. WriterT w m a -> WriterT w m (a, w)
listen (WriterT StateT w m a
act) = StateT w m (a, w) -> WriterT w m (a, w)
forall w (m :: * -> *) a. StateT w m a -> WriterT w m a
WriterT do
    old <- StateT w m w
forall s (m :: * -> *). MonadState s m => m s
get
    put mempty
    a <- act
    diff <- get
    put (old <> diff)
    pure (a, diff)

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

{-# INLINE runWriterT #-}
runWriterT :: Monoid w => Monad m => WriterT w m a -> m (a, w)
runWriterT :: forall w (m :: * -> *) a.
(Monoid w, Monad m) =>
WriterT w m a -> m (a, w)
runWriterT (WriterT StateT w m a
act) = StateT w m a -> w -> m (a, w)
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m (a, s)
runStateT StateT w m a
act w
forall a. Monoid a => a
mempty

{-# INLINE execWriterT #-}
execWriterT :: Monoid w => Monad m => WriterT w m a -> m w
execWriterT :: forall w (m :: * -> *) a.
(Monoid w, Monad m) =>
WriterT w m a -> m w
execWriterT (WriterT StateT w m a
act) = StateT w m a -> w -> m w
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m s
execStateT StateT w m a
act w
forall a. Monoid a => a
mempty