Safe Haskell	None
Language	Haskell2010

Agda.TypeChecking.Implicit

Description

Functions for inserting implicit arguments at the right places.

Synopsis

implicitArgs :: (MonadReduce m, MonadMetaSolver m, MonadDebug m, MonadTCM m) => Int -> (Hiding -> Bool) -> Type -> m (Args, Type)
implicitNamedArgs :: (MonadReduce m, MonadMetaSolver m, MonadDebug m, MonadTCM m) => Int -> (Hiding -> ArgName -> Bool) -> Type -> m (NamedArgs, Type)
newMetaArg :: 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

implicitArgs Source #

Arguments

:: (MonadReduce m, MonadMetaSolver m, MonadDebug 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

:: (MonadReduce m, MonadMetaSolver m, MonadDebug 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

:: 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 # 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.