| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.TypeChecking.Free.Lazy
Contents
Description
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.
Worst-case complexity does not change (i.e. the case when a variable
does not occur), but best case-complexity does matter. For instance,
see mkAbs: each time we construct
a dependent function type, we check 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).
Synopsis
- type MetaSet = Set MetaId
- data FlexRig
- composeFlexRig :: FlexRig -> FlexRig -> FlexRig
- data VarOcc = VarOcc {}
- maxVarOcc :: VarOcc -> VarOcc -> VarOcc
- topVarOcc :: VarOcc
- botVarOcc :: VarOcc
- composeVarOcc :: VarOcc -> VarOcc -> VarOcc
- class (Semigroup a, Monoid a) => IsVarSet a where
- type TheVarMap = IntMap VarOcc
- newtype VarMap = VarMap {}
- mapVarMap :: (TheVarMap -> TheVarMap) -> VarMap -> VarMap
- data IgnoreSorts
- data FreeEnv c = FreeEnv {
- feIgnoreSorts :: !IgnoreSorts
- feFlexRig :: !FlexRig
- feRelevance :: !Relevance
- feSingleton :: Maybe Variable -> c
- type Variable = Int
- type SingleVar c = Variable -> c
- initFreeEnv :: Monoid c => SingleVar c -> FreeEnv c
- type FreeM c = Reader (FreeEnv c) c
- runFreeM :: IsVarSet c => SingleVar c -> IgnoreSorts -> FreeM c -> c
- variable :: IsVarSet c => Int -> FreeM c
- subVar :: Int -> Maybe Variable -> Maybe Variable
- bind :: FreeM a -> FreeM a
- bind' :: Nat -> FreeM a -> FreeM a
- go :: FlexRig -> FreeM a -> FreeM a
- goRel :: Relevance -> FreeM a -> FreeM a
- underConstructor :: ConHead -> FreeM a -> FreeM a
- class Free a where
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 MetaSet | 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. |
| StronglyRigid | Under at least one and only inductive constructors. |
composeFlexRig :: FlexRig -> FlexRig -> FlexRig #
FlexRig composition. For accumulating the context of a variable.
Flexible is dominant. Once we are under a meta, we are flexible
regardless what else comes.
WeaklyRigid is next in strength. Destroys strong rigidity.
StronglyRigid is still dominant over Unguarded.
Unguarded is the unit. It is the top (identity) context.
Occurrence of free variables is classified by several dimensions.
Currently, we have FlexRig and Relevance.
Constructors
| VarOcc | |
Fields | |
maxVarOcc :: VarOcc -> VarOcc -> VarOcc #
When we extract information about occurrence, we care most about
about StronglyRigid Relevant occurrences.
composeVarOcc :: VarOcc -> VarOcc -> VarOcc #
First argument is the outer occurrence and second is the inner.
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] # | |
Instances
| Show VarMap # | |
| Semigroup VarMap # | |
| Monoid VarMap # | Proper monoid instance for |
| IsVarSet VarMap # | |
Defined in Agda.TypeChecking.Free.Lazy Methods withVarOcc :: VarOcc -> VarMap -> VarMap # | |
| Singleton (Variable, VarOcc) VarMap # | |
Collecting free variables.
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 # | |
The current context.
Constructors
| FreeEnv | |
Fields
| |
initFreeEnv :: Monoid c => SingleVar c -> FreeEnv c #
The initial context.
subVar :: Int -> Maybe Variable -> Maybe Variable #
Subtract, but return Nothing if result is negative.
underConstructor :: ConHead -> FreeM a -> FreeM a #
What happens to the variables occurring under a constructor?
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 | |