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

Safe HaskellNone
LanguageHaskell98

Agda.TypeChecking.Records

Synopsis

Documentation

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

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

recordModule :: QName -> ModuleName Source

The name of the module corresponding to a record.

getRecordDef :: QName -> TCM Defn Source

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

getRecordOfField :: QName -> TCM (Maybe QName) Source

Get the record name belonging to a field name.

getRecordFieldNames :: QName -> TCM [Arg Name] Source

Get the field names of a record.

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

Find all records with at least the given fields.

getRecordFieldTypes :: QName -> TCM Telescope Source

Get the field types of a record.

getRecordTypeFields :: Type -> TCM [Arg QName] Source

Get the field names belonging to a record type.

getRecordConstructorType :: QName -> TCM Type Source

Get the type of the record constructor.

getRecordConstructor :: QName -> TCM ConHead Source

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

isRecord :: HasConstInfo m => QName -> m (Maybe Defn) Source

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

isRecordType :: Type -> TCM (Maybe (QName, Args, Defn)) Source

Reduce a type and check whether it is a record type. Succeeds only if type is not blocked by a meta var. If yes, return its name, parameters, and definition.

tryRecordType :: Type -> TCM (Either (Maybe Type) (QName, Args, Defn)) Source

Reduce a type and check whether it is a record type. Succeeds only if type is not blocked by a meta var. If yes, return its name, parameters, and definition. If no, return the reduced type (unless it is blocked).

projectType :: Type -> QName -> TCM (Maybe Type) Source

The analogue of piApply. If v is a value of record type T with field f, then projectType T f returns the type of f v.

isEtaRecord :: HasConstInfo m => QName -> m Bool Source

Check if a name refers to an eta expandable record.

isInductiveRecord :: QName -> TCM Bool Source

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

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

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

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

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

isGeneratedRecordConstructor :: QName -> TCM Bool Source

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

unguardedRecord :: QName -> TCM () Source

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

recursiveRecord :: QName -> TCM () Source

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

isRecursiveRecord :: QName -> TCM Bool Source

Check whether record type is marked as recursive.

Precondition: record type identifier exists in signature.

recRecursive_ :: Defn -> Bool Source

Version of recRecursive with proper internal error.

etaExpandBoundVar :: Int -> TCM (Maybe (Telescope, Substitution, Substitution)) Source

etaExpandBoundVar i = (Δ, σ, τ)

Precondition: The current context is Γ = Γ₁, x:R pars, Γ₂ where |Γ₂| = i and R is a eta-expandable record type with constructor c and fields Γ'.

Postcondition: Δ = Γ₁, Γ', Γ₂[c Γ'] and Γ ⊢ σ : Δ and Δ ⊢ τ : Γ.

curryAt :: Type -> Int -> TCM (Term -> Term, Term -> Term, Type) Source

curryAt v (Γ (y : R pars) -> B) n =
     (  v -> λ Γ ys → v Γ (c ys)            {- curry   -}
     ,  v -> λ Γ y → v Γ (p1 y) ... (pm y)  {- uncurry -}
     , Γ (ys : As) → B[c ys / y]
     )

where n = size Γ.

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

etaExpand r pars u computes the eta expansion of record value u at record type r pars.

The first argument r should be the name of a record type. Given

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

and r : R,

etaExpand R [] r = (tel, [R.x r, R.y r, R.z r])

where tel is the record telescope instantiated at the parameters pars.

etaContractRecord :: HasConstInfo m => QName -> ConHead -> Args -> m Term Source

The fields should be eta contracted already.

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

TODO: this can be moved out of TCM (but only if ConHead stores also the Arg-decoration of the record fields.

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

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.

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

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

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

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

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

Auxiliary function.