- success {α ι : Type} (pos : ι) (res : α) : ParseResult α ι
- error {α ι : Type} (pos : ι) (err : String) : ParseResult α ι
Instances For
instance
Std.Internal.Parsec.instReprParseResult
{α✝ ι✝ : Type}
[Repr α✝]
[Repr ι✝]
:
Repr (ParseResult α✝ ι✝)
Equations
Equations
- Std.Internal.Parsec ι α = (ι → Std.Internal.Parsec.ParseResult α ι)
Instances For
class
Std.Internal.Parsec.Input
(ι : Type)
(elem idx : outParam Type)
[DecidableEq idx]
[DecidableEq elem]
:
- pos : ι → idx
- next : ι → ι
- curr : ι → elem
- hasNext : ι → Bool
Instances
Equations
- Std.Internal.Parsec.instInhabited = { default := fun (it : ι) => Std.Internal.Parsec.ParseResult.error it "" }
@[inline]
Equations
Instances For
@[inline]
Equations
- f.bind g it = match f it with | Std.Internal.Parsec.ParseResult.success rem a => g a rem | Std.Internal.Parsec.ParseResult.error pos msg => Std.Internal.Parsec.ParseResult.error pos msg
Instances For
@[always_inline]
Equations
@[inline]
Equations
- Std.Internal.Parsec.fail msg it = Std.Internal.Parsec.ParseResult.error it msg
Instances For
@[inline]
def
Std.Internal.Parsec.tryCatch
{α ι elem idx : Type}
[DecidableEq idx]
[DecidableEq elem]
[Input ι elem idx]
{β : Type}
(p : Parsec ι α)
(csuccess : α → Parsec ι β)
(cerror : Unit → Parsec ι β)
:
Parsec ι β
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[inline]
def
Std.Internal.Parsec.orElse
{α ι elem idx : Type}
[DecidableEq idx]
[DecidableEq elem]
[Input ι elem idx]
(p : Parsec ι α)
(q : Unit → Parsec ι α)
:
Parsec ι α
Instances For
@[inline]
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[always_inline]
instance
Std.Internal.Parsec.instAlternative
{ι elem idx : Type}
[DecidableEq idx]
[DecidableEq elem]
[Input ι elem idx]
:
Alternative (Parsec ι)
Equations
- Std.Internal.Parsec.instAlternative = Alternative.mk (fun {α : Type} => Std.Internal.Parsec.fail "") fun {α : Type} => Std.Internal.Parsec.orElse
Equations
- Std.Internal.Parsec.expectedEndOfInput = "expected end of input"
Instances For
@[inline]
def
Std.Internal.Parsec.eof
{ι elem idx : Type}
[DecidableEq idx]
[DecidableEq elem]
[Input ι elem idx]
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[inline]
def
Std.Internal.Parsec.isEof
{ι elem idx : Type}
[DecidableEq idx]
[DecidableEq elem]
[Input ι elem idx]
:
Equations
Instances For
@[specialize #[]]
partial def
Std.Internal.Parsec.manyCore
{α ι elem idx : Type}
[DecidableEq idx]
[DecidableEq elem]
[Input ι elem idx]
(p : Parsec ι α)
(acc : Array α)
:
@[inline]
def
Std.Internal.Parsec.many
{α ι elem idx : Type}
[DecidableEq idx]
[DecidableEq elem]
[Input ι elem idx]
(p : Parsec ι α)
:
Equations
- p.many = p.manyCore #[]
Instances For
@[inline]
def
Std.Internal.Parsec.many1
{α ι elem idx : Type}
[DecidableEq idx]
[DecidableEq elem]
[Input ι elem idx]
(p : Parsec ι α)
:
Equations
- p.many1 = do let __do_lift ← p p.manyCore #[__do_lift]
Instances For
Equations
- Std.Internal.Parsec.unexpectedEndOfInput = "unexpected end of input"
Instances For
@[inline]
def
Std.Internal.Parsec.any
{ι elem idx : Type}
[DecidableEq idx]
[DecidableEq elem]
[Input ι elem idx]
:
Parsec ι elem
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[inline]
def
Std.Internal.Parsec.satisfy
{ι elem idx : Type}
[DecidableEq idx]
[DecidableEq elem]
[Input ι elem idx]
(p : elem → Bool)
:
Parsec ι elem
Equations
- Std.Internal.Parsec.satisfy p = (do let c ← Std.Internal.Parsec.any if p c = true then pure c else Std.Internal.Parsec.fail "condition not satisfied").attempt
Instances For
@[inline]
def
Std.Internal.Parsec.peek?
{ι elem idx : Type}
[DecidableEq idx]
[DecidableEq elem]
[Input ι elem idx]
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[inline]
def
Std.Internal.Parsec.peek!
{ι elem idx : Type}
[DecidableEq idx]
[DecidableEq elem]
[Input ι elem idx]
:
Parsec ι elem
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[inline]
def
Std.Internal.Parsec.peekD
{ι elem idx : Type}
[DecidableEq idx]
[DecidableEq elem]
[Input ι elem idx]
(default : elem)
:
Parsec ι elem
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[inline]
def
Std.Internal.Parsec.skip
{ι elem idx : Type}
[DecidableEq idx]
[DecidableEq elem]
[Input ι elem idx]
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[specialize #[]]
partial def
Std.Internal.Parsec.manyCharsCore
{ι elem idx : Type}
[DecidableEq idx]
[DecidableEq elem]
[Input ι elem idx]
(p : Parsec ι Char)
(acc : String)
:
@[inline]
def
Std.Internal.Parsec.manyChars
{ι elem idx : Type}
[DecidableEq idx]
[DecidableEq elem]
[Input ι elem idx]
(p : Parsec ι Char)
:
Equations
- p.manyChars = p.manyCharsCore ""
Instances For
@[inline]
def
Std.Internal.Parsec.many1Chars
{ι elem idx : Type}
[DecidableEq idx]
[DecidableEq elem]
[Input ι elem idx]
(p : Parsec ι Char)
:
Equations
- p.many1Chars = do let __do_lift ← p p.manyCharsCore __do_lift.toString