From 047f6aaf89b7a92356f9718615555b8055826ec4 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Thu, 14 May 2026 10:20:57 -0700 Subject: [PATCH] feat: efficient tactic configuration elaborators and configurability (#13651) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR replaces the previous tactic configuration system with a significantly more efficient one that supports custom configuration syntaxes and processing. On a simple benchmark, configuration evaluation takes 6.2% of the time it used to. The `declare_config_elab` command generates a configuration elaborator that now directly constructs configuration objects; previously it relied on `Meta.evalExpr'`, which involved running a configuration through the full term elaboration, compilation, and evaluation processes. The generated configuration elaborators now also have the capability to do direct `Syntax` evaluation in common cases, skipping term elaboration. Furthermore, the elaborator accepts configurations more liberally: any user-defined syntax that has the form of an `optConfig`-style configuration or configuration item (including, e.g., `namedArgument`s) is accepted. Import `Lean.Elab.ConfigEval` to use the system; see this module for some documentation in addition to the docstrings in `Lean.Elab.ConfigEval.Commands`. Furthermore, the `simp` tactic now also has `(user.optionName := ...)` user configuration options, which can be declared using a global `tactic.simp.user.optionName` option; use `getUserConfigOption` and `withUserConfig` to access and set these in metaprograms. Other features: - `declare_config_elab` creates a function that exposes an `init` parameter for the configuration that will be modified. It also now has a `where` clause, enabling defining custom handlers for specific keys. - Elaborators can be given additional binders, to make parameterized elaborators. This is used by `simp` and `grind ` to support multiple default configurations with the correct expected type for `(config := ...)` elaboration. - The `EvalTerm` class supports direct evaluation of `Syntax`, skipping term elaboration. The system will attempt to automatically derive this class when generating the elaborator. - In case `EvalTerm` does not recognize the term, then the syntax is elaborated to an expression and an `EvalExpr` instance is applied to evaluate the expression. The system will similarly automatically derive these instances if possible. - Automatic derivation is *transitive*. It is able to seek instances through other instances; e.g. if it needs an `EvalTerm (List T)` instance it will be able to reduce this to seeking an `EvalTerm T` instance. - The system is designed to be flexible, and the various components can be combined to construct a configuration elaborator. There are also now `declare_core_config_elab` and `declare_term_config_elab` for conveniently generating elaborators for `CoreM` and `TermElabM`. The difference is that the first takes an explicit flag for whether to log exceptions, and the second uses the current `errToSorry` state. **Warning:** if you use the `TermElabM` one from `TacticM`, it will be unaware of the current `recover` state. The only differences between these macros are the ways error recovery is handled per monad. Other changes: - `#reduce` tactic configuration now makes use of this system and has more options - The module `Lean.Elab.Tactic.ConfigSetter` is removed; the `declare_config_elab`-family macros subsume its functionality. - The module `Lean.Elab.Tactic.Config` is deprecated and will be removed; migration notes appear in the module docs there. Import `Lean.Elab.ConfigEval` instead. - One of the mvcgen benchmarks got significantly slower, but it turned out to be caused by the new tactic configuration elaboration no longer resetting the MetaM caches. Adding an explicit `resetCache` into the test driver fixed the benchmark. ### Notes for metaprogram authors If you are using the module system, you just need a `meta import Lean.Elab.ConfigEval` to use the macros, and it should serve as a drop-in replacement to the previous system so long as 1. your configuration type is a `structure` with no parameters, indices, or universes (only `Type` is supported); 2. default values are self-contained and not dependent on other fields; and 3. all fields have types that are composed from `Option`, `List`, `Array`, `String`, `DataValue`, and inductive types in `Type` with no parameters or indices, whose fields are similarly composed. The macros synthesize a self-contained configuration elaboration procedure, analyzing the `EvalTerm` and `EvalExpr` instances that are currently available or can be automatically derived. These are the components of the system: - `EvalTerm` instances provide `Term → TermElabM α` functions for evaluation of raw syntax; these handle the common cases where an option value is a identifier, application, or other simple expression. They are responsible for adding TermInfo when info is enabled, to support hovers. One can invoke derivation of a `EvalTerm T` instance with the `ensure_eval_term_instance T` command (after `open scoped Lean.Elab.ConfigEval`). - `EvalExpr` instances provide `Expr → TermElabM α` functions for evaluation of elaborated expressions; these handle cases where an option value may require reduction to evaluate. Similarly, one can invoke derivation of an `EvalExpr T` instance with the `ensure_eval_expr_instance T` command. If needed, there's also `derive_eval_expr_instance_using_meta_eval T` for creating a `Meta.evalExpr'`-based evaluator. - Functions like `ConfigEval.evalExprWithElab` compose `EvalTerm` and `EvalExpr` instances into a single procedure that first attempts `EvalTerm`, and, if that fails, applies the standard term elaborator and then attempts `EvalExpr`. This way term elaboration can be skipped in all but uncommon cases. - Configuration item interpretation is through `ConfigEval.foldConfigM`, which is a procedure with a lax specification for what counts as a configuration item, calling the provided function on each recognized configuration item. The idea is: - Null nodes are lists of configurations - One-argument nodes are considered to be wrappers like `optConfig` or `configItem` - Two-argument nodes of the form `("+"<|>"-") (atom<|>ident)` are considered to be boolean options - Five-argument nodes of the form `"(" (atom<|>ident) ":=" syntax ")"` are considered to be general configuration items. (It only checks for the presence of `(` and that there are two-to-five arguments.) - Bare atoms are considered to be positive boolean options - Configuration evaluation then uses `EvalConfigItem.set` on each item produced by the fold, for an `EvalConfigItem` structure defined for the given configuration type. The `def_eval_config_item` command can be used to generate this structure. It analyzes which `EvalTerm` and `EvalExpr` instances exist and derives missing ones, then builds an efficient procedure to process configuration items and apply evaluators. - Lastly, there are the `declare_core_config_elab`, `declare_term_config_elab`, `declare_config_elab`, and `declare_command_config_elab` macros for conveniently running the `def_eval_config_item` command and constructing a self-contained elaboration function. The derivation procedures analyze which `EvalTerm`/`EvalExpr` instances already exist and only derive the "leaf" instances that are necessary to construct `EvalTerm` and `EvalExpr` instances. The derived instances are made `private local` — since configuration elaborators are meant to be self-contained, we decided not to let the additional instances be a side effect of the macros. The instances can be globally added by manually using the `ensure_*` commands. The macros support making parameterized elaborators with arbitrary additional binders. See `make_elab_grind_config` and `make_elab_simp_config` in core Lean for examples of generating a single elaborator that's used with multiple default value configurations. To see how to create a key handler that matches all configuration keys with a given prefix, see `make_elab_simp_config`. There is a todo item at `Lean.Elab.ConfigEval.ReflectConfigItems` for reflecting configurations back to syntax, which is not yet supported. ### Performance evaluation A legacy configuration parser was temporarily added to `Lean.Elab.Tactic.Grind.Config` using `declare_term_config_elab_legacy elabGrindConfigLegacy Grind.Config`, and then this file was used for measuring elaboration time: ```lean import Lean open Lean Elab Meta Tactic Parser def cfgs : Array Syntax := Unhygienic.run do return #[ ← `(Tactic.optConfig| ), ← `(Tactic.optConfig| +clean), ← `(Tactic.optConfig| +trace +markInstances -lookahead -useSorry), ← `(Tactic.optConfig| (trace := true) (markInstances := true) (lookahead := false) (useSorry := false)), ← `(Tactic.optConfig| -trace (splits := 20) +revert (maxSuggestions := some 3) (ematch := 2)), ← `(Tactic.optConfig| (gen := 5) -reducible +splitImp -funCC), ← `(Tactic.optConfig| (config := { trace := true, lookahead := false, maxSuggestions := some 3 })), ] def testGrindElab (cfgs : Array Syntax) (n : Nat) : TacticM Unit := do profileitM Exception "test grind elab" (← getOptions) do let mut ematch := 0 for _ in [0:n] do for cfg in cfgs do let c ← Tactic.elabGrindConfig cfg ematch := ematch + c.ematch logInfo m!"sum = {ematch}" def testGrindElabLegacy (cfgs : Array Syntax) (n : Nat) : TacticM Unit := do profileitM Exception "test grind elab legacy" (← getOptions) do let mut ematch := 0 for _ in [0:n] do for cfg in cfgs do let c ← Tactic.elabGrindConfigLegacy cfg ematch := ematch + c.ematch logInfo m!"sum = {ematch}" def runTest (info : Bool) (test : TacticM Unit) : TermElabM Unit := do withEnableInfoTree info do let mvar ← mkFreshExprMVar none discard <| Tactic.run mvar.mvarId! test set_option maxHeartbeats 0 set_option profiler true set_option profiler.threshold 1 def iters : Nat := 1000 #eval runTest false <| testGrindElab cfgs iters #eval runTest true <| testGrindElab cfgs iters #eval runTest false <| testGrindElabLegacy cfgs iters #eval runTest true <| testGrindElabLegacy cfgs iters ``` A representative output is ``` test grind elab took 315ms test grind elab took 333ms test grind elab legacy took 5.22s test grind elab legacy took 5.33s ``` Computing `(315.0 + 333.0) / (5220 + 5330)` and rounding up to the nearest tenth gives the 6.2% figure. --- The #13426 draft PR includes some LSP modifications to support completions for `simp` user configuration options. --- src/Init/Meta/Defs.lean | 12 +- src/Init/MetaTypes.lean | 25 +- src/Init/Notation.lean | 4 +- src/Lean/Elab.lean | 2 + src/Lean/Elab/BuiltinCommand.lean | 25 +- src/Lean/Elab/ConfigEval.lean | 95 +++++ src/Lean/Elab/ConfigEval/Basic.lean | 341 ++++++++++++++++ src/Lean/Elab/ConfigEval/Commands.lean | 306 +++++++++++++++ .../Elab/ConfigEval/DeriveEvalConfigItem.lean | 371 ++++++++++++++++++ src/Lean/Elab/ConfigEval/DeriveEvalExpr.lean | 129 ++++++ src/Lean/Elab/ConfigEval/DeriveEvalTerm.lean | 156 ++++++++ src/Lean/Elab/ConfigEval/Extra.lean | 38 ++ src/Lean/Elab/ConfigEval/Instances.lean | 288 ++++++++++++++ src/Lean/Elab/ConfigEval/MetaInstances.lean | 29 ++ src/Lean/Elab/ConfigEval/Types.lean | 115 ++++++ src/Lean/Elab/ConfigEval/Util.lean | 143 +++++++ .../Elab/Tactic/BVDecide/Frontend/Attr.lean | 1 + src/Lean/Elab/Tactic/Config.lean | 41 +- src/Lean/Elab/Tactic/ConfigSetter.lean | 72 ---- src/Lean/Elab/Tactic/Decide.lean | 1 + src/Lean/Elab/Tactic/Do/VCGen/Basic.lean | 1 + src/Lean/Elab/Tactic/ElabTerm.lean | 3 +- src/Lean/Elab/Tactic/Grind/Config.lean | 63 ++- src/Lean/Elab/Tactic/Grind/Main.lean | 10 +- src/Lean/Elab/Tactic/Lets.lean | 1 + src/Lean/Elab/Tactic/LibrarySearch.lean | 1 + src/Lean/Elab/Tactic/NormCast.lean | 1 + src/Lean/Elab/Tactic/Omega/Frontend.lean | 2 +- src/Lean/Elab/Tactic/Rewrite.lean | 1 + src/Lean/Elab/Tactic/Simp.lean | 118 +++++- src/Lean/Elab/Tactic/SolveByElim.lean | 18 +- src/Lean/Elab/Tactic/Try.lean | 1 + src/Lean/Meta/Tactic/Simp/Types.lean | 20 +- src/Lean/Parser/Term.lean | 26 ++ tests/bench/mvcgen/sym/lib/Driver.lean | 2 + tests/elab/config_eval.lean | 170 ++++++++ tests/elab/extraModUses.lean | 2 +- tests/elab/match_expr_perf.lean | 1 - tests/elab/tactic_config.lean | 206 +++++++++- tests/elab/whereCmd.lean | 2 +- 40 files changed, 2682 insertions(+), 161 deletions(-) create mode 100644 src/Lean/Elab/ConfigEval.lean create mode 100644 src/Lean/Elab/ConfigEval/Basic.lean create mode 100644 src/Lean/Elab/ConfigEval/Commands.lean create mode 100644 src/Lean/Elab/ConfigEval/DeriveEvalConfigItem.lean create mode 100644 src/Lean/Elab/ConfigEval/DeriveEvalExpr.lean create mode 100644 src/Lean/Elab/ConfigEval/DeriveEvalTerm.lean create mode 100644 src/Lean/Elab/ConfigEval/Extra.lean create mode 100644 src/Lean/Elab/ConfigEval/Instances.lean create mode 100644 src/Lean/Elab/ConfigEval/MetaInstances.lean create mode 100644 src/Lean/Elab/ConfigEval/Types.lean create mode 100644 src/Lean/Elab/ConfigEval/Util.lean delete mode 100644 src/Lean/Elab/Tactic/ConfigSetter.lean create mode 100644 tests/elab/config_eval.lean diff --git a/src/Init/Meta/Defs.lean b/src/Init/Meta/Defs.lean index 8a65ffcc70..bec12e59fa 100644 --- a/src/Init/Meta/Defs.lean +++ b/src/Init/Meta/Defs.lean @@ -1788,14 +1788,16 @@ namespace Tactic /-- Extracts the items from a tactic configuration, either a `Lean.Parser.Tactic.optConfig`, `Lean.Parser.Tactic.config`, or these wrapped in null nodes. + +New metaprograms should use `Lean.Elab.ConfigEval.foldConfigM` instead. -/ partial def getConfigItems (c : Syntax) : TSyntaxArray ``configItem := if c.isOfKind nullKind then c.getArgs.flatMap getConfigItems else match c with - | `(optConfig| $items:configItem*) => items - | `(config| (config := $_)) => #[⟨c⟩] -- handled by mkConfigItemViews + | `(Tactic.optConfig| $items:configItem*) => items + | `(Tactic.config| (config := $_)) => #[⟨c⟩] -- handled by mkConfigItemViews | _ => #[] def mkOptConfig (items : TSyntaxArray ``configItem) : TSyntax ``optConfig := @@ -1808,3 +1810,9 @@ or these wrapped in null nodes (for example because the syntax is `(config)?`). -/ def appendConfig (cfg cfg' : Syntax) : TSyntax ``optConfig := mkOptConfig <| getConfigItems cfg ++ getConfigItems cfg' + +end Tactic + +end Parser + +end Lean diff --git a/src/Init/MetaTypes.lean b/src/Init/MetaTypes.lean index 9578906a3e..73e4774a60 100644 --- a/src/Init/MetaTypes.lean +++ b/src/Init/MetaTypes.lean @@ -204,7 +204,7 @@ end DSimp namespace Simp -@[inline] +@[inline, expose] def defaultMaxSteps := 100000 /-- @@ -388,7 +388,7 @@ structure ConfigCtx extends Config where /-- A neutral configuration for `simp`, turning off all reductions and other built-in simplifications. -/ -def neutralConfig : Simp.Config := { +@[expose] def neutralConfig : Simp.Config := { zeta := false beta := false eta := false @@ -464,4 +464,25 @@ structure LiftLetsConfig extends ExtractLetsConfig where lift := true preserveBinderNames := true +namespace Command + +structure ReduceConfig where + /-- Do reductions of types and propositions. Default: `false`. -/ + types : Bool := false + /-- Do reductions of proof terms. Default: `false`. -/ + proofs : Bool := false + /-- In applications, do reductions of implicit arguments. Default: `false`. -/ + implicits : Bool := false + /-- Transparency mode for reduction. Default: `all`. -/ + transparency : TransparencyMode := .all + /-- Use "smart unfolding" when reducing definitions, to ensure the primitive recursors + are not exposed. Default: `false`. -/ + smartUnfolding : Bool := false + /-- Typecheck the elaborated term before reducing. Default: `true`. -/ + check : Bool := true + /-- Ignore stuck typeclass synthesis while elaborating the term. Default: `false`. -/ + ignoreStuckTC : Bool := false + +end Command + end Lean.Meta diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean index 5323fb54ab..e6dfae5155 100644 --- a/src/Init/Notation.lean +++ b/src/Init/Notation.lean @@ -745,6 +745,8 @@ This is the same as `#eval show MetaM Unit from discard do doSeq`. -/ syntax (name := runMeta) "run_meta " doSeq : command +/-- Configuration for the `#reduce` command. -/ +syntax reduceConfig := many(colGt atomic(" (" ident " := ") term ")") /-- `#reduce ` reduces the expression `` to its normal form. This involves applying reduction rules until no further reduction is possible. @@ -759,7 +761,7 @@ especially for complex expressions. Consider using `#eval ` for simple evaluation/execution of expressions. -/ -syntax (name := reduceCmd) "#reduce " (atomic("(" &"proofs" " := " &"true" ")"))? (atomic("(" &"types" " := " &"true" ")"))? term : command +syntax (name := reduceCmd) "#reduce" reduceConfig term : command set_option linter.missingDocs false in syntax guardMsgsFilterAction := &"check" <|> &"drop" <|> &"pass" diff --git a/src/Lean/Elab.lean b/src/Lean/Elab.lean index fc934546b4..4dbee43305 100644 --- a/src/Lean/Elab.lean +++ b/src/Lean/Elab.lean @@ -68,3 +68,5 @@ public import Lean.Elab.DocString.Builtin public import Lean.Elab.Parallel public import Lean.Elab.BuiltinDo public import Lean.Elab.Idbg +public import Lean.Elab.ConfigEval +public import Lean.Elab.Tactic.Config diff --git a/src/Lean/Elab/BuiltinCommand.lean b/src/Lean/Elab/BuiltinCommand.lean index 465ea30c7f..2d51855b40 100644 --- a/src/Lean/Elab/BuiltinCommand.lean +++ b/src/Lean/Elab/BuiltinCommand.lean @@ -9,6 +9,7 @@ prelude public import Lean.Meta.Reduce public import Lean.Elab.Eval public import Lean.Elab.Command +import Lean.Elab.ConfigEval import Lean.Elab.DeprecatedSyntax public import Lean.Elab.Open import Init.Data.Nat.Order @@ -453,23 +454,25 @@ def elabCheckCore (ignoreStuckTC : Bool) : CommandElab @[builtin_command_elab Lean.Parser.Command.check] def elabCheck : CommandElab := elabCheckCore (ignoreStuckTC := true) +declare_command_config_elab elabReduceConfig Command.ReduceConfig + @[builtin_command_elab Lean.reduceCmd] def elabReduce : CommandElab - | `(#reduce%$tk $term) => go tk term - | `(#reduce%$tk (proofs := true) $term) => go tk term (skipProofs := false) - | `(#reduce%$tk (types := true) $term) => go tk term (skipTypes := false) - | `(#reduce%$tk (proofs := true) (types := true) $term) => go tk term (skipProofs := false) (skipTypes := false) + | `(#reduce%$tk $cfg $term) => do + let cfg ← elabReduceConfig cfg + go tk term cfg | _ => throwUnsupportedSyntax where - go (tk : Syntax) (term : Syntax) (skipProofs := true) (skipTypes := true) : CommandElabM Unit := + go (tk : Syntax) (term : Syntax) (cfg : Command.ReduceConfig) : CommandElabM Unit := withoutModifyingEnv <| runTermElabM fun _ => Term.withDeclName `_reduce do let e ← Term.elabTerm term none - Term.synthesizeSyntheticMVarsNoPostponing - -- Users might be testing out buggy elaborators. Let's typecheck before proceeding: - withRef tk <| Meta.check e + Term.synthesizeSyntheticMVarsNoPostponing (ignoreStuckTC := cfg.ignoreStuckTC) + let e ← instantiateMVars e + if cfg.check then + -- Users might be testing out buggy elaborators. Let's typecheck before proceeding: + withRef tk <| Meta.check e let e ← Term.levelMVarToParam (← instantiateMVars e) - -- TODO: add options or notation for setting the following parameters - withTheReader Core.Context (fun ctx => { ctx with options := ctx.options.set `smartUnfolding false }) do - let e ← withTransparency (mode := TransparencyMode.all) <| reduce e (skipProofs := skipProofs) (skipTypes := skipTypes) + withTheReader Core.Context (fun ctx => { ctx with options := ctx.options.set `smartUnfolding cfg.smartUnfolding }) do + let e ← withTransparency (mode := cfg.transparency) <| reduce e (explicitOnly := !cfg.implicits) (skipProofs := !cfg.proofs) (skipTypes := !cfg.types) logInfoAt tk e def hasNoErrorMessages : CommandElabM Bool := do diff --git a/src/Lean/Elab/ConfigEval.lean b/src/Lean/Elab/ConfigEval.lean new file mode 100644 index 0000000000..2ece69cdec --- /dev/null +++ b/src/Lean/Elab/ConfigEval.lean @@ -0,0 +1,95 @@ +/- +Copyright (c) 2026 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Kyle Miller +-/ +module + +prelude +public import Lean.Elab.ConfigEval.Types +public import Lean.Elab.ConfigEval.Basic +public import Lean.Elab.ConfigEval.Commands +public import Lean.Elab.ConfigEval.Instances +public import Lean.Elab.ConfigEval.MetaInstances +public import Lean.Elab.ConfigEval.Extra + +/-! +# Configuration evaluation + +This module provides a system for constructing efficient elaborators for +evaluating configuration syntaxes. + +Users should import this module to ensure they have all elaborators and +instances in scope. + +The main interfaces are the `declare_core_config_elab`, `declare_term_config_elab`, +`declare_config_elab` and `declare_command_config_elab` commands. These are +macros that construct configuration elaborators from lower-level components. +Metaprogram authors may choose to directly interface with the lower-level components instead. + +These commands handle the common cases where +1. your configuration type is a `structure` with no parameters, indices, or universes + (only `Type` is supported); +2. default values are self-contained and not dependent on other fields; and +3. all fields have types that are composed from `Option`, `List`, `Array`, `String`, + and inductive types in `Type` with no parameters or indices, whose + constructor fields are similarly composed. + +The macros synthesize a self-contained configuration elaboration procedure, analyzing +the `EvalTerm` and `EvalExpr` instances that are currently available or automatically +derivable. These are the components of the system: + +- `EvalTerm` instances provide `Term → TermElabM α` functions for evaluation of raw syntax; + these handle the common cases where an option value is a identifier, application, or other + simple expression. They are responsible for adding TermInfo when info is enabled, to support + hovers. One can invoke derivation of a `EvalTerm T` instance with the + `ensure_eval_term_instance T` command (after `open scoped Lean.Elab.ConfigEval`). +- `EvalExpr` instances provide `Expr → TermElabM α` functions for evaluation of elaborated + expressions; these handle cases where an option value may require reduction to evaluate. + Similarly, one can invoke derivation of an `EvalExpr T` instance with the + `ensure_eval_expr_instance T` command. If needed, there's also + `derive_eval_expr_instance_using_meta_eval T` for creating a `Meta.evalExpr'`-based evaluator. +- Functions like `ConfigEval.evalExprWithElab` compose `EvalTerm` and `EvalExpr` instances + into a single procedure that first attempts `EvalTerm`, and, if that fails, applies the + standard term elaborator and then attempts `EvalExpr`. This way term elaboration can be + skipped in all but uncommon cases. +- Configuration item interpretation is through `ConfigEval.foldConfigM`, which is a + procedure with a lax specification for what counts as a configuration item. The idea is: + - Null nodes are lists of configurations + - One-argument nodes wrapping null nodes are considered to be wrappers like `optConfig` or `configItem` + - Two-argument nodes of the form `("+"<|>"-") (atom<|>ident)` are considered to be + boolean options + - Five-argument nodes of the form `"(" (atom<|>ident) ":=" syntax ")"` are considered + to be general configuration items. (It only checks for the presence of `(` and that + there are two-to-five arguments.) + - Bare atoms are considered to be positive boolean options +- Configuration evaluation then uses `EvalConfigItem.set` on each item produced by the + fold, for an `EvalConfigItem` structure defined for the given configuration type. + The `def_eval_config_item` command can be used to derive this structure. It + analyzes which `EvalTerm` and `EvalExpr` instances exist and derives missing ones, + then builds an efficient procedure to process configuration items and apply evaluators. +- Lastly, there are the `declare_core_config_elab`, `declare_term_config_elab`, + `declare_config_elab`, and `declare_command_config_elab` macros for conveniently + running the `def_eval_config_item` command and constructing a self-contained + elaboration function. + +The derivation procedures analyze which `EvalTerm`/`EvalExpr` instances already exist +and only derive the "leaf" instances that are necessary to construct `EvalTerm` and +`EvalExpr` instances. The derived instances are made `private local` — since +configuration elaborators are meant to be self-contained, we decided not to let +the additional instances be a side effect of the macros, except in the current section. +The instances can be added globally by manually using the `ensure_*` commands. + +## Notes for core Lean + +Builtin elaborators should put their configuration types in, for example, +`Init.MetaTypes` or `Init.Meta.Defs` so that hovers can function when +nothing is imported. + +Due to the flexibility of `ConfigEval.foldConfigM`, changing the syntax +definitions for custom configurations doesn't generally lead to bootstrapping +issues. Custom configuration options with a non-`Term` values are fine with the caveat +that their use ought to be avoided in the prelude, to avoid bootstrapping issues when their +syntax changes or the custom configuration elaborator changes. + +-/ diff --git a/src/Lean/Elab/ConfigEval/Basic.lean b/src/Lean/Elab/ConfigEval/Basic.lean new file mode 100644 index 0000000000..da8b588ad7 --- /dev/null +++ b/src/Lean/Elab/ConfigEval/Basic.lean @@ -0,0 +1,341 @@ +/- +Copyright (c) 2026 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Kyle Miller +-/ +module + +prelude +public import Lean.Elab.ConfigEval.Types +public import Lean.Elab.SyntheticMVars +import Lean.Elab.ConfigEval.Util + +/-! +# Basic interface for configuration evaluation +-/ + +public section + +namespace Lean.Elab.ConfigEval + +open Meta Term + +def evalTermWithRef {α : Type} [EvalTerm α] (stx : Term) : TermElabM α := + withRef stx <| Prod.fst <$> evalTerm stx + +/-- +Evaluate `stx` using either `evalExpr`. +-/ +def evalExprWithElab {α : Type} [EvalExpr α] (stx : Term) : TermElabM α := + withRef stx do + let ty? := EvalExpr.expectedType? α + let e ← Term.withSynthesize <| Term.elabTermEnsuringType stx ty? + let e ← instantiateMVars e + if e.hasSorry then + if e.hasSyntheticSorry then + -- An error has already been logged. + throwAbortTerm + throwError "Expression contains `sorry`:{indentExpr e}" + if (← Term.logUnassignedUsingErrorInfos (← getMVars e)) then + throwAbortTerm + catchInternalId unsupportedSyntaxExceptionId + (evalExpr e) + (fun _ => do + let extra := if let some ty := ty? then m!"\nof type `{ty}`" else m!"" + throwError "Could not evaluate the expression{indentExpr e}{extra}") + +/-- +Evaluate `stx` using either `evalStx` or `evalExpr`. +-/ +def evalTermOrExprWithElab {α : Type} [EvalTerm α] [EvalExpr α] (stx : Term) : TermElabM α := + withRef stx do + catchInternalId unsupportedSyntaxExceptionId + (Prod.fst <$> evalTerm stx) + (fun _ => do + evalExprWithElab stx) + +private partial def stripParens : Term → Term + | `(($t)) => stripParens t + | t => t + +@[inline] def EvalTerm.evalTermWithInfo {α : Type} + (expectedType? : Option Expr) (f : Term → TermElabM (α × Expr)) (stx : Term) : + TermElabM (α × Expr) := do + let (v, e) ← withRef stx <| f (stripParens stx) + if (← getInfoState).enabled then + addTermInfo' stx e (expectedType? := expectedType?) + return (v, e) + +/-- Like `evalTermWithInfo`, but uses an existing `ToExpr` instance +for `expectedType?` and for constructing the expression. -/ +@[inline] def EvalTerm.evalTermWithInfo' {α : Type} [ToExpr α] + (f : Term → TermElabM α) : + Term → TermElabM (α × Expr) := + evalTermWithInfo (toTypeExpr α) (fun stx => do + let v ← f stx + return (v, toExpr v)) + +/-- +Evaluates `f e`, and if that does `throwUnsupportedExpr`, evaluates `f (← whnf e)`. +If either throw another exception, aborts immediately with that exception. +If both do `throwUnsupportedExpr`, then this generates an exception. +-/ +def EvalExpr.withWHNF {α : Type} (f : Expr → MetaM α) (e : Expr) (errMsg : MessageData) : MetaM α := do + catchInternalId unsupportedExprExceptionId + (f e) + (fun _ => + catchInternalId unsupportedExprExceptionId + (do f (← whnf e)) + (fun _ => + throwError "Could not evaluate the expression:{indentExpr e}{errMsg}")) + +def ConfigItem.isAnonymous (item : ConfigItem) : Bool := item.optionComps.isEmpty + +def ConfigItem.root (item : ConfigItem) : Syntax := + match item.optionComps with + | c :: _ => c + | _ => .missing + +def ConfigItem.getRootStr (item : ConfigItem) : String := + if let .str _ s := item.root.getId then + s + else + "" + +def ConfigItem.prevRoot? (item : ConfigItem) : Option Syntax := + item.prevOptionComps[0]? + +def ConfigItem.prevRoot (item : ConfigItem) : Syntax := + match item.prevOptionComps with + | c :: _ => c + | _ => .missing + +/-- +Gets the current name of the option after any shifting. +For example, if an option is named `a.b.c.d` and there is a handler +for `a.b.*`, then the handler receives a `ConfigItem` whose current option +name is `c.d`. +-/ +def ConfigItem.getCurrOptionName (item : ConfigItem) : Name := + (item.optionComps.map (·.getId)).foldl (init := .anonymous) Name.appendCore + +/-- +Drops the first component of the `optionName`, returning the new config item. +The first component is stored at the front of `prevOptionComps`. +-/ +def ConfigItem.shift (item : ConfigItem) : ConfigItem := + { item with + optionComps := item.optionComps.tail + prevOptionComps := item.root :: item.prevOptionComps } + +def ConfigItem.checkNotBool (item : ConfigItem) : TermElabM Unit := do + if item.bool?.isSome then + throwErrorAt item.option m!"Option is not boolean-valued, so `({item.origOptionName} := ...)` syntax must be used" + +def ConfigItem.throwInvalidOption {α} (item : ConfigItem) (structName? : Option Name) : TermElabM α := + let name := item.origOptionName + let nameMsg := if name.isAnonymous then m!"" else m!" `{name}`" + let structMsg := if let some structName := structName? then m!" for `{.ofConstName structName}`" else m!"" + throwErrorAt item.option "Invalid configuration option{nameMsg}{structMsg}" + +def ConfigItem.throwCannotSetOption {α} (item : ConfigItem) (structName? : Option Name) : TermElabM α := + let name := item.origOptionName + let nameMsg := if name.isAnonymous then m!"" else m!" `{name}`" + let structMsg := if let some structName := structName? then m!" for `{.ofConstName structName}`" else m!"" + throwErrorAt item.option "Cannot set option{nameMsg}{structMsg} using configuration syntax." + +nonrec def ConfigItem.addConstInfo (item : ConfigItem) (projFn : Name) : TermElabM Unit := do + if (← getInfoState).enabled then + if (← getEnv).contains projFn then -- in case we are in Lean prelude + addConstInfo item.root projFn + +nonrec def ConfigItem.addCompletionInfo (item : ConfigItem) (structName : Name) : TermElabM Unit := do + if (← getInfoState).enabled then + if (← getEnv).contains structName then -- in case we are in Lean prelude + addCompletionInfo (CompletionInfo.fieldId item.root item.root.getId {} structName) + +variable {α : Type} {m : Type → Type} [Monad m] [MonadRef m] in +mutual +/-- +Interprets `cfg` as configuration item or list of configuration items. + +Items are interpreted in a way that allows user-defined configurations. +Nearly anything that looks like configuration items or lists of configuration items +will be interpreted. We're expecting an item that has one of the following formats: +- `"(" ident/atom ":=" syntax ")"` +- `"+" ident/atom` +- `"-" ident/atom` + +The specification: +- A null node is a list of configurations +- A one-argument node is considered to be a wrapper like `optConfig` or `configItem`. +- A node with at two arguments starting with a "+"/"-" atom and whose second + argument is an ident or atom is a `posConfigItem`/`negConfigItem` +- A node with at most five arguments starting with a "(" atom and whose second argument + is an ident or atom is a `valConfigItem`. The fourth argument is the value, + and it is allowed to have arbitary syntax (it does not need to be a `Term`). +- A bare atom is considered to be a `"+"` option. + +We trust that any atoms are valid as idents. The atom will be parsed using `String.toName` +to form the name. (Small optimization: if the name doesn't contain `.`, we use `Name.mkSimple` +to skip parsing. Atoms must not contain numerals or `«»` escapes.) + +On interpretation error, `onErr` is called with the current configuration object and the offending +syntax item. It may process the item itself or otherwise throw an error. We leave it to `onErr` +to decide what to do for items containing `Syntax.missing`. +-/ +@[specialize] partial def foldConfigM + (init : α) (cfg : Syntax) + (k : α → ConfigItem → m α) + (onErr : α → Syntax → m α) : + m α := do + let doFail (_ : Unit) : m α := withRef cfg do onErr init cfg + let atomAsIdent (si : SourceInfo) (val : String) : Ident := + let n := if val.contains '.' then String.toName val else Name.mkSimple val + ⟨.ident si val.toRawSubstring n []⟩ + -- Matches ident/atom. Trusts that atoms are valid as idents and converts to idents, + -- preserving the original source info. + let getIdent? (stx : Syntax) : Option Ident := + match stx with + | .ident .. => some ⟨stx⟩ + | .atom si val => some <| atomAsIdent si val + | _ => none + let isPosNeg? (val : String) : Option Bool := + if val == "+" then some true + else if val == "-" then some false + else none + if cfg.isOfKind nullKind then + foldConfigsM init cfg.getArgs k onErr + else if cfg.getNumArgs == 1 then + foldConfigM init (cfg.getArg 0) k onErr + else if cfg.getNumArgs ≥ 1 then + match cfg.getArg 0 with + | arg@(.atom _ val) => + if let some b := isPosNeg? val then + if cfg.getNumArgs == 2 then + if let some ident := getIdent? (cfg.getArg 1) then + let value := if b then mkCIdentFrom arg ``true else mkCIdentFrom arg ``false + return ← k init { ref := cfg, option := ident, bool? := some b, value } + else if val == "(" then + if cfg.getNumArgs ≤ 5 then + if let some ident := getIdent? (cfg.getArg 1) then + -- Assuming `cfg.getArg 2` is `:=` + return ← k init { ref := cfg, option := ident, value := cfg.getArg 3 } + doFail () + | _ => doFail () + else if let .atom si val := cfg then + k init { ref := cfg, option := atomAsIdent si val, bool? := true, value := mkCIdentFrom cfg ``true } + else + doFail () + +/-- +Like `foldConfigM` but takes an array of configurations or configuration items. +-/ +@[specialize] partial def foldConfigsM (init : α) (cfgs : Array Syntax) + (k : α → ConfigItem → m α) + (onErr : α → Syntax → m α) : + m α := do + cfgs.foldlM (init := init) fun x cfg' => foldConfigM x cfg' k onErr + +end + +def EvalConfigItem.trySet {α} (eval : EvalConfigItem α) + (config : α) (item : ConfigItem) (logExceptions : Bool) : + TermElabM α := do + try + eval.set config item + catch ex => + if logExceptions then + if let .internal id := ex then + if id == abortTermExceptionId then + -- An error has already been logged + return config + logException ex + return config + else + throw ex + +/-- +Default `onErr` handler. If the `cfgItem` contains `.missing`, we assume an error has already been +reported by the parser and return `cfg`. Otherwise, we throw an unsupported syntax exception. + +If `cfgType?` is present, then it adds completion info when the identifier is missing. +-/ +def EvalConfigItem.defaultOnErr {α : Type} (cfg : α) (cfgItem : Syntax) (cfgType? : Option Expr := none) : TermElabM α := do + if let some cfgType := cfgType? then + if (← getInfoState).enabled then + -- Assumption: the configuration item might be malformed, but if the + -- first token is an atom and the second is missing, it is almost surely + -- `"(" ...`, `"+" ...`, or `"-" ...` and completion would be helpful. + if (cfgItem.getArg 0).isAtom && (cfgItem.getArg 1).isMissing then + -- This expression is used only for its inferred type in the completion system. + let expr : Expr := mkApp2 (.const ``id [1]) cfgType (.const `_cfg_dummy []) + let info := { elaborator := `ConfigEval, stx := cfgItem.getArg 0, lctx := {}, expectedType? := none, expr } + addCompletionInfo <| .dot info none + if cfgItem.hasMissing then + return cfg + else + throwUnsupportedSyntax + +/-- +Applies the configuration `cfg` to `init` using `eval.set`. +If `logExceptions` is true, then catches and logs exceptions. + +The `onErr` callback is used for invalid configuration syntax. + +Note: this should be run from within `runConfigElab`. +-/ +def EvalConfigItem.setConfig {α} (eval : EvalConfigItem α) + (init : α) (cfg : Syntax) + (onErr : α → Syntax → TermElabM α := defaultOnErr) + (logExceptions : Bool := false) : TermElabM α := + foldConfigM init cfg (eval.trySet (logExceptions := logExceptions)) onErr + +/-- +Applies the configuration `cfg` to `init` using `eval.set`. +If `logExceptions` is true, then catches and logs exceptions. + +The `onErr` callback is used for invalid configuration syntax. + +Note: this should be run from within `runConfigElab`. +-/ +def EvalConfigItem.setConfigs {α} (eval : EvalConfigItem α) + (init : α) (cfgs : Array Syntax) + (onErr : α → Syntax → TermElabM α := defaultOnErr) + (logExceptions : Bool := false) : TermElabM α := + foldConfigsM init cfgs (eval.trySet (logExceptions := logExceptions)) onErr + +/-- +Runs `mx` using a fresh meta and term state. +This should be used around any configuration elaboration. +-/ +def runConfigElab {α} (mx : TermElabM α) : CoreM α := + MetaM.run' <| TermElabM.run' <| withSaveInfoContext mx + +/-- +Calls `EvalConfigItem.setConfig'` from within `runConfigElab`. +-/ +def EvalConfigItem.setConfig' {α : Type} (eval : EvalConfigItem α) + (init : α) (cfg : Syntax) + (onErr : α → Syntax → TermElabM α := defaultOnErr) + (logExceptions : Bool := false) : CoreM α := do + if cfg.matchesNull 0 || (cfg.getNumArgs == 1 && (cfg.getArg 0).matchesNull 0) then + -- These represent an empty null node or an `optConfig`-like syntax with no arguments. + -- Return without doing `runConfigElab`. + return init + else + runConfigElab (eval.setConfig init cfg onErr logExceptions) + +/-- +Calls `EvalConfigItem.setConfigs'` from within `runConfigElab`. +-/ +def EvalConfigItem.setConfigs' {α : Type} (eval : EvalConfigItem α) + (init : α) (cfgs : Array Syntax) + (onErr : α → Syntax → TermElabM α := defaultOnErr) + (logExceptions : Bool := false) : CoreM α := do + if cfgs.isEmpty then + return init + else + runConfigElab (eval.setConfigs init cfgs onErr logExceptions) + +end Lean.Elab.ConfigEval diff --git a/src/Lean/Elab/ConfigEval/Commands.lean b/src/Lean/Elab/ConfigEval/Commands.lean new file mode 100644 index 0000000000..fdc7e708f1 --- /dev/null +++ b/src/Lean/Elab/ConfigEval/Commands.lean @@ -0,0 +1,306 @@ +/- +Copyright (c) 2026 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Kyle Miller +-/ +module + +prelude +public import Lean.Elab.ConfigEval.DeriveEvalTerm +public meta import Lean.Elab.ConfigEval.DeriveEvalTerm +public import Lean.Elab.ConfigEval.DeriveEvalExpr +public meta import Lean.Elab.ConfigEval.DeriveEvalExpr +public import Lean.Elab.ConfigEval.DeriveEvalConfigItem +public meta import Lean.Elab.ConfigEval.DeriveEvalConfigItem +public import Lean.Elab.Tactic.ElabTerm +import Lean.Linter.MissingDocs + +public section + +namespace Lean.Elab.ConfigEval + +open Meta Term Command + +/-- +`ensure_eval_term_instance t` ensures there is a `ConfigItem.EvalTerm t` instance by +deriving one or more instances if it needs to. +-/ +scoped elab vis?:(visibility)? kind:attrKind tk:"ensure_eval_term_instance " t:term : command => do + let type ← liftTermElabM do withoutErrToSorry <| elabTermAndSynthesize t none + ensureEvalTerm vis? kind tk t type + +/-- +`ensure_eval_expr_instance t` ensures there is a `ConfigItem.EvalExpr t` instance by +deriving one or more instances if it needs to. +-/ +scoped elab vis?:(visibility)? kind:attrKind tk:"ensure_eval_expr_instance " t:term : command => do + let type ← liftTermElabM do withoutErrToSorry <| elabTermAndSynthesize t none + ensureEvalExpr vis? kind tk t type + +/-- +`ensure_eval_term_expr_instances t` is a macro for running both `ensure_eval_term_instance t` +and `ensure_eval_expr_instance t`, which ensurs there are `ConfigItem.EvalTerm t` and +`ConfigItem.EvalExpr t` instances by deriving one or more instances if it needs to. +-/ +scoped macro vis?:(visibility)? kind:attrKind tk:"ensure_eval_term_expr_instances " t:term : command => + `($[$vis?]? $kind ensure_eval_term_instance%$tk $t + $[$vis?]? $kind ensure_eval_expr_instance%$tk $t) + +/-- +`derive_eval_expr_instance_using_meta_eval type` defines a `ConfigItem.EvalExpr type` instance +using `Meta.evalExpr'` to evaluate expressions. This sort of item evaluator is a reasonable +backup strategy for infrequently used configuration options, if term- or expression-based +evaluation does not work and the cost of compilation is acceptible. + +This should be avoided in core Lean due to the difficulties it creates for bootstrapping. +-/ +scoped elab vis?:(visibility)? kind:attrKind tk:"derive_eval_expr_instance_using_meta_eval " t:term : command => do + let type ← liftTermElabM do withoutErrToSorry <| elabTermAndSynthesize t none + deriveEvalExprUsingMetaEval vis? kind tk t type + +section +open Parser +/-- `omit f1, f2, f3` disables generating setters for fields `f1`, `f2`, and `f3` +of the structure. -/ +meta def configEntryOmit := leading_parser + nonReservedSymbol "omit " >> sepBy1 ident ", " (allowTrailingSep := true) +meta def configEntryHandlerKeyPrefix := leading_parser + ident >> optional (checkNoWsBefore >> "." >> checkNoWsBefore >> "*") +meta def configEntryHandlerKeyWildcard := leading_parser + "*" +/-- +- `key` matches a specific key +- `key.*` matches any keys for which `key` is a proper prefix +- `*` matches all keys +-/ +meta def configEntryHandlerKey := leading_parser + configEntryHandlerKeyPrefix <|> configEntryHandlerKeyWildcard +/-- +`option key := fun cfg item => ...` adds a configuration option named `key` with the given +expression as its handler. The handler is only called when the key is an exact match. +The provided value is in `item.value`. Such a handler implies `omit key`. + +`option key.* := fun cfg item => ...` adds configuration options with `key` as a proper prefix. +The most-specific `*` handler is called if no handlers for exact matches apply. +-/ +meta def configEntryHandler := leading_parser + nonReservedSymbol "option " >> configEntryHandlerKey >> " := " >> termParser +meta def configEntry := leading_parser + ppGroup (configEntryOmit <|> configEntryHandler) +meta def configEntries := leading_parser + "where" >> (sepByIndent configEntry "; " (allowTrailingSep := true)) +end + +meta def mkEvalConfigItemView (entries? : Option (TSyntax ``configEntries)) : + CommandElabM EvalConfigItemView := do + let mut omitFields : Array (Ident × Name) := #[] + let mut handlers : Array EvalConfigItemHandler := #[] + if let some entries := entries? then + match entries with + | `(configEntries| where $[$entries:configEntry];*) => + for entry in entries do + match entry with + | `(configEntry| omit $[$fields],*) => + omitFields := omitFields ++ fields.map fun f => (f, f.getId.eraseMacroScopes) + | `(configEntry| option $key:configEntryHandlerKey := $body) => + let (optName, kind) ← + match key with + | `(configEntryHandlerKey| $opt:ident) => pure (opt.getId.eraseMacroScopes, .exact) + | `(configEntryHandlerKey| $opt:ident.*) => pure (opt.getId.eraseMacroScopes, .wildcard) + | `(configEntryHandlerKey| *) => pure (.anonymous, .wildcard) + | _ => throwUnsupportedSyntax + handlers := handlers.push { ref := key, key := optName, body, kind } + | _ => throwUnsupportedSyntax + | _ => throwUnsupportedSyntax + return { omitFields, handlers } + +/-- +`def_eval_config_item f binders* for struct` defines a `ConfigEval.EvalConfigItem struct` structure named `f` +parameterized by the given binders. This structure contains a setter for updating a configuration +object of type `struct`. + +The command will transitively derive any necessary `ConfigEval.EvalTerm`/`ConfigEval.EvalExpr` +instances to support evaluation of configuration options for structure fields. +The syntax supports `public`/`private` modifiers. It also supports `scoped`/`local`, which apply +to any derived instances. + +The `EvalConfigItem struct` structure can be customized with a `where` clause. +The possible items of the `where` clause are: +- `omit f1, f2, f3` disables generating setters for fields `f1`, `f2`, and `f3` of `struct` +- `option key := fun cfg item => ...` adds a configuration option named `key` with the given +expression as its handler. The handler is only called when the key is an exact match. +The provided value is in `item.value`. Such a handler implies `omit key`. +- `option key* := fun cfg item => ...` adds configuration options with `key` as a proper prefix. +The most-specific `*` handler is called if no handlers for exact matches apply. +-/ +elab (name := defEvalConfigItemCmd) + doc?:(docComment)? vis?:(visibility)? kind:attrKind tk:"def_eval_config_item " fn:ident binders:(bracketedBinder)* " for " struct:ident + entries?:(configEntries)? : command => do + let view ← mkEvalConfigItemView entries? + defEvalConfigItem doc? vis? kind tk struct fn binders view + +open Linter.MissingDocs in +@[builtin_missing_docs_handler defEvalConfigItemCmd] +private def checkDefEvalConfigItemCmd : SimpleHandler := mkSimpleHandler "config elab" + +open Lean.Parser.Term in +private meta def getBracketedBinderArgs (stx : Syntax) : MacroM (Array Term) := + match stx with + | `(bracketedBinderF|($ids:ident* $[: $ty?]? $(_annot?)?)) => return ids + | `(bracketedBinderF|{$ids:ident* $[: $_]?}) => return ids + | `(bracketedBinderF|⦃$ids:ident* : $_⦄) => return ids + | `(bracketedBinderF|[$id:ident : $_]) => return #[id] + | `(bracketedBinderF|[$_]) => return #[mkHole stx] + | _ => Macro.throwErrorAt stx "Unsupported binder" + +private meta def mkElabConfigCmd + (monad : Ident) + (mkMonadAdapt : Term → MacroM Term) + (logExceptionsDefault : Term) + (mkLogExceptionsTerm : Term → MacroM Term) + (doc? : Option (TSyntax ``Parser.Command.docComment)) + (vis? : Option (TSyntax ``Parser.Command.visibility)) + (tk : Syntax) + (elabName type : Ident) + (binders : TSyntaxArray ``Parser.Term.bracketedBinder) + (entries? : Option (TSyntax ``Elab.ConfigEval.configEntries)) : + MacroM Command := do + let fnName := mkIdentFrom elabName (elabName.getId ++ `evalConfigItem) + let binderArgs ← binders.foldlM (init := #[]) fun args binder => do + pure <| args ++ (← getBracketedBinderArgs binder) + let cfgIdent := mkIdent `cfg + let initIdent := mkIdent `init + let logExceptionsIdent := mkIdent `logExceptions + let logExceptionsTerm ← mkLogExceptionsTerm logExceptionsIdent + let go ← mkMonadAdapt =<< `(EvalConfigItem.setConfig' eval $initIdent $cfgIdent (onErr := onErr) (logExceptions := $logExceptionsTerm)) + withRef (mkNullNode #[tk, elabName, type]) do + `(private local def_eval_config_item $fnName $[$binders]* for $type $[$entries?:configEntries]? + $[$doc?:docComment]? + $[$vis?:visibility]? def $elabName $[$binders]* ($cfgIdent : Lean.Syntax) ($initIdent : $type := {}) ($logExceptionsIdent : Bool := $logExceptionsDefault) : $monad $type := do + let eval : EvalConfigItem $type := @$fnName $binderArgs* + let onErr := EvalConfigItem.defaultOnErr (cfgType? := mkConst ``$type) + $go:term) + +/-- +`declare_core_config_elab f struct binders* [where ...]` defines a configuration elaborator +```lean +f binders* (cfg : Syntax) (init : struct := {}) (logExceptions : Bool := false) : CoreM struct +``` +that evaluates the `cfg` configuration items to update `init`. +Acceptable configuration syntax is documented in `Lean.Elab.ConfigEval.foldConfigM`, +which includes anything that looks like `Lean.Parser.Term.optConfig`, possibly wrapped +in null nodes. + +The command will transitively derive any necessary `ConfigEval.EvalTerm`/`ConfigEval.EvalExpr` +instances to support evaluation of configuration options for structure fields. +These instances will be `private local`. + +See `ConfigEval.defEvalConfigItemCmd` for further documentation. + +See also `declare_term_config_elab`, `declare_config_elab`, and `declare_command_config_elab`. +-/ +macro (name := elabDeclareCoreConfigElab) doc?:(docComment)? vis?:(visibility)? + tk:"declare_core_config_elab" elabName:ident type:ident binders:(bracketedBinder)* + entries?:(configEntries)? : command => do + mkElabConfigCmd (mkCIdent ``CoreM) pure (mkCIdent ``false) + (fun logExceptions => pure logExceptions) + doc? vis? tk elabName type binders entries? + +open Linter.MissingDocs in +@[builtin_missing_docs_handler elabDeclareCoreConfigElab] +private def checkDeclareCoreConfigElab : SimpleHandler := mkSimpleHandler "config elab" + +/-- +`declare_term_config_elab f struct binders* [where ...]` defines a configuration elaborator +```lean +f binders* (cfg : Syntax) (init : struct := {}) (logExceptions : Bool := true) : TermElabM struct +``` +that evaluates the `cfg` configuration items to update `init`. +Acceptable configuration syntax is documented in `Lean.Elab.ConfigEval.foldConfigM`, +which includes anything that looks like `Lean.Parser.Term.optConfig`, possibly wrapped +in null nodes. + +When `logExceptions` is true, it uses the current `errToSorry` state to decide whether or not to +recover by logging errors and skipping invalid options. + +The command will transitively derive any necessary `ConfigEval.EvalTerm`/`ConfigEval.EvalExpr` +instances to support evaluation of configuration options for structure fields. +These instances will be `private local`. + +See `ConfigEval.defEvalConfigItemCmd` for further documentation. + +See also `declare_core_config_elab`, `declare_config_elab`, and `declare_command_config_elab`. +-/ +macro (name := elabDeclareTermConfigElab) doc?:(docComment)? vis?:(visibility)? + tk:"declare_term_config_elab" elabName:ident type:ident binders:(bracketedBinder)* + entries?:(configEntries)? : command => do + mkElabConfigCmd (mkCIdent ``TermElabM) pure (mkCIdent ``true) + (fun logExceptions => `($logExceptions && (← read).errToSorry)) + doc? vis? tk elabName type binders entries? + +open Linter.MissingDocs in +@[builtin_missing_docs_handler elabDeclareTermConfigElab] +private def checkDeclareTermConfigElab : SimpleHandler := mkSimpleHandler "config elab" + +/-- +`declare_config_elab f struct binders* [where ...]` defines a configuration elaborator +```lean +f binders* (cfg : Syntax) (init : struct := {}) (logExceptions : Bool := true) : TacticM struct +``` +that evaluates the `cfg` configuration items to update `init`. +Acceptable configuration syntax is documented in `Lean.Elab.ConfigEval.foldConfigM`, +which includes anything that looks like `Lean.Parser.Term.optConfig`, possibly wrapped +in null nodes. + +When `logExceptions` is true, it uses the current `recover` state to decide whether or not to +recover by logging errors and skipping invalid options. + +The command will transitively derive any necessary `ConfigEval.EvalTerm`/`ConfigEval.EvalExpr` +instances to support evaluation of configuration options for structure fields. +These instances will be `private local`. + +See `ConfigEval.defEvalConfigItemCmd` for further documentation. + +See also `declare_core_config_elab`, `declare_term_config_elab`, and `declare_command_config_elab`. +-/ +macro (name := elabDeclareTacticConfig) doc?:(docComment)? vis?:(visibility)? + tk:"declare_config_elab" elabName:ident type:ident binders:(bracketedBinder)* + entries?:(configEntries)? : command => do + mkElabConfigCmd (mkCIdent ``Tactic.TacticM) pure (mkCIdent ``true) + (fun logExceptions => `($logExceptions && (← read).recover)) + doc? vis? tk elabName type binders entries? + +open Linter.MissingDocs in +@[builtin_missing_docs_handler elabDeclareTacticConfig] +private def checkDeclareTacticConfig : SimpleHandler := mkSimpleHandler "config elab" + +/-- +`declare_core_config_elab f struct binders* [where ...]` defines a configuration elaborator +```lean +f binders* (cfg : Syntax) (init : struct := {}) (logExceptions : Bool := true) : CommandElabM struct +``` +that evaluates the `cfg` configuration items to update `init`. +Acceptable configuration syntax is documented in `Lean.Elab.ConfigEval.foldConfigM`, +which includes anything that looks like `Lean.Parser.Term.optConfig`, possibly wrapped +in null nodes. + +The command will transitively derive any necessary `ConfigEval.EvalTerm`/`ConfigEval.EvalExpr` +instances to support evaluation of configuration options for structure fields. +These instances will be `private local`. + +See `ConfigEval.defEvalConfigItemCmd` for further documentation. + +See also `declare_core_config_elab`, `declare_term_config_elab`, and `declare_config_elab`. +-/ +macro (name := elabDeclareCommandConfig) doc?:(docComment)? vis?:(visibility)? + tk:"declare_command_config_elab" elabName:ident type:ident binders:(bracketedBinder)* + entries?:(configEntries)? : command => do + mkElabConfigCmd (mkCIdent ``CommandElabM) (fun eval => `(Command.liftTermElabM $eval)) (mkCIdent ``true) + (fun logExceptions => pure logExceptions) + doc? vis? tk elabName type binders entries? + +open Linter.MissingDocs in +@[builtin_missing_docs_handler elabDeclareCommandConfig] +private def checkCommandConfigElab : SimpleHandler := mkSimpleHandler "config elab" + +end Lean.Elab.ConfigEval diff --git a/src/Lean/Elab/ConfigEval/DeriveEvalConfigItem.lean b/src/Lean/Elab/ConfigEval/DeriveEvalConfigItem.lean new file mode 100644 index 0000000000..1fb205140b --- /dev/null +++ b/src/Lean/Elab/ConfigEval/DeriveEvalConfigItem.lean @@ -0,0 +1,371 @@ +/- +Copyright (c) 2026 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Kyle Miller +-/ +module + +prelude +public import Lean.Elab.ConfigEval.DeriveEvalTerm +public import Lean.Elab.ConfigEval.DeriveEvalExpr +import Lean.Elab.ConfigEval.Util +public import Lean.Elab.ConfigEval.Basic +public import Lean.Elab.ConfigEval.Instances + +/-! +# Derivation of `EvalConfigItem` + +This module defines `defEvalConfigItem`, which derives an `EvalConfigItem` object for structures. +Its main interface are the command syntaxes defined in `Lean.Elab.ConfigEval.Commands`. + +-/ + +public section + +namespace Lean.Elab.ConfigEval + +open Meta Term Command + +inductive EvalConfigItemHandlerKind + /-- Handler is called when its key matches the configuration key exactly. + The matched key is not allowed to be `Name.anonymous`. -/ + | exact + /-- Handler is called when its key is a strict prefix of the configuration key. + The matched key may be `Name.anonymous`. -/ + | wildcard + deriving BEq + +structure EvalConfigItemHandler where + /-- Ref for the key. -/ + ref : Syntax + /-- The key that's handled. May be anonymous for certain kinds. -/ + key : Name + /-- The kind of match this handler is looking for. -/ + kind : EvalConfigItemHandlerKind + /-- A function `fun cfg item => ...`. -/ + body : Term + /-- Constant to use for terminfo. This is added to the `HandlerTrie`. -/ + projFn? : Option Name := none + /-- Constant to use for field completion terminfo. -/ + struct? : Option Name := none + +structure EvalConfigItemView where + /-- Fields to not automatically synthesize handlers for, in addition to those keys + already appearing in `handlers`. -/ + omitFields : Array (Ident × Name) + /-- Explicitly provided handlers. -/ + handlers : Array EvalConfigItemHandler + +/-- +Trie used to organize those handlers provided in `EvalConfigItemView` and those +handlers that are synthesized. + +The fields in this `structure` are given in the order they are applied. +Conceptually, searching for handlers is done recursively (however the algorithm is compiled +into non-recursive code via metaprogramming). At each step of the search the state +consists of a trie key `tkey`, a trie node `trie`, and a configuration key `ckey`. +Once any handler is applied, matching is complete (handlers can't decide not to apply at run time). +1. If `exact?` is present and `tkey == ckey`, then it is applied. +2. If `ckey` is of the form `root.ckey'` and there's a `(root, trie')` entry in `children`, + then we recursively search for a handler using `tkey.root`, `trie'`, `ckey'`. + If one is found, it is applied. +3. If `wildcard?` is present and `ckey'` is nonempty, then that handler is applied. +4. Otherwise, the search failed. If this is recursive, we return and continue. +-/ +private structure HandlerTrie where + /-- The `EvalConfigItemHandlerKind.exact` handler for this trie position's key. -/ + exact? : Option EvalConfigItemHandler := none + /-- Handlers for which this trie position's key is a strict prefix. -/ + children : Array (String × HandlerTrie) := #[] + /-- The `EvalConfigItemHandlerKind.wildcard` handler for this trie position's key. -/ + wildcard? : Option EvalConfigItemHandler := none + /-- Constant to use for terminfo. The root of the trie does not have this set. + Collected from `EvalConfigItemHandler.projFn?`. -/ + projFn? : Option Name := none + /-- Constant to use for field completion terminfo. The root of the trie has this set. + Collected from `EvalConfigItemHandler.struct?`. -/ + struct? : Option Name := none + deriving Inhabited + +/-- +Finds a handler that applies to this key. +Returns the trie key and the handler. + +If `kind` is `exact` then it returns the handler that would actually apply, +and if it is `wildcard` then it returns the wildcard handler corresponding to that +key if an `exact` handler would also apply. +-/ +private partial def HandlerTrie.find? (trie : HandlerTrie) (key : Name) (kind : EvalConfigItemHandlerKind) : + Option (Name × EvalConfigItemHandler) := do + let root := key.getRoot + if root.isAnonymous then + match kind with + | .exact => return (.anonymous, ← trie.exact?) + | .wildcard => return (.anonymous, ← trie.wildcard?) + else + let s := root.getString! + try + let (_, child) ← trie.children.find? (·.1 == s) + let (key', h) ← child.find? (key.replacePrefix root .anonymous) kind + pure (root.appendCore key', h) + catch _ => + let h ← trie.wildcard? + return (key, h) + +/-- +Inserts the handler into the trie. The expectation is that a handler is not already +installed at a given key (use `HandlerTrie.find?` to verify this ahead of time), +but it is implemented to replace handlers. + +`EvalConfigItemHandler.key` is modified +-/ +private partial def HandlerTrie.insert (trie : HandlerTrie) (h : EvalConfigItemHandler) (key : Name := h.key) : + HandlerTrie := + let root := key.getRoot + if root.isAnonymous then + let projFn? := trie.projFn? <|> h.projFn? + let struct? := trie.struct? <|> h.struct? + match h.kind with + | .exact => { trie with projFn?, struct?, exact? := some h } + | .wildcard => { trie with projFn?, struct?, wildcard? := some h } + else + let s := root.getString! + let key' := key.replacePrefix root .anonymous + if let some idx := trie.children.findIdx? (·.1 == s) then + let children := trie.children.modify idx fun (s, child) => (s, child.insert h key') + { trie with children } + else + let child := HandlerTrie.insert {} h key' + { trie with children := trie.children.push (s, child)} + +private partial def HandlerTrie.insertStruct (trie : HandlerTrie) (key : Name) (struct : Name) : + HandlerTrie := + let root := key.getRoot + if root.isAnonymous then + let struct := trie.struct?.getD struct + { trie with struct? := some struct } + else + let s := root.getString! + let key' := key.replacePrefix root .anonymous + if let some idx := trie.children.findIdx? (·.1 == s) then + let children := trie.children.modify idx fun (s, child) => (s, child.insertStruct key' struct) + { trie with children } + else + let child := HandlerTrie.insertStruct {} key' struct + { trie with children := trie.children.push (s, child)} + +/-- +Precompiled version of `evalTermOrExprWithElab (α := Bool)` that +also makes use of the cached `item.bool?` value. +-/ +def evalBoolItem (item : ConfigItem) : TermElabM Bool := do + if let some b := item.bool? then + if (← getInfoState).enabled then + addTermInfo' item.value (if b then toExpr true else toExpr false) + return b + else + evalTermOrExprWithElab ⟨item.value⟩ + +def addConstInfo' (ref : Syntax) (projFn : Name) : TermElabM Unit := do + if (← getInfoState).enabled then + if (← getEnv).contains projFn then -- in case we are in Lean prelude + addConstInfo ref projFn + +private structure State where + toDerive : NameMap ExprSet := {} + toOmit : Array (Ident × Name) + +/-- Monad for collecting types that we should try deriving `EvalTerm` or `EvalExpr` instances for. -/ +private abbrev M := StateRefT State TermElabM + +private def addToDerive (cls : Name) (ty : Expr) : M Unit := + modify fun s => { s with toDerive := s.toDerive.insert cls (s.toDerive.getD cls {} |>.insert ty) } + +private def hasToOmit (key : Name) (projFn : Name) : M Bool := do + let s ← get + if let some idx := s.toOmit.findIdx? (fun (_, name) => name == key) then + let (ref, _) := s.toOmit[idx]! + addConstInfo ref projFn + set { s with toOmit := s.toOmit.eraseIdx! idx } + return true + else + return false + +/-- +Makes an `EvalConfigItem` for the structure. +Supports structures with no parameters or universes. +-/ +partial def defEvalConfigItem + (doc? : Option (TSyntax ``Parser.Command.docComment)) + (vis? : Option (TSyntax ``Parser.Command.visibility)) + (kind : TSyntax ``Parser.Term.attrKind) + (tk : Syntax) + (struct : Ident) + (fnIdent : Ident) + (extraBinders : TSyntaxArray ``Parser.Term.bracketedBinder) + (view : EvalConfigItemView) : + CommandElabM Unit := do + let structName ← liftTermElabM <| realizeGlobalConstNoOverloadWithInfo struct + -- Pass one: make the trie to collect the missing instances + let (_, { toOmit, toDerive }) ← liftTermElabM <| mkTrie structName true |>.run { toOmit := view.omitFields } + for (ref, name) in toOmit do + logErrorAt ref m!"No such field `{name}` of `{.ofConstName structName}`" + -- Now that we're back in CommandElabM, derive instances + for ty in toDerive.getD ``EvalTerm {} do + try + ensureEvalTerm vis? kind tk struct ty + catch ex => + trace[Elab.ConfigEval] "Deriving EvalTerm instance for `{ty}` failed: {ex.toMessageData}" + for ty in toDerive.getD ``EvalExpr {} do + try + ensureEvalExpr vis? kind tk struct ty + catch ex => + trace[Elab.ConfigEval] "Deriving EvalEval instance for `{ty}` failed: {ex.toMessageData}" + -- Pass two: rebuild the trie in the presense of these instances, and build the command + let cmd ← liftTermElabM <| withFreshMacroScope <| mkCmd structName + elabCommand cmd +where + hasInstance (cls : Name) (ty : Expr) : M Bool := do + try + discard <| synthInstance (← mkAppM cls #[ty]) + return true + catch _ => + unless ty.hasFVar do + addToDerive cls ty + return false + checkStruct (structName : Name) : MetaM Unit := do + let env ← getEnv + unless isStructure env structName do + throwErrorAt struct "`{.ofConstName structName}` is not a structure" + let .inductInfo val ← getConstInfo structName + | throwErrorAt struct "`{.ofConstName structName}` is not a structure" + unless val.levelParams.isEmpty && val.numIndices == 0 && val.numParams == 0 do + throwErrorAt struct "`{.ofConstName structName}` must not have parameters, indices, or universe parameters" + visitStruct (trie : HandlerTrie) (keyPrefix : Name) (structName : Name) (allowFailure : Bool) : M HandlerTrie := do + withTraceNode `Elab.ConfigEval (fun _ => return m!"adding handlers for fields of `{.ofConstName structName}` with prefix `{keyPrefix}`, allowFailure: {allowFailure}") do + checkStruct structName + let fields := getStructureFieldsFlattened (← getEnv) structName (includeSubobjectFields := false) + withLocalDeclD `self (Expr.const structName []) fun self => do + let mut trie := trie + for field in fields do + let key := keyPrefix ++ field + let proj ← mkProjection self field + let some projFn := proj.getAppFn.constName? | panic! "(Internal error) Invalid projection {inlineExpr proj}" + if (← hasToOmit key projFn) then + trace[Elab.ConfigEval] "key `{key}` was excluded, skipping" + continue + let fieldTy ← inferType proj + let exactHandler? := trie.find? key .exact + let mut hasExact := exactHandler?.any fun (key', _) => key == key' + let hasWildcard := (trie.find? key .wildcard).isSome + trace[Elab.ConfigEval] m!"key `{key}` hasExact: {hasExact}, hasWildcard: {hasWildcard}" + let mut synthesizedHandler := false + -- If there's no exact key for this field yet, synthesize a handler + if !hasExact then + let mut body ← `(pure { config with $(mkIdent key):ident := value }) + if ← withReducible <| isDefEq fieldTy (mkConst ``Bool) then + trace[Elab.ConfigEval] "field `{.ofConstName projFn}`, using {.ofConstName ``evalBoolItem}" + body ← `(fun config item => evalBoolItem item >>= fun value => $body:term) + trie := trie.insert { ref := struct, key, kind := .exact, body, projFn? := projFn } + hasExact := true + synthesizedHandler := true + else + let hasEvalTerm ← hasInstance ``EvalTerm fieldTy + let hasEvalExpr ← hasInstance ``EvalExpr fieldTy + trace[Elab.ConfigEval] "field `{.ofConstName projFn}`, hasEvalTerm: {hasEvalTerm}, hasEvalExpr: {hasEvalExpr}" + hasExact := hasEvalTerm || hasEvalExpr + synthesizedHandler := synthesizedHandler || hasEvalTerm || hasEvalExpr + let mkHandler (eval : Term) : M Term := + `(item.checkNotBool >>= fun _ => $eval:term >>= fun value => $body) + body ← + match hasEvalTerm, hasEvalExpr with + | true, true => `(evalTermOrExprWithElab ⟨item.value⟩) >>= mkHandler + | false, true => `(evalExprWithElab ⟨item.value⟩) >>= mkHandler + | true, false => `(evalTermWithRef ⟨item.value⟩) >>= mkHandler + | false, false => `(item.throwCannotSetOption $(quote structName)) + body ← `(fun _ item => $body) + trie := trie.insert { ref := struct, key, kind := .exact, body, projFn? := projFn } + if let some structName' := (← whnfR fieldTy).constName? then + if isStructure (← getEnv) structName' then + trie := trie.insertStruct key structName' + if ← try checkStruct structName'; pure true catch _ => pure false then + /- + Heuristic: if there is already a handler for an exact match, we shouldn't report errors + if sub-keys can't be used. In Mathlib for example, the `linarith` tactic has configuration + options that are `structure`s wrapping monadic and functional values. Users are only + meant to set the entire `structure`, not the fields within them. We are imagining here + that `structure` configuration values are not common, so we shouldn't rigidly expect + handlers for sub-keys (saving metaprogram authors the hassle of writing complete `except` + clauses). We may consider `(allowFailure := true)` in the future, and/or `except foo.*` clauses. + -/ + trie ← visitStruct trie key structName' (allowFailure := allowFailure || hasExact || exactHandler?.isSome) + unless allowFailure || hasExact || hasWildcard || synthesizedHandler do + throwErrorAt struct (m!"Field `{key}` of type{inlineExpr fieldTy}is missing both `{.ofConstName ``EvalTerm}` and `{.ofConstName ``EvalExpr}` instances." + ++ .note m!"The scoped `ensure_eval_term_instance` and `ensure_eval_expr_instance` commands in `Lean.Elab.ConfigEval` were not able to derive instances.") + return trie + mkTrie (structName : Name) (allowFailure : Bool) : M HandlerTrie := do + let mut trie : HandlerTrie := {} + trie := trie.insertStruct Name.anonymous structName + for handler in view.handlers do + if handler.key.isAnonymous && handler.kind matches .exact then + throwErrorAt handler.ref "Unexpected empty key for handler" + if let some (key, _) := trie.find? handler.key handler.kind then + throwErrorAt handler.ref "Duplicate handler for key `{key}`" + trie := trie.insert handler + trie ← visitStruct trie .anonymous structName allowFailure + unless (← hasToOmit `config structName) || (trie.find? `config .exact).isSome do + if ← hasInstance ``EvalExpr (mkConst structName) then + -- Only use an `EvalExpr` instance; we don't have plans to support structure instance notation with `EvalTerm`. + let cfgBody ← `(fun _ item => (evalExprWithElab ⟨item.value⟩ : TermElabM $struct)) + trie := trie.insert { ref := tk, key := `config, kind := .exact, body := cfgBody } + return trie + /-- + Assembles the full key matcher from the trie. Makes use of `item` in the current macro scope. + -/ + assemble (trie : HandlerTrie) (onFail : Term) : TermElabM Term := do + let { exact?, children, wildcard?, projFn?, struct? } := trie + let bodyApplied (handler : EvalConfigItemHandler) : TermElabM Term := do + `(($handler.body : $struct → ConfigItem → TermElabM $struct) config item') + let handleChildren (onFail : Term) : TermElabM Term := do + if children.isEmpty then + return onFail + else + let children ← children.mapM fun (s, trie') => return (s, ← assemble trie' onFail) + let body ← makeStringMatcher (← `(ident| root)) children onFail + `(have root := item.getRootStr + have item' := item + have item := item.shift + $body) + let handleWildcard : TermElabM Term := do + if let some h := wildcard? then + let body ← bodyApplied h + if children.isEmpty then + return body + else + let jp ← withFreshMacroScope `(ident| doWildcard) + let body' ← handleChildren (← `($jp ())) + `(have $jp (_ : Unit) := $body; $body') + else + handleChildren onFail + let handleExact : TermElabM Term := do + let body ← handleWildcard + let onAnon ← if let some h := exact? then bodyApplied h else pure onFail + `(if item.isAnonymous then $onAnon else $body) + let mut body ← handleExact + if let some projFn := projFn? then + body ← `(item'.addConstInfo $(quote projFn) >>= fun _ => $body) + if let some struct := struct? then + body ← `(item.addCompletionInfo $(quote struct) >>= fun _ => $body) + return body + mkCmd (structName : Name) : TermElabM Command := do + let trie ← mkTrie structName false |>.run' { toOmit := view.omitFields } + let body ← assemble trie (← `(invalidOption item)) + `($[$doc?:docComment]? + $[$vis?:visibility]? + def $fnIdent $[$extraBinders]* : EvalConfigItem $struct where + set (config : $struct) (item : ConfigItem) : TermElabM $struct := do + have invalidOption (item : ConfigItem) : TermElabM $struct := item.throwInvalidOption (some $(quote structName)) + let item' := item + $body:term) + +end Lean.Elab.ConfigEval diff --git a/src/Lean/Elab/ConfigEval/DeriveEvalExpr.lean b/src/Lean/Elab/ConfigEval/DeriveEvalExpr.lean new file mode 100644 index 0000000000..54ee15bc8b --- /dev/null +++ b/src/Lean/Elab/ConfigEval/DeriveEvalExpr.lean @@ -0,0 +1,129 @@ +/- +Copyright (c) 2026 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Kyle Miller +-/ +module + +prelude +public import Lean.Elab.ConfigEval.Basic +import Lean.Elab.ConfigEval.Util +public import Lean.Elab.Command +import Lean.Elab.DeclNameGen +import all Lean.Elab.ErrorUtils +public import Lean.Meta.Eval + +public section + +namespace Lean.Elab.ConfigEval + +open Meta Term Command + +namespace EvalExpr + +def withSimpleEvalExpr {α : Type} (c : Name) (evalExprImpl : String → Array Expr → MetaM α) : Expr → MetaM α := + withWHNF (errMsg := m!"\nExpecting `{.ofConstName c}`.") fun e => do + let some ctor := e.getAppFn.constName? | throwUnsupportedExpr + let Name.str c' s := ctor | throwUnsupportedExpr + unless (c == c') do throwUnsupportedExpr + evalExprImpl s e.getAppArgs + +end EvalExpr + +open EvalExpr + +/-- +Ensures an `EvalExpr` instance exists for the given type by deriving one if necessary. +Derivation can handle `EvalExpr` instance for nonrecursive inductive types without universes, parameters, or indices, +and which only does simple recursion. +-/ +def ensureEvalExpr + (vis? : Option (TSyntax `Lean.Parser.Command.visibility)) + (kind : TSyntax `Lean.Parser.Term.attrKind) + (cmdRef typeRef : Syntax) (type : Expr) : CommandElabM Unit := do + withClassInstDeps ``EvalExpr type extraDeps fun type' => withRef cmdRef do + let ival ← getIndType type' + let indTypeIdent := mkCIdentFrom typeRef ival.name + let instName ← NameGen.mkBaseNameWithSuffix' "inst" #[] <| ← ``(EvalExpr $indTypeIdent) + let evalExprDef := mkIdent (instName ++ Name.mkSimple "evalExpr") + let mut exprCases : Array (String × Term) := #[] + for ctorName in ival.ctors do + if useCtor ival ctorName then + let (xs, _, _) ← forallMetaTelescopeReducing (← inferType (mkConst ctorName)) + let .str _ ctorName' := ctorName | unreachable! + let vs ← xs.mapM fun _ => mkIdent <$> Core.mkFreshUserName `v + let val ← `(pure ($(mkCIdent ctorName) $vs*)) + let recArgs ← xs.mapM fun x => return (← instantiateMVars (← inferType x)) == type' + let val ← (((Array.range xs.size).zip recArgs).zip vs).foldrM (init := val) fun ((idx, recArg), v) val => + if recArg then + `($evalExprDef args[$(quote idx)]! >>= fun $v => $val) + else + `(EvalExpr.evalExpr args[$(quote idx)]! >>= fun $v => $val) + let val ← `(guard (args.size == $(quote xs.size)) *> $val) + exprCases := exprCases.push (ctorName', val) + let exprMatcher ← makeStringMatcher (← `(ident| ctor)) exprCases (← `(throwUnsupportedExpr)) + `($[$vis?:visibility]? partial def $evalExprDef : Expr → MetaM $indTypeIdent := + withSimpleEvalExpr $(quote ival.name) fun ctor args => $exprMatcher + $[$vis?:visibility]? $kind:attrKind instance%$cmdRef $(mkIdentFrom cmdRef instName (canonical := type == type')):ident : EvalExpr $indTypeIdent where + evalExpr := $evalExprDef + expectedType? := some (Expr.const $(quote ival.name) [])) +where + getIndType (type : Expr) : TermElabM InductiveVal := withRef typeRef do + let some indTypeName := (← whnfR type).constName? + | throwError "`{type}` is not a constant" + let .inductInfo ival ← getConstInfo indTypeName + | throwError "`{.ofConstName indTypeName}` is not an inductive type" + unless ival.levelParams.isEmpty && ival.numParams == 0 && ival.numIndices == 0 do + throwError "`{.ofConstName indTypeName}` has universe parameters, parameters, or indices" + if ival.isNested || ival.isReflexive then + throwError "`{.ofConstName indTypeName}` has unsupported recursion" + return ival + useCtor (ival : InductiveVal) (ctorName : Name) : Bool := + ctorName.isStr && !ctorName.hasMacroScopes && !isPrivateName ctorName && ctorName.getPrefix == ival.name + extraDeps (type : Expr) : TermElabM (Array Expr) := withRef typeRef do + let ival ← getIndType type + let mut deps := #[] + for ctorName in ival.ctors do + if useCtor ival ctorName then + let (xs, bis, _) ← forallMetaTelescopeReducing (← inferType (mkConst ctorName)) + unless bis.all (·.isExplicit) do + throwError "Every field of `{.ofConstName ctorName}` must be explicit" + for x in xs do + let xTy ← inferType x + if xTy.hasMVar then + throwError "Field `{x}` of `{.ofConstName ctorName}` is dependent" + if xTy == type then + continue + deps := deps.push xTy + return deps + +@[expose] unsafe def evalMetaEval (α : Type) (typeName : Name) (moduleName? : Option Name) (e : Expr) : MetaM α := do + unless (← getEnv).contains typeName do + let fromMsg := if let some moduleName := moduleName? then m!" (from `{moduleName}`)" else m!"" + throwError m!"Error evaluating configuration: the type `{typeName}`{fromMsg} is not in scope here" + recordExtraModUseFromDecl (isMeta := true) typeName + let eType ← inferType e + unless ← isDefEqGuarded (mkConst typeName) eType do + throwError "Type mismatch. Option value{inlineExpr e}{← mkHasTypeButIsExpectedMsg eType (mkConst typeName)}" + try + withoutModifyingEnv <| Meta.evalExpr' α typeName e (safety := .partial) + catch ex => + throwError m!"Error evaluating{indentExpr e}\n\nException: {ex.toMessageData}" + +/-- Creates an `EvalExpr` instance that uses `Meta.evalExpr` to compile and evaluate the expression. -/ +def deriveEvalExprUsingMetaEval + (vis? : Option (TSyntax `Lean.Parser.Command.visibility)) + (kind : TSyntax `Lean.Parser.Term.attrKind) + (cmdRef typeRef : Syntax) (type : Expr) : CommandElabM Unit := do + let cmd ← liftTermElabM <| withFreshMacroScope do + let Expr.const typeName [] := type + | throwErrorAt typeRef "Expecting a constant with no universes, not `{type}`" + let env ← getEnv + let moduleName? := (env.header.moduleNames[·]!) <$> env.getModuleIdxFor? typeName + let typeId := mkCIdentFrom typeRef typeName + `($[$vis?:visibility]? $kind:attrKind instance%$cmdRef : EvalExpr @$typeId where + evalExpr := unsafe evalMetaEval @$typeId $(quote typeName) $(quote moduleName?) + expectedType? := some (mkConst @$(quote typeName))) + elabCommand cmd + +end Lean.Elab.ConfigEval diff --git a/src/Lean/Elab/ConfigEval/DeriveEvalTerm.lean b/src/Lean/Elab/ConfigEval/DeriveEvalTerm.lean new file mode 100644 index 0000000000..11131bfe0e --- /dev/null +++ b/src/Lean/Elab/ConfigEval/DeriveEvalTerm.lean @@ -0,0 +1,156 @@ +/- +Copyright (c) 2026 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Kyle Miller +-/ +module + +prelude +public import Lean.Elab.ConfigEval.Basic +import Lean.Elab.ConfigEval.Util +public import Lean.Elab.Command +import Lean.Elab.DeclNameGen +import all Lean.Elab.ErrorUtils + +public section + +namespace Lean.Elab.ConfigEval + +open Meta Term Command + +namespace EvalTerm + +/-- +Resolves `id`, making sure the result is in namespace `c`. +Returns `s` if the resolved name is of the form of the form `Name.str c s`. +-/ +private def resolveAtomicNameForConstNamespace (c : Name) (id : Ident) : TermElabM String := do + let n := id.getId.eraseMacroScopes + -- For atomic names, resolve them as if `c` is the namespace. + if let Name.str Name.anonymous s := n then + let n' := Name.str c s + if (← getEnv).contains n' then + if (← getInfoState).enabled then + addConstInfo id n' + return s + let n ← realizeGlobalConstNoOverloadWithInfo id + if !n.hasMacroScopes && n.getPrefix == c then + if let Name.str _ s := n then + return s + throwUnsupportedSyntax + +/-- +Resolves `id` as if it were a dotted identifier for namespace `c`, +and returns `s` if the resolved name is of the form `Name.str c s`. +-/ +private def resolveDottedAtomicNameForConstNamespace (c : Name) (id : Ident) : TermElabM String := do + let n := id.getId.eraseMacroScopes + if let Name.str Name.anonymous s := n then + addCompletionInfo <| CompletionInfo.dotId id n {} (← mkConstWithLevelParams c) + let n' := Name.str c s + if (← getEnv).contains n' then + if (← getInfoState).enabled then + addConstInfo id n' + return s + else + resolveAtomicNameForConstNamespace c (mkIdentFrom id n') + else + throwUnsupportedSyntax + +/-- +Wrapper to handle atomic identifiers and dotted identifiers. +-/ +partial def withSimpleEvalStx {α} (indTypeName : Name) (evalStxImpl : String → TSyntaxArray `term → TermElabM (α × Expr)) : Term → TermElabM (α × Expr) := + evalTermWithInfo (Expr.const indTypeName []) fun + | `($f:ident) => do + let ctorName ← resolveAtomicNameForConstNamespace indTypeName f + evalStxImpl ctorName #[] + | `($f:ident $args*) => do + let ctorName ← resolveAtomicNameForConstNamespace indTypeName f + evalStxImpl ctorName args + | `(.$f:ident) => do + let ctorName ← resolveDottedAtomicNameForConstNamespace indTypeName f + evalStxImpl ctorName #[] + | `(.$f:ident $args*) => do + let ctorName ← resolveDottedAtomicNameForConstNamespace indTypeName f + evalStxImpl ctorName args + | _ => throwUnsupportedSyntax + +def checkExpectedNumberOfArguments (ctor : Name) (expected : Nat) (args : TSyntaxArray `term) : TermElabM Unit := do + unless expected == args.size do + throwError "unexpected number of arguments, `{.ofConstName ctor}` expects {expected} argument{expected.plural}, \ + but {args.size} {args.size.plural "was" "were"} provided" + +end EvalTerm + +open EvalTerm + +/-- +Ensures an `EvalTerm` instance exists for the given type by deriving one if necessary. +Derivation can handle `EvalTerm` instance for inductive types without universes, parameters, or indices, +and which only does simple recursion. +-/ +def ensureEvalTerm + (vis? : Option (TSyntax `Lean.Parser.Command.visibility)) + (kind : TSyntax `Lean.Parser.Term.attrKind) + (cmdRef typeRef : Syntax) (type : Expr) : CommandElabM Unit := do + withClassInstDeps ``EvalTerm type extraDeps fun type' => withRef cmdRef do + let ival ← getIndType type' + let indTypeIdent := mkCIdentFrom typeRef ival.name + let instName ← NameGen.mkBaseNameWithSuffix' "inst" #[] <| ← ``(EvalTerm $indTypeIdent) + let evalTermDef := mkIdent (instName ++ Name.mkSimple "evalTerm") + let mut stxCases : Array (String × Term) := #[] + for ctorName in ival.ctors do + if useCtor ival ctorName then + let (xs, _, _) ← forallMetaTelescopeReducing (← inferType (mkConst ctorName)) + let .str _ ctorName' := ctorName | unreachable! + let vs ← xs.mapM fun _ => mkIdent <$> Core.mkFreshUserName `v + let es ← xs.mapM fun _ => mkIdent <$> Core.mkFreshUserName `e + let expr ← `(Expr.const $(quote ctorName) []) + let expr ← es.foldlM (init := expr) fun expr e => `(Expr.app $expr $e) + let val ← `(pure ($(mkCIdent ctorName) $vs*, $expr)) + let recArgs ← xs.mapM fun x => return (← instantiateMVars (← inferType x)) == type' + let val ← (((Array.range xs.size).zip recArgs).zip (vs.zip es)).foldrM (init := val) fun ((idx, recArg), v, e) val => + if recArg then + `($evalTermDef args[$(quote idx)]! >>= fun ($v, $e) => $val) + else + `(EvalTerm.evalTerm args[$(quote idx)]! >>= fun ($v, $e) => $val) + let val ← `(checkExpectedNumberOfArguments $(quote ctorName) $(quote xs.size) args *> $val) + stxCases := stxCases.push (ctorName', val) + let stxMatcher ← makeStringMatcher (← `(ident| ctor)) stxCases (← `(throwUnsupportedSyntax)) + `($[$vis?:visibility]? partial def $evalTermDef : Term → TermElabM ($indTypeIdent × Expr) := + withSimpleEvalStx $(quote ival.name) fun ctor args => $stxMatcher + $[$vis?:visibility]? $kind:attrKind instance%$cmdRef $(mkIdentFrom cmdRef instName (canonical := type == type')):ident : EvalTerm $indTypeIdent where + evalTerm := $evalTermDef + typeExpr := Expr.const $(quote ival.name) []) +where + getIndType (type : Expr) : TermElabM InductiveVal := withRef typeRef do + let some indTypeName := (← whnfR type).constName? + | throwError "`{type}` is not a constant" + let .inductInfo ival ← getConstInfo indTypeName + | throwError "`{.ofConstName indTypeName}` is not an inductive type" + unless ival.levelParams.isEmpty && ival.numParams == 0 && ival.numIndices == 0 do + throwError "`{.ofConstName indTypeName}` has universe parameters, parameters, or indices" + if ival.isNested || ival.isReflexive then + throwError "`{.ofConstName indTypeName}` has unsupported recursion" + return ival + useCtor (ival : InductiveVal) (ctorName : Name) : Bool := + ctorName.isStr && !ctorName.hasMacroScopes && !isPrivateName ctorName && ctorName.getPrefix == ival.name + extraDeps (type : Expr) : TermElabM (Array Expr) := withRef typeRef do + let ival ← getIndType type + let mut deps := #[] + for ctorName in ival.ctors do + if useCtor ival ctorName then + let (xs, bis, _) ← forallMetaTelescopeReducing (← inferType (mkConst ctorName)) + unless bis.all (·.isExplicit) do + throwError "Every field of `{.ofConstName ctorName}` must be explicit" + for x in xs do + let xTy ← inferType x + if xTy.hasMVar then + throwError "Field `{x}` of `{.ofConstName ctorName}` is dependent" + if xTy == type then + continue + deps := deps.push xTy + return deps + +end Lean.Elab.ConfigEval diff --git a/src/Lean/Elab/ConfigEval/Extra.lean b/src/Lean/Elab/ConfigEval/Extra.lean new file mode 100644 index 0000000000..c5acd33639 --- /dev/null +++ b/src/Lean/Elab/ConfigEval/Extra.lean @@ -0,0 +1,38 @@ +/- +Copyright (c) 2026 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Kyle Miller +-/ +module + +prelude +public import Lean.Elab.ConfigEval.Instances + +public section + +namespace Lean.Elab.ConfigEval + +open Meta Term + +/-- +Uses global option declarations with the prefix `optionPrefix` when setting `Options`. +Assumes that `item` is shifted, with the rest of the item being the option name suffix to use. +-/ +def EvalConfigItem.evalSetOptions (optionPrefix : Name) (opts : Options) (item : ConfigItem) : TermElabM Options := do + let optName := optionPrefix ++ item.getCurrOptionName + -- TODO(kmill): record `optionPrefix` so that LSP can make correct suggestions + addCompletionInfo <| CompletionInfo.option (mkNullNode #[item.prevRoot, mkNullNode item.optionComps.toArray]) + let decl ← getOptionDecl optName + pushInfoLeaf <| .ofOptionInfo { stx := item.option, optionName := optName, declName := decl.declName } + let set (α : Type) [EvalTerm α] [EvalExpr α] [KVMap.Value α] : TermElabM Options := do + let value : α ← evalTermOrExprWithElab ⟨item.value⟩ + return opts.set optName value + match decl.defValue with + | .ofBool _ => set Bool + | .ofNat _ => item.checkNotBool; set Nat + | .ofInt _ => item.checkNotBool; set Int + | .ofString _ => item.checkNotBool; set String + | .ofName _ => item.checkNotBool; set Name + | .ofSyntax _ => throwErrorAt item.option "Cannot set `Syntax` option `{optName}`" + +end Lean.Elab.ConfigEval diff --git a/src/Lean/Elab/ConfigEval/Instances.lean b/src/Lean/Elab/ConfigEval/Instances.lean new file mode 100644 index 0000000000..d359db6613 --- /dev/null +++ b/src/Lean/Elab/ConfigEval/Instances.lean @@ -0,0 +1,288 @@ +/- +Copyright (c) 2026 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Kyle Miller +-/ +module + +prelude +public import Lean.Elab.ConfigEval.Basic + +/-! +# Evaluator instances for built-in types + +Some of these instances are hand-written instead of being derived, since the syntax may be special, +or they might make special assumptions on the type (e.g. for `Bool`, we assume the identifiers +`true` and `false` always refer to `Bool`'s constructors). +-/ + +public section + +namespace Lean.Elab.ConfigEval + +open Meta Term + +namespace EvalTerm +/-! +## `EvalTerm` instances +-/ + +def evalBoolStx : Term → TermElabM (Bool × Expr) := + evalTermWithInfo' fun stx => + let id := stx.raw.getId.eraseMacroScopes + if id == `true || id == ``true then + return true + else if id == `false || id == ``false then + return false + else + match stx with + | `(.true) => return true + | `(.false) => return false + | _ => throwUnsupportedSyntax + +def evalNatStx : Term → TermElabM (Nat × Expr) := + evalTermWithInfo' fun + | `($n:num) => return n.getNat + | _ => throwUnsupportedSyntax + +def evalIntStx : Term → TermElabM (Int × Expr) := + evalTermWithInfo' fun + | `($n:num) => return n.getNat + | `(-$n:num) => return -n.getNat + | _ => throwUnsupportedSyntax + +def evalStringStx : Term → TermElabM (String × Expr) := + evalTermWithInfo' fun + | `($s:str) => return s.getString + | _ => throwUnsupportedSyntax + +def evalNameStx : Term → TermElabM (Name × Expr) := + evalTermWithInfo' fun stx => do + if stx.raw.isOfKind ``Parser.Term.quotedName then + if let some n := stx.raw[0].isNameLit? then + return n + if stx.raw.isOfKind ``Parser.Term.doubleQuotedName then + -- Always allow quoting private names. + return ← withoutExporting do + let n ← realizeGlobalConstNoOverloadWithInfo stx.raw[2] + recordExtraModUseFromDecl (isMeta := false) n + return n + throwUnsupportedSyntax + +def evalOptionStx {α : Type} (typeExpr : Expr) (ev : Term → TermElabM (α × Expr)) : Term → TermElabM (Option α × Expr) := + evalTermWithInfo (Expr.app (Expr.const ``Option [0]) typeExpr) fun + | `(none) | `(.none) => return (none, Expr.app (Expr.const ``Option.none [0]) typeExpr) + | `(some $stx) | `(.some $stx) | stx => do + let (v, e) ← ev stx + return (some v, mkApp2 (Expr.const ``Option.some [0]) typeExpr e) + +def evalListStx {α : Type} (typeExpr : Expr) (ev : Term → TermElabM (α × Expr)) : Term → TermElabM (List α × Expr) := + evalTermWithInfo (Expr.app (Expr.const ``List [0]) typeExpr) fun + | `([$[$xs],*]) => do + let (vs, es) := (← xs.mapM ev).unzip + let e := es.foldr (init := Expr.app (Expr.const ``List.nil [0]) typeExpr) fun x e => + mkApp3 (Expr.const ``List.cons [0]) typeExpr x e + return (vs.toList, e) + | _ => throwUnsupportedSyntax + +def evalArrayStx {α : Type} (typeExpr : Expr) (ev : Term → TermElabM (α × Expr)) : Term → TermElabM (Array α × Expr) := + evalTermWithInfo (Expr.app (Expr.const ``Array [0]) typeExpr) fun + | `(#[$[$xs],*]) => do + let (vs, es) := (← xs.mapM ev).unzip + let e := es.foldr (init := Expr.app (Expr.const ``List.nil [0]) typeExpr) fun x e => + mkApp3 (Expr.const ``List.cons [0]) typeExpr x e + return (vs, mkApp2 (Expr.const ``List.toArray [0]) typeExpr e) + | _ => throwUnsupportedSyntax + +def evalProdStx {α α' : Type} (typeExpr typeExpr' : Expr) + (ev : Term → TermElabM (α × Expr)) (ev' : Term → TermElabM (α' × Expr)) : + Term → TermElabM ((α × α') × Expr) := + evalTermWithInfo (mkApp2 (Expr.const ``Prod [0, 0]) typeExpr typeExpr') fun + | `(($x, $x')) => do + let (v, e) ← ev x + let (v', e') ← ev' x' + return ((v, v'), mkApp4 (Expr.const ``Prod.mk [0, 0]) typeExpr typeExpr' e e') + | _ => throwUnsupportedSyntax + +def evalDataValueStx (stx : Term) : TermElabM (DataValue × Expr) := + let mk {α} (c : Name) (f : α → DataValue) (x : α × Expr) := (f x.1, Expr.app (.const c []) x.2) + (mk ``DataValue.ofBool DataValue.ofBool <$> evalBoolStx stx) + <|> (mk ``DataValue.ofNat DataValue.ofNat <$> evalNatStx stx) + <|> (mk ``DataValue.ofInt DataValue.ofInt <$> evalIntStx stx) + <|> (mk ``DataValue.ofString DataValue.ofString <$> evalStringStx stx) + <|> (mk ``DataValue.ofName DataValue.ofName <$> evalNameStx stx) + -- skipping `DataValue.ofSyntax` for now + <|> throwUnsupportedSyntax + +instance : EvalTerm Bool where + evalTerm := evalBoolStx + typeExpr := toTypeExpr Bool + +instance : EvalTerm Nat where + evalTerm := evalNatStx + typeExpr := toTypeExpr Nat + +instance : EvalTerm Int where + evalTerm := evalIntStx + typeExpr := toTypeExpr Int + +instance : EvalTerm String where + evalTerm := evalStringStx + typeExpr := toTypeExpr String + +instance : EvalTerm Name where + evalTerm := evalNameStx + typeExpr := toTypeExpr Name + +instance {α : Type} [EvalTerm α] : EvalTerm (Option α) where + evalTerm := evalOptionStx (EvalTerm.typeExpr α) evalTerm + typeExpr := Expr.app (Expr.const ``Option [0]) (EvalTerm.typeExpr α) + +instance {α : Type} [EvalTerm α] : EvalTerm (List α) where + evalTerm := evalListStx (EvalTerm.typeExpr α) evalTerm + typeExpr := Expr.app (Expr.const ``List [0]) (EvalTerm.typeExpr α) + +instance {α : Type} [EvalTerm α] : EvalTerm (Array α) where + evalTerm := evalArrayStx (EvalTerm.typeExpr α) evalTerm + typeExpr := Expr.app (Expr.const ``Array [0]) (EvalTerm.typeExpr α) + +instance {α α' : Type} [EvalTerm α] [EvalTerm α'] : EvalTerm (α × α') where + evalTerm := evalProdStx (EvalTerm.typeExpr α) (EvalTerm.typeExpr α') evalTerm evalTerm + typeExpr := mkApp2 (Expr.const ``Prod [0, 0]) (EvalTerm.typeExpr α) (EvalTerm.typeExpr α') + +instance : EvalTerm DataValue where + evalTerm := evalDataValueStx + typeExpr := Expr.const ``DataValue [] + +end EvalTerm + +namespace EvalExpr +/-! +## `EvalExpr` instances +-/ + +def evalBoolExprCore (e : Expr) : MetaM Bool := + match_expr e with + | Bool.true => return true + | Bool.false => return false + | _ => throwUnsupportedExpr + +def evalBoolExpr : Expr → MetaM Bool := + withWHNF (errMsg := m!"\nof type `{.ofConstName ``Bool}`.") evalBoolExprCore + +def evalNatExprCore (e : Expr) : MetaM Nat := + (e.nat? <|> e.rawNatLit?).getDM throwUnsupportedExpr + +def evalNatExpr : Expr → MetaM Nat := + withWHNF (errMsg := m!"\nof type `{.ofConstName ``Nat}`.") evalNatExprCore + +def evalIntExprCore (e : Expr) : MetaM Int := + e.int?.getM <|> Int.ofNat <$> evalNatExprCore e <|> + match_expr e with + | Int.ofNat e' => Int.ofNat <$> evalNatExpr e' + | Int.negSucc e' => Int.negSucc <$> evalNatExpr e' + | _ => throwUnsupportedExpr + +def evalIntExpr : Expr → MetaM Int := + withWHNF (errMsg := m!"\nof type `{.ofConstName ``Int}`.") evalIntExprCore + +def evalStringExprCore : Expr → MetaM String + | .lit (.strVal s) => return s + | _ => throwUnsupportedExpr + +def evalStringExpr : Expr → MetaM String := + withWHNF (errMsg := m!"\nof type `{.ofConstName ``String}`.") evalStringExprCore + +def evalNameExprCore (e : Expr) : MetaM Name := + e.name?.getDM throwUnsupportedExpr + +def evalNameExpr : Expr → MetaM Name := + withWHNF (errMsg := m!"\nof type `{.ofConstName ``Name}`.") evalNameExprCore + +def evalOptionExprCore {α : Type} (ev : Expr → MetaM α) (e : Expr) : MetaM (Option α) := + match_expr e with + | Option.none _ => return none + | Option.some _ x => some <$> ev x + | _ => throwUnsupportedExpr + +def evalOptionExpr {α : Type} (ev : Expr → MetaM α) (e : Expr) : MetaM (Option α) := + withWHNF (errMsg := m!"\nof type `{.ofConstName ``Option}`.") (evalOptionExprCore ev) e <|> some <$> ev e + +partial def evalListExpr {α : Type} (ev : Expr → MetaM α) (e : Expr) (didWHNF : Bool := false) : MetaM (List α) := do + match_expr (meta := false) e with + | List.nil _ => return [] + | List.cons _ x xs => + let v ← ev x + let vs ← evalListExpr ev xs (didWHNF := false) + return v :: vs + | _ => + if didWHNF then + throwError "Could not evaluate the expression{indentExpr e}\nof type `{.ofConstName ``List}`." + else + evalListExpr ev (← whnf e) (didWHNF := true) + +partial def evalArrayExpr {α : Type} (ev : Expr → MetaM α) : Expr → MetaM (Array α) := + withWHNF (errMsg := m!"\nof type `{.ofConstName ``Array}`.") fun e => + match_expr e with + | List.toArray _ e' => List.toArray <$> evalListExpr ev e' + | Array.mk _ e' => List.toArray <$> evalListExpr ev e' + | _ => throwUnsupportedExpr + +def evalDataValueExprCore (e : Expr) : MetaM DataValue := + match_expr e with + | DataValue.ofBool e => DataValue.ofBool <$> evalBoolExpr e + | DataValue.ofNat e => DataValue.ofNat <$> evalNatExpr e + | DataValue.ofInt e => DataValue.ofInt <$> evalIntExpr e + | DataValue.ofString e => DataValue.ofString <$> evalStringExpr e + | DataValue.ofName e => DataValue.ofName <$> evalNameExpr e + | _ => + (DataValue.ofBool <$> evalBoolExprCore e) + <|> (DataValue.ofNat <$> evalNatExprCore e) + <|> (DataValue.ofInt <$> evalIntExprCore e) + <|> (DataValue.ofString <$> evalStringExprCore e) + <|> (DataValue.ofName <$> evalNameExprCore e) + -- skipping `DataValue.ofSyntax` for now + <|> throwUnsupportedExpr + +def evalDataValueExpr : Expr → MetaM DataValue := + withWHNF (errMsg := m!"\nof type `{.ofConstName ``DataValue}`.") evalDataValueExprCore + +instance : EvalExpr Bool where + evalExpr := evalBoolExpr + expectedType? := toTypeExpr Bool + +instance : EvalExpr Nat where + evalExpr := evalNatExpr + expectedType? := toTypeExpr Nat + +instance : EvalExpr Int where + evalExpr := evalIntExpr + expectedType? := toTypeExpr Int + +instance : EvalExpr String where + evalExpr := evalStringExpr + expectedType? := toTypeExpr String + +instance : EvalExpr Name where + evalExpr := evalNameExpr + expectedType? := toTypeExpr Name + +instance {α : Type} [EvalExpr α] : EvalExpr (Option α) where + evalExpr := evalOptionExpr evalExpr + expectedType? := Expr.app (Expr.const ``Option [0]) <$> EvalExpr.expectedType? α + +instance {α : Type} [EvalExpr α] : EvalExpr (List α) where + evalExpr := evalListExpr evalExpr + expectedType? := Expr.app (Expr.const ``List [0]) <$> EvalExpr.expectedType? α + +instance {α : Type} [EvalExpr α] : EvalExpr (Array α) where + evalExpr := evalArrayExpr evalExpr + expectedType? := Expr.app (Expr.const ``Array [0]) <$> EvalExpr.expectedType? α + +instance : EvalExpr DataValue where + evalExpr := evalDataValueExpr + expectedType? := none -- don't want to elaborate with an expected type, since numeric literals will fail + +end EvalExpr + +end Lean.Elab.ConfigEval diff --git a/src/Lean/Elab/ConfigEval/MetaInstances.lean b/src/Lean/Elab/ConfigEval/MetaInstances.lean new file mode 100644 index 0000000000..9ab551fbd5 --- /dev/null +++ b/src/Lean/Elab/ConfigEval/MetaInstances.lean @@ -0,0 +1,29 @@ +/- +Copyright (c) 2026 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Kyle Miller +-/ +module + +prelude +public import Lean.Elab.ConfigEval.Commands +public import Lean.Elab.ConfigEval.Instances +public import Lean.Elab.DeprecatedSyntax -- shake: skip (workaround for command elaborators failing to interpret `deprecatedSyntaxExt`, to be fixed #13108) + +/-! +# Derived evaluator instances for built-in Meta types + +-/ + +public section + +namespace Lean.Elab.ConfigEval + +open Meta Term + +ensure_eval_term_expr_instances ApplyNewGoals +ensure_eval_term_expr_instances EtaStructMode +ensure_eval_term_expr_instances TransparencyMode +ensure_eval_term_expr_instances Occurrences + +end Lean.Elab.ConfigEval diff --git a/src/Lean/Elab/ConfigEval/Types.lean b/src/Lean/Elab/ConfigEval/Types.lean new file mode 100644 index 0000000000..d94bd8af15 --- /dev/null +++ b/src/Lean/Elab/ConfigEval/Types.lean @@ -0,0 +1,115 @@ +/- +Copyright (c) 2026 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Kyle Miller +-/ +module + +prelude +public import Lean.Elab.Term.TermElabM +public import Lean.Parser.Term + +/-! +# Types for configuration elaboration +-/ + +public section + +namespace Lean.Elab.ConfigEval + +open Term + +/-- +Class for evaluation of `Term` syntax directly to a runtime value. +-/ +class EvalTerm (α : Type) where + /-- + 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. + -/ + evalTerm : Term → TermElabM (α × Expr) + /-- + A type that can be used when constructing expression for the `TermInfo`. + -/ + typeExpr : Expr + +export EvalTerm (evalTerm) + +builtin_initialize unsupportedExprExceptionId : InternalExceptionId ← registerInternalExceptionId `ConfigEval.unsupportedExpr + +def throwUnsupportedExpr {m α} [MonadExceptOf Exception m] : m α := + throw <| Exception.internal unsupportedExprExceptionId + +/-- +Class for evaluation of an expression to a runtime value. +-/ +class EvalExpr (α : Type) where + /-- + 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. + -/ + evalExpr : Expr → MetaM α + /-- + 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. + -/ + expectedType? : Option Expr + +export EvalExpr (evalExpr) + +/-- +A view of a `Lean.Parser.Term.configItem`. +-/ +structure ConfigItem where + /-- Ref for the entire configuration item -/ + ref : Syntax + /-- Ref for the option name itself. -/ + option : Ident + /-- The configuration value. Usually this is a `Term`, but user-defined configuration items + can use arbitrary syntax. For `+`/`-` booleans, this syntax is synthetic. -/ + value : Syntax + /-- 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. -/ + bool? : Option Bool := none + /-- The original option name (without macro scopes), even after shifting. -/ + origOptionName : Name := option.getId.eraseMacroScopes + /-- 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. -/ + optionComps : List Syntax := Lean.Syntax.identComponents option + /-- Previous root components of `option` in reverse order, collecting results from `ConfigItem.shift`. -/ + prevOptionComps : List Syntax := [] + +/-- +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. +-/ +structure EvalConfigItem (α : Type) where + /-- + Evaluates setting the configuration item described by `item` in `config`. + -/ + set (config : α) (item : ConfigItem) : TermElabM α + +-- TODO +private structure ReflectConfigItems (α : Type) where + /-- + Given a configuration, produces an array of configuration items representing it. + -/ + reflect (config : α) : TermElabM (TSyntaxArray ``Parser.Term.configItem) + +end Lean.Elab.ConfigEval diff --git a/src/Lean/Elab/ConfigEval/Util.lean b/src/Lean/Elab/ConfigEval/Util.lean new file mode 100644 index 0000000000..f4418b7c72 --- /dev/null +++ b/src/Lean/Elab/ConfigEval/Util.lean @@ -0,0 +1,143 @@ +/- +Copyright (c) 2026 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Kyle Miller +-/ +module + +prelude +public import Lean.Elab.Command + +public section + +namespace Lean.Elab.ConfigEval + +open Meta Term Command + +/-- +Creates a decision tree to implement `match discr with $cases* | _ => onFail`, +where `discr : String`. +-/ +partial def makeStringMatcher (discr : Ident) (cases : Array (String × Term)) (onFail : Term) : + TermElabM Term := do + let cases := Array.qsort cases (fun c c' => c.1 < c'.1) + build 0 cases.size cases +where + build (start stop : Nat) (cases : Array (String × Term)) : TermElabM Term := do + if stop - start ≤ 5 then + -- Switch to if/else chains once we get to a small number of options. + cases[start:stop].foldrM (init := onFail) fun (s, body) res => + `(if $discr == $(quote s) then $body else $res) + else + let mid := (start + stop) / 2 + let (s, _) := cases[mid]! + let low ← build start mid cases + let high ← build mid stop cases + `(if $discr < $(quote s) then $low else $high) + +/-- +Returns a list of types that are are missing `cls` instances such that +implementing them would ensure a `cls type` instance. If there are no conditional +instances to support this, returns `#[type]`. If there's already a `cls type` instance, +returns `#[]`. + +Only supports one-parameter classes. + +For example, `planDerivation C t` where `t` is `Array t₁ × Option t₂` might return `#[t₁, t₂]` +if there are instances for `Array`, `Option`, and `Prod`, but not for `t₁` and `t₂`. + +The `extraDeps` function is called whenever a type cannot be satisfied by existing instances. +It should return an array of types that need an instance to be implemented for the implementation +of the instance to succeed. For example, a `structure` might report the list of the types of all +its fields. +-/ +private partial def planDerivation (className : Name) (type : Expr) + (extraDeps : Expr → TermElabM (Array Expr)) : + TermElabM (Array Expr) := do + withTraceNode `Elab.ConfigEval + (fun r => return m!"derivation plan `{.ofConstName className}` for `{type}`: " + ++ match r with | .ok types => m!"{types}" | .error ex => ex.toMessageData) do + go #[] {type} type +where + go (plan : Array Expr) (processing : ExprSet) (type : Expr) : TermElabM (Array Expr) := withIncRecDepth do + trace[Elab.ConfigEval] "plan: {plan}, processing: {processing.toList}, type: {type}" + if plan.contains type then + return plan + else + let cls ← mkAppM className #[type] + let insts ← SynthInstance.getInstances cls + trace[Elab.ConfigEval] "num insts for `{cls}`: {insts.size}" + for inst in insts do + try + return ← tryInst plan processing cls inst + catch _ => pure () + let depTypes ← extraDeps type + trace[Elab.ConfigEval] "extra deps for `{type}`: {depTypes}" + let plan ← useDepTypes plan processing depTypes + return plan.push type + tryInst (plan : Array Expr) (processing : ExprSet) (cls : Expr) (inst : SynthInstance.Instance) : + TermElabM (Array Expr) := do + trace[Elab.ConfigEval] "tryInst {cls}" + let (xs, bis, cls') ← forallMetaTelescopeReducing (← inferType inst.val) + trace[Elab.ConfigEval] "inst: {xs}, {cls'}" + guard <| ← isDefEq cls cls' + let mut depTypes := #[] -- types that need instances of the class + -- Analyze instance arguments; fail if instances not of the class can't be synthesized + for i in inst.synthOrder do + let x := xs[i]! + let depCls ← instantiateMVars (← whnf (← inferType x)) + if depCls.isAppOfArity className 1 then -- foralls not supported + let depType := depCls.appArg! + depTypes := depTypes.push depType + else + guard <| ← synthesizeInstMVarCore x.mvarId! + -- Ensure everything's been solved for but the instances + for h : i in [0:xs.size] do + unless inst.synthOrder.contains i do + let x ← instantiateMVars xs[i] + guard <| !x.hasMVar + trace[Elab.ConfigEval] "inst for `{cls}` deps: {depTypes}" + useDepTypes plan processing depTypes + useDepTypes (plan : Array Expr) (processing : ExprSet) (depTypes : Array Expr) : TermElabM (Array Expr) := do + let depTypes ← depTypes.mapM instantiateMVars + if let some depType := depTypes.find? (·.hasMVar) then + throwError "dependency has metavariables: {depType}" + -- Filter out those instances that are part of the derivation plan + let depTypes := depTypes.filter (!plan.contains ·) + -- If any are currently being processed, then we have a cyclic dependency. + if let some depType := depTypes.find? processing.contains then + throwError "cyclic dependency on {depType}" + let mut plan := plan + for depType in depTypes do + plan ← go plan (processing.insert depType) depType + return plan + +/-- +Helper for deriving instances along with all dependencies. +Given a one-parameter class `className` and a type `type`, +uses pre-existing conditional instances to figure out which types would +suffice to be implemented, then runs `mkCmd` on each type with fresh macro scopes. + +The commands are generated and elaborated one at a time. +-/ +def withClassInstDeps (className : Name) (type : Expr) + (extraDeps : Expr → TermElabM (Array Expr)) + (mkCmd : Expr → TermElabM Command) : + CommandElabM Unit := do + let types ← liftTermElabM <| planDerivation className type extraDeps + let env ← getEnv + for type' in types do + let cmd ← liftTermElabM do + try + withFreshMacroScope (mkCmd type') + catch ex => + trace[Elab.ConfigEval] m!"failure deriving instance for `{type'}`: {ex.toMessageData}" + setEnv env + throw ex + elabCommand cmd + trace[Elab.ConfigEval] m!"added instance of {.ofConstName className} for `{type'}`" + +builtin_initialize + registerTraceClass `Elab.ConfigEval + +end Lean.Elab.ConfigEval diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/Attr.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/Attr.lean index a80919f81a..1c63dd57b1 100644 --- a/src/Lean/Elab/Tactic/BVDecide/Frontend/Attr.lean +++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/Attr.lean @@ -8,6 +8,7 @@ module prelude public import Lean.Elab.Tactic.Simp public import Std.Tactic.BVDecide.Syntax +import Lean.Elab.ConfigEval public section diff --git a/src/Lean/Elab/Tactic/Config.lean b/src/Lean/Elab/Tactic/Config.lean index 8decf5bfb1..11e9977d9b 100644 --- a/src/Lean/Elab/Tactic/Config.lean +++ b/src/Lean/Elab/Tactic/Config.lean @@ -6,10 +6,29 @@ Authors: Leonardo de Moura, Kyle Miller module prelude -public import Lean.Meta.Eval -public import Lean.Elab.SyntheticMVars +public import Lean.Elab.ConfigEval import Lean.Linter.MissingDocs +/-! +# Legacy tactic configuration elaboration + +This module exists for reverse compatibility — users should import `Lean.Elab.ConfigEval` directly. +It has been deprecated since 2026-05-14 and will be removed. + +The new `declare_config_elab` and `declare_command_config_elab` commands are generally drop-in +replacements for the legacy ones. + +Migration notes: +- You may need to add a `where except field1, field2, ...` clause to omit things like function + fields that do not have expression interpreters (e.g. `Lean.Elab.Tactic.SolveByElim.elabConfig`) +- You may choose to use `derive_eval_expr_instance_using_meta_eval` to derive a `Meta.evalTerm'`-based + expression evaluator for one or more fields, or for the configuration structure itself to support + the `(config := ...)` option, replicating the technique used in this module. + Note that these instances are slow. +- If all else fails, until this module is removed there are the + `declare_config_elab_legacy` and `declare_command_config_elab_legacy` commands. +-/ + public section namespace Lean.Elab.Tactic @@ -64,7 +83,7 @@ private partial def expandField (structName : Name) (field : Name) : MetaM (Name return (field' ++ field'', projFn) /-- Elaborates a tactic configuration. -/ -def elabConfig (recover : Bool) (structName : Name) (items : Array ConfigItemView) : TermElabM Expr := +def elabConfig (recover : Bool) (structName : Name) (items : Array ConfigItemView) : TermElabM Expr := do withoutModifyingStateWithInfoAndMessages <| withLCtx {} {} <| withSaveInfoContext do let mkStructInst (source? : Option Term) (fields : TSyntaxArray ``Parser.Term.structInstField) : TermElabM Term := match source? with @@ -161,8 +180,8 @@ private meta def mkConfigElaborator end -/-! -`declare_config_elab elabName TypeName` declares a function `elabName : Syntax → TacticM TypeName` +/-- +`declare_config_elab_legacy elabName TypeName` declares a function `elabName : Syntax → TacticM TypeName` that elaborates a tactic configuration. The tactic configuration can be from `Lean.Parser.Tactic.optConfig` or `Lean.Parser.Tactic.config`, and these can also be wrapped in null nodes (for example, from `(config)?`). @@ -170,23 +189,27 @@ and these can also be wrapped in null nodes (for example, from `(config)?`). The elaborator responds to the current recovery state. For defining elaborators for commands, use `declare_command_config_elab`. + +This command has been deprecated since 2026-05-14. Use `declare_config_elab` instead. -/ -macro (name := configElab) doc?:(docComment)? "declare_config_elab" elabName:ident type:ident : command => do +macro (name := configElab) doc?:(docComment)? "declare_config_elab_legacy" elabName:ident type:ident : command => do mkConfigElaborator doc? elabName type (mkCIdent ``TacticM) (mkCIdent ``id) (← `((← read).recover)) open Linter.MissingDocs in @[builtin_missing_docs_handler Elab.Tactic.configElab] private def checkConfigElab : SimpleHandler := mkSimpleHandler "config elab" -/-! -`declare_command_config_elab elabName TypeName` declares a function `elabName : Syntax → CommandElabM TypeName` +/-- +`declare_command_config_elab_legacy elabName TypeName` declares a function `elabName : Syntax → CommandElabM TypeName` that elaborates a command configuration. The configuration can be from `Lean.Parser.Tactic.optConfig` or `Lean.Parser.Tactic.config`, and these can also be wrapped in null nodes (for example, from `(config)?`). The elaborator has error recovery enabled. + +This command has been deprecated since 2026-05-14. Use `declare_command_config_elab` instead. -/ -macro (name := commandConfigElab) doc?:(docComment)? "declare_command_config_elab" elabName:ident type:ident : command => do +macro (name := commandConfigElab) doc?:(docComment)? "declare_command_config_elab_legacy" elabName:ident type:ident : command => do mkConfigElaborator doc? elabName type (mkCIdent ``CommandElabM) (mkCIdent ``liftTermElabM) (mkCIdent ``true) open Linter.MissingDocs in diff --git a/src/Lean/Elab/Tactic/ConfigSetter.lean b/src/Lean/Elab/Tactic/ConfigSetter.lean deleted file mode 100644 index ffea511e8d..0000000000 --- a/src/Lean/Elab/Tactic/ConfigSetter.lean +++ /dev/null @@ -1,72 +0,0 @@ -/- -Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Leonardo de Moura --/ -module -prelude -public import Lean.Elab.Command -public meta import Lean.Elab.Command -public section -namespace Lean.Elab -open Command Meta - --- We automatically disable the following option for `macro`s but the subsequent `def` both contains --- a quotation and is called only by `macro`s, so we disable the option for it manually. Note that --- we can't use `in` as it is parsed as a single command and so the option would not influence the --- parser. -set_option internal.parseQuotWithCurrentStage false - -/-- -Generates a function `setterName` for updating the `Bool` and `Nat` fields -of the structure `struct`. -This is a very simple implementation. There is no support for subobjects. --/ -meta def mkConfigSetter (doc? : Option (TSyntax ``Parser.Command.docComment)) - (setterName struct : Ident) : CommandElabM Unit := do - let structName ← resolveGlobalConstNoOverload struct - let .inductInfo val ← getConstInfo structName - | throwErrorAt struct "`{structName}` is not s structure" - unless val.levelParams.isEmpty do - throwErrorAt struct "`{structName}` is universe polymorphic" - unless val.numIndices == 0 && val.numParams == 0 do - throwErrorAt struct "`{structName}` must not be parametric" - let env ← getEnv - let some structInfo := getStructureInfo? env structName - | throwErrorAt struct "`{structName}` is not a structure" - let code : Term ← liftTermElabM do - let mut code : Term ← `(throwError "invalid configuration option `{fieldName}`") - for fieldInfo in structInfo.fieldInfo do - if fieldInfo.subobject?.isSome then continue -- ignore subobject's - let projInfo ← getConstInfo fieldInfo.projFn - let fieldType ← forallTelescope projInfo.type fun _ body => pure body - -- **Note**: We only support `Nat` and `Bool` fields - let fieldIdent : Ident := mkCIdent fieldInfo.fieldName - if fieldType.isConstOf ``Nat then - code ← `(if fieldName == $(quote fieldInfo.fieldName) then do - Term.addTermInfo' (← getRef) (← mkConstWithLevelParams $(quote fieldInfo.projFn)) - return { s with $fieldIdent:ident := (← getNatField) } - else $code) - else if fieldType.isConstOf ``Bool then - code ← `(if fieldName == $(quote fieldInfo.fieldName) then do - Term.addTermInfo' (← getRef) (← mkConstWithLevelParams $(quote fieldInfo.projFn)) - return { s with $fieldIdent:ident := (← getBoolField) } - else $code) - return code - let cmd ← `(command| - $[$doc?:docComment]? - def $setterName (s : $struct) (fieldName : Name) (val : DataValue) : TermElabM $struct := - let getBoolField : TermElabM Bool := do - let .ofBool b := val | throwError "`{fieldName}` is a Boolean" - return b - let getNatField : TermElabM Nat := do - let .ofNat n := val | throwError "`{fieldName}` is a natural number" - return n - $code - ) - elabCommand cmd - -elab (name := elabConfigGetter) doc?:(docComment)? "declare_config_getter" setterName:ident type:ident : command => do - mkConfigSetter doc? setterName type - -end Lean.Elab diff --git a/src/Lean/Elab/Tactic/Decide.lean b/src/Lean/Elab/Tactic/Decide.lean index bcdd0f0507..aa99499ca9 100644 --- a/src/Lean/Elab/Tactic/Decide.lean +++ b/src/Lean/Elab/Tactic/Decide.lean @@ -10,6 +10,7 @@ public import Lean.Elab.Tactic.Basic public import Lean.Meta.Tactic.Cleanup import Lean.Meta.Native import Lean.Elab.Tactic.ElabTerm +import Lean.Elab.ConfigEval public section diff --git a/src/Lean/Elab/Tactic/Do/VCGen/Basic.lean b/src/Lean/Elab/Tactic/Do/VCGen/Basic.lean index 640fbfeb47..65a96e4cf9 100644 --- a/src/Lean/Elab/Tactic/Do/VCGen/Basic.lean +++ b/src/Lean/Elab/Tactic/Do/VCGen/Basic.lean @@ -9,6 +9,7 @@ prelude public import Lean.Elab.Tactic.Simp public import Lean.Elab.Tactic.Do.Attr import Init.Omega +import Lean.Elab.ConfigEval public section diff --git a/src/Lean/Elab/Tactic/ElabTerm.lean b/src/Lean/Elab/Tactic/ElabTerm.lean index 1a986cfdc0..bffcd08d24 100644 --- a/src/Lean/Elab/Tactic/ElabTerm.lean +++ b/src/Lean/Elab/Tactic/ElabTerm.lean @@ -9,7 +9,8 @@ prelude public import Lean.Meta.Tactic.Constructor public import Lean.Meta.Tactic.Replace public import Lean.Meta.Tactic.Rename -public import Lean.Elab.Tactic.Config +public import Lean.Elab.Tactic.Basic +public import Lean.Elab.SyntheticMVars public section diff --git a/src/Lean/Elab/Tactic/Grind/Config.lean b/src/Lean/Elab/Tactic/Grind/Config.lean index 6d1ca45c2f..df2ed3fbb4 100644 --- a/src/Lean/Elab/Tactic/Grind/Config.lean +++ b/src/Lean/Elab/Tactic/Grind/Config.lean @@ -6,32 +6,53 @@ Authors: Leonardo de Moura module prelude public import Lean.Elab.Tactic.Grind.Basic -import Lean.Elab.Tactic.ConfigSetter -import Lean.Elab.DeprecatedSyntax -- shake: skip (workaround for `mkConfigSetter` failing to interpret `deprecatedSyntaxExt`, to be fixed) +import Lean.Elab.ConfigEval public section -namespace Lean.Elab.Tactic.Grind +namespace Lean.Elab.Tactic -/-- Sets a field of the `grind` configuration object. -/ -declare_config_getter setConfigField Grind.Config +open ConfigEval -def elabConfigItems (init : Grind.Config) (items : Array (TSyntax `Lean.Parser.Tactic.configItem)) - : TermElabM Grind.Config := do - let mut config := init - for item in items do - match item with - | `(Lean.Parser.Tactic.configItem| ($fieldName:ident := true)) - | `(Lean.Parser.Tactic.configItem| +$fieldName:ident) => - config ← withRef fieldName <| setConfigField config fieldName.getId true - | `(Lean.Parser.Tactic.configItem| ($fieldName:ident := false)) - | `(Lean.Parser.Tactic.configItem| -$fieldName:ident) => - config ← withRef fieldName <| setConfigField config fieldName.getId false - | `(Lean.Parser.Tactic.configItem| ($fieldName:ident := $val:num)) => - config ← withRef fieldName <| setConfigField config fieldName.getId (.ofNat val.getNat) - | _ => throwErrorAt item "unexpected configuration option" - return config +/-- +Elaborator for grind configurations, with the `(config := ...)` elaborator exposed. +This allows overriding which structure is used as the expected type when elaborating +the term, which affects which default values are used in `{...}` structure instance notation. +-/ +private declare_term_config_elab elabGrindConfigCore Grind.Config + (evalConfig : Term → TermElabM Grind.Config) where + option config := fun _ item => evalConfig ⟨item.value⟩ -def withConfigItems (items : Array (TSyntax `Lean.Parser.Tactic.configItem)) +local macro "make_elab_grind_config" fn:ident struct:ident : command => do + let cfg := mkIdent `cfg + let init := mkIdent `init + let logExceptions := mkIdent `logExceptions + `(private local ensure_eval_expr_instance $struct + def $fn ($cfg : Syntax) + ($init : $struct := {}) + ($logExceptions : Bool := true) : + TacticM Grind.Config := do + elabGrindConfigCore $cfg { $init with } + (evalConfig := fun c => do + let cfg : $struct ← evalExprWithElab c + return { cfg with }) + (logExceptions := $logExceptions && (← read).recover)) + +make_elab_grind_config elabGrindConfig Grind.Config +make_elab_grind_config elabGrindConfigInteractive Grind.ConfigInteractive +make_elab_grind_config elabCutsatConfig Grind.CutsatConfig +make_elab_grind_config elabLinarithConfig Grind.LinarithConfig +make_elab_grind_config elabOrderConfig Grind.OrderConfig +make_elab_grind_config elabGrobnerConfig Grind.GrobnerConfig + +namespace Grind + +def elabConfigItems (init : Grind.Config) (items : Array Syntax) : + TermElabM Grind.Config := do + elabGrindConfigCore (mkNullNode items) init + (evalConfig := fun c => evalExprWithElab c) + (logExceptions := false) + +def withConfigItems (items : Array Syntax) (k : GrindTacticM α) : GrindTacticM α := do if items.isEmpty then k diff --git a/src/Lean/Elab/Tactic/Grind/Main.lean b/src/Lean/Elab/Tactic/Grind/Main.lean index ed3e9d3c5f..f22dcc3a3f 100644 --- a/src/Lean/Elab/Tactic/Grind/Main.lean +++ b/src/Lean/Elab/Tactic/Grind/Main.lean @@ -7,7 +7,7 @@ module prelude public import Lean.Meta.Tactic.Grind.Main public import Lean.Meta.Tactic.TryThis -public import Lean.Elab.Tactic.Config +public import Lean.Elab.Tactic.Grind.Config public import Lean.LibrarySuggestions.Basic import Lean.Meta.Tactic.Grind.SimpUtil import Lean.Elab.Tactic.Grind.Param @@ -17,12 +17,6 @@ import Lean.Meta.Tactic.Grind.Parser public section namespace Lean.Elab.Tactic open Meta -declare_config_elab elabGrindConfig Grind.Config -declare_config_elab elabGrindConfigInteractive Grind.ConfigInteractive -declare_config_elab elabCutsatConfig Grind.CutsatConfig -declare_config_elab elabLinarithConfig Grind.LinarithConfig -declare_config_elab elabOrderConfig Grind.OrderConfig -declare_config_elab elabGrobnerConfig Grind.GrobnerConfig open Command Term in open Lean.Parser.Command.GrindCnstr in @@ -334,7 +328,7 @@ def filterSuggestionsAndLocalsFromGrindConfig (config : TSyntax ``Lean.Parser.Ta private def elabGrindConfig' (config : TSyntax ``Lean.Parser.Tactic.optConfig) (interactive : Bool) : TacticM Grind.Config := do if interactive then - return (← elabGrindConfigInteractive config).toConfig + elabGrindConfigInteractive config else elabGrindConfig config diff --git a/src/Lean/Elab/Tactic/Lets.lean b/src/Lean/Elab/Tactic/Lets.lean index f5b03aacf3..edc65e1c01 100644 --- a/src/Lean/Elab/Tactic/Lets.lean +++ b/src/Lean/Elab/Tactic/Lets.lean @@ -10,6 +10,7 @@ public import Lean.Meta.Tactic.Lets public import Lean.Elab.Tactic.Location import Lean.Elab.Binders import Lean.Linter.Init +import Lean.Elab.ConfigEval public section diff --git a/src/Lean/Elab/Tactic/LibrarySearch.lean b/src/Lean/Elab/Tactic/LibrarySearch.lean index 15ae885372..17e947a432 100644 --- a/src/Lean/Elab/Tactic/LibrarySearch.lean +++ b/src/Lean/Elab/Tactic/LibrarySearch.lean @@ -9,6 +9,7 @@ prelude public import Lean.Meta.Tactic.LibrarySearch public import Lean.Meta.Tactic.TryThis public import Lean.Elab.Tactic.ElabTerm +import Lean.Elab.ConfigEval public section diff --git a/src/Lean/Elab/Tactic/NormCast.lean b/src/Lean/Elab/Tactic/NormCast.lean index ca68a1f6ea..a2dfa2b9cb 100644 --- a/src/Lean/Elab/Tactic/NormCast.lean +++ b/src/Lean/Elab/Tactic/NormCast.lean @@ -8,6 +8,7 @@ module prelude public import Lean.Meta.Tactic.NormCast public import Lean.Elab.Tactic.Conv.Simp +import Lean.Elab.ConfigEval public section diff --git a/src/Lean/Elab/Tactic/Omega/Frontend.lean b/src/Lean/Elab/Tactic/Omega/Frontend.lean index 1c807cc35b..3c1a7aabf2 100644 --- a/src/Lean/Elab/Tactic/Omega/Frontend.lean +++ b/src/Lean/Elab/Tactic/Omega/Frontend.lean @@ -8,7 +8,7 @@ module prelude public import Lean.Elab.Tactic.Omega.Core public import Lean.Elab.Tactic.FalseOrByContra -public import Lean.Elab.Tactic.Config +import Lean.Elab.ConfigEval public import Lean.Meta.Tactic.Simp.Attr import Lean.Elab.Tactic.BuiltinTactic import Init.Data.Int.Pow diff --git a/src/Lean/Elab/Tactic/Rewrite.lean b/src/Lean/Elab/Tactic/Rewrite.lean index 03ee156974..1b3cfa8902 100644 --- a/src/Lean/Elab/Tactic/Rewrite.lean +++ b/src/Lean/Elab/Tactic/Rewrite.lean @@ -9,6 +9,7 @@ prelude public import Lean.Meta.Tactic.Rewrite public import Lean.Meta.Tactic.Replace public import Lean.Elab.Tactic.Location +import Lean.Elab.ConfigEval import Lean.Meta.Eqns public section diff --git a/src/Lean/Elab/Tactic/Simp.lean b/src/Lean/Elab/Tactic/Simp.lean index 60d27077c2..cf28d89371 100644 --- a/src/Lean/Elab/Tactic/Simp.lean +++ b/src/Lean/Elab/Tactic/Simp.lean @@ -11,16 +11,117 @@ public import Lean.Meta.Tactic.Simp.LoopProtection public import Lean.Elab.BuiltinNotation public import Lean.Elab.Tactic.Location import Lean.Meta.Check +import Lean.Elab.ConfigEval public section -namespace Lean.Elab.Tactic +namespace Lean + +/-- +Configuration for `simp`, for supporting tactic configuration option syntax. +-/ +structure Meta.Simp.ConfigWithOptions extends config : Meta.Simp.Config where + /-- User options. Registering a global option `tactic.simp.user.myOption` enables the tactic + configurations `(user.myOption := ...)` and `+user.myOption`. -/ + userConfig : Options := {} + +/-- +Configuration for `dsimp`, for supporting tactic configuration option syntax. +-/ +structure Meta.DSimp.ConfigWithOptions extends config : Meta.DSimp.Config where + /-- User options. Registering a global option `tactic.simp.user.myOption` enables the tactic + configurations `(user.myOption := ...)` and `+user.myOption`. -/ + userConfig : Options := {} + +namespace Elab.Tactic open Meta open TSyntax.Compat -declare_config_elab elabSimpConfigCore Meta.Simp.Config -declare_config_elab elabSimpConfigCtxCore Meta.Simp.ConfigCtx -declare_config_elab elabDSimpConfigCore Meta.DSimp.Config +section +open ConfigEval + +/-- +Generic `simp` configuration elaborator, with an `evalConfig` argument for overriding how +the `(config := ...)` syntax is elaborated. +-/ +private declare_config_elab elabSimpConfigAux Simp.ConfigWithOptions (evalConfig : Term → TermElabM Meta.Simp.Config) where + omit userConfig + option config := fun cfg item => do + let config ← evalConfig item.value + return { cfg with config } + option user := fun _ item => do + item.addConstInfo ``Simp.ConfigWithOptions.userConfig + throwErrorAt item.root "User options are of the form `user.optionName`" + option user.* := fun cfg item => do + item.addConstInfo ``Simp.ConfigWithOptions.userConfig + let userConfig ← EvalConfigItem.evalSetOptions `tactic.simp.user cfg.userConfig item.shift + return { cfg with userConfig } + option userConfig := fun _ item => do + item.addConstInfo ``Simp.ConfigWithOptions.userConfig + throwErrorAt item.root "Cannot set `userConfig` directly. User options are of the form `user.optionName`" + +/-- +Specializes the `elabSimpConfigAux` configuration elaborator to a specific `Simp` default configuration. +This is necessary for `(config := {...})` to elaborate the `{...}` expression with the correct expected type. +-/ +local macro "make_elab_simp_config" fn:ident struct:ident : command => do + let optConfig := mkIdent `optConfig + let initConfig := mkIdent `initConfig + let initUserConfig := mkIdent `initUserConfig + `(private local ensure_eval_expr_instance $struct + def $fn ($optConfig : Syntax) + ($initConfig : $struct := {}) ($initUserConfig : Options := {}) : + TacticM Simp.ConfigWithOptions := do + elabSimpConfigAux $optConfig { $initConfig with userConfig := $initUserConfig } + (evalConfig := fun c => do + let config : $struct ← evalExprWithElab c + return { config with })) + +make_elab_simp_config elabSimpConfigCore Simp.Config +make_elab_simp_config elabSimpConfigCtxCore Simp.ConfigCtx + +private local ensure_eval_expr_instance DSimp.Config + +/-- Elaborates a `dsimp` configuration, which uses only a subset of the options +of a `simp` configuration. The `elabSimpConfig` function calls this and immediately +converts the result to a `Simp.Config`. -/ +private declare_config_elab elabDSimpConfigCore DSimp.ConfigWithOptions where + omit userConfig + option config := fun cfg item => do + let config : DSimp.Config ← evalExprWithElab item.value + return { cfg with config } + option user := fun _ item => do + item.addConstInfo ``DSimp.ConfigWithOptions.userConfig + throwErrorAt item.root "User options are of the form `user.optionName`" + option user.* := fun cfg item => do + item.addConstInfo ``DSimp.ConfigWithOptions.userConfig + let userConfig ← EvalConfigItem.evalSetOptions `tactic.simp.user cfg.userConfig item.shift + return { cfg with userConfig } + option userConfig := fun _ item => do + item.addConstInfo ``DSimp.ConfigWithOptions.userConfig + throwErrorAt item.root "Cannot set `userConfig` directly. User options are of the form `user.optionName`" + +end + +register_builtin_option tactic.simp.user.exampleBool : Bool := { + defValue := false + descr := "(simp user option) example Bool-valued option, for testing" +} + +register_builtin_option tactic.simp.user.exampleNat : Nat := { + defValue := 0 + descr := "(simp user option) example Nat-valued option, for testing" +} + +register_builtin_option tactic.simp.user.exampleInt : Int := { + defValue := 0 + descr := "(simp user option) example Int-valued option, for testing" +} + +register_builtin_option tactic.simp.user.exampleString : String := { + defValue := "" + descr := "(simp user option) example String-valued option, for testing" +} inductive SimpKind where | simp @@ -85,12 +186,12 @@ private def mkDischargeWrapper (optDischargeSyntax : Syntax) : TacticM Simp.Disc return Simp.DischargeWrapper.custom ref d /- - `optConfig` is of the form `("(" "config" ":=" term ")")?` + `optConfig` is `Lean.Parser.Tactic.optConfig` -/ -def elabSimpConfig (optConfig : Syntax) (kind : SimpKind) : TacticM Meta.Simp.Config := do +def elabSimpConfig (optConfig : Syntax) (kind : SimpKind) : TacticM Simp.ConfigWithOptions := do match kind with | .simp => elabSimpConfigCore optConfig - | .simpAll => pure (← elabSimpConfigCtxCore optConfig).toConfig + | .simpAll => elabSimpConfigCtxCore optConfig | .dsimp => pure { (← elabDSimpConfigCore optConfig) with } inductive ResolveSimpIdResult where @@ -466,12 +567,13 @@ def mkSimpContext (stx : Syntax) (eraseLocal : Bool) (kind := SimpKind.simp) simpTheorems let simprocs ← if simpOnly then pure {} else Simp.getSimprocs let congrTheorems ← getSimpCongrTheorems - let config ← elabSimpConfig stx[1] (kind := kind) + let { config, userConfig } ← elabSimpConfig stx[1] (kind := kind) -- Add local definitions if +locals is enabled if config.locals then simpTheorems ← elabSimpLocals simpTheorems kind let ctx ← Simp.mkContext (config := config) + (userConfig := userConfig) (simpTheorems := #[simpTheorems]) congrTheorems let r ← elabSimpArgs stx[4] (eraseLocal := eraseLocal) (kind := kind) (simprocs := #[simprocs]) (ignoreStarArg := ignoreStarArg) ctx diff --git a/src/Lean/Elab/Tactic/SolveByElim.lean b/src/Lean/Elab/Tactic/SolveByElim.lean index 4d574f1deb..8ea60a6e37 100644 --- a/src/Lean/Elab/Tactic/SolveByElim.lean +++ b/src/Lean/Elab/Tactic/SolveByElim.lean @@ -7,8 +7,8 @@ module prelude public import Lean.Meta.Tactic.SolveByElim -public import Lean.Elab.Tactic.Config public import Lean.LibrarySuggestions.Basic +import Lean.Elab.ConfigEval public section @@ -22,13 +22,21 @@ open Lean.Meta.SolveByElim (SolveByElimConfig mkAssumptionSet) /-- Allow elaboration of `Config` arguments to tactics. + +Note: does not generate a `(config := ...)` option due to the fields in the `omit` +clause, which are all function-valued and have no `EvalExpr` instances. -/ -declare_config_elab elabConfig Lean.Meta.SolveByElim.SolveByElimConfig +declare_config_elab elabConfig Lean.Meta.SolveByElim.SolveByElimConfig where + omit proc, suspend, discharge /-- Allow elaboration of `ApplyRulesConfig` arguments to tactics. + +Note: does not generate a `(config := ...)` option due to the fields in the `omit` +clause, which are all function-valued and have no `EvalExpr` instances. -/ -declare_config_elab elabApplyRulesConfig Lean.Meta.SolveByElim.ApplyRulesConfig +declare_config_elab elabApplyRulesConfig Lean.Meta.SolveByElim.ApplyRulesConfig where + omit proc, suspend, discharge /-- Parse the lemma argument of a call to `solve_by_elim`. @@ -76,7 +84,7 @@ def evalApplyAssumption : Tactic := fun stx => | `(tactic| apply_assumption $cfg:optConfig $[only%$o]? $[$t:args]? $[$use:using_]?) => do let (star, add, remove) := parseArgs t let use := parseUsing use - let cfg ← elabConfig (mkOptionalNode cfg) + let cfg ← elabConfig cfg let cfg := { cfg with backtracking := false maxDepth := 1 } @@ -94,7 +102,7 @@ def evalApplyRules : Tactic := fun stx => | `(tactic| apply_rules $cfg:optConfig $[only%$o]? $[$t:args]? $[$use:using_]?) => do let (star, add, remove) := parseArgs t let use := parseUsing use - let cfg ← elabApplyRulesConfig (mkOptionalNode cfg) + let cfg ← elabApplyRulesConfig cfg let cfg := { cfg with backtracking := false } liftMetaTactic fun g => processSyntax cfg o.isSome star add remove use [g] | _ => throwUnsupportedSyntax diff --git a/src/Lean/Elab/Tactic/Try.lean b/src/Lean/Elab/Tactic/Try.lean index af3d5a2804..950c0480d4 100644 --- a/src/Lean/Elab/Tactic/Try.lean +++ b/src/Lean/Elab/Tactic/Try.lean @@ -14,6 +14,7 @@ public import Lean.Elab.Parallel public meta import Lean.Elab.Command import Lean.Elab.BuiltinTerm import Init.Omega +import Lean.Elab.ConfigEval public section namespace Lean.Elab.Tactic open Meta diff --git a/src/Lean/Meta/Tactic/Simp/Types.lean b/src/Lean/Meta/Tactic/Simp/Types.lean index 4252b15eba..2b459d3f87 100644 --- a/src/Lean/Meta/Tactic/Simp/Types.lean +++ b/src/Lean/Meta/Tactic/Simp/Types.lean @@ -61,6 +61,9 @@ abbrev CongrCache := ExprMap (Option CongrTheorem) structure Context where private mk :: config : Config := {} + /-- User-extensible configuration. Tactic options of the form `(user.optName := ...)` + set keys `tactic.simp.user.optName`, if there is a global option named `tactic.simp.user.optName`. -/ + userConfig : Options := {} /-- Local declarations to propagate to `Meta.Context` -/ zetaDeltaSet : FVarIdSet := {} /-- @@ -170,11 +173,11 @@ private def mkMetaConfig (c : Config) : MetaM ConfigWithKey := do transparency := .reducible : Meta.Config }.toConfigWithKey -def mkContext (config : Config := {}) (simpTheorems : SimpTheoremsArray := {}) (congrTheorems : SimpCongrTheorems := {}) : MetaM Context := do +def mkContext (config : Config := {}) (simpTheorems : SimpTheoremsArray := {}) (congrTheorems : SimpCongrTheorems := {}) (userConfig : Options := {}) : MetaM Context := do let config ← updateArith config let config ← if backward.dsimp.instances.get (← getOptions) then pure { config with instances := true } else pure config return { - config, simpTheorems, congrTheorems + config, userConfig, simpTheorems, congrTheorems metaConfig := (← mkMetaConfig config) indexConfig := (← mkIndexConfig config) } @@ -464,6 +467,19 @@ def post (e : Expr) : SimpM Step := do def getConfig : SimpM Config := return (← getContext).config +@[inline] +def getUserConfig : SimpM Options := + return (← getContext).userConfig + +def getUserConfigOption [KVMap.Value α] (opt : Lean.Option α) : SimpM α := do + if let some v := (← getUserConfig).get? opt.name then + return v + else + return Lean.Option.get (← getOptions) opt + +@[inline] def withUserConfig (f : Options → Options) : SimpM α → SimpM α := + withTheReader Context (fun ctx => { ctx with userConfig := f ctx.userConfig}) + @[inline] def withParent (parent : Expr) (f : SimpM α) : SimpM α := withTheReader Context (fun ctx => { ctx with parent? := parent }) f diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean index 4d1645205c..e6107d0317 100644 --- a/src/Lean/Parser/Term.lean +++ b/src/Lean/Parser/Term.lean @@ -409,6 +409,31 @@ existent in the current context, or else fails. @[builtin_term_parser] def doubleQuotedName := leading_parser "`" >> checkNoWsBefore >> rawCh '`' (trailingWs := false) >> ident +/-- +`+opt` is short for `(opt := true)`. It sets the `opt` configuration option to `true`. +-/ +def posConfigItem := leading_parser + " +" >> checkNoWsBefore >> ident +/-- +`-opt` is short for `(opt := false)`. It sets the `opt` configuration option to `false`. +-/ +def negConfigItem := leading_parser + " -" >> checkNoWsBefore >> ident +/-- +`(opt := val)` sets the `opt` configuration option to `val`. + +As a special case, `(config := ...)` sets the entire configuration. +-/ +def valConfigItem := leading_parser + atomic (" (" >> ident >> " := ") >> withoutPosition termParser >> ")" +/-- A configuration item. -/ +def configItem := leading_parser + posConfigItem <|> negConfigItem <|> valConfigItem +/-- Configuration options for tactics, commands, and other elaborators. -/ +@[run_builtin_parser_attribute_hooks] +def optConfig := leading_parser + many (checkColGt >> configItem) + def letId := leading_parser (withAnonymousAntiquot := false) (ppSpace >> binderIdent >> notFollowedBy (checkNoWsBefore "" >> "[") "space is required before instance '[...]' binders to distinguish them from array updates `let x[i] := e; ...`") @@ -1106,6 +1131,7 @@ builtin_initialize register_parser_alias attrKind register_parser_alias optSemicolon register_parser_alias structInstFields + register_parser_alias optConfig end Parser end Lean diff --git a/tests/bench/mvcgen/sym/lib/Driver.lean b/tests/bench/mvcgen/sym/lib/Driver.lean index 13ad38f6d9..df725c9801 100644 --- a/tests/bench/mvcgen/sym/lib/Driver.lean +++ b/tests/bench/mvcgen/sym/lib/Driver.lean @@ -69,6 +69,7 @@ For many benchmarks, this is `[step, loop]`. -/ public def runBenchUsingTactic (goal : Name) (unfold : List Name) (solve : MetaM (TSyntax `tactic)) (discharge : MetaM (TSyntax `tactic)) (sizes : List Nat) : MetaM Unit := do for n in sizes do + resetCache solveUsingTactic goal unfold n solve discharge def solveUsingSym (goal : Name) (unfold : List Name) (n : Nat) (solve : MVarId → SymM (List MVarId)) (discharge : MetaM (TSyntax `tactic)) : MetaM Unit := do @@ -81,4 +82,5 @@ For many benchmarks, this is `[step, loop]`. -/ public def runBenchUsingSym (goal : Name) (unfold : List Name) (solve : MVarId → SymM (List MVarId)) (discharge : MetaM (TSyntax `tactic)) (sizes : List Nat) : MetaM Unit := do for n in sizes do + resetCache solveUsingSym goal unfold n solve discharge diff --git a/tests/elab/config_eval.lean b/tests/elab/config_eval.lean new file mode 100644 index 0000000000..dd27580285 --- /dev/null +++ b/tests/elab/config_eval.lean @@ -0,0 +1,170 @@ +import Lean.Elab.ConfigEval + +/-! +# Tests of `ConfigEval` configuration evaluation system +-/ + +open Lean Elab + +/-! +Set up some configuration objects, and then derive some configuration elaborators for each monad. +We're testing inductive variants, parent structures, and embedded structures. +-/ + +inductive TransparencyMode where + | default + | all + | none + deriving ToExpr + +structure ParentCfg1 where + parentBoolVal : Bool := false + deriving ToExpr + +structure SubCfg1 where + bool : Bool := false + nat : Nat := 0 + transparency : TransparencyMode := .default + deriving ToExpr + +structure Cfg1 extends ParentCfg1 where + boolVal : Bool := false + natVal : Nat := 0 + intVal : Int := 0 + strVal : String := "" + extra : SubCfg1 := {} + parentBoolVal := true + deriving ToExpr + +declare_core_config_elab elabCoreCfg1 Cfg1 +declare_term_config_elab elabTermCfg1 Cfg1 +declare_config_elab elabTacticCfg1 Cfg1 +declare_command_config_elab elabCommandCfg1 Cfg1 + +/-! +Check the types of each of these elaborators. +-/ +/-- +info: elabCoreCfg1 (cfg : Syntax) (init : Cfg1 := { }) (logExceptions : Bool := false) : CoreM Cfg1 +-/ +#guard_msgs in #check elabCoreCfg1 +/-- +info: elabTermCfg1 (cfg : Syntax) (init : Cfg1 := { }) (logExceptions : Bool := true) : TermElabM Cfg1 +-/ +#guard_msgs in #check elabTermCfg1 +/-- +info: elabTacticCfg1 (cfg : Syntax) (init : Cfg1 := { }) (logExceptions : Bool := true) : Tactic.TacticM Cfg1 +-/ +#guard_msgs in #check elabTacticCfg1 +/-- +info: elabCommandCfg1 (cfg : Syntax) (init : Cfg1 := { }) (logExceptions : Bool := true) : Command.CommandElabM Cfg1 +-/ +#guard_msgs in #check elabCommandCfg1 + +/-! +Create commands and tactics to test these elaborators. +-/ +elab "#test_core_cfg1" cfg:optConfig : command => Command.liftTermElabM do + let c ← elabCoreCfg1 cfg + logInfo m!"{toExpr c}" + +elab "#test_term_cfg1" cfg:optConfig : command => Command.liftTermElabM do + let c ← elabTermCfg1 cfg + logInfo m!"{toExpr c}" + +elab "test_tactic_cfg1" cfg:optConfig : tactic => Tactic.withMainContext do + let c ← elabTacticCfg1 cfg + logInfo m!"{toExpr c}" + +elab "#test_command_cfg1" cfg:optConfig : command => do + let c ← elabCommandCfg1 cfg + logInfo m!"{toExpr c}" + +/-! +Testing configuration option evaluation. Only need to exercise all the optinos for one of them. +-/ +/-- info: { } -/ +#guard_msgs in #test_core_cfg1 +/-- info: { boolVal := true } -/ +#guard_msgs in #test_core_cfg1 (boolVal := true) +/-- info: { boolVal := true } -/ +#guard_msgs in #test_core_cfg1 +boolVal +/-- info: { boolVal := true, intVal := -2 } -/ +#guard_msgs in #test_core_cfg1 +boolVal (intVal := -2) +/-- info: { boolVal := true, natVal := 3, intVal := -2 } -/ +#guard_msgs in #test_core_cfg1 +boolVal (intVal := -2) (natVal := 3) +/-- info: { strVal := "yo" } -/ +#guard_msgs in #test_core_cfg1 (strVal := "yo") +/-- info: { extra := { bool := true, nat := 3 } } -/ +#guard_msgs in #test_core_cfg1 (extra := { bool := true, nat := 3 }) +/-- info: { extra := { bool := true, nat := 3 } } -/ +#guard_msgs in #test_core_cfg1 (extra.bool := true) (extra.nat := 3) +/-- info: { parentBoolVal := false } -/ +#guard_msgs in #test_core_cfg1 -parentBoolVal +/-- info: { natVal := 4 } -/ +#guard_msgs in #test_core_cfg1 (natVal := 2 + 2) +/-- info: { natVal := 100000 } -/ +#guard_msgs in #test_core_cfg1 (natVal := Meta.Simp.defaultMaxSteps) +/-- info: { extra := { bool := true } } -/ +#guard_msgs in #test_core_cfg1 +extra.bool +/-- info: { extra := { transparency := TransparencyMode.all } } -/ +#guard_msgs in #test_core_cfg1 (extra.transparency := .all) +/-- info: { extra := { bool := true } } -/ +#guard_msgs in #test_core_cfg1 (config := { extra.bool := true }) + +/-! +Testing that each elaborator works. +-/ +/-- info: { boolVal := true } -/ +#guard_msgs in #test_core_cfg1 +boolVal +/-- info: { boolVal := true } -/ +#guard_msgs in #test_term_cfg1 +boolVal +/-- info: { boolVal := true } -/ +#guard_msgs in example : True := by test_tactic_cfg1 +boolVal; trivial +/-- info: { boolVal := true } -/ +#guard_msgs in #test_command_cfg1 +boolVal + +/-! +Testing default error behaviors. +- `CoreM` doesn't allow errors +- `TermM` allows errors if errToSorry is enabled +- `TacticM` allows errors if recovery is enabled +- `CommandM` allows errors +-/ + +/-- error: Unknown identifier `config_eval_test.invalid` -/ +#guard_msgs in #test_core_cfg1 (boolVal := config_eval_test.invalid) (natVal := 2 + 2) +/-- +error: Unknown identifier `config_eval_test.invalid` +--- +info: { natVal := 2 } +-/ +#guard_msgs in #test_term_cfg1 (boolVal := config_eval_test.invalid) (natVal := 2) +/-- +error: Type mismatch + Nat.zero +has type + Nat +but is expected to have type + Bool +--- +info: { natVal := 2 } +-/ +#guard_msgs in #test_term_cfg1 (boolVal := Nat.zero) (natVal := 2) +/-- +error: Unknown identifier `config_eval_test.invalid` +--- +info: { natVal := 2 } +-/ +#guard_msgs in example : True := by + test_tactic_cfg1 (boolVal := config_eval_test.invalid) (natVal := 2) + trivial +-- Recovery disabled -> fails, allowing `trivial` to be applied. +#guard_msgs in example : True := by + first | test_tactic_cfg1 (boolVal := config_eval_test.invalid) (natVal := 2) | trivial +/-- +error: Unknown identifier `config_eval_test.invalid` +--- +info: { natVal := 4 } +-/ +#guard_msgs in #test_command_cfg1 (boolVal := config_eval_test.invalid) (natVal := 2 + 2) diff --git a/tests/elab/extraModUses.lean b/tests/elab/extraModUses.lean index dbd617502f..20c889090f 100644 --- a/tests/elab/extraModUses.lean +++ b/tests/elab/extraModUses.lean @@ -128,7 +128,7 @@ Tactic configuration structures are recorded. public def test4 : True := by simp +contextual /-- -info: Entries: [import Init.Tactics, meta import Init.MetaTypes] +info: Entries: [import Init.Tactics] Is rev mod use: false -/ #guard_msgs in #eval showExtraModUses diff --git a/tests/elab/match_expr_perf.lean b/tests/elab/match_expr_perf.lean index b1a43fef53..defb4f42b2 100644 --- a/tests/elab/match_expr_perf.lean +++ b/tests/elab/match_expr_perf.lean @@ -7,7 +7,6 @@ prelude import Lean.Elab.Tactic.Omega.Core import Lean.Elab.Tactic.FalseOrByContra import Lean.Meta.Tactic.Cases -import Lean.Elab.Tactic.Config open Lean Meta Omega diff --git a/tests/elab/tactic_config.lean b/tests/elab/tactic_config.lean index b273c81a33..d21685e03f 100644 --- a/tests/elab/tactic_config.lean +++ b/tests/elab/tactic_config.lean @@ -57,7 +57,7 @@ error: unsolved goals #guard_msgs in example : True := by my_tactic +x /-- -error: Structure `MyTacticConfig` does not have a field named `w` +error: Invalid configuration option `w` for `MyTacticConfig` --- info: config is { x := 0, y := false } --- @@ -67,7 +67,7 @@ error: unsolved goals #guard_msgs in example : True := by my_tactic +w /-- -error: Field `x` of structure `MyTacticConfig` is not a structure +error: Invalid configuration option `x.a` for `MyTacticConfig` --- info: config is { x := 0, y := false } --- @@ -99,6 +99,8 @@ info: config is { toMyTacticConfig := { x := 1, y := true } } --- info: config is { toMyTacticConfig := { x := 2, y := false } } --- +info: config is { toMyTacticConfig := { x := 2, y := false } } +--- info: config is { toMyTacticConfig := { x := 1, y := true } } --- info: config is { toMyTacticConfig := { x := 22, y := false } } @@ -109,12 +111,30 @@ example : True := by my_tactic' +y my_tactic' (x := 1) my_tactic' -y (x := 2) + my_tactic' (x := 2) -y my_tactic' (config := {x := 1, y := true}) my_tactic' +y (config := {y := false}) trivial /-! -Tactic configurations with hierarchical fields +Evaluation failure +-/ +opaque fooNat : Nat := 22 +/-- +error: Could not evaluate the expression: + fooNat +of type `Nat`. +--- +info: config is { x := 0, y := true } +-/ +#guard_msgs in +example : True := by + my_tactic (x := fooNat) +y + trivial + +/-! +Tactic configurations with hierarchical fields. +The `toA` parent projections are not made available for use. -/ structure A where @@ -131,14 +151,19 @@ elab "ctac" cfg:Parser.Tactic.optConfig : tactic => do let config ← elabC cfg logInfo m!"config is {repr config}" -/-- -info: config is { b := { toA := { x := false } } } ---- -info: config is { b := { toA := { x := false } } } --/ +/-- info: config is { b := { toA := { x := false } } } -/ #guard_msgs in example : True := by ctac -b.x + trivial + +/-- +error: Invalid configuration option `b.toA.x` for `C` +--- +info: config is { b := { toA := { x := true } } } +-/ +#guard_msgs in +example : True := by ctac -b.toA.x trivial @@ -147,7 +172,7 @@ Responds to recovery mode. In these, `ctac` continues even though configuration -/ /-- -error: Structure `C` does not have a field named `x` +error: Invalid configuration option `x` for `C` --- info: config is { b := { toA := { x := true } } } --- @@ -159,7 +184,7 @@ example : True := by trace_state trivial --- Check that when recovery mode is false, no error is reported. +-- Check that when recovery mode is false, no error is reported, since there was an exception. /-- trace: ⊢ True -/ #guard_msgs in example : True := by @@ -168,7 +193,7 @@ example : True := by trivial /-- -error: Structure `C` does not have a field named `x` +error: Invalid configuration option `x` for `C` --- info: config is { b := { toA := { x := true } } } --- @@ -195,11 +220,11 @@ Elaboration errors cause the tactic to use the default configuration. /-- error: Type mismatch - false + "oops" has type - Bool + String but is expected to have type - B + Bool --- info: config is { b := { toA := { x := true } } } --- @@ -208,7 +233,7 @@ error: unsolved goals -/ #guard_msgs in example : True := by - ctac (b := false) + ctac (b.x := "oops") done @@ -247,6 +272,31 @@ info: config is { x := 0, y := false } -/ #guard_msgs in my_command (x := true) +/-! +Testing `Occurrences.pos` +-/ +/-- +trace: a : Nat +this : a = 0 + a +⊢ 0 + a = 0 + a +-/ +#guard_msgs in +example (a : Nat) : a = 0 + a := by + have : a = 0 + a := by rw [Nat.zero_add] + rewrite (occs := .pos [1]) [this] + trace_state + rfl +/-- +trace: a : Nat +this : a = 0 + a +⊢ 0 + a = 0 + a +-/ +#guard_msgs in +example (a : Nat) : a = 0 + a := by + have : a = 0 + a := by rw [Nat.zero_add] + rewrite (occs := [1]) [this] + trace_state + rfl /-! Pretty printing of configuration, checking whitespace is present. @@ -262,3 +312,129 @@ elab "#pp_tac " t:tactic : command => Elab.Command.liftTermElabM do #guard_msgs in #pp_tac simp (contextual := true) +zeta /-- info: simp (contextual := true) +zeta -/ #guard_msgs in #pp_tac simp(contextual := true)+zeta + + +/-! +Simp user configuration. +-/ + +open Meta.Simp Elab.Tactic in +simproc testUserConfig (_) := fun _ => do + let v1 ← getUserConfigOption tactic.simp.user.exampleBool + let v2 ← getUserConfigOption tactic.simp.user.exampleNat + let v3 ← getUserConfigOption tactic.simp.user.exampleInt + let v4 ← getUserConfigOption tactic.simp.user.exampleString + logInfo m!"exampleBool: {v1} exampleNat: {v2} exampleInt: {v3} exampleString: {repr v4}" + return .continue + +/-- +info: exampleBool: false exampleNat: 0 exampleInt: 0 exampleString: "" +--- +info: exampleBool: true exampleNat: 0 exampleInt: 0 exampleString: "" +--- +info: exampleBool: false exampleNat: 22 exampleInt: 0 exampleString: "" +--- +info: exampleBool: false exampleNat: 0 exampleInt: -22 exampleString: "" +--- +info: exampleBool: false exampleNat: 0 exampleInt: 0 exampleString: "hi" +--- +info: exampleBool: true exampleNat: 22 exampleInt: -22 exampleString: "hi" +--- +error: User options are of the form `user.optionName` +--- +info: exampleBool: false exampleNat: 0 exampleInt: 0 exampleString: "" +-/ +#guard_msgs in +example (h : False) : False := by + simp -failIfUnchanged + simp -failIfUnchanged +user.exampleBool + simp -failIfUnchanged (user.exampleNat := 22) + simp -failIfUnchanged (user.exampleInt := -22) + simp -failIfUnchanged (user.exampleString := "hi") + simp -failIfUnchanged +user.exampleBool (user.exampleNat := 22) (user.exampleInt := -22) (user.exampleString := "hi") + simp -failIfUnchanged +user + exact h + +/-! +Testing the `derive_eval_expr_instance_using_meta_eval` instance. +-/ +section +open Lean.Elab.ConfigEval + +structure MetaEvalTest where + x : Nat + b : Bool + f : Nat → Nat + +derive_eval_expr_instance_using_meta_eval MetaEvalTest + +/-- info: x: 3, b: true, f 10: 12, f 100: 102 -/ +#guard_msgs in +#eval do + let stx ← `({ x := 3, b := true, f := (·+2) }) + let c ← evalExprWithElab (α := MetaEvalTest) stx + logInfo m!"x: {c.x}, b: {c.b}, f 10: {c.f 10}, f 100: {c.f 100}" + +/-! +Testing bare atoms for positive options +-/ +structure TestBareConfig where + only : Bool := false + x : Nat := 0 + deriving Repr +syntax testBareConfigOnly := &"only" +syntax testBareConfigCfg := many(testBareConfigOnly <|> Parser.Term.configItem) + +declare_command_config_elab elabTestBareConfig TestBareConfig + +elab "#test_bare_config" cfg:testBareConfigCfg : command => do + let config ← elabTestBareConfig cfg + logInfo m!"config is {repr config}" + +/-- info: config is { only := false, x := 0 } -/ +#guard_msgs in #test_bare_config +/-- info: config is { only := true, x := 0 } -/ +#guard_msgs in #test_bare_config only +/-- info: config is { only := true, x := 0 } -/ +#guard_msgs in #test_bare_config +only +/-- info: config is { only := true, x := 0 } -/ +#guard_msgs in #test_bare_config (only := true) +/-- info: config is { only := true, x := 2 } -/ +#guard_msgs in #test_bare_config (x := 2) only +/-- info: config is { only := true, x := 2 } -/ +#guard_msgs in #test_bare_config only (x := 2) + +/-! +Testing auto-derivations +-/ +namespace AutoDeriveTest + +structure A where + n : Nat + +inductive B where + | ctor1 + | ctor2 (a : Option A) + +structure C where + opt1 : List A + opt2 : Option (Array B) + +open scoped Lean.Elab.ConfigEval + +ensure_eval_term_expr_instances C + +/-- info: instEvalTermA -/ +#guard_msgs in #synth EvalTerm A +/-- info: instEvalTermB -/ +#guard_msgs in #synth EvalTerm B +/-- info: instEvalTermC -/ +#guard_msgs in #synth EvalTerm C +/-- info: instEvalExprA -/ +#guard_msgs in #synth EvalExpr A +/-- info: instEvalExprB -/ +#guard_msgs in #synth EvalExpr B +/-- info: instEvalExprC -/ +#guard_msgs in #synth EvalExpr C + +end AutoDeriveTest diff --git a/tests/elab/whereCmd.lean b/tests/elab/whereCmd.lean index 4e203c8c01..fdb2fbe2b4 100644 --- a/tests/elab/whereCmd.lean +++ b/tests/elab/whereCmd.lean @@ -89,7 +89,7 @@ open Array renaming map -> listMap /-- info: open Lean Lean.Meta open Lean.Elab hiding TermElabM -open Lean.Elab.Command Std +open Lean.Elab.Command Lean.Meta.Command Std open Array renaming map → listMap -/ #guard_msgs in #where