Safe Haskell	None
Language	Haskell2010

Agda.TypeChecking.Rules.Data

Contents

Datatypes

Synopsis

checkDataDef :: DefInfo -> QName -> PositivityCheck -> 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
checkNoLocalRewrites :: QName -> TCM ()
checkNoLocalRewrites' :: QName -> Tele (Dom Type) -> TCM ()
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 :: DataOrRecord_ -> 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 -> PositivityCheck -> 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 Source #

Arguments

:: QName	Datatype name.
-> ConHead	Constructor.
-> Telescope	`Γ` parameters.
-> [QName]	Projection names.
-> Telescope	`Γ ⊢ Φ` field types.
-> Type	`Γ ⊢ T` target type.
-> Boundary	[(i,t_i,b_i)], Γ.Φ ⊢ [ (i=0) -> t_i; (i=1) -> u_i ] : B_i
-> TCM CompKit

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 #

checkNoLocalRewrites :: QName -> TCM () Source #

I am not sure what the generated transport functions should look like in the presence of local rewrite rule parameters. The easiest solution is to just refuse to generate the transport function, and throw a type error.

checkNoLocalRewrites' :: QName -> Tele (Dom Type) -> TCM () 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 :: DataOrRecord_ -> 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.