Grip.Byte: point combinators over the graded byte backend

The non-looping combinators. Atomic byte readers (satisfy, byte, takeN), the functor / sequence / choice / monad algebra (map, seqR, seqL, alt, bind, map2), the capture/captureWith/captureWith? slice readers, first-byte dispatch, and the <?> label. The total scanning loops are in Grip.Scan; the graded type, weakening, run?, and fix are in Grip.Graded.

@[inline]

def Grip.GParser.pure {α : Type} (a : α) : GParser 1 α

Consume nothing, never fail.

Equations

• Grip.GParser.pure a = { run := fun (x : ByteArray) (p : Nat) => Grip.ParseResult.ok a p, cwit := ⋯, ewit := ⋯, swit := ⋯, bwit := ⋯, fwit := ⋯ }

@[inline]

def Grip.GParser.fail {α : Type} : GParser empty α

Always fail, recording the current position as the furthest offset reached.

Equations

• Grip.GParser.fail = { run := fun (x : ByteArray) (p : Nat) => Grip.ParseResult.error { pos := p, expected := [] }, cwit := ⋯, ewit := ⋯, swit := ⋯, bwit := ⋯, fwit := ⋯ }

@[inline]

def Grip.GParser.satisfy (f : UInt8 → Bool) : GParser conditional UInt8

Consume one byte satisfying f, or fail without consuming. On failure the furthest offset is the current position p.

Equations

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

@[inline]

def Grip.GParser.byte (c : UInt8) : GParser conditional Unit

Match a specific byte. On failure the furthest offset is the current position p.

Equations

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

@[inline]

def Grip.GParser.capture {g : Grade} {α : Type} (p : GParser g α) : GParser g String

Return the input slice a parser consumed, decoded as text (grade preserved). Lets combinator parsers build real syntax trees (atom names, identifiers, header fields) instead of only structural counts. Invalid UTF-8 in the slice decodes to "".

Equations

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

@[inline]

def Grip.GParser.captureWith {g : Grade} {α β : Type} (f : ByteArray → Nat → Nat → β) (p : GParser g α) : GParser g β

Like capture, but hand the consumed byte range (arr, start, stop) to f instead of decoding it to a String. Lets a value parser fold over the raw input bytes directly, with no extract/fromUTF8?/String round-trip.

Equations

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

@[inline]

def Grip.GParser.captureWith? {g : Grade} {α β : Type} (f : ByteArray → Nat → Nat → Option β) (p : GParser g α) : GParser { errors := possibly, consumes := g.consumes } β

Like captureWith, but f may reject the consumed range by returning none, in which case the parse fails at the entry offset. The result grade keeps p's consumption but sets errors := possibly (the extra failure path), so a conditional p yields a conditional parser. Lets a value decoder veto a syntactically-valid but semantically-out-of-range slice (e.g. a JSON exponent so large that folding it would blow up).

Equations

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

@[inline]

def Grip.GParser.dispatch {α : Type} (select : UInt8 → GParser conditional α) : GParser conditional α

First-byte dispatch: read the current byte and run the parser select chooses for it, without an intermediate allocation. Fails without consuming at end-of-input. This is peek-then-branch fused into one step, so a keyword/number/string/array/object choice costs a single byte read and a jump rather than an alt chain of failed attempts.

Equations

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

@[inline]

def Grip.GParser.map {g : Grade} {α β : Type} (h : α → β) (x : GParser g α) : GParser g β

Map over the result (grade preserved).

Equations

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

@[inline]

def Grip.GParser.seqR {g g' : Grade} {α β : Type} (x : GParser g α) (y : GParser g' β) : GParser (g * g') β

Sequence, keeping the right value; grades multiply. Furthest offset from either x or y propagates on failure.

Equations

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

@[inline]

def Grip.GParser.seqL {g g' : Grade} {α β : Type} (x : GParser g α) (y : GParser g' β) : GParser (g * g') α

Sequence, keeping the left value; grades multiply. Furthest offset propagates on failure.

Equations

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

@[inline]

def Grip.GParser.alt {ge ge' gc gc' : Modality} {α : Type} (x : GParser { errors := ge, consumes := gc } α) (y : GParser { errors := ge', consumes := gc' } α) : GParser { errors := min ge ge', consumes := ge.ite gc' gc } α

Ordered choice; grade follows Grade.choice. On failure, the two errors are merged furthest-wins: if one branch reached a farther offset, that error wins; on a tie the expected-label sets are unioned. This is the megaparsec-style furthest-failure merge.

Equations

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

@[inline]

def Grip.GParser.bind {g g' : Grade} {α β : Type} (x : GParser g α) (f : α → GParser g' β) : GParser (g * g') β

Monadic bind; grades multiply. Furthest offset propagates on failure.

Equations

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

@[inline]

def Grip.GParser.map2 {g g' : Grade} {α β γ : Type} (f : α → β → γ) (x : GParser g α) (y : GParser g' β) : GParser (g * g') γ

Apply a binary function across two parses; grades multiply. Furthest offset propagates on failure.

Equations

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

@[inline]

def Grip.GParser.takeN (n : Nat) : GParser fallible Unit

Consume exactly n bytes if available. On failure the furthest offset is the current position.

Equations

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

@[inline]

def Grip.GParser.label {g : Grade} {α : Type} (name : String) (p : GParser g α) : GParser g α

Replace the expected-label set of p's failure with [name]. Mirrors megaparsec's <?> operator: on success the result is unchanged; on failure the expected field is overwritten so error messages read "expected name" rather than a raw position.

Equations

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

def Grip.«term_<?>_» : Lean.TrailingParserDescr

Attach an expected label to a parser (megaparsec-style <?>). p <?> "name" produces "expected name" on failure at the same position.

Equations

• Grip.«term_<?>_» = Lean.ParserDescr.trailingNode `Grip.«term_<?>_» 10 10 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " <?> ") (Lean.ParserDescr.cat `term 11))