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

Safe Haskell | Safe-Inferred
Language | Haskell2010

Agda.TypeChecking.Implicit

Description

Functions for inserting implicit arguments at the right places.

Synopsis

- insertImplicitBindersT :: (PureTCM m, MonadError TCErr m, MonadFresh NameId m, MonadTrace m) => [NamedArg Binder] -> Type -> m [NamedArg Binder]
- insertImplicitBindersT1 :: (PureTCM m, MonadError TCErr m, MonadFresh NameId m, MonadTrace m) => List1 (NamedArg Binder) -> Type -> m (List1 (NamedArg Binder))
- 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) => 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

insertImplicitBindersT Source #

Arguments

:: (PureTCM m, MonadError TCErr m, MonadFresh NameId m, MonadTrace m) |
=> [NamedArg Binder] | Should be non-empty, otherwise nothing happens.
-> Type | Function type eliminated by arguments given by binders.
-> m [NamedArg Binder] | Padded binders.

Insert implicit binders in a list of binders, but not at the end.

insertImplicitBindersT1 Source #

Arguments

:: (PureTCM m, MonadError TCErr m, MonadFresh NameId m, MonadTrace m) |
=> List1 (NamedArg Binder) | Non-empty.
-> Type | Function type eliminated by arguments given by binders.
-> m (List1 (NamedArg Binder)) | Padded binders.

Insert implicit binders in a list of binders, but not at the end.

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) |
=> ArgInfo | Kind/relevance 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 according to the `Hiding` info.

newInteractionMetaArg Source #

Arguments

:: ArgInfo | Kind/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 according to the `Hiding` info.

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.