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.
Trailing Functions #
Consume optional horizontal whitespace (i.e., tab or space).
Equations
- Lake.Toml.wsFn = Lean.Parser.takeWhileFn fun (c : Char) => decide (c = ' ') || decide (c = '\t')
Consumes the LF following a CR in a CRLF newline.
Equations
- One or more equations did not get rendered due to their size.
Consume a newline.
Equations
- One or more equations did not get rendered due to their size.
Consumes the body of a comment.
Consumes a line comment.
Equations
- Lake.Toml.commentFn = HAndThen.hAndThen (Lake.Toml.chFn '#' ["comment"]) fun (x : Unit) => Lake.Toml.commentBodyFn
Consume optional whitespace (space, tab, or newline).
Consume optional sequence of whitespace / newline(s) / comment (s).
Strings #
Consumes a TOML string escape sequence after a \
.
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lake.Toml.basicStringFn = Lake.Toml.usePosFn fun (startPos : String.Pos) => HAndThen.hAndThen (Lake.Toml.chFn '\"' ["basic string"]) fun (x : Unit) => Lake.Toml.basicStringAuxFn startPos
Equations
- Lake.Toml.literalStringFn = Lake.Toml.usePosFn fun (startPos : String.Pos) => HAndThen.hAndThen (Lake.Toml.chFn ''' ["literal string"]) fun (x : Unit) => Lake.Toml.literalStringAuxFn startPos
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Numerals (Date-Times, Floats, and Integers) #
Equations
- Lake.Toml.hourMinFn = HAndThen.hAndThen (Lake.Toml.digitPairFn ["hour digit"]) fun (x : Unit) => HAndThen.hAndThen (Lake.Toml.chFn ':') fun (x : Unit) => Lake.Toml.digitPairFn ["minute digit"]
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)
:
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lake.Toml.timeFn allowOffset = HAndThen.hAndThen (Lake.Toml.digitPairFn ["hour"]) fun (x : Unit) => HAndThen.hAndThen (Lake.Toml.chFn ':') fun (x : Unit) => Lake.Toml.timeAuxFn allowOffset
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lake.Toml.dateTimeLitFn = Lake.Toml.litFn `Lake.Toml.dateTime Lake.Toml.dateTimeFn
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lake.Toml.infAuxFn startPos = HAndThen.hAndThen (Lake.Toml.strFn "nf" ["'inf'"]) fun (x : Unit) => Lake.Toml.pushLit `Lake.Toml.float startPos
Equations
- Lake.Toml.nanAuxFn startPos = HAndThen.hAndThen (Lake.Toml.strFn "an" ["'nan'"]) fun (x : Unit) => Lake.Toml.pushLit `Lake.Toml.float startPos
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Parsers #
Equations
- Lake.Toml.unquotedKeyFn = Lake.Toml.takeWhile1Fn (fun (c : Char) => c.isAlphanum || c == '_' || c == '-') ["unquoted key"]
Equations
- Lake.Toml.unquotedKey = Lake.Toml.litWithAntiquot "unquotedKey" `Lake.Toml.unquotedKey Lake.Toml.unquotedKeyFn
Equations
- Lake.Toml.basicString = Lake.Toml.litWithAntiquot "basicString" `Lake.Toml.basicString Lake.Toml.basicStringFn
Equations
- Lake.Toml.literalString = Lake.Toml.litWithAntiquot "literalString" `Lake.Toml.literalString Lake.Toml.literalStringFn
Equations
- Lake.Toml.mlBasicString = Lake.Toml.litWithAntiquot "mlBasicString" `Lake.Toml.mlBasicString Lake.Toml.mlBasicStringFn
Equations
- Lake.Toml.mlLiteralString = Lake.Toml.litWithAntiquot "mlLiteralString" `Lake.Toml.mlLiteralString Lake.Toml.mlLiteralStringFn
Equations
Equations
- Lake.Toml.simpleKey = Lean.Parser.nodeWithAntiquot "simpleKey" `Lake.Toml.simpleKey (HOrElse.hOrElse Lake.Toml.unquotedKey fun (x : Unit) => Lake.Toml.quotedKey) true
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lake.Toml.header = Lake.Toml.litWithAntiquot "header" `Lake.Toml.header Lake.Toml.skipFn Lake.Toml.trailingFn
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lake.Toml.true = Lake.Toml.lit `Lake.Toml.true (Lake.Toml.strFn "true")
Equations
- Lake.Toml.false = Lake.Toml.lit `Lake.Toml.false (Lake.Toml.strFn "false")
Equations
- Lake.Toml.boolean = Lean.Parser.nodeWithAntiquot "boolean" `Lake.Toml.boolean (HOrElse.hOrElse Lake.Toml.true fun (x : Unit) => Lake.Toml.false)
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lake.Toml.float = Lake.Toml.numeralOfKind "float" `Lake.Toml.float
Equations
- Lake.Toml.decInt = Lake.Toml.numeralOfKind "decimal integer" `Lake.Toml.decInt
Equations
- Lake.Toml.binNum = Lake.Toml.numeralOfKind "binary number" `Lake.Toml.binNum
Equations
- Lake.Toml.octNum = Lake.Toml.numeralOfKind "octal number" `Lake.Toml.octNum
Equations
- Lake.Toml.hexNum = Lake.Toml.numeralOfKind "hexadecimal number" `Lake.Toml.hexNum
Equations
- Lake.Toml.dateTime = Lake.Toml.numeralOfKind "date-time" `Lake.Toml.dateTime
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lake.Toml.val = Lake.Toml.recNodeWithAntiquot "val" `Lake.Toml.val Lake.Toml.valCore true
Equations
- Lake.Toml.toml = Lean.Parser.withCache `Lake.Toml.toml (Lake.Toml.tomlCore Lake.Toml.val)