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

Equations

• Lean.Parser.epsilonInfo = { collectTokens := id, collectKinds := id, firstTokens := Lean.Parser.FirstTokens.epsilon }

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

Equations

• Lean.Parser.checkStackTopFn p msg x s = if p (Lean.Parser.SyntaxStack.back s.stxStack) = true then s else Lean.Parser.ParserState.mkUnexpectedError s msg []

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

Equations

• Lean.Parser.andthenFn p q c s = let s := p c s; if Lean.Parser.ParserState.hasError s = true then s else q c s

@[noinline]

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

Equations

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

def Lean.Parser.andthen (p : Lean.Parser.Parser) (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

Equations

• Lean.Parser.instAndThenParser = { andThen := fun a b => Lean.Parser.andthen a (b ()) }

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

Equations

• Lean.Parser.nodeFn n p c s = let iniSz := Lean.Parser.ParserState.stackSize s; let s := p c s; Lean.Parser.ParserState.mkNode s n iniSz

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

Equations

• Lean.Parser.trailingNodeFn n p c s = let iniSz := Lean.Parser.ParserState.stackSize s; let s := p c s; Lean.Parser.ParserState.mkTrailingNode s n iniSz

@[noinline]

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

Equations

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

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

Equations

• Lean.Parser.node n p = { info := Lean.Parser.nodeInfo n p.info, fn := Lean.Parser.nodeFn n p.fn }

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

Equations

• Lean.Parser.errorFn msg x s = Lean.Parser.ParserState.mkUnexpectedError s msg []

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

Equations

• Lean.Parser.error msg = { info := Lean.Parser.epsilonInfo, fn := Lean.Parser.errorFn msg }

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

Equations

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

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.

Equations

• Lean.Parser.errorAtSavedPos msg delta = { info := { collectTokens := id, collectKinds := id, firstTokens := Lean.Parser.FirstTokens.unknown }, fn := Lean.Parser.errorAtSavedPosFn msg delta }

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

Succeeds if c.prec <= prec

Equations

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

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

Equations

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

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

Equations

• Lean.Parser.checkLhsPrec prec = { info := Lean.Parser.epsilonInfo, fn := Lean.Parser.checkLhsPrecFn prec }

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

Equations

• Lean.Parser.setLhsPrecFn prec x s = if Lean.Parser.ParserState.hasError s = true then s else { stxStack := s.stxStack, lhsPrec := prec, pos := s.pos, cache := s.cache, errorMsg := s.errorMsg }

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

Equations

• Lean.Parser.setLhsPrec prec = { info := Lean.Parser.epsilonInfo, fn := Lean.Parser.setLhsPrecFn prec }

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 = HAndThen.hAndThen (Lean.Parser.checkPrec prec) fun x => HAndThen.hAndThen (Lean.Parser.node n p) fun x => 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 : Nat) (lhsPrec : Nat) (p : Lean.Parser.Parser) : Lean.Parser.TrailingParser

Equations

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

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.

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

Equations

• Lean.Parser.instBEqOrElseOnAntiquotBehavior = { beq := Lean.Parser.beqOrElseOnAntiquotBehavior✝ }

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

Equations

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

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

Equations

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

@[noinline]

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

Equations

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

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.

Equations

• Lean.Parser.orelse p q = { info := Lean.Parser.orelseInfo p.info q.info, fn := Lean.Parser.orelseFn p.fn q.fn }

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

Equations

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

@[noinline]

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

Equations

• Lean.Parser.noFirstTokenInfo info = { collectTokens := info.collectTokens, collectKinds := info.collectKinds, firstTokens := Lean.Parser.FirstTokens.unknown }

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

Equations

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

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

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

Equations

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

@[noinline]

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

Equations

• Lean.Parser.optionaInfo p = { collectTokens := p.collectTokens, collectKinds := p.collectKinds, firstTokens := Lean.Parser.FirstTokens.toOptional p.firstTokens }

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

Equations

• Lean.Parser.optionalNoAntiquot p = { info := Lean.Parser.optionaInfo p.info, fn := Lean.Parser.optionalFn p.fn }

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

Equations

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

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.

Equations

• Lean.Parser.lookahead = Lean.Parser.withFn Lean.Parser.lookaheadFn

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

Equations

• Lean.Parser.manyFn p c s = let iniSz := Lean.Parser.ParserState.stackSize s; let s := Lean.Parser.manyAux p c s; Lean.Parser.ParserState.mkNode s Lean.nullKind iniSz

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

Equations

