module Agda.TypeChecking.Conversion.Pure where

-- Control.Monad.Fail import is redundant since GHC 8.8.1
import Control.Monad.Fail (MonadFail)

import Control.Monad.Except
import Control.Monad.State

import Data.String

import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.Syntax.Internal.MetaVars (unblockOnAnyMetaIn)

import {-# SOURCE #-} Agda.TypeChecking.Conversion
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Reduce (isBlocked)
import Agda.TypeChecking.Warnings

import Agda.Utils.Either
import Agda.Utils.Maybe
import Agda.Utils.Null

import Agda.Utils.Impossible

data FreshThings = FreshThings
  { FreshThings -> Int
freshInt       :: Int
  , FreshThings -> ProblemId
freshProblemId :: ProblemId
  , FreshThings -> NameId
freshNameId    :: NameId
  }

newtype PureConversionT m a = PureConversionT
  { forall (m :: * -> *) a.
PureConversionT m a -> ExceptT TCErr (StateT FreshThings m) a
unPureConversionT :: ExceptT TCErr (StateT FreshThings m) a }
  deriving (forall a b. a -> PureConversionT m b -> PureConversionT m a
forall a b. (a -> b) -> PureConversionT m a -> PureConversionT m b
forall (m :: * -> *) a b.
Functor m =>
a -> PureConversionT m b -> PureConversionT m a
forall (m :: * -> *) a b.
Functor m =>
(a -> b) -> PureConversionT m a -> PureConversionT m b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> PureConversionT m b -> PureConversionT m a
$c<$ :: forall (m :: * -> *) a b.
Functor m =>
a -> PureConversionT m b -> PureConversionT m a
fmap :: forall a b. (a -> b) -> PureConversionT m a -> PureConversionT m b
$cfmap :: forall (m :: * -> *) a b.
Functor m =>
(a -> b) -> PureConversionT m a -> PureConversionT m b
Functor, forall a. a -> PureConversionT m a
forall a b.
PureConversionT m a -> PureConversionT m b -> PureConversionT m a
forall a b.
PureConversionT m a -> PureConversionT m b -> PureConversionT m b
forall a b.
PureConversionT m (a -> b)
-> PureConversionT m a -> PureConversionT m b
forall a b c.
(a -> b -> c)
-> PureConversionT m a
-> PureConversionT m b
-> PureConversionT m c
forall {m :: * -> *}. Monad m => Functor (PureConversionT m)
forall (m :: * -> *) a. Monad m => a -> PureConversionT m a
forall (m :: * -> *) a b.
Monad m =>
PureConversionT m a -> PureConversionT m b -> PureConversionT m a
forall (m :: * -> *) a b.
Monad m =>
PureConversionT m a -> PureConversionT m b -> PureConversionT m b
forall (m :: * -> *) a b.
Monad m =>
PureConversionT m (a -> b)
-> PureConversionT m a -> PureConversionT m b
forall (m :: * -> *) a b c.
Monad m =>
(a -> b -> c)
-> PureConversionT m a
-> PureConversionT m b
-> PureConversionT 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
<* :: forall a b.
PureConversionT m a -> PureConversionT m b -> PureConversionT m a
$c<* :: forall (m :: * -> *) a b.
Monad m =>
PureConversionT m a -> PureConversionT m b -> PureConversionT m a
*> :: forall a b.
PureConversionT m a -> PureConversionT m b -> PureConversionT m b
$c*> :: forall (m :: * -> *) a b.
Monad m =>
PureConversionT m a -> PureConversionT m b -> PureConversionT m b
liftA2 :: forall a b c.
(a -> b -> c)
-> PureConversionT m a
-> PureConversionT m b
-> PureConversionT m c
$cliftA2 :: forall (m :: * -> *) a b c.
Monad m =>
(a -> b -> c)
-> PureConversionT m a
-> PureConversionT m b
-> PureConversionT m c
<*> :: forall a b.
PureConversionT m (a -> b)
-> PureConversionT m a -> PureConversionT m b
$c<*> :: forall (m :: * -> *) a b.
Monad m =>
PureConversionT m (a -> b)
-> PureConversionT m a -> PureConversionT m b
pure :: forall a. a -> PureConversionT m a
$cpure :: forall (m :: * -> *) a. Monad m => a -> PureConversionT m a
Applicative, forall a. a -> PureConversionT m a
forall a b.
PureConversionT m a -> PureConversionT m b -> PureConversionT m b
forall a b.
PureConversionT m a
-> (a -> PureConversionT m b) -> PureConversionT m b
forall (m :: * -> *). Monad m => Applicative (PureConversionT m)
forall (m :: * -> *) a. Monad m => a -> PureConversionT m a
forall (m :: * -> *) a b.
Monad m =>
PureConversionT m a -> PureConversionT m b -> PureConversionT m b
forall (m :: * -> *) a b.
Monad m =>
PureConversionT m a
-> (a -> PureConversionT m b) -> PureConversionT 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
return :: forall a. a -> PureConversionT m a
$creturn :: forall (m :: * -> *) a. Monad m => a -> PureConversionT m a
>> :: forall a b.
PureConversionT m a -> PureConversionT m b -> PureConversionT m b
$c>> :: forall (m :: * -> *) a b.
Monad m =>
PureConversionT m a -> PureConversionT m b -> PureConversionT m b
>>= :: forall a b.
PureConversionT m a
-> (a -> PureConversionT m b) -> PureConversionT m b
$c>>= :: forall (m :: * -> *) a b.
Monad m =>
PureConversionT m a
-> (a -> PureConversionT m b) -> PureConversionT m b
Monad, MonadError TCErr, MonadState FreshThings, forall (m :: * -> *).
HasBuiltins m
-> HasConstInfo m
-> MonadAddContext m
-> MonadDebug m
-> MonadReduce m
-> MonadTCEnv m
-> ReadTCState m
-> PureTCM m
forall {m :: * -> *}.
(HasBuiltins m, HasConstInfo m, MonadAddContext m,
 MonadReduce m) =>
MonadDebug (PureConversionT m)
forall {m :: * -> *}.
(HasBuiltins m, HasConstInfo m, MonadAddContext m,
 MonadReduce m) =>
MonadTCEnv (PureConversionT m)
forall {m :: * -> *}.
(HasBuiltins m, HasConstInfo m, MonadAddContext m,
 MonadReduce m) =>
MonadReduce (PureConversionT m)
forall {m :: * -> *}.
(HasBuiltins m, HasConstInfo m, MonadAddContext m,
 MonadReduce m) =>
ReadTCState (PureConversionT m)
forall {m :: * -> *}.
(HasBuiltins m, HasConstInfo m, MonadAddContext m,
 MonadReduce m) =>
MonadAddContext (PureConversionT m)
forall {m :: * -> *}.
(HasBuiltins m, HasConstInfo m, MonadAddContext m,
 MonadReduce m) =>
HasBuiltins (PureConversionT m)
forall {m :: * -> *}.
(HasBuiltins m, HasConstInfo m, MonadAddContext m,
 MonadReduce m) =>
HasConstInfo (PureConversionT m)
PureTCM)

pureEqualTerm
  :: (PureTCM m, MonadBlock m)
  => Type -> Term -> Term -> m Bool
pureEqualTerm :: forall (m :: * -> *).
(PureTCM m, MonadBlock m) =>
Type -> Term -> Term -> m Bool
pureEqualTerm Type
a Term
u Term
v =
  forall a. Maybe a -> Bool
isJust forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a.
(MonadBlock m, PureTCM m, Show a) =>
PureConversionT m a -> m (Maybe a)
runPureConversion (forall (m :: * -> *).
MonadConversion m =>
Type -> Term -> Term -> m ()
equalTerm Type
a Term
u Term
v)

pureEqualType
  :: (PureTCM m, MonadBlock m)
  => Type -> Type -> m Bool
pureEqualType :: forall (m :: * -> *).
(PureTCM m, MonadBlock m) =>
Type -> Type -> m Bool
pureEqualType Type
a Type
b =
  forall a. Maybe a -> Bool
isJust forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a.
(MonadBlock m, PureTCM m, Show a) =>
PureConversionT m a -> m (Maybe a)
runPureConversion (forall (m :: * -> *). MonadConversion m => Type -> Type -> m ()
equalType Type
a Type
b)

pureCompareAs
  :: (PureTCM m, MonadBlock m)
  => Comparison -> CompareAs -> Term -> Term -> m Bool
pureCompareAs :: forall (m :: * -> *).
(PureTCM m, MonadBlock m) =>
Comparison -> CompareAs -> Term -> Term -> m Bool
pureCompareAs Comparison
cmp CompareAs
a Term
u Term
v =
  forall a. Maybe a -> Bool
isJust forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a.
(MonadBlock m, PureTCM m, Show a) =>
PureConversionT m a -> m (Maybe a)
runPureConversion (forall (m :: * -> *).
MonadConversion m =>
Comparison -> CompareAs -> Term -> Term -> m ()
compareAs Comparison
cmp CompareAs
a Term
u Term
v)

runPureConversion
  :: (MonadBlock m, PureTCM m, Show a)
  => PureConversionT m a -> m (Maybe a)
runPureConversion :: forall (m :: * -> *) a.
(MonadBlock m, PureTCM m, Show a) =>
PureConversionT m a -> m (Maybe a)
runPureConversion (PureConversionT ExceptT TCErr (StateT FreshThings m) a
m) = forall (m :: * -> *) a b.
MonadTCEnv m =>
Lens' a TCEnv -> (a -> a) -> m b -> m b
locallyTC Lens' Bool TCEnv
eCompareBlocked (forall a b. a -> b -> a
const Bool
True) forall a b. (a -> b) -> a -> b
$
  forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> Int -> VerboseKey -> m a -> m a
verboseBracket VerboseKey
"tc.conv.pure" Int
40 VerboseKey
"runPureConversion" forall a b. (a -> b) -> a -> b
$ do
  Int
i <- forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useR Lens' Int TCState
stFreshInt
  ProblemId
pid <- forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useR Lens' ProblemId TCState
stFreshProblemId
  NameId
nid <- forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useR Lens' NameId TCState
stFreshNameId
  let frsh :: FreshThings
frsh = Int -> ProblemId -> NameId -> FreshThings
FreshThings Int
i ProblemId
pid NameId
nid
  Either TCErr a
result <- forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT ExceptT TCErr (StateT FreshThings m) a
m) FreshThings
frsh
  case Either TCErr a
