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

Equations

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

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

Equations

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

@[noinline]

def Lean.Parser.epsilonInfo : ParserInfo

Equations

• Lean.Parser.epsilonInfo = { firstTokens := Lean.Parser.FirstTokens.epsilon }

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

Equations

• Lean.Parser.checkStackTopFn p msg x✝ s = if p s.stxStack.back = true then s else s.mkUnexpectedError msg

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

Equations

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

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

Equations

• Lean.Parser.andthenInfo p q = { collectTokens := p.collectTokens ∘ q.collectTokens, collectKinds := p.collectKinds ∘ q.collectKinds, firstTokens := p.firstTokens.seq q.firstTokens }

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

Equations

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

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

Equations

• Lean.Parser.nodeFn n p c s = (p c s).mkNode n s.stackSize

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

Equations

• Lean.Parser.trailingNodeFn n p c s = (p c s).mkTrailingNode n s.stackSize

@[noinline]

def Lean.Parser.nodeInfo (n : SyntaxNodeKind) (p : ParserInfo) : 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 : SyntaxNodeKind) (p : 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) : ParserFn

Equations

• Lean.Parser.errorFn msg x✝ s = s.mkUnexpectedError msg

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

Equations

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

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

Equations

• Lean.Parser.errorAtSavedPosFn msg delta c s = match c.savedPos? with | none => s | some pos => let pos := if delta = true then c.input.next pos else pos; s.mkUnexpectedErrorAt msg pos

def Lean.Parser.errorAtSavedPos (msg : String) (delta : Bool) : 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 = { fn := Lean.Parser.errorAtSavedPosFn msg delta }

def Lean.Parser.checkPrecFn (prec : Nat) : 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) : Parser

Equations

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

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

Succeeds if c.lhsPrec >= prec

Equations

• Lean.Parser.checkLhsPrecFn prec x✝ s = if s.lhsPrec ≥ prec then s else s.mkUnexpectedError "unexpected token at this precedence level; consider parenthesizing the term"

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

def Lean.Parser.suppressInsideQuot : Parser → Parser

Equations

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

def Lean.Parser.leadingNode (n : SyntaxNodeKind) (prec : Nat) (p : 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 : SyntaxNodeKind) (p : 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 : SyntaxNodeKind) (prec lhsPrec : Nat) (p : Parser) : TrailingParser

Equations

• Lean.Parser.trailingNode n prec lhsPrec p = Lean.Parser.checkPrec prec >> Lean.Parser.checkLhsPrec lhsPrec >> Lean.Parser.trailingNodeAux n p >> Lean.Parser.setLhsPrec prec

def Lean.Parser.mergeOrElseErrors (s : ParserState) (error1 : Error) (iniPos : String.Pos) (mergeErrors : Bool) : 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 : OrElseOnAntiquotBehavior
• takeLongest : OrElseOnAntiquotBehavior
• merge : OrElseOnAntiquotBehavior

Instances For

• Lean.Parser.instBEqOrElseOnAntiquotBehavior

instance Lean.Parser.instBEqOrElseOnAntiquotBehavior : BEq OrElseOnAntiquotBehavior

Equations

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

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

Equations

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

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

Equations

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

@[noinline]

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

Equations

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

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

Equations

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

def Lean.Parser.atomic : 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

Instances For

• Lean.Parser.instBEqRecoveryContext
• Lean.Parser.instReprRecoveryContext

instance Lean.Parser.instBEqRecoveryContext : BEq RecoveryContext

Equations

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

instance Lean.Parser.instDecidableEqRecoveryContext : DecidableEq RecoveryContext

Equations

• Lean.Parser.instDecidableEqRecoveryContext = Lean.Parser.decEqRecoveryContext✝

instance Lean.Parser.instReprRecoveryContext : Repr RecoveryContext

Equations

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

def Lean.Parser.recoverFn (p : ParserFn) (recover : RecoveryContext → ParserFn) : 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.

Equations

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

def Lean.Parser.recover' (parser : Parser) (handler : RecoveryContext → 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 : 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.

Equations

• Lean.Parser.recover parser handler = Lean.Parser.recover' parser fun (x : Lean.Parser.RecoveryContext) => handler

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

Equations

• Lean.Parser.optionalFn p c s = (if ((p c s).hasError && (p c s).pos == s.pos) = true then (p c s).restore s.stackSize s.pos else p c s).mkNode Lean.nullKind s.stackSize

@[noinline]

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

Equations

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

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

Equations

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

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

Equations

• Lean.Parser.lookaheadFn p c s = if (p c s).hasError = true then p c s else (p c s).restore s.stackSize s.pos

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

Equations

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

def Lean.Parser.notFollowedBy (p : Parser) (msg : String) : 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 = { fn := Lean.Parser.notFollowedByFn p.fn msg }

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

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

