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)