TOML Parser Utilities

Generic parser utilities used by Lake's TOML parser.

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

Equations

• Lake.Toml.isBinDigit c = (c == '0' || c == '1')

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

Equations

• Lake.Toml.isOctDigit c = (decide ('0' ≤ c) && decide (c ≤ '7'))

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

Equations

• Lake.Toml.isHexDigit c = (decide ('0' ≤ c) && decide (c ≤ '9') || decide ('a' ≤ c) && decide (c ≤ 'f') || decide ('A' ≤ c) && decide (c ≤ 'F'))

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

Equations

• Lake.Toml.skipFn x s = s

def Lake.Toml.instAndThenParserFn_lake : AndThen Lean.Parser.ParserFn

Equations

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

@[inline]

def Lake.Toml.usePosFn (f : String.Pos → Lean.Parser.ParserFn) : Lean.Parser.ParserFn

ParserFn combinator that runs f with the current position.

Equations

• Lake.Toml.usePosFn f c s = f s.pos c s

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

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]

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

A sequence of n repetitions of a parser function.

Equations

• Lake.Toml.repeatFn n p c s = Lake.Toml.repeatFn.loop p c n s

@[specialize #[]]

def Lake.Toml.repeatFn.loop (p : Lean.Parser.ParserFn) (c : Lean.Parser.ParserContext) : Nat → Lean.Parser.ParserState → Lean.Parser.ParserState

Equations

• Lake.Toml.repeatFn.loop p c 0 x = x
• Lake.Toml.repeatFn.loop p c n.succ x = if (p c x).hasError = true then p c x else Lake.Toml.repeatFn.loop p c n (p c x)

def Lake.Toml.mkUnexpectedCharError (s : Lean.Parser.ParserState) (c : Char) (expected : optParam (List String) []) (pushMissing : optParam Bool true) : Lean.Parser.ParserState

Equations

• Lake.Toml.mkUnexpectedCharError s c expected pushMissing = s.mkUnexpectedError (toString "unexpected '" ++ toString c ++ toString "'") expected pushMissing

@[inline]

def Lake.Toml.satisfyFn (p : Char → Bool) (expected : optParam (List String) []) : Lean.Parser.ParserFn

Equations

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

def Lake.Toml.takeWhile1Fn (p : Char → Bool) (expected : optParam (List String) []) : Lean.Parser.ParserFn

Equations

• Lake.Toml.takeWhile1Fn p expected = HAndThen.hAndThen (Lake.Toml.satisfyFn p expected) fun (x : Unit) => Lean.Parser.takeWhileFn p

def Lake.Toml.digitFn (expected : optParam (List String) ["digit"]) : Lean.Parser.ParserFn

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

Equations

• Lake.Toml.digitFn expected = Lake.Toml.satisfyFn Char.isDigit expected

def Lake.Toml.digitPairFn (expected : optParam (List String) ["digit"]) : Lean.Parser.ParserFn

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

Equations

• Lake.Toml.digitPairFn expected = HAndThen.hAndThen (Lake.Toml.digitFn expected) fun (x : Unit) => Lake.Toml.digitFn expected

def Lake.Toml.chFn (c : Char) (expected : optParam (List String) [toString "'" ++ toString c ++ toString "'"]) : Lean.Parser.ParserFn

Consume a single matching character.

Equations

• Lake.Toml.chFn c expected = Lake.Toml.satisfyFn (fun (d : Char) => d == c) expected

partial def Lake.Toml.strAuxFn (str : String) (expected : List String) (strPos : String.Pos) : Lean.Parser.ParserFn

def Lake.Toml.strFn (str : String) (expected : optParam (List String) [toString "'" ++ toString str ++ toString "'"]) : Lean.Parser.ParserFn

Consume a matching string atomically.

Equations

• Lake.Toml.strFn str expected = Lean.Parser.atomicFn (Lake.Toml.strAuxFn str expected 0)

partial def Lake.Toml.sepByChar1AuxFn (p : Char → Bool) (sep : Char) (expected : optParam (List String) []) : Lean.Parser.ParserFn

partial def Lake.Toml.sepByChar1Fn (p : Char → Bool) (sep : Char) (expected : optParam (List String) []) : Lean.Parser.ParserFn

def Lake.Toml.pushAtom (startPos : String.Pos) (trailingFn : optParam Lean.Parser.ParserFn Lake.Toml.skipFn) : Lean.Parser.ParserFn

Push a new atom onto the syntax stack.

Equations

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

def Lake.Toml.atomFn (p : Lean.Parser.ParserFn) (trailingFn : optParam Lean.Parser.ParserFn Lake.Toml.skipFn) : Lean.Parser.ParserFn

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

Equations

• Lake.Toml.atomFn p trailingFn c s = if (p c s).hasError = true then p c s else Lake.Toml.pushAtom s.pos trailingFn c (p c s)

def Lake.Toml.atom (p : Lean.Parser.ParserFn) (trailingFn : optParam Lean.Parser.ParserFn Lake.Toml.skipFn) : Lean.Parser.Parser

Equations

• Lake.Toml.atom p trailingFn = { info := { collectTokens := id, collectKinds := id, firstTokens := Lean.Parser.FirstTokens.unknown }, fn := Lake.Toml.atomFn p trailingFn }

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

Equations

• Lake.Toml.getInfoExprPos? (Lean.SourceInfo.synthetic pos endPos canonical) = some pos
• Lake.Toml.getInfoExprPos? x = none

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

Equations

• Lake.Toml.getSyntaxExprPos? (Lean.Syntax.node info kind args) = Lake.Toml.getInfoExprPos? info
• Lake.Toml.getSyntaxExprPos? (Lean.Syntax.atom info val) = Lake.Toml.getInfoExprPos? info
• Lake.Toml.getSyntaxExprPos? (Lean.Syntax.ident info rawVal val preresolved) = Lake.Toml.getInfoExprPos? info
• Lake.Toml.getSyntaxExprPos? Lean.Syntax.missing = none

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

Equations

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

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

Equations

• Lake.Toml.atom.parenthesizer x✝ x = Lean.PrettyPrinter.Parenthesizer.visitToken

def Lake.Toml.chAtom (c : Char) (expected : optParam (List String) [toString "'" ++ toString c ++ toString "'"]) (trailingFn : optParam Lean.Parser.ParserFn Lake.Toml.skipFn) : Lean.Parser.Parser

Parse a single character as an atom.

Equations

• Lake.Toml.chAtom c expected trailingFn = Lake.Toml.atom (Lake.Toml.chFn c expected) trailingFn

def Lake.Toml.chAtom.formatter (c : Char) : List String → Lean.Parser.ParserFn → Lean.PrettyPrinter.Formatter

Equations

• Lake.Toml.chAtom.formatter c x✝ x = Lean.PrettyPrinter.Formatter.rawCh.formatter c

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

Equations

• Lake.Toml.chAtom.parenthesizer x✝¹ x✝ x = Lean.PrettyPrinter.Parenthesizer.visitToken

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

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

Equations

• Lake.Toml.strAtom s expected trailingFn = Lake.Toml.atom (Lake.Toml.strFn s.trim expected) trailingFn

def Lake.Toml.strAtom.formatter (s : String) : List String → Lean.Parser.ParserFn → Lean.PrettyPrinter.Formatter

Equations

• Lake.Toml.strAtom.formatter s x✝ x = Lean.PrettyPrinter.Formatter.symbolNoAntiquot.formatter s

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

Equations

• Lake.Toml.strAtom.parenthesizer x✝¹ x✝ x = Lean.PrettyPrinter.Parenthesizer.visitToken

def Lake.Toml.pushLit (kind : Lean.SyntaxNodeKind) (startPos : String.Pos) (trailingFn : optParam Lean.Parser.ParserFn Lake.Toml.skipFn) : Lean.Parser.ParserFn

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

Equations

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

def Lake.Toml.litFn (kind : Lean.SyntaxNodeKind) (p : Lean.Parser.ParserFn) (trailingFn : optParam Lean.Parser.ParserFn Lake.Toml.skipFn) : Lean.Parser.ParserFn

Equations

• Lake.Toml.litFn kind p trailingFn c s = if (p c s).hasError = true then p c s else Lake.Toml.pushLit kind s.pos trailingFn c (p c s)

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

Equations

• Lake.Toml.lit kind p trailingFn = { info := { collectTokens := id, collectKinds := id, firstTokens := Lean.Parser.FirstTokens.unknown }, fn := Lake.Toml.litFn kind p trailingFn }

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

Equations

• Lake.Toml.lit.formatter kind x✝ x = Lean.PrettyPrinter.Formatter.visitAtom kind

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

Equations

• Lake.Toml.lit.parenthesizer x✝¹ x✝ x = Lean.PrettyPrinter.Parenthesizer.visitToken

def Lake.Toml.litWithAntiquot (name : String) (kind : Lean.SyntaxNodeKind) (p : Lean.Parser.ParserFn) (trailingFn : optParam Lean.Parser.ParserFn Lake.Toml.skipFn) (anonymous : optParam Bool false) : Lean.Parser.Parser

Equations

• Lake.Toml.litWithAntiquot name kind p trailingFn anonymous = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot name kind anonymous) (Lake.Toml.lit kind p trailingFn)

