Basic Lean parser infrastructure

The Lean parser was developed with the following primary goals in mind:

• flexibility: Lean's grammar is complex and includes indentation and other whitespace sensitivity. It should be possible to introduce such custom "tweaks" locally without having to adjust the fundamental parsing approach.
• extensibility: Lean's grammar can be extended on the fly within a Lean file, and with Lean 4 we want to extend this to cover embedding domain-specific languages that may look nothing like Lean, down to using a separate set of tokens.
• losslessness: The parser should produce a concrete syntax tree that preserves all whitespace and other "sub-token" information for the use in tooling.
• performance: The overhead of the parser building blocks, and the overall parser performance on average-complexity input, should be comparable with that of the previous parser hand-written in C++. No fancy optimizations should be necessary for this.

Given these constraints, we decided to implement a combinatoric, non-monadic, lexer-less, memoizing recursive-descent parser. Using combinators instead of some more formal and introspectible grammar representation ensures ultimate flexibility as well as efficient extensibility: there is (almost) no pre-processing necessary when extending the grammar with a new parser. However, because all the results the combinators produce are of the homogeneous Syntax type, the basic parser type is not actually a monad but a monomorphic linear function ParserState → ParserState, avoiding constructing and deconstructing countless monadic return values. Instead of explicitly returning syntax objects, parsers push (zero or more of) them onto a syntax stack inside the linear state. Chaining parsers via >> accumulates their output on the stack. Combinators such as node then pop off all syntax objects produced during their invocation and wrap them in a single Syntax.node object that is again pushed on this stack. Instead of calling node directly, we usually use the macro leading_parser p, which unfolds to node k p where the new syntax node kind k is the name of the declaration being defined.

The lack of a dedicated lexer ensures we can modify and replace the lexical grammar at any point, and simplifies detecting and propagating whitespace. The parser still has a concept of "tokens", however, and caches the most recent one for performance: when tokenFn is called twice at the same position in the input, it will reuse the result of the first call. tokenFn recognizes some built-in variable-length tokens such as identifiers as well as any fixed token in the ParserContext's TokenTable (a trie); however, the same cache field and strategy could be reused by custom token parsers. Tokens also play a central role in the prattParser combinator, which selects a leading parser followed by zero or more trailing parsers based on the current token (via peekToken); see the documentation of prattParser for more details. Tokens are specified via the symbol parser, or with symbolNoWs for tokens that should not be preceded by whitespace.

The Parser type is extended with additional metadata over the mere parsing function to propagate token information: collectTokens collects all tokens within a parser for registering. firstTokens holds information about the "FIRST" token set used to speed up parser selection in prattParser. This approach of combining static and dynamic information in the parser type is inspired by the paper "Deterministic, Error-Correcting Combinator Parsers" by Swierstra and Duponcheel. If multiple parsers accept the same current token, prattParser tries all of them using the backtracking longestMatchFn combinator. This is the only case where standard parsers might execute arbitrary backtracking. Repeated invocations of the same category or concrete parser at the same position are cached where possible; see withCache.

Finally, error reporting follows the standard combinatoric approach of collecting a single unexpected token/... and zero or more expected tokens (see Error below). Expected tokens are e.g. set by symbol and merged by <|>. Combinators running multiple parsers should check if an error message is set in the parser state (hasError) and act accordingly. Error recovery is left to the designer of the specific language; for example, Lean's top-level parseCommand loop skips tokens until the next command keyword on error.

def Lean.Parser.dbgTraceStateFn (label : String) (p : Lean.Parser.ParserFn) : Lean.Parser.ParserFn

def Lean.Parser.dbgTraceState (label : String) : Lean.Parser.Parser → Lean.Parser.Parser

@[noinline]

def Lean.Parser.epsilonInfo : Lean.Parser.ParserInfo

def Lean.Parser.checkStackTopFn (p : Lean.Syntax → Bool) (msg : String) : Lean.Parser.ParserFn

def Lean.Parser.checkStackTop (p : Lean.Syntax → Bool) (msg : String) : Lean.Parser.Parser

def Lean.Parser.andthenFn (p : Lean.Parser.ParserFn) (q : Lean.Parser.ParserFn) : Lean.Parser.ParserFn

@[noinline]

def Lean.Parser.andthenInfo (p : Lean.Parser.ParserInfo) (q : Lean.Parser.ParserInfo) : Lean.Parser.ParserInfo

def Lean.Parser.andthen (p : Lean.Parser.Parser) (q : Lean.Parser.Parser) : Lean.Parser.Parser

instance Lean.Parser.instAndThenParser : AndThen Lean.Parser.Parser

def Lean.Parser.nodeFn (n : Lean.SyntaxNodeKind) (p : Lean.Parser.ParserFn) : Lean.Parser.ParserFn

def Lean.Parser.trailingNodeFn (n : Lean.SyntaxNodeKind) (p : Lean.Parser.ParserFn) : Lean.Parser.ParserFn

