TOML Grammar

A Lean encoding of the v1.0.0 TOML grammar (en, [abnf]]2) using Lean.Parser objects. The current encoding elides the use of tokens entirely, relying purely on custom parser functions.

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

Is it a TOML control character? (excludes tabs and spaces)

Trailing Functions

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

Consume optional horizontal whitespace (i.e., tab or space).

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

Consumes the LF following a CR in a CRLF newline.

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

Consume a newline.

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

Consumes the body of a comment.

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

Consumes a line comment.

partial def Lake.Toml.wsNewlineFn : Lean.Parser.ParserFn

Consume optional whitespace (space, tab, or newline).

partial def Lake.Toml.trailingFn : Lean.Parser.ParserFn

Consume optional sequence of whitespace / newline(s) / comment (s).

Strings

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

A TOML character escape.

def Lake.Toml.escapeSeqFn (stringGap : Bool) : Lean.Parser.ParserFn

Consumes a TOML string escape sequence after a \.

partial def Lake.Toml.basicStringAuxFn (startPos : String.Pos) : Lean.Parser.ParserFn

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

partial def Lake.Toml.literalStringAuxFn (startPos : String.Pos) : Lean.Parser.ParserFn

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

partial def Lake.Toml.mlLiteralStringAuxFn (startPos : String.Pos) (quoteDepth : Nat) : Lean.Parser.ParserFn

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

partial def Lake.Toml.mlBasicStringAuxFn (startPos : String.Pos) (quoteDepth : Nat) : Lean.Parser.ParserFn

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

Numerals (Date-Times, Floats, and Integers)

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

def Lake.Toml.timeTailFn (allowOffset : Bool) : Lean.Parser.ParserFn

@[inline]

def Lake.Toml.timeTailFn.timeOffsetFn (allowOffset : Bool) (curr : Char) (nextPos : String.Pos) (c : Lean.Parser.ParserContext) (s : Lean.Parser.ParserState) : Lean.Parser.ParserState

def Lake.Toml.timeAuxFn (allowOffset : Bool) : Lean.Parser.ParserFn

def Lake.Toml.timeFn (allowOffset : Bool := false) : Lean.Parser.ParserFn

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

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

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

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

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

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

def Lake.Toml.decNumberTailAuxFn (startPos : String.Pos) (curr : Char) (nextPos : String.Pos) : Lean.Parser.ParserFn

def Lake.Toml.decNumberTailFn (startPos : String.Pos) : Lean.Parser.ParserFn

partial def Lake.Toml.decNumberSepFn (startPos : String.Pos) (curr : Char) (nextPos : String.Pos) : Lean.Parser.ParserFn

partial def Lake.Toml.decNumberAuxFn (startPos : String.Pos) : Lean.Parser.ParserFn

partial def Lake.Toml.decNumberFn (startPos : String.Pos) : Lean.Parser.ParserFn

def Lake.Toml.infAuxFn (startPos : String.Pos) : Lean.Parser.ParserFn

def Lake.Toml.nanAuxFn (startPos : String.Pos) : Lean.Parser.ParserFn

def Lake.Toml.decimalFn (startPos : String.Pos) : Lean.Parser.ParserFn

def Lake.Toml.decNumeralAuxFn (startPos : String.Pos) : Lean.Parser.ParserFn

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

Parsers

def Lake.Toml.trailingWs : Lean.Parser.Parser

def Lake.Toml.trailingSep : Lean.Parser.Parser

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

def Lake.Toml.unquotedKey : Lean.Parser.Parser

def Lake.Toml.basicString : Lean.Parser.Parser

def Lake.Toml.literalString : Lean.Parser.Parser

def Lake.Toml.mlBasicString : Lean.Parser.Parser

def Lake.Toml.mlLiteralString : Lean.Parser.Parser

def Lake.Toml.quotedKey : Lean.Parser.Parser

def Lake.Toml.simpleKey : Lean.Parser.Parser

def Lake.Toml.key : Lean.Parser.Parser

def Lake.Toml.stdTable : Lean.Parser.Parser

def Lake.Toml.arrayTable : Lean.Parser.Parser

def Lake.Toml.table : Lean.Parser.Parser

def Lake.Toml.keyvalCore (val : Lean.Parser.Parser) : Lean.Parser.Parser

def Lake.Toml.expressionCore (val : Lean.Parser.Parser) : Lean.Parser.Parser

def Lake.Toml.header : Lean.Parser.Parser

def Lake.Toml.tomlCore (val : Lean.Parser.Parser) : Lean.Parser.Parser

def Lake.Toml.inlineTableCore (val : Lean.Parser.Parser) : Lean.Parser.Parser

def Lake.Toml.arrayCore (val : Lean.Parser.Parser) : Lean.Parser.Parser

def Lake.Toml.string : Lean.Parser.Parser

def Lake.Toml.true : Lean.Parser.Parser

def Lake.Toml.false : Lean.Parser.Parser

def Lake.Toml.boolean : Lean.Parser.Parser

def Lake.Toml.numeralAntiquot : Lean.Parser.Parser

def Lake.Toml.numeral : Lean.Parser.Parser

def Lake.Toml.numeralOfKind (name : String) (kind : Lean.SyntaxNodeKind) : Lean.Parser.Parser

def Lake.Toml.float : Lean.Parser.Parser

def Lake.Toml.decInt : Lean.Parser.Parser

def Lake.Toml.binNum : Lean.Parser.Parser

def Lake.Toml.octNum : Lean.Parser.Parser

def Lake.Toml.hexNum : Lean.Parser.Parser

def Lake.Toml.dateTime : Lean.Parser.Parser

def Lake.Toml.valCore (val : Lean.Parser.Parser) : Lean.Parser.Parser

def Lake.Toml.val : Lean.Parser.Parser

def Lake.Toml.array : Lean.Parser.Parser

def Lake.Toml.inlineTable : Lean.Parser.Parser

def Lake.Toml.keyval : Lean.Parser.Parser

def Lake.Toml.expression : Lean.Parser.Parser

def Lake.Toml.toml : Lean.Parser.Parser