TOML Parser Utilities

Generic parser utilities used by Lake's TOML parser.

def Lake.Toml.isBinDigit (c : Char) : Bool

def Lake.Toml.isOctDigit (c : Char) : Bool

Equations

• Lake.Toml.isOctDigit c = (decide ('0' ≤ c) && decide (c ≤ '7'))

def Lake.Toml.isHexDigit (c : Char) : Bool

def Lake.Toml.skipFn : Lean.Parser.ParserFn

Equations

• Lake.Toml.skipFn x s = s

def Lake.Toml.instAndThenParserFn_lake : AndThen Lean.Parser.ParserFn

@[inline]

def Lake.Toml.usePosFn (f : String.Pos → Lean.Parser.ParserFn) : Lean.Parser.ParserFn

ParserFn combinator that runs f with the current position.

Equations

• Lake.Toml.usePosFn f c s = f s.pos c s

def Lake.Toml.optFn (p : Lean.Parser.ParserFn) : Lean.Parser.ParserFn

Match an arbitrary parser or do nothing.

Equations

• Lake.Toml.optFn 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

@[inline]

def Lake.Toml.repeatFn (n : Nat) (p : Lean.Parser.ParserFn) : Lean.Parser.ParserFn

A sequence of n repetitions of a parser function.

Equations

• Lake.Toml.repeatFn n p c s = Lake.Toml.repeatFn.loop p c n s