Equations

• Lean.Parser.manyFn p c s = (Lean.Parser.manyAux p c s).mkNode Lean.nullKind s.stackSize

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

Equations

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

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

Equations

• Lean.Parser.many1Fn p c s = (Lean.Parser.andthenFn p (Lean.Parser.manyAux p) c s).mkNode Lean.nullKind s.stackSize

def Lean.Parser.many1NoAntiquot : Parser → Parser

Equations

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

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

Equations

• Lean.Parser.sepByFn allowTrailingSep p sep c s = Lean.Parser.sepByFnAux✝ p sep allowTrailingSep s.stackSize true c s

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

Equations

• Lean.Parser.sepBy1Fn allowTrailingSep p sep c s = Lean.Parser.sepByFnAux✝ p sep allowTrailingSep s.stackSize false c s

@[noinline]

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

Equations

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

@[noinline]

def Lean.Parser.sepBy1Info (p sep : ParserInfo) : 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 sep : Parser) (allowTrailingSep : Bool := false) : 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 : Parser) (allowTrailingSep : Bool := false) : 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 : ParserFn) (f : Syntax → Syntax) : 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 : ParserInfo) : ParserInfo

Equations

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

def Lean.Parser.withResultOf (p : Parser) (f : Syntax → Syntax) : 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 : 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") : 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) : ParserFn

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

Equations

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

def Lean.Parser.takeWhile1Fn (p : Char → Bool) (errorMsg : String) : 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) : ParserFn

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

Equations

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

partial def Lean.Parser.whitespace : 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 : ParserFn) (trailingWs : Bool := false) : 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) : 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) : Parser

Equations

• Lean.Parser.rawCh c trailingWs = { fn := Lean.Parser.chFn c trailingWs }

def Lean.Parser.hexDigitFn : ParserFn

Equations

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

partial def Lean.Parser.stringGapFn (seenNewline : Bool) : 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) : 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.

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 == '\' || c == '\"' || c == ''' || c == 'r' || c == 'n' || c == 't')

def Lean.Parser.quotedCharFn : ParserFn

Equations

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

def Lean.Parser.quotedStringFn : 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 : SyntaxNodeKind) (startPos : String.Pos) : ParserFn

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

Equations

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

partial def Lean.Parser.strLitFnAux (startPos : String.Pos) : 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) : 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.

Equations

• Lean.Parser.rawStrLitFnAux startPos = Lean.Parser.rawStrLitFnAux.initState startPos 0

def Lean.Parser.rawStrLitFnAux.errorUnterminated (startPos : String.Pos) (s : ParserState) : 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) : ParserContext → ParserState → 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) : ParserContext → ParserState → 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) : ParserContext → ParserState → 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.

partial def Lean.Parser.takeDigitsFn (isDigit : Char → Bool) (expecting : String) (needDigit : Bool) : ParserFn

Parses a sequence of the form many (many '_' >> many1 digit), but if needDigit is true the parsed result must be nonempty.

Note: this does not report that it is expecting _ if we reach EOI or an unexpected character. Rationale: this error happens if there is already a _, and while sequences of _ are allowed, it's a bit perverse to suggest extending the sequence.

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

def Lean.Parser.numberFnAux : ParserFn

Equations

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

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

Equations

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

def Lean.Parser.mkTokenAndFixPos (startPos : String.Pos) (tk : Option Token) : 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 Token) (val : Name) : ParserFn

Equations

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

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

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

Equations

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

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

Equations

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

def Lean.Parser.peekToken (c : ParserContext) (s : ParserState) : ParserState × Except ParserState 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 : ParserFn

Treat keywords as identifiers.

Equations

• Lean.Parser.rawIdentFn c s = if c.input.atEnd s.pos = true then s.mkEOIError else Lean.Parser.identFnAux s.pos none Lean.Name.anonymous c s

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

def Lean.Parser.nonReservedSymbolNoAntiquot (sym : String) (includeIdent : Bool := false) : 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) : 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 : ParserContext) (s : ParserState) : ParserState

def Lean.Parser.checkTailWs (prev : 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) : ParserFn

Equations

• Lean.Parser.checkWsBeforeFn errorMsg x✝ s = if Lean.Parser.checkTailWs s.stxStack.back = true then s else s.mkError errorMsg

def Lean.Parser.checkWsBefore (errorMsg : String := "space before") : 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 : 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) : 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") : 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) : 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") : 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 asciiSym : String) (expected : List String) : ParserFn

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• Lean.Parser.mkAtomicInfo k = { firstTokens := Lean.Parser.FirstTokens.tokens [k] }

def Lean.Parser.expectTokenFn (k : SyntaxNodeKind) (desc : String) : 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 : ParserFn

