Agda-2.6.0.1: A dependently typed functional programming language and proof assistant

Safe Haskell | None
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 :: QName -> TCM Bool
- getConType :: ConHead -> Type -> TCM (Maybe ((QName, Type, Args), Type))
- getFullyAppliedConType :: (HasConstInfo m, MonadReduce m, MonadDebug m) => ConHead -> Type -> m (Maybe ((QName, Type, Args), Type))
- data ConstructorInfo
  - = DataCon Nat
  - | RecordCon HasEta [Arg QName]
- getConstructorInfo :: QName -> TCM ConstructorInfo
- isDatatype :: QName -> TCM Bool
- isDataOrRecordType :: QName -> TCM (Maybe DataOrRecord)
- isDataOrRecord :: Term -> TCM (Maybe QName)
- getNumberOfParameters :: QName -> TCM (Maybe Nat)
- getConstructors :: QName -> TCM [QName]
- getConstructors' :: QName -> TCM (Maybe [QName])
- getConstructors_ :: Defn -> Maybe [QName]
- getConHeads :: QName -> TCM [ConHead]
- getConHeads' :: QName -> TCM (Maybe [ConHead])
- getConHeads_ :: Defn -> Maybe [ConHead]

# 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 :: QName -> TCM 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

:: ConHead | Constructor.
-> Type | Ending in data/record type.
-> TCM (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

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

Constructors

DataCon Nat | Arity.
RecordCon HasEta [Arg QName] | List of field names.

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.

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 `reduce`d.

getNumberOfParameters :: QName -> TCM (Maybe Nat) 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.

getConHeads :: QName -> TCM [ConHead] Source #

Precondition: Name is a data or record type.

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

`Nothing` if not data or record type name.

getConHeads_ :: Defn -> Maybe [ConHead] Source #

`Nothing` if not data or record definition.