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
  { PureConversionT m a -> ExceptT TCErr (StateT FreshThings m) a
unPureConversionT :: ExceptT TCErr (StateT FreshThings m) a }
  deriving (a -> PureConversionT m b -> PureConversionT m a
(a -> b) -> PureConversionT m a -> PureConversionT m b
(forall a b.
 (a -> b) -> PureConversionT m a -> PureConversionT m b)
-> (forall a b. a -> PureConversionT m b -> PureConversionT m a)
-> Functor (PureConversionT m)
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
<$ :: a -> PureConversionT m b -> PureConversionT m a
$c<$ :: forall (m :: * -> *) a b.
Functor m =>
a -> PureConversionT m b -> PureConversionT m a
fmap :: (a -> b) -> PureConversionT m a -> PureConversionT m b
$cfmap :: forall (m :: * -> *) a b.
Functor m =>
(a -> b) -> PureConversionT m a -> PureConversionT m b
Functor, Functor (PureConversionT m)
a -> PureConversionT m a
Functor (PureConversionT m)
-> (forall a. a -> PureConversionT m a)
-> (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 a b.
    PureConversionT m a -> PureConversionT m b -> PureConversionT m b)
-> (forall a b.
    PureConversionT m a -> PureConversionT m b -> PureConversionT m a)
-> Applicative (PureConversionT m)
PureConversionT m a -> PureConversionT m b -> PureConversionT m b
PureConversionT m a -> PureConversionT m b -> PureConversionT m a
PureConversionT m (a -> b)
-> PureConversionT m a -> PureConversionT m b
(a -> b -> c)
-> PureConversionT m a
-> PureConversionT m b
-> PureConversionT m c
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
<* :: 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
*> :: 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 :: (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
<*> :: 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 :: a -> PureConversionT m a
$cpure :: forall (m :: * -> *) a. Monad m => a -> PureConversionT m a
$cp1Applicative :: forall (m :: * -> *). Monad m => Functor (PureConversionT m)
Applicative, Applicative (PureConversionT m)
a -> PureConversionT m a
Applicative (PureConversionT m)
-> (forall a b.
    PureConversionT m a
    -> (a -> PureConversionT m b) -> PureConversionT m b)
-> (forall a b.
    PureConversionT m a -> PureConversionT m b -> PureConversionT m b)
-> (forall a. a -> PureConversionT m a)
-> Monad (PureConversionT m)
PureConversionT m a
-> (a -> PureConversionT m b) -> PureConversionT m b
PureConversionT m a -> PureConversionT m b -> PureConversionT m b
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 :: a -> PureConversionT m a
$creturn :: forall (m :: * -> *) a. Monad m => a -> PureConversionT m a
>> :: 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
>>= :: 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
$cp1Monad :: forall (m :: * -> *). Monad m => Applicative (PureConversionT m)
Monad, MonadError TCErr, MonadState FreshThings, MonadDebug (PureConversionT m)
MonadTCEnv (PureConversionT m)
MonadReduce (PureConversionT m)
ReadTCState (PureConversionT m)
MonadAddContext (PureConversionT m)
HasBuiltins (PureConversionT m)
HasConstInfo (PureConversionT m)
HasBuiltins (PureConversionT m)
-> HasConstInfo (PureConversionT m)
-> MonadAddContext (PureConversionT m)
-> MonadDebug (PureConversionT m)
-> MonadReduce (PureConversionT m)
-> MonadTCEnv (PureConversionT m)
-> ReadTCState (PureConversionT m)
-> PureTCM (PureConversionT m)
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)
$cp7PureTCM :: forall (m :: * -> *).
(HasBuiltins m, HasConstInfo m, MonadAddContext m,
 MonadReduce m) =>
ReadTCState (PureConversionT m)
$cp6PureTCM :: forall (m :: * -> *).
(HasBuiltins m, HasConstInfo m, MonadAddContext m,
 MonadReduce m) =>
MonadTCEnv (PureConversionT m)
$cp5PureTCM :: forall (m :: * -> *).
(HasBuiltins m, HasConstInfo m, MonadAddContext m,
 MonadReduce m) =>
MonadReduce (PureConversionT m)
$cp4PureTCM :: forall (m :: * -> *).
(HasBuiltins m, HasConstInfo m, MonadAddContext m,
 MonadReduce m) =>
MonadDebug (PureConversionT m)
$cp3PureTCM :: forall (m :: * -> *).
(HasBuiltins m, HasConstInfo m, MonadAddContext m,
 MonadReduce m) =>
MonadAddContext (PureConversionT m)
$cp2PureTCM :: forall (m :: * -> *).
(HasBuiltins m, HasConstInfo m, MonadAddContext m,
 MonadReduce m) =>
HasConstInfo (PureConversionT m)
$cp1PureTCM :: forall (m :: * -> *).
(HasBuiltins m, HasConstInfo m, MonadAddContext m,
 MonadReduce m) =>
HasBuiltins (PureConversionT m)
PureTCM)

