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

Agda.TypeChecking.Records

Synopsis

- orderFields :: MonadTCM tcm => QName -> a -> [Name] -> [(Name, a)] -> tcm [a]
- recordModule :: QName -> ModuleName
- getRecordDef :: MonadTCM tcm => QName -> tcm Defn
- getRecordFieldNames :: MonadTCM tcm => QName -> tcm [Arg Name]
- getRecordFieldTypes :: MonadTCM tcm => QName -> tcm Telescope
- getRecordConstructorType :: MonadTCM tcm => QName -> tcm Type
- getRecordConstructor :: MonadTCM tcm => QName -> tcm QName
- isRecord :: MonadTCM tcm => QName -> tcm Bool
- isEtaRecord :: MonadTCM tcm => QName -> tcm Bool
- isRecordConstructor :: MonadTCM tcm => QName -> tcm Bool
- isGeneratedRecordConstructor :: MonadTCM tcm => QName -> tcm Bool
- etaExpandRecord :: MonadTCM tcm => QName -> Args -> Term -> tcm (Telescope, Args)
- etaContractRecord :: MonadTCM tcm => QName -> QName -> Args -> tcm Term
- isSingletonRecord :: MonadTCM tcm => QName -> Args -> tcm (Either MetaId Bool)

# Documentation

orderFields :: MonadTCM tcm => 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 :: MonadTCM tcm => QName -> tcm Defn

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

getRecordFieldNames :: MonadTCM tcm => QName -> tcm [Arg Name]

Get the field names of a record.

getRecordFieldTypes :: MonadTCM tcm => QName -> tcm Telescope

Get the field types of a record.

getRecordConstructorType :: MonadTCM tcm => QName -> tcm Type

Get the type of the record constructor.

getRecordConstructor :: MonadTCM tcm => QName -> tcm QName

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

isRecord :: MonadTCM tcm => QName -> tcm Bool

Check if a name refers to a record.

isEtaRecord :: MonadTCM tcm => QName -> tcm Bool

Check if a name refers to an eta expandable record.

isRecordConstructor :: MonadTCM tcm => QName -> tcm Bool

Check if a name refers to a record constructor.

isGeneratedRecordConstructor :: MonadTCM tcm => QName -> tcm Bool

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

etaExpandRecord :: MonadTCM tcm => 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 :: MonadTCM tcm => QName -> QName -> Args -> tcm Term

The fields should be eta contracted already.

isSingletonRecord :: MonadTCM tcm => 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.