{-# OPTIONS_GHC -Wunused-imports #-}
{-# LANGUAGE NondecreasingIndentation #-}
module Agda.TypeChecking.MetaVars.Occurs where
import Control.Monad
import Control.Monad.Except
import Control.Monad.Reader
import Data.Foldable (traverse_)
import Data.Functor
import Data.Monoid
import Data.Set (Set)
import qualified Data.Set as Set
import qualified Data.IntMap as IntMap
import qualified Data.IntSet as IntSet
import Data.IntSet (IntSet)
import qualified Agda.Benchmarking as Bench
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.Syntax.Internal.MetaVars
import Agda.TypeChecking.Constraints
import Agda.TypeChecking.Monad
import qualified Agda.TypeChecking.Monad.Benchmark as Bench
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Free
import Agda.TypeChecking.Free.Lazy
import Agda.TypeChecking.Free.Reduce
import Agda.TypeChecking.ProjectionLike
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Datatypes
import Agda.TypeChecking.Records
import {-# SOURCE #-} Agda.TypeChecking.MetaVars
import Agda.Interaction.Options (optFirstOrder)
import Agda.Utils.Either
import Agda.Utils.Function
import Agda.Utils.Lens
import Agda.Utils.List (downFrom)
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Permutation
import Agda.Syntax.Common.Pretty (prettyShow)
import Agda.Utils.Size
import Agda.Utils.Impossible
modifyOccursCheckDefs :: (Set QName -> Set QName) -> TCM ()
modifyOccursCheckDefs :: (Set QName -> Set QName) -> TCM ()
modifyOccursCheckDefs Set QName -> Set QName
f = (Set QName -> f (Set QName)) -> TCState -> f TCState
Lens' TCState (Set QName)
stOccursCheckDefs Lens' TCState (Set QName) -> (Set QName -> Set QName) -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> (a -> a) -> m ()
`modifyTCLens` Set QName -> Set QName
f
initOccursCheck :: MetaVariable -> TCM ()
initOccursCheck :: MetaVariable -> TCM ()
initOccursCheck MetaVariable
mv = (Set QName -> Set QName) -> TCM ()
modifyOccursCheckDefs ((Set QName -> Set QName) -> TCM ())
-> (Set QName -> Set QName -> Set QName) -> Set QName -> TCM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set QName -> Set QName -> Set QName
forall a b. a -> b -> a
const (Set QName -> TCM ()) -> TCMT IO (Set QName) -> TCM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<
if (MetaInfo -> RunMetaOccursCheck
miMetaOccursCheck (MetaVariable -> MetaInfo
mvInfo MetaVariable
mv) RunMetaOccursCheck -> RunMetaOccursCheck -> Bool
forall a. Eq a => a -> a -> Bool
== RunMetaOccursCheck
DontRunMetaOccursCheck)
then do
[Char] -> Nat -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> [Char] -> m ()
reportSLn [Char]
"tc.meta.occurs" Nat
20 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$
[Char]
"initOccursCheck: we do not look into definitions"
Set QName -> TCMT IO (Set QName)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Set QName
forall a. Set a
Set.empty
else do
[Char] -> Nat -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> [Char] -> m ()
reportSLn [Char]
"tc.meta.occurs" Nat
20 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$
[Char]
"initOccursCheck: we look into the following definitions:"
mb <- (TCEnv -> Maybe MutualId) -> TCMT IO (Maybe MutualId)
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Maybe MutualId
envMutualBlock
case mb of
Maybe MutualId
Nothing -> do
[Char] -> Nat -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> [Char] -> m ()
reportSLn [Char]
"tc.meta.occurs" Nat
20 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$ [Char]
"(none)"
Set QName -> TCMT IO (Set QName)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Set QName
forall a. Set a
Set.empty
Just MutualId
b -> do
ds <- MutualBlock -> Set QName
mutualNames (MutualBlock -> Set QName)
-> TCMT IO MutualBlock -> TCMT IO (Set QName)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MutualId -> TCMT IO MutualBlock
forall (tcm :: * -> *).
ReadTCState tcm =>
MutualId -> tcm MutualBlock
lookupMutualBlock MutualId
b
reportSDoc "tc.meta.occurs" 20 $ sep $ map prettyTCM $ Set.toList ds
return ds
defNeedsChecking :: QName -> TCM Bool
defNeedsChecking :: QName -> TCM Bool
defNeedsChecking QName
d = QName -> Set QName -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member QName
d (Set QName -> Bool) -> TCMT IO (Set QName) -> TCM Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' TCState (Set QName) -> TCMT IO (Set QName)
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC (Set QName -> f (Set QName)) -> TCState -> f TCState
Lens' TCState (Set QName)
stOccursCheckDefs
tallyDef :: QName -> TCM ()
tallyDef :: QName -> TCM ()
tallyDef QName
d = (Set QName -> Set QName) -> TCM ()
modifyOccursCheckDefs ((Set QName -> Set QName) -> TCM ())
-> (Set QName -> Set QName) -> TCM ()
forall a b. (a -> b) -> a -> b
$ QName -> Set QName -> Set QName
forall a. Ord a => a -> Set a -> Set a
Set.delete QName
d
data =
{ OccursExtra -> UnfoldStrategy
occUnfold :: UnfoldStrategy
, OccursExtra -> VarMap
occVars :: VarMap
, OccursExtra -> MetaId
occMeta :: MetaId
, OccursExtra -> Nat
occCxtSize :: Nat
}
type OccursCtx = FreeEnv' () OccursExtra AllowedVar
type OccursM = ReaderT OccursCtx TCM
type AllowedVar = Modality -> All
instance IsVarSet () AllowedVar where
withVarOcc :: VarOcc' () -> AllowedVar -> AllowedVar
withVarOcc VarOcc' ()
o AllowedVar
f = AllowedVar
f AllowedVar -> (Modality -> Modality) -> AllowedVar
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Modality -> Modality -> Modality
composeModality (VarOcc' () -> Modality
forall a. LensModality a => a -> Modality
getModality VarOcc' ()
o)
variableCheck :: VarMap -> Maybe Variable -> AllowedVar
variableCheck :: VarMap -> Maybe Nat -> AllowedVar
variableCheck VarMap
xs Maybe Nat
mi Modality
q = Bool -> All
All (Bool -> All) -> Bool -> All
forall a b. (a -> b) -> a -> b
$
Maybe Nat -> Bool -> (Nat -> Bool) -> Bool
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe Nat
mi Bool
True ((Nat -> Bool) -> Bool) -> (Nat -> Bool) -> Bool
forall a b. (a -> b) -> a -> b
$ \ Nat
i ->
Maybe (VarOcc' MetaSet)
-> Bool -> (VarOcc' MetaSet -> Bool) -> Bool
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe (Nat -> VarMap -> Maybe (VarOcc' MetaSet)
forall a. Nat -> VarMap' a -> Maybe (VarOcc' a)
lookupVarMap Nat
i VarMap
xs) Bool
False ((VarOcc' MetaSet -> Bool) -> Bool)
-> (VarOcc' MetaSet -> Bool) -> Bool
forall a b. (a -> b) -> a -> b
$ \ VarOcc' MetaSet
o ->
VarOcc' MetaSet -> Modality
forall a. LensModality a => a -> Modality
getModality VarOcc' MetaSet
o Modality -> Modality -> Bool
`moreUsableModality` Modality
q
definitionCheck :: QName -> OccursM ()
definitionCheck :: QName -> OccursM ()
definitionCheck QName
d = do
cxt <- ReaderT OccursCtx (TCMT IO) OccursCtx
forall r (m :: * -> *). MonadReader r m => m r
ask
let irr = OccursCtx -> Bool
forall a. LensRelevance a => a -> Bool
isIrrelevant OccursCtx
cxt
er = OccursCtx -> Bool
forall a. LensQuantity a => a -> Bool
hasQuantity0 OccursCtx
cxt
m = OccursExtra -> MetaId
occMeta (OccursExtra -> MetaId) -> OccursExtra -> MetaId
forall a b. (a -> b) -> a -> b
$ OccursCtx -> OccursExtra
forall a b c. FreeEnv' a b c -> b
feExtra OccursCtx
cxt
unless (irr && er) $ getConstInfo' d >>= \case
Left SigError
_ -> do
Blocker -> Nat -> [Char] -> OccursM ()
forall (m :: * -> *) a.
MonadTCM m =>
Blocker -> Nat -> [Char] -> m a
patternViolation' Blocker
alwaysUnblock Nat
35 ([Char] -> OccursM ()) -> [Char] -> OccursM ()
forall a b. (a -> b) -> a -> b
$
[[Char]] -> [Char]
unwords [[Char]
"occursCheck: definition", QName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow QName
d, [Char]
"not in scope" ]
Right Definition
def -> do
let dmod :: Modality
dmod = Definition -> Modality
forall a. LensModality a => a -> Modality
getModality Definition
def
Bool -> OccursM () -> OccursM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Bool
irr Bool -> Bool -> Bool
|| Modality -> Bool
forall a. LensRelevance a => a -> Bool
usableRelevance Modality
dmod) (OccursM () -> OccursM ()) -> OccursM () -> OccursM ()
forall a b. (a -> b) -> a -> b
$ do
[Char] -> Nat -> TCMT IO Doc -> OccursM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.occurs" Nat
35 (TCMT IO Doc -> OccursM ()) -> TCMT IO Doc -> OccursM ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep
[ TCMT IO Doc
"occursCheck: definition"
, QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
d
, TCMT IO Doc
"has relevance"
, [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> TCMT IO Doc)
-> (Relevance -> [Char]) -> Relevance -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Relevance -> [Char]
forall a. Show a => a -> [Char]
show (Relevance -> TCMT IO Doc) -> Relevance -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Modality -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance Modality
dmod
]
Blocker -> TypeError -> OccursM ()
forall a. Blocker -> TypeError -> OccursM a
abort Blocker
neverUnblock (TypeError -> OccursM ()) -> TypeError -> OccursM ()
forall a b. (a -> b) -> a -> b
$ MetaId -> Term -> TypeError
MetaIrrelevantSolution MetaId
m (Term -> TypeError) -> Term -> TypeError
forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Term
Def QName
d []
Bool -> OccursM () -> OccursM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Bool
er Bool -> Bool -> Bool
|| Modality -> Bool
forall a. LensQuantity a => a -> Bool
usableQuantity Modality
dmod) (OccursM () -> OccursM ()) -> OccursM () -> OccursM ()
forall a b. (a -> b) -> a -> b
$ do
[Char] -> Nat -> TCMT IO Doc -> OccursM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.occurs" Nat
35 (TCMT IO Doc -> OccursM ()) -> TCMT IO Doc -> OccursM ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep
[ TCMT IO Doc
"occursCheck: definition"
, QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
d
, TCMT IO Doc
"has quantity"
, [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> TCMT IO Doc)
-> (Quantity -> [Char]) -> Quantity -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Quantity -> [Char]
forall a. Show a => a -> [Char]
show (Quantity -> TCMT IO Doc) -> Quantity -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Modality -> Quantity
forall a. LensQuantity a => a -> Quantity
getQuantity Modality
dmod
]
Blocker -> TypeError -> OccursM ()
forall a. Blocker -> TypeError -> OccursM a
abort Blocker
neverUnblock (TypeError -> OccursM ()) -> TypeError -> OccursM ()
forall a b. (a -> b) -> a -> b
$ MetaId -> Term -> TypeError
MetaErasedSolution MetaId
m (Term -> TypeError) -> Term -> TypeError
forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Term
Def QName
d []
metaCheck :: MetaId -> OccursM MetaId
metaCheck :: MetaId -> OccursM MetaId
metaCheck MetaId
m = do
cxt <- ReaderT OccursCtx (TCMT IO) OccursCtx
forall r (m :: * -> *). MonadReader r m => m r
ask
let rel = OccursCtx -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance OccursCtx
cxt
qnt = OccursCtx -> Quantity
forall a. LensQuantity a => a -> Quantity
getQuantity OccursCtx
cxt
m0 = OccursExtra -> MetaId
occMeta (OccursExtra -> MetaId) -> OccursExtra -> MetaId
forall a b. (a -> b) -> a -> b
$ OccursCtx -> OccursExtra
forall a b c. FreeEnv' a b c -> b
feExtra OccursCtx
cxt
when (m == m0) $ patternViolation' neverUnblock 50 $ "occursCheck failed: Found " ++ prettyShow m
mv <- lookupLocalMeta m
let mmod = MetaVariable -> Modality
forall a. LensModality a => a -> Modality
getModality MetaVariable
mv
mmod' = Relevance -> Modality -> Modality
forall a. LensRelevance a => Relevance -> a -> a
setRelevance Relevance
rel (Modality -> Modality) -> Modality -> Modality
forall a b. (a -> b) -> a -> b
$ Quantity -> Modality -> Modality
forall a. LensQuantity a => Quantity -> a -> a
setQuantity Quantity
qnt (Modality -> Modality) -> Modality -> Modality
forall a b. (a -> b) -> a -> b
$ Modality
mmod
if (mmod `moreUsableModality` mmod') then return m else do
reportSDoc "tc.meta.occurs" 35 $ hsep
[ "occursCheck: meta variable"
, prettyTCM m
, "has relevance"
, text . show $ getRelevance mmod
, "and quantity"
, text . show $ getQuantity mmod
]
allowAssign <- asksTC envAssignMetas
let fail TCMT IO Doc
reason = do
[Char] -> Nat -> TCMT IO Doc -> OccursM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.occurs" Nat
20 (TCMT IO Doc -> OccursM ()) -> TCMT IO Doc -> OccursM ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Meta occurs check found bad relevance"
[Char] -> Nat -> TCMT IO Doc -> OccursM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.occurs" Nat
20 (TCMT IO Doc -> OccursM ()) -> TCMT IO Doc -> OccursM ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"aborting because" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
reason
Blocker -> OccursM ()
forall a. Blocker -> ReaderT OccursCtx (TCMT IO) a
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation (Blocker -> OccursM ()) -> Blocker -> OccursM ()
forall a b. (a -> b) -> a -> b
$ MetaId -> Blocker
unblockOnMeta MetaId
m
when (mvFrozen mv == Frozen) $ fail "meta is frozen"
unless (isOpenMeta $ mvInstantiation mv) $ fail "meta is already solved"
unlessM (asksTC envAssignMetas) $ fail "assigning metas is not allowed here"
whenM (pure (isFlexible cxt) `and2M` (not . optFirstOrder <$> pragmaOptions))
$ fail "occurrence is flexible"
when (isUnguarded cxt) $ fail "occurrence is unguarded"
reportSDoc "tc.meta.occurs" 20 $ "Promoting meta" <+> prettyTCM m <+> "to modality" <+> prettyTCM mmod'
updateMetaVar m $ \ MetaVariable
mv -> MetaVariable
mv { mvInfo = setModality mmod' $ mvInfo mv }
etaExpandListeners m
wakeupConstraints m
return m
allowedVars :: OccursM (Nat -> Bool)
allowedVars :: OccursM (Nat -> Bool)
allowedVars = do
n <- (Nat -> Nat -> Nat)
-> ReaderT OccursCtx (TCMT IO) Nat
-> ReaderT OccursCtx (TCMT IO) Nat
-> ReaderT OccursCtx (TCMT IO) Nat
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (-) ReaderT OccursCtx (TCMT IO) Nat
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Nat
getContextSize ((OccursCtx -> Nat) -> ReaderT OccursCtx (TCMT IO) Nat
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks (OccursExtra -> Nat
occCxtSize (OccursExtra -> Nat)
-> (OccursCtx -> OccursExtra) -> OccursCtx -> Nat
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OccursCtx -> OccursExtra
forall a b c. FreeEnv' a b c -> b
feExtra))
xs <- asks (theVarMap . occVars . feExtra)
return $ \ Nat
i -> Nat
i Nat -> Nat -> Bool
forall a. Ord a => a -> a -> Bool
< Nat
n Bool -> Bool -> Bool
|| (Nat
i Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
n) Nat -> TheVarMap' MetaSet -> Bool
forall a. Nat -> IntMap a -> Bool
`IntMap.member` TheVarMap' MetaSet
xs
data UnfoldStrategy = YesUnfold | NoUnfold
deriving (UnfoldStrategy -> UnfoldStrategy -> Bool
(UnfoldStrategy -> UnfoldStrategy -> Bool)
-> (UnfoldStrategy -> UnfoldStrategy -> Bool) -> Eq UnfoldStrategy
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: UnfoldStrategy -> UnfoldStrategy -> Bool
== :: UnfoldStrategy -> UnfoldStrategy -> Bool
$c/= :: UnfoldStrategy -> UnfoldStrategy -> Bool
/= :: UnfoldStrategy -> UnfoldStrategy -> Bool
Eq, Nat -> UnfoldStrategy -> [Char] -> [Char]
[UnfoldStrategy] -> [Char] -> [Char]
UnfoldStrategy -> [Char]
(Nat -> UnfoldStrategy -> [Char] -> [Char])
-> (UnfoldStrategy -> [Char])
-> ([UnfoldStrategy] -> [Char] -> [Char])
-> Show UnfoldStrategy
forall a.
(Nat -> a -> [Char] -> [Char])
-> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
$cshowsPrec :: Nat -> UnfoldStrategy -> [Char] -> [Char]
showsPrec :: Nat -> UnfoldStrategy -> [Char] -> [Char]
$cshow :: UnfoldStrategy -> [Char]
show :: UnfoldStrategy -> [Char]
$cshowList :: [UnfoldStrategy] -> [Char] -> [Char]
showList :: [UnfoldStrategy] -> [Char] -> [Char]
Show)
defArgs :: OccursM a -> OccursM a
defArgs :: forall a. OccursM a -> OccursM a
defArgs OccursM a
m = (OccursCtx -> UnfoldStrategy)
-> ReaderT OccursCtx (TCMT IO) UnfoldStrategy
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks (OccursExtra -> UnfoldStrategy
occUnfold (OccursExtra -> UnfoldStrategy)
-> (OccursCtx -> OccursExtra) -> OccursCtx -> UnfoldStrategy
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OccursCtx -> OccursExtra
forall a b c. FreeEnv' a b c -> b
feExtra) ReaderT OccursCtx (TCMT IO) UnfoldStrategy
-> (UnfoldStrategy -> OccursM a) -> OccursM a
forall a b.
ReaderT OccursCtx (TCMT IO) a
-> (a -> ReaderT OccursCtx (TCMT IO) b)
-> ReaderT OccursCtx (TCMT IO) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
UnfoldStrategy
NoUnfold -> OccursM a -> OccursM a
forall a. OccursM a -> OccursM a
flexibly OccursM a
m
UnfoldStrategy
YesUnfold -> OccursM a -> OccursM a
forall a. OccursM a -> OccursM a
weakly OccursM a
m
conArgs :: Elims -> OccursM a -> OccursM a
conArgs :: forall a. Elims -> OccursM a -> OccursM a
conArgs Elims
es OccursM a
m = (OccursCtx -> UnfoldStrategy)
-> ReaderT OccursCtx (TCMT IO) UnfoldStrategy
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks (OccursExtra -> UnfoldStrategy
occUnfold (OccursExtra -> UnfoldStrategy)
-> (OccursCtx -> OccursExtra) -> OccursCtx -> UnfoldStrategy
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OccursCtx -> OccursExtra
forall a b c. FreeEnv' a b c -> b
feExtra) ReaderT OccursCtx (TCMT IO) UnfoldStrategy
-> (UnfoldStrategy -> OccursM a) -> OccursM a
forall a b.
ReaderT OccursCtx (TCMT IO) a
-> (a -> ReaderT OccursCtx (TCMT IO) b)
-> ReaderT OccursCtx (TCMT IO) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
UnfoldStrategy
YesUnfold -> OccursM a
m
UnfoldStrategy
NoUnfold | [()] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [ () | IApply{} <- Elims
es ]
-> OccursM a
m
UnfoldStrategy
NoUnfold -> OccursM a -> OccursM a
forall a. OccursM a -> OccursM a
flexibly OccursM a
m
unfoldB :: (Instantiate t, Reduce t) => t -> OccursM (Blocked t)
unfoldB :: forall t. (Instantiate t, Reduce t) => t -> OccursM (Blocked t)
unfoldB t
v = do
unfold <- (OccursCtx -> UnfoldStrategy)
-> ReaderT OccursCtx (TCMT IO) UnfoldStrategy
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks ((OccursCtx -> UnfoldStrategy)
-> ReaderT OccursCtx (TCMT IO) UnfoldStrategy)
-> (OccursCtx -> UnfoldStrategy)
-> ReaderT OccursCtx (TCMT IO) UnfoldStrategy
forall a b. (a -> b) -> a -> b
$ OccursExtra -> UnfoldStrategy
occUnfold (OccursExtra -> UnfoldStrategy)
-> (OccursCtx -> OccursExtra) -> OccursCtx -> UnfoldStrategy
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OccursCtx -> OccursExtra
forall a b c. FreeEnv' a b c -> b
feExtra
rel <- asks feModality
case unfold of
UnfoldStrategy
YesUnfold | Bool -> Bool
not (Modality -> Bool
forall a. LensRelevance a => a -> Bool
isIrrelevant Modality
rel) -> t -> ReaderT OccursCtx (TCMT IO) (Blocked t)
forall a (m :: * -> *).
(Reduce a, MonadReduce m) =>
a -> m (Blocked a)
reduceB t
v
UnfoldStrategy
_ -> t -> Blocked t
forall a t. a -> Blocked' t a
notBlocked (t -> Blocked t)
-> ReaderT OccursCtx (TCMT IO) t
-> ReaderT OccursCtx (TCMT IO) (Blocked t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> t -> ReaderT OccursCtx (TCMT IO) t
forall a (m :: * -> *). (Instantiate a, MonadReduce m) => a -> m a
instantiate t
v
unfold :: (Instantiate t, Reduce t) => t -> OccursM t
unfold :: forall t. (Instantiate t, Reduce t) => t -> OccursM t
unfold t
v = (OccursCtx -> UnfoldStrategy)
-> ReaderT OccursCtx (TCMT IO) UnfoldStrategy
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks (OccursExtra -> UnfoldStrategy
occUnfold (OccursExtra -> UnfoldStrategy)
-> (OccursCtx -> OccursExtra) -> OccursCtx -> UnfoldStrategy
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OccursCtx -> OccursExtra
forall a b c. FreeEnv' a b c -> b
feExtra) ReaderT OccursCtx (TCMT IO) UnfoldStrategy
-> (UnfoldStrategy -> ReaderT OccursCtx (TCMT IO) t)
-> ReaderT OccursCtx (TCMT IO) t
forall a b.
ReaderT OccursCtx (TCMT IO) a
-> (a -> ReaderT OccursCtx (TCMT IO) b)
-> ReaderT OccursCtx (TCMT IO) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
UnfoldStrategy
NoUnfold -> t -> ReaderT OccursCtx (TCMT IO) t
forall a (m :: * -> *). (Instantiate a, MonadReduce m) => a -> m a
instantiate t
v
UnfoldStrategy
YesUnfold -> t -> ReaderT OccursCtx (TCMT IO) t
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce t
v
weakly :: OccursM a -> OccursM a
weakly :: forall a. OccursM a -> OccursM a
weakly = (OccursCtx -> OccursCtx)
-> ReaderT OccursCtx (TCMT IO) a -> ReaderT OccursCtx (TCMT IO) a
forall a.
(OccursCtx -> OccursCtx)
-> ReaderT OccursCtx (TCMT IO) a -> ReaderT OccursCtx (TCMT IO) a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local ((OccursCtx -> OccursCtx)
-> ReaderT OccursCtx (TCMT IO) a -> ReaderT OccursCtx (TCMT IO) a)
-> (OccursCtx -> OccursCtx)
-> ReaderT OccursCtx (TCMT IO) a
-> ReaderT OccursCtx (TCMT IO) a
forall a b. (a -> b) -> a -> b
$ Lens' OccursCtx (FlexRig' ()) -> LensMap OccursCtx (FlexRig' ())
forall o i. Lens' o i -> LensMap o i
over (FlexRig' () -> f (FlexRig' ())) -> OccursCtx -> f OccursCtx
forall o a. LensFlexRig o a => Lens' o (FlexRig' a)
Lens' OccursCtx (FlexRig' ())
lensFlexRig LensMap OccursCtx (FlexRig' ()) -> LensMap OccursCtx (FlexRig' ())
forall a b. (a -> b) -> a -> b
$ FlexRig' () -> FlexRig' () -> FlexRig' ()
forall a. Semigroup a => FlexRig' a -> FlexRig' a -> FlexRig' a
composeFlexRig FlexRig' ()
forall a. FlexRig' a
WeaklyRigid
strongly :: OccursM a -> OccursM a
strongly :: forall a. OccursM a -> OccursM a
strongly = (OccursCtx -> OccursCtx)
-> ReaderT OccursCtx (TCMT IO) a -> ReaderT OccursCtx (TCMT IO) a
forall a.
(OccursCtx -> OccursCtx)
-> ReaderT OccursCtx (TCMT IO) a -> ReaderT OccursCtx (TCMT IO) a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local ((OccursCtx -> OccursCtx)
-> ReaderT OccursCtx (TCMT IO) a -> ReaderT OccursCtx (TCMT IO) a)
-> (OccursCtx -> OccursCtx)
-> ReaderT OccursCtx (TCMT IO) a
-> ReaderT OccursCtx (TCMT IO) a
forall a b. (a -> b) -> a -> b
$ Lens' OccursCtx (FlexRig' ()) -> LensMap OccursCtx (FlexRig' ())
forall o i. Lens' o i -> LensMap o i
over (FlexRig' () -> f (FlexRig' ())) -> OccursCtx -> f OccursCtx
forall o a. LensFlexRig o a => Lens' o (FlexRig' a)
Lens' OccursCtx (FlexRig' ())
lensFlexRig LensMap OccursCtx (FlexRig' ()) -> LensMap OccursCtx (FlexRig' ())
forall a b. (a -> b) -> a -> b
$ \case
FlexRig' ()
WeaklyRigid -> FlexRig' ()
forall a. FlexRig' a
StronglyRigid
FlexRig' ()
Unguarded -> FlexRig' ()
forall a. FlexRig' a
StronglyRigid
FlexRig' ()
ctx -> FlexRig' ()
ctx
flexibly :: OccursM a -> OccursM a
flexibly :: forall a. OccursM a -> OccursM a
flexibly = (OccursCtx -> OccursCtx)
-> ReaderT OccursCtx (TCMT IO) a -> ReaderT OccursCtx (TCMT IO) a
forall a.
(OccursCtx -> OccursCtx)
-> ReaderT OccursCtx (TCMT IO) a -> ReaderT OccursCtx (TCMT IO) a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local ((OccursCtx -> OccursCtx)
-> ReaderT OccursCtx (TCMT IO) a -> ReaderT OccursCtx (TCMT IO) a)
-> (OccursCtx -> OccursCtx)
-> ReaderT OccursCtx (TCMT IO) a
-> ReaderT OccursCtx (TCMT IO) a
forall a b. (a -> b) -> a -> b
$ Lens' OccursCtx (FlexRig' ()) -> LensSet OccursCtx (FlexRig' ())
forall o i. Lens' o i -> LensSet o i
set (FlexRig' () -> f (FlexRig' ())) -> OccursCtx -> f OccursCtx
forall o a. LensFlexRig o a => Lens' o (FlexRig' a)
Lens' OccursCtx (FlexRig' ())
lensFlexRig LensSet OccursCtx (FlexRig' ()) -> LensSet OccursCtx (FlexRig' ())
forall a b. (a -> b) -> a -> b
$ () -> FlexRig' ()
forall a. a -> FlexRig' a
Flexible ()
patternViolation' :: MonadTCM m => Blocker -> Int -> String -> m a
patternViolation' :: forall (m :: * -> *) a.
MonadTCM m =>
Blocker -> Nat -> [Char] -> m a
patternViolation' Blocker
unblock Nat
n [Char]
err = TCM a -> m a
forall a. TCM a -> m a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM a -> m a) -> TCM a -> m a
forall a b. (a -> b) -> a -> b
$ do
[Char] -> Nat -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> [Char] -> m ()
reportSLn [Char]
"tc.meta.occurs" Nat
n [Char]
err
Blocker -> TCM a
forall a. Blocker -> TCMT IO a
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
unblock
abort :: Blocker -> TypeError -> OccursM a
abort :: forall a. Blocker -> TypeError -> OccursM a
abort Blocker
unblock TypeError
err = do
ctx <- ReaderT OccursCtx (TCMT IO) OccursCtx
forall r (m :: * -> *). MonadReader r m => m r
ask
lift $ do
if | isIrrelevant ctx -> soft
| StronglyRigid <- ctx ^. lensFlexRig -> hard
| otherwise -> soft
where
hard :: TCM a
hard = TypeError -> TCM a
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError TypeError
err
soft :: TCM a
soft = Blocker -> Nat -> [Char] -> TCM a
forall (m :: * -> *) a.
MonadTCM m =>
Blocker -> Nat -> [Char] -> m a
patternViolation' Blocker
unblock Nat
70 (TypeError -> [Char]
forall a. Show a => a -> [Char]
show TypeError
err)
class Occurs t where
occurs :: t -> OccursM t
metaOccurs :: MetaId -> t -> TCM ()
default metaOccurs :: (Foldable f, Occurs a, f a ~ t) => MetaId -> t -> TCM ()
metaOccurs = (a -> TCM ()) -> t -> TCM ()
(a -> TCM ()) -> f a -> TCM ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ ((a -> TCM ()) -> t -> TCM ())
-> (MetaId -> a -> TCM ()) -> MetaId -> t -> TCM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MetaId -> a -> TCM ()
forall t. Occurs t => MetaId -> t -> TCM ()
metaOccurs
occurs_ :: (Occurs t, TypeOf t ~ ()) => t -> OccursM t
occurs_ :: forall t. (Occurs t, TypeOf t ~ ()) => t -> OccursM t
occurs_ t
t = t -> OccursM t
forall t. Occurs t => t -> OccursM t
occurs t
t
metaOccurs2 :: (Occurs a, Occurs b) => MetaId -> a -> b -> TCM ()
metaOccurs2 :: forall a b. (Occurs a, Occurs b) => MetaId -> a -> b -> TCM ()
metaOccurs2 MetaId
m a
x b
y = MetaId -> a -> TCM ()
forall t. Occurs t => MetaId -> t -> TCM ()
metaOccurs MetaId
m a
x TCM () -> TCM () -> TCM ()
forall a b. TCMT IO a -> TCMT IO b -> TCMT IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> MetaId -> b -> TCM ()
forall t. Occurs t => MetaId -> t -> TCM ()
metaOccurs MetaId
m b
y
metaOccurs3 :: (Occurs a, Occurs b, Occurs c) => MetaId -> a -> b -> c -> TCM ()
metaOccurs3 :: forall a b c.
(Occurs a, Occurs b, Occurs c) =>
MetaId -> a -> b -> c -> TCM ()
metaOccurs3 MetaId
m a
x b
y c
z = MetaId -> a -> TCM ()
forall t. Occurs t => MetaId -> t -> TCM ()
metaOccurs MetaId
m a
x TCM () -> TCM () -> TCM ()
forall a b. TCMT IO a -> TCMT IO b -> TCMT IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> MetaId -> b -> TCM ()
forall t. Occurs t => MetaId -> t -> TCM ()
metaOccurs MetaId
m b
y TCM () -> TCM () -> TCM ()
forall a b. TCMT IO a -> TCMT IO b -> TCMT IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> MetaId -> c -> TCM ()
forall t. Occurs t => MetaId -> t -> TCM ()
metaOccurs MetaId
m c
z
occursCheck
:: MetaId -> VarMap -> Term -> TCM Term
occursCheck :: MetaId -> VarMap -> Term -> TCM Term
occursCheck MetaId
m VarMap
xs Term
v = Account (BenchPhase (TCMT IO)) -> TCM Term -> TCM Term
forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
Bench.billTo [ BenchPhase (TCMT IO)
Phase
Bench.Typing, BenchPhase (TCMT IO)
Phase
Bench.OccursCheck ] (TCM Term -> TCM Term) -> TCM Term -> TCM Term
forall a b. (a -> b) -> a -> b
$ do
mv <- MetaId -> TCMT IO MetaVariable
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta MetaId
m
n <- getContextSize
reportSDoc "tc.meta.occurs" 65 $ "occursCheck" <+> pretty m <+> text (show xs)
let initEnv UnfoldStrategy
unf = FreeEnv
{ feExtra :: OccursExtra
feExtra = OccursExtra
{ occUnfold :: UnfoldStrategy
occUnfold = UnfoldStrategy
unf
, occVars :: VarMap
occVars = VarMap
xs
, occMeta :: MetaId
occMeta = MetaId
m
, occCxtSize :: Nat
occCxtSize = Nat
n
}
, feFlexRig :: FlexRig' ()
feFlexRig = FlexRig' ()
forall a. FlexRig' a
StronglyRigid
, feModality :: Modality
feModality = MetaVariable -> Modality
forall a. LensModality a => a -> Modality
getModality MetaVariable
mv
, feSingleton :: Maybe Nat -> AllowedVar
feSingleton = VarMap -> Maybe Nat -> AllowedVar
variableCheck VarMap
xs
}
initOccursCheck mv
nicerErrorMessage $ do
(occurs v `runReaderT` initEnv NoUnfold) `catchError` \TCErr
err -> do
case TCErr
err of
PatternErr{} | Bool -> Bool
not (Modality -> Bool
forall a. LensRelevance a => a -> Bool
isIrrelevant (Modality -> Bool) -> Modality -> Bool
forall a b. (a -> b) -> a -> b
$ MetaVariable -> Modality
forall a. LensModality a => a -> Modality
getModality MetaVariable
mv) -> do
MetaVariable -> TCM ()
initOccursCheck MetaVariable
mv
Term -> OccursM Term
forall t. Occurs t => t -> OccursM t
occurs Term
v OccursM Term -> OccursCtx -> TCM Term
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
`runReaderT` UnfoldStrategy -> OccursCtx
initEnv UnfoldStrategy
YesUnfold
TCErr
_ -> TCErr -> TCM Term
forall a. TCErr -> TCMT IO a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError TCErr
err
where
nicerErrorMessage :: TCM a -> TCM a
nicerErrorMessage :: forall a. TCM a -> TCM a
nicerErrorMessage TCM a
f = TCM a
f TCM a -> (TCErr -> TCM a) -> TCM a
forall a. TCMT IO a -> (TCErr -> TCMT IO a) -> TCMT IO a
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \ TCErr
err -> case TCErr
err of
TypeError CallStack
_ TCState
_ Closure TypeError
cl -> case Closure TypeError -> TypeError
forall a. Closure a -> a
clValue Closure TypeError
cl of
MetaOccursInItself{} ->
TypeError -> TCM a
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM a) -> (Doc -> TypeError) -> Doc -> TCM a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError (Doc -> TCM a) -> TCMT IO Doc -> TCM a
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<
[TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep [ [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
"Refuse to construct infinite term by instantiating"
, MetaId -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => MetaId -> m Doc
prettyTCM MetaId
m
, TCMT IO Doc
"to"
, Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM (Term -> TCMT IO Doc) -> TCM Term -> TCMT IO Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Term -> TCM Term
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull Term
v
]
MetaCannotDependOn MetaId
_ Nat
i ->
TCM Bool -> TCM a -> TCM a -> TCM a
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (MetaId -> TCM Bool
forall (m :: * -> *). ReadTCState m => MetaId -> m Bool
isSortMeta MetaId
m TCM Bool -> TCM Bool -> TCM Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`and2M` (Bool -> Bool
not (Bool -> Bool) -> TCM Bool -> TCM Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCM Bool
forall (m :: * -> *). HasOptions m => m Bool
hasUniversePolymorphism))
( TypeError -> TCM a
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM a) -> (Doc -> TypeError) -> Doc -> TCM a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError (Doc -> TCM a) -> TCMT IO Doc -> TCM a
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<
[TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep [ [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
"Cannot instantiate the metavariable"
, MetaId -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => MetaId -> m Doc
prettyTCM MetaId
m
, TCMT IO Doc
"to"
, Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
v
, TCMT IO Doc
"since universe polymorphism is disabled"
]
)
( TypeError -> TCM a
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM a) -> (Doc -> TypeError) -> Doc -> TCM a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError (Doc -> TCM a) -> TCMT IO Doc -> TCM a
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<
[TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep [ [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
"Cannot instantiate the metavariable"
, MetaId -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => MetaId -> m Doc
prettyTCM MetaId
m
, TCMT IO Doc
"to solution"
, Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
v
, TCMT IO Doc
"since it contains the variable"
, Closure TypeError -> (TypeError -> TCMT IO Doc) -> TCMT IO Doc
forall (m :: * -> *) c a b.
(MonadTCEnv m, ReadTCState m, LensClosure c a) =>
c -> (a -> m b) -> m b
enterClosure Closure TypeError
cl ((TypeError -> TCMT IO Doc) -> TCMT IO Doc)
-> (TypeError -> TCMT IO Doc) -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ \TypeError
_ -> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM (Nat -> Elims -> Term
Var Nat
i [])
, TCMT IO Doc
"which is not in scope of the metavariable"
]
)
MetaIrrelevantSolution MetaId
_ Term
_ ->
TypeError -> TCM a
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM a) -> (Doc -> TypeError) -> Doc -> TCM a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError (Doc -> TCM a) -> TCMT IO Doc -> TCM a
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<
[TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep [ [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
"Cannot instantiate the metavariable"
, MetaId -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => MetaId -> m Doc
prettyTCM MetaId
m
, TCMT IO Doc
"to solution"
, Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
v
, TCMT IO Doc
"since (part of) the solution was created in an irrelevant context"
]
MetaErasedSolution MetaId
_ Term
_ ->
TypeError -> TCM a
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM a) -> (Doc -> TypeError) -> Doc -> TCM a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError (Doc -> TCM a) -> TCMT IO Doc -> TCM a
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<
[TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep [ [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
"Cannot instantiate the metavariable"
, MetaId -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => MetaId -> m Doc
prettyTCM MetaId
m
, TCMT IO Doc
"to solution"
, Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
v
, TCMT IO Doc
"since (part of) the solution was created in an erased context"
]
TypeError
_ -> TCErr -> TCM a
forall a. TCErr -> TCMT IO a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError TCErr
err
TCErr
_ -> TCErr -> TCM a
forall a. TCErr -> TCMT IO a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError TCErr
err
instance Occurs Term where
occurs :: Term -> OccursM Term
occurs Term
v = do
vb <- Term -> OccursM (Blocked Term)
forall t. (Instantiate t, Reduce t) => t -> OccursM (Blocked t)
unfoldB Term
v
let block = Blocked Term -> Blocker
forall t a. Blocked' t a -> Blocker
getBlocker Blocked Term
vb
flexIfBlocked = if
| MetaV{} <- Blocked Term -> Term
forall t a. Blocked' t a -> a
ignoreBlocking Blocked Term
vb -> Blocker -> OccursM Term -> OccursM Term
forall (m :: * -> *) a.
(PureTCM m, MonadBlock m) =>
Blocker -> m a -> m a
addOrUnblocker Blocker
block
| Blocker
block Blocker -> Blocker -> Bool
forall a. Eq a => a -> a -> Bool
/= Blocker
neverUnblock -> OccursM Term -> OccursM Term
forall a. OccursM a -> OccursM a
flexibly (OccursM Term -> OccursM Term)
-> (OccursM Term -> OccursM Term) -> OccursM Term -> OccursM Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Blocker -> OccursM Term -> OccursM Term
forall (m :: * -> *) a.
(PureTCM m, MonadBlock m) =>
Blocker -> m a -> m a
addOrUnblocker Blocker
block
| NotBlocked{blockingStatus :: forall t a. Blocked' t a -> NotBlocked' t
blockingStatus = NotBlocked' Term
Underapplied} <- Blocked Term
vb -> OccursM Term -> OccursM Term
forall a. OccursM a -> OccursM a
flexibly
| Bool
otherwise -> OccursM Term -> OccursM Term
forall a. a -> a
id
v <- reduceProjectionLike $ ignoreBlocking vb
flexIfBlocked $ do
ctx <- ask
let m = OccursExtra -> MetaId
occMeta (OccursExtra -> MetaId)
-> (OccursCtx -> OccursExtra) -> OccursCtx -> MetaId
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OccursCtx -> OccursExtra
forall a b c. FreeEnv' a b c -> b
feExtra (OccursCtx -> MetaId) -> OccursCtx -> MetaId
forall a b. (a -> b) -> a -> b
$ OccursCtx
ctx
reportSDoc "tc.meta.occurs" 45 $
text ("occursCheck " ++ prettyShow m ++ " (" ++ show (feFlexRig ctx) ++ ") of ") <+> prettyTCM v
reportSDoc "tc.meta.occurs" 70 $
nest 2 $ pretty v
case v of
Var Nat
i Elims
es -> do
allowed <- All -> Bool
getAll (All -> Bool) -> (AllowedVar -> All) -> AllowedVar -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (AllowedVar -> AllowedVar
forall a b. (a -> b) -> a -> b
$ Modality
unitModality) (AllowedVar -> Bool)
-> ReaderT OccursCtx (TCMT IO) AllowedVar
-> ReaderT OccursCtx (TCMT IO) Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Nat -> ReaderT OccursCtx (TCMT IO) AllowedVar
forall (m :: * -> *) a c b.
(Monad m, IsVarSet a c) =>
Nat -> FreeT a b m c
variable Nat
i
if allowed then Var i <$> weakly (occurs es) else do
reportSDoc "tc.meta.occurs" 35 $ "offending variable: " <+> prettyTCM (var i)
t <- typeOfBV i
reportSDoc "tc.meta.occurs" 35 $ nest 2 $ "of type " <+> prettyTCM t
isST <- typeLevelReductions $ isSingletonType t
reportSDoc "tc.meta.occurs" 35 $ nest 2 $ "(after singleton test)"
case isST of
Maybe Term
Nothing ->
ReaderT OccursCtx (TCMT IO) Bool
-> OccursM Term -> OccursM Term -> OccursM Term
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (((Nat -> Bool) -> Nat -> Bool
forall a b. (a -> b) -> a -> b
$ Nat
i) ((Nat -> Bool) -> Bool)
-> OccursM (Nat -> Bool) -> ReaderT OccursCtx (TCMT IO) Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> OccursM (Nat -> Bool)
allowedVars)
(Blocker -> Nat -> [Char] -> OccursM Term
forall (m :: * -> *) a.
MonadTCM m =>
Blocker -> Nat -> [Char] -> m a
patternViolation' Blocker
neverUnblock Nat
70 ([Char] -> OccursM Term) -> [Char] -> OccursM Term
forall a b. (a -> b) -> a -> b
$ [Char]
"Disallowed var " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Nat -> [Char]
forall a. Show a => a -> [Char]
show Nat
i [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" due to modality/relevance")
(OccursM Term -> OccursM Term
forall a. OccursM a -> OccursM a
strongly (OccursM Term -> OccursM Term) -> OccursM Term -> OccursM Term
forall a b. (a -> b) -> a -> b
$ Blocker -> TypeError -> OccursM Term
forall a. Blocker -> TypeError -> OccursM a
abort Blocker
neverUnblock (TypeError -> OccursM Term) -> TypeError -> OccursM Term
forall a b. (a -> b) -> a -> b
$ MetaId -> Nat -> TypeError
MetaCannotDependOn MetaId
m Nat
i)
(Just Term
sv) -> Term -> OccursM Term
forall a. a -> ReaderT OccursCtx (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> OccursM Term) -> Term -> OccursM Term
forall a b. (a -> b) -> a -> b
$ Term
sv Term -> Elims -> Term
forall t. Apply t => t -> Elims -> t
`applyE` Elims
es
Lam ArgInfo
h Abs Term
f -> do
ArgInfo -> Abs Term -> Term
Lam ArgInfo
h (Abs Term -> Term)
-> ReaderT OccursCtx (TCMT IO) (Abs Term) -> OccursM Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Abs Term -> ReaderT OccursCtx (TCMT IO) (Abs Term)
forall t. Occurs t => t -> OccursM t
occurs Abs Term
f
Level Level
l -> Level -> Term
Level (Level -> Term)
-> ReaderT OccursCtx (TCMT IO) Level -> OccursM Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Level -> ReaderT OccursCtx (TCMT IO) Level
forall t. (Occurs t, TypeOf t ~ ()) => t -> OccursM t
occurs_ Level
l
Lit Literal
l -> Term -> OccursM Term
forall a. a -> ReaderT OccursCtx (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return Term
v
Dummy{} -> Term -> OccursM Term
forall a. a -> ReaderT OccursCtx (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return Term
v
DontCare Term
v -> Term -> Term
dontCare (Term -> Term) -> OccursM Term -> OccursM Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
OccursM Term -> OccursM Term
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
onlyReduceTypes (OccursM Term -> OccursM Term) -> OccursM Term -> OccursM Term
forall a b. (a -> b) -> a -> b
$ Relevance -> OccursM Term -> OccursM Term
forall r (m :: * -> *) o z.
(MonadReader r m, LensRelevance r, LensRelevance o) =>
o -> m z -> m z
underRelevance Relevance
Irrelevant (OccursM Term -> OccursM Term) -> OccursM Term -> OccursM Term
forall a b. (a -> b) -> a -> b
$ Term -> OccursM Term
forall t. Occurs t => t -> OccursM t
occurs Term
v
Def QName
d Elims
es -> do
QName -> OccursM ()
definitionCheck QName
d
QName -> Elims -> Term
Def QName
d (Elims -> Term)
-> ReaderT OccursCtx (TCMT IO) Elims -> OccursM Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> Elims -> ReaderT OccursCtx (TCMT IO) Elims
forall {b}. Occurs b => QName -> b -> ReaderT OccursCtx (TCMT IO) b
occDef QName
d Elims
es
Con ConHead
c ConInfo
ci Elims
vs -> do
QName -> OccursM ()
definitionCheck (ConHead -> QName
conName ConHead
c)
ConHead -> ConInfo -> Elims -> Term
Con ConHead
c ConInfo
ci (Elims -> Term)
-> ReaderT OccursCtx (TCMT IO) Elims -> OccursM Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Elims
-> ReaderT OccursCtx (TCMT IO) Elims
-> ReaderT OccursCtx (TCMT IO) Elims
forall a. Elims -> OccursM a -> OccursM a
conArgs Elims
vs (Elims -> ReaderT OccursCtx (TCMT IO) Elims
forall t. Occurs t => t -> OccursM t
occurs Elims
vs)
Pi Dom Type
a Abs Type
b -> Dom Type -> Abs Type -> Term
Pi (Dom Type -> Abs Type -> Term)
-> ReaderT OccursCtx (TCMT IO) (Dom Type)
-> ReaderT OccursCtx (TCMT IO) (Abs Type -> Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Dom Type -> ReaderT OccursCtx (TCMT IO) (Dom Type)
forall t. (Occurs t, TypeOf t ~ ()) => t -> OccursM t
occurs_ Dom Type
a ReaderT OccursCtx (TCMT IO) (Abs Type -> Term)
-> ReaderT OccursCtx (TCMT IO) (Abs Type) -> OccursM Term
forall a b.
ReaderT OccursCtx (TCMT IO) (a -> b)
-> ReaderT OccursCtx (TCMT IO) a -> ReaderT OccursCtx (TCMT IO) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Abs Type -> ReaderT OccursCtx (TCMT IO) (Abs Type)
forall t. Occurs t => t -> OccursM t
occurs Abs Type
b
Sort Sort
s -> Sort -> Term
Sort (Sort -> Term) -> ReaderT OccursCtx (TCMT IO) Sort -> OccursM Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do Relevance
-> ReaderT OccursCtx (TCMT IO) Sort
-> ReaderT OccursCtx (TCMT IO) Sort
forall r (m :: * -> *) o z.
(MonadReader r m, LensRelevance r, LensRelevance o) =>
o -> m z -> m z
underRelevance Relevance
NonStrict (ReaderT OccursCtx (TCMT IO) Sort
-> ReaderT OccursCtx (TCMT IO) Sort)
-> ReaderT OccursCtx (TCMT IO) Sort
-> ReaderT OccursCtx (TCMT IO) Sort
forall a b. (a -> b) -> a -> b
$ Sort -> ReaderT OccursCtx (TCMT IO) Sort
forall t. (Occurs t, TypeOf t ~ ()) => t -> OccursM t
occurs_ Sort
s
MetaV MetaId
m' Elims
es -> do
m' <- MetaId -> OccursM MetaId
metaCheck MetaId
m'
(MetaV m' <$> do flexibly $ occurs es) `catchError` \ TCErr
err -> do
ctx <- ReaderT OccursCtx (TCMT IO) OccursCtx
forall r (m :: * -> *). MonadReader r m => m r
ask
reportSDoc "tc.meta.kill" 25 $ vcat
[ text $ "error during flexible occurs check, we are " ++ show (ctx ^. lensFlexRig)
, text $ show err
]
case err of
PatternErr{} | Bool -> Bool
not (OccursCtx -> Bool
forall o a. LensFlexRig o a => o -> Bool
isFlexible OccursCtx
ctx) -> do
[Char] -> Nat -> [Char] -> OccursM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> [Char] -> m ()
reportSLn [Char]
"tc.meta.kill" Nat
20 ([Char] -> OccursM ()) -> [Char] -> OccursM ()
forall a b. (a -> b) -> a -> b
$
[Char]
"oops, pattern violation for " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ MetaId -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow MetaId
m'
Maybe [Arg Term]
-> OccursM Term -> ([Arg Term] -> OccursM Term) -> OccursM Term
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe (Elims -> Maybe [Arg Term]
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es) (TCErr -> OccursM Term
forall a. TCErr -> ReaderT OccursCtx (TCMT IO) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError TCErr
err) (([Arg Term] -> OccursM Term) -> OccursM Term)
-> ([Arg Term] -> OccursM Term) -> OccursM Term
forall a b. (a -> b) -> a -> b
$ \ [Arg Term]
vs -> do
killResult <- TCM PruneResult -> ReaderT OccursCtx (TCMT IO) PruneResult
forall (m :: * -> *) a. Monad m => m a -> ReaderT OccursCtx m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM PruneResult -> ReaderT OccursCtx (TCMT IO) PruneResult)
-> ((Nat -> Bool) -> TCM PruneResult)
-> (Nat -> Bool)
-> ReaderT OccursCtx (TCMT IO) PruneResult
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MetaId -> [Arg Term] -> (Nat -> Bool) -> TCM PruneResult
forall (m :: * -> *).
(PureTCM m, MonadMetaSolver m) =>
MetaId -> [Arg Term] -> (Nat -> Bool) -> m PruneResult
prune MetaId
m' [Arg Term]
vs ((Nat -> Bool) -> ReaderT OccursCtx (TCMT IO) PruneResult)
-> OccursM (Nat -> Bool) -> ReaderT OccursCtx (TCMT IO) PruneResult
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< OccursM (Nat -> Bool)
allowedVars
if (killResult == PrunedEverything) then do
reportSDoc "tc.meta.prune" 40 $ "Pruned everything"
v' <- instantiate (MetaV m' es)
occurs v'
else throwError err
TCErr
_ -> TCErr -> OccursM Term
forall a. TCErr -> ReaderT OccursCtx (TCMT IO) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError TCErr
err
where
occDef :: QName -> b -> ReaderT OccursCtx (TCMT IO) b
occDef QName
d b
vs = do
m <- (OccursCtx -> MetaId) -> OccursM MetaId
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks (OccursExtra -> MetaId
occMeta (OccursExtra -> MetaId)
-> (OccursCtx -> OccursExtra) -> OccursCtx -> MetaId
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OccursCtx -> OccursExtra
forall a b c. FreeEnv' a b c -> b
feExtra)
lift $ metaOccurs m d
ifM (liftTCM $ isJust <$> isDataOrRecordType d)
(occurs vs)
(defArgs $ occurs vs)
metaOccurs :: MetaId -> Term -> TCM ()
metaOccurs MetaId
m Term
v = do
v <- Term -> TCM Term
forall a (m :: * -> *). (Instantiate a, MonadReduce m) => a -> m a
instantiate Term
v
case v of
Var Nat
i Elims
vs -> MetaId -> Elims -> TCM ()
forall t. Occurs t => MetaId -> t -> TCM ()
metaOccurs MetaId
m Elims
vs
Lam ArgInfo
h Abs Term
f -> MetaId -> Abs Term -> TCM ()
forall t. Occurs t => MetaId -> t -> TCM ()
metaOccurs MetaId
m Abs Term
f
Level Level
l -> MetaId -> Level -> TCM ()
forall t. Occurs t => MetaId -> t -> TCM ()
metaOccurs MetaId
m Level
l
Lit Literal
l -> () -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
Dummy{} -> () -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
DontCare Term
v -> MetaId -> Term -> TCM ()
forall t. Occurs t => MetaId -> t -> TCM ()
metaOccurs MetaId
m Term
v
Def QName
d Elims
vs -> MetaId -> QName -> Elims -> TCM ()
forall a b. (Occurs a, Occurs b) => MetaId -> a -> b -> TCM ()
metaOccurs2 MetaId
m QName
d Elims
vs
Con ConHead
c ConInfo
_ Elims
vs -> MetaId -> Elims -> TCM ()
forall t. Occurs t => MetaId -> t -> TCM ()
metaOccurs MetaId
m Elims
vs
Pi Dom Type
a Abs Type
b -> MetaId -> Dom Type -> Abs Type -> TCM ()
forall a b. (Occurs a, Occurs b) => MetaId -> a -> b -> TCM ()
metaOccurs2 MetaId
m Dom Type
a Abs Type
b
Sort Sort
s -> MetaId -> Sort -> TCM ()
forall t. Occurs t => MetaId -> t -> TCM ()
metaOccurs MetaId
m Sort
s
MetaV MetaId
m' Elims
vs | MetaId
m MetaId -> MetaId -> Bool
forall a. Eq a => a -> a -> Bool
== MetaId
m' -> Blocker -> Nat -> [Char] -> TCM ()
forall (m :: * -> *) a.
MonadTCM m =>
Blocker -> Nat -> [Char] -> m a
patternViolation' Blocker
neverUnblock Nat
50 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$ [Char]
"Found occurrence of " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ MetaId -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow MetaId
m
| Bool
otherwise -> Blocker -> TCM () -> TCM ()
forall (m :: * -> *) a.
(PureTCM m, MonadBlock m) =>
Blocker -> m a -> m a
addOrUnblocker (MetaId -> Blocker
unblockOnMeta MetaId
m') (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ MetaId -> Elims -> TCM ()
forall t. Occurs t => MetaId -> t -> TCM ()
metaOccurs MetaId
m Elims
vs
instance Occurs QName where
occurs :: QName -> OccursM QName
occurs QName
d = OccursM QName
forall a. HasCallStack => a
__IMPOSSIBLE__
metaOccurs :: MetaId -> QName -> TCM ()
metaOccurs MetaId
m QName
d = TCM Bool -> TCM () -> TCM ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM (QName -> TCM Bool
defNeedsChecking QName
d) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
QName -> TCM ()
tallyDef QName
d
[Char] -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.occurs" Nat
30 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Checking for occurrences in " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
d
MetaId -> QName -> TCM ()
metaOccursQName MetaId
m QName
d
metaOccursQName :: MetaId -> QName -> TCM ()
metaOccursQName :: MetaId -> QName -> TCM ()
metaOccursQName MetaId
m QName
x = MetaId -> Defn -> TCM ()
forall t. Occurs t => MetaId -> t -> TCM ()
metaOccurs MetaId
m (Defn -> TCM ()) -> (Definition -> Defn) -> Definition -> TCM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> Defn
theDef (Definition -> TCM ()) -> TCMT IO Definition -> TCM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
TCMT IO Definition -> TCMT IO Definition
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
ignoreAbstractMode (TCMT IO Definition -> TCMT IO Definition)
-> TCMT IO Definition -> TCMT IO Definition
forall a b. (a -> b) -> a -> b
$ QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
x
instance Occurs Defn where
occurs :: Defn -> OccursM Defn
occurs Defn
def = OccursM Defn
forall a. HasCallStack => a
__IMPOSSIBLE__
metaOccurs :: MetaId -> Defn -> TCM ()
metaOccurs MetaId
m Axiom{} = () -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
metaOccurs MetaId
m DataOrRecSig{} = () -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
metaOccurs MetaId
m Function{ funClauses :: Defn -> [Clause]
funClauses = [Clause]
cls } = (Clause -> TCM ()) -> [Clause] -> TCM ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ (MetaId -> Clause -> TCM ()
forall t. Occurs t => MetaId -> t -> TCM ()
metaOccurs MetaId
m) [Clause]
cls
metaOccurs MetaId
m Datatype{ dataCons :: Defn -> [QName]
dataCons = [QName]
cs } = (QName -> TCM ()) -> [QName] -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (MetaId -> QName -> TCM ()
metaOccursQName MetaId
m) [QName]
cs
metaOccurs MetaId
m Record{ recConHead :: Defn -> ConHead
recConHead = ConHead
c } = MetaId -> QName -> TCM ()
metaOccursQName MetaId
m (QName -> TCM ()) -> QName -> TCM ()
forall a b. (a -> b) -> a -> b
$ ConHead -> QName
conName ConHead
c
metaOccurs MetaId
m Constructor{} = () -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
metaOccurs MetaId
m Primitive{} = () -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
metaOccurs MetaId
m PrimitiveSort{} = TCM ()
forall a. HasCallStack => a
__IMPOSSIBLE__
metaOccurs MetaId
m AbstractDefn{} = TCM ()
forall a. HasCallStack => a
__IMPOSSIBLE__
metaOccurs MetaId
m GeneralizableVar{} = TCM ()
forall a. HasCallStack => a
__IMPOSSIBLE__
instance Occurs Clause where
occurs :: Clause -> OccursM Clause
occurs Clause
cl = OccursM Clause
forall a. HasCallStack => a
__IMPOSSIBLE__
metaOccurs :: MetaId -> Clause -> TCM ()
metaOccurs MetaId
m Clause
cl = Maybe Term -> (Term -> TCM ()) -> TCM ()
forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
whenJust (Clause -> Maybe Term
clauseBody Clause
cl) ((Term -> TCM ()) -> TCM ()) -> (Term -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ MetaId -> Term -> TCM ()
forall t. Occurs t => MetaId -> t -> TCM ()
metaOccurs MetaId
m
instance Occurs Level where
occurs :: Level -> ReaderT OccursCtx (TCMT IO) Level
occurs (Max Integer
n [PlusLevel' Term]
as) = Integer -> [PlusLevel' Term] -> Level
forall t. Integer -> [PlusLevel' t] -> Level' t
Max Integer
n ([PlusLevel' Term] -> Level)
-> ReaderT OccursCtx (TCMT IO) [PlusLevel' Term]
-> ReaderT OccursCtx (TCMT IO) Level
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (PlusLevel' Term -> ReaderT OccursCtx (TCMT IO) (PlusLevel' Term))
-> [PlusLevel' Term]
-> ReaderT OccursCtx (TCMT IO) [PlusLevel' Term]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse PlusLevel' Term -> ReaderT OccursCtx (TCMT IO) (PlusLevel' Term)
forall t. (Occurs t, TypeOf t ~ ()) => t -> OccursM t
occurs_ [PlusLevel' Term]
as
metaOccurs :: MetaId -> Level -> TCM ()
metaOccurs MetaId
m (Max Integer
_ [PlusLevel' Term]
as) =
Blocker -> TCM () -> TCM ()
forall (m :: * -> *) a.
(PureTCM m, MonadBlock m) =>
Blocker -> m a -> m a
addOrUnblocker ([PlusLevel' Term] -> Blocker
forall t. AllMetas t => t -> Blocker
unblockOnAnyMetaIn [PlusLevel' Term]
as) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ (PlusLevel' Term -> TCM ()) -> [PlusLevel' Term] -> TCM ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ (MetaId -> PlusLevel' Term -> TCM ()
forall t. Occurs t => MetaId -> t -> TCM ()
metaOccurs MetaId
m) [PlusLevel' Term]
as
instance Occurs PlusLevel where
occurs :: PlusLevel' Term -> ReaderT OccursCtx (TCMT IO) (PlusLevel' Term)
occurs (Plus Integer
n Term
l) = do
Integer -> Term -> PlusLevel' Term
forall t. Integer -> t -> PlusLevel' t
Plus Integer
n (Term -> PlusLevel' Term)
-> OccursM Term -> ReaderT OccursCtx (TCMT IO) (PlusLevel' Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> OccursM Term
forall t. Occurs t => t -> OccursM t
occurs Term
l
metaOccurs :: MetaId -> PlusLevel' Term -> TCM ()
metaOccurs MetaId
m (Plus Integer
n Term
l) = MetaId -> Term -> TCM ()
forall t. Occurs t => MetaId -> t -> TCM ()
metaOccurs MetaId
m Term
l
instance Occurs Type where
occurs :: Type -> ReaderT OccursCtx (TCMT IO) Type
occurs (El Sort
s Term
v) = Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El (Sort -> Term -> Type)
-> ReaderT OccursCtx (TCMT IO) Sort
-> ReaderT OccursCtx (TCMT IO) (Term -> Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sort -> ReaderT OccursCtx (TCMT IO) Sort
forall t. (Occurs t, TypeOf t ~ ()) => t -> OccursM t
occurs_ Sort
s ReaderT OccursCtx (TCMT IO) (Term -> Type)
-> OccursM Term -> ReaderT OccursCtx (TCMT IO) Type
forall a b.
ReaderT OccursCtx (TCMT IO) (a -> b)
-> ReaderT OccursCtx (TCMT IO) a -> ReaderT OccursCtx (TCMT IO) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term -> OccursM Term
forall t. Occurs t => t -> OccursM t
occurs Term
v
metaOccurs :: MetaId -> Type -> TCM ()
metaOccurs MetaId
m (El Sort
s Term
v) = MetaId -> Sort -> Term -> TCM ()
forall a b. (Occurs a, Occurs b) => MetaId -> a -> b -> TCM ()
metaOccurs2 MetaId
m Sort
s Term
v
instance Occurs Sort where
occurs :: Sort -> ReaderT OccursCtx (TCMT IO) Sort
occurs Sort
s = do
Sort -> ReaderT OccursCtx (TCMT IO) Sort
forall t. (Instantiate t, Reduce t) => t -> OccursM t
unfold Sort
s ReaderT OccursCtx (TCMT IO) Sort
-> (Sort -> ReaderT OccursCtx (TCMT IO) Sort)
-> ReaderT OccursCtx (TCMT IO) Sort
forall a b.
ReaderT OccursCtx (TCMT IO) a
-> (a -> ReaderT OccursCtx (TCMT IO) b)
-> ReaderT OccursCtx (TCMT IO) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
PiSort Dom' Term Term
a Sort
s1 Abs Sort
s2 -> do
s1' <- ReaderT OccursCtx (TCMT IO) Sort
-> ReaderT OccursCtx (TCMT IO) Sort
forall a. OccursM a -> OccursM a
flexibly (ReaderT OccursCtx (TCMT IO) Sort
-> ReaderT OccursCtx (TCMT IO) Sort)
-> ReaderT OccursCtx (TCMT IO) Sort
-> ReaderT OccursCtx (TCMT IO) Sort
forall a b. (a -> b) -> a -> b
$ Sort -> ReaderT OccursCtx (TCMT IO) Sort
forall t. (Occurs t, TypeOf t ~ ()) => t -> OccursM t
occurs_ Sort
s1
a' <- (a $>) <$> do flexibly $ occurs (unDom a)
s2' <- mapAbstraction (El s1' <$> a') (flexibly . underBinder . occurs_) s2
return $ PiSort a' s1' s2'
FunSort Sort
s1 Sort
s2 -> Sort -> Sort -> Sort
forall t. Sort' t -> Sort' t -> Sort' t
FunSort (Sort -> Sort -> Sort)
-> ReaderT OccursCtx (TCMT IO) Sort
-> ReaderT OccursCtx (TCMT IO) (Sort -> Sort)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ReaderT OccursCtx (TCMT IO) Sort
-> ReaderT OccursCtx (TCMT IO) Sort
forall a. OccursM a -> OccursM a
flexibly (Sort -> ReaderT OccursCtx (TCMT IO) Sort
forall t. (Occurs t, TypeOf t ~ ()) => t -> OccursM t
occurs_ Sort
s1) ReaderT OccursCtx (TCMT IO) (Sort -> Sort)
-> ReaderT OccursCtx (TCMT IO) Sort
-> ReaderT OccursCtx (TCMT IO) Sort
forall a b.
ReaderT OccursCtx (TCMT IO) (a -> b)
-> ReaderT OccursCtx (TCMT IO) a -> ReaderT OccursCtx (TCMT IO) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ReaderT OccursCtx (TCMT IO) Sort
-> ReaderT OccursCtx (TCMT IO) Sort
forall a. OccursM a -> OccursM a
flexibly (Sort -> ReaderT OccursCtx (TCMT IO) Sort
forall t. (Occurs t, TypeOf t ~ ()) => t -> OccursM t
occurs_ Sort
s2)
Univ Univ
u Level
a -> Univ -> Level -> Sort
forall t. Univ -> Level' t -> Sort' t
Univ Univ
u (Level -> Sort)
-> ReaderT OccursCtx (TCMT IO) Level
-> ReaderT OccursCtx (TCMT IO) Sort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Level -> ReaderT OccursCtx (TCMT IO) Level
forall t. (Occurs t, TypeOf t ~ ()) => t -> OccursM t
occurs_ Level
a
s :: Sort
s@Inf{} -> Sort -> ReaderT OccursCtx (TCMT IO) Sort
forall a. a -> ReaderT OccursCtx (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return Sort
s
s :: Sort
s@Sort
SizeUniv -> Sort -> ReaderT OccursCtx (TCMT IO) Sort
forall a. a -> ReaderT OccursCtx (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return Sort
s
s :: Sort
s@Sort
LockUniv -> Sort -> ReaderT OccursCtx (TCMT IO) Sort
forall a. a -> ReaderT OccursCtx (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return Sort
s
s :: Sort
s@Sort
LevelUniv -> Sort -> ReaderT OccursCtx (TCMT IO) Sort
forall a. a -> ReaderT OccursCtx (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return Sort
s
s :: Sort
s@Sort
IntervalUniv -> Sort -> ReaderT OccursCtx (TCMT IO) Sort
forall a. a -> ReaderT OccursCtx (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return Sort
s
UnivSort Sort
s -> Sort -> Sort
forall t. Sort' t -> Sort' t
UnivSort (Sort -> Sort)
-> ReaderT OccursCtx (TCMT IO) Sort
-> ReaderT OccursCtx (TCMT IO) Sort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do ReaderT OccursCtx (TCMT IO) Sort
-> ReaderT OccursCtx (TCMT IO) Sort
forall a. OccursM a -> OccursM a
flexibly (ReaderT OccursCtx (TCMT IO) Sort
-> ReaderT OccursCtx (TCMT IO) Sort)
-> ReaderT OccursCtx (TCMT IO) Sort
-> ReaderT OccursCtx (TCMT IO) Sort
forall a b. (a -> b) -> a -> b
$ Sort -> ReaderT OccursCtx (TCMT IO) Sort
forall t. (Occurs t, TypeOf t ~ ()) => t -> OccursM t
occurs_ Sort
s
MetaS MetaId
x Elims
es -> do
MetaV x es <- Term -> OccursM Term
forall t. Occurs t => t -> OccursM t
occurs (MetaId -> Elims -> Term
MetaV MetaId
x Elims
es)
return $ MetaS x es
DefS QName
x Elims
es -> do
Def x es <- Term -> OccursM Term
forall t. Occurs t => t -> OccursM t
occurs (QName -> Elims -> Term
Def QName
x Elims
es)
return $ DefS x es
DummyS{} -> Sort -> ReaderT OccursCtx (TCMT IO) Sort
forall a. a -> ReaderT OccursCtx (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return Sort
s
metaOccurs :: MetaId -> Sort -> TCM ()
metaOccurs MetaId
m Sort
s = do
s <- Sort -> TCMT IO Sort
forall a (m :: * -> *). (Instantiate a, MonadReduce m) => a -> m a
instantiate Sort
s
case s of
PiSort Dom' Term Term
a Sort
s1 Abs Sort
s2 -> do
MetaId -> Dom' Term Term -> TCM ()
forall t. Occurs t => MetaId -> t -> TCM ()
metaOccurs MetaId
m Dom' Term Term
a
MetaId -> Sort -> TCM ()
forall t. Occurs t => MetaId -> t -> TCM ()
metaOccurs MetaId
m Sort
s1
MetaId -> Sort -> TCM ()
forall t. Occurs t => MetaId -> t -> TCM ()
metaOccurs MetaId
m (Abs Sort -> Sort
forall a. Subst a => Abs a -> a
absBody Abs Sort
s2)
FunSort Sort
s1 Sort
s2 -> MetaId -> Sort -> Sort -> TCM ()
forall a b. (Occurs a, Occurs b) => MetaId -> a -> b -> TCM ()
metaOccurs2 MetaId
m Sort
s1 Sort
s2
Univ Univ
_ Level
a -> MetaId -> Level -> TCM ()
forall t. Occurs t => MetaId -> t -> TCM ()
metaOccurs MetaId
m Level
a
Inf Univ
_ Integer
_ -> () -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
Sort
SizeUniv -> () -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
Sort
LockUniv -> () -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
Sort
LevelUniv -> () -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
Sort
IntervalUniv -> () -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
UnivSort Sort
s -> MetaId -> Sort -> TCM ()
forall t. Occurs t => MetaId -> t -> TCM ()
metaOccurs MetaId
m Sort
s
MetaS MetaId
x Elims
es -> MetaId -> Term -> TCM ()
forall t. Occurs t => MetaId -> t -> TCM ()
metaOccurs MetaId
m (Term -> TCM ()) -> Term -> TCM ()
forall a b. (a -> b) -> a -> b
$ MetaId -> Elims -> Term
MetaV MetaId
x Elims
es
DefS QName
d Elims
es -> MetaId -> Term -> TCM ()
forall t. Occurs t => MetaId -> t -> TCM ()
metaOccurs MetaId
m (Term -> TCM ()) -> Term -> TCM ()
forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Term
Def QName
d Elims
es
DummyS{} -> () -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
instance Occurs Elims where
occurs :: Elims -> ReaderT OccursCtx (TCMT IO) Elims
occurs [] = Elims -> ReaderT OccursCtx (TCMT IO) Elims
forall a. a -> ReaderT OccursCtx (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return []
occurs (Elim' Term
e:Elims
es) = do
[Char] -> Nat -> TCMT IO Doc -> OccursM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.occurs.elim" Nat
45 (TCMT IO Doc -> OccursM ()) -> TCMT IO Doc -> OccursM ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"occurs" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Elim' Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Elim' Term -> m Doc
prettyTCM Elim' Term
e
[Char] -> Nat -> TCMT IO Doc -> OccursM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.occurs.elim" Nat
70 (TCMT IO Doc -> OccursM ()) -> TCMT IO Doc -> OccursM ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"occurs" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Elim' Term -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Elim' Term
e
e' <- case Elim' Term
e of
(Proj ProjOrigin
o QName
f) -> do
QName -> OccursM ()
definitionCheck QName
f
Elim' Term -> ReaderT OccursCtx (TCMT IO) (Elim' Term)
forall a. a -> ReaderT OccursCtx (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return Elim' Term
e
(Apply Arg Term
u) -> do
u' <- Arg Term -> OccursM (Arg Term)
forall t. Occurs t => t -> OccursM t
occurs Arg Term
u
return (Apply u')
(IApply Term
x Term
y Term
u) -> do
x' <- Term -> OccursM Term
forall t. Occurs t => t -> OccursM t
occurs Term
x
y' <- occurs y
u' <- occurs u
return (IApply x' y' u')
(e':) <$> occurs es
metaOccurs :: MetaId -> Elims -> TCM ()
metaOccurs MetaId
m Elims
es = Elims -> (Elim' Term -> TCM ()) -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ Elims
es ((Elim' Term -> TCM ()) -> TCM ())
-> (Elim' Term -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \case
Proj{} -> () -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
Apply Arg Term
a -> MetaId -> Arg Term -> TCM ()
forall t. Occurs t => MetaId -> t -> TCM ()
metaOccurs MetaId
m Arg Term
a
IApply Term
x Term
y Term
a -> MetaId -> Term -> Term -> Term -> TCM ()
forall a b c.
(Occurs a, Occurs b, Occurs c) =>
MetaId -> a -> b -> c -> TCM ()
metaOccurs3 MetaId
m Term
x Term
y Term
a
instance Occurs (Abs Term) where
occurs :: Abs Term -> ReaderT OccursCtx (TCMT IO) (Abs Term)
occurs (NoAbs [Char]
s Term
x) = [Char] -> Term -> Abs Term
forall a. [Char] -> a -> Abs a
NoAbs [Char]
s (Term -> Abs Term)
-> OccursM Term -> ReaderT OccursCtx (TCMT IO) (Abs Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> OccursM Term
forall t. Occurs t => t -> OccursM t
occurs Term
x
occurs Abs Term
x = (Term -> OccursM Term)
-> Abs Term -> ReaderT OccursCtx (TCMT IO) (Abs Term)
forall a b (m :: * -> *).
(Subst a, Subst b, MonadAddContext m) =>
(a -> m b) -> Abs a -> m (Abs b)
mapAbstraction_ (\Term
body -> OccursM Term -> OccursM Term
forall a b c (m :: * -> *) z.
MonadReader (FreeEnv' a b c) m =>
m z -> m z
underBinder (OccursM Term -> OccursM Term) -> OccursM Term -> OccursM Term
forall a b. (a -> b) -> a -> b
$ Term -> OccursM Term
forall t. Occurs t => t -> OccursM t
occurs Term
body) Abs Term
x
metaOccurs :: MetaId -> Abs Term -> TCM ()
metaOccurs MetaId
m (Abs [Char]
_ Term
x) = MetaId -> Term -> TCM ()
forall t. Occurs t => MetaId -> t -> TCM ()
metaOccurs MetaId
m Term
x
metaOccurs MetaId
m (NoAbs [Char]
_ Term
x) = MetaId -> Term -> TCM ()
forall t. Occurs t => MetaId -> t -> TCM ()
metaOccurs MetaId
m Term
x
instance Occurs (Abs Type) where
occurs :: Abs Type -> ReaderT OccursCtx (TCMT IO) (Abs Type)
occurs (NoAbs [Char]
s Type
x) = [Char] -> Type -> Abs Type
forall a. [Char] -> a -> Abs a
NoAbs [Char]
s (Type -> Abs Type)
-> ReaderT OccursCtx (TCMT IO) Type
-> ReaderT OccursCtx (TCMT IO) (Abs Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> ReaderT OccursCtx (TCMT IO) Type
forall t. (Occurs t, TypeOf t ~ ()) => t -> OccursM t
occurs_ Type
x
occurs Abs Type
x = (Type -> ReaderT OccursCtx (TCMT IO) Type)
-> Abs Type -> ReaderT OccursCtx (TCMT IO) (Abs Type)
forall a b (m :: * -> *).
(Subst a, Subst b, MonadAddContext m) =>
(a -> m b) -> Abs a -> m (Abs b)
mapAbstraction_ (\Type
body -> ReaderT OccursCtx (TCMT IO) Type
-> ReaderT OccursCtx (TCMT IO) Type
forall a b c (m :: * -> *) z.
MonadReader (FreeEnv' a b c) m =>
m z -> m z
underBinder (ReaderT OccursCtx (TCMT IO) Type
-> ReaderT OccursCtx (TCMT IO) Type)
-> ReaderT OccursCtx (TCMT IO) Type
-> ReaderT OccursCtx (TCMT IO) Type
forall a b. (a -> b) -> a -> b
$ Type -> ReaderT OccursCtx (TCMT IO) Type
forall t. (Occurs t, TypeOf t ~ ()) => t -> OccursM t
occurs_ Type
body) Abs Type
x
metaOccurs :: MetaId -> Abs Type -> TCM ()
metaOccurs MetaId
m (Abs [Char]
_ Type
x) = MetaId -> Type -> TCM ()
forall t. Occurs t => MetaId -> t -> TCM ()
metaOccurs MetaId
m Type
x
metaOccurs MetaId
m (NoAbs [Char]
_ Type
x) = MetaId -> Type -> TCM ()
forall t. Occurs t => MetaId -> t -> TCM ()
metaOccurs MetaId
m Type
x
instance Occurs a => Occurs (Arg a) where
occurs :: Arg a -> OccursM (Arg a)
occurs (Arg ArgInfo
info a
v) = ArgInfo -> a -> Arg a
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
info (a -> Arg a) -> ReaderT OccursCtx (TCMT IO) a -> OccursM (Arg a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
Bool
-> (ReaderT OccursCtx (TCMT IO) a -> ReaderT OccursCtx (TCMT IO) a)
-> ReaderT OccursCtx (TCMT IO) a
-> ReaderT OccursCtx (TCMT IO) a
forall b a. IsBool b => b -> (a -> a) -> a -> a
applyWhen (ArgInfo -> Bool
forall a. LensRelevance a => a -> Bool
isIrrelevant ArgInfo
info) ReaderT OccursCtx (TCMT IO) a -> ReaderT OccursCtx (TCMT IO) a
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
onlyReduceTypes (ReaderT OccursCtx (TCMT IO) a -> ReaderT OccursCtx (TCMT IO) a)
-> ReaderT OccursCtx (TCMT IO) a -> ReaderT OccursCtx (TCMT IO) a
forall a b. (a -> b) -> a -> b
$
ArgInfo
-> ReaderT OccursCtx (TCMT IO) a -> ReaderT OccursCtx (TCMT IO) a
forall r (m :: * -> *) o z.
(MonadReader r m, LensModality r, LensModality o) =>
o -> m z -> m z
underModality ArgInfo
info (ReaderT OccursCtx (TCMT IO) a -> ReaderT OccursCtx (TCMT IO) a)
-> ReaderT OccursCtx (TCMT IO) a -> ReaderT OccursCtx (TCMT IO) a
forall a b. (a -> b) -> a -> b
$ a -> ReaderT OccursCtx (TCMT IO) a
forall t. Occurs t => t -> OccursM t
occurs a
v
metaOccurs :: MetaId -> Arg a -> TCM ()
metaOccurs MetaId
m = MetaId -> a -> TCM ()
forall t. Occurs t => MetaId -> t -> TCM ()
metaOccurs MetaId
m (a -> TCM ()) -> (Arg a -> a) -> Arg a -> TCM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg a -> a
forall e. Arg e -> e
unArg
instance Occurs a => Occurs (Dom a) where
occurs :: Occurs a => Dom a -> OccursM (Dom a)
occurs :: Occurs a => Dom a -> OccursM (Dom a)
occurs (Dom ArgInfo
info Maybe NamedName
n Bool
f Maybe Term
t a
x) =
ArgInfo -> Maybe NamedName -> Bool -> Maybe Term -> a -> Dom a
forall t e.
ArgInfo -> Maybe NamedName -> Bool -> Maybe t -> e -> Dom' t e
Dom ArgInfo
info Maybe NamedName
n Bool
f Maybe Term
t (a -> Dom a) -> ReaderT OccursCtx (TCMT IO) a -> OccursM (Dom a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ArgInfo
-> ReaderT OccursCtx (TCMT IO) a -> ReaderT OccursCtx (TCMT IO) a
forall r (m :: * -> *) o a.
(MonadReader r m, LensQuantity r, LensQuantity o) =>
o -> m a -> m a
underQuantity ArgInfo
info (a -> ReaderT OccursCtx (TCMT IO) a
forall t. Occurs t => t -> OccursM t
occurs a
x)
prune
:: (PureTCM m, MonadMetaSolver m)
=> MetaId
-> Args
-> (Nat -> Bool)
-> m PruneResult
prune :: forall (m :: * -> *).
(PureTCM m, MonadMetaSolver m) =>
MetaId -> [Arg Term] -> (Nat -> Bool) -> m PruneResult
prune MetaId
m' [Arg Term]
vs Nat -> Bool
xs = do
m (Either () [Bool])
-> (() -> m PruneResult)
-> ([Bool] -> m PruneResult)
-> m PruneResult
forall (m :: * -> *) a b c.
Monad m =>
m (Either a b) -> (a -> m c) -> (b -> m c) -> m c
caseEitherM (ExceptT () m [Bool] -> m (Either () [Bool])
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (ExceptT () m [Bool] -> m (Either () [Bool]))
-> ExceptT () m [Bool] -> m (Either () [Bool])
forall a b. (a -> b) -> a -> b
$ (Arg Term -> ExceptT () m Bool)
-> [Arg Term] -> ExceptT () m [Bool]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (((Nat -> Bool) -> Term -> ExceptT () m Bool
forall (m :: * -> *).
PureTCM m =>
(Nat -> Bool) -> Term -> ExceptT () m Bool
hasBadRigid Nat -> Bool
xs) (Term -> ExceptT () m Bool)
-> (Arg Term -> Term) -> Arg Term -> ExceptT () m Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg Term -> Term
forall e. Arg e -> e
unArg) [Arg Term]
vs)
(m PruneResult -> () -> m PruneResult
forall a b. a -> b -> a
const (m PruneResult -> () -> m PruneResult)
-> m PruneResult -> () -> m PruneResult
forall a b. (a -> b) -> a -> b
$ PruneResult -> m PruneResult
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return PruneResult
PrunedNothing) (([Bool] -> m PruneResult) -> m PruneResult)
-> ([Bool] -> m PruneResult) -> m PruneResult
forall a b. (a -> b) -> a -> b
$ \ [Bool]
kills -> do
[Char] -> Nat -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.kill" Nat
10 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ TCMT IO Doc
"attempting kills"
, Nat -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ TCMT IO Doc
"m' =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> MetaId -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty MetaId
m'
, TCMT IO Doc
"vs =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList ((Arg Term -> TCMT IO Doc) -> [Arg Term] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Arg Term -> m Doc
prettyTCM [Arg Term]
vs)
, TCMT IO Doc
"kills =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Bool] -> [Char]
forall a. Show a => a -> [Char]
show [Bool]
kills)
]
]
[Bool] -> MetaId -> m PruneResult
forall (m :: * -> *).
MonadMetaSolver m =>
[Bool] -> MetaId -> m PruneResult
killArgs [Bool]
kills MetaId
m'
hasBadRigid
:: PureTCM m
=> (Nat -> Bool)
-> Term
-> ExceptT () m Bool
hasBadRigid :: forall (m :: * -> *).
PureTCM m =>
(Nat -> Bool) -> Term -> ExceptT () m Bool
hasBadRigid Nat -> Bool
xs Term
t = do
let failure :: ExceptT () m a
failure = () -> ExceptT () m a
forall a. () -> ExceptT () m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError ()
tb <- Term -> ExceptT () m (Blocked Term)
forall a (m :: * -> *).
(Reduce a, MonadReduce m) =>
a -> m (Blocked a)
reduceB Term
t
let t = Blocked Term -> Term
forall t a. Blocked' t a -> a
ignoreBlocking Blocked Term
tb
case t of
Var Nat
x Elims
_ -> Bool -> ExceptT () m Bool
forall a. a -> ExceptT () m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> ExceptT () m Bool) -> Bool -> ExceptT () m Bool
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Nat -> Bool
xs Nat
x
Lam ArgInfo
_ Abs Term
v -> ExceptT () m Bool
forall {a}. ExceptT () m a
failure
DontCare Term
v -> (Nat -> Bool) -> Term -> ExceptT () m Bool
forall (m :: * -> *).
PureTCM m =>
(Nat -> Bool) -> Term -> ExceptT () m Bool
hasBadRigid Nat -> Bool
xs Term
v
v :: Term
v@(Def QName
f Elims
es) -> ExceptT () m Bool
-> ExceptT () m Bool -> ExceptT () m Bool -> ExceptT () m Bool
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifNotM (Blocked Term -> QName -> Elims -> ExceptT () m Bool
forall (m :: * -> *) t.
HasConstInfo m =>
Blocked t -> QName -> Elims -> m Bool
isNeutral Blocked Term
tb QName
f Elims
es) ExceptT () m Bool
forall {a}. ExceptT () m a
failure (ExceptT () m Bool -> ExceptT () m Bool)
-> ExceptT () m Bool -> ExceptT () m Bool
forall a b. (a -> b) -> a -> b
$ do
m Bool -> ExceptT () m Bool
forall (m :: * -> *) a. Monad m => m a -> ExceptT () m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m Bool -> ExceptT () m Bool) -> m Bool -> ExceptT () m Bool
forall a b. (a -> b) -> a -> b
$ Elims
es Elims -> (Nat -> Bool) -> m Bool
forall (m :: * -> *) a.
(PureTCM m, AnyRigid a) =>
a -> (Nat -> Bool) -> m Bool
`rigidVarsNotContainedIn` Nat -> Bool
xs
Pi Dom Type
a Abs Type
b -> m Bool -> ExceptT () m Bool
forall (m :: * -> *) a. Monad m => m a -> ExceptT () m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m Bool -> ExceptT () m Bool) -> m Bool -> ExceptT () m Bool
forall a b. (a -> b) -> a -> b
$ (Dom Type
a,Abs Type
b) (Dom Type, Abs Type) -> (Nat -> Bool) -> m Bool
forall (m :: * -> *) a.
(PureTCM m, AnyRigid a) =>
a -> (Nat -> Bool) -> m Bool
`rigidVarsNotContainedIn` Nat -> Bool
xs
Level Level
v -> m Bool -> ExceptT () m Bool
forall (m :: * -> *) a. Monad m => m a -> ExceptT () m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m Bool -> ExceptT () m Bool) -> m Bool -> ExceptT () m Bool
forall a b. (a -> b) -> a -> b
$ Level
v Level -> (Nat -> Bool) -> m Bool
forall (m :: * -> *) a.
(PureTCM m, AnyRigid a) =>
a -> (Nat -> Bool) -> m Bool
`rigidVarsNotContainedIn` Nat -> Bool
xs
Sort Sort
s -> m Bool -> ExceptT () m Bool
forall (m :: * -> *) a. Monad m => m a -> ExceptT () m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m Bool -> ExceptT () m Bool) -> m Bool -> ExceptT () m Bool
forall a b. (a -> b) -> a -> b
$ Sort
s Sort -> (Nat -> Bool) -> m Bool
forall (m :: * -> *) a.
(PureTCM m, AnyRigid a) =>
a -> (Nat -> Bool) -> m Bool
`rigidVarsNotContainedIn` Nat -> Bool
xs
Con ConHead
c ConInfo
_ Elims
es | Just [Arg Term]
args <- Elims -> Maybe [Arg Term]
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es -> do
ExceptT () m Bool
-> ExceptT () m Bool -> ExceptT () m Bool -> ExceptT () m Bool
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (QName -> ExceptT () m Bool
forall (m :: * -> *). HasConstInfo m => QName -> m Bool
isEtaCon (ConHead -> QName
conName ConHead
c))
([Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ([Bool] -> Bool) -> ExceptT () m [Bool] -> ExceptT () m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Arg Term -> ExceptT () m Bool)
-> [Arg Term] -> ExceptT () m [Bool]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ((Nat -> Bool) -> Term -> ExceptT () m Bool
forall (m :: * -> *).
PureTCM m =>
(Nat -> Bool) -> Term -> ExceptT () m Bool
hasBadRigid Nat -> Bool
xs (Term -> ExceptT () m Bool)
-> (Arg Term -> Term) -> Arg Term -> ExceptT () m Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg Term -> Term
forall e. Arg e -> e
unArg) [Arg Term]
args)
ExceptT () m Bool
forall {a}. ExceptT () m a
failure
Con ConHead
c ConInfo
_ Elims
es | Bool
otherwise -> ExceptT () m Bool
forall {a}. ExceptT () m a
failure
Lit{} -> ExceptT () m Bool
forall {a}. ExceptT () m a
failure
MetaV{} -> ExceptT () m Bool
forall {a}. ExceptT () m a
failure
Dummy{} -> Bool -> ExceptT () m Bool
forall a. a -> ExceptT () m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
isNeutral :: (HasConstInfo m) => Blocked t -> QName -> Elims -> m Bool
isNeutral :: forall (m :: * -> *) t.
HasConstInfo m =>
Blocked t -> QName -> Elims -> m Bool
isNeutral Blocked t
b QName
f Elims
es = do
let yes :: m Bool
yes = Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
no :: m Bool
no = Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
def <- QName -> m Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
f
if not (null $ defMatchable def) then no else do
case theDef def of
AbstractDefn{} -> m Bool
yes
Axiom{} -> m Bool
yes
Datatype{} -> m Bool
yes
Record{} -> m Bool
yes
Function{} -> case Blocked t
b of
NotBlocked StuckOn{} t
_ -> m Bool
yes
NotBlocked NotBlocked' Term
AbsurdMatch t
_ -> m Bool
yes
Blocked t
_ -> m Bool
no
GeneralizableVar{} -> m Bool
forall a. HasCallStack => a
__IMPOSSIBLE__
Defn
_ -> m Bool
no
rigidVarsNotContainedIn
:: (PureTCM m, AnyRigid a)
=> a
-> (Nat -> Bool)
-> m Bool
rigidVarsNotContainedIn :: forall (m :: * -> *) a.
(PureTCM m, AnyRigid a) =>
a -> (Nat -> Bool) -> m Bool
rigidVarsNotContainedIn a
v Nat -> Bool
is = do
n0 <- m Nat
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Nat
getContextSize
let
levels = Nat -> Bool
is (Nat -> Bool) -> (Nat -> Nat) -> Nat -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Nat
n0Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
-Nat
1 Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
-)
test Nat
i = do
n <- m Nat
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Nat
getContextSize
let l = Nat
nNat -> Nat -> Nat
forall a. Num a => a -> a -> a
-Nat
1 Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
i
forbidden = Nat
l Nat -> Nat -> Bool
forall a. Ord a => a -> a -> Bool
< Nat
n0 Bool -> Bool -> Bool
&& Bool -> Bool
not (Nat -> Bool
levels Nat
l)
when forbidden $
reportSLn "tc.meta.kill" 20 $
"found forbidden de Bruijn level " ++ show l
return forbidden
anyRigid test v
class AnyRigid a where
anyRigid :: (PureTCM tcm)
=> (Nat -> tcm Bool) -> a -> tcm Bool
instance AnyRigid Term where
anyRigid :: forall (tcm :: * -> *).
PureTCM tcm =>
(Nat -> tcm Bool) -> Term -> tcm Bool
anyRigid Nat -> tcm Bool
f Term
t = do
b <- Term -> tcm (Blocked Term)
forall a (m :: * -> *).
(Reduce a, MonadReduce m) =>
a -> m (Blocked a)
reduceB Term
t
case ignoreBlocking b of
Var Nat
i Elims
es -> Nat -> tcm Bool
f Nat
i tcm Bool -> tcm Bool -> tcm Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`or2M` (Nat -> tcm Bool) -> Elims -> tcm Bool
forall a (tcm :: * -> *).
(AnyRigid a, PureTCM tcm) =>
(Nat -> tcm Bool) -> a -> tcm Bool
forall (tcm :: * -> *).
PureTCM tcm =>
(Nat -> tcm Bool) -> Elims -> tcm Bool
anyRigid Nat -> tcm Bool
f Elims
es
Lam ArgInfo
_ Abs Term
t -> (Nat -> tcm Bool) -> Abs Term -> tcm Bool
forall a (tcm :: * -> *).
(AnyRigid a, PureTCM tcm) =>
(Nat -> tcm Bool) -> a -> tcm Bool
forall (tcm :: * -> *).
PureTCM tcm =>
(Nat -> tcm Bool) -> Abs Term -> tcm Bool
anyRigid Nat -> tcm Bool
f Abs Term
t
Lit{} -> Bool -> tcm Bool
forall a. a -> tcm a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
Def QName
_ Elims
es -> case Blocked Term
b of
Blocked{} -> Bool -> tcm Bool
forall a. a -> tcm a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
NotBlocked (MissingClauses QName
_) Term
_ -> Bool -> tcm Bool
forall a. a -> tcm a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
Blocked Term
_ -> (Nat -> tcm Bool) -> Elims -> tcm Bool
forall a (tcm :: * -> *).
(AnyRigid a, PureTCM tcm) =>
(Nat -> tcm Bool) -> a -> tcm Bool
forall (tcm :: * -> *).
PureTCM tcm =>
(Nat -> tcm Bool) -> Elims -> tcm Bool
anyRigid Nat -> tcm Bool
f Elims
es
Con ConHead
_ ConInfo
_ Elims
ts -> (Nat -> tcm Bool) -> Elims -> tcm Bool
forall a (tcm :: * -> *).
(AnyRigid a, PureTCM tcm) =>
(Nat -> tcm Bool) -> a -> tcm Bool
forall (tcm :: * -> *).
PureTCM tcm =>
(Nat -> tcm Bool) -> Elims -> tcm Bool
anyRigid Nat -> tcm Bool
f Elims
ts
Pi Dom Type
a Abs Type
b -> (Nat -> tcm Bool) -> (Dom Type, Abs Type) -> tcm Bool
forall a (tcm :: * -> *).
(AnyRigid a, PureTCM tcm) =>
(Nat -> tcm Bool) -> a -> tcm Bool
forall (tcm :: * -> *).
PureTCM tcm =>
(Nat -> tcm Bool) -> (Dom Type, Abs Type) -> tcm Bool
anyRigid Nat -> tcm Bool
f (Dom Type
a,Abs Type
b)
Sort Sort
s -> (Nat -> tcm Bool) -> Sort -> tcm Bool
forall a (tcm :: * -> *).
(AnyRigid a, PureTCM tcm) =>
(Nat -> tcm Bool) -> a -> tcm Bool
forall (tcm :: * -> *).
PureTCM tcm =>
(Nat -> tcm Bool) -> Sort -> tcm Bool
anyRigid Nat -> tcm Bool
f Sort
s
Level Level
l -> (Nat -> tcm Bool) -> Level -> tcm Bool
forall a (tcm :: * -> *).
(AnyRigid a, PureTCM tcm) =>
(Nat -> tcm Bool) -> a -> tcm Bool
forall (tcm :: * -> *).
PureTCM tcm =>
(Nat -> tcm Bool) -> Level -> tcm Bool
anyRigid Nat -> tcm Bool
f Level
l
MetaV{} -> Bool -> tcm Bool
forall a. a -> tcm a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
DontCare{} -> Bool -> tcm Bool
forall a. a -> tcm a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
Dummy{} -> Bool -> tcm Bool
forall a. a -> tcm a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
instance AnyRigid Type where
anyRigid :: forall (tcm :: * -> *).
PureTCM tcm =>
(Nat -> tcm Bool) -> Type -> tcm Bool
anyRigid Nat -> tcm Bool
f (El Sort
s Term
t) = (Nat -> tcm Bool) -> (Sort, Term) -> tcm Bool
forall a (tcm :: * -> *).
(AnyRigid a, PureTCM tcm) =>
(Nat -> tcm Bool) -> a -> tcm Bool
forall (tcm :: * -> *).
PureTCM tcm =>
(Nat -> tcm Bool) -> (Sort, Term) -> tcm Bool
anyRigid Nat -> tcm Bool
f (Sort
s,Term
t)
instance AnyRigid Sort where
anyRigid :: forall (tcm :: * -> *).
PureTCM tcm =>
(Nat -> tcm Bool) -> Sort -> tcm Bool
anyRigid Nat -> tcm Bool
f Sort
s =
case Sort
s of
Univ Univ
_ Level
l -> (Nat -> tcm Bool) -> Level -> tcm Bool
forall a (tcm :: * -> *).
(AnyRigid a, PureTCM tcm) =>
(Nat -> tcm Bool) -> a -> tcm Bool
forall (tcm :: * -> *).
PureTCM tcm =>
(Nat -> tcm Bool) -> Level -> tcm Bool
anyRigid Nat -> tcm Bool
f Level
l
Inf Univ
_ Integer
_ -> Bool -> tcm Bool
forall a. a -> tcm a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
Sort
SizeUniv -> Bool -> tcm Bool
forall a. a -> tcm a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
Sort
LockUniv -> Bool -> tcm Bool
forall a. a -> tcm a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
Sort
LevelUniv -> Bool -> tcm Bool
forall a. a -> tcm a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
Sort
IntervalUniv -> Bool -> tcm Bool
forall a. a -> tcm a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
PiSort Dom' Term Term
a Sort
s1 Abs Sort
s2 -> Bool -> tcm Bool
forall a. a -> tcm a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
FunSort Sort
s1 Sort
s2 -> Bool -> tcm Bool
forall a. a -> tcm a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
UnivSort Sort
s -> (Nat -> tcm Bool) -> Sort -> tcm Bool
forall a (tcm :: * -> *).
(AnyRigid a, PureTCM tcm) =>
(Nat -> tcm Bool) -> a -> tcm Bool
forall (tcm :: * -> *).
PureTCM tcm =>
(Nat -> tcm Bool) -> Sort -> tcm Bool
anyRigid Nat -> tcm Bool
f Sort
s
MetaS{} -> Bool -> tcm Bool
forall a. a -> tcm a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
DefS{} -> Bool -> tcm Bool
forall a. a -> tcm a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
DummyS{} -> Bool -> tcm Bool
forall a. a -> tcm a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
instance AnyRigid Level where
anyRigid :: forall (tcm :: * -> *).
PureTCM tcm =>
(Nat -> tcm Bool) -> Level -> tcm Bool
anyRigid Nat -> tcm Bool
f (Max Integer
_ [PlusLevel' Term]
ls) = (Nat -> tcm Bool) -> [PlusLevel' Term] -> tcm Bool
forall a (tcm :: * -> *).
(AnyRigid a, PureTCM tcm) =>
(Nat -> tcm Bool) -> a -> tcm Bool
forall (tcm :: * -> *).
PureTCM tcm =>
(Nat -> tcm Bool) -> [PlusLevel' Term] -> tcm Bool
anyRigid Nat -> tcm Bool
f [PlusLevel' Term]
ls
instance AnyRigid PlusLevel where
anyRigid :: forall (tcm :: * -> *).
PureTCM tcm =>
(Nat -> tcm Bool) -> PlusLevel' Term -> tcm Bool
anyRigid Nat -> tcm Bool
f (Plus Integer
_ Term
l) = (Nat -> tcm Bool) -> Term -> tcm Bool
forall a (tcm :: * -> *).
(AnyRigid a, PureTCM tcm) =>
(Nat -> tcm Bool) -> a -> tcm Bool
forall (tcm :: * -> *).
PureTCM tcm =>
(Nat -> tcm Bool) -> Term -> tcm Bool
anyRigid Nat -> tcm Bool
f Term
l
instance (Subst a, AnyRigid a) => AnyRigid (Abs a) where
anyRigid :: forall (tcm :: * -> *).
PureTCM tcm =>
(Nat -> tcm Bool) -> Abs a -> tcm Bool
anyRigid Nat -> tcm Bool
f Abs a
b = Abs a -> (a -> tcm Bool) -> tcm Bool
forall a (m :: * -> *) b.
(Subst a, MonadAddContext m) =>
Abs a -> (a -> m b) -> m b
underAbstraction_ Abs a
b ((a -> tcm Bool) -> tcm Bool) -> (a -> tcm Bool) -> tcm Bool
forall a b. (a -> b) -> a -> b
$ (Nat -> tcm Bool) -> a -> tcm Bool
forall a (tcm :: * -> *).
(AnyRigid a, PureTCM tcm) =>
(Nat -> tcm Bool) -> a -> tcm Bool
forall (tcm :: * -> *).
PureTCM tcm =>
(Nat -> tcm Bool) -> a -> tcm Bool
anyRigid Nat -> tcm Bool
f
instance AnyRigid a => AnyRigid (Arg a) where
anyRigid :: forall (tcm :: * -> *).
PureTCM tcm =>
(Nat -> tcm Bool) -> Arg a -> tcm Bool
anyRigid Nat -> tcm Bool
f Arg a
a =
case Arg a -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance Arg a
a of
Relevance
Irrelevant -> Bool -> tcm Bool
forall a. a -> tcm a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
Relevance
_ -> (Nat -> tcm Bool) -> a -> tcm Bool
forall a (tcm :: * -> *).
(AnyRigid a, PureTCM tcm) =>
(Nat -> tcm Bool) -> a -> tcm Bool
forall (tcm :: * -> *).
PureTCM tcm =>
(Nat -> tcm Bool) -> a -> tcm Bool
anyRigid Nat -> tcm Bool
f (a -> tcm Bool) -> a -> tcm Bool
forall a b. (a -> b) -> a -> b
$ Arg a -> a
forall e. Arg e -> e
unArg Arg a
a
instance AnyRigid a => AnyRigid (Dom a) where
anyRigid :: forall (tcm :: * -> *).
PureTCM tcm =>
(Nat -> tcm Bool) -> Dom a -> tcm Bool
anyRigid Nat -> tcm Bool
f Dom a
dom = (Nat -> tcm Bool) -> a -> tcm Bool
forall a (tcm :: * -> *).
(AnyRigid a, PureTCM tcm) =>
(Nat -> tcm Bool) -> a -> tcm Bool
forall (tcm :: * -> *).
PureTCM tcm =>
(Nat -> tcm Bool) -> a -> tcm Bool
anyRigid Nat -> tcm Bool
f (a -> tcm Bool) -> a -> tcm Bool
forall a b. (a -> b) -> a -> b
$ Dom a -> a
forall t e. Dom' t e -> e
unDom Dom a
dom
instance AnyRigid a => AnyRigid (Elim' a) where
anyRigid :: forall (tcm :: * -> *).
PureTCM tcm =>
(Nat -> tcm Bool) -> Elim' a -> tcm Bool
anyRigid Nat -> tcm Bool
f (Apply Arg a
a) = (Nat -> tcm Bool) -> Arg a -> tcm Bool
forall a (tcm :: * -> *).
(AnyRigid a, PureTCM tcm) =>
(Nat -> tcm Bool) -> a -> tcm Bool
forall (tcm :: * -> *).
PureTCM tcm =>
(Nat -> tcm Bool) -> Arg a -> tcm Bool
anyRigid Nat -> tcm Bool
f Arg a
a
anyRigid Nat -> tcm Bool
f (IApply a
x a
y a
a) = (Nat -> tcm Bool) -> (a, (a, a)) -> tcm Bool
forall a (tcm :: * -> *).
(AnyRigid a, PureTCM tcm) =>
(Nat -> tcm Bool) -> a -> tcm Bool
forall (tcm :: * -> *).
PureTCM tcm =>
(Nat -> tcm Bool) -> (a, (a, a)) -> tcm Bool
anyRigid Nat -> tcm Bool
f (a
x,(a
y,a
a))
anyRigid Nat -> tcm Bool
f Proj{} = Bool -> tcm Bool
forall a. a -> tcm a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
instance AnyRigid a => AnyRigid [a] where
anyRigid :: forall (tcm :: * -> *).
PureTCM tcm =>
(Nat -> tcm Bool) -> [a] -> tcm Bool
anyRigid Nat -> tcm Bool
f [a]
xs = [a] -> (a -> tcm Bool) -> tcm Bool
forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, Monad m) =>
f a -> (a -> m Bool) -> m Bool
anyM [a]
xs ((a -> tcm Bool) -> tcm Bool) -> (a -> tcm Bool) -> tcm Bool
forall a b. (a -> b) -> a -> b
$ (Nat -> tcm Bool) -> a -> tcm Bool
forall a (tcm :: * -> *).
(AnyRigid a, PureTCM tcm) =>
(Nat -> tcm Bool) -> a -> tcm Bool
forall (tcm :: * -> *).
PureTCM tcm =>
(Nat -> tcm Bool) -> a -> tcm Bool
anyRigid Nat -> tcm Bool
f
instance (AnyRigid a, AnyRigid b) => AnyRigid (a,b) where
anyRigid :: forall (tcm :: * -> *).
PureTCM tcm =>
(Nat -> tcm Bool) -> (a, b) -> tcm Bool
anyRigid Nat -> tcm Bool
f (a
a,b
b) = (Nat -> tcm Bool) -> a -> tcm Bool
forall a (tcm :: * -> *).
(AnyRigid a, PureTCM tcm) =>
(Nat -> tcm Bool) -> a -> tcm Bool
forall (tcm :: * -> *).
PureTCM tcm =>
(Nat -> tcm Bool) -> a -> tcm Bool
anyRigid Nat -> tcm Bool
f a
a tcm Bool -> tcm Bool -> tcm Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`or2M` (Nat -> tcm Bool) -> b -> tcm Bool
forall a (tcm :: * -> *).
(AnyRigid a, PureTCM tcm) =>
(Nat -> tcm Bool) -> a -> tcm Bool
forall (tcm :: * -> *).
PureTCM tcm =>
(Nat -> tcm Bool) -> b -> tcm Bool
anyRigid Nat -> tcm Bool
f b
b
data PruneResult
= NothingToPrune
| PrunedNothing
| PrunedSomething
| PrunedEverything
deriving (PruneResult -> PruneResult -> Bool
(PruneResult -> PruneResult -> Bool)
-> (PruneResult -> PruneResult -> Bool) -> Eq PruneResult
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: PruneResult -> PruneResult -> Bool
== :: PruneResult -> PruneResult -> Bool
$c/= :: PruneResult -> PruneResult -> Bool
/= :: PruneResult -> PruneResult -> Bool
Eq, Nat -> PruneResult -> [Char] -> [Char]
[PruneResult] -> [Char] -> [Char]
PruneResult -> [Char]
(Nat -> PruneResult -> [Char] -> [Char])
-> (PruneResult -> [Char])
-> ([PruneResult] -> [Char] -> [Char])
-> Show PruneResult
forall a.
(Nat -> a -> [Char] -> [Char])
-> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
$cshowsPrec :: Nat -> PruneResult -> [Char] -> [Char]
showsPrec :: Nat -> PruneResult -> [Char] -> [Char]
$cshow :: PruneResult -> [Char]
show :: PruneResult -> [Char]
$cshowList :: [PruneResult] -> [Char] -> [Char]
showList :: [PruneResult] -> [Char] -> [Char]
Show)
killArgs :: (MonadMetaSolver m) => [Bool] -> MetaId -> m PruneResult
killArgs :: forall (m :: * -> *).
MonadMetaSolver m =>
[Bool] -> MetaId -> m PruneResult
killArgs [Bool]
kills MetaId
_
| Bool -> Bool
not ([Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or [Bool]
kills) = PruneResult -> m PruneResult
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return PruneResult
NothingToPrune
killArgs [Bool]
kills MetaId
m = do
mv <- MetaId -> m MetaVariable
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta MetaId
m
allowAssign <- asksTC envAssignMetas
if mvFrozen mv == Frozen || not allowAssign then return PrunedNothing else do
let a = Judgement MetaId -> Type
forall a. Judgement a -> Type
jMetaType (Judgement MetaId -> Type) -> Judgement MetaId -> Type
forall a b. (a -> b) -> a -> b
$ MetaVariable -> Judgement MetaId
mvJudgement MetaVariable
mv
TelV tel b <- telView' <$> instantiateFull a
let args = [Dom ([Char], Type)] -> [Bool] -> [(Dom ([Char], Type), Bool)]
forall a b. [a] -> [b] -> [(a, b)]
zip (Tele (Dom Type) -> [Dom ([Char], Type)]
forall t. Tele (Dom t) -> [Dom ([Char], t)]
telToList Tele (Dom Type)
tel) ([Bool]
kills [Bool] -> [Bool] -> [Bool]
forall a. [a] -> [a] -> [a]
++ Bool -> [Bool]
forall a. a -> [a]
repeat Bool
False)
(kills', a') <- killedType args b
dbg kills' a a'
if not (any unArg kills') then return PrunedNothing else do
addContext tel $ performKill kills' m a'
return $ if (and $ zipWith implies kills $ map unArg kills')
then PrunedEverything
else PrunedSomething
where
implies :: Bool -> Bool -> Bool
implies :: Bool -> Bool -> Bool
implies Bool
False Bool
_ = Bool
True
implies Bool
True Bool
x = Bool
x
dbg :: [Arg Bool] -> Type -> Type -> m ()
dbg [Arg Bool]
kills' Type
a Type
a' =
[Char] -> Nat -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.kill" Nat
10 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ TCMT IO Doc
"after kill analysis"
, Nat -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ TCMT IO Doc
"metavar =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> MetaId -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => MetaId -> m Doc
prettyTCM MetaId
m
, TCMT IO Doc
"kills =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Bool] -> [Char]
forall a. Show a => a -> [Char]
show [Bool]
kills)
, TCMT IO Doc
"kills' =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList ((Arg Bool -> TCMT IO Doc) -> [Arg Bool] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map Arg Bool -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Arg Bool -> m Doc
prettyTCM [Arg Bool]
kills')
, TCMT IO Doc
"oldType =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
a
, TCMT IO Doc
"newType =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
a'
]
]
killedType :: (MonadReduce m) => [(Dom (ArgName, Type), Bool)] -> Type -> m ([Arg Bool], Type)
killedType :: forall (m :: * -> *).
MonadReduce m =>
[(Dom ([Char], Type), Bool)] -> Type -> m ([Arg Bool], Type)
killedType [(Dom ([Char], Type), Bool)]
args Type
b = do
let n :: Nat
n = [(Dom ([Char], Type), Bool)] -> Nat
forall a. [a] -> Nat
forall (t :: * -> *) a. Foldable t => t a -> Nat
length [(Dom ([Char], Type), Bool)]
args
let iargs :: [(Nat, (Dom ([Char], Type), Bool))]
iargs = [Nat]
-> [(Dom ([Char], Type), Bool)]
-> [(Nat, (Dom ([Char], Type), Bool))]
forall a b. [a] -> [b] -> [(a, b)]
zip (Nat -> [Nat]
forall a. Integral a => a -> [a]
downFrom Nat
n) [(Dom ([Char], Type), Bool)]
args
let tokill :: IntSet
tokill = [Nat] -> IntSet
IntSet.fromList [ Nat
i | (Nat
i, (Dom ([Char], Type)
_, Bool
True)) <- [(Nat, (Dom ([Char], Type), Bool))]
iargs ]
(tokill, b) <- IntSet -> Type -> m (IntSet, Type)
forall (m :: * -> *).
MonadReduce m =>
IntSet -> Type -> m (IntSet, Type)
reallyNotFreeIn IntSet
tokill Type
b
(killed, b) <- go (reverse $ map fst args) tokill b
let kills = [ ArgInfo -> Bool -> Arg Bool
forall e. ArgInfo -> e -> Arg e
Arg (Dom ([Char], Type) -> ArgInfo
forall a. LensArgInfo a => a -> ArgInfo
getArgInfo Dom ([Char], Type)
dom) (Nat -> IntSet -> Bool
IntSet.member Nat
i IntSet
killed)
| (Nat
i, (Dom ([Char], Type)
dom, Bool
_)) <- [(Nat, (Dom ([Char], Type), Bool))]
iargs ]
return (kills, b)
where
down :: IntSet -> IntSet
down = (Nat -> Nat) -> IntSet -> IntSet
IntSet.map Nat -> Nat
forall a. Enum a => a -> a
pred
up :: IntSet -> IntSet
up = (Nat -> Nat) -> IntSet -> IntSet
IntSet.map Nat -> Nat
forall a. Enum a => a -> a
succ
go :: (MonadReduce m) => [Dom (ArgName, Type)] -> IntSet -> Type -> m (IntSet, Type)
go :: forall (m :: * -> *).
MonadReduce m =>
[Dom ([Char], Type)] -> IntSet -> Type -> m (IntSet, Type)
go [] IntSet
xs Type
b | IntSet -> Bool
IntSet.null IntSet
xs = (IntSet, Type) -> m (IntSet, Type)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (IntSet
xs, Type
b)
| Bool
otherwise = m (IntSet, Type)
forall a. HasCallStack => a
__IMPOSSIBLE__
go (Dom ([Char], Type)
arg : [Dom ([Char], Type)]
args) IntSet
xs Type
b
| Nat -> IntSet -> Bool
IntSet.member Nat
0 IntSet
xs = do
let ys :: IntSet
ys = IntSet -> IntSet
down (Nat -> IntSet -> IntSet
IntSet.delete Nat
0 IntSet
xs)
(ys, b) <- [Dom ([Char], Type)] -> IntSet -> Type -> m (IntSet, Type)
forall (m :: * -> *).
MonadReduce m =>
[Dom ([Char], Type)] -> IntSet -> Type -> m (IntSet, Type)
go [Dom ([Char], Type)]
args IntSet
ys (Type -> m (IntSet, Type)) -> Type -> m (IntSet, Type)
forall a b. (a -> b) -> a -> b
$ Impossible -> Type -> Type
forall a. Subst a => Impossible -> a -> a
strengthen Impossible
HasCallStack => Impossible
impossible Type
b
return (IntSet.insert 0 $ up ys, b)
| Bool
otherwise = do
let xs' :: IntSet
xs' = IntSet -> IntSet
down IntSet
xs
([Char]
name, Type
a) = Dom ([Char], Type) -> ([Char], Type)
forall t e. Dom' t e -> e
unDom Dom ([Char], Type)
arg
(ys, a) <- IntSet -> Type -> m (IntSet, Type)
forall (m :: * -> *).
MonadReduce m =>
IntSet -> Type -> m (IntSet, Type)
reallyNotFreeIn IntSet
xs' Type
a
(zs, b) <- go args ys $ mkPi ((name, a) <$ arg) b
return (up zs, b)
reallyNotFreeIn :: (MonadReduce m) => IntSet -> Type -> m (IntSet, Type)
reallyNotFreeIn :: forall (m :: * -> *).
MonadReduce m =>
IntSet -> Type -> m (IntSet, Type)
reallyNotFreeIn IntSet
xs Type
a | IntSet -> Bool
IntSet.null IntSet
xs = (IntSet, Type) -> m (IntSet, Type)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (IntSet
xs, Type
a)
reallyNotFreeIn IntSet
xs Type
a = do
let fvs :: VarMap
fvs = Type -> VarMap
forall a c t. (IsVarSet a c, Singleton Nat c, Free t) => t -> c
freeVars Type
a
anywhere :: IntSet
anywhere = VarMap -> IntSet
allVars VarMap
fvs
rigid :: IntSet
rigid = [IntSet] -> IntSet
forall (f :: * -> *). Foldable f => f IntSet -> IntSet
IntSet.unions [VarMap -> IntSet
stronglyRigidVars VarMap
fvs, VarMap -> IntSet
unguardedVars VarMap
fvs]
nonrigid :: IntSet
nonrigid = IntSet -> IntSet -> IntSet
IntSet.difference IntSet
anywhere IntSet
rigid
hasNo :: IntSet -> Bool
hasNo = IntSet -> IntSet -> Bool
IntSet.disjoint IntSet
xs
if IntSet -> Bool
hasNo IntSet
nonrigid
then
(IntSet, Type) -> m (IntSet, Type)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (IntSet -> IntSet -> IntSet
IntSet.difference IntSet
xs IntSet
rigid, Type
a)
else do
(fvs, a) <- IntSet -> Type -> m (IntMap IsFree, Type)
forall a (m :: * -> *).
(ForceNotFree a, Reduce a, MonadReduce m) =>
IntSet -> a -> m (IntMap IsFree, a)
forceNotFree (IntSet -> IntSet -> IntSet
IntSet.difference IntSet
xs IntSet
rigid) Type
a
let xs = IntMap IsFree -> IntSet
forall a. IntMap a -> IntSet
IntMap.keysSet (IntMap IsFree -> IntSet) -> IntMap IsFree -> IntSet
forall a b. (a -> b) -> a -> b
$ (IsFree -> Bool) -> IntMap IsFree -> IntMap IsFree
forall a. (a -> Bool) -> IntMap a -> IntMap a
IntMap.filter (IsFree -> IsFree -> Bool
forall a. Eq a => a -> a -> Bool
== IsFree
NotFree) IntMap IsFree
fvs
return (xs, a)
performKill
:: MonadMetaSolver m
=> [Arg Bool]
-> MetaId
-> Type
-> m ()
performKill :: forall (m :: * -> *).
MonadMetaSolver m =>
[Arg Bool] -> MetaId -> Type -> m ()
performKill [Arg Bool]
kills MetaId
m Type
a = do
mv <- MetaId -> m MetaVariable
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta MetaId
m
when (mvFrozen mv == Frozen) __IMPOSSIBLE__
let n = [Arg Bool] -> Nat
forall a. Sized a => a -> Nat
size [Arg Bool]
kills
let perm = Nat -> [Nat] -> Permutation
Perm Nat
n
[ Nat
i | (Nat
i, Arg ArgInfo
_ Bool
False) <- [Nat] -> [Arg Bool] -> [(Nat, Arg Bool)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Nat
0..] [Arg Bool]
kills ]
oldPerm = Nat -> Permutation -> Permutation
liftP (Nat -> Nat -> Nat
forall a. Ord a => a -> a -> a
max Nat
0 (Nat -> Nat) -> Nat -> Nat
forall a b. (a -> b) -> a -> b
$ Nat
n Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
m) Permutation
p
where p :: Permutation
p = MetaVariable -> Permutation
mvPermutation MetaVariable
mv
m :: Nat
m = Permutation -> Nat
forall a. Sized a => a -> Nat
size Permutation
p
judg = case MetaVariable -> Judgement MetaId
mvJudgement MetaVariable
mv of
HasType{ jComparison :: forall a. Judgement a -> Comparison
jComparison = Comparison
cmp } -> Any -> Comparison -> Type -> Judgement Any
forall a. a -> Comparison -> Type -> Judgement a
HasType Any
forall a. HasCallStack => a
__IMPOSSIBLE__ Comparison
cmp Type
a
IsSort{} -> Any -> Type -> Judgement Any
forall a. a -> Type -> Judgement a
IsSort Any
forall a. HasCallStack => a
__IMPOSSIBLE__ Type
a
m' <- newMeta Instantiable (mvInfo mv) (mvPriority mv) (composeP perm oldPerm) judg
etaExpandMetaSafe m'
let
vars = [ ArgInfo -> Term -> Arg Term
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
info (Nat -> Term
var Nat
i)
| (Nat
i, Arg ArgInfo
info Bool
False) <- [Nat] -> [Arg Bool] -> [(Nat, Arg Bool)]
forall a b. [a] -> [b] -> [(a, b)]
zip (Nat -> [Nat]
forall a. Integral a => a -> [a]
downFrom Nat
n) [Arg Bool]
kills ]
u = MetaId -> Elims -> Term
MetaV MetaId
m' (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ (Arg Term -> Elim' Term) -> [Arg Term] -> Elims
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply [Arg Term]
vars
tel = (Arg Bool -> Arg [Char]) -> [Arg Bool] -> [Arg [Char]]
forall a b. (a -> b) -> [a] -> [b]
map ([Char]
"v" [Char] -> Arg Bool -> Arg [Char]
forall a b. a -> Arg b -> Arg a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$) [Arg Bool]
kills
dbg m' u
assignTerm m tel u
where
dbg :: MetaId -> Term -> m ()
dbg MetaId
m' Term
u = [Char] -> Nat -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.kill" Nat
10 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ TCMT IO Doc
"actual killing"
, Nat -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ TCMT IO Doc
"new meta:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> MetaId -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty MetaId
m'
, TCMT IO Doc
"kills :" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ ((Arg Bool -> TCMT IO Doc) -> [Arg Bool] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map ([Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> TCMT IO Doc)
-> (Arg Bool -> [Char]) -> Arg Bool -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> [Char]
forall a. Show a => a -> [Char]
show (Bool -> [Char]) -> (Arg Bool -> Bool) -> Arg Bool -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg Bool -> Bool
forall e. Arg e -> e
unArg) [Arg Bool]
kills)
, TCMT IO Doc
"inst :" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> MetaId -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty MetaId
m TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":=" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
u
]
]