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

Safe HaskellNone
LanguageHaskell2010

Agda.TypeChecking.Free

Contents

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

Synopsis

Documentation

data FreeVars Source #

Free variables of a term, (disjointly) partitioned into strongly and and weakly rigid variables, flexible variables and irrelevant variables.

Constructors

FV 

Fields

  • stronglyRigidVars :: VarSet

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

  • unguardedVars :: 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.

  • weaklyRigidVars :: VarSet

    Ordinary rigid variables, e.g., in arguments of variables or functions.

  • flexibleVars :: 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.

  • irrelevantVars :: VarSet

    Variables in irrelevant arguments and under a DontCare, i.e., in irrelevant positions.

Instances
Eq FreeVars Source # 
Instance details

Defined in Agda.TypeChecking.Free

Show FreeVars Source # 
Instance details

Defined in Agda.TypeChecking.Free

Semigroup FreeVars Source #

Free variable sets form a monoid under union.

Instance details

Defined in Agda.TypeChecking.Free

Monoid FreeVars Source # 
Instance details

Defined in Agda.TypeChecking.Free

Null FreeVars Source # 
Instance details

Defined in Agda.TypeChecking.Free

IsVarSet FreeVars Source # 
Instance details

Defined in Agda.TypeChecking.Free

Singleton Variable FreeVars Source # 
Instance details

Defined in Agda.TypeChecking.Free

class Free a Source #

Gather free variables in a collection.

Minimal complete definition

freeVars'

Instances
Free EqualityView Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Free Clause Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Methods

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

Free LevelAtom Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Free PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Free Level Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Methods

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

Free Sort Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Methods

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

Free Term Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Methods

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

Free Candidate Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Free NLPType Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting

Methods

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

Free NLPat Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting

Methods

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

Free DisplayTerm Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Free DisplayForm Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Free Constraint Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

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

Defined in Agda.TypeChecking.Free.Lazy

Methods

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

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

Defined in Agda.TypeChecking.Free.Lazy

Methods

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

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

Defined in Agda.TypeChecking.Free.Lazy

Methods

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

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

Defined in Agda.TypeChecking.Free.Lazy

Methods

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

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

Defined in Agda.TypeChecking.Free.Lazy

Methods

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

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

Defined in Agda.TypeChecking.Free.Lazy

Methods

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

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

Defined in Agda.TypeChecking.Free.Lazy

Methods

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

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

Defined in Agda.TypeChecking.Free.Lazy

Methods

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

(Free a, Free b) => Free (a, b) Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Methods

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

class (Semigroup a, Monoid a) => IsVarSet a where Source #

Any representation 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`.

Minimal complete definition

withVarOcc

Methods

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

Laws * Respects monoid operations: ``` withVarOcc o mempty == mempty withVarOcc o (x <> y) == withVarOcc o x <> withVarOcc o y ``` * Respects VarOcc composition ``` withVarOcc (composeVarOcc o1 o2) = withVarOcc o1 . withVarOcc o2 ```

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

Defined in Agda.TypeChecking.Free.Lazy

IsVarSet VarCounts Source # 
Instance details

Defined in Agda.TypeChecking.Free

IsVarSet FreeVars Source # 
Instance details

Defined in Agda.TypeChecking.Free

IsVarSet [Int] Source # 
Instance details

Defined in Agda.TypeChecking.Free

Methods

withVarOcc :: VarOcc -> [Int] -> [Int] 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.

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

Compute free variables.

rigidVars :: FreeVars -> VarSet Source #

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

relevantVars :: FreeVars -> VarSet Source #

All but the irrelevant variables.

allVars :: FreeVars -> VarSet Source #

allVars fv includes irrelevant variables.

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

Collect all free variables.

allFreeVarsWithOcc :: Free a => a -> TheVarMap Source #

Collect all free variables together with information about their occurrence.

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

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

allRelevantVarsIgnoring :: Free a => IgnoreSorts -> a -> 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 a => Nat -> a -> Bool Source #

data Occurrence Source #

Constructors

NoOccurrence 
Irrelevantly 
StronglyRigid

Under at least one and only inductive constructors.

Unguarded

In top position, or only under inductive record constructors.

WeaklyRigid

In arguments to variables and definitions.

Flexible MetaSet

In arguments of metas.

Instances
Eq Occurrence Source # 
Instance details

Defined in Agda.TypeChecking.Free

Show Occurrence Source # 
Instance details

Defined in Agda.TypeChecking.Free

data VarOcc Source #

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

Constructors

VarOcc 

occurrence :: Free a => Nat -> a -> Occurrence Source #

Compute an occurrence of a single variable in a piece of internal syntax.

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

Is the term entirely closed (no free variables)?

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

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

freeVars' :: (Free a, IsVarSet c) => a -> FreeM c 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 #