pureEqualTerm
  :: (PureTCM m, MonadBlock m)
  => Type -> Term -> Term -> m Bool
pureEqualTerm :: Type -> Term -> Term -> m Bool
pureEqualTerm Type
a Term
u Term
v =
  Maybe () -> Bool
forall a. Maybe a -> Bool
isJust (Maybe () -> Bool) -> m (Maybe ()) -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PureConversionT m () -> m (Maybe ())
forall (m :: * -> *) a.
(MonadBlock m, PureTCM m, Show a) =>
PureConversionT m a -> m (Maybe a)
runPureConversion (Type -> Term -> Term -> PureConversionT m ()
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 :: Type -> Type -> m Bool
pureEqualType Type
a Type
b =
  Maybe () -> Bool
forall a. Maybe a -> Bool
isJust (Maybe () -> Bool) -> m (Maybe ()) -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PureConversionT m () -> m (Maybe ())
forall (m :: * -> *) a.
(MonadBlock m, PureTCM m, Show a) =>
PureConversionT m a -> m (Maybe a)
runPureConversion (Type -> Type -> PureConversionT m ()
forall (m :: * -> *). MonadConversion m => Type -> Type -> m ()
equalType Type
a Type
b)

pureCompareAs
  :: (PureTCM m, MonadBlock m)
  => Comparison -> CompareAs -> Term -> Term -> m Bool
pureCompareAs :: Comparison -> CompareAs -> Term -> Term -> m Bool
pureCompareAs Comparison
cmp CompareAs
a Term
u Term
v =
  Maybe () -> Bool
forall a. Maybe a -> Bool
isJust (Maybe () -> Bool) -> m (Maybe ()) -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PureConversionT m () -> m (Maybe ())
forall (m :: * -> *) a.
(MonadBlock m, PureTCM m, Show a) =>
PureConversionT m a -> m (Maybe a)
runPureConversion (Comparison -> CompareAs -> Term -> Term -> PureConversionT m ()
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 :: PureConversionT m a -> m (Maybe a)
runPureConversion (PureConversionT ExceptT TCErr (StateT FreshThings m) a
m) = Lens' Bool TCEnv -> (Bool -> Bool) -> m (Maybe a) -> m (Maybe a)
forall (m :: * -> *) a b.
MonadTCEnv m =>
Lens' a TCEnv -> (a -> a) -> m b -> m b
locallyTC Lens' Bool TCEnv
eCompareBlocked (Bool -> Bool -> Bool
forall a b. a -> b -> a
const Bool
True) (m (Maybe a) -> m (Maybe a)) -> m (Maybe a) -> m (Maybe a)
forall a b. (a -> b) -> a -> b
$ do
  Int
i <- Lens' Int TCState -> m Int
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useR Lens' Int TCState
stFreshInt
  ProblemId
pid <- Lens' ProblemId TCState -> m ProblemId
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useR Lens' ProblemId TCState
stFreshProblemId
  NameId
nid <- Lens' NameId TCState -> m NameId
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 <- (Either TCErr a, FreshThings) -> Either TCErr a
forall a b. (a, b) -> a
fst ((Either TCErr a, FreshThings) -> Either TCErr a)
-> m (Either TCErr a, FreshThings) -> m (Either TCErr a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT FreshThings m (Either TCErr a)
-> FreshThings -> m (Either TCErr a, FreshThings)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (ExceptT TCErr (StateT FreshThings m) a
-> StateT FreshThings m (Either TCErr a)
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT ExceptT TCErr (StateT FreshThings m) a
m) FreshThings
frsh
  VerboseKey -> Int -> VerboseKey -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> VerboseKey -> m ()
reportSLn VerboseKey
"tc.conv.pure" Int
40 (VerboseKey -> m ()) -> VerboseKey -> m ()
forall a b. (a -> b) -> a -> b
$ VerboseKey
"runPureConversion result: " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ Either TCErr a -> VerboseKey
forall a. Show a => a -> VerboseKey
show Either TCErr a
result
  case Either TCErr a
result of
    Left (PatternErr Blocker
block)
     | Blocker
block Blocker -> Blocker -> Bool
forall a. Eq a => a -> a -> Bool
== Blocker
neverUnblock -> Maybe a -> m (Maybe a)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe a
forall a. Maybe a
Nothing
     | Bool
otherwise             -> Blocker -> m (Maybe a)
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
block
    Left TypeError{}   -> Maybe a -> m (Maybe a)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe a
forall a. Maybe a
Nothing
    Left Exception{}   -> m (Maybe a)
forall a. HasCallStack => a
__IMPOSSIBLE__
    Left IOException{} -> m (Maybe a)
forall a. HasCallStack => a
__IMPOSSIBLE__
    Right a
x            -> Maybe a -> m (Maybe a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe a -> m (Maybe a)) -> Maybe a -> m (Maybe a)
forall a b. (a -> b) -> a -> b
$ a -> Maybe a
forall a. a -> Maybe a
Just a
x

instance MonadTrans PureConversionT where
  lift :: m a -> PureConversionT m a
lift = ExceptT TCErr (StateT FreshThings m) a -> PureConversionT m a
forall (m :: * -> *) a.
ExceptT TCErr (StateT FreshThings m) a -> PureConversionT m a
PureConversionT (ExceptT TCErr (StateT FreshThings m) a -> PureConversionT m a)
-> (m a -> ExceptT TCErr (StateT FreshThings m) a)
-> m a
-> PureConversionT m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StateT FreshThings m a -> ExceptT TCErr (StateT FreshThings m) a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (StateT FreshThings m a -> ExceptT TCErr (StateT FreshThings m) a)
-> (m a -> StateT FreshThings m a)
-> m a
-> ExceptT TCErr (StateT FreshThings m) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m a -> StateT FreshThings m a
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 = a -> a -> a
forall a. Semigroup a => a -> a -> a
(<>) (a -> a -> a) -> PureConversionT m a -> PureConversionT m (a -> a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PureConversionT m a
d1 PureConversionT m (a -> a)
-> PureConversionT m a -> PureConversionT m a
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 = a -> PureConversionT m a
forall (m :: * -> *) a. Monad m => a -> m a
return (VerboseKey -> a
forall a. IsString a => VerboseKey -> a
fromString VerboseKey
s)

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

instance Monad m => MonadBlock (PureConversionT m) where
  patternViolation :: Blocker -> PureConversionT m a
patternViolation = TCErr -> PureConversionT m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TCErr -> PureConversionT m a)
-> (Blocker -> TCErr) -> Blocker -> PureConversionT m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Blocker -> TCErr
PatternErr
  catchPatternErr :: (Blocker -> PureConversionT m a)
-> PureConversionT m a -> PureConversionT m a
catchPatternErr Blocker -> PureConversionT m a
handle PureConversionT m a
m = PureConversionT m a
m PureConversionT m a
-> (TCErr -> PureConversionT m a) -> PureConversionT m a
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          -> TCErr -> PureConversionT m a
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
_ = Blocker -> PureConversionT m ()
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
u
  addAwakeConstraint :: Blocker -> Constraint -> PureConversionT m ()
addAwakeConstraint Blocker
u Constraint
_ = Blocker -> PureConversionT m ()
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
u
  solveConstraint :: Constraint -> PureConversionT m ()
solveConstraint Constraint
c = Blocker -> PureConversionT m ()
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
_ = () -> PureConversionT m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  wakeConstraints :: (ProblemConstraint -> WakeUp) -> PureConversionT m ()
wakeConstraints ProblemConstraint -> WakeUp
_ = () -> PureConversionT m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  stealConstraints :: ProblemId -> PureConversionT m ()
stealConstraints ProblemId
_ = () -> PureConversionT m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  modifyAwakeConstraints :: (Constraints -> Constraints) -> PureConversionT m ()
modifyAwakeConstraints Constraints -> Constraints
_ = Blocker -> PureConversionT m ()
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
alwaysUnblock  -- TODO: does this happen?
  modifySleepingConstraints :: (Constraints -> Constraints) -> PureConversionT m ()
modifySleepingConstraints Constraints -> Constraints
_ = Blocker -> PureConversionT m ()
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' :: MetaInstantiation
-> Frozen
-> MetaInfo
-> MetaPriority
-> Permutation
-> Judgement a
-> PureConversionT m MetaId
newMeta' MetaInstantiation
_ Frozen
_ MetaInfo
_ MetaPriority
_ Permutation
_ Judgement a
_ = Blocker -> PureConversionT m MetaId
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 <- Term -> PureConversionT m (Maybe Blocker)
forall t (m :: * -> *).
(Reduce t, IsMeta t, MonadReduce m) =>
t -> m (Maybe Blocker)
isBlocked Term
v
    let blocker :: Blocker
blocker = Maybe Blocker
-> (Blocker -> Blocker)
-> (Blocker -> Blocker -> Blocker)
-> Blocker
-> Blocker
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe Blocker
bv Blocker -> Blocker
forall a. a -> a
id Blocker -> Blocker -> Blocker
unblockOnEither (Blocker -> Blocker) -> Blocker -> Blocker
forall a b. (a -> b) -> a -> b
$ MetaId -> Blocker
unblockOnMeta MetaId
m
    Blocker -> PureConversionT m ()
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
blocker
  assignTerm' :: MetaId -> [Arg VerboseKey] -> Term -> PureConversionT m ()
assignTerm' MetaId
m [Arg VerboseKey]
_ Term
v = do
    Maybe Blocker
bv <- Term -> PureConversionT m (Maybe Blocker)
forall t (m :: * -> *).
(Reduce t, IsMeta t, MonadReduce m) =>
t -> m (Maybe Blocker)
isBlocked Term
v
    let blocker :: Blocker
blocker = Maybe Blocker
-> (Blocker -> Blocker)
-> (Blocker -> Blocker -> Blocker)
-> Blocker
-> Blocker
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe Blocker
bv Blocker -> Blocker
forall a. a -> a
id Blocker -> Blocker -> Blocker
unblockOnEither (Blocker -> Blocker) -> Blocker -> Blocker
forall a b. (a -> b) -> a -> b
$ MetaId -> Blocker
unblockOnMeta MetaId
m
    Blocker -> PureConversionT m ()
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
blocker
  etaExpandMeta :: [MetaKind] -> MetaId -> PureConversionT m ()
etaExpandMeta [MetaKind]
_ MetaId
_ = () -> PureConversionT m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  updateMetaVar :: MetaId -> (MetaVariable -> MetaVariable) -> PureConversionT m ()
updateMetaVar MetaId
_ MetaVariable -> MetaVariable
_ = Blocker -> PureConversionT m ()
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 PureConversionT m KeepMetas
-> (KeepMetas -> PureConversionT m ()) -> PureConversionT m ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    KeepMetas
KeepMetas     -> () -> PureConversionT m ()
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 = Blocker -> PureConversionT m InteractionId
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
alwaysUnblock  -- TODO: does this happen?
  modifyInteractionPoints :: (InteractionPoints -> InteractionPoints) -> PureConversionT m ()
modifyInteractionPoints InteractionPoints -> InteractionPoints
_ = Blocker -> PureConversionT m ()
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 :: StateT ConcreteNames (PureConversionT m) a -> PureConversionT m a
runStConcreteNames StateT ConcreteNames (PureConversionT m) a
m = do
    ConcreteNames
concNames <- Lens' ConcreteNames TCState -> PureConversionT m ConcreteNames
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useR Lens' ConcreteNames TCState
stConcreteNames
    (a, ConcreteNames) -> a
forall a b. (a, b) -> a
fst ((a, ConcreteNames) -> a)
-> PureConversionT m (a, ConcreteNames) -> PureConversionT m a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ConcreteNames (PureConversionT m) a
-> ConcreteNames -> PureConversionT m (a, ConcreteNames)
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 -> Blocker -> PureConversionT m ()
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
neverUnblock
    WhichWarnings
AllWarnings   -> () -> PureConversionT m ()
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
_ = () -> PureConversionT m ()
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 <- (FreshThings -> ProblemId) -> PureConversionT m ProblemId
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets FreshThings -> ProblemId
freshProblemId
    (FreshThings -> FreshThings) -> PureConversionT m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((FreshThings -> FreshThings) -> PureConversionT m ())
-> (FreshThings -> FreshThings) -> PureConversionT m ()
forall a b. (a -> b) -> a -> b
$ \FreshThings
f -> FreshThings
f { freshProblemId :: ProblemId
freshProblemId = ProblemId
i ProblemId -> ProblemId -> ProblemId
forall a. Num a => a -> a -> a
+ ProblemId
1 }
    ProblemId -> PureConversionT m ProblemId
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 <- (FreshThings -> NameId) -> PureConversionT m NameId
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets FreshThings -> NameId
freshNameId
    (FreshThings -> FreshThings) -> PureConversionT m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((FreshThings -> FreshThings) -> PureConversionT m ())
-> (FreshThings -> FreshThings) -> PureConversionT m ()
forall a b. (a -> b) -> a -> b
$ \FreshThings
f -> FreshThings
f { freshNameId :: NameId
freshNameId = NameId -> NameId
forall a. Enum a => a -> a
succ NameId
i }
    NameId -> PureConversionT m NameId
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 <- (FreshThings -> Int) -> PureConversionT m Int
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets FreshThings -> Int
freshInt
    (FreshThings -> FreshThings) -> PureConversionT m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((FreshThings -> FreshThings) -> PureConversionT m ())
-> (FreshThings -> FreshThings) -> PureConversionT m ()
forall a b. (a -> b) -> a -> b
$ \FreshThings
f -> FreshThings
f { freshInt :: Int
freshInt = Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1 }
    Int -> PureConversionT m Int
forall (m :: * -> *) a. Monad m => a -> m a
return Int
i