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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.Parser.dbgTraceState label = Lean.Parser.withFn (Lean.Parser.dbgTraceStateFn label)

@[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

Equations

• Lean.Parser.checkStackTop p msg = { info := Lean.Parser.epsilonInfo, fn := Lean.Parser.checkStackTopFn p msg }

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

Equations

• Lean.Parser.andthenFn p q c s = if (p c s).hasError = true then p c s else q c (p c s)

@[noinline]

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

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

The andthen(p, q) combinator, usually written as adjacency in syntax declarations (p q), parses p followed by q.

The arity of this parser is the sum of the arities of p and q: that is, it accumulates all the nodes produced by p followed by the nodes from q into the list of arguments to the surrounding parse node.

Equations

• Lean.Parser.andthen p q = { info := Lean.Parser.andthenInfo p.info q.info, fn := Lean.Parser.andthenFn p.fn q.fn }

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

Equations

• Lean.Parser.nodeInfo n p = { collectTokens := p.collectTokens, collectKinds := fun (s : Lean.Parser.SyntaxNodeKindSet) => (p.collectKinds s).insert n, firstTokens := p.firstTokens }

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

Equations

• Lean.Parser.checkPrecFn prec c s = if c.prec ≤ prec then s else s.mkUnexpectedError "unexpected token at this precedence level; consider parenthesizing the term"

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

Equations

• Lean.Parser.checkPrec prec = { info := Lean.Parser.epsilonInfo, fn := Lean.Parser.checkPrecFn prec }

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

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• Lean.Parser.incQuotDepth p = Lean.Parser.addQuotDepth✝ 1 p

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

Equations

• Lean.Parser.decQuotDepth p = Lean.Parser.addQuotDepth✝ (-1) p

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.Parser.leadingNode n prec p = Lean.Parser.checkPrec prec >> Lean.Parser.node n p >> Lean.Parser.setLhsPrec prec

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

Equations

• Lean.Parser.trailingNodeAux n p = { info := Lean.Parser.nodeInfo n p.info, fn := Lean.Parser.trailingNodeFn n p.fn }

def Lean.Parser.trailingNode (n : Lean.SyntaxNodeKind) (prec 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

Equations

• One or more equations did not get rendered due to their size.
• Lean.Parser.mergeOrElseErrors s error1 iniPos mergeErrors = s

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 q : Lean.Parser.ParserFn) (antiquotBehavior : Lean.Parser.OrElseOnAntiquotBehavior := Lean.Parser.OrElseOnAntiquotBehavior.merge) : Lean.Parser.ParserFn

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

Equations

• Lean.Parser.orelseFn p q = Lean.Parser.orelseFnCore p q

@[noinline]

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

Equations

• Lean.Parser.orelseInfo p q = { collectTokens := p.collectTokens ∘ q.collectTokens, collectKinds := p.collectKinds ∘ q.collectKinds, firstTokens := p.firstTokens.merge q.firstTokens }

def Lean.Parser.orelse (p 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

Equations

• Lean.Parser.instOrElseParser = { orElse := fun (a : Lean.Parser.Parser) (b : Unit → Lean.Parser.Parser) => Lean.Parser.orelse a (b ()) }

@[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

The atomic(p) parser parses p, returns the same result as p and fails iff p fails, but if p fails after consuming some tokens atomic(p) will fail without consuming tokens. This is important for the p <|> q combinator, because it is not backtracking, and will fail if p fails after consuming some tokens. To get backtracking behavior, use atomic(p) <|> q instead.

This parser has the same arity as p - it produces the same result as p.

Equations

• Lean.Parser.atomic = Lean.Parser.withFn Lean.Parser.atomicFn

structure Lean.Parser.RecoveryContext : Type

Information about the state of the parse prior to the failing parser's execution

• initialPos : String.Pos

  The position prior to the failing parser

• initialSize : Nat

  The syntax stack height prior to the failing parser's execution

instance Lean.Parser.instBEqRecoveryContext : BEq Lean.Parser.RecoveryContext

Equations

• Lean.Parser.instBEqRecoveryContext = { beq := Lean.Parser.beqRecoveryContext✝ }

instance Lean.Parser.instDecidableEqRecoveryContext : DecidableEq Lean.Parser.RecoveryContext

instance Lean.Parser.instReprRecoveryContext : Repr Lean.Parser.RecoveryContext

Equations

• Lean.Parser.instReprRecoveryContext = { reprPrec := Lean.Parser.reprRecoveryContext✝ }

def Lean.Parser.recoverFn (p : Lean.Parser.ParserFn) (recover : Lean.Parser.RecoveryContext → Lean.Parser.ParserFn) : Lean.Parser.ParserFn

Recover from errors in p using recover to consume input until a known-good state has appeared. If recover fails itself, then no recovery is performed.

recover is provided with information about the failing parser's effects , and it is run in the state immediately after the failure.

def Lean.Parser.recover' (parser : Lean.Parser.Parser) (handler : Lean.Parser.RecoveryContext → Lean.Parser.Parser) : Lean.Parser.Parser

Recover from errors in parser using handler to consume input until a known-good state has appeared. If handler fails itself, then no recovery is performed.

handler is provided with information about the failing parser's effects , and it is run in the state immediately after the failure.

The interactions between <|> and recover' are subtle, especially for syntactic categories that admit user extension. Consider avoiding it in these cases.

Equations

• Lean.Parser.recover' parser handler = { info := parser.info, fn := Lean.Parser.recoverFn parser.fn fun (s : Lean.Parser.RecoveryContext) => (handler s).fn }

def Lean.Parser.recover (parser handler : Lean.Parser.Parser) : Lean.Parser.Parser

Recover from errors in parser using handler to consume input until a known-good state has appeared. If handler fails itself, then no recovery is performed.

handler is run in the state immediately after the failure.

The interactions between <|> and recover are subtle, especially for syntactic categories that admit user extension. Consider avoiding it in these cases.

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

lookahead(p) runs p and fails if p does, but it produces no parse nodes and rewinds the position to the original state on success. So for example lookahead("=>") will ensure that the next token is "=>", without actually consuming this token.

This parser has arity 0 - it does not capture anything.

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

Equations

• One or more equations did not get rendered due to their size.

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

notFollowedBy(p, "foo") succeeds iff p fails; if p succeeds then it fails with the message "unexpected foo".

This parser has arity 0 - it does not capture anything.

Equations

• Lean.Parser.notFollowedBy p msg = { info := { collectTokens := id, collectKinds := id, firstTokens := Lean.Parser.FirstTokens.unknown }, fn := Lean.Parser.notFollowedByFn p.fn msg }

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

Equations

• Lean.Parser.many1NoAntiquot = Lean.Parser.withFn Lean.Parser.many1Fn

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

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

@[noinline]

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

@[noinline]

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

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

Equations

• Lean.Parser.sepByNoAntiquot p sep allowTrailingSep = { info := Lean.Parser.sepByInfo p.info sep.info, fn := Lean.Parser.sepByFn allowTrailingSep p.fn sep.fn }

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

Equations

• Lean.Parser.sepBy1NoAntiquot p sep allowTrailingSep = { info := Lean.Parser.sepBy1Info p.info sep.info, fn := Lean.Parser.sepBy1Fn allowTrailingSep p.fn sep.fn }

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

Equations

• Lean.Parser.withResultOfFn p f c s = if (p c s).hasError = true then p c s else let stx := (p c s).stxStack.back; (p c s).popSyntax.pushSyntax (f stx)

@[noinline]

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

Equations

• Lean.Parser.withResultOfInfo p = { collectTokens := p.collectTokens, collectKinds := p.collectKinds, firstTokens := Lean.Parser.FirstTokens.unknown }

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

Equations

• Lean.Parser.withResultOf p f = { info := Lean.Parser.withResultOfInfo p.info, fn := Lean.Parser.withResultOfFn p.fn f }

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

Equations

• Lean.Parser.many1Unbox p = Lean.Parser.withResultOf (Lean.Parser.many1NoAntiquot p) fun (stx : Lean.Syntax) => if (stx.getNumArgs == 1) = true then stx.getArg 0 else stx

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

Equations

• Lean.Parser.satisfyFn p errorMsg c s = if h : c.input.atEnd s.pos = true then s.mkEOIError else if p (c.input.get' s.pos h) = true then s.next' c.input s.pos h else s.mkUnexpectedError errorMsg

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

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

Equations

• Lean.Parser.takeWhileFn p = Lean.Parser.takeUntilFn fun (c : Char) => !p c

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

Equations

• Lean.Parser.finishCommentBlock.eoi pushMissingOnError s = s.mkUnexpectedError "unterminated comment" [] pushMissingOnError

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

Consume whitespace and comments

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

Equations

• Lean.Parser.mkEmptySubstringAt s p = { str := s, startPos := p, stopPos := p }

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

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

Equations

• Lean.Parser.rawFn p trailingWs c s = if (p c s).hasError = true then p c s else Lean.Parser.rawAux✝ s.pos trailingWs c (p c s)

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

Equations

• Lean.Parser.chFn c trailingWs = Lean.Parser.rawFn (Lean.Parser.satisfyFn (fun (d : Char) => c == d) ("'" ++ toString c ++ "'")) trailingWs

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

Equations

• Lean.Parser.rawCh c trailingWs = { info := { collectTokens := id, collectKinds := id, firstTokens := Lean.Parser.FirstTokens.unknown }, fn := Lean.Parser.chFn c trailingWs }

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

partial def Lean.Parser.stringGapFn (seenNewline : Bool) : Lean.Parser.ParserFn

Parses the whitespace after the \ when there is a string gap. Raises an error if the whitespace does not contain exactly one newline character.

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

Parses a string quotation after a \.

• isQuotable determines which characters are valid escapes
• inString enables features that are only valid within strings, in particular "\" newline whitespace* gaps.

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

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

Equations

• Lean.Parser.quotedCharFn = Lean.Parser.quotedCharCoreFn Lean.Parser.isQuotableCharDefault false

def Lean.Parser.quotedStringFn : Lean.Parser.ParserFn

Like quotedCharFn but enables escapes that are only valid inside strings. In particular, string gaps ("\" newline whitespace*).

Equations

• Lean.Parser.quotedStringFn = Lean.Parser.quotedCharCoreFn Lean.Parser.isQuotableCharDefault true

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

Push (Syntax.node tk <new-atom>) 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

partial def Lean.Parser.isRawStrLitStart (input : String) (i : String.Pos) : Bool

Raw strings have the syntax r##...#"..."#...## with zero or more #'s. If we are looking at a valid start to a raw string (r##...#"), returns true. We assume i begins at the position immediately after r.

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

Parses a raw string literal assuming isRawStrLitStart has returned true. The startPos is the start of the raw string (at the r). The parser state is assumed to be immediately after the r.

def Lean.Parser.rawStrLitFnAux.errorUnterminated (startPos : String.Pos) (s : Lean.Parser.ParserState) : Lean.Parser.ParserState

Gives the "unterminated raw string literal" error.

Equations

• Lean.Parser.rawStrLitFnAux.errorUnterminated startPos s = s.mkUnexpectedErrorAt "unterminated raw string literal" startPos

partial def Lean.Parser.rawStrLitFnAux.initState (startPos : String.Pos) (num : Nat) : Lean.Parser.ParserContext → Lean.Parser.ParserState → Lean.Parser.ParserState

Parses the #'s and " at the beginning of the raw string. The num variable counts the number of #s after the r.

partial def Lean.Parser.rawStrLitFnAux.normalState (startPos : String.Pos) (num : Nat) : Lean.Parser.ParserContext → Lean.Parser.ParserState → Lean.Parser.ParserState

Parses characters after the first ". If we need to start counting #'s to decide if we are closing the raw string literal, we switch to closingState.

partial def Lean.Parser.rawStrLitFnAux.closingState (startPos : String.Pos) (num closingNum : Nat) : Lean.Parser.ParserContext → Lean.Parser.ParserState → Lean.Parser.ParserState

Parses # characters immediately after a ". The closingNum variable counts the number of #s seen after the ". Note: num > 0 since the num = 0 case is entirely handled by normalState.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.Parser.binNumberFn startPos c s = Lean.Parser.mkNodeToken Lean.numLitKind startPos c (Lean.Parser.takeWhile1Fn (fun (c : Char) => c == '0' || c == '1') "binary number" c s)

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.
• Lean.Parser.mkTokenAndFixPos startPos none c s = s.mkErrorAt "token" startPos

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.Parser.identFnAux startPos tk r = Lean.Parser.identFnAux.parse startPos tk r

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

def Lean.Parser.tokenFn (expected : 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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.Parser.peekToken c s = if (s.cache.tokenCache.startPos == s.pos) = true then (s, Except.ok s.cache.tokenCache.token) else Lean.Parser.peekTokenAux c s

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

Treat keywords as identifiers.

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

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• Lean.Parser.symbolInfo sym = { collectTokens := fun (tks : List Lean.Parser.Token) => sym :: tks, collectKinds := id, firstTokens := Lean.Parser.FirstTokens.tokens [sym] }

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 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).

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.Parser.nonReservedSymbolFn sym = Lean.Parser.nonReservedSymbolFnAux sym ("'" ++ sym ++ "'")

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.Parser.nonReservedSymbolNoAntiquot sym includeIdent = { info := Lean.Parser.nonReservedSymbolInfo sym.trim includeIdent, fn := Lean.Parser.nonReservedSymbolFn sym.trim }

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

Equations

• Lean.Parser.strAux sym errorMsg j = Lean.Parser.strAux.parse sym errorMsg j

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

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

Equations

• Lean.Parser.checkTailWs prev = match prev.getTailInfo with | Lean.SourceInfo.original leading pos trailing endPos => decide (trailing.stopPos > trailing.startPos) | x => false

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

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

The ws parser requires that there is some whitespace at this location. For example, the parser "foo" ws "+" parses foo + or foo/- -/+ but not foo+.

This parser has arity 0 - it does not capture anything.

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

Equations

• Lean.Parser.checkTailLinebreak prev = match prev.getTailInfo with | Lean.SourceInfo.original leading pos trailing endPos => trailing.contains '\n' | x => false

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

Equations

• Lean.Parser.checkLinebreakBeforeFn errorMsg x s = if Lean.Parser.checkTailLinebreak s.stxStack.back = true then s else s.mkError errorMsg

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

The linebreak parser requires that there is at least one line break at this location. (The line break may be inside a comment.)

This parser has arity 0 - it does not capture anything.

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

Equations

• Lean.Parser.checkNoWsBeforeFn errorMsg x s = if Lean.Parser.checkTailNoWs (Lean.Parser.pickNonNone✝ s.stxStack) = true then s else s.mkError errorMsg

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

The noWs parser requires that there is no whitespace between the preceding and following parsers. For example, the parser "foo" noWs "+" parses foo+ but not foo +.

This is almost the same as "foo+", but using this parser will make foo+ a token, which may cause problems for the use of "foo" and "+" as separate tokens in other parsers.

This parser has arity 0 - it does not capture anything.

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

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

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• Lean.Parser.unicodeSymbolNoAntiquot sym asciiSym = { info := Lean.Parser.unicodeSymbolInfo sym.trim asciiSym.trim, fn := Lean.Parser.unicodeSymbolFn sym.trim asciiSym.trim }

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

def Lean.Parser.expectTokenFn (k : Lean.SyntaxNodeKind) (desc : String) : Lean.Parser.ParserFn

Parses a token and asserts the result is of the given kind. desc is used in error messages as the token kind.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.Parser.strLitFn = Lean.Parser.expectTokenFn Lean.strLitKind "string literal"

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

Equations

• Lean.Parser.strLitNoAntiquot = { info := Lean.Parser.mkAtomicInfo "str", fn := Lean.Parser.strLitFn }

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

Equations

• Lean.Parser.charLitFn = Lean.Parser.expectTokenFn Lean.charLitKind "character literal"

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

Equations

• Lean.Parser.identFn = Lean.Parser.expectTokenFn Lean.identKind "identifier"

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

Equations

• Lean.Parser.identNoAntiquot = { info := Lean.Parser.mkAtomicInfo "ident", fn := Lean.Parser.identFn }

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

Equations

• Lean.Parser.rawIdentNoAntiquot = { info := { collectTokens := id, collectKinds := id, firstTokens := Lean.Parser.FirstTokens.unknown }, fn := Lean.Parser.rawIdentFn }

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

Equations

• One or more equations did not get rendered due to their size.

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

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

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

Equations

• Lean.Parser.hygieneInfoNoAntiquot = { info := Lean.Parser.nodeInfo Lean.hygieneInfoKind Lean.Parser.epsilonInfo, fn := Lean.Parser.hygieneInfoFn }

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

Equations

• Lean.Parser.ParserState.keepTop s startStackSize = (s.take startStackSize).push s.back

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.Parser.invalidLongestMatchParser s = s.mkError "longestMatch parsers must generate exactly one Syntax node"

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.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• Lean.Parser.longestMatchFnAux left? startSize startLhsPrec startPos prevPrio ps = Lean.Parser.longestMatchFnAux.parse left? startSize startLhsPrec startPos prevPrio ps

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

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

Equations

• One or more equations did not get rendered due to their size.
• Lean.Parser.longestMatchFn left? [] = fun (x : Lean.Parser.ParserContext) (s : Lean.Parser.ParserState) => s.mkError "longestMatch: empty list"
• Lean.Parser.longestMatchFn left? [p] = fun (c : Lean.Parser.ParserContext) (s : Lean.Parser.ParserState) => Lean.Parser.runLongestMatchParser left? s.lhsPrec p.fst.fn c s

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

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

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

The colEq parser ensures that the next token starts at exactly the column of the saved position (see withPosition). This can be used to do whitespace sensitive syntax like a by block or do block, where all the lines have to line up.

This parser has arity 0 - it does not capture anything.

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

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

The colGe parser requires that the next token starts from at least the column of the saved position (see withPosition), but allows it to be more indented. This can be used for whitespace sensitive syntax to ensure that a block does not go outside a certain indentation scope. For example it is used in the lean grammar for else if, to ensure that the else is not less indented than the if it matches with.

This parser has arity 0 - it does not capture anything.

Equations

• Lean.Parser.checkColGe errorMsg = { info := { collectTokens := id, collectKinds := id, firstTokens := Lean.Parser.FirstTokens.unknown }, fn := Lean.Parser.checkColGeFn errorMsg }

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

Equations

• One or more equations did not get rendered due to their size.

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

The colGt parser requires that the next token starts a strictly greater column than the saved position (see withPosition). This can be used for whitespace sensitive syntax for the arguments to a tactic, to ensure that the following tactic is not interpreted as an argument.

example (x : False) : False := by
  revert x
  exact id

Here, the revert tactic is followed by a list of colGt ident, because otherwise it would interpret exact as an identifier and try to revert a variable named exact.

This parser has arity 0 - it does not capture anything.

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

Equations

• One or more equations did not get rendered due to their size.

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

The lineEq parser requires that the current token is on the same line as the saved position (see withPosition). This can be used to ensure that composite tokens are not "broken up" across different lines. For example, else if is parsed using lineEq to ensure that the two tokens are on the same line.

This parser has arity 0 - it does not capture anything.

Equations

• Lean.Parser.checkLineEq errorMsg = { info := { collectTokens := id, collectKinds := id, firstTokens := Lean.Parser.FirstTokens.unknown }, fn := Lean.Parser.checkLineEqFn errorMsg }

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

withPosition(p) runs p while setting the "saved position" to the current position. This has no effect on its own, but various other parsers access this position to achieve some composite effect:

• colGt, colGe, colEq compare the column of the saved position to the current position, used to implement Python-style indentation sensitive blocks
• lineEq ensures that the current position is still on the same line as the saved position, used to implement composite tokens

The saved position is only available in the read-only state, which is why this is a scoping parser: after the withPosition(..) block the saved position will be restored to its original value.

This parser has the same arity as p - it just forwards the results of p.

Equations

• One or more equations did not get rendered due to their size.

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

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

withoutPosition(p) runs p without the saved position, meaning that position-checking parsers like colGt will have no effect. This is usually used by bracketing constructs like (...) so that the user can locally override whitespace sensitivity.

This parser has the same arity as p - it just forwards the results of p.

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

withForbidden tk p runs p with tk as a "forbidden token". This means that if the token appears anywhere in p (unless it is nested in withoutForbidden), parsing will immediately stop there, making tk effectively a lowest-precedence operator. This is used for parsers like for x in arr do ...: arr is parsed as withForbidden "do" term because otherwise arr do ... would be treated as an application.

This parser has the same arity as p - it just forwards the results of p.

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

withoutForbidden(p) runs p disabling the "forbidden token" (see withForbidden), if any. This is usually used by bracketing constructs like (...) because there is no parsing ambiguity inside these nested constructs.

This parser has the same arity as p - it just forwards the results of p.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.Parser.eoiFn c s = if c.input.atEnd s.pos = true then s else s.mkError "expected end of file"

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 : Lean.Name) (v : α) : Lean.Parser.TokenMap α

Equations

• map.insert k v = match Lean.RBMap.find? map k with | none => Lean.RBMap.insert map k [v] | some vs => Lean.RBMap.insert map k (v :: vs)

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

Equations

• Lean.Parser.TokenMap.instInhabited = { default := Lean.RBMap.empty }

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

Equations

• Lean.Parser.TokenMap.instEmptyCollection = { emptyCollection := Lean.RBMap.empty }

instance Lean.Parser.TokenMap.instForInProdNameList {m : Type u_1 → Type u_2} {α : Type} : ForIn m (Lean.Parser.TokenMap α) (Lean.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

Equations

• Lean.Parser.instInhabitedPrattParsingTables = { default := { leadingTable := ∅, leadingParsers := [], trailingTable := ∅, trailingParsers := [] } }

inductive Lean.Parser.LeadingIdentBehavior : Type

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).

• 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 <foo>, and there are parsers P associated with the token <foo>, 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 <foo>, the it executes the parsers associated with token <foo> and parsers associated with the auxiliary token "ident".

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

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

Equations

• Lean.Parser.instBEqLeadingIdentBehavior = { beq := Lean.Parser.beqLeadingIdentBehavior✝ }

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

Equations

• Lean.Parser.instReprLeadingIdentBehavior = { reprPrec := Lean.Parser.reprLeadingIdentBehavior✝ }

structure Lean.Parser.ParserCategory : Type

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.

• declName : Lean.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.).

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

Equations

• Lean.Parser.instInhabitedParserCategory = { default := { declName := default, kinds := default, tables := default, behavior := default } }

@[reducible, inline]

abbrev Lean.Parser.ParserCategories : Type

Equations

• Lean.Parser.ParserCategories = Lean.PersistentHashMap Lean.Name Lean.Parser.ParserCategory

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 α

@[reducible, inline]

abbrev Lean.Parser.CategoryParserFn : Type

Equations

• Lean.Parser.CategoryParserFn = (Lean.Name → Lean.Parser.ParserFn)

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

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

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

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

Equations

• One or more equations did not get rendered due to their size.

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

Antiquotations

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

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.Parser.setExpected expected = Lean.Parser.withFn (Lean.Parser.setExpectedFn expected)

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

Equations

• One or more equations did not get rendered due to their size.

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 : Bool := false) : Lean.Parser.Parser

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

def Lean.Parser.mkAntiquot (name : String) (kind : Lean.SyntaxNodeKind) (anonymous : Bool := true) (isPseudoKind : 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.

Equations

• One or more equations did not get rendered due to their size.

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

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

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

Equations

• Lean.Parser.withAntiquot antiquotP p = { info := Lean.Parser.orelseInfo antiquotP.info p.info, fn := Lean.Parser.withAntiquotFn antiquotP.fn p.fn }

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

Equations

• Lean.Parser.withoutInfo p = { info := { collectTokens := id, collectKinds := id, firstTokens := Lean.Parser.FirstTokens.unknown }, fn := p.fn }

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

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

def Lean.Parser.withAntiquotSuffixSplice (kind : Lean.SyntaxNodeKind) (p 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 suffix : Lean.Parser.Parser) : Lean.Parser.Parser

Equations

• One or more equations did not get rendered due to their size.

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

End of Antiquotations

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

Equations

• Lean.Parser.sepByElemParser p sep = Lean.Parser.withAntiquotSpliceAndSuffix `sepBy p (Lean.Parser.symbol (sep.trim ++ "*"))

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

Equations

• Lean.Parser.sepBy p sep psep allowTrailingSep = Lean.Parser.sepByNoAntiquot (Lean.Parser.sepByElemParser p sep) psep allowTrailingSep

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

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

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

Equations

• Lean.Parser.leadingParser kind tables behavior antiquotParser = Lean.Parser.withAntiquotFn antiquotParser (Lean.Parser.leadingParserAux kind tables behavior) true

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 : Lean.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 algorithm, precedences are only checked before calling trailing parsers. In our implementation, leading and trailing parsers check the precedence. 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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.Parser.fieldIdx = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "fieldIdx" `fieldIdx) { info := Lean.Parser.mkAtomicInfo "fieldIdx", fn := Lean.Parser.fieldIdxFn }

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

Equations

• Lean.Parser.skip = { info := Lean.Parser.epsilonInfo, fn := fun (x : Lean.Parser.ParserContext) (s : Lean.Parser.ParserState) => s }

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 : β) : β

Equations

• s.foldArgs f b = (s.foldArgsM f b).run

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