- modifyOccursCheckDefs :: (Set QName -> Set QName) -> TCM ()
- initOccursCheck :: MetaVariable -> TCM ()
- defNeedsChecking :: QName -> TCM Bool
- tallyDef :: QName -> TCM ()
- data OccursCtx
- data UnfoldStrategy
- defArgs :: UnfoldStrategy -> OccursCtx -> OccursCtx
- unfold :: UnfoldStrategy -> Term -> TCM (Blocked Term)
- leaveTop :: OccursCtx -> OccursCtx
- weakly :: OccursCtx -> OccursCtx
- strongly :: OccursCtx -> OccursCtx
- abort :: OccursCtx -> TypeError -> TCM a
- type Vars = ([Nat], [Nat])
- goIrrelevant :: Vars -> Vars
- allowedVar :: Nat -> Vars -> Bool
- takeRelevant :: Vars -> [Nat]
- liftUnderAbs :: Vars -> Vars
- class Occurs t where
- occursCheck :: MetaId -> Vars -> Term -> TCM Term
- prune :: MetaId -> Args -> [Nat] -> TCM PruneResult
- hasBadRigid :: [Nat] -> Term -> TCM Bool
- rigidVarsNotContainedIn :: Free a => a -> [Nat] -> Bool
- data PruneResult
- killArgs :: [Bool] -> MetaId -> TCM PruneResult
- killedType :: [(Dom (String, Type), Bool)] -> Type -> ([Arg Bool], Type)
- performKill :: [Arg Bool] -> MetaId -> Type -> TCM ()
Set the names of definitions to be looked at to the defs in the current mutual block.
we are in arguments of a meta
we are not in arguments of a meta but a bound var
we are at the start or in the arguments of a constructor
we are at the term root (this turns into
we are in an irrelevant argument
Extended occurs check.
m xs := v, check that
m does not occur in
and that the free variables of
v are contained in
Getting rid of flexible occurrences
prune m' vs xs attempts to remove all arguments from
free variables are not contained in
m' is solved by the new, pruned meta variable and we
hasBadRigid xs v = True iff one of the rigid variables in
v is not in
Actually we can only prune if a bad variable is in the head. See issue 458.
Or in a non-eliminateable position (see succeed/PruningNonMillerPattern).
the kill list is empty or only
there is no possible kill (because of type dep.)
managed to kill some args in the list
all prescribed kills where performed
killArgs [k1,...,kn] X prunes argument
i from metavar
Pruning is carried out whenever > 0 arguments can be pruned.
True is only returned if all arguments could be pruned.
killedType [((x1,a1),k1)..((xn,an),kn)] b = ([k'1..k'n],t')
t' = (xs:as) -> b.
k'i == True iff
ki == True and pruning the
ith argument from
b is possible without creating unbound variables.
t' is type
t after pruning all