module Agda.TypeChecking.Conversion.Pure where

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 pureEqualTermB :: Type -> Term -> Term -> TCM (Either Blocker Bool) #-}
-- | Return the blocker instead of throwing a `patternViolation`.
pureEqualTermB :: PureTCM m => Type -> Term -> Term -> m (Either Blocker Bool)
pureEqualTermB :: forall (m :: * -> *).
PureTCM m =>
Type -> Term -> Term -> m (Either Blocker Bool)
pureEqualTermB Type
a Term
u Term
v =
  (Maybe () -> Bool)
-> Either Blocker (Maybe ()) -> Either Blocker Bool
forall a b. (a -> b) -> Either Blocker a -> Either Blocker b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Maybe () -> Bool
forall a. Maybe a -> Bool
isJust (Either Blocker (Maybe ()) -> Either Blocker Bool)
-> m (Either Blocker (Maybe ())) -> m (Either Blocker Bool)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PureConversionT m () -> m (Either Blocker (Maybe ()))
forall (m :: * -> *) a.
PureTCM m =>
PureConversionT m a -> m (Either Blocker (Maybe a))
runPureConversionB (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 pureEqualType :: Type -> Type -> TCM Bool #-}
-- | Return the blocker instead of throwing a `patternViolation`.
pureEqualTypeB :: PureTCM m => Type -> Type -> m (Either Blocker Bool)
pureEqualTypeB :: forall (m :: * -> *).
PureTCM m =>
Type -> Type -> m (Either Blocker Bool)
pureEqualTypeB Type
a Type
b =
  (Maybe () -> Bool)
-> Either Blocker (Maybe ()) -> Either Blocker Bool
forall a b. (a -> b) -> Either Blocker a -> Either Blocker b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Maybe () -> Bool
forall a. Maybe a -> Bool
isJust (Either Blocker (Maybe ()) -> Either Blocker Bool)
-> m (Either Blocker (Maybe ())) -> m (Either Blocker Bool)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PureConversionT m () -> m (Either Blocker (Maybe ()))
forall (m :: * -> *) a.
PureTCM m =>
PureConversionT m a -> m (Either Blocker (Maybe a))
runPureConversionB (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 m a
m = (Blocker -> m (Maybe a))
-> (Maybe a -> m (Maybe a))
-> Either Blocker (Maybe a)
-> m (Maybe a)
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either Blocker -> m (Maybe a)
forall a. Blocker -> m a
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Maybe a -> m (Maybe a)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either Blocker (Maybe a) -> m (Maybe a))
-> m (Either Blocker (Maybe a)) -> m (Maybe a)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< PureConversionT m a -> m (Either Blocker (Maybe a))
forall (m :: * -> *) a.
PureTCM m =>
PureConversionT m a -> m (Either Blocker (Maybe a))
runPureConversionB PureConversionT m a
m

{-# SPECIALIZE runPureConversionB :: PureConversionT TCM a -> TCM (Either Blocker (Maybe a)) #-}
runPureConversionB :: PureTCM m => PureConversionT m a -> m (Either Blocker (Maybe a))
runPureConversionB :: forall (m :: * -> *) a.
PureTCM m =>
PureConversionT m a -> m (Either Blocker (Maybe a))
runPureConversionB (PureConversionT ExceptT TCErr (StateT FreshThings m) a
m) = Lens' TCEnv Bool
-> (Bool -> Bool)
-> m (Either Blocker (Maybe a))
-> m (Either Blocker (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 (Either Blocker (Maybe a)) -> m (Either Blocker (Maybe a)))
-> m (Either Blocker (Maybe a)) -> m (Either Blocker (Maybe a))
forall a b. (a -> b) -> a -> b
$
  VerboseKey
-> Int
-> VerboseKey
-> m (Either Blocker (Maybe a))
-> m (Either Blocker (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 (Either Blocker (Maybe a)) -> m (Either Blocker (Maybe a)))
-> m (Either Blocker (Maybe a)) -> m (Either Blocker (Maybe a))
forall a b. (a -> b) -> a -> b
$ do
  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
  pid <- useR stFreshProblemId
  nid <- useR stFreshNameId
  let frsh = Int -> ProblemId -> NameId -> FreshThings
FreshThings Int
i ProblemId
pid NameId
nid
  result <- fst <$> runStateT (runExceptT m) frsh
  case 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"
         Either Blocker (Maybe a) -> m (Either Blocker (Maybe a))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either Blocker (Maybe a) -> m (Either Blocker (Maybe a)))
-> Either Blocker (Maybe a) -> m (Either Blocker (Maybe a))
forall a b. (a -> b) -> a -> b
$ Maybe a -> Either Blocker (Maybe a)
forall a b. b -> Either a b
Right 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
         Either Blocker (Maybe a) -> m (Either Blocker (Maybe a))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either Blocker (Maybe a) -> m (Either Blocker (Maybe a)))
-> Either Blocker (Maybe a) -> m (Either Blocker (Maybe a))
forall a b. (a -> b) -> a -> b
$ Blocker -> Either Blocker (Maybe a)
forall a b. a -> Either a b
Left Blocker
block
    Left TypeError{}         -> do
      TCMT IO Doc -> m ()
forall {m :: * -> *}. MonadDebug m => TCMT IO Doc -> m ()
debugResult TCMT IO Doc
"type error"
      Either Blocker (Maybe a) -> m (Either Blocker (Maybe a))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either Blocker (Maybe a) -> m (Either Blocker (Maybe a)))
-> Either Blocker (Maybe a) -> m (Either Blocker (Maybe a))
forall a b. (a -> b) -> a -> b
$ Maybe a -> Either Blocker (Maybe a)
forall a b. b -> Either a b
Right Maybe a
forall a. Maybe a
Nothing
    Left GenericException{}  -> m (Either Blocker (Maybe a))
forall a. HasCallStack => a
__IMPOSSIBLE__
    Left IOException{}       -> m (Either Blocker (Maybe a))
forall a. HasCallStack => a
__IMPOSSIBLE__
    Left ParserError{}       -> m (Either Blocker (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"
      Either Blocker (Maybe a) -> m (Either Blocker (Maybe a))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either Blocker (Maybe a) -> m (Either Blocker (Maybe a)))
-> Either Blocker (Maybe a) -> m (Either Blocker (Maybe a))
forall a b. (a -> b) -> a -> b
$ Maybe a -> Either Blocker (Maybe a)
forall a b. b -> Either a b
Right (Maybe a -> Either Blocker (Maybe a))
-> Maybe a -> Either Blocker (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 => 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 => 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
    bv <- Term -> PureConversionT m (Maybe Blocker)
forall t (m :: * -> *).
(Reduce t, IsMeta t, MonadReduce m) =>
t -> m (Maybe Blocker)
isBlocked Term
v
    let 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
    patternViolation blocker
  assignTerm' :: MonadMetaSolver (PureConversionT m) =>
MetaId -> [Arg VerboseKey] -> Term -> PureConversionT m ()
assignTerm' MetaId
m [Arg VerboseKey]
_ Term
v = do
    bv <- Term -> PureConversionT m (Maybe Blocker)
forall t (m :: * -> *).
(Reduce t, IsMeta t, MonadReduce m) =>
t -> m (Maybe Blocker)
isBlocked Term
v
    let 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
    patternViolation 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 => 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
    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
    fst <$> runStateT m concNames

instance PureTCM 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
    i <- (FreshThings -> ProblemId) -> PureConversionT m ProblemId
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets FreshThings -> ProblemId
freshProblemId
    modify $ \FreshThings
f -> FreshThings
f { freshProblemId = i + 1 }
    return i

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

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