From 4174643dbd395ec9ef1904e0c7e056c5adbbef94 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Sun, 1 May 2022 11:46:06 +0200 Subject: [PATCH] perf: optimize `withAntiquot` parenthesizer Doesn't look like we'll get rid of the backtracking anytime soon --- src/Lean/PrettyPrinter/Parenthesizer.lean | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/src/Lean/PrettyPrinter/Parenthesizer.lean b/src/Lean/PrettyPrinter/Parenthesizer.lean index 0f9b3cf148..73abed8bf7 100644 --- a/src/Lean/PrettyPrinter/Parenthesizer.lean +++ b/src/Lean/PrettyPrinter/Parenthesizer.lean @@ -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