@[inline, reducible]

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

Equations

• Lean.Parser.mkAtom info val = Lean.Syntax.atom info val

@[inline, reducible]

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

Equations

• Lean.Parser.mkIdent info rawVal val = Lean.Syntax.ident info rawVal val []

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

Return character after position pos

Equations

• Lean.Parser.getNext input pos = String.get input (String.next input 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.

Equations

• Lean.Parser.maxPrec = 1024

def Lean.Parser.argPrec : Nat

Equations

• Lean.Parser.argPrec = 1023

def Lean.Parser.leadPrec : Nat

Equations

• Lean.Parser.leadPrec = 1022

def Lean.Parser.minPrec : Nat

Equations

• Lean.Parser.minPrec = 10

@[inline, reducible]

abbrev Lean.Parser.Token : Type

Equations

• Lean.Parser.Token = String

@[inline, reducible]

abbrev Lean.Parser.TokenTable : Type

Equations

• Lean.Parser.TokenTable = Lean.Data.Trie Lean.Parser.Token

@[inline, reducible]

abbrev Lean.Parser.SyntaxNodeKindSet : Type

Equations

• Lean.Parser.SyntaxNodeKindSet = Lean.PersistentHashMap Lean.SyntaxNodeKind Unit

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

Equations

• Lean.Parser.SyntaxNodeKindSet.insert s k = Lean.PersistentHashMap.insert s k ()

structure Lean.Parser.InputContext : Type

• input : String
• fileName : String
• fileMap : Lean.FileMap

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.

instance Lean.Parser.instInhabitedInputContext : Inhabited Lean.Parser.InputContext

Equations

• Lean.Parser.instInhabitedInputContext = { default := { input := default, fileName := default, fileMap := default } }

structure Lean.Parser.ParserModuleContext : Type

• env : Lean.Environment
• options : Lean.Options
• currNamespace : Lake.Name
• openDecls : List Lean.OpenDecl

Input context derived from elaboration of previous commands.

structure Lean.Parser.CacheableParserContext : Type

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

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

instance Lean.Parser.instBEqCacheableParserContext : BEq Lean.Parser.CacheableParserContext

Equations

• Lean.Parser.instBEqCacheableParserContext = { beq := Lean.Parser.beqCacheableParserContext✝ }

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

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

Parser context updateable in adaptUncacheableContextFn.

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

Opaque parser context updateable using adaptCacheableContextFn and adaptUncacheableContextFn.

structure Lean.Parser.Error : Type

• unexpectedTk : Lean.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 Lean.Parser.Error

Equations

• Lean.Parser.instInhabitedError = { default := { unexpectedTk := default, unexpected := default, expected := default } }

instance Lean.Parser.instBEqError : BEq Lean.Parser.Error

Equations

• Lean.Parser.instBEqError = { beq := Lean.Parser.beqError✝ }

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

Equations

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

instance Lean.Parser.Error.instToStringError : ToString Lean.Parser.Error

Equations

• Lean.Parser.Error.instToStringError = { toString := Lean.Parser.Error.toString }

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

Equations

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

structure Lean.Parser.TokenCacheEntry : Type

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

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

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

instance Lean.Parser.instBEqParserCacheKey : BEq Lean.Parser.ParserCacheKey

Equations

• Lean.Parser.instBEqParserCacheKey = { beq := Lean.Parser.beqParserCacheKey✝ }

instance Lean.Parser.instHashableParserCacheKey : Hashable Lean.Parser.ParserCacheKey

Equations

• Lean.Parser.instHashableParserCacheKey = { hash := fun k => hash (k.pos, k.parserName) }

structure Lean.Parser.ParserCacheEntry : Type

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

structure Lean.Parser.ParserCache : Type

• tokenCache : Lean.Parser.TokenCacheEntry
• parserCache : Lean.HashMap Lean.Parser.ParserCacheKey Lean.Parser.ParserCacheEntry

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

Equations

• Lean.Parser.initCacheForInput input = { tokenCache := { startPos := String.endPos input + Char.ofNat 32, stopPos := 0, token := Lean.Syntax.missing }, parserCache := ∅ }

structure Lean.Parser.SyntaxStack : Type

• raw : Array Lean.Syntax
• drop : Nat

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

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

Equations

• Lean.Parser.SyntaxStack.toSubarray stack = Array.toSubarray stack.raw stack.drop (Array.size stack.raw)

def Lean.Parser.SyntaxStack.empty : Lean.Parser.SyntaxStack

Equations

• Lean.Parser.SyntaxStack.empty = { raw := #[], drop := 0 }

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

Equations

• Lean.Parser.SyntaxStack.size stack = Array.size stack.raw - stack.drop

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

Equations

• Lean.Parser.SyntaxStack.isEmpty stack = (Lean.Parser.SyntaxStack.size stack == 0)

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

Equations

• Lean.Parser.SyntaxStack.shrink stack n = { raw := Array.shrink stack.raw (stack.drop + n), drop := stack.drop }

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

Equations

• Lean.Parser.SyntaxStack.push stack a = { raw := Array.push stack.raw a, drop := stack.drop }

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

Equations

• Lean.Parser.SyntaxStack.pop stack = if Lean.Parser.SyntaxStack.size stack > 0 then { raw := Array.pop stack.raw, drop := stack.drop } else stack

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

Equations

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

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

Equations

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

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

Equations

• Lean.Parser.SyntaxStack.extract stack start stop = Array.extract stack.raw (stack.drop + start) (stack.drop + stop)

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

Equations

• Lean.Parser.SyntaxStack.instHAppendSyntaxStackArraySyntax = { hAppend := fun stack stxs => { raw := stack.raw ++ stxs, drop := stack.drop } }

structure Lean.Parser.ParserState : Type

• stxStack : Lean.Parser.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 : Lean.Parser.ParserCache
• errorMsg : Option Lean.Parser.Error

@[inline]

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

Equations

• Lean.Parser.ParserState.hasError s = (s.errorMsg != none)

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

Equations

• Lean.Parser.ParserState.stackSize s = Lean.Parser.SyntaxStack.size s.stxStack

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

Equations

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

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

Equations

• Lean.Parser.ParserState.setPos s pos = { stxStack := s.stxStack, lhsPrec := s.lhsPrec, pos := pos, cache := s.cache, errorMsg := s.errorMsg }

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

Equations

• Lean.Parser.ParserState.setCache s cache = { stxStack := s.stxStack, lhsPrec := s.lhsPrec, pos := s.pos, cache := cache, errorMsg := s.errorMsg }

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

Equations

• Lean.Parser.ParserState.pushSyntax s n = { stxStack := Lean.Parser.SyntaxStack.push s.stxStack n, lhsPrec := s.lhsPrec, pos := s.pos, cache := s.cache, errorMsg := s.errorMsg }

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

Equations

• Lean.Parser.ParserState.popSyntax s = { stxStack := Lean.Parser.SyntaxStack.pop s.stxStack, lhsPrec := s.lhsPrec, pos := s.pos, cache := s.cache, errorMsg := s.errorMsg }

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

Equations

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

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

Equations

• Lean.Parser.ParserState.next s input pos = { stxStack := s.stxStack, lhsPrec := s.lhsPrec, pos := String.next input pos, cache := s.cache, errorMsg := s.errorMsg }

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

Equations

• Lean.Parser.ParserState.next' s input pos h = { stxStack := s.stxStack, lhsPrec := s.lhsPrec, pos := String.next' input pos h, cache := s.cache, errorMsg := s.errorMsg }

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

Equations

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

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

Equations

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

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

Equations

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

@[inline]

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• Lean.Parser.ParserState.mkEOIError s expected = Lean.Parser.ParserState.mkUnexpectedError s "unexpected end of input" expected

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

Equations

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

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

Equations

• Lean.Parser.ParserState.mkErrorAt s msg pos initStackSz? = Lean.Parser.ParserState.mkErrorsAt s [msg] pos initStackSz?

def Lean.Parser.ParserState.mkUnexpectedTokenErrors (s : Lean.Parser.ParserState) (ex : List String) (iniPos : optParam String.Pos 0) : Lean.Parser.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.

Equations

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

def Lean.Parser.ParserState.mkUnexpectedTokenError (s : Lean.Parser.ParserState) (msg : String) (iniPos : optParam String.Pos 0) : Lean.Parser.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.

Equations

• Lean.Parser.ParserState.mkUnexpectedTokenError s msg iniPos = Lean.Parser.ParserState.mkUnexpectedTokenErrors s [msg] iniPos

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

Equations

• Lean.Parser.ParserState.mkUnexpectedErrorAt s msg pos = Lean.Parser.ParserState.mkUnexpectedError (Lean.Parser.ParserState.setPos s pos) msg []

def Lean.Parser.ParserFn : Type

Equations

• Lean.Parser.ParserFn = (Lean.Parser.ParserContext → Lean.Parser.ParserState → Lean.Parser.ParserState)

instance Lean.Parser.instInhabitedParserFn : Inhabited Lean.Parser.ParserFn

Equations

• Lean.Parser.instInhabitedParserFn = { default := fun x s => s }

inductive Lean.Parser.FirstTokens : Type

• epsilon: Lean.Parser.FirstTokens
• unknown: Lean.Parser.FirstTokens
• tokens: List Lean.Parser.Token → Lean.Parser.FirstTokens
• optTokens: List Lean.Parser.Token → Lean.Parser.FirstTokens

instance Lean.Parser.instInhabitedFirstTokens : Inhabited Lean.Parser.FirstTokens

Equations

• Lean.Parser.instInhabitedFirstTokens = { default := Lean.Parser.FirstTokens.epsilon }

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

Equations

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

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

Equations

• Lean.Parser.FirstTokens.toOptional x = match x with | Lean.Parser.FirstTokens.tokens tks => Lean.Parser.FirstTokens.optTokens tks | tks => tks

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

Equations

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

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

Equations

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

instance Lean.Parser.FirstTokens.instToStringFirstTokens : ToString Lean.Parser.FirstTokens

Equations

• Lean.Parser.FirstTokens.instToStringFirstTokens = { toString := Lean.Parser.FirstTokens.toStr }

structure Lean.Parser.ParserInfo : Type

• collectTokens : List Lean.Parser.Token → List Lean.Parser.Token
• collectKinds : Lean.Parser.SyntaxNodeKindSet → Lean.Parser.SyntaxNodeKindSet
• firstTokens : Lean.Parser.FirstTokens

instance Lean.Parser.instInhabitedParserInfo : Inhabited Lean.Parser.ParserInfo

Equations

• Lean.Parser.instInhabitedParserInfo = { default := { collectTokens := default, collectKinds := default, firstTokens := default } }

structure Lean.Parser.Parser : Type

• info : Lean.Parser.ParserInfo
• fn : Lean.Parser.ParserFn

instance Lean.Parser.instInhabitedParser : Inhabited Lean.Parser.Parser

Equations

• Lean.Parser.instInhabitedParser = { default := { info := default, fn := default } }

@[inline, reducible]

abbrev Lean.Parser.TrailingParser : Type

Equations

• Lean.Parser.TrailingParser = Lean.Parser.Parser

@[inline]

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

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

Equations

• Lean.Parser.withFn f p = { info := p.info, fn := f p.fn }

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

Equations

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

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

Equations

• Lean.Parser.adaptCacheableContext f = Lean.Parser.withFn (Lean.Parser.adaptCacheableContextFn f)

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

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

Equations

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

def Lean.Parser.withResetCache : Lean.Parser.Parser → Lean.Parser.Parser

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

Equations

• Lean.Parser.withResetCache = Lean.Parser.withFn Lean.Parser.withResetCacheFn

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

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

Equations

• Lean.Parser.adaptUncacheableContextFn f p = Lean.Parser.withResetCacheFn fun c s => p { toParserContextCore := f c.toParserContextCore } s

def Lean.Parser.withCacheFn (parserName : Lake.Name) (p : Lean.Parser.ParserFn) : Lean.Parser.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.

Equations

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

def Lean.Parser.withCache (parserName : Lake.Name) : Lean.Parser.Parser → Lean.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.

Equations

• Lean.Parser.withCache parserName = Lean.Parser.withFn (Lean.Parser.withCacheFn parserName)

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

Equations

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