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

chore: improve pretty printer traces, avoid recursion

Browse source
This commit is contained in:
Sebastian Ullrich 2020-11-17 12:11:53 +01:00
parent 45a315d273
commit 6126fd6388
2 changed files with 13 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -175,6 +175,7 @@ def withAntiquot.formatter (antiP p : Formatter) : Formatter :=
@[combinatorFormatter Lean.Parser.categoryParser]
def categoryParser.formatter (cat : Name) : Formatter := group $ indent do
let stx ← getCur
trace[PrettyPrinter.format]! "formatting {MessageData.nest 2 (Format.line ++ fmt stx)}"
if stx.getKind == `choice then
visitArgs do
let stx ← getCur;
@ -266,7 +267,7 @@ def symbol.formatter (sym : String) : Formatter := do
pushToken sym;
goLeft
else do
trace[PrettyPrinter.format.backtrack]! "unexpected syntax '{stx}', expected symbol '{sym}'"
trace[PrettyPrinter.format.backtrack]! "unexpected syntax '{fmt stx}', expected symbol '{sym}'"
throwBacktrack
@[combinatorFormatter Lean.Parser.nonReservedSymbol] def nonReservedSymbol.formatter := symbol.formatter
@ -453,13 +454,14 @@ end Formatter
open Formatter
def format (formatter : Formatter) (stx : Syntax) : CoreM Format := do
let options ← getOptions
let table ← Parser.builtinTokenTable.get
catchInternalId backtrackExceptionId
(do
let (_, st) ← (concat formatter { table := table, options := options }).run { stxTrav := Syntax.Traverser.fromSyntax stx };
pure $ Format.fill $ st.stack.get! 0)
(fun _ => throwError "format: uncaught backtrack exception")
trace[PrettyPrinter.format.input]! "{fmt stx}"
let options ← getOptions
let table ← Parser.builtinTokenTable.get
catchInternalId backtrackExceptionId
(do
let (_, st) ← (concat formatter { table := table, options := options }).run { stxTrav := Syntax.Traverser.fromSyntax stx };
pure $ Format.fill $ st.stack.get! 0)
(fun _ => throwError "format: uncaught backtrack exception")
def formatTerm := format $ categoryParser.formatter `term
def formatCommand := format $ categoryParser.formatter `command

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

@ -208,7 +208,7 @@ def maybeParenthesize (cat : Name) (canJuxtapose : Bool) (mkParen : Syntax → S
let st ← get
-- reset precs for the recursive call
set { stxTrav := st.stxTrav : State }
trace[PrettyPrinter.parenthesize]! "parenthesizing (cont := {(st.contPrec, st.contCat)}){MessageData.nest 2 (line ++ stx)}"
trace[PrettyPrinter.parenthesize]! "parenthesizing (cont := {(st.contPrec, st.contCat)}){MessageData.nest 2 (line ++ fmt stx)}"
x
let { minPrec := some minPrec, trailPrec := trailPrec, trailCat := trailCat, .. } ← get
| panic! "maybeParenthesize: visited a syntax tree without precedences?!"
@ -532,7 +532,8 @@ end Parenthesizer
open Parenthesizer
/-- Add necessary parentheses in `stx` parsed by `parser`. -/
def parenthesize (parenthesizer : Parenthesizer) (stx : Syntax) : CoreM Syntax :=
def parenthesize (parenthesizer : Parenthesizer) (stx : Syntax) : CoreM Syntax := do
trace[PrettyPrinter.parenthesize.input]! "{fmt stx}"
catchInternalId backtrackExceptionId
(do
let (_, st) ← (parenthesizer {}).run { stxTrav := Syntax.Traverser.fromSyntax stx }