| Safe Haskell | Safe-Inferred |
|---|---|
| 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 :: forall m. (PureTCM m, MonadBlock m, MonadConstraint m) => Term -> m Sort
- sortOfType :: forall m. (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 #
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.
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 :: forall m. (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 :: forall m. (PureTCM m, MonadBlock m, MonadConstraint m) => Type -> m Sort Source #
Reconstruct the minimal sort of a type (ignoring the sort annotation).