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

• 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 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 := 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 : ℕ} {a : Necessity} : a ≤ 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 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

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

A failed parse result

• error : ε
• restSize : ℕ
• restText : Text self.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, restText := f.restText, witness := ⋯ }

@[simp]

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

Equations

• ⋯ = ⋯

@[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 | never => Parser.Success n g.consumes α | possibly => Parser.Failure n ε ⊕ Parser.Success n g.consumes α | always => Parser.Failure n ε

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 : possibly ≤ ge → Failure n ε → β) (s : ge ≤ 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.instGradedFunctorNecessitySuccess {n : ℕ} : GradedFunctor (Success n)

Equations

• Parser.instGradedFunctorNecessitySuccess = { 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.le {α : Type} {n : ℕ} {gc : Necessity} (p : Success n gc α) : p.restSize ≤ n

Equations

• ⋯ = ⋯

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

Equations

• p.weakenConsumes = { result := p.result, restSize := p.restSize, restText := p.restText, 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, restText := s.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 := 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 = Parser.Failure.trans ((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.trans ⋯)

instance Parser.instGradedFunctorGrade {ε : Type} : GradedFunctor (Parser ε)

Equations

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

def Parser.Outcome.throwFailure {α ε : Type} {n : ℕ} {g : Grade} (f : Failure n ε) (h : possibly ≤ g.errors := by simp) : Outcome ε n g α

Equations

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

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

Equations

• Parser.Outcome.throw e t h = Parser.Outcome.throwFailure { error := e, restSize := n, restText := t, witness := ⋯ } h

def Parser.Outcome.ofSuccess {α ε : Type} {n : ℕ} {ge gc : Necessity} (r : Success n gc α) (c : ge ≤ 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 ε 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.instGradedApplicativeGrade {ε : Type} : GradedApplicative (Parser ε)

Equations

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

instance Parser.instGradedMonadGrade {ε : Type} : GradedMonad (Parser ε)

Equations

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

def Parser.fix {α ε : Type} {ge : Necessity} [Inhabited ε] (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 : Text n) => Parser.fix.go f h t }

@[irreducible]

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

Equations

• Parser.fix.go f h t_2 = Parser.Outcome.throw default t_2 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 t' h }).run t_2

def Parser.withBacktracking {α ε : Type} {g : Grade} (p : Parser ε g α) : Parser ε g α

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

Equations

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

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.committedChoice {α ε : 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} {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 f.restText

Equations

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

def Parser.oneOf {α ε : 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} {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} {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 : ℕ} (t : Text n) => Parser.Outcome.throw e t c }

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

def Parser.relaxConsumes {α ε : 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} {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} {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} {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} {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} {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.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 : possibly ≤ ge) (x_1 : Parser.Failure n ε) => none) fun (x : ge ≤ 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 : possibly ≤ ge) (x_1 : Parser.Failure n ε) => none) fun (x : ge ≤ possibly) (r : Parser.Success n gc α) => some r.result

def Parser.anyChar : Parser Error 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 ≤ 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_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 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 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.skipSatisfy (f : Char → Bool) : Parser Error conditional PUnit.{1}

Like satisfy but returns PUnit.

Equations

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

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

Match a specific character.

Equations

• Parser.char c = Parser.skipSatisfy fun (x : Char) => x == c

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

Match an exact string.

Equations

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

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

Equations

• Parser.string.go [] = Parser.throw Parser.Error.fail Parser.Outcome.handle._proof_3
• Parser.string.go [c] = Parser.skipSatisfy fun (x : Char) => x == c
• Parser.string.go (c :: cs) = (Parser.skipSatisfy fun (x : Char) => x == c) >>=ᵍ fun (x : PUnit.{1}) => Parser.string.go cs

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

Equations

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

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

def Parser.many {α ε : 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 : ℕ} => Parser.many.go p }

@[irreducible]

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

Equations

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

def Parser.many1 {α ε : 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} {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} {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.takeWhile (f : Char → Bool) : Parser Error 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 conditional String

Consume one or more characters while f holds.

Equations

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

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

Skip characters while f holds.

Equations

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

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

Skip one or more characters while f holds.

Equations

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

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

Skip zero or more whitespace characters.

Equations

• Parser.whitespace = Parser.skipWhile Char.isWhitespace

def Parser.whitespace1 : Parser Error 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 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 conditional PUnit.{1}

Equations

• Parser.lparen = Parser.char '('

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

Equations

• Parser.rparen = Parser.char ')'

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

Equations

• Parser.lbracket = Parser.char '['

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

Equations

• Parser.rbracket = Parser.char ']'

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

Equations

• Parser.lbrace = Parser.char '{'

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

Equations

• Parser.rbrace = Parser.char '}'

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

Equations

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

def Parser.comma : Parser Error 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 possibly, consumes := 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 possibly, consumes := 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 possibly, consumes := 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 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 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 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.space : Parser Error conditional PUnit.{1}

Equations

• Parser.space = Parser.skipSatisfy fun (x : Char) => x == ' '

def Parser.tab : Parser Error conditional PUnit.{1}

Equations

• Parser.tab = Parser.skipSatisfy fun (x : Char) => x == '\t'

def Parser.ASCII.lf : Parser Error conditional PUnit.{1}

Equations

• Parser.ASCII.lf = Parser.skipSatisfy fun (x : Char) => x == '\n'

def Parser.ASCII.cr : Parser Error conditional PUnit.{1}

Equations

• Parser.ASCII.cr = Parser.skipSatisfy fun (x : Char) => x == '\x0d'

def Parser.ASCII.uppercase : Parser Error conditional Char

Match an ASCII uppercase letter.

Equations

• Parser.ASCII.uppercase = Parser.satisfy Char.isUpper

def Parser.ASCII.lowercase : Parser Error conditional Char

Match an ASCII lowercase letter.

Equations

• Parser.ASCII.lowercase = Parser.satisfy Char.isLower

def Parser.ASCII.alpha : Parser Error conditional Char

Match an ASCII letter.

Equations

• Parser.ASCII.alpha = Parser.satisfy Char.isAlpha

def Parser.ASCII.alphanum : Parser Error conditional Char

Match an ASCII letter or digit.

Equations

• Parser.ASCII.alphanum = Parser.satisfy Char.isAlphanum

def Parser.ASCII.control : Parser Error conditional Char

Match an ASCII control character.

Equations

• Parser.ASCII.control = Parser.satisfy fun (c : Char) => decide (c.val < 32) || c.val == 127

def Parser.ASCII.binDigit : Parser Error conditional Bool

Match a binary digit.

Equations

• Parser.ASCII.binDigit = Parser.token fun (x : Char) => match x with | '0' => some false | '1' => some true | x => none

def Parser.ASCII.octDigit : Parser Error conditional (Fin 8)

Match an octal digit, returning its numeric value.

Equations

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

def Parser.ASCII.hexDigit : Parser Error conditional (Fin 16)

Match a hexadecimal digit, returning its numeric value.

Equations

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

def Parser.eol : Parser Error conditional PUnit.{1}

Match a line terminator: LF or CRLF.

Equations

• Parser.eol = gcast Parser.eol._proof_1 (Parser.ASCII.cr.optional >>=ᵍ fun (x : Option PUnit.{1}) => Parser.ASCII.lf)

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 = 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} {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 : α) => have item := gcast ⋯ (sep >>=ᵍ fun (x : β) => p); item.many >>=ᵍ fun (rest : List α) => gpure (first ::₁ rest))

