From 4279df417063a03500c7b47b81332cf74acfe698 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Sat, 1 Feb 2020 14:58:57 +0100 Subject: [PATCH] perf: special-case antiquotation syntax in Pratt parser to avoid choice nodes fixes #99 --- src/Init/Lean/Parser/Command.lean | 1 - src/Init/Lean/Parser/Parser.lean | 59 +++++++++++++++++-------------- src/Init/Lean/Parser/Term.lean | 1 - 3 files changed, 32 insertions(+), 29 deletions(-) diff --git a/src/Init/Lean/Parser/Command.lean b/src/Init/Lean/Parser/Command.lean index a888614230..9ff4656676 100644 --- a/src/Init/Lean/Parser/Command.lean +++ b/src/Init/Lean/Parser/Command.lean @@ -24,7 +24,6 @@ categoryParser `command rbp Multiple command will be put in a `null node, but a single command will not (so that you can directly match against a quotation in a command kind's elaborator). -/ @[builtinTermParser] def Term.stxQuot := parser! symbol "`(" appPrec >> (termParser <|> many1 commandParser true) >> ")" -@[builtinCommandParser] def Command.antiquot := (mkAntiquot "command" none true : Parser) namespace Command def commentBody : Parser := diff --git a/src/Init/Lean/Parser/Parser.lean b/src/Init/Lean/Parser/Parser.lean index d6d12610ac..525a2014e7 100644 --- a/src/Init/Lean/Parser/Parser.lean +++ b/src/Init/Lean/Parser/Parser.lean @@ -1364,8 +1364,8 @@ private def mkResult (s : ParserState) (iniSz : Nat) : ParserState := if s.stackSize == iniSz + 1 then s else s.mkNode nullKind iniSz -- throw error instead? -def leadingParser (kind : Name) (tables : PrattParsingTables) (leadingIdentAsSymbol : Bool) : ParserFn := -fun c s => +def leadingParser (kind : Name) (tables : PrattParsingTables) (preLeadingParser : Parser) (leadingIdentAsSymbol : Bool) : ParserFn := +orelseFn preLeadingParser.fn $ fun c s => let iniSz := s.stackSize; let (s, ps) := indexed tables.leadingTable c s leadingIdentAsSymbol; let ps := tables.leadingParsers ++ ps; @@ -1405,9 +1405,16 @@ partial def trailingLoop (tables : PrattParsingTables) (c : ParserContext) : Par let s := mkTrailingResult s iniSz; trailingLoop s -def prattParser (kind : Name) (tables : PrattParsingTables) (leadingIdentAsSymbol : Bool) : ParserFn := +/-- + Implements a recursive precedence parser according to Pratt's algorithm. + + `preLeadingParser` is a parser that is preferred over all other leading + parsers. We use it to inject the antiquotation parser into syntax categories. + It should not be added to the regular leading parsers because it would heavily + overlap with antiquotation parsers nested inside them. -/ +def prattParser (kind : Name) (tables : PrattParsingTables) (preLeadingParser : Parser) (leadingIdentAsSymbol : Bool) : ParserFn := fun c s => - let s := leadingParser kind tables leadingIdentAsSymbol c s; + let s := leadingParser kind tables preLeadingParser leadingIdentAsSymbol c s; if s.hasError then s else trailingLoop tables c s @@ -1784,22 +1791,23 @@ match (parserExtension.getState env).categories.find? catName with | none => false | some cat => cat.leadingIdentAsSymbol -def categoryParserFnImplAux (catName : Name) : ParserFn := -fun ctx s => - let categories := (parserExtension.getState ctx.env).categories; - match categories.find? catName with - | some cat => prattParser catName cat.tables cat.leadingIdentAsSymbol ctx s - | none => s.mkUnexpectedError ("unknown parser category '" ++ toString catName ++ "'") - private def catNameToString : Name → String | Name.str Name.anonymous s _ => s | n => n.toString def categoryParserFnImpl (catName : Name) : ParserFn := -if catName != `term then - orelseFn (mkAntiquot (catNameToString catName) none false).fn (categoryParserFnImplAux catName) -else - categoryParserFnImplAux catName +fun ctx s => + let categories := (parserExtension.getState ctx.env).categories; + match categories.find? catName with + | some cat => + -- allow "anonymous" antiquotations `$x` for the `term` category only + -- TODO: make customizable + -- one good example for a category that should not be anonymous is + -- `index` in `tests/lean/run/bigop.lean`. + let anonAntiquot := catName == `term; + let preP := mkAntiquot (catNameToString catName) none anonAntiquot; + prattParser catName cat.tables preP cat.leadingIdentAsSymbol ctx s + | none => s.mkUnexpectedError ("unknown parser category '" ++ toString catName ++ "'") @[init] def setCategoryParserFnRef : IO Unit := categoryParserFnRef.set categoryParserFnImpl @@ -1838,19 +1846,16 @@ def mkParserContext (env : Environment) (ctx : InputContext) : ParserContext := def mkParserState (input : String) : ParserState := { cache := initCacheForInput input } +/- convenience function for testing -/ def runParserCategory (env : Environment) (catName : Name) (input : String) (fileName := "") : Except String Syntax := -let categories := (parserExtension.getState env).categories; -match categories.find? catName with -| some cat => - let c := mkParserContext env (mkInputContext input fileName); - let s := mkParserState input; - let s := whitespace c s; - let s := prattParser catName cat.tables cat.leadingIdentAsSymbol c s; - if s.hasError then - Except.error (s.toErrorMsg c) - else - Except.ok s.stxStack.back -| none => throwUnknownParserCategory catName +let c := mkParserContext env (mkInputContext input fileName); +let s := mkParserState input; +let s := whitespace c s; +let s := categoryParserFnImpl catName c s; +if s.hasError then + Except.error (s.toErrorMsg c) +else + Except.ok s.stxStack.back def declareBuiltinParser (env : Environment) (addFnName : Name) (catName : Name) (declName : Name) : IO Environment := let name := `_regBuiltinParser ++ declName; diff --git a/src/Init/Lean/Parser/Term.lean b/src/Init/Lean/Parser/Term.lean index 0e6a51ed17..2f2e60ab33 100644 --- a/src/Init/Lean/Parser/Term.lean +++ b/src/Init/Lean/Parser/Term.lean @@ -98,7 +98,6 @@ withPosition $ fun pos => @[builtinTermParser] def borrowed := parser! symbol "@&" appPrec >> termParser (appPrec - 1) @[builtinTermParser] def quotedName := parser! nameLit -- NOTE: syntax quotations are defined in Init.Lean.Parser.Command -@[builtinTermParser] def antiquot := (mkAntiquot "term" none true : Parser) @[builtinTermParser] def «match_syntax» := parser! "match_syntax" >> termParser >> " with " >> matchAlts /- Remark: we use `checkWsBefore` to ensure `let x[i] := e; b` is not parsed as `let x [i] := e; b` where `[i]` is an `instBinder`. -/