Safe Haskell  None 

Language  Haskell98 
Computing the free variables of a term lazily.
We implement a reduce (traversal into monoid) over internal syntax for a generic collection (monoid with singletons). This should allow a more efficient test for the presence of a particular variable.
Worstcase complexity does not change (i.e. the case when a variable
does not occur), but best casecomplexity does matter. For instance,
see mkAbs
: each time we construct
a dependent function type, we check it is actually dependent.
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 FlexRig
 composeFlexRig :: FlexRig > FlexRig > FlexRig
 data VarOcc = VarOcc {}
 maxVarOcc :: VarOcc > VarOcc > VarOcc
 topVarOcc :: VarOcc
 botVarOcc :: VarOcc
 type VarMap = IntMap VarOcc
 data IgnoreSorts
 data FreeEnv c = FreeEnv {
 feIgnoreSorts :: !IgnoreSorts
 feBinders :: !Int
 feFlexRig :: !FlexRig
 feRelevance :: !Relevance
 feSingleton :: SingleVar c
 type Variable = (Int, VarOcc)
 type SingleVar c = Variable > c
 initFreeEnv :: SingleVar c > FreeEnv c
 type FreeM c = Reader (FreeEnv c) c
 variable :: Monoid c => Int > FreeM c
 bind :: FreeM a > FreeM a
 go :: FlexRig > FreeM a > FreeM a
 goRel :: Relevance > FreeM a > FreeM a
 underConstructor :: ConHead > FreeM a > FreeM a
 class Free' a c where
Documentation
Depending on the surrounding context of a variable, it's occurrence can be classified as flexible or rigid, with finer distinctions.
The constructors are listed in increasing order (wrt. information content).
Flexible  In arguments of metas. 
WeaklyRigid  In arguments to variables and definitions. 
Unguarded  In top position, or only under inductive record constructors. 
StronglyRigid  Under at least one and only inductive constructors. 
composeFlexRig :: FlexRig > FlexRig > FlexRig Source
FlexRig
composition. For accumulating the context of a variable.
Flexible
is dominant. Once we are under a meta, we are flexible
regardless what else comes.
WeaklyRigid
is next in strength. Destroys strong rigidity.
StronglyRigid
is still dominant over Unguarded
.
Unguarded
is the unit. It is the top (identity) context.
maxVarOcc :: VarOcc > VarOcc > VarOcc Source
When we extract information about occurrence, we care most about
about StronglyRigid
Relevant
occurrences.
Collecting free variables.
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. 
The current context.
FreeEnv  

initFreeEnv :: SingleVar c > FreeEnv c Source
The initial context.
underConstructor :: ConHead > FreeM a > FreeM a Source
What happens to the variables occurring under a constructor?
Gather free variables in a collection.
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' (Tele a) c Source  
Free' a c => Free' (Abs a) c Source  
Free' a c => Free' (Elim' a) c Source  
Free' a c => Free' (Dom a) c Source  
Free' a c => Free' (Arg a) c Source  
(Free' a c, Free' b c) => Free' (a, b) c Source 