Computing the free variables of a term.
- data FreeVars = FV {}
- class Free a
- freeVars :: Free a => a -> FreeVars
- allVars :: FreeVars -> VarSet
- relevantVars :: FreeVars -> VarSet
- rigidVars :: FreeVars -> VarSet
- freeIn :: Free a => Nat -> a -> Bool
- isBinderUsed :: Free a => Abs a -> Bool
- freeInIgnoringSorts :: Free a => Nat -> a -> Bool
- relevantIn :: Free a => Nat -> a -> Bool
- data Occurrence
- = NoOccurrence
- | StronglyRigid
- | WeaklyRigid
- | Flexible
- occurrence :: Nat -> FreeVars -> Occurrence
Documentation
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.
FV | |
|
freeVars :: Free a => a -> FreeVarsSource
Doesn't go inside solved metas, but collects the variables from a
metavariable application X ts
as flexibleVars
.
relevantVars :: FreeVars -> VarSetSource
All but the irrelevant variables.
isBinderUsed :: Free a => Abs a -> BoolSource
Is the variable bound by the abstraction actually used?
freeInIgnoringSorts :: Free a => Nat -> a -> BoolSource
relevantIn :: Free a => Nat -> a -> BoolSource
occurrence :: Nat -> FreeVars -> OccurrenceSource
occurrence x fv
ignores irrelevant variables in fv