Agda-2.6.2.2.20221128: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.TypeChecking.Free

Description

Computing the free variables of a term.

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

If you need the occurrence information for all free variables, you can use freeVars which has amoungst others this instance freeVars :: Term -> VarMap From VarMap, specific information can be extracted, e.g., relevantVars :: VarMap -> VarSet relevantVars = filterVarMap isRelevant

To just check the status of a single free variable, there are more efficient methods, e.g., freeIn :: Nat -> Term -> Bool

Tailored optimized variable checks can be implemented as semimodules to VarOcc', see, for example, VarCounts or SingleFlexRig.

Synopsis

Documentation

newtype VarCounts Source #

Constructors

VarCounts 

Fields

class Free t Source #

Gather free variables in a collection.

Instances

Instances details
Free Clause Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Methods

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

Free EqualityView Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Methods

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

Free Level Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Methods

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

Free Sort Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Methods

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

Free Term Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Methods

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

Free Candidate Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

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

Free CompareAs Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

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

Free Constraint Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

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

Free DisplayForm Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

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

Free DisplayTerm Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

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

Free NLPSort Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

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

Free NLPType Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

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

Free NLPat Source #

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

Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

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

Free t => Free (Arg t) Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Methods

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

Free t => Free (WithHiding t) Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Methods

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

Free t => Free (Abs t) Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Methods

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

Free t => Free (Dom t) Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Methods

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

Free t => Free (PlusLevel' t) Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Methods

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

Free t => Free (Tele t) Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Methods

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

Free t => Free (Type' t) Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Methods

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

Free t => Free (Elim' t) Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Methods

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

Free t => Free (SingleLevel' t) Source # 
Instance details

Defined in Agda.TypeChecking.Level

Methods

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

Free t => Free (Maybe t) Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Methods

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

Free t => Free [t] Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Methods

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

Free t => Free (Named nm t) Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Methods

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

(Free t, Free u) => Free (t, u) Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Methods

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

(Free t, Free u, Free v) => Free (t, u, v) Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Methods

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

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

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

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

Instances details
IsVarSet () VarCounts Source # 
Instance details

Defined in Agda.TypeChecking.Free

IsVarSet () FlexRigMap Source #

Compose everything with the varFlexRig part of the VarOcc'.

Instance details

Defined in Agda.TypeChecking.Free.Lazy

IsVarSet () AllowedVar Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

IsVarSet () All Source # 
Instance details

Defined in Agda.TypeChecking.Free

Methods

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

IsVarSet () Any Source # 
Instance details

Defined in Agda.TypeChecking.Free

Methods

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

IsVarSet () [Int] Source # 
Instance details

Defined in Agda.TypeChecking.Free

Methods

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

(Singleton MetaId a, Semigroup a, Monoid a) => IsVarSet a (VarMap' a) Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Methods

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

data IgnoreSorts Source #

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

Instances details
Show IgnoreSorts Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Eq IgnoreSorts Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

freeVars :: (IsVarSet a c, Singleton Variable c, Free t) => t -> c Source #

Collect all free variables together with information about their occurrence.

Doesn't go inside solved metas, but collects the variables from a metavariable application X ts as flexibleVars.

freeVars' :: (Free t, IsVarSet a c) => t -> FreeM a c Source #

filterVarMap :: (VarOcc -> Bool) -> VarMap -> VarSet Source #

runFree :: (IsVarSet a c, Free t) => SingleVar c -> IgnoreSorts -> t -> c Source #

Compute free variables.

rigidVars :: VarMap -> VarSet Source #

Rigid variables: either strongly rigid, unguarded, or weakly rigid.

stronglyRigidVars :: VarMap -> VarSet Source #

Variables under only and at least one inductive constructor(s).

unguardedVars :: VarMap -> VarSet Source #

Variables at top or only under inductive record constructors λs and Πs. The purpose of recording these separately is that they can still become strongly rigid if put under a constructor whereas weakly rigid ones stay weakly rigid.

allVars :: VarMap -> VarSet Source #

flexibleVars :: VarMap -> IntMap MetaSet Source #

Variables occuring in arguments of metas. These are only potentially free, depending how the meta variable is instantiated. The set contains the id's of the meta variables that this variable is an argument to.

allFreeVars :: Free t => t -> VarSet Source #

Collect all free variables.

allRelevantVars :: Free t => t -> VarSet Source #

Collect all relevant free variables, excluding the "unused" ones.

allRelevantVarsIgnoring :: Free t => IgnoreSorts -> t -> VarSet Source #

Collect all relevant free variables, possibly ignoring sorts.

freeIn :: Free a => Nat -> a -> Bool Source #

isBinderUsed :: Free a => Abs a -> Bool Source #

Is the variable bound by the abstraction actually used?

relevantIn :: Free t => Nat -> t -> Bool Source #

data FlexRig' a Source #

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

Instances details
Foldable FlexRig' Source # 
Instance details

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' Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Methods

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

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

LensFlexRig a (FlexRig' a) Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Show a => Show (FlexRig' a) Source # 
Instance details

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) Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Methods

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

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

Singleton (Variable, FlexRig' ()) FlexRigMap Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

class LensFlexRig a o | o -> a where Source #

Instances

Instances details
LensFlexRig a (FlexRig' a) Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

LensFlexRig a (VarOcc' a) Source #

Access to varFlexRig in VarOcc'.

Instance details

Defined in Agda.TypeChecking.Free.Lazy

LensFlexRig a (FreeEnv' a b c) Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Methods

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

data VarOcc' a Source #

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

Constructors

VarOcc 

Instances

Instances details
LensFlexRig a (VarOcc' a) Source #

Access to varFlexRig in VarOcc'.

Instance details

Defined in Agda.TypeChecking.Free.Lazy

LensModality (VarOcc' a) Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

LensQuantity (VarOcc' a) Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

LensRelevance (VarOcc' a) Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

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

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.

Instance details

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) Source #

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.

Instance details

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) Source # 
Instance details

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) Source #

Equality up to origin.

Instance details

Defined in Agda.TypeChecking.Free.Lazy

Methods

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

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

varOccurrenceIn :: Free a => Nat -> a -> Maybe VarOcc Source #

Get the full occurrence information of a free variable.

flexRigOccurrenceIn :: Free a => Nat -> a -> Maybe FlexRig Source #

Get the full occurrence information of a free variable.

closed :: Free t => t -> Bool Source #

Is the term entirely closed (no free variables)?

data MetaSet Source #

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

Instances

Instances details
Null MetaSet Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Monoid MetaSet Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Semigroup MetaSet Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Show MetaSet Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Eq MetaSet Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Methods

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

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

Singleton MetaId MetaSet Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

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

Orphan instances

IsVarSet () All Source # 
Instance details

Methods

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

IsVarSet () Any Source # 
Instance details

Methods

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

IsVarSet () [Int] Source # 
Instance details

Methods

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