{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses #-}
-- | Missing instances for WriterT in Agda's internals.
--
-- NB: we are not exporting any definitions, just typeclass instances.
module AgdaInternals () where

import Data.String

import Control.Monad
import Control.Monad.Writer
import Control.Monad.State

import Agda.TypeChecking.Monad
import Agda.TypeChecking.Warnings
import Agda.TypeChecking.Pretty

instance (Monoid r, Monad m, Semigroup (m Doc)) => Semigroup (WriterT r m Doc) where
  <> :: WriterT r m Doc -> WriterT r m Doc -> WriterT r m Doc
(<>) = (Doc -> Doc -> Doc)
-> WriterT r m Doc -> WriterT r m Doc -> WriterT r m Doc
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
(<>)
instance (Monoid r, Monad m, IsString (m a)) => IsString (WriterT r m a) where
  fromString :: String -> WriterT r m a
fromString String
s = m (a, r) -> WriterT r m a
forall w (m :: * -> *) a. m (a, w) -> WriterT w m a
WriterT (m (a, r) -> WriterT r m a) -> m (a, r) -> WriterT r m a
forall a b. (a -> b) -> a -> b
$ (a -> (a, r)) -> m a -> m (a, r)
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (,r
forall a. Monoid a => a
mempty) (m a -> m (a, r)) -> m a -> m (a, r)
forall a b. (a -> b) -> a -> b
$ String -> m a
forall a. IsString a => String -> a
fromString String
s
instance (Monoid r, MonadStConcreteNames m) => MonadStConcreteNames (WriterT r m) where
  runStConcreteNames :: forall a. StateT ConcreteNames (WriterT r m) a -> WriterT r m a
runStConcreteNames StateT ConcreteNames (WriterT r m) a
m = m (a, r) -> WriterT r m a
forall w (m :: * -> *) a. m (a, w) -> WriterT w m a
WriterT (m (a, r) -> WriterT r m a) -> m (a, r) -> WriterT r m a
forall a b. (a -> b) -> a -> b
$ StateT ConcreteNames m (a, r) -> m (a, r)
forall a. StateT ConcreteNames m a -> m a
forall (m :: * -> *) a.
MonadStConcreteNames m =>
StateT ConcreteNames m a -> m a
runStConcreteNames (StateT ConcreteNames m (a, r) -> m (a, r))
-> StateT ConcreteNames m (a, r) -> m (a, r)
forall a b. (a -> b) -> a -> b
$ (ConcreteNames -> m ((a, r), ConcreteNames))
-> StateT ConcreteNames m (a, r)
forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
StateT ((ConcreteNames -> m ((a, r), ConcreteNames))
 -> StateT ConcreteNames m (a, r))
-> (ConcreteNames -> m ((a, r), ConcreteNames))
-> StateT ConcreteNames m (a, r)
forall a b. (a -> b) -> a -> b
$ \ConcreteNames
s -> do
    ((a
x,ConcreteNames
s'),r
ns) <- WriterT r m (a, ConcreteNames) -> m ((a, ConcreteNames), r)
forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
runWriterT (WriterT r m (a, ConcreteNames) -> m ((a, ConcreteNames), r))
-> WriterT r m (a, ConcreteNames) -> m ((a, ConcreteNames), r)
forall a b. (a -> b) -> a -> b
$ StateT ConcreteNames (WriterT r m) a
-> ConcreteNames -> WriterT r m (a, ConcreteNames)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT StateT ConcreteNames (WriterT r m) a
m ConcreteNames
s
    ((a, r), ConcreteNames) -> m ((a, r), ConcreteNames)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ((a
x,r
ns),ConcreteNames
s')
instance (Monoid r, MonadInteractionPoints m) => MonadInteractionPoints (WriterT r m)
instance (Monoid r, MonadFresh i m) => MonadFresh i (WriterT r m)
instance (Monoid r, MonadWarning m) => MonadWarning (WriterT r m) where
instance (Monoid r, MonadBlock m) => MonadBlock (WriterT r m) where
  catchPatternErr :: forall a.
(Blocker -> WriterT r m a) -> WriterT r m a -> WriterT r m a
catchPatternErr Blocker -> WriterT r m a
h WriterT r m a
m = m (a, r) -> WriterT r m a
forall w (m :: * -> *) a. m (a, w) -> WriterT w m a
WriterT (m (a, r) -> WriterT r m a) -> m (a, r) -> WriterT r m a
forall a b. (a -> b) -> a -> b
$ (Blocker -> m (a, r)) -> m (a, r) -> m (a, r)
forall a. (Blocker -> m a) -> m a -> m a
forall (m :: * -> *) a.
MonadBlock m =>
(Blocker -> m a) -> m a -> m a
catchPatternErr (WriterT r m a -> m (a, r)
forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
runWriterT (WriterT r m a -> m (a, r))
-> (Blocker -> WriterT r m a) -> Blocker -> m (a, r)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Blocker -> WriterT r m a
h) (WriterT r m a -> m (a, r)
forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
runWriterT WriterT r m a
m)
instance (Monoid r, MonadTCM m, MonadConstraint m) => MonadConstraint (WriterT r m) where
  addConstraint :: Blocker -> Constraint -> WriterT r m ()
addConstraint Blocker
x = m () -> WriterT r m ()
forall (m :: * -> *) a. Monad m => m a -> WriterT r m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> WriterT r m ())
-> (Constraint -> m ()) -> Constraint -> WriterT r m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Blocker -> Constraint -> m ()
forall (m :: * -> *).
MonadConstraint m =>
Blocker -> Constraint -> m ()
addConstraint Blocker
x
  addAwakeConstraint :: Blocker -> Constraint -> WriterT r m ()
addAwakeConstraint Blocker
x = m () -> WriterT r m ()
forall (m :: * -> *) a. Monad m => m a -> WriterT r m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> WriterT r m ())
-> (Constraint -> m ()) -> Constraint -> WriterT r m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Blocker -> Constraint -> m ()
forall (m :: * -> *).
MonadConstraint m =>
Blocker -> Constraint -> m ()
addAwakeConstraint Blocker
x
  solveConstraint :: Constraint -> WriterT r m ()
solveConstraint = m () -> WriterT r m ()
forall (m :: * -> *) a. Monad m => m a -> WriterT r m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> WriterT r m ())
-> (Constraint -> m ()) -> Constraint -> WriterT r m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Constraint -> m ()
forall (m :: * -> *). MonadConstraint m => Constraint -> m ()
solveConstraint
  solveSomeAwakeConstraints :: (ProblemConstraint -> Bool) -> Bool -> WriterT r m ()
