Safe Haskell | None |
---|---|
Language | Haskell2010 |
Agda.TypeChecking.Datatypes
Contents
- getConHead :: QName -> TCM ConHead
- getConForm :: QName -> TCM ConHead
- getOrigConHead :: QName -> TCM ConHead
- 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)
- getConstructors :: QName -> TCM [QName]
Constructors
getConHead :: QName -> TCM ConHead #
Get true constructor with record fields.
getConForm :: QName -> TCM ConHead #
Get true constructor with fields, expanding literals to constructors if possible.
getOrigConHead :: QName -> TCM ConHead #
Augment constructor with record fields (preserve constructor name).
The true constructor might only surface via reduce
.
getConstructorData :: HasConstInfo m => QName -> m QName #
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) #
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 #
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
.
getConstructorArity :: QName -> TCM Nat #
Data types
isDatatype :: QName -> TCM Bool #
Check if a name refers to a datatype or a record with a named constructor.
data DataOrRecord #
Instances
isDataOrRecordType :: QName -> TCM (Maybe DataOrRecord) #
Check if a name refers to a datatype or a record.
getConstructors :: QName -> TCM [QName] #
Precondition: Name is a data or record type.