| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Agda.TypeChecking.Rules.Data
Contents
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
- 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
- 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.
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.
Special cases of Type
A Type with sort Type l
Such a type supports both hcomp and transp.
lTypeLevel :: LType -> Level 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 |
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) |
bindGeneralizedParameters :: [Maybe Name] -> Type -> (Telescope -> Type -> TCM a) -> TCM a Source #
Bind the named generalized parameters.
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 =
Instances
| Show IsPathCons Source # | |
Defined in Agda.TypeChecking.Rules.Data Methods showsPrec :: Int -> IsPathCons -> ShowS # show :: IsPathCons -> String # showList :: [IsPathCons] -> ShowS # | |
| Eq IsPathCons Source # | |
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).