Safe Haskell	Safe-Inferred
Language	Haskell2010

Agda.TypeChecking.Datatypes

Contents

Constructors
Data types

Synopsis

getConHead :: HasConstInfo m => QName -> m (Either SigError ConHead)
getConForm :: QName -> TCM (Either SigError ConHead)
getOrigConHead :: QName -> TCM (Either SigError ConHead)
getConstructorData :: HasConstInfo m => QName -> m QName
consOfHIT :: HasConstInfo m => QName -> m Bool
getConType :: PureTCM m => ConHead -> Type -> m (Maybe ((QName, Type, Args), Type))
getFullyAppliedConType :: PureTCM m => ConHead -> Type -> m (Maybe ((QName, Type, Args), Type))
data ConstructorInfo
- = DataCon Nat
- | RecordCon PatternOrCopattern HasEta [Dom QName]
getConstructorInfo :: HasConstInfo m => QName -> m ConstructorInfo
isDatatype :: QName -> TCM Bool
isDataOrRecordType :: QName -> TCM (Maybe DataOrRecord)
isDataOrRecord :: Term -> TCM (Maybe QName)
getNumberOfParameters :: HasConstInfo m => QName -> m (Maybe Nat)
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.

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.

getNumberOfParameters :: HasConstInfo m => QName -> m (Maybe Nat) Source #

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

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.