module Agda.TypeChecking.MetaVars where
import Control.Monad.Reader
import Data.Function
import Data.List hiding (sort)
import qualified Data.List as List
import qualified Data.Map as Map
import qualified Data.Foldable as Fold
import qualified Data.Traversable as Trav
import Agda.Syntax.Common
import Agda.Syntax.Internal as I
import Agda.Syntax.Internal.Generic
import Agda.Syntax.Position
import qualified Agda.Syntax.Abstract as A
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Monad.Builtin
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Constraints
import Agda.TypeChecking.Errors
import Agda.TypeChecking.Free
import Agda.TypeChecking.Level
import Agda.TypeChecking.Records
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Irrelevance
import Agda.TypeChecking.EtaContract
import Agda.TypeChecking.SizedTypes (boundedSizeMetaHook, isSizeProblem)
import Agda.TypeChecking.MetaVars.Occurs
import Agda.Utils.Except
( ExceptT
#if !MIN_VERSION_transformers(0,4,1)
, Error(noMsg)
#endif
, MonadError(throwError)
, runExceptT
)
import Agda.Utils.List
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Size
import Agda.Utils.Tuple
import Agda.Utils.Permutation
import Agda.Utils.Pretty (prettyShow)
import qualified Agda.Utils.VarSet as Set
#include "undefined.h"
import Agda.Utils.Impossible
findIdx :: Eq a => [a] -> a -> Maybe Int
findIdx vs v = findIndex (==v) (reverse vs)
isBlockedTerm :: MetaId -> TCM Bool
isBlockedTerm x = do
reportSLn "tc.meta.blocked" 12 $ "is " ++ prettyShow x ++ " a blocked term? "
i <- mvInstantiation <$> lookupMeta x
let r = case i of
BlockedConst{} -> True
PostponedTypeCheckingProblem{} -> True
InstV{} -> False
InstS{} -> False
Open{} -> False
OpenIFS{} -> False
reportSLn "tc.meta.blocked" 12 $
if r then " yes, because " ++ show i else " no"
return r
isEtaExpandable :: MetaId -> TCM Bool
isEtaExpandable x = do
i <- mvInstantiation <$> lookupMeta x
return $ case i of
Open{} -> True
OpenIFS{} -> False
InstV{} -> False
InstS{} -> False
BlockedConst{} -> False
PostponedTypeCheckingProblem{} -> False
assignTerm :: MetaId -> [I.Arg ArgName] -> Term -> TCM ()
assignTerm x tel v = do
whenM (isFrozen x) __IMPOSSIBLE__
assignTerm' x tel v
assignTerm' :: MetaId -> [I.Arg ArgName] -> Term -> TCM ()
assignTerm' x tel v = do
reportSLn "tc.meta.assign" 70 $ prettyShow x ++ " := " ++ show v ++ "\n in " ++ show tel
whenM (not <$> asks envAssignMetas) __IMPOSSIBLE__
let i = metaInstance tel v
verboseS "profile.metas" 10 $ liftTCM $ tickMax "max-open-metas" . size =<< getOpenMetas
modifyMetaStore $ ins x i
etaExpandListeners x
wakeupConstraints x
reportSLn "tc.meta.assign" 20 $ "completed assignment of " ++ prettyShow x
where
metaInstance tel v = InstV tel v
ins x i store = Map.adjust (inst i) x store
inst i mv = mv { mvInstantiation = i }
newSortMeta :: TCM Sort
newSortMeta =
ifM typeInType (return $ mkType 0) $
ifM hasUniversePolymorphism (newSortMetaCtx =<< getContextArgs)
$ do i <- createMetaInfo
lvl <- levelType
x <- newMeta i normalMetaPriority (idP 0) $ IsSort () lvl
return $ Type $ Max [Plus 0 $ MetaLevel x []]
newSortMetaCtx :: Args -> TCM Sort
newSortMetaCtx vs =
ifM typeInType (return $ mkType 0) $ do
i <- createMetaInfo
tel <- getContextTelescope
lvl <- levelType
let t = telePi_ tel lvl
x <- newMeta i normalMetaPriority (idP 0) (IsSort () t)
reportSDoc "tc.meta.new" 50 $
text "new sort meta" <+> prettyTCM x <+> text ":" <+> prettyTCM t
return $ Type $ Max [Plus 0 $ MetaLevel x $ map Apply vs]
newTypeMeta :: Sort -> TCM Type
newTypeMeta s = El s <$> newValueMeta RunMetaOccursCheck (sort s)
newTypeMeta_ :: TCM Type
newTypeMeta_ = newTypeMeta =<< (workOnTypes $ newSortMeta)
newIFSMeta :: MetaNameSuggestion -> Type -> Maybe [(Term, Type)] -> TCM Term
newIFSMeta s t cands = do
TelV tel t' <- telView t
addCtxTel tel $ do
vs <- getContextArgs
ctx <- getContextTelescope
teleLam tel <$> newIFSMetaCtx s (telePi_ ctx t') vs (raise (size tel) cands)
newIFSMetaCtx :: MetaNameSuggestion -> Type -> Args -> Maybe [(Term, Type)] -> TCM Term
newIFSMetaCtx s t vs cands = do
reportSDoc "tc.meta.new" 50 $ fsep
[ text "new ifs meta:"
, nest 2 $ prettyTCM vs <+> text "|-"
]
i0 <- createMetaInfo
let i = i0 { miNameSuggestion = s }
TelV tel _ <- telView t
let perm = idP (size tel)
x <- newMeta' OpenIFS i normalMetaPriority perm (HasType () t)
reportSDoc "tc.meta.new" 50 $ fsep
[ nest 2 $ pretty x <+> text ":" <+> prettyTCM t
]
addConstraint $ FindInScope x cands
return $ MetaV x $ map Apply vs
newNamedValueMeta :: RunMetaOccursCheck -> MetaNameSuggestion -> Type -> TCM Term
newNamedValueMeta b s t = do
v <- newValueMeta b t
setValueMetaName v s
return v
newValueMeta :: RunMetaOccursCheck -> Type -> TCM Term
newValueMeta b t = do
vs <- getContextArgs
tel <- getContextTelescope
newValueMetaCtx b (telePi_ tel t) vs
newValueMetaCtx :: RunMetaOccursCheck -> Type -> Args -> TCM Term
newValueMetaCtx b t ctx =
instantiateFull =<< newValueMetaCtx' b t ctx
newValueMeta' :: RunMetaOccursCheck -> Type -> TCM Term
newValueMeta' b t = do
vs <- getContextArgs
tel <- getContextTelescope
newValueMetaCtx' b (telePi_ tel t) vs
newValueMetaCtx' :: RunMetaOccursCheck -> Type -> Args -> TCM Term
newValueMetaCtx' b t vs = do
i <- createMetaInfo' b
TelV tel a <- telView t
let perm = idP (size tel)
x <- newMeta i normalMetaPriority perm (HasType () t)
reportSDoc "tc.meta.new" 50 $ fsep
[ text "new meta:"
, nest 2 $ prettyTCM vs <+> text "|-"
, nest 2 $ pretty x <+> text ":" <+> prettyTCM t
]
etaExpandMetaSafe x
let u = shared $ MetaV x $ map Apply vs
boundedSizeMetaHook u tel a
return u
newTelMeta :: Telescope -> TCM Args
newTelMeta tel = newArgsMeta (abstract tel $ typeDontCare)
type Condition = I.Dom Type -> Abs Type -> Bool
trueCondition :: Condition
trueCondition _ _ = True
newArgsMeta :: Type -> TCM Args
newArgsMeta = newArgsMeta' trueCondition
newArgsMeta' :: Condition -> Type -> TCM Args
newArgsMeta' condition t = do
args <- getContextArgs
tel <- getContextTelescope
newArgsMetaCtx' condition t tel args
newArgsMetaCtx :: Type -> Telescope -> Args -> TCM Args
newArgsMetaCtx = newArgsMetaCtx' trueCondition
newArgsMetaCtx' :: Condition -> Type -> Telescope -> Args -> TCM Args
newArgsMetaCtx' condition (El s tm) tel ctx = do
tm <- reduce tm
case ignoreSharing tm of
Pi dom@(Dom info a) codom | condition dom codom -> do
arg <- Arg info <$> do
applyRelevanceToContext (getRelevance info) $
newValueMetaCtx RunMetaOccursCheck (telePi_ tel a) ctx
args <- newArgsMetaCtx' condition (El s tm `piApply` [arg]) tel ctx
return $ arg : args
_ -> return []
newRecordMeta :: QName -> Args -> TCM Term
newRecordMeta r pars = do
args <- getContextArgs
tel <- getContextTelescope
newRecordMetaCtx r pars tel args
newRecordMetaCtx :: QName -> Args -> Telescope -> Args -> TCM Term
newRecordMetaCtx r pars tel ctx = do
ftel <- flip apply pars <$> getRecordFieldTypes r
fields <- newArgsMetaCtx (telePi_ ftel $ sort Prop) tel ctx
con <- getRecordConstructor r
return $ Con con fields
newQuestionMark :: InteractionId -> Type -> TCM Term
newQuestionMark ii t = do
m <- newValueMeta' DontRunMetaOccursCheck t
let MetaV x _ = ignoreSharing m
connectInteractionPoint ii x
return m
blockTerm :: Type -> TCM Term -> TCM Term
blockTerm t blocker = do
(pid, v) <- newProblem blocker
blockTermOnProblem t v pid
blockTermOnProblem :: Type -> Term -> ProblemId -> TCM Term
blockTermOnProblem t v pid =
ifM (isProblemSolved pid `or2M` isSizeProblem pid) (return v) $ do
i <- createMetaInfo
es <- map Apply <$> getContextArgs
tel <- getContextTelescope
x <- newMeta' (BlockedConst $ abstract tel v)
i lowMetaPriority (idP $ size tel)
(HasType () $ telePi_ tel t)
inTopContext $ addConstraint (Guarded (UnBlock x) pid)
reportSDoc "tc.meta.blocked" 20 $ vcat
[ text "blocked" <+> prettyTCM x <+> text ":=" <+> inTopContext (prettyTCM $ abstract tel v)
, text " by" <+> (prettyTCM =<< getConstraintsForProblem pid) ]
inst <- isInstantiatedMeta x
case inst of
True -> instantiate (MetaV x es)
False -> do
v <- newValueMeta DontRunMetaOccursCheck t
i <- liftTCM fresh
cmp <- buildProblemConstraint 0 (ValueCmp CmpEq t v (MetaV x es))
listenToMeta (CheckConstraint i cmp) x
return v
blockTypeOnProblem :: Type -> ProblemId -> TCM Type
blockTypeOnProblem (El s a) pid = El s <$> blockTermOnProblem (El Inf $ Sort s) a pid
unblockedTester :: Type -> TCM Bool
unblockedTester t = ifBlockedType t (\ m t -> return False) (\ t -> return True)
postponeTypeCheckingProblem_ :: TypeCheckingProblem -> TCM Term
postponeTypeCheckingProblem_ p = do
postponeTypeCheckingProblem p (unblock p)
where
unblock (CheckExpr _ t) = unblockedTester t
unblock (CheckArgs _ _ _ _ t _ _) = unblockedTester t
unblock (CheckLambda _ _ t) = unblockedTester t
postponeTypeCheckingProblem :: TypeCheckingProblem -> TCM Bool -> TCM Term
postponeTypeCheckingProblem p unblock = do
i <- createMetaInfo' DontRunMetaOccursCheck
tel <- getContextTelescope
cl <- buildClosure p
let t = problemType p
m <- newMeta' (PostponedTypeCheckingProblem cl unblock)
i normalMetaPriority (idP (size tel))
$ HasType () $ telePi_ tel t
es <- map Apply <$> getContextArgs
v <- newValueMeta DontRunMetaOccursCheck t
cmp <- buildProblemConstraint 0 (ValueCmp CmpEq t v (MetaV m es))
i <- liftTCM fresh
listenToMeta (CheckConstraint i cmp) m
addConstraint (UnBlock m)
return v
problemType :: TypeCheckingProblem -> Type
problemType (CheckExpr _ t ) = t
problemType (CheckArgs _ _ _ _ _ t _ ) = t
problemType (CheckLambda _ _ t ) = t
etaExpandListeners :: MetaId -> TCM ()
etaExpandListeners m = do
ls <- getMetaListeners m
clearMetaListeners m
mapM_ wakeupListener ls
wakeupListener :: Listener -> TCM ()
wakeupListener (EtaExpand x) = etaExpandMetaSafe x
wakeupListener (CheckConstraint _ c) = do
reportSDoc "tc.meta.blocked" 20 $ text "waking boxed constraint" <+> prettyTCM c
addAwakeConstraints [c]
solveAwakeConstraints
etaExpandMetaSafe :: MetaId -> TCM ()
etaExpandMetaSafe = etaExpandMeta [SingletonRecords,Levels]
data MetaKind =
Records
| SingletonRecords
| Levels
deriving (Eq, Enum, Bounded, Show)
allMetaKinds :: [MetaKind]
allMetaKinds = [minBound .. maxBound]
etaExpandMeta :: [MetaKind] -> MetaId -> TCM ()
etaExpandMeta kinds m = whenM (isEtaExpandable m) $ do
verboseBracket "tc.meta.eta" 20 ("etaExpandMeta " ++ prettyShow m) $ do
let waitFor x = do
reportSDoc "tc.meta.eta" 20 $ do
text "postponing eta-expansion of meta variable" <+>
prettyTCM m <+>
text "which is blocked by" <+> prettyTCM x
listenToMeta (EtaExpand m) x
dontExpand = do
reportSDoc "tc.meta.eta" 20 $ do
text "we do not expand meta variable" <+> prettyTCM m <+>
text ("(requested was expansion of " ++ show kinds ++ ")")
meta <- lookupMeta m
let HasType _ a = mvJudgement meta
TelV tel b <- telView a
ifBlocked (unEl b) (\ x _ -> waitFor x) $ \ t -> case ignoreSharing t of
lvl@(Def r es) ->
ifM (isEtaRecord r) (do
let ps = fromMaybe __IMPOSSIBLE__ $ allApplyElims es
let expand = do
u <- withMetaInfo' meta $ newRecordMetaCtx r ps tel $ teleArgs tel
inTopContext $ do
verboseS "tc.meta.eta" 15 $ do
du <- prettyTCM u
reportSDoc "tc.meta.eta" 15 $ sep
[ text "eta expanding: " <+> pretty m <+> text " --> "
, nest 2 $ prettyTCM u
]
noConstraints $ assignTerm' m (telToArgs tel) u
if Records `elem` kinds then
expand
else if (SingletonRecords `elem` kinds) then do
singleton <- isSingletonRecord r ps
case singleton of
Left x -> waitFor x
Right False -> dontExpand
Right True -> expand
else dontExpand
) $ ifM (andM [ return $ Levels `elem` kinds
, typeInType
, (Just lvl ==) <$> getBuiltin' builtinLevel
]) (do
reportSLn "tc.meta.eta" 20 $ "Expanding level meta to 0 (type-in-type)"
noConstraints $ assignTerm m (telToArgs tel) (Level $ Max [])
) $ dontExpand
_ -> dontExpand
etaExpandBlocked :: Reduce t => Blocked t -> TCM (Blocked t)
etaExpandBlocked t@NotBlocked{} = return t
etaExpandBlocked (Blocked m t) = do
etaExpandMeta [Records] m
t <- reduceB t
case t of
Blocked m' _ | m /= m' -> etaExpandBlocked t
_ -> return t
assignV :: CompareDirection -> MetaId -> Args -> Term -> TCM ()
assignV dir x args v = assignWrapper dir x (map Apply args) v $ assign dir x args v
assignWrapper :: CompareDirection -> MetaId -> Elims -> Term -> TCM () -> TCM ()
assignWrapper dir x es v doAssign = do
ifNotM (asks envAssignMetas) patternViolation $ do
reportSDoc "tc.meta.assign" 10 $ do
text "term" <+> prettyTCM (MetaV x es) <+> text (":" ++ show dir) <+> prettyTCM v
liftTCM $ nowSolvingConstraints doAssign `finally` solveAwakeConstraints
assign :: CompareDirection -> MetaId -> Args -> Term -> TCM ()
assign dir x args v = do
mvar <- lookupMeta x
let t = jMetaType $ mvJudgement mvar
v <- instantiate v
reportSLn "tc.meta.assign" 50 $ "MetaVars.assign: assigning to " ++ show v
case (ignoreSharing v, mvJudgement mvar) of
(Sort Inf, HasType{}) -> typeError SetOmegaNotValidType
_ -> return ()
when (mvFrozen mvar == Frozen) $ do
reportSLn "tc.meta.assign" 25 $ "aborting: meta is frozen!"
patternViolation
whenM (isBlockedTerm x) patternViolation
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 m0 _ -> text "r.h.s. blocked on:" <+> prettyTCM m0
NotBlocked{} -> text "r.h.s. not blocked"
subtypingForSizeLt dir x mvar t args v $ \ v -> do
expandProjectedVars args v $ \ args v -> do
let relVL = Set.toList $ allRelevantVars args
let fromIrrVar (Var i []) = return [i]
fromIrrVar (Con c vs) =
ifM (isNothing <$> isRecordConstructor (conName c)) (return []) $
concat <$> mapM (fromIrrVar . unArg) vs
fromIrrVar (Shared p) = fromIrrVar (derefPtr p)
fromIrrVar _ = return []
irrVL <- concat <$> mapM fromIrrVar
[ v | Arg info v <- args, irrelevantOrUnused (getRelevance info) ]
reportSDoc "tc.meta.assign" 20 $
let pr (Var n []) = text (show n)
pr (Def c []) = prettyTCM c
pr _ = text ".."
in vcat
[ text "mvar args:" <+> sep (map (pr . unArg) args)
, text "fvars lhs (rel):" <+> sep (map (text . show) relVL)
, text "fvars lhs (irr):" <+> sep (map (text . show) irrVL)
]
v <- liftTCM $ occursCheck x (relVL, irrVL) v
reportSLn "tc.meta.assign" 15 "passed occursCheck"
verboseS "tc.meta.assign" 30 $ do
let n = termSize v
when (n > 200) $ reportSDoc "tc.meta.assign" 30 $
sep [ text "size" <+> text (show n)
, nest 2 $ text "term" <+> prettyTCM v
]
let fvs = allFreeVars v
reportSDoc "tc.meta.assign" 20 $
text "fvars rhs:" <+> sep (map (text . show) $ Set.toList fvs)
mids <- do
res <- runExceptT $ inverseSubst args
case res of
Right ids -> do
reportSDoc "tc.meta.assign" 50 $
text "inverseSubst returns:" <+> sep (map prettyTCM ids)
return $ Just ids
Left CantInvert -> return Nothing
Left NeutralArg -> Just <$> attemptPruning x args fvs
Left (ProjectedVar i qs) -> Just <$> attemptPruning x args fvs
case mids of
Nothing -> patternViolation
Just ids -> do
ids <- do
res <- runExceptT $ checkLinearity ids
case res of
Right ids -> return ids
Left () -> attemptPruning x args fvs
m <- getContextSize
assignMeta' m x t (length args) ids v
where
attemptPruning x args fvs = do
killResult <- prune x args $ Set.toList fvs
reportSDoc "tc.meta.assign" 10 $
text "pruning" <+> prettyTCM x <+> do
text $
if killResult `elem` [PrunedSomething,PrunedEverything] then "succeeded"
else "failed"
patternViolation
assignMeta :: Int -> MetaId -> Type -> [Int] -> Term -> TCM ()
assignMeta m x t ids v = do
let n = length ids
cand = List.sort $ zip ids $ map var $ downFrom n
assignMeta' m x t n cand v
assignMeta' :: Int -> MetaId -> Type -> Int -> SubstCand -> Term -> TCM ()
assignMeta' m x t n ids v = do
reportSDoc "tc.meta.assign" 25 $
text "preparing to instantiate: " <+> prettyTCM v
v' <- do
let assocToList i l = case l of
_ | i >= m -> []
((j,u) : l) | i == j -> Just u : assocToList (i+1) l
_ -> Nothing : assocToList (i+1) l
ivs = assocToList 0 ids
rho = prependS __IMPOSSIBLE__ ivs $ raiseS n
return $ applySubst rho v
inTopContext $ do
reportSDoc "tc.meta.assign" 15 $ text "type of meta =" <+> prettyTCM t
reportSDoc "tc.meta.assign" 70 $ text "type of meta =" <+> text (show t)
TelV tel' _ <- telViewUpTo n t
reportSDoc "tc.meta.assign" 30 $ text "tel' =" <+> prettyTCM tel'
reportSDoc "tc.meta.assign" 30 $ text "#args =" <+> text (show n)
when (size tel' < n)
patternViolation
reportSDoc "tc.meta.assign" 10 $
text "solving" <+> prettyTCM x <+> text ":=" <+> prettyTCM (abstract tel' v')
assignTerm x (telToArgs tel') v'
subtypingForSizeLt
:: CompareDirection
-> MetaId
-> MetaVariable
-> Type
-> Args
-> Term
-> (Term -> TCM ())
-> TCM ()
subtypingForSizeLt DirEq x mvar t args v cont = cont v
subtypingForSizeLt dir x mvar t args v cont = do
let fallback = cont v
(mSize, mSizeLt) <- getBuiltinSize
caseMaybe mSize fallback $ \ qSize -> do
caseMaybe mSizeLt fallback $ \ qSizeLt -> do
v <- reduce v
case ignoreSharing v of
Def q [Apply (Arg ai u)] | q == qSizeLt -> do
TelV tel _ <- telView t
let size = sizeType_ qSize
t' = telePi tel size
y <- newMeta (mvInfo mvar) (mvPriority mvar) (mvPermutation mvar)
(HasType __IMPOSSIBLE__ t')
let yArgs = MetaV y $ map Apply args
addConstraint $ dirToCmp (`ValueCmp` size) dir yArgs u
let xArgs = MetaV x $ map Apply args
v' = Def qSizeLt [Apply $ Arg ai yArgs]
c = dirToCmp (`ValueCmp` sizeUniv) dir xArgs v'
catchConstraint c $ cont v'
_ -> fallback
expandProjectedVars :: (Normalise a, TermLike a, Show a, PrettyTCM a, NoProjectedVar a, Subst a, PrettyTCM b, Subst b) =>
a -> b -> (a -> b -> TCM c) -> TCM c
expandProjectedVars args v ret = loop (args, v) where
loop (args, v) = do
reportSDoc "tc.meta.assign.proj" 45 $ text "meta args: " <+> prettyTCM args
args <- etaContract =<< normalise args
reportSDoc "tc.meta.assign.proj" 45 $ text "norm args: " <+> prettyTCM args
reportSDoc "tc.meta.assign.proj" 85 $ text "norm args: " <+> text (show args)
let done = ret args v
case noProjectedVar args of
Right () -> do
reportSDoc "tc.meta.assign.proj" 40 $
text "no projected var found in args: " <+> prettyTCM args
done
Left (ProjVarExc i _) -> etaExpandProjectedVar i (args, v) done loop
etaExpandProjectedVar :: (PrettyTCM a, Subst a) => Int -> a -> TCM c -> (a -> TCM c) -> TCM c
etaExpandProjectedVar i v fail succeed = do
reportSDoc "tc.meta.assign.proj" 40 $
text "trying to expand projected variable" <+> prettyTCM (var i)
caseMaybeM (etaExpandBoundVar i) fail $ \ (delta, sigma, tau) -> do
reportSDoc "tc.meta.assign.proj" 25 $
text "eta-expanding var " <+> prettyTCM (var i) <+>
text " in terms " <+> prettyTCM v
inTopContext $ addContext delta $
succeed $ applySubst tau v
class NoProjectedVar a where
noProjectedVar :: a -> Either ProjVarExc ()
data ProjVarExc = ProjVarExc Int [QName]
instance NoProjectedVar Term where
noProjectedVar t =
case ignoreSharing t of
Var i es
| qs@(_:_) <- takeWhileJust id $ map isProjElim es -> Left $ ProjVarExc i qs
Con (ConHead _ Inductive (_:_)) vs -> noProjectedVar vs
_ -> return ()
instance NoProjectedVar a => NoProjectedVar (I.Arg a) where
noProjectedVar = Fold.mapM_ noProjectedVar
instance NoProjectedVar a => NoProjectedVar [a] where
noProjectedVar = Fold.mapM_ noProjectedVar
type FVs = Set.VarSet
type SubstCand = [(Nat,Term)]
checkLinearity :: SubstCand -> ExceptT () TCM SubstCand
checkLinearity ids0 = do
let ids = sortBy (compare `on` fst) ids0
let grps = groupOn fst ids
concat <$> mapM makeLinear grps
where
makeLinear :: SubstCand -> ExceptT () TCM SubstCand
makeLinear [] = __IMPOSSIBLE__
makeLinear grp@[_] = return grp
makeLinear (p@(i,t) : _) =
ifM ((Right True ==) <$> do isSingletonTypeModuloRelevance =<< typeOfBV i)
(return [p])
(throwError ())
type Res = [(I.Arg Nat, Term)]
data InvertExcept
= CantInvert
| NeutralArg
| ProjectedVar Int [QName]
#if !MIN_VERSION_transformers(0,4,1)
instance Error InvertExcept where
noMsg = CantInvert
#endif
inverseSubst :: Args -> ExceptT InvertExcept TCM SubstCand
inverseSubst args = map (mapFst unArg) <$> loop (zip args terms)
where
loop = foldM isVarOrIrrelevant []
terms = map var (downFrom (size args))
failure = do
lift $ reportSDoc "tc.meta.assign" 15 $ vcat
[ text "not all arguments are variables: " <+> prettyTCM args
, text " aborting assignment" ]
throwError CantInvert
neutralArg = throwError NeutralArg
isVarOrIrrelevant :: Res -> (I.Arg Term, Term) -> ExceptT InvertExcept TCM Res
isVarOrIrrelevant vars (arg, t) =
case ignoreSharing <$> arg of
Arg info (Var i []) -> return $ (Arg info i, t) `cons` vars
Arg _ (Var i es) | Just qs <- mapM isProjElim es ->
throwError $ ProjectedVar i qs
Arg info (Con c vs) -> do
let fallback
| irrelevantOrUnused (getRelevance info) = return vars
| otherwise = failure
isRC <- lift $ isRecordConstructor $ conName c
case isRC of
Just (_, Record{ recFields = fs })
| length fs == length vs -> do
let aux (Arg _ v) (Arg info' f) = (Arg ai v,) $ t `applyE` [Proj f] where
ai = ArgInfo
{ argInfoColors = argInfoColors info
, argInfoHiding = min (getHiding info) (getHiding info')
, argInfoRelevance = max (getRelevance info) (getRelevance info')
}
res <- loop $ zipWith aux vs fs
return $ res `append` vars
| otherwise -> fallback
Just _ -> __IMPOSSIBLE__
Nothing -> fallback
Arg info _ | irrelevantOrUnused (getRelevance info) -> return vars
Arg _ DontCare{} -> return vars
Arg _ Var{} -> neutralArg
Arg _ Def{} -> neutralArg
Arg _ Lam{} -> failure
Arg _ Lit{} -> failure
Arg _ MetaV{} -> failure
Arg _ Pi{} -> neutralArg
Arg _ Sort{} -> neutralArg
Arg _ Level{} -> neutralArg
Arg _ ExtLam{} -> __IMPOSSIBLE__
Arg info (Shared p) -> isVarOrIrrelevant vars (Arg info $ derefPtr p, t)
append :: Res -> Res -> Res
append res vars = foldr cons vars res
cons :: (I.Arg Nat, Term) -> Res -> Res
cons a@(Arg (ArgInfo _ Irrelevant _) i, t) vars
| any ((i==) . unArg . fst) vars = vars
| otherwise = a : vars
cons a@(Arg info i, t) vars = a :
filter (not . (\ a@(Arg info j, t) -> isIrrelevant info && i == j)) vars
updateMeta :: MetaId -> Term -> TCM ()
updateMeta mI v = do
mv <- lookupMeta mI
withMetaInfo' mv $ do
args <- getContextArgs
noConstraints $ assignV DirEq mI args v
allMetas :: TermLike a => a -> [MetaId]
allMetas = foldTerm metas
where
metas (MetaV m _) = [m]
metas _ = []