Parser utils for ReaderT and StateT

def Parser.remaining (it : Std.Iter Char) : Nat

Equations

• Parser.remaining it = it.internalState.slice.utf8ByteSize - it.internalState.pos.offset.byteIdx

@[reducible, inline]

abbrev Parser.SimpleCharParser (α : Type) : Type

Equations

• Parser.SimpleCharParser = ParseIt.Parser (ParseIt.Error.Simple ParseIt.CharIterator) ParseIt.CharIterator Char

@[instance_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.fail {α : Type} (msg : String) : SimpleCharParser α

Equations

• Parser.fail msg = ParseIt.throwUnexpectedWithMessage none msg

def Parser.mkSimpleError {α : Type} (it : Std.Iter Char) (msg : String) : ParseIt.Result (ParseIt.Error.Simple ParseIt.CharIterator) it α

Equations

• Parser.mkSimpleError it msg = ParseIt.Result.error ((ParseIt.Error.Simple.unexpected (ParseIt.HasPos.pos it) none).addMessage (ParseIt.HasPos.pos it) msg)

@[irreducible]

def Parser.loop {ρ σ α : Type} (f : 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.StateT.efoldlP {ε ι τ : Type u} {m : Type u → Type v} [Std.Iterator ι Id τ] {β α σ : Type u} [Std.Iterators.Finite ι Id] [Monad m] (f : β → α → StateT σ (ParseIt.ParserT ε ι τ m) β) (init : β) (p : StateT σ (ParseIt.ParserT ε ι τ m) α) : StateT σ (ParseIt.ParserT ε ι τ m) (β × Option ε)

Equations

• Parser.StateT.efoldlP f init p s it = Parser.StateT.efoldlP.loop f p s it init it (ParseIt.Progress.refl it)

@[irreducible]

def Parser.StateT.efoldlP.loop {ε ι τ : Type u} {m : Type u → Type v} [Std.Iterator ι Id τ] {β α σ : Type u} [Monad m] (f : β → α → StateT σ (ParseIt.ParserT ε ι τ m) β) (p : StateT σ (ParseIt.ParserT ε ι τ m) α) [Std.Iterators.Finite ι Id] (s : σ) (it : Std.Iter τ) (y : β) (cur : Std.Iter τ) (hcur : ParseIt.Progress cur it) : m (ParseIt.Result ε it ((β × Option ε) × σ))

Fold from iterator cur, which it progressed to, with accumulator y.

Equations

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

def Parser.StateT.foldlP {ε ι τ : Type u} {m : Type u → Type v} [Std.Iterator ι Id τ] {β α σ : Type u} [Std.Iterators.Finite ι Id] [Monad m] (f : β → α → StateT σ (ParseIt.ParserT ε ι τ m) β) (init : β) (p : StateT σ (ParseIt.ParserT ε ι τ m) α) : StateT σ (ParseIt.ParserT ε ι τ m) β

Equations

• Parser.StateT.foldlP f init p = Prod.fst <$> Parser.StateT.efoldlP f init p

def Parser.StateT.foldl {ε ι τ : Type u} {m : Type u → Type v} [Std.Iterator ι Id τ] {β α σ : Type u} [Std.Iterators.Finite ι Id] [Monad m] (f : β → α → β) (init : β) (p : StateT σ (ParseIt.ParserT ε ι τ m) α) : StateT σ (ParseIt.ParserT ε ι τ m) β

Equations

• Parser.StateT.foldl f init p = Parser.StateT.foldlP (fun (y : β) (x : α) => pure (f y x)) init p

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

Equations

• Parser.manyM p r = Parser.StateT.foldl (fun (acc : Array α) (a : α) => acc.push a) #[] (p r)

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

Equations

• Parser.ws x✝ s = do let _ ← ParseIt.foldl (fun (acc : Array Char) (x : Char) => acc) #[] ParseIt.Char.ASCII.whitespace pure ((), s)

def Parser.peekChar? : SimpleCharParser (Option Char)

Equations

• Parser.peekChar? = ParseIt.option? (ParseIt.lookAhead ParseIt.anyToken)

def Parser.peekChar : SimpleCharParser Char

Equations

• Parser.peekChar = ParseIt.lookAhead ParseIt.anyToken

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

Equations

• Parser.withPos p = do let __x ← ParseIt.withSpan p match __x with | (a, s1, s2) => pure (s1, s2, 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 __x ← ParseIt.withSpan (p f s) match __x with | (a, s1, s2) => pure ((s1, s2, 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 = ParseIt.anyToken *> pure ()

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

Equations

• Parser.skipChar? c = tryCatch (Parser.skipChar c) fun (x : ParseIt.Error.Simple ParseIt.CharIterator) => pure ()

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

Equations

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

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

Equations

• Parser.skipString? tks = tryCatch (Parser.skipString tks) fun (x : ParseIt.Error.Simple ParseIt.CharIterator) => 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 ParseIt.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 ← ParseIt.foldl (fun (acc : Array Char) (a : Char) => acc.push a) #[] 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 ← ParseIt.foldl (fun (acc : Array Char) (a : Char) => acc.push a) #[__do_lift] p pure (String.ofList chars.toList)