solveSomeAwakeConstraints ProblemConstraint -> Bool
x = m () -> WriterT r m ()
forall (m :: * -> *) a. Monad m => m a -> WriterT r m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> WriterT r m ())
-> (Bool -> m ()) -> Bool -> WriterT r m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ProblemConstraint -> Bool) -> Bool -> m ()
forall (m :: * -> *).
MonadConstraint m =>
(ProblemConstraint -> Bool) -> Bool -> m ()
solveSomeAwakeConstraints ProblemConstraint -> Bool
x
  wakeConstraints :: (ProblemConstraint -> WakeUp) -> WriterT r m ()
wakeConstraints = m () -> WriterT r m ()
forall (m :: * -> *) a. Monad m => m a -> WriterT r m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> WriterT r m ())
-> ((ProblemConstraint -> WakeUp) -> m ())
-> (ProblemConstraint -> WakeUp)
-> WriterT r m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ProblemConstraint -> WakeUp) -> m ()
forall (m :: * -> *).
MonadConstraint m =>
(ProblemConstraint -> WakeUp) -> m ()
wakeConstraints
  stealConstraints :: ProblemId -> WriterT r m ()
stealConstraints = m () -> WriterT r m ()
forall (m :: * -> *) a. Monad m => m a -> WriterT r m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> WriterT r m ())
-> (ProblemId -> m ()) -> ProblemId -> WriterT r m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProblemId -> m ()
forall (m :: * -> *). MonadConstraint m => ProblemId -> m ()
stealConstraints
  modifyAwakeConstraints :: (Constraints -> Constraints) -> WriterT r m ()
modifyAwakeConstraints = m () -> WriterT r m ()
forall (m :: * -> *) a. Monad m => m a -> WriterT r m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> WriterT r m ())
-> ((Constraints -> Constraints) -> m ())
-> (Constraints -> Constraints)
-> WriterT r m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Constraints -> Constraints) -> m ()
forall (m :: * -> *).
MonadConstraint m =>
(Constraints -> Constraints) -> m ()
modifyAwakeConstraints
  modifySleepingConstraints :: (Constraints -> Constraints) -> WriterT r m ()
modifySleepingConstraints = m () -> WriterT r m ()
forall (m :: * -> *) a. Monad m => m a -> WriterT r m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> WriterT r m ())
-> ((Constraints -> Constraints) -> m ())
-> (Constraints -> Constraints)
-> WriterT r m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Constraints -> Constraints) -> m ()
forall (m :: * -> *).
MonadConstraint m =>
(Constraints -> Constraints) -> m ()
modifySleepingConstraints
instance (Monoid r, MonadTCM m, MonadMetaSolver m) => MonadMetaSolver (WriterT r m) where
  newMeta' :: forall a.
