Agda-2.6.2.0.20211129: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.TypeChecking.Rules.Data

Synopsis

Datatypes

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

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

forceSort :: Type -> TCM Sort Source #

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

checkConstructor Source #

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.

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

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.

Special cases of Type

data LType Source #

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

Constructors

LEl Level Term 

Instances

Instances details
Subst LType Source # 
Instance details

Defined in Agda.TypeChecking.Rules.Data

Associated Types

type SubstArg LType Source #

Show LType Source # 
Instance details

Defined in Agda.TypeChecking.Rules.Data

Methods

showsPrec :: Int -> LType -> ShowS #

show :: LType -> String #

showList :: [LType] -> ShowS #

Eq LType Source # 
Instance details

Defined in Agda.TypeChecking.Rules.Data

Methods

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

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

type SubstArg LType Source # 
Instance details

Defined in Agda.TypeChecking.Rules.Data

data CType Source #

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.

Instances

Instances details
Subst CType Source # 
Instance details

Defined in Agda.TypeChecking.Rules.Data

Associated Types

type SubstArg CType Source #

Show CType Source # 
Instance details

Defined in Agda.TypeChecking.Rules.Data

Methods

showsPrec :: Int -> CType -> ShowS #

show :: CType -> String #

showList :: [CType] -> ShowS #

Eq CType Source # 
Instance details

Defined in Agda.TypeChecking.Rules.Data

Methods

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

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

type SubstArg CType Source # 
Instance details

Defined in Agda.TypeChecking.Rules.Data

defineTranspOrHCompForFields Source #

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 Source #

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 Source #

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) 

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

Bind the named generalized parameters.

bindParameters Source #

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 Source #

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

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 () Source #

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

data IsPathCons Source #

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

Constructors

PathCons 
PointCons 

Instances

Instances details
Show IsPathCons Source # 
Instance details

Defined in Agda.TypeChecking.Rules.Data

Eq IsPathCons Source # 
Instance details

Defined in Agda.TypeChecking.Rules.Data

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

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

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