Agda.TypeChecking.Datatypes

Constructors

getConHead :: HasConstInfo m => QName -> m (Either SigError ConHead)

Get true constructor with record fields.

getConForm :: QName -> TCM (Either SigError ConHead)

Get true constructor with fields, expanding literals to constructors if possible.

getOrigConHead :: QName -> TCM (Either SigError 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

consOfHIT :: QName -> TCM Bool

Is the datatype of this constructor a Higher Inductive Type? Precondition: The argument must refer to a constructor of a datatype or record.

getConType

Arguments

:: (MonadReduce m, MonadAddContext m, HasConstInfo m, MonadDebug m)

=> ConHead

Constructor.

-> Type

Ending in data/record type.

-> m (Maybe ((QName, Type, Args), Type))

Nothing if not ends in data or record type.

Just ((d, dt, pars), ct) otherwise, where d is the data or record type name, dt is the type of the data or record name, pars are the reconstructed parameters, ct is the type of the constructor instantiated to the parameters.

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.

getFullyAppliedConType

Arguments

:: (HasConstInfo m, MonadReduce m, MonadDebug m)

=> ConHead

Constructor.

-> Type

Reduced type of the fully applied constructor.

-> m (Maybe ((QName, Type, Args), Type))

Nothing if not data or record type.

Just ((d, dt, pars), ct) otherwise, where d is the data or record type name, dt is the type of the data or record name, pars are the reconstructed parameters, ct is the type of the constructor instantiated to the parameters.

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.

data ConstructorInfo

Constructors

DataCon Nat

Arity.

RecordCon HasEta [Dom QName]

List of field names.

getConstructorInfo :: HasConstInfo m => QName -> m 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.

Data types

isDatatype :: QName -> TCM Bool

Check if a name refers to a datatype or a record with a named constructor.

isDataOrRecordType :: QName -> TCM (Maybe DataOrRecord)

Check if a name refers to a datatype or a record.

isDataOrRecord :: Term -> TCM (Maybe QName)

Precodition: Term is reduced.

getNumberOfParameters :: QName -> TCM (Maybe Nat)

getConstructors :: QName -> TCM [QName]

Precondition: Name is a data or record type.

getConstructors' :: QName -> TCM (Maybe [QName])

Nothing if not data or record type name.

getConstructors_ :: Defn -> Maybe [QName]

Nothing if not data or record definition.

getConHeads :: QName -> TCM [ConHead]

Precondition: Name is a data or record type.

getConHeads' :: QName -> TCM (Maybe [ConHead])

Nothing if not data or record type name.

makeConHead :: QName -> TCM ConHead

Fills in the fields.