Agda-2.6.3.20230805: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.TypeChecking.Records

Synopsis

Documentation

orderFields Source #

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.

orderFieldsWarn Source #

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

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

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

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

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 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 :: (HasConstInfo m, ReadTCState m, MonadError TCErr m) => QName -> m [Dom 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 Source #

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 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 :: PureTCM m => Type -> m (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 :: PureTCM m => Type -> m (Either (Blocked 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).

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

Get the original projection info for name.

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

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

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

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

Typing of an elimination.

Constructors

ArgT (Dom Type)

Type of the argument.

ProjT 

Fields

Instances

Instances details
PrettyTCM ElimType Source # 
Instance details

Defined in Agda.TypeChecking.Records

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Works also for abstract constructors.

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

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

updateEtaForRecord :: QName -> TCM () Source #

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

recursiveRecord :: QName -> TCM () Source #

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

nonRecursiveRecord :: QName -> TCM () Source #

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

isRecursiveRecord :: QName -> TCM Bool Source #

Check whether record type is marked as recursive.

Precondition: record type identifier exists in signature.

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

expandRecordVar :: PureTCM m => Int -> Telescope -> m (Maybe (Telescope, Substitution, Substitution, Telescope)) Source #

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

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

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

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

etaContractRecord :: HasConstInfo m => QName -> ConHead -> ConInfo -> 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.

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

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

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

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

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

isSingletonType' Source #

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

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

Replace projection patterns by the original projections.

Methods

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

Instances

Instances details
NormaliseProjP Clause Source # 
Instance details

Defined in Agda.TypeChecking.Records

NormaliseProjP a => NormaliseProjP (Arg a) Source # 
Instance details

Defined in Agda.TypeChecking.Records

Methods

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

NormaliseProjP a => NormaliseProjP (Named_ a) Source # 
Instance details

Defined in Agda.TypeChecking.Records

Methods

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

NormaliseProjP (Pattern' x) Source # 
Instance details

Defined in Agda.TypeChecking.Records

NormaliseProjP a => NormaliseProjP [a] Source # 
Instance details

Defined in Agda.TypeChecking.Records

Methods

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