Token Functions

@[inline]

def Parser.tokenCore {σ : Type (max u_1 u_2)} {τ : Type u_1} {ε : Type (max u_1 u_2)} {m : Type (max u_1 u_2) → Type u_3} [Parser.Stream σ τ] [Parser.Error ε σ τ] [Monad m] (next? : σ → Option (τ × σ)) : ParserT ε σ τ m (ULift τ)

tokenCore next? reads a token from the stream using next?.

This is a low-level parser to customize how the parser stream is used.

Equations

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

@[specialize #[]]

def Parser.tokenMap {σ : Type (max u_1 u_2)} {τ : Type u_2} {ε : Type (max u_1 u_2)} {m : Type (max u_1 u_2) → Type u_3} [Parser.Stream σ τ] [Parser.Error ε σ τ] [Monad m] {α : Type (max u_1 u_2)} (test : τ → Option α) : ParserT ε σ τ m α

tokenMap test accepts token t with result x if test t = some x, otherise fails reporting the unexpected token.

Equations

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

@[inline]

def Parser.anyToken {σ τ ε : Type (max u_1 u_2)} {m : Type (max u_1 u_2) → Type u_3} [Parser.Stream σ τ] [Parser.Error ε σ τ] [Monad m] : ParserT ε σ τ m τ

anyToken consumes and returns one token from the stream. Only fails on end of stream.

Equations

• Parser.anyToken = Parser.tokenMap some

@[inline]

def Parser.tokenFilter {σ τ ε : Type (max u_1 u_2)} {m : Type (max u_1 u_2) → Type u_3} [Parser.Stream σ τ] [Parser.Error ε σ τ] [Monad m] (test : τ → Bool) : ParserT ε σ τ m τ

tokenFilter test accepts and returns token t if test t = true, otherwise fails reporting unexpected token.

Equations

• Parser.tokenFilter test = Parser.tokenMap fun (c : τ) => if test c = true then some c else none

@[inline]

def Parser.token {σ τ ε : Type (max u_1 u_2)} {m : Type (max u_1 u_2) → Type u_3} [Parser.Stream σ τ] [Parser.Error ε σ τ] [Monad m] [BEq τ] (tk : τ) : ParserT ε σ τ m τ

token tk accepts and returns tk, otherwise fails otherwise fails reporting unexpected token.

Equations

• Parser.token tk = Parser.tokenFilter fun (x : τ) => x == tk

def Parser.tokenArray {σ τ ε : Type (max u_1 u_2)} {m : Type (max u_1 u_2) → Type u_3} [Parser.Stream σ τ] [Parser.Error ε σ τ] [Monad m] [BEq τ] (tks : Array τ) : ParserT ε σ τ m (Array τ)

tokenArray tks accepts and returns tokens from tks in order, otherwise fails reporting the first unexpected token.

Equations

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

def Parser.tokenList {σ τ ε : Type (max u_1 u_2)} {m : Type (max u_1 u_2) → Type u_3} [Parser.Stream σ τ] [Parser.Error ε σ τ] [Monad m] [BEq τ] (tks : List τ) : ParserT ε σ τ m (List τ)

tokenArray tks accepts and returns tokens from tks in order, otherwise fails reporting the first unexpected token.

Equations

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

Basic Combinators

def Parser.lookAhead {σ : Type u_1} {τ : Type u_2} {ε : Type u_1} {m : Type u_1 → Type u_3} [Parser.Stream σ τ] [Parser.Error ε σ τ] [Monad m] {α : Type u_1} (p : ParserT ε σ τ m α) : ParserT ε σ τ m α

lookAhead p tries to parses p without consuming any input. If p fails then the stream is backtracked with the same error.

Equations

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

@[reducible, inline]

abbrev Parser.peek {σ τ ε : Type (max u_1 u_2)} {m : Type (max u_1 u_2) → Type u_3} [Parser.Stream σ τ] [Parser.Error ε σ τ] [Monad m] : ParserT ε σ τ m τ

peek returns the next token, without consuming any input. Only fails on end of stream.

Equations

• Parser.peek = Parser.lookAhead Parser.anyToken

@[inline]

def Parser.notFollowedBy {σ : Type u_1} {τ : Type u_2} {ε : Type u_1} {m : Type u_1 → Type u_3} [Parser.Stream σ τ] [Parser.Error ε σ τ] [Monad m] {α : Type u_1} (p : ParserT ε σ τ m α) : ParserT ε σ τ m PUnit

notFollowedBy p succeeds only if p fails. Consumes no input regardless of outcome.

Equations

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

@[reducible, inline]

abbrev Parser.endOfInput {σ τ ε : Type (max u_1 u_2)} {m : Type (max u_1 u_2) → Type u_3} [Parser.Stream σ τ] [Parser.Error ε σ τ] [Monad m] : ParserT ε σ τ m PUnit

endOfInput succeeds only on end of stream. Consumes no input.

Equations

• Parser.endOfInput = Parser.notFollowedBy Parser.anyToken

@[inline]

def Parser.test {σ : Type} {τ : Type u_1} {ε : Type} {m : Type → Type u_2} [Parser.Stream σ τ] [Parser.Error ε σ τ] [Monad m] {α : Type} (p : ParserT ε σ τ m α) : ParserT ε σ τ m Bool

test p returns true if p succeeds and false otherwise. This parser never fails.

Equations

• Parser.test p = Parser.optionD (p *> pure true) false

foldr

@[inline]

partial def Parser.foldr {σ : Type u_1} {τ : Type u_2} {ε : Type u_1} {m : Type u_1 → Type u_3} [Parser.Stream σ τ] [Parser.Error ε σ τ] [Monad m] {α β : Type u_1} (f : α → β → β) (p : ParserT ε σ τ m α) (q : ParserT ε σ τ m β) : ParserT ε σ τ m β

foldr f p q

take family

@[inline]

def Parser.take {σ : Type u_1} {τ : Type u_2} {ε : Type u_1} {m : Type u_1 → Type u_3} [Parser.Stream σ τ] [Parser.Error ε σ τ] [Monad m] {α : Type u_1} (n : Nat) (p : ParserT ε σ τ m α) : ParserT ε σ τ m (Array α)

take n p parses exactly n occurrences of p, and returns an array of the returned values of p.

Equations

• Parser.take n p = Parser.withBacktracking (Parser.take.rest p n #[])

def Parser.take.rest {σ : Type u_1} {τ : Type u_2} {ε : Type u_1} {m : Type u_1 → Type u_3} [Parser.Stream σ τ] [Parser.Error ε σ τ] [Monad m] {α : Type u_1} (p : ParserT ε σ τ m α) : Nat → Array α → ParserT ε σ τ m (Array α)

Equations

• Parser.take.rest p 0 x✝ = pure x✝
• Parser.take.rest p n.succ x✝ = do let __do_lift ← p Parser.take.rest p n (x✝.push __do_lift)

@[inline]

def Parser.takeUpTo {σ : Type u_1} {τ : Type u_2} {ε : Type u_1} {m : Type u_1 → Type u_3} [Parser.Stream σ τ] [Parser.Error ε σ τ] [Monad m] {α : Type u_1} (n : Nat) (p : ParserT ε σ τ m α) : ParserT ε σ τ m (Array α)

takeUpTo n p parses up to n occurrences of p, and returns an array of the returned values of p. This parser never fails.

Equations

• Parser.takeUpTo n p = Parser.takeUpTo.rest p n #[]

def Parser.takeUpTo.rest {σ : Type u_1} {τ : Type u_2} {ε : Type u_1} {m : Type u_1 → Type u_3} [Parser.Stream σ τ] [Parser.Error ε σ τ] [Monad m] {α : Type u_1} (p : ParserT ε σ τ m α) : Nat → Array α → ParserT ε σ τ m (Array α)

Equations

• Parser.takeUpTo.rest p 0 x✝ = pure x✝
• Parser.takeUpTo.rest p n.succ x✝ = do let __do_lift ← Parser.option? p match __do_lift with | some x => Parser.takeUpTo.rest p n (x✝.push x) | none => pure x✝

@[inline]

def Parser.takeMany {σ : Type u_1} {τ : Type u_2} {ε : Type u_1} {m : Type u_1 → Type u_3} [Parser.Stream σ τ] [Parser.Error ε σ τ] [Monad m] {α : Type u_1} (p : ParserT ε σ τ m α) : ParserT ε σ τ m (Array α)

takeMany p parses zero or more occurrences of p until it fails, and returns the array of returned values of p. This parser never fails.

Equations

• Parser.takeMany p = Parser.foldl Array.push #[] p

@[inline]

def Parser.takeMany1 {σ : Type u_1} {τ : Type u_2} {ε : Type u_1} {m : Type u_1 → Type u_3} [Parser.Stream σ τ] [Parser.Error ε σ τ] [Monad m] {α : Type u_1} (p : ParserT ε σ τ m α) : ParserT ε σ τ m (Array α)

takeMany1 p parses one or more occurrences of p until it fails, and returns the array of returned values of p. Consumes no input on error.

Equations

• Parser.takeMany1 p = Parser.withBacktracking do let __do_lift ← p Parser.foldl Array.push #[__do_lift] p

@[inline]

def Parser.takeManyN {σ : Type u_1} {τ : Type u_2} {ε : Type u_1} {m : Type u_1 → Type u_3} [Parser.Stream σ τ] [Parser.Error ε σ τ] [Monad m] {α : Type u_1} (n : Nat) (p : ParserT ε σ τ m α) : ParserT ε σ τ m (Array α)

takeManyN n p parses n or more occurrences of p until it fails, and returns the array of returned values of p. Consumes no input on error.

Equations

• Parser.takeManyN n p = Parser.withBacktracking do let __do_lift ← Parser.take n p Parser.foldl Array.push __do_lift p

def Parser.takeUntil {σ : Type (max u_1 u_2)} {τ : Type u_3} {ε : Type (max u_1 u_2)} {m : Type (max u_1 u_2) → Type u_4} [Parser.Stream σ τ] [Parser.Error ε σ τ] [Monad m] {β α : Type (max u_1 u_2)} (stop : ParserT ε σ τ m β) (p : ParserT ε σ τ m α) : ParserT ε σ τ m (Array α × β)

takeUntil stop p parses zero or more occurrences of p until stop succeeds, and returns the array of returned values of p and the output of stop. If p fails before stop is encountered, the error from p is reported and no input is consumed.

Equations

• Parser.takeUntil stop p = Parser.withBacktracking (Parser.takeUntil.rest stop p #[])

partial def Parser.takeUntil.rest {σ : Type (max u_1 u_2)} {τ : Type u_3} {ε : Type (max u_1 u_2)} {m : Type (max u_1 u_2) → Type u_4} [Parser.Stream σ τ] [Parser.Error ε σ τ] [Monad m] {β α : Type (max u_1 u_2)} (stop : ParserT ε σ τ m β) (p : ParserT ε σ τ m α) [Inhabited (ParserT ε σ τ m (Array α × β))] (acc : Array α) : ParserT ε σ τ m (Array α × β)

drop family

@[inline]

def Parser.drop {σ : Type u_1} {τ : Type u_2} {ε : Type u_1} {m : Type u_1 → Type u_3} [Parser.Stream σ τ] [Parser.Error ε σ τ] [Monad m] {α : Type u_1} (n : Nat) (p : ParserT ε σ τ m α) : ParserT ε σ τ m PUnit

drop n p parses exactly n occurrences of p (without backtracking), ignoring all outputs.

Equations

• Parser.drop 0 p = pure PUnit.unit
• Parser.drop n_2.succ p = p *> Parser.drop n_2 p

@[inline]

def Parser.dropUpTo {σ : Type u_1} {τ : Type u_2} {ε : Type u_1} {m : Type u_1 → Type u_3} [Parser.Stream σ τ] [Parser.Error ε σ τ] [Monad m] {α : Type u_1} (n : Nat) (p : ParserT ε σ τ m α) : ParserT ε σ τ m PUnit

dropUpTo n p parses up to n occurrences of p (with backtracking) ignoring all outputs. This parser never fails.

Equations

• Parser.dropUpTo 0 p = pure PUnit.unit
• Parser.dropUpTo n_2.succ p = do let __do_lift ← Parser.option? p match __do_lift with | some val => Parser.drop n_2 p | none => pure PUnit.unit

@[inline]

def Parser.dropMany {σ : Type u_1} {τ : Type u_2} {ε : Type u_1} {m : Type u_1 → Type u_3} [Parser.Stream σ τ] [Parser.Error ε σ τ] [Monad m] {α : Type u_1} (p : ParserT ε σ τ m α) : ParserT ε σ τ m PUnit

dropMany p parses zero or more occurrences of p (with backtracking) until it fails, ignoring all outputs.

Equations

• Parser.dropMany p = Parser.foldl (Function.const α) PUnit.unit p

@[inline]

def Parser.dropMany1 {σ : Type} {τ : Type u_1} {ε : Type} {m : Type → Type u_2} [Parser.Stream σ τ] [Parser.Error ε σ τ] [Monad m] {α : Type} (p : ParserT ε σ τ m α) : ParserT ε σ τ m PUnit

dropMany1 p parses one or more occurrences of p (with backtracking) until it fails, ignoring all outputs.

Equations

• Parser.dropMany1 p = Parser.withBacktracking p *> Parser.foldl (Function.const α) () p

@[inline]

def Parser.dropManyN {σ : Type} {τ : Type u_1} {ε : Type} {m : Type → Type u_2} [Parser.Stream σ τ] [Parser.Error ε σ τ] [Monad m] {α : Type} (n : Nat) (p : ParserT ε σ τ m α) : ParserT ε σ τ m PUnit

dropManyN n p parses n or more occurrences of p until it fails, ignoring all outputs.

Equations

• Parser.dropManyN n p = Parser.withBacktracking (Parser.drop n p *> Parser.foldl (Function.const α) () p)

def Parser.dropUntil {σ : Type u_1} {τ : Type u_2} {ε : Type u_1} {m : Type u_1 → Type u_3} [Parser.Stream σ τ] [Parser.Error ε σ τ] [Monad m] {β α : Type u_1} (stop : ParserT ε σ τ m β) (p : ParserT ε σ τ m α) : ParserT ε σ τ m β

dropUntil stop p runs p until stop succeeds, returns the output of stop ignoring all outputs from p. If p fails before encountering stop then the error from p is reported and no input is consumed.

Equations

• Parser.dropUntil stop p = Parser.withBacktracking (Parser.dropUntil.loop stop p)

partial def Parser.dropUntil.loop {σ : Type u_1} {τ : Type u_2} {ε : Type u_1} {m : Type u_1 → Type u_3} [Parser.Stream σ τ] [Parser.Error ε σ τ] [Monad m] {β α : Type u_1} (stop : ParserT ε σ τ m β) (p : ParserT ε σ τ m α) : ParserT ε σ τ m β

count family

@[inline]

def Parser.count {σ : Type} {τ : Type u_1} {ε : Type} {m : Type → Type u_2} [Parser.Stream σ τ] [Parser.Error ε σ τ] [Monad m] {α : Type} (p : ParserT ε σ τ m α) : ParserT ε σ τ m Nat

count p parses occurrences of p (with backtracking) until it fails and returns the count of successes.

Equations

• Parser.count p = Parser.foldl (fun (n : Nat) (x : α) => n + 1) 0 p

@[inline]

def Parser.countUpTo {σ : Type} {τ : Type u_1} {ε : Type} {m : Type → Type u_2} [Parser.Stream σ τ] [Parser.Error ε σ τ] [Monad m] {α : Type} (n : Nat) (p : ParserT ε σ τ m α) : ParserT ε σ τ m Nat

countUpTo n p parses up to n occurrences of p until it fails, and returns the count of successes. This parser never fails.

Equations

• Parser.countUpTo n p = Parser.countUpTo.loop p n 0

def Parser.countUpTo.loop {σ : Type} {τ : Type u_1} {ε : Type} {m : Type → Type u_2} [Parser.Stream σ τ] [Parser.Error ε σ τ] [Monad m] {α : Type} (p : ParserT ε σ τ m α) : Nat → Nat → ParserT ε σ τ m Nat

Equations

• Parser.countUpTo.loop p 0 x✝ = pure x✝
• Parser.countUpTo.loop p n.succ x✝ = do let __do_lift ← Parser.option? p match __do_lift with | some val => Parser.countUpTo.loop p n (x✝ + 1) | none => pure x✝

def Parser.countUntil {σ : Type u_1} {τ : Type u_2} {ε : Type u_1} {m : Type u_1 → Type u_3} [Parser.Stream σ τ] [Parser.Error ε σ τ] [Monad m] {β α : Type u_1} (stop : ParserT ε σ τ m β) (p : ParserT ε σ τ m α) : ParserT ε σ τ m (Nat × β)

countUntil stop p counts zero or more occurrences of p until stop succeeds, and returns the count of successes and the output of stop. If p fails before encountering stop then the error from p is reported and no input is consumed.

Equations

• Parser.countUntil stop p = Parser.withBacktracking (Parser.countUntil.loop stop p 0)

partial def Parser.countUntil.loop {σ : Type u_1} {τ : Type u_2} {ε : Type u_1} {m : Type u_1 → Type u_3} [Parser.Stream σ τ] [Parser.Error ε σ τ] [Monad m] {β α : Type u_1} (stop : ParserT ε σ τ m β) (p : ParserT ε σ τ m α) [Inhabited (ParserT ε σ τ m (Nat × β))] (ct : Nat) : ParserT ε σ τ m (Nat × β)

endBy family

@[inline]

def Parser.endBy {σ : Type u_1} {τ : Type u_2} {ε : Type u_1} {m : Type u_1 → Type u_3} [Parser.Stream σ τ] [Parser.Error ε σ τ] [Monad m] {β α : Type u_1} (sep : ParserT ε σ τ m β) (p : ParserT ε σ τ m α) (strict : Bool := false) : ParserT ε σ τ m (Array α)

endBy p sep parses zero or more occurrences of p, separated and ended by sep, returns the array of values returned by p.

The optional strict parameter controls error reporting:

• If strict = false then this parser never fails and returns the longest possible array.
• If strict = true then this parser returns the longest possible array but fails if there is a final occurrence of p without a trailing sep. Then the error of sep is reported.

No input is consumed on error.

Equations

• Parser.endBy sep p strict = Parser.withBacktracking (Parser.endByCore✝ sep p #[] strict)

@[inline]

def Parser.endBy1 {σ : Type u_1} {τ : Type u_2} {ε : Type u_1} {m : Type u_1 → Type u_3} [Parser.Stream σ τ] [Parser.Error ε σ τ] [Monad m] {β α : Type u_1} (sep : ParserT ε σ τ m β) (p : ParserT ε σ τ m α) (strict : Bool := decide False) : ParserT ε σ τ m (Array α)

endBy1 p sep parses one or more occurrences of p, separated and ended by sep, returns the array of values returned by p.

The optional strict parameter controls error reporting after parsing the initial p and sep:

• If strict = false then this parser never fails and returns the longest possible array.
• If strict = true then this parser returns the longest possible array but fails if there is a final occurrence of p without a trailing sep. Then the error of sep is reported.

No input is consumed on error.

Equations

• Parser.endBy1 sep p strict = Parser.withBacktracking do let __do_lift ← p <* sep Parser.endByCore✝ sep p #[__do_lift] strict

sepBy family

@[inline]

def Parser.sepBy {σ : Type u_1} {τ : Type u_2} {ε : Type u_1} {m : Type u_1 → Type u_3} [Parser.Stream σ τ] [Parser.Error ε σ τ] [Monad m] {β α : Type u_1} (sep : ParserT ε σ τ m β) (p : ParserT ε σ τ m α) (strict : Bool := false) : ParserT ε σ τ m (Array α)

sepBy p sep parses zero or more occurrences of p, separated by sep, returns the array of values returned by p.

The optional strict parameter controls error reporting:

• If strict = false then this parser never fails and returns the longest possible array.
• If strict = true then this parser returns the longest possible array but fails if there is a final occurrence of sep without a trailing p. Then the error of p is reported.

No input is consumed on error.

Equations

• Parser.sepBy sep p strict = Parser.withBacktracking do let __do_lift ← Parser.option? p match __do_lift with | some x => Parser.sepByCore✝ sep p #[x] strict | none => pure #[]

@[inline]

def Parser.sepBy1 {σ : Type u_1} {τ : Type u_2} {ε : Type u_1} {m : Type u_1 → Type u_3} [Parser.Stream σ τ] [Parser.Error ε σ τ] [Monad m] {β α : Type u_1} (sep : ParserT ε σ τ m β) (p : ParserT ε σ τ m α) (strict : Bool := false) : ParserT ε σ τ m (Array α)

sepBy1 p sep parses one or more occurrences of p, separated by sep, returns the array of values returned by p.

The optional strict parameter controls error reporting after parsing the initial p:

• If strict = false then this parser never fails and returns the longest possible array.
• If strict = true then this parser returns the longest possible array but fails if there is a final occurrence of sep without a trailing p. Then the error of p is reported.

No input is consumed on error.

Equations

• Parser.sepBy1 sep p strict = Parser.withBacktracking do let __do_lift ← p Parser.sepByCore✝ sep p #[__do_lift] strict

@[inline]

def Parser.sepNoEndBy {σ : Type u_1} {τ : Type u_2} {ε : Type u_1} {m : Type u_1 → Type u_3} [Parser.Stream σ τ] [Parser.Error ε σ τ] [Monad m] {β α : Type u_1} (sep : ParserT ε σ τ m β) (p : ParserT ε σ τ m α) : ParserT ε σ τ m (Array α)

sepNoEndBy p sep parses zero or more occurrences of p, separated sep but without a trailing sep, returns the array of values returned by p.

Equations

• Parser.sepNoEndBy sep p = Parser.sepBy sep p true

@[inline]

def Parser.sepNoEndBy1 {σ : Type u_1} {τ : Type u_2} {ε : Type u_1} {m : Type u_1 → Type u_3} [Parser.Stream σ τ] [Parser.Error ε σ τ] [Monad m] {β α : Type u_1} (sep : ParserT ε σ τ m β) (p : ParserT ε σ τ m α) : ParserT ε σ τ m (Array α)

sepNoEndBy1 p sep parses one or more occurrences of p, separated sep but without a trailing sep, returns the array of values returned by p.

Equations

• Parser.sepNoEndBy1 sep p = Parser.sepBy1 sep p true

@[inline]

def Parser.sepEndBy {σ : Type u_1} {τ : Type u_2} {ε : Type u_1} {m : Type u_1 → Type u_3} [Parser.Stream σ τ] [Parser.Error ε σ τ] [Monad m] {β α : Type u_1} (sep : ParserT ε σ τ m β) (p : ParserT ε σ τ m α) : ParserT ε σ τ m (Array α)

sepEndBy p sep parses zero or more occurrences of p, separated by sep with an optional trailing sep, returns the array of values returned by p. This parser never fails.

Equations

• Parser.sepEndBy sep p = Parser.sepBy sep p <* Parser.optional sep

@[inline]

def Parser.sepEndBy1 {σ : Type u_1} {τ : Type u_2} {ε : Type u_1} {m : Type u_1 → Type u_3} [Parser.Stream σ τ] [Parser.Error ε σ τ] [Monad m] {β α : Type u_1} (sep : ParserT ε σ τ m β) (p : ParserT ε σ τ m α) : ParserT ε σ τ m (Array α)

sepEndBy1 p sep parses one or more occurrences of p, separated by sep with an optional trailing sep, returns the array of values returned by p. This parser never fails.

Equations

• Parser.sepEndBy1 sep p = Parser.sepBy1 sep p <* Parser.optional sep