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

@[reducible, inline]

abbrev Text (n : ℕ) : Type

Input text of statically known length n.

Equations

• Text n = List.Vector Char n

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

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

Equations

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

instance instReprGrade : Repr Grade

Equations

• instReprGrade = { reprPrec := instReprGrade.repr }

@[reducible, inline]

abbrev Grade.impossible : Grade

Equations

• Grade.impossible = { errors := Necessity.never, consumes := Necessity.always }

@[reducible, inline]

abbrev Grade.conditional : Grade

Equations

• Grade.conditional = { errors := Necessity.possibly, consumes := Necessity.always }

@[reducible, inline]

abbrev Grade.flexible : Grade

Equations

• Grade.flexible = { errors := Necessity.never, consumes := Necessity.possibly }

@[reducible, inline]

abbrev Grade.fallible : Grade

Equations

• Grade.fallible = { errors := Necessity.possibly, consumes := Necessity.possibly }

@[reducible, inline]

abbrev Grade.pure : Grade

Equations

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

@[reducible, inline]

abbrev Grade.lookahead : Grade

Equations

• Grade.lookahead = { errors := Necessity.possibly, consumes := Necessity.never }

@[reducible, inline]

abbrev Grade.empty : Grade

Equations

• Grade.empty = { errors := Necessity.always, consumes := Necessity.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 Grade.instMax : Max Grade

Equations

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

instance Grade.instMonoid : Monoid Grade

Equations

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

instance Grade.instZero : Zero Grade

Equations

• Grade.instZero = { zero := Grade.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 := Necessity.never, consumes := Necessity.never }

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 Necessity.always = (n < m)
• Parser.consumptionWitness n m Necessity.possibly = (n ≤ m)
• Parser.consumptionWitness n m Necessity.never = (n = m)

@[simp]

theorem Parser.consumptionWitness.rfl {n : ℕ} {a : Necessity} : a ≤ Necessity.possibly → consumptionWitness n n a

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

theorem Parser.consumptionWitness.min_possibly {n m : ℕ} {a : Necessity} : consumptionWitness n m a → consumptionWitness n m (min Necessity.possibly a)

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 : ℕ
• restText : Text self.restSize
• witness : consumptionWitness self.restSize n consumes

@[reducible, inline]

abbrev Parser.Outcome (ε : Type) (n : ℕ) (g : Grade) (α : Type) : Type

The result type of running a parser

Equations

• Parser.Outcome ε n g α = match g.errors with | Necessity.never => Parser.Success n g.consumes α | Necessity.possibly => ε ⊕ Parser.Success n g.consumes α | Necessity.always => ε

structure Parser (ε : 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 : ℕ} : Text n → Outcome ε n g α

def Parser.Outcome.handle {α β ε : Type} {n : ℕ} {ge gc : Necessity} (p : Outcome ε n { errors := ge, consumes := gc } α) (e : Necessity.possibly ≤ ge → ε → β) (s : ge ≤ Necessity.possibly → Success n gc α → β) : β

Equations

• p_2.handle e_2 s_2 = e_2 Parser.Outcome.handle._proof_1 p_2
• p_2.handle e_2 s_2 = s_2 Parser.Outcome.handle._proof_2 p_2
• Parser.Outcome.handle (Sum.inl x) e_2 s_2 = e_2 Parser.Outcome.handle._proof_3 x
• Parser.Outcome.handle (Sum.inr x) e_2 s_2 = s_2 Parser.Outcome.handle._proof_3 x

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, restText := x.restText, witness := ⋯ } }

instance Parser.instGFunctorNecessitySuccess {n : ℕ} : GFunctor (Success n)

Equations

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

instance Parser.instFunctorOutcome {ε : Type} {n : ℕ} {g : Grade} : Functor (Outcome ε n g)

Equations

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

def Parser.Error.eof : Error

Equations

• Parser.Error.eof = "eof"

def Parser.Error.fail : Error

Equations

• Parser.Error.fail = "fail"

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

Equations

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

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

Equations

• r1.ap' r2 = { result := r2.result r1.result, restSize := r2.restSize, restText := r2.restText, 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, restText := r2.restText, witness := ⋯ }

def Parser.Success.bindParser {α β ε : Type} {n : ℕ} {xc fe fc : Necessity} (x : Success n xc α) (f : α → Parser ε { errors := fe, consumes := fc } β) : Outcome ε n { errors := fe, consumes := max xc fc } β

