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

Safe Haskell | None
Language | Haskell2010

Agda.TypeChecking.Sort

Description

This module contains the rules for Agda's sort system viewed as a pure type system (pts). The specification of a pts consists of a set of axioms of the form `s1 : s2` specifying when a sort fits in another sort, and a set of rules of the form `(s1,s2,s3)` specifying that a pi type with domain in `s1` and codomain in `s2` itself fits into sort `s3`.

To ensure unique principal types, the axioms and rules of Agda's pts are given by two partial functions `univSort'` and `piSort'` (see `Agda.TypeChecking.Substitute`). If these functions return `Nothing`, a constraint is added to ensure that the sort will be computed eventually.

One `upgrade` over the standard definition of a pts is that in a rule `(s1,s2,s3)`, in Agda the sort `s2` can depend on a variable of some type in `s1`. This is needed to support Agda's universe polymorphism where we can have e.g. a function of type `∀ {ℓ} → Set ℓ`.

Synopsis

- inferUnivSort :: (PureTCM m, MonadConstraint m) => Sort -> m Sort
- sortFitsIn :: MonadConversion m => Sort -> Sort -> m ()
- hasBiggerSort :: Sort -> TCM ()
- inferPiSort :: (PureTCM m, MonadConstraint m) => Dom Type -> Abs Sort -> m Sort
- inferFunSort :: (PureTCM m, MonadConstraint m) => Dom Type -> Sort -> m Sort
- hasPTSRule :: Dom Type -> Abs Sort -> TCM ()
- checkTelePiSort :: Type -> TCM ()
- ifIsSort :: (MonadReduce m, MonadBlock m) => Type -> (Sort -> m a) -> m a -> m a
- ifNotSort :: (MonadReduce m, MonadBlock m) => Type -> m a -> (Sort -> m a) -> m a
- shouldBeSort :: (PureTCM m, MonadBlock m, MonadError TCErr m) => Type -> m Sort
- sortOf :: (PureTCM m, MonadBlock m, MonadConstraint m) => Term -> m Sort
- sortOfType :: (PureTCM m, MonadBlock m, MonadConstraint m) => Type -> m Sort

# Documentation

inferUnivSort :: (PureTCM m, MonadConstraint m) => Sort -> m Sort Source #

Infer the sort of another sort. If we can compute the bigger sort straight away, return that. Otherwise, return `UnivSort s` and add a constraint to ensure we can compute the sort eventually.

sortFitsIn :: MonadConversion m => Sort -> Sort -> m () Source #

hasBiggerSort :: Sort -> TCM () Source #

inferPiSort Source #

Arguments

:: (PureTCM m, MonadConstraint m) |
=> Dom Type | Domain of the Pi type.
-> Abs Sort | (Dependent) sort of the codomain of the Pi type.
-> m Sort | Sort of the Pi type.

Infer the sort of a Pi type. If we can compute the sort straight away, return that. Otherwise, return a `PiSort` and add a constraint to ensure we can compute the sort eventually.

inferFunSort Source #

Arguments

:: (PureTCM m, MonadConstraint m) |
=> Dom Type | Domain of the function type.
-> Sort | Sort of the codomain of the function type.
-> m Sort | Sort of the function type.

As `inferPiSort`, but for a nondependent function type.

hasPTSRule :: Dom Type -> Abs Sort -> TCM () Source #

`hasPTSRule a x.s` checks that we can form a Pi-type `(x : a) -> b` where `b : s`.

checkTelePiSort :: Type -> TCM () Source #

Recursively check that an iterated function type constructed by `telePi` is well-sorted.

ifIsSort :: (MonadReduce m, MonadBlock m) => Type -> (Sort -> m a) -> m a -> m a Source #

ifNotSort :: (MonadReduce m, MonadBlock m) => Type -> m a -> (Sort -> m a) -> m a Source #

shouldBeSort :: (PureTCM m, MonadBlock m, MonadError TCErr m) => Type -> m Sort Source #

Result is in reduced form.

sortOf :: (PureTCM m, MonadBlock m, MonadConstraint m) => Term -> m Sort Source #

Reconstruct the sort of a term.

Precondition: given term is a well-sorted type.

sortOfType :: (PureTCM m, MonadBlock m, MonadConstraint m) => Type -> m Sort Source #

Reconstruct the minimal sort of a type (ignoring the sort annotation).