| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.TypeChecking.Free
Description
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
The most general function here is freeVarMap, which returns returns occurrence information about
every free variable. It is also a legacy function in the sense that it used to be the only function
for computing free occurrences, and it came with various functions for taking views of the resulting
VarMap. You can find these under the "Legacy API" here.
There are also also a bunch of specialized and optimized implementations of traversals here.
If you want to write a new function for computing free occurrence information, your task is
essentially to write a ComputeFree instance and invoke freeVars. These together implement a
generic traversal which has a good chance of being converted to decent code by GHC. You can look at
examples here and also look at the comments at ComputeFree.
Synopsis
- type FlexRig = FlexRig' MetaSet
- data FlexRig' a
- = Flexible !a
- | WeaklyRigid
- | Unguarded
- | StronglyRigid
- class Free t where
- freeVars :: ComputeFree r => t -> Reader r (Collect r)
- type FreeEnv c = FreeEnv' MetaSet IgnoreSorts c
- data FreeEnv' a b c = FreeEnv {
- feExtra :: !b
- feFlexRig :: !(FlexRig' a)
- feModality :: !Modality
- feSingleton :: !(b -> Maybe Variable -> c)
- data IgnoreSorts
- class (Singleton MetaId a, Monoid a, Monoid c) => IsVarSet a c | c -> a where
- withVarOcc :: VarOcc' a -> c -> c
- class LensFlexRig o a | o -> a where
- lensFlexRig :: Lens' o (FlexRig' a)
- newtype VarCounts = VarCounts {}
- type VarMap = VarMap' MetaSet
- newtype VarMap' a = VarMap {
- theVarMap :: TheVarMap' a
- type VarOcc = VarOcc' MetaSet
- data VarOcc' a = VarOcc {
- varFlexRig :: !(FlexRig' a)
- varModality :: !Modality
- composeFlexRig :: Semigroup a => FlexRig' a -> FlexRig' a -> FlexRig' a
- lookupVarMap :: Variable -> VarMap' a -> Maybe (VarOcc' a)
- mapVarMap :: (TheVarMap' a -> TheVarMap' b) -> VarMap' a -> VarMap' b
- allVars :: VarMap -> VarSet
- filterVarMap :: (VarOcc -> Bool) -> VarMap -> VarSet
- filterVarMapToList :: (VarOcc -> Bool) -> VarMap -> [Int]
- flexibleVars :: VarMap -> IntMap MetaSet
- freeVarMap :: Free t => t -> VarMap
- isFlexible :: LensFlexRig o a => o -> Bool
- isStronglyRigid :: LensFlexRig o a => o -> Bool
- isUnguarded :: LensFlexRig o a => o -> Bool
- isWeaklyRigid :: LensFlexRig o a => o -> Bool
- rigidVars :: VarMap -> VarSet
- stronglyRigidVars :: VarMap -> VarSet
- unguardedVars :: VarMap -> VarSet
- newtype MetaSet = MetaSet {}
- foldrMetaSet :: (MetaId -> a -> a) -> a -> MetaSet -> a
- insertMetaSet :: MetaId -> MetaSet -> MetaSet
- metaSetToBlocker :: MetaSet -> Blocker
- allFreeVar :: Free t => (Int -> Bool) -> t -> Bool
- allFreeVarIgnoreAll :: Free t => (Int -> Bool) -> t -> Bool
- anyFreeVar :: Free t => (Int -> Bool) -> t -> Bool
- anyFreeVarIgnoreAll :: (Int -> Bool) -> Term -> Bool
- closed :: Free t => t -> Bool
- flexRigOccurrenceIn :: Free a => Nat -> a -> Maybe FlexRig
- freeIn :: Free t => Nat -> t -> Bool
- freeInIgnoringSorts :: Free a => Nat -> a -> Bool
- freeVarCounts :: Free t => t -> VarCounts
- freeVarList :: Free t => t -> [Int]
- freeVarMapIgnoreAnn :: Free t => t -> VarMap
- freeVarSet :: Free t => t -> VarSet
- isBinderUsed :: Free a => Abs a -> Bool
- relevantInIgnoringSortAnn :: Free t => Nat -> t -> Bool
- setRelInIgnoring :: Free t => VarSet -> t -> VarSet
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).
Constructors
| 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
Instances
The current context.
Constructors
| FreeEnv | |
Fields
| |
Instances
| LensModality (FreeEnv' a b c) Source # | |
Defined in Agda.TypeChecking.Free.Base | |
| LensQuantity (FreeEnv' a b c) Source # | |
Defined in Agda.TypeChecking.Free.Base | |
| LensRelevance (FreeEnv' a b c) Source # | |
Defined in Agda.TypeChecking.Free.Base | |
| LensFlexRig (FreeEnv' a b c) a Source # | |
Defined in Agda.TypeChecking.Free.Base | |
data IgnoreSorts Source #
Where should we skip sorts in free variable analysis?
Constructors
| IgnoreNot | Do not skip. |
| IgnoreInAnnotations | Skip when annotation to a type. |
| IgnoreAll | Skip unconditionally. |
Instances
| Show IgnoreSorts Source # | |
Defined in Agda.TypeChecking.Free.Base Methods showsPrec :: Int -> IgnoreSorts -> ShowS # show :: IgnoreSorts -> String # showList :: [IgnoreSorts] -> ShowS # | |
| Eq IgnoreSorts Source # | |
Defined in Agda.TypeChecking.Free.Base | |
class (Singleton MetaId a, Monoid a, 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.
Methods
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 () FlexRigMap Source # | Compose everything with the |
Defined in Agda.TypeChecking.Free.Base Methods withVarOcc :: VarOcc' () -> FlexRigMap -> FlexRigMap Source # | |
| IsVarSet () VarCounts Source # | |
Defined in Agda.TypeChecking.Free.Base | |
| IsVarSet () AllowedVar Source # | |
Defined in Agda.TypeChecking.MetaVars.Occurs Methods withVarOcc :: VarOcc' () -> AllowedVar -> AllowedVar Source # | |
| (Singleton MetaId a, Monoid a) => IsVarSet a (VarMap' a) Source # | |
Defined in Agda.TypeChecking.Free.Base | |
class LensFlexRig o a | o -> a where Source #
Methods
lensFlexRig :: Lens' o (FlexRig' a) Source #
Instances
| LensFlexRig (FlexRig' a) a Source # | |
Defined in Agda.TypeChecking.Free.Base | |
| LensFlexRig (VarOcc' a) a Source # | Access to |
Defined in Agda.TypeChecking.Free.Base | |
| LensFlexRig (FreeEnv' a b c) a Source # | |
Defined in Agda.TypeChecking.Free.Base | |
Constructors
| VarMap | |
Fields
| |
Instances
| (Singleton MetaId a, Monoid a) => IsVarSet a (VarMap' a) Source # | |
Defined in Agda.TypeChecking.Free.Base | |
| Singleton Variable (VarMap' a) Source # | A "set"-style |
| PrettyTCM a => PrettyTCM (VarMap' a) Source # | |
Defined in Agda.TypeChecking.Pretty | |
| Semigroup a => Monoid (VarMap' a) Source # | |
| Semigroup a => Semigroup (VarMap' a) Source # | Proper monoid instance for |
| Show a => Show (VarMap' a) Source # | |
| Eq a => Eq (VarMap' a) Source # | |
Occurrence of free variables is classified by several dimensions.
Currently, we have FlexRig and Modality.
Constructors
| VarOcc | |
Fields
| |
Instances
| LensModality (VarOcc' a) Source # | |
Defined in Agda.TypeChecking.Free.Base | |
| LensQuantity (VarOcc' a) Source # | |
Defined in Agda.TypeChecking.Free.Base | |
| LensRelevance (VarOcc' a) Source # | |
Defined in Agda.TypeChecking.Free.Base | |
| Pretty a => Pretty (VarOcc' a) Source # | |
| PrettyTCM a => PrettyTCM (VarOcc' a) Source # | |
Defined in Agda.TypeChecking.Pretty | |
| 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 |
| 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
|
| Show a => Show (VarOcc' a) Source # | |
| Eq a => Eq (VarOcc' a) Source # | Equality up to origin. |
| LensFlexRig (VarOcc' a) a Source # | Access to |
Defined in Agda.TypeChecking.Free.Base | |
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.
mapVarMap :: (TheVarMap' a -> TheVarMap' b) -> VarMap' a -> VarMap' b Source #
Legacy API
flexibleVars :: VarMap -> IntMap MetaSet 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.
freeVarMap :: Free t => t -> VarMap Source #
Return information about every free variable.
isFlexible :: LensFlexRig o a => o -> Bool Source #
isStronglyRigid :: LensFlexRig o a => o -> Bool Source #
isUnguarded :: LensFlexRig o a => o -> Bool Source #
isWeaklyRigid :: LensFlexRig o a => o -> Bool Source #
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.
MetaSet
A set of meta variables. Forms a monoid under union.
Constructors
| MetaSet | |
Fields | |
foldrMetaSet :: (MetaId -> a -> a) -> a -> MetaSet -> a Source #
metaSetToBlocker :: MetaSet -> Blocker Source #
Specialized traversals
allFreeVar :: Free t => (Int -> Bool) -> t -> Bool Source #
Compute the conjunction of a predicate on free variables.
allFreeVarIgnoreAll :: Free t => (Int -> Bool) -> t -> Bool Source #
Same as allFreeVar except occurrences in sorts of types are ignored.
anyFreeVar :: Free t => (Int -> Bool) -> t -> Bool Source #
Compute the disjunction of a predicate on free variables.
anyFreeVarIgnoreAll :: (Int -> Bool) -> Term -> Bool Source #
Same as anyFreeVar except occurrences in sorts of types are ignored.
flexRigOccurrenceIn :: Free a => Nat -> a -> Maybe FlexRig Source #
Compute FlexRig for a single variable.
freeInIgnoringSorts :: Free a => Nat -> a -> Bool Source #
Check if a single variable occurs freely outside of sorts of types.
freeVarCounts :: Free t => t -> VarCounts Source #
Return how many times each free variable occurs.
freeVarList :: Free t => t -> [Int] Source #
Compute a (possibly non-unique) list of free variables, in preorder traversal order.
freeVarMapIgnoreAnn :: Free t => t -> VarMap Source #
Return information about every free variable, but ignore occurrences in sorts of types.
freeVarSet :: Free t => t -> VarSet Source #
Compute the set of free variables.
isBinderUsed :: Free a => Abs a -> Bool Source #
Is the variable bound by the abstraction actually used?