MetaInstantiation
-> Frozen
-> MetaInfo
-> MetaPriority
-> Permutation
-> Judgement a
-> WriterT r m MetaId
newMeta' MetaInstantiation
x Frozen
y MetaInfo
z MetaPriority
k Permutation
l = m MetaId -> WriterT r m MetaId
forall (m :: * -> *) a. Monad m => m a -> WriterT r m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m MetaId -> WriterT r m MetaId)
-> (Judgement a -> m MetaId) -> Judgement a -> WriterT r m MetaId
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MetaInstantiation
-> Frozen
-> MetaInfo
-> MetaPriority
-> Permutation
-> Judgement a
-> m MetaId
forall a.
MetaInstantiation
-> Frozen
-> MetaInfo
-> MetaPriority
-> Permutation
-> Judgement a
-> m MetaId
forall (m :: * -> *) a.
MonadMetaSolver m =>
MetaInstantiation
-> Frozen
-> MetaInfo
-> MetaPriority
-> Permutation
-> Judgement a
-> m MetaId
newMeta' MetaInstantiation
x Frozen
y MetaInfo
z MetaPriority
k Permutation
l
  assignV :: CompareDirection
-> MetaId -> Args -> Term -> CompareAs -> WriterT r m ()
assignV CompareDirection
x MetaId
y Args
z Term
w = m () -> WriterT r m ()
forall (m :: * -> *) a. Monad m => m a -> WriterT r m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> WriterT r m ())
-> (CompareAs -> m ()) -> CompareAs -> WriterT r m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CompareDirection -> MetaId -> Args -> Term -> CompareAs -> m ()
forall (m :: * -> *).
MonadMetaSolver m =>
CompareDirection -> MetaId -> Args -> Term -> CompareAs -> m ()
assignV CompareDirection
x MetaId
y Args
z Term
w
  assignTerm' :: MonadMetaSolver (WriterT r m) =>
MetaId -> [Arg String] -> Term -> WriterT r m ()
assignTerm' MetaId
x [Arg String]
y = m () -> WriterT r m ()
forall (m :: * -> *) a. Monad m => m a -> WriterT r m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> WriterT r m ())
-> (Term -> m ()) -> Term -> WriterT r m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MetaId -> [Arg String] -> Term -> m ()
forall (m :: * -> *).
(MonadMetaSolver m, MonadMetaSolver m) =>
MetaId -> [Arg String] -> Term -> m ()
assignTerm' MetaId
x [Arg String]
y
  etaExpandMeta :: [MetaKind] -> MetaId -> WriterT r m ()
etaExpandMeta [MetaKind]
x = m () -> WriterT r m ()
forall (m :: * -> *) a. Monad m => m a -> WriterT r m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> WriterT r m ())
-> (MetaId -> m ()) -> MetaId -> WriterT r m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [MetaKind] -> MetaId -> m ()
forall (m :: * -> *).
MonadMetaSolver m =>
[MetaKind] -> MetaId -> m ()
etaExpandMeta [MetaKind]
x
  updateMetaVar :: MetaId -> (MetaVariable -> MetaVariable) -> WriterT r m ()
updateMetaVar MetaId
x = m () -> WriterT r m ()
forall (m :: * -> *) a. Monad m => m a -> WriterT r m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> WriterT r m ())
-> ((MetaVariable -> MetaVariable) -> m ())
-> (MetaVariable -> MetaVariable)
-> WriterT r m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MetaId -> (MetaVariable -> MetaVariable) -> m ()
forall (m :: * -> *).
MonadMetaSolver m =>
MetaId -> (MetaVariable -> MetaVariable) -> m ()
updateMetaVar MetaId
x
  speculateMetas :: WriterT r m () -> WriterT r m KeepMetas -> WriterT r m ()
speculateMetas WriterT r m ()
x = m ((), r) -> WriterT r m ()
forall w (m :: * -> *) a. m (a, w) -> WriterT w m a
WriterT (m ((), r) -> WriterT r m ())
-> (WriterT r m KeepMetas -> m ((), r))
-> WriterT r m KeepMetas
-> WriterT r m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WriterT r m () -> m ((), r)
forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
runWriterT (WriterT r m () -> m ((), r))
-> (WriterT r m KeepMetas -> WriterT r m ())
-> WriterT r m KeepMetas
-> m ((), r)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WriterT r m () -> WriterT r m KeepMetas -> WriterT r m ()
forall (m :: * -> *).
MonadMetaSolver m =>
m () -> m KeepMetas -> m ()
speculateMetas WriterT r m ()
x