Documentation

Lake.Toml.ParserUtil

TOML Parser Utilities #

Generic parser utilities used by Lake's TOML parser.

Equations
Equations
Equations
  • One or more equations did not get rendered due to their size.
@[inline]

ParserFn combinator that runs f with the current position.

Equations

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]

A sequence of n repetitions of a parser function.

Equations
@[specialize #[]]
Equations
Equations
@[inline]
def Lake.Toml.satisfyFn (p : CharBool) (expected : List String := []) :
Equations
  • One or more equations did not get rendered due to their size.
def Lake.Toml.digitFn (expected : List String := ["digit"]) :

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

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

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

Equations

Consume a single matching character.

Equations
partial def Lake.Toml.strAuxFn (str : String) (expected : List String) (strPos : String.Pos) :

Consume a matching string atomically.

Equations
partial def Lake.Toml.sepByChar1AuxFn (p : CharBool) (sep : Char) (expected : List String := []) :
partial def Lake.Toml.sepByChar1Fn (p : CharBool) (sep : Char) (expected : List String := []) :

Push a new atom onto the syntax stack.

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

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

Equations
Equations
Equations
  • One or more equations did not get rendered due to their size.
def Lake.Toml.chAtom (c : Char) (expected : List String := [toString "'" ++ toString c ++ toString "'"]) (trailingFn : Lean.Parser.ParserFn := skipFn) :

Parse a single character as an atom.

Equations

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

Equations

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

Equations
  • One or more equations did not get rendered due to their size.
Equations
Equations
Equations
Equations
  • One or more equations did not get rendered due to their size.
Equations
@[reducible, inline]

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

Equations
Equations
  • One or more equations did not get rendered due to their size.
@[inline]
Equations
  • One or more equations did not get rendered due to their size.
@[inline]
Equations
  • One or more equations did not get rendered due to their size.