Agda.TypeChecking.Records

Documentation

mkCon :: ConHead -> ConInfo -> Args -> Term

orderFields

Arguments

:: forall a. HasRange a

=> QName

Name of record type (for error message).

-> (Arg Name -> a)

How to fill a missing field.

-> [Arg Name]

Field names of the record type.

-> [(Name, a)]

Provided fields with content in the record expression.

-> Writer [RecordFieldWarning] [a]

Content arranged in official order.

Order the fields of a record construction.

warnOnRecordFieldWarnings :: Writer [RecordFieldWarning] a -> TCM a

Raise generated RecordFieldWarnings as warnings.

failOnRecordFieldWarnings :: Writer [RecordFieldWarning] a -> TCM a

Raise generated RecordFieldWarnings as errors.

orderFieldsWarn

Arguments

:: forall a. HasRange a

=> QName

Name of record type (for error message).

-> (Arg Name -> a)

How to fill a missing field.

-> [Arg Name]

Field names of the record type.

-> [(Name, a)]

Provided fields with content in the record expression.

-> TCM [a]

Content arranged in official order.

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

orderFieldsFail

Arguments

:: forall a. HasRange a

=> QName

Name of record type (for error message).

-> (Arg Name -> a)

How to fill a missing field.

-> [Arg Name]

Field names of the record type.

-> [(Name, a)]

Provided fields with content in the record expression.

-> TCM [a]

Content arranged in official order.

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

insertMissingFields

Arguments

:: forall a. HasRange a

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

-> Writer [RecordFieldWarning] [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.

insertMissingFieldsWarn

Arguments

:: forall a. HasRange a

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

insertMissingFieldsFail

Arguments

:: forall a. HasRange a

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

getRecordDef :: (HasConstInfo m, ReadTCState m, MonadError TCErr m) => QName -> m Defn

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)

Get the record name belonging to a field name.

getRecordFieldNames :: (HasConstInfo m, ReadTCState m, MonadError TCErr m) => QName -> m [Dom Name]

Get the field names of a record.

getRecordFieldNames_ :: (HasConstInfo m, ReadTCState m) => QName -> m (Maybe [Dom Name])

recordFieldNames :: Defn -> [Dom Name]

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

Arguments

:: Type

Record type. Need not be reduced.

-> TCM [Dom QName]

Get the field names belonging to a record type.

getRecordConstructor :: (HasConstInfo m, ReadTCState m, MonadError TCErr m) => QName -> m ConHead

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

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

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

isRecordType :: PureTCM m => Type -> m (Maybe (QName, Args, Defn))

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 :: PureTCM m => Type -> m (Either (Blocked Type) (QName, Args, Defn))

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

origProjection :: HasConstInfo m => QName -> m (QName, Definition, Maybe Projection)

Get the original projection info for name.

getDefType :: PureTCM m => QName -> Type -> m (Maybe Type)

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

shouldBeProjectible :: (PureTCM m, MonadTCError m, MonadBlock m) => Term -> Type -> ProjOrigin -> QName -> m Type

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.

projectTyped

Arguments

:: PureTCM m

=> Term

Head (record value).

-> Type

Its type.

-> ProjOrigin

-> QName

Projection.

-> m (Maybe (Dom Type, Term, Type))

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.

data ElimType

Typing of an elimination.

Constructors

ArgT (Dom Type)

Type of the argument.

ProjT

Fields

• projTRec :: Dom Type

  The type of the record which is eliminated.

• projTField :: Type

  The type of the field.

Instances

PrettyTCM ElimType

Defined in Agda.TypeChecking.Records

Methods

prettyTCM :: MonadPretty m => ElimType -> m Doc

typeElims :: Type -> Term -> Elims -> TCM [ElimType]

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

eliminateType :: PureTCM m => m Empty -> Term -> Type -> Elims -> m Type

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

eliminateType' :: PureTCM m => m Empty -> (Elims -> Term) -> Type -> Elims -> m Type

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

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

isEtaCon :: HasConstInfo m => QName -> m Bool

isEtaOrCoinductiveRecordConstructor :: HasConstInfo m => QName -> m Bool

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

isInductiveRecord :: HasConstInfo m => QName -> m Bool

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

isEtaRecordType :: HasConstInfo m => Type -> m (Maybe (QName, Args))

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

