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

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

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

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

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

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