Agda.TypeChecking.Implicit

Functions for inserting implicit arguments at the right places.

Documentation

insertImplicitBindersT

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

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

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

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

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

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

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

Defined in Agda.TypeChecking.Implicit

Methods

showsPrec :: Int -> ImplicitInsertion -> ShowS

show :: ImplicitInsertion -> String

showList :: [ImplicitInsertion] -> ShowS

pattern NoInsertNeeded :: ImplicitInsertion

insertImplicit

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'

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.