@[specialize #[]]

def Lake.Toml.repeatFn.loop (p : Lean.Parser.ParserFn) (c : Lean.Parser.ParserContext) : Nat → Lean.Parser.ParserState → Lean.Parser.ParserState

def Lake.Toml.mkUnexpectedCharError (s : Lean.Parser.ParserState) (c : Char) (expected : List String := []) (pushMissing : Bool := true) : Lean.Parser.ParserState

@[inline]

def Lake.Toml.satisfyFn (p : Char → Bool) (expected : List String := []) : Lean.Parser.ParserFn

Equations

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

def Lake.Toml.takeWhile1Fn (p : Char → Bool) (expected : List String := []) : Lean.Parser.ParserFn

def Lake.Toml.digitFn (expected : List String := ["digit"]) : Lean.Parser.ParserFn

Consume a single digit (i.e., Char.isDigit).

def Lake.Toml.digitPairFn (expected : List String := ["digit"]) : Lean.Parser.ParserFn

Consume a two digits (i.e., Char.isDigit).

Equations

• Lake.Toml.digitPairFn expected = Lake.Toml.digitFn expected >> Lake.Toml.digitFn expected

def Lake.Toml.chFn (c : Char) (expected : List String := [toString "'" ++ toString c ++ toString "'"]) : Lean.Parser.ParserFn

Consume a single matching character.

partial def Lake.Toml.strAuxFn (str : String) (expected : List String) (strPos : String.Pos) : Lean.Parser.ParserFn

def Lake.Toml.strFn (str : String) (expected : List String := [toString "'" ++ toString str ++ toString "'"]) : Lean.Parser.ParserFn

Consume a matching string atomically.

Equations

• Lake.Toml.strFn str expected = Lean.Parser.atomicFn (Lake.Toml.strAuxFn str expected 0)

partial def Lake.Toml.sepByChar1AuxFn (p : Char → Bool) (sep : Char) (expected : List String := []) : Lean.Parser.ParserFn

partial def Lake.Toml.sepByChar1Fn (p : Char → Bool) (sep : Char) (expected : List String := []) : Lean.Parser.ParserFn

def Lake.Toml.pushAtom (startPos : String.Pos) (trailingFn : Lean.Parser.ParserFn := Lake.Toml.skipFn) : Lean.Parser.ParserFn

Push a new atom onto the syntax stack.

Equations

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

def Lake.Toml.atomFn (p : Lean.Parser.ParserFn) (trailingFn : Lean.Parser.ParserFn := Lake.Toml.skipFn) : Lean.Parser.ParserFn

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

def Lake.Toml.atom (p : Lean.Parser.ParserFn) (trailingFn : Lean.Parser.ParserFn := Lake.Toml.skipFn) : Lean.Parser.Parser

Equations

• Lake.Toml.atom p trailingFn = { info := { collectTokens := id, collectKinds := id, firstTokens := Lean.Parser.FirstTokens.unknown }, fn := Lake.Toml.atomFn p trailingFn }

def Lake.Toml.getInfoExprPos? : Lean.SourceInfo → Option String.Pos

Equations

• Lake.Toml.getInfoExprPos? (Lean.SourceInfo.synthetic pos endPos canonical) = some pos
• Lake.Toml.getInfoExprPos? x = none

def Lake.Toml.getSyntaxExprPos? : Lean.Syntax → Option String.Pos

Equations

• Lake.Toml.getSyntaxExprPos? (Lean.Syntax.node info kind args) = Lake.Toml.getInfoExprPos? info
• Lake.Toml.getSyntaxExprPos? (Lean.Syntax.atom info val) = Lake.Toml.getInfoExprPos? info
• Lake.Toml.getSyntaxExprPos? (Lean.Syntax.ident info rawVal val preresolved) = Lake.Toml.getInfoExprPos? info
• Lake.Toml.getSyntaxExprPos? Lean.Syntax.missing = none

def Lake.Toml.atom.formatter : Lean.Parser.ParserFn → Lean.Parser.ParserFn → Lean.PrettyPrinter.Formatter

def Lake.Toml.atom.parenthesizer : Lean.Parser.ParserFn → Lean.Parser.ParserFn → Lean.PrettyPrinter.Parenthesizer

Equations

• Lake.Toml.atom.parenthesizer x✝ x = Lean.PrettyPrinter.Parenthesizer.visitToken

def Lake.Toml.chAtom (c : Char) (expected : List String := [toString "'" ++ toString c ++ toString "'"]) (trailingFn : Lean.Parser.ParserFn := Lake.Toml.skipFn) : Lean.Parser.Parser

Parse a single character as an atom.

def Lake.Toml.chAtom.formatter (c : Char) : List String → Lean.Parser.ParserFn → Lean.PrettyPrinter.Formatter

Equations

• Lake.Toml.chAtom.formatter c x✝ x = Lean.PrettyPrinter.Formatter.rawCh.formatter c

def Lake.Toml.chAtom.parenthesizer : Char → List String → Lean.Parser.ParserFn → Lean.PrettyPrinter.Parenthesizer

Equations

• Lake.Toml.chAtom.parenthesizer x✝¹ x✝ x = Lean.PrettyPrinter.Parenthesizer.visitToken

def Lake.Toml.strAtom (s : String) (expected : List String := [toString "'" ++ toString s ++ toString "'"]) (trailingFn : Lean.Parser.ParserFn := Lake.Toml.skipFn) : Lean.Parser.Parser

Parse the trimmed string as an atom (but use the full string for formatting).

Equations

• Lake.Toml.strAtom s expected trailingFn = Lake.Toml.atom (Lake.Toml.strFn s.trim expected) trailingFn

def Lake.Toml.strAtom.formatter (s : String) : List String → Lean.Parser.ParserFn → Lean.PrettyPrinter.Formatter

def Lake.Toml.strAtom.parenthesizer : String → List String → Lean.Parser.ParserFn → Lean.PrettyPrinter.Parenthesizer

Equations

• Lake.Toml.strAtom.parenthesizer x✝¹ x✝ x = Lean.PrettyPrinter.Parenthesizer.visitToken

def Lake.Toml.pushLit (kind : Lean.SyntaxNodeKind) (startPos : String.Pos) (trailingFn : Lean.Parser.ParserFn := Lake.Toml.skipFn) : Lean.Parser.ParserFn

Push (Syntax.node kind <new-atom>) onto the syntax stack.

def Lake.Toml.litFn (kind : Lean.SyntaxNodeKind) (p : Lean.Parser.ParserFn) (trailingFn : Lean.Parser.ParserFn := Lake.Toml.skipFn) : Lean.Parser.ParserFn

Equations

• Lake.Toml.litFn kind p trailingFn c s = if (p c s).hasError = true then p c s else Lake.Toml.pushLit kind s.pos trailingFn c (p c s)

def Lake.Toml.lit (kind : Lean.SyntaxNodeKind) (p : Lean.Parser.ParserFn) (trailingFn : Lean.Parser.ParserFn := Lake.Toml.skipFn) : Lean.Parser.Parser

Equations

• Lake.Toml.lit kind p trailingFn = { info := { collectTokens := id, collectKinds := id, firstTokens := Lean.Parser.FirstTokens.unknown }, fn := Lake.Toml.litFn kind p trailingFn }

def Lake.Toml.lit.formatter (kind : Lean.SyntaxNodeKind) : Lean.Parser.ParserFn → Lean.Parser.ParserFn → Lean.PrettyPrinter.Formatter

Equations

• Lake.Toml.lit.formatter kind x✝ x = Lean.PrettyPrinter.Formatter.visitAtom kind

def Lake.Toml.lit.parenthesizer : Lean.SyntaxNodeKind → Lean.Parser.ParserFn → Lean.Parser.ParserFn → Lean.PrettyPrinter.Parenthesizer

def Lake.Toml.litWithAntiquot (name : String) (kind : Lean.SyntaxNodeKind) (p : Lean.Parser.ParserFn) (trailingFn : Lean.Parser.ParserFn := Lake.Toml.skipFn) (anonymous : Bool := false) : Lean.Parser.Parser

@[inline]

def Lake.Toml.epsilon (fn : Lean.Parser.ParserFn) : Lean.Parser.Parser

def Lake.Toml.epsilon.formatter : Lean.Parser.ParserFn → Lean.PrettyPrinter.Formatter

Equations

• Lake.Toml.epsilon.formatter x = pure ()

def Lake.Toml.epsilon.parenthesizer : Lean.Parser.ParserFn → Lean.PrettyPrinter.Parenthesizer

Equations

• Lake.Toml.epsilon.parenthesizer x = pure ()

def Lake.Toml.SourceInfo.updateTrailing (trailing : Substring) : Lean.SourceInfo → Lean.SourceInfo

partial def Lake.Toml.modifyTailInfo (f : Lean.SourceInfo → Lean.SourceInfo) (stx : Lean.Syntax) : Lean.Syntax

def Lake.Toml.extendTrailingFn (p : Lean.Parser.ParserFn) : Lean.Parser.ParserFn

Equations

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

def Lake.Toml.trailing (p : Lean.Parser.ParserFn) : Lean.Parser.Parser

def Lake.Toml.dynamicNode (p : Lean.Parser.ParserFn) : Lean.Parser.Parser

Equations

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

def Lake.Toml.dynamicNode.formatter : Lean.Parser.ParserFn → Lean.PrettyPrinter.Formatter

def Lake.Toml.dynamicNode.parenthesizer : Lean.Parser.ParserFn → Lean.PrettyPrinter.Parenthesizer

Equations

• Lake.Toml.dynamicNode.parenthesizer x = do let __do_lift ← Lean.Syntax.MonadTraverser.getCur Lean.PrettyPrinter.Parenthesizer.parenthesizerForKind __do_lift.getKind

partial def Lake.Toml.recNodeFn (f : Lean.Parser.Parser → Lean.Parser.Parser) : Lean.Parser.ParserFn

@[reducible, inline]

abbrev Lake.Toml.ParserMapFn : Type

Parser → Parser hidden by an abbrev. Prevents the formatter/parenthesizer generator from transforming it.

Equations

• Lake.Toml.ParserMapFn = (Lean.Parser.Parser → Lean.Parser.Parser)

def Lake.Toml.recNode (f : Lake.Toml.ParserMapFn) : Lean.Parser.Parser

Equations

• Lake.Toml.recNode f = Lake.Toml.dynamicNode (Lake.Toml.recNodeFn f)

def Lake.Toml.recNodeWithAntiquot (name : String) (kind : Lean.SyntaxNodeKind) (f : Lake.Toml.ParserMapFn) (anonymous : Bool := false) : Lean.Parser.Parser

Equations

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

def Lake.Toml.recNodeWithAntiquot.go (name : String) (kind : Lean.SyntaxNodeKind) (f : Lake.Toml.ParserMapFn) (anonymous : Bool := false) (p : Lean.Parser.Parser) : Lean.Parser.Parser

Equations

• Lake.Toml.recNodeWithAntiquot.go name kind f anonymous p = Lean.Parser.withCache kind (Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot name kind anonymous true) (f p))

@[inline]

def Lake.Toml.sepByLinebreak (p : Lean.Parser.Parser) (allowTrailingLinebreak : Bool := true) : Lean.Parser.Parser

Equations

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

@[inline]

def Lake.Toml.sepBy1Linebreak (p : Lean.Parser.Parser) (allowTrailingLinebreak : Bool := true) : Lean.Parser.Parser

Equations

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

def Lake.Toml.skipInsideQuotFn (p : Lean.Parser.ParserFn) : Lean.Parser.ParserFn

def Lake.Toml.skipInsideQuot (p : Lean.Parser.Parser) : Lean.Parser.Parser

Equations

• Lake.Toml.skipInsideQuot p = Lean.Parser.withFn Lake.Toml.skipInsideQuotFn p