From 691acde69698ac057208cbdf48248166b1685be9 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Fri, 15 Nov 2024 11:11:54 -0800 Subject: [PATCH] feat: `pp.parens` option to pretty print with all parentheses (#2934) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR adds the option `pp.parens` (default: false) that causes the pretty printer to eagerly insert parentheses, which can be useful for teaching and for understanding the structure of expressions. For example, it causes `p → q → r` to pretty print as `p → (q → r)`. Any notations with precedence greater than or equal to `maxPrec` do not receive such discretionary parentheses, since this precedence level is considered to be infinity. This option was a feature in the Lean 3 community edition. --- .../PrettyPrinter/Delaborator/Options.lean | 6 ++ src/Lean/PrettyPrinter/Parenthesizer.lean | 27 +++++++-- tests/lean/run/ppParens.lean | 56 +++++++++++++++++++ 3 files changed, 83 insertions(+), 6 deletions(-) create mode 100644 tests/lean/run/ppParens.lean diff --git a/src/Lean/PrettyPrinter/Delaborator/Options.lean b/src/Lean/PrettyPrinter/Delaborator/Options.lean index 4b36881261..c8e70fbc36 100644 --- a/src/Lean/PrettyPrinter/Delaborator/Options.lean +++ b/src/Lean/PrettyPrinter/Delaborator/Options.lean @@ -24,6 +24,11 @@ register_builtin_option pp.notation : Bool := { group := "pp" descr := "(pretty printer) disable/enable notation (infix, mixfix, postfix operators and unicode characters)" } +register_builtin_option pp.parens : Bool := { + defValue := false + group := "pp" + descr := "(pretty printer) if set to true, notation is wrapped in parentheses regardless of precedence" +} register_builtin_option pp.unicode.fun : Bool := { defValue := false group := "pp" @@ -248,6 +253,7 @@ def getPPNatLit (o : Options) : Bool := o.get pp.natLit.name (getPPNumericTypes def getPPCoercions (o : Options) : Bool := o.get pp.coercions.name (!getPPAll o) def getPPExplicit (o : Options) : Bool := o.get pp.explicit.name (getPPAll o) def getPPNotation (o : Options) : Bool := o.get pp.notation.name (!getPPAll o) +def getPPParens (o : Options) : Bool := o.get pp.parens.name pp.parens.defValue def getPPUnicodeFun (o : Options) : Bool := o.get pp.unicode.fun.name false def getPPMatch (o : Options) : Bool := o.get pp.match.name (!getPPAll o) def getPPFieldNotation (o : Options) : Bool := o.get pp.fieldNotation.name (!getPPAll o) diff --git a/src/Lean/PrettyPrinter/Parenthesizer.lean b/src/Lean/PrettyPrinter/Parenthesizer.lean index ab41996d70..9b04f6fe9a 100644 --- a/src/Lean/PrettyPrinter/Parenthesizer.lean +++ b/src/Lean/PrettyPrinter/Parenthesizer.lean @@ -8,6 +8,7 @@ import Lean.Parser.Extension import Lean.Parser.StrInterpolation import Lean.ParserCompiler.Attribute import Lean.PrettyPrinter.Basic +import Lean.PrettyPrinter.Delaborator.Options /-! @@ -82,8 +83,10 @@ namespace PrettyPrinter namespace Parenthesizer structure Context where - -- We need to store this `categoryParser` argument to deal with the implicit Pratt parser call in `trailingNode.parenthesizer`. + /-- We need to store this `categoryParser` argument to deal with the implicit Pratt parser call in `trailingNode.parenthesizer`. -/ cat : Name := Name.anonymous + /-- Whether to add parentheses regardless of any other conditions. This is cached from the `pp.parens` option. -/ + forceParens : Bool := false structure State where stxTrav : Syntax.Traverser @@ -217,8 +220,13 @@ def maybeParenthesize (cat : Name) (canJuxtapose : Bool) (mkParen : Syntax → S let { minPrec := some minPrec, trailPrec := trailPrec, trailCat := trailCat, .. } ← get | trace[PrettyPrinter.parenthesize] "visited a syntax tree without precedences?!{line ++ format stx}" trace[PrettyPrinter.parenthesize] (m!"...precedences are {prec} >? {minPrec}" ++ if canJuxtapose then m!", {(trailPrec, trailCat)} <=? {(st.contPrec, st.contCat)}" else "") - -- Should we parenthesize? - if (prec > minPrec || canJuxtapose && match trailPrec, st.contPrec with | some trailPrec, some contPrec => trailCat == st.contCat && trailPrec <= contPrec | _, _ => false) then + /- Should we parenthesize? + * Note about forceParens mode: we don't insert outermost parentheses (we use the syntax traverser parents to detect this), + and we don't insert parentheses when we are at `maxPrec` (since this is effectively infinity). + -/ + if (((← read).forceParens && !st.stxTrav.parents.isEmpty && minPrec < Parser.maxPrec) + || prec > minPrec + || canJuxtapose && match trailPrec, st.contPrec with | some trailPrec, some contPrec => trailCat == st.contCat && trailPrec <= contPrec | _, _ => false) then -- The recursive `visit` call, by the invariant, has moved to the preceding node. In order to parenthesize -- the original node, we must first move to the right, except if we already were at the left-most child in the first -- place. @@ -540,16 +548,23 @@ instance : Coe (Parenthesizer → Parenthesizer → Parenthesizer) Parenthesizer end Parenthesizer open Parenthesizer -/-- Add necessary parentheses in `stx` parsed by `parser`. -/ +/-- +Adds necessary parentheses in `stx` parsed by `parser`. +-/ def parenthesize (parenthesizer : Parenthesizer) (stx : Syntax) : CoreM Syntax := do trace[PrettyPrinter.parenthesize.input] "{format stx}" + let opts ← getOptions catchInternalId backtrackExceptionId (do - let (_, st) ← (parenthesizer {}).run { stxTrav := Syntax.Traverser.fromSyntax stx } + let (_, st) ← (parenthesizer { forceParens := getPPParens opts }).run { stxTrav := Syntax.Traverser.fromSyntax stx } pure st.stxTrav.cur) (fun _ => throwError "parenthesize: uncaught backtrack exception") -def parenthesizeCategory (cat : Name) := parenthesize <| categoryParser.parenthesizer cat 0 +/-- +Adds necessary parentheses to the syntax in the given category (for example, `term`, `tactic`, or `command`). +-/ +def parenthesizeCategory (cat : Name) (stx : Syntax) := + parenthesize (categoryParser.parenthesizer cat 0) stx def parenthesizeTerm := parenthesizeCategory `term def parenthesizeTactic := parenthesizeCategory `tactic diff --git a/tests/lean/run/ppParens.lean b/tests/lean/run/ppParens.lean new file mode 100644 index 0000000000..478f8808af --- /dev/null +++ b/tests/lean/run/ppParens.lean @@ -0,0 +1,56 @@ +/-! +# Tests for the `pp.parens` pretty printing option +-/ + +set_option pp.parens true + +/-! +No parentheses around numeral. +-/ +/-- info: 1 : Nat -/ +#guard_msgs in #check 1 + +/-! +No parentheses around variable. +-/ +/-- info: x : Nat -/ +#guard_msgs in variable (x : Nat) in #check x + +/-! +No parentheses around each individual function application. +-/ +def f (x y z : Nat) : Nat := x + y + z +/-- info: f 1 2 3 : Nat -/ +#guard_msgs in #check f 1 2 3 + +/-! +Example arithmetic expressions +-/ +/-- info: (1 + (2 * 3)) + 4 : Nat -/ +#guard_msgs in #check 1 + 2 * 3 + 4 +/-- info: Nat.add_assoc : ∀ (n m k : Nat), (((n + m) + k) = (n + (m + k))) -/ +#guard_msgs in #check (Nat.add_assoc) + +/-! +Implication chains +-/ +/-- info: p → (q → r) : Prop -/ +#guard_msgs in variable (p q r : Prop) in #check p → q → r + +/-! +No parentheses around list literals +-/ +/-- info: [1, 2, 3] ++ [3, 4, 5] : List Nat -/ +#guard_msgs in #check [1,2,3] ++ [3,4,5] + +/-! +Parentheses around body of forall. +-/ +/-- info: ∀ (p : (Nat → (Nat → Prop))), (p (1 + 2) 3) : Prop -/ +#guard_msgs in #check ∀ (p : Nat → Nat → Prop), p (1 + 2) 3 + +/-! +Parentheses around branches of `if`. +-/ +/-- info: if True then (1 + 2) else (2 + 3) : Nat -/ +#guard_msgs in #check if True then 1 + 2 else 2 + 3