Agda-2.3.2: A dependently typed functional programming language and proof assistant

Safe Haskell | None

Agda.TypeChecking.Records

Synopsis

- orderFields :: QName -> a -> [Name] -> [(Name, a)] -> TCM [a]
- recordModule :: QName -> ModuleName
- getRecordDef :: QName -> TCM Defn
- getRecordFieldNames :: QName -> TCM [Arg Name]
- findPossibleRecords :: [Name] -> TCM [QName]
- getRecordFieldTypes :: QName -> TCM Telescope
- getRecordTypeFields :: Type -> TCM [Arg QName]
- getRecordConstructorType :: QName -> TCM Type
- getRecordConstructor :: QName -> TCM QName
- isRecord :: QName -> TCM (Maybe Defn)
- isEtaRecord :: QName -> TCM Bool
- isInductiveRecord :: QName -> TCM Bool
- isEtaRecordType :: Type -> TCM (Maybe (QName, Args))
- isRecordConstructor :: QName -> TCM (Maybe (QName, Defn))
- isGeneratedRecordConstructor :: QName -> TCM Bool
- unguardedRecord :: QName -> TCM ()
- recursiveRecord :: QName -> TCM ()
- etaExpandRecord :: QName -> Args -> Term -> TCM (Telescope, Args)
- etaContractRecord :: QName -> QName -> Args -> TCM Term
- isSingletonRecord :: QName -> Args -> TCM (Either MetaId Bool)
- isSingletonRecordModuloRelevance :: QName -> Args -> TCM (Either MetaId Bool)
- isSingletonRecord' :: Bool -> QName -> Args -> TCM (Either MetaId (Maybe Term))
- isSingletonType :: Type -> TCM (Either MetaId (Maybe Term))
- isSingletonTypeModuloRelevance :: MonadTCM tcm => Type -> tcm (Either MetaId Bool)
- isSingletonType' :: Bool -> Type -> TCM (Either MetaId (Maybe Term))
- emap :: (a -> b) -> Either c (Maybe a) -> Either c (Maybe b)

# Documentation

orderFields :: QName -> a -> [Name] -> [(Name, a)] -> TCM [a]

Order the fields of a record construction. Use the second argument for missing fields.

recordModule :: QName -> ModuleName

The name of the module corresponding to a record.

getRecordDef :: QName -> TCM Defn

Get the definition for a record. Throws an exception if the name does not refer to a record.

getRecordFieldNames :: QName -> TCM [Arg Name]

Get the field names of a record.

findPossibleRecords :: [Name] -> TCM [QName]

Find all records with at least the given fields.

getRecordFieldTypes :: QName -> TCM Telescope

Get the field types of a record.

getRecordTypeFields :: Type -> TCM [Arg QName]

Get the field names belonging to a record type.

getRecordConstructorType :: QName -> TCM Type

Get the type of the record constructor.

getRecordConstructor :: QName -> TCM QName

Returns the given record type's constructor name (with an empty range).

isRecord :: QName -> TCM (Maybe Defn)

Check if a name refers to a record. If yes, return record definition.

isEtaRecord :: QName -> TCM Bool

Check if a name refers to an eta expandable record.

isInductiveRecord :: QName -> TCM Bool

Check if a name refers to a record which is not coinductive. (Projections are then size-preserving)

isEtaRecordType :: Type -> TCM (Maybe (QName, Args))

Check if a type is an eta expandable record and return the record identifier and the parameters.

isRecordConstructor :: QName -> TCM (Maybe (QName, Defn))

Check if a name refers to a record constructor. If yes, return record definition.

isGeneratedRecordConstructor :: QName -> TCM Bool

Check if a constructor name is the internally generated record constructor.

unguardedRecord :: QName -> TCM ()

Mark record type as unguarded. No eta-expansion. Projections do not preserve guardedness.

recursiveRecord :: QName -> TCM ()

Mark record type as recursive. Projections do not preserve guardedness.

etaExpandRecord :: QName -> Args -> Term -> TCM (Telescope, Args)

Compute the eta expansion of a record. The first argument should be the name of a record type. Given

    record R : Set where x : A; y : B; .z : C

and `r : R`, `etaExpand R [] r` is `[R.x r, R.y r, DontCare]`

etaContractRecord :: QName -> QName -> Args -> TCM Term

The fields should be eta contracted already.

We can eta constract if all fields `f = ...` are irrelevant or the corresponding projection `f = f v` of the same value `v`, but we need at least one relevant field to find the value `v`.

isSingletonRecord :: QName -> Args -> TCM (Either MetaId Bool)

Is the type a hereditarily singleton record type? May return a blocking metavariable.

Precondition: The name should refer to a record type, and the arguments should be the parameters to the type.

isSingletonRecordModuloRelevance :: QName -> Args -> TCM (Either MetaId Bool)

isSingletonRecord' :: Bool -> QName -> Args -> TCM (Either MetaId (Maybe Term))

Return the unique (closed) inhabitant if exists. In case of counting irrelevance in, the returned inhabitant contains garbage.

isSingletonType :: Type -> TCM (Either MetaId (Maybe Term))

Check whether a type has a unique inhabitant and return it. Can be blocked by a metavar.

isSingletonTypeModuloRelevance :: MonadTCM tcm => Type -> tcm (Either MetaId Bool)

Check whether a type has a unique inhabitant (irrelevant parts ignored). Can be blocked by a metavar.

isSingletonType' :: Bool -> Type -> TCM (Either MetaId (Maybe Term))

emap :: (a -> b) -> Either c (Maybe a) -> Either c (Maybe b)

Auxiliary function.