The kind of a tactic metavariable, used for additional error reporting.
- term : TacticMVarKind
Standard tactic metavariable, arising from
by ...
syntax. - autoParam
(argName : Name)
: TacticMVarKind
Tactic metavariable arising from an autoparam for a function application.
- fieldAutoParam
(fieldName structName : Name)
: TacticMVarKind
Tactic metavariable arising from an autoparam for a structure field.
Instances For
We use synthetic metavariables as placeholders for pending elaboration steps.
- typeClass
(extraErrorMsg? : Option MessageData)
: SyntheticMVarKind
Use typeclass resolution to synthesize value for metavariable. If
extraErrorMsg?
issome msg
,msg
contains additional information to include in error messages regarding type class synthesis failure. - coe
(header? : Option String)
(expectedType e : Expr)
(f? : Option Expr)
(mkErrorMsg? : Option (MVarId → Expr → Expr → MetaM MessageData))
: SyntheticMVarKind
Use coercion to synthesize value for the metavariable. If synthesis fails, then throws an error.
- If
mkErrorMsg?
is provided, then the errormkErrorMsg expectedType e
is thrown. ThemkErrorMsg
function is allowed to throw an error itself. - Otherwise, throws a default type mismatch error message.
If
header?
is not provided, the default header is "type mismatch". Iff?
is provided, then throws an application type mismatch error.
- If
- tactic
(tacticCode : Syntax)
(ctx : SavedContext)
(kind : TacticMVarKind)
: SyntheticMVarKind
Use tactic to synthesize value for metavariable.
- postponed
(ctx : SavedContext)
: SyntheticMVarKind
Metavariable represents a hole whose elaboration has been postponed.
Instances For
Convert an "extra" optional error message into a message "\n{msg}"
(if some msg
) and MessageData.nil
(if none
)
Equations
Instances For
- stx : Syntax
- kind : SyntheticMVarKind
Instances For
We can optionally associate an error context with a metavariable (see MVarErrorInfo
).
We have three different kinds of error context.
- implicitArg
(lctx : LocalContext)
(ctx : Expr)
: MVarErrorKind
Metavariable for implicit arguments.
ctx
is the parent application,lctx
is a local context where it is valid (necessary for eta feature for named arguments). - hole : MVarErrorKind
Metavariable for explicit holes provided by the user (e.g.,
_
and?m
) - custom
(msgData : MessageData)
: MVarErrorKind
"Custom",
msgData
stores the additional error messages.
Instances For
We can optionally associate an error context with metavariables.
- mvarId : MVarId
- ref : Syntax
- kind : MVarErrorKind
Instances For
When reporting unexpected universe level metavariables, it is useful to localize the errors
to particular terms, especially at let
bindings and function binders,
where universe polymorphism is not permitted.
- lctx : LocalContext
- expr : Expr
- ref : Syntax
- msgData? : Option MessageData
Instances For
Equations
Nested let rec
expressions are eagerly lifted by the elaborator.
We store the information necessary for performing the lifting here.
- ref : Syntax
- fvarId : FVarId
- shortDeclName : Name
- declName : Name
- lctx : LocalContext
- localInstances : LocalInstances
- type : Expr
- val : Expr
- mvarId : MVarId
- termination : TerminationHints
Instances For
State of the TermElabM
monad.
- syntheticMVars : MVarIdMap SyntheticMVarDecl
- mvarErrorInfos : List MVarErrorInfo
List of errors associated to a metavariable that are shown to the user if the metavariable could not be fully instantiated
- levelMVarErrorInfos : List LevelMVarErrorInfo
List of data to be able to localize universe level metavariable errors to particular expressions.
mvarArgNames
stores the argument names associated to metavariables. These are used in combination withmvarErrorInfos
for throwing errors about metavariables that could not be fully instantiated. For example when elaboratingList _
, the argument name of the placeholder will beα
.While elaborating an application,
mvarArgNames
is set for each metavariable argument, using the available argument name. This may happen before or after themvarErrorInfos
is set for the same metavariable.We used to store the argument names in
mvarErrorInfos
, updating theMVarErrorInfos
to add the argument name when it is available, but this doesn't work if the argument name is available before themvarErrorInfos
is set for that metavariable.- letRecsToLift : List LetRecToLift
Instances For
State of the TacticM
monad.
Instances For
Snapshots are used to implement the save
tactic.
This tactic caches the state of the system, and allows us to "replay"
expensive proofs efficiently. This is only relevant implementing the
LSP server.
- core : Core.State
- meta : Meta.State
- term : Term.State
- tactic : State
- stx : Syntax
Instances For
Snapshot after finishing execution of a tactic.
- state? : Option SavedState
State saved for reuse, if no fatal exception occurred.
- moreSnaps : Array (Language.SnapshotTask Language.SnapshotTree)
Untyped snapshots from
logSnapshotTask
, saved at this level for cancellation.
Instances For
Snapshot just before execution of a tactic.
- stx : Syntax
Syntax tree of the tactic, stored and compared for incremental reuse.
- inner? : Option (Language.SnapshotTask TacticParsedSnapshot)
Task for nested incrementality, if enabled for tactic.
- finished : Language.SnapshotTask TacticFinishedSnapshot
Task for state after tactic execution.
Tasks for subsequent, potentially parallel, tactic steps.
Instances For
- macroStack : MacroStack
- mayPostpone : Bool
When
mayPostpone == true
, an elaboration function may interrupt its execution by throwingException.postpone
. The functionelabTerm
catches this exception and creates fresh synthetic metavariable?m
, stores?m
in the list of pending synthetic metavariables, and returns?m
. - errToSorry : Bool
When
errToSorry
is set to true, the methodelabTerm
catches exceptions and converts them into syntheticsorry
s. The implementation of choice nodes and overloaded symbols rely on the fact that whenerrToSorry
is set to false for an elaboration functionF
, thenerrToSorry
remainsfalse
for all elaboration functions invoked byF
. That is, it is safe to transitionerrToSorry
fromtrue
tofalse
, but we must not seterrToSorry
totrue
when it is currently set tofalse
. - autoBoundImplicit : Bool
When
autoBoundImplicit
is set to true, instead of producing an "unknown identifier" error for unbound variables, we generate an internal exception. This exception is caught atelabBinders
andelabTypeWithUnboldImplicit
. Both methods add implicit declarations for the unbound variable and try again. A name
n
is only eligible to be an auto implicit name ifautoBoundImplicitForbidden n = false
. We use this predicate to disallowf
to be considered an auto implicit name in a definition such asdef f : f → Bool := fun _ => true
Map from user name to internal unique name
Map from internal name to fvar
- implicitLambda : Bool
Enable/disable implicit lambdas feature.
- heedElabAsElim : Bool
Heed
elab_as_elim
attribute. - isNoncomputableSection : Bool
Noncomputable sections automatically add the
noncomputable
modifier to any declaration we cannot generate code for. - ignoreTCFailures : Bool
When
true
we skip TC failures. We use this option when processing patterns. - inPattern : Bool
true
when elaborating patterns. It affects how we elaborate named holes. - tacSnap? : Option (Language.SnapshotBundle Tactic.TacticParsedSnapshot)
Snapshot for incremental processing of current tactic, if any.
Invariant: if the bundle's
old?
is set, then the state up to the start of the tactic is unchanged, i.e. reuse is possible. - saveRecAppSyntax : Bool
If
true
, we store in theExpr
theSyntax
for recursive applications (i.e., applications of free variables tagged withisAuxDecl
). We store theSyntax
usingmkRecAppWithSyntax
. We use theSyntax
object to produce better error messages atStructural.lean
andWF.lean
. - holesAsSyntheticOpaque : Bool
If
holesAsSyntheticOpaque
istrue
, then we mark metavariables associated with_
s assyntheticOpaque
if they do not occur in patterns. This option is useful when elaborating terms in tactics such asrefine'
where we want holes there to become new goals. See issue #1681, we have `refine' (fun x => _) - checkDeprecated : Bool
If
checkDeprecated := true
, thenLinter.checkDeprecated
when creating constants.
Instances For
Equations
Instances For
Like Meta.withRestoreOrSaveFull
for TermElabM
, but also takes a tacSnap?
that
- when running
act
, is set asContext.tacSnap?
- otherwise (i.e. on restore) is used to update the new snapshot promise to the old task's
value.
This extra restore step is necessary because while
reusableResult?
can be used to replay any effects onState
,Context.tacSnap?
is not part of it but changed via anIO
side effect, so it needs to be replayed separately.
We use an explicit parameter instead of accessing Context.tacSnap?
directly because this prevents
withRestoreOrSaveFull
and withReader
from being used in the wrong order.
Equations
Instances For
Incremental elaboration helper. Avoids leakage of data from outside syntax via the monadic context
when running act
on stx
by
- setting
stx
as theref
and - deactivating
suppressElabErrors
ifstx
ismissing
-free, which also helps with not hiding useful errors in this part of the input. Note that ifstx
hasmissing
, this should always be true for the outer syntax as well, so taking the old value ofsuppressElabErrors
into account should not introduce data leakage.
This combinator should always be used when narrowing reuse to a syntax subtree, usually (in the case
of tactics, to be generalized) via withNarrowed(Arg)TacticReuse
.
Equations
Instances For
Manages reuse information for nested tactics by split
ting given syntax into an outer and inner
part. act
is then run on the inner part but with reuse information adjusted as following:
- If the old (from
tacSnap?
'sSyntaxGuarded.stx
) and new (fromstx
) outer syntax are not identical according toSyntax.eqWithInfo
, reuse is disabled. - Otherwise, the old syntax as stored in
tacSnap?
is updated to the old inner syntax. - In any case,
withReuseContext
is used on the new inner syntax to further prepare the monadic context.
For any tactic that participates in reuse, withNarrowedTacticReuse
should be applied to the
tactic's syntax and act
should be used to do recursive tactic evaluation of nested parts. Also,
after this function, getAndEmptySnapshotTasks
should be called and the result stored in a snapshot
so that the tasks don't end up in a snapshot further up and are cancelled together with it; see
note [Incremental Cancellation].
Equations
Instances For
A variant of withNarrowedTacticReuse
that uses stx[argIdx]
as the inner syntax and all stx
child nodes before that as the outer syntax, i.e. reuse is disabled if there was any change before
argIdx
.
NOTE: child nodes after argIdx
are not tested (which would almost always disable reuse as they are
necessarily shifted by changes at argIdx
) so it must be ensured that the result of arg
does not
depend on them (i.e. they should not be inspected beforehand).
Equations
Instances For
Disables incremental tactic reuse and reporting for act
if cond
is true by setting tacSnap?
to none
. This should be done for tactic blocks that are run multiple times as otherwise the
reported progress will jump back and forth (and partial reuse for these kinds of tact blocks is
similarly questionable).
Equations
Instances For
Disables incremental tactic reuse for act
if cond
is true.
Equations
Instances For
Wraps the given action for use in BaseIO.asTask
etc., discarding its final state except for
logSnapshotTask
tasks, which are reported as part of the returned tree. The given cancellation
token, if any, should be stored in a SnapshotTask
for the server to trigger it when the result is
no longer needed.
Equations
Instances For
Equations
Instances For
Execute x
, save resulting expression and new state.
We remove any Info
created by x
.
The info nodes are committed when we execute applyResult
.
We use observing
to implement overloaded notation and decls.
We want to save Info
nodes for the chosen alternative.
Equations
Instances For
Apply the result/exception and state captured with observing
.
We use this method to implement overloaded notation and symbols.
Equations
Instances For
Execute x
, but keep state modifications only if x
did not postpone.
This method is useful to implement elaboration functions that cannot decide whether
they need to postpone or not without updating the state.
Equations
Instances For
Return the universe level names explicitly provided by the user.
Equations
Instances For
Given a free variable fvar
, return its declaration.
This function panics if fvar
is not a free variable.
Equations
Instances For
Execute x
without storing Syntax
for recursive applications. See saveRecAppSyntax
field at Context
.
Equations
Instances For
Equations
Instances For
Auxiliary datatype for presenting a Lean lvalue modifier.
We represent an unelaborated lvalue as a Syntax
(or Expr
) and List LVal
.
Example: a.foo.1
is represented as the Syntax
a
and the list
[LVal.fieldName "foo", LVal.fieldIdx 1]
.
- fieldIdx (ref : Syntax) (i : Nat) : LVal
- fieldName
(ref : Syntax)
(name : String)
(suffix? : Option Name)
(fullRef : Syntax)
: LVal
Field
suffix?
is for producing better error messages becausex.y
may be a field access or a hierarchical/composite name.ref
is the syntax object representing the field.fullRef
includes the LHS.
Instances For
Return the name of the declaration being elaborated if available.
Equations
Instances For
Return the list of nested let rec
declarations that need to be lifted.
Equations
Instances For
Return the declaration of the given metavariable
Equations
Instances For
Executes x
in the context of the given declaration name. Ensures that the info tree is set up
correctly and adjusts the declaration name generator to generate names below this name, resetting
the nested counter.
Equations
Instances For
Execute x
using levelNames
as the universe level parameter names. See getLevelNames
.
Equations
Instances For
Equations
Instances For
Execute x
without converting errors (i.e., exceptions) to sorry
applications.
Recall that when errToSorry = true
, the method elabTerm
catches exceptions and converts them into sorry
applications.
Equations
Instances For
Equations
Instances For
Execute x
without heeding the elab_as_elim
attribute. Useful when there is
no expected type (so elabAppArgs
would fail), but expect that the user wants
to use such constants.
Equations
Instances For
Execute x
but discard changes performed at Term.State
and Meta.State
.
Recall that the Environment
, InfoState
and messages are at Core.State
. Thus, any updates to
it will be preserved.
This method is useful for performing computations where all metavariable must be resolved or
discarded.
The InfoTree
s are not discarded, however, and wrapped in InfoTree.Context
to store their metavariable context.
Equations
Instances For
Wraps the trees returned from getInfoTrees
, if any, in an InfoTree.context
node based on the
current monadic context and state. This is mainly used to report info trees early via
Snapshot.infoTree?
. The trees are not removed from the getInfoTrees
state as the final info tree
of the elaborated command should be complete and not depend on whether parts have been reported
early.
As InfoTree.context
can have only one child, this function panics if trees
contains more than 1
tree. Also, PartialContextInfo.parentDeclCtx
is not currently generated as that information is not
available in the monadic context and only needed for the final info tree.
Equations
Instances For
Equations
Instances For
Equations
Instances For
Add the given metavariable to the list of pending synthetic metavariables.
The method synthesizeSyntheticMVars
is used to process the metavariables on this list.
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Auxiliary method for reporting errors of the form "... contains metavariables ...".
This kind of error is thrown, for example, at Match.lean
where elaboration
cannot continue if there are metavariables in patterns.
We only want to log it if we haven't logged any errors so far.
Equations
Instances For
Equations
Instances For
Append the argument name (if available) to the message. Remark: if the argument name contains macro scopes we do not append it.
Equations
Instances For
Equations
Instances For
Try to log errors for the unassigned metavariables pendingMVarIds
.
Return true
if there were "unfilled holes", and we should "abort" declaration.
TODO: try to fill "all" holes using synthetic "sorry's"
Remark: We only log the "unfilled holes" as new errors if no error has been logged so far.
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Try to log errors for unassigned level metavariables pendingLevelMVarIds
.
Returns true
if there are any relevant LevelMVarErrorInfo
s and we should "abort" the declaration.
Remark: we only log unassigned level metavariables as new errors if no error has been logged so far.
Equations
Instances For
Ensure metavariables registered using registerMVarErrorInfos
(and used in the given declaration) have been assigned.
Equations
Instances For
Execute x
without allowing it to postpone elaboration tasks.
That is, tryPostpone
is a noop.
Equations
Instances For
Creates syntax for (
<ident> :
<type> )
Equations
Instances For
Convert unassigned universe level metavariables into parameters.
The new parameter names are fresh names of the form u_i
with regard to ctx.levelNames
, which is updated with the new names.
Equations
Instances For
Creates a fresh inaccessible binder name based on x
.
Equivalent to Lean.Core.mkFreshUserName `x
.
Do not confuse with Lean.mkFreshId
, for creating fresh free variable and metavariable ids.
Equations
Instances For
Auxiliary method for creating a Syntax.ident
containing
a fresh name. This method is intended for creating fresh binder names.
It is just a thin layer on top of mkFreshUserName
.
Equations
Instances For
Apply given attributes at a given application time
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
See containsPostponedTerm
Return true
if e
contains a pending metavariable. Remark: it also visits let-declarations.
Equations
Instances For
Try to synthesize metavariable using type class resolution.
This method assumes the local context and local instances of instMVar
coincide
with the current local context and local instances.
Return true
if the instance was synthesized successfully, and false
if
the instance contains unassigned metavariables that are blocking the type class
resolution procedure. Throw an exception if resolution or assignment irrevocably fails.
If extraErrorMsg?
is not none, it contains additional information that should be attached
to type class synthesis failures.
Equations
Instances For
Equations
Instances For
Equations
Instances For
If expectedType?
is some t
, then ensures t
and eType
are definitionally equal by inserting a coercion if necessary.
Argument f?
is used only for generating error messages when inserting coercions fails.
Equations
Instances For
Equations
Instances For
Return true
if e
reduces (by unfolding only [reducible]
declarations) to ?m ...
Equations
Instances For
If mayPostpone == true
and e
's head is a metavariable, throw Exception.postpone
.
Equations
Instances For
Throws Exception.postpone
, if expectedType?
contains unassigned metavariables.
It is a noop if mayPostpone == false
.
Equations
Instances For
Throws Exception.postpone
, if expectedType?
contains unassigned metavariables.
If mayPostpone == false
, it throws error msg
.
Equations
Instances For
Save relevant context for term elaboration postponement.
Equations
Instances For
Execute x
with the context saved using saveContext
.
Equations
Instances For
Equations
Instances For
Creates a new metavariable of type type
that will be synthesized using the tactic code.
The tacticCode
syntax is the full by ..
syntax.
Equations
Instances For
Create an auxiliary annotation to make sure we create an Info
even if e
is a metavariable.
See mkTermInfo
.
We use this function because some elaboration functions elaborate subterms that may not be immediately part of the resulting term. Example:
let_mvar% ?m := b; wait_if_type_mvar% ?m; body
If the type of b
is not known, then wait_if_type_mvar% ?m; body
is postponed and just returns a fresh
metavariable ?n
. The elaborator for
let_mvar% ?m := b; wait_if_type_mvar% ?m; body
returns mkSaveInfoAnnotation ?n
to make sure the info nodes created when elaborating b
are "saved".
This is a bit hackish, but elaborators like let_mvar%
are rare.
Equations
Instances For
Return some mvarId
if e
corresponds to a hole that is going to be filled "later" by executing a tactic or resuming elaboration.
We do not save ofTermInfo
for this kind of node in the InfoTree
.
Equations
Instances For
Pushes a new leaf node to the info tree associating the expression e
to the syntax stx
.
As a result, when the user hovers over stx
they will see the type of e
, and if e
is a constant they will see the constant's doc string.
expectedType?
: the expected type ofe
at the point of elaboration, if availablelctx?
: the local context in which to interprete
(otherwise it will use← getLCtx
)elaborator
: a declaration name used as an alternative target for go-to-definitionisBinder
: if true, this will be treated as defininge
(which should be a local constant) for the purpose of go-to-definition on local variablesforce
: In patterns, the effect ofaddTermInfo
is usually suppressed and replaced by apatternWithRef?
annotation which will be turned into a term info on the post-match-elaboration expression. This flag overrides that behavior and adds the term info immediately. (See https://github.com/leanprover/lean4/pull/1664.)
Equations
Instances For
Info node capturing def/let rec
bodies, used by the unused variables linter.
The body as a fully elaborated term.
none
if the body failed to elaborate.
Instances For
Block usage of implicit lambdas if stx
is @f
or @f arg1 ...
or fun
with an implicit binder annotation.
Equations
Instances For
- no : UseImplicitLambdaResult
- yes (expectedType : Expr) : UseImplicitLambdaResult
- postpone : UseImplicitLambdaResult
Instances For
Main function for elaborating terms.
It extracts the elaboration methods from the environment using the node kind.
Recall that the environment has a mapping from SyntaxNodeKind
to TermElab
methods.
It creates a fresh macro scope for executing the elaboration method.
All unlogged trace messages produced by the elaboration method are logged using
the position information at stx
. If the elaboration method throws an Exception.error
and errToSorry == true
,
the error is logged and a synthetic sorry expression is returned.
If the elaboration throws Exception.postpone
and catchExPostpone == true
,
a new synthetic metavariable of kind SyntheticMVarKind.postponed
is created, registered,
and returned.
The option catchExPostpone == false
is used to implement resumeElabTerm
to prevent the creation of another synthetic metavariable when resuming the elaboration.
If implicitLambda == false
, then disable implicit lambdas feature for the given syntax, but not for its subterms.
We use this flag to implement, for example, the @
modifier. If Context.implicitLambda == false
, then this parameter has no effect.
Equations
Instances For
Similar to Lean.Elab.Term.elabTerm
, but ensures that the type of the elaborated term is expectedType?
by inserting coercions if necessary.
If errToSorry
is true, then if coercion insertion fails, this function returns sorry
and logs the error.
Otherwise, it throws the error.
Equations
Instances For
Create a new metavariable with the given type, and try to synthesize it.
If type class resolution cannot be executed (e.g., it is stuck because of metavariables in type
),
register metavariable as a pending one.
Equations
Instances For
Make sure e
is a type by inferring its type and making sure it is an Expr.sort
or is unifiable with Expr.sort
, or can be coerced into one.
Equations
Instances For
Enable auto-bound implicits, and execute k
while catching auto bound implicit exceptions. When an exception is caught,
a new local declaration is created, registered, and k
is tried to be executed again.
Equations
Instances For
Equations
Instances For
Adds an InlayHintInfo
for the fvar auto implicits in autos
at inlayHintPos
.
The inserted inlay hint has a hover that denotes the type of the auto-implicit (with meta-variables)
and can be inserted at inlayHintPos
.
Equations
Instances For
Return autoBoundImplicits ++ xs
This method throws an error if a variable in autoBoundImplicits
depends on some x
in xs
.
The autoBoundImplicits
may contain free variables created by the auto-implicit feature, and unassigned free variables.
It avoids the hack used at autoBoundImplicitsOld
.
If inlayHintPos?
is set, this function also inserts an inlay hint denoting autoBoundImplicits
.
See addAutoBoundImplicitsInlayHint
for more information.
Remark: we cannot simply replace every occurrence of addAutoBoundImplicitsOld
with this one because a particular
use-case may not be able to handle the metavariables in the array being given to k
.
Equations
Instances For
Similar to addAutoBoundImplicits
, but converts all metavariables into free variables.
It uses mkForallFVars
+ forallBoundedTelescope
to convert metavariables into free variables.
The type type
is modified during the process if type depends on xs
.
We use this method to simplify the conversion of code using autoBoundImplicitsOld
to autoBoundImplicits
.
Equations
Instances For
Return true if mvarId is an auxiliary metavariable created for compiling let rec
or it
is delayed assigned to one.
Equations
Instances For
Create an Expr.const
using the given name and explicit levels.
Remark: fresh universe metavariables are created if the constant has more universe
parameters than explicitLevels
.
If checkDeprecated := true
, then Linter.checkDeprecated
is invoked.
Equations
Instances For
Equations
Instances For
Similar to resolveName
, but creates identifiers for the main part and each projection with position information derived from ident
.
Example: Assume resolveName v.head.bla.boo
produces (v.head, ["bla", "boo"])
, then this method produces
(v.head, id, [f₁, f₂])
where id
is an identifier for v.head
, and f₁
and f₂
are identifiers for fields "bla"
and "boo"
.
Equations
Instances For
Equations
Instances For
Execute x
and then tries to solve pending universe constraints.
Note that, stuck constraints will not be discarded.
Equations
Instances For
Helper function for "embedding" an Expr
in Syntax
.
It creates a named hole ?m
and immediately assigns e
to it.
Examples:
let e := mkConst ``Nat.zero
`(Nat.succ $(← exprToSyntax e))
Equations
Instances For
Equations
Instances For
Checks whether a declaration is annotated with [builtin_incremental]
or [incremental]
.