@[noinline]

def Lean.Parser.nodeInfo (n : Lean.SyntaxNodeKind) (p : Lean.Parser.ParserInfo) : Lean.Parser.ParserInfo

def Lean.Parser.node (n : Lean.SyntaxNodeKind) (p : Lean.Parser.Parser) : Lean.Parser.Parser

def Lean.Parser.errorFn (msg : String) : Lean.Parser.ParserFn

def Lean.Parser.error (msg : String) : Lean.Parser.Parser

def Lean.Parser.errorAtSavedPosFn (msg : String) (delta : Bool) : Lean.Parser.ParserFn

def Lean.Parser.errorAtSavedPos (msg : String) (delta : Bool) : Lean.Parser.Parser

Generate an error at the position saved with the withPosition combinator. If delta == true, then it reports at saved position+1. This useful to make sure a parser consumed at least one character.

def Lean.Parser.checkPrecFn (prec : Nat) : Lean.Parser.ParserFn

Succeeds if c.prec <= prec

def Lean.Parser.checkPrec (prec : Nat) : Lean.Parser.Parser

def Lean.Parser.checkLhsPrecFn (prec : Nat) : Lean.Parser.ParserFn

Succeeds if c.lhsPrec >= prec

def Lean.Parser.checkLhsPrec (prec : Nat) : Lean.Parser.Parser

def Lean.Parser.setLhsPrecFn (prec : Nat) : Lean.Parser.ParserFn

def Lean.Parser.setLhsPrec (prec : Nat) : Lean.Parser.Parser

def Lean.Parser.incQuotDepth (p : Lean.Parser.Parser) : Lean.Parser.Parser

def Lean.Parser.decQuotDepth (p : Lean.Parser.Parser) : Lean.Parser.Parser

def Lean.Parser.suppressInsideQuot : Lean.Parser.Parser → Lean.Parser.Parser

def Lean.Parser.leadingNode (n : Lean.SyntaxNodeKind) (prec : Nat) (p : Lean.Parser.Parser) : Lean.Parser.Parser

def Lean.Parser.trailingNodeAux (n : Lean.SyntaxNodeKind) (p : Lean.Parser.Parser) : Lean.Parser.TrailingParser

def Lean.Parser.trailingNode (n : Lean.SyntaxNodeKind) (prec : Nat) (lhsPrec : Nat) (p : Lean.Parser.Parser) : Lean.Parser.TrailingParser

def Lean.Parser.mergeOrElseErrors (s : Lean.Parser.ParserState) (error1 : Lean.Parser.Error) (iniPos : String.Pos) (mergeErrors : Bool) : Lean.Parser.ParserState

inductive Lean.Parser.OrElseOnAntiquotBehavior : Type

• acceptLhs: Lean.Parser.OrElseOnAntiquotBehavior
• takeLongest: Lean.Parser.OrElseOnAntiquotBehavior
• merge: Lean.Parser.OrElseOnAntiquotBehavior

instance Lean.Parser.instBEqOrElseOnAntiquotBehavior : BEq Lean.Parser.OrElseOnAntiquotBehavior

def Lean.Parser.orelseFnCore (p : Lean.Parser.ParserFn) (q : Lean.Parser.ParserFn) (antiquotBehavior : optParam Lean.Parser.OrElseOnAntiquotBehavior Lean.Parser.OrElseOnAntiquotBehavior.merge) : Lean.Parser.ParserFn

def Lean.Parser.orelseFn (p : Lean.Parser.ParserFn) (q : Lean.Parser.ParserFn) : Lean.Parser.ParserFn

@[noinline]

def Lean.Parser.orelseInfo (p : Lean.Parser.ParserInfo) (q : Lean.Parser.ParserInfo) : Lean.Parser.ParserInfo

def Lean.Parser.orelse (p : Lean.Parser.Parser) (q : Lean.Parser.Parser) : Lean.Parser.Parser

Run p, falling back to q if p failed without consuming any input.

NOTE: In order for the pretty printer to retrace an orelse, p must be a call to node or some other parser producing a single node kind. Nested orelse calls are flattened for this, i.e. (node k1 p1 <|> node k2 p2) <|> ... is fine as well.

instance Lean.Parser.instOrElseParser : OrElse Lean.Parser.Parser

@[noinline]

def Lean.Parser.noFirstTokenInfo (info : Lean.Parser.ParserInfo) : Lean.Parser.ParserInfo

def Lean.Parser.atomicFn (p : Lean.Parser.ParserFn) : Lean.Parser.ParserFn

def Lean.Parser.atomic : Lean.Parser.Parser → Lean.Parser.Parser

def Lean.Parser.optionalFn (p : Lean.Parser.ParserFn) : Lean.Parser.ParserFn

@[noinline]

def Lean.Parser.optionaInfo (p : Lean.Parser.ParserInfo) : Lean.Parser.ParserInfo

