Safe Haskell	None
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) => 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

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)
=> 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 show :: ImplicitInsertion -> String showList :: [ImplicitInsertion] -> ShowS

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.