HORIZON HASKELLDocslts/ghc-9.10.xc74966e2026-09-27Search names, modules, packages, or :: a typeCtrl K

GHC 9.10.3 · lts/ghc-9.10.x · c74966e · 2026-09-27

ModuleAgda-2.7.0.1Haskell2010

Agda.TypeChecking.Free

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.

  • 7 types
  • 3 classes
  • 28 values
  • PackageAgda-2.7.0.1
  • Exports39
  • LanguageHaskell2010
  • LicenceMIT
  • SourceFree.hs
classclass Free t where
#

Gather free variables in a collection.

Instances27Free, …
  • Free ClauseDefined in Agda-2.7.0.1 · Agda.TypeChecking.Free.Lazy
  • Free EqualityViewDefined in Agda-2.7.0.1 · Agda.TypeChecking.Free.Lazy
  • Free LevelDefined in Agda-2.7.0.1 · Agda.TypeChecking.Free.Lazy
  • Free SortDefined in Agda-2.7.0.1 · Agda.TypeChecking.Free.Lazy
  • Free TermDefined in Agda-2.7.0.1 · Agda.TypeChecking.Free.Lazy
  • Free CandidateDefined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Base
  • Free CompareAsDefined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Base
  • Free ConstraintDefined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Base
  • Free DisplayFormDefined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Base
  • Free DisplayTermDefined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Base
  • Free NLPSortDefined in Agda-2.7.0.1 · Agda.TypeChecking.Rewriting.NonLinPattern · orphan
  • Free NLPTypeDefined in Agda-2.7.0.1 · Agda.TypeChecking.Rewriting.NonLinPattern · orphan
  • Free NLPatDefined in Agda-2.7.0.1 · Agda.TypeChecking.Rewriting.NonLinPattern · orphan

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

  • Free t => Free (Arg t)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Free.Lazy
  • Free t => Free (WithHiding t)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Free.Lazy
  • Free t => Free (Abs t)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Free.Lazy
  • Free t => Free (Dom t)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Free.Lazy
  • Free t => Free (PlusLevel' t)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Free.Lazy
  • Free t => Free (Tele t)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Free.Lazy
  • Free t => Free (Type' t)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Free.Lazy
  • Free t => Free (Elim' t)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Free.Lazy
  • Free t => Free (SingleLevel' t)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Level
  • Free t => Free (Maybe t)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Free.Lazy
  • Free t => Free [t]Defined in Agda-2.7.0.1 · Agda.TypeChecking.Free.Lazy
  • Free t => Free (Named nm t)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Free.Lazy
  • (Free t, Free u) => Free (t, u)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Free.Lazy
  • (Free t, Free u, Free v) => Free (t, u, v)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Free.Lazy
classclass (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.

Instances11IsVarSet, …
valuefreeVars :: (IsVarSet a c, Singleton Variable c, Free t) => t -> c
#

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.

valuerigidVars :: VarMap -> VarSet
#

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

valueunguardedVars :: VarMap -> VarSet
#

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.

valueflexibleVars :: VarMap -> IntMap MetaSet
#

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.

valueallRelevantVars :: Free t => t -> VarSet
#

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

datadata 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 'Agda.TypeChecking.Rewriting.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.

Instances6Functor, Foldable, Eq, Show, LensFlexRig, Singleton
datadata VarOcc' a
#

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

Constructors

Instances8Eq, Show, Semigroup, Monoid, LensModality, LensQuantity, …
  • Eq a => Eq (VarOcc' a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Free.Lazy

    Equality up to origin.

  • Show a => Show (VarOcc' a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Free.Lazy
  • Semigroup a => Semigroup (VarOcc' a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Free.Lazy

    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.

  • (Semigroup a, Monoid a) => Monoid (VarOcc' a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Free.Lazy

    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.

  • LensModality (VarOcc' a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Free.Lazy
  • LensQuantity (VarOcc' a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Free.Lazy
  • LensRelevance (VarOcc' a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Free.Lazy
  • LensFlexRig (VarOcc' a) aDefined in Agda-2.7.0.1 · Agda.TypeChecking.Free.Lazy

    Access to varFlexRig in VarOcc.

valueclosed :: Free t => t -> Bool
#

Is the term entirely closed (no free variables)?

newtypenewtype MetaSet
#

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

Instances8Eq, Show, Semigroup, Monoid, Null, Singleton, …
  • Eq MetaSetDefined in Agda-2.7.0.1 · Agda.TypeChecking.Free.Lazy
  • Show MetaSetDefined in Agda-2.7.0.1 · Agda.TypeChecking.Free.Lazy
  • Semigroup MetaSetDefined in Agda-2.7.0.1 · Agda.TypeChecking.Free.Lazy
  • Monoid MetaSetDefined in Agda-2.7.0.1 · Agda.TypeChecking.Free.Lazy
  • Null MetaSetDefined in Agda-2.7.0.1 · Agda.TypeChecking.Free.Lazy
  • Singleton MetaId MetaSetDefined in Agda-2.7.0.1 · Agda.TypeChecking.Free.Lazy
  • IsVarSet MetaSet SingleFlexRigDefined in Agda-2.7.0.1 · Agda.TypeChecking.Free
  • IsVarSet MetaSet SingleVarOccDefined in Agda-2.7.0.1 · Agda.TypeChecking.Free

Orphan instances

4 instances