def Lean.Parser.optionalNoAntiquot (p : Lean.Parser.Parser) : Lean.Parser.Parser

def Lean.Parser.lookaheadFn (p : Lean.Parser.ParserFn) : Lean.Parser.ParserFn

def Lean.Parser.lookahead : Lean.Parser.Parser → Lean.Parser.Parser

def Lean.Parser.notFollowedByFn (p : Lean.Parser.ParserFn) (msg : String) : Lean.Parser.ParserFn

def Lean.Parser.notFollowedBy (p : Lean.Parser.Parser) (msg : String) : Lean.Parser.Parser

partial def Lean.Parser.manyAux (p : Lean.Parser.ParserFn) : Lean.Parser.ParserFn

def Lean.Parser.manyFn (p : Lean.Parser.ParserFn) : Lean.Parser.ParserFn

def Lean.Parser.manyNoAntiquot (p : Lean.Parser.Parser) : Lean.Parser.Parser

def Lean.Parser.many1Fn (p : Lean.Parser.ParserFn) : Lean.Parser.ParserFn

def Lean.Parser.many1NoAntiquot : Lean.Parser.Parser → Lean.Parser.Parser

def Lean.Parser.sepByFn (allowTrailingSep : Bool) (p : Lean.Parser.ParserFn) (sep : Lean.Parser.ParserFn) : Lean.Parser.ParserFn

def Lean.Parser.sepBy1Fn (allowTrailingSep : Bool) (p : Lean.Parser.ParserFn) (sep : Lean.Parser.ParserFn) : Lean.Parser.ParserFn

@[noinline]

def Lean.Parser.sepByInfo (p : Lean.Parser.ParserInfo) (sep : Lean.Parser.ParserInfo) : Lean.Parser.ParserInfo

@[noinline]

def Lean.Parser.sepBy1Info (p : Lean.Parser.ParserInfo) (sep : Lean.Parser.ParserInfo) : Lean.Parser.ParserInfo

def Lean.Parser.sepByNoAntiquot (p : Lean.Parser.Parser) (sep : Lean.Parser.Parser) (allowTrailingSep : optParam Bool false) : Lean.Parser.Parser

def Lean.Parser.sepBy1NoAntiquot (p : Lean.Parser.Parser) (sep : Lean.Parser.Parser) (allowTrailingSep : optParam Bool false) : Lean.Parser.Parser

def Lean.Parser.withResultOfFn (p : Lean.Parser.ParserFn) (f : Lean.Syntax → Lean.Syntax) : Lean.Parser.ParserFn

Apply f to the syntax object produced by p

@[noinline]

def Lean.Parser.withResultOfInfo (p : Lean.Parser.ParserInfo) : Lean.Parser.ParserInfo

def Lean.Parser.withResultOf (p : Lean.Parser.Parser) (f : Lean.Syntax → Lean.Syntax) : Lean.Parser.Parser

def Lean.Parser.many1Unbox (p : Lean.Parser.Parser) : Lean.Parser.Parser

def Lean.Parser.satisfyFn (p : Char → Bool) (errorMsg : optParam String "unexpected character") : Lean.Parser.ParserFn

partial def Lean.Parser.takeUntilFn (p : Char → Bool) : Lean.Parser.ParserFn

def Lean.Parser.takeWhileFn (p : Char → Bool) : Lean.Parser.ParserFn

def Lean.Parser.takeWhile1Fn (p : Char → Bool) (errorMsg : String) : Lean.Parser.ParserFn

partial def Lean.Parser.finishCommentBlock (pushMissingOnError : Bool) (nesting : Nat) : Lean.Parser.ParserFn

def Lean.Parser.finishCommentBlock.eoi (pushMissingOnError : Bool) (s : Lean.Parser.ParserState) : Lean.Parser.ParserState

partial def Lean.Parser.whitespace : Lean.Parser.ParserFn

Consume whitespace and comments

def Lean.Parser.mkEmptySubstringAt (s : String) (p : String.Pos) : Substring

def Lean.Parser.rawFn (p : Lean.Parser.ParserFn) (trailingWs : optParam Bool false) : Lean.Parser.ParserFn

Match an arbitrary Parser and return the consumed String in a Syntax.atom.

def Lean.Parser.chFn (c : Char) (trailingWs : optParam Bool false) : Lean.Parser.ParserFn

def Lean.Parser.rawCh (c : Char) (trailingWs : optParam Bool false) : Lean.Parser.Parser

def Lean.Parser.hexDigitFn : Lean.Parser.ParserFn

def Lean.Parser.quotedCharCoreFn (isQuotable : Char → Bool) : Lean.Parser.ParserFn

def Lean.Parser.isQuotableCharDefault (c : Char) : Bool

def Lean.Parser.quotedCharFn : Lean.Parser.ParserFn

def Lean.Parser.mkNodeToken (n : Lean.SyntaxNodeKind) (startPos : String.Pos) : Lean.Parser.ParserFn