Equations

• x.bindParser f_2 = (f_2 x.result).run x.restText
• x.bindParser f_2 = x.seq ((f_2 x.result).run x.restText)
• x.bindParser f_2 = match (f_2 x.result).run x.restText with | Sum.inr y => Sum.inr (x.seq y) | Sum.inl e => Sum.inl e

instance Parser.instGFunctorGrade {ε : Type} : GFunctor (Parser ε)

Equations

• Parser.instGFunctorGrade = { gmap := fun {i : Grade} {α β : Type} (f : α → β) (p : Parser ε i α) => { run := fun {n : ℕ} (t : Text n) => f <$> p.run t } }

def Parser.Outcome.throw {α ε : Type} {n : ℕ} {g : Grade} (e : ε) (h : Necessity.possibly ≤ g.errors := by simp) : Outcome ε n g α

Equations

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

def Parser.Outcome.ofSuccess {α ε : Type} {n : ℕ} {ge gc : Necessity} (r : Success n gc α) (c : ge ≤ Necessity.possibly := by decide) : Outcome ε n { errors := ge, consumes := gc } α

Equations

• Parser.Outcome.ofSuccess r c_2 = r
• Parser.Outcome.ofSuccess r c_2 = Sum.inr r

def Parser.bind {α β ε : 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.instIsEmptyImpossible {α ε : Type} : IsEmpty (Parser ε Grade.impossible α)

@[reducible, inline]

abbrev Parser.pure {α ε : Type} (a : α) : Parser ε 1 α

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

Equations

• Parser.pure a = { run := fun {n : ℕ} (t : Text n) => { result := a, restSize := n, restText := t, witness := ⋯ } }

instance Parser.instGApplicativeGrade {ε : Type} : GApplicative (Parser ε)

Equations

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

instance Parser.instGMonadGrade {ε : Type} : GMonad (Parser ε)

Equations

• Parser.instGMonadGrade = { toGApplicative := Parser.instGApplicativeGrade, gbind := fun {i j : Grade} {α β : Type} => Parser.bind }

def Parser.fix {α ε : Type} {ge : Necessity} [Inhabited ε] (f : Parser ε { errors := ge, consumes := Necessity.always } α → Parser ε { errors := ge, consumes := Necessity.always } α) (h : Necessity.possibly ≤ ge := by simp) : Parser ε { errors := ge, consumes := Necessity.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 : Text n) => Parser.fix.go f h t }

@[irreducible]

def Parser.fix.go {α ε : Type} {ge : Necessity} [Inhabited ε] (f : Parser ε { errors := ge, consumes := Necessity.always } α → Parser ε { errors := ge, consumes := Necessity.always } α) (h : Necessity.possibly ≤ ge) {n : ℕ} (t : Text n) : Outcome ε n { errors := ge, consumes := Necessity.always } α

Equations