Equations

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

def Lean.Parser.numLitNoAntiquot : Parser

Equations

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

def Lean.Parser.scientificLitFn : ParserFn

Equations

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

def Lean.Parser.scientificLitNoAntiquot : Parser

Equations

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

def Lean.Parser.strLitFn : ParserFn

Equations

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

def Lean.Parser.strLitNoAntiquot : Parser

Equations

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

def Lean.Parser.charLitFn : ParserFn

Equations

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

def Lean.Parser.charLitNoAntiquot : Parser

Equations

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

def Lean.Parser.nameLitFn : ParserFn

Equations

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

def Lean.Parser.nameLitNoAntiquot : Parser

Equations

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

def Lean.Parser.identFn : ParserFn

Equations

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

def Lean.Parser.identNoAntiquot : Parser

Equations

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

def Lean.Parser.rawIdentNoAntiquot : Parser

Equations

• Lean.Parser.rawIdentNoAntiquot = { fn := Lean.Parser.rawIdentFn }

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

Equations

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

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

Equations

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

def Lean.Parser.hygieneInfoFn : ParserFn

Equations

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

def Lean.Parser.hygieneInfoNoAntiquot : Parser

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• One or more equations did not get rendered due to their size.
• s.mergeErrors oldStackSize oldError = s

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

Equations

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

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

Equations

• s.replaceLongest startStackSize = s.keepLatest startStackSize

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

Equations

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

def Lean.Parser.runLongestMatchParser (left? : Option Syntax) (startLhsPrec : Nat) (p : ParserFn) : 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 Syntax) (startSize startLhsPrec : Nat) (startPos : String.Pos) (prevPrio prio : Nat) (p : ParserFn) : ParserContext → ParserState → ParserState × Nat

Equations

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

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

Equations

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

def Lean.Parser.longestMatchFnAux (left? : Option Syntax) (startSize startLhsPrec : Nat) (startPos : String.Pos) (prevPrio : Nat) (ps : List (Parser × Nat)) : 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 Syntax) (startSize startLhsPrec : Nat) (startPos : String.Pos) (prevPrio : Nat) (ps : List (Parser × Nat)) : ParserFn

Equations

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

def Lean.Parser.longestMatchFn (left? : Option Syntax) : List (Parser × Nat) → 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 Parser → ParserFn

Equations

• Lean.Parser.anyOfFn [] x✝¹ x✝ = x✝.mkError "anyOf: empty list"
• Lean.Parser.anyOfFn [p] x✝¹ x✝ = p.fn 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) : ParserFn

Equations

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

def Lean.Parser.checkColEq (errorMsg : String := "checkColEq") : 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 = { fn := Lean.Parser.checkColEqFn errorMsg }

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

Equations

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

def Lean.Parser.checkColGe (errorMsg : String := "checkColGe") : 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 = { fn := Lean.Parser.checkColGeFn errorMsg }

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

Equations

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

def Lean.Parser.checkColGt (errorMsg : String := "checkColGt") : 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 = { fn := Lean.Parser.checkColGtFn errorMsg }

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

Equations

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

def Lean.Parser.checkLineEq (errorMsg : String := "checkLineEq") : 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 = { fn := Lean.Parser.checkLineEqFn errorMsg }

def Lean.Parser.withPosition : 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 : Parser → Parser

Equations

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

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

Equations

