@[reducible, inline]

abbrev Lean.Parser.mkAtom (info : SourceInfo) (val : String) : Syntax

@[reducible, inline]

abbrev Lean.Parser.mkIdent (info : SourceInfo) (rawVal : Substring) (val : Name) : Syntax

def Lean.Parser.getNext (input : String) (pos : String.Pos) : Char

Return character after position pos

def Lean.Parser.maxPrec : Nat

Maximal (and function application) precedence. In the standard lean language, no parser has precedence higher than maxPrec.

Note that nothing prevents users from using a higher precedence, but we strongly discourage them from doing it.

def Lean.Parser.argPrec : Nat

def Lean.Parser.leadPrec : Nat

def Lean.Parser.minPrec : Nat

@[reducible, inline]

abbrev Lean.Parser.Token : Type

@[reducible, inline]

abbrev Lean.Parser.TokenTable : Type

@[reducible, inline]

abbrev Lean.Parser.SyntaxNodeKindSet : Type

def Lean.Parser.SyntaxNodeKindSet.insert (s : SyntaxNodeKindSet) (k : SyntaxNodeKind) : SyntaxNodeKindSet

structure Lean.Parser.InputContext : Type

Input string and related data. Recall that the FileMap is a helper structure for mapping String.Pos in the input string to line/column information.

• input : String
• fileName : String
• fileMap : FileMap

instance Lean.Parser.instInhabitedInputContext : Inhabited InputContext

structure Lean.Parser.ParserModuleContext : Type

Input context derived from elaboration of previous commands.

• env : Environment
• options : Options
• currNamespace : Name
• openDecls : List OpenDecl

structure Lean.Parser.CacheableParserContext : Type

Parser context parts that can be updated without invalidating the parser cache.

• prec : Nat
• quotDepth : Nat
• suppressInsideQuot : Bool
• savedPos? : Option String.Pos
• forbiddenTk? : Option Token

instance Lean.Parser.instBEqCacheableParserContext : BEq CacheableParserContext

structure Lean.Parser.ParserContextCoreextends Lean.Parser.InputContext, Lean.Parser.ParserModuleContext, Lean.Parser.CacheableParserContext : Type

Parser context updateable in adaptUncacheableContextFn.

• input : String
• fileName : String
• fileMap : FileMap
• env : Environment
• options : Options
• currNamespace : Name
• openDecls : List OpenDecl
• prec : Nat
• quotDepth : Nat
• suppressInsideQuot : Bool
• savedPos? : Option String.Pos
• forbiddenTk? : Option Token
• tokens : TokenTable

structure Lean.Parser.ParserContextextends Lean.Parser.ParserContextCore : Type

Opaque parser context updateable using adaptCacheableContextFn and adaptUncacheableContextFn.

• input : String
• fileName : String
• fileMap : FileMap
• env : Environment
• options : Options
• currNamespace : Name
• openDecls : List OpenDecl
• prec : Nat
• quotDepth : Nat
• suppressInsideQuot : Bool
• savedPos? : Option String.Pos
• forbiddenTk? : Option Token
• tokens : TokenTable

structure Lean.Parser.Error : Type

• unexpectedTk : Syntax

  If not missing, used for lazily calculating unexpected message and range in mkErrorMessage. Otherwise, ParserState.pos is used as an empty range.

• unexpected : String
• expected : List String

instance Lean.Parser.instInhabitedError : Inhabited Error

instance Lean.Parser.instBEqError : BEq Error

def Lean.Parser.Error.toString (e : Error) : String

instance Lean.Parser.Error.instToString : ToString Error

def Lean.Parser.Error.merge (e₁ e₂ : Error) : Error

structure Lean.Parser.TokenCacheEntry : Type

• startPos : String.Pos
• stopPos : String.Pos
• token : Syntax

structure Lean.Parser.ParserCacheKeyextends Lean.Parser.CacheableParserContext : Type

• prec : Nat
• quotDepth : Nat
• suppressInsideQuot : Bool
• savedPos? : Option String.Pos
• forbiddenTk? : Option Token
• parserName : Name
• pos : String.Pos

instance Lean.Parser.instBEqParserCacheKey : BEq ParserCacheKey

instance Lean.Parser.instHashableParserCacheKey : Hashable ParserCacheKey

structure Lean.Parser.ParserCacheEntry : Type

• stx : Syntax
• lhsPrec : Nat
• newPos : String.Pos
• errorMsg : Option Error

