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.

checkDataSort :: QName -> Sort -> TCM ()

Make sure that the target universe admits data type definitions. E.g. IUniv, SizeUniv etc. do not accept new constructions.

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

defineTranspIx

Arguments

:: QName

datatype name

-> TCM (Maybe QName)

Defines and returns the name of the transpIx function.

defineTranspFun

Arguments

:: QName

datatype

-> Maybe QName

transpX "constructor"

-> [QName]

constructor names

-> [QName]

path cons

-> TCM (Maybe QName)

defineConClause

Arguments

:: QName

trD

-> Bool

HIT

-> Maybe QName

trX

-> Nat

npars = size Δ

-> Nat

nixs = size X

-> Telescope

Δ ⊢ X

-> Telescope

(Δ.X)^I

-> Substitution

(Δ.X)^I, i : I ⊢ σ : Δ.X

-> Type

(Δ.X)^I, i : I ⊢ D[δ i,x i] -- datatype

-> [QName]

Constructors

-> TCM [Clause]

defineKanOperationForFields

Arguments

:: Command

-> 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)

((name, tel, rtype, clause_types, bodies), sigma) name: name of transport function for this constructor/record. clauses still missing. tel: Ξ telescope for the RHS, Ξ ⊃ (Δ^I, φ : I), also Ξ ⊢ us0 : Φ[δ 0] rtype: Ξ ⊢ T' := T[δ 1] clause_types: Ξ ⊢ Φ' := Φ[δ 1] bodies: Ξ ⊢ us1 : Φ' sigma: Ξ, i : I ⊢ σ : Δ.Φ -- line [δ 0,us0] ≡ [δ 0,us1]

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.

When --without-K is active and the type is fibrant the procedure also checks that the type is usable at the current modality. See #4784 and #5434.

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

Show IsPathCons

Defined in Agda.TypeChecking.Rules.Data

Methods

showsPrec :: Int -> IsPathCons -> ShowS

show :: IsPathCons -> String

showList :: [IsPathCons] -> ShowS

Eq IsPathCons

Defined in Agda.TypeChecking.Rules.Data

Methods

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

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

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.