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

@[implicit_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 }

@[implicit_reducible]

instance Grade.instMax : Max Grade

Equations

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

@[implicit_reducible]

instance Grade.instMonoid : Monoid Grade

Equations

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

@[implicit_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} : 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) (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.consumes α
• sound {n : ℕ} (t : Text n) : Outcome.Sound g.errors (self.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)

@[implicit_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 := ⋯ } }

@[implicit_reducible]

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

Equations

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

@[implicit_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"

@[implicit_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} {n : ℕ} {xc fe fc : Necessity} (t : Text 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)

@[implicit_reducible]

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, 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} {g g' : Grade} (p : Parser ε g α) (onSuccess : {n : ℕ} → Text n → g.errors ≤ possibly → Success n g.consumes α → Outcome ε' n g'.consumes β) (soundSuccess : ∀ {n : ℕ} {t : Text n} (h : g.errors ≤ possibly) (r : Success n g.consumes α), Outcome.Sound g'.errors (onSuccess t h r)) (onError : {n : ℕ} → Text n → possibly ≤ g.errors → Failure n ε → Outcome ε' n g'.consumes β) (soundError : ∀ {n : ℕ} {t : Text 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 : Text n) => (p.run t).handle ⋯ (onSuccess t) (onError t), sound := ⋯ }

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 : ℕ} (x : Text n) => Parser.success { result := a, restSize := n, witness := ⋯ }, sound := ⋯ }

@[implicit_reducible]

instance Parser.instGradedApplicativeGrade {ε : Type} : GradedApplicative (Parser ε)

Equations

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

@[implicit_reducible]

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} [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 : Text n) => ↑(Parser.fixGo✝ h f t), sound := ⋯ }

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, 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} {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 the input left at f.restSize

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 : ℕ} (x : Text 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} {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.runParser {α ε : Type} {g : Grade} (p : Parser ε g α) (s : String) : Except ε α

Run a parser on a String.

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.runParser_sound {α ε : Type} {g : Grade} (p : Parser ε g α) (s : String) : Except.Sound g.errors (p.runParser s)

def Parser.runOption {α ε : Type} {ge gc : Necessity} (p : Parser ε { errors := ge, consumes := gc } α) (s : String) : Option α

Run a parser on a String, discarding the error and returning the value as an Option.

Equations

• p.runOption s = (p.runParser s).toOption

def Parser.anyByte : Parser Error conditional UInt8

Consume a single byte.

Equations

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

def Parser.anyChar : Parser Error conditional Char

Consume a single UTF-8 character.

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 = { run := fun {n : ℕ} (x : Text n) => Parser.success { result := a, restSize := n, witness := ⋯ }, sound := ⋯ }

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.token._proof_1
• 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.test {α ε : 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} {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 = ⋯.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 : ℕ} (t : Text n) => Parser.success (Parser.many.go p t), sound := @Parser.many._proof_2 }

@[irreducible]

def Parser.many.go {α ε : Type} {ge : Necessity} (p : Parser ε { errors := ge, consumes := always } α) {n : ℕ} (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.rawBracket {α : 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 (x : PUnit.{1}) => p >>=ᵍ fun (x : α) => r >>=ᵍ fun (x_1 : PUnit.{1}) => gpure x)

def Parser.bracket {α : 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. Delimiters consume whitespace after them.

Equations

• l.bracket r p = l.lexeme.rawBracket r.lexeme p

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 = Parser.lparen.bracket Parser.rparen p

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 = Parser.lbracket.bracket Parser.rbracket p

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 = Parser.lbrace.bracket Parser.rbrace p

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 : α) => (Parser.sepItem✝ sep p h).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 = (Parser.endItem✝ sep p h).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 = (Parser.endItem✝ sep p h).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.token._proof_2 Parser.token._proof_1

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} [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} {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 := 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.