def Parser.endBy {α β ε : 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 = (gcast ⋯ (p >>=ᵍ fun (x : α) => sep >>=ᵍ fun (x_1 : β) => gpure x)).many

def Parser.endBy1 {α β ε : 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 = (gcast ⋯ (p >>=ᵍ fun (x : α) => sep >>=ᵍ fun (x_1 : β) => gpure x)).many1

def Parser.sepEndBy1 {α β ε : 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.optional.weakenConsumes >>=ᵍ fun (x : Option β) => gpure xs)

def Parser.sepEndBy {α β ε : 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 = gcast Parser.sepEndBy._proof_1 (sep.sepBy p h >>=ᵍ fun (xs : List α) => sep.optional.weakenConsumes >>=ᵍ fun (x : Option β) => gpure xs)

def Parser.count1 {α ε : 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))

def Parser.count {α ε : 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} {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} {ge : Necessity} (n : ℕ) : Parser ε { errors := ge, consumes := always } α → Parser ε flexible PUnit.{1}

Skip up to n occurrences of p; never fails.

Equations

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

def Parser.skipManyN {α ε : 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 (x : PUnit.{1}) => p.skipMany)

def Parser.skipUntil {α β ε : Type} {ge ge' : Necessity} [Inhabited ε] (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} {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.Outcome.handle._proof_3 Parser.Outcome.handle._proof_3
• sep.sepByN p n_1.succ = (have sepP := gcast ⋯ (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} {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 : 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 := 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 : Parser Error Grade.lookahead Char

Equations

• Parser.peek = Parser.anyChar.lookahead

def Parser.notFollowedBy {α : 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} {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.