inductive Parser.Result (ε σ α : Type u) : Type u

Parser result type.

• ok {ε σ α : Type u} : σ → α → Parser.Result ε σ α

  Result: success!

• error {ε σ α : Type u} : σ → ε → Parser.Result ε σ α

  Result: error!

instance Parser.instInhabitedResult {a✝ a✝¹ : Type u_1} [Inhabited a✝¹] {a✝² : Type u_1} [Inhabited a✝²] : Inhabited (Parser.Result a✝ a✝¹ a✝²)

Equations

• Parser.instInhabitedResult = { default := Parser.Result.ok default default }

instance Parser.instReprResult {ε✝ σ✝ α✝ : Type u_1} [Repr ε✝] [Repr σ✝] [Repr α✝] : Repr (Parser.Result ε✝ σ✝ α✝)

Equations

• Parser.instReprResult = { reprPrec := Parser.reprResult✝ }

def ParserT (ε σ : Type u_1) (τ : Type u_2) [Parser.Stream σ τ] [Parser.Error ε σ τ] (m : Type u_1 → Type u_4) (α : Type u_1) : Type (max u_4 u_1)

ParserT ε σ τ is a monad transformer to parse tokens of type τ from the stream type σ with error type ε.

Equations

• ParserT ε σ τ m α = (σ → m (Parser.Result ε σ α))

@[inline]

def ParserT.run {σ : Type u_1} {τ : Type u_2} {ε : Type u_1} {m : Type u_1 → Type u_3} {α : Type u_1} [Parser.Stream σ τ] [Parser.Error ε σ τ] (p : ParserT ε σ τ m α) (s : σ) : m (Parser.Result ε σ α)

Run the monadic parser p on input stream s.

Equations

• p.run s = p s

instance instMonadParserT (σ ε : Type u_1) (τ : Type u_2) (m : Type u_1 → Type u_3) [Parser.Stream σ τ] [Parser.Error ε σ τ] [Monad m] : Monad (ParserT ε σ τ m)

Equations

• instMonadParserT σ ε τ m = Monad.mk

instance instMonadExceptOfParserTOfMonad (σ ε : Type u_1) (τ : Type u_2) (m : Type u_1 → Type u_3) [Parser.Stream σ τ] [Parser.Error ε σ τ] [Monad m] : MonadExceptOf ε (ParserT ε σ τ m)

Equations

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

instance instOrElseParserTOfMonad {α : Type u_1} (σ ε : Type u_1) (τ : Type u_2) (m : Type u_1 → Type u_3) [Parser.Stream σ τ] [Parser.Error ε σ τ] [Monad m] : OrElse (ParserT ε σ τ m α)

Equations

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

instance instMonadLiftParserTOfMonad (σ ε : Type u_1) (τ : Type u_2) (m : Type u_1 → Type u_3) [Parser.Stream σ τ] [Parser.Error ε σ τ] [Monad m] : MonadLift m (ParserT ε σ τ m)

Equations

• instMonadLiftParserTOfMonad σ ε τ m = { monadLift := fun {α : Type ?u.62} (x : m α) (s : σ) => (fun (x : α) => Parser.Result.ok s x) <$> x }

@[reducible, inline]

abbrev Parser (ε σ : Type u_1) (τ : Type u_2) [Parser.Stream σ τ] [Parser.Error ε σ τ] (α : Type u_1) : Type u_1

Parser ε σ τ monad to parse tokens of type τ from the stream type σ with error type ε.

Equations

• Parser ε σ τ = ParserT ε σ τ Id

@[inline]

def Parser.run {ε σ : Type u_1} {τ : Type u_2} {α : Type u_1} [Parser.Stream σ τ] [Parser.Error ε σ τ] (p : Parser ε σ τ α) (s : σ) : Parser.Result ε σ α

Run parser p on input stream s.

Equations

• p.run s = p s

@[reducible, inline]

abbrev TrivialParserT (σ : Type) (τ : Type u_1) [Parser.Stream σ τ] (m : Type → Type u_3) (α : Type) : Type u_3

