Parser utils for ReaderT and StateT

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

Equations

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

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

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) : SimpleParser Substring Char α

Equations

• Parser.fail msg = Parser.throwUnexpectedWithMessage none msg

instance Parser.instHOrElseSimpleParserSubstringCharReaderTStateT_regex {α ρ σ : Type} : HOrElse (SimpleParser Substring Char α) (ReaderT ρ (StateT σ (SimpleParser Substring Char)) α) (ReaderT ρ (StateT σ (SimpleParser Substring Char)) α)

Equations

• Parser.instHOrElseSimpleParserSubstringCharReaderTStateT_regex = { hOrElse := Parser.orElseT✝ }

def Parser.manyCore {α : Type} (p : SimpleParser Substring Char α) (acc : Array α) : SimpleParser Substring Char (Array α)

Equations

• Parser.manyCore p acc = do let r ← Parser.efoldl (fun (arr : Array α) (x : α) => arr.push x) acc (Parser.withBacktracking p) pure r.fst

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

extends Lean.Parser.many

Equations

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

def Parser.ws {ρ σ : Type} : ReaderT ρ (StateT σ (SimpleParser Substring Char)) PUnit

Equations

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

def Parser.peekChar? : SimpleParser Substring Char (Option Char)

Equations

• Parser.peekChar? = do let __do_lift ← Parser.eoption Parser.peek match __do_lift with | Sum.inl x => pure (some x) | Sum.inr val => pure none

def Parser.peekChar : SimpleParser Substring Char Char

Equations

• Parser.peekChar = Parser.peek

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

Equations

• Parser.withPos p = do let cap ← Parser.Char.captureStr p pure (cap.snd.startPos, cap.snd.stopPos, cap.fst)

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

Equations

• Parser.withPosM p f s = do let cap ← Parser.Char.captureStr (p f s) pure ((cap.snd.startPos, cap.snd.stopPos, cap.fst.fst), cap.fst.snd)

def Parser.withPosSkip : SimpleParser Substring Char String.Pos.Raw

Equations

• Parser.withPosSkip = do let __discr ← Parser.withPos Parser.anyToken match __discr with | (fst, t, snd) => pure t

def Parser.skipChar (c : Char) : SimpleParser Substring Char Unit

Equations

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

def Parser.skipAnyChar : SimpleParser Substring Char Unit

Equations

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

def Parser.skipChar? (c : Char) : SimpleParser Substring Char Unit

Equations

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

def Parser.skipString (tks : String) : SimpleParser Substring Char Unit

Equations

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

def Parser.skipString? (tks : String) : SimpleParser Substring Char Unit

Equations

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

def Parser.testChar (check : Char → Bool) : SimpleParser Substring Char 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) : SimpleParser Substring Char (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) : SimpleParser Substring Char 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 : SimpleParser Substring Char α) : SimpleParser Substring Char (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 σ (SimpleParser Substring Char)) α) : ReaderT ρ (StateT σ (SimpleParser Substring Char)) (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) : SimpleParser Substring Char (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 → α) : SimpleParser Substring Char (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 : SimpleParser Substring Char Char) : SimpleParser Substring Char String

Equations

• Parser.manyChars p = do let chars ← Parser.manyCore p #[] pure chars.toList.asString

def Parser.many1Chars (p : SimpleParser Substring Char Char) : SimpleParser Substring Char String

Equations

• Parser.many1Chars p = do let __do_lift ← p let chars ← Parser.manyCore p #[__do_lift] pure chars.toList.asString