Agda-2.3.2: A dependently typed functional programming language and proof assistant

Safe Haskell | None

Agda.TypeChecking.Polarity

Contents

- Polarity lattice.
- Auxiliary functions
- Computing the polarity of a symbol.
- Turn polarity `Nonvariant` into relevance `UnusedArg`
- Sized types

Synopsis

- (/\) :: 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 :: 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

Infimum on the information lattice. `Invariant` is bottom (dominant for inf), `Nonvariant` is top (neutral for inf).

neg :: Polarity -> Polarity

`Polarity` negation, swapping monotone and antitone.

composePol :: Polarity -> Polarity -> Polarity

What is the polarity of a function composition?

polFromOcc :: Occurrence -> Polarity

# Auxiliary functions

nextPolarity :: [Polarity] -> (Polarity, [Polarity])

Get the next polarity from a list, `Invariant` if empty.

purgeNonvariant :: [Polarity] -> [Polarity]

Replace `Nonvariant` by `Invariant`.

# Computing the polarity of a symbol.

computePolarity :: QName -> TCM ()

Main function of this module.

enablePhantomTypes :: Defn -> [Polarity] -> [Polarity]

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]

Make arguments `Invariant` if the type of a not-`Nonvariant` later argument depends on it.

relevantInIgnoringNonvariant :: Nat -> Type -> [Polarity] -> TCM Bool

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

Record information that an argument is unused in `Relevance`.

nonvariantToUnusedArg :: [Polarity] -> Type -> TCM Type

Improve `Relevance` information in a type by polarity information. `Nonvariant` becomes `UnusedArg`.

nonvariantToUnusedArgInDef :: [Polarity] -> Defn -> Defn

Propagate `Nonvariant` `Polarity` to `Relevance` information in `Arg`s of a defined symbol.

nonvariantToUnusedArgInClause :: [Polarity] -> Clause -> Clause

# Sized types

sizePolarity :: QName -> [Polarity] -> TCM [Polarity]

Hack for polarity of size indices.

checkSizeIndex :: Nat -> Nat -> Type -> TCM Bool

class HasPolarity a where

`polarities i a` computes the list of polarities of de Bruijn index `i` in syntactic entity `a`.

Methods

polarities :: Nat -> a -> TCM [Polarity]

Instances

HasPolarity LevelAtom |
HasPolarity PlusLevel |
HasPolarity Level |
HasPolarity Type |
HasPolarity Term |
HasPolarity a => HasPolarity [a] |
HasPolarity a => HasPolarity (Arg a) |
HasPolarity a => HasPolarity (Dom a) |
HasPolarity a => HasPolarity (Abs a) |
(HasPolarity a, HasPolarity b) => HasPolarity (a, b) |

polarity :: HasPolarity a => Nat -> a -> TCM Polarity

`polarity i a` computes the polarity of de Bruijn index `i` in syntactic entity `a` by taking the infimum of all `polarities`.