Agda.TypeChecking.Free.Lazy

Computing the free variables of a term lazily.

We implement a reduce (traversal into monoid) over internal syntax for a generic collection (monoid with singletons). This should allow a more efficient test for the presence of a particular variable.

Worst-case complexity does not change (i.e. the case when a variable does not occur), but best case-complexity does matter. For instance, see mkAbs: each time we construct a dependent function type, we check whether it is actually dependent.

The distinction between rigid and strongly rigid occurrences comes from: Jason C. Reed, PhD thesis, 2009, page 96 (see also his LFMTP 2009 paper)

The main idea is that x = t(x) is unsolvable if x occurs strongly rigidly in t. It might have a solution if the occurrence is not strongly rigid, e.g.

x = f -> suc (f (x ( y -> k))) has x = f -> suc (f (suc k))

Jason C. Reed, PhD thesis, page 106

Under coinductive constructors, occurrences are never strongly rigid. Also, function types and lambdas do not establish strong rigidity. Only inductive constructors do so. (See issue 1271).

For further reading on semirings and semimodules for variable occurrence, see e.g. Conor McBrides "I got plenty of nuttin'" (Wadlerfest 2016). There, he treats the "quantity" dimension of variable occurrences.

The semiring has an additive operation for combining occurrences of subterms, and a multiplicative operation of representing function composition. E.g. if variable x appears o in term u, but u appears in context q in term t then occurrence of variable x coming from u is accounted for as q o in t.

Consider example (λ{ x → (x,x)}) y:

• Variable x occurs once unguarded in x.
• It occurs twice unguarded in the aggregation x x
• Inductive constructor , turns this into two strictly rigid occurrences.

If , is a record constructor, then we stay unguarded.

• The function ({λ x → (x,x)}) provides a context for variable y. This context can be described as weakly rigid with quantity two.
• The final occurrence of y is obtained as composing the context with the occurrence of y in itself (which is the unit for composition). Thus, y occurs weakly rigid with quantity two.

It is not a given that the context can be described in the same way as the variable occurrence. However, for quantity it is the case and we obtain a semiring of occurrences with 0, 1, and even ω, which is an absorptive element for addition.

Set of meta variables.

newtype MetaSet

A set of meta variables. Forms a monoid under union.

Constructors

MetaSet

Fields

• theMetaSet :: HashSet MetaId

Instances

Null MetaSet

Defined in Agda.TypeChecking.Free.Lazy

Methods

empty :: MetaSet

null :: MetaSet -> Bool

Monoid MetaSet

Defined in Agda.TypeChecking.Free.Lazy

Methods

mempty :: MetaSet

mappend :: MetaSet -> MetaSet -> MetaSet

mconcat :: [MetaSet] -> MetaSet

Semigroup MetaSet

Defined in Agda.TypeChecking.Free.Lazy

Methods

(<>) :: MetaSet -> MetaSet -> MetaSet

sconcat :: NonEmpty MetaSet -> MetaSet

stimes :: Integral b => b -> MetaSet -> MetaSet

Show MetaSet

Defined in Agda.TypeChecking.Free.Lazy

Methods

showsPrec :: Int -> MetaSet -> ShowS

show :: MetaSet -> String

showList :: [MetaSet] -> ShowS

Eq MetaSet

Defined in Agda.TypeChecking.Free.Lazy

Methods

(==) :: MetaSet -> MetaSet -> Bool

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

Singleton MetaId MetaSet

Defined in Agda.TypeChecking.Free.Lazy

Methods

singleton :: MetaId -> MetaSet

insertMetaSet :: MetaId -> MetaSet -> MetaSet

foldrMetaSet :: (MetaId -> a -> a) -> a -> MetaSet -> a

metaSetToBlocker :: MetaSet -> Blocker

Flexible and rigid occurrences (semigroup)

data FlexRig' a

Depending on the surrounding context of a variable, it's occurrence can be classified as flexible or rigid, with finer distinctions.

The constructors are listed in increasing order (wrt. information content).

Constructors

Flexible a