Push (Syntax.node tk ) onto syntax stack if parse was successful.

def Lean.Parser.charLitFnAux (startPos : String.Pos) : Lean.Parser.ParserFn

partial def Lean.Parser.strLitFnAux (startPos : String.Pos) : Lean.Parser.ParserFn

def Lean.Parser.decimalNumberFn (startPos : String.Pos) (c : Lean.Parser.ParserContext) : Lean.Parser.ParserState → Lean.Parser.ParserState

def Lean.Parser.decimalNumberFn.parseOptDot (c : Lean.Parser.ParserContext) (s : Lean.Parser.ParserState) : Lean.Parser.ParserState

def Lean.Parser.decimalNumberFn.parseOptExp (c : Lean.Parser.ParserContext) (s : Lean.Parser.ParserState) : Lean.Parser.ParserState

def Lean.Parser.binNumberFn (startPos : String.Pos) : Lean.Parser.ParserFn

def Lean.Parser.octalNumberFn (startPos : String.Pos) : Lean.Parser.ParserFn

def Lean.Parser.hexNumberFn (startPos : String.Pos) : Lean.Parser.ParserFn

def Lean.Parser.numberFnAux : Lean.Parser.ParserFn

def Lean.Parser.isIdCont : String → Lean.Parser.ParserState → Bool

def Lean.Parser.mkTokenAndFixPos (startPos : String.Pos) (tk : Option Lean.Parser.Token) : Lean.Parser.ParserFn

def Lean.Parser.mkIdResult (startPos : String.Pos) (tk : Option Lean.Parser.Token) (val : Lake.Name) : Lean.Parser.ParserFn

def Lean.Parser.identFnAux (startPos : String.Pos) (tk : Option Lean.Parser.Token) (r : Lake.Name) : Lean.Parser.ParserFn

partial def Lean.Parser.identFnAux.parse (startPos : String.Pos) (tk : Option Lean.Parser.Token) (r : Lake.Name) (c : Lean.Parser.ParserContext) (s : Lean.Parser.ParserState) : Lean.Parser.ParserState

def Lean.Parser.tokenFn (expected : optParam (List String) []) : Lean.Parser.ParserFn

def Lean.Parser.peekTokenAux (c : Lean.Parser.ParserContext) (s : Lean.Parser.ParserState) : Lean.Parser.ParserState × Except Lean.Parser.ParserState Lean.Syntax

def Lean.Parser.peekToken (c : Lean.Parser.ParserContext) (s : Lean.Parser.ParserState) : Lean.Parser.ParserState × Except Lean.Parser.ParserState Lean.Syntax

def Lean.Parser.rawIdentFn : Lean.Parser.ParserFn

Treat keywords as identifiers.

def Lean.Parser.satisfySymbolFn (p : String → Bool) (expected : List String) : Lean.Parser.ParserFn

def Lean.Parser.symbolFnAux (sym : String) (errorMsg : String) : Lean.Parser.ParserFn

def Lean.Parser.symbolInfo (sym : String) : Lean.Parser.ParserInfo

def Lean.Parser.symbolFn (sym : String) : Lean.Parser.ParserFn

def Lean.Parser.symbolNoAntiquot (sym : String) : Lean.Parser.Parser

def Lean.Parser.checkTailNoWs (prev : Lean.Syntax) : Bool

def Lean.Parser.nonReservedSymbolFnAux (sym : String) (errorMsg : String) : Lean.Parser.ParserFn

Check if the following token is the symbol or identifier sym. Useful for parsing local tokens that have not been added to the token table (but may have been so by some unrelated code).

For example, the universe max Function is parsed using this combinator so that it can still be used as an identifier outside of universe (but registering it as a token in a Term Syntax would not break the universe Parser).

def Lean.Parser.nonReservedSymbolFn (sym : String) : Lean.Parser.ParserFn

def Lean.Parser.nonReservedSymbolInfo (sym : String) (includeIdent : Bool) : Lean.Parser.ParserInfo

def Lean.Parser.nonReservedSymbolNoAntiquot (sym : String) (includeIdent : optParam Bool false) : Lean.Parser.Parser

def Lean.Parser.strAux (sym : String) (errorMsg : String) (j : String.Pos) : Lean.Parser.ParserFn

partial def Lean.Parser.strAux.parse (sym : String) (errorMsg : String) (j : String.Pos) (c : Lean.Parser.ParserContext) (s : Lean.Parser.ParserState) : Lean.Parser.ParserState

def Lean.Parser.checkTailWs (prev : Lean.Syntax) : Bool

def Lean.Parser.checkWsBeforeFn (errorMsg : String) : Lean.Parser.ParserFn

def Lean.Parser.checkWsBefore (errorMsg : optParam String "space before") : Lean.Parser.Parser

def Lean.Parser.checkTailLinebreak (prev : Lean.Syntax) : Bool

def Lean.Parser.checkLinebreakBeforeFn (errorMsg : String) : Lean.Parser.ParserFn

