| 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).
Synopsis
- data FreeVars = FV {
- stronglyRigidVars :: VarSet
- unguardedVars :: VarSet
- weaklyRigidVars :: VarSet
- flexibleVars :: IntMap MetaSet
- irrelevantVars :: VarSet
- newtype VarCounts = VarCounts {}
- class Free a
- class (Semigroup a, Monoid a) => IsVarSet a where
- withVarOcc :: VarOcc -> a -> a
- data IgnoreSorts
- runFree :: (IsVarSet c, Free a) => SingleVar c -> IgnoreSorts -> a -> c
- rigidVars :: FreeVars -> VarSet
- relevantVars :: FreeVars -> VarSet
- allVars :: FreeVars -> VarSet
- allFreeVars :: Free a => a -> VarSet
- allFreeVarsWithOcc :: Free a => a -> TheVarMap
- allRelevantVars :: Free a => a -> VarSet
- allRelevantVarsIgnoring :: Free a => IgnoreSorts -> a -> VarSet
- freeIn :: Free a => Nat -> a -> Bool
- freeInIgnoringSorts :: Free a => Nat -> a -> Bool
- isBinderUsed :: Free a => Abs a -> Bool
- relevantIn :: Free a => Nat -> a -> Bool
- relevantInIgnoringSortAnn :: Free a => Nat -> a -> Bool
- data Occurrence
- data VarOcc = VarOcc {}
- occurrence :: Free a => Nat -> a -> Occurrence
- closed :: Free a => a -> Bool
- freeVars :: (IsVarSet c, Singleton Variable c, Free a) => a -> c
- freeVars' :: (Free a, IsVarSet c) => a -> FreeM c
- type MetaSet = Set MetaId
Documentation
Free variables of a term, (disjointly) partitioned into strongly and and weakly rigid variables, flexible variables and irrelevant variables.
Constructors
| FV | |
Fields
| |
Gather free variables in a collection.
Minimal complete definition
Instances
| Free EqualityView Source # | |
Defined in Agda.TypeChecking.Free.Lazy | |
| Free Clause Source # | |
| Free LevelAtom Source # | |
| Free PlusLevel Source # | |
| Free Level Source # | |
| Free Sort Source # | |
| Free Term Source # | |
| Free Candidate Source # | |
| Free NLPType Source # | |
| Free NLPat Source # | |
| Free DisplayTerm Source # | |
Defined in Agda.TypeChecking.Monad.Base | |
| Free DisplayForm Source # | |
Defined in Agda.TypeChecking.Monad.Base | |
| Free Constraint Source # | |
Defined in Agda.TypeChecking.Monad.Base | |
| Free a => Free [a] Source # | |
| Free a => Free (Maybe a) Source # | |
| Free a => Free (Dom a) Source # | |
| Free a => Free (Arg a) Source # | |
| Free a => Free (Tele a) Source # | |
| Free a => Free (Type' a) Source # | |
| Free a => Free (Abs a) Source # | |
| Free a => Free (Elim' a) Source # | |
| (Free a, Free b) => Free (a, b) Source # | |
class (Semigroup a, Monoid a) => IsVarSet a where Source #
Any representation 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`.
Methods
withVarOcc :: VarOcc -> a -> a Source #
Laws * Respects monoid operations: ``` withVarOcc o mempty == mempty withVarOcc o (x <> y) == withVarOcc o x <> withVarOcc o y ``` * Respects VarOcc composition ``` withVarOcc (composeVarOcc o1 o2) = withVarOcc o1 . withVarOcc o2 ```
Instances
| IsVarSet All Source # | |
Defined in Agda.TypeChecking.Free | |
| IsVarSet Any Source # | |
Defined in Agda.TypeChecking.Free | |
| IsVarSet VarMap Source # | |
Defined in Agda.TypeChecking.Free.Lazy | |
| IsVarSet VarCounts Source # | |
Defined in Agda.TypeChecking.Free | |
| IsVarSet FreeVars Source # | |
Defined in Agda.TypeChecking.Free | |
| IsVarSet [Int] Source # | |
Defined in Agda.TypeChecking.Free | |
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
| Eq IgnoreSorts Source # | |
Defined in Agda.TypeChecking.Free.Lazy | |
| Show IgnoreSorts Source # | |
Defined in Agda.TypeChecking.Free.Lazy Methods showsPrec :: Int -> IgnoreSorts -> ShowS # show :: IgnoreSorts -> String # showList :: [IgnoreSorts] -> ShowS # | |
runFree :: (IsVarSet c, Free a) => SingleVar c -> IgnoreSorts -> a -> c Source #
Compute free variables.
rigidVars :: FreeVars -> VarSet Source #
Rigid variables: either strongly rigid, unguarded, or weakly rigid.
relevantVars :: FreeVars -> VarSet Source #
All but the irrelevant variables.
allFreeVars :: Free a => a -> VarSet Source #
Collect all free variables.
allFreeVarsWithOcc :: Free a => a -> TheVarMap Source #
Collect all free variables together with information about their occurrence.
allRelevantVars :: Free a => a -> VarSet Source #
Collect all relevant free variables, excluding the "unused" ones.
allRelevantVarsIgnoring :: Free a => IgnoreSorts -> a -> 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?
data Occurrence Source #
Constructors
| NoOccurrence | |
| Irrelevantly | |
| StronglyRigid | Under at least one and only inductive constructors. |
| Unguarded | In top position, or only under inductive record constructors. |
| WeaklyRigid | In arguments to variables and definitions. |
| Flexible MetaSet | In arguments of metas. |
Instances
| Eq Occurrence Source # | |
Defined in Agda.TypeChecking.Free | |
| Show Occurrence Source # | |
Defined in Agda.TypeChecking.Free Methods showsPrec :: Int -> Occurrence -> ShowS # show :: Occurrence -> String # showList :: [Occurrence] -> ShowS # | |
Occurrence of free variables is classified by several dimensions.
Currently, we have FlexRig and Relevance.
Constructors
| VarOcc | |
Fields | |
occurrence :: Free a => Nat -> a -> Occurrence Source #
Compute an occurrence of a single variable in a piece of internal syntax.
freeVars :: (IsVarSet c, Singleton Variable c, Free a) => a -> c Source #
Doesn't go inside solved metas, but collects the variables from a
metavariable application X ts as flexibleVars.