In arguments of metas. The set of metas is used by 'NonLinMatch' to generate the right blocking information. The semantics is that the status of a variable occurrence may change if one of the metas in the set gets solved. We may say the occurrence is tainted by the meta variables in the set.

WeaklyRigid

In arguments to variables and definitions.

Unguarded

In top position, or only under inductive record constructors (unit).

StronglyRigid

Under at least one and only inductive constructors.

Instances

Foldable FlexRig'

Defined in Agda.TypeChecking.Free.Lazy

Methods

fold :: Monoid m => FlexRig' m -> m

foldMap :: Monoid m => (a -> m) -> FlexRig' a -> m

foldMap' :: Monoid m => (a -> m) -> FlexRig' a -> m

foldr :: (a -> b -> b) -> b -> FlexRig' a -> b

foldr' :: (a -> b -> b) -> b -> FlexRig' a -> b

foldl :: (b -> a -> b) -> b -> FlexRig' a -> b

foldl' :: (b -> a -> b) -> b -> FlexRig' a -> b

foldr1 :: (a -> a -> a) -> FlexRig' a -> a

foldl1 :: (a -> a -> a) -> FlexRig' a -> a

toList :: FlexRig' a -> [a]

null :: FlexRig' a -> Bool

length :: FlexRig' a -> Int

elem :: Eq a => a -> FlexRig' a -> Bool

maximum :: Ord a => FlexRig' a -> a

minimum :: Ord a => FlexRig' a -> a

sum :: Num a => FlexRig' a -> a

product :: Num a => FlexRig' a -> a

Functor FlexRig'

Defined in Agda.TypeChecking.Free.Lazy

Methods

fmap :: (a -> b) -> FlexRig' a -> FlexRig' b

(<$) :: a -> FlexRig' b -> FlexRig' a

