Safe Haskell  None 

Language  Haskell2010 
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).
If you need the occurrence information for all free variables, you can use
freeVars
which has amoungst others this instance
freeVars :: Term > VarMap
From VarMap
, specific information can be extracted, e.g.,
relevantVars :: VarMap > VarSet
relevantVars = filterVarMap isRelevant
To just check the status of a single free variable, there are more
efficient methods, e.g.,
freeIn :: Nat > Term > Bool
Tailored optimized variable checks can be implemented as semimodules to VarOcc'
,
see, for example, VarCounts
or SingleFlexRig
.
Synopsis
 newtype VarCounts = VarCounts {}
 class Free t
 class (Singleton MetaId a, Semigroup a, Monoid a, Semigroup c, Monoid c) => IsVarSet a c  c > a where
 withVarOcc :: VarOcc' a > c > c
 data IgnoreSorts
 freeVars :: (IsVarSet a c, Singleton Variable c, Free t) => t > c
 freeVars' :: (Free t, IsVarSet a c) => t > FreeM a c
 filterVarMap :: (VarOcc > Bool) > VarMap > VarSet
 filterVarMapToList :: (VarOcc > Bool) > VarMap > [Variable]
 runFree :: (IsVarSet a c, Free t) => SingleVar c > IgnoreSorts > t > c
 rigidVars :: VarMap > VarSet
 stronglyRigidVars :: VarMap > VarSet
 unguardedVars :: VarMap > VarSet
 allVars :: VarMap > VarSet
 allFreeVars :: Free t => t > VarSet
 allRelevantVars :: Free t => t > VarSet
 allRelevantVarsIgnoring :: Free t => IgnoreSorts > t > VarSet
 freeIn :: Free a => Nat > a > Bool
 freeInIgnoringSorts :: Free a => Nat > a > Bool
 isBinderUsed :: Free a => Abs a > Bool
 relevantIn :: Free t => Nat > t > Bool
 relevantInIgnoringSortAnn :: Free t => Nat > t > Bool
 data FlexRig' a
 type FlexRig = FlexRig' MetaSet
 class LensFlexRig a o  o > a where
 lensFlexRig :: Lens' (FlexRig' a) o
 isFlexible :: LensFlexRig a o => o > Bool
 isUnguarded :: LensFlexRig a o => o > Bool
 isStronglyRigid :: LensFlexRig a o => o > Bool
 isWeaklyRigid :: LensFlexRig a o => o > Bool
 data VarOcc' a = VarOcc {
 varFlexRig :: FlexRig' a
 varModality :: Modality
 type VarOcc = VarOcc' MetaSet
 varOccurrenceIn :: Free a => Nat > a > Maybe VarOcc
 flexRigOccurrenceIn :: Free a => Nat > a > Maybe (FlexRig' ())
 closed :: Free t => t > Bool
 data MetaSet
 insertMetaSet :: MetaId > MetaSet > MetaSet
 foldrMetaSet :: (MetaId > a > a) > a > MetaSet > a
Documentation
Gather free variables in a collection.
Instances
class (Singleton MetaId a, Semigroup a, Monoid a, Semigroup c, Monoid c) => IsVarSet a c  c > a where Source #
Any representation c
of a set of variables need to be able to be modified by
a variable occurrence. This is to ensure that free variable analysis is
compositional. For instance, it should be possible to compute `fv (v [u/x])`
from `fv v` and `fv u`.
In algebraic terminology, a variable set a
needs to be (almost) a left semimodule
to the semiring VarOcc'
.
withVarOcc :: VarOcc' a > c > c Source #
Laws * Respects monoid operations: ``` withVarOcc o mempty == mempty withVarOcc o (x <> y) == withVarOcc o x <> withVarOcc o y ``` * Respects VarOcc composition: ``` withVarOcc oneVarOcc = id withVarOcc (composeVarOcc o1 o2) = withVarOcc o1 . withVarOcc o2 ``` * Respects VarOcc aggregation: ``` withVarOcc (o1 <> o2) x = withVarOcc o1 x <> withVarOcc o2 x ``` Since the corresponding unit law may fail, ``` withVarOcc mempty x = mempty ``` it is not quite a semimodule.
Instances
IsVarSet () All Source #  
Defined in Agda.TypeChecking.Free  
IsVarSet () Any Source #  
Defined in Agda.TypeChecking.Free  
IsVarSet () FlexRigMap Source #  Compose everything with the 
Defined in Agda.TypeChecking.Free.Lazy withVarOcc :: VarOcc' () > FlexRigMap > FlexRigMap Source #  
IsVarSet () VarCounts Source #  
Defined in Agda.TypeChecking.Free  
IsVarSet () AllowedVar Source #  
Defined in Agda.TypeChecking.MetaVars.Occurs withVarOcc :: VarOcc' () > AllowedVar > AllowedVar Source #  
IsVarSet () [Int] Source #  
Defined in Agda.TypeChecking.Free  
(Singleton MetaId a, Semigroup a, Monoid a) => IsVarSet a (VarMap' a) Source #  
Defined in Agda.TypeChecking.Free.Lazy 
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. 
Instances
Eq IgnoreSorts Source #  
Defined in Agda.TypeChecking.Free.Lazy (==) :: IgnoreSorts > IgnoreSorts > Bool # (/=) :: IgnoreSorts > IgnoreSorts > Bool #  
Show IgnoreSorts Source #  
Defined in Agda.TypeChecking.Free.Lazy showsPrec :: Int > IgnoreSorts > ShowS # show :: IgnoreSorts > String # showList :: [IgnoreSorts] > ShowS # 
freeVars :: (IsVarSet a c, Singleton Variable c, Free t) => t > c Source #
Collect all free variables together with information about their occurrence.
Doesn't go inside solved metas, but collects the variables from a
metavariable application X ts
as flexibleVars
.
runFree :: (IsVarSet a c, Free t) => SingleVar c > IgnoreSorts > t > c Source #
Compute free variables.
rigidVars :: VarMap > VarSet Source #
Rigid variables: either strongly rigid, unguarded, or weakly rigid.
stronglyRigidVars :: VarMap > VarSet Source #
Variables under only and at least one inductive constructor(s).
unguardedVars :: VarMap > VarSet Source #
Variables at top or only under inductive record constructors λs and Πs. The purpose of recording these separately is that they can still become strongly rigid if put under a constructor whereas weakly rigid ones stay weakly rigid.
allVars :: VarMap > VarSet Source #
Variables occuring in arguments of metas.
These are only potentially free, depending how the meta variable is instantiated.
The set contains the id's of the meta variables that this variable is an argument to.
flexibleVars :: VarMap > IntMap MetaSet
flexibleVars (VarMap m) = (mapMaybe
m) $ case
VarOcc (Flexible ms) _ > Just ms
_ > Nothing
allFreeVars :: Free t => t > VarSet Source #
Collect all free variables.
allRelevantVars :: Free t => t > VarSet Source #
Collect all relevant free variables, excluding the "unused" ones.
allRelevantVarsIgnoring :: Free t => IgnoreSorts > t > 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?
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 a  In arguments of metas.
The set of metas is used by ' 
WeaklyRigid  In arguments to variables and definitions. 
Unguarded  In top position, or only under inductive record constructors (unit). 
StronglyRigid  Under at least one and only inductive constructors. 
Instances
Functor FlexRig' Source #  
Foldable FlexRig' Source #  
Defined in Agda.TypeChecking.Free.Lazy fold :: Monoid m => FlexRig' m > m # foldMap :: Monoid m => (a > m) > FlexRig' a > m # foldr :: (a > b > b) > b > FlexRig' a > b # foldr' :: (a > b > b) > b > FlexRig' a > b # foldl :: (b > a > b) > b > FlexRig' a > b # foldl' :: (b > a > b) > b > FlexRig' a > b # foldr1 :: (a > a > a) > FlexRig' a > a # foldl1 :: (a > a > a) > FlexRig' a > a # elem :: Eq a => a > FlexRig' a > Bool # maximum :: Ord a => FlexRig' a > a # minimum :: Ord a => FlexRig' a > a #  
LensFlexRig a (FlexRig' a) Source #  
Defined in Agda.TypeChecking.Free.Lazy  
Eq a => Eq (FlexRig' a) Source #  
Show a => Show (FlexRig' a) Source #  
Singleton (Variable, FlexRig' ()) FlexRigMap Source #  
Defined in Agda.TypeChecking.Free.Lazy 
class LensFlexRig a o  o > a where Source #
lensFlexRig :: Lens' (FlexRig' a) o Source #
Instances
LensFlexRig a (VarOcc' a) Source #  Access to 
Defined in Agda.TypeChecking.Free.Lazy  
LensFlexRig a (FlexRig' a) Source #  
Defined in Agda.TypeChecking.Free.Lazy  
LensFlexRig a (FreeEnv' a b c) Source #  
Defined in Agda.TypeChecking.Free.Lazy 
isFlexible :: LensFlexRig a o => o > Bool Source #
isUnguarded :: LensFlexRig a o => o > Bool Source #
isStronglyRigid :: LensFlexRig a o => o > Bool Source #
isWeaklyRigid :: LensFlexRig a o => o > Bool Source #
Occurrence of free variables is classified by several dimensions.
Currently, we have FlexRig
and Modality
.
VarOcc  

Instances
LensFlexRig a (VarOcc' a) Source #  Access to 
Defined in Agda.TypeChecking.Free.Lazy  
Eq a => Eq (VarOcc' a) Source #  Equality up to origin. 
Show a => Show (VarOcc' a) Source #  
Semigroup a => Semigroup (VarOcc' a) Source #  The default way of aggregating free variable info from subterms is by adding
the variable occurrences. For instance, if we have a pair From counting

(Semigroup a, Monoid a) => Monoid (VarOcc' a) Source #  The neutral element for variable occurrence aggregation is least serious
occurrence: flexible, irrelevant.
This is also the absorptive element for 
LensRelevance (VarOcc' a) Source #  
Defined in Agda.TypeChecking.Free.Lazy  
LensQuantity (VarOcc' a) Source #  
Defined in Agda.TypeChecking.Free.Lazy  
LensModality (VarOcc' a) Source #  
Defined in Agda.TypeChecking.Free.Lazy 
varOccurrenceIn :: Free a => Nat > a > Maybe VarOcc Source #
Get the full occurrence information of a free variable.
flexRigOccurrenceIn :: Free a => Nat > a > Maybe (FlexRig' ()) Source #
Get the full occurrence information of a free variable.
A set of meta variables. Forms a monoid under union.
foldrMetaSet :: (MetaId > a > a) > a > MetaSet > a Source #