From c2fbb3d30780bc2a977b246ed0e47a41b465412a Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 20 Aug 2020 18:07:01 +0200 Subject: [PATCH] fix: parenthesizer: parenthesize only because of subsequent parser if in same syntax category MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Otherwise, we would parenthesize `... : α → β := ...` as `... : (α → β) := ...` since in ``` def declValSimple := parser! " := " >> termParser ``` there is an implicit `checkPrec 1024` from `parser!`. --- src/Lean/PrettyPrinter/Parenthesizer.lean | 68 ++++++++++++----------- 1 file changed, 35 insertions(+), 33 deletions(-) diff --git a/src/Lean/PrettyPrinter/Parenthesizer.lean b/src/Lean/PrettyPrinter/Parenthesizer.lean index 09ed49ac83..68847f876b 100644 --- a/src/Lean/PrettyPrinter/Parenthesizer.lean +++ b/src/Lean/PrettyPrinter/Parenthesizer.lean @@ -28,7 +28,8 @@ supposedly produced by `p prec` if 1. the leading/any trailing parser involved in `stx` has precedence < `prec` (because without parentheses, `p prec` would not produce all of `stx`), or 2. the trailing parser parsing the input to *the right of* `stx`, if any, has precedence >= `prec` (because without - parentheses, `p prec` would have parsed it as well and made it a part of `stx`). + parentheses, `p prec` would have parsed it as well and made it a part of `stx`). We also check that the two parsers + are from the same syntax category. Note that in case 2, it is also sufficient to parenthesize a *parent* node as long as the offending parser is still to the right of that node. For example, imagine the tree structure of `(f $ fun x => x) y` without parentheses. We need to @@ -82,14 +83,14 @@ namespace PrettyPrinter namespace Parenthesizer structure Context := --- We need to store this argument of `maybeParenthesize` to deal with the implicit Pratt parser call in --- `trailingNode.parenthesizer`. -(mkParen : Option (Syntax → Syntax) := none) +-- We need to store this `categoryParser` argument to deal with the implicit Pratt parser call in `trailingNode.parenthesizer`. +(cat : Name := Name.anonymous) structure State := (stxTrav : Syntax.Traverser) ---- precedence of the current left-most trailing parser, if any; see module doc for details +--- precedence and category of the current left-most trailing parser, if any; see module doc for details (contPrec : Option Nat := none) +(contCat := Name.anonymous) -- current minimum precedence in this Pratt parser call, if any; see module doc for details (minPrec : Option Nat := none) -- precedence of the trailing Pratt parser call if any; see module doc for details @@ -130,9 +131,9 @@ KeyedDeclsAttribute.init { descr := "Register a parenthesizer for a syntax category. [parenthesizer cat] registers a declaration of type `Lean.PrettyPrinter.CategoryParenthesizer` for the category `cat`, -which is used when parenthesizing calls of `categoryParser cat prec`. Implementations should call `maybeParenthesize` with -the precedence and an appropriate parentheses builder. If no category parenthesizer is registered, the category will never be -parenthesized, but still be traversed for parenthesizing nested categories.", +which is used when parenthesizing calls of `categoryParser cat prec`. Implementations should call `maybeParenthesize` +with the precedence and `cat`. If no category parenthesizer is registered, the category will never be parenthesized, +but still be traversed for parenthesizing nested categories.", valueTypeName := `Lean.PrettyPrinter.CategoryParenthesizer, evalKey := fun _ env args => match attrParamSyntaxToIdentifier args with | some id => @@ -186,19 +187,19 @@ instance monadQuotation : MonadQuotation ParenthesizerM := { set_option class.instance_max_depth 100 -- TODO delete /-- Run `x` and parenthesize the result using `mkParen` if necessary. -/ -def maybeParenthesize (mkParen : Syntax → Syntax) (prec : Nat) (x : ParenthesizerM Unit) : ParenthesizerM Unit := do +def maybeParenthesize (cat : Name) (mkParen : Syntax → Syntax) (prec : Nat) (x : ParenthesizerM Unit) : ParenthesizerM Unit := do stx ← getCur; idx ← getIdx; st ← get; --- reset prec/prec and store `mkParen` for the recursive call +-- reset precs for the recursive call set { stxTrav := st.stxTrav : State }; -trace! `PrettyPrinter.parenthesize ("parenthesizing (contPrec := " ++ toString st.contPrec ++ ")" ++ MessageData.nest 2 (line ++ stx)); -adaptReader (fun (ctx : Context) => { ctx with mkParen := some mkParen }) x; +trace! `PrettyPrinter.parenthesize ("parenthesizing (cont := " ++ toString (st.contPrec, st.contCat) ++ ")" ++ MessageData.nest 2 (line ++ stx)); +x; { minPrec := some minPrec, trailPrec := trailPrec, .. } ← get | panic! "maybeParenthesize: visited a syntax tree without precedences?!"; -trace! `PrettyPrinter.parenthesize ("...precedences are " ++ fmt prec ++ " >? " ++ fmt minPrec ++ ", " ++ fmt trailPrec ++ " <=? " ++ fmt st.contPrec); +trace! `PrettyPrinter.parenthesize ("...precedences are " ++ fmt prec ++ " >? " ++ fmt minPrec ++ ", " ++ fmt (trailPrec, cat) ++ " <=? " ++ fmt (st.contPrec, st.contCat)); -- Should we parenthesize? -when (prec > minPrec || match trailPrec, st.contPrec with some trailPrec, some contPrec => trailPrec <= contPrec | _, _ => false) $ do { +when (prec > minPrec || match trailPrec, st.contPrec with some trailPrec, some contPrec => cat == st.contCat && trailPrec <= contPrec | _, _ => false) $ do { -- 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. @@ -215,7 +216,7 @@ when (prec > minPrec || match trailPrec, st.contPrec with some trailPrec, some c stx ← getCur; trace! `PrettyPrinter.parenthesize ("parenthesized: " ++ stx.formatStx none); goLeft; -- after parenthesization, there is no more trailing parser - modify (fun st => { st with contPrec := Parser.maxPrec, trailPrec := none }) + modify (fun st => { st with contPrec := Parser.maxPrec, contCat := cat, trailPrec := none }) }; { trailPrec := trailPrec, .. } ← get; -- If we already had a token at this level, keep the trailing parser. Otherwise, use the minimum of @@ -227,7 +228,7 @@ modify (fun stP => { stP with minPrec := st.minPrec, trailPrec := trailPrec }) /-- Adjust state and advance. -/ def visitToken : Parenthesizer := do -modify (fun st => { st with contPrec := none, visitedToken := true }); +modify (fun st => { st with contPrec := none, contCat := Name.anonymous, visitedToken := true }); goLeft @[combinatorParenthesizer Lean.Parser.orelse] def orelse.parenthesizer (p1 p2 : Parenthesizer) : Parenthesizer := do @@ -258,14 +259,16 @@ def withAntiquot.parenthesizer (antiP p : Parenthesizer) : Parenthesizer := -- fix the backtracking hack outright. orelse.parenthesizer antiP p -def parenthesizeCategoryCore (cat : Name) (prec : Nat) : Parenthesizer := do -stx ← getCur; -if stx.getKind == `choice then - visitArgs $ stx.getArgs.size.forM $ fun _ => do - stx ← getCur; - parenthesizerForKind stx.getKind -else - withAntiquot.parenthesizer (mkAntiquot.parenthesizer' cat.toString none) (parenthesizerForKind stx.getKind) +def parenthesizeCategoryCore (cat : Name) (prec : Nat) : Parenthesizer := +adaptReader (fun (ctx : Context) => { ctx with cat := cat }) do + stx ← getCur; + if stx.getKind == `choice then + visitArgs $ stx.getArgs.size.forM $ fun _ => do + stx ← getCur; + parenthesizerForKind stx.getKind + else + withAntiquot.parenthesizer (mkAntiquot.parenthesizer' cat.toString none) (parenthesizerForKind stx.getKind); + modify fun st => { st with contCat := cat } @[combinatorParenthesizer Lean.Parser.categoryParser] def categoryParser.parenthesizer (cat : Name) (prec : Nat) : Parenthesizer := do @@ -289,17 +292,17 @@ stx ← getCur; if stx.getKind == nullKind then throw $ Exception.other Syntax.missing "BACKTRACK" else do - maybeParenthesize (fun stx => Unhygienic.run `(($stx))) prec $ + maybeParenthesize `term (fun stx => Unhygienic.run `(($stx))) prec $ parenthesizeCategoryCore `term prec @[builtinCategoryParenthesizer tactic] def tactic.parenthesizer : CategoryParenthesizer | prec => do -maybeParenthesize (fun stx => Unhygienic.run `(tactic|($stx))) prec $ +maybeParenthesize `tactic (fun stx => Unhygienic.run `(tactic|($stx))) prec $ parenthesizeCategoryCore `tactic prec @[builtinCategoryParenthesizer level] def level.parenthesizer : CategoryParenthesizer | prec => do -maybeParenthesize (fun stx => Unhygienic.run `(level|($stx))) prec $ +maybeParenthesize `level (fun stx => Unhygienic.run `(level|($stx))) prec $ parenthesizeCategoryCore `level prec @[combinatorParenthesizer Lean.Parser.try] @@ -332,7 +335,7 @@ addPrecCheck prec def leadingNode.parenthesizer (k : SyntaxNodeKind) (prec : Nat) (p : Parenthesizer) : Parenthesizer := do node.parenthesizer k p; addPrecCheck prec; --- Limit `contPrec` to `maxPrec-1`. +-- Limit `cont` precedence to `maxPrec-1`. -- This is because `maxPrec-1` is the precedence of function application, which is the only way to turn a leading parser -- into a trailing one. modify fun st => { st with contPrec := Nat.min (Parser.maxPrec-1) prec } @@ -348,14 +351,13 @@ when (k != stx.getKind) $ do { visitArgs $ do { p; addPrecCheck prec; + ctx ← read; + modify fun st => { st with contCat := ctx.cat }; -- After visiting the nodes actually produced by the parser passed to `trailingNode`, we are positioned on the -- left-most child, which is the term injected by `trailingNode` in place of the recursion. Left recursion is not an -- issue for the parenthesizer, so we can think of this child being produced by `termParser 0`, or whichever Pratt - -- parser is calling us; we only need to know its `mkParen`, which we retrieve from the context. - { mkParen := some mkParen, .. } ← read - | panic! "trailingNode.parenthesizer called outside of maybeParenthesize call"; - maybeParenthesize mkParen 0 $ - categoryParser.parenthesizer `someCategory 0 + -- parser is calling us. + categoryParser.parenthesizer ctx.cat 0 } @[combinatorParenthesizer Lean.Parser.symbol] def symbol.parenthesizer := visitToken