| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.TypeChecking.Implicit
Description
Functions for inserting implicit arguments at the right places.
Synopsis
- splitImplicitBinderT :: HasRange a => NamedArg a -> Type -> TCM (Telescope, Type)
- implicitArgs :: (PureTCM m, MonadMetaSolver m, MonadTCM m) => Int -> (Hiding -> Bool) -> Type -> m (Args, Type)
- implicitNamedArgs :: (PureTCM m, MonadMetaSolver m, MonadTCM m) => Int -> (Hiding -> ArgName -> Bool) -> Type -> m (NamedArgs, Type)
- newMetaArg :: (PureTCM m, MonadMetaSolver m) => MetaKind -> ArgInfo -> ArgName -> Comparison -> Type -> m (MetaId, Term)
- newInteractionMetaArg :: ArgInfo -> ArgName -> Comparison -> Type -> TCM (MetaId, Term)
- data ImplicitInsertion
- = ImpInsert [Dom ()]
- | BadImplicits
- | NoSuchName ArgName
- pattern NoInsertNeeded :: ImplicitInsertion
- insertImplicit :: NamedArg e -> [Dom a] -> ImplicitInsertion
- insertImplicit' :: NamedArg e -> [Dom ArgName] -> ImplicitInsertion
Documentation
splitImplicitBinderT :: HasRange a => NamedArg a -> Type -> TCM (Telescope, Type) Source #
Split a given Pi Type until you reach the given named argument,
returning the number of arguments skipped to reach the right plicity
and name.
Arguments
| :: (PureTCM m, MonadMetaSolver m, MonadTCM m) | |
| => Int |
|
| -> (Hiding -> Bool) |
|
| -> Type | The (function) type |
| -> m (Args, Type) | The eliminating arguments and the remaining type. |
implicitArgs n expand t generates up to n implicit argument
metas (unbounded if n<0), as long as t is a function type
and expand holds on the hiding info of its domain.
Arguments
| :: (PureTCM m, MonadMetaSolver m, MonadTCM m) | |
| => Int |
|
| -> (Hiding -> ArgName -> Bool) |
|
| -> Type | The (function) type |
| -> m (NamedArgs, Type) | The eliminating arguments and the remaining type. |
implicitNamedArgs n expand t generates up to n named implicit arguments
metas (unbounded if n<0), as long as t is a function type
and expand holds on the hiding and name info of its domain.
Arguments
| :: (PureTCM m, MonadMetaSolver m) | |
| => MetaKind | Kind of meta. |
| -> ArgInfo | Rrelevance of meta. |
| -> ArgName | Name suggestion for meta. |
| -> Comparison | Check ( |
| -> Type | Type of meta. |
| -> m (MetaId, Term) | The created meta as id and as term. |
Create a metavariable of MetaKind.
newInteractionMetaArg Source #
Arguments
| :: ArgInfo | Relevance of meta. |
| -> ArgName | Name suggestion for meta. |
| -> Comparison | Check ( |
| -> Type | Type of meta. |
| -> TCM (MetaId, Term) | The created meta as id and as term. |
Create a questionmark (always UnificationMeta).
data ImplicitInsertion Source #
Possible results of insertImplicit.
Constructors
| ImpInsert [Dom ()] | Success: this many implicits have to be inserted (list can be empty). |
| BadImplicits | Error: hidden argument where there should have been a non-hidden argument. |
| NoSuchName ArgName | Error: bad named argument. |
Instances
| Show ImplicitInsertion Source # | |
Defined in Agda.TypeChecking.Implicit Methods showsPrec :: Int -> ImplicitInsertion -> ShowS # show :: ImplicitInsertion -> String # showList :: [ImplicitInsertion] -> ShowS # | |
pattern NoInsertNeeded :: ImplicitInsertion Source #
Arguments
| :: NamedArg e | Next given argument |
| -> [Dom a] | Expected arguments |
| -> ImplicitInsertion |
If the next given argument is a and the expected arguments are ts
insertImplicit' a ts returns the prefix of ts that precedes a.
If a is named but this name does not appear in ts, the NoSuchName exception is thrown.
Arguments
| :: NamedArg e | Next given argument |
| -> [Dom ArgName] | Expected arguments |
| -> ImplicitInsertion |
If the next given argument is a and the expected arguments are ts
insertImplicit' a ts returns the prefix of ts that precedes a.
If a is named but this name does not appear in ts, the NoSuchName exception is thrown.