Agda.TypeChecking.Records

Order the fields of a record construction.

Raise generated RecordFieldWarnings as warnings.

Raise generated RecordFieldWarnings as errors.

Order the fields of a record construction. Raise generated RecordFieldWarnings as warnings.

Order the fields of a record construction. Raise generated RecordFieldWarnings as errors.

A record field assignment record{xs = es} might not mention all visible fields. insertMissingFields inserts placeholders for the missing visible fields and returns the values in order of the fields in the record declaration.

A record field assignment record{xs = es} might not mention all visible fields. insertMissingFields inserts placeholders for the missing visible fields and returns the values in order of the fields in the record declaration.

A record field assignment record{xs = es} might not mention all visible fields. insertMissingFields inserts placeholders for the missing visible fields and returns the values in order of the fields in the record declaration.

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

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

Get the record name belonging to a field name.

Get the field names of a record.

Find all records with at least the given fields.

Get the field names belonging to a record type.

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

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.

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

Get the original projection info for name.

getDefType f t computes the type of (possibly projection-(like)) function f whose first argument has type t. The parameters for f are extracted from t. Nothing if f is projection(like) but t is not a datarecordaxiom type.

Precondition: t is reduced.

See also: getConType

Apply a projection to an expression with a known type, returning the type of the projected value. The given type should either be a record type or a type eligible for the principal argument of a projection-like function.

The analogue of piApply. If v is a value of record type t with field f, then projectTyped v t f returns the type of f v. And also the record type (as first result).

Works also for projection-like definitions f. In this case, the first result is not a record type.

Precondition: t is reduced.

Typing of an elimination.

Given a head and its type, compute the types of the eliminations.

Given a term with a given type and a list of eliminations, returning the type of the term applied to the eliminations.

Check if a name refers to an eta expandable record.

The answer is no for a record type with an erased constructor unless the current quantity is "erased".

Going under one of these does not count as a decrease in size for the termination checker.

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

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

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

Turn off eta for unguarded recursive records. Projections do not preserve guardedness.

Turn on eta for non-recursive and inductive guarded recursive records, unless user declared otherwise. Projections do not preserve guardedness.

Turn on eta for inductive guarded recursive records. Projections do not preserve guardedness.

Turn on eta for non-recursive record, unless user declared otherwise.

Check whether record type is marked as recursive.

Precondition: record type identifier exists in signature.

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 Δ ⊢ τ : Γ.

expandRecordVar i Γ = (Δ, σ, τ, Γ')

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

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

Precondition: variable list is ordered descendingly. Can be empty.

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

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 an eta-expandable 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.

Eta expand a record regardless of whether it's an eta-record or not.

Eta-expand a value at the given record type (must match).

Eta-expand a value at the given eta record type (must match).

Eta-expand a value at the given record type (must match).

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.

If all fields are erased, we cannot eta-contract.

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.

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

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

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

Checks whether the given term (of the given type) is beta-eta-equivalent to a variable. Returns just the de Bruijn-index of the variable if it is, or nothing otherwise.

Replace projection patterns by the original projections.