Agda.TypeChecking.MetaVars.Occurs

The occurs check for unification. Does pruning on the fly.

When hitting a meta variable:

• Compute flex/rigid for its arguments.
• Compare to allowed variables.
• Mark arguments with rigid occurrences of disallowed variables for deletion.
• Attempt to delete marked arguments.
• We don't need to check for success, we can just continue occurs checking.

Documentation

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

initOccursCheck :: MetaVariable -> TCM ()

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

defNeedsChecking :: QName -> TCM Bool

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

tallyDef :: QName -> TCM ()

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

data OccursCtx

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

Methods

(==) :: OccursCtx -> OccursCtx -> Bool

(/=) :: OccursCtx -> OccursCtx -> Bool

Show OccursCtx

Methods

showsPrec :: Int -> OccursCtx -> ShowS

show :: OccursCtx -> String

showList :: [OccursCtx] -> ShowS

data UnfoldStrategy

Constructors

YesUnfold

NoUnfold

Instances

Eq UnfoldStrategy

Methods

(==) :: UnfoldStrategy -> UnfoldStrategy -> Bool

(/=) :: UnfoldStrategy -> UnfoldStrategy -> Bool

Show UnfoldStrategy

Methods

showsPrec :: Int -> UnfoldStrategy -> ShowS

show :: UnfoldStrategy -> String

showList :: [UnfoldStrategy] -> ShowS

defArgs :: UnfoldStrategy -> OccursCtx -> OccursCtx

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

leaveTop :: OccursCtx -> OccursCtx

Leave the top position.

weakly :: OccursCtx -> OccursCtx

Leave the strongly rigid position.

strongly :: OccursCtx -> OccursCtx

patternViolation' :: Int -> String -> TCM a

abort :: OccursCtx -> TypeError -> TCM a

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

Distinguish relevant and irrelevant variables in occurs check.

goIrrelevant :: Vars -> Vars

allowedVar :: Nat -> Vars -> Bool

takeRelevant :: Vars -> [Nat]

liftUnderAbs :: Vars -> Vars

class Occurs t where

Extended occurs check.

Minimal complete definition

occurs, metaOccurs

Methods

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

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

Instances

Occurs QName

Methods

occurs :: UnfoldStrategy -> OccursCtx -> MetaId -> Vars -> QName -> TCM QName

metaOccurs :: MetaId -> QName -> TCM ()

Occurs Clause

Methods

occurs :: UnfoldStrategy -> OccursCtx -> MetaId -> Vars -> Clause -> TCM Clause

metaOccurs :: MetaId -> Clause -> TCM ()

Occurs LevelAtom

Methods

occurs :: UnfoldStrategy -> OccursCtx -> MetaId -> Vars -> LevelAtom -> TCM LevelAtom

metaOccurs :: MetaId -> LevelAtom -> TCM ()

Occurs PlusLevel

Methods

occurs :: UnfoldStrategy -> OccursCtx -> MetaId -> Vars -> PlusLevel -> TCM PlusLevel

metaOccurs :: MetaId -> PlusLevel -> TCM ()

Occurs Level

Methods

occurs :: UnfoldStrategy -> OccursCtx -> MetaId -> Vars -> Level -> TCM Level

metaOccurs :: MetaId -> Level -> TCM ()

Occurs Sort

Methods

occurs :: UnfoldStrategy -> OccursCtx -> MetaId -> Vars -> Sort -> TCM Sort

metaOccurs :: MetaId -> Sort -> TCM ()

Occurs Type

Methods

occurs :: UnfoldStrategy -> OccursCtx -> MetaId -> Vars -> Type -> TCM Type

metaOccurs :: MetaId -> Type -> TCM ()

Occurs Term

Methods

occurs :: UnfoldStrategy -> OccursCtx -> MetaId -> Vars -> Term -> TCM Term

metaOccurs :: MetaId -> Term -> TCM ()

Occurs Defn

Methods

occurs :: UnfoldStrategy -> OccursCtx -> MetaId -> Vars -> Defn -> TCM Defn

metaOccurs :: MetaId -> Defn -> TCM ()

Occurs a => Occurs [a]

Methods

occurs :: UnfoldStrategy -> OccursCtx -> MetaId -> Vars -> [a] -> TCM [a]

metaOccurs :: MetaId -> [a] -> TCM ()

Occurs a => Occurs (Maybe a)

Methods

occurs :: UnfoldStrategy -> OccursCtx -> MetaId -> Vars -> Maybe a -> TCM (Maybe a)

metaOccurs :: MetaId -> Maybe a -> TCM ()

Occurs a => Occurs (Dom a)

Methods

occurs :: UnfoldStrategy -> OccursCtx -> MetaId -> Vars -> Dom a -> TCM (Dom a)

metaOccurs :: MetaId -> Dom a -> TCM ()

Occurs a => Occurs (Arg a)

Methods

