source
inductive Std.Internal.Parsec.Error :
Type

Represents an error that can occur during parsing.

- eof : Error

  Indicates that the parser reached the end of the input unexpectedly.

- other (s : String) : Error

  Represents any other kind of parsing error with an associated message.

Instances For

source
instance Std.Internal.Parsec.instReprError :
Repr Error
Equations

- Std.Internal.Parsec.instReprError = { reprPrec := Std.Internal.Parsec.instReprError.repr }

source
def Std.Internal.Parsec.instReprError.repr :
Error → Nat → Format
Equations

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

Instances For

source
instance Std.Internal.Parsec.instToStringError :
ToString Error
Equations

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

source
inductive Std.Internal.Parsec.ParseResult (α ι : Type) :
Type

The result of parsing some string.

- success {α ι : Type} (pos : ι) (res : α) : ParseResult α ι

  Parsing succeeded, returning the new position `pos` and the parsed result `res`.

- error {α ι : Type} (pos : ι) (err : Error) : ParseResult α ι

  Parsing failed, returning the position `pos` where the error occurred and the error `err`.

Instances For

source
instance Std.Internal.Parsec.instReprParseResult {α✝ ι✝ : Type} [Repr α✝] [Repr ι✝] :
Repr (ParseResult α✝ ι✝)
Equations

- Std.Internal.Parsec.instReprParseResult = { reprPrec := Std.Internal.Parsec.instReprParseResult.repr }

source
def Std.Internal.Parsec.instReprParseResult.repr {α✝ ι✝ : Type} [Repr α✝] [Repr ι✝] :
ParseResult α✝ ι✝ → Nat → Format
Equations

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

Instances For

source
def Std.Internal.Parsec (ι α : Type) :
Type

A `Parsec ι α` represents a parser that consumes input of type `ι` and, produces a `ParseResult` containing a value of type `α` (the result of parsing) and the remaining input.

Equations

- Std.Internal.Parsec ι α = (ι → Std.Internal.Parsec.ParseResult α ι)

Instances For

source
class Std.Internal.Parsec.Input (ι : Type) (elem idx : outParam Type) [DecidableEq idx] [DecidableEq elem] :
Type

Interface for an input iterator with position tracking and lookahead support.

- pos : ι → idx
- next : ι → ι
- curr : ι → elem
- hasNext : ι → Bool
- next' (it : ι) : hasNext it = true → ι
- curr' (it : ι) : hasNext it = true → elem

Instances

source
instance Std.Internal.Parsec.instInhabited {α ι : Type} :
Inhabited (Parsec ι α)
Equations

- Std.Internal.Parsec.instInhabited = { default := fun (it : ι) => Std.Internal.Parsec.ParseResult.error it (Std.Internal.Parsec.Error.other "") }

source
@[inline]
def Std.Internal.Parsec.pure {α ι : Type} (a : α) :
Parsec ι α
Equations

- Std.Internal.Parsec.pure a it = Std.Internal.Parsec.ParseResult.success it a

Instances For

source
@[inline]
def Std.Internal.Parsec.bind {ι α β : Type} (f : Parsec ι α) (g : α → Parsec ι β) :
Parsec ι β
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

source
@[inline]
def Std.Internal.Parsec.fail {α ι : Type} (msg : String) :
Parsec ι α

Parser that always fails with the given error message.

Equations

- Std.Internal.Parsec.fail msg it = Std.Internal.Parsec.ParseResult.error it (Std.Internal.Parsec.Error.other msg)

Instances For