• Parser.fix.go f h x = Parser.Outcome.throw default h
• Parser.fix.go f h t_2 = (f { run := fun {k : ℕ} (t' : Text k) => if k ≤ n_2 then Parser.fix.go f h t' else Parser.Outcome.throw default h }).run t_2

def Parser.choice {α ε : 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, try p2. The error grade is the infimum and the consumption grade is computed via Necessity.ite.

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.oneOf {α ε : Type} {g : Grade} (l : List (Parser ε g α)) (p : l.length ≠ 0 := by simp) : Parser ε g α

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

Equations

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

def Parser.throw {α ε : Type} {ge gc : Necessity} (e : ε) (c : Necessity.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 : Text n) => Parser.Outcome.throw e c }

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

Equations

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

def Parser.relaxConsumes {α ε : Type} {ge gc : Necessity} (p : Parser ε { errors := ge, consumes := gc } α) : Parser ε { errors := ge, consumes := min gc Necessity.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} {ge gc : Necessity} (p : Parser ε { errors := ge, consumes := gc } α) : Parser ε { errors := min ge Necessity.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} {ge gc : Necessity} (p : Parser ε { errors := ge, consumes := gc } α) : Parser ε { errors := min ge Necessity.possibly, consumes := min gc Necessity.possibly } α

Cap both error and consumption grades at possibly.

Equations

• p.relax = p.relaxErrors.relaxConsumes

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

Equations

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

def Parser.weakenConsumes {α ε : Type} {ge gc : Necessity} (p : Parser ε { errors := ge, consumes := gc } α) : Parser ε { errors := ge, consumes := Necessity.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} {ge gc : Necessity} (p : Parser ε { errors := ge, consumes := gc } α) : Parser ε { errors := Necessity.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} {ge gc : Necessity} (p : Parser ε { errors := ge, consumes := gc } α) : Parser ε Grade.fallible α

Weaken both grades to possibly, yielding a fallible parser.

Equations

• p.weaken = p.weakenErrors.weakenConsumes

def Parser.runOption {α ε : Type} {n : ℕ} {ge gc : Necessity} (p : Parser ε { errors := ge, consumes := gc } α) (t : Text n) : Option (Success n gc α)

Run a parser, discarding the error and returning the Success as an Option.

Equations

• p.runOption t = (p.run t).handle (fun (x : Necessity.possibly ≤ ge) (x_1 : ε) => none) fun (x : ge ≤ Necessity.possibly) (r : Parser.Success n gc α) => some r

def Parser.runResult? {α ε : Type} {n : ℕ} {ge gc : Necessity} (p : Parser ε { errors := ge, consumes := gc } α) (t : Text n) : Option α

Run a parser, returning only the parsed value as an Option.

Equations

• p.runResult? t = (p.run t).handle (fun (x : Necessity.possibly ≤ ge) (x_1 : ε) => none) fun (x : ge ≤ Necessity.possibly) (r : Parser.Success n gc α) => some r.result

def Parser.anyChar : Parser Error Grade.conditional Char

Consume and return a single character, or fail on empty input.

Equations

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

def Parser.ok {α ε : Type} {ge gc : Necessity} (a : α) (he : ge ≤ Necessity.possibly := by simp) (hc : gc ≤ Necessity.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_2 = (gpure a).weakenErrors.weakenConsumes
• Parser.ok a he hc_2 = (gpure a).weakenConsumes
• Parser.ok a he hc_2 = (absurd ⋯ Parser.ok._proof_2).weakenConsumes
• Parser.ok a he_2 hc_2 = (gpure a).weakenErrors
• Parser.ok a he_2 hc_2 = gpure a

def Parser.token {α : Type} (f : Char → Option α) : Parser Error Grade.conditional α

Consume a character 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 (f : Char → Bool) : Parser Error Grade.conditional Char

Consume a character that satisfies predicate f, or fail.

Equations

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

def Parser.char (c : Char) : Parser Error Grade.conditional PUnit.{1}

Match a specific character.

Equations

• Parser.char c = () <$ᵍ Parser.satisfy fun (x : Char) => x == c

def Parser.string (str : String) : Parser Error Grade.conditional PUnit.{1}

Match an exact string.

Equations

• Parser.string str = Parser.string.go str.toList

def Parser.string.go : List Char → Parser Error Grade.conditional PUnit.{1}

Equations

• Parser.string.go [] = Parser.throw Parser.Error.fail Parser.Outcome.handle._proof_3
• Parser.string.go [c] = () <$ᵍ Parser.satisfy fun (x : Char) => x == c
• Parser.string.go (c :: cs) = (Parser.satisfy fun (x : Char) => x == c) >>=ᵍ fun (x : Char) => Parser.string.go cs

def Parser.optional {α ε : Type} {ge gc : Necessity} (p : Parser ε { errors := ge, consumes := gc } α) : Parser ε { errors := Necessity.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} {ge gc : Necessity} (p : Parser ε { errors := ge, consumes := gc } α) (d : α) : Parser ε { errors := Necessity.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.optionalBind {α β ε : Type} {ge ge' gc gc' : Necessity} (p : Parser ε { errors := ge, consumes := gc } α) (cont : α → Parser ε { errors := ge', consumes := gc' } β) : Parser ε { errors := Necessity.never, consumes := min (max ge ge').complement (max gc gc') } (Option β)

Try p then apply cont to its result; wrap the final result in Option.

Equations

• p.optionalBind cont = (gcast ⋯ (p >>=ᵍ fun (a : α) => cont a)).optional

def Parser.manyTill {α β ε : Type} {ge ge' : Necessity} [Inhabited ε] (p : Parser ε { errors := ge, consumes := Necessity.always } α) (e : Parser ε { errors := ge', consumes := Necessity.always } β) : Parser ε { errors := ge, consumes := Necessity.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 = ⋯.elim

def Parser.many {α ε : Type} {ge : Necessity} (p : Parser ε { errors := ge, consumes := Necessity.always } α) : Parser ε Grade.flexible (List α)

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

Equations

• p.many = { run := fun {n : ℕ} => Parser.many.go p }

@[irreducible]

def Parser.many.go {α ε : Type} {ge : Necessity} {n : ℕ} (p : Parser ε { errors := ge, consumes := Necessity.always } α) (t : Text n) : Success n Necessity.possibly (List α)

Equations

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

@[reducible, inline]

abbrev Parser.NonEmptyList (α : Type u_1) : Type u_1

Equations

• Parser.NonEmptyList α = { l : List α // l ≠ [] }

@[reducible, inline]

abbrev Parser.NonEmptyList.mk {α : Type} (x : α) (xs : List α) : NonEmptyList α

Equations

• x ::₁ xs = ⟨x :: xs, ⋯⟩

@[reducible, inline]

abbrev Parser.NonEmptyList.toList {α : Type} : NonEmptyList α → List α

Equations

• x✝.toList = ↑x✝

def Parser.«term_::₁_» : Lean.TrailingParserDescr

Equations

• Parser.«term_::₁_» = Lean.ParserDescr.trailingNode `Parser.«term_::₁_» 67 68 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ::₁ ") (Lean.ParserDescr.cat `term 67))

def Parser.many1 {α ε : Type} {ge : Necessity} (p : Parser ε { errors := ge, consumes := Necessity.always } α) : Parser ε { errors := ge, consumes := Necessity.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.takeWhile (f : Char → Bool) : Parser Error Grade.flexible String

Consume characters while f holds, returning the collected string.

Equations

• Parser.takeWhile f = String.ofList <$>ᵍ (Parser.satisfy f).many

def Parser.takeWhile1 (f : Char → Bool) : Parser Error Grade.conditional String

Consume one or more characters while f holds.

Equations

• Parser.takeWhile1 f = (String.ofList ∘ Parser.NonEmptyList.toList) <$>ᵍ (Parser.satisfy f).many1

def Parser.skipWhile (f : Char → Bool) : Parser Error Grade.flexible PUnit.{1}

Skip characters while f holds.

Equations

• Parser.skipWhile f = () <$ᵍ Parser.takeWhile f

def Parser.skipWhile1 (f : Char → Bool) : Parser Error Grade.conditional PUnit.{1}

Skip one or more characters while f holds.

Equations

• Parser.skipWhile1 f = () <$ᵍ Parser.takeWhile1 f

def Parser.whitespace : Parser Error Grade.flexible PUnit.{1}

Skip zero or more whitespace characters.

Equations

• Parser.whitespace = Parser.skipWhile Char.isWhitespace

def Parser.whitespace1 : Parser Error Grade.conditional PUnit.{1}

Skip one or more whitespace characters.

Equations

• Parser.whitespace1 = Parser.skipWhile1 Char.isWhitespace

def Parser.lexeme {α : Type} {ge gc : Necessity} (p : Parser Error { errors := ge, consumes := gc } α) : Parser Error { errors := ge, consumes := max gc Necessity.possibly } α

Run p then skip trailing whitespace.

Equations

• p.lexeme = gcast ⋯ (p >>=ᵍ fun (r : α) => Parser.whitespace >>=ᵍ fun (x : PUnit.{1}) => gpure r)

def Parser.lparen : Parser Error Grade.conditional PUnit.{1}

Equations

• Parser.lparen = Parser.char '('

def Parser.rparen : Parser Error Grade.conditional PUnit.{1}

Equations

• Parser.rparen = Parser.char ')'

def Parser.lbracket : Parser Error Grade.conditional PUnit.{1}

Equations

• Parser.lbracket = Parser.char '['

def Parser.rbracket : Parser Error Grade.conditional PUnit.{1}

Equations

• Parser.rbracket = Parser.char ']'

def Parser.lbrace : Parser Error Grade.conditional PUnit.{1}

Equations

• Parser.lbrace = Parser.char '{'

def Parser.rbrace : Parser Error Grade.conditional PUnit.{1}

Equations

• Parser.rbrace = Parser.char '}'

def Parser.dquote : Parser Error Grade.conditional PUnit.{1}

Equations

• Parser.dquote = Parser.char '\"'

def Parser.comma : Parser Error Grade.conditional PUnit.{1}

Equations

• Parser.comma = Parser.char ','

def Parser.parens {α : Type} {ge gc : Necessity} (p : Parser Error { errors := ge, consumes := gc } α) : Parser Error { errors := max ge Necessity.possibly, consumes := Necessity.always } α

Parse p surrounded by parentheses.

Equations

• p.parens = gcast ⋯ (Parser.lparen.lexeme >>=ᵍ fun (x : PUnit.{1}) => p >>=ᵍ fun (r : α) => Parser.rparen.lexeme >>=ᵍ fun (x : PUnit.{1}) => gpure r)

def Parser.brackets {α : Type} {ge gc : Necessity} (p : Parser Error { errors := ge, consumes := gc } α) : Parser Error { errors := max ge Necessity.possibly, consumes := Necessity.always } α

Parse p surrounded by square brackets.

Equations

• p.brackets = gcast ⋯ (Parser.lbracket.lexeme >>=ᵍ fun (x : PUnit.{1}) => p >>=ᵍ fun (r : α) => Parser.rbracket.lexeme >>=ᵍ fun (x : PUnit.{1}) => gpure r)

def Parser.braces {α : Type} {ge gc : Necessity} (p : Parser Error { errors := ge, consumes := gc } α) : Parser Error { errors := max ge Necessity.possibly, consumes := Necessity.always } α

Parse p surrounded by curly braces.

Equations

• p.braces = gcast ⋯ (Parser.lbrace.lexeme >>=ᵍ fun (x : PUnit.{1}) => p >>=ᵍ fun (r : α) => Parser.rbrace.lexeme >>=ᵍ fun (x : PUnit.{1}) => gpure r)

def Parser.digit : Parser Error Grade.conditional ℕ

Parse a single decimal digit, returning its numeric value.

Equations

• Parser.digit = Parser.token fun (c : Char) => if c.isDigit = true then some (c.toNat - '0'.toNat) else none

def Parser.nat : Parser Error Grade.conditional ℕ

Parse a natural number (one or more digits).

Equations

• Parser.nat = Parser.digit >>=ᵍ fun (d : ℕ) => Parser.digit.many >>=ᵍ fun (ds : List ℕ) => gpure (List.foldl (fun (acc d : ℕ) => acc * 10 + d) d ds)

def Parser.int : Parser Error Grade.conditional ℤ

Parse an integer (optional leading - followed by digits).

Equations

• Parser.int = gcast Parser.int._proof_1 ((Parser.char '-').optional >>=ᵍ fun (neg : Option PUnit.{1}) => Parser.nat >>=ᵍ fun (n : ℕ) => gpure (if neg.isSome = true then -↑n else ↑n))

def Parser.sepBy {α β ε : Type} {ge ge' gc gc' : Necessity} (sep : Parser ε { errors := ge', consumes := gc' } β) (p : Parser ε { errors := ge, consumes := gc } α) (h : max gc' gc = Necessity.always := by simp) : Parser ε Grade.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.countSucc {α ε : Type} {ge gc : Necessity} (p : Parser ε { errors := ge, consumes := gc } α) (n : ℕ) : Parser ε { errors := ge, consumes := gc } (List.Vector α (n + 1))

Parse exactly n + 1 occurrences of p.

Equations

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

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

Parse exactly n occurrences of p.

Equations

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

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

Parse exactly n occurrences of p separated by sep.

Equations

• sep.sepByN p 0 = Parser.ok List.Vector.nil Parser.Outcome.handle._proof_3 Parser.Outcome.handle._proof_3
• sep.sepByN p n.succ = (have sepP := gcast ⋯ (sep >>=ᵍ fun (x : β) => p); p >>=ᵍ fun (p1 : α) => sepP.count n >>=ᵍ fun (ps : List.Vector α n) => gpure (p1 ::ᵥ ps)).weaken

def Parser.chainl1 {α ε : Type} {ge ge' : Necessity} (op : Parser ε { errors := ge', consumes := Necessity.always } (α → α → α)) (p : Parser ε { errors := ge, consumes := Necessity.always } α) : Parser ε { errors := ge, consumes := Necessity.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 : 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} {ge gc : Necessity} (p : Parser Error { errors := ge, consumes := gc } α) : Parser Error { errors := ge, consumes := Necessity.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.notFollowedBy {α : Type} {ge gc : Necessity} (p : Parser Error { errors := ge, consumes := gc } α) : Parser Error { errors := ge.complement, consumes := Necessity.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} {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.