Parser utils for ReaderT and StateT

@[reducible, inline]

abbrev Parser.SimpleCharParser (α : Type) : Type

Equations

• Parser.SimpleCharParser = SimpleParser String.Slice Char

@[implicit_reducible]

instance Parser.Parser.coeSimpleParser {α ρ σ : Type} : Coe (SimpleCharParser α) (ReaderT ρ (StateT σ SimpleCharParser) α)

Equations

• Parser.Parser.coeSimpleParser = { coe := fun (p : Parser.SimpleCharParser α) (x : ρ) (σ_1 : σ) => do let __do_lift ← p pure (__do_lift, σ_1) }

def Parser.attemptM {ρ σ α : Type} (p : ReaderT ρ (StateT σ SimpleCharParser) α) : ReaderT ρ (StateT σ SimpleCharParser) α

extends Lean.Parser.attempt

Equations

• Parser.attemptM p f = do let __do_lift ← get let __discr ← liftM (Parser.withBacktracking (p f __do_lift)) match __discr with | (a, s) => do set s pure a

def Parser.fail {α : Type} (msg : String) : SimpleCharParser α

Equations

• Parser.fail msg = Parser.throwUnexpectedWithMessage none msg

class Parser.Parser.Stream.Remaining (σ : Type) : Type

Returns a natural number measure of remaining input. see https://github.com/fgdorais/lean4-parser/pull/99

• remaining : σ → Nat

@[implicit_reducible]

instance Parser.instRemainingSlice : Parser.Stream.Remaining String.Slice

Equations

• Parser.instRemainingSlice = { remaining := fun (s : String.Slice) => s.utf8ByteSize }

@[irreducible]

def Parser.loop {ρ σ α : Type} (p : ReaderT ρ (StateT σ SimpleCharParser) α → ReaderT ρ (StateT σ SimpleCharParser) α) : ReaderT ρ (StateT σ SimpleCharParser) α

The recursive function loop calls p with a parser that acts like p except it fails if called from the same or lower string position

see https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/Advent.20of.20Code.3F/near/405471085

Equations

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

def Parser.manyM {ρ σ α : Type} (p : ReaderT ρ (StateT σ SimpleCharParser) α) : ReaderT ρ (StateT σ SimpleCharParser) (Array α)

Equations

• Parser.manyM p = do let __do_lift ← read liftM (Parser.foldM✝ (p __do_lift) #[])

def Parser.ws {ρ σ : Type} : ReaderT ρ (StateT σ SimpleCharParser) PUnit

Equations

• Parser.ws x✝ t = do let __discr ← Parser.fold✝ Parser.Char.ASCII.whitespace #[] have x : Array Char := __discr pure ((), t)

def Parser.peekChar? : SimpleCharParser (Option Char)

Equations

• Parser.peekChar? = Parser.option? Parser.peek

def Parser.peekChar : SimpleCharParser Char

Equations

• Parser.peekChar = Parser.peek

def Parser.withPos {α : Type} (p : SimpleCharParser α) : SimpleCharParser (String.Pos.Raw × String.Pos.Raw × α)

Equations

• Parser.withPos p = do let __discr ← Parser.withCapture p match __discr with | (a, s) => pure (s.start, s.stop, a)

def Parser.withPosM {ρ σ α : Type} (p : ReaderT ρ (StateT σ SimpleCharParser) α) : ReaderT ρ (StateT σ SimpleCharParser) (String.Pos.Raw × String.Pos.Raw × α)

Equations

• Parser.withPosM p f s = do let __discr ← Parser.withCapture (p f s) match __discr with | (a, s) => pure ((s.start, s.stop, a.fst), a.snd)

def Parser.skipChar (c : Char) : SimpleCharParser Unit

Equations

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

def Parser.skipAnyChar : SimpleCharParser Unit

Equations

• Parser.skipAnyChar = Parser.anyToken *> pure ()

def Parser.skipChar? (c : Char) : SimpleCharParser Unit

Equations

• Parser.skipChar? c = tryCatch (Parser.skipChar c) fun (x : Parser.Error.Simple String.Slice Char) => pure ()

def Parser.skipString (tks : String) : SimpleCharParser Unit

Equations

• Parser.skipString tks = Parser.Char.chars tks *> pure ()

def Parser.skipString? (tks : String) : SimpleCharParser Unit

Equations

• Parser.skipString? tks = tryCatch (Parser.withBacktracking (Parser.skipString tks)) fun (x : Parser.Error.Simple String.Slice Char) => pure ()

def Parser.testChar (check : Char → Bool) : SimpleCharParser Bool

exec check on current char

Equations

• Parser.testChar check = do let __do_lift ← Parser.peekChar? match __do_lift with | some c => if check c = true then pure true else pure false | none => pure false

def Parser.tryChar (check : Char → Bool) : SimpleCharParser (Option Char)

exec check on current char and consume char on success

Equations

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

def Parser.trySkipChar (check : Char → Bool) : SimpleCharParser Bool

exec check on current char and skip char on success

Equations

• Parser.trySkipChar check = do let __do_lift ← Parser.tryChar check match __do_lift with | some val => pure true | x => pure false

def Parser.tryCharThenPWithPos {α : Type} (check : Char → Bool) (p : SimpleCharParser α) : SimpleCharParser (Option (String.Pos.Raw × String.Pos.Raw × α))

exec check on current char and then exec p on success

Equations

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

def Parser.tryCharThenPWithPosM {ρ σ α : Type} (check : Char → Bool) (p : ReaderT ρ (StateT σ SimpleCharParser) α) : ReaderT ρ (StateT σ SimpleCharParser) (Option (String.Pos.Raw × String.Pos.Raw × α))

exec check on current char and then exec p on success

Equations

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

def Parser.tryCharWithPos (check : Char → Bool) : SimpleCharParser (Option (String.Pos.Raw × String.Pos.Raw × Char))

Equations

• Parser.tryCharWithPos check = Parser.tryCharThenPWithPos check Parser.anyToken

def Parser.tryCharWithPosMap {α : Type} (check : Char → Bool) (f : Char → String.Pos.Raw → String.Pos.Raw → α) : SimpleCharParser (Option α)

Equations

• Parser.tryCharWithPosMap check f = do let __do_lift ← Parser.tryCharWithPos check match __do_lift with | some (p1, p2, c) => pure (some (f c p1 p2)) | x => pure none

def Parser.manyChars (p : SimpleCharParser Char) : SimpleCharParser String

Equations

• Parser.manyChars p = do let chars ← Parser.fold✝ p #[] pure (String.ofList chars.toList)

def Parser.many1Chars (p : SimpleCharParser Char) : SimpleCharParser String

Equations

• Parser.many1Chars p = do let __do_lift ← p let chars ← Parser.fold✝ p #[__do_lift] pure (String.ofList chars.toList)