Agda-2.8.0: 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)
- isConstructor :: HasConstInfo m => QName -> m Bool
- getConForm :: QName -> TCM (Either SigError ConHead)
- getOrigConHead :: QName -> TCM (Either SigError ConHead)
- getConstructorData :: HasConstInfo m => QName -> m QName
- consOfHIT :: HasConstInfo m => QName -> m Bool
- isPathCons :: HasConstInfo m => QName -> m Bool
- getFullyAppliedConType :: PureTCM m => ConHead -> Type -> m (Maybe ((QName, Type, Args), Type))
- fullyApplyCon :: (PureTCM m, MonadBlock m, MonadTCError m) => ConHead -> Elims -> Type -> (QName -> Type -> Args -> Type -> Elims -> Telescope -> Type -> m a) -> m a
- fullyApplyCon' :: (PureTCM m, MonadBlock m) => ConHead -> Elims -> Type -> (QName -> Type -> Args -> Type -> Elims -> Telescope -> Type -> m a) -> (Type -> m a) -> m a
- getConType :: (PureTCM m, MonadBlock m) => ConHead -> Type -> m (Maybe ((QName, Type, Args), Type))
- data ConstructorInfo
  - = DataCon Arity
  - | RecordCon PatternOrCopattern HasEta Arity [Dom QName]
- getConstructorInfo :: HasConstInfo m => QName -> m ConstructorInfo
- getConstructorInfo' :: HasConstInfo m => QName -> m (Maybe ConstructorInfo)
- isDatatype :: QName -> TCM Bool
- isDataOrRecordType :: QName -> TCM (Maybe DataOrRecord)
- isDataOrRecord :: Term -> TCM (Maybe (QName, DataOrRecord))
- getNumberOfParameters :: HasConstInfo m => QName -> m (Maybe Nat)
- getDatatypeArgs :: HasConstInfo m => Type -> m (Maybe (QName, Args, Args))
- 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.

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

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.

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

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

- PatternOrCopattern
- HasEta
- Arity

  Arity of the record constructor.

- [Dom QName]

  List of field names. Has length `Arity`.

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

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

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

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

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.

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.