Agda- A dependently typed functional programming language and proof assistant

Safe HaskellNone



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



data FreeVars Source

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




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.

flexibleVars :: VarSet

Variables occuring in arguments of metas. These are only potentially free, depending how the meta variable is instantiated.

irrelevantVars :: VarSet

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

unusedVars :: VarSet

Variables in UnusedArguments.


Eq FreeVars Source 
Show FreeVars Source 
Monoid FreeVars Source

Free variable sets form a monoid under union.

Singleton Variable FreeVars Source 

type Free a = Free' a Any Source

type FreeVS a = Free' a VarSet Source

data IgnoreSorts Source

Where should we skip sorts in free variable analysis?



Do not skip.


Skip when annotation to a type.


Skip unconditionally.

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

Collect all free variables.

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

Collect all relevant free variables.

allRelevantVarsIgnoring :: Free' a VarSet => 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



Under at least one and only inductive constructors.


In top position, or only under inductive record constructors.


In arguments to variables and definitions.


In arguments of metas.


occurrence :: FreeV a => Nat -> a -> Occurrence Source

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

closed :: Free' a All => a -> Bool Source

Is the term entirely closed (no free variables)?

freeVars :: (Monoid c, Singleton Variable c, Free' a c) => a -> c Source

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