Agda-2.6.2.2: A dependently typed functional programming language and proof assistant

Safe Haskell | Safe-Inferred
Language | Haskell2010

Agda.TypeChecking.Rules.Data

Contents

- Datatypes
- Special cases of Type

Synopsis

- checkDataDef :: DefInfo -> QName -> UniverseCheck -> DataDefParams -> [Constructor] -> 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
- data LType = LEl Level Term
- fromLType :: LType -> Type
- lTypeLevel :: LType -> Level
- toLType :: MonadReduce m => Type -> m (Maybe LType)
- data CType
  - = ClosedType Sort QName
  - | LType LType
- fromCType :: CType -> Type
- toCType :: MonadReduce m => Type -> m (Maybe CType)
- defineTranspOrHCompForFields :: TranspOrHComp -> 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 :: 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.

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 #

# 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 # Methods applySubst :: Substitution' (SubstArg LType) -> LType -> LType Source #
Show LType Source # |
Instance details Defined in Agda.TypeChecking.Rules.Data Methods showsPrec :: Int -> LType -> ShowS Source # show :: LType -> String Source # showList :: [LType] -> ShowS Source #
Eq LType Source # |
Instance details Defined in Agda.TypeChecking.Rules.Data Methods (==) :: LType -> LType -> Bool Source # (/=) :: LType -> LType -> Bool Source #
type SubstArg LType Source # |
Instance details Defined in Agda.TypeChecking.Rules.Data type SubstArg LType = Term

fromLType :: LType -> Type Source #

lTypeLevel :: LType -> Level Source #

toLType :: MonadReduce m => Type -> m (Maybe LType) Source #

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`.

Constructors

ClosedType Sort QName |
LType LType |

#### Instances

Instances details

Subst CType Source # |
Instance details Defined in Agda.TypeChecking.Rules.Data Associated Types type SubstArg CType Source # Methods applySubst :: Substitution' (SubstArg CType) -> CType -> CType Source #
Show CType Source # |
Instance details Defined in Agda.TypeChecking.Rules.Data Methods showsPrec :: Int -> CType -> ShowS Source # show :: CType -> String Source # showList :: [CType] -> ShowS Source #
Eq CType Source # |
Instance details Defined in Agda.TypeChecking.Rules.Data Methods (==) :: CType -> CType -> Bool Source # (/=) :: CType -> CType -> Bool Source #
type SubstArg CType Source # |
Instance details Defined in Agda.TypeChecking.Rules.Data type SubstArg CType = Term

fromCType :: CType -> Type Source #

toCType :: MonadReduce m => Type -> m (Maybe CType) Source #

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

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

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.