Show a => Show (FlexRig' a)

Defined in Agda.TypeChecking.Free.Lazy

Methods

showsPrec :: Int -> FlexRig' a -> ShowS

show :: FlexRig' a -> String

showList :: [FlexRig' a] -> ShowS

Eq a => Eq (FlexRig' a)

Defined in Agda.TypeChecking.Free.Lazy

Methods

(==) :: FlexRig' a -> FlexRig' a -> Bool

(/=) :: FlexRig' a -> FlexRig' a -> Bool

LensFlexRig (FlexRig' a) a

Defined in Agda.TypeChecking.Free.Lazy

Methods

lensFlexRig :: Lens' (FlexRig' a) (FlexRig' a)

Singleton (Variable, FlexRig' ()) FlexRigMap

Defined in Agda.TypeChecking.Free.Lazy

Methods

singleton :: (Variable, FlexRig' ()) -> FlexRigMap

type FlexRig = FlexRig' MetaSet

class LensFlexRig o a | o -> a where

Methods

lensFlexRig :: Lens' o (FlexRig' a)

Instances

LensFlexRig (FlexRig' a) a

Defined in Agda.TypeChecking.Free.Lazy

Methods

lensFlexRig :: Lens' (FlexRig' a) (FlexRig' a)

LensFlexRig (VarOcc' a) a

Access to varFlexRig in VarOcc'.

Defined in Agda.TypeChecking.Free.Lazy

Methods

lensFlexRig :: Lens' (VarOcc' a) (FlexRig' a)

LensFlexRig (FreeEnv' a b c) a

Defined in Agda.TypeChecking.Free.Lazy

Methods

lensFlexRig :: Lens' (FreeEnv' a b c) (FlexRig' a)

isFlexible :: LensFlexRig o a => o -> Bool

isUnguarded :: LensFlexRig o a => o -> Bool

isWeaklyRigid :: LensFlexRig o a => o -> Bool

isStronglyRigid :: LensFlexRig o a => o -> Bool

addFlexRig :: Semigroup a => FlexRig' a -> FlexRig' a -> FlexRig' a

FlexRig aggregation (additive operation of the semiring). For combining occurrences of the same variable in subterms. This is a refinement of the max operation for FlexRig which would work if Flexible did not have the MetaSet as an argument. Now, to aggregate two Flexible occurrences, we union the involved MetaSets.

zeroFlexRig :: Monoid a => FlexRig' a

Unit for addFlexRig.

omegaFlexRig :: FlexRig' a

Absorptive for addFlexRig.

composeFlexRig :: Semigroup a => FlexRig' a -> FlexRig' a -> FlexRig' a

FlexRig composition (multiplicative operation of the semiring). For accumulating the context of a variable.

Flexible is dominant. Once we are under a meta, we are flexible regardless what else comes. We taint all variable occurrences under a meta by this meta.

WeaklyRigid is next in strength. Destroys strong rigidity.

StronglyRigid is still dominant over Unguarded.

Unguarded is the unit. It is the top (identity) context.

oneFlexRig :: FlexRig' a

Unit for composeFlexRig.

Multi-dimensional feature vector for variable occurrence (semigroup)

data VarOcc' a

Occurrence of free variables is classified by several dimensions. Currently, we have FlexRig and Modality.

Constructors

VarOcc

Fields

• varFlexRig :: FlexRig' a
• varModality :: Modality

Instances

LensModality (VarOcc' a)

Defined in Agda.TypeChecking.Free.Lazy

Methods

getModality :: VarOcc' a -> Modality

setModality :: Modality -> VarOcc' a -> VarOcc' a

mapModality :: (Modality -> Modality) -> VarOcc' a -> VarOcc' a

LensQuantity (VarOcc' a)

Defined in Agda.TypeChecking.Free.Lazy

Methods

getQuantity :: VarOcc' a -> Quantity

setQuantity :: Quantity -> VarOcc' a -> VarOcc' a

mapQuantity :: (Quantity -> Quantity) -> VarOcc' a -> VarOcc' a

LensRelevance (VarOcc' a)

Defined in Agda.TypeChecking.Free.Lazy

Methods

getRelevance :: VarOcc' a -> Relevance

setRelevance :: Relevance -> VarOcc' a -> VarOcc' a

mapRelevance :: (Relevance -> Relevance) -> VarOcc' a -> VarOcc' a

(Semigroup a, Monoid a) => Monoid (VarOcc' a)

The neutral element for variable occurrence aggregation is least serious occurrence: flexible, irrelevant. This is also the absorptive element for composeVarOcc, if we ignore the MetaSet in Flexible.

Defined in Agda.TypeChecking.Free.Lazy

Methods

mempty :: VarOcc' a

mappend :: VarOcc' a -> VarOcc' a -> VarOcc' a

mconcat :: [VarOcc' a] -> VarOcc' a

Semigroup a => Semigroup (VarOcc' a)

The default way of aggregating free variable info from subterms is by adding the variable occurrences. For instance, if we have a pair (t₁,t₂) then and t₁ has o₁ the occurrences of a variable x and t₂ has o₂ the occurrences of the same variable, then (t₁,t₂) has mappend o₁ o₂ occurrences of that variable.

From counting Quantity, we extrapolate this to FlexRig and Relevance: we care most about about StronglyRigid Relevant occurrences. E.g., if t₁ has a StronglyRigid occurrence and t₂ a Flexible occurrence, then (t₁,t₂) still has a StronglyRigid occurrence. Analogously, Relevant occurrences count most, as we wish e.g. to forbid relevant occurrences of variables that are declared to be irrelevant.

VarOcc' forms a semiring, and this monoid is the addition of the semiring.

Defined in Agda.TypeChecking.Free.Lazy

Methods

(<>) :: VarOcc' a -> VarOcc' a -> VarOcc' a

sconcat :: NonEmpty (VarOcc' a) -> VarOcc' a

stimes :: Integral b => b -> VarOcc' a -> VarOcc' a

Show a => Show (VarOcc' a)

Defined in Agda.TypeChecking.Free.Lazy

Methods

showsPrec :: Int -> VarOcc' a -> ShowS

show :: VarOcc' a -> String

showList :: [VarOcc' a] -> ShowS

Eq a => Eq (VarOcc' a)

Equality up to origin.

Defined in Agda.TypeChecking.Free.Lazy

Methods

(==) :: VarOcc' a -> VarOcc' a -> Bool

(/=) :: VarOcc' a -> VarOcc' a -> Bool

LensFlexRig (VarOcc' a) a

Access to varFlexRig in VarOcc'.

Defined in Agda.TypeChecking.Free.Lazy

Methods

lensFlexRig :: Lens' (VarOcc' a) (FlexRig' a)

type VarOcc = VarOcc' MetaSet

topVarOcc :: VarOcc' a

The absorptive element of variable occurrence under aggregation: strongly rigid, relevant.

composeVarOcc :: Semigroup a => VarOcc' a -> VarOcc' a -> VarOcc' a

First argument is the outer occurrence (context) and second is the inner. This multiplicative operation is to modify an occurrence under a context.

oneVarOcc :: VarOcc' a

Storing variable occurrences (semimodule).

class (Singleton MetaId a, Semigroup a, Monoid a, Semigroup c, Monoid c) => IsVarSet a c | c -> a where

Any representation c of a set of variables need to be able to be modified by a variable occurrence. This is to ensure that free variable analysis is compositional. For instance, it should be possible to compute `fv (v [u/x])` from `fv v` and `fv u`.

In algebraic terminology, a variable set a needs to be (almost) a left semimodule to the semiring VarOcc'.

Methods

withVarOcc :: VarOcc' a -> c -> c

Laws * Respects monoid operations: ``` withVarOcc o mempty == mempty withVarOcc o (x <> y) == withVarOcc o x <> withVarOcc o y ``` * Respects VarOcc composition: ``` withVarOcc oneVarOcc = id withVarOcc (composeVarOcc o1 o2) = withVarOcc o1 . withVarOcc o2 ``` * Respects VarOcc aggregation: ``` withVarOcc (o1 <> o2) x = withVarOcc o1 x <> withVarOcc o2 x ``` Since the corresponding unit law may fail, ``` withVarOcc mempty x = mempty ``` it is not quite a semimodule.

Instances

IsVarSet () VarCounts

Defined in Agda.TypeChecking.Free

Methods

withVarOcc :: VarOcc' () -> VarCounts -> VarCounts

IsVarSet () FlexRigMap

Compose everything with the varFlexRig part of the VarOcc'.

Defined in Agda.TypeChecking.Free.Lazy

Methods

withVarOcc :: VarOcc' () -> FlexRigMap -> FlexRigMap

IsVarSet () AllowedVar

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

withVarOcc :: VarOcc' () -> AllowedVar -> AllowedVar

IsVarSet () All

Defined in Agda.TypeChecking.Free

Methods

withVarOcc :: VarOcc' () -> All -> All

IsVarSet () Any

Defined in Agda.TypeChecking.Free

Methods

withVarOcc :: VarOcc' () -> Any -> Any

IsVarSet () [Int]

Defined in Agda.TypeChecking.Free

Methods

withVarOcc :: VarOcc' () -> [Int] -> [Int]

(Singleton MetaId a, Semigroup a, Monoid a) => IsVarSet a (VarMap' a)

Defined in Agda.TypeChecking.Free.Lazy

Methods

withVarOcc :: VarOcc' a -> VarMap' a -> VarMap' a

type TheVarMap' a = IntMap (VarOcc' a)

Representation of a variable set as map from de Bruijn indices to VarOcc'.

newtype VarMap' a

Constructors

VarMap

Fields

• theVarMap :: TheVarMap' a

Instances

(Singleton MetaId a, Semigroup a, Monoid a) => IsVarSet a (VarMap' a)

Defined in Agda.TypeChecking.Free.Lazy

Methods

withVarOcc :: VarOcc' a -> VarMap' a -> VarMap' a

Singleton Variable (VarMap' a)

A "set"-style Singleton instance with default/initial variable occurrence.

Defined in Agda.TypeChecking.Free.Lazy

Methods

singleton :: Variable -> VarMap' a

Semigroup a => Monoid (VarMap' a)

Defined in Agda.TypeChecking.Free.Lazy

Methods

mempty :: VarMap' a

mappend :: VarMap' a -> VarMap' a -> VarMap' a

mconcat :: [VarMap' a] -> VarMap' a

Semigroup a => Semigroup (VarMap' a)

Proper monoid instance for VarMap rather than inheriting the broken one from IntMap. We combine two occurrences of a variable using mappend.

Defined in Agda.TypeChecking.Free.Lazy

Methods

(<>) :: VarMap' a -> VarMap' a -> VarMap' a

sconcat :: NonEmpty (VarMap' a) -> VarMap' a

stimes :: Integral b => b -> VarMap' a -> VarMap' a

Show a => Show (VarMap' a)

Defined in Agda.TypeChecking.Free.Lazy

Methods

showsPrec :: Int -> VarMap' a -> ShowS

show :: VarMap' a -> String

showList :: [VarMap' a] -> ShowS

Eq a => Eq (VarMap' a)

Defined in Agda.TypeChecking.Free.Lazy

Methods

(==) :: VarMap' a -> VarMap' a -> Bool

(/=) :: VarMap' a -> VarMap' a -> Bool

type TheVarMap = TheVarMap' MetaSet

type VarMap = VarMap' MetaSet

mapVarMap :: (TheVarMap' a -> TheVarMap' b) -> VarMap' a -> VarMap' b

lookupVarMap :: Variable -> VarMap' a -> Maybe (VarOcc' a)

Simple flexible/rigid variable collection.

type TheFlexRigMap = IntMap (FlexRig' ())

Keep track of FlexRig for every variable, but forget the involved meta vars.

newtype FlexRigMap

Constructors

FlexRigMap

Fields

• theFlexRigMap :: TheFlexRigMap

Instances

Monoid FlexRigMap

Defined in Agda.TypeChecking.Free.Lazy

Methods

mempty :: FlexRigMap

mappend :: FlexRigMap -> FlexRigMap -> FlexRigMap

mconcat :: [FlexRigMap] -> FlexRigMap

Semigroup FlexRigMap

Defined in Agda.TypeChecking.Free.Lazy

Methods

(<>) :: FlexRigMap -> FlexRigMap -> FlexRigMap

sconcat :: NonEmpty FlexRigMap -> FlexRigMap

stimes :: Integral b => b -> FlexRigMap -> FlexRigMap

Show FlexRigMap

Defined in Agda.TypeChecking.Free.Lazy

Methods

showsPrec :: Int -> FlexRigMap -> ShowS

show :: FlexRigMap -> String

showList :: [FlexRigMap] -> ShowS

IsVarSet () FlexRigMap

Compose everything with the varFlexRig part of the VarOcc'.

Defined in Agda.TypeChecking.Free.Lazy

Methods

withVarOcc :: VarOcc' () -> FlexRigMap -> FlexRigMap

Singleton (Variable, FlexRig' ()) FlexRigMap

Defined in Agda.TypeChecking.Free.Lazy

Methods

singleton :: (Variable, FlexRig' ()) -> FlexRigMap

mapFlexRigMap :: (TheFlexRigMap -> TheFlexRigMap) -> FlexRigMap -> FlexRigMap

Environment for collecting free variables.

data IgnoreSorts

Where should we skip sorts in free variable analysis?

Constructors

IgnoreNot

Do not skip.

IgnoreInAnnotations

Skip when annotation to a type.

IgnoreAll

Skip unconditionally.

Instances

Show IgnoreSorts

Defined in Agda.TypeChecking.Free.Lazy

Methods

showsPrec :: Int -> IgnoreSorts -> ShowS

show :: IgnoreSorts -> String

showList :: [IgnoreSorts] -> ShowS

Eq IgnoreSorts

Defined in Agda.TypeChecking.Free.Lazy

Methods

(==) :: IgnoreSorts -> IgnoreSorts -> Bool

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

data FreeEnv' a b c

The current context.

Constructors

FreeEnv

Fields

• feExtra :: !b

  Additional context, e.g., whether to ignore free variables in sorts.

• feFlexRig :: !(FlexRig' a)

  Are we flexible or rigid?

• feModality :: !Modality

  What is the current relevance and quantity?

• feSingleton :: Maybe Variable -> c

  Method to return a single variable.

Instances

LensModality (FreeEnv' a b c)

Defined in Agda.TypeChecking.Free.Lazy

Methods

getModality :: FreeEnv' a b c -> Modality

setModality :: Modality -> FreeEnv' a b c -> FreeEnv' a b c

mapModality :: (Modality -> Modality) -> FreeEnv' a b c -> FreeEnv' a b c

LensQuantity (FreeEnv' a b c)

Defined in Agda.TypeChecking.Free.Lazy

Methods

getQuantity :: FreeEnv' a b c -> Quantity

setQuantity :: Quantity -> FreeEnv' a b c -> FreeEnv' a b c

mapQuantity :: (Quantity -> Quantity) -> FreeEnv' a b c -> FreeEnv' a b c

LensRelevance (FreeEnv' a b c)

Defined in Agda.TypeChecking.Free.Lazy

Methods

getRelevance :: FreeEnv' a b c -> Relevance

setRelevance :: Relevance -> FreeEnv' a b c -> FreeEnv' a b c

mapRelevance :: (Relevance -> Relevance) -> FreeEnv' a b c -> FreeEnv' a b c

LensFlexRig (FreeEnv' a b c) a

Defined in Agda.TypeChecking.Free.Lazy

Methods

lensFlexRig :: Lens' (FreeEnv' a b c) (FlexRig' a)

(Functor m, Applicative m, Monad m, Semigroup c, Monoid c) => Monoid (FreeT a b m c)

Defined in Agda.TypeChecking.Free.Lazy

Methods

mempty :: FreeT a b m c

mappend :: FreeT a b m c -> FreeT a b m c -> FreeT a b m c

mconcat :: [FreeT a b m c] -> FreeT a b m c

type Variable = Int

type SingleVar c = Variable -> c

type FreeEnv c = FreeEnv' MetaSet IgnoreSorts c

feIgnoreSorts :: FreeEnv' a IgnoreSorts c -> IgnoreSorts

Ignore free variables in sorts.

initFreeEnv :: Monoid c => b -> SingleVar c -> FreeEnv' a b c

The initial context.

type FreeT a b m c = ReaderT (FreeEnv' a b c) m c

type FreeM a c = Reader (FreeEnv' a IgnoreSorts c) c

runFreeM :: IsVarSet a c => SingleVar c -> IgnoreSorts -> FreeM a c -> c

Run function for FreeM.

variable :: (Monad m, IsVarSet a c) => Int -> FreeT a b m c

Base case: a variable.

subVar :: Int -> Maybe Variable -> Maybe Variable

Subtract, but return Nothing if result is negative.

underBinder :: MonadReader (FreeEnv' a b c) m => m z -> m z

Going under a binder.

underBinder' :: MonadReader (FreeEnv' a b c) m => Nat -> m z -> m z

Going under n binders.

underModality :: (MonadReader r m, LensModality r, LensModality o) => o -> m z -> m z

Changing the Modality.

underRelevance :: (MonadReader r m, LensRelevance r, LensRelevance o) => o -> m z -> m z

Changing the Relevance.

underQuantity :: (MonadReader r m, LensQuantity r, LensQuantity o) => o -> m a -> m a

In the given computation the Quantity is locally scaled using the Quantity of the first argument.

underFlexRig :: (MonadReader r m, LensFlexRig r a, Semigroup a, LensFlexRig o a) => o -> m z -> m z

Changing the FlexRig context.

underConstructor :: (MonadReader r m, LensFlexRig r a, Semigroup a) => ConHead -> Elims -> m z -> m z

What happens to the variables occurring under a constructor?

Recursively collecting free variables.

class Free t where

Gather free variables in a collection.

Minimal complete definition

Nothing

Methods

freeVars' :: IsVarSet a c => t -> FreeM a c

default freeVars' :: (t ~ f b, Foldable f, Free b) => IsVarSet a c => t -> FreeM a c

Instances

Free Clause

Defined in Agda.TypeChecking.Free.Lazy

Methods

freeVars' :: IsVarSet a c => Clause -> FreeM a c

Free EqualityView

Defined in Agda.TypeChecking.Free.Lazy

Methods

freeVars' :: IsVarSet a c => EqualityView -> FreeM a c

Free Level

Defined in Agda.TypeChecking.Free.Lazy

Methods

freeVars' :: IsVarSet a c => Level -> FreeM a c

Free Sort

Defined in Agda.TypeChecking.Free.Lazy

Methods

freeVars' :: IsVarSet a c => Sort -> FreeM a c

Free Term

Defined in Agda.TypeChecking.Free.Lazy

Methods

freeVars' :: IsVarSet a c => Term -> FreeM a c

Free Candidate

Defined in Agda.TypeChecking.Monad.Base

Methods

freeVars' :: IsVarSet a c => Candidate -> FreeM a c

Free CompareAs

Defined in Agda.TypeChecking.Monad.Base

Methods

freeVars' :: IsVarSet a c => CompareAs -> FreeM a c

Free Constraint

Defined in Agda.TypeChecking.Monad.Base

Methods

freeVars' :: IsVarSet a c => Constraint -> FreeM a c

Free DisplayForm

Defined in Agda.TypeChecking.Monad.Base

Methods

freeVars' :: IsVarSet a c => DisplayForm -> FreeM a c

Free DisplayTerm

Defined in Agda.TypeChecking.Monad.Base

Methods

freeVars' :: IsVarSet a c => DisplayTerm -> FreeM a c

Free NLPSort

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

freeVars' :: IsVarSet a c => NLPSort -> FreeM a c

Free NLPType

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

freeVars' :: IsVarSet a c => NLPType -> FreeM a c

Free NLPat

Only computes free variables that are not bound (see nlPatVars), i.e., those in a PTerm.

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

freeVars' :: IsVarSet a c => NLPat -> FreeM a c

Free t => Free (Arg t)

Defined in Agda.TypeChecking.Free.Lazy

Methods

freeVars' :: IsVarSet a c => Arg t -> FreeM a c

Free t => Free (WithHiding t)

Defined in Agda.TypeChecking.Free.Lazy

Methods

freeVars' :: IsVarSet a c => WithHiding t -> FreeM a c

Free t => Free (Abs t)

Defined in Agda.TypeChecking.Free.Lazy

Methods

freeVars' :: IsVarSet a c => Abs t -> FreeM a c

Free t => Free (Dom t)

Defined in Agda.TypeChecking.Free.Lazy

Methods

freeVars' :: IsVarSet a c => Dom t -> FreeM a c

Free t => Free (PlusLevel' t)

Defined in Agda.TypeChecking.Free.Lazy

Methods

freeVars' :: IsVarSet a c => PlusLevel' t -> FreeM a c

Free t => Free (Tele t)

Defined in Agda.TypeChecking.Free.Lazy

Methods

freeVars' :: IsVarSet a c => Tele t -> FreeM a c

Free t => Free (Type' t)

Defined in Agda.TypeChecking.Free.Lazy

Methods

freeVars' :: IsVarSet a c => Type' t -> FreeM a c

Free t => Free (Elim' t)

Defined in Agda.TypeChecking.Free.Lazy

Methods

freeVars' :: IsVarSet a c => Elim' t -> FreeM a c

Free t => Free (SingleLevel' t)

Defined in Agda.TypeChecking.Level

Methods

freeVars' :: IsVarSet a c => SingleLevel' t -> FreeM a c

Free t => Free (Maybe t)

Defined in Agda.TypeChecking.Free.Lazy

Methods

freeVars' :: IsVarSet a c => Maybe t -> FreeM a c

Free t => Free [t]

Defined in Agda.TypeChecking.Free.Lazy

Methods

freeVars' :: IsVarSet a c => [t] -> FreeM a c

Free t => Free (Named nm t)

Defined in Agda.TypeChecking.Free.Lazy

Methods

freeVars' :: IsVarSet a c => Named nm t -> FreeM a c

(Free t, Free u) => Free (t, u)

Defined in Agda.TypeChecking.Free.Lazy

Methods

freeVars' :: IsVarSet a c => (t, u) -> FreeM a c

(Free t, Free u, Free v) => Free (t, u, v)

Defined in Agda.TypeChecking.Free.Lazy

Methods

freeVars' :: IsVarSet a c => (t, u, v) -> FreeM a c

Orphan instances

Singleton MetaId ()

Methods

singleton :: MetaId -> ()