def Lean.Parser.checkLinebreakBefore (errorMsg : optParam String "line break") : Lean.Parser.Parser

def Lean.Parser.checkNoWsBeforeFn (errorMsg : String) : Lean.Parser.ParserFn

def Lean.Parser.checkNoWsBefore (errorMsg : optParam String "no space before") : Lean.Parser.Parser

def Lean.Parser.unicodeSymbolFnAux (sym : String) (asciiSym : String) (expected : List String) : Lean.Parser.ParserFn

def Lean.Parser.unicodeSymbolInfo (sym : String) (asciiSym : String) : Lean.Parser.ParserInfo

def Lean.Parser.unicodeSymbolFn (sym : String) (asciiSym : String) : Lean.Parser.ParserFn

def Lean.Parser.unicodeSymbolNoAntiquot (sym : String) (asciiSym : String) : Lean.Parser.Parser

def Lean.Parser.mkAtomicInfo (k : String) : Lean.Parser.ParserInfo

def Lean.Parser.numLitFn : Lean.Parser.ParserFn

def Lean.Parser.numLitNoAntiquot : Lean.Parser.Parser

def Lean.Parser.scientificLitFn : Lean.Parser.ParserFn

def Lean.Parser.scientificLitNoAntiquot : Lean.Parser.Parser

def Lean.Parser.strLitFn : Lean.Parser.ParserFn

def Lean.Parser.strLitNoAntiquot : Lean.Parser.Parser

def Lean.Parser.charLitFn : Lean.Parser.ParserFn

def Lean.Parser.charLitNoAntiquot : Lean.Parser.Parser

def Lean.Parser.nameLitFn : Lean.Parser.ParserFn

def Lean.Parser.nameLitNoAntiquot : Lean.Parser.Parser

def Lean.Parser.identFn : Lean.Parser.ParserFn

def Lean.Parser.identNoAntiquot : Lean.Parser.Parser

def Lean.Parser.rawIdentNoAntiquot : Lean.Parser.Parser

def Lean.Parser.identEqFn (id : Lake.Name) : Lean.Parser.ParserFn

def Lean.Parser.identEq (id : Lake.Name) : Lean.Parser.Parser

def Lean.Parser.hygieneInfoFn : Lean.Parser.ParserFn

def Lean.Parser.hygieneInfoNoAntiquot : Lean.Parser.Parser

def Lean.Parser.ParserState.keepTop (s : Lean.Parser.SyntaxStack) (startStackSize : Nat) : Lean.Parser.SyntaxStack

def Lean.Parser.ParserState.keepNewError (s : Lean.Parser.ParserState) (oldStackSize : Nat) : Lean.Parser.ParserState

def Lean.Parser.ParserState.keepPrevError (s : Lean.Parser.ParserState) (oldStackSize : Nat) (oldStopPos : String.Pos) (oldError : Option Lean.Parser.Error) (oldLhsPrec : Nat) : Lean.Parser.ParserState

def Lean.Parser.ParserState.mergeErrors (s : Lean.Parser.ParserState) (oldStackSize : Nat) (oldError : Lean.Parser.Error) : Lean.Parser.ParserState

def Lean.Parser.ParserState.keepLatest (s : Lean.Parser.ParserState) (startStackSize : Nat) : Lean.Parser.ParserState

def Lean.Parser.ParserState.replaceLongest (s : Lean.Parser.ParserState) (startStackSize : Nat) : Lean.Parser.ParserState

def Lean.Parser.invalidLongestMatchParser (s : Lean.Parser.ParserState) : Lean.Parser.ParserState

def Lean.Parser.runLongestMatchParser (left? : Option Lean.Syntax) (startLhsPrec : Nat) (p : Lean.Parser.ParserFn) : Lean.Parser.ParserFn

Auxiliary function used to execute parsers provided to longestMatchFn. Push left? into the stack if it is not none, and execute p.

Remark: p must produce exactly one syntax node. Remark: the left? is not none when we are processing trailing parsers.

def Lean.Parser.longestMatchStep (left? : Option Lean.Syntax) (startSize : Nat) (startLhsPrec : Nat) (startPos : String.Pos) (prevPrio : Nat) (prio : Nat) (p : Lean.Parser.ParserFn) : Lean.Parser.ParserContext → Lean.Parser.ParserState → Lean.Parser.ParserState × Nat

def Lean.Parser.longestMatchMkResult (startSize : Nat) (s : Lean.Parser.ParserState) : Lean.Parser.ParserState

def Lean.Parser.longestMatchFnAux (left? : Option Lean.Syntax) (startSize : Nat) (startLhsPrec : Nat) (startPos : String.Pos) (prevPrio : Nat) (ps : List (Lean.Parser.Parser × Nat)) : Lean.Parser.ParserFn

