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

Safe Haskell | Safe-Inferred
Language | Haskell2010

Agda.TypeChecking.Records

Synopsis

- mkCon :: ConHead -> ConInfo -> Args -> Term
- orderFields :: forall a. 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 :: forall a. HasRange a => QName -> (Arg Name -> a) -> [Arg Name] -> [(Name, a)] -> TCM [a]
- orderFieldsFail :: forall a. HasRange a => QName -> (Arg Name -> a) -> [Arg Name] -> [(Name, a)] -> TCM [a]
- insertMissingFields :: forall a. HasRange a => QName -> (Name -> a) -> [FieldAssignment' a] -> [Arg Name] -> Writer [RecordFieldWarning] [NamedArg a]
- insertMissingFieldsWarn :: forall a. HasRange a => QName -> (Name -> a) -> [FieldAssignment' a] -> [Arg Name] -> TCM [NamedArg a]
- insertMissingFieldsFail :: forall a. HasRange a => QName -> (Name -> a) -> [FieldAssignment' a] -> [Arg Name] -> TCM [NamedArg a]
- getRecordDef :: (HasConstInfo m, ReadTCState m, MonadError TCErr m) => QName -> m Defn
- getRecordOfField :: QName -> TCM (Maybe QName)
- getRecordFieldNames :: (HasConstInfo m, ReadTCState m, MonadError TCErr m) => QName -> m [Dom Name]
- getRecordFieldNames_ :: (HasConstInfo m, ReadTCState m) => QName -> m (Maybe [Dom Name])
- recordFieldNames :: Defn -> [Dom Name]
- findPossibleRecords :: [Name] -> TCM [QName]
- getRecordFieldTypes :: QName -> TCM Telescope
- getRecordTypeFields :: Type -> TCM [Dom QName]
- getRecordConstructor :: (HasConstInfo m, ReadTCState m, MonadError TCErr m) => QName -> m ConHead
- isRecord :: HasConstInfo m => QName -> m (Maybe Defn)
- isRecordType :: PureTCM m => Type -> m (Maybe (QName, Args, Defn))
- tryRecordType :: PureTCM m => Type -> m (Either (Blocked Type) (QName, Args, Defn))
- origProjection :: HasConstInfo m => QName -> m (QName, Definition, Maybe Projection)
- getDefType :: PureTCM m => QName -> Type -> m (Maybe 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]
- isEtaRecord :: HasConstInfo m => QName -> m Bool
- isEtaCon :: HasConstInfo m => QName -> m Bool
- isEtaOrCoinductiveRecordConstructor :: HasConstInfo m => QName -> m Bool
- isInductiveRecord :: QName -> TCM Bool
- isEtaRecordType :: HasConstInfo m => Type -> m (Maybe (QName, Args))
- isRecordConstructor :: HasConstInfo m => QName -> m (Maybe (QName, Defn))
- isGeneratedRecordConstructor :: (MonadTCEnv m, HasConstInfo m) => QName -> m Bool
- unguardedRecord :: QName -> PatternOrCopattern -> TCM ()
- recursiveRecord :: QName -> TCM ()
- nonRecursiveRecord :: QName -> TCM ()
- isRecursiveRecord :: QName -> TCM Bool
- etaExpandBoundVar :: Int -> TCM (Maybe (Telescope, Substitution, Substitution))
- expandRecordVar :: Int -> Telescope -> TCM (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 -> 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
- isSingletonRecord :: (PureTCM m, MonadBlock m) => QName -> Args -> m Bool
- isSingletonRecordModuloRelevance :: (PureTCM m, MonadBlock m) => QName -> Args -> m Bool
- isSingletonRecord' :: forall m. (PureTCM m, MonadBlock m) => Bool -> QName -> Args -> 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 -> m (Maybe Term)
- isEtaVar :: forall m. PureTCM m => Term -> Type -> m (Maybe Int)
- class NormaliseProjP a where
  - normaliseProjP :: HasConstInfo m => a -> m a

# Documentation

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

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.

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

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

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

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

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`

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.

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

Check if a name refers to an eta expandable record.

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

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 :: Int -> Telescope -> TCM (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.

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

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

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

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

isSingletonRecordModuloRelevance :: (PureTCM m, MonadBlock m) => QName -> Args -> m Bool Source #

isSingletonRecord' :: forall m. (PureTCM m, MonadBlock m) => Bool -> QName -> Args -> m (Maybe Term) Source #

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' :: (PureTCM m, MonadBlock m) => Bool -> Type -> m (Maybe Term) Source #

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