From 376ae32c7c692b830bfc2afa82800d12aebfeab5 Mon Sep 17 00:00:00 2001 From: Kim Morrison <477956+kim-em@users.noreply.github.com> Date: Sat, 21 Jun 2025 10:50:25 +1000 Subject: [PATCH] feat: fix pretty printing of grind attributes (#8892) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR corrects the pretty printing of `grind` modifiers. Previously `@[grind →]` was being pretty printed as `@[grind→ ]` (Space on the right of the symbol, rather than left.) This fixes the pretty printing of attributes, and preserves the presence of spaces after the symbol in the output of `grind?`. --------- Co-authored-by: Leonardo de Moura --- src/Init/Grind/Tactics.lean | 34 +++++++++--------- src/Lean/Meta/Tactic/Grind/Attr.lean | 53 ++++++++++++++++------------ stage0/src/stdlib_flags.h | 2 +- tests/lean/run/grind_pp_attr.lean | 27 ++++++++++++++ 4 files changed, 75 insertions(+), 41 deletions(-) create mode 100644 tests/lean/run/grind_pp_attr.lean diff --git a/src/Init/Grind/Tactics.lean b/src/Init/Grind/Tactics.lean index 0dabeb1141..8ea6fcf78c 100644 --- a/src/Init/Grind/Tactics.lean +++ b/src/Init/Grind/Tactics.lean @@ -66,26 +66,26 @@ Reset all `grind` attributes. This command is intended for testing purposes only syntax (name := resetGrindAttrs) "reset_grind_attrs%" : command namespace Attr -syntax grindGen := &"gen " -syntax grindEq := "= " (grindGen)? -syntax grindEqBoth := atomic("_" "=" "_ ") (grindGen)? -syntax grindEqRhs := atomic("=" "_ ") (grindGen)? -syntax grindEqBwd := atomic("←" "= ") <|> atomic("<-" "= ") -syntax grindBwd := ("← " <|> "<- ") (grindGen)? -syntax grindFwd := "→ " <|> "-> " -syntax grindRL := "⇐ " <|> "<= " -syntax grindLR := "⇒ " <|> "=> " -syntax grindUsr := &"usr " -syntax grindCases := &"cases " -syntax grindCasesEager := atomic(&"cases" &"eager ") -syntax grindIntro := &"intro " -syntax grindExt := &"ext " +syntax grindGen := ppSpace &"gen" +syntax grindEq := "=" (grindGen)? +syntax grindEqBoth := atomic("_" "=" "_") (grindGen)? +syntax grindEqRhs := atomic("=" "_") (grindGen)? +syntax grindEqBwd := atomic("←" "=") <|> atomic("<-" "=") +syntax grindBwd := ("← " <|> "←" <|> "<-") (grindGen)? -- TODO remove "← " after update stage 0 +syntax grindFwd := "→ " <|> "→" <|> "->" -- TODO remove "→ " after update stage 0 +syntax grindRL := "⇐" <|> "<=" +syntax grindLR := "⇒" <|> "=>" +syntax grindUsr := &"usr" +syntax grindCases := &"cases" +syntax grindCasesEager := atomic(&"cases" &"eager") +syntax grindIntro := &"intro" +syntax grindExt := &"ext" syntax grindMod := grindEqBoth <|> grindEqRhs <|> grindEq <|> grindEqBwd <|> grindBwd <|> grindFwd <|> grindRL <|> grindLR <|> grindUsr <|> grindCasesEager <|> grindCases <|> grindIntro <|> grindExt <|> grindGen -syntax (name := grind) "grind" (grindMod)? : attr -syntax (name := grind?) "grind?" (grindMod)? : attr +syntax (name := grind) "grind" ppSpace (grindMod)? : attr +syntax (name := grind?) "grind?" ppSpace (grindMod)? : attr end Attr end Lean.Parser @@ -204,7 +204,7 @@ namespace Lean.Parser.Tactic -/ syntax grindErase := "-" ident -syntax grindLemma := (Attr.grindMod)? ident +syntax grindLemma := (Attr.grindMod ppSpace)? ident syntax grindParam := grindErase <|> grindLemma syntax (name := grind) diff --git a/src/Lean/Meta/Tactic/Grind/Attr.lean b/src/Lean/Meta/Tactic/Grind/Attr.lean index d1c5bc3710..a0c46c0f8b 100644 --- a/src/Lean/Meta/Tactic/Grind/Attr.lean +++ b/src/Lean/Meta/Tactic/Grind/Attr.lean @@ -20,29 +20,36 @@ inductive AttrKind where /-- Return theorem kind for `stx` of the form `Attr.grindThmMod` -/ def getAttrKindCore (stx : Syntax) : CoreM AttrKind := do match stx with - | `(Parser.Attr.grindMod| =) => return .ematch (.eqLhs false) - | `(Parser.Attr.grindMod| = gen) => return .ematch (.eqLhs true) - | `(Parser.Attr.grindMod| →) - | `(Parser.Attr.grindMod| ->) => return .ematch .fwd - | `(Parser.Attr.grindMod| ←) - | `(Parser.Attr.grindMod| <-) => return .ematch (.bwd false) - | `(Parser.Attr.grindMod| <- gen) => return .ematch (.bwd true) - | `(Parser.Attr.grindMod| =_) => return .ematch (.eqRhs false) - | `(Parser.Attr.grindMod| =_ gen) => return .ematch (.eqRhs true) - | `(Parser.Attr.grindMod| _=_) => return .ematch (.eqBoth false) - | `(Parser.Attr.grindMod| _=_ gen) => return .ematch (.eqBoth true) - | `(Parser.Attr.grindMod| ←=) => return .ematch .eqBwd - | `(Parser.Attr.grindMod| ⇒) - | `(Parser.Attr.grindMod| =>) => return .ematch .leftRight - | `(Parser.Attr.grindMod| ⇐) - | `(Parser.Attr.grindMod| <=) => return .ematch .rightLeft - | `(Parser.Attr.grindMod| usr) => return .ematch .user - | `(Parser.Attr.grindMod| gen) => return .ematch (.default true) - | `(Parser.Attr.grindMod| cases) => return .cases false - | `(Parser.Attr.grindMod| cases eager) => return .cases true - | `(Parser.Attr.grindMod| intro) => return .intro - | `(Parser.Attr.grindMod| ext) => return .ext - | _ => throwError "unexpected `grind` theorem kind: `{stx}`" + | `(Parser.Attr.grindMod|=) => return .ematch (.eqLhs false) + | `(Parser.Attr.grindMod|= gen) => return .ematch (.eqLhs true) + | `(Parser.Attr.grindMod|→) + | `(Parser.Attr.grindMod|->) => return .ematch .fwd + | `(Parser.Attr.grindMod|←) + | `(Parser.Attr.grindMod|<-) => return .ematch (.bwd false) + | `(Parser.Attr.grindMod|<- gen) => return .ematch (.bwd true) + | `(Parser.Attr.grindMod|=_) => return .ematch (.eqRhs false) + | `(Parser.Attr.grindMod|=_ gen) => return .ematch (.eqRhs true) + | `(Parser.Attr.grindMod|_=_) => return .ematch (.eqBoth false) + | `(Parser.Attr.grindMod|_=_ gen) => return .ematch (.eqBoth true) + | `(Parser.Attr.grindMod|←=) => return .ematch .eqBwd + | `(Parser.Attr.grindMod|⇒) + | `(Parser.Attr.grindMod|=>) => return .ematch .leftRight + | `(Parser.Attr.grindMod|⇐) + | `(Parser.Attr.grindMod|<=) => return .ematch .rightLeft + | `(Parser.Attr.grindMod|usr) => return .ematch .user + | `(Parser.Attr.grindMod|gen) => return .ematch (.default true) + | `(Parser.Attr.grindMod|cases) => return .cases false + | `(Parser.Attr.grindMod|cases eager) => return .cases true + | `(Parser.Attr.grindMod|intro) => return .intro + | `(Parser.Attr.grindMod|ext) => return .ext + | _ => + -- TODO: remove after update stage0 + let stx := stx[0] + if stx.isOfKind ``Parser.Attr.grindFwd then return .ematch .fwd + if stx.isOfKind ``Parser.Attr.grindBwd then return .ematch (.bwd false) + if stx.isOfKind ``Parser.Attr.grindRL then return .ematch .rightLeft + if stx.isOfKind ``Parser.Attr.grindLR then return .ematch .leftRight + throwError "unexpected `grind` theorem kind: `{stx}`" /-- Return theorem kind for `stx` of the form `(Attr.grindMod)?` -/ def getAttrKindFromOpt (stx : Syntax) : CoreM AttrKind := do diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h index 79a0e58edd..6b964da742 100644 --- a/stage0/src/stdlib_flags.h +++ b/stage0/src/stdlib_flags.h @@ -11,7 +11,7 @@ options get_default_options() { opts = opts.update({"debug", "terminalTacticsAsSorry"}, false); // switch to `true` for ABI-breaking changes affecting meta code; // see also next option! - opts = opts.update({"interpreter", "prefer_native"}, false); + opts = opts.update({"interpreter", "prefer_native"}, true); // switch to `false` when enabling `prefer_native` should also affect use // of built-in parsers in quotations; this is usually the case, but setting // both to `true` may be necessary for handling non-builtin parsers with diff --git a/tests/lean/run/grind_pp_attr.lean b/tests/lean/run/grind_pp_attr.lean new file mode 100644 index 0000000000..3c582e4fce --- /dev/null +++ b/tests/lean/run/grind_pp_attr.lean @@ -0,0 +1,27 @@ +import Lean.Elab.Command + +open Lean Elab Command + +def test (stx : Syntax) : CommandElabM Unit := do + let fmt : Option Format := ← + liftCoreM <| PrettyPrinter.ppCategory `command stx + if let some fmt := fmt then + let st := fmt.pretty + dbg_trace st + + +/-- +info: @[grind =] +example := + 0 +-/ +#guard_msgs in +run_cmd test (← `(@[grind =] example := 0)) + +/-- +info: @[grind _=_] +example := + 0 +-/ +#guard_msgs in +run_cmd test (← `(@[grind _=_] example := 0))