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

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.

implicitArgs Source #

Arguments

:: (PureTCM m, MonadMetaSolver m, MonadTCM m) |
=> Int | `n`, the maximum number of implicts to be inserted.
-> (Hiding -> Bool) | `expand`, the predicate to test whether we should keep inserting.
-> Type | The (function) type `t` we are eliminating.
-> 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.

implicitNamedArgs Source #

Arguments

:: (PureTCM m, MonadMetaSolver m, MonadTCM m) |
=> Int | `n`, the maximum number of implicts to be inserted.
-> (Hiding -> ArgName -> Bool) | `expand`, the predicate to test whether we should keep inserting.
-> Type | The (function) type `t` we are eliminating.
-> 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.

newMetaArg Source #

Arguments

:: (PureTCM m, MonadMetaSolver m) |
=> MetaKind | Kind of meta.
-> ArgInfo | Rrelevance of meta.
-> ArgName | Name suggestion for meta.
-> Comparison | Check (`CmpLeq`) or infer (`CmpEq`) the type.
-> 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 (`CmpLeq`) or infer (`CmpEq`) the type.
-> 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

Instances details

Show ImplicitInsertion Source # |
Instance details Defined in Agda.TypeChecking.Implicit Methods showsPrec :: Int -> ImplicitInsertion -> ShowS Source # show :: ImplicitInsertion -> String Source # showList :: [ImplicitInsertion] -> ShowS Source #

pattern NoInsertNeeded :: ImplicitInsertion Source #

insertImplicit Source #

Arguments

:: NamedArg e | Next given argument `a`.
-> [Dom a] | Expected arguments `ts`.
-> 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.

insertImplicit' Source #

Arguments

:: NamedArg e | Next given argument `a`.
-> [Dom ArgName] | Expected arguments `ts`.
-> 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.