Safe Haskell	None
Language	Haskell2010

Agda.TypeChecking.Rules.Data

Contents

Datatypes

Synopsis

checkDataDef :: DefInfo -> QName -> UniverseCheck -> DataDefParams -> [Constructor] -> TCM ()
checkDataSort :: QName -> Sort -> TCM ()
forceSort :: Type -> TCM Sort
checkConstructor :: QName -> UniverseCheck -> Telescope -> Nat -> Sort -> Constructor -> TCM IsPathCons
defineCompData :: QName -> ConHead -> Telescope -> [QName] -> Telescope -> Type -> Boundary -> TCM CompKit
defineProjections :: QName -> ConHead -> Telescope -> [QName] -> Telescope -> Type -> TCM ()
freshAbstractQName'_ :: String -> TCM QName
defineTranspIx :: QName -> TCM (Maybe QName)
defineTranspFun :: QName -> Maybe QName -> [QName] -> [QName] -> TCM (Maybe QName)
defineConClause :: QName -> Bool -> Maybe QName -> Nat -> Nat -> Telescope -> Telescope -> Substitution -> Type -> [QName] -> TCM [Clause]
defineKanOperationForFields :: Command -> Maybe Term -> (Term -> QName -> Term) -> QName -> Telescope -> Telescope -> [Arg QName] -> Type -> TCM (Maybe ((QName, Telescope, Type, [Dom Type], [Term]), Substitution))
defineTranspForFields :: Maybe Term -> (Term -> QName -> Term) -> QName -> Telescope -> Tele (Dom CType) -> [Arg QName] -> Type -> TCM ((QName, Telescope, Type, [Dom Type], [Term]), Substitution)
defineHCompForFields :: (Term -> QName -> Term) -> QName -> Telescope -> Tele (Dom LType) -> [Arg QName] -> LType -> 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
bindParameters :: Int -> [LamBinding] -> Type -> (Telescope -> Type -> TCM a) -> TCM a
bindParameter :: Int -> [LamBinding] -> Name -> Dom Type -> Abs Type -> (Telescope -> Type -> TCM a) -> TCM a
fitsIn :: QName -> UniverseCheck -> [IsForced] -> Type -> Sort -> TCM Int
checkIndexSorts :: Sort -> Telescope -> TCM ()
data IsPathCons
- = PathCons
- | PointCons
constructs :: Int -> Int -> Type -> QName -> TCM IsPathCons
isCoinductive :: Type -> TCM (Maybe Bool)

Datatypes

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

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

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

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

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.

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

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.

freshAbstractQName'_ :: String -> TCM QName Source #

defineTranspIx Source #

Arguments

:: QName	datatype name
-> TCM (Maybe QName)

Defines and returns the name of the transpIx function.

defineTranspFun Source #

Arguments

:: QName	datatype
-> Maybe QName	transpX "constructor"
-> [QName]	constructor names
-> [QName]	path cons
-> TCM (Maybe QName)

defineConClause Source #

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

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

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

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 :: QName -> 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 Methods showsPrec :: Int -> IsPathCons -> ShowS show :: IsPathCons -> String showList :: [IsPathCons] -> ShowS
Eq IsPathCons Source #
Instance details Defined in Agda.TypeChecking.Rules.Data Methods (==) :: IsPathCons -> IsPathCons -> Bool (/=) :: IsPathCons -> IsPathCons -> Bool

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.