Agda-2.6.3.20230914: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.TypeChecking.Implicit

Description

Functions for inserting implicit arguments at the right places.

Synopsis

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

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.