Token functions

@[inline]

def ParseIt.tokenMap {ε ι τ α : Type u} {m : Type u → Type v} [Std.Iterator ι Id τ] [Std.Iterators.Productive ι Id] [Pure m] [Error ε ι τ] (f : τ → Option α) : ParserT ε ι τ m α

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

Equations

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

@[inline]

def ParseIt.anyToken {ε ι τ : Type u} {m : Type u → Type v} [Std.Iterator ι Id τ] [Std.Iterators.Productive ι Id] [Pure m] [Error ε ι τ] : ParserT ε ι τ m τ

anyToken consumes and returns one token. Only fails at the end of the input.

Equations

• ParseIt.anyToken = ParseIt.tokenMap some

@[inline]

def ParseIt.tokenFilter {ε ι τ : Type u} {m : Type u → Type v} [Std.Iterator ι Id τ] [Std.Iterators.Productive ι Id] [Pure m] [Error ε ι τ] (test : τ → Bool) : ParserT ε ι τ m τ

tokenFilter test accepts and returns token t if test t = true.

Equations

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

@[inline]

def ParseIt.token {ε ι τ : Type u} {m : Type u → Type v} [Std.Iterator ι Id τ] [Std.Iterators.Productive ι Id] [Pure m] [Error ε ι τ] [BEq τ] (tk : τ) : ParserT ε ι τ m τ

token tk accepts and returns tk.

Equations

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

def ParseIt.tokenArray {ε ι τ : Type u} {m : Type u → Type v} [Std.Iterator ι Id τ] [Std.Iterators.Productive ι Id] [Monad m] [Error ε ι τ] [BEq τ] (tks : Array τ) : ParserT ε ι τ m (Array τ)

tokenArray tks accepts the tokens of tks in order and returns the tokens read. Fails, reporting the first unexpected token, if any token does not match.

Equations

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

def ParseIt.tokenList {ε ι τ : Type u} {m : Type u → Type v} [Std.Iterator ι Id τ] [Std.Iterators.Productive ι Id] [Monad m] [Error ε ι τ] [BEq τ] (tks : List τ) : ParserT ε ι τ m (List τ)

tokenList tks accepts the tokens of tks in order and returns the tokens read. Fails, reporting the first unexpected token, if any token does not match.

Equations

• ParseIt.tokenList tks = Array.toList <$> ParseIt.tokenArray tks.toArray

@[inline]

def ParseIt.endOfInput {ε ι τ : Type u} {m : Type u → Type v} [Std.Iterator ι Id τ] [Std.Iterators.Productive ι Id] [Pure m] [Error ε ι τ] : ParserT ε ι τ m Unitᵤ

endOfInput succeeds only at the end of the input. Consumes no input.

Equations

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

Folding

@[inline]

def ParseIt.foldlP {ε ι τ α β : Type u} {m : Type u → Type v} [Std.Iterator ι Id τ] [Std.Iterators.Finite ι Id] [Monad m] (f : β → α → ParserT ε ι τ m β) (init : β) (p : ParserT ε ι τ m α) : ParserT ε ι τ m β

foldlP f init p folds the parser function f from left to right using init as an initial value and the parser p to generate inputs of type α. Folding ends as soon as the update parser p >>= f y fails, or right after it succeeds without consuming input. This parser never fails.

Equations

• ParseIt.foldlP f init p = Prod.fst <$> ParseIt.efoldlP✝ f init p

@[inline]

def ParseIt.foldlM {ε ι τ α β : Type u} {m : Type u → Type v} [Std.Iterator ι Id τ] [Std.Iterators.Finite ι Id] [Monad m] (f : β → α → m β) (init : β) (p : ParserT ε ι τ m α) : ParserT ε ι τ m β

foldlM f init p folds the monadic function f from left to right using init as an initial value and the parser p to generate inputs of type α. Folding ends as soon as p fails, or right after p succeeds without consuming input. This parser never fails.

Equations

• ParseIt.foldlM f init p = ParseIt.foldlP (fun (y : β) (x : α) => monadLift (f y x)) init p

@[inline]

def ParseIt.foldl {ε ι τ α β : Type u} {m : Type u → Type v} [Std.Iterator ι Id τ] [Std.Iterators.Finite ι Id] [Monad m] (f : β → α → β) (init : β) (p : ParserT ε ι τ m α) : ParserT ε ι τ m β

foldl f init p folds the function f from left to right using init as an initial value and the parser p to generate inputs of type α. Folding ends as soon as p fails, or right after p succeeds without consuming input. This parser never fails.

Equations

• ParseIt.foldl f init p = ParseIt.foldlP (fun (y : β) (x : α) => pure (f y x)) init p

