Agda-2.3.0.1: A dependently typed functional programming language and proof assistant

Safe HaskellSafe-Infered

Agda.TypeChecking.MetaVars.Occurs

Contents

Synopsis

Documentation

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

Irrel

we are in an irrelevant argument

weakly :: OccursCtx -> OccursCtx

Leave the strongly rigid position.

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

Distinguish relevant and irrelevant variables in occurs check.

class Occurs t where

Extended occurs check.

Methods

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

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

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.

hasBadRigid :: [Nat] -> Term -> Bool

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.

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

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. True is only returned if all arguments could be pruned.

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

killedType [((x1,a1),k1)..((xn,an),kn)] b = ([k'1..k'n],t') (ignoring Arg). 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.