Safe Haskell  None 

Language  Haskell98 
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 = FV {
 stronglyRigidVars :: VarSet
 unguardedVars :: VarSet
 weaklyRigidVars :: VarSet
 flexibleVars :: IntMap [MetaId]
 irrelevantVars :: VarSet
 unusedVars :: VarSet
 type Free a = Free' a Any
 class Free' a c
 type FreeV a = Free' a FreeVars
 type FreeVS a = Free' a VarSet
 data IgnoreSorts
 runFree :: (Monoid c, Free' a c) => SingleVar c > IgnoreSorts > a > c
 rigidVars :: FreeVars > VarSet
 relevantVars :: FreeVars > VarSet
 allVars :: FreeVars > VarSet
 allFreeVars :: Free' a VarSet => a > VarSet
 allRelevantVars :: Free' a VarSet => a > VarSet
 allRelevantVarsIgnoring :: Free' a VarSet => IgnoreSorts > a > VarSet
 freeIn :: Free a => Nat > a > Bool
 freeInIgnoringSorts :: Free a => Nat > a > Bool
 isBinderUsed :: Free a => Abs a > Bool
 relevantIn :: Free a => Nat > a > Bool
 relevantInIgnoringSortAnn :: Free a => Nat > a > Bool
 data Occurrence
 occurrence :: FreeV a => Nat > a > Occurrence
 closed :: Free' a All => a > Bool
 freeVars :: (Monoid c, Singleton Variable c, Free' a c) => a > c
Documentation
Free variables of a term, (disjointly) partitioned into strongly and and weakly rigid variables, flexible variables and irrelevant variables.
FV  

Gather free variables in a collection.
Free' EqualityView c Source #  
Free' ClauseBody c Source #  
Free' Clause c Source #  
Free' LevelAtom c Source #  
Free' PlusLevel c Source #  
Free' Level c Source #  
Free' Sort c Source #  
Free' Type c Source #  
Free' Term c Source #  
Free' a c => Free' [a] c Source #  
Free' a c => Free' (Maybe a) c Source #  
Free' a c => Free' (Dom a) c Source #  
Free' a c => Free' (Arg a) c Source #  
Free' a c => Free' (Tele a) c Source #  
Free' a c => Free' (Abs a) c Source #  
Free' a c => Free' (Elim' a) c Source #  
(Free' a c, Free' b c) => Free' (a, b) c 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. 
rigidVars :: FreeVars > VarSet Source #
Rigid variables: either strongly rigid, unguarded, or weakly rigid.
relevantVars :: FreeVars > VarSet Source #
All but the irrelevant variables.
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.
isBinderUsed :: Free a => Abs a > Bool Source #
Is the variable bound by the abstraction actually used?
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 [MetaId]  In arguments of metas. 
Unused 
occurrence :: FreeV a => Nat > a > Occurrence Source #
Compute an occurrence of a single variable in a piece of internal syntax.