def Lean.Parser.longestMatchFnAux.parse (left? : Option Lean.Syntax) (startSize : Nat) (startLhsPrec : Nat) (startPos : String.Pos) (prevPrio : Nat) (ps : List (Lean.Parser.Parser × Nat)) : Lean.Parser.ParserFn

Equations

• One or more equations did not get rendered due to their size.
• Lean.Parser.longestMatchFnAux.parse left? startSize startLhsPrec startPos prevPrio [] = fun x s => Lean.Parser.longestMatchMkResult startSize s

def Lean.Parser.longestMatchFn (left? : Option Lean.Syntax) : List (Lean.Parser.Parser × Nat) → Lean.Parser.ParserFn

def Lean.Parser.anyOfFn : List Lean.Parser.Parser → Lean.Parser.ParserFn

Equations

• Lean.Parser.anyOfFn [] x x = Lean.Parser.ParserState.mkError x "anyOf: empty list"
• Lean.Parser.anyOfFn [p] x x = Lean.Parser.Parser.fn p x x
• Lean.Parser.anyOfFn (p :: ps) x x = Lean.Parser.orelseFn p.fn (Lean.Parser.anyOfFn ps) x x

def Lean.Parser.checkColEqFn (errorMsg : String) : Lean.Parser.ParserFn

def Lean.Parser.checkColEq (errorMsg : optParam String "checkColEq") : Lean.Parser.Parser

def Lean.Parser.checkColGeFn (errorMsg : String) : Lean.Parser.ParserFn

def Lean.Parser.checkColGe (errorMsg : optParam String "checkColGe") : Lean.Parser.Parser

def Lean.Parser.checkColGtFn (errorMsg : String) : Lean.Parser.ParserFn

def Lean.Parser.checkColGt (errorMsg : optParam String "checkColGt") : Lean.Parser.Parser

def Lean.Parser.checkLineEqFn (errorMsg : String) : Lean.Parser.ParserFn

def Lean.Parser.checkLineEq (errorMsg : optParam String "checkLineEq") : Lean.Parser.Parser

def Lean.Parser.withPosition : Lean.Parser.Parser → Lean.Parser.Parser

def Lean.Parser.withPositionAfterLinebreak : Lean.Parser.Parser → Lean.Parser.Parser

def Lean.Parser.withoutPosition (p : Lean.Parser.Parser) : Lean.Parser.Parser

def Lean.Parser.withForbidden (tk : Lean.Parser.Token) (p : Lean.Parser.Parser) : Lean.Parser.Parser

def Lean.Parser.withoutForbidden (p : Lean.Parser.Parser) : Lean.Parser.Parser

def Lean.Parser.eoiFn : Lean.Parser.ParserFn

def Lean.Parser.eoi : Lean.Parser.Parser

def Lean.Parser.TokenMap (α : Type) : Type

A multimap indexed by tokens. Used for indexing parsers by their leading token.

def Lean.Parser.TokenMap.insert {α : Type} (map : Lean.Parser.TokenMap α) (k : Lake.Name) (v : α) : Lean.Parser.TokenMap α

instance Lean.Parser.TokenMap.instInhabitedTokenMap {α : Type} : Inhabited (Lean.Parser.TokenMap α)

instance Lean.Parser.TokenMap.instEmptyCollectionTokenMap {α : Type} : EmptyCollection (Lean.Parser.TokenMap α)

instance Lean.Parser.TokenMap.instForInTokenMapProdNameList {m : Type u_1 → Type u_2} {α : Type} : ForIn m (Lean.Parser.TokenMap α) (Lake.Name × List α)

structure Lean.Parser.PrattParsingTables : Type

• leadingTable : Lean.Parser.TokenMap (Lean.Parser.Parser × Nat)
• leadingParsers : List (Lean.Parser.Parser × Nat)
• trailingTable : Lean.Parser.TokenMap (Lean.Parser.Parser × Nat)
• trailingParsers : List (Lean.Parser.Parser × Nat)

instance Lean.Parser.instInhabitedPrattParsingTables : Inhabited Lean.Parser.PrattParsingTables

inductive Lean.Parser.LeadingIdentBehavior : Type

• default: Lean.Parser.LeadingIdentBehavior

  LeadingIdentBehavior.default: if the leading token is an identifier, then prattParser just executes the parsers associated with the auxiliary token "ident".

• symbol: Lean.Parser.LeadingIdentBehavior

  LeadingIdentBehavior.symbol: if the leading token is an identifier , and there are parsers P associated with the token , then it executes P. Otherwise, it executes only the parsers associated with the auxiliary token "ident".

• both: Lean.Parser.LeadingIdentBehavior

  LeadingIdentBehavior.both: if the leading token an identifier , the it executes the parsers associated with token and parsers associated with the auxiliary token "ident".

The type LeadingIdentBehavior specifies how the parsing table lookup function behaves for identifiers. The function prattParser uses two tables leadingTable and trailingTable. They map tokens to parsers.

