Agda-2.6.3.20230930: 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.

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.

fullyApplyCon Source #

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' Source #

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

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

Constructors

DataCon Arity

Arity of the data constructor.

RecordCon 

Fields

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

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

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