@[irreducible, specialize #[]]

def ParseIt.foldr {ε ι τ α β : Type u} {m : Type u → Type v} [Std.Iterator ι Id τ] [Std.Iterators.Finite ι Id] [Monad m] (f : α → β → β) (p : ParserT ε ι τ m α) (q : ParserT ε ι τ m β) : ParserT ε ι τ m β

foldr f p q parses p repeatedly until it fails and then parses q, folding f from right to left over the results, starting from the result of q. Repetition also ends right after p succeeds without consuming input. If q fails after some occurrences of p then the parse is retried with fewer occurrences.

Equations

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

@[specialize #[]]

def ParseIt.foldlN {ε ι τ α β : Type u} {m : Type u → Type v} [Std.Iterator ι Id τ] [Monad m] (n : Nat) (f : β → α → β) (init : β) (p : ParserT ε ι τ m α) : ParserT ε ι τ m β

foldlN n f init p folds the function f from left to right using init as an initial value over the results of exactly n occurrences of p. Fails if any occurrence of p fails.

Equations

• ParseIt.foldlN 0 f init p = pure init
• ParseIt.foldlN n_2.succ f init p = do let __do_lift ← p ParseIt.foldlN n_2 f (f init __do_lift) p

@[specialize #[]]

def ParseIt.foldlUpTo {ε ι τ α β : Type u} {m : Type u → Type v} [Std.Iterator ι Id τ] [Monad m] (n : Nat) (f : β → α → β) (init : β) (p : ParserT ε ι τ m α) : ParserT ε ι τ m β

foldlUpTo n f init p folds the function f from left to right using init as an initial value over the results of up to n occurrences of p. Folding ends early when p fails. This parser never fails.

Equations

• ParseIt.foldlUpTo 0 f init p = pure init
• ParseIt.foldlUpTo n_2.succ f init p = do let __do_lift ← ParseIt.option? p match __do_lift with | some x => ParseIt.foldlUpTo n_2 f (f init x) p | none => pure init

@[inline]

def ParseIt.foldlUntil {ε ι τ α β γ : Type u} {m : Type u → Type v} [Std.Iterator ι Id τ] [Std.Iterators.Finite ι Id] [Monad m] (f : γ → α → γ) (init : γ) (stop : ParserT ε ι τ m β) (p : ParserT ε ι τ m α) : ParserT ε ι τ m (γ × β)

foldlUntil f init stop p folds the function f from left to right using init as an initial value over the results of zero or more occurrences of p until stop succeeds, and returns the result of folding with the result of stop. If p fails before stop succeeds then the error from p is reported. If p succeeds without consuming input then the error from stop is reported.

Equations

• ParseIt.foldlUntil f init stop p it = ParseIt.foldlUntil.loop✝ f stop p it init it (ParseIt.Progress.refl it)

take family

@[inline]

def ParseIt.take {ε ι τ α : Type u} {m : Type u → Type v} [Std.Iterator ι Id τ] [Monad m] (n : Nat) (p : ParserT ε ι τ m α) : ParserT ε ι τ m (Array α)

take n p parses exactly n occurrences of p and returns the array of results.

Equations

• ParseIt.take n p = ParseIt.foldlN n Array.push (Array.emptyWithCapacity n) p

@[inline]

def ParseIt.takeUpTo {ε ι τ α : Type u} {m : Type u → Type v} [Std.Iterator ι Id τ] [Monad m] (n : Nat) (p : ParserT ε ι τ m α) : ParserT ε ι τ m (Array α)

takeUpTo n p parses up to n occurrences of p and returns the array of results. This parser never fails.

Equations

• ParseIt.takeUpTo n p = ParseIt.foldlUpTo n Array.push #[] p

@[inline]

def ParseIt.takeMany {ε ι τ α : Type u} {m : Type u → Type v} [Std.Iterator ι Id τ] [Std.Iterators.Finite ι Id] [Monad m] (p : ParserT ε ι τ m α) : ParserT ε ι τ m (Array α)

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

Equations

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

@[inline]

def ParseIt.takeMany1 {ε ι τ α : Type u} {m : Type u → Type v} [Std.Iterator ι Id τ] [Std.Iterators.Finite ι Id] [Monad m] (p : ParserT ε ι τ m α) : ParserT ε ι τ m (Array α)

takeMany1 p parses one or more occurrences of p until it fails and returns the array of results.

Equations

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

@[inline]

def ParseIt.takeManyN {ε ι τ α : Type u} {m : Type u → Type v} [Std.Iterator ι Id τ] [Std.Iterators.Finite ι Id] [Monad m] (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 results.

Equations

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

@[inline]

def ParseIt.takeUntil {ε ι τ α β : Type u} {m : Type u → Type v} [Std.Iterator ι Id τ] [Std.Iterators.Finite ι Id] [Monad m] (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 results of p and the result of stop. If p fails before stop succeeds then the error from p is reported. If p succeeds without consuming input then the error from stop is reported.

Equations

• ParseIt.takeUntil stop p = ParseIt.foldlUntil Array.push #[] stop p

drop family

@[inline]

def ParseIt.drop {ε ι τ α : Type u} {m : Type u → Type v} [Std.Iterator ι Id τ] [Monad m] (n : Nat) (p : ParserT ε ι τ m α) : ParserT ε ι τ m Unitᵤ

drop n p parses exactly n occurrences of p, ignoring the results.

Equations

• ParseIt.drop n p = ParseIt.foldlN n (fun (x : ParseIt.Unitᵤ) (x_1 : α) => PUnit.unit) PUnit.unit p

@[inline]

def ParseIt.dropUpTo {ε ι τ α : Type u} {m : Type u → Type v} [Std.Iterator ι Id τ] [Monad m] (n : Nat) (p : ParserT ε ι τ m α) : ParserT ε ι τ m Unitᵤ

dropUpTo n p parses up to n occurrences of p, ignoring the results. Never fails.

Equations

• ParseIt.dropUpTo n p = ParseIt.foldlUpTo n (fun (x : ParseIt.Unitᵤ) (x_1 : α) => PUnit.unit) PUnit.unit p

@[inline]

def ParseIt.dropMany {ε ι τ α : Type u} {m : Type u → Type v} [Std.Iterator ι Id τ] [Std.Iterators.Finite ι Id] [Monad m] (p : ParserT ε ι τ m α) : ParserT ε ι τ m Unitᵤ

dropMany p parses zero or more occurrences of p until it fails, ignoring the results. This parser never fails.

Equations

• ParseIt.dropMany p = ParseIt.foldl (fun (x : ParseIt.Unitᵤ) (x_1 : α) => PUnit.unit) PUnit.unit p

@[inline]

def ParseIt.dropMany1 {ε ι τ α : Type u} {m : Type u → Type v} [Std.Iterator ι Id τ] [Std.Iterators.Finite ι Id] [Monad m] (p : ParserT ε ι τ m α) : ParserT ε ι τ m Unitᵤ

dropMany1 p parses one or more occurrences of p until it fails, ignoring the results.

Equations

• ParseIt.dropMany1 p = p *> ParseIt.dropMany p

@[inline]

def ParseIt.dropManyN {ε ι τ α : Type u} {m : Type u → Type v} [Std.Iterator ι Id τ] [Std.Iterators.Finite ι Id] [Monad m] (n : Nat) (p : ParserT ε ι τ m α) : ParserT ε ι τ m Unitᵤ

dropManyN n p parses n or more occurrences of p until it fails, ignoring the results.

Equations

• ParseIt.dropManyN n p = ParseIt.drop n p *> ParseIt.dropMany p

@[inline]

def ParseIt.dropUntil {ε ι τ α β : Type u} {m : Type u → Type v} [Std.Iterator ι Id τ] [Std.Iterators.Finite ι Id] [Monad m] (stop : ParserT ε ι τ m β) (p : ParserT ε ι τ m α) : ParserT ε ι τ m β

dropUntil stop p parses zero or more occurrences of p until stop succeeds, and returns the result of stop, ignoring the results of p. Errors are reported as for takeUntil.

Equations

• ParseIt.dropUntil stop p = Prod.snd <$> ParseIt.foldlUntil (fun (x : ParseIt.Unitᵤ) (x_1 : α) => PUnit.unit) PUnit.unit stop p

count family

@[inline]

def ParseIt.count {ε ι τ α : Type u} {m : Type u → Type v} [Std.Iterator ι Id τ] [Std.Iterators.Finite ι Id] [Monad m] (p : ParserT ε ι τ m α) : ParserT ε ι τ m Natᵤ

count p parses zero or more occurrences of p until it fails and returns the number of successes. This parser never fails.

Equations

• ParseIt.count p = ParseIt.foldl (fun (n : ParseIt.Natᵤ) (x : α) => { val := ↑n + 1 }) 0 p

@[inline]

def ParseIt.countUpTo {ε ι τ α : Type u} {m : Type u → Type v} [Std.Iterator ι Id τ] [Monad m] (n : Nat) (p : ParserT ε ι τ m α) : ParserT ε ι τ m Natᵤ

countUpTo n p parses up to n occurrences of p and returns the number of successes. This parser never fails.

Equations

• ParseIt.countUpTo n p = ParseIt.foldlUpTo n (fun (n : ParseIt.Natᵤ) (x : α) => { val := ↑n + 1 }) 0 p

@[inline]

def ParseIt.countUntil {ε ι τ α β : Type u} {m : Type u → Type v} [Std.Iterator ι Id τ] [Std.Iterators.Finite ι Id] [Monad m] (stop : ParserT ε ι τ m β) (p : ParserT ε ι τ m α) : ParserT ε ι τ m (Natᵤ × β)

countUntil stop p parses zero or more occurrences of p until stop succeeds, and returns the number of occurrences of p and the result of stop. Errors are reported as for takeUntil.

Equations

• ParseIt.countUntil stop p = ParseIt.foldlUntil (fun (n : ParseIt.Natᵤ) (x : α) => { val := ↑n + 1 }) 0 stop p

endBy family

@[inline]

def ParseIt.endBy {ε ι τ α β : Type u} {m : Type u → Type v} [Std.Iterator ι Id τ] [Std.Iterators.Finite ι Id] [Monad m] (sep : ParserT ε ι τ m β) (p : ParserT ε ι τ m α) (strict : Bool := false) : ParserT ε ι τ m (Array α)

endBy sep p parses zero or more occurrences of p, each followed by sep, and returns the array of results of 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 fails if there is a final occurrence of p without a trailing sep. Then the error of sep is reported.

Equations

• ParseIt.endBy sep p strict = ParseIt.endByCore✝ sep p #[] strict

@[inline]

def ParseIt.endBy1 {ε ι τ α β : Type u} {m : Type u → Type v} [Std.Iterator ι Id τ] [Std.Iterators.Finite ι Id] [Monad m] (sep : ParserT ε ι τ m β) (p : ParserT ε ι τ m α) (strict : Bool := false) : ParserT ε ι τ m (Array α)

endBy1 sep p parses one or more occurrences of p, each followed by sep, and returns the array of results of p. The optional strict parameter controls error reporting after the first occurrence, as for endBy.

Equations

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

sepBy family

@[inline]

def ParseIt.sepBy {ε ι τ α β : Type u} {m : Type u → Type v} [Std.Iterator ι Id τ] [Std.Iterators.Finite ι Id] [Monad m] (sep : ParserT ε ι τ m β) (p : ParserT ε ι τ m α) (strict : Bool := false) : ParserT ε ι τ m (Array α)

sepBy sep p parses zero or more occurrences of p separated by sep, and returns the array of results of 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 fails if there is a final sep without a following p. Then the error of p is reported.

Equations

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

@[inline]

def ParseIt.sepBy1 {ε ι τ α β : Type u} {m : Type u → Type v} [Std.Iterator ι Id τ] [Std.Iterators.Finite ι Id] [Monad m] (sep : ParserT ε ι τ m β) (p : ParserT ε ι τ m α) (strict : Bool := false) : ParserT ε ι τ m (Array α)

sepBy1 sep p parses one or more occurrences of p separated by sep, and returns the array of results of p. The optional strict parameter controls error reporting after the first occurrence, as for sepBy.

Equations

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

@[inline]

def ParseIt.sepNoEndBy {ε ι τ α β : Type u} {m : Type u → Type v} [Std.Iterator ι Id τ] [Std.Iterators.Finite ι Id] [Monad m] (sep : ParserT ε ι τ m β) (p : ParserT ε ι τ m α) : ParserT ε ι τ m (Array α)

sepNoEndBy sep p parses zero or more occurrences of p separated by sep without a trailing sep, and returns the array of results of p.

Equations

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

@[inline]

def ParseIt.sepNoEndBy1 {ε ι τ α β : Type u} {m : Type u → Type v} [Std.Iterator ι Id τ] [Std.Iterators.Finite ι Id] [Monad m] (sep : ParserT ε ι τ m β) (p : ParserT ε ι τ m α) : ParserT ε ι τ m (Array α)

sepNoEndBy1 sep p parses one or more occurrences of p separated by sep without a trailing sep, and returns the array of results of p.

Equations

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

@[inline]

def ParseIt.sepEndBy {ε ι τ α β : Type u} {m : Type u → Type v} [Std.Iterator ι Id τ] [Std.Iterators.Finite ι Id] [Monad m] (sep : ParserT ε ι τ m β) (p : ParserT ε ι τ m α) : ParserT ε ι τ m (Array α)

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

Equations

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

@[inline]

def ParseIt.sepEndBy1 {ε ι τ α β : Type u} {m : Type u → Type v} [Std.Iterator ι Id τ] [Std.Iterators.Finite ι Id] [Monad m] (sep : ParserT ε ι τ m β) (p : ParserT ε ι τ m α) : ParserT ε ι τ m (Array α)

sepEndBy1 sep p parses one or more occurrences of p separated by sep with an optional trailing sep, and returns the array of results of p.

Equations

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