| Safe Haskell | None |
|---|---|
| Language | Haskell98 |
Agda.TypeChecking.Datatypes
Contents
- getConHead :: QName -> TCM ConHead
- getConTerm :: QName -> TCM Term
- getConForm :: QName -> TCM ConHead
- getOrigConHead :: QName -> TCM ConHead
- getOrigConTerm :: QName -> TCM Term
- getConstructorData :: HasConstInfo m => QName -> m QName
- getConType :: ConHead -> Type -> TCM (Maybe Type)
- data HasEta
- data ConstructorInfo
- getConstructorInfo :: QName -> TCM ConstructorInfo
- getConstructorArity :: QName -> TCM Nat
- isDatatype :: QName -> TCM Bool
- data DataOrRecord
- isDataOrRecordType :: QName -> TCM (Maybe DataOrRecord)
- isDataOrRecord :: Term -> TCM (Maybe QName)
- getNumberOfParameters :: QName -> TCM (Maybe Nat)
Constructors
getConForm :: QName -> TCM ConHead Source #
Get true constructor with fields, expanding literals to constructors if possible.
getOrigConHead :: QName -> TCM ConHead Source #
Augment constructor with record fields (preserve constructor name).
The true constructor might only surface via reduce.
getOrigConTerm :: QName -> TCM Term Source #
Analogous to getConTerm.
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
getConType :: ConHead -> Type -> TCM (Maybe Type) Source #
getConType c t computes the constructor parameters from type t
and returns 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.
getConstructorInfo :: QName -> TCM ConstructorInfo Source #
Return the number of non-parameter arguments to a data constructor, or the field names of a record constructor.
For getting just the arity of constructor c,
use either id size $ getConstructorArity c.
Data types
isDatatype :: QName -> TCM Bool Source #
Check if a name refers to a datatype or a record with a named constructor.
data DataOrRecord Source #
Instances
isDataOrRecordType :: QName -> TCM (Maybe DataOrRecord) Source #
Check if a name refers to a datatype or a record.