@[inline]

def Lake.Toml.epsilon (fn : Lean.Parser.ParserFn) : Lean.Parser.Parser

Equations

• Lake.Toml.epsilon fn = { info := Lean.Parser.epsilonInfo, fn := fn }

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

Equations

• Lake.Toml.epsilon.formatter x = pure ()

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

Equations

• Lake.Toml.epsilon.parenthesizer x = pure ()

def Lake.Toml.SourceInfo.updateTrailing (trailing : Substring) : Lean.SourceInfo → Lean.SourceInfo

Equations

• Lake.Toml.SourceInfo.updateTrailing trailing (Lean.SourceInfo.original leading pos trailing_1 endPos) = Lean.SourceInfo.original leading pos trailing endPos
• Lake.Toml.SourceInfo.updateTrailing trailing x = x

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

Equations

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

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

Equations

• Lake.Toml.trailing p = Lake.Toml.epsilon (Lake.Toml.extendTrailingFn p)

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

Equations

• Lake.Toml.dynamicNode p = { info := { collectTokens := id, collectKinds := id, firstTokens := Lean.Parser.FirstTokens.unknown }, fn := p }

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

Equations

• Lake.Toml.dynamicNode.formatter x = do let __do_lift ← Lean.Syntax.MonadTraverser.getCur Lean.PrettyPrinter.Formatter.formatterForKind __do_lift.getKind

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

Equations

• Lake.Toml.dynamicNode.parenthesizer x = do let __do_lift ← Lean.Syntax.MonadTraverser.getCur Lean.PrettyPrinter.Parenthesizer.parenthesizerForKind __do_lift.getKind

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.

Equations

• Lake.Toml.ParserMapFn = (Lean.Parser.Parser → Lean.Parser.Parser)

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

Equations

• Lake.Toml.recNode f = Lake.Toml.dynamicNode (Lake.Toml.recNodeFn f)

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

Equations

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

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

Equations

• Lake.Toml.recNodeWithAntiquot.go name kind f anonymous p = Lean.Parser.withCache kind (Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot name kind anonymous true) (f p))

@[inline]

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

Equations

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

@[inline]

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

Equations

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

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

Equations

• Lake.Toml.skipInsideQuotFn p c s = if c.quotDepth > 0 then s else p c s

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

Equations

• Lake.Toml.skipInsideQuot p = Lean.Parser.withFn Lake.Toml.skipInsideQuotFn p