ModuleAgda-2.7.0.1Haskell2010

Agda.TypeChecking.Implicit

Functions for inserting implicit arguments at the right places.

1 type
8 values

PackageAgda-2.7.0.1
Exports10
LanguageHaskell2010
LicenceMIT
SourceImplicit.hs

valueinsertImplicitBindersT

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

valueinsertImplicitBindersT1

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

valueimplicitArgs

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

valueimplicitNamedArgs

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

valuenewMetaArg

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

valuenewInteractionMetaArg

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

datadata 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.

Instances1Show

Show ImplicitInsertionDefined in Agda-2.7.0.1 · Agda.TypeChecking.Implicit

patternpattern NoInsertNeeded :: ImplicitInsertion

valueinsertImplicit

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

valueinsertImplicit'

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