| Safe Haskell | None |
|---|---|
| Language | Haskell98 |
Agda.TypeChecking.Polarity
Contents
- (/\) :: Polarity -> Polarity -> Polarity
- neg :: Polarity -> Polarity
- composePol :: Polarity -> Polarity -> Polarity
- polFromOcc :: Occurrence -> Polarity
- nextPolarity :: [Polarity] -> (Polarity, [Polarity])
- purgeNonvariant :: [Polarity] -> [Polarity]
- computePolarity :: QName -> TCM ()
- enablePhantomTypes :: Defn -> [Polarity] -> [Polarity]
- dependentPolarity :: Type -> [Polarity] -> TCM [Polarity]
- relevantInIgnoringNonvariant :: Nat -> Type -> [Polarity] -> TCM Bool
- mkUnused :: Relevance -> Relevance
- nonvariantToUnusedArg :: [Polarity] -> Type -> TCM Type
- nonvariantToUnusedArgInDef :: [Polarity] -> Defn -> Defn
- nonvariantToUnusedArgInClause :: [Polarity] -> Clause -> Clause
- sizePolarity :: QName -> [Polarity] -> TCM [Polarity]
- checkSizeIndex :: QName -> Nat -> Nat -> Type -> TCM Bool
- class HasPolarity a where
- polarities :: Nat -> a -> TCM [Polarity]
- polarity :: HasPolarity a => Nat -> a -> TCM Polarity
Polarity lattice.
(/\) :: Polarity -> Polarity -> Polarity Source
Infimum on the information lattice.
Invariant is bottom (dominant for inf),
Nonvariant is top (neutral for inf).
composePol :: Polarity -> Polarity -> Polarity Source
What is the polarity of a function composition?
polFromOcc :: Occurrence -> Polarity Source
Auxiliary functions
nextPolarity :: [Polarity] -> (Polarity, [Polarity]) Source
Get the next polarity from a list, Invariant if empty.
purgeNonvariant :: [Polarity] -> [Polarity] Source
Replace Nonvariant by Invariant.
Computing the polarity of a symbol.
computePolarity :: QName -> TCM () Source
Main function of this module.
enablePhantomTypes :: Defn -> [Polarity] -> [Polarity] Source
Data and record parameters are used as phantom arguments all over
the test suite (and possibly in user developments).
enablePhantomTypes turns Nonvariant parameters to Invariant
to enable phantoms.
dependentPolarity :: Type -> [Polarity] -> TCM [Polarity] Source
Make arguments Invariant if the type of a not-Nonvariant
later argument depends on it.
relevantInIgnoringNonvariant :: Nat -> Type -> [Polarity] -> TCM Bool Source
Check whether a variable is relevant in a type expression, ignoring domains of non-variant arguments.
Turn polarity Nonvariant into relevance UnusedArg
mkUnused :: Relevance -> Relevance Source
Record information that an argument is unused in Relevance.
nonvariantToUnusedArg :: [Polarity] -> Type -> TCM Type Source
Improve Relevance information in a type by polarity information.
Nonvariant becomes UnusedArg.
nonvariantToUnusedArgInDef :: [Polarity] -> Defn -> Defn Source
Propagate Nonvariant Polarity to Relevance information in
Args of a defined symbol.
nonvariantToUnusedArgInClause :: [Polarity] -> Clause -> Clause Source
Sized types
checkSizeIndex :: QName -> Nat -> Nat -> Type -> TCM Bool Source
checkSizeIndex d np i a checks that constructor target type a
has form d ps (↑ i) idxs where |ps| = np.
Precondition: a is reduced and of form d ps idxs0.
class HasPolarity a where Source
polarities i a computes the list of polarities of de Bruijn index i
in syntactic entity a.
Methods
polarities :: Nat -> a -> TCM [Polarity] Source
Instances
| HasPolarity LevelAtom | |
| HasPolarity PlusLevel | |
| HasPolarity Level | |
| HasPolarity Type | |
| HasPolarity Term | |
| HasPolarity a => HasPolarity [a] | |
| HasPolarity a => HasPolarity (Abs a) | |
| HasPolarity a => HasPolarity (Elim' a) | |
| HasPolarity a => HasPolarity (Dom a) | |
| HasPolarity a => HasPolarity (Arg a) | |
| (HasPolarity a, HasPolarity b) => HasPolarity (a, b) |
polarity :: HasPolarity a => Nat -> a -> TCM Polarity Source
polarity i a computes the polarity of de Bruijn index i
in syntactic entity a by taking the infimum of all polarities.