TrivialParserT σ τ monad transformer to parse tokens of type τ from the stream σ with trivial error handling.

Equations

• TrivialParserT σ τ m = ParserT Parser.Error.Trivial σ τ m

@[reducible, inline]

abbrev TrivialParser (σ : Type) (τ : Type u_1) [Parser.Stream σ τ] (α : Type) : Type

TrivialParser σ τ monad to parse tokens of type τ from the stream σ with trivial error handling.

Equations

• TrivialParser σ τ = Parser Parser.Error.Trivial σ τ

@[reducible, inline]

abbrev BasicParserT (σ : Type (max u_1 u_2)) (τ : Type u_2) [Parser.Stream σ τ] (m : Type (max u_1 u_2) → Type u_3) (α : Type (max u_1 u_2)) : Type (max u_3 u_1 u_2)

BasicParserT σ τ monad transformer to parse tokens of type τ from the stream σ with basic error handling.

Equations

• BasicParserT σ τ m = ParserT (Parser.Error.Basic σ τ) σ τ m

@[reducible, inline]

abbrev BasicParser (σ : Type (max u_1 u_2)) (τ : Type u_2) [Parser.Stream σ τ] (α : Type (max u_1 u_2)) : Type (max u_1 u_2)

BasicParser σ τ monad to parse tokens of type τ from the stream σ with basic error handling.

Equations

• BasicParser σ τ = Parser (Parser.Error.Basic σ τ) σ τ

@[reducible, inline]

abbrev SimpleParserT (σ : Type (max u_1 u_2)) (τ : Type u_2) [Parser.Stream σ τ] (m : Type (max u_1 u_2) → Type u_3) (α : Type (max u_1 u_2)) : Type (max u_3 u_1 u_2)

SimpleParserT σ τ monad transformer to parse tokens of type τ from the stream σ with simple error handling.

Equations

• SimpleParserT σ τ m = ParserT (Parser.Error.Simple σ τ) σ τ m

@[reducible, inline]

abbrev SimpleParser (σ : Type (max u_1 u_2)) (τ : Type u_2) [Parser.Stream σ τ] (α : Type (max u_1 u_2)) : Type (max u_1 u_2)

SimpleParser σ τ monad to parse tokens of type τ from the stream σ with simple error handling.

Equations

• SimpleParser σ τ = Parser (Parser.Error.Simple σ τ) σ τ

Stream Functions

@[inline]

def Parser.getStream {τ : Type u_1} {m : Type u → Type u_2} {ε σ : Type u} [Parser.Stream σ τ] [Parser.Error ε σ τ] [Monad m] : ParserT ε σ τ m σ

Get parser stream.

Equations

• Parser.getStream s = pure (Parser.Result.ok s s)

@[inline]

def Parser.setStream {τ : Type u_1} {m : Type u → Type u_2} {ε σ : Type u} [Parser.Stream σ τ] [Parser.Error ε σ τ] [Monad m] (s : σ) : ParserT ε σ τ m PUnit

Set parser stream.

Equations

• Parser.setStream s x✝ = pure (Parser.Result.ok s PUnit.unit)

@[inline]

def Parser.getPosition {τ : Type u_1} {m : Type u → Type u_2} {ε σ : Type u} [Parser.Stream σ τ] [Parser.Error ε σ τ] [Monad m] : ParserT ε σ τ m (Stream.Position σ)

Get stream position from parser.

Equations

• Parser.getPosition = Parser.Stream.getPosition <$> Parser.getStream

@[inline]

def Parser.setPosition {τ : Type u_1} {m : Type u → Type u_2} {ε σ : Type u} [Parser.Stream σ τ] [Parser.Error ε σ τ] [Monad m] (pos : Stream.Position σ) : ParserT ε σ τ m PUnit

Set stream position from parser.

Equations

• Parser.setPosition pos = do let __do_lift ← Parser.getStream Parser.setStream (Parser.Stream.setPosition __do_lift pos)

@[inline]

def Parser.withBacktracking {τ : Type u_1} {m : Type u → Type u_2} {ε σ α : Type u} [Parser.Stream σ τ] [Parser.Error ε σ τ] [Monad m] (p : ParserT ε σ τ m α) : ParserT ε σ τ m α

