| 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
- 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
Documentation
Free variables of a term, (disjointly) partitioned into strongly and and weakly rigid variables, flexible variables and irrelevant variables.
Constructors
| FV | |
Fields
| |
Instances
| Eq FreeVars # | |
| Show FreeVars # | |
| Semigroup FreeVars # | Free variable sets form a monoid under |
| Monoid FreeVars # | |
| Null FreeVars # | |
| IsVarSet FreeVars # | |
Defined in Agda.TypeChecking.Free Methods withVarOcc :: VarOcc -> FreeVars -> FreeVars # | |
| Singleton Variable FreeVars # | |
Defined in Agda.TypeChecking.Free | |
Gather free variables in a collection.
Minimal complete definition
Instances
| Free EqualityView # | |
Defined in Agda.TypeChecking.Free.Lazy Methods freeVars' :: IsVarSet c => EqualityView -> FreeM c # | |
| Free Clause # | |
| Free LevelAtom # | |
| Free PlusLevel # | |
| Free Level # | |
| Free Sort # | |
| Free Term # | |
| Free Candidate # | |
| Free NLPType # | |
| Free NLPat # | |
| Free DisplayTerm # | |
Defined in Agda.TypeChecking.Monad.Base Methods freeVars' :: IsVarSet c => DisplayTerm -> FreeM c # | |
| Free DisplayForm # | |
Defined in Agda.TypeChecking.Monad.Base Methods freeVars' :: IsVarSet c => DisplayForm -> FreeM c # | |
| Free Constraint # | |
Defined in Agda.TypeChecking.Monad.Base Methods freeVars' :: IsVarSet c => Constraint -> FreeM c # | |
| Free a => Free [a] # | |
Defined in Agda.TypeChecking.Free.Lazy | |
| Free a => Free (Maybe a) # | |
| Free a => Free (Dom a) # | |
| Free a => Free (Arg a) # | |
| Free a => Free (Tele a) # | |
| Free a => Free (Type' a) # | |
| Free a => Free (Abs a) # | |
| Free a => Free (Elim' a) # | |
| (Free a, Free b) => Free (a, b) # | |
Defined in Agda.TypeChecking.Free.Lazy | |
class (Semigroup a, Monoid a) => IsVarSet a where #
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`.
Minimal complete definition
Methods
withVarOcc :: VarOcc -> a -> a #
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 # | |
Defined in Agda.TypeChecking.Free Methods withVarOcc :: VarOcc -> All -> All # | |
| IsVarSet Any # | |
Defined in Agda.TypeChecking.Free Methods withVarOcc :: VarOcc -> Any -> Any # | |
| IsVarSet VarMap # | |
Defined in Agda.TypeChecking.Free.Lazy Methods withVarOcc :: VarOcc -> VarMap -> VarMap # | |
| IsVarSet VarCounts # | |
Defined in Agda.TypeChecking.Free Methods withVarOcc :: VarOcc -> VarCounts -> VarCounts # | |
| IsVarSet FreeVars # | |
Defined in Agda.TypeChecking.Free Methods withVarOcc :: VarOcc -> FreeVars -> FreeVars # | |
| IsVarSet [Int] # | |
Defined in Agda.TypeChecking.Free Methods withVarOcc :: VarOcc -> [Int] -> [Int] # | |
data IgnoreSorts #
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 # | |
Defined in Agda.TypeChecking.Free.Lazy | |
| Show IgnoreSorts # | |
Defined in Agda.TypeChecking.Free.Lazy Methods showsPrec :: Int -> IgnoreSorts -> ShowS # show :: IgnoreSorts -> String # showList :: [IgnoreSorts] -> ShowS # | |
rigidVars :: FreeVars -> VarSet #
Rigid variables: either strongly rigid, unguarded, or weakly rigid.
relevantVars :: FreeVars -> VarSet #
All but the irrelevant variables.
allFreeVars :: Free a => a -> VarSet #
Collect all free variables.
allFreeVarsWithOcc :: Free a => a -> TheVarMap #
Collect all free variables together with information about their occurrence.
allRelevantVars :: Free a => a -> VarSet #
Collect all relevant free variables, excluding the "unused" ones.
allRelevantVarsIgnoring :: Free a => IgnoreSorts -> a -> VarSet #
Collect all relevant free variables, possibly ignoring sorts.
freeInIgnoringSorts :: Free a => Nat -> a -> Bool #
isBinderUsed :: Free a => Abs a -> Bool #
Is the variable bound by the abstraction actually used?
relevantIn :: Free a => Nat -> a -> Bool #
relevantInIgnoringSortAnn :: Free a => Nat -> a -> Bool #
data Occurrence #
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 # | |
Defined in Agda.TypeChecking.Free | |
| Show Occurrence # | |
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 #
Compute an occurrence of a single variable in a piece of internal syntax.
freeVars :: (IsVarSet c, Singleton Variable c, Free a) => a -> c #
Doesn't go inside solved metas, but collects the variables from a
metavariable application X ts as flexibleVars.