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

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

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

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.

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

Match an arbitrary parser or do nothing.

@[inline]

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

A sequence of n repetitions of a parser function.

@[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

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

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.

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 := skipFn) : Lean.Parser.ParserFn

Push a new atom onto the syntax stack.

def Lake.Toml.atomFn (p : Lean.Parser.ParserFn) (trailingFn : Lean.Parser.ParserFn := 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 := skipFn) : Lean.Parser.Parser

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

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

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

def Lake.Toml.chAtom (c : Char) (expected : List String := [toString "'" ++ toString c ++ toString "'"]) (trailingFn : Lean.Parser.ParserFn := 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

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

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

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

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

def Lake.Toml.pushLit (kind : Lean.SyntaxNodeKind) (startPos : String.Pos) (trailingFn : Lean.Parser.ParserFn := 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 := skipFn) : Lean.Parser.ParserFn

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

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

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

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

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

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

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

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

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

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.

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

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

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

@[inline]

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

@[inline]

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

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

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