Agda-2.6.2.2.20230105: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.TypeChecking.Datatypes

Synopsis

Constructors

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

Get true constructor with record fields.

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.

getConType Source #

Arguments

:: PureTCM 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 Source #

Arguments

:: PureTCM 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 Source #

Constructors

DataCon Nat

Arity.

RecordCon PatternOrCopattern HasEta [Dom QName]

List of field names.

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

isDataOrRecordType :: QName -> TCM (Maybe DataOrRecord) Source #

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

isDataOrRecord :: Term -> TCM (Maybe QName) Source #

Precodition: Term is reduced.

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.

getConstructors :: QName -> TCM [QName] Source #

Precondition: Name is a data or record type.

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

Nothing if not data or record type name.

getConstructors_ :: Defn -> Maybe [QName] Source #

Nothing if not data or record definition.