PrimParser

A parser combinator library with precise grades tracking error and consumption behavior at the type level via Necessity.

@[reducible, inline]

abbrev Error : Type

Equations

• Error = String

class ParserError (ε : Type) : Type

• endOfInput : ε

  Unexpected end of input.

structure Grade : Type

A parser's static grade: whether it may/must produce errors and whether it may/must consume input.

• errors : Necessity
• consumes : Necessity

@[instance_reducible]

instance instReprGrade : Repr Grade

Equations

• instReprGrade = { reprPrec := instReprGrade.repr }

def instReprGrade.repr : Grade → ℕ → Std.Format

Equations

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

@[reducible, inline]

abbrev Grade.impossible : Grade

Equations

• impossible = { errors := never, consumes := always }

@[reducible, inline]

abbrev Grade.conditional : Grade

Equations

• conditional = { errors := possibly, consumes := always }

@[reducible, inline]

abbrev Grade.flexible : Grade

Equations

• flexible = { errors := never, consumes := possibly }

@[reducible, inline]

abbrev Grade.fallible : Grade

Equations

• fallible = { errors := possibly, consumes := possibly }

@[reducible, inline]

abbrev Grade.pure : Grade

Equations

• Grade.pure = { errors := never, consumes := never }

@[reducible, inline]

abbrev Grade.lookahead : Grade

Equations

• lookahead = { errors := possibly, consumes := never }

@[reducible, inline]

abbrev Grade.empty : Grade

Equations

• empty = { errors := always, consumes := never }

def Grade.max (a b : Grade) : Grade

Equations

• a.max b = { errors := max a.errors b.errors, consumes := max a.consumes b.consumes }

@[instance_reducible]

instance Grade.instMax : Max Grade

Equations

• Grade.instMax = { max := Grade.max }

@[instance_reducible]

instance Grade.instMonoid : Monoid Grade

Equations

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

@[instance_reducible]

instance Grade.instZero : Zero Grade

Equations

• Grade.instZero = { zero := empty }

@[simp]

theorem Grade.mul_mk (e1 e2 c1 c2 : Necessity) : { errors := e1, consumes := c1 } * { errors := e2, consumes := c2 } = { errors := Max.max e1 e2, consumes := Max.max c1 c2 }

@[simp]

theorem Grade.one_mk : 1 = { errors := never, consumes := never }

@[simp]

theorem Grade.mul_idem (g : Grade) : g * g = g

def Grade.choice (a b : Grade) : Grade

Equations

• a.choice b = { errors := min a.errors b.errors, consumes := a.errors.ite b.consumes a.consumes }

@[reducible, inline]

abbrev Parser.consumptionWitness (n m : ℕ) : Necessity → Prop

Relates input size n and remaining size m according to a consumption grade: always requires strict decrease, possibly allows ≤, never requires equality.

Equations

• Parser.consumptionWitness n m always = (n < m)
• Parser.consumptionWitness n m possibly = (n ≤ m)
• Parser.consumptionWitness n m never = (n = m)

@[simp]

theorem Parser.consumptionWitness.rfl {n : ℕ} {gc : Necessity} (h : gc ≤ possibly) : consumptionWitness n n gc

theorem Parser.consumptionWitness.le {n m : ℕ} {gc : Necessity} : consumptionWitness n m gc → n ≤ m

theorem Parser.consumptionWitness.inf_of_possibly_le {n m : ℕ} {gc x : Necessity} (h : possibly ≤ x) (w : consumptionWitness n m gc) : consumptionWitness n m (min x gc)

