Grip.Combinators: a megaparsec-style vocabulary over the grip core

Ready-made byte parsers (ws, digit, oneOf, ...) and higher-order combinators (sepBy, between, choice, ...), each with a precise grade where the grade is stable, or at the Parser (fallible) face where it depends on runtime data. Batteries-only.

Byte parsers

@[inline]

def Grip.GParser.ch (c : Char) : GParser conditional Unit

Match the byte of an ASCII Char literal: ch '{' matches {.

Equations

• Grip.GParser.ch c = Grip.GParser.byte (Grip.Ascii.code c)

@[inline]

def Grip.GParser.ws : GParser flexible Nat

Skip zero or more whitespace bytes; returns the count.

Equations

• Grip.GParser.ws = Grip.GParser.takeWhile Grip.Ascii.isWs

@[inline]

def Grip.GParser.ws1 : GParser conditional Nat

Skip one or more whitespace bytes; returns the count.

Equations

• Grip.GParser.ws1 = Grip.GParser.takeWhile1 Grip.Ascii.isWs

@[inline]

def Grip.GParser.digit : GParser conditional UInt8

One decimal digit byte.

Equations

• Grip.GParser.digit = Grip.GParser.satisfy Grip.Ascii.isDigit

@[inline]

def Grip.GParser.hexDigit : GParser conditional UInt8

One hex digit byte.

Equations

• Grip.GParser.hexDigit = Grip.GParser.satisfy Grip.Ascii.isHexDigit

@[inline]

def Grip.GParser.letter : GParser conditional UInt8

One ASCII letter byte.

Equations

• Grip.GParser.letter = Grip.GParser.satisfy Grip.Ascii.isAlpha

@[inline]

def Grip.GParser.alphaNum : GParser conditional UInt8

One letter-or-digit byte.

Equations

• Grip.GParser.alphaNum = Grip.GParser.satisfy Grip.Ascii.isAlphaNum

@[inline]

def Grip.GParser.upper : GParser conditional UInt8

One uppercase letter byte.

Equations

• Grip.GParser.upper = Grip.GParser.satisfy Grip.Ascii.isUpper

@[inline]

def Grip.GParser.lower : GParser conditional UInt8

One lowercase letter byte.

Equations

• Grip.GParser.lower = Grip.GParser.satisfy Grip.Ascii.isLower

@[inline]

def Grip.GParser.oneOf (bs : List UInt8) : GParser conditional UInt8

One byte from bs.

Equations

• Grip.GParser.oneOf bs = Grip.GParser.satisfy fun (b : UInt8) => bs.contains b

@[inline]

def Grip.GParser.noneOf (bs : List UInt8) : GParser conditional UInt8

One byte not in bs.

Equations

• Grip.GParser.noneOf bs = Grip.GParser.satisfy fun (b : UInt8) => !bs.contains b

Higher-order combinators

@[inline]

def Grip.GParser.between {α β γ : Type} {g g₁ g₂ : Grade} (open_ : GParser g₁ β) (close : GParser g₂ γ) (p : GParser g α) : GParser (g₁ * (g * g₂)) α

p between open/close; grades multiply (megaparsec order: open, close, body).

Equations

• open_.between close p = open_.seqR (p.seqL close)

@[inline]

def Grip.GParser.sepBy1 {α β : Type} (p : GParser conditional α) (sep : GParser conditional β) : GParser conditional (List α)

One or more p separated by sep; both must always consume.

Equations

• p.sepBy1 sep = Grip.GParser.map2 (fun (x : α) (xs : List α) => x :: xs) p (sep.seqR p).many

@[inline]

def Grip.GParser.sepBy {α β : Type} (p : GParser conditional α) (sep : GParser conditional β) : GParser flexible (List α)

Zero or more p separated by sep.

Equations

• p.sepBy sep = (p.sepBy1 sep).alt (Grip.GParser.pure [])

@[inline]

def Grip.GParser.endBy {α β : Type} (p : GParser conditional α) (sep : GParser conditional β) : GParser flexible (List α)

Zero or more p each followed by sep.

Equations

• p.endBy sep = (p.seqL sep).many

@[inline]

def Grip.GParser.endBy1 {α β : Type} (p : GParser conditional α) (sep : GParser conditional β) : GParser conditional (List α)

One or more p each followed by sep.

Equations

• p.endBy1 sep = Grip.GParser.map2 (fun (x : α) (xs : List α) => x :: xs) (p.seqL sep) (p.endBy sep)

@[inline]

def Grip.GParser.many1 {α : Type} {ge : Modality} (p : GParser { errors := ge, consumes := always } α) : GParser { errors := ge, consumes := always } (List α)

One or more p (always-consuming); the grade is the element parser's.

Equations

• p.many1 = Grip.GParser.gcast ⋯ (Grip.GParser.map2 (fun (x : α) (xs : List α) => x :: xs) p p.many)

@[inline]

def Grip.GParser.skipMany {α : Type} {ge : Modality} (p : GParser { errors := ge, consumes := always } α) : GParser flexible Nat

Skip zero or more p (always-consuming); returns the count skipped.

Equations

• p.skipMany = Grip.GParser.foldMany (fun (n : Nat) (x : α) => n + 1) 0 p

@[inline]

def Grip.GParser.skipMany1 {α : Type} (p : GParser conditional α) : GParser conditional Nat

Skip one or more p (always-consuming); returns the count.

Equations

• p.skipMany1 = Grip.GParser.map2 (fun (x : α) (n : Nat) => n + 1) p p.skipMany

@[inline]

def Grip.GParser.option {α : Type} {g : Grade} (x : α) (p : GParser g α) : GParser (g.choice 1) α

p, or x if p fails. Never fails; consumption follows p's grade.

Equations

• Grip.GParser.option x p = p.alt (Grip.GParser.pure x)

@[inline]

def Grip.GParser.optional {α : Type} {g : Grade} (p : GParser g α) : GParser (g.choice 1) (Option α)

some of p, or none. Never fails; consumption follows p's grade.

Equations

• p.optional = (Grip.GParser.map some p).alt (Grip.GParser.pure none)

@[inline]

def Grip.GParser.notFollowedBy {α : Type} {g : Grade} (p : GParser g α) : GParser lookahead Unit

Succeed (consuming nothing) exactly when p fails.

Equations

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

@[inline]

def Grip.GParser.manyTill {α β : Type} (p : GParser conditional α) (endp : GParser conditional β) : GParser conditional (List α)

Zero or more p until endp succeeds; endp's result is discarded and the p results are collected. Total via fix; both parsers must always consume.

Equations

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

@[inline]

def Grip.GParser.eof : GParser lookahead Unit

End of input: succeed (consuming nothing) exactly when no byte remains. Defined as notFollowedBy of the any-byte parser; used to reject trailing input after a top-level parse. Labelled, since a failure here always means the same thing: something followed what should have been the last byte.

Equations

• Grip.GParser.eof = (fun (p : Grip.GParser lookahead Unit) (name : String) => Grip.GParser.label name p) (Grip.GParser.satisfy fun (x : UInt8) => true).notFollowedBy "end of input"

@[inline]

def Grip.GParser.chooseG {α : Type} {g : Grade} (x : GParser g α) (xs : List (GParser g α)) : GParser g α

Ordered choice over a non-empty list at a single grade g. The grade is preserved via choice_self (choosing between two grade-g parsers is again grade g).

Equations

• x.chooseG xs = List.foldl (fun (acc : Grip.GParser g α) (p : Grip.GParser { errors := g.errors, consumes := g.consumes } α) => Grip.GParser.gcast ⋯ (acc.alt p)) x xs

@[inline]

def Grip.GParser.choice {α : Type} (ps : List (Parser α)) : Parser α

Ordered choice at the ungraded Parser face; empty list fails.

Equations

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

def Grip.GParser.count {α : Type} (n : Nat) (p : Parser α) : Parser (List α)

Exactly n copies of p, at the Parser face (grade is n-dependent).

Equations

• Grip.GParser.count 0 p = Pure.pure []
• Grip.GParser.count n_2.succ p = do let x ← p let xs ← Grip.GParser.count n_2 p Pure.pure (x :: xs)

Notation

The familiar parser-combinator operators, at the graded level (grades multiply/combine as the underlying combinator dictates). scoped, so they activate on open Grip. The Parser (ungraded) face additionally gets the standard Monad/Alternative operators for free; these graded versions coexist with those and are chosen when the operands are graded GParsers. The label operator <?> is global (declared with the core).

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

Functor map: f <$> p.

Equations

• Grip.«term_<$>_» = Lean.ParserDescr.trailingNode `Grip.«term_<$>_» 100 101 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " <$> ") (Lean.ParserDescr.cat `term 100))