• Lean.Parser.eoi = { 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 Lean.Name (List α) Lean.Name.quickCmp

Instances For

• Lean.Parser.TokenMap.instEmptyCollection
• Lean.Parser.TokenMap.instForInProdNameList
• Lean.Parser.TokenMap.instInhabited

def Lean.Parser.TokenMap.insert {α : Type} (map : TokenMap α) (k : Name) (v : α) : 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 (TokenMap α)

Equations

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

instance Lean.Parser.TokenMap.instEmptyCollection {α : Type} : EmptyCollection (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 (TokenMap α) (Name × List α)

Equations

• Lean.Parser.TokenMap.instForInProdNameList = inferInstanceAs (ForIn m (Lean.RBMap Lean.Name (List α) Lean.Name.quickCmp) (Lean.Name × List α))

structure Lean.Parser.PrattParsingTables : Type

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

Instances For

• Lean.Parser.instInhabitedPrattParsingTables

instance Lean.Parser.instInhabitedPrattParsingTables : Inhabited PrattParsingTables

Equations

• Lean.Parser.instInhabitedPrattParsingTables = { default := { } }

inductive Lean.Parser.LeadingIdentBehavior : Type

Specifies how the parsing table lookup function behaves for identifiers.

The function Lean.Parser.prattParser uses two tables: one each for leading and trailing parsers. These tables map tokens to parsers. Because keyword tokens are distinct from identifier tokens, keywords and identifiers cannot be confused, even when they are syntactically identical. Specifying an alternative leading identifier behavior allows greater flexiblity and makes it possible to avoid reserved keywords in some situations.

When the leading token is syntactically an identifier, the current syntax category's LeadingIdentBehavior specifies how the parsing table lookup function behaves, and allows controlled “punning” between identifiers and keywords. This feature is used to avoid creating a reserved symbol for each built-in tactic (e.g., apply or assumption). As a result, tactic names can be used as identifiers.

• default : LeadingIdentBehavior

  If the leading token is an identifier, then the parser just executes the parsers associated with the auxiliary token “ident”, which parses identifiers.

• symbol : LeadingIdentBehavior

  If the leading token is an identifier <foo>, and there are parsers P associated with the token <foo>, then the parser executes P. Otherwise, it executes only the parsers associated with the auxiliary token “ident”, which parses identifiers.

• both : LeadingIdentBehavior

  If the leading token is an identifier <foo>, then it executes the parsers associated with token <foo> and parsers associated with the auxiliary token “ident”, which parses identifiers.

Instances For

• Lean.Parser.instBEqLeadingIdentBehavior
• Lean.Parser.instInhabitedLeadingIdentBehavior
• Lean.Parser.instReprLeadingIdentBehavior

instance Lean.Parser.instInhabitedLeadingIdentBehavior : Inhabited LeadingIdentBehavior

Equations

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

instance Lean.Parser.instBEqLeadingIdentBehavior : BEq LeadingIdentBehavior

Equations

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

instance Lean.Parser.instReprLeadingIdentBehavior : Repr 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 : 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 : SyntaxNodeKindSet

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

• tables : PrattParsingTables

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

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

Instances For

• Lean.Parser.instInhabitedParserCategory

instance Lean.Parser.instInhabitedParserCategory : Inhabited 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 : TokenMap α) (c : ParserContext) (s : ParserState) (behavior : LeadingIdentBehavior) : ParserState × List α

Equations

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

@[reducible, inline]

abbrev Lean.Parser.CategoryParserFn : Type

Equations

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

opaque Lean.Parser.categoryParserFnRef : IO.Ref CategoryParserFn

opaque Lean.Parser.categoryParserFnExtension : EnvExtension CategoryParserFn

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

Equations

• Lean.Parser.categoryParserFn catName ctx s = Lean.Parser.categoryParserFnExtension.getState ctx.env Lean.Parser.categoryParserFnExtension.asyncMode catName ctx s

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

Equations

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

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

Equations

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

Antiquotations

def Lean.Parser.checkNoImmediateColon : 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 : ParserFn) : ParserFn

Equations

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

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

Equations

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

def Lean.Parser.pushNone : Parser

Equations

• Lean.Parser.pushNone = { fn := fun (x : Lean.Parser.ParserContext) (s : Lean.Parser.ParserState) => s.pushSyntax Lean.mkNullNode }

def Lean.Parser.antiquotNestedExpr : Parser

Equations

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

def Lean.Parser.antiquotExpr : Parser

Equations

• Lean.Parser.antiquotExpr = (Lean.Parser.identNoAntiquot <|> Lean.Parser.symbolNoAntiquot "_" <|> Lean.Parser.antiquotNestedExpr)

def Lean.Parser.tokenAntiquotFn : ParserFn

Equations

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

def Lean.Parser.tokenWithAntiquot : Parser → Parser

Equations

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

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

Equations

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

instance Lean.Parser.instCoeStringParser : Coe String Parser

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• Lean.Parser.withoutInfo p = { fn := p.fn }

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

Equations

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

def Lean.Parser.nodeWithAntiquot (name : String) (kind : SyntaxNodeKind) (p : Parser) (anonymous : Bool := false) : 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 : Parser) (sep : String) : Parser

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

def Lean.Parser.leadingParser (kind : Name) (tables : PrattParsingTables) (behavior : LeadingIdentBehavior) (antiquotParser : ParserFn) : 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 : PrattParsingTables) (left : Syntax) (ps : List (Parser × Nat)) : 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 : PrattParsingTables) (c : ParserContext) (s : ParserState) : ParserState

def Lean.Parser.prattParser (kind : Name) (tables : PrattParsingTables) (behavior : LeadingIdentBehavior) (antiquotParser : ParserFn) : 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.

Equations

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

def Lean.Parser.fieldIdxFn : ParserFn

Equations

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

def Lean.Parser.fieldIdx : 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 : 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 : Syntax) (f : Syntax → β → m β) (b : β) : m β

Equations

• s.foldArgsM f b = Array.foldlM (flip f) b s.getArgs

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

Equations

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

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

Equations

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