ParseIt core

Parsers read tokens from a pure iterator Std.Iter (α := ι) τ. The parser state is the iterator itself, so backtracking is simply reusing an earlier iterator value.

Every successful parse reports its Progress: either the iterator did not move, or it moved strictly forward along plausible successor steps. Proofs are erased at runtime, so Progress compiles to a one-bit tag, and that tag is what allows repetition combinators to be total.

def ParseIt.Advanced {ι τ : Type u} [Std.Iterator ι Id τ] (it' it : Std.Iter τ) : Prop

it' is reachable from it by one or more plausible successor steps.

Equations

• ParseIt.Advanced it' it = it'.finitelyManySteps!.Rel it.finitelyManySteps!

theorem ParseIt.Advanced.trans {ι τ : Type u} [Std.Iterator ι Id τ] {it'' it' it : Std.Iter τ} : Advanced it'' it' → Advanced it' it → Advanced it'' it

theorem ParseIt.Advanced.of_yield {ι τ : Type u} [Std.Iterator ι Id τ] {it' it : Std.Iter τ} {out : τ} (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) : Advanced it' it

theorem ParseIt.Advanced.of_skip {ι τ : Type u} [Std.Iterator ι Id τ] {it' it : Std.Iter τ} (h : it.IsPlausibleStep (Std.IterStep.skip it')) : Advanced it' it

inductive ParseIt.Progress {ι τ : Type u} [Std.Iterator ι Id τ] (it' it : Std.Iter τ) : Type u

How far a parser moved the iterator from it to it'.

• stay {ι τ : Type u} [Std.Iterator ι Id τ] {it' it : Std.Iter τ} : it' = it → Progress it' it

  The iterator did not move.

• moved {ι τ : Type u} [Std.Iterator ι Id τ] {it' it : Std.Iter τ} : Advanced it' it → Progress it' it

  The iterator moved strictly forward.

@[inline]

def ParseIt.Progress.isMoved {ι τ : Type u} [Std.Iterator ι Id τ] {it' it : Std.Iter τ} : Progress it' it → Bool

Whether the iterator moved.

Equations

• (ParseIt.Progress.stay a).isMoved = false
• (ParseIt.Progress.moved a).isMoved = true

@[inline]

def ParseIt.Progress.refl {ι τ : Type u} [Std.Iterator ι Id τ] (it : Std.Iter τ) : Progress it it

No progress.

Equations

• ParseIt.Progress.refl it = ParseIt.Progress.stay ⋯

@[inline]

def ParseIt.Progress.trans {ι τ : Type u} [Std.Iterator ι Id τ] {it'' it' it : Std.Iter τ} : Progress it'' it' → Progress it' it → Progress it'' it

Compose progress.

Equations

• (ParseIt.Progress.stay h₁).trans (ParseIt.Progress.stay h₂) = ParseIt.Progress.stay ⋯
• (ParseIt.Progress.stay h₁).trans (ParseIt.Progress.moved h₂) = ParseIt.Progress.moved ⋯
• (ParseIt.Progress.moved h₁).trans (ParseIt.Progress.stay h₂) = ParseIt.Progress.moved ⋯
• (ParseIt.Progress.moved h₁).trans (ParseIt.Progress.moved h₂) = ParseIt.Progress.moved ⋯

inductive ParseIt.Result {ι τ : Type u} [Std.Iterator ι Id τ] (ε : Type u) (it : Std.Iter τ) (α : Type u) : Type u

Parser result for a parse starting at iterator it.

• ok {ι τ : Type u} [Std.Iterator ι Id τ] {ε : Type u} {it : Std.Iter τ} {α : Type u} (rest : Std.Iter τ) (progress : Progress rest it) (value : α) : Result ε it α

  Success, with the remaining iterator and the progress made.

• error {ι τ : Type u} [Std.Iterator ι Id τ] {ε : Type u} {it : Std.Iter τ} {α : Type u} (err : ε) : Result ε it α

  Failure. No input is consumed on failure.

def ParseIt.ParserT (ε ι τ : Type u) [Std.Iterator ι Id τ] (m : Type u → Type v) (α : Type u) : Type (max u v)

ParserT ε ι τ m is a monad transformer to parse tokens of type τ from an iterator with internal state ι, with error type ε.

Equations

• ParseIt.ParserT ε ι τ m α = ((it : Std.Iter τ) → m (ParseIt.Result ε it α))

@[reducible, inline]

abbrev ParseIt.Parser (ε ι τ : Type u) [Std.Iterator ι Id τ] (α : Type u) : Type u

Parser ε ι τ is the parser monad without an underlying monad.

Equations

• ParseIt.Parser ε ι τ = ParseIt.ParserT ε ι τ Id

@[inline]

def ParseIt.ParserT.run {ε ι τ α : Type u} {m : Type u → Type v} [Std.Iterator ι Id τ] (p : ParserT ε ι τ m α) (it : Std.Iter τ) : m (Result ε it α)

Run parser p on iterator it.

Equations

• p.run it = p it

@[instance_reducible]

instance ParseIt.ParserT.instMonad {ε ι τ : Type u} {m : Type u → Type v} [Std.Iterator ι Id τ] [Monad m] : Monad (ParserT ε ι τ m)

Equations

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

@[instance_reducible]

instance ParseIt.ParserT.instMonadExceptOfOfMonad {ε ι τ : Type u} {m : Type u → Type v} [Std.Iterator ι Id τ] [Monad m] : MonadExceptOf ε (ParserT ε ι τ m)

Equations

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

@[instance_reducible]

instance ParseIt.ParserT.instMonadLiftOfMonad {ε ι τ : Type u} {m : Type u → Type v} [Std.Iterator ι Id τ] [Monad m] : MonadLift m (ParserT ε ι τ m)

Equations

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

@[instance_reducible]

instance ParseIt.ParserT.instOrElseOfMonadOfError {ε ι τ α : Type u} {m : Type u → Type v} [Std.Iterator ι Id τ] [Monad m] [Error ε ι τ] : OrElse (ParserT ε ι τ m α)

p <|> q runs q from the same starting point when p fails, merging both errors.

Equations

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

@[inline]

def ParseIt.Parser.run {ε ι τ α : Type u} [Std.Iterator ι Id τ] (p : Parser ε ι τ α) (it : Std.Iter τ) : Result ε it α

Run parser p on iterator it.

Equations

• p.run it = p it

@[inline]

def ParseIt.Parser.parse {ε ι τ α : Type u} [Std.Iterator ι Id τ] (p : Parser ε ι τ α) (it : Std.Iter τ) : Except ε α

Run parser p on iterator it, returning the parsed value or the error.

Equations

• p.parse it = match p.run it with | ParseIt.Result.ok rest progress x => Except.ok x | ParseIt.Result.error e => Except.error e

Positions and errors

@[inline]

def ParseIt.getPos {ε ι τ : Type u} {m : Type u → Type v} [Std.Iterator ι Id τ] [Pure m] [HasPos ι τ] : ParserT ε ι τ m (HasPos.Pos ι)

getPos returns the current input position. Consumes no input and never fails.

Equations

• ParseIt.getPos it = pure (ParseIt.Result.ok it (ParseIt.Progress.refl it) (ParseIt.HasPos.pos it))

@[inline]

def ParseIt.withSpan {ε ι τ α : Type u} {m : Type u → Type v} [Std.Iterator ι Id τ] [Monad m] [HasPos ι τ] (p : ParserT ε ι τ m α) : ParserT ε ι τ m (α × HasPos.Pos ι × HasPos.Pos ι)

withSpan p parses p and returns its result together with the input positions where p started and stopped.

Equations

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

@[inline]

def ParseIt.throwUnexpected {ε ι τ α : Type u} {m : Type u → Type v} [Std.Iterator ι Id τ] [Pure m] [Error ε ι τ] (input : Option τ := none) : ParserT ε ι τ m α

Throw an unexpected input error at the current position.

Equations

• ParseIt.throwUnexpected input it = pure (ParseIt.Result.error (ParseIt.Error.unexpected it input))

@[inline]

def ParseIt.throwUnexpectedWithMessage {ε ι τ α : Type u} {m : Type u → Type v} [Std.Iterator ι Id τ] [Pure m] [Error ε ι τ] (input : Option τ := none) (msg : String) : ParserT ε ι τ m α

Throw an unexpected input error with an additional message.

Equations

• ParseIt.throwUnexpectedWithMessage input msg it = pure (ParseIt.Result.error (ParseIt.Error.addMessage (ParseIt.Error.unexpected it input) it msg))

@[inline]

def ParseIt.withErrorMessage {ε ι τ α : Type u} {m : Type u → Type v} [Std.Iterator ι Id τ] [Monad m] [Error ε ι τ] (msg : String) (p : ParserT ε ι τ m α) : ParserT ε ι τ m α

Add a message to errors reported by p.

Equations

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

Basic combinators

@[inline]

def ParseIt.lookAhead {ε ι τ α : Type u} {m : Type u → Type v} [Std.Iterator ι Id τ] [Monad m] (p : ParserT ε ι τ m α) : ParserT ε ι τ m α

lookAhead p parses p without consuming any input. If p fails then lookAhead p fails with the same error.

Equations

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

@[inline]

def ParseIt.notFollowedBy {ε ι τ α : Type u} {m : Type u → Type v} [Std.Iterator ι Id τ] [Monad m] [Error ε ι τ] (p : ParserT ε ι τ m α) : ParserT ε ι τ m Unitᵤ

notFollowedBy p succeeds only if p fails. Consumes no input.

Equations

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

option family

@[inline]

def ParseIt.optionD {ε ι τ α : Type u} {m : Type u → Type v} [Std.Iterator ι Id τ] [Monad m] (p : ParserT ε ι τ m α) (default : m α) : ParserT ε ι τ m α

optionD p default tries to parse p and returns x if p returns x, otherwise returns the monadic value default. This parser never fails.

Equations

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

@[inline]

def ParseIt.option! {ε ι τ α : Type u} {m : Type u → Type v} [Std.Iterator ι Id τ] [Monad m] [Inhabited α] (p : ParserT ε ι τ m α) : ParserT ε ι τ m α

option! p tries to parse p and returns x if p returns x, otherwise returns Inhabited.default. This parser never fails.

Equations

• ParseIt.option! p = ParseIt.optionD p (pure default)

@[inline]

def ParseIt.option? {ε ι τ α : Type u} {m : Type u → Type v} [Std.Iterator ι Id τ] [Monad m] (p : ParserT ε ι τ m α) : ParserT ε ι τ m (Option α)

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

Equations

• ParseIt.option? p = ParseIt.optionD (some <$> p) (pure none)

@[inline]

def ParseIt.optional {ε ι τ α : Type u} {m : Type u → Type v} [Std.Iterator ι Id τ] [Monad m] (p : ParserT ε ι τ m α) : ParserT ε ι τ m Unitᵤ

optional p tries to parse p, ignoring its output and errors. This parser never fails.

Equations

• ParseIt.optional p = ParseIt.optionD (p *> pure PUnit.unit) (pure PUnit.unit)

@[inline]

def ParseIt.test {ε ι τ α : Type u} {m : Type u → Type v} [Std.Iterator ι Id τ] [Monad m] (p : ParserT ε ι τ m α) : ParserT ε ι τ m Boolᵤ

test p returns true if p succeeds and false otherwise. This parser never fails.

Equations

• ParseIt.test p = ParseIt.optionD (p *> pure ParseIt.Boolᵤ.true) (pure ParseIt.Boolᵤ.false)

first family

def ParseIt.first {ε ι τ α : Type u} {m : Type u → Type v} [Std.Iterator ι Id τ] [Monad m] [Error ε ι τ] (ps : List (ParserT ε ι τ m α)) (combine : ε → ε → ε := Error.merge ι) : ParserT ε ι τ m α

first ps tries the parsers from the list ps in order until one succeeds and returns its result.

When all parsers fail, their errors are folded with combine, from left to right. The default is Error.merge. When ps is empty, an unexpected input error at the current position is reported.

Equations

• One or more equations did not get rendered due to their size.
• ParseIt.first [] combine it = pure (ParseIt.Result.error (ParseIt.Error.unexpected it none))