ModuleAgda-2.7.0.1Haskell2010

Agda.TypeChecking.Datatypes

1 type
22 values

PackageAgda-2.7.0.1
Exports23
LanguageHaskell2010
LicenceMIT
SourceDatatypes.hs

Constructors

14 declarations

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

Get true constructor with record fields.

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

valuegetConForm :: QName -> TCM (Either SigError ConHead)

Get true constructor with fields, expanding literals to constructors if possible.

valuegetOrigConHead :: QName -> TCM (Either SigError ConHead)

Augment constructor with record fields (preserve constructor name). The true constructor might only surface via reduce.

valuegetConstructorData :: HasConstInfo m => QName -> m QName

Get the name of the datatype constructed by a given constructor. Precondition: The argument must refer to a constructor

valueconsOfHIT :: 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.

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

valuegetFullyAppliedConType

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

valuefullyApplyCon

:: (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.

valuefullyApplyCon'

:: (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.

valuegetConType

:: (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.

datadata ConstructorInfo

Constructors

DataCon Arity
Arity of the data constructor.
RecordCon PatternOrCopattern HasEta Arity [Dom QName]

valuegetConstructorInfo :: 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).

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

Data types

9 declarations

valueisDatatype :: QName -> TCM Bool

Check if a name refers to a datatype or a record with a named constructor.

valueisDataOrRecordType :: QName -> TCM (Maybe DataOrRecord)

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

valueisDataOrRecord :: Term -> TCM (Maybe (QName, DataOrRecord))

Precodition: Term is reduced.

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

valuegetDatatypeArgs :: 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.

valuegetNotErasedConstructors :: QName -> TCM [QName]

valuegetConstructors :: QName -> TCM [QName]

Precondition: Name is a data or record type.

valuegetConstructors' :: QName -> TCM (Maybe [QName])

Nothing if not data or record type name.

valuegetConstructors_ :: Defn -> Maybe [QName]

Nothing if not data or record definition.