Documentation

Std.Internal.Parsec.Basic

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

success: {α ι : Type} → ι → α → Std.Internal.Parsec.ParseResult α ι
error: {α ι : Type} → ι → String → Std.Internal.Parsec.ParseResult α ι

Instances For

Std.Internal.Parsec.instReprParseResult

instance Std.Internal.Parsec.instReprParseResult :

{α ι : Type} → [inst : Repr α] → [inst : Repr ι] → Repr (Std.Internal.Parsec.ParseResult α ι)

Equations

Std.Internal.Parsec.instReprParseResult = { reprPrec := Std.Internal.Parsec.reprParseResult✝ }

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

Equations

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

Instances For

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

pos : ι → idx
next : ι → ι
curr : ι → elem
hasNext : ι → Bool
next' : (it : ι) → Std.Internal.Parsec.Input.hasNext it = true → ι
curr' : (it : ι) → Std.Internal.Parsec.Input.hasNext it = true → elem

Instances

instance Std.Internal.Parsec.instInhabited {α : Type} {ι : Type} :

Inhabited (Std.Internal.Parsec ι α)

Equations

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

@[inline]

def Std.Internal.Parsec.pure {α : Type} {ι : Type} (a : α) :

Std.Internal.Parsec ι α

Equations

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

@[inline]

def Std.Internal.Parsec.bind {ι : Type} {α : Type} {β : Type} (f : Std.Internal.Parsec ι α) (g : α → Std.Internal.Parsec ι β) :

Std.Internal.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

@[always_inline]

instance Std.Internal.Parsec.instMonad {ι : Type} :

Monad (Std.Internal.Parsec ι)

Equations

Std.Internal.Parsec.instMonad = Monad.mk

@[inline]

def Std.Internal.Parsec.fail {α : Type} {ι : Type} (msg : String) :

Std.Internal.Parsec ι α

Equations

Std.Internal.Parsec.fail msg it = Std.Internal.Parsec.ParseResult.error it msg

@[inline]

def Std.Internal.Parsec.tryCatch {α : Type} {ι : Type} {elem : Type} {idx : Type} [DecidableEq idx] [DecidableEq elem] [Std.Internal.Parsec.Input ι elem idx] {β : Type} (p : Std.Internal.Parsec ι α) (csuccess : α → Std.Internal.Parsec ι β) (cerror : Unit → Std.Internal.Parsec ι β) :

Std.Internal.Parsec ι β

Equations

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

@[inline]

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

Std.Internal.Parsec ι α

Equations

p.orElse q = p.tryCatch pure q

@[inline]

def Std.Internal.Parsec.attempt {α : Type} {ι : Type} (p : Std.Internal.Parsec ι α) :

Std.Internal.Parsec ι α

Equations

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

@[always_inline]

instance Std.Internal.Parsec.instAlternative {ι : Type} {elem : Type} {idx : Type} [DecidableEq idx] [DecidableEq elem] [Std.Internal.Parsec.Input ι elem idx] :

Alternative (Std.Internal.Parsec ι)

Equations

Std.Internal.Parsec.instAlternative = Alternative.mk (fun {α : Type} => Std.Internal.Parsec.fail "") fun {α : Type} => Std.Internal.Parsec.orElse

def Std.Internal.Parsec.expectedEndOfInput :

Equations

Std.Internal.Parsec.expectedEndOfInput = "expected end of input"

@[inline]

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

Std.Internal.Parsec ι Unit

Equations

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

@[inline]

def Std.Internal.Parsec.isEof {ι : Type} {elem : Type} {idx : Type} [DecidableEq idx] [DecidableEq elem] [Std.Internal.Parsec.Input ι elem idx] :

Std.Internal.Parsec ι Bool

Equations

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

@[specialize #[]]

partial def Std.Internal.Parsec.manyCore {α : Type} {ι : Type} {elem : Type} {idx : Type} [DecidableEq idx] [DecidableEq elem] [Std.Internal.Parsec.Input ι elem idx] (p : Std.Internal.Parsec ι α) (acc : Array α) :

Std.Internal.Parsec ι (Array α)

@[inline]

def Std.Internal.Parsec.many {α : Type} {ι : Type} {elem : Type} {idx : Type} [DecidableEq idx] [DecidableEq elem] [Std.Internal.Parsec.Input ι elem idx] (p : Std.Internal.Parsec ι α) :

Std.Internal.Parsec ι (Array α)

Equations

p.many = p.manyCore #[]

@[inline]

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

Std.Internal.Parsec ι (Array α)

Equations

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

def Std.Internal.Parsec.unexpectedEndOfInput :

Equations

Std.Internal.Parsec.unexpectedEndOfInput = "unexpected end of input"

@[inline]

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

Std.Internal.Parsec ι elem

Equations

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

@[inline]

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

Std.Internal.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

@[inline]

def Std.Internal.Parsec.notFollowedBy {α : Type} {ι : Type} (p : Std.Internal.Parsec ι α) :

Std.Internal.Parsec ι Unit

Equations

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

@[inline]

def Std.Internal.Parsec.peek? {ι : Type} {elem : Type} {idx : Type} [DecidableEq idx] [DecidableEq elem] [Std.Internal.Parsec.Input ι elem idx] :

Std.Internal.Parsec ι (Option elem)

Equations

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

@[inline]

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

Std.Internal.Parsec ι elem

Equations

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

@[inline]

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

Std.Internal.Parsec ι elem

Equations

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

@[inline]

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

Std.Internal.Parsec ι Unit

Equations

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

@[specialize #[]]

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

Std.Internal.Parsec ι String

@[inline]

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

Std.Internal.Parsec ι String

Equations

p.manyChars = p.manyCharsCore ""

@[inline]

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

Std.Internal.Parsec ι String

Equations

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