• Lean.Parser.manyNoAntiquot p = { info := Lean.Parser.noFirstTokenInfo p.info, fn := Lean.Parser.manyFn p.fn }

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

Equations

• Lean.Parser.many1Fn p c s = let iniSz := Lean.Parser.ParserState.stackSize s; let s := Lean.Parser.andthenFn p (Lean.Parser.manyAux p) c s; Lean.Parser.ParserState.mkNode s Lean.nullKind iniSz

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 : Lean.Parser.ParserFn) (sep : Lean.Parser.ParserFn) : Lean.Parser.ParserFn

Equations

• Lean.Parser.sepByFn allowTrailingSep p sep c s = let iniSz := Lean.Parser.ParserState.stackSize s; Lean.Parser.sepByFnAux p sep allowTrailingSep iniSz true c s

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

Equations

• Lean.Parser.sepBy1Fn allowTrailingSep p sep c s = let iniSz := Lean.Parser.ParserState.stackSize s; Lean.Parser.sepByFnAux p sep allowTrailingSep iniSz false c s

@[noinline]

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

Equations

• Lean.Parser.sepByInfo p sep = { collectTokens := p.collectTokens ∘ sep.collectTokens, collectKinds := p.collectKinds ∘ sep.collectKinds, firstTokens := Lean.Parser.FirstTokens.unknown }

@[noinline]

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

Equations

• Lean.Parser.sepBy1Info p sep = { collectTokens := p.collectTokens ∘ sep.collectTokens, collectKinds := p.collectKinds ∘ sep.collectKinds, firstTokens := p.firstTokens }