structure Lean.Parser.ParserCache : Type

• tokenCache : TokenCacheEntry
• parserCache : Std.HashMap ParserCacheKey ParserCacheEntry

def Lean.Parser.initCacheForInput (input : String) : ParserCache

structure Lean.Parser.SyntaxStack : Type

A syntax array with an inaccessible prefix, used for sound caching.

• raw : Array Lean.Syntax
• drop : Nat

def Lean.Parser.SyntaxStack.toSubarray (stack : SyntaxStack) : Subarray Syntax

def Lean.Parser.SyntaxStack.empty : SyntaxStack

def Lean.Parser.SyntaxStack.size (stack : SyntaxStack) : Nat

def Lean.Parser.SyntaxStack.isEmpty (stack : SyntaxStack) : Bool

def Lean.Parser.SyntaxStack.shrink (stack : SyntaxStack) (n : Nat) : SyntaxStack

def Lean.Parser.SyntaxStack.push (stack : SyntaxStack) (a : Syntax) : SyntaxStack

def Lean.Parser.SyntaxStack.pop (stack : SyntaxStack) : SyntaxStack

def Lean.Parser.SyntaxStack.back (stack : SyntaxStack) : Syntax

def Lean.Parser.SyntaxStack.get! (stack : SyntaxStack) (i : Nat) : Syntax

def Lean.Parser.SyntaxStack.extract (stack : SyntaxStack) (start stop : Nat) : Array Syntax

instance Lean.Parser.SyntaxStack.instHAppendArraySyntax : HAppend SyntaxStack (Array Syntax) SyntaxStack

structure Lean.Parser.ParserState : Type

• stxStack : SyntaxStack
• lhsPrec : Nat

  Set to the precedence of the preceding (not surrounding) parser by runLongestMatchParser for the use of checkLhsPrec in trailing parsers. Note that with chaining, the preceding parser can be another trailing parser: in 1 * 2 + 3, the preceding parser is '*' when '+' is executed.

• pos : String.Pos
• cache : ParserCache
• errorMsg : Option Error
• recoveredErrors : Array (String.Pos × SyntaxStack × Error)

@[inline]

def Lean.Parser.ParserState.hasError (s : ParserState) : Bool

def Lean.Parser.ParserState.stackSize (s : ParserState) : Nat

def Lean.Parser.ParserState.restore (s : ParserState) (iniStackSz : Nat) (iniPos : String.Pos) : ParserState

def Lean.Parser.ParserState.setPos (s : ParserState) (pos : String.Pos) : ParserState

def Lean.Parser.ParserState.setCache (s : ParserState) (cache : ParserCache) : ParserState

def Lean.Parser.ParserState.pushSyntax (s : ParserState) (n : Syntax) : ParserState

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

def Lean.Parser.ParserState.shrinkStack (s : ParserState) (iniStackSz : Nat) : ParserState

def Lean.Parser.ParserState.next (s : ParserState) (input : String) (pos : String.Pos) : ParserState

def Lean.Parser.ParserState.next' (s : ParserState) (input : String) (pos : String.Pos) (h : ¬input.atEnd pos = true) : ParserState

def Lean.Parser.ParserState.mkNode (s : ParserState) (k : SyntaxNodeKind) (iniStackSz : Nat) : ParserState

def Lean.Parser.ParserState.mkTrailingNode (s : ParserState) (k : SyntaxNodeKind) (iniStackSz : Nat) : ParserState

def Lean.Parser.ParserState.allErrors (s : ParserState) : Array (String.Pos × SyntaxStack × Error)

@[inline]

def Lean.Parser.ParserState.setError (s : ParserState) (e : Error) : ParserState

def Lean.Parser.ParserState.mkError (s : ParserState) (msg : String) : ParserState

def Lean.Parser.ParserState.mkUnexpectedError (s : ParserState) (msg : String) (expected : List String := []) (pushMissing : Bool := true) : ParserState

def Lean.Parser.ParserState.mkEOIError (s : ParserState) (expected : List String := []) : ParserState

def Lean.Parser.ParserState.mkErrorsAt (s : ParserState) (ex : List String) (pos : String.Pos) (initStackSz? : Option Nat := none) : ParserState

def Lean.Parser.ParserState.mkErrorAt (s : ParserState) (msg : String) (pos : String.Pos) (initStackSz? : Option Nat := none) : ParserState

