Types for configuration elaboration

class Lean.Elab.ConfigEval.EvalTerm (α : Type) : Type

Class for evaluation of Term syntax directly to a runtime value.

• evalTerm : Term → TermElabM (α × Expr)

  Direct evaluation of Term syntax, avoiding term elaboration. Instances should use throwUnsupportedSyntax to signal that the syntax is not recognized. Instances shouldn't generally throw other exceptions.

  Evaluation is allowed to imagine that certain coercions are implicitly inserted. For example, the Option Int instance is allowed to recognize 1 as an Option Int even though term elaboration would fail here. This allowance should be used lightly, since generally EvalTerm is used as the fast path, and when using the EvalExpr backup, such expressions will no longer be recognized.

  Implementations should add TermInfo when the info is enabled. The Expr return value is to support constructing such expressions in combinators.

• typeExpr : Expr

  A type that can be used when constructing expression for the TermInfo.

opaque Lean.Elab.ConfigEval.unsupportedExprExceptionId : InternalExceptionId

def Lean.Elab.ConfigEval.throwUnsupportedExpr {m : Type u_1 → Type u_2} {α : Type u_1} [MonadExceptOf Exception m] : m α

Equations

• Lean.Elab.ConfigEval.throwUnsupportedExpr = throw (Lean.Exception.internal Lean.Elab.ConfigEval.unsupportedExprExceptionId)

class Lean.Elab.ConfigEval.EvalExpr (α : Type) : Type

Class for evaluation of an expression to a runtime value.

• evalExpr : Expr → MetaM α

  Evaluation of an elaborated expression. If the expression is not recognizable, then the instance may throw an exception. They can throw ConfigEval.throwUnsupportedExpr to signal that a generic error should be reported.

  The provided expression does not contain expression metavariables or sorry, but level metavariables may be present. We assume these do not affect evaluation. If expectedType? is provided, then the expression is coerced as necessary to have this type.

• expectedType? : Option Expr

  The expected type to use when elaborating a term for use with this EvalExpr instance. If present, the expression will be coerced to this type.

structure Lean.Elab.ConfigEval.ConfigItem : Type

A view of a Lean.Parser.Term.configItem.

• ref : Syntax

  Ref for the entire configuration item

• option : Ident

  Ref for the option name itself.

• value : Syntax

  The configuration value. Usually this is a Term, but user-defined configuration items can use arbitrary syntax. For +/- booleans, this syntax is synthetic.

• bool? : Option Bool

  Whether this was using +/-, to be able to give a better error message on type mismatch. It also caches the value so we can skip evaluation for Bool, which is a very common case.

• origOptionName : Name

  The original option name (without macro scopes), even after shifting.

• optionComps : List Syntax

  The option identifier split into components, without macro scopes. This allows us to pull off components one at a time if we have hierarchical configuration options.

• prevOptionComps : List Syntax

  Previous root components of option in reverse order, collecting results from ConfigItem.shift.

structure Lean.Elab.ConfigEval.EvalConfigItem (α : Type) : Type

An evaluator for updating a configuration object using configuration items.

This is not a class. In practice, it might be composed out of evaluators or otherwise parameterized in a number of ways.

• set (config : α) (item : ConfigItem) : TermElabM α

  Evaluates setting the configuration item described by item in config.