Agda- A dependently typed functional programming language and proof assistant

Safe HaskellNone





initOccursCheck :: MetaVariable -> TCM ()Source

Set the names of definitions to be looked at to the defs in the current mutual block.

defNeedsChecking :: QName -> TCM BoolSource

Is a def in the list of stuff to be checked?

tallyDef :: QName -> TCM ()Source

Remove a def from the list of defs to be looked at.

data OccursCtx Source



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 StronglyRigid)


we are in an irrelevant argument

leaveTop :: OccursCtx -> OccursCtxSource

Leave the top position.

weakly :: OccursCtx -> OccursCtxSource

Leave the strongly rigid position.

type Vars = ([Nat], [Nat])Source

Distinguish relevant and irrelevant variables in occurs check.

class Occurs t whereSource

Extended occurs check.


occurs :: UnfoldStrategy -> OccursCtx -> MetaId -> Vars -> t -> TCM tSource

metaOccurs :: MetaId -> t -> TCM ()Source

occursCheck :: MetaId -> Vars -> Term -> TCM TermSource

When assigning m xs := v, check that m does not occur in v and that the free variables of v are contained in xs.

Getting rid of flexible occurrences

prune :: MetaId -> Args -> [Nat] -> TCM PruneResultSource

prune m' vs xs attempts to remove all arguments from vs whose free variables are not contained in xs. If successful, m' is solved by the new, pruned meta variable and we return True else False.

hasBadRigid :: [Nat] -> Term -> TCM BoolSource

hasBadRigid xs v = True iff one of the rigid variables in v is not in xs. 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).

data PruneResult Source



the kill list is empty or only Falses


there is no possible kill (because of type dep.)


managed to kill some args in the list


all prescribed kills where performed

killArgs :: [Bool] -> MetaId -> TCM PruneResultSource

killArgs [k1,...,kn] X prunes argument i from metavar X if ki==True. Pruning is carried out whenever > 0 arguments can be pruned. True is only returned if all arguments could be pruned.

killedType :: [(Dom (String, Type), Bool)] -> Type -> ([Arg Bool], Type)Source

killedType [((x1,a1),k1)..((xn,an),kn)] b = ([k'1..k'n],t') (ignoring Dom). Let t' = (xs:as) -> b. Invariant: k'i == True iff ki == True and pruning the ith argument from type b is possible without creating unbound variables. t' is type t after pruning all k'i==True.