def Lean.Parser.ParserState.mkUnexpectedTokenErrors (s : ParserState) (ex : List String) (iniPos : String.Pos := 0) : ParserState

Reports given 'expected' messages at range of top stack element (assumed to be a single token). Replaces the element with missing and resets position to the token position. iniPos can be specified to avoid this position lookup but still must be identical to the token position.

def Lean.Parser.ParserState.mkUnexpectedTokenError (s : ParserState) (msg : String) (iniPos : String.Pos := 0) : ParserState

Reports given 'expected' message at range of top stack element (assumed to be a single token). Replaces the element with missing and resets position to the token position. iniPos can be specified to avoid this position lookup but still must be identical to the token position.

def Lean.Parser.ParserState.mkUnexpectedErrorAt (s : ParserState) (msg : String) (pos : String.Pos) : ParserState

def Lean.Parser.ParserState.toErrorMsg (ctx : InputContext) (s : ParserState) : String

def Lean.Parser.ParserFn : Type

instance Lean.Parser.instInhabitedParserFn : Inhabited ParserFn

inductive Lean.Parser.FirstTokens : Type

• epsilon : FirstTokens
• unknown : FirstTokens
• tokens : List Token → FirstTokens
• optTokens : List Token → FirstTokens

instance Lean.Parser.instInhabitedFirstTokens : Inhabited FirstTokens

def Lean.Parser.FirstTokens.seq : FirstTokens → FirstTokens → FirstTokens

def Lean.Parser.FirstTokens.toOptional : FirstTokens → FirstTokens

def Lean.Parser.FirstTokens.merge : FirstTokens → FirstTokens → FirstTokens

def Lean.Parser.FirstTokens.toStr : FirstTokens → String

instance Lean.Parser.FirstTokens.instToString : ToString FirstTokens

structure Lean.Parser.ParserInfo : Type

• collectTokens : List Token → List Token
• collectKinds : SyntaxNodeKindSet → SyntaxNodeKindSet
• firstTokens : FirstTokens

instance Lean.Parser.instInhabitedParserInfo : Inhabited ParserInfo

structure Lean.Parser.Parser : Type

• info : ParserInfo
• fn : ParserFn

instance Lean.Parser.instInhabitedParser : Inhabited Parser

@[reducible, inline]

abbrev Lean.Parser.TrailingParser : Type

@[inline]

def Lean.Parser.withFn (f : ParserFn → ParserFn) (p : Parser) : Parser

Create a simple parser combinator that inherits the info of the nested parser.

def Lean.Parser.adaptCacheableContextFn (f : CacheableParserContext → CacheableParserContext) (p : ParserFn) : ParserFn

def Lean.Parser.adaptCacheableContext (f : CacheableParserContext → CacheableParserContext) : Parser → Parser

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

Run p with a fresh cache, restore outer cache afterwards. p may access the entire syntax stack.

def Lean.Parser.withResetCache : Parser → Parser

Run p with a fresh cache, restore outer cache afterwards. p may access the entire syntax stack.

def Lean.Parser.adaptUncacheableContextFn (f : ParserContextCore → ParserContextCore) (p : ParserFn) : ParserFn

Run p under the given context transformation with a fresh cache (see also withResetCacheFn).

def Lean.Parser.withCacheFn (parserName : Name) (p : ParserFn) : ParserFn

Run p and record result in parser cache for any further invocation with this parserName, parser context, and parser state. p cannot access syntax stack elements pushed before the invocation in order to make caching independent of parser history. As this excludes trailing parsers from being cached, we also reset lhsPrec, which is not read but set by leading parsers, to 0 in order to increase cache hits. Finally, errorMsg is also reset to none as a leading parser should not be called in the first place if there was an error.

def Lean.Parser.withCache (parserName : Name) : Parser → Parser

Run p and record result in parser cache for any further invocation with this parserName, parser context, and parser state. p cannot access syntax stack elements pushed before the invocation in order to make caching independent of parser history. As this excludes trailing parsers from being cached, we also reset lhsPrec, which is not read but set by leading parsers, to 0 in order to increase cache hits. Finally, errorMsg is also reset to none as a leading parser should not be called in the first place if there was an error.

def Lean.Parser.ParserFn.run (p : ParserFn) (ictx : InputContext) (pmctx : ParserModuleContext) (tokens : TokenTable) (s : ParserState) : ParserState