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

Agda.TypeChecking.Free

Description

Computing the free variables of a term.

Synopsis

# Documentation

data FreeVars Source

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

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

Constructors

 FV FieldsstronglyRigidVars :: VarSetvariables at top and under constructors weaklyRigidVars :: VarSetord. rigid variables, e.g., in arguments of variables flexibleVars :: VarSetvariables occuring in arguments of metas. These are potentially free, depending how the meta variable is instantiated. irrelevantVars :: VarSetvariables in irrelevant arguments and under a `DontCare`, i.e., in irrelevant positions unusedVars :: VarSetvariables in `UnusedArg`uments

class Free a Source

Instances

 Free ClauseBody Free LevelAtom Free PlusLevel Free Level Free Sort Free Type Free Term Free a => Free [a] Free a => Free (Maybe a) Free a => Free (Arg a) Free a => Free (Dom a) Free a => Free (Tele a) Free a => Free (Abs a) (Free a, Free b) => Free (a, b)

freeVars :: Free a => a -> FreeVarsSource

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

`allVars fv` includes irrelevant variables.

All but the irrelevant variables.

freeIn :: Free a => Nat -> a -> BoolSource

isBinderUsed :: Free a => Abs a -> BoolSource

Is the variable bound by the abstraction actually used?

relevantIn :: Free a => Nat -> a -> BoolSource

data Occurrence Source

Constructors

 NoOccurrence Irrelevantly StronglyRigid WeaklyRigid Flexible Unused

Instances

 Eq Occurrence Show Occurrence