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 -> 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
<$ :: 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, Functor (PureConversionT m)
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)
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, Applicative (PureConversionT m)
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)
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, 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)
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 =
  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 :: forall (m :: * -> *).
(PureTCM m, MonadBlock m) =>
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 :: forall (m :: * -> *).
(PureTCM m, MonadBlock m) =>
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 :: forall (m :: * -> *) a.
(MonadBlock m, PureTCM m, Show a) =>
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
  [Char] -> Int -> [Char] -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.conv.pure" Int
40 ([Char] -> m ()) -> [Char] -> m ()
forall a b. (a -> b) -> a -> b
$ [Char]
"runPureConversion result: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Either TCErr a -> [Char]
forall a. Show a => a -> [Char]
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 :: forall (m :: * -> *) a. Monad m => 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 :: [Char] -> PureConversionT m a
fromString [Char]
s = a -> PureConversionT m a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Char] -> a
forall a. IsString a => [Char] -> a
fromString [Char]
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 :: forall a. 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 :: 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 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' :: forall a.
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' :: MonadMetaSolver (PureConversionT m) =>
MetaId -> [Arg [Char]] -> Term -> PureConversionT m ()
assignTerm' MetaId
m [Arg [Char]]
_ 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 :: forall a.
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 :: [Char] -> (Integer -> Integer) -> PureConversionT m ()
modifyCounter [Char]
_ 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