max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: improve pretty printer antiquotation support

Browse source
This commit is contained in:
Sebastian Ullrich 2022-10-17 12:57:50 +02:00
parent 5f38a483f2
commit b8ebfbfecc
3 changed files with 28 additions and 13 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/Lean/Parser.lean
View file

@ -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)

16
src/Lean/PrettyPrinter/Formatter.lean
View file

@ -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

19
src/Lean/PrettyPrinter/Parenthesizer.lean
View file

@ -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 }