Safe Haskell	None

Agda.TypeChecking.MetaVars.Occurs

Contents

Getting rid of flexible occurrences

Synopsis

Documentation

modifyOccursCheckDefs :: (Set QName -> Set QName) -> TCM ()Source

initOccursCheck :: MetaVariable -> TCM ()Source

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

defNeedsChecking :: QName -> TCM Bool Source

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

Constructors

Flex	we are in arguments of a meta
Rigid	we are not in arguments of a meta but a bound var
StronglyRigid	we are at the start or in the arguments of a constructor
Top	we are at the term root (this turns into `StronglyRigid`)
Irrel	we are in an irrelevant argument

Instances

Eq OccursCtx
Show OccursCtx

data UnfoldStrategy Source

Constructors

YesUnfold
NoUnfold

Instances

Eq UnfoldStrategy
Show UnfoldStrategy

defArgs :: UnfoldStrategy -> OccursCtx -> OccursCtx Source

unfold :: UnfoldStrategy -> Term -> TCM (Blocked Term)Source

leaveTop :: OccursCtx -> OccursCtx Source

Leave the top position.

weakly :: OccursCtx -> OccursCtx Source

Leave the strongly rigid position.

strongly :: OccursCtx -> OccursCtx Source

abort :: OccursCtx -> TypeError -> TCM aSource

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

Distinguish relevant and irrelevant variables in occurs check.

goIrrelevant :: Vars -> Vars Source

allowedVar :: Nat -> Vars -> Bool Source

takeRelevant :: Vars -> [Nat]Source

liftUnderAbs :: Vars -> Vars Source

class Occurs t whereSource

Extended occurs check.

Methods

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

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

Instances

Occurs QName
Occurs Clause
Occurs LevelAtom
Occurs PlusLevel
Occurs Level
Occurs Sort
Occurs Type
Occurs Term
Occurs Defn
Occurs a => Occurs [a]
Occurs a => Occurs (Arg a)
Occurs a => Occurs (Dom a)
(Occurs a, Subst a) => Occurs (Abs a)
(Occurs a, Occurs b) => Occurs (a, b)

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

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 PruneResult Source

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 Bool Source

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

rigidVarsNotContainedIn :: Free a => a -> [Nat] -> Bool Source

data PruneResult Source

Constructors

NothingToPrune	the kill list is empty or only `False`s
PrunedNothing	there is no possible kill (because of type dep.)
PrunedSomething	managed to kill some args in the list
PrunedEverything	all prescribed kills where performed

Instances

Eq PruneResult
Show PruneResult

killArgs :: [Bool] -> MetaId -> TCM PruneResult Source

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.

performKill :: [Arg Bool] -> MetaId -> Type -> TCM ()Source