From b8ebfbfecc88b999cabcf176cf1696e8b0348d35 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Mon, 17 Oct 2022 12:57:50 +0200 Subject: [PATCH] chore: improve pretty printer antiquotation support --- src/Lean/Parser.lean | 6 ++++-- src/Lean/PrettyPrinter/Formatter.lean | 16 ++++++++++++---- src/Lean/PrettyPrinter/Parenthesizer.lean | 19 ++++++++++++------- 3 files changed, 28 insertions(+), 13 deletions(-) diff --git a/src/Lean/Parser.lean b/src/Lean/Parser.lean index c831c224c1..8b3683a998 100644 --- a/src/Lean/Parser.lean +++ b/src/Lean/Parser.lean @@ -76,7 +76,8 @@ unsafe def interpretParserDescr : ParserDescr → CoreM Parenthesizer | ParserDescr.unary n d => return (← getUnaryAlias parenthesizerAliasesRef n) (← interpretParserDescr d) | ParserDescr.binary n d₁ d₂ => return (← getBinaryAlias parenthesizerAliasesRef n) (← interpretParserDescr d₁) (← interpretParserDescr d₂) | ParserDescr.node k prec d => return leadingNode.parenthesizer k prec (← interpretParserDescr d) - | ParserDescr.nodeWithAntiquot _ k d => return node.parenthesizer k (← interpretParserDescr d) + | ParserDescr.nodeWithAntiquot n k d => return withAntiquot.parenthesizer (mkAntiquot.parenthesizer' n k (anonymous := true)) <| + node.parenthesizer k (← interpretParserDescr d) | ParserDescr.sepBy p sep psep trail => return sepBy.parenthesizer (← interpretParserDescr p) sep (← interpretParserDescr psep) trail | ParserDescr.sepBy1 p sep psep trail => return sepBy1.parenthesizer (← interpretParserDescr p) sep (← interpretParserDescr psep) trail | ParserDescr.trailingNode k prec lhsPrec d => return trailingNode.parenthesizer k prec lhsPrec (← interpretParserDescr d) @@ -107,7 +108,8 @@ unsafe def interpretParserDescr : ParserDescr → CoreM Formatter | ParserDescr.unary n d => return (← getUnaryAlias formatterAliasesRef n) (← interpretParserDescr d) | ParserDescr.binary n d₁ d₂ => return (← getBinaryAlias formatterAliasesRef n) (← interpretParserDescr d₁) (← interpretParserDescr d₂) | ParserDescr.node k _ d => return node.formatter k (← interpretParserDescr d) - | ParserDescr.nodeWithAntiquot _ k d => return node.formatter k (← interpretParserDescr d) + | ParserDescr.nodeWithAntiquot n k d => return withAntiquot.formatter (mkAntiquot.formatter' n k (anonymous := true)) <| + node.formatter k (← interpretParserDescr d) | ParserDescr.sepBy p sep psep trail => return sepBy.formatter (← interpretParserDescr p) sep (← interpretParserDescr psep) trail | ParserDescr.sepBy1 p sep psep trail => return sepBy1.formatter (← interpretParserDescr p) sep (← interpretParserDescr psep) trail | ParserDescr.trailingNode k prec lhsPrec d => return trailingNode.formatter k prec lhsPrec (← interpretParserDescr d) diff --git a/src/Lean/PrettyPrinter/Formatter.lean b/src/Lean/PrettyPrinter/Formatter.lean index 4774077246..87c613c1b0 100644 --- a/src/Lean/PrettyPrinter/Formatter.lean +++ b/src/Lean/PrettyPrinter/Formatter.lean @@ -173,10 +173,18 @@ def withMaybeTag (pos? : Option String.Pos) (x : FormatterM Unit) : Formatter := else x -@[combinator_formatter orelse] def orelse.formatter (p1 p2 : Formatter) : Formatter := - -- HACK: We have no (immediate) information on which side of the orelse could have produced the current node, so try - -- them in turn. Uses the syntax traverser non-linearly! - p1 <|> p2 +@[combinator_formatter orelse] partial def orelse.formatter (p1 p2 : Formatter) : Formatter := do + let stx ← getCur + -- `orelse` may produce `choice` nodes for antiquotations + if stx.getKind == `choice then + visitArgs do + -- format only last choice + -- TODO: We could use elaborator data here to format the chosen child when available + orelse.formatter p1 p2 + else + -- HACK: We have no (immediate) information on which side of the orelse could have produced the current node, so try + -- them in turn. Uses the syntax traverser non-linearly! + p1 <|> p2 -- `mkAntiquot` is quite complex, so we'd rather have its formatter synthesized below the actual parser definition. -- Note that there is a mutual recursion diff --git a/src/Lean/PrettyPrinter/Parenthesizer.lean b/src/Lean/PrettyPrinter/Parenthesizer.lean index fd7646c5d2..1ff7eae7bd 100644 --- a/src/Lean/PrettyPrinter/Parenthesizer.lean +++ b/src/Lean/PrettyPrinter/Parenthesizer.lean @@ -247,10 +247,16 @@ def visitToken : Parenthesizer := do modify fun st => { st with contPrec := none, contCat := Name.anonymous, visitedToken := true } goLeft -@[combinator_parenthesizer orelse] def orelse.parenthesizer (p1 p2 : Parenthesizer) : Parenthesizer := do - -- HACK: We have no (immediate) information on which side of the orelse could have produced the current node, so try - -- them in turn. Uses the syntax traverser non-linearly! - p1 <|> p2 +@[combinator_parenthesizer orelse] partial def orelse.parenthesizer (p1 p2 : Parenthesizer) : Parenthesizer := do + let stx ← getCur + -- `orelse` may produce `choice` nodes for antiquotations + if stx.getKind == `choice then + visitArgs $ stx.getArgs.size.forM fun _ => do + orelse.parenthesizer p1 p2 + else + -- HACK: We have no (immediate) information on which side of the orelse could have produced the current node, so try + -- them in turn. Uses the syntax traverser non-linearly! + p1 <|> p2 -- `mkAntiquot` is quite complex, so we'd rather have its parenthesizer synthesized below the actual parser definition. -- Note that there is a mutual recursion @@ -299,13 +305,12 @@ def tokenWithAntiquot.parenthesizer (p : Parenthesizer) : Parenthesizer := do else p -def parenthesizeCategoryCore (cat : Name) (_prec : Nat) : Parenthesizer := +partial def parenthesizeCategoryCore (cat : Name) (_prec : Nat) : Parenthesizer := withReader (fun ctx => { ctx with cat := cat }) do let stx ← getCur if stx.getKind == `choice then visitArgs $ stx.getArgs.size.forM fun _ => do - let stx ← getCur - parenthesizerForKind stx.getKind + parenthesizeCategoryCore cat _prec else withAntiquot.parenthesizer (mkAntiquot.parenthesizer' cat.toString cat (isPseudoKind := true)) (parenthesizerForKind stx.getKind) modify fun st => { st with contCat := cat }