TOML Parser Utilities #
Generic parser utilities used by Lake's TOML parser.
Equations
- Lake.Toml.isBinDigit c = (c == '0' || c == '1')
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[inline]
ParserFn
combinator that runs f
with the current position.
Equations
- Lake.Toml.usePosFn f c s = f s.pos c s
Instances For
Match an arbitrary parser or do nothing.
Equations
Instances For
@[inline]
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
Instances For
@[specialize #[]]
Equations
- Lake.Toml.repeatFn.loop p c 0 x = x
- Lake.Toml.repeatFn.loop p c n.succ x = let s := p c x; if s.hasError = true then s else Lake.Toml.repeatFn.loop p c n s
Instances For
def
Lake.Toml.mkUnexpectedCharError
(s : Lean.Parser.ParserState)
(c : Char)
(expected : optParam (List String) [])
(pushMissing : optParam Bool true)
:
Equations
Instances For
Equations
- Lake.Toml.takeWhile1Fn p expected = HAndThen.hAndThen (Lake.Toml.satisfyFn p expected) fun (x : Unit) => Lean.Parser.takeWhileFn p
Instances For
Consume a single digit (i.e., Char.isDigit
).
Equations
- Lake.Toml.digitFn expected = Lake.Toml.satisfyFn Char.isDigit expected
Instances For
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
Instances For
def
Lake.Toml.chFn
(c : Char)
(expected : optParam (List String) [toString "'" ++ toString c ++ toString "'"])
:
Consume a single matching character.
Equations
- Lake.Toml.chFn c expected = Lake.Toml.satisfyFn (fun (d : Char) => d == c) expected
Instances For
def
Lake.Toml.strFn
(str : String)
(expected : optParam (List String) [toString "'" ++ toString str ++ toString "'"])
:
Consume a matching string atomically.
Equations
- Lake.Toml.strFn str expected = Lean.Parser.atomicFn (Lake.Toml.strAuxFn str expected 0)
Instances For
def
Lake.Toml.pushAtom
(startPos : String.Pos)
(trailingFn : optParam Lean.Parser.ParserFn Lake.Toml.skipFn)
:
Push a new atom onto the syntax stack.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Lake.Toml.atomFn
(p : Lean.Parser.ParserFn)
(trailingFn : optParam Lean.Parser.ParserFn Lake.Toml.skipFn)
:
Match an arbitrary ParserFn
and return the consumed String in a Syntax.atom
.
Equations
- Lake.Toml.atomFn p trailingFn c s = let startPos := s.pos; let s := p c s; if s.hasError = true then s else Lake.Toml.pushAtom startPos trailingFn c s
Instances For
def
Lake.Toml.atom
(p : Lean.Parser.ParserFn)
(trailingFn : optParam Lean.Parser.ParserFn Lake.Toml.skipFn)
:
Equations
- Lake.Toml.atom p trailingFn = { info := { collectTokens := id, collectKinds := id, firstTokens := Lean.Parser.FirstTokens.unknown }, fn := Lake.Toml.atomFn p trailingFn }
Instances For
Equations
- Lake.Toml.getInfoExprPos? x = match x with | Lean.SourceInfo.synthetic pos endPos canonical => some pos | x => none
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Lake.Toml.chAtom
(c : Char)
(expected : optParam (List String) [toString "'" ++ toString c ++ toString "'"])
(trailingFn : optParam Lean.Parser.ParserFn Lake.Toml.skipFn)
:
Parse a single character as an atom.
Equations
- Lake.Toml.chAtom c expected trailingFn = Lake.Toml.atom (Lake.Toml.chFn c expected) trailingFn
Instances For
def
Lake.Toml.strAtom
(s : String)
(expected : optParam (List String) [toString "'" ++ toString s ++ toString "'"])
(trailingFn : optParam Lean.Parser.ParserFn Lake.Toml.skipFn)
:
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
Instances For
def
Lake.Toml.pushLit
(kind : Lean.SyntaxNodeKind)
(startPos : String.Pos)
(trailingFn : optParam Lean.Parser.ParserFn Lake.Toml.skipFn)
:
Push (Syntax.node kind <new-atom>)
onto the syntax stack.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Lake.Toml.litFn
(kind : Lean.SyntaxNodeKind)
(p : Lean.Parser.ParserFn)
(trailingFn : optParam Lean.Parser.ParserFn Lake.Toml.skipFn)
:
Equations
- Lake.Toml.litFn kind p trailingFn c s = let iniPos := s.pos; let s := p c s; if s.hasError = true then s else Lake.Toml.pushLit kind iniPos trailingFn c s
Instances For
def
Lake.Toml.lit
(kind : Lean.SyntaxNodeKind)
(p : Lean.Parser.ParserFn)
(trailingFn : optParam Lean.Parser.ParserFn Lake.Toml.skipFn)
:
Equations
- Lake.Toml.lit kind p trailingFn = { info := { collectTokens := id, collectKinds := id, firstTokens := Lean.Parser.FirstTokens.unknown }, fn := Lake.Toml.litFn kind p trailingFn }
Instances For
Equations
- Lake.Toml.lit.formatter kind x✝ x = Lean.PrettyPrinter.Formatter.visitAtom kind
Instances For
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)
:
Equations
- Lake.Toml.litWithAntiquot name kind p trailingFn anonymous = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot name kind anonymous) (Lake.Toml.lit kind p trailingFn)
Instances For
@[inline]
Equations
- Lake.Toml.epsilon fn = { info := Lean.Parser.epsilonInfo, fn := fn }
Instances For
Equations
Instances For
Equations
Instances For
Equations
- Lake.Toml.SourceInfo.updateTrailing trailing x = match x with | Lean.SourceInfo.original leading pos trailing_1 endPos => Lean.SourceInfo.original leading pos trailing endPos | info => info
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
Instances For
Equations
- Lake.Toml.dynamicNode p = { info := { collectTokens := id, collectKinds := id, firstTokens := Lean.Parser.FirstTokens.unknown }, fn := p }
Instances For
Equations
- Lake.Toml.dynamicNode.formatter x = do let __do_lift ← Lean.Syntax.MonadTraverser.getCur Lean.PrettyPrinter.Formatter.formatterForKind __do_lift.getKind
Instances For
Equations
- Lake.Toml.dynamicNode.parenthesizer x = do let __do_lift ← Lean.Syntax.MonadTraverser.getCur Lean.PrettyPrinter.Parenthesizer.parenthesizerForKind __do_lift.getKind
Instances For
@[reducible, inline]
Parser → Parser
hidden by an abbrev
.
Prevents the formatter/parenthesizer generator from transforming it.
Equations
Instances For
Equations
Instances For
def
Lake.Toml.recNodeWithAntiquot
(name : String)
(kind : Lean.SyntaxNodeKind)
(f : Lake.Toml.ParserMapFn)
(anonymous : optParam Bool false)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Lake.Toml.recNodeWithAntiquot.go
(name : String)
(kind : Lean.SyntaxNodeKind)
(f : Lake.Toml.ParserMapFn)
(anonymous : optParam Bool false)
(p : 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))
Instances For
@[inline]
def
Lake.Toml.sepByLinebreak
(p : Lean.Parser.Parser)
(allowTrailingLinebreak : optParam Bool true)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[inline]
def
Lake.Toml.sepBy1Linebreak
(p : Lean.Parser.Parser)
(allowTrailingLinebreak : optParam Bool true)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Lake.Toml.skipInsideQuotFn p c s = if c.quotDepth > 0 then s else p c s