Safe Haskell | None |
---|---|
Language | Haskell98 |
- orderFields :: QName -> a -> [Name] -> [(Name, a)] -> TCM [a]
- recordModule :: QName -> ModuleName
- getRecordDef :: QName -> TCM Defn
- getRecordOfField :: QName -> TCM (Maybe QName)
- getRecordFieldNames :: QName -> TCM [Arg Name]
- recordFieldNames :: Defn -> [Arg Name]
- findPossibleRecords :: [Name] -> TCM [QName]
- getRecordFieldTypes :: QName -> TCM Telescope
- getRecordTypeFields :: Type -> TCM [Arg QName]
- getOriginalProjection :: QName -> TCM QName
- getRecordConstructorType :: QName -> TCM Type
- getRecordConstructor :: QName -> TCM ConHead
- isRecord :: HasConstInfo m => QName -> m (Maybe Defn)
- isRecordType :: Type -> TCM (Maybe (QName, Args, Defn))
- tryRecordType :: Type -> TCM (Either (Maybe Type) (QName, Args, Defn))
- projectTyped :: Term -> Type -> QName -> TCM (Maybe (Term, Type))
- isEtaRecord :: HasConstInfo m => QName -> m Bool
- isEtaCon :: HasConstInfo m => QName -> m Bool
- isInductiveRecord :: QName -> TCM Bool
- isEtaRecordType :: Type -> TCM (Maybe (QName, Args))
- isRecordConstructor :: MonadTCM tcm => QName -> tcm (Maybe (QName, Defn))
- isGeneratedRecordConstructor :: QName -> TCM Bool
- unguardedRecord :: QName -> TCM ()
- recursiveRecord :: QName -> TCM ()
- isRecursiveRecord :: QName -> TCM Bool
- recRecursive_ :: Defn -> 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 :: QName -> Args -> Term -> TCM (Telescope, Args)
- etaExpandRecord_ :: QName -> Args -> Defn -> Term -> TCM (Telescope, ConHead, Args)
- etaExpandAtRecordType :: Type -> Term -> TCM (Telescope, Term)
- etaContractRecord :: HasConstInfo m => QName -> ConHead -> Args -> m Term
- isSingletonRecord :: QName -> Args -> TCM (Either MetaId Bool)
- isSingletonRecordModuloRelevance :: QName -> Args -> TCM (Either MetaId Bool)
- isSingletonRecord' :: Bool -> QName -> Args -> TCM (Either MetaId (Maybe Term))
- isSingletonType :: Type -> TCM (Either MetaId (Maybe Term))
- isSingletonTypeModuloRelevance :: MonadTCM tcm => Type -> tcm (Either MetaId Bool)
- isSingletonType' :: Bool -> Type -> TCM (Either MetaId (Maybe Term))
- emap :: (a -> b) -> Either c (Maybe a) -> Either c (Maybe b)
Documentation
orderFields :: QName -> a -> [Name] -> [(Name, a)] -> TCM [a] Source
Order the fields of a record construction. Use the second argument for missing fields.
recordModule :: QName -> ModuleName Source
The name of the module corresponding to a record.
getRecordDef :: QName -> TCM 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.
recordFieldNames :: Defn -> [Arg 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 :: Type -> TCM [Arg QName] Source
Get the field names belonging to a record type.
getOriginalProjection :: QName -> TCM QName Source
Get the original name of the projection (the current one could be from a module application).
getRecordConstructorType :: QName -> TCM Type Source
Get the type of the record constructor.
getRecordConstructor :: QName -> TCM 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 :: Type -> TCM (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 :: Type -> TCM (Either (Maybe 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).
projectTyped :: Term -> Type -> QName -> TCM (Maybe (Term, Type)) Source
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
.
Works also for projection-like definitions f
.
Precondition: t
is reduced.
isEtaRecord :: HasConstInfo m => QName -> m Bool Source
Check if a name refers to an eta expandable record.
isEtaCon :: HasConstInfo m => QName -> m Bool Source
isInductiveRecord :: QName -> TCM Bool Source
Check if a name refers to a record which is not coinductive. (Projections are then size-preserving)
isEtaRecordType :: Type -> TCM (Maybe (QName, Args)) Source
Check if a type is an eta expandable record and return the record identifier and the parameters.
isRecordConstructor :: MonadTCM tcm => QName -> tcm (Maybe (QName, Defn)) Source
Check if a name refers to a record constructor. If yes, return record definition.
isGeneratedRecordConstructor :: QName -> TCM Bool Source
Check if a constructor name is the internally generated record constructor.
unguardedRecord :: QName -> TCM () Source
Mark record type as unguarded. No eta-expansion. Projections do not preserve guardedness.
recursiveRecord :: QName -> TCM () Source
Mark record type as recursive. Projections do not preserve guardedness.
isRecursiveRecord :: QName -> TCM Bool Source
Check whether record type is marked as recursive.
Precondition: record type identifier exists in signature.
recRecursive_ :: Defn -> Bool Source
Version of recRecursive
with proper internal error.
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 :: QName -> Args -> Term -> TCM (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 a 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
.
etaContractRecord :: HasConstInfo m => QName -> ConHead -> 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
.
TODO: this can be moved out of TCM (but only if ConHead stores also the Arg-decoration of the record fields.
isSingletonRecord :: QName -> Args -> TCM (Either MetaId 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' :: Bool -> QName -> Args -> TCM (Either MetaId (Maybe Term)) Source
Return the unique (closed) inhabitant if exists. In case of counting irrelevance in, the returned inhabitant contains garbage.
isSingletonType :: Type -> TCM (Either MetaId (Maybe Term)) Source
Check whether a type has a unique inhabitant and return it. Can be blocked by a metavar.