- options : Lean.Options
- openDecls : List Lean.OpenDecl
- macroStack : Lean.Elab.MacroStack
- errToSorry : Bool
Saved context for postponed terms and tactics to be executed.
Instances For
- typeClass: Lean.Elab.Term.SyntheticMVarKind
Use typeclass resolution to synthesize value for metavariable.
- coe: Option String → Lean.Expr → Lean.Expr → Option Lean.Expr → Lean.Elab.Term.SyntheticMVarKind
Use coercion to synthesize value for the metavariable. if
f?
issome f
, we produce an application type mismatch error message. Otherwise, ifheader?
issome header
, we generate the error(header ++ "has type" ++ eType ++ "but it is expected to have type" ++ expectedType)
Otherwise, we generate the error("type mismatch" ++ e ++ "has type" ++ eType ++ "but it is expected to have type" ++ expectedType)
- tactic: Lean.Syntax → Lean.Elab.Term.SavedContext → Lean.Elab.Term.SyntheticMVarKind
Use tactic to synthesize value for metavariable.
- postponed: Lean.Elab.Term.SavedContext → Lean.Elab.Term.SyntheticMVarKind
Metavariable represents a hole whose elaboration has been postponed.
We use synthetic metavariables as placeholders for pending elaboration steps.
Instances For
- stx : Lean.Syntax
Instances For
- implicitArg: Lean.Expr → Lean.Elab.Term.MVarErrorKind
Metavariable for implicit arguments.
ctx
is the parent application. - hole: Lean.Elab.Term.MVarErrorKind
Metavariable for explicit holes provided by the user (e.g.,
_
and?m
) - custom: Lean.MessageData → Lean.Elab.Term.MVarErrorKind
"Custom",
msgData
stores the additional error messages.
We can optionally associate an error context with a metavariable (see MVarErrorInfo
).
We have three different kinds of error context.
Instances For
- mvarId : Lean.MVarId
- ref : Lean.Syntax
- kind : Lean.Elab.Term.MVarErrorKind
We can optionally associate an error context with metavariables.
Instances For
- ref : Lean.Syntax
- fvarId : Lean.FVarId
- attrs : Array Lean.Elab.Attribute
- shortDeclName : Lake.Name
- declName : Lake.Name
- lctx : Lean.LocalContext
- localInstances : Lean.LocalInstances
- type : Lean.Expr
- val : Lean.Expr
- mvarId : Lean.MVarId
Nested let rec
expressions are eagerly lifted by the elaborator.
We store the information necessary for performing the lifting here.
Instances For
- syntheticMVars : Lean.MVarIdMap Lean.Elab.Term.SyntheticMVarDecl
- pendingMVars : List Lean.MVarId
- mvarErrorInfos : Lean.MVarIdMap Lean.Elab.Term.MVarErrorInfo
- letRecsToLift : List Lean.Elab.Term.LetRecToLift
State of the TermElabM
monad.
Instances For
- core : Lean.Core.State
- meta : Lean.Meta.State
- term : Lean.Elab.Term.State
- tactic : Lean.Elab.Tactic.State
- stx : Lean.Syntax
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.
Instances For
- mvarId : Lean.MVarId
- pos : String.Pos
Key for the cache used to implement the save
tactic.
Instances For
Cache for the save
tactic.
Instances For
- auxDeclToFullName : Lean.FVarIdMap Lake.Name
Map
.auxDecl
local declarations used to encode recursive declarations to their full-names. - macroStack : Lean.Elab.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. - autoBoundImplicits : Lean.PArray Lean.Expr
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
- sectionVars : Lake.NameMap Lake.Name
Map from user name to internal unique name
- sectionFVars : Lake.NameMap Lean.Expr
Map from internal name to fvar
- implicitLambda : Bool
Enable/disable implicit lambdas feature.
- 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. - tacticCache? : Option (IO.Ref Lean.Elab.Tactic.Cache)
Cache for the
save
tactic. It is onlysome
in the LSP server. - 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 assynthethicOpaque
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 => _)
Instances For
- meta : Lean.Meta.SavedState
- elab : Lean.Elab.Term.State
Backtrackable state for the TermElabM
monad.
Instances For
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.
Instances For
Apply the result/exception and state captured with observing
.
We use this method to implement overloaded notation and symbols.
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.
Instances For
Return the universe level names explicitly provided by the user.
Instances For
Given a free variable fvar
, return its declaration.
This function panics if fvar
is not a free variable.
Instances For
Execute x
but discard changes performed at Term.State
and Meta.State
.
Recall that the Environment
and InfoState
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.
Instances For
Execute x
without storing Syntax
for recursive applications. See saveRecAppSyntax
field at Context
.
Instances For
Instances For
- fieldIdx: Lean.Syntax → Nat → Lean.Elab.Term.LVal
- fieldName: Lean.Syntax → String → Option Lake.Name → Lean.Syntax → Lean.Elab.Term.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.targetStx
is the target object being accessed.
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]
.
Instances For
Return the name of the declaration being elaborated if available.
Instances For
Return the list of nested let rec
declarations that need to be lifted.
Instances For
Return the declaration of the given metavariable
Instances For
Execute x
with declName? := name
. See getDeclName?
.
Instances For
Update the universe level parameter names.
Instances For
Execute x
using levelNames
as the universe level parameter names. See getLevelNames
.
Instances For
Declare an auxiliary local declaration shortDeclName : type
for elaborating recursive declaration declName
,
update the mapping auxDeclToFullName
, and then execute k
.
Instances For
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.
Instances For
For testing TermElabM
methods. The #eval command will sign the error.
Instances For
Instances For
Instances For
Instances For
Elaborate x
with stx
on the macro stack
Instances For
Elaborate x
with stx
on the macro stack and produce macro expansion info
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.
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
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.
Instances For
Instances For
Append mvarErrorInfo
argument name (if available) to the message.
Remark: if the argument name contains macro scopes we do not append it.
Instances For
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.
Instances For
Ensure metavariables registered using registerMVarErrorInfos
(and used in the given declaration) have been assigned.
Instances For
Execute x
without allowing it to postpone elaboration tasks.
That is, tryPostpone
is a noop.
Instances For
Creates syntax for (
:
)
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.
Instances For
Auxiliary method for creating fresh binder names. Do not confuse with the method for creating fresh free/meta variable ids.
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
.
Instances For
Apply given attributes at a given application time
Instances For
Instances For
Instances For
Instances For
See containsPostponedTerm
Return true
if e
contains a pending metavariable. Remark: it also visits let-declarations.
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.
Instances For
If expectedType?
is some t
, then ensure t
and eType
are definitionally equal.
If they are not, then try coercions.
Argument f?
is used only for generating error messages.
Instances For
Log the given exception, and create a synthetic sorry for representing the failed
elaboration step with exception ex
.
Instances For
If mayPostpone == true
, throw Expection.postpone
.
Instances For
Return true
if e
reduces (by unfolding only [reducible]
declarations) to ?m ...
Instances For
If mayPostpone == true
and e
's head is a metavariable, throw Exception.postpone
.
Instances For
If e? = some e
, then tryPostponeIfMVar e
, otherwise it is just tryPostpone
.
Instances For
Throws Exception.postpone
, if expectedType?
contains unassigned metavariables.
It is a noop if mayPostpone == false
.
Instances For
Throws Exception.postpone
, if expectedType?
contains unassigned metavariables.
If mayPostpone == false
, it throws error msg
.
Instances For
Save relevant context for term elaboration postponement.
Instances For
Execute x
with the context saved using saveContext
.
Instances For
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.
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
.
Instances For
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.)
Instances For
Instances For
Instances For
Postpone the elaboration of stx
, return a metavariable that acts as a placeholder, and
ensures the info tree is updated and a hole id is introduced.
When stx
is elaborated, new info nodes are created and attached to the new hole id in the info tree.
Instances For
Block usage of implicit lambdas if stx
is @f
or @f arg1 ...
or fun
with an implicit binder annotation.
Instances For
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Return true iff stx
is a Syntax.ident
, and it is a local variable.
Instances For
- no: Lean.Elab.Term.UseImplicitLambdaResult
- yes: Lean.Expr → Lean.Elab.Term.UseImplicitLambdaResult
- postpone: Lean.Elab.Term.UseImplicitLambdaResult
Instances For
Store in the InfoTree
that e
is a "dot"-completion target.
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.
Instances For
Execute x
and return some
if no new errors were recorded or exceptions were thrown. Otherwise, return none
.
Instances For
Adapt a syntax transformation to a regular, term-producing elaborator.
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.
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.
Instances For
Elaborate stx
and ensure result is a type.
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.
Instances For
Instances For
Instances For
Collect unassigned metavariables in type
that are not already in init
and not satisfying except
.
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
.
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
.
Instances For
Similar to autoBoundImplicits
, but immediately if the resulting array of expressions contains metavariables,
it immediately uses mkForallFVars
+ forallBoundedTelescope
to convert them 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
.
Instances For
Return true if mvarId is an auxiliary metavariable created for compiling let rec
or it
is delayed assigned to one.
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
.
Instances For
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"
.
Instances For
Instances For
Instances For
Instances For
Instances For
Execute x
and then tries to solve pending universe constraints.
Note that, stuck constraints will not be discarded.
Instances For
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))