occurs :: UnfoldStrategy -> OccursCtx -> MetaId -> Vars -> Arg a -> TCM (Arg a)

metaOccurs :: MetaId -> Arg a -> TCM ()

(Occurs a, Subst t a) => Occurs (Abs a)

Methods

occurs :: UnfoldStrategy -> OccursCtx -> MetaId -> Vars -> Abs a -> TCM (Abs a)

metaOccurs :: MetaId -> Abs a -> TCM ()

Occurs a => Occurs (Elim' a)

Methods

occurs :: UnfoldStrategy -> OccursCtx -> MetaId -> Vars -> Elim' a -> TCM (Elim' a)

metaOccurs :: MetaId -> Elim' a -> TCM ()

(Occurs a, Occurs b) => Occurs (a, b)

Methods

occurs :: UnfoldStrategy -> OccursCtx -> MetaId -> Vars -> (a, b) -> TCM (a, b)

metaOccurs :: MetaId -> (a, b) -> TCM ()

occursCheck :: (Occurs a, InstantiateFull a, PrettyTCM a) => MetaId -> Vars -> a -> TCM a

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

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.

Issue 1147: If any of the meta args vs is matchable, e.g., is a constructor term, we cannot prune, because the offending variables could be removed by reduction for a suitable instantiation of the meta variable.

hasBadRigid :: [Nat] -> Term -> ExceptT () TCM Bool

hasBadRigid xs v = Just 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).

hasBadRigid xs v = Nothing means that we cannot prune at all as one of the meta args is matchable. (See issue 1147.)

isNeutral :: MonadTCM tcm => Blocked t -> QName -> Elims -> tcm Bool

Check whether a term Def f es is finally stuck. Currently, we give only a crude approximation.

rigidVarsNotContainedIn :: (MonadTCM tcm, FoldRigid a) => a -> [Nat] -> tcm Bool

Check whether any of the variables (given as de Bruijn indices) occurs *definitely* in the term in a rigid position. Reduces the term successively to remove variables in dead subterms. This fixes issue 1386.

class FoldRigid a where

Collect the *definitely* rigid variables in a monoid. We need to successively reduce the expression to do this.

Minimal complete definition

foldRigid

Methods

foldRigid :: Monoid (TCM m) => (Nat -> TCM m) -> a -> TCM m

Instances

FoldRigid LevelAtom

Methods

foldRigid :: Monoid (TCM m) => (Nat -> TCM m) -> LevelAtom -> TCM m

FoldRigid PlusLevel

Methods

foldRigid :: Monoid (TCM m) => (Nat -> TCM m) -> PlusLevel -> TCM m

FoldRigid Level

Methods

foldRigid :: Monoid (TCM m) => (Nat -> TCM m) -> Level -> TCM m

FoldRigid Sort

Methods

foldRigid :: Monoid (TCM m) => (Nat -> TCM m) -> Sort -> TCM m

FoldRigid Type

Methods

foldRigid :: Monoid (TCM m) => (Nat -> TCM m) -> Type -> TCM m

FoldRigid Term

Methods

foldRigid :: Monoid (TCM m) => (Nat -> TCM m) -> Term -> TCM m

FoldRigid a => FoldRigid [a]

Methods

foldRigid :: Monoid (TCM m) => (Nat -> TCM m) -> [a] -> TCM m

FoldRigid a => FoldRigid (Dom a)

Methods

foldRigid :: Monoid (TCM m) => (Nat -> TCM m) -> Dom a -> TCM m

FoldRigid a => FoldRigid (Arg a)

Methods

foldRigid :: Monoid (TCM m) => (Nat -> TCM m) -> Arg a -> TCM m

(Subst t a, FoldRigid a) => FoldRigid (Abs a)

Methods

foldRigid :: Monoid (TCM m) => (Nat -> TCM m) -> Abs a -> TCM m

FoldRigid a => FoldRigid (Elim' a)

Methods

foldRigid :: Monoid (TCM m) => (Nat -> TCM m) -> Elim' a -> TCM m

(FoldRigid a, FoldRigid b) => FoldRigid (a, b)

Methods

foldRigid :: Monoid (TCM m) => (Nat -> TCM m) -> (a, b) -> TCM m

data PruneResult

Constructors

NothingToPrune

the kill list is empty or only Falses

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

Methods

(==) :: PruneResult -> PruneResult -> Bool

(/=) :: PruneResult -> PruneResult -> Bool

Show PruneResult

Methods

showsPrec :: Int -> PruneResult -> ShowS

show :: PruneResult -> String

showList :: [PruneResult] -> ShowS

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

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

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

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

Arguments

:: [Arg Bool]

Arguments to old meta var in left to right order with Bool indicating whether they can be pruned.

-> MetaId

The old meta var to receive pruning.

-> Type

The pruned type of the new meta var.

-> TCM ()

Instantiate a meta variable with a new one that only takes the arguments which are not pruneable.