result of
    Left (PatternErr Blocker
block)
     | Blocker
block forall a. Eq a => a -> a -> Bool
== Blocker
neverUnblock -> do
         forall {m :: * -> *}. MonadDebug m => TCMT IO Doc -> m ()
debugResult TCMT IO Doc
"stuck"
         forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
     | Bool
otherwise             -> do
         forall {m :: * -> *}. MonadDebug m => TCMT IO Doc -> m ()
debugResult forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"blocked on" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Blocker
block
         forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
block
    Left TypeError{}   -> do
      forall {m :: * -> *}. MonadDebug m => TCMT IO Doc -> m ()
debugResult TCMT IO Doc
"type error"
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
    Left Exception{}   -> forall a. HasCallStack => a
__IMPOSSIBLE__
    Left IOException{} -> forall a. HasCallStack => a
__IMPOSSIBLE__
    Right a
x            -> do
      forall {m :: * -> *}. MonadDebug m => TCMT IO Doc -> m ()
debugResult TCMT IO Doc
"success"
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just a
x
  where
    debugResult :: TCMT IO Doc -> m ()
debugResult TCMT IO Doc
msg = forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"tc.conv.pure" Int
40 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"runPureConversion result: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
msg

instance MonadTrans PureConversionT where
  lift :: forall (m :: * -> *) a. Monad m => m a -> PureConversionT m a
