Safe Haskell  None 

Language  Haskell2010 
 Set of meta variables.
 Flexible and rigid occurrences (semigroup)
 Multidimensional feature vector for variable occurrence (semigroup)
 Storing variable occurrences (semimodule).
 Simple flexible/rigid variable collection.
 Environment for collecting free variables.
 Recursively collecting free variables.
 Orphan instances
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 whether 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).
For further reading on semirings and semimodules for variable occurrence, see e.g. Conor McBrides "I got plenty of nuttin'" (Wadlerfest 2016). There, he treats the "quantity" dimension of variable occurrences.
The semiring has an additive operation for combining occurrences of subterms,
and a multiplicative operation of representing function composition. E.g.
if variable x
appears o
in term u
, but u
appears in context q
in
term t
then occurrence of variable x
coming from u
is accounted for
as q o
in t
.
Consider example (λ{ x → (x,x)}) y
:
 Variable
x
occurs once unguarded inx
.  It occurs twice unguarded in the aggregation
x
x
 Inductive constructor
,
turns this into two strictly rigid occurrences.
If ,
is a record constructor, then we stay unguarded.
 The function
({λ x → (x,x)})
provides a context for variabley
. This context can be described as weakly rigid with quantity two.  The final occurrence of
y
is obtained as composing the context with the occurrence ofy
in itself (which is the unit for composition). Thus,y
occurs weakly rigid with quantity two.
It is not a given that the context can be described in the same way as the variable occurrence. However, for quantity it is the case and we obtain a semiring of occurrences with 0, 1, and even ω, which is an absorptive element for addition.
Synopsis
 newtype MetaSet = MetaSet {
 theMetaSet :: IntSet
 insertMetaSet :: MetaId > MetaSet > MetaSet
 foldrMetaSet :: (MetaId > a > a) > a > MetaSet > a
 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
 isWeaklyRigid :: LensFlexRig a o => o > Bool
 isStronglyRigid :: LensFlexRig a o => o > Bool
 addFlexRig :: Semigroup a => FlexRig' a > FlexRig' a > FlexRig' a
 zeroFlexRig :: Monoid a => FlexRig' a
 omegaFlexRig :: FlexRig' a
 composeFlexRig :: Semigroup a => FlexRig' a > FlexRig' a > FlexRig' a
 oneFlexRig :: FlexRig' a
 data VarOcc' a = VarOcc {
 varFlexRig :: FlexRig' a
 varModality :: Modality
 type VarOcc = VarOcc' MetaSet
 topVarOcc :: VarOcc' a
 composeVarOcc :: Semigroup a => VarOcc' a > VarOcc' a > VarOcc' a
 oneVarOcc :: VarOcc' a
 class (Singleton MetaId a, Semigroup a, Monoid a, Semigroup c, Monoid c) => IsVarSet a c  c > a where
 withVarOcc :: VarOcc' a > c > c
 type TheVarMap' a = IntMap (VarOcc' a)
 newtype VarMap' a = VarMap {
 theVarMap :: TheVarMap' a
 type TheVarMap = TheVarMap' MetaSet
 type VarMap = VarMap' MetaSet
 mapVarMap :: (TheVarMap' a > TheVarMap' b) > VarMap' a > VarMap' b
 lookupVarMap :: Variable > VarMap' a > Maybe (VarOcc' a)
 type TheFlexRigMap = IntMap (FlexRig' ())
 newtype FlexRigMap = FlexRigMap {}
 mapFlexRigMap :: (TheFlexRigMap > TheFlexRigMap) > FlexRigMap > FlexRigMap
 data IgnoreSorts
 data FreeEnv' a b c = FreeEnv {
 feExtra :: !b
 feFlexRig :: !(FlexRig' a)
 feModality :: !Modality
 feSingleton :: Maybe Variable > c
 type Variable = Int
 type SingleVar c = Variable > c
 type FreeEnv c = FreeEnv' MetaSet IgnoreSorts c
 feIgnoreSorts :: FreeEnv' a IgnoreSorts c > IgnoreSorts
 initFreeEnv :: Monoid c => b > SingleVar c > FreeEnv' a b c
 type FreeT a b m c = ReaderT (FreeEnv' a b c) m c
 type FreeM a c = Reader (FreeEnv' a IgnoreSorts c) c
 runFreeM :: IsVarSet a c => SingleVar c > IgnoreSorts > FreeM a c > c
 variable :: (Monad m, IsVarSet a c) => Int > FreeT a b m c
 subVar :: Int > Maybe Variable > Maybe Variable
 underBinder :: MonadReader (FreeEnv' a b c) m => m z > m z
 underBinder' :: MonadReader (FreeEnv' a b c) m => Nat > m z > m z
 underModality :: (MonadReader r m, LensModality r, LensModality o) => o > m z > m z
 underRelevance :: (MonadReader r m, LensRelevance r, LensRelevance o) => o > m z > m z
 underFlexRig :: (MonadReader r m, LensFlexRig a r, Semigroup a, LensFlexRig a o) => o > m z > m z
 underConstructor :: (MonadReader r m, LensFlexRig a r, Semigroup a) => ConHead > m z > m z
 class Free t where
Set of meta variables.
A set of meta variables. Forms a monoid under union.
foldrMetaSet :: (MetaId > a > a) > a > MetaSet > a Source #
Flexible and rigid occurrences (semigroup)
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 #
isWeaklyRigid :: LensFlexRig a o => o > Bool Source #
isStronglyRigid :: LensFlexRig a o => o > Bool Source #
addFlexRig :: Semigroup a => FlexRig' a > FlexRig' a > FlexRig' a Source #
FlexRig
aggregation (additive operation of the semiring).
For combining occurrences of the same variable in subterms.
This is a refinement of the max
operation for FlexRig
which would work if Flexible
did not have the MetaSet
as an argument.
Now, to aggregate two Flexible
occurrences, we union the involved MetaSet
s.
zeroFlexRig :: Monoid a => FlexRig' a Source #
Unit for addFlexRig
.
omegaFlexRig :: FlexRig' a Source #
Absorptive for addFlexRig
.
composeFlexRig :: Semigroup a => FlexRig' a > FlexRig' a > FlexRig' a Source #
FlexRig
composition (multiplicative operation of the semiring).
For accumulating the context of a variable.
Flexible
is dominant. Once we are under a meta, we are flexible
regardless what else comes. We taint all variable occurrences
under a meta by this meta.
WeaklyRigid
is next in strength. Destroys strong rigidity.
StronglyRigid
is still dominant over Unguarded
.
Unguarded
is the unit. It is the top (identity) context.
oneFlexRig :: FlexRig' a Source #
Unit for composeFlexRig
.
Multidimensional feature vector for variable occurrence (semigroup)
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 
topVarOcc :: VarOcc' a Source #
The absorptive element of variable occurrence under aggregation: strongly rigid, relevant.
composeVarOcc :: Semigroup a => VarOcc' a > VarOcc' a > VarOcc' a Source #
First argument is the outer occurrence (context) and second is the inner. This multiplicative operation is to modify an occurrence under a context.
Storing variable occurrences (semimodule).
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 
type TheVarMap' a = IntMap (VarOcc' a) Source #
Representation of a variable set as map from de Bruijn indices
to VarOcc'
.
VarMap  

Instances
Singleton Variable (VarMap' a) Source #  A "set"style 
(Singleton MetaId a, Semigroup a, Monoid a) => IsVarSet a (VarMap' a) Source #  
Defined in Agda.TypeChecking.Free.Lazy  
Eq a => Eq (VarMap' a) Source #  
Show a => Show (VarMap' a) Source #  
Semigroup a => Semigroup (VarMap' a) Source #  Proper monoid instance for 
Semigroup a => Monoid (VarMap' a) Source #  
type TheVarMap = TheVarMap' MetaSet Source #
mapVarMap :: (TheVarMap' a > TheVarMap' b) > VarMap' a > VarMap' b Source #
Simple flexible/rigid variable collection.
type TheFlexRigMap = IntMap (FlexRig' ()) Source #
Keep track of FlexRig
for every variable, but forget the involved meta vars.
newtype FlexRigMap Source #
Instances
Show FlexRigMap Source #  
Defined in Agda.TypeChecking.Free.Lazy showsPrec :: Int > FlexRigMap > ShowS # show :: FlexRigMap > String # showList :: [FlexRigMap] > ShowS #  
Semigroup FlexRigMap Source #  
Defined in Agda.TypeChecking.Free.Lazy (<>) :: FlexRigMap > FlexRigMap > FlexRigMap # sconcat :: NonEmpty FlexRigMap > FlexRigMap # stimes :: Integral b => b > FlexRigMap > FlexRigMap #  
Monoid FlexRigMap Source #  
Defined in Agda.TypeChecking.Free.Lazy mempty :: FlexRigMap # mappend :: FlexRigMap > FlexRigMap > FlexRigMap # mconcat :: [FlexRigMap] > FlexRigMap #  
IsVarSet () FlexRigMap Source #  Compose everything with the 
Defined in Agda.TypeChecking.Free.Lazy withVarOcc :: VarOcc' () > FlexRigMap > FlexRigMap Source #  
Singleton (Variable, FlexRig' ()) FlexRigMap Source #  
Defined in Agda.TypeChecking.Free.Lazy 
mapFlexRigMap :: (TheFlexRigMap > TheFlexRigMap) > FlexRigMap > FlexRigMap Source #
Environment for 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. 
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 # 
The current context.
FreeEnv  

Instances
LensFlexRig a (FreeEnv' a b c) Source #  
Defined in Agda.TypeChecking.Free.Lazy  
LensRelevance (FreeEnv' a b c) Source #  
Defined in Agda.TypeChecking.Free.Lazy  
LensQuantity (FreeEnv' a b c) Source #  
Defined in Agda.TypeChecking.Free.Lazy  
LensModality (FreeEnv' a b c) Source #  
Defined in Agda.TypeChecking.Free.Lazy  
(Applicative m, Semigroup c) => Semigroup (FreeT a b m c) Source #  
(Functor m, Applicative m, Monad m, Semigroup c, Monoid c) => Monoid (FreeT a b m c) Source #  
feIgnoreSorts :: FreeEnv' a IgnoreSorts c > IgnoreSorts Source #
Ignore free variables in sorts.
runFreeM :: IsVarSet a c => SingleVar c > IgnoreSorts > FreeM a c > c Source #
Run function for FreeM.
subVar :: Int > Maybe Variable > Maybe Variable Source #
Subtract, but return Nothing if result is negative.
underBinder :: MonadReader (FreeEnv' a b c) m => m z > m z Source #
Going under a binder.
underBinder' :: MonadReader (FreeEnv' a b c) m => Nat > m z > m z Source #
Going under n
binders.
underModality :: (MonadReader r m, LensModality r, LensModality o) => o > m z > m z Source #
Changing the Modality
.
underRelevance :: (MonadReader r m, LensRelevance r, LensRelevance o) => o > m z > m z Source #
Changing the Relevance
.
underFlexRig :: (MonadReader r m, LensFlexRig a r, Semigroup a, LensFlexRig a o) => o > m z > m z Source #
Changing the FlexRig
context.
underConstructor :: (MonadReader r m, LensFlexRig a r, Semigroup a) => ConHead > m z > m z Source #
What happens to the variables occurring under a constructor?
Recursively collecting free variables.
Gather free variables in a collection.
Nothing
freeVars' :: IsVarSet a c => t > FreeM a c Source #
freeVars' :: (t ~ f b, Foldable f, Free b) => IsVarSet a c => t > FreeM a c Source #