theorem Parser.consumptionWitness.trans {gc gc' : Necessity} {n1 n2 n3 : ℕ} (w1 : consumptionWitness n2 n1 gc) (w2 : consumptionWitness n3 n2 gc') : consumptionWitness n3 n1 (max gc gc')

structure Parser.Success (n : ℕ) (consumes : Necessity) (α : Type) : Type

A successful parse result.

• result : α
• restSize : ℕ
• witness : consumptionWitness self.restSize n consumes

structure Parser.Failure (n : ℕ) (ε : Type) : Type

A failed parse result

• error : ε
• restSize : ℕ
• witness : self.restSize ≤ n

def Parser.Failure.trans {n m : ℕ} {ε : Type} (f : Failure m ε) (h : m ≤ n) : Failure n ε

Equations

• f.trans h = { error := f.error, restSize := f.restSize, witness := ⋯ }

@[simp]

theorem Parser.Failure.trans_rfl {n : ℕ} {ε : Type} (f : Failure n ε) : f.trans ⋯ = f

inductive Parser.Outcome (ε : Type) (n : ℕ) (consumes : Necessity) (α : Type) : Type

The result type of running a parser.

• failure {ε : Type} {n : ℕ} {consumes : Necessity} {α : Type} (f : Failure n ε) : Outcome ε n consumes α
• success {ε : Type} {n : ℕ} {consumes : Necessity} {α : Type} (r : Success n consumes α) : Outcome ε n consumes α

@[reducible, inline]

abbrev Parser.Outcome.Sound {n : ℕ} {ε : Type} (errors : Necessity) {c : Necessity} {α : Type} (o : Outcome ε n c α) : Prop

Equations

• Parser.Outcome.Sound errors (Parser.failure f) = (possibly ≤ errors)
• Parser.Outcome.Sound errors (Parser.success r) = (errors ≤ possibly)

@[simp]

theorem Parser.Outcome.sound_possibly {n : ℕ} {gc : Necessity} {ε α : Type} {o : Outcome ε n gc α} : Sound possibly o

structure Parser (σ τ : Type) [Buffer σ] [Reader σ τ] (ε : Type) (g : Grade) (α : Type) : Type

A parser with error type ε, static grade g, and result type α. The grade tracks error and consumption behavior at the type level.

• run {n : ℕ} : Input σ n → Outcome ε n g.consumes α
• sound {n : ℕ} (inp : Input σ n) : Outcome.Sound g.errors (self.run inp)

@[reducible, inline]

abbrev Parser.TokenParser (τ ε : Type) (g : Grade) (α : Type) : Type

Equations

• Parser.TokenParser τ ε g α = Parser (Array τ) τ ε g α

theorem Parser.ext {σ τ : Type} [Buffer σ] [Reader σ τ] {α ε : Type} {g : Grade} {p q : Parser σ τ ε g α} (h : ∀ {m : ℕ} (t : Input σ m), p.run t = q.run t) : p = q

theorem Parser.ext_iff {σ τ : Type} [Buffer σ] [Reader σ τ] {α ε : Type} {g : Grade} {p q : Parser σ τ ε g α} : p = q ↔ ∀ {m : ℕ} (t : Input σ m), p.run t = q.run t

@[inline]

def Parser.Outcome.handle {α β ε : Type} {n : ℕ} {ge gc : Necessity} (o : Outcome ε n gc α) (sound : Sound ge o) (onSuccess : ge ≤ possibly → Success n gc α → β) (onError : possibly ≤ ge → Failure n ε → β) : β

Equations

• (Parser.failure f).handle sound_2 onSuccess onError = onError sound_2 f
• (Parser.success r).handle sound_2 onSuccess onError = onSuccess sound_2 r

theorem Parser.Outcome.handle_prop {α β ε : Type} {n : ℕ} {ge gc : Necessity} {P : β → Prop} {o : Outcome ε n gc α} (sound : Sound ge o) {onSuccess : ge ≤ possibly → Success n gc α → β} {onError : possibly ≤ ge → Failure n ε → β} (hSuccess : ∀ (h : ge ≤ possibly) (r : Success n gc α), P (onSuccess h r)) (hError : ∀ (h : possibly ≤ ge) (f : Failure n ε), P (onError h f)) : P (o.handle sound onSuccess onError)

theorem Parser.Outcome.handle_sound {α β ε ε' : Type} {n m : ℕ} {ge ge' gc gc' : Necessity} {o : Outcome ε n gc α} (sound : Sound ge o) {onSuccess : ge ≤ possibly → Success n gc α → Outcome ε' m gc' β} {onError : possibly ≤ ge → Failure n ε → Outcome ε' m gc' β} (soundSuccess : ∀ (h : ge ≤ possibly) (r : Success n gc α), Sound ge' (onSuccess h r)) (soundError : ∀ (h : possibly ≤ ge) (f : Failure n ε), Sound ge' (onError h f)) : Sound ge' (o.handle sound onSuccess onError)

theorem Parser.Outcome.handle_success {α β ε : Type} {n : ℕ} {ge gc : Necessity} {o : Outcome ε n gc α} {sound : Sound ge o} {onSuccess : ge ≤ possibly → Success n gc α → β} {onError : possibly ≤ ge → Failure n ε → β} {r : Success n gc α} (h : o = success r) (hge : ge ≤ possibly := by simp) : o.handle sound onSuccess onError = onSuccess hge r

Reduce handle when the outcome is known to succeed.

theorem Parser.Outcome.handle_failure {α β ε : Type} {n : ℕ} {ge gc : Necessity} {o : Outcome ε n gc α} {sound : Sound ge o} {onSuccess : ge ≤ possibly → Success n gc α → β} {onError : possibly ≤ ge → Failure n ε → β} {f : Failure n ε} (h : o = failure f) (hge : possibly ≤ ge := by simp) : o.handle sound onSuccess onError = onError hge f

Reduce handle when the outcome is known to fail.

@[instance_reducible]

instance Parser.instFunctorSuccess {n : ℕ} {gc : Necessity} : Functor (Success n gc)

Equations

• Parser.instFunctorSuccess = { map := fun {α β : Type} (f : α → β) (x : Parser.Success n gc α) => { result := f x.result, restSize := x.restSize, witness := ⋯ } }

@[instance_reducible]

instance Parser.instGradedFunctorNecessitySuccess {n : ℕ} : GradedFunctor (Success n)

Equations

• Parser.instGradedFunctorNecessitySuccess = { gmap := fun {i : Necessity} {α β : Type} => Functor.map }

@[instance_reducible]

instance Parser.instFunctorOutcome {ε : Type} {n : ℕ} {gc : Necessity} : Functor (Outcome ε n gc)

Equations

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

theorem Parser.Outcome.map_sound {α β ε : Type} {n : ℕ} {ge gc : Necessity} (f : α → β) (o : Outcome ε n gc α) (ho : Sound ge o) : Sound ge (f <$> o)

def Parser.Error.eof : Error

Equations

• Parser.Error.eof = "unexpected end of input"

def Parser.Error.fail : Error

Equations

• Parser.Error.fail = "fail"

@[instance_reducible]

instance Parser.instParserErrorError : ParserError Error

Equations

• Parser.instParserErrorError = { endOfInput := Parser.Error.eof }

theorem Parser.Success.le {α : Type} {n : ℕ} {gc : Necessity} (p : Success n gc α) : p.restSize ≤ n

def Parser.Success.weakenConsumes {α : Type} {n : ℕ} {gc : Necessity} (p : Success n gc α) : Success n possibly α

Equations

• p.weakenConsumes = { result := p.result, restSize := p.restSize, witness := ⋯ }

def Parser.Success.trans {α : Type} {n m : ℕ} {gc : Necessity} (s : Success m gc α) (h : m ≤ n) : Success n (max gc possibly) α

Equations

• s.trans h = { result := s.result, restSize := s.restSize, witness := ⋯ }

def Parser.Success.seq {α β : Type} {n : ℕ} {gc gc' : Necessity} (r1 : Success n gc α) (r2 : Success r1.restSize gc' β) : Success n (max gc gc') β

Equations

• r1.seq r2 = { result := r2.result, restSize := r2.restSize, witness := ⋯ }

@[inline]

def Parser.Success.bindParser {σ τ : Type} [Buffer σ] [Reader σ τ] {α β ε : Type} {n : ℕ} {xc fe fc : Necessity} (t : Input σ n) (x : Success n xc α) (f : α → Parser σ τ ε { errors := fe, consumes := fc } β) : Outcome ε n (max xc fc) β

Equations

• Parser.Success.bindParser t x f = match (f x.result).run (t.dropTo x.restSize ⋯) with | Parser.failure e => Parser.failure (e.trans ⋯) | Parser.success y => Parser.success (x.seq y)

@[instance_reducible]

instance Parser.instGradedFunctorGrade {σ τ : Type} [Buffer σ] [Reader σ τ] {ε : Type} : GradedFunctor (Parser σ τ ε)

Equations

• Parser.instGradedFunctorGrade = { gmap := fun {i : Grade} {α β : Type} (f : α → β) (p : Parser σ τ ε i α) => { run := fun {n : ℕ} (t : Input σ n) => f <$> p.run t, sound := ⋯ } }

def Parser.Outcome.throw {α ε : Type} {n : ℕ} {gc : Necessity} (e : ε) : Outcome ε n gc α

Equations

• Parser.Outcome.throw e = Parser.failure { error := e, restSize := n, witness := ⋯ }

theorem Parser.Outcome.throw_sound {α ε : Type} {n : ℕ} {ge gc : Necessity} {e : ε} (h : possibly ≤ ge) : Sound ge (throw e)

@[inline]

def Parser.handle {σ τ : Type} [Buffer σ] [Reader σ τ] {α β ε ε' : Type} {g g' : Grade} (p : Parser σ τ ε g α) (onSuccess : {n : ℕ} → Input σ n → g.errors ≤ possibly → Success n g.consumes α → Outcome ε' n g'.consumes β) (soundSuccess : ∀ {n : ℕ} {t : Input σ n} (h : g.errors ≤ possibly) (r : Success n g.consumes α), Outcome.Sound g'.errors (onSuccess t h r)) (onError : {n : ℕ} → Input σ n → possibly ≤ g.errors → Failure n ε → Outcome ε' n g'.consumes β) (soundError : ∀ {n : ℕ} {t : Input σ n} (h : possibly ≤ g.errors) (f : Failure n ε), Outcome.Sound g'.errors (onError t h f)) : Parser σ τ ε' g' β

Equations

• p.handle onSuccess soundSuccess onError soundError = { run := fun {n : ℕ} (t : Input σ n) => (p.run t).handle ⋯ (onSuccess t) (onError t), sound := ⋯ }

def Parser.bind {σ τ : Type} [Buffer σ] [Reader σ τ] {α β ε : Type} {g g' : Grade} (m : Parser σ τ ε g α) (f : α → Parser σ τ ε g' β) : Parser σ τ ε (g * g') β

Monadic bind for parsers. The resulting grade is the product (max) of the two grades.

Equations

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

instance Parser.instIsEmptyImpossibleOfNonempty {σ τ : Type} [Buffer σ] [Reader σ τ] {α ε : Type} [i : Nonempty σ] : IsEmpty (Parser σ τ ε impossible α)

@[reducible, inline]

abbrev Parser.pure {σ τ : Type} [Buffer σ] [Reader σ τ] {α ε : Type} (a : α) : Parser σ τ ε 1 α

Lift a value into a parser that consumes nothing and never fails.

Equations

• Parser.pure a = { run := fun {n : ℕ} (x : Input σ n) => Parser.success { result := a, restSize := n, witness := ⋯ }, sound := ⋯ }

@[instance_reducible]

instance Parser.instGradedApplicativeGrade {σ τ : Type} [Buffer σ] [Reader σ τ] {ε : Type} : GradedApplicative (Parser σ τ ε)

Equations

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

@[instance_reducible]

instance Parser.instGradedMonadGrade {σ τ : Type} [Buffer σ] [Reader σ τ] {ε : Type} : GradedMonad (Parser σ τ ε)

Equations

• Parser.instGradedMonadGrade = { toGradedApplicative := Parser.instGradedApplicativeGrade, gbind := fun {i j : Grade} {α β : Type} => Parser.bind }

theorem Parser.gmap_run {σ τ : Type} [Buffer σ] [Reader σ τ] {α β ε : Type} {n : ℕ} {g : Grade} (f : α → β) (p : Parser σ τ ε g α) (t : Input σ n) : (f <$>ᵍ p).run t = f <$> p.run t

theorem Parser.gbind_run {σ τ : Type} [Buffer σ] [Reader σ τ] {α β ε : Type} {n : ℕ} {g g' : Grade} (m : Parser σ τ ε g α) (k : α → Parser σ τ ε g' β) (t : Input σ n) : (m >>=ᵍ k).run t = (m.run t).handle ⋯ (fun (x : g.errors ≤ possibly) (x_1 : Success n g.consumes α) => Success.bindParser t x_1 k) fun (x : possibly ≤ g.errors) (e : Failure n ε) => failure e

def Parser.fix {σ τ : Type} [Buffer σ] [Reader σ τ] {α ε : Type} {ge : Necessity} [ParserError ε] (f : Parser σ τ ε { errors := ge, consumes := always } α → Parser σ τ ε { errors := ge, consumes := always } α) (h : possibly ≤ ge := by simp) : Parser σ τ ε { errors := ge, consumes := always } α

Build a recursive parser via a fixpoint. Termination is guaranteed by requiring the body to always consume input.

Equations

• Parser.fix f h = { run := fun {n : ℕ} (t : Input σ n) => ↑(Parser.fixGo✝ h f t), sound := ⋯ }

def Parser.withBacktracking {σ τ : Type} [Buffer σ] [Reader σ τ] {α ε : Type} {g : Grade} (p : Parser σ τ ε g α) : Parser σ τ ε g α

Run p. If it fails, restores the original input.

Equations

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

def Parser.choice {σ τ : Type} [Buffer σ] [Reader σ τ] {α ε : Type} {ge ge' gc gc' : Necessity} (p1 : Parser σ τ ε { errors := ge, consumes := gc } α) (p2 : Parser σ τ ε { errors := ge', consumes := gc' } α) : Parser σ τ ε { errors := min ge ge', consumes := ge.ite gc' gc } α

Try p1; if it fails, run p2.

Equations

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

def Parser.«term_<|>_» : Lean.TrailingParserDescr

Equations

• Parser.«term_<|>_» = Lean.ParserDescr.trailingNode `Parser.«term_<|>_» 20 20 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " <|> ") (Lean.ParserDescr.cat `term 21))

def Parser.committedChoice {σ τ : Type} [Buffer σ] [Reader σ τ] {α ε : Type} {ge ge' gc gc' : Necessity} (p1 : Parser σ τ ε { errors := ge, consumes := gc } α) (p2 : Parser σ τ ε { errors := ge', consumes := gc' } α) : Parser σ τ ε { errors := min ge (max ge' possibly), consumes := ge.ite gc' gc } α

try p1; if it fails without consuming, then try p2

Equations

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

def Parser.tryResume {σ τ : Type} [Buffer σ] [Reader σ τ] {α ε : Type} {ge ge' gc gc' : Necessity} (p1 : Parser σ τ ε { errors := ge, consumes := gc } α) (p2 : Parser σ τ ε { errors := ge', consumes := gc' } α) : Parser σ τ ε { errors := min ge ge', consumes := ge.ite (max gc' possibly) gc } α

Try p1 first, if it fails with Failure f, run p2 on the input left at f.restSize

Equations

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

def Parser.oneOf {σ τ : Type} [Buffer σ] [Reader σ τ] {α ε : Type} {g : Grade} (l : NonEmptyList (Parser σ τ ε g α)) : Parser σ τ ε g α

Try each parser in the list in order, returning the first success.

Equations

• Parser.oneOf l = Parser.oneOf.go ↑l ⋯

def Parser.oneOf.go {σ τ : Type} [Buffer σ] [Reader σ τ] {α ε : Type} {g : Grade} (l : List (Parser σ τ ε g α)) (p : l.length ≠ 0 := by simp) : Parser σ τ ε g α

Equations

• Parser.oneOf.go [x] p_2 = x
• Parser.oneOf.go (x :: y :: xs) p_2 = cast ⋯ (x <|> Parser.oneOf.go (y :: xs) ⋯)

def Parser.throw {σ τ : Type} [Buffer σ] [Reader σ τ] {α ε : Type} {ge gc : Necessity} (e : ε) (c : possibly ≤ ge := by simp) : Parser σ τ ε { errors := ge, consumes := gc } α

A parser that always fails with error e.

Equations

• Parser.throw e c = { run := fun {n : ℕ} (x : Input σ n) => Parser.Outcome.throw e, sound := ⋯ }

def Parser.Success.relaxConsumes {α : Type} {n : ℕ} {gc : Necessity} (p : Success n gc α) : Success n (min gc possibly) α

Equations

• p_2.relaxConsumes = p_2
• p_2.relaxConsumes = p_2
• p_2.relaxConsumes = { result := p_2.result, restSize := p_2.restSize, witness := ⋯ }

def Parser.relaxConsumes {σ τ : Type} [Buffer σ] [Reader σ τ] {α ε : Type} {ge gc : Necessity} (p : Parser σ τ ε { errors := ge, consumes := gc } α) : Parser σ τ ε { errors := ge, consumes := min gc possibly } α

Weaken the consumption grade by capping at possibly.

Equations

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

def Parser.relaxErrors {σ τ : Type} [Buffer σ] [Reader σ τ] {α ε : Type} {ge gc : Necessity} (p : Parser σ τ ε { errors := ge, consumes := gc } α) : Parser σ τ ε { errors := min ge possibly, consumes := gc } α

Weaken the error grade by capping at possibly.

Equations

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

def Parser.relax {σ τ : Type} [Buffer σ] [Reader σ τ] {α ε : Type} {ge gc : Necessity} (p : Parser σ τ ε { errors := ge, consumes := gc } α) : Parser σ τ ε { errors := min ge possibly, consumes := min gc possibly } α

Cap both error and consumption grades at possibly.

Equations

• p.relax = p.relaxErrors.relaxConsumes

def Parser.weakenConsumes {σ τ : Type} [Buffer σ] [Reader σ τ] {α ε : Type} {ge gc : Necessity} (p : Parser σ τ ε { errors := ge, consumes := gc } α) : Parser σ τ ε { errors := ge, consumes := possibly } α

Forget consumption precision, setting it to possibly.

Equations

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

def Parser.weakenErrors {σ τ : Type} [Buffer σ] [Reader σ τ] {α ε : Type} {ge gc : Necessity} (p : Parser σ τ ε { errors := ge, consumes := gc } α) : Parser σ τ ε { errors := possibly, consumes := gc } α

Forget error precision, setting it to possibly.

Equations

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

def Parser.weaken {σ τ : Type} [Buffer σ] [Reader σ τ] {α ε : Type} {ge gc : Necessity} (p : Parser σ τ ε { errors := ge, consumes := gc } α) : Parser σ τ ε fallible α

Weaken both grades to possibly, yielding a fallible parser.

Equations

• p.weaken = p.weakenErrors.weakenConsumes

def Parser.runOn {σ τ : Type} [Buffer σ] [Reader σ τ] {α ε : Type} {n : ℕ} {g : Grade} (p : Parser σ τ ε g α) (t : Input σ n) : Except ε α

Run a parser on a Input.

Equations

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

@[reducible, inline]

abbrev Parser.Except.Sound {ε : Type} (errors : Necessity) {α : Type} (r : Except ε α) : Prop

Equations

• Parser.Except.Sound errors (Except.error a) = (possibly ≤ errors)
• Parser.Except.Sound errors (Except.ok a) = (errors ≤ possibly)

theorem Parser.runOn_sound {σ τ : Type} [Buffer σ] [Reader σ τ] {α ε : Type} {n : ℕ} {g : Grade} (p : Parser σ τ ε g α) (t : Input σ n) : Except.Sound g.errors (p.runOn t)

def Parser.anyTok {σ τ : Type} [Buffer σ] [Reader σ τ] : Parser σ τ Error conditional τ

Consume a single token.

Equations

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

theorem Parser.anyTok_run_some {σ τ : Type} [Buffer σ] [Reader σ τ] {n : ℕ} {t : τ} {inp : Input σ n} (h : inp.nextTok = some t := by assumption) : anyTok.run inp = success { result := t, restSize := n - Reader.width σ t, witness := ⋯ }

theorem Parser.anyTok_run_eof {σ τ : Type} [Buffer σ] [Reader σ τ] {n : ℕ} {inp : Input σ n} (h : inp.nextTok = none := by first | assumption | exact Input.nextTok_eq_none) : anyTok.run inp = failure { error := Error.eof, restSize := n, witness := ⋯ }

def Parser.ok {σ τ : Type} [Buffer σ] [Reader σ τ] {α ε : Type} {ge gc : Necessity} (a : α) (he : ge ≤ possibly := by simp) (hc : gc ≤ possibly := by simp) : Parser σ τ ε { errors := ge, consumes := gc } α

Like gpure but with a flexible grade: both ge and gc can be never or possibly. Useful in match branches where all cases must share the same grade.

Equations

• Parser.ok a he hc = { run := fun {n : ℕ} (x : Input σ n) => Parser.success { result := a, restSize := n, witness := ⋯ }, sound := ⋯ }

def Parser.token {σ τ : Type} [Buffer σ] [Reader σ τ] {α : Type} (f : τ → Option α) : Parser σ τ Error conditional α

Consume a token and apply f; succeed with the result or fail if f returns none.

Equations

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

def Parser.satisfy {σ τ : Type} [Buffer σ] [Reader σ τ] (f : τ → Bool) : Parser σ τ Error conditional τ

Consume a token that satisfies predicate f, or fail.

Equations

• Parser.satisfy f = Parser.token fun (t : τ) => if f t = true then some t else none

theorem Parser.satisfy_run_accept {σ τ : Type} [Buffer σ] [Reader σ τ] {n : ℕ} {f : τ → Bool} {t : τ} {inp : Input σ n} (h : inp.nextTok = some t := by assumption) (cond : f t = true := by assumption) : (satisfy f).run inp = success { result := t, restSize := n - Reader.width σ t, witness := ⋯ }

theorem Parser.satisfy_run_reject {σ τ : Type} [Buffer σ] [Reader σ τ] {n : ℕ} {f : τ → Bool} {t : τ} {inp : Input σ n} (h : inp.nextTok = some t := by assumption) (hf : ¬f t = true := by assumption) : (satisfy f).run inp = failure { error := Error.fail, restSize := n - Reader.width σ t, witness := ⋯ }

theorem Parser.satisfy_run_eof {σ τ : Type} [Buffer σ] [Reader σ τ] {n : ℕ} {f : τ → Bool} {inp : Input σ n} (h : inp.nextTok = none := by first | assumption | exact Input.nextTok_eq_none) : (satisfy f).run inp = failure { error := Error.eof, restSize := n, witness := ⋯ }

def Parser.skipSatisfy {σ τ : Type} [Buffer σ] [Reader σ τ] (f : τ → Bool) : Parser σ τ Error conditional PUnit.{1}

Like satisfy but returns PUnit.

Equations

• Parser.skipSatisfy f = () <$ᵍ Parser.satisfy f

def Parser.optional {σ τ : Type} [Buffer σ] [Reader σ τ] {α ε : Type} {ge gc : Necessity} (p : Parser σ τ ε { errors := ge, consumes := gc } α) : Parser σ τ ε { errors := never, consumes := min ge.complement gc } (Option α)

Try p; return some result on success or none on failure, never failing itself.

Equations

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

def Parser.optionalD {σ τ : Type} [Buffer σ] [Reader σ τ] {α ε : Type} {ge gc : Necessity} (p : Parser σ τ ε { errors := ge, consumes := gc } α) (d : α) : Parser σ τ ε { errors := never, consumes := min ge.complement gc } α

Try p; return the result on success or the default value d on failure.

Equations

• p.optionalD d = (fun (x : Option α) => x.getD d) <$>ᵍ p.optional

def Parser.skipOptional {σ τ : Type} [Buffer σ] [Reader σ τ] {α ε : Type} {ge gc : Necessity} (p : Parser σ τ ε { errors := ge, consumes := gc } α) : Parser σ τ ε { errors := never, consumes := min ge.complement gc } PUnit.{1}

Try p, discarding the result; never fails.

Equations

• p.skipOptional = () <$ᵍ p.optional

def Parser.test {σ τ : Type} [Buffer σ] [Reader σ τ] {α ε : Type} {ge gc : Necessity} (p : Parser σ τ ε { errors := ge, consumes := gc } α) : Parser σ τ ε { errors := never, consumes := min ge.complement gc } Bool

Try p; report whether it succeeded, never failing itself.

Equations

• p.test = Option.isSome <$>ᵍ p.optional

def Parser.manyTill {σ τ : Type} [Buffer σ] [Reader σ τ] {α β ε : Type} {ge ge' : Necessity} [ParserError ε] (p : Parser σ τ ε { errors := ge, consumes := always } α) (e : Parser σ τ ε { errors := ge', consumes := always } β) : Parser σ τ ε { errors := ge, consumes := always } (List α)

Repeatedly apply p until e succeeds, collecting the results of p.

Equations

• One or more equations did not get rendered due to their size.
• p_2.manyTill e = (fun (x : α) => [x]) <$>ᵍ p_2
• p_2.manyTill e = (fun (x : α) => [x]) <$>ᵍ p_2

def Parser.many {σ τ : Type} [Buffer σ] [Reader σ τ] {α ε : Type} {ge : Necessity} (p : Parser σ τ ε { errors := ge, consumes := always } α) : Parser σ τ ε flexible (List α)

Apply p zero or more times, collecting results. Requires p to always consume.

Equations

• p.many = { run := fun {n : ℕ} (t : Input σ n) => Parser.success (Parser.many.go p t), sound := ⋯ }

@[irreducible]

def Parser.many.go {σ τ : Type} [Buffer σ] [Reader σ τ] {α ε : Type} {ge : Necessity} (p : Parser σ τ ε { errors := ge, consumes := always } α) {n : ℕ} (t : Input σ n) : Success n possibly (List α)

Equations

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

def Parser.many1 {σ τ : Type} [Buffer σ] [Reader σ τ] {α ε : Type} {ge : Necessity} (p : Parser σ τ ε { errors := ge, consumes := always } α) : Parser σ τ ε { errors := ge, consumes := always } (NonEmptyList α)

Apply p one or more times, collecting results.

Equations

• p.many1 = gcast ⋯ (p >>=ᵍ fun (x : α) => p.many >>=ᵍ fun (xs : List α) => gpure (x ::₁ xs))

def Parser.skipMany {σ τ : Type} [Buffer σ] [Reader σ τ] {α ε : Type} {ge : Necessity} (p : Parser σ τ ε { errors := ge, consumes := always } α) : Parser σ τ ε flexible PUnit.{1}

Apply p zero or more times, discarding results.

Equations

• p.skipMany = () <$ᵍ p.many

def Parser.skipMany1 {σ τ : Type} [Buffer σ] [Reader σ τ] {α ε : Type} {ge : Necessity} (p : Parser σ τ ε { errors := ge, consumes := always } α) : Parser σ τ ε { errors := ge, consumes := always } PUnit.{1}

Apply p one or more times, discarding results.

Equations

• p.skipMany1 = () <$ᵍ p.many1

def Parser.rawBracket {σ τ : Type} [Buffer σ] [Reader σ τ] {α : Type} {ge gc : Necessity} (l r : Parser σ τ Error conditional PUnit.{1}) (p : Parser σ τ Error { errors := ge, consumes := gc } α) : Parser σ τ Error { errors := max ge possibly, consumes := always } α

Parse p surrounded by the delimiters l and r.

Equations

• l.rawBracket r p = gcast ⋯ (l >>=ᵍ fun (__r : Unit) => p >>=ᵍ fun (x : α) => r >>=ᵍ fun (__r : Unit) => gpure x)

def Parser.sepBy {σ τ : Type} [Buffer σ] [Reader σ τ] {α β ε : Type} {ge ge' gc gc' : Necessity} (sep : Parser σ τ ε { errors := ge', consumes := gc' } β) (p : Parser σ τ ε { errors := ge, consumes := gc } α) (h : max gc' gc = always := by simp) : Parser σ τ ε flexible (List α)

Parse zero or more occurrences of p separated by sep.

Equations

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

def Parser.sepBy1 {σ τ : Type} [Buffer σ] [Reader σ τ] {α β ε : Type} {ge ge' gc gc' : Necessity} (sep : Parser σ τ ε { errors := ge', consumes := gc' } β) (p : Parser σ τ ε { errors := ge, consumes := gc } α) (h : max gc' gc = always := by simp) : Parser σ τ ε { errors := ge, consumes := max gc possibly } (NonEmptyList α)

Parse one or more occurrences of p separated by sep.

Equations

• sep.sepBy1 p h = gcast ⋯ (p >>=ᵍ fun (first : α) => (Parser.sepItem✝ sep p h).many >>=ᵍ fun (rest : List α) => gpure (first ::₁ rest))

def Parser.endBy {σ τ : Type} [Buffer σ] [Reader σ τ] {α β ε : Type} {ge ge' gc gc' : Necessity} (sep : Parser σ τ ε { errors := ge', consumes := gc' } β) (p : Parser σ τ ε { errors := ge, consumes := gc } α) (h : max gc gc' = always := by simp) : Parser σ τ ε flexible (List α)

Parse zero or more occurrences of p, each followed by sep.

Equations

• sep.endBy p h = (Parser.endItem✝ sep p h).many

def Parser.endBy1 {σ τ : Type} [Buffer σ] [Reader σ τ] {α β ε : Type} {ge ge' gc gc' : Necessity} (sep : Parser σ τ ε { errors := ge', consumes := gc' } β) (p : Parser σ τ ε { errors := ge, consumes := gc } α) (h : max gc gc' = always := by simp) : Parser σ τ ε { errors := max ge ge', consumes := always } (NonEmptyList α)

Parse one or more occurrences of p, each followed by sep.

Equations

• sep.endBy1 p h = (Parser.endItem✝ sep p h).many1

def Parser.sepEndBy1 {σ τ : Type} [Buffer σ] [Reader σ τ] {α β ε : Type} {ge ge' gc gc' : Necessity} (sep : Parser σ τ ε { errors := ge', consumes := gc' } β) (p : Parser σ τ ε { errors := ge, consumes := gc } α) (h : max gc' gc = always := by simp) : Parser σ τ ε { errors := ge, consumes := max gc possibly } (NonEmptyList α)

Parse one or more occurrences of p separated by sep, with an optional trailing sep.

Equations

• sep.sepEndBy1 p h = gcast ⋯ (sep.sepBy1 p h >>=ᵍ fun (xs : NonEmptyList α) => sep.skipOptional.weakenConsumes >>=ᵍ fun (__r : Unit) => gpure xs)

def Parser.sepEndBy {σ τ : Type} [Buffer σ] [Reader σ τ] {α β ε : Type} {ge ge' gc gc' : Necessity} (sep : Parser σ τ ε { errors := ge', consumes := gc' } β) (p : Parser σ τ ε { errors := ge, consumes := gc } α) (h : max gc' gc = always := by simp) : Parser σ τ ε flexible (List α)

Parse zero or more occurrences of p separated by sep, with an optional trailing sep.

Equations

• sep.sepEndBy p h = sep.sepBy p h >>=ᵍ fun (xs : List α) => sep.skipOptional.weakenConsumes >>=ᵍ fun (__r : Unit) => gpure xs

def Parser.count1 {σ τ : Type} [Buffer σ] [Reader σ τ] {α ε : Type} {ge gc : Necessity} (n : ℕ) (p : Parser σ τ ε { errors := ge, consumes := gc } α) : Parser σ τ ε { errors := ge, consumes := gc } (List.Vector α (n + 1))

Parse exactly n + 1 occurrences of p.

Equations

• Parser.count1 0 p = (fun (x : α) => x ::ᵥ List.Vector.nil) <$>ᵍ p
• Parser.count1 n_2.succ p = gcast ⋯ (p >>=ᵍ fun (x : α) => Parser.count1 n_2 p >>=ᵍ fun (rest : List.Vector α (n_2 + 1)) => gpure (x ::ᵥ rest))

theorem Parser.count1_succ {σ τ : Type} [Buffer σ] [Reader σ τ] {α ε : Type} (n : ℕ) (p : Parser σ τ ε conditional α) : count1 (n + 1) p = p >>=ᵍ fun (x : α) => count1 n p >>=ᵍ fun (rest : List.Vector α (n + 1)) => gpure (x ::ᵥ rest)

def Parser.count {σ τ : Type} [Buffer σ] [Reader σ τ] {α ε : Type} {ge gc : Necessity} (n : ℕ) (p : Parser σ τ ε { errors := ge, consumes := gc } α) : Parser σ τ ε { errors := min ge possibly, consumes := min gc possibly } (List.Vector α n)

Parse exactly n occurrences of p.

Equations

• Parser.count 0 p = Parser.ok List.Vector.nil ⋯ ⋯
• Parser.count n_2.succ p = (Parser.count1 n_2 p).relax

def Parser.skip {σ τ : Type} [Buffer σ] [Reader σ τ] {α ε : Type} {ge gc : Necessity} (n : ℕ) (p : Parser σ τ ε { errors := ge, consumes := gc } α) : Parser σ τ ε { errors := min ge possibly, consumes := min gc possibly } PUnit.{1}

Skip exactly n occurrences of p.

Equations

• Parser.skip n p = () <$ᵍ Parser.count n p

def Parser.skipUpTo {σ τ : Type} [Buffer σ] [Reader σ τ] {α ε : Type} {ge : Necessity} (n : ℕ) : Parser σ τ ε { errors := ge, consumes := always } α → Parser σ τ ε flexible PUnit.{1}

Skip up to n occurrences of p.

Equations

• One or more equations did not get rendered due to their size.
• Parser.skipUpTo 0 x✝ = Parser.ok () Parser.token._proof_2 Parser.token._proof_1

def Parser.skipManyN {σ τ : Type} [Buffer σ] [Reader σ τ] {α ε : Type} {ge : Necessity} (n : ℕ) (p : Parser σ τ ε { errors := ge, consumes := always } α) : Parser σ τ ε { errors := min ge possibly, consumes := possibly } PUnit.{1}

Skip n or more occurrences of p.

Equations

• Parser.skipManyN n p = gcast ⋯ (Parser.skip n p >>=ᵍ fun (__r : Unit) => p.skipMany)

def Parser.skipUntil {σ τ : Type} [Buffer σ] [Reader σ τ] {α β ε : Type} {ge ge' : Necessity} [ParserError ε] (stop : Parser σ τ ε { errors := ge', consumes := always } β) (p : Parser σ τ ε { errors := ge, consumes := always } α) : Parser σ τ ε { errors := ge, consumes := always } PUnit.{1}

Run p until stop succeeds; discard p's results.

Equations

• stop.skipUntil p = () <$ᵍ p.manyTill stop

def Parser.sepByN {σ τ : Type} [Buffer σ] [Reader σ τ] {α β ε : Type} {ge ge' gc gc' : Necessity} (sep : Parser σ τ ε { errors := ge', consumes := gc' } β) (p : Parser σ τ ε { errors := ge, consumes := gc } α) (n : ℕ) : Parser σ τ ε fallible (List.Vector α n)

Parse exactly n occurrences of p separated by sep.

Equations

• sep.sepByN p 0 = Parser.ok List.Vector.nil Parser.token._proof_1 Parser.token._proof_1
• sep.sepByN p n_1.succ = (have sepP := sep >>=ᵍ fun (__x : β) => p; p >>=ᵍ fun (p1 : α) => Parser.count n_1 sepP >>=ᵍ fun (ps : List.Vector α n_1) => gpure (p1 ::ᵥ ps)).weaken

def Parser.chainl1 {σ τ : Type} [Buffer σ] [Reader σ τ] {α ε : Type} {ge ge' : Necessity} (op : Parser σ τ ε { errors := ge', consumes := always } (α → α → α)) (p : Parser σ τ ε { errors := ge, consumes := always } α) : Parser σ τ ε { errors := ge, consumes := always } α

Parse one or more occurrences of p separated by left-associative operator op.

Equations

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

def Parser.eof {σ τ : Type} [Buffer σ] [Reader σ τ] : Parser σ τ Error Grade.lookahead PUnit.{1}

Succeed only at end of input, consuming nothing.

Equations

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

def Parser.lookahead {σ τ : Type} [Buffer σ] [Reader σ τ] {α : Type} {ge gc : Necessity} (p : Parser σ τ Error { errors := ge, consumes := gc } α) : Parser σ τ Error { errors := ge, consumes := never } α

Run p without consuming input, keeping only the result.

Equations

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

def Parser.peek {σ τ : Type} [Buffer σ] [Reader σ τ] : Parser σ τ Error Grade.lookahead τ

Equations

• Parser.peek = Parser.anyTok.lookahead

def Parser.notFollowedBy {σ τ : Type} [Buffer σ] [Reader σ τ] {α : Type} {ge gc : Necessity} (p : Parser σ τ Error { errors := ge, consumes := gc } α) : Parser σ τ Error { errors := ge.complement, consumes := never } PUnit.{1}

Succeed (without consuming) only when p fails.

Equations

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

def Parser.withRecovery {σ τ : Type} [Buffer σ] [Reader σ τ] {α ε ε' : Type} {ge ge' gc gc' : Necessity} (recover : ε' → Parser σ τ ε { errors := ge, consumes := gc } α) (p : Parser σ τ ε' { errors := ge', consumes := gc' } α) : Parser σ τ ε' { errors := min ge ge', consumes := ge'.ite gc gc' } α

Run p; if it fails with error e, run recover e. If recovery also fails, report p's original error.

Equations

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