| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.TypeChecking.Free
Contents
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
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 {
- varCounts :: IntMap Int
- 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
- flexibleVars :: VarMap -> IntMap MetaSet
- allFreeVars :: Free t => t -> VarSet
- allRelevantVars :: Free t => t -> VarSet
- allRelevantVarsIgnoring :: Free t => IgnoreSorts -> t -> VarSet
- freeVarsIgnore :: (IsVarSet a c, Singleton Variable c, Free t) => IgnoreSorts -> t -> c
- 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 o a | o -> a where
- lensFlexRig :: Lens' o (FlexRig' a)
- isFlexible :: LensFlexRig o a => o -> Bool
- isUnguarded :: LensFlexRig o a => o -> Bool
- isStronglyRigid :: LensFlexRig o a => o -> Bool
- isWeaklyRigid :: LensFlexRig o a => 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
- metaSetToBlocker :: MetaSet -> Blocker
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.
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 () VarCounts Source # | |
Defined in Agda.TypeChecking.Free | |
| IsVarSet () FlexRigMap Source # | Compose everything with the |
Defined in Agda.TypeChecking.Free.Lazy Methods withVarOcc :: VarOcc' () -> FlexRigMap -> FlexRigMap Source # | |
| IsVarSet () AllowedVar Source # | |
Defined in Agda.TypeChecking.MetaVars.Occurs Methods withVarOcc :: VarOcc' () -> AllowedVar -> AllowedVar Source # | |
| IsVarSet () All Source # | |
Defined in Agda.TypeChecking.Free Methods withVarOcc :: VarOcc' () -> All -> All Source # | |
| IsVarSet () Any Source # | |
Defined in Agda.TypeChecking.Free Methods withVarOcc :: VarOcc' () -> Any -> Any Source # | |
| IsVarSet () [Int] Source # | |
Defined in Agda.TypeChecking.Free Methods withVarOcc :: VarOcc' () -> [Int] -> [Int] Source # | |
| (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?
Constructors
| IgnoreNot | Do not skip. |
| IgnoreInAnnotations | Skip when annotation to a type. |
| IgnoreAll | Skip unconditionally. |
Instances
| Show IgnoreSorts Source # | |
Defined in Agda.TypeChecking.Free.Lazy Methods showsPrec :: Int -> IgnoreSorts -> ShowS show :: IgnoreSorts -> String showList :: [IgnoreSorts] -> ShowS | |
| Eq IgnoreSorts Source # | |
Defined in Agda.TypeChecking.Free.Lazy | |
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.
filterVarMap :: (VarOcc -> Bool) -> VarMap -> VarSet Source #
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.
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.
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.
freeVarsIgnore :: (IsVarSet a c, Singleton Variable c, Free t) => IgnoreSorts -> t -> c Source #
freeInIgnoringSorts :: Free a => Nat -> a -> Bool Source #
isBinderUsed :: Free a => Abs a -> Bool Source #
Is the variable bound by the abstraction actually used?
relevantIn :: Free t => Nat -> t -> Bool Source #
relevantInIgnoringSortAnn :: Free t => Nat -> t -> Bool Source #
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
| Functor FlexRig' Source # | |
| Foldable FlexRig' Source # | |
Defined in Agda.TypeChecking.Free.Lazy Methods fold :: Monoid m => FlexRig' m -> m foldMap :: Monoid m => (a -> m) -> FlexRig' a -> 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 | |
| Show a => Show (FlexRig' a) Source # | |
| Eq a => Eq (FlexRig' a) Source # | |
| LensFlexRig (FlexRig' a) a Source # | |
Defined in Agda.TypeChecking.Free.Lazy | |
| Singleton (Variable, FlexRig' ()) FlexRigMap Source # | |
Defined in Agda.TypeChecking.Free.Lazy | |
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.Lazy | |
| LensFlexRig (VarOcc' a) a Source # | Access to |
Defined in Agda.TypeChecking.Free.Lazy | |
| LensFlexRig (FreeEnv' a b c) a Source # | |
Defined in Agda.TypeChecking.Free.Lazy | |
isFlexible :: LensFlexRig o a => o -> Bool Source #
isUnguarded :: LensFlexRig o a => o -> Bool Source #
isStronglyRigid :: LensFlexRig o a => o -> Bool Source #
isWeaklyRigid :: LensFlexRig o a => o -> Bool 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.Lazy | |
| LensQuantity (VarOcc' a) Source # | |
Defined in Agda.TypeChecking.Free.Lazy | |
| LensRelevance (VarOcc' a) Source # | |
Defined in Agda.TypeChecking.Free.Lazy | |
| (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 |
| 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.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 #
metaSetToBlocker :: MetaSet -> Blocker Source #