| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.TypeChecking.Datatypes
Contents
Synopsis
- getConHead :: HasConstInfo m => QName -> m (Either SigError ConHead)
- isConstructor :: HasConstInfo m => QName -> m Bool
- getConForm :: QName -> TCM (Either SigError ConHead)
- getOrigConHead :: QName -> TCM (Either SigError ConHead)
- getConstructorData :: HasConstInfo m => QName -> m QName
- consOfHIT :: HasConstInfo m => QName -> m Bool
- isPathCons :: HasConstInfo m => QName -> m Bool
- getFullyAppliedConType :: PureTCM m => ConHead -> Type -> m (Maybe ((QName, Type, Args), Type))
- fullyApplyCon :: (PureTCM m, MonadBlock m, MonadTCError m) => ConHead -> Elims -> Type -> (QName -> Type -> Args -> Type -> Elims -> Telescope -> Type -> m a) -> m a
- fullyApplyCon' :: (PureTCM m, MonadBlock m) => ConHead -> Elims -> Type -> (QName -> Type -> Args -> Type -> Elims -> Telescope -> Type -> m a) -> (Type -> m a) -> m a
- getConType :: (PureTCM m, MonadBlock m) => ConHead -> Type -> m (Maybe ((QName, Type, Args), Type))
- data ConstructorInfo
- getConstructorInfo :: HasConstInfo m => QName -> m ConstructorInfo
- getConstructorInfo' :: HasConstInfo m => QName -> m (Maybe ConstructorInfo)
- isDatatype :: QName -> TCM Bool
- isDataOrRecordType :: QName -> TCM (Maybe DataOrRecord)
- isDataOrRecord :: Term -> TCM (Maybe (QName, DataOrRecord))
- getNumberOfParameters :: HasConstInfo m => QName -> m (Maybe Nat)
- getDatatypeArgs :: HasConstInfo m => Type -> m (Maybe (QName, Args, Args))
- getNotErasedConstructors :: QName -> TCM [QName]
- getConstructors :: QName -> TCM [QName]
- getConstructors' :: QName -> TCM (Maybe [QName])
- getConstructors_ :: Defn -> Maybe [QName]
Constructors
getConHead :: HasConstInfo m => QName -> m (Either SigError ConHead) Source #
Get true constructor with record fields.
isConstructor :: HasConstInfo m => QName -> m Bool Source #
getConForm :: QName -> TCM (Either SigError ConHead) Source #
Get true constructor with fields, expanding literals to constructors if possible.
getOrigConHead :: QName -> TCM (Either SigError ConHead) Source #
Augment constructor with record fields (preserve constructor name).
The true constructor might only surface via reduce.
getConstructorData :: HasConstInfo m => QName -> m QName Source #
Get the name of the datatype constructed by a given constructor. Precondition: The argument must refer to a constructor
consOfHIT :: HasConstInfo m => QName -> m Bool Source #
Is the datatype of this constructor a Higher Inductive Type? Precondition: The argument must refer to a constructor of a datatype or record.
isPathCons :: HasConstInfo m => QName -> m Bool Source #
getFullyAppliedConType Source #
Arguments
| :: PureTCM m | |
| => ConHead | Constructor. |
| -> Type | Reduced type of the fully applied constructor. |
| -> m (Maybe ((QName, Type, Args), Type)) |
|
getFullyAppliedConType c t computes the constructor parameters
from data type t and returns them
plus the instantiated type of constructor c.
Nothing if t is not a data/record type or does not have
a constructor c.
Precondition: t is reduced.
Arguments
| :: (PureTCM m, MonadBlock m, MonadTCError m) | |
| => ConHead | Constructor. |
| -> Elims | Constructor arguments. |
| -> Type | Type of the constructor application. |
| -> (QName -> Type -> Args -> Type -> Elims -> Telescope -> Type -> m a) | Name of the data/record type, type of the data/record type, reconstructed parameters, type of the constructor (applied to parameters), full application arguments, types of missing arguments (already added to context), type of the full application. |
| -> m a |
Make sure a constructor is fully applied and infer the type of the constructor. Raises a type error if the constructor does not belong to the given type.
Arguments
| :: (PureTCM m, MonadBlock m) | |
| => ConHead | Constructor. |
| -> Elims | Constructor arguments. |
| -> Type | Type of the constructor application. |
| -> (QName -> Type -> Args -> Type -> Elims -> Telescope -> Type -> m a) | See |
| -> (Type -> m a) | Fallback function |
| -> m a |
Like fullyApplyCon, but calls the given fallback function if
it encounters something other than a datatype.
Arguments
| :: (PureTCM m, MonadBlock m) | |
| => ConHead | Constructor. |
| -> Type | Ending in data/record type. |
| -> m (Maybe ((QName, Type, Args), Type)) |
|
getConType c t computes the constructor parameters from type t
and returns them plus the instantiated type of constructor c.
This works also if t is a function type ending in a data/record type;
the term from which c comes need not be fully applied
Nothing if t is not a data/record type or does not have
a constructor c.
data ConstructorInfo Source #
getConstructorInfo :: HasConstInfo m => QName -> m ConstructorInfo Source #
Return the number of non-parameter arguments to a constructor (arity). In case of record constructors, also return the field names (plus other info).
getConstructorInfo' :: HasConstInfo m => QName -> m (Maybe ConstructorInfo) Source #
Data types
isDatatype :: QName -> TCM Bool Source #
Check if a name refers to a datatype or a record with a named constructor.
isDataOrRecordType :: QName -> TCM (Maybe DataOrRecord) Source #
Check if a name refers to a datatype or a record.
isDataOrRecord :: Term -> TCM (Maybe (QName, DataOrRecord)) Source #
getNumberOfParameters :: HasConstInfo m => QName -> m (Maybe Nat) Source #
getDatatypeArgs :: HasConstInfo m => Type -> m (Maybe (QName, Args, Args)) Source #
This is a simplified version of isDatatype from Coverage,
useful when we do not want to import the module.