def Grip.«term_<$_» : Lean.TrailingParserDescr

Replace the result with a constant: x <$ p.

Equations

• Grip.«term_<$_» = Lean.ParserDescr.trailingNode `Grip.«term_<$_» 100 101 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " <$ ") (Lean.ParserDescr.cat `term 100))

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

Applicative apply: pf <*> px; grades multiply.

Equations

• Grip.«term_<*>_» = Lean.ParserDescr.trailingNode `Grip.«term_<*>_» 60 60 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " <*> ") (Lean.ParserDescr.cat `term 61))

def Grip.«term_*>_» : Lean.TrailingParserDescr

Sequence, keep the right result: p *> q; grades multiply.

Equations

• Grip.«term_*>_» = Lean.ParserDescr.trailingNode `Grip.«term_*>_» 60 60 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " *> ") (Lean.ParserDescr.cat `term 61))

def Grip.«term_<*_» : Lean.TrailingParserDescr

Sequence, keep the left result: p <* q; grades multiply.

Equations

• Grip.«term_<*_» = Lean.ParserDescr.trailingNode `Grip.«term_<*_» 60 60 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " <* ") (Lean.ParserDescr.cat `term 61))

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

Ordered choice: p <|> q; grade follows Grade.choice.

Equations

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

Sanity guards.