Type check a datatype definition. Assumes that the type has already been checked.
ModuleAgda-2.7.0.1Haskell2010
Agda.TypeChecking.Rules.Data
- 1 type
- 21 values
- PackageAgda-2.7.0.1
- Exports22
- LanguageHaskell2010
- LicenceMIT
- SourceData.hs
Datatypes
22 declarationsMake sure that the target universe admits data type definitions.
E.g. IUniv, SizeUniv etc. do not accept new constructions.
Ensure that the type is a sort. If it is not directly a sort, compare it to a newSortMetaBelowInf.
value
checkConstructor :: QNameName of data type.
-> UniverseCheckCheck universes?
-> TelescopeParameter telescope.
-> NatNumber of indices of the data type.
-> SortSort of the data type.
-> ConstructorConstructor 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.
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.
Defines and returns the name of the transpIx function.
value
defineKanOperationForFields :: Command-> Maybe TermPathCons, Δ.Φ ⊢ u : R δ
-> (Term -> QName -> Term)how to apply a "projection" to a term
-> QNamesome name, e.g. record name
-> Telescopeparam types Δ
-> Telescopefields' types Δ ⊢ Φ
-> [Arg QName]fields' names
-> Typerecord type Δ ⊢ T
-> TCM (Maybe ((QName, Telescope, Type, [Dom Type], [Term]), Substitution))
value
defineTranspForFields :: Maybe TermPathCons, Δ.Φ ⊢ u : R δ
-> (Term -> QName -> Term)how to apply a "projection" to a term
-> QNamesome name, e.g. record name
-> Telescopeparam types Δ
-> Tele (Dom CType)fields' types Δ ⊢ Φ
-> [Arg QName]fields' names
-> Typerecord 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]
value
defineHCompForFields Bind the named generalized parameters.
value
bindParameters 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
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.
When --without-K is enabled, we should check that the sorts of the index types fit into the sort of the datatype.
Return the parameters that share variables with the indices nonLinearParameters :: Int -> Type -> TCM [Int] nonLinearParameters nPars t =
Instances2Eq, Show
Eq IsPathConsDefined in Agda-2.7.0.1 · Agda.TypeChecking.Rules.DataShow IsPathConsDefined in Agda-2.7.0.1 · Agda.TypeChecking.Rules.Data
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).
Is the type coinductive? Returns Nothing if the answer cannot be determined.