| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Agda.TypeChecking.Datatypes
Contents
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
- getConType :: PureTCM m => ConHead -> Type -> m (Maybe ((QName, Type, Args), Type))
- getFullyAppliedConType :: PureTCM m => ConHead -> Type -> m (Maybe ((QName, Type, Args), Type))
- data ConstructorInfo
- 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)
- 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 #
Arguments
| :: PureTCM m | |
| => ConHead | Constructor. |
| -> Type | Ending in data/record type. |
| -> m (Maybe ((QName, Type, Args), Type)) |
|
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
| :: PureTCM m | |
| => ConHead | Constructor. |
| -> Type | Reduced type of the fully applied constructor. |
| -> m (Maybe ((QName, Type, Args), Type)) |
|
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 #
getConstructorInfo :: HasConstInfo m => QName -> m 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.
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.
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.