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)

Equations

• Lake.Toml.isControlChar c = (decide (c = '\x7f') || decide (c < ' ') && c != '\t')

Trailing Functions

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

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

Equations

• Lake.Toml.wsFn = Lean.Parser.takeWhileFn fun (c : Char) => decide (c = ' ') || decide (c = '\t')

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

Consumes the LF following a CR in a CRLF newline.

Equations

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

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

Consume a newline.

Equations

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

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

Consumes the body of a comment.

Equations

• Lake.Toml.commentBodyFn = Lean.Parser.takeUntilFn Lake.Toml.isControlChar

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

Consumes a line comment.

Equations

• Lake.Toml.commentFn = Lake.Toml.chFn '#' ["comment"] >> Lake.Toml.commentBodyFn

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.

Equations

• Lake.Toml.isEscapeChar c = (c == 'b' || c == 't' || c == 'n' || c == 'f' || c == 'r' || c == '\"' || c == '\\')

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

Consumes a TOML string escape sequence after a \.

Equations

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

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

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

Equations

• Lake.Toml.basicStringFn = Lake.Toml.usePosFn fun (startPos : String.Pos) => Lake.Toml.chFn '\"' ["basic string"] >> Lake.Toml.basicStringAuxFn startPos

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

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

Equations

• Lake.Toml.literalStringFn = Lake.Toml.usePosFn fun (startPos : String.Pos) => Lake.Toml.chFn '\'' ["literal string"] >> Lake.Toml.literalStringAuxFn startPos

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

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

Equations

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

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

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

Equations

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

Numerals (Date-Times, Floats, and Integers)

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

Equations

• Lake.Toml.hourMinFn = Lake.Toml.digitPairFn ["hour digit"] >> Lake.Toml.chFn ':' >> Lake.Toml.digitPairFn ["minute digit"]

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

Equations

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

@[inline]

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

Equations

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

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

Equations

• Lake.Toml.timeAuxFn allowOffset = Lake.Toml.digitPairFn ["minute digit"] >> Lake.Toml.chFn ':' >> Lake.Toml.digitPairFn ["second digit"] >> Lake.Toml.timeTailFn allowOffset

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

Equations

• Lake.Toml.timeFn allowOffset = Lake.Toml.digitPairFn ["hour"] >> Lake.Toml.chFn ':' >> Lake.Toml.timeAuxFn allowOffset

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

Equations

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

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

Equations

• Lake.Toml.dateTimeAuxFn = Lake.Toml.digitPairFn ["month digit"] >> Lake.Toml.chFn '-' >> Lake.Toml.digitPairFn ["day digit"] >> Lake.Toml.optTimeFn

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

Equations

• Lake.Toml.dateTimeFn = Lake.Toml.repeatFn 4 (Lake.Toml.digitFn ["year digit"]) >> Lake.Toml.chFn '-' >> Lake.Toml.dateTimeAuxFn

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

Equations

• Lake.Toml.dateTimeLitFn = Lake.Toml.litFn `Lake.Toml.dateTime Lake.Toml.dateTimeFn

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• Lake.Toml.infAuxFn startPos = Lake.Toml.strFn "nf" ["'inf'"] >> Lake.Toml.pushLit `Lake.Toml.float startPos

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

Equations

• Lake.Toml.nanAuxFn startPos = Lake.Toml.strFn "an" ["'nan'"] >> Lake.Toml.pushLit `Lake.Toml.float startPos

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

Equations

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

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

Equations

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

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

Equations

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

Parsers

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

Equations

• Lake.Toml.trailingWs = Lake.Toml.trailing Lake.Toml.wsFn

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

Equations

• Lake.Toml.trailingSep = Lake.Toml.trailing Lake.Toml.trailingFn

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

Equations

• Lake.Toml.unquotedKeyFn = Lake.Toml.takeWhile1Fn (fun (c : Char) => c.isAlphanum || c == '_' || c == '-') ["unquoted key"]

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

Equations

• Lake.Toml.unquotedKey = Lake.Toml.litWithAntiquot "unquotedKey" `Lake.Toml.unquotedKey Lake.Toml.unquotedKeyFn

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

Equations

• Lake.Toml.basicString = Lake.Toml.litWithAntiquot "basicString" `Lake.Toml.basicString Lake.Toml.basicStringFn

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

Equations

• Lake.Toml.literalString = Lake.Toml.litWithAntiquot "literalString" `Lake.Toml.literalString Lake.Toml.literalStringFn

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

Equations

