From 8f01619c3d87a681de73ce4147a78709bfeb4f04 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Wed, 28 Oct 2020 10:11:45 +0100 Subject: [PATCH] perf: work around parser performance issue I forgot about and the speedcenter had to remind me of --- src/Lean/Parser/Extension.lean | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/Lean/Parser/Extension.lean b/src/Lean/Parser/Extension.lean index d5c5b6cd0e..7ea4a660b5 100644 --- a/src/Lean/Parser/Extension.lean +++ b/src/Lean/Parser/Extension.lean @@ -313,13 +313,17 @@ match getCategory (parserExtension.getState env).categories catName with def mkCategoryAntiquotParser (kind : Name) : Parser := mkAntiquot kind.toString none +-- helper decl to work around inlining issue https://github.com/leanprover/lean4/commit/3f6de2af06dd9a25f62294129f64bc05a29ea912#r41340377 +@[inline] private def mkCategoryAntiquotParserFn (kind : Name) : ParserFn := + (mkCategoryAntiquotParser kind).fn + def categoryParserFnImpl (catName : Name) : ParserFn := fun ctx s => let catName := if catName == `syntax then `stx else catName -- temporary Hack let categories := (parserExtension.getState ctx.env).categories match getCategory categories catName with | some cat => - prattParser catName cat.tables cat.leadingIdentAsSymbol (mkCategoryAntiquotParser catName).fn ctx s + prattParser catName cat.tables cat.leadingIdentAsSymbol (mkCategoryAntiquotParserFn catName) ctx s | none => s.mkUnexpectedError ("unknown parser category '" ++ toString catName ++ "'") @[builtinInit] def setCategoryParserFnRef : IO Unit :=