ModuleAgda-2.8.0.2Haskell2010

Agda.TypeChecking.Implicit

Functions for inserting implicit arguments at the right places.

1 type
7 values

PackageAgda-2.8.0.2
Exports9
LanguageHaskell2010
LicenceMIT
SourceImplicit.hs

valuesplitImplicitBinderT

:: HasRange a
=> NamedArg a
-> Type
-> TCM (Telescope, Type)

Split a given Pi Type until you reach the given named argument, returning the number of arguments skipped to reach the right plicity and name.

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.8.0.2 · 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.