lift = forall (m :: * -> *) a.
ExceptT TCErr (StateT FreshThings m) a -> PureConversionT m a
PureConversionT forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift

deriving instance MonadFail       m => MonadFail       (PureConversionT m)
deriving instance HasBuiltins     m => HasBuiltins     (PureConversionT m)
deriving instance HasConstInfo    m => HasConstInfo    (PureConversionT m)
deriving instance HasOptions      m => HasOptions      (PureConversionT m)
deriving instance MonadTCEnv      m => MonadTCEnv      (PureConversionT m)
deriving instance ReadTCState     m => ReadTCState     (PureConversionT m)
deriving instance MonadReduce     m => MonadReduce     (PureConversionT m)
deriving instance MonadAddContext m => MonadAddContext (PureConversionT m)
deriving instance MonadDebug      m => MonadDebug      (PureConversionT m)

instance (Monad m, Semigroup a) => Semigroup (PureConversionT m a) where
  PureConversionT m a
d1 <> :: PureConversionT m a -> PureConversionT m a -> PureConversionT m a
<> PureConversionT m a
d2 = forall a. Semigroup a => a -> a -> a
(<>) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PureConversionT m a
d1 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> PureConversionT m a
d2

instance (IsString a, Monad m) => IsString (PureConversionT m a) where
  fromString :: VerboseKey -> PureConversionT m a