withBacktracking p parses p but does not consume any input on error.

Equations

• Parser.withBacktracking p = do let savePos ← Parser.getPosition tryCatch p fun (e : ε) => do Parser.setPosition savePos throw e

def Parser.withCapture {τ : Type u_1} {m : Type (max u_2 u_3) → Type u_4} [Monad m] {ε σ α : Type (max u_2 u_3)} [Parser.Stream σ τ] [Parser.Error ε σ τ] (p : ParserT ε σ τ m α) : ParserT ε σ τ m (α × Stream.Segment σ)

withCapture p parses p and returns the output of p with the corresponding stream segment.

Equations

• Parser.withCapture p = do let startPos ← Parser.getPosition let x ← p let stopPos ← Parser.getPosition pure (x, startPos, stopPos)

Error Functions

@[inline]

def Parser.throwUnexpected {τ : Type u_1} {m : Type u → Type u_2} {ε σ α : Type u} [Parser.Stream σ τ] [Parser.Error ε σ τ] [Monad m] (input : Option τ := none) : ParserT ε σ τ m α

Throw error on unexpected token.

Equations

• Parser.throwUnexpected input = do let __do_lift ← Parser.getPosition throw (Parser.Error.unexpected __do_lift input)

@[inline]

def Parser.throwErrorWithMessage {τ : Type u_1} {m : Type u → Type u_2} {ε σ α : Type u} [Parser.Stream σ τ] [Parser.Error ε σ τ] [Monad m] (e : ε) (msg : String) : ParserT ε σ τ m α

Throw error with additional message.

Equations

• Parser.throwErrorWithMessage e msg = do let __do_lift ← Parser.getPosition throw (Parser.Error.addMessage e __do_lift msg)

@[inline]

def Parser.throwUnexpectedWithMessage {τ : Type u_1} {m : Type u → Type u_2} {ε σ α : Type u} [Parser.Stream σ τ] [Parser.Error ε σ τ] [Monad m] (input : Option τ := none) (msg : String) : ParserT ε σ τ m α

Throw error on unexpected token with error message.

Equations

• Parser.throwUnexpectedWithMessage input msg = do let __do_lift ← Parser.getPosition Parser.throwErrorWithMessage (Parser.Error.unexpected __do_lift input) msg

@[inline]

def Parser.withErrorMessage {τ : Type u_1} {m : Type u → Type u_2} {ε σ α : Type u} [Parser.Stream σ τ] [Parser.Error ε σ τ] [Monad m] (msg : String) (p : ParserT ε σ τ m α) : ParserT ε σ τ m α

Add message on parser error.

Equations

• Parser.withErrorMessage msg p = tryCatch p fun (e : ε) => Parser.throwErrorWithMessage e msg

Low-Level Combinators

foldl family

@[inline]

def Parser.efoldlP {τ : Type u_1} {m : Type u → Type u_2} {ε σ α β : Type u} [Parser.Stream σ τ] [Parser.Error ε σ τ] [Monad m] (f : β → α → ParserT ε σ τ m β) (init : β) (p : ParserT ε σ τ m α) : ParserT ε σ τ m (β × ε × Bool)

foldlP f init p folds the parser function f from left to right using init as an intitial value and the parser p to generate inputs of type α. The folding ends as soon as the update parser function (p >>= f ⬝) fails. Then the final folding result is returned along with the pair:

• (e, true) if the final p succeeds but then f fails reporting error e.
• (e, false) if the final p fails reporting error e.

In either case, the final p is not consumed. This parser never fails.

Equations

• Parser.efoldlP f init p s = Parser.efoldlPAux✝ f p init s

@[inline]

def Parser.efoldlM {τ : Type u_1} {m : Type u → Type u_2} {ε σ α β : Type u} [Parser.Stream σ τ] [Parser.Error ε σ τ] [Monad m] (f : β → α → m β) (init : β) (p : ParserT ε σ τ m α) : ParserT ε σ τ m (β × ε)