isRecordConstructor :: HasConstInfo m => QName -> m (Maybe (QName, Defn))

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

isGeneratedRecordConstructor :: (MonadTCEnv m, HasConstInfo m) => QName -> m Bool

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

Works also for abstract constructors.

unguardedRecord :: QName -> PatternOrCopattern -> TCM ()

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

updateEtaForRecord :: QName -> TCM ()

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

recursiveRecord :: QName -> TCM ()

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

nonRecursiveRecord :: QName -> TCM ()

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

isRecursiveRecord :: QName -> TCM Bool

Check whether record type is marked as recursive.

Precondition: record type identifier exists in signature.

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

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 :: PureTCM m => Int -> Telescope -> m (Maybe (Telescope, Substitution, Substitution, Telescope))

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

expandRecordVarsRecursively :: [Int] -> Telescope -> TCM (Telescope, Substitution, Substitution)

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

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

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 :: (HasConstInfo m, MonadDebug m, ReadTCState m) => QName -> Args -> Term -> m (Telescope, Args)

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.

forceEtaExpandRecord :: (HasConstInfo m, MonadDebug m, ReadTCState m, MonadError TCErr m) => QName -> Args -> Term -> m (Telescope, Args)

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

etaExpandRecord' :: (HasConstInfo m, MonadDebug m, ReadTCState m) => Bool -> QName -> Args -> Term -> m (Telescope, Args)

etaExpandRecord_ :: HasConstInfo m => QName -> Args -> Defn -> Term -> m (Telescope, ConHead, ConInfo, Args)

etaExpandRecord'_ :: HasConstInfo m => Bool -> QName -> Args -> Defn -> Term -> m (Telescope, ConHead, ConInfo, Args)

etaExpandAtRecordType :: Type -> Term -> TCM (Telescope, Term)

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

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.

isSingletonRecord :: (PureTCM m, MonadBlock m) => QName -> Args -> m 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 :: (PureTCM m, MonadBlock m) => QName -> Args -> m Bool

isSingletonRecord'

Arguments

:: forall m. (PureTCM m, MonadBlock m)

=> Bool

Should disregard irrelevant fields?

-> QName

Name of record type to check.

-> Args

Parameters given to the record type.

-> Set QName

Non-terminating record types we already encountered. These are considered as non-singletons, otherwise we would construct an infinite inhabitant (in an infinite time...).

-> m (Maybe Term)

The unique inhabitant, if any. May contain dummy terms in irrelevant positions.

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

isSingletonType :: (PureTCM m, MonadBlock m) => Type -> m (Maybe Term)

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

isSingletonTypeModuloRelevance :: (PureTCM m, MonadBlock m) => Type -> m Bool

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

isSingletonType'

Arguments

:: forall m. (PureTCM m, MonadBlock m)

=> Bool

Should disregard irrelevant fields?

-> Type

Type to check.

-> Set QName

Non-terminating record typess we already encountered. These are considered as non-singletons, otherwise we would construct an infinite inhabitant (in an infinite time...).

-> m (Maybe Term)

The unique inhabitant, if any. May contain dummy terms in irrelevant positions.

isEtaVar :: forall m. PureTCM m => Term -> Type -> m (Maybe Int)

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.

class NormaliseProjP a where

Replace projection patterns by the original projections.

Methods

normaliseProjP :: HasConstInfo m => a -> m a

Instances

NormaliseProjP Clause

Defined in Agda.TypeChecking.Records

Methods

normaliseProjP :: HasConstInfo m => Clause -> m Clause

NormaliseProjP a => NormaliseProjP (Arg a)

Defined in Agda.TypeChecking.Records

Methods

normaliseProjP :: HasConstInfo m => Arg a -> m (Arg a)

NormaliseProjP a => NormaliseProjP (Named_ a)

Defined in Agda.TypeChecking.Records

Methods

normaliseProjP :: HasConstInfo m => Named_ a -> m (Named_ a)

NormaliseProjP (Pattern' x)

Defined in Agda.TypeChecking.Records

Methods

normaliseProjP :: HasConstInfo m => Pattern' x -> m (Pattern' x)

NormaliseProjP a => NormaliseProjP [a]

Defined in Agda.TypeChecking.Records

Methods

normaliseProjP :: HasConstInfo m => [a] -> m [a]