{-# OPTIONS_GHC -Wunused-imports #-}
{-# LANGUAGE NondecreasingIndentation #-}
module Agda.TypeChecking.MetaVars where
import Prelude hiding (null)
import Control.Monad ( foldM, forM, forM_, liftM2, void, guard )
import Control.Monad.Except ( MonadError(..), ExceptT, runExceptT )
import Control.Monad.Trans ( lift )
import Control.Monad.Trans.Maybe
import qualified Data.IntSet as IntSet
import qualified Data.IntMap as IntMap
import qualified Data.List as List
import qualified Data.Map.Strict as MapS
import qualified Data.Set as Set
import qualified Data.Foldable as Fold
import qualified Data.Traversable as Trav
import Agda.Interaction.Options
import Agda.Syntax.Abstract.Name as A
import Agda.Syntax.Common
import Agda.Syntax.Info ( MetaKind( InstanceMeta, UnificationMeta ), MetaNameSuggestion)
import qualified Agda.Syntax.Info as A
import Agda.Syntax.Internal
import Agda.Syntax.Internal.Generic
import Agda.Syntax.Internal.MetaVars
import Agda.Syntax.Position (getRange, killRange)
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Sort
import Agda.TypeChecking.Substitute
import qualified Agda.TypeChecking.SyntacticEquality as SynEq
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Constraints
import Agda.TypeChecking.Free
import Agda.TypeChecking.Lock
import Agda.TypeChecking.Level (levelType)
import Agda.TypeChecking.Records
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.EtaContract
import Agda.TypeChecking.SizedTypes (boundedSizeMetaHook, isSizeProblem)
import {-# SOURCE #-} Agda.TypeChecking.CheckInternal
import {-# SOURCE #-} Agda.TypeChecking.Conversion
import Agda.TypeChecking.MetaVars.Occurs
import qualified Agda.Utils.BiMap as BiMap
import Agda.Utils.Function
import Agda.Utils.Lens
import Agda.Utils.List
import Agda.Utils.List1 (List1, pattern (:|))
import qualified Agda.Utils.List1 as List1
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Size
import Agda.Utils.Tuple
import Agda.Utils.Permutation
import Agda.Syntax.Common.Pretty (Pretty, prettyShow, render)
import qualified Agda.Utils.ProfileOptions as Profile
import Agda.Utils.Singleton
import qualified Agda.Utils.Graph.TopSort as Graph
import Agda.Utils.VarSet (VarSet)
import qualified Agda.Utils.VarSet as VarSet
import Agda.Utils.Impossible
instance MonadMetaSolver TCM where
newMeta' :: forall a.
MetaInstantiation
-> Frozen
-> MetaInfo
-> MetaPriority
-> Permutation
-> Judgement a
-> TCM MetaId
newMeta' = MetaInstantiation
-> Frozen
-> MetaInfo
-> MetaPriority
-> Permutation
-> Judgement a
-> TCM MetaId
forall a.
MetaInstantiation
-> Frozen
-> MetaInfo
-> MetaPriority
-> Permutation
-> Judgement a
-> TCM MetaId
newMetaTCM'
assignV :: CompareDirection -> MetaId -> Args -> Term -> CompareAs -> TCM ()
assignV CompareDirection
dir MetaId
x Args
args Term
v CompareAs
t = CompareDirection -> MetaId -> Elims -> Term -> TCM () -> TCM ()
forall (m :: * -> *).
(MonadMetaSolver m, MonadConstraint m, MonadError TCErr m,
MonadDebug m, HasOptions m) =>
CompareDirection -> MetaId -> Elims -> Term -> m () -> m ()
assignWrapper CompareDirection
dir MetaId
x ((Arg Term -> Elim) -> Args -> Elims
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim
forall a. Arg a -> Elim' a
Apply Args
args) Term
v (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ CompareDirection -> MetaId -> Args -> Term -> CompareAs -> TCM ()
assign CompareDirection
dir MetaId
x Args
args Term
v CompareAs
t
assignTerm' :: MonadMetaSolver (TCMT IO) =>
MetaId -> [Arg [Char]] -> Term -> TCM ()
assignTerm' = MetaId -> [Arg [Char]] -> Term -> TCM ()
assignTermTCM'
etaExpandMeta :: [MetaClass] -> MetaId -> TCM ()
etaExpandMeta = [MetaClass] -> MetaId -> TCM ()
etaExpandMetaTCM
updateMetaVar :: MetaId -> (MetaVariable -> MetaVariable) -> TCM ()
updateMetaVar = HasCallStack => MetaId -> (MetaVariable -> MetaVariable) -> TCM ()
MetaId -> (MetaVariable -> MetaVariable) -> TCM ()
updateMetaVarTCM
speculateMetas :: TCM () -> TCM KeepMetas -> TCM ()
speculateMetas TCM ()
fallback TCM KeepMetas
m = do
(a, s) <- TCM KeepMetas -> TCM (KeepMetas, TCState)
forall a. TCM a -> TCM (a, TCState)
localTCStateSaving TCM KeepMetas
m
case a of
KeepMetas
KeepMetas -> TCState -> TCM ()
forall (m :: * -> *). MonadTCState m => TCState -> m ()
putTC TCState
s
KeepMetas
RollBackMetas -> TCM ()
fallback
findIdx :: Eq a => [a] -> a -> Maybe Int
findIdx :: forall a. Eq a => [a] -> a -> Maybe Nat
findIdx [a]
vs a
v = a -> [a] -> Maybe Nat
forall a. Eq a => a -> [a] -> Maybe Nat
List.elemIndex a
v ([a] -> [a]
forall a. [a] -> [a]
reverse [a]
vs)
hasTwinMeta :: MetaId -> TCM Bool
hasTwinMeta :: MetaId -> TCM Bool
hasTwinMeta MetaId
x = do
m <- MetaId -> TCMT IO MetaVariable
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta MetaId
x
return $ isJust $ mvTwin m
isBlockedTerm :: MetaId -> TCM Bool
isBlockedTerm :: MetaId -> TCM Bool
isBlockedTerm MetaId
x = do
[Char] -> Nat -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> [Char] -> m ()
reportSLn [Char]
"tc.meta.blocked" Nat
12 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$ [Char]
"is " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ MetaId -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow MetaId
x [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" a blocked term? "
i <- MetaId -> TCMT IO MetaInstantiation
forall (m :: * -> *).
ReadTCState m =>
MetaId -> m MetaInstantiation
lookupMetaInstantiation MetaId
x
let r = case MetaInstantiation
i of
BlockedConst{} -> Bool
True
PostponedTypeCheckingProblem{} -> Bool
True
InstV{} -> Bool
False
OpenMeta{} -> Bool
False
reportSLn "tc.meta.blocked" 12 $
if r then " yes, because " ++ prettyShow i else " no"
return r
isEtaExpandable :: [MetaClass] -> MetaId -> TCM Bool
isEtaExpandable :: [MetaClass] -> MetaId -> TCM Bool
isEtaExpandable [MetaClass]
classes MetaId
x = do
i <- MetaId -> TCMT IO MetaInstantiation
forall (m :: * -> *).
ReadTCState m =>
MetaId -> m MetaInstantiation
lookupMetaInstantiation MetaId
x
return $ case i of
OpenMeta MetaKind
UnificationMeta -> Bool
True
OpenMeta MetaKind
InstanceMeta -> MetaClass
Records MetaClass -> [MetaClass] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [MetaClass]
classes
InstV{} -> Bool
False
BlockedConst{} -> Bool
False
PostponedTypeCheckingProblem{} -> Bool
False
assignTerm :: MonadMetaSolver m => MetaId -> [Arg ArgName] -> Term -> m ()
assignTerm :: forall (m :: * -> *).
MonadMetaSolver m =>
MetaId -> [Arg [Char]] -> Term -> m ()
assignTerm MetaId
x [Arg [Char]]
tel Term
v = do
m Bool -> m () -> m ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM (MetaId -> m Bool
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m Bool
isFrozen MetaId
x) m ()
forall a. HasCallStack => a
__IMPOSSIBLE__
MetaId -> [Arg [Char]] -> Term -> m ()
forall (m :: * -> *).
(MonadMetaSolver m, MonadMetaSolver m) =>
MetaId -> [Arg [Char]] -> Term -> m ()
assignTerm' MetaId
x [Arg [Char]]
tel Term
v
assignTermTCM' :: MetaId -> [Arg ArgName] -> Term -> TCM ()
assignTermTCM' :: MetaId -> [Arg [Char]] -> Term -> TCM ()
assignTermTCM' MetaId
x [Arg [Char]]
tel Term
v = do
[Char] -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.assign" Nat
70 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
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
"assignTerm" 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
x 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
v
, 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
"tel =" 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 [Char] -> TCMT IO Doc) -> [Arg [Char]] -> [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 [Char] -> [Char]) -> Arg [Char] -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg [Char] -> [Char]
forall e. Arg e -> e
unArg) [Arg [Char]]
tel)
]
TCM Bool -> TCM () -> TCM ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM (Bool -> Bool
not (Bool -> Bool) -> TCM Bool -> TCM Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (TCEnv -> Bool) -> TCM Bool
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Bool
envAssignMetas) TCM ()
forall a. HasCallStack => a
__IMPOSSIBLE__
ProfileOption -> TCM () -> TCM ()
forall (m :: * -> *). MonadDebug m => ProfileOption -> m () -> m ()
whenProfile ProfileOption
Profile.Metas (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM () -> TCM ()
forall a. TCM a -> TCM a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ () -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
HasCallStack => MetaId -> (MetaVariable -> MetaVariable) -> TCM ()
MetaId -> (MetaVariable -> MetaVariable) -> TCM ()
updateMetaVarTCM MetaId
x ((MetaVariable -> MetaVariable) -> TCM ())
-> (MetaVariable -> MetaVariable) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ MetaVariable
mv ->
MetaVariable
mv { mvInstantiation = InstV $ Instantiation
{ instTel = tel
, instBody = v
}
}
MetaId -> TCM ()
forall (m :: * -> *). MonadMetaSolver m => MetaId -> m ()
etaExpandListeners MetaId
x
MetaId -> TCM ()
forall (m :: * -> *). MonadMetaSolver m => MetaId -> m ()
wakeupConstraints MetaId
x
[Char] -> Nat -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> [Char] -> m ()
reportSLn [Char]
"tc.meta.assign" Nat
20 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$ [Char]
"completed assignment of " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ MetaId -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow MetaId
x
newSortMetaBelowInf :: TCM Sort
newSortMetaBelowInf :: TCM Sort
newSortMetaBelowInf = do
x <- TCM Sort
forall (m :: * -> *). MonadMetaSolver m => m Sort
newSortMeta
hasBiggerSort x
return x
{-# SPECIALIZE newSortMeta :: TCM Sort #-}
newSortMeta :: MonadMetaSolver m => m Sort
newSortMeta :: forall (m :: * -> *). MonadMetaSolver m => m Sort
newSortMeta =
m Bool -> m Sort -> m Sort -> m Sort
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM m Bool
forall (m :: * -> *). HasOptions m => m Bool
hasUniversePolymorphism (Args -> m Sort
forall (m :: * -> *). MonadMetaSolver m => Args -> m Sort
newSortMetaCtx (Args -> m Sort) -> m Args -> m Sort
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< m Args
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Args
getContextArgs)
(m Sort -> m Sort) -> m Sort -> m Sort
forall a b. (a -> b) -> a -> b
$ do i <- m MetaInfo
forall (m :: * -> *). (MonadTCEnv m, ReadTCState m) => m MetaInfo
createMetaInfo
let j = () -> Type -> Judgement ()
forall a. a -> Type -> Judgement a
IsSort () Type
HasCallStack => Type
__DUMMY_TYPE__
x <- newMeta Instantiable i normalMetaPriority (idP 0) j
reportSDoc "tc.meta.new" 50 $
"new sort meta" <+> prettyTCM x
return $ MetaS x []
newSortMetaCtx :: MonadMetaSolver m => Args -> m Sort
newSortMetaCtx :: forall (m :: * -> *). MonadMetaSolver m => Args -> m Sort
newSortMetaCtx Args
vs = do
i <- m MetaInfo
forall (m :: * -> *). (MonadTCEnv m, ReadTCState m) => m MetaInfo
createMetaInfo
tel <- getContextTelescope
let t = Tele (Dom Type) -> Type -> Type
telePi_ Tele (Dom Type)
tel Type
HasCallStack => Type
__DUMMY_TYPE__
x <- newMeta Instantiable i normalMetaPriority (idP $ size tel) $ IsSort () t
reportSDoc "tc.meta.new" 50 $
"new sort meta" <+> prettyTCM x <+> ":" <+> prettyTCM t
return $ MetaS x $ map Apply vs
newTypeMeta' :: Comparison -> Sort -> TCM Type
newTypeMeta' :: Comparison -> Sort -> TCM Type
newTypeMeta' Comparison
cmp Sort
s = Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El Sort
s (Term -> Type)
-> ((MetaId, Term) -> Term) -> (MetaId, Term) -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (MetaId, Term) -> Term
forall a b. (a, b) -> b
snd ((MetaId, Term) -> Type) -> TCMT IO (MetaId, Term) -> TCM Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RunMetaOccursCheck -> Comparison -> Type -> TCMT IO (MetaId, Term)
forall (m :: * -> *).
MonadMetaSolver m =>
RunMetaOccursCheck -> Comparison -> Type -> m (MetaId, Term)
newValueMeta RunMetaOccursCheck
RunMetaOccursCheck Comparison
cmp (Sort -> Type
sort Sort
s)
newTypeMeta :: Sort -> TCM Type
newTypeMeta :: Sort -> TCM Type
newTypeMeta = Comparison -> Sort -> TCM Type
newTypeMeta' Comparison
CmpLeq
newTypeMeta_ :: TCM Type
newTypeMeta_ :: TCM Type
newTypeMeta_ = Comparison -> Sort -> TCM Type
newTypeMeta' Comparison
CmpEq (Sort -> TCM Type) -> TCM Sort -> TCM Type
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (TCM Sort -> TCM Sort
forall (m :: * -> *) a.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
m a -> m a
workOnTypes (TCM Sort -> TCM Sort) -> TCM Sort -> TCM Sort
forall a b. (a -> b) -> a -> b
$ TCM Sort
forall (m :: * -> *). MonadMetaSolver m => m Sort
newSortMeta)
{-# SPECIALIZE newLevelMeta :: TCM Level #-}
newLevelMeta :: MonadMetaSolver m => m Level
newLevelMeta :: forall (m :: * -> *). MonadMetaSolver m => m Level
newLevelMeta = do
(x, v) <- RunMetaOccursCheck -> Comparison -> Type -> m (MetaId, Term)
forall (m :: * -> *).
MonadMetaSolver m =>
RunMetaOccursCheck -> Comparison -> Type -> m (MetaId, Term)
newValueMeta RunMetaOccursCheck
RunMetaOccursCheck Comparison
CmpEq (Type -> m (MetaId, Term)) -> m Type -> m (MetaId, Term)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< m Type
forall (m :: * -> *). (HasBuiltins m, MonadTCError m) => m Type
levelType
return $ case v of
Level Level
l -> Level
l
Term
_ -> Term -> Level
forall t. t -> Level' t
atomicLevel Term
v
{-# SPECIALIZE newInstanceMeta :: MetaNameSuggestion -> Type -> TCM (MetaId, Term) #-}
newInstanceMeta
:: MonadMetaSolver m
=> MetaNameSuggestion -> Type -> m (MetaId, Term)
newInstanceMeta :: forall (m :: * -> *).
MonadMetaSolver m =>
[Char] -> Type -> m (MetaId, Term)
newInstanceMeta [Char]
s Type
t = do
vs <- m Args
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Args
getContextArgs
ctx <- getContextTelescope
newInstanceMetaCtx s (telePi_ ctx t) vs
newInstanceMetaCtx
:: MonadMetaSolver m
=> MetaNameSuggestion -> Type -> Args -> m (MetaId, Term)
newInstanceMetaCtx :: forall (m :: * -> *).
MonadMetaSolver m =>
[Char] -> Type -> Args -> m (MetaId, Term)
newInstanceMetaCtx [Char]
s Type
t Args
vs = do
[Char] -> Nat -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.new" Nat
50 (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
fsep
[ TCMT IO Doc
"new instance meta:"
, 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
$ Args -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Args -> m Doc
prettyTCM Args
vs TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"|-"
]
i0 <- RunMetaOccursCheck -> m MetaInfo
forall (m :: * -> *).
(MonadTCEnv m, ReadTCState m) =>
RunMetaOccursCheck -> m MetaInfo
createMetaInfo' RunMetaOccursCheck
DontRunMetaOccursCheck
let i = MetaInfo
i0 { miNameSuggestion = s }
TelV tel _ <- telView t
let perm = Nat -> Permutation
idP (Tele (Dom Type) -> Nat
forall a. Sized a => a -> Nat
size Tele (Dom Type)
tel)
x <- newMeta' (OpenMeta InstanceMeta) Instantiable i normalMetaPriority perm (HasType () CmpLeq t)
reportSDoc "tc.meta.new" 50 $ fsep
[ nest 2 $ pretty x <+> ":" <+> prettyTCM t
]
let c = MetaId -> Maybe [Candidate] -> Constraint
FindInstance MetaId
x Maybe [Candidate]
forall a. Maybe a
Nothing
addAwakeConstraint alwaysUnblock c
etaExpandMetaSafe x
return (x, MetaV x $ map Apply vs)
newNamedValueMeta :: MonadMetaSolver m => RunMetaOccursCheck -> MetaNameSuggestion -> Comparison -> Type -> m (MetaId, Term)
newNamedValueMeta :: forall (m :: * -> *).
MonadMetaSolver m =>
RunMetaOccursCheck
-> [Char] -> Comparison -> Type -> m (MetaId, Term)
newNamedValueMeta RunMetaOccursCheck
b [Char]
s Comparison
cmp Type
t = do
(x, v) <- RunMetaOccursCheck -> Comparison -> Type -> m (MetaId, Term)
forall (m :: * -> *).
MonadMetaSolver m =>
RunMetaOccursCheck -> Comparison -> Type -> m (MetaId, Term)
newValueMeta RunMetaOccursCheck
b Comparison
cmp Type
t
setMetaNameSuggestion x s
return (x, v)
newNamedValueMeta' :: MonadMetaSolver m => RunMetaOccursCheck -> MetaNameSuggestion -> Comparison -> Type -> m (MetaId, Term)
newNamedValueMeta' :: forall (m :: * -> *).
MonadMetaSolver m =>
RunMetaOccursCheck
-> [Char] -> Comparison -> Type -> m (MetaId, Term)
newNamedValueMeta' RunMetaOccursCheck
b [Char]
s Comparison
cmp Type
t = do
(x, v) <- RunMetaOccursCheck -> Comparison -> Type -> m (MetaId, Term)
forall (m :: * -> *).
MonadMetaSolver m =>
RunMetaOccursCheck -> Comparison -> Type -> m (MetaId, Term)
newValueMeta' RunMetaOccursCheck
b Comparison
cmp Type
t
setMetaNameSuggestion x s
return (x, v)
{-# SPECIALIZE newValueMetaOfKind :: A.MetaInfo -> RunMetaOccursCheck -> Comparison -> Type -> TCM (MetaId, Term) #-}
newValueMetaOfKind :: MonadMetaSolver m
=> A.MetaInfo
-> RunMetaOccursCheck
-> Comparison
-> Type
-> m (MetaId, Term)
newValueMetaOfKind :: forall (m :: * -> *).
MonadMetaSolver m =>
MetaInfo
-> RunMetaOccursCheck -> Comparison -> Type -> m (MetaId, Term)
newValueMetaOfKind MetaInfo
info = case MetaInfo -> MetaKind
A.metaKind MetaInfo
info of
MetaKind
UnificationMeta -> RunMetaOccursCheck -> Comparison -> Type -> m (MetaId, Term)
forall (m :: * -> *).
MonadMetaSolver m =>
RunMetaOccursCheck -> Comparison -> Type -> m (MetaId, Term)
newValueMeta
MetaKind
InstanceMeta -> \ RunMetaOccursCheck
_run Comparison
_cmp -> [Char] -> Type -> m (MetaId, Term)
forall (m :: * -> *).
MonadMetaSolver m =>
[Char] -> Type -> m (MetaId, Term)
newInstanceMeta (MetaInfo -> [Char]
A.metaNameSuggestion MetaInfo
info)
{-# SPECIALIZE newValueMeta :: RunMetaOccursCheck -> Comparison -> Type -> TCM (MetaId, Term) #-}
newValueMeta :: MonadMetaSolver m => RunMetaOccursCheck -> Comparison -> Type -> m (MetaId, Term)
newValueMeta :: forall (m :: * -> *).
MonadMetaSolver m =>
RunMetaOccursCheck -> Comparison -> Type -> m (MetaId, Term)
newValueMeta RunMetaOccursCheck
b Comparison
cmp Type
t = do
vs <- m Args
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Args
getContextArgs
tel <- getContextTelescope
newValueMetaCtx Instantiable b cmp t tel (idP $ size tel) vs
newValueMetaCtx
:: MonadMetaSolver m
=> Frozen -> RunMetaOccursCheck -> Comparison -> Type -> Telescope -> Permutation -> Args -> m (MetaId, Term)
newValueMetaCtx :: forall (m :: * -> *).
MonadMetaSolver m =>
Frozen
-> RunMetaOccursCheck
-> Comparison
-> Type
-> Tele (Dom Type)
-> Permutation
-> Args
-> m (MetaId, Term)
newValueMetaCtx Frozen
frozen RunMetaOccursCheck
b Comparison
cmp Type
t Tele (Dom Type)
tel Permutation
perm Args
ctx =
(Term -> m Term) -> (MetaId, Term) -> m (MetaId, Term)
forall (m :: * -> *) b d a.
Functor m =>
(b -> m d) -> (a, b) -> m (a, d)
mapSndM Term -> m Term
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull ((MetaId, Term) -> m (MetaId, Term))
-> m (MetaId, Term) -> m (MetaId, Term)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Frozen
-> RunMetaOccursCheck
-> Comparison
-> Type
-> Tele (Dom Type)
-> Permutation
-> Args
-> m (MetaId, Term)
forall (m :: * -> *).
MonadMetaSolver m =>
Frozen
-> RunMetaOccursCheck
-> Comparison
-> Type
-> Tele (Dom Type)
-> Permutation
-> Args
-> m (MetaId, Term)
newValueMetaCtx' Frozen
frozen RunMetaOccursCheck
b Comparison
cmp Type
t Tele (Dom Type)
tel Permutation
perm Args
ctx
{-# SPECIALIZE newValueMeta' :: RunMetaOccursCheck -> Comparison -> Type -> TCM (MetaId, Term) #-}
newValueMeta'
:: MonadMetaSolver m
=> RunMetaOccursCheck -> Comparison -> Type -> m (MetaId, Term)
newValueMeta' :: forall (m :: * -> *).
MonadMetaSolver m =>
RunMetaOccursCheck -> Comparison -> Type -> m (MetaId, Term)
newValueMeta' RunMetaOccursCheck
b Comparison
cmp Type
t = do
vs <- m Args
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Args
getContextArgs
tel <- getContextTelescope
newValueMetaCtx' Instantiable b cmp t tel (idP $ size tel) vs
newValueMetaCtx'
:: MonadMetaSolver m
=> Frozen -> RunMetaOccursCheck -> Comparison -> Type -> Telescope -> Permutation -> Args -> m (MetaId, Term)
newValueMetaCtx' :: forall (m :: * -> *).
MonadMetaSolver m =>
Frozen
-> RunMetaOccursCheck
-> Comparison
-> Type
-> Tele (Dom Type)
-> Permutation
-> Args
-> m (MetaId, Term)
newValueMetaCtx' Frozen
frozen RunMetaOccursCheck
b Comparison
cmp Type
a Tele (Dom Type)
tel Permutation
perm Args
vs = do
i <- RunMetaOccursCheck -> m MetaInfo
forall (m :: * -> *).
(MonadTCEnv m, ReadTCState m) =>
RunMetaOccursCheck -> m MetaInfo
createMetaInfo' RunMetaOccursCheck
b
let t = Tele (Dom Type) -> Type -> Type
telePi_ Tele (Dom Type)
tel Type
a
x <- newMeta frozen i normalMetaPriority perm (HasType () cmp t)
modality <- currentModality
reportSDoc "tc.meta.new" 50 $ fsep
[ text $ "new meta (" ++ show (i ^. lensIsAbstract) ++ "):"
, nest 2 $ prettyTCM vs <+> "|-"
, nest 2 $ pretty x <+> ":" <+> pretty modality <+> prettyTCM t
]
etaExpandMetaSafe x
let u = MetaId -> Elims -> Term
MetaV MetaId
x (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ (Arg Term -> Elim) -> Args -> Elims
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim
forall a. Arg a -> Elim' a
Apply Args
vs
boundedSizeMetaHook u tel a
return (x, u)
newTelMeta :: MonadMetaSolver m => Telescope -> m Args
newTelMeta :: forall (m :: * -> *).
MonadMetaSolver m =>
Tele (Dom Type) -> m Args
newTelMeta Tele (Dom Type)
tel = Type -> m Args
forall (m :: * -> *). MonadMetaSolver m => Type -> m Args
newArgsMeta (Tele (Dom Type) -> Type -> Type
forall t. Abstract t => Tele (Dom Type) -> t -> t
abstract Tele (Dom Type)
tel (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ Type
HasCallStack => Type
__DUMMY_TYPE__)
type Condition = Dom Type -> Abs Type -> Bool
trueCondition :: Condition
trueCondition :: Condition
trueCondition Dom Type
_ Abs Type
_ = Bool
True
{-# SPECIALIZE newArgsMeta :: Type -> TCM Args #-}
newArgsMeta :: MonadMetaSolver m => Type -> m Args
newArgsMeta :: forall (m :: * -> *). MonadMetaSolver m => Type -> m Args
newArgsMeta = Condition -> Type -> m Args
forall (m :: * -> *).
MonadMetaSolver m =>
Condition -> Type -> m Args
newArgsMeta' Condition
trueCondition
{-# SPECIALIZE newArgsMeta' :: Condition -> Type -> TCM Args #-}
newArgsMeta' :: MonadMetaSolver m => Condition -> Type -> m Args
newArgsMeta' :: forall (m :: * -> *).
MonadMetaSolver m =>
Condition -> Type -> m Args
newArgsMeta' Condition
condition Type
t = do
args <- m Args
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Args
getContextArgs
tel <- getContextTelescope
newArgsMetaCtx' Instantiable condition t tel (idP $ size tel) args
newArgsMetaCtx :: Type -> Telescope -> Permutation -> Args -> TCM Args
newArgsMetaCtx :: Type -> Tele (Dom Type) -> Permutation -> Args -> TCM Args
newArgsMetaCtx = Frozen
-> Condition
-> Type
-> Tele (Dom Type)
-> Permutation
-> Args
-> TCM Args
forall (m :: * -> *).
MonadMetaSolver m =>
Frozen
-> Condition
-> Type
-> Tele (Dom Type)
-> Permutation
-> Args
-> m Args
newArgsMetaCtx' Frozen
Instantiable Condition
trueCondition
newArgsMetaCtx''
:: MonadMetaSolver m
=> MetaNameSuggestion -> Frozen -> Condition -> Type -> Telescope -> Permutation -> Args -> m Args
newArgsMetaCtx'' :: forall (m :: * -> *).
MonadMetaSolver m =>
[Char]
-> Frozen
-> Condition
-> Type
-> Tele (Dom Type)
-> Permutation
-> Args
-> m Args
newArgsMetaCtx'' [Char]
pref Frozen
frozen Condition
condition (El Sort
s Term
tm) Tele (Dom Type)
tel Permutation
perm Args
ctx = do
tm <- Term -> m Term
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Term
tm
case tm of
Pi dom :: Dom Type
dom@(Dom{domInfo :: forall t e. Dom' t e -> ArgInfo
domInfo = ArgInfo
info, unDom :: forall t e. Dom' t e -> e
unDom = Type
a}) Abs Type
codom | Condition
condition Dom Type
dom Abs Type
codom -> do
let mod :: Modality
mod = ArgInfo -> Modality
forall a. LensModality a => a -> Modality
getModality ArgInfo
info
tel' :: Tele (Dom Type)
tel' = ListTel -> Tele (Dom Type)
telFromList (ListTel -> Tele (Dom Type)) -> ListTel -> Tele (Dom Type)
forall a b. (a -> b) -> a -> b
$
(Dom ([Char], Type) -> Dom ([Char], Type)) -> ListTel -> ListTel
forall a b. (a -> b) -> [a] -> [b]
map (Modality
mod Modality -> Dom ([Char], Type) -> Dom ([Char], Type)
forall a. LensModality a => Modality -> a -> a
`inverseApplyModalityButNotQuantity`) (ListTel -> ListTel) -> ListTel -> ListTel
forall a b. (a -> b) -> a -> b
$
Tele (Dom Type) -> ListTel
forall t. Tele (Dom t) -> [Dom ([Char], t)]
telToList Tele (Dom Type)
tel
ctx' :: Args
ctx' = (Arg Term -> Arg Term) -> Args -> Args
forall a b. (a -> b) -> [a] -> [b]
map (Modality
mod Modality -> Arg Term -> Arg Term
forall a. LensModality a => Modality -> a -> a
`inverseApplyModalityButNotQuantity`) Args
ctx
(m, u) <- ArgInfo -> m (MetaId, Term) -> m (MetaId, Term)
forall (tcm :: * -> *) m a.
(MonadTCEnv tcm, LensModality m) =>
m -> tcm a -> tcm a
applyModalityToContext ArgInfo
info (m (MetaId, Term) -> m (MetaId, Term))
-> m (MetaId, Term) -> m (MetaId, Term)
forall a b. (a -> b) -> a -> b
$
Frozen
-> RunMetaOccursCheck
-> Comparison
-> Type
-> Tele (Dom Type)
-> Permutation
-> Args
-> m (MetaId, Term)
forall (m :: * -> *).
MonadMetaSolver m =>
Frozen
-> RunMetaOccursCheck
-> Comparison
-> Type
-> Tele (Dom Type)
-> Permutation
-> Args
-> m (MetaId, Term)
newValueMetaCtx Frozen
frozen RunMetaOccursCheck
RunMetaOccursCheck Comparison
CmpLeq Type
a Tele (Dom Type)
tel' Permutation
perm Args
ctx'
whenM ((== YesGeneralizeVar) <$> viewTC eGeneralizeMetas) $
setMetaGeneralizableArgInfo m $ hideOrKeepInstance info
setMetaNameSuggestion m (suffixNameSuggestion pref (absName codom))
args <- newArgsMetaCtx'' pref frozen condition (codom `absApp` u) tel perm ctx
return $ Arg info u : args
Term
_ -> Args -> m Args
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return []
newArgsMetaCtx'
:: MonadMetaSolver m
=> Frozen -> Condition -> Type -> Telescope -> Permutation -> Args -> m Args
newArgsMetaCtx' :: forall (m :: * -> *).
MonadMetaSolver m =>
Frozen
-> Condition
-> Type
-> Tele (Dom Type)
-> Permutation
-> Args
-> m Args
newArgsMetaCtx' = [Char]
-> Frozen
-> Condition
-> Type
-> Tele (Dom Type)
-> Permutation
-> Args
-> m Args
forall (m :: * -> *).
MonadMetaSolver m =>
[Char]
-> Frozen
-> Condition
-> Type
-> Tele (Dom Type)
-> Permutation
-> Args
-> m Args
newArgsMetaCtx'' [Char]
forall a. Monoid a => a
mempty
newRecordMeta :: QName -> Args -> TCM Term
newRecordMeta :: QName -> Args -> TCM Term
newRecordMeta QName
r Args
pars = do
args <- TCM Args
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Args
getContextArgs
tel <- getContextTelescope
newRecordMetaCtx mempty Instantiable r pars tel (idP $ size tel) args
newRecordMetaCtx
:: MetaNameSuggestion
-> Frozen
-> QName
-> Args
-> Telescope -> Permutation -> Args -> TCM Term
newRecordMetaCtx :: [Char]
-> Frozen
-> QName
-> Args
-> Tele (Dom Type)
-> Permutation
-> Args
-> TCM Term
newRecordMetaCtx [Char]
pref Frozen
frozen QName
r Args
pars Tele (Dom Type)
tel Permutation
perm Args
ctx = do
rdef <- QName -> TCMT IO RecordData
forall (m :: * -> *).
(HasConstInfo m, ReadTCState m, MonadError TCErr m) =>
QName -> m RecordData
getRecordDef QName
r
let con = KillRangeT ConHead
forall a. KillRange a => KillRangeT a
killRange KillRangeT ConHead -> KillRangeT ConHead
forall a b. (a -> b) -> a -> b
$ RecordData -> ConHead
_recConHead RecordData
rdef
let ftel = Tele (Dom Type) -> Args -> Tele (Dom Type)
forall t. Apply t => t -> Args -> t
apply (RecordData -> Tele (Dom Type)
_recTel RecordData
rdef) Args
pars
fields <- newArgsMetaCtx'' pref frozen trueCondition
(telePi_ ftel __DUMMY_TYPE__) tel perm ctx
return $ Con con ConOSystem (map Apply fields)
newQuestionMark :: InteractionId -> Comparison -> Type -> TCM (MetaId, Term)
newQuestionMark :: InteractionId -> Comparison -> Type -> TCMT IO (MetaId, Term)
newQuestionMark InteractionId
ii Comparison
cmp = (Comparison -> Type -> TCMT IO (MetaId, Term))
-> InteractionId -> Comparison -> Type -> TCMT IO (MetaId, Term)
newQuestionMark' (RunMetaOccursCheck -> Comparison -> Type -> TCMT IO (MetaId, Term)
forall (m :: * -> *).
MonadMetaSolver m =>
RunMetaOccursCheck -> Comparison -> Type -> m (MetaId, Term)
newValueMeta' RunMetaOccursCheck
RunMetaOccursCheck) InteractionId
ii Comparison
cmp
newQuestionMark'
:: (Comparison -> Type -> TCM (MetaId, Term))
-> InteractionId -> Comparison -> Type -> TCM (MetaId, Term)
newQuestionMark' :: (Comparison -> Type -> TCMT IO (MetaId, Term))
-> InteractionId -> Comparison -> Type -> TCMT IO (MetaId, Term)
newQuestionMark' Comparison -> Type -> TCMT IO (MetaId, Term)
new InteractionId
ii Comparison
cmp Type
t = InteractionId -> TCMT IO (Maybe MetaId)
forall (m :: * -> *).
ReadTCState m =>
InteractionId -> m (Maybe MetaId)
lookupInteractionMeta InteractionId
ii TCMT IO (Maybe MetaId)
-> (Maybe MetaId -> TCMT IO (MetaId, Term))
-> TCMT IO (MetaId, Term)
forall a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Maybe MetaId
Nothing -> do
(x, m) <- Comparison -> Type -> TCMT IO (MetaId, Term)
new Comparison
cmp Type
t
connectInteractionPoint ii x
return (x, m)
Just MetaId
x -> do
MetaVar
{ mvInfo = MetaInfo{ miClosRange = Closure{ clEnv = TCEnv{ envContext = gamma }}}
, mvPermutation = p
} <- MetaVariable -> Maybe MetaVariable -> MetaVariable
forall a. a -> Maybe a -> a
fromMaybe MetaVariable
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe MetaVariable -> MetaVariable)
-> TCMT IO (Maybe MetaVariable) -> TCMT IO MetaVariable
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> TCMT IO (Maybe MetaVariable)
forall (m :: * -> *).
ReadTCState m =>
MetaId -> m (Maybe MetaVariable)
lookupLocalMeta' MetaId
x
delta <- getContext
let glen = Context -> Nat
forall a. [a] -> Nat
forall (t :: * -> *) a. Foldable t => t a -> Nat
length Context
gamma
let dlen = Context -> Nat
forall a. [a] -> Nat
forall (t :: * -> *) a. Foldable t => t a -> Nat
length Context
delta
let gxs = (Dom (Name, Type) -> Name) -> Context -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map ((Name, Type) -> Name
forall a b. (a, b) -> a
fst ((Name, Type) -> Name)
-> (Dom (Name, Type) -> (Name, Type)) -> Dom (Name, Type) -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom (Name, Type) -> (Name, Type)
forall t e. Dom' t e -> e
unDom) Context
gamma
let dxs = (Dom (Name, Type) -> Name) -> Context -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map ((Name, Type) -> Name
forall a b. (a, b) -> a
fst ((Name, Type) -> Name)
-> (Dom (Name, Type) -> (Name, Type)) -> Dom (Name, Type) -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom (Name, Type) -> (Name, Type)
forall t e. Dom' t e -> e
unDom) Context
delta
reportSDoc "tc.interaction" 20 $ vcat
[ "reusing meta"
, nest 2 $ "creation context:" <+> pretty gxs
, nest 2 $ "reusage context:" <+> pretty dxs
]
rev_args <- case List.findIndex nameIsRecordName dxs of
Maybe Nat
Nothing -> do
Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([Name]
gxs [Name] -> [Name] -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`List.isSuffixOf` [Name]
dxs) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
[Char] -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"impossible" Nat
10 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
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
"expecting meta-creation context"
, 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
$ [Name] -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [Name]
gxs
, TCMT IO Doc
"to be a suffix of the meta-reuse context"
, 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
$ [Name] -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [Name]
dxs
]
[Char] -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"impossible" Nat
70 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
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
"expecting meta-creation context"
, 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
$ ([Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> TCMT IO Doc)
-> ([Name] -> [Char]) -> [Name] -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Name] -> [Char]
forall a. Show a => a -> [Char]
show) [Name]
gxs
, TCMT IO Doc
"to be a suffix of the meta-reuse context"
, 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
$ ([Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> TCMT IO Doc)
-> ([Name] -> [Char]) -> [Name] -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Name] -> [Char]
forall a. Show a => a -> [Char]
show) [Name]
dxs
]
TCM ()
forall a. HasCallStack => a
__IMPOSSIBLE__
[Term] -> TCMT IO [Term]
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Term] -> TCMT IO [Term]) -> [Term] -> TCMT IO [Term]
forall a b. (a -> b) -> a -> b
$ (Nat -> Term) -> [Nat] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map Nat -> Term
var [Nat
dlen Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
glen .. Nat
dlen Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
1]
Just Nat
k -> do
let g0len :: Nat
g0len = [Name] -> Nat
forall a. [a] -> Nat
forall (t :: * -> *) a. Foldable t => t a -> Nat
length [Name]
dxs Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
k Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
1
let gys :: [Name]
gys = (Name -> Name) -> [Name] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map Name -> Name
nameCanonical [Name]
gxs
let dys :: [Name]
dys = (Name -> Name) -> [Name] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map Name -> Name
nameCanonical [Name]
dxs
let (Nat
d2len, Nat
g1len) = [Name] -> [Name] -> (Nat, Nat)
forall a. Eq a => [a] -> [a] -> (Nat, Nat)
findOverlap (Nat -> [Name] -> [Name]
forall a. Nat -> [a] -> [a]
take Nat
k [Name]
dys) [Name]
gys
[Char] -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.interaction" Nat
30 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
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] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ (TCMT IO Doc -> TCMT IO Doc) -> [TCMT IO Doc] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Nat -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2)
[ TCMT IO Doc
"glen =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Nat -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Nat
glen
, TCMT IO Doc
"g0len =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Nat -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Nat
g0len
, TCMT IO Doc
"g1len =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Nat -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Nat
g1len
, TCMT IO Doc
"d2len =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Nat -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Nat
d2len
]
Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Nat -> [Name] -> [Name]
forall a. Nat -> [a] -> [a]
drop (Nat
glen Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
g0len) [Name]
gxs [Name] -> [Name] -> Bool
forall a. Eq a => a -> a -> Bool
== Nat -> [Name] -> [Name]
forall a. Nat -> [a] -> [a]
drop (Nat
k Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
+ Nat
1) [Name]
dxs) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
[Char] -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"impossible" Nat
10 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
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
"expecting meta-creation context (with fields instead of record var)"
, 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
$ [Name] -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [Name]
gxs
, TCMT IO Doc
"to share ancestry (suffix) with the meta-reuse context (with record var)"
, 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
$ [Name] -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [Name]
dxs
]
TCM ()
forall a. HasCallStack => a
__IMPOSSIBLE__
Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ( ([Name] -> [Name] -> Bool
forall a. Eq a => a -> a -> Bool
(==) ([Name] -> [Name] -> Bool)
-> ([Name] -> [Name]) -> [Name] -> [Name] -> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Nat -> [Name] -> [Name]
forall a. Nat -> [a] -> [a]
take Nat
g1len) [Name]
gys (Nat -> [Name] -> [Name]
forall a. Nat -> [a] -> [a]
drop Nat
d2len [Name]
dys) ) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
[Char] -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"impossible" Nat
10 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
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
"expecting meta-creation context (with fields instead of record var)"
, 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
$ [Name] -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [Name]
gxs
, TCMT IO Doc
"to be an expansion of the meta-reuse context (with record var)"
, 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
$ [Name] -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [Name]
dxs
]
TCM ()
forall a. HasCallStack => a
__IMPOSSIBLE__
let ([Term]
vs1, Term
v : [Term]
vs0) = Nat -> [Term] -> ([Term], [Term])
forall a. Nat -> [a] -> ([a], [a])
splitAt Nat
g1len ([Term] -> ([Term], [Term])) -> [Term] -> ([Term], [Term])
forall a b. (a -> b) -> a -> b
$ (Nat -> Term) -> [Nat] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map Nat -> Term
var [Nat
d2len..Nat
dlenNat -> Nat -> Nat
forall a. Num a => a -> a -> a
-Nat
1]
let numFields :: Nat
numFields = Nat
glen Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
g1len Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
g0len
if Nat
numFields Nat -> Nat -> Bool
forall a. Ord a => a -> a -> Bool
<= Nat
0 then [Term] -> TCMT IO [Term]
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Term] -> TCMT IO [Term]) -> [Term] -> TCMT IO [Term]
forall a b. (a -> b) -> a -> b
$ [Term]
vs1 [Term] -> [Term] -> [Term]
forall a. [a] -> [a] -> [a]
++ [Term]
vs0 else do
let t :: Type
t = (Name, Type) -> Type
forall a b. (a, b) -> b
snd ((Name, Type) -> Type)
-> (Maybe (Dom (Name, Type)) -> (Name, Type))
-> Maybe (Dom (Name, Type))
-> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom (Name, Type) -> (Name, Type)
forall t e. Dom' t e -> e
unDom (Dom (Name, Type) -> (Name, Type))
-> (Maybe (Dom (Name, Type)) -> Dom (Name, Type))
-> Maybe (Dom (Name, Type))
-> (Name, Type)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom (Name, Type) -> Maybe (Dom (Name, Type)) -> Dom (Name, Type)
forall a. a -> Maybe a -> a
fromMaybe Dom (Name, Type)
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe (Dom (Name, Type)) -> Type)
-> Maybe (Dom (Name, Type)) -> Type
forall a b. (a -> b) -> a -> b
$ Context
delta Context -> Nat -> Maybe (Dom (Name, Type))
forall a. [a] -> Nat -> Maybe a
!!! Nat
k
fs <- Type -> TCM [Dom QName]
getRecordTypeFields Type
t
let vfs = (Dom QName -> Term) -> [Dom QName] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map ((\ QName
x -> Term
v Term -> Elims -> Term
forall t. Apply t => t -> Elims -> t
`applyE` [ProjOrigin -> QName -> Elim
forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
ProjSystem QName
x]) (QName -> Term) -> (Dom QName -> QName) -> Dom QName -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom QName -> QName
forall t e. Dom' t e -> e
unDom) [Dom QName]
fs
return $ vs1 ++ reverse (take numFields vfs) ++ vs0
let args = Args -> Args
forall a. [a] -> [a]
reverse (Args -> Args) -> Args -> Args
forall a b. (a -> b) -> a -> b
$ (Term -> Arg (Name, Type) -> Arg Term)
-> [Term] -> [Arg (Name, Type)] -> Args
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Term -> Arg (Name, Type) -> Arg Term
forall a b. a -> Arg b -> Arg a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
(<$) [Term]
rev_args ([Arg (Name, Type)] -> Args) -> [Arg (Name, Type)] -> Args
forall a b. (a -> b) -> a -> b
$ (Dom (Name, Type) -> Arg (Name, Type))
-> Context -> [Arg (Name, Type)]
forall a b. (a -> b) -> [a] -> [b]
map Dom (Name, Type) -> Arg (Name, Type)
forall t a. Dom' t a -> Arg a
argFromDom Context
gamma
let vs = Permutation -> Args -> Args
forall a. Permutation -> [a] -> [a]
permute (Nat -> Permutation -> Permutation
takeP (Args -> Nat
forall a. [a] -> Nat
forall (t :: * -> *) a. Foldable t => t a -> Nat
length Args
args) Permutation
p) Args
args
reportSDoc "tc.interaction" 20 $ vcat
[ "meta reuse arguments:" <+> prettyTCM vs ]
return (x, MetaV x $ map Apply vs)
{-# SPECIALIZE blockTerm :: Type -> TCM Term -> TCM Term #-}
blockTerm
:: (MonadMetaSolver m, MonadConstraint m, MonadFresh Nat m, MonadFresh ProblemId m)
=> Type -> m Term -> m Term
blockTerm :: forall (m :: * -> *).
(MonadMetaSolver m, MonadConstraint m, MonadFresh Nat m,
MonadFresh ProblemId m) =>
Type -> m Term -> m Term
blockTerm Type
t m Term
blocker = do
(pid, v) <- m Term -> m (ProblemId, Term)
forall (m :: * -> *) a.
(MonadFresh ProblemId m, MonadConstraint m) =>
m a -> m (ProblemId, a)
newProblem m Term
blocker
blockTermOnProblem t v pid
{-# SPECIALIZE blockTermOnProblem :: Type -> Term -> ProblemId -> TCM Term #-}
blockTermOnProblem
:: (MonadMetaSolver m, MonadFresh Nat m)
=> Type -> Term -> ProblemId -> m Term
blockTermOnProblem :: forall (m :: * -> *).
(MonadMetaSolver m, MonadFresh Nat m) =>
Type -> Term -> ProblemId -> m Term
blockTermOnProblem Type
t Term
v ProblemId
pid = do
solved <- ProblemId -> m Bool
forall (m :: * -> *).
(MonadTCEnv m, ReadTCState m) =>
ProblemId -> m Bool
isProblemSolved ProblemId
pid
ifM (return solved `or2M` isSizeProblem pid)
(v <$ reportSLn "tc.meta.blocked" 20 ("Not blocking because " ++ show pid ++ " is " ++
if solved then "solved" else "a size problem")) $ do
i <- createMetaInfo
es <- map Apply <$> getContextArgs
tel <- getContextTelescope
x <- newMeta' (BlockedConst $ abstract tel v)
Instantiable
i
lowMetaPriority
(idP $ size tel)
(HasType () CmpLeq $ telePi_ tel t)
inTopContext $ addConstraint (unblockOnProblem pid) (UnBlock x)
reportSDoc "tc.meta.blocked" 20 $ vcat
[ "blocked" <+> prettyTCM x <+> ":=" <+> inTopContext
(prettyTCM $ abstract tel v)
, " by" <+> (prettyTCM =<< getConstraintsForProblem pid)
]
inst <- isInstantiatedMeta x
if inst
then instantiate (MetaV x es)
else do
(m', v) <- newValueMeta DontRunMetaOccursCheck CmpLeq t
reportSDoc "tc.meta.blocked" 30
$ "setting twin of"
<+> prettyTCM m'
<+> "to be"
<+> prettyTCM x
updateMetaVar m' (\MetaVariable
mv -> MetaVariable
mv { mvTwin = Just x })
i <- fresh
cmp <- buildProblemConstraint_ (unblockOnMeta x) (ValueCmp CmpEq (AsTermsOf t) v (MetaV x es))
reportSDoc "tc.constr.add" 20 $ "adding constraint" <+> prettyTCM cmp
listenToMeta (CheckConstraint i cmp) x
return v
{-# SPECIALIZE blockTypeOnProblem :: Type -> ProblemId -> TCM Type #-}
blockTypeOnProblem
:: (MonadMetaSolver m, MonadFresh Nat m)
=> Type -> ProblemId -> m Type
blockTypeOnProblem :: forall (m :: * -> *).
(MonadMetaSolver m, MonadFresh Nat m) =>
Type -> ProblemId -> m Type
blockTypeOnProblem (El Sort
s Term
a) ProblemId
pid = Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El Sort
s (Term -> Type) -> m Term -> m Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Term -> ProblemId -> m Term
forall (m :: * -> *).
(MonadMetaSolver m, MonadFresh Nat m) =>
Type -> Term -> ProblemId -> m Term
blockTermOnProblem (Sort -> Type
sort Sort
s) Term
a ProblemId
pid
unblockedTester :: Type -> TCM Blocker
unblockedTester :: Type -> TCM Blocker
unblockedTester Type
t = Type
-> (Blocker -> Type -> TCM Blocker)
-> (NotBlocked -> Type -> TCM Blocker)
-> TCM Blocker
forall t (m :: * -> *) a.
(Reduce t, IsMeta t, MonadReduce m) =>
t -> (Blocker -> t -> m a) -> (NotBlocked -> t -> m a) -> m a
ifBlocked Type
t (\ Blocker
b Type
_ -> Blocker -> TCM Blocker
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Blocker
b) (\ NotBlocked
_ Type
_ -> Blocker -> TCM Blocker
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Blocker
alwaysUnblock)
postponeTypeCheckingProblem_ :: TypeCheckingProblem -> TCM Term
postponeTypeCheckingProblem_ :: TypeCheckingProblem -> TCM Term
postponeTypeCheckingProblem_ TypeCheckingProblem
p = do
TypeCheckingProblem -> Blocker -> TCM Term
postponeTypeCheckingProblem TypeCheckingProblem
p (Blocker -> TCM Term) -> TCM Blocker -> TCM Term
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TypeCheckingProblem -> TCM Blocker
unblock TypeCheckingProblem
p
where
unblock :: TypeCheckingProblem -> TCM Blocker
unblock (CheckExpr Comparison
_ Expr
_ Type
t) = Type -> TCM Blocker
unblockedTester Type
t
unblock (CheckArgs Comparison
_ ExpandHidden
_ Range
_ [NamedArg Expr]
_ Type
t Type
_ ArgsCheckState CheckedTarget -> TCM Term
_) = Type -> TCM Blocker
unblockedTester Type
t
unblock (CheckProjAppToKnownPrincipalArg Comparison
_ Expr
_ ProjOrigin
_ List1 QName
_ [NamedArg Expr]
_ Type
_ Nat
_ Term
_ Type
t PrincipalArgTypeMetas
_) = Type -> TCM Blocker
unblockedTester Type
t
unblock (CheckLambda Comparison
_ Arg (List1 (WithHiding Name), Maybe Type)
_ Expr
_ Type
t) = Type -> TCM Blocker
unblockedTester Type
t
unblock (DoQuoteTerm Comparison
_ Term
_ Type
_) = TCM Blocker
forall a. HasCallStack => a
__IMPOSSIBLE__
postponeTypeCheckingProblem :: TypeCheckingProblem -> Blocker -> TCM Term
postponeTypeCheckingProblem :: TypeCheckingProblem -> Blocker -> TCM Term
postponeTypeCheckingProblem TypeCheckingProblem
p Blocker
unblock | Blocker
unblock Blocker -> Blocker -> Bool
forall a. Eq a => a -> a -> Bool
== Blocker
alwaysUnblock = do
[Char] -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"impossible" Nat
2 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Postponed without blocker:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> TypeCheckingProblem -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => TypeCheckingProblem -> m Doc
prettyTCM TypeCheckingProblem
p
TCM Term
forall a. HasCallStack => a
__IMPOSSIBLE__
postponeTypeCheckingProblem TypeCheckingProblem
p Blocker
unblock = do
i <- RunMetaOccursCheck -> TCMT IO MetaInfo
forall (m :: * -> *).
(MonadTCEnv m, ReadTCState m) =>
RunMetaOccursCheck -> m MetaInfo
createMetaInfo' RunMetaOccursCheck
DontRunMetaOccursCheck
tel <- getContextTelescope
cl <- buildClosure p
let t = TypeCheckingProblem -> Type
problemType TypeCheckingProblem
p
m <- newMeta' (PostponedTypeCheckingProblem cl)
Instantiable i normalMetaPriority (idP (size tel))
$ HasType () CmpLeq $ telePi_ tel t
inTopContext $ reportSDoc "tc.meta.postponed" 20 $ vcat
[ "new meta" <+> prettyTCM m <+> ":" <+> prettyTCM (telePi_ tel t)
, "for postponed typechecking problem" <+> prettyTCM p
]
es <- map Apply <$> getContextArgs
(_, v) <- newValueMeta DontRunMetaOccursCheck CmpLeq t
cmp <- buildProblemConstraint_ (unblockOnMeta m) (ValueCmp CmpEq (AsTermsOf t) v (MetaV m es))
reportSDoc "tc.constr.add" 20 $ "adding constraint" <+> prettyTCM cmp
i <- liftTCM fresh
listenToMeta (CheckConstraint i cmp) m
addConstraint unblock (UnBlock m)
return v
problemType :: TypeCheckingProblem -> Type
problemType :: TypeCheckingProblem -> Type
problemType (CheckExpr Comparison
_ Expr
_ Type
t ) = Type
t
problemType (CheckArgs Comparison
_ ExpandHidden
_ Range
_ [NamedArg Expr]
_ Type
_ Type
t ArgsCheckState CheckedTarget -> TCM Term
_ ) = Type
t
problemType (CheckProjAppToKnownPrincipalArg Comparison
_ Expr
_ ProjOrigin
_ List1 QName
_ [NamedArg Expr]
_ Type
t Nat
_ Term
_ Type
_ PrincipalArgTypeMetas
_) = Type
t
problemType (CheckLambda Comparison
_ Arg (List1 (WithHiding Name), Maybe Type)
_ Expr
_ Type
t ) = Type
t
problemType (DoQuoteTerm Comparison
_ Term
_ Type
t) = Type
t
etaExpandMetaTCM :: [MetaClass] -> MetaId -> TCM ()
etaExpandMetaTCM :: [MetaClass] -> MetaId -> TCM ()
etaExpandMetaTCM [MetaClass]
kinds MetaId
m = TCM Bool -> TCM () -> TCM ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM ((Bool -> Bool
not (Bool -> Bool) -> TCM Bool -> TCM Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> TCM Bool
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m Bool
isFrozen MetaId
m) TCM Bool -> TCM Bool -> TCM Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`and2M` (TCEnv -> Bool) -> TCM Bool
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Bool
envAssignMetas TCM Bool -> TCM Bool -> TCM Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`and2M` [MetaClass] -> MetaId -> TCM Bool
isEtaExpandable [MetaClass]
kinds MetaId
m) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
[Char] -> Nat -> [Char] -> TCM () -> TCM ()
forall a. [Char] -> Nat -> [Char] -> TCMT IO a -> TCMT IO a
forall (m :: * -> *) a.
MonadDebug m =>
[Char] -> Nat -> [Char] -> m a -> m a
verboseBracket [Char]
"tc.meta.eta" Nat
20 ([Char]
"etaExpandMeta " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ MetaId -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow MetaId
m) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
let waitFor :: Blocker -> TCM ()
waitFor Blocker
b = do
[Char] -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.eta" Nat
20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
TCMT IO Doc
"postponing eta-expansion of meta variable" 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 -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
TCMT IO Doc
"which is blocked by" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Blocker -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Blocker -> m Doc
prettyTCM Blocker
b
(MetaId -> TCM ()) -> Set MetaId -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Listener -> MetaId -> TCM ()
forall (m :: * -> *).
MonadMetaSolver m =>
Listener -> MetaId -> m ()
listenToMeta (MetaId -> Listener
EtaExpand MetaId
m)) (Set MetaId -> TCM ()) -> Set MetaId -> TCM ()
forall a b. (a -> b) -> a -> b
$ Blocker -> Set MetaId
allBlockingMetas Blocker
b
dontExpand :: TCM ()
dontExpand = do
[Char] -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.eta" Nat
20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
TCMT IO Doc
"we do not expand meta variable" 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 -> 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 ([Char]
"(requested was expansion of " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [MetaClass] -> [Char]
forall a. Show a => a -> [Char]
show [MetaClass]
kinds [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
")")
meta <- MetaId -> TCMT IO MetaVariable
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta MetaId
m
case mvJudgement meta of
IsSort{} -> TCM ()
dontExpand
HasType MetaId
_ Comparison
cmp Type
a -> do
[Char] -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.eta" Nat
40 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
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
sep
[ [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
"considering eta-expansion at type "
, Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
a
, [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
" raw: "
, Type -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Type
a
]
TelV tel b <- Type -> TCMT IO (TelV Type)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView Type
a
reportSDoc "tc.meta.eta" 40 $ sep
[ text "considering eta-expansion at type"
, addContext tel (prettyTCM b)
, text "under telescope"
, prettyTCM tel
]
if any domIsFinite (flattenTel tel) then dontExpand else do
addContext tel $ do
ifBlocked (unEl b) (\ Blocker
x Term
_ -> Blocker -> TCM ()
waitFor Blocker
x) $ \ NotBlocked
_ Term
t -> case Term
t of
lvl :: Term
lvl@(Def QName
r Elims
es) ->
TCM Bool -> TCM () -> TCM () -> TCM ()
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (QName -> TCM Bool
forall (m :: * -> *). HasConstInfo m => QName -> m Bool
isEtaRecord QName
r) (do
let ps :: Args
ps = Args -> Maybe Args -> Args
forall a. a -> Maybe a -> a
fromMaybe Args
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
forall a b. (a -> b) -> a -> b
$ Elims -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
let expand :: TCM ()
expand = do
u <- MetaVariable -> TCM Term -> TCM Term
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadTrace m) =>
MetaVariable -> m a -> m a
withMetaInfo' MetaVariable
meta (TCM Term -> TCM Term) -> TCM Term -> TCM Term
forall a b. (a -> b) -> a -> b
$
[Char]
-> Frozen
-> QName
-> Args
-> Tele (Dom Type)
-> Permutation
-> Args
-> TCM Term
newRecordMetaCtx (MetaInfo -> [Char]
miNameSuggestion (MetaVariable -> MetaInfo
mvInfo MetaVariable
meta))
(MetaVariable -> Frozen
mvFrozen MetaVariable
meta) QName
r Args
ps Tele (Dom Type)
tel (Nat -> Permutation
idP (Nat -> Permutation) -> Nat -> Permutation
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> Nat
forall a. Sized a => a -> Nat
size Tele (Dom Type)
tel) (Args -> TCM Term) -> Args -> TCM Term
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> Args
forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
teleArgs Tele (Dom Type)
tel
inTopContext $ do
reportSDoc "tc.meta.eta" 15 $ sep
[ "eta expanding: " <+> pretty m <+> " --> "
, nest 2 $ prettyTCM u
]
noConstraints $ assignTerm' m (telToArgs tel) u
if MetaClass
Records MetaClass -> [MetaClass] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [MetaClass]
kinds then
TCM ()
expand
else if (MetaClass
SingletonRecords MetaClass -> [MetaClass] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [MetaClass]
kinds) then
(Blocker -> TCM ()) -> TCM () -> TCM ()
forall a. (Blocker -> TCMT IO a) -> TCMT IO a -> TCMT IO a
forall (m :: * -> *) a.
MonadBlock m =>
(Blocker -> m a) -> m a -> m a
catchPatternErr (\Blocker
x -> Blocker -> TCM ()
waitFor Blocker
x) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
TCM Bool -> TCM () -> TCM () -> TCM ()
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (QName -> Args -> TCM Bool
forall (m :: * -> *).
(PureTCM m, MonadBlock m) =>
QName -> Args -> m Bool
isSingletonRecord QName
r Args
ps) TCM ()
expand TCM ()
dontExpand
else TCM ()
dontExpand
) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM Bool -> TCM () -> TCM () -> TCM ()
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM ([TCM Bool] -> TCM Bool
forall (f :: * -> *) (m :: * -> *).
(Foldable f, Monad m) =>
f (m Bool) -> m Bool
andM [ Bool -> TCM Bool
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> TCM Bool) -> Bool -> TCM Bool
forall a b. (a -> b) -> a -> b
$ MetaClass
Levels MetaClass -> [MetaClass] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [MetaClass]
kinds
, TCM Bool
forall (m :: * -> *). HasOptions m => m Bool
typeInType
, (Term -> Maybe Term
forall a. a -> Maybe a
Just Term
lvl Maybe Term -> Maybe Term -> Bool
forall a. Eq a => a -> a -> Bool
==) (Maybe Term -> Bool) -> TCMT IO (Maybe Term) -> TCM Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BuiltinId -> TCMT IO (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinLevel
]) (do
[Char] -> Nat -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> [Char] -> m ()
reportSLn [Char]
"tc.meta.eta" Nat
20 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$ [Char]
"Expanding level meta to 0 (type-in-type)"
TCM () -> TCM ()
forall (m :: * -> *) a.
(MonadConstraint m, MonadWarning m, MonadError TCErr m,
MonadFresh ProblemId m) =>
m a -> m a
noConstraints (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ MetaId -> [Arg [Char]] -> Term -> TCM ()
forall (m :: * -> *).
MonadMetaSolver m =>
MetaId -> [Arg [Char]] -> Term -> m ()
assignTerm MetaId
m (Tele (Dom Type) -> [Arg [Char]]
forall a. TelToArgs a => a -> [Arg [Char]]
telToArgs Tele (Dom Type)
tel) (Term -> TCM ()) -> Term -> TCM ()
forall a b. (a -> b) -> a -> b
$ Level -> Term
Level (Level -> Term) -> Level -> Term
forall a b. (a -> b) -> a -> b
$ Integer -> Level
ClosedLevel Integer
0
) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM ()
dontExpand
Term
_ -> TCM ()
dontExpand
etaExpandBlocked :: (MonadReduce m, MonadMetaSolver m, IsMeta t, Reduce t)
=> Blocked t -> m (Blocked t)
etaExpandBlocked :: forall (m :: * -> *) t.
(MonadReduce m, MonadMetaSolver m, IsMeta t, Reduce t) =>
Blocked t -> m (Blocked t)
etaExpandBlocked t :: Blocked t
t@NotBlocked{} = Blocked t -> m (Blocked t)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Blocked t
t
etaExpandBlocked t :: Blocked t
t@(Blocked Blocker
_ t
v) | Just{} <- t -> Maybe MetaId
forall a. IsMeta a => a -> Maybe MetaId
isMeta t
v = Blocked t -> m (Blocked t)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Blocked t
t
etaExpandBlocked (Blocked Blocker
b t
t) = do
[Char] -> Nat -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.eta" Nat
30 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Eta expanding blockers" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Blocker -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Blocker
b
(MetaId -> m ()) -> Set MetaId -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ([MetaClass] -> MetaId -> m ()
forall (m :: * -> *).
MonadMetaSolver m =>
[MetaClass] -> MetaId -> m ()
etaExpandMeta [MetaClass
Records]) (Set MetaId -> m ()) -> Set MetaId -> m ()
forall a b. (a -> b) -> a -> b
$ Blocker -> Set MetaId
allBlockingMetas Blocker
b
t <- t -> m (Blocked t)
forall a (m :: * -> *).
(Reduce a, MonadReduce m) =>
a -> m (Blocked a)
reduceB t
t
case t of
Blocked Blocker
b' t
_ | Blocker
b Blocker -> Blocker -> Bool
forall a. Eq a => a -> a -> Bool
/= Blocker
b' -> Blocked t -> m (Blocked t)
forall (m :: * -> *) t.
(MonadReduce m, MonadMetaSolver m, IsMeta t, Reduce t) =>
Blocked t -> m (Blocked t)
etaExpandBlocked Blocked t
t
Blocked t
_ -> Blocked t -> m (Blocked t)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Blocked t
t
{-# SPECIALIZE assignWrapper :: CompareDirection -> MetaId -> Elims -> Term -> TCM () -> TCM () #-}
assignWrapper :: (MonadMetaSolver m, MonadConstraint m, MonadError TCErr m, MonadDebug m, HasOptions m)
=> CompareDirection -> MetaId -> Elims -> Term -> m () -> m ()
assignWrapper :: forall (m :: * -> *).
(MonadMetaSolver m, MonadConstraint m, MonadError TCErr m,
MonadDebug m, HasOptions m) =>
CompareDirection -> MetaId -> Elims -> Term -> m () -> m ()
assignWrapper CompareDirection
dir MetaId
x Elims
es Term
v m ()
doAssign = do
m Bool -> m () -> m () -> m ()
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifNotM ((TCEnv -> Bool) -> m Bool
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Bool
envAssignMetas) m ()
forall {b}. m b
dontAssign (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
[Char] -> Nat -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.assign" Nat
10 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ do
TCMT IO Doc
"term" 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 (MetaId -> Elims -> Term
MetaV MetaId
x Elims
es) 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 ([Char]
":" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ CompareDirection -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow CompareDirection
dir) 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
v
m () -> m ()
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
nowSolvingConstraints m ()
doAssign m () -> m () -> m ()
forall e (m :: * -> *) a. MonadError e m => m a -> m () -> m a
`finally` m ()
forall (m :: * -> *). MonadConstraint m => m ()
solveAwakeConstraints
where dontAssign :: m b
dontAssign = do
[Char] -> Nat -> [Char] -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> [Char] -> m ()
reportSLn [Char]
"tc.meta.assign" Nat
10 [Char]
"don't assign metas"
Blocker -> m b
forall a. Blocker -> m a
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
alwaysUnblock
assign :: CompareDirection -> MetaId -> Args -> Term -> CompareAs -> TCM ()
assign :: CompareDirection -> MetaId -> Args -> Term -> CompareAs -> TCM ()
assign CompareDirection
dir MetaId
x Args
args Term
v CompareAs
target = Blocker -> TCM () -> TCM ()
forall (m :: * -> *) a.
(PureTCM m, MonadBlock m) =>
Blocker -> m a -> m a
addOrUnblocker (MetaId -> Blocker
unblockOnMeta MetaId
x) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
mvar <- MetaId -> TCMT IO MetaVariable
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta MetaId
x
let t = 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
mvar
reportSDoc "tc.meta.assign" 25 $ "v = " <+> prettyTCM v
v <- instantiate v
reportSDoc "tc.meta.assign" 25 $ "v = " <+> prettyTCM v
reportSDoc "tc.meta.assign" 45 $
"MetaVars.assign: assigning meta " <+> prettyTCM (MetaV x []) <+>
" with args " <+> prettyList_ (map (prettyTCM . unArg) args) <+>
" to " <+> prettyTCM v
reportSDoc "tc.meta.assign" 45 $
"MetaVars.assign: type of meta: " <+> prettyTCM t
reportSDoc "tc.meta.assign" 75 $
text "MetaVars.assign: assigning meta " <> pretty x <> text " with args " <> pretty args <> text " to " <> pretty v
let
boundary Term
v = do
cubical <- TCMT IO (Maybe Cubical)
forall (m :: * -> *). HasOptions m => m (Maybe Cubical)
cubicalOption
isip <- isInteractionMetaB x args
case (,) <$> cubical <*> isip of
Just (Cubical
_, (MetaId
x, InteractionId
ip, Args
args)) -> CompareDirection
-> MetaId -> InteractionId -> Args -> Term -> CompareAs -> TCM ()
tryAddBoundary CompareDirection
dir MetaId
x InteractionId
ip Args
args Term
v CompareAs
target
Maybe (Cubical, (MetaId, InteractionId, Args))
_ -> () -> TCM ()
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
case (v, mvJudgement mvar) of
(Sort Sort
s, HasType{}) -> Sort -> TCM ()
hasBiggerSort Sort
s
(Term, Judgement MetaId)
_ -> () -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
cumulativity <- optCumulativity <$> pragmaOptions
let checkSolutionSort Comparison
cmp Sort
s Term
v = do
s' <- Term -> TCM Sort
forall (m :: * -> *).
(PureTCM m, MonadBlock m, MonadConstraint m) =>
Term -> m Sort
sortOf Term
v
reportSDoc "tc.meta.assign" 40 $
"Instantiating sort" <+> prettyTCM s <+>
"to sort" <+> prettyTCM s' <+> "of solution" <+> prettyTCM v
traceCall (CheckMetaSolution (getRange mvar) x (sort s) v) $
compareSort cmp s' s
case (target , mvJudgement mvar) of
(AsTypes{} , HasType MetaId
_ Comparison
cmp0 Type
t) -> do
let cmp :: Comparison
cmp = if Bool
cumulativity then Comparison
cmp0 else Comparison
CmpEq
abort :: TCMT IO Empty
abort = Blocker -> TCMT IO Empty
forall a. Blocker -> TCMT IO a
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation (Blocker -> TCMT IO Empty) -> TCM Blocker -> TCMT IO Empty
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Blocker -> TCM Blocker
forall (m :: * -> *). PureTCM m => Blocker -> m Blocker
updateBlocker (Type -> Blocker
forall t. AllMetas t => t -> Blocker
unblockOnAnyMetaIn Type
t)
t' <- TCMT IO Empty -> Type -> Args -> TCM Type
forall a (m :: * -> *).
(PiApplyM a, MonadReduce m, HasBuiltins m) =>
m Empty -> Type -> a -> m Type
forall (m :: * -> *).
(MonadReduce m, HasBuiltins m) =>
m Empty -> Type -> Args -> m Type
piApplyM' TCMT IO Empty
abort Type
t Args
args
s <- shouldBeSort t'
checkSolutionSort cmp s v
(AsTermsOf{} , HasType MetaId
_ Comparison
cmp Type
t)
| Bool
cumulativity -> do
let abort :: TCMT IO Empty
abort = Blocker -> TCMT IO Empty
forall a. Blocker -> TCMT IO a
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation (Blocker -> TCMT IO Empty) -> TCM Blocker -> TCMT IO Empty
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Blocker -> TCM Blocker
forall (m :: * -> *). PureTCM m => Blocker -> m Blocker
updateBlocker (Type -> Blocker
forall t. AllMetas t => t -> Blocker
unblockOnAnyMetaIn Type
t)
t' <- TCMT IO Empty -> Type -> Args -> TCM Type
forall a (m :: * -> *).
(PiApplyM a, MonadReduce m, HasBuiltins m) =>
m Empty -> Type -> a -> m Type
forall (m :: * -> *).
(MonadReduce m, HasBuiltins m) =>
m Empty -> Type -> Args -> m Type
piApplyM' TCMT IO Empty
abort Type
t Args
args
TelV tel t'' <- telView t'
addContext tel $ ifNotSort t'' (return ()) $ \Sort
s -> do
let v' :: Term
v' = Nat -> Term -> Term
forall a. Subst a => Nat -> a -> a
raise (Tele (Dom Type) -> Nat
forall a. Sized a => a -> Nat
size Tele (Dom Type)
tel) Term
v Term -> Args -> Term
forall t. Apply t => t -> Args -> t
`apply` Tele (Dom Type) -> Args
forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
teleArgs Tele (Dom Type)
tel
Comparison -> Sort -> Term -> TCM ()
checkSolutionSort Comparison
cmp Sort
s Term
v'
(AsTypes{} , IsSort{} ) -> () -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
(AsTermsOf{} , Judgement MetaId
_ ) -> () -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
(AsSizes{} , Judgement MetaId
_ ) -> () -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
when (mvFrozen mvar == Frozen) $ do
reportSLn "tc.meta.assign" 25 $ "aborting: meta is frozen!"
boundary v
patternViolation neverUnblock
whenM (isBlockedTerm x) $ do
reportSLn "tc.meta.assign" 25 $ "aborting: meta is a blocked term!"
patternViolation (unblockOnMeta x)
reportSLn "tc.meta.assign" 50 $ "MetaVars.assign: I want to see whether rhs is blocked"
reportSDoc "tc.meta.assign" 25 $ do
v0 <- reduceB v
case v0 of
Blocked Blocker
m0 Term
_ -> TCMT IO Doc
"r.h.s. blocked on:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Blocker -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Blocker -> m Doc
prettyTCM Blocker
m0
NotBlocked{} -> TCMT IO Doc
"r.h.s. not blocked"
reportSDoc "tc.meta.assign" 25 $ "v = " <+> prettyTCM v
subtypingForSizeLt dir x mvar t args v $ \ Term
v -> do
[Char] -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.assign" Nat
25 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"v = " 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
v
[Char] -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.assign.proj" Nat
45 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
cxt <- TCMT IO (Tele (Dom Type))
forall (m :: * -> *).
(Applicative m, MonadTCEnv m) =>
m (Tele (Dom Type))
getContextTelescope
vcat
[ "context before projection expansion"
, nest 2 $ inTopContext $ prettyTCM cxt
]
Args
-> (Term, CompareAs)
-> (Args -> (Term, CompareAs) -> TCM ())
-> TCM ()
forall a b c.
(Pretty a, PrettyTCM a, NoProjectedVar a, ReduceAndEtaContract a,
PrettyTCM b, TermSubst b) =>
a -> b -> (a -> b -> TCM c) -> TCM c
expandProjectedVars Args
args (Term
v, CompareAs
target) ((Args -> (Term, CompareAs) -> TCM ()) -> TCM ())
-> (Args -> (Term, CompareAs) -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ Args
args (Term
v, CompareAs
target) -> do
[Char] -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.assign.proj" Nat
45 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
cxt <- TCMT IO (Tele (Dom Type))
forall (m :: * -> *).
(Applicative m, MonadTCEnv m) =>
m (Tele (Dom Type))
getContextTelescope
vcat
[ "context after projection expansion"
, nest 2 $ inTopContext $ prettyTCM cxt
]
let
vars :: VarMap
vars = Args -> VarMap
forall a c t. (IsVarSet a c, Singleton Nat c, Free t) => t -> c
freeVars Args
args
relVL :: [Nat]
relVL = (VarOcc -> Bool) -> VarMap -> [Nat]
filterVarMapToList VarOcc -> Bool
forall a. LensRelevance a => a -> Bool
isRelevant VarMap
vars
nonstrictVL :: [Nat]
nonstrictVL = (VarOcc -> Bool) -> VarMap -> [Nat]
filterVarMapToList VarOcc -> Bool
forall a. LensRelevance a => a -> Bool
isNonStrict VarMap
vars
irrVL :: [Nat]
irrVL = (VarOcc -> Bool) -> VarMap -> [Nat]
filterVarMapToList ((Bool -> Bool -> Bool)
-> (VarOcc -> Bool) -> (VarOcc -> Bool) -> VarOcc -> Bool
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 Bool -> Bool -> Bool
(&&) VarOcc -> Bool
forall a. LensRelevance a => a -> Bool
isIrrelevant VarOcc -> Bool
forall o a. LensFlexRig o a => o -> Bool
isUnguarded) VarMap
vars
[Char] -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.assign" Nat
20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
let pr :: Term -> m Doc
pr (Var Nat
n []) = [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text (Nat -> [Char]
forall a. Show a => a -> [Char]
show Nat
n)
pr (Def QName
c []) = QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
c
pr Term
_ = m Doc
".."
in [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ TCMT IO Doc
"mvar args:" 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, Foldable t) =>
t (m Doc) -> m Doc
sep ((Arg Term -> TCMT IO Doc) -> Args -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Term -> TCMT IO Doc
forall {m :: * -> *}.
(MonadFresh NameId m, MonadInteractionPoints m,
MonadStConcreteNames m, PureTCM m, IsString (m Doc), Null (m Doc),
Semigroup (m Doc)) =>
Term -> m Doc
pr (Term -> TCMT IO Doc)
-> (Arg Term -> Term) -> Arg Term -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg Term -> Term
forall e. Arg e -> e
unArg) Args
args)
, TCMT IO Doc
"fvars lhs (rel):" 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, Foldable t) =>
t (m Doc) -> m Doc
sep ((Nat -> TCMT IO Doc) -> [Nat] -> [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) -> (Nat -> [Char]) -> Nat -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Nat -> [Char]
forall a. Show a => a -> [Char]
show) [Nat]
relVL)
, TCMT IO Doc
"fvars lhs (nonstrict):" 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, Foldable t) =>
t (m Doc) -> m Doc
sep ((Nat -> TCMT IO Doc) -> [Nat] -> [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) -> (Nat -> [Char]) -> Nat -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Nat -> [Char]
forall a. Show a => a -> [Char]
show) [Nat]
nonstrictVL)
, TCMT IO Doc
"fvars lhs (irr):" 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, Foldable t) =>
t (m Doc) -> m Doc
sep ((Nat -> TCMT IO Doc) -> [Nat] -> [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) -> (Nat -> [Char]) -> Nat -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Nat -> [Char]
forall a. Show a => a -> [Char]
show) [Nat]
irrVL)
]
v <- TCM Term -> TCM Term
forall a. TCM a -> TCM a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM Term -> TCM Term) -> TCM Term -> TCM Term
forall a b. (a -> b) -> a -> b
$ MetaId -> VarMap -> Term -> TCM Term
occursCheck MetaId
x VarMap
vars Term
v
reportSLn "tc.meta.assign" 15 "passed occursCheck"
reportSDoc "tc.meta.assign" 25 $ "v = " <+> prettyTCM v
verboseS "tc.meta.assign" 30 $ do
let n = Term -> Nat
forall a. TermSize a => a -> Nat
termSize Term
v
when (n > 200) $ reportSDoc "tc.meta.assign" 30 $
sep [ "size" <+> text (show n)
, nest 2 $ "term" <+> prettyTCM v
]
let fvs = Term -> VarSet
forall t. Free t => t -> VarSet
allFreeVars Term
v
reportSDoc "tc.meta.assign" 20 $
"fvars rhs:" <+> sep (map (text . show) $ VarSet.toList fvs)
mids <- do
res <- runExceptT $ inverseSubst' (const False) args
case res of
Right [(Nat, Term)]
ids -> do
[Char] -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.assign" Nat
60 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
TCMT IO Doc
"inverseSubst returns:" 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, Foldable t) =>
t (m Doc) -> m Doc
sep (((Nat, Term) -> TCMT IO Doc) -> [(Nat, Term)] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Nat, Term) -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [(Nat, Term)]
ids)
[Char] -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.assign" Nat
50 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
TCMT IO Doc
"inverseSubst returns:" 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, Foldable t) =>
t (m Doc) -> m Doc
sep (((Nat, Term) -> TCMT IO Doc) -> [(Nat, Term)] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Nat, Term) -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => (Nat, Term) -> m Doc
prettyTCM [(Nat, Term)]
ids)
let boundVars :: VarSet
boundVars = [Nat] -> VarSet
VarSet.fromList ([Nat] -> VarSet) -> [Nat] -> VarSet
forall a b. (a -> b) -> a -> b
$ ((Nat, Term) -> Nat) -> [(Nat, Term)] -> [Nat]
forall a b. (a -> b) -> [a] -> [b]
map (Nat, Term) -> Nat
forall a b. (a, b) -> a
fst [(Nat, Term)]
ids
if VarSet
fvs VarSet -> VarSet -> Bool
`VarSet.isSubsetOf` VarSet
boundVars
then Maybe [(Nat, Term)] -> TCMT IO (Maybe [(Nat, Term)])
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe [(Nat, Term)] -> TCMT IO (Maybe [(Nat, Term)]))
-> Maybe [(Nat, Term)] -> TCMT IO (Maybe [(Nat, Term)])
forall a b. (a -> b) -> a -> b
$ [(Nat, Term)] -> Maybe [(Nat, Term)]
forall a. a -> Maybe a
Just [(Nat, Term)]
ids
else Maybe [(Nat, Term)] -> TCMT IO (Maybe [(Nat, Term)])
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe [(Nat, Term)]
forall a. Maybe a
Nothing
Left (CantInvert Term
tm) -> Maybe [(Nat, Term)]
forall a. Maybe a
Nothing Maybe [(Nat, Term)] -> TCM () -> TCMT IO (Maybe [(Nat, Term)])
forall a b. a -> TCMT IO b -> TCMT IO a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Term -> TCM ()
boundary Term
v
Left InvertExcept
NeutralArg -> [(Nat, Term)] -> Maybe [(Nat, Term)]
forall a. a -> Maybe a
Just ([(Nat, Term)] -> Maybe [(Nat, Term)])
-> TCMT IO [(Nat, Term)] -> TCMT IO (Maybe [(Nat, Term)])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> Args -> VarSet -> TCMT IO [(Nat, Term)]
forall a. MetaId -> Args -> VarSet -> TCM a
attemptPruning MetaId
x Args
args VarSet
fvs
Left ProjVar{} -> [(Nat, Term)] -> Maybe [(Nat, Term)]
forall a. a -> Maybe a
Just ([(Nat, Term)] -> Maybe [(Nat, Term)])
-> TCMT IO [(Nat, Term)] -> TCMT IO (Maybe [(Nat, Term)])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> Args -> VarSet -> TCMT IO [(Nat, Term)]
forall a. MetaId -> Args -> VarSet -> TCM a
attemptPruning MetaId
x Args
args VarSet
fvs
case mids of
Maybe [(Nat, Term)]
Nothing -> Blocker -> TCM ()
forall a. Blocker -> TCMT IO a
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation (Blocker -> TCM ()) -> TCM Blocker -> TCM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Blocker -> TCM Blocker
forall (m :: * -> *). PureTCM m => Blocker -> m Blocker
updateBlocker (Term -> Blocker
forall t. AllMetas t => t -> Blocker
unblockOnAnyMetaIn Term
v)
Just [(Nat, Term)]
ids -> do
ids <- do
res <- ExceptT () (TCMT IO) [(Nat, Term)] -> TCM (Either () [(Nat, Term)])
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (ExceptT () (TCMT IO) [(Nat, Term)]
-> TCM (Either () [(Nat, Term)]))
-> ExceptT () (TCMT IO) [(Nat, Term)]
-> TCM (Either () [(Nat, Term)])
forall a b. (a -> b) -> a -> b
$ [(Nat, Term)] -> ExceptT () (TCMT IO) [(Nat, Term)]
checkLinearity [(Nat, Term)]
ids
case res of
Right [(Nat, Term)]
ids -> [(Nat, Term)] -> TCMT IO [(Nat, Term)]
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return [(Nat, Term)]
ids
Left () -> do
block <- Blocker -> TCM Blocker
forall (m :: * -> *). PureTCM m => Blocker -> m Blocker
updateBlocker (Blocker -> TCM Blocker) -> Blocker -> TCM Blocker
forall a b. (a -> b) -> a -> b
$ Term -> Blocker
forall t. AllMetas t => t -> Blocker
unblockOnAnyMetaIn Term
v
addOrUnblocker block $ attemptPruning x args fvs
() <- do
let idvars = ((Nat, Term) -> (Nat, VarSet)) -> [(Nat, Term)] -> [(Nat, VarSet)]
forall a b. (a -> b) -> [a] -> [b]
map ((Term -> VarSet) -> (Nat, Term) -> (Nat, VarSet)
forall b d a. (b -> d) -> (a, b) -> (a, d)
mapSnd Term -> VarSet
forall t. Free t => t -> VarSet
allFreeVars) [(Nat, Term)]
ids
let earlierThan a
l a
j = a
j a -> a -> Bool
forall a. Ord a => a -> a -> Bool
> a
l
TelV tel' _ <- telViewUpToPath (length args) t
forM_ ids $ \(Nat
i,Term
u) -> do
d <- Nat -> TCMT IO (Dom (Name, Type))
forall (m :: * -> *).
(MonadFail m, MonadTCEnv m) =>
Nat -> m (Dom (Name, Type))
lookupBV Nat
i
case getLock (getArgInfo d) of
Lock
IsNotLock -> () -> TCM ()
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
IsLock{} -> do
let us :: VarSet
us = [VarSet] -> VarSet
forall (f :: * -> *). Foldable f => f VarSet -> VarSet
IntSet.unions ([VarSet] -> VarSet) -> [VarSet] -> VarSet
forall a b. (a -> b) -> a -> b
$ ((Nat, VarSet) -> VarSet) -> [(Nat, VarSet)] -> [VarSet]
forall a b. (a -> b) -> [a] -> [b]
map (Nat, VarSet) -> VarSet
forall a b. (a, b) -> b
snd ([(Nat, VarSet)] -> [VarSet]) -> [(Nat, VarSet)] -> [VarSet]
forall a b. (a -> b) -> a -> b
$ ((Nat, VarSet) -> Bool) -> [(Nat, VarSet)] -> [(Nat, VarSet)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Nat -> Nat -> Bool
forall a. Ord a => a -> a -> Bool
earlierThan Nat
i (Nat -> Bool) -> ((Nat, VarSet) -> Nat) -> (Nat, VarSet) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Nat, VarSet) -> Nat
forall a b. (a, b) -> a
fst) [(Nat, VarSet)]
idvars
Tele (Dom Type) -> TCM () -> TCM ()
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Tele (Dom Type) -> m a -> m a
addContext Tele (Dom Type)
tel' (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ Term -> VarSet -> TCM ()
checkEarlierThan Term
u VarSet
us
TCM () -> (TCErr -> TCM ()) -> TCM ()
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` \case
TypeError{} -> Blocker -> TCM ()
forall a. Blocker -> TCMT IO a
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation (MetaId -> Blocker
unblockOnMeta MetaId
x)
TCErr
err -> TCErr -> TCM ()
forall a. TCErr -> TCMT IO a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError TCErr
err
let n = Args -> Nat
forall a. [a] -> Nat
forall (t :: * -> *) a. Foldable t => t a -> Nat
length Args
args
TelV tel' _ <- telViewUpToPath n t
let sigma = [Term] -> Substitution
forall a. DeBruijn a => [a] -> Substitution' a
parallelS ([Term] -> Substitution) -> [Term] -> Substitution
forall a b. (a -> b) -> a -> b
$ [Term] -> [Term]
forall a. [a] -> [a]
reverse ([Term] -> [Term]) -> [Term] -> [Term]
forall a b. (a -> b) -> a -> b
$ (Arg Term -> Term) -> Args -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Term
forall e. Arg e -> e
unArg Args
args
hasSubtyping <- optCumulativity <$> pragmaOptions
when hasSubtyping $ forM_ ids $ \(Nat
i , Term
u) -> do
a <- Substitution' (SubstArg Type) -> Type -> Type
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution
Substitution' (SubstArg Type)
sigma (Type -> Type) -> TCM Type -> TCM Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Tele (Dom Type) -> TCM Type -> TCM Type
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Tele (Dom Type) -> m a -> m a
addContext Tele (Dom Type)
tel' (Term -> TCM Type
forall (m :: * -> *). MonadCheckInternal m => Term -> m Type
infer Term
u)
a' <- typeOfBV i
checkSubtypeIsEqual a' a
`catchError` \case
TypeError{} -> Blocker -> TCM ()
forall a. Blocker -> TCMT IO a
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation (MetaId -> Blocker
unblockOnMeta MetaId
x)
TCErr
err -> TCErr -> TCM ()
forall a. TCErr -> TCMT IO a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError TCErr
err
m <- getContextSize
assignMeta' m x t n ids v
where
attemptPruning
:: MetaId
-> Args
-> FVs
-> TCM a
attemptPruning :: forall a. MetaId -> Args -> VarSet -> TCM a
attemptPruning MetaId
x Args
args VarSet
fvs = do
killResult <- MetaId -> Args -> (Nat -> Bool) -> TCMT IO PruneResult
forall (m :: * -> *).
(PureTCM m, MonadMetaSolver m) =>
MetaId -> Args -> (Nat -> Bool) -> m PruneResult
prune MetaId
x Args
args ((Nat -> Bool) -> TCMT IO PruneResult)
-> (Nat -> Bool) -> TCMT IO PruneResult
forall a b. (a -> b) -> a -> b
$ (Nat -> VarSet -> Bool
`VarSet.member` VarSet
fvs)
let success = PruneResult
killResult PruneResult -> [PruneResult] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [PruneResult
PrunedSomething,PruneResult
PrunedEverything]
reportSDoc "tc.meta.assign" 10 $
"pruning" <+> prettyTCM x <+> do text $ if success then "succeeded" else "failed"
blocker <- if
| success -> return alwaysUnblock
| otherwise -> unblockOnAnyMetaIn . MetaV x . map Apply <$> instantiateFull args
patternViolation blocker
isInteractionMetaB
:: forall m. (ReadTCState m, MonadReduce m, MonadPretty m)
=> MetaId
-> Args
-> m (Maybe (MetaId, InteractionId, Args))
isInteractionMetaB :: forall (m :: * -> *).
(ReadTCState m, MonadReduce m, MonadPretty m) =>
MetaId -> Args -> m (Maybe (MetaId, InteractionId, Args))
isInteractionMetaB MetaId
mid Args
args =
MaybeT m (MetaId, InteractionId, Args)
-> m (Maybe (MetaId, InteractionId, Args))
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (MaybeT m (MetaId, InteractionId, Args)
-> m (Maybe (MetaId, InteractionId, Args)))
-> MaybeT m (MetaId, InteractionId, Args)
-> m (Maybe (MetaId, InteractionId, Args))
forall a b. (a -> b) -> a -> b
$ MetaId -> Args -> MaybeT m (MetaId, InteractionId, Args)
forall {m :: * -> *} {c}.
ReadTCState m =>
MetaId -> c -> MaybeT m (MetaId, InteractionId, c)
here MetaId
mid Args
args MaybeT m (MetaId, InteractionId, Args)
-> MaybeT m (MetaId, InteractionId, Args)
-> MaybeT m (MetaId, InteractionId, Args)
forall a. MaybeT m a -> MaybeT m a -> MaybeT m a
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` do
m Term -> MaybeT m Term
forall (m :: * -> *) a. Monad m => m a -> MaybeT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Term -> m Term
instantiateBlockingFull (MetaId -> Elims -> Term
MetaV MetaId
mid (Arg Term -> Elim
forall a. Arg a -> Elim' a
Apply (Arg Term -> Elim) -> Args -> Elims
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Args
args))) MaybeT m Term
-> (Term -> MaybeT m (MetaId, InteractionId, Args))
-> MaybeT m (MetaId, InteractionId, Args)
forall a b. MaybeT m a -> (a -> MaybeT m b) -> MaybeT m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Term -> MaybeT m (MetaId, InteractionId, Args)
there
where
here :: MetaId -> c -> MaybeT m (MetaId, InteractionId, c)
here MetaId
mid c
args = do
iid <- m (Maybe InteractionId) -> MaybeT m InteractionId
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (MetaId -> m (Maybe InteractionId)
forall (m :: * -> *).
ReadTCState m =>
MetaId -> m (Maybe InteractionId)
isInteractionMeta MetaId
mid)
pure (mid, iid, args)
instantiateBlockingFull :: Term -> m Term
instantiateBlockingFull = Lens' TCState Bool -> (Bool -> Bool) -> m Term -> m Term
forall a b. Lens' TCState a -> (a -> a) -> m b -> m b
forall (m :: * -> *) a b.
ReadTCState m =>
Lens' TCState a -> (a -> a) -> m b -> m b
locallyTCState (Bool -> f Bool) -> TCState -> f TCState
Lens' TCState Bool
stInstantiateBlocking (Bool -> Bool -> Bool
forall a b. a -> b -> a
const Bool
True) (m Term -> m Term) -> (Term -> m Term) -> Term -> m Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> m Term
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull
there :: Term -> MaybeT m (MetaId, InteractionId, Args)
there :: Term -> MaybeT m (MetaId, InteractionId, Args)
there (MetaV MetaId
m Elims
args) = do
iid <- m (Maybe InteractionId) -> MaybeT m InteractionId
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (MetaId -> m (Maybe InteractionId)
forall (m :: * -> *).
ReadTCState m =>
MetaId -> m (Maybe InteractionId)
isInteractionMeta MetaId
m)
args <- MaybeT (pure (allApplyElims args))
pure (m, iid, args)
there (Lam ArgInfo
_ Abs Term
as) = Term -> MaybeT m (MetaId, InteractionId, Args)
there (Abs Term -> SubstArg Term -> Term
forall a. Subst a => Abs a -> SubstArg a -> a
absApp Abs Term
as (Nat -> Term
var Nat
0))
there Term
_ = MaybeT m (MetaId, InteractionId, Args)
forall a. MaybeT m a
forall (m :: * -> *) a. MonadPlus m => m a
mzero
assignMeta :: Int -> MetaId -> Type -> [Int] -> Term -> TCM ()
assignMeta :: Nat -> MetaId -> Type -> [Nat] -> Term -> TCM ()
assignMeta Nat
m MetaId
x Type
t [Nat]
ids Term
v = do
let n :: Nat
n = [Nat] -> Nat
forall a. [a] -> Nat
forall (t :: * -> *) a. Foldable t => t a -> Nat
length [Nat]
ids
cand :: [(Nat, Term)]
cand = [(Nat, Term)] -> [(Nat, Term)]
forall a. Ord a => [a] -> [a]
List.sort ([(Nat, Term)] -> [(Nat, Term)]) -> [(Nat, Term)] -> [(Nat, Term)]
forall a b. (a -> b) -> a -> b
$ [Nat] -> [Term] -> [(Nat, Term)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Nat]
ids ([Term] -> [(Nat, Term)]) -> [Term] -> [(Nat, Term)]
forall a b. (a -> b) -> a -> b
$ (Nat -> Term) -> [Nat] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map Nat -> Term
var ([Nat] -> [Term]) -> [Nat] -> [Term]
forall a b. (a -> b) -> a -> b
$ Nat -> [Nat]
forall a. Integral a => a -> [a]
downFrom Nat
n
Nat -> MetaId -> Type -> Nat -> [(Nat, Term)] -> Term -> TCM ()
assignMeta' Nat
m MetaId
x Type
t Nat
n [(Nat, Term)]
cand Term
v
assignMeta' :: Int -> MetaId -> Type -> Int -> SubstCand -> Term -> TCM ()
assignMeta' :: Nat -> MetaId -> Type -> Nat -> [(Nat, Term)] -> Term -> TCM ()
assignMeta' Nat
m MetaId
x Type
t Nat
n [(Nat, Term)]
ids Term
v = do
[Char] -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.assign" Nat
25 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
TCMT IO Doc
"preparing to instantiate: " 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
v
let assocToList :: Nat -> [(Nat, Term)] -> [Maybe Term]
assocToList Nat
i = \case
[(Nat, Term)]
_ | Nat
i Nat -> Nat -> Bool
forall a. Ord a => a -> a -> Bool
>= Nat
m -> []
((Nat
j,Term
u) : [(Nat, Term)]
l) | Nat
i Nat -> Nat -> Bool
forall a. Eq a => a -> a -> Bool
== Nat
j -> Term -> Maybe Term
forall a. a -> Maybe a
Just Term
u Maybe Term -> [Maybe Term] -> [Maybe Term]
forall a. a -> [a] -> [a]
: Nat -> [(Nat, Term)] -> [Maybe Term]
assocToList (Nat
i Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
+ Nat
1) [(Nat, Term)]
l
[(Nat, Term)]
l -> Maybe Term
forall a. Maybe a
Nothing Maybe Term -> [Maybe Term] -> [Maybe Term]
forall a. a -> [a] -> [a]
: Nat -> [(Nat, Term)] -> [Maybe Term]
assocToList (Nat
i Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
+ Nat
1) [(Nat, Term)]
l
ivs :: [Maybe Term]
ivs = Nat -> [(Nat, Term)] -> [Maybe Term]
assocToList Nat
0 [(Nat, Term)]
ids
rho :: Substitution
rho = Impossible -> [Maybe Term] -> Substitution -> Substitution
forall a.
DeBruijn a =>
Impossible -> [Maybe a] -> Substitution' a -> Substitution' a
prependS Impossible
HasCallStack => Impossible
impossible [Maybe Term]
ivs (Substitution -> Substitution) -> Substitution -> Substitution
forall a b. (a -> b) -> a -> b
$ Nat -> Substitution
forall a. Nat -> Substitution' a
raiseS Nat
n
v' :: Term
v' = Substitution' (SubstArg Term) -> Term -> Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution
Substitution' (SubstArg Term)
rho Term
v
TCM () -> TCM ()
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
[Char] -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.assign" Nat
15 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"type of meta =" 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
t
(telv@(TelV tel' a), bs) <- Nat -> Type -> TCMT IO (TelV Type, Boundary)
forall (m :: * -> *).
PureTCM m =>
Nat -> Type -> m (TelV Type, Boundary)
telViewUpToPathBoundary Nat
n Type
t
reportSDoc "tc.meta.assign" 30 $ "tel' =" <+> prettyTCM tel'
reportSDoc "tc.meta.assign" 30 $ "#args =" <+> text (show n)
when (size tel' < n) $ do
a <- abortIfBlocked a
reportSDoc "impossible" 10 $ "not enough pis, but not blocked?" <?> pretty a
__IMPOSSIBLE__
let vsol = Tele (Dom Type) -> Term -> Term
forall t. Abstract t => Tele (Dom Type) -> t -> t
abstract Tele (Dom Type)
tel' Term
v'
whenM (optDoubleCheck <$> pragmaOptions) $ do
m <- lookupLocalMeta x
reportSDoc "tc.meta.check" 30 $ "double checking solution"
catchConstraint (CheckMetaInst x) $
addContext tel' $ checkSolutionForMeta x m v' a
reportSDoc "tc.meta.assign" 10 $
"solving" <+> prettyTCM x <+> ":=" <+> prettyTCM vsol
v' <- blockOnBoundary telv bs v'
assignTerm x (telToArgs tel') v'
where
blockOnBoundary :: TelView -> Boundary -> Term -> TCM Term
blockOnBoundary :: TelV Type -> Boundary -> Term -> TCM Term
blockOnBoundary TelV Type
telv [] Term
v = Term -> TCM Term
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Term
v
blockOnBoundary (TelV Tele (Dom Type)
tel Type
t) Boundary
bs Term
v = Tele (Dom Type) -> TCM Term -> TCM Term
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Tele (Dom Type) -> m a -> m a
addContext Tele (Dom Type)
tel (TCM Term -> TCM Term) -> TCM Term -> TCM Term
forall a b. (a -> b) -> a -> b
$
Type -> TCM Term -> TCM Term
forall (m :: * -> *).
(MonadMetaSolver m, MonadConstraint m, MonadFresh Nat m,
MonadFresh ProblemId m) =>
Type -> m Term -> m Term
blockTerm Type
t (TCM Term -> TCM Term) -> TCM Term -> TCM Term
forall a b. (a -> b) -> a -> b
$ do
neg <- TCM Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primINeg
forM_ bs $ \ (Term
r,(Term
x,Term
y)) -> do
Term -> Type -> Term -> Term -> TCM ()
forall (m :: * -> *).
MonadConversion m =>
Term -> Type -> Term -> Term -> m ()
equalTermOnFace (Term
neg Term -> Term -> Term
forall t. Apply t => t -> Term -> t
`apply1` Term
r) Type
t Term
x Term
v
Term -> Type -> Term -> Term -> TCM ()
forall (m :: * -> *).
MonadConversion m =>
Term -> Type -> Term -> Term -> m ()
equalTermOnFace Term
r Type
t Term
y Term
v
return v
checkMetaInst :: MetaId -> TCM ()
checkMetaInst :: MetaId -> TCM ()
checkMetaInst MetaId
x = do
m <- MetaId -> TCMT IO MetaVariable
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta MetaId
x
let postpone = Blocker -> Constraint -> TCM ()
forall (m :: * -> *).
MonadConstraint m =>
Blocker -> Constraint -> m ()
addConstraint (MetaId -> Blocker
unblockOnMeta MetaId
x) (Constraint -> TCM ()) -> Constraint -> TCM ()
forall a b. (a -> b) -> a -> b
$ MetaId -> Constraint
CheckMetaInst MetaId
x
case mvInstantiation m of
BlockedConst{} -> TCM ()
postpone
PostponedTypeCheckingProblem{} -> TCM ()
postpone
OpenMeta{} -> TCM ()
postpone
InstV Instantiation
inst -> do
let n :: Nat
n = [Arg [Char]] -> Nat
forall a. Sized a => a -> Nat
size (Instantiation -> [Arg [Char]]
instTel Instantiation
inst)
t :: Type
t = 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
m
(telv@(TelV tel a),bs) <- Nat -> Type -> TCMT IO (TelV Type, Boundary)
forall (m :: * -> *).
PureTCM m =>
Nat -> Type -> m (TelV Type, Boundary)
telViewUpToPathBoundary Nat
n Type
t
catchConstraint (CheckMetaInst x) $ addContext tel $
checkSolutionForMeta x m (instBody inst) a
checkSolutionForMeta :: MetaId -> MetaVariable -> Term -> Type -> TCM ()
checkSolutionForMeta :: MetaId -> MetaVariable -> Term -> Type -> TCM ()
checkSolutionForMeta MetaId
x MetaVariable
m Term
v Type
a = do
[Char] -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.check" Nat
30 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"checking solution for 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 a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => MetaId -> m Doc
prettyTCM MetaId
x
case MetaVariable -> Judgement MetaId
mvJudgement MetaVariable
m of
HasType{ jComparison :: forall a. Judgement a -> Comparison
jComparison = Comparison
cmp } -> do
[Char] -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.check" Nat
30 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ 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
$
MetaId -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => MetaId -> m Doc
prettyTCM MetaId
x 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
<+> 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 -> 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
v
[Char] -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.check" Nat
50 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ 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
$ do
ctx <- TCMT IO Context
forall (m :: * -> *). MonadTCEnv m => m Context
getContext
inTopContext $ "in context: " <+> prettyTCM (PrettyContext ctx)
Call -> TCM () -> TCM ()
forall a. Call -> TCMT IO a -> TCMT IO a
forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
traceCall (Range -> MetaId -> Type -> Term -> Call
CheckMetaSolution (MetaVariable -> Range
forall a. HasRange a => a -> Range
getRange MetaVariable
m) MetaId
x Type
a Term
v) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
Term -> Comparison -> TypeOf Term -> TCM ()
forall a (m :: * -> *).
(CheckInternal a, MonadCheckInternal m) =>
a -> Comparison -> TypeOf a -> m ()
forall (m :: * -> *).
MonadCheckInternal m =>
Term -> Comparison -> TypeOf Term -> m ()
checkInternal Term
v Comparison
cmp TypeOf Term
Type
a
IsSort{} -> TCM () -> TCM ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
[Char] -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.check" Nat
30 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ 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
$
MetaId -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => MetaId -> m Doc
prettyTCM MetaId
x 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
v TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
" is a sort"
s <- Type -> TCM Sort
forall (m :: * -> *).
(PureTCM m, MonadBlock m, MonadError TCErr m) =>
Type -> m Sort
shouldBeSort (Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El Sort
HasCallStack => Sort
__DUMMY_SORT__ Term
v)
traceCall (CheckMetaSolution (getRange m) x (sort (univSort s)) (Sort s)) $
inferInternal s
checkSubtypeIsEqual :: Type -> Type -> TCM ()
checkSubtypeIsEqual :: Type -> Type -> TCM ()
checkSubtypeIsEqual Type
a Type
b = do
[Char] -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.subtype" Nat
30 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
TCMT IO Doc
"checking that subtype" 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 -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
TCMT IO Doc
"of" 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
b TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"is actually equal."
Type
-> Type
-> (Type -> Type -> TCM ())
-> (Type -> Type -> TCM ())
-> TCM ()
forall a (m :: * -> *) b.
(Instantiate a, SynEq a, MonadReduce m) =>
a -> a -> (a -> a -> m b) -> (a -> a -> m b) -> m b
SynEq.checkSyntacticEquality Type
a Type
b (\Type
_ Type
_ -> () -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()) ((Type -> Type -> TCM ()) -> TCM ())
-> (Type -> Type -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \Type
a Type
b -> do
cumulativity <- PragmaOptions -> Bool
optCumulativity (PragmaOptions -> Bool) -> TCMT IO PragmaOptions -> TCM Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
abortIfBlocked (unEl b) >>= \case
Sort Sort
sb -> Term -> TCM Term
forall (m :: * -> *) t.
(MonadReduce m, MonadBlock m, IsMeta t, Reduce t) =>
t -> m t
abortIfBlocked (Type -> Term
forall t a. Type'' t a -> a
unEl Type
a) TCM Term -> (Term -> TCM ()) -> TCM ()
forall a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Sort Sort
sa | Bool
cumulativity -> Sort -> Sort -> TCM ()
forall (m :: * -> *). MonadConversion m => Sort -> Sort -> m ()
equalSort Sort
sa Sort
sb
| Bool
otherwise -> () -> 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 ()
Term
a -> Blocker -> TCM ()
forall a. Blocker -> TCMT IO a
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation (Blocker -> TCM ()) -> TCM Blocker -> TCM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Blocker -> TCM Blocker
forall (m :: * -> *). PureTCM m => Blocker -> m Blocker
updateBlocker (Term -> Blocker
forall t. AllMetas t => t -> Blocker
unblockOnAnyMetaIn Term
a)
Pi Dom Type
b1 Abs Type
b2 -> Term -> TCM Term
forall (m :: * -> *) t.
(MonadReduce m, MonadBlock m, IsMeta t, Reduce t) =>
t -> m t
abortIfBlocked (Type -> Term
forall t a. Type'' t a -> a
unEl Type
a) TCM Term -> (Term -> TCM ()) -> TCM ()
forall a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Pi Dom Type
a1 Abs Type
a2
| Dom Type -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance Dom Type
a1 Relevance -> Relevance -> Bool
forall a. Eq a => a -> a -> Bool
/= Dom Type -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance Dom Type
b1 -> Blocker -> TCM ()
forall a. Blocker -> TCMT IO a
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
neverUnblock
| Dom Type -> Quantity
forall a. LensQuantity a => a -> Quantity
getQuantity Dom Type
a1 Quantity -> Quantity -> Bool
forall a. Eq a => a -> a -> Bool
/= Dom Type -> Quantity
forall a. LensQuantity a => a -> Quantity
getQuantity Dom Type
b1 -> Blocker -> TCM ()
forall a. Blocker -> TCMT IO a
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
neverUnblock
| Dom Type -> Cohesion
forall a. LensCohesion a => a -> Cohesion
getCohesion Dom Type
a1 Cohesion -> Cohesion -> Bool
forall a. Eq a => a -> a -> Bool
/= Dom Type -> Cohesion
forall a. LensCohesion a => a -> Cohesion
getCohesion Dom Type
b1 -> Blocker -> TCM ()
forall a. Blocker -> TCMT IO a
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
neverUnblock
| Bool
otherwise -> do
Type -> Type -> TCM ()
checkSubtypeIsEqual (Dom Type -> Type
forall t e. Dom' t e -> e
unDom Dom Type
b1) (Dom Type -> Type
forall t e. Dom' t e -> e
unDom Dom Type
a1)
Dom Type -> Abs Type -> (Type -> TCM ()) -> TCM ()
forall a (m :: * -> *) b.
(Subst a, MonadAddContext m) =>
Dom Type -> Abs a -> (a -> m b) -> m b
underAbstractionAbs Dom Type
a1 Abs Type
a2 ((Type -> TCM ()) -> TCM ()) -> (Type -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \Type
a2' -> Type -> Type -> TCM ()
checkSubtypeIsEqual Type
a2' (Abs Type -> Type
forall a. Subst a => Abs a -> a
absBody Abs Type
b2)
Dummy{} -> () -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
Term
a -> Blocker -> TCM ()
forall a. Blocker -> TCMT IO a
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation (Blocker -> TCM ()) -> TCM Blocker -> TCM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Blocker -> TCM Blocker
forall (m :: * -> *). PureTCM m => Blocker -> m Blocker
updateBlocker (Term -> Blocker
forall t. AllMetas t => t -> Blocker
unblockOnAnyMetaIn Term
a)
Term
_ -> () -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
subtypingForSizeLt
:: CompareDirection
-> MetaId
-> MetaVariable
-> Type
-> Args
-> Term
-> (Term -> TCM ())
-> TCM ()
subtypingForSizeLt :: CompareDirection
-> MetaId
-> MetaVariable
-> Type
-> Args
-> Term
-> (Term -> TCM ())
-> TCM ()
subtypingForSizeLt CompareDirection
DirEq MetaId
x MetaVariable
mvar Type
t Args
args Term
v Term -> TCM ()
cont = Term -> TCM ()
cont Term
v
subtypingForSizeLt CompareDirection
dir MetaId
x MetaVariable
mvar Type
t Args
args Term
v Term -> TCM ()
cont = do
let fallback :: TCM ()
fallback = Term -> TCM ()
cont Term
v
(mSize, mSizeLt) <- TCMT IO (Maybe QName, Maybe QName)
forall (m :: * -> *). HasBuiltins m => m (Maybe QName, Maybe QName)
getBuiltinSize
caseMaybe mSize fallback $ \ QName
qSize -> do
Maybe QName -> TCM () -> (QName -> TCM ()) -> TCM ()
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe QName
mSizeLt TCM ()
fallback ((QName -> TCM ()) -> TCM ()) -> (QName -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ QName
qSizeLt -> do
v <- Term -> TCM Term
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Term
v
case v of
Def QName
q [Apply (Arg ArgInfo
ai Term
u)] | QName
q QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
qSizeLt -> do
TelV tel _ <- Type -> TCMT IO (TelV Type)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView Type
t
let size = QName -> Type
sizeType_ QName
qSize
t' = Tele (Dom Type) -> Type -> Type
telePi Tele (Dom Type)
tel Type
size
y <- newMeta Instantiable (mvInfo mvar) (mvPriority mvar) (mvPermutation mvar)
(HasType __IMPOSSIBLE__ CmpLeq t')
let yArgs = MetaId -> Elims -> Term
MetaV MetaId
y (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ (Arg Term -> Elim) -> Args -> Elims
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim
forall a. Arg a -> Elim' a
Apply Args
args
addConstraint (unblockOnMeta y) $ dirToCmp (`ValueCmp` AsSizes) dir yArgs u
let xArgs = MetaId -> Elims -> Term
MetaV MetaId
x (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ (Arg Term -> Elim) -> Args -> Elims
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim
forall a. Arg a -> Elim' a
Apply Args
args
v' = QName -> Elims -> Term
Def QName
qSizeLt [Arg Term -> Elim
forall a. Arg a -> Elim' a
Apply (Arg Term -> Elim) -> Arg Term -> Elim
forall a b. (a -> b) -> a -> b
$ ArgInfo -> Term -> Arg Term
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai Term
yArgs]
c = (Comparison -> Term -> Term -> Constraint)
-> CompareDirection -> Term -> Term -> Constraint
forall a c.
(Comparison -> a -> a -> c) -> CompareDirection -> a -> a -> c
dirToCmp (Comparison -> CompareAs -> Term -> Term -> Constraint
`ValueCmp` (Type -> CompareAs
AsTermsOf Type
sizeUniv)) CompareDirection
dir Term
xArgs Term
v'
catchConstraint c $ cont v'
Term
_ -> TCM ()
fallback
expandProjectedVars
:: ( Pretty a, PrettyTCM a, NoProjectedVar a
, ReduceAndEtaContract a
, PrettyTCM b, TermSubst b
)
=> a
-> b
-> (a -> b -> TCM c)
-> TCM c
expandProjectedVars :: forall a b c.
(Pretty a, PrettyTCM a, NoProjectedVar a, ReduceAndEtaContract a,
PrettyTCM b, TermSubst b) =>
a -> b -> (a -> b -> TCM c) -> TCM c
expandProjectedVars a
args b
v a -> b -> TCM c
ret = (a, b) -> TCM c
loop (a
args, b
v) where
loop :: (a, b) -> TCM c
loop (a
args, b
v) = do
[Char] -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.assign.proj" Nat
45 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"meta args: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> a -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => a -> m Doc
prettyTCM a
args
args <- TCM a -> TCM a
forall a. TCM a -> TCM a
callByName (TCM a -> TCM a) -> TCM a -> TCM a
forall a b. (a -> b) -> a -> b
$ a -> TCM a
forall a. ReduceAndEtaContract a => a -> TCM a
reduceAndEtaContract a
args
reportSDoc "tc.meta.assign.proj" 45 $ "norm args: " <+> prettyTCM args
reportSDoc "tc.meta.assign.proj" 85 $ "norm args: " <+> pretty args
let done = a -> b -> TCM c
ret a
args b
v
case noProjectedVar args of
Right () -> do
[Char] -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.assign.proj" Nat
40 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
TCMT IO Doc
"no projected var found in args: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> a -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => a -> m Doc
prettyTCM a
args
TCM c
done
Left (ProjectedVar Nat
i [(ProjOrigin, QName)]
_) -> Nat -> (a, b) -> TCM c -> ((a, b) -> TCM c) -> TCM c
forall a c.
(PrettyTCM a, TermSubst a) =>
Nat -> a -> TCM c -> (a -> TCM c) -> TCM c
etaExpandProjectedVar Nat
i (a
args, b
v) TCM c
done (a, b) -> TCM c
loop
etaExpandProjectedVar :: (PrettyTCM a, TermSubst a) => Int -> a -> TCM c -> (a -> TCM c) -> TCM c
etaExpandProjectedVar :: forall a c.
(PrettyTCM a, TermSubst a) =>
Nat -> a -> TCM c -> (a -> TCM c) -> TCM c
etaExpandProjectedVar Nat
i a
v TCM c
fail a -> TCM c
succeed = do
[Char] -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.assign.proj" Nat
40 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
TCMT IO Doc
"trying to expand projected variable" 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 (Nat -> Term
var Nat
i)
TCMT IO (Maybe (Tele (Dom Type), Substitution, Substitution))
-> TCM c
-> ((Tele (Dom Type), Substitution, Substitution) -> TCM c)
-> TCM c
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (Nat
-> TCMT IO (Maybe (Tele (Dom Type), Substitution, Substitution))
etaExpandBoundVar Nat
i) TCM c
fail (((Tele (Dom Type), Substitution, Substitution) -> TCM c) -> TCM c)
-> ((Tele (Dom Type), Substitution, Substitution) -> TCM c)
-> TCM c
forall a b. (a -> b) -> a -> b
$ \ (Tele (Dom Type)
delta, Substitution
sigma, Substitution
tau) -> do
[Char] -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.assign.proj" Nat
25 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
TCMT IO Doc
"eta-expanding var " 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 (Nat -> Term
var Nat
i) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
TCMT IO Doc
" in terms " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> a -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => a -> m Doc
prettyTCM a
v
TCM c -> TCM c
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
unsafeInTopContext (TCM c -> TCM c) -> TCM c -> TCM c
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> TCM c -> TCM c
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Tele (Dom Type) -> m a -> m a
addContext Tele (Dom Type)
delta (TCM c -> TCM c) -> TCM c -> TCM c
forall a b. (a -> b) -> a -> b
$
a -> TCM c
succeed (a -> TCM c) -> a -> TCM c
forall a b. (a -> b) -> a -> b
$ Substitution' (SubstArg a) -> a -> a
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution
Substitution' (SubstArg a)
tau a
v
class NoProjectedVar a where
noProjectedVar :: a -> Either ProjectedVar ()
default noProjectedVar
:: (NoProjectedVar b, Foldable t, t b ~ a)
=> a -> Either ProjectedVar ()
noProjectedVar = (b -> Either ProjectedVar ()) -> t b -> Either ProjectedVar ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
Fold.mapM_ b -> Either ProjectedVar ()
forall a. NoProjectedVar a => a -> Either ProjectedVar ()
noProjectedVar
instance NoProjectedVar a => NoProjectedVar (Arg a)
instance NoProjectedVar a => NoProjectedVar [a]
instance NoProjectedVar Term where
noProjectedVar :: Term -> Either ProjectedVar ()
noProjectedVar = \case
Var Nat
i Elims
es
| qs :: [(ProjOrigin, QName)]
qs@((ProjOrigin, QName)
_:[(ProjOrigin, QName)]
_) <- (Maybe (ProjOrigin, QName) -> Maybe (ProjOrigin, QName))
-> [Maybe (ProjOrigin, QName)] -> [(ProjOrigin, QName)]
forall a b. (a -> Maybe b) -> [a] -> Prefix b
takeWhileJust Maybe (ProjOrigin, QName) -> Maybe (ProjOrigin, QName)
forall a. a -> a
id ([Maybe (ProjOrigin, QName)] -> [(ProjOrigin, QName)])
-> [Maybe (ProjOrigin, QName)] -> [(ProjOrigin, QName)]
forall a b. (a -> b) -> a -> b
$ (Elim -> Maybe (ProjOrigin, QName))
-> Elims -> [Maybe (ProjOrigin, QName)]
forall a b. (a -> b) -> [a] -> [b]
map Elim -> Maybe (ProjOrigin, QName)
forall e. IsProjElim e => e -> Maybe (ProjOrigin, QName)
isProjElim Elims
es
-> ProjectedVar -> Either ProjectedVar ()
forall a b. a -> Either a b
Left (ProjectedVar -> Either ProjectedVar ())
-> ProjectedVar -> Either ProjectedVar ()
forall a b. (a -> b) -> a -> b
$ Nat -> [(ProjOrigin, QName)] -> ProjectedVar
ProjectedVar Nat
i [(ProjOrigin, QName)]
qs
Con (ConHead QName
_ IsRecord{} Induction
Inductive [Arg QName]
_) ConInfo
_ Elims
es
| Just Args
vs <- Elims -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
-> Args -> Either ProjectedVar ()
forall a. NoProjectedVar a => a -> Either ProjectedVar ()
noProjectedVar Args
vs
Term
_ -> () -> Either ProjectedVar ()
forall a. a -> Either ProjectedVar a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
class (TermLike a, TermSubst a, Reduce a) => ReduceAndEtaContract a where
reduceAndEtaContract :: a -> TCM a
default reduceAndEtaContract
:: (Traversable f, TermLike b, Subst b, Reduce b, ReduceAndEtaContract b, f b ~ a)
=> a -> TCM a
reduceAndEtaContract = (b -> TCMT IO b) -> f b -> TCMT IO (f b)
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) -> f a -> m (f b)
Trav.mapM b -> TCMT IO b
forall a. ReduceAndEtaContract a => a -> TCM a
reduceAndEtaContract
instance ReduceAndEtaContract a => ReduceAndEtaContract [a]
instance ReduceAndEtaContract a => ReduceAndEtaContract (Arg a)
instance ReduceAndEtaContract Term where
reduceAndEtaContract :: Term -> TCM Term
reduceAndEtaContract Term
u = do
Term -> TCM Term
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Term
u TCM Term -> (Term -> TCM Term) -> TCM Term
forall a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Lam ArgInfo
ai (Abs [Char]
x Term
b) -> ArgInfo -> [Char] -> Term -> TCM Term
forall (m :: * -> *).
(MonadTCEnv m, HasConstInfo m, HasOptions m) =>
ArgInfo -> [Char] -> Term -> m Term
etaLam ArgInfo
ai [Char]
x (Term -> TCM Term) -> TCM Term -> TCM Term
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Term -> TCM Term
forall a. ReduceAndEtaContract a => a -> TCM a
reduceAndEtaContract Term
b
Con ConHead
c ConInfo
ci Elims
es -> ConHead
-> ConInfo
-> Elims
-> (QName -> ConHead -> ConInfo -> Args -> TCM Term)
-> TCM Term
forall (m :: * -> *).
(MonadTCEnv m, HasConstInfo m, HasOptions m) =>
ConHead
-> ConInfo
-> Elims
-> (QName -> ConHead -> ConInfo -> Args -> m Term)
-> m Term
etaCon ConHead
c ConInfo
ci Elims
es ((QName -> ConHead -> ConInfo -> Args -> TCM Term) -> TCM Term)
-> (QName -> ConHead -> ConInfo -> Args -> TCM Term) -> TCM Term
forall a b. (a -> b) -> a -> b
$ \ QName
r ConHead
c ConInfo
ci Args
args -> do
args <- Args -> TCM Args
forall a. ReduceAndEtaContract a => a -> TCM a
reduceAndEtaContract Args
args
etaContractRecord r c ci args
Term
v -> Term -> TCM Term
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Term
v
type FVs = VarSet
type SubstCand = [(Int,Term)]
checkLinearity :: SubstCand -> ExceptT () TCM SubstCand
checkLinearity :: [(Nat, Term)] -> ExceptT () (TCMT IO) [(Nat, Term)]
checkLinearity [(Nat, Term)]
ids = do
[(Nat, Term)] -> [(Nat, Term)]
[(Nat, Term)] -> [Item [(Nat, Term)]]
forall l. IsList l => l -> [Item l]
List1.toList ([(Nat, Term)] -> [(Nat, Term)])
-> ExceptT () (TCMT IO) [(Nat, Term)]
-> ExceptT () (TCMT IO) [(Nat, Term)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (List1 (Nat, Term) -> ExceptT () (TCMT IO) (Nat, Term))
-> [List1 (Nat, Term)] -> ExceptT () (TCMT IO) [(Nat, Term)]
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 List1 (Nat, Term) -> ExceptT () (TCMT IO) (Nat, Term)
makeLinear (((Nat, Term) -> Nat) -> [(Nat, Term)] -> [List1 (Nat, Term)]
forall b a. Ord b => (a -> b) -> [a] -> [List1 a]
List1.groupOn (Nat, Term) -> Nat
forall a b. (a, b) -> a
fst [(Nat, Term)]
ids)
where
makeLinear :: List1 (Int, Term) -> ExceptT () TCM (Int, Term)
makeLinear :: List1 (Nat, Term) -> ExceptT () (TCMT IO) (Nat, Term)
makeLinear ((Nat, Term)
p :| []) = (Nat, Term) -> ExceptT () (TCMT IO) (Nat, Term)
forall a. a -> ExceptT () (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Nat, Term)
p
makeLinear (p :: (Nat, Term)
p@(Nat
i,Term
t) :| [(Nat, Term)]
_ ) =
ExceptT () (TCMT IO) Bool
-> ExceptT () (TCMT IO) (Nat, Term)
-> ExceptT () (TCMT IO) (Nat, Term)
-> ExceptT () (TCMT IO) (Nat, Term)
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM ((Bool -> Either Blocker Bool
forall a b. b -> Either a b
Right Bool
True Either Blocker Bool -> Either Blocker Bool -> Bool
forall a. Eq a => a -> a -> Bool
==) (Either Blocker Bool -> Bool)
-> ExceptT () (TCMT IO) (Either Blocker Bool)
-> ExceptT () (TCMT IO) Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do TCM (Either Blocker Bool)
-> ExceptT () (TCMT IO) (Either Blocker 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 (TCM (Either Blocker Bool)
-> ExceptT () (TCMT IO) (Either Blocker Bool))
-> (Type -> TCM (Either Blocker Bool))
-> Type
-> ExceptT () (TCMT IO) (Either Blocker Bool)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BlockT (TCMT IO) Bool -> TCM (Either Blocker Bool)
forall (m :: * -> *) a.
Monad m =>
BlockT m a -> m (Either Blocker a)
runBlocked (BlockT (TCMT IO) Bool -> TCM (Either Blocker Bool))
-> (Type -> BlockT (TCMT IO) Bool)
-> Type
-> TCM (Either Blocker Bool)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> BlockT (TCMT IO) Bool
forall (m :: * -> *). (PureTCM m, MonadBlock m) => Type -> m Bool
isSingletonTypeModuloRelevance (Type -> ExceptT () (TCMT IO) (Either Blocker Bool))
-> ExceptT () (TCMT IO) Type
-> ExceptT () (TCMT IO) (Either Blocker Bool)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Nat -> ExceptT () (TCMT IO) Type
forall (m :: * -> *).
(Applicative m, MonadFail m, MonadTCEnv m) =>
Nat -> m Type
typeOfBV Nat
i)
((Nat, Term) -> ExceptT () (TCMT IO) (Nat, Term)
forall a. a -> ExceptT () (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Nat, Term)
p)
(() -> ExceptT () (TCMT IO) (Nat, Term)
forall a. () -> ExceptT () (TCMT IO) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError ())
type Res = [(Arg Nat, Term)]
data InvertExcept
= CantInvert Term
| NeutralArg
| ProjVar ProjectedVar
inverseSubst' :: (Term -> Bool) -> Args -> ExceptT InvertExcept TCM SubstCand
inverseSubst' :: (Term -> Bool)
-> Args -> ExceptT InvertExcept (TCMT IO) [(Nat, Term)]
inverseSubst' Term -> Bool
skip Args
args = ((Arg Nat, Term) -> (Nat, Term))
-> [(Arg Nat, Term)] -> [(Nat, Term)]
forall a b. (a -> b) -> [a] -> [b]
map ((Arg Nat -> Nat) -> (Arg Nat, Term) -> (Nat, Term)
forall a c b. (a -> c) -> (a, b) -> (c, b)
mapFst Arg Nat -> Nat
forall e. Arg e -> e
unArg) ([(Arg Nat, Term)] -> [(Nat, Term)])
-> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)]
-> ExceptT InvertExcept (TCMT IO) [(Nat, Term)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Arg Term, Term)]
-> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)]
loop (Args -> [Term] -> [(Arg Term, Term)]
forall a b. [a] -> [b] -> [(a, b)]
zip Args
args [Term]
terms)
where
loop :: [(Arg Term, Term)]
-> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)]
loop = ([(Arg Nat, Term)]
-> (Arg Term, Term)
-> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)])
-> [(Arg Nat, Term)]
-> [(Arg Term, Term)]
-> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)]
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM [(Arg Nat, Term)]
-> (Arg Term, Term)
-> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)]
isVarOrIrrelevant []
terms :: [Term]
terms = (Nat -> Term) -> [Nat] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map Nat -> Term
var (Nat -> [Nat]
forall a. Integral a => a -> [a]
downFrom (Args -> Nat
forall a. Sized a => a -> Nat
size Args
args))
failure :: Term -> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)]
failure Term
c = do
TCM () -> ExceptT InvertExcept (TCMT IO) ()
forall (m :: * -> *) a. Monad m => m a -> ExceptT InvertExcept m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM () -> ExceptT InvertExcept (TCMT IO) ())
-> TCM () -> ExceptT InvertExcept (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ [Char] -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.assign" Nat
15 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
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
"not all arguments are variables: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Args -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Args -> m Doc
prettyTCM Args
args
, TCMT IO Doc
" aborting assignment" ]
InvertExcept -> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)]
forall a. InvertExcept -> ExceptT InvertExcept (TCMT IO) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Term -> InvertExcept
CantInvert Term
c)
neutralArg :: ExceptT InvertExcept (TCMT IO) a
neutralArg = InvertExcept -> ExceptT InvertExcept (TCMT IO) a
forall a. InvertExcept -> ExceptT InvertExcept (TCMT IO) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError InvertExcept
NeutralArg
isVarOrIrrelevant :: Res -> (Arg Term, Term) -> ExceptT InvertExcept TCM Res
isVarOrIrrelevant :: [(Arg Nat, Term)]
-> (Arg Term, Term)
-> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)]
isVarOrIrrelevant [(Arg Nat, Term)]
vars (Arg ArgInfo
info Term
v, Term
t) = do
let irr :: Bool
irr | ArgInfo -> Bool
forall a. LensRelevance a => a -> Bool
isIrrelevant ArgInfo
info = Bool
True
| DontCare{} <- Term
v = Bool
True
| Bool
otherwise = Bool
False
ineg <- PrimitiveId -> ExceptT InvertExcept (TCMT IO) (Maybe QName)
forall (m :: * -> *).
HasBuiltins m =>
PrimitiveId -> m (Maybe QName)
getPrimitiveName' PrimitiveId
builtinINeg
case stripDontCare v of
Var Nat
i [] -> [(Arg Nat, Term)]
-> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)]
forall a. a -> ExceptT InvertExcept (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Arg Nat, Term)]
-> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)])
-> [(Arg Nat, Term)]
-> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)]
forall a b. (a -> b) -> a -> b
$ (ArgInfo -> Nat -> Arg Nat
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
info Nat
i, Term
t) (Arg Nat, Term) -> [(Arg Nat, Term)] -> [(Arg Nat, Term)]
`cons` [(Arg Nat, Term)]
vars
Var Nat
i Elims
es | Just [(ProjOrigin, QName)]
qs <- (Elim -> Maybe (ProjOrigin, QName))
-> Elims -> Maybe [(ProjOrigin, QName)]
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 Elim -> Maybe (ProjOrigin, QName)
forall e. IsProjElim e => e -> Maybe (ProjOrigin, QName)
isProjElim Elims
es ->
InvertExcept -> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)]
forall a. InvertExcept -> ExceptT InvertExcept (TCMT IO) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (InvertExcept -> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)])
-> InvertExcept -> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)]
forall a b. (a -> b) -> a -> b
$ ProjectedVar -> InvertExcept
ProjVar (ProjectedVar -> InvertExcept) -> ProjectedVar -> InvertExcept
forall a b. (a -> b) -> a -> b
$ Nat -> [(ProjOrigin, QName)] -> ProjectedVar
ProjectedVar Nat
i [(ProjOrigin, QName)]
qs
tm :: Term
tm@(Con ConHead
c ConInfo
ci Elims
es) -> do
let fallback :: ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)]
fallback
| ArgInfo -> Bool
forall a. LensRelevance a => a -> Bool
isIrrelevant ArgInfo
info = [(Arg Nat, Term)]
-> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)]
forall a. a -> ExceptT InvertExcept (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return [(Arg Nat, Term)]
vars
| Term -> Bool
skip Term
tm = [(Arg Nat, Term)]
-> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)]
forall a. a -> ExceptT InvertExcept (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return [(Arg Nat, Term)]
vars
| Bool
otherwise = Term -> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)]
failure Term
tm
irrProj <- PragmaOptions -> Bool
optIrrelevantProjections (PragmaOptions -> Bool)
-> ExceptT InvertExcept (TCMT IO) PragmaOptions
-> ExceptT InvertExcept (TCMT IO) Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExceptT InvertExcept (TCMT IO) PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
lift (isEtaRecordConstructor $ conName c) >>= \case
Just (QName
_, RecordData{ _recFields :: RecordData -> [Dom QName]
_recFields = [Dom QName]
fs })
| [Dom QName] -> Nat
forall a. [a] -> Nat
forall (t :: * -> *) a. Foldable t => t a -> Nat
length [Dom QName]
fs Nat -> Nat -> Bool
forall a. Eq a => a -> a -> Bool
== Elims -> Nat
forall a. [a] -> Nat
forall (t :: * -> *) a. Foldable t => t a -> Nat
length Elims
es
, ArgInfo -> Bool
forall a. LensQuantity a => a -> Bool
hasQuantity0 ArgInfo
info Bool -> Bool -> Bool
|| (Dom QName -> Bool) -> [Dom QName] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Dom QName -> Bool
forall a. LensQuantity a => a -> Bool
usableQuantity [Dom QName]
fs
, Bool
irrProj Bool -> Bool -> Bool
|| (Dom QName -> Bool) -> [Dom QName] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Dom QName -> Bool
forall a. LensRelevance a => a -> Bool
isRelevant [Dom QName]
fs -> do
let aux :: Arg Term -> Dom QName -> (Arg Term, Term)
aux (Arg ArgInfo
_ Term
v) Dom{domInfo :: forall t e. Dom' t e -> ArgInfo
domInfo = ArgInfo
info', unDom :: forall t e. Dom' t e -> e
unDom = QName
f} =
(ArgInfo -> Term -> Arg Term
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai Term
v,) (Term -> (Arg Term, Term)) -> Term -> (Arg Term, Term)
forall a b. (a -> b) -> a -> b
$ Term
t Term -> Elims -> Term
forall t. Apply t => t -> Elims -> t
`applyE` [ProjOrigin -> QName -> Elim
forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
ProjSystem QName
f]
where
ai :: ArgInfo
ai = ArgInfo
{ argInfoHiding :: Hiding
argInfoHiding = Hiding -> Hiding -> Hiding
forall a. Ord a => a -> a -> a
min (ArgInfo -> Hiding
forall a. LensHiding a => a -> Hiding
getHiding ArgInfo
info) (ArgInfo -> Hiding
forall a. LensHiding a => a -> Hiding
getHiding ArgInfo
info')
, argInfoModality :: Modality
argInfoModality = Modality
{ modRelevance :: Relevance
modRelevance = Relevance -> Relevance -> Relevance
forall a. Ord a => a -> a -> a
max (ArgInfo -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance ArgInfo
info) (ArgInfo -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance ArgInfo
info')
, modQuantity :: Quantity
modQuantity = Quantity -> Quantity -> Quantity
forall a. Ord a => a -> a -> a
max (ArgInfo -> Quantity
forall a. LensQuantity a => a -> Quantity
getQuantity ArgInfo
info) (ArgInfo -> Quantity
forall a. LensQuantity a => a -> Quantity
getQuantity ArgInfo
info')
, modCohesion :: Cohesion
modCohesion = Cohesion -> Cohesion -> Cohesion
forall a. Ord a => a -> a -> a
max (ArgInfo -> Cohesion
forall a. LensCohesion a => a -> Cohesion
getCohesion ArgInfo
info) (ArgInfo -> Cohesion
forall a. LensCohesion a => a -> Cohesion
getCohesion ArgInfo
info')
}
, argInfoOrigin :: Origin
argInfoOrigin = Origin -> Origin -> Origin
forall a. Ord a => a -> a -> a
min (ArgInfo -> Origin
forall a. LensOrigin a => a -> Origin
getOrigin ArgInfo
info) (ArgInfo -> Origin
forall a. LensOrigin a => a -> Origin
getOrigin ArgInfo
info')
, argInfoFreeVariables :: FreeVariables
argInfoFreeVariables = FreeVariables
unknownFreeVariables
, argInfoAnnotation :: Annotation
argInfoAnnotation = ArgInfo -> Annotation
argInfoAnnotation ArgInfo
info'
}
vs :: Args
vs = Args -> Maybe Args -> Args
forall a. a -> Maybe a -> a
fromMaybe Args
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
forall a b. (a -> b) -> a -> b
$ Elims -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
res <- [(Arg Term, Term)]
-> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)]
loop ([(Arg Term, Term)]
-> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)])
-> [(Arg Term, Term)]
-> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)]
forall a b. (a -> b) -> a -> b
$ (Arg Term -> Dom QName -> (Arg Term, Term))
-> Args -> [Dom QName] -> [(Arg Term, Term)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Arg Term -> Dom QName -> (Arg Term, Term)
aux Args
vs [Dom QName]
fs
return $ res `append` vars
| Bool
otherwise -> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)]
fallback
Maybe (QName, RecordData)
_ -> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)]
fallback
Term
_ | Bool
irr -> [(Arg Nat, Term)]
-> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)]
forall a. a -> ExceptT InvertExcept (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return [(Arg Nat, Term)]
vars
Var{} -> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)]
forall {a}. ExceptT InvertExcept (TCMT IO) a
neutralArg
Def QName
qn Elims
es | Just [Arg ArgInfo
_ (Var Nat
i [])] <- Elims -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es, QName -> Maybe QName
forall a. a -> Maybe a
Just QName
qn Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe QName
ineg ->
[(Arg Nat, Term)]
-> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)]
forall a. a -> ExceptT InvertExcept (TCMT IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([(Arg Nat, Term)]
-> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)])
-> [(Arg Nat, Term)]
-> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)]
forall a b. (a -> b) -> a -> b
$ (ArgInfo -> Nat -> Arg Nat
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
info Nat
i, QName -> Elims -> Term
Def QName
qn [Arg Term -> Elim
forall a. Arg a -> Elim' a
Apply (Term -> Arg Term
forall a. a -> Arg a
defaultArg Term
t)]) (Arg Nat, Term) -> [(Arg Nat, Term)] -> [(Arg Nat, Term)]
`cons` [(Arg Nat, Term)]
vars
Def{} -> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)]
forall {a}. ExceptT InvertExcept (TCMT IO) a
neutralArg
t :: Term
t@Lam{} -> Term -> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)]
failure Term
t
t :: Term
t@Lit{} -> Term -> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)]
failure Term
t
t :: Term
t@MetaV{} -> Term -> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)]
failure Term
t
Pi{} -> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)]
forall {a}. ExceptT InvertExcept (TCMT IO) a
neutralArg
Sort{} -> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)]
forall {a}. ExceptT InvertExcept (TCMT IO) a
neutralArg
Level{} -> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)]
forall {a}. ExceptT InvertExcept (TCMT IO) a
neutralArg
DontCare{} -> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)]
forall a. HasCallStack => a
__IMPOSSIBLE__
Dummy [Char]
s Elims
_ -> [Char] -> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)]
forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
[Char] -> m a
__IMPOSSIBLE_VERBOSE__ [Char]
s
append :: Res -> Res -> Res
append :: [(Arg Nat, Term)] -> [(Arg Nat, Term)] -> [(Arg Nat, Term)]
append [(Arg Nat, Term)]
res [(Arg Nat, Term)]
vars = ((Arg Nat, Term) -> [(Arg Nat, Term)] -> [(Arg Nat, Term)])
-> [(Arg Nat, Term)] -> [(Arg Nat, Term)] -> [(Arg Nat, Term)]
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Arg Nat, Term) -> [(Arg Nat, Term)] -> [(Arg Nat, Term)]
cons [(Arg Nat, Term)]
vars [(Arg Nat, Term)]
res
cons :: (Arg Nat, Term) -> Res -> Res
cons :: (Arg Nat, Term) -> [(Arg Nat, Term)] -> [(Arg Nat, Term)]
cons a :: (Arg Nat, Term)
a@(Arg ArgInfo
ai Nat
i, Term
t) [(Arg Nat, Term)]
vars
| ArgInfo -> Bool
forall a. LensRelevance a => a -> Bool
isIrrelevant ArgInfo
ai = Bool
-> ([(Arg Nat, Term)] -> [(Arg Nat, Term)])
-> [(Arg Nat, Term)]
-> [(Arg Nat, Term)]
forall b a. IsBool b => b -> (a -> a) -> a -> a
applyUnless (((Arg Nat, Term) -> Bool) -> [(Arg Nat, Term)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ((Nat
i Nat -> Nat -> Bool
forall a. Eq a => a -> a -> Bool
==) (Nat -> Bool)
-> ((Arg Nat, Term) -> Nat) -> (Arg Nat, Term) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg Nat -> Nat
forall e. Arg e -> e
unArg (Arg Nat -> Nat)
-> ((Arg Nat, Term) -> Arg Nat) -> (Arg Nat, Term) -> Nat
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Arg Nat, Term) -> Arg Nat
forall a b. (a, b) -> a
fst) [(Arg Nat, Term)]
vars) ((Arg Nat, Term)
a (Arg Nat, Term) -> [(Arg Nat, Term)] -> [(Arg Nat, Term)]
forall a. a -> [a] -> [a]
:) [(Arg Nat, Term)]
vars
| Bool
otherwise = (Arg Nat, Term)
a (Arg Nat, Term) -> [(Arg Nat, Term)] -> [(Arg Nat, Term)]
forall a. a -> [a] -> [a]
:
((Arg Nat, Term) -> Bool) -> [(Arg Nat, Term)] -> [(Arg Nat, Term)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool)
-> ((Arg Nat, Term) -> Bool) -> (Arg Nat, Term) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\ a :: (Arg Nat, Term)
a@(Arg ArgInfo
info Nat
j, Term
t) -> ArgInfo -> Bool
forall a. LensRelevance a => a -> Bool
isIrrelevant ArgInfo
info Bool -> Bool -> Bool
&& Nat
i Nat -> Nat -> Bool
forall a. Eq a => a -> a -> Bool
== Nat
j)) [(Arg Nat, Term)]
vars
isFaceConstraint
:: MetaId
-> Args
-> TCM (Maybe (MetaVariable, IntMap.IntMap Bool, SubstCand, Substitution))
isFaceConstraint :: MetaId
-> Args
-> TCM
(Maybe (MetaVariable, IntMap Bool, [(Nat, Term)], Substitution))
isFaceConstraint MetaId
mid Args
args = MaybeT
(TCMT IO) (MetaVariable, IntMap Bool, [(Nat, Term)], Substitution)
-> TCM
(Maybe (MetaVariable, IntMap Bool, [(Nat, Term)], Substitution))
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (MaybeT
(TCMT IO) (MetaVariable, IntMap Bool, [(Nat, Term)], Substitution)
-> TCM
(Maybe (MetaVariable, IntMap Bool, [(Nat, Term)], Substitution)))
-> MaybeT
(TCMT IO) (MetaVariable, IntMap Bool, [(Nat, Term)], Substitution)
-> TCM
(Maybe (MetaVariable, IntMap Bool, [(Nat, Term)], Substitution))
forall a b. (a -> b) -> a -> b
$ do
iv <- MaybeT (TCMT IO) (Term -> IntervalView)
forall (m :: * -> *). HasBuiltins m => m (Term -> IntervalView)
intervalView'
mvar <- lookupLocalMeta mid
(_, _, _) <- MaybeT $ isInteractionMetaB mid args
let
t = 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
mvar
n = Args -> Nat
forall a. [a] -> Nat
forall (t :: * -> *) a. Foldable t => t a -> Nat
length Args
args
isEndpoint Term
tm = Maybe (Nat, Bool) -> Bool
forall a. Maybe a -> Bool
isJust (Arg Term -> Nat -> Maybe (Nat, Bool)
fin (Term -> Arg Term
forall a. a -> Arg a
defaultArg Term
tm) Nat
0)
fin (Arg ArgInfo
_ Term
tm) Nat
i = case Term -> IntervalView
iv Term
tm of
IntervalView
IOne -> (Nat, Bool) -> Maybe (Nat, Bool)
forall a. a -> Maybe a
Just (Nat
i, Bool
True)
IntervalView
IZero -> (Nat, Bool) -> Maybe (Nat, Bool)
forall a. a -> Maybe a
Just (Nat
i, Bool
False)
IntervalView
_ -> Maybe (Nat, Bool)
forall a. Maybe a
Nothing
sub <- MaybeT $ either (const Nothing) Just <$> runExceptT (inverseSubst' isEndpoint args)
ids <- MaybeT $ either (const Nothing) Just <$> runExceptT (checkLinearity sub)
m <- getContextSize
TelV tel' _ <- telViewUpToPath n t
tel'' <- enterClosure mvar $ \Range
_ -> MaybeT (TCMT IO) (Tele (Dom Type))
forall (m :: * -> *).
(Applicative m, MonadTCEnv m) =>
m (Tele (Dom Type))
getContextTelescope
let
assocToList Nat
i = \case
[(Nat, Term)]
_ | Nat
i Nat -> Nat -> Bool
forall a. Ord a => a -> a -> Bool
>= Nat
m -> []
((Nat
j,Term
u) : [(Nat, Term)]
l) | Nat
i Nat -> Nat -> Bool
forall a. Eq a => a -> a -> Bool
== Nat
j -> Term -> Maybe Term
forall a. a -> Maybe a
Just Term
u Maybe Term -> [Maybe Term] -> [Maybe Term]
forall a. a -> [a] -> [a]
: Nat -> [(Nat, Term)] -> [Maybe Term]
assocToList (Nat
i Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
+ Nat
1) [(Nat, Term)]
l
[(Nat, Term)]
l -> Maybe Term
forall a. Maybe a
Nothing Maybe Term -> [Maybe Term] -> [Maybe Term]
forall a. a -> [a] -> [a]
: Nat -> [(Nat, Term)] -> [Maybe Term]
assocToList (Nat
i Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
+ Nat
1) [(Nat, Term)]
l
ivs = Nat -> [(Nat, Term)] -> [Maybe Term]
assocToList Nat
0 [(Nat, Term)]
ids
rho = Impossible -> [Maybe Term] -> Substitution -> Substitution
forall a.
DeBruijn a =>
Impossible -> [Maybe a] -> Substitution' a -> Substitution' a
prependS Impossible
HasCallStack => Impossible
impossible [Maybe Term]
ivs (Substitution -> Substitution) -> Substitution -> Substitution
forall a b. (a -> b) -> a -> b
$ Nat -> Substitution
forall a. Nat -> Substitution' a
raiseS Nat
n
over = Tele (Dom Type) -> Nat
forall a. Sized a => a -> Nat
size Tele (Dom Type)
tel' Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Tele (Dom Type) -> Nat
forall a. Sized a => a -> Nat
size Tele (Dom Type)
tel''
endps = [(Nat, Bool)] -> IntMap Bool
forall a. [(Nat, a)] -> IntMap a
IntMap.fromList ([(Nat, Bool)] -> IntMap Bool) -> [(Nat, Bool)] -> IntMap Bool
forall a b. (a -> b) -> a -> b
$ [Maybe (Nat, Bool)] -> [(Nat, Bool)]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe (Nat, Bool)] -> [(Nat, Bool)])
-> [Maybe (Nat, Bool)] -> [(Nat, Bool)]
forall a b. (a -> b) -> a -> b
$ (Arg Term -> Nat -> Maybe (Nat, Bool))
-> Args -> [Nat] -> [Maybe (Nat, Bool)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\Arg Term
a Nat
i -> Arg Term -> Nat -> Maybe (Nat, Bool)
fin Arg Term
a (Nat
i Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
over)) Args
args (Nat -> [Nat]
forall a. Integral a => a -> [a]
downFrom Nat
n)
reportSDoc "tc.ip.boundary" 45 $ vcat
[ "ivs =" <+> prettyTCM ivs
, "tel' =" <+> prettyTCM tel'
, "tel'' =" <+> prettyTCM tel''
, "ids =" <+> prettyTCM ids
, "sub =" <+> prettyTCM sub
, "endps =" <+> pretty endps
]
guard (not (IntMap.null endps))
guard (all (>= 0) (IntMap.keys endps))
pure (mvar, endps, ids, rho)
tryAddBoundary :: CompareDirection -> MetaId -> InteractionId -> Args -> Term -> CompareAs -> TCM ()
tryAddBoundary :: CompareDirection
-> MetaId -> InteractionId -> Args -> Term -> CompareAs -> TCM ()
tryAddBoundary CompareDirection
dir MetaId
x InteractionId
iid Args
args Term
v CompareAs
target = do
[Char] -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.ip.boundary" Nat
30 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
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
"boundary: looking at equational constraint"
, Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM (MetaId -> Elims -> Term
MetaV MetaId
x (Arg Term -> Elim
forall a. Arg a -> Elim' a
Apply (Arg Term -> Elim) -> Args -> Elims
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Args
args)) 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
v
]
iv <- TCMT IO (Term -> IntervalView)
forall (m :: * -> *). HasBuiltins m => m (Term -> IntervalView)
intervalView'
mvar <- lookupLocalMeta x
let
t = 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
mvar
n = Args -> Nat
forall a. [a] -> Nat
forall (t :: * -> *) a. Foldable t => t a -> Nat
length Args
args
rhsv = Term -> VarSet
forall t. Free t => t -> VarSet
allFreeVars Term
v
allVars :: SubstCand -> Bool
allVars [(Nat, Term)]
sub = VarSet
rhsv VarSet -> VarSet -> Bool
`VarSet.isSubsetOf` [Nat] -> VarSet
VarSet.fromList (((Nat, Term) -> Nat) -> [(Nat, Term)] -> [Nat]
forall a b. (a -> b) -> [a] -> [b]
map (Nat, Term) -> Nat
forall a b. (a, b) -> a
fst [(Nat, Term)]
sub)
TelV tel' _ <- telViewUpToPath n t
void . runMaybeT $ do
(_, endps, ids, rho) <- MaybeT $ isFaceConstraint x args
guard (allVars ids)
let v' = Tele (Dom Type) -> Term -> Term
forall t. Abstract t => Tele (Dom Type) -> t -> t
abstract Tele (Dom Type)
tel' (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Substitution' (SubstArg Term) -> Term -> Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution
Substitution' (SubstArg Term)
rho Term
v
enterClosure mvar $ \Range
_ -> do
[Char] -> Nat -> TCMT IO Doc -> MaybeT (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.ip.boundary" Nat
30 (TCMT IO Doc -> MaybeT (TCMT IO) ())
-> TCMT IO Doc -> MaybeT (TCMT IO) ()
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
"recovered interaction point boundary"
, TCMT IO Doc
" endps =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> IntMap Bool -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty IntMap Bool
endps
, TCMT IO Doc
" rho =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Substitution -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Substitution
rho
, TCMT IO Doc
" t =" 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 (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t)
, TCMT IO Doc
" v' =" 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 (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
v')
]
let
upd :: IPBoundary' Term -> IPBoundary' Term
upd (IPBoundary Map (IntMap Bool) Term
m) = case IntMap Bool -> Map (IntMap Bool) Term -> Maybe Term
forall k a. Ord k => k -> Map k a -> Maybe a
MapS.lookup IntMap Bool
endps Map (IntMap Bool) Term
m of
Just Term
t -> if Term -> Nat
forall a. TermSize a => a -> Nat
termSize Term
t Nat -> Nat -> Bool
forall a. Ord a => a -> a -> Bool
< Term -> Nat
forall a. TermSize a => a -> Nat
termSize Term
v'
then Map (IntMap Bool) Term -> IPBoundary' Term
forall t. Map (IntMap Bool) t -> IPBoundary' t
IPBoundary Map (IntMap Bool) Term
m
else Map (IntMap Bool) Term -> IPBoundary' Term
forall t. Map (IntMap Bool) t -> IPBoundary' t
IPBoundary (Map (IntMap Bool) Term -> IPBoundary' Term)
-> Map (IntMap Bool) Term -> IPBoundary' Term
forall a b. (a -> b) -> a -> b
$ IntMap Bool
-> Term -> Map (IntMap Bool) Term -> Map (IntMap Bool) Term
forall k a. Ord k => k -> a -> Map k a -> Map k a
MapS.insert IntMap Bool
endps Term
v' Map (IntMap Bool) Term
m
Maybe Term
Nothing -> Map (IntMap Bool) Term -> IPBoundary' Term
forall t. Map (IntMap Bool) t -> IPBoundary' t
IPBoundary (Map (IntMap Bool) Term -> IPBoundary' Term)
-> Map (IntMap Bool) Term -> IPBoundary' Term
forall a b. (a -> b) -> a -> b
$ IntMap Bool
-> Term -> Map (IntMap Bool) Term -> Map (IntMap Bool) Term
forall k a. Ord k => k -> a -> Map k a -> Map k a
MapS.insert IntMap Bool
endps Term
v' Map (IntMap Bool) Term
m
f :: InteractionPoint -> InteractionPoint
f InteractionPoint
ip = InteractionPoint
ip{ ipBoundary = upd (ipBoundary ip) }
TCM () -> MaybeT (TCMT IO) ()
forall (m :: * -> *) a. Monad m => m a -> MaybeT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM () -> MaybeT (TCMT IO) ()) -> TCM () -> MaybeT (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ (InteractionPoints -> InteractionPoints) -> TCM ()
forall (m :: * -> *).
MonadInteractionPoints m =>
(InteractionPoints -> InteractionPoints) -> m ()
modifyInteractionPoints ((InteractionPoint -> InteractionPoint)
-> InteractionId -> InteractionPoints -> InteractionPoints
forall k v.
(Ord k, Ord (Tag v), HasTag v) =>
(v -> v) -> k -> BiMap k v -> BiMap k v
BiMap.adjust InteractionPoint -> InteractionPoint
f InteractionId
iid)
openMetasToPostulates :: TCM ()
openMetasToPostulates :: TCM ()
openMetasToPostulates = do
m <- (TCEnv -> ModuleName) -> TCMT IO ModuleName
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> ModuleName
envCurrentModule
ms <- MapS.assocs <$> useTC stOpenMetaStore
forM_ ms $ \ (MetaId
x, MetaVariable
mv) -> do
let t :: Type
t = Type -> Type
dummyTypeToOmega (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ 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
let r :: Range
r = Closure Range -> Range
forall a. Closure a -> a
clValue (Closure Range -> Range) -> Closure Range -> Range
forall a b. (a -> b) -> a -> b
$ MetaInfo -> Closure Range
miClosRange (MetaInfo -> Closure Range) -> MetaInfo -> Closure Range
forall a b. (a -> b) -> a -> b
$ MetaVariable -> MetaInfo
mvInfo MetaVariable
mv
s' <- Doc -> [Char]
forall a. Doc a -> [Char]
render (Doc -> [Char]) -> TCMT IO Doc -> TCMT IO [Char]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => MetaId -> m Doc
prettyTCM MetaId
x
let s = [Char]
"unsolved#meta." [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ (Char -> Bool) -> [Char] -> [Char]
forall a. (a -> Bool) -> [a] -> [a]
filter (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= Char
'_') [Char]
s'
n <- freshName r s
let q = ModuleName -> Name -> QName
A.QName ModuleName
m Name
n
reportSDoc "meta.postulate" 20 $ vcat
[ text ("Turning " ++ if isSortMeta_ mv then "sort" else "value" ++ " meta ")
<+> prettyTCM x <+> " into postulate."
, nest 2 $ vcat
[ "Name: " <+> prettyTCM q
, "Type: " <+> prettyTCM t
]
]
addConstant' q defaultArgInfo q t defaultAxiom
let inst = Instantiation -> MetaInstantiation
InstV (Instantiation -> MetaInstantiation)
-> Instantiation -> MetaInstantiation
forall a b. (a -> b) -> a -> b
$ Instantiation
{ instTel :: [Arg [Char]]
instTel = [], instBody :: Term
instBody = QName -> Elims -> Term
Def QName
q [] }
updateMetaVar x $ \ MetaVariable
mv0 -> MetaVariable
mv0 { mvInstantiation = inst }
return ()
where
dummyTypeToOmega :: Type -> Type
dummyTypeToOmega Type
t =
case Type -> TelV Type
telView' Type
t of
TelV Tele (Dom Type)
tel (El Sort
_ Dummy{}) -> Tele (Dom Type) -> Type -> Type
forall t. Abstract t => Tele (Dom Type) -> t -> t
abstract Tele (Dom Type)
tel (Sort -> Type
sort (Sort -> Type) -> Sort -> Type
forall a b. (a -> b) -> a -> b
$ Univ -> Integer -> Sort
forall t. Univ -> Integer -> Sort' t
Inf Univ
UType Integer
0)
TelV Type
_ -> Type
t
dependencySortMetas :: [MetaId] -> TCM (Maybe [MetaId])
dependencySortMetas :: [MetaId] -> TCM (Maybe [MetaId])
dependencySortMetas [MetaId]
metas = do
metaGraph <- [[(MetaId, MetaId)]] -> [(MetaId, MetaId)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[(MetaId, MetaId)]] -> [(MetaId, MetaId)])
-> TCMT IO [[(MetaId, MetaId)]] -> TCMT IO [(MetaId, MetaId)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
[MetaId]
-> (MetaId -> TCMT IO [(MetaId, MetaId)])
-> TCMT IO [[(MetaId, MetaId)]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [MetaId]
metas ((MetaId -> TCMT IO [(MetaId, MetaId)])
-> TCMT IO [[(MetaId, MetaId)]])
-> (MetaId -> TCMT IO [(MetaId, MetaId)])
-> TCMT IO [[(MetaId, MetaId)]]
forall a b. (a -> b) -> a -> b
$ \ MetaId
m -> do
deps <- (MetaId -> Set MetaId) -> Maybe Type -> Set MetaId
forall m. Monoid m => (MetaId -> m) -> Maybe Type -> m
forall t m. (AllMetas t, Monoid m) => (MetaId -> m) -> t -> m
allMetas (\MetaId
m' -> if MetaId
m' MetaId -> Set MetaId -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set MetaId
metas'
then MetaId -> Set MetaId
forall el coll. Singleton el coll => el -> coll
singleton MetaId
m'
else Set MetaId
forall a. Monoid a => a
mempty) (Maybe Type -> Set MetaId)
-> TCMT IO (Maybe Type) -> TCMT IO (Set MetaId)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
MetaId -> TCMT IO (Maybe Type)
forall {m :: * -> *}. MonadReduce m => MetaId -> m (Maybe Type)
getType MetaId
m
return [ (m, m') | m' <- Set.toList deps ]
return $ Graph.topSort metas' metaGraph
where
metas' :: Set MetaId
metas' = [MetaId] -> Set MetaId
forall a. Ord a => [a] -> Set a
Set.fromList [MetaId]
metas
getType :: MetaId -> m (Maybe Type)
getType MetaId
m = do
j <- MetaId -> m (Judgement MetaId)
forall (m :: * -> *).
ReadTCState m =>
MetaId -> m (Judgement MetaId)
lookupMetaJudgement MetaId
m
case j of
IsSort{} -> Maybe Type -> m (Maybe Type)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Type
forall a. Maybe a
Nothing
HasType{ jMetaType :: forall a. Judgement a -> Type
jMetaType = Type
t } -> Type -> Maybe Type
forall a. a -> Maybe a
Just (Type -> Maybe Type) -> m Type -> m (Maybe Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> m Type
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull Type
t