We use LeadingIdentBehavior.symbol and LeadingIdentBehavior.both and nonReservedSymbol parser to implement the tactic parsers. The idea is to avoid creating a reserved symbol for each builtin tactic (e.g., apply, assumption, etc.). That is, users may still use these symbols as identifiers (e.g., naming a function).

instance Lean.Parser.instInhabitedLeadingIdentBehavior : Inhabited Lean.Parser.LeadingIdentBehavior

instance Lean.Parser.instBEqLeadingIdentBehavior : BEq Lean.Parser.LeadingIdentBehavior

instance Lean.Parser.instReprLeadingIdentBehavior : Repr Lean.Parser.LeadingIdentBehavior

structure Lean.Parser.ParserCategory : Type

• declName : Lake.Name

  The name of a declaration which will be used as the target of go-to-definition queries and from which doc strings will be extracted. This is a dummy declaration of type Lean.Parser.Category created by declare_syntax_cat, but for builtin categories the declaration is made manually and passed to registerBuiltinParserAttribute.

• kinds : Lean.Parser.SyntaxNodeKindSet

  The list of syntax nodes that can parse into this category. This can be used to list all syntaxes in the category.

• tables : Lean.Parser.PrattParsingTables

  The parsing tables, which consist of a dynamic set of parser functions based on the syntaxes that have been declared so far.

• behavior : Lean.Parser.LeadingIdentBehavior

  The LeadingIdentBehavior, which specifies how the parsing table lookup function behaves for the first identifier to be parsed. This is used by the tactic parser to avoid creating a reserved symbol for each builtin tactic (e.g., apply, assumption, etc.).

Each parser category is implemented using a Pratt's parser. The system comes equipped with the following categories: level, term, tactic, and command. Users and plugins may define extra categories.

The method

