Agda.TypeChecking.Datatypes

Constructors

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

Get true constructor with record fields.

isConstructor :: HasConstInfo m => QName -> m Bool

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

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

isPathCons :: HasConstInfo m => QName -> m Bool

getFullyAppliedConType

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.

fullyApplyCon

Arguments

:: (PureTCM m, MonadBlock m, MonadTCError m)

=> ConHead

Constructor.

-> Elims

Constructor arguments.

-> Type

Type of the constructor application.

-> (QName -> Type -> Args -> Type -> Elims -> Telescope -> Type -> m a)

Name of the data/record type, type of the data/record type, reconstructed parameters, type of the constructor (applied to parameters), full application arguments, types of missing arguments (already added to context), type of the full application.

-> m a

Make sure a constructor is fully applied and infer the type of the constructor. Raises a type error if the constructor does not belong to the given type.

fullyApplyCon'

Arguments

:: (PureTCM m, MonadBlock m)

=> ConHead

Constructor.

-> Elims

Constructor arguments.

-> Type

Type of the constructor application.

-> (QName -> Type -> Args -> Type -> Elims -> Telescope -> Type -> m a)

See fullyApplyCon

-> (Type -> m a)

Fallback function

-> m a

Like fullyApplyCon, but calls the given fallback function if it encounters something other than a datatype.

getConType

Arguments

:: (PureTCM m, MonadBlock 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.

data ConstructorInfo

Constructors

DataCon Arity

Arity of the data constructor.

RecordCon

Fields

• PatternOrCopattern
• HasEta
• Arity

  Arity of the record constructor.

• [Dom QName]

  List of field names. Has length Arity.

getConstructorInfo :: HasConstInfo m => QName -> m ConstructorInfo

Return the number of non-parameter arguments to a constructor (arity). In case of record constructors, also return the field names (plus other info).

getConstructorInfo' :: HasConstInfo m => QName -> m (Maybe ConstructorInfo)

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, DataOrRecord))

Precodition: Term is reduced.

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

getDatatypeArgs :: HasConstInfo m => Type -> m (Maybe (QName, Args, Args))

This is a simplified version of isDatatype from Coverage, useful when we do not want to import the module.

getNotErasedConstructors :: QName -> TCM [QName]

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.