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

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.

Arguments

 :: QName Name of record type (for error reporting). -> (Name -> a) Function to generate a placeholder for missing visible field. -> [FieldAssignment' a] Given fields. -> [Arg Name] All record field names with ArgInfo. -> TCM [NamedArg a] Given fields enriched by placeholders for missing explicit fields.

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.

The name of the module corresponding to a record.

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.

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

Find all records with at least the given fields.

Get the field types of a record.

Get the field names belonging to a record type.

Get the original name of the projection (the current one could be from a module application).

Get the type of the record constructor.

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.

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

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

projectTyped :: Term -> Type -> QName -> TCM (Maybe (Term, Type)) Source #

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.

Works also for projection-like definitions f.

Precondition: t is reduced.

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

Check if a name refers to an eta expandable record.

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.

isRecordConstructor :: MonadTCM tcm => QName -> tcm (Maybe (QName, Defn)) Source #

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

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

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

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

Check whether record type is marked as recursive.

Precondition: record type identifier exists in signature.

Version of recRecursive with proper internal error.

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

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.

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

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.