fromString VerboseKey
s = forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. IsString a => VerboseKey -> a
fromString VerboseKey
s)

instance Monad m => Null (PureConversionT m Doc) where
  empty :: PureConversionT m Doc
empty = forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Null a => a
empty
  null :: PureConversionT m Doc -> Bool
null = forall a. HasCallStack => a
__IMPOSSIBLE__

instance Monad m => MonadBlock (PureConversionT m) where
  patternViolation :: forall a. Blocker -> PureConversionT m a
patternViolation = forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall b c a. (b -> c) -> (a -> b) -> a -> c
. Blocker -> TCErr
PatternErr
  catchPatternErr :: forall a.
(Blocker -> PureConversionT m a)
-> PureConversionT m a -> PureConversionT m a
catchPatternErr Blocker -> PureConversionT m a
handle PureConversionT m a
m = PureConversionT m a
m forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \case
    PatternErr Blocker
b -> Blocker -> PureConversionT m a
handle Blocker
b
    TCErr
err          -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError TCErr
err


instance (PureTCM m, MonadBlock m) => MonadConstraint (PureConversionT m) where
  addConstraint :: Blocker -> Constraint -> PureConversionT m ()
addConstraint Blocker
u Constraint
_ = forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
u
  addAwakeConstraint :: Blocker -> Constraint -> PureConversionT m ()
addAwakeConstraint Blocker
u Constraint
_ = forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
u
  solveConstraint :: Constraint -> PureConversionT m ()
solveConstraint Constraint
c = forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
alwaysUnblock  -- TODO: does this happen?
  solveSomeAwakeConstraints :: (ProblemConstraint -> Bool) -> Bool -> PureConversionT m ()
solveSomeAwakeConstraints ProblemConstraint -> Bool
_ Bool
_ = forall (m :: * -> *) a. Monad m => a -> m a
return ()
  wakeConstraints :: (ProblemConstraint -> WakeUp) -> PureConversionT m ()
wakeConstraints ProblemConstraint -> WakeUp
_ = forall (m :: * -> *) a. Monad m => a -> m a
return ()
  stealConstraints :: ProblemId -> PureConversionT m ()
stealConstraints ProblemId
_ = forall (m :: * -> *) a. Monad m => a -> m a
return ()
  modifyAwakeConstraints :: (Constraints -> Constraints) -> PureConversionT m ()
modifyAwakeConstraints Constraints -> Constraints
_ = forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
alwaysUnblock  -- TODO: does this happen?
  modifySleepingConstraints :: (Constraints -> Constraints) -> PureConversionT m ()
modifySleepingConstraints Constraints -> Constraints
_ = forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
alwaysUnblock  -- TODO: does this happen?

instance (PureTCM m, MonadBlock m) => MonadMetaSolver (PureConversionT m) where
  newMeta' :: forall a.
MetaInstantiation
-> Frozen
-> MetaInfo
-> MetaPriority
-> Permutation
-> Judgement a
-> PureConversionT m MetaId
newMeta' MetaInstantiation
_ Frozen
_ MetaInfo
_ MetaPriority
_ Permutation
_ Judgement a
_ = forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
alwaysUnblock  -- TODO: does this happen?
  assignV :: CompareDirection
-> MetaId -> Args -> Term -> CompareAs -> PureConversionT m ()
assignV CompareDirection
_ MetaId
m Args
_ Term
v CompareAs
_ = do
    Maybe Blocker
bv <- forall t (m :: * -> *).
(Reduce t, IsMeta t, MonadReduce m) =>
t -> m (Maybe Blocker)
isBlocked Term
v
    let blocker :: Blocker
blocker = forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe Blocker
bv forall a. a -> a
id Blocker -> Blocker -> Blocker
unblockOnEither forall a b. (a -> b) -> a -> b
$ MetaId -> Blocker
unblockOnMeta MetaId
m
    forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
blocker
  assignTerm' :: MonadMetaSolver (PureConversionT m) =>
MetaId -> [Arg VerboseKey] -> Term -> PureConversionT m ()
assignTerm' MetaId
m [Arg VerboseKey]
_ Term
v = do
    Maybe Blocker
