Safe Haskell  None 

Language  Haskell98 
Computing the free variables of a term.
This is the old version of 'Free'
, using
IntSet
s for the separate variable categories.
We keep it as a specification.
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 = FV {}
 class Free a
 data IgnoreSorts
 freeVars :: Free a => a > FreeVars
 freeVarsIgnore :: Free a => IgnoreSorts > 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
 freeInIgnoringSortAnn :: Free a => Nat > a > Bool
 relevantIn :: Free a => Nat > a > Bool
 relevantInIgnoringSortAnn :: Free a => Nat > a > Bool
 data Occurrence
 occurrence :: Nat > FreeVars > Occurrence
Documentation
Free variables of a term, (disjointly) partitioned into strongly and and weakly rigid variables, flexible variables and irrelevant variables.
FV  

freeVars'
Free ClauseBody Source  
Free Clause Source  
Free LevelAtom Source  
Free PlusLevel Source  
Free Level Source  
Free Sort Source  
Free Type Source  
Free Term Source  
Free a => Free [a] Source  
Free a => Free (Maybe a) Source  
Free a => Free (Tele a) Source  
Free a => Free (Abs a) Source  
Free a => Free (Elim' a) Source  
Free a => Free (Dom a) Source  
Free a => Free (Arg a) Source  
(Free a, Free b) => Free (a, b) Source 
data IgnoreSorts Source
Where should we skip sorts in free variable analysis?
IgnoreNot  Do not skip. 
IgnoreInAnnotations  Skip when annotation to a type. 
IgnoreAll  Skip unconditionally. 
freeVars :: Free a => a > FreeVars Source
Doesn't go inside solved metas, but collects the variables from a
metavariable application X ts
as flexibleVars
.
freeVarsIgnore :: Free a => IgnoreSorts > a > FreeVars Source
relevantVars :: FreeVars > VarSet Source
All but the irrelevant variables.
rigidVars :: FreeVars > VarSet Source
Rigid variables: either strongly rigid, unguarded, or weakly rigid.
isBinderUsed :: Free a => Abs a > Bool Source
Is the variable bound by the abstraction actually used?
freeInIgnoringSorts :: Free a => Nat > a > Bool Source
freeInIgnoringSortAnn :: Free a => Nat > a > Bool Source
relevantIn :: Free a => Nat > a > Bool Source
relevantInIgnoringSortAnn :: Free a => Nat > a > Bool Source
data Occurrence Source
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  In arguments of metas. 
Unused 
occurrence :: Nat > FreeVars > Occurrence Source