Documentation

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.

Apply the result/exception and state captured with observing. We use this method to implement overloaded notation and symbols.

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.

Execute x but discard changes performed at Term.State and Meta.State. Recall that the environment is 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 info trees are not discarded, however, and wrapped in InfoTree.Context to store their metavariable context.

Execute x without storing Syntax for recursive applications. See saveRecAppSyntax field at Context.

For testing TermElabM methods. The #eval command will sign the error.

Append mvarErrorInfo argument name (if available) to the message. Remark: if the argument name contains macro scopes we do not append it.

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.

Ensure metavariables registered using registerMVarErrorInfos (and used in the given declaration) have been assigned.

Creates syntax for ( : )

Convert unassigned universe level metavariables into parameters. The new parameter names are of the form u_i where i >= nextParamIdx. The method returns the updated expression and new nextParamIdx.

Remark: we make sure the generated parameter names do not clash with the universe at ctx.levelNames.

Variant of levelMVarToParam where nextParamIdx is stored in a state monad.

Auxiliary method for creating fresh binder names. Do not confuse with the method for creating fresh free/meta variable ids.

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.

Apply given attributes at a given application time

Return true if e contains a pending metavariable. Remark: it also visits let-declarations.

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.

If expectedType? is some t, then ensure t and type of e are definitionally equal. If they are not, then try coercions.

If mayPostpone == true, throw Expection.postpone.

If mayPostpone == true and e's head is a metavariable, throw Exception.postpone.

Create an auxiliary annotation to make sure we create a Info even if e is a metavariable. See mkTermInfo.

We use this functions 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 return 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.

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.

Block usage of implicit lambdas if stx is @f or @f arg1 ... or fun with an implicit binder annotation.

Store in the InfoTree that e is a "dot"-completion target.

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 == true, 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.

Execute x and then restore syntheticMVars, levelNames, mvarErrorInfos, and letRecsToLift. We use this combinator when we don't want the pending problems created by x to persist after its execution.

Execute x and return some if no new errors were recorded or exceptions was thrown. Otherwise, return none

Adapt a syntax transformation to a regular, term-producing elaborator.

Make sure e is a type by inferring its type and making sure it is a Expr.sort or is unifiable with Expr.sort, or can be coerced into one.

Elaborate stx and ensure result is a type.

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.

Collect unassigned metavariables in type that are not already in init and not satisfying except.

Return autoBoundImplicits ++ xs This methoid 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.

Similar to autoBoundImplicits, but immediately if the resulting array of expressions contains metavariables, it immediately use 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

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.

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

Execute x and then tries to solve pending universe constraints. Note that, stuck constraints will not be discarded.

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