bv <- forall t (m :: * -> *).
(Reduce t, IsMeta t, MonadReduce m) =>
t -> m (Maybe Blocker)
isBlocked Term
v
    let blocker :: Blocker
blocker = forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe Blocker
bv forall a. a -> a
id Blocker -> Blocker -> Blocker
unblockOnEither forall a b. (a -> b) -> a -> b
$ MetaId -> Blocker
unblockOnMeta MetaId
m
    forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
blocker
  etaExpandMeta :: [MetaKind] -> MetaId -> PureConversionT m ()
etaExpandMeta [MetaKind]
_ MetaId
_ = forall (m :: * -> *) a. Monad m => a -> m a
return ()
  updateMetaVar :: MetaId -> (MetaVariable -> MetaVariable) -> PureConversionT m ()
updateMetaVar MetaId
_ MetaVariable -> MetaVariable
_ = forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
alwaysUnblock  -- TODO: does this happen?
  speculateMetas :: PureConversionT m ()
-> PureConversionT m KeepMetas -> PureConversionT m ()
speculateMetas PureConversionT m ()
fallback PureConversionT m KeepMetas
m = PureConversionT m KeepMetas
m forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    KeepMetas
KeepMetas     -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
    KeepMetas
RollBackMetas -> PureConversionT m ()
fallback

instance (PureTCM m, MonadBlock m) => MonadInteractionPoints (PureConversionT m) where
  freshInteractionId :: PureConversionT m InteractionId
freshInteractionId = forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
alwaysUnblock  -- TODO: does this happen?
  modifyInteractionPoints :: (InteractionPoints -> InteractionPoints) -> PureConversionT m ()
modifyInteractionPoints InteractionPoints -> InteractionPoints
_ = forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
alwaysUnblock  -- TODO: does this happen?

-- This is a bogus instance that promptly forgets all concrete names,
-- but we don't really care
instance ReadTCState m => MonadStConcreteNames (PureConversionT m) where
  runStConcreteNames :: forall a.
StateT ConcreteNames (PureConversionT m) a -> PureConversionT m a
runStConcreteNames StateT ConcreteNames (PureConversionT m) a
m = do
    ConcreteNames
concNames <- forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useR Lens' ConcreteNames TCState
stConcreteNames
    forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT StateT ConcreteNames (PureConversionT m) a
m ConcreteNames
concNames

instance (PureTCM m, MonadBlock m) => MonadWarning (PureConversionT m) where
  addWarning :: TCWarning -> PureConversionT m ()
addWarning TCWarning
w = case Warning -> WhichWarnings
classifyWarning (TCWarning -> Warning
tcWarning TCWarning
w) of
    WhichWarnings
ErrorWarnings -> forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
neverUnblock
    WhichWarnings
AllWarnings   -> forall (m :: * -> *) a. Monad m => a -> m a
return ()

instance ReadTCState m => MonadStatistics (PureConversionT m) where
  modifyCounter :: VerboseKey -> (Integer -> Integer) -> PureConversionT m ()
modifyCounter VerboseKey
_ Integer -> Integer
_ = forall (m :: * -> *) a. Monad m => a -> m a
return ()

instance Monad m => MonadFresh ProblemId (PureConversionT m) where
  fresh :: PureConversionT m ProblemId
fresh = do
    ProblemId
i <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets FreshThings -> ProblemId
freshProblemId
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \FreshThings
f -> FreshThings
f { freshProblemId :: ProblemId
freshProblemId = ProblemId
i forall a. Num a => a -> a -> a
+ ProblemId
1 }
    forall (m :: * -> *) a. Monad m => a -> m a
return ProblemId
i

instance Monad m => MonadFresh NameId (PureConversionT m) where
  fresh :: PureConversionT m NameId
fresh = do
    NameId
i <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets FreshThings -> NameId
freshNameId
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \FreshThings
f -> FreshThings
f { freshNameId :: NameId
freshNameId = forall a. Enum a => a -> a
succ NameId
i }
    forall (m :: * -> *) a. Monad m => a -> m a
return NameId
i

instance Monad m => MonadFresh Int (PureConversionT m) where
  fresh :: PureConversionT m Int
fresh = do
    Int
i <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets FreshThings -> Int
freshInt
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \FreshThings
f -> FreshThings
f { freshInt :: Int
freshInt = Int
i forall a. Num a => a -> a -> a
+ Int
1 }
    forall (m :: * -> *) a. Monad m => a -> m a
return Int
i