Agda-2.3.0: 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 

Fields

stronglyRigidVars :: VarSet

variables at top and under constructors

weaklyRigidVars :: VarSet

ord. rigid variables, e.g., in arguments of variables

flexibleVars :: VarSet

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

irrelevantVars :: VarSet

variables under a DontCare, i.e., in irrelevant positions

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 (Abs a) 
Free a => Free (Tele 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 :: FreeVars -> VarSetSource

allVars fv includes irrelevant variables.

relevantVars :: FreeVars -> VarSetSource

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

occurrence :: Nat -> FreeVars -> OccurrenceSource

occurrence x fv ignores irrelevant variables in fv