categoryParser `term prec

executes the Pratt's parser for category term with precedence prec. That is, only parsers with precedence at least prec are considered. The method termParser prec is equivalent to the method above.

instance Lean.Parser.instInhabitedParserCategory : Inhabited Lean.Parser.ParserCategory

@[inline, reducible]

abbrev Lean.Parser.ParserCategories : Type

def Lean.Parser.indexed {α : Type} (map : Lean.Parser.TokenMap α) (c : Lean.Parser.ParserContext) (s : Lean.Parser.ParserState) (behavior : Lean.Parser.LeadingIdentBehavior) : Lean.Parser.ParserState × List α

@[inline, reducible]

abbrev Lean.Parser.CategoryParserFn : Type

opaque Lean.Parser.categoryParserFnRef : IO.Ref Lean.Parser.CategoryParserFn

opaque Lean.Parser.categoryParserFnExtension : Lean.EnvExtension Lean.Parser.CategoryParserFn

def Lean.Parser.categoryParserFn (catName : Lake.Name) : Lean.Parser.ParserFn

def Lean.Parser.categoryParser (catName : Lake.Name) (prec : Nat) : Lean.Parser.Parser

def Lean.Parser.termParser (prec : optParam Nat 0) : Lean.Parser.Parser

Antiquotations

def Lean.Parser.checkNoImmediateColon : Lean.Parser.Parser

Fail if previous token is immediately followed by ':'.

def Lean.Parser.setExpectedFn (expected : List String) (p : Lean.Parser.ParserFn) : Lean.Parser.ParserFn

def Lean.Parser.setExpected (expected : List String) : Lean.Parser.Parser → Lean.Parser.Parser

def Lean.Parser.pushNone : Lean.Parser.Parser

def Lean.Parser.antiquotNestedExpr : Lean.Parser.Parser

def Lean.Parser.antiquotExpr : Lean.Parser.Parser

def Lean.Parser.tokenAntiquotFn : Lean.Parser.ParserFn

def Lean.Parser.tokenWithAntiquot : Lean.Parser.Parser → Lean.Parser.Parser

def Lean.Parser.symbol (sym : String) : Lean.Parser.Parser

instance Lean.Parser.instCoeStringParser : Coe String Lean.Parser.Parser

def Lean.Parser.nonReservedSymbol (sym : String) (includeIdent : optParam Bool false) : Lean.Parser.Parser

def Lean.Parser.unicodeSymbol (sym : String) (asciiSym : String) : Lean.Parser.Parser

def Lean.Parser.mkAntiquot (name : String) (kind : Lean.SyntaxNodeKind) (anonymous : optParam Bool true) (isPseudoKind : optParam Bool false) : Lean.Parser.Parser

Define parser for $e (if anonymous == true) and $e:name. kind is embedded in the antiquotation's kind, and checked at syntax match unless isPseudoKind is true. Antiquotations can be escaped as in $$e, which produces the syntax tree for $e.

def Lean.Parser.withAntiquotFn (antiquotP : Lean.Parser.ParserFn) (p : Lean.Parser.ParserFn) (isCatAntiquot : optParam Bool false) : Lean.Parser.ParserFn

def Lean.Parser.withAntiquot (antiquotP : Lean.Parser.Parser) (p : Lean.Parser.Parser) : Lean.Parser.Parser

Optimized version of mkAntiquot ... <|> p.

def Lean.Parser.withoutInfo (p : Lean.Parser.Parser) : Lean.Parser.Parser

def Lean.Parser.mkAntiquotSplice (kind : Lean.SyntaxNodeKind) (p : Lean.Parser.Parser) (suffix : Lean.Parser.Parser) : Lean.Parser.Parser

Parse $[p]suffix, e.g. $[p],*.

def Lean.Parser.withAntiquotSuffixSplice (kind : Lean.SyntaxNodeKind) (p : Lean.Parser.Parser) (suffix : Lean.Parser.Parser) : Lean.Parser.Parser

Parse suffix after an antiquotation, e.g. $x,*, and put both into a new node.

def Lean.Parser.withAntiquotSpliceAndSuffix (kind : Lean.SyntaxNodeKind) (p : Lean.Parser.Parser) (suffix : Lean.Parser.Parser) : Lean.Parser.Parser

def Lean.Parser.nodeWithAntiquot (name : String) (kind : Lean.SyntaxNodeKind) (p : Lean.Parser.Parser) (anonymous : optParam Bool false) : Lean.Parser.Parser

End of Antiquotations

def Lean.Parser.sepByElemParser (p : Lean.Parser.Parser) (sep : String) : Lean.Parser.Parser

def Lean.Parser.sepBy (p : Lean.Parser.Parser) (sep : String) (psep : optParam Lean.Parser.Parser (Lean.Parser.symbol sep)) (allowTrailingSep : optParam Bool false) : Lean.Parser.Parser

def Lean.Parser.sepBy1 (p : Lean.Parser.Parser) (sep : String) (psep : optParam Lean.Parser.Parser (Lean.Parser.symbol sep)) (allowTrailingSep : optParam Bool false) : Lean.Parser.Parser

def Lean.Parser.leadingParserAux (kind : Lake.Name) (tables : Lean.Parser.PrattParsingTables) (behavior : Lean.Parser.LeadingIdentBehavior) : Lean.Parser.ParserFn

def Lean.Parser.leadingParser (kind : Lake.Name) (tables : Lean.Parser.PrattParsingTables) (behavior : Lean.Parser.LeadingIdentBehavior) (antiquotParser : Lean.Parser.ParserFn) : Lean.Parser.ParserFn

def Lean.Parser.trailingLoopStep (tables : Lean.Parser.PrattParsingTables) (left : Lean.Syntax) (ps : List (Lean.Parser.Parser × Nat)) : Lean.Parser.ParserFn

partial def Lean.Parser.trailingLoop (tables : Lean.Parser.PrattParsingTables) (c : Lean.Parser.ParserContext) (s : Lean.Parser.ParserState) : Lean.Parser.ParserState

def Lean.Parser.prattParser (kind : Lake.Name) (tables : Lean.Parser.PrattParsingTables) (behavior : Lean.Parser.LeadingIdentBehavior) (antiquotParser : Lean.Parser.ParserFn) : Lean.Parser.ParserFn

Implements a variant of Pratt's algorithm. In Pratt's algorithms tokens have a right and left binding power. In our implementation, parsers have precedence instead. This method selects a parser (or more, via longestMatchFn) from leadingTable based on the current token. Note that the unindexed leadingParsers parsers are also tried. We have the unidexed leadingParsers because some parsers do not have a "first token". Example:

syntax term:51 "≤" ident "<" term "|" term : index

Example, in principle, the set of first tokens for this parser is any token that can start a term, but this set is always changing. Thus, this parsing rule is stored as an unindexed leading parser at leadingParsers. After processing the leading parser, we chain with parsers from trailingTable/trailingParsers that have precedence at least c.prec where c is the ParsingContext. Recall that c.prec is set by categoryParser.

Note that in the original Pratt's algorith, precedences are only checked before calling trailing parsers. In our implementation, leading and trailing parsers check the precendece. We claim our algorithm is more flexible, modular and easier to understand.

antiquotParser should be a mkAntiquot parser (or always fail) and is tried before all other parsers. It should not be added to the regular leading parsers because it would heavily overlap with antiquotation parsers nested inside them.

def Lean.Parser.fieldIdxFn : Lean.Parser.ParserFn

def Lean.Parser.fieldIdx : Lean.Parser.Parser

def Lean.Parser.skip : Lean.Parser.Parser

def Lean.Syntax.foldArgsM {m : Type u_1 → Type u_2} [Monad m] {β : Type u_1} (s : Lean.Syntax) (f : Lean.Syntax → β → m β) (b : β) : m β

def Lean.Syntax.foldArgs {β : Type u_1} (s : Lean.Syntax) (f : Lean.Syntax → β → β) (b : β) : β

def Lean.Syntax.forArgsM {m : Type → Type u_1} [Monad m] (s : Lean.Syntax) (f : Lean.Syntax → m Unit) : m Unit