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

Safe Haskell | None
Language | Haskell2010

Agda.TypeChecking.Records

Contents

- Tools to build record values
- Query information about records from signature

Synopsis

- mkCon :: ConHead -> ConInfo -> Args -> Term
- orderFields :: HasRange a => QName -> (Arg Name -> a) -> [Arg Name] -> [(Name, a)] -> Writer [RecordFieldWarning] [a]
- warnOnRecordFieldWarnings :: Writer [RecordFieldWarning] a -> TCM a
- failOnRecordFieldWarnings :: Writer [RecordFieldWarning] a -> TCM a
- orderFieldsWarn :: HasRange a => QName -> (Arg Name -> a) -> [Arg Name] -> [(Name, a)] -> TCM [a]
- orderFieldsFail :: HasRange a => QName -> (Arg Name -> a) -> [Arg Name] -> [(Name, a)] -> TCM [a]
- insertMissingFields :: HasRange a => QName -> (Name -> a) -> [FieldAssignment' a] -> [Arg Name] -> Writer [RecordFieldWarning] [NamedArg a]
- insertMissingFieldsWarn :: HasRange a => QName -> (Name -> a) -> [FieldAssignment' a] -> [Arg Name] -> TCM [NamedArg a]
- insertMissingFieldsFail :: HasRange a => QName -> (Name -> a) -> [FieldAssignment' a] -> [Arg Name] -> TCM [NamedArg a]
- isRecord :: HasConstInfo m => QName -> m (Maybe RecordData)
- getRecordDef :: (HasConstInfo m, ReadTCState m, MonadError TCErr m) => QName -> m RecordData
- getRecordOfField :: QName -> TCM (Maybe QName)
- getRecordFieldNames :: (HasConstInfo m, ReadTCState m, MonadError TCErr m) => QName -> m [Dom Name]
- recordFieldNames :: RecordData -> [Dom Name]
- findPossibleRecords :: [Name] -> TCM [QName]
- getRecordTypeFields :: Type -> TCM [Dom QName]
- getRecordConstructor :: (HasConstInfo m, ReadTCState m, MonadError TCErr m) => QName -> m ConHead
- isRecordType :: PureTCM m => Type -> m (Maybe (QName, Args, RecordData))
- tryRecordType :: PureTCM m => Type -> m (Either (Blocked Type) (QName, Args, RecordData))
- origProjection :: HasConstInfo m => QName -> m (QName, Definition, Maybe Projection)
- getDefType :: PureTCM m => QName -> Type -> m (Maybe Type)
- shouldBeProjectible :: (PureTCM m, MonadTCError m, MonadBlock m) => Term -> Type -> ProjOrigin -> QName -> m Type
- projectTyped :: PureTCM m => Term -> Type -> ProjOrigin -> QName -> m (Maybe (Dom Type, Term, Type))
- data ElimType
  - = ArgT (Dom Type)
  - | ProjT {
    - projTRec :: Dom Type
    - projTField :: Type
    }
- typeElims :: Type -> Term -> Elims -> TCM [ElimType]
- eliminateType :: PureTCM m => m Empty -> Term -> Type -> Elims -> m Type
- eliminateType' :: PureTCM m => m Empty -> (Elims -> Term) -> Type -> Elims -> m Type
- isEtaRecord :: HasConstInfo m => QName -> m Bool
- isEtaRecordDef :: RecordData -> Bool
- isEtaCon :: HasConstInfo m => QName -> m Bool
- isEtaOrCoinductiveRecordConstructor :: HasConstInfo m => QName -> m Bool
- isInductiveRecord :: HasConstInfo m => QName -> m Bool
- isEtaRecordType :: HasConstInfo m => Type -> m (Maybe (QName, Args))
- isRecordConstructor :: HasConstInfo m => QName -> m (Maybe (QName, RecordData))
- isEtaRecordConstructor :: HasConstInfo m => QName -> m (Maybe (QName, RecordData))
- unguardedRecord :: QName -> PatternOrCopattern -> TCM ()
- updateEtaForRecord :: QName -> TCM ()
- recursiveRecord :: QName -> TCM ()
- nonRecursiveRecord :: QName -> TCM ()
- isRecursiveRecord :: QName -> TCM Bool
- etaExpandBoundVar :: Int -> TCM (Maybe (Telescope, Substitution, Substitution))
- expandRecordVar :: PureTCM m => Int -> Telescope -> m (Maybe (Telescope, Substitution, Substitution, Telescope))
- expandRecordVarsRecursively :: [Int] -> Telescope -> TCM (Telescope, Substitution, Substitution)
- curryAt :: Type -> Int -> TCM (Term -> Term, Term -> Term, Type)
- etaExpandRecord :: (HasConstInfo m, MonadDebug m, ReadTCState m) => QName -> Args -> Term -> m (Telescope, Args)
- forceEtaExpandRecord :: (HasConstInfo m, MonadDebug m, ReadTCState m, MonadError TCErr m) => QName -> Args -> Term -> m (Telescope, Args)
- etaExpandRecord' :: (HasConstInfo m, MonadDebug m, ReadTCState m) => Bool -> QName -> Args -> Term -> m (Telescope, Args)
- etaExpandRecord_ :: HasConstInfo m => QName -> Args -> RecordData -> Term -> m (Telescope, ConHead, ConInfo, Args)
- etaExpandRecord'_ :: HasConstInfo m => Bool -> QName -> Args -> RecordData -> Term -> m (Telescope, ConHead, ConInfo, Args)
- etaExpandAtRecordType :: Type -> Term -> TCM (Telescope, Term)
- etaContractRecord :: HasConstInfo m => QName -> ConHead -> ConInfo -> Args -> m Term
- isSingletonRecord :: (PureTCM m, MonadBlock m) => QName -> Args -> m Bool
- isSingletonRecordModuloRelevance :: (PureTCM m, MonadBlock m) => QName -> Args -> m Bool
- isSingletonRecord' :: (PureTCM m, MonadBlock m) => Bool -> QName -> Args -> Set QName -> m (Maybe Term)
- isSingletonType :: (PureTCM m, MonadBlock m) => Type -> m (Maybe Term)
- isSingletonTypeModuloRelevance :: (PureTCM m, MonadBlock m) => Type -> m Bool
- isSingletonType' :: (PureTCM m, MonadBlock m) => Bool -> Type -> Set QName -> m (Maybe Term)
- isEtaVar :: PureTCM m => Term -> Type -> m (Maybe Int)
- class NormaliseProjP a where
  - normaliseProjP :: HasConstInfo m => a -> m a

# Tools to build record values

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

orderFields Source #

Arguments

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

Raise generated `RecordFieldWarning`s as warnings.

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

Raise generated `RecordFieldWarning`s as errors.

orderFieldsWarn Source #

Arguments

:: 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 `RecordFieldWarning`s as warnings.

orderFieldsFail Source #

Arguments

:: 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 `RecordFieldWarning`s as errors.

insertMissingFields Source #

Arguments

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

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

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

# Query information about records from signature

isRecord :: HasConstInfo m => QName -> m (Maybe RecordData) Source #

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

getRecordDef :: (HasConstInfo m, ReadTCState m, MonadError TCErr m) => QName -> m RecordData 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.

recordFieldNames :: RecordData -> [Dom Name] Source #

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

Find all records with at least the given fields.

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

isRecordType :: PureTCM m => Type -> m (Maybe (QName, Args, RecordData)) 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, RecordData)) 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

- projTRec :: Dom Type

  The type of the record which is eliminated.

- projTField :: Type

  The type of the field.

#### Instances

Instances details

PrettyTCM ElimType Source # |
Instance details Defined in Agda.TypeChecking.Records Methods prettyTCM :: MonadPretty m => ElimType -> m Doc Source #

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

isEtaRecordDef :: RecordData -> Bool Source #

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

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

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

isEtaRecordConstructor :: HasConstInfo m => QName -> m (Maybe (QName, RecordData)) Source #

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

Arguments

:: (HasConstInfo m, MonadDebug m, ReadTCState m) |
=> QName | Name of record type.
-> Args | Parameters applied to record type.
-> Term | Term to eta-expand.
-> m (Telescope, Args) | Field types instantiated to parameters, field values.

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

Arguments

:: (HasConstInfo m, MonadDebug m, ReadTCState m, MonadError TCErr m) |
=> QName | Name of record type.
-> Args | Parameters applied to record type.
-> Term | Term to eta-expand.
-> m (Telescope, Args) | Field types instantiated to parameters, field values.

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

etaExpandRecord' Source #

Arguments

:: (HasConstInfo m, MonadDebug m, ReadTCState m) |
=> Bool | Force expansion, overriding `_recEtaEquality`?
-> QName | Name of record type.
-> Args | Parameters applied to record type.
-> Term | Term to eta-expand.
-> m (Telescope, Args) | Field types instantiated to parameters, field values.

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

etaExpandRecord_ Source #

Arguments

:: HasConstInfo m |
=> QName | Name of record type.
-> Args | Parameters applied to record type.
-> RecordData | Definition of record type.
-> Term | Term to eta-expand.
-> m (Telescope, ConHead, ConInfo, Args) | Field types instantiated to parameters, disassembled constructor term.

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

etaExpandRecord'_ Source #

Arguments

:: HasConstInfo m |
=> Bool | Force expansion, overriding `_recEtaEquality`?
-> QName | Name of record type.
-> Args | Parameters applied to record type.
-> RecordData | Definition of record type.
-> Term | Term to eta-expand.
-> m (Telescope, ConHead, ConInfo, Args) | Field types instantiated to parameters, disassembled constructor term.

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

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

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

Arguments

:: (PureTCM m, MonadBlock m) |
=> QName | Name of record type to check.
-> Args | Parameters given to the record type.
-> 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 Source #

Arguments

:: (PureTCM m, MonadBlock m) |
=> QName | Name of record type to check.
-> Args | Parameters given to the record type.
-> m Bool |

isSingletonRecord' Source #

Arguments

:: (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

:: (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 :: 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 Methods normaliseProjP :: HasConstInfo m => Clause -> m Clause Source #
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 Methods normaliseProjP :: HasConstInfo m => Pattern' x -> m (Pattern' x) Source #
NormaliseProjP a => NormaliseProjP [a] Source # |
Instance details Defined in Agda.TypeChecking.Records Methods normaliseProjP :: HasConstInfo m => [a] -> m [a] Source #