From d4b1be094d3c10152be01d041fe5b3b8e5adf389 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Wed, 30 Oct 2024 16:31:34 -0700 Subject: [PATCH] feat: adds `optConfig` syntax for tactic configuration (#5883) This PR adds a new syntax for tactic and command configurations. It also updates the elaborator construction command to be able to process this new syntax. We do not update core tactics yet. Once tactics switch over to it, rather than (for example) writing `simp (config := { contextual := true, maxSteps := 22})`, one can write `simp +contextual (maxSteps := 22)`. The new syntax is reverse compatible in the sense that `(config := ...)` still sets the entire configuration. Note to metaprogrammers: Use `optConfig` instead of `(config)?`. The elaborator generated by `declare_config_elab` accepts both old and new configurations. The elaborator has also been written to be tolerant to null nodes, so adapting to `optConfig` should be as easy as changing just the syntax for your tactics and deleting `mkOptionalNode`. Breaking change: The new system is mostly reverse compatible, however the type of the generated elaborator now lands in `TacticM` to make use of the current recovery state. Commands that wish to elaborate configurations should now use `declare_command_config_elab` instead of `declare_config_elab` to get an elaborator landing in `CommandElabM`. --- src/Init/Conv.lean | 2 +- src/Init/Tactics.lean | 22 ++- src/Lean/Elab/Tactic/Config.lean | 184 ++++++++++++++++++++--- src/Lean/Elab/Tactic/Simp.lean | 2 +- tests/lean/1576.lean.expected.out | 2 + tests/lean/run/tactic_config.lean | 237 ++++++++++++++++++++++++++++++ 6 files changed, 429 insertions(+), 20 deletions(-) create mode 100644 tests/lean/run/tactic_config.lean diff --git a/src/Init/Conv.lean b/src/Init/Conv.lean index 3ca904f59b06..17d2c3a69db3 100644 --- a/src/Init/Conv.lean +++ b/src/Init/Conv.lean @@ -252,7 +252,7 @@ macro "rw" c:(config)? s:rwRuleSeq : conv => `(conv| rewrite $[$c]? $s) /-- `erw [rules]` is a shorthand for `rw (config := { transparency := .default }) [rules]`. This does rewriting up to unfolding of regular definitions (by comparison to regular `rw` which only unfolds `@[reducible]` definitions). -/ -macro "erw" s:rwRuleSeq : conv => `(conv| rw (config := { transparency := .default }) $s) +macro "erw" s:rwRuleSeq : conv => `(conv| rw (config := { transparency := .default }) $s:rwRuleSeq) /-- `args` traverses into all arguments. Synonym for `congr`. -/ macro "args" : conv => `(conv| congr) diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean index f96e371c50e1..8bd0260fbe52 100644 --- a/src/Init/Tactics.lean +++ b/src/Init/Tactics.lean @@ -417,7 +417,27 @@ It synthesizes a value of any target type by typeclass inference. -/ macro "infer_instance" : tactic => `(tactic| exact inferInstance) -/-- Optional configuration option for tactics -/ +/-- +`+opt` is short for `(opt := true)`. It sets the `opt` configuration option to `true`. +-/ +syntax posConfigItem := "+" noWs ident +/-- +`-opt` is short for `(opt := false)`. It sets the `opt` configuration option to `false`. +-/ +syntax negConfigItem := "-" noWs ident +/-- +`(opt := val)` sets the `opt` configuration option to `val`. + +As a special case, `(config := ...)` sets the entire configuration. +-/ +syntax valConfigItem := atomic("(" (ident <|> &"config")) " := " withoutPosition(term) ")" +/-- A configuration item for a tactic configuration. -/ +syntax configItem := posConfigItem <|> negConfigItem <|> valConfigItem + +/-- Configuration options for tactics. -/ +syntax optConfig := configItem* + +/-- Optional configuration option for tactics. (Deprecated. Replace `(config)?` with `optConfig`.) -/ syntax config := atomic(" (" &"config") " := " withoutPosition(term) ")" /-- The `*` location refers to all hypotheses and the goal. -/ diff --git a/src/Lean/Elab/Tactic/Config.lean b/src/Lean/Elab/Tactic/Config.lean index bcfcca1fcc41..6d1d89d2e520 100644 --- a/src/Lean/Elab/Tactic/Config.lean +++ b/src/Lean/Elab/Tactic/Config.lean @@ -1,7 +1,7 @@ /- Copyright (c) 2021 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Leonardo de Moura +Authors: Leonardo de Moura, Kyle Miller -/ prelude import Lean.Meta.Eval @@ -10,25 +10,175 @@ import Lean.Elab.SyntheticMVars import Lean.Linter.MissingDocs namespace Lean.Elab.Tactic -open Meta -macro (name := configElab) doc?:(docComment)? "declare_config_elab" elabName:ident type:ident : command => - `(unsafe def evalUnsafe (e : Expr) : TermElabM $type := - Meta.evalExpr' (safety := .unsafe) $type ``$type e - @[implemented_by evalUnsafe] opaque eval (e : Expr) : TermElabM $type - $[$doc?:docComment]? - def $elabName (optConfig : Syntax) : TermElabM $type := do - if optConfig.isNone then - return { : $type } - else - let c ← withoutModifyingStateWithInfoAndMessages <| withLCtx {} {} <| withSaveInfoContext <| Term.withSynthesize do - let c ← Term.elabTermEnsuringType optConfig[0][3] (Lean.mkConst ``$type) - Term.synthesizeSyntheticMVarsNoPostponing - instantiateMVars c - eval c - ) +open Meta Parser.Tactic Command + +/-- +Extracts the items from a tactic configuration, +either a `Lean.Parser.Tactic.optConfig`, `Lean.Parser.Tactic.config`, or these wrapped in null nodes. +-/ +private 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 := $val)) => #[Unhygienic.run <| withRef c `(configItem| (config := $val))] + | _ => #[] + +/-- +Appends two tactic configurations. +The configurations can be `Lean.Parser.Tactic.optConfig`, `Lean.Parser.Tactic.config`, +or these wrapped in null nodes (for example because the syntax is `(config)?`). +-/ +def appendConfig (cfg cfg' : Syntax) : TSyntax ``optConfig := + Unhygienic.run `(optConfig| $(getConfigItems cfg)* $(getConfigItems cfg')*) + +private structure ConfigItemView where + ref : Syntax + option : Ident + value : Term + /-- Whether this was using `+`/`-`, to be able to give a better error message on type mismatch. -/ + (bool : Bool := false) + +/-- Interprets the `config` as an array of option/value pairs. -/ +private def mkConfigItemViews (c : TSyntaxArray ``configItem) : Array ConfigItemView := + c.map fun item => + match item with + | `(configItem| ($option:ident := $value)) => { ref := item, option, value } + | `(configItem| +$option) => { ref := item, option, bool := true, value := mkCIdentFrom item ``true } + | `(configItem| -$option) => { ref := item, option, bool := true, value := mkCIdentFrom item ``false } + | _ => { ref := item, option := ⟨Syntax.missing⟩, value := ⟨Syntax.missing⟩ } + +/-- +Expands a field access into full field access like `toB.toA.x`. +Returns that and the last projection function for `x` itself. +-/ +private def expandFieldName (structName : Name) (fieldName : Name) : MetaM (Name × Name) := do + let env ← getEnv + unless isStructure env structName do throwError "'{.ofConstName structName}' is not a structure" + let some baseStructName := findField? env structName fieldName + | throwError "structure '{.ofConstName structName}' does not have a field named '{fieldName}'" + let some path := getPathToBaseStructure? env baseStructName structName + | throwError "(internal error) failed to access field '{fieldName}' in parent structure" + let field := path.foldl (init := .anonymous) (fun acc s => Name.appendCore acc <| Name.mkSimple s.getString!) ++ fieldName + let fieldInfo := (getFieldInfo? env baseStructName fieldName).get! + return (field, fieldInfo.projFn) + + +/-- +Given a hierarchical name `field`, returns the fully resolved field access, the base struct name, and the last projection function. +-/ +private partial def expandField (structName : Name) (field : Name) : MetaM (Name × Name) := do + match field with + | .num .. | .anonymous => throwError m!"invalid configuration field" + | .str .anonymous fieldName => expandFieldName structName (Name.mkSimple fieldName) + | .str field' fieldName => + let (field', projFn) ← expandField structName field' + let notStructure {α} : MetaM α := throwError "field '{field'}' of structure '{.ofConstName structName}' is not a structure" + let .const structName' _ := (← getConstInfo projFn).type.getForallBody | notStructure + unless isStructure (← getEnv) structName' do notStructure + let (field'', projFn) ← expandFieldName structName' (Name.mkSimple fieldName) + return (field' ++ field'', projFn) + +/-- Elaborates a tactic configuration. -/ +private def elabConfig (recover : Bool) (structName : Name) (items : Array ConfigItemView) : TermElabM Expr := + withoutModifyingStateWithInfoAndMessages <| withLCtx {} {} <| withSaveInfoContext do + let mut base? : Option Term := none + let mut fields : TSyntaxArray ``Parser.Term.structInstField := #[] + for item in items do + try + let option := item.option.getId.eraseMacroScopes + if option == `config then + base? ← withRef item.value `(($item.value : $(mkCIdent structName))) + fields := #[] + else + addCompletionInfo <| CompletionInfo.fieldId item.option option {} structName + let (path, projFn) ← withRef item.option <| expandField structName option + if item.bool then + -- Verify that the type is `Bool` + unless (← getConstInfo projFn).type.bindingBody! == .const ``Bool [] do + throwErrorAt item.ref m!"option is not boolean-valued, so '({option} := ...)' syntax must be used" + let value ← + match item.value with + | `(by $seq:tacticSeq) => + -- Special case: `(opt := by tacs)` uses the `tacs` syntax itself + withRef item.value <| `(Unhygienic.run `(tacticSeq| $seq)) + | value => pure value + fields := fields.push <| ← `(Parser.Term.structInstField| + $(mkCIdentFrom item.option path (canonical := true)):ident := $value) + catch ex => + if recover then + logException ex + else + throw ex + let stx : Term ← `({$[$base? with]? $fields*}) + let e ← Term.withSynthesize <| Term.elabTermEnsuringType stx (mkConst structName) + instantiateMVars e + +private def mkConfigElaborator + (doc? : Option (TSyntax ``Parser.Command.docComment)) (elabName type monadName : Ident) + (adapt recover : Term) : MacroM (TSyntax `command) := do + let empty ← withRef type `({ : $type}) + `(unsafe def evalUnsafe (e : Expr) : TermElabM $type := + Meta.evalExpr' (safety := .unsafe) $type ``$type e + @[implemented_by evalUnsafe] opaque eval (e : Expr) : TermElabM $type + $[$doc?:docComment]? + def $elabName (optConfig : Syntax) : $monadName $type := $adapt do + let recover := $recover + let go : TermElabM $type := withRef optConfig do + let items := mkConfigItemViews (getConfigItems optConfig) + if items.isEmpty then + return $empty + unless (← getEnv).contains ``$type do + throwError m!"error evaluating configuration, environment does not yet contain type {``$type}" + let c ← elabConfig recover ``$type items + if c.hasSyntheticSorry then + -- An error is already logged, return the default. + return $empty + if c.hasSorry then + throwError m!"configuration contains 'sorry'" + try + let res ← eval c + return res + catch ex => + let msg := m!"error evaluating configuration\n{indentD c}\n\nException: {ex.toMessageData}" + if false then + logError msg + return $empty + else + throwError msg + go) + +/-! +`declare_config_elab 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)?`). + +The elaborator responds to the current recovery state. + +For defining elaborators for commands, use `declare_command_config_elab`. +-/ +macro (name := configElab) doc?:(docComment)? "declare_config_elab" 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] def checkConfigElab : SimpleHandler := mkSimpleHandler "config elab" +/-! +`declare_command_config_elab 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. +-/ +macro (name := commandConfigElab) doc?:(docComment)? "declare_command_config_elab" elabName:ident type:ident : command => do + mkConfigElaborator doc? elabName type (mkCIdent ``CommandElabM) (mkCIdent ``liftTermElabM) (mkCIdent ``true) + +open Linter.MissingDocs in +@[builtin_missing_docs_handler Elab.Tactic.commandConfigElab] +def checkCommandConfigElab : SimpleHandler := mkSimpleHandler "config elab" + end Lean.Elab.Tactic diff --git a/src/Lean/Elab/Tactic/Simp.lean b/src/Lean/Elab/Tactic/Simp.lean index 6a3b0890c38e..fdfff857dd99 100644 --- a/src/Lean/Elab/Tactic/Simp.lean +++ b/src/Lean/Elab/Tactic/Simp.lean @@ -85,7 +85,7 @@ private def mkDischargeWrapper (optDischargeSyntax : Syntax) : TacticM Simp.Disc /- `optConfig` is of the form `("(" "config" ":=" term ")")?` -/ -def elabSimpConfig (optConfig : Syntax) (kind : SimpKind) : TermElabM Meta.Simp.Config := do +def elabSimpConfig (optConfig : Syntax) (kind : SimpKind) : TacticM Meta.Simp.Config := do match kind with | .simp => elabSimpConfigCore optConfig | .simpAll => return (← elabSimpConfigCtxCore optConfig).toConfig diff --git a/tests/lean/1576.lean.expected.out b/tests/lean/1576.lean.expected.out index 7ad0f7f2b858..d4986a660775 100644 --- a/tests/lean/1576.lean.expected.out +++ b/tests/lean/1576.lean.expected.out @@ -1,2 +1,4 @@ 1576.lean:1:35-1:38: error: unknown identifier 'non' 1576.lean:1:41-1:46: error: unknown identifier 'sense' +1576.lean:1:18-1:50: error: unsolved goals +⊢ True diff --git a/tests/lean/run/tactic_config.lean b/tests/lean/run/tactic_config.lean new file mode 100644 index 000000000000..4f0dc86ead34 --- /dev/null +++ b/tests/lean/run/tactic_config.lean @@ -0,0 +1,237 @@ +import Lean +/-! +# Tests for tactic configuration elaboration +-/ + +open Lean + +/-! +Simple tactic configuration +-/ +structure MyTacticConfig where + x : Nat := 0 + y : Bool := false + deriving Repr + +declare_config_elab elabMyTacticConfig MyTacticConfig + +elab "my_tactic" cfg:Parser.Tactic.optConfig : tactic => do + let config ← elabMyTacticConfig cfg + logInfo m!"config is {repr config}" + +/-- +info: config is { x := 0, y := false } +--- +info: config is { x := 0, y := true } +--- +info: config is { x := 1, y := false } +--- +info: config is { x := 2, y := false } +--- +info: config is { x := 1, y := true } +--- +info: config is { x := 0, y := false } +-/ +#guard_msgs in +example : True := by + my_tactic + my_tactic +y + my_tactic (x := 1) + my_tactic -y (x := 2) + my_tactic (config := {x := 1, y := true}) + my_tactic +y (config := {y := false}) + trivial + +/-! +Basic errors +-/ + +/-- +error: option is not boolean-valued, so '(x := ...)' syntax must be used +--- +info: config is { x := 0, y := false } +--- +error: unsolved goals +⊢ True +-/ +#guard_msgs in example : True := by my_tactic +x + +/-- +error: structure 'MyTacticConfig' does not have a field named 'w' +--- +info: config is { x := 0, y := false } +--- +error: unsolved goals +⊢ True +-/ +#guard_msgs in example : True := by my_tactic +w + +/-- +error: field 'x' of structure 'MyTacticConfig' is not a structure +--- +info: config is { x := 0, y := false } +--- +error: unsolved goals +⊢ True +-/ +#guard_msgs in example : True := by my_tactic +x.a + +/-! +A tactic configuration extending another with different default values. +-/ +structure MyTacticConfig' extends MyTacticConfig where + x := 22 + y := true + deriving Repr + +declare_config_elab elabMyTacticConfig' MyTacticConfig' + +elab "my_tactic'" cfg:Parser.Tactic.optConfig : tactic => do + let config ← elabMyTacticConfig' cfg + logInfo m!"config is {repr config}" + +/-- +info: config is { toMyTacticConfig := { x := 22, y := true } } +--- +info: config is { toMyTacticConfig := { x := 22, y := true } } +--- +info: config is { toMyTacticConfig := { x := 1, y := true } } +--- +info: config is { toMyTacticConfig := { x := 2, y := false } } +--- +info: config is { toMyTacticConfig := { x := 1, y := true } } +--- +info: config is { toMyTacticConfig := { x := 22, y := false } } +-/ +#guard_msgs in +example : True := by + my_tactic' + my_tactic' +y + my_tactic' (x := 1) + my_tactic' -y (x := 2) + my_tactic' (config := {x := 1, y := true}) + my_tactic' +y (config := {y := false}) + trivial + +/-! +Tactic configurations with hierarchical fields +-/ + +structure A where + x : Bool := true + deriving Repr +structure B extends A + deriving Repr +structure C where + b : B := {} + deriving Repr +declare_config_elab elabC C + +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 } } } +-/ +#guard_msgs in +example : True := by + ctac -b.x + ctac -b.toA.x + trivial + +/-! +Responds to recovery mode. In these, `ctac` continues even though configuration elaboration failed. +-/ + +/-- +error: structure 'C' does not have a field named 'x' +--- +info: config is { b := { toA := { x := true } } } +-/ +#guard_msgs in +example : True := by + ctac -x + trivial + +/-- +error: structure 'C' does not have a field named 'x' +--- +info: config is { b := { toA := { x := true } } } +--- +error: unsolved goals +⊢ True +-/ +#guard_msgs in +example : True := by + ctac -x + done + +/-! +Responds to recovery mode. In this, `ctac` fails, doesn't report anything, and then execution continues to `exact`. +-/ + +/-- error: unknown identifier 'blah' -/ +#guard_msgs in +example : True := by + first | ctac +x | exact blah + +/-! +Elaboration errors cause the tactic to use the default configuration. +-/ + +/-- +error: type mismatch + false +has type + Bool : Type +but is expected to have type + B : Type +--- +info: config is { b := { toA := { x := true } } } +--- +error: unsolved goals +⊢ True +-/ +#guard_msgs in +example : True := by + ctac (b := false) + done + + +/-! +Elaboration for command configuration +-/ + +structure MyCommandConfig where + x : Nat := 0 + y : Bool := false + deriving Repr + +declare_command_config_elab elabMyCommandConfig MyCommandConfig + +elab "my_command" cfg:Parser.Tactic.optConfig : command => do + let config ← elabMyCommandConfig cfg + logInfo m!"config is {repr config}" + +/-- info: config is { x := 0, y := false } -/ +#guard_msgs in my_command +/-- info: config is { x := 0, y := true } -/ +#guard_msgs in my_command +y +/-- info: config is { x := 1, y := true } -/ +#guard_msgs in my_command (x := 1) (y := true) +/-- info: config is { x := 0, y := false } -/ +#guard_msgs in my_command (x := 1) (y := true) (config := {}) +/-- +error: type mismatch + true +has type + Bool : Type +but is expected to have type + Nat : Type +--- +info: config is { x := 0, y := false } +-/ +#guard_msgs in my_command (x := true)