{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses #-}
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