Agda.TypeChecking.Rules.Data

Datatypes

checkDataDef :: DefInfo -> QName -> UniverseCheck -> DataDefParams -> [Constructor] -> TCM ()

Type check a datatype definition. Assumes that the type has already been checked.

forceSort :: Type -> TCM Sort

Ensure that the type is a sort. If it is not directly a sort, compare it to a newSortMetaBelowInf.

checkConstructor

Arguments

:: QName

Name of data type.

-> UniverseCheck

Check universes?

-> Telescope

Parameter telescope.

-> Nat

Number of indices of the data type.

-> Sort

Sort of the data type.

-> Constructor

Constructor declaration (type signature).

-> TCM IsPathCons

Type check a constructor declaration. Checks that the constructor targets the datatype and that it fits inside the declared sort. Returns the non-linear parameters.

defineCompData :: QName -> ConHead -> Telescope -> [QName] -> Telescope -> Type -> Boundary -> TCM CompKit

defineProjections :: QName -> ConHead -> Telescope -> [QName] -> Telescope -> Type -> TCM ()

Define projections for non-indexed data types (families don't work yet). Of course, these projections are partial functions in general.

Precondition: we are in the context Γ of the data type parameters.

freshAbstractQName'_ :: String -> TCM QName

Special cases of Type

data LType

A Type with sort Type l Such a type supports both hcomp and transp.

Constructors

LEl Level Term

Instances

Eq LType

Defined in Agda.TypeChecking.Rules.Data

Methods

(==) :: LType -> LType -> Bool

(/=) :: LType -> LType -> Bool

Show LType

Defined in Agda.TypeChecking.Rules.Data

Methods

showsPrec :: Int -> LType -> ShowS

show :: LType -> String

showList :: [LType] -> ShowS

Subst Term LType

Defined in Agda.TypeChecking.Rules.Data

Methods

applySubst :: Substitution' Term -> LType -> LType

fromLType :: LType -> Type

lTypeLevel :: LType -> Level

toLType :: MonadReduce m => Type -> m (Maybe LType)

data CType

A Type that either has sort Type l or is a closed definition. Such a type supports some version of transp. In particular we want to allow the Interval as a ClosedType.

Constructors

ClosedType QName

LType LType

Instances

Eq CType

Defined in Agda.TypeChecking.Rules.Data

Methods

(==) :: CType -> CType -> Bool

(/=) :: CType -> CType -> Bool

Show CType

Defined in Agda.TypeChecking.Rules.Data

Methods

showsPrec :: Int -> CType -> ShowS

show :: CType -> String

showList :: [CType] -> ShowS

Subst Term CType

Defined in Agda.TypeChecking.Rules.Data

Methods

applySubst :: Substitution' Term -> CType -> CType

fromCType :: CType -> Type

toCType :: MonadReduce m => Type -> m (Maybe CType)

defineTranspOrHCompForFields

Arguments

:: TranspOrHComp

-> Maybe Term

PathCons, Δ.Φ ⊢ u : R δ

-> (Term -> QName -> Term)

how to apply a "projection" to a term

-> QName

some name, e.g. record name

-> Telescope

param types Δ

-> Telescope

fields' types Δ ⊢ Φ

-> [Arg QName]

fields' names

-> Type

record type Δ ⊢ T

-> TCM (Maybe ((QName, Telescope, Type, [Dom Type], [Term]), Substitution))

defineTranspForFields

Arguments

:: Maybe Term

PathCons, Δ.Φ ⊢ u : R δ

-> (Term -> QName -> Term)

how to apply a "projection" to a term

-> QName

some name, e.g. record name

-> Telescope

param types Δ

-> Tele (Dom CType)

fields' types Δ ⊢ Φ

-> [Arg QName]

fields' names

-> Type

record type Δ ⊢ T

-> TCM ((QName, Telescope, Type, [Dom Type], [Term]), Substitution)

defineHCompForFields

Arguments

:: (Term -> QName -> Term)

how to apply a "projection" to a term

-> QName

some name, e.g. record name

-> Telescope

param types Δ

-> Tele (Dom LType)

fields' types Δ ⊢ Φ

-> [Arg QName]

fields' names

-> LType

record type (δ : Δ) ⊢ R[δ]

-> TCM ((QName, Telescope, Type, [Dom Type], [Term]), Substitution)

getGeneralizedParameters :: Set Name -> QName -> TCM [Maybe Name]

bindGeneralizedParameters :: [Maybe Name] -> Type -> (Telescope -> Type -> TCM a) -> TCM a

Bind the named generalized parameters.

bindParameters

Arguments

:: Int

Number of parameters

-> [LamBinding]

Bindings from definition site.

-> Type

Pi-type of bindings coming from signature site.

-> (Telescope -> Type -> TCM a)

Continuation, accepting parameter telescope and rest of type. The parameters are part of the context when the continutation is invoked.

-> TCM a

Bind the parameters of a datatype.

We allow omission of hidden parameters at the definition site. Example: data D {a} (A : Set a) : Set a data D A where c : A -> D A

bindParameter :: Int -> [LamBinding] -> Name -> Dom Type -> Abs Type -> (Telescope -> Type -> TCM a) -> TCM a

fitsIn :: UniverseCheck -> [IsForced] -> Type -> Sort -> TCM Int

Check that the arguments to a constructor fits inside the sort of the datatype. The third argument is the type of the constructor.

As a side effect, return the arity of the constructor.

checkIndexSorts :: Sort -> Telescope -> TCM ()

When --without-K is enabled, we should check that the sorts of the index types fit into the sort of the datatype.

data IsPathCons

Return the parameters that share variables with the indices nonLinearParameters :: Int -> Type -> TCM [Int] nonLinearParameters nPars t =

Constructors

PathCons

PointCons

Instances

Eq IsPathCons

Defined in Agda.TypeChecking.Rules.Data

Methods

(==) :: IsPathCons -> IsPathCons -> Bool

(/=) :: IsPathCons -> IsPathCons -> Bool

Show IsPathCons

Defined in Agda.TypeChecking.Rules.Data

Methods

showsPrec :: Int -> IsPathCons -> ShowS

show :: IsPathCons -> String

showList :: [IsPathCons] -> ShowS

constructs :: Int -> Int -> Type -> QName -> TCM IsPathCons

Check that a type constructs something of the given datatype. The first argument is the number of parameters to the datatype and the second the number of additional non-parameters in the context (1 when generalizing, 0 otherwise).

isCoinductive :: Type -> TCM (Maybe Bool)

Is the type coinductive? Returns Nothing if the answer cannot be determined.