Agda.TypeChecking.Records

Documentation

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

orderFields

Arguments

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

insertMissingFields

Arguments

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

recordModule :: QName -> ModuleName

The name of the module corresponding to a record.

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 :: (MonadReduce m, HasConstInfo m, HasBuiltins 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 :: (MonadReduce m, HasConstInfo m, HasBuiltins 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 :: (HasConstInfo m, MonadReduce m, MonadDebug 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

projectTyped

Arguments

:: (HasConstInfo m, MonadReduce m, MonadDebug 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.

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

Check if a name refers to an eta expandable record.

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 :: QName -> TCM 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 -> TCM ()

Turn off eta for unguarded recursive records. 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 :: Int -> Telescope -> TCM (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, MonadError TCErr 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, MonadError TCErr 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 :: (MonadReduce m, MonadAddContext m, HasConstInfo m, HasBuiltins m, ReadTCState m) => QName -> Args -> m (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.

isSingletonRecordModuloRelevance :: (MonadReduce m, MonadAddContext m, HasConstInfo m, HasBuiltins m, ReadTCState m) => QName -> Args -> m (Either MetaId Bool)

isSingletonRecord' :: forall m. (MonadReduce m, MonadAddContext m, HasConstInfo m, HasBuiltins m, ReadTCState m) => Bool -> QName -> Args -> m (Either MetaId (Maybe Term))

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

isSingletonType :: (MonadReduce m, MonadAddContext m, HasConstInfo m, HasBuiltins m, ReadTCState m) => Type -> m (Either MetaId (Maybe Term))

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

isSingletonTypeModuloRelevance :: (MonadReduce m, MonadAddContext m, HasConstInfo m, HasBuiltins m, ReadTCState m) => Type -> m (Either MetaId Bool)

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

isSingletonType' :: (MonadReduce m, MonadAddContext m, HasConstInfo m, HasBuiltins m, ReadTCState m) => Bool -> Type -> m (Either MetaId (Maybe Term))

isEtaVar :: Term -> Type -> TCM (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.

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

Auxiliary function.

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 [a]

Defined in Agda.TypeChecking.Records

Methods

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

NormaliseProjP a => NormaliseProjP (Named_ a)

Defined in Agda.TypeChecking.Records

Methods

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

NormaliseProjP a => NormaliseProjP (Arg a)

Defined in Agda.TypeChecking.Records

Methods

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

NormaliseProjP (Pattern' x)

Defined in Agda.TypeChecking.Records

Methods

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