source
@[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 ι β

Try `p`, then decide what to do based on success or failure without consuming input on failure.

Equations

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

Instances For

source
@[always_inline]
instance Std.Internal.Parsec.instMonad {ι : Type} :
Monad (Parsec ι)
Equations

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

source
@[inline]
def Std.Internal.Parsec.orElse {α ι elem idx : Type} [DecidableEq idx] [DecidableEq elem] [Input ι elem idx] (p : Parsec ι α) (q : Unit → Parsec ι α) :
Parsec ι α

Try `p`, and if it fails without consuming input, run `q ()` instead.

Equations

- p.orElse q = p.tryCatch pure q

Instances For

source
@[inline]
def Std.Internal.Parsec.attempt {α ι : Type} (p : Parsec ι α) :
Parsec ι α

Attempt to parse with `p`, but don't consume input on failure.

Equations

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

Instances For

source
@[always_inline]
instance Std.Internal.Parsec.instAlternative {ι elem idx : Type} [DecidableEq idx] [DecidableEq elem] [Input ι elem idx] :
Alternative (Parsec ι)
Equations

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

source
@[inline]
def Std.Internal.Parsec.eof {ι elem idx : Type} [DecidableEq idx] [DecidableEq elem] [Input ι elem idx] :
Parsec ι Unit

Succeeds only if input is at end-of-file.

Equations

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

Instances For

source
@[inline]
def Std.Internal.Parsec.isEof {ι elem idx : Type} [DecidableEq idx] [DecidableEq elem] [Input ι elem idx] :
Parsec ι Bool
Equations

- Std.Internal.Parsec.isEof it = Std.Internal.Parsec.ParseResult.success it !Std.Internal.Parsec.Input.hasNext it

Instances For

source
@[specialize #[]]
partial def Std.Internal.Parsec.manyCore {α ι elem idx : Type} [DecidableEq idx] [DecidableEq elem] [Input ι elem idx] (p : Parsec ι α) (acc : Array α) :
Parsec ι (Array α)
source
@[inline]
def Std.Internal.Parsec.many {α ι elem idx : Type} [DecidableEq idx] [DecidableEq elem] [Input ι elem idx] (p : Parsec ι α) :
Parsec ι (Array α)
Equations

- p.many = p.manyCore #[]

Instances For

source
@[inline]
def Std.Internal.Parsec.many1 {α ι elem idx : Type} [DecidableEq idx] [DecidableEq elem] [Input ι elem idx] (p : Parsec ι α) :
Parsec ι (Array α)
Equations

- p.many1 = do let __do_lift ← p p.manyCore #[__do_lift]

Instances For

source
@[inline]
def Std.Internal.Parsec.any {ι elem idx : Type} [DecidableEq idx] [DecidableEq elem] [Input ι elem idx] :
Parsec ι elem

Gets the next input element.

Equations

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

Instances For

source
@[inline]
def Std.Internal.Parsec.satisfy {ι elem idx : Type} [DecidableEq idx] [DecidableEq elem] [Input ι elem idx] (p : elem → Bool) :
Parsec ι elem

Checks if the next input element matches some condition.

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

source
@[inline]
def Std.Internal.Parsec.notFollowedBy {α ι : Type} (p : Parsec ι α) :
Parsec ι Unit

Fails if `p` succeeds, otherwise succeeds without consuming input.

Equations

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

Instances For

source
@[inline]
def Std.Internal.Parsec.peek? {ι elem idx : Type} [DecidableEq idx] [DecidableEq elem] [Input ι elem idx] :
Parsec ι (Option elem)

Peeks at the next element, returns `some` if exists else `none`, does not consume input.

Equations

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

Instances For

source
@[inline]
def Std.Internal.Parsec.peekWhen? {ι elem idx : Type} [DecidableEq idx] [DecidableEq elem] [Input ι elem idx] (p : elem → Bool) :
Parsec ι (Option elem)

Peeks at the next element, returns `some elem` if it satisfies `p`, else `none`. Does not consume input.

Equations

- Std.Internal.Parsec.peekWhen? p = do let __discr ← Std.Internal.Parsec.peek? match __discr with | some data => if p data = true then pure (some data) else pure none | x => pure none

Instances For

source
@[inline]
def Std.Internal.Parsec.peek! {ι elem idx : Type} [DecidableEq idx] [DecidableEq elem] [Input ι elem idx] :
Parsec ι elem

Peeks at the next element, errors on EOF, does not consume input.

Equations

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

Instances For

source
@[inline]
def Std.Internal.Parsec.peekD {ι elem idx : Type} [DecidableEq idx] [DecidableEq elem] [Input ι elem idx] (default : elem) :
Parsec ι elem

Peeks at the next element or returns a default if at EOF, does not consume input.

Equations

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

Instances For

source
@[inline]
def Std.Internal.Parsec.skip {ι elem idx : Type} [DecidableEq idx] [DecidableEq elem] [Input ι elem idx] :
Parsec ι Unit

Consumes one element if available, otherwise errors on EOF.

Equations

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

Instances For

source
@[specialize #[]]
partial def Std.Internal.Parsec.manyCharsCore {ι elem idx : Type} [DecidableEq idx] [DecidableEq elem] [Input ι elem idx] (p : Parsec ι Char) (acc : String) :
Parsec ι String

Parses zero or more chars with `p`, accumulates into a string.

source
@[inline]
def Std.Internal.Parsec.manyChars {ι elem idx : Type} [DecidableEq idx] [DecidableEq elem] [Input ι elem idx] (p : Parsec ι Char) :
Parsec ι String

Parses zero or more chars with `p` into a string.

Equations

- p.manyChars = p.manyCharsCore ""

Instances For

source
@[inline]
def Std.Internal.Parsec.many1Chars {ι elem idx : Type} [DecidableEq idx] [DecidableEq elem] [Input ι elem idx] (p : Parsec ι Char) :
Parsec ι String

Parses one or more chars with `p` into a string, errors if none.

Equations

- p.many1Chars = do let __do_lift ← p p.manyCharsCore __do_lift.toString

Instances For