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

perf: optimize withAntiquot parenthesizer

Browse source 
Doesn't look like we'll get rid of the backtracking anytime soon
This commit is contained in:
Sebastian Ullrich 2022-05-01 11:46:06 +02:00
parent fa943d3864
commit 4174643dbd
1 changed files with 7 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -279,10 +279,13 @@ unsafe def parenthesizerForKindUnsafe (k : SyntaxNodeKind) : Parenthesizer := do
constant parenthesizerForKind (k : SyntaxNodeKind) : Parenthesizer
@[combinatorParenthesizer Lean.Parser.withAntiquot]
def withAntiquot.parenthesizer (antiP p : Parenthesizer) : Parenthesizer :=
-- TODO: could be optimized using `isAntiquot` (which would have to be moved), but I'd rather
-- fix the backtracking hack outright.
orelse.parenthesizer antiP p
def withAntiquot.parenthesizer (antiP p : Parenthesizer) : Parenthesizer := do
let stx ← getCur
-- early check as minor optimization that also cleans up the backtrack traces
if stx.isAntiquot || stx.isAntiquotSplice then
orelse.parenthesizer antiP p
else
p
@[combinatorParenthesizer Lean.Parser.withAntiquotSuffixSplice]
def withAntiquotSuffixSplice.parenthesizer (k : SyntaxNodeKind) (p suffix : Parenthesizer) : Parenthesizer := do