def Lean.Parser.sepByNoAntiquot (p : Lean.Parser.Parser) (sep : Lean.Parser.Parser) (allowTrailingSep : optParam 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 : Lean.Parser.Parser) (sep : Lean.Parser.Parser) (allowTrailingSep : optParam 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

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

@[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 => if (Lean.Syntax.getNumArgs stx == 1) = true then Lean.Syntax.getArg stx 0 else stx

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

Equations

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

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 => !p c

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

Equations

• Lean.Parser.takeWhile1Fn p errorMsg = Lean.Parser.andthenFn (Lean.Parser.satisfyFn p errorMsg) (Lean.Parser.takeWhileFn p)

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 = Lean.Parser.ParserState.mkUnexpectedError s "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 : optParam 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 = let startPos := s.pos; let s := p c s; if Lean.Parser.ParserState.hasError s = true then s else Lean.Parser.rawAux startPos trailingWs c s

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

Equations

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

def Lean.Parser.rawCh (c : Char) (trailingWs : optParam 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

Equations

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

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

Equations

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

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

Equations

• Lean.Parser.isQuotableCharDefault c = (c == Char.ofNat 92 || c == Char.ofNat 34 || c == Char.ofNat 39 || c == Char.ofNat 114 || c == Char.ofNat 110 || c == Char.ofNat 116)

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

Equations

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

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

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

Equations

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

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

Equations

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

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

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

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

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

Equations

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

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

Equations

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

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.

def Lean.Parser.mkIdResult (startPos : String.Pos) (tk : Option Lean.Parser.Token) (val : Lake.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 : Lake.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 : Lake.Name) (c : Lean.Parser.ParserContext) (s : Lean.Parser.ParserState) : Lean.Parser.ParserState

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

Equations

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

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 = let tkc := s.cache.tokenCache; if (tkc.startPos == s.pos) = true then (s, Except.ok tkc.token) else Lean.Parser.peekTokenAux c s

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

Treat keywords as identifiers.

Equations

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

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 : String) (errorMsg : String) : Lean.Parser.ParserFn

Equations

• Lean.Parser.symbolFnAux sym errorMsg = Lean.Parser.satisfySymbolFn (fun s => s == sym) [errorMsg]

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

Equations

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

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

Equations

• Lean.Parser.symbolFn sym = Lean.Parser.symbolFnAux sym ("'" ++ sym ++ "'")

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

Equations

• Lean.Parser.symbolNoAntiquot sym = let sym := String.trim sym; { info := Lean.Parser.symbolInfo sym, fn := Lean.Parser.symbolFn sym }

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

Equations

• Lean.Parser.checkTailNoWs prev = match Lean.Syntax.getTailInfo prev with | Lean.SourceInfo.original leading pos trailing endPos => trailing.stopPos == trailing.startPos | x => false

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

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

Equations

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

def Lean.Parser.strAux (sym : String) (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 : 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

Equations

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

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

Equations

• Lean.Parser.checkWsBeforeFn errorMsg x s = let prev := Lean.Parser.SyntaxStack.back s.stxStack; if Lean.Parser.checkTailWs prev = true then s else Lean.Parser.ParserState.mkError s errorMsg

def Lean.Parser.checkWsBefore (errorMsg : optParam 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.

Equations

• Lean.Parser.checkWsBefore errorMsg = { info := Lean.Parser.epsilonInfo, fn := Lean.Parser.checkWsBeforeFn errorMsg }

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

Equations

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

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

Equations

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

def Lean.Parser.checkLinebreakBefore (errorMsg : optParam 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.

Equations

• Lean.Parser.checkLinebreakBefore errorMsg = { info := Lean.Parser.epsilonInfo, fn := Lean.Parser.checkLinebreakBeforeFn errorMsg }

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

Equations

• Lean.Parser.checkNoWsBeforeFn errorMsg x s = let prev := Lean.Parser.pickNonNone s.stxStack; if Lean.Parser.checkTailNoWs prev = true then s else Lean.Parser.ParserState.mkError s errorMsg

def Lean.Parser.checkNoWsBefore (errorMsg : optParam 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.

Equations

• Lean.Parser.checkNoWsBefore errorMsg = { info := Lean.Parser.epsilonInfo, fn := Lean.Parser.checkNoWsBeforeFn errorMsg }

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

Equations

• Lean.Parser.unicodeSymbolFnAux sym asciiSym expected = Lean.Parser.satisfySymbolFn (fun s => s == sym || s == asciiSym) expected

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

Equations

• Lean.Parser.unicodeSymbolInfo sym asciiSym = { collectTokens := fun tks => sym :: asciiSym :: tks, collectKinds := id, firstTokens := Lean.Parser.FirstTokens.tokens [sym, asciiSym] }

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

Equations

• Lean.Parser.unicodeSymbolFn sym asciiSym = Lean.Parser.unicodeSymbolFnAux sym asciiSym ["'" ++ sym ++ "', '" ++ asciiSym ++ "'"]

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

Equations

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

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

Equations

• Lean.Parser.mkAtomicInfo k = { collectTokens := id, collectKinds := id, firstTokens := Lean.Parser.FirstTokens.tokens [k] }

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

Equations

• Lean.Parser.numLitFn = Lean.Parser.expectTokenFn Lean.numLitKind "numeral"

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

Equations

• Lean.Parser.numLitNoAntiquot = { info := Lean.Parser.mkAtomicInfo "num", fn := Lean.Parser.numLitFn }

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

Equations

• Lean.Parser.scientificLitFn = Lean.Parser.expectTokenFn Lean.scientificLitKind "scientific number"

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

Equations

• Lean.Parser.scientificLitNoAntiquot = { info := Lean.Parser.mkAtomicInfo "scientific", fn := Lean.Parser.scientificLitFn }

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

Equations

• Lean.Parser.charLitNoAntiquot = { info := Lean.Parser.mkAtomicInfo "char", fn := Lean.Parser.charLitFn }

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

Equations

• Lean.Parser.nameLitFn = Lean.Parser.expectTokenFn Lean.nameLitKind "Name literal"

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

Equations

• Lean.Parser.nameLitNoAntiquot = { info := Lean.Parser.mkAtomicInfo "name", fn := Lean.Parser.nameLitFn }

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 : Lake.Name) : Lean.Parser.ParserFn

Equations

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

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

Equations

• Lean.Parser.identEq id = { info := Lean.Parser.mkAtomicInfo "ident", fn := Lean.Parser.identEqFn id }

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

Equations

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

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 = let node := Lean.Parser.SyntaxStack.back s; Lean.Parser.SyntaxStack.push (Lean.Parser.SyntaxStack.shrink s startStackSize) node

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

Equations

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

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

Equations

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

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

Equations

• Lean.Parser.ParserState.replaceLongest s startStackSize = Lean.Parser.ParserState.keepLatest s startStackSize

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

Equations

• Lean.Parser.invalidLongestMatchParser s = Lean.Parser.ParserState.mkError s "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 : Nat) (startLhsPrec : Nat) (startPos : String.Pos) (prevPrio : Nat) (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

Equations

• Lean.Parser.longestMatchMkResult startSize s = if Lean.Parser.ParserState.stackSize s > startSize + 1 then Lean.Parser.ParserState.mkNode s Lean.choiceKind startSize else s

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

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

Equations

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

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

Equations

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

def Lean.Parser.checkColEq (errorMsg : optParam 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.

Equations

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

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

Equations

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

def Lean.Parser.checkColGe (errorMsg : optParam 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 : optParam 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.

Equations

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

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 : optParam 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

Equations

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

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.

Equations

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

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.

Equations

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

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 = let i := s.pos; if String.atEnd c.toParserContextCore.toInputContext.input i = true then s else Lean.Parser.ParserState.mkError s "expected end of file"

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

Equations

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

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

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

Equations

• Lean.Parser.TokenMap α = Lean.RBMap Lake.Name (List α) Lean.Name.quickCmp

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

Equations

• Lean.Parser.TokenMap.insert map 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.instInhabitedTokenMap {α : Type} : Inhabited (Lean.Parser.TokenMap α)

Equations

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

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

Equations

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

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

Equations

• Lean.Parser.TokenMap.instForInTokenMapProdNameList = inferInstanceAs (ForIn m (Lean.RBMap Lake.Name (List α) Lean.Name.quickCmp) (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

Equations

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

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

Equations

• Lean.Parser.instInhabitedLeadingIdentBehavior = { default := Lean.Parser.LeadingIdentBehavior.default }

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

• 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

Equations

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

@[inline, reducible]

abbrev Lean.Parser.ParserCategories : Type

Equations

• Lean.Parser.ParserCategories = Lean.PersistentHashMap Lake.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 α

Equations

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

@[inline, reducible]

abbrev Lean.Parser.CategoryParserFn : Type

Equations

• Lean.Parser.CategoryParserFn = (Lake.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 : Lake.Name) : Lean.Parser.ParserFn

Equations

• Lean.Parser.categoryParserFn catName ctx s = Lean.EnvExtension.getState Lean.Parser.categoryParserFnExtension ctx.toParserContextCore.toParserModuleContext.env catName ctx s

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

Equations

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

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

Equations

• Lean.Parser.termParser prec = Lean.Parser.categoryParser `term prec

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

Equations

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

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

Equations

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

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

Equations

• Lean.Parser.antiquotExpr = HOrElse.hOrElse Lean.Parser.identNoAntiquot fun x => HOrElse.hOrElse (Lean.Parser.symbolNoAntiquot "_") fun x => Lean.Parser.antiquotNestedExpr

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

Equations

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

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

Equations

• Lean.Parser.symbol sym = Lean.Parser.tokenWithAntiquot (Lean.Parser.symbolNoAntiquot sym)

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

Equations

• Lean.Parser.instCoeStringParser = { coe := Lean.Parser.symbol }

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

Equations

• Lean.Parser.nonReservedSymbol sym includeIdent = Lean.Parser.tokenWithAntiquot (Lean.Parser.nonReservedSymbolNoAntiquot sym includeIdent)

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

Equations

• Lean.Parser.unicodeSymbol sym asciiSym = Lean.Parser.tokenWithAntiquot (Lean.Parser.unicodeSymbolNoAntiquot sym asciiSym)

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.

Equations

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

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

Equations

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

def Lean.Parser.withAntiquot (antiquotP : Lean.Parser.Parser) (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 false }

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 : Lean.Parser.Parser) (suffix : Lean.Parser.Parser) : Lean.Parser.Parser

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

Equations

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

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.

Equations

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

def Lean.Parser.withAntiquotSpliceAndSuffix (kind : Lean.SyntaxNodeKind) (p : Lean.Parser.Parser) (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 : optParam Bool false) : Lean.Parser.Parser

Equations

• Lean.Parser.nodeWithAntiquot name kind p anonymous = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot name kind anonymous) (Lean.Parser.node kind p)

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 (String.trim sep ++ "*"))

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

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 : optParam Lean.Parser.Parser (Lean.Parser.symbol sep)) (allowTrailingSep : optParam Bool false) : Lean.Parser.Parser

Equations

• Lean.Parser.sepBy1 p sep psep allowTrailingSep = Lean.Parser.sepBy1NoAntiquot (Lean.Parser.sepByElemParser p sep) psep allowTrailingSep

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

Equations

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

def Lean.Parser.leadingParser (kind : Lake.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

Equations

• Lean.Parser.trailingLoopStep tables left ps c s = Lean.Parser.longestMatchFn (some left) (ps ++ tables.trailingParsers) c s

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.

Equations

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

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 true) { 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 s => 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 β

Equations

• Lean.Syntax.foldArgsM s f b = Array.foldlM (flip f) b (Lean.Syntax.getArgs s) 0 (Array.size (Lean.Syntax.getArgs s))

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

Equations

• Lean.Syntax.foldArgs s f b = Id.run (Lean.Syntax.foldArgsM s f b)

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

Equations

• Lean.Syntax.forArgsM s f = Lean.Syntax.foldArgsM s (fun s x => f s) ()