• Lake.Toml.mlBasicString = Lake.Toml.litWithAntiquot "mlBasicString" `Lake.Toml.mlBasicString Lake.Toml.mlBasicStringFn

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

Equations

• Lake.Toml.mlLiteralString = Lake.Toml.litWithAntiquot "mlLiteralString" `Lake.Toml.mlLiteralString Lake.Toml.mlLiteralStringFn

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

Equations

• Lake.Toml.quotedKey = (Lake.Toml.basicString <|> Lake.Toml.literalString)

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

Equations

• Lake.Toml.simpleKey = Lean.Parser.nodeWithAntiquot "simpleKey" `Lake.Toml.simpleKey (Lake.Toml.unquotedKey <|> Lake.Toml.quotedKey) true

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• Lake.Toml.table = (Lake.Toml.stdTable <|> Lake.Toml.arrayTable)

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

Equations

• Lake.Toml.keyvalCore val = Lean.Parser.nodeWithAntiquot "keyval" `Lake.Toml.keyval (Lake.Toml.key >> Lake.Toml.trailingWs >> Lake.Toml.chAtom '=' >> Lake.Toml.trailingWs >> val) true

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

Equations

• Lake.Toml.expressionCore val = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "expression" `Lake.Toml.expression true true) (Lake.Toml.keyvalCore val <|> Lake.Toml.table)

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

Equations

• Lake.Toml.header = Lake.Toml.litWithAntiquot "header" `Lake.Toml.header Lake.Toml.skipFn Lake.Toml.trailingFn

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

Equations

• Lake.Toml.tomlCore val = Lean.Parser.nodeWithAntiquot "toml" `Lake.Toml.toml (Lake.Toml.header >> Lake.Toml.sepByLinebreak (Lake.Toml.expressionCore val >> Lake.Toml.trailingSep)) true

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• Lake.Toml.true = Lake.Toml.lit `Lake.Toml.true (Lake.Toml.strFn "true")

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

Equations

• Lake.Toml.false = Lake.Toml.lit `Lake.Toml.false (Lake.Toml.strFn "false")

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

Equations

• Lake.Toml.boolean = Lean.Parser.nodeWithAntiquot "boolean" `Lake.Toml.boolean (Lake.Toml.true <|> Lake.Toml.false)

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

Equations

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

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

Equations

• Lake.Toml.numeral = Lean.Parser.withAntiquot Lake.Toml.numeralAntiquot (Lake.Toml.dynamicNode Lake.Toml.numeralFn)

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

Equations

• Lake.Toml.numeralOfKind name kind = Lake.Toml.numeral >> Lean.Parser.setExpected [name] (Lean.Parser.checkStackTop (fun (x : Lean.Syntax) => x.isOfKind kind) "illegal numeral kind")

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

Equations

• Lake.Toml.float = Lake.Toml.numeralOfKind "float" `Lake.Toml.float

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

Equations

• Lake.Toml.decInt = Lake.Toml.numeralOfKind "decimal integer" `Lake.Toml.decInt

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

Equations

• Lake.Toml.binNum = Lake.Toml.numeralOfKind "binary number" `Lake.Toml.binNum

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

Equations

• Lake.Toml.octNum = Lake.Toml.numeralOfKind "octal number" `Lake.Toml.octNum

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

Equations

• Lake.Toml.hexNum = Lake.Toml.numeralOfKind "hexadecimal number" `Lake.Toml.hexNum

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

Equations

• Lake.Toml.dateTime = Lake.Toml.numeralOfKind "date-time" `Lake.Toml.dateTime

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

Equations

• Lake.Toml.valCore val = (Lake.Toml.string <|> Lake.Toml.boolean <|> Lake.Toml.numeral <|> Lake.Toml.arrayCore val <|> Lake.Toml.inlineTableCore val)

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

Equations

• Lake.Toml.val = Lake.Toml.recNodeWithAntiquot "val" `Lake.Toml.val Lake.Toml.valCore true

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

Equations

• Lake.Toml.array = Lake.Toml.arrayCore Lake.Toml.val

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

Equations

• Lake.Toml.inlineTable = Lake.Toml.inlineTableCore Lake.Toml.val

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

Equations

• Lake.Toml.keyval = Lake.Toml.keyvalCore Lake.Toml.val

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

Equations

• Lake.Toml.expression = Lake.Toml.expressionCore Lake.Toml.val

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

Equations

• Lake.Toml.toml = Lean.Parser.withCache `Lake.Toml.toml (Lake.Toml.tomlCore Lake.Toml.val)