Parser utils for ReaderT and StateT

def Parser.attemptM {ρ σ α : Type} (p : ReaderT ρ (StateT σ Std.Internal.Parsec.String.Parser) α) : ReaderT ρ (StateT σ Std.Internal.Parsec.String.Parser) α

extends Lean.Parser.attempt

Equations

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

instance Parser.instHOrElseParserReaderTStateT_regex {α ρ σ : Type} : HOrElse (Std.Internal.Parsec.String.Parser α) (ReaderT ρ (StateT σ Std.Internal.Parsec.String.Parser) α) (ReaderT ρ (StateT σ Std.Internal.Parsec.String.Parser) α)

Equations

• Parser.instHOrElseParserReaderTStateT_regex = { hOrElse := Parser.orElseT }

def Parser.tryCatchT {σ α β : Type} (p : StateT σ Std.Internal.Parsec.String.Parser α) (csuccess : α → StateT σ Std.Internal.Parsec.String.Parser β) (cerror : Unit → StateT σ Std.Internal.Parsec.String.Parser β) : StateT σ Std.Internal.Parsec.String.Parser β

extends Lean.Parser.tryCatch

Equations

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

def Parser.manyM {ρ σ α : Type} (p : ReaderT ρ (StateT σ Std.Internal.Parsec.String.Parser) α) : ReaderT ρ (StateT σ Std.Internal.Parsec.String.Parser) (Array α)

extends Lean.Parser.many

Equations

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

def Parser.failM {ρ σ α : Type} (msg : String) : ReaderT ρ (StateT σ Std.Internal.Parsec.String.Parser) α

Equations

• Parser.failM msg = liftM (Std.Internal.Parsec.fail msg)

def Parser.peekChar? : Std.Internal.Parsec.String.Parser (Option Char)

Equations

• Parser.peekChar? = Std.Internal.Parsec.peek?

def Parser.peekChar! : Std.Internal.Parsec.String.Parser Char

Equations

• Parser.peekChar! = Std.Internal.Parsec.peek!

def Parser.withPos {α : Type} (p : Std.Internal.Parsec.String.Parser α) : Std.Internal.Parsec.String.Parser (String.Pos × String.Pos × α)

Equations

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

def Parser.withPosM {ρ σ α : Type} (p : ReaderT ρ (StateT σ Std.Internal.Parsec.String.Parser) α) : ReaderT ρ (StateT σ Std.Internal.Parsec.String.Parser) (String.Pos × String.Pos × α)

Equations

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

def Parser.withPosSkip : Std.Internal.Parsec.String.Parser String.Pos

Equations

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

def Parser.optSkipChar (c : Char) : Std.Internal.Parsec.String.Parser Unit

Equations

• Parser.optSkipChar c = do let __do_lift ← Std.Internal.Parsec.peek? match __do_lift with | some c' => if c = c' then Std.Internal.Parsec.skip *> pure () else pure () | none => pure ()

def Parser.optSkipString (s : String) : Std.Internal.Parsec.String.Parser Unit

Equations

• Parser.optSkipString s = do let __do_lift ← Std.Internal.Parsec.peek? match __do_lift with | some val => Std.Internal.Parsec.String.skipString s | none => pure ()

def Parser.testChar (check : Char → Bool) : Std.Internal.Parsec.String.Parser Bool

exec check on current char

Equations

• Parser.testChar check = do let __do_lift ← Std.Internal.Parsec.peek? 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) : Std.Internal.Parsec.String.Parser (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) : Std.Internal.Parsec.String.Parser 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.tryCharThen {α : Type} (check : Char → Bool) (f : Char → α) (msg : String := "") : Std.Internal.Parsec.String.Parser α

exec check on current char and then exec f on consumed char on success

Equations

• Parser.tryCharThen check f msg = do let __do_lift ← Parser.tryChar check match __do_lift with | some c => pure (f c) | x => Std.Internal.Parsec.fail msg

def Parser.tryCharMap {α : Type} (check : Char → Bool) (f : Char → α) : Std.Internal.Parsec.String.Parser (Option α)

exec check on current char and map f on consumed char on success

Equations

• Parser.tryCharMap check f = do let __do_lift ← Parser.tryChar check match __do_lift with | some c => pure (some (f c)) | x => pure none

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

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 σ Std.Internal.Parsec.String.Parser) α) : ReaderT ρ (StateT σ Std.Internal.Parsec.String.Parser) (Option (String.Pos × String.Pos × α))

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) : Std.Internal.Parsec.String.Parser (Option (String.Pos × String.Pos × Char))

Equations

• Parser.tryCharWithPos check = Parser.tryCharThenPWithPos check Std.Internal.Parsec.any

def Parser.tryCharWithPosMap {α : Type} (check : Char → Bool) (f : Char → String.Pos → String.Pos → α) : Std.Internal.Parsec.String.Parser (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