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 {-# SOURCE #-} Agda.TypeChecking.Conversion
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Reduce (isBlocked)
import Agda.TypeChecking.Warnings

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

{-# SPECIALIZE pureEqualTerm :: Type -> Term -> Term -> TCM Bool #-}
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) =>
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)

{-# SPECIALIZE pureEqualType :: Type -> Type -> TCM Bool #-}
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) =>
PureConversionT m a -> m (Maybe a)
runPureConversion (Type -> Type -> PureConversionT m ()
forall (m :: * -> *). MonadConversion m => Type -> Type -> m ()
equalType Type
a Type
b)

{-# SPECIALIZE pureCompareAs :: Comparison -> CompareAs -> Term -> Term -> TCM Bool #-}
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) =>
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)

{-# SPECIALIZE runPureConversion :: PureConversionT TCM a -> TCM (Maybe a) #-}
runPureConversion
  :: (MonadBlock m, PureTCM m)
  => PureConversionT m a -> m (Maybe a)
runPureConversion :: forall (m :: * -> *) a.
(MonadBlock m, PureTCM m) =>
PureConversionT m a -> m (Maybe a)
runPureConversion (PureConversionT ExceptT TCErr (StateT FreshThings m) a
m) = Lens' TCEnv Bool -> (Bool -> Bool) -> m (Maybe a) -> m (Maybe a)
forall (m :: * -> *) a b.
MonadTCEnv m =>
Lens' TCEnv a -> (a -> a) -> m b -> m b
locallyTC (Bool -> f Bool) -> TCEnv -> f TCEnv
Lens' TCEnv Bool
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
$
  VerboseKey -> Int -> VerboseKey -> m (Maybe a) -> m (Maybe a)
forall a. VerboseKey -> Int -> VerboseKey -> m a -> m a
forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> Int -> VerboseKey -> m a -> m a
verboseBracket VerboseKey
"tc.conv.pure" Int
40 VerboseKey
"runPureConversion" (m (Maybe a) -> m (Maybe a)) -> m (Maybe a) -> m (Maybe a)
forall a b. (a -> b) -> a -> b
$ do
  Int
i <- Lens' TCState Int -> m Int
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useR (Int -> f Int) -> TCState -> f TCState
Lens' TCState Int
stFreshInt
  ProblemId
pid <- Lens' TCState ProblemId -> m ProblemId
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useR (ProblemId -> f ProblemId) -> TCState -> f TCState
Lens' TCState ProblemId
stFreshProblemId
  NameId
nid <- Lens' TCState NameId -> m NameId
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useR (NameId -> f NameId) -> TCState -> f TCState
Lens' TCState NameId
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
  case Either TCErr a
result of
    Left (PatternErr Blocker
block)
     | Blocker
block Blocker -> Blocker -> Bool
forall a. Eq a => a -> a -> Bool
== Blocker
neverUnblock -> do
         TCMT IO Doc -> m ()
forall {m :: * -> *}. MonadDebug m => TCMT IO Doc -> m ()
debugResult TCMT IO Doc
"stuck"
         Maybe a -> m (Maybe a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe a
forall a. Maybe a
Nothing
     | Bool
otherwise             -> do
         TCMT IO Doc -> m ()
forall {m :: * -> *}. MonadDebug m => TCMT IO Doc -> m ()
debugResult (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"blocked on" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Blocker -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Blocker -> m Doc
prettyTCM Blocker
block
         Blocker -> m (Maybe a)
forall a. Blocker -> m a
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
block
    Left TypeError{}   -> do
      TCMT IO Doc -> m ()
forall {m :: * -> *}. MonadDebug m => TCMT IO Doc -> m ()
debugResult TCMT IO Doc
"type error"
      Maybe a -> m (Maybe a)
forall a. a -> m 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            -> do
      TCMT IO Doc -> m ()
forall {m :: * -> *}. MonadDebug m => TCMT IO Doc -> m ()
debugResult TCMT IO Doc
"success"
      Maybe a -> m (Maybe a)
forall a. a -> m 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
  where
    debugResult :: TCMT IO Doc -> m ()
debugResult TCMT IO Doc
msg = VerboseKey -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"tc.conv.pure" Int
40 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"runPureConversion result: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
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 = 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 (m :: * -> *) a. Monad m => m a -> ExceptT TCErr 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 (m :: * -> *) a. Monad m => 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 a b.
PureConversionT m (a -> b)
-> PureConversionT m a -> PureConversionT m b
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 a. 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 a. a -> PureConversionT m a
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 a. 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 a.
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 a. 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 a. Blocker -> PureConversionT m a
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
u
  addAwakeConstraint :: Blocker -> Constraint -> PureConversionT m ()
addAwakeConstraint Blocker
u Constraint
_ = Blocker -> PureConversionT m ()
forall a. Blocker -> PureConversionT m a
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
u
  solveConstraint :: Constraint -> PureConversionT m ()
solveConstraint Constraint
c = Blocker -> PureConversionT m ()
forall a. Blocker -> PureConversionT m a
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 a. a -> PureConversionT m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  wakeConstraints :: (ProblemConstraint -> WakeUp) -> PureConversionT m ()
wakeConstraints ProblemConstraint -> WakeUp
_ = () -> PureConversionT m ()
forall a. a -> PureConversionT m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  stealConstraints :: ProblemId -> PureConversionT m ()
stealConstraints ProblemId
_ = () -> PureConversionT m ()
forall a. a -> PureConversionT m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  modifyAwakeConstraints :: (Constraints -> Constraints) -> PureConversionT m ()
modifyAwakeConstraints Constraints -> Constraints
_ = Blocker -> PureConversionT m ()
forall a. Blocker -> PureConversionT m a
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 a. Blocker -> PureConversionT m a
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 a. Blocker -> PureConversionT m 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 <- 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 a. Blocker -> PureConversionT m a
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 <- 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 a. Blocker -> PureConversionT m a
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
blocker
  etaExpandMeta :: [MetaClass] -> MetaId -> PureConversionT m ()
etaExpandMeta [MetaClass]
_ MetaId
_ = () -> PureConversionT m ()
forall a. a -> PureConversionT m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  updateMetaVar :: MetaId -> (MetaVariable -> MetaVariable) -> PureConversionT m ()
updateMetaVar MetaId
_ MetaVariable -> MetaVariable
_ = Blocker -> PureConversionT m ()
forall a. Blocker -> PureConversionT m a
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 a b.
PureConversionT m a
-> (a -> PureConversionT m b) -> PureConversionT m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    KeepMetas
KeepMetas     -> () -> PureConversionT m ()
forall a. a -> PureConversionT m a
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 a. Blocker -> PureConversionT m a
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 a. Blocker -> PureConversionT m a
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' TCState ConcreteNames -> PureConversionT m ConcreteNames
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useR (ConcreteNames -> f ConcreteNames) -> TCState -> f TCState
Lens' TCState ConcreteNames
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 a. Blocker -> PureConversionT m a
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
neverUnblock
    WhichWarnings
AllWarnings   -> () -> PureConversionT m ()
forall a. a -> PureConversionT m a
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 a. a -> PureConversionT m a
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 = i + 1 }
    ProblemId -> PureConversionT m ProblemId
forall a. a -> PureConversionT m a
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 = succ i }
    NameId -> PureConversionT m NameId
forall a. a -> PureConversionT m a
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 = i + 1 }
    Int -> PureConversionT m Int
forall a. a -> PureConversionT m a
forall (m :: * -> *) a. Monad m => a -> m a
return Int
i