foldlM f init p folds the monadic function f from left to right using init as an intitial value and the parser p to generate inputs of type α. The folding ends as soon as p fails and the error reported by p is returned along with the result of folding. This parser never fails.

Equations

• Parser.efoldlM f init p = do let x ← Parser.efoldlP (fun (y : β) (x : α) => monadLift (f y x)) init p match x with | (y, e, snd) => pure (y, e)

@[inline]

def Parser.efoldl {τ : Type u_1} {m : Type u → Type u_2} {ε σ α β : Type u} [Parser.Stream σ τ] [Parser.Error ε σ τ] [Monad m] (f : β → α → β) (init : β) (p : ParserT ε σ τ m α) : ParserT ε σ τ m (β × ε)

foldl f init p folds the function f from left to right using init as an intitial value and the parser p to generate inputs of type α. The folding ends as soon as p fails and the error reported by p is returned along with the result of folding. This parser never fails.

Equations

• Parser.efoldl f init p = Parser.efoldlM (fun (y : β) (x : α) => pure (f y x)) init p

@[inline]

def Parser.foldlP {τ : Type u_1} {m : Type u → Type u_2} {ε σ α β : Type u} [Parser.Stream σ τ] [Parser.Error ε σ τ] [Monad m] (f : β → α → ParserT ε σ τ m β) (init : β) (p : ParserT ε σ τ m α) : ParserT ε σ τ m β

foldlP f init p folds the parser function f from left to right using init as an intitial value and the parser p to generate inputs of type α. The folding ends as soon as the update function (p >>= f ·) fails. This parser never fails.

Equations

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

@[inline]

def Parser.foldlM {τ : Type u_1} {m : Type u → Type u_2} {ε σ α β : Type u} [Parser.Stream σ τ] [Parser.Error ε σ τ] [Monad m] (f : β → α → m β) (init : β) (p : ParserT ε σ τ m α) : ParserT ε σ τ m β

foldlM f init p folds the monadic function f from left to right using init as an intitial value and the parser p to generate inputs of type α. The folding ends as soon as p fails. This parser never fails.

Equations

• Parser.foldlM f init p = Prod.fst <$> Parser.efoldlM f init p

@[inline]

def Parser.foldl {τ : Type u_1} {m : Type u → Type u_2} {ε σ α β : Type u} [Parser.Stream σ τ] [Parser.Error ε σ τ] [Monad m] (f : β → α → β) (init : β) (p : ParserT ε σ τ m α) : ParserT ε σ τ m β

foldl f init p folds the function f from left to right using init as an intitial value and the parser p to generate inputs of type α. The folding ends as soon as p fails. This parser never fails.

Equations

• Parser.foldl f init p = Prod.fst <$> Parser.efoldl f init p

option family

@[specialize #[]]

def Parser.eoption {τ : Type u_1} {m : Type u → Type u_2} {ε σ α : Type u} [Parser.Stream σ τ] [Parser.Error ε σ τ] [Monad m] (p : ParserT ε σ τ m α) : ParserT ε σ τ m (α ⊕ ε)

eoption p tries to parse p (with backtracking) and returns:

• Sum.inl x if p returns x,
• Sum.inr e if pfails with error e.

This parser never fails.

Equations

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

@[inline]

def Parser.optionM {τ : Type u_1} {m : Type u → Type u_2} {ε σ α : Type u} [Parser.Stream σ τ] [Parser.Error ε σ τ] [Monad m] (p : ParserT ε σ τ m α) (default : m α) : ParserT ε σ τ m α

optionM p tries to parse p (with backtracking) and returns x if p returns x, returns the monadic value default if p fails. This parser never fails.

Equations

• Parser.optionM p default = do let __do_lift ← Parser.eoption p match __do_lift with | Sum.inl x => pure x | Sum.inr val => liftM default

@[inline]

def Parser.optionD {τ : Type u_1} {m : Type u → Type u_2} {ε σ α : Type u} [Parser.Stream σ τ] [Parser.Error ε σ τ] [Monad m] (p : ParserT ε σ τ m α) (default : α) : ParserT ε σ τ m α

optionD p tries to parse p (with backtracking) and returns x if p returns x, returns default if p fails. This parser never fails.

Equations

• Parser.optionD p default = Parser.optionM p (pure default)

@[inline]

def Parser.option! {τ : Type u_1} {m : Type u → Type u_2} {ε σ α : Type u} [Parser.Stream σ τ] [Parser.Error ε σ τ] [Monad m] [Inhabited α] (p : ParserT ε σ τ m α) : ParserT ε σ τ m α

option! p tries to parse p (with backtracking) and returns x if p returns x, returns Inhabited.default if p fails. This parser never fails.

Equations

• Parser.option! p = Parser.optionD p default

@[inline]

def Parser.option? {τ : Type u_1} {m : Type u → Type u_2} {ε σ α : Type u} [Parser.Stream σ τ] [Parser.Error ε σ τ] [Monad m] (p : ParserT ε σ τ m α) : ParserT ε σ τ m (Option α)

option? p tries to parse p and returns some x if p returns x, returns none if p fails. This parser never fails.

Equations

• Parser.option? p = Parser.option! (some <$> p)

@[inline]

def Parser.optional {τ : Type u_1} {m : Type u → Type u_2} {ε σ α : Type u} [Parser.Stream σ τ] [Parser.Error ε σ τ] [Monad m] (p : ParserT ε σ τ m α) : ParserT ε σ τ m PUnit

optional p tries to parse p (with backtracking) ignoring output or errors. This parser never fails.

Equations

• Parser.optional p = Parser.eoption p *> pure PUnit.unit

first family

def Parser.efirst {τ : Type u_1} {m : Type u → Type u_2} {ε σ α : Type u} [Parser.Stream σ τ] [Parser.Error ε σ τ] [Monad m] (ps : List (ParserT ε σ τ m α)) : ParserT ε σ τ m (Option α × List ε)

efirst ps tries parsers from the list ps in order (with backtracking) until one succeeds:

• Once a parser p succeeds with value x then some x is returne along with the list of errors from all previous parsers.
• If none succeed then none is returned along with the list of errors of all parsers.

This parser never fails.

Equations

• Parser.efirst ps = Parser.efirst.go ps []

def Parser.efirst.go {τ : Type u_1} {m : Type u → Type u_2} {ε σ α : Type u} [Parser.Stream σ τ] [Parser.Error ε σ τ] [Monad m] : List (ParserT ε σ τ m α) → List ε → ParserT ε σ τ m (Option α × List ε)

Equations

• Parser.efirst.go [] x✝ = pure (none, x✝.reverse)
• Parser.efirst.go (p :: ps) x✝ = do let __do_lift ← Parser.eoption p match __do_lift with | Sum.inl x => pure (some x, x✝.reverse) | Sum.inr e => Parser.efirst.go ps (e :: x✝)

def Parser.first {τ : Type u_1} {m : Type u → Type u_2} {ε σ α : Type u} [Parser.Stream σ τ] [Parser.Error ε σ τ] [Monad m] (ps : List (ParserT ε σ τ m α)) (combine : ε → ε → ε := fun (x : ε) => id) : ParserT ε σ τ m α

first ps tries parsers from the list ps in order (with backtracking) until one succeeds and returns the result of that parser.

The optional parameter combine can be used to control the error reported when all parsers fail. The default is to only report the error from the last parser.

Equations

• Parser.first ps combine = do let __do_lift ← Parser.getPosition Parser.first.go combine ps (Parser.Error.unexpected __do_lift none)

def Parser.first.go {τ : Type u_1} {m : Type u → Type u_2} {ε σ α : Type u} [Parser.Stream σ τ] [Parser.Error ε σ τ] [Monad m] (combine : ε → ε → ε := fun (x : ε) => id) : List (ParserT ε σ τ m α) → ε → σ → m (Parser.Result ε σ α)

Equations

• One or more equations did not get rendered due to their size.
• Parser.first.go combine [] x✝¹ x✝ = pure (Parser.Result.error x✝ x✝¹)