structure ParseError (σ : Type u_1) (τ : Type u_2) [Parser.Stream σ τ] : Type (max u_2 u_3)

A megaparsec-shape parse error, ε for every Parser_ lexer/parser: the token that failed to match (none at end of input) and every spelling that would have matched there instead. ErrorCombine unions two same-position errors' expected; Parser_.withErrorMessage replaces one outright, only when its own parser failed without consuming (megaparsec's <?>/label) — never appends, which is what made the old chain-of-messages design repeat "expected expression" once per level of parseExpression's recursive descent.

posOverride, unset in the ordinary case, is for a sub-parser running over a stream this error's own Stream.Position σ cannot describe on its own (Annotations.tryParseAnnotations', over the flat concatenated comment text): it resolves its own position eagerly, against comment boundaries only it has in scope, and hands the result over pre-resolved.

• pos : Parser.Stream.Position σ
• unexpected : Option τ
• expected : List String
• posOverride : Option SourceSpan

@[implicit_reducible]

instance instReprParseErrorOfPosition {σ : Type u_1} {τ : Type u_2} [Parser.Stream σ τ] [Repr (Parser.Stream.Position σ)] [Repr τ] : Repr (ParseError σ τ)

Equations

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

@[implicit_reducible]

instance instInhabitedParseErrorOfPosition {σ : Type u_1} {τ : Type u_2} [Parser.Stream σ τ] [Inhabited (Parser.Stream.Position σ)] : Inhabited (ParseError σ τ)

Equations

• instInhabitedParseErrorOfPosition = { default := { pos := Inhabited.default, unexpected := none } }

@[implicit_reducible]

instance instErrorParseError {σ : Type u_1} {τ : Type u_2} [Parser.Stream σ τ] : Parser.Error (ParseError σ τ) σ τ

Equations

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

class ErrorCombine (ε : Type u_1) : Type u_1

How two errors alt/first found at the same position (their job to establish that) combine into the one actually reported.

• combine : ε → ε → ε

@[implicit_reducible]

instance instErrorCombineParseError {σ : Type u_1} {τ : Type u_2} [Parser.Stream σ τ] : ErrorCombine (ParseError σ τ)

Equations

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

@[implicit_reducible]

instance instErrorCombineSimple {σ : Type u_1} {τ : Type u_2} [Parser.Stream σ τ] : ErrorCombine (Parser.Error.Simple σ τ)

Equations

• instErrorCombineSimple = { combine := fun (x e₂ : Parser.Error.Simple σ τ) => e₂ }

def ParseError.expectedHints {σ : Type u_1} {τ : Type u_2} [Parser.Stream σ τ] (e : ParseError σ τ) : List String

Render a ParseError's expected as the Unexpected hint it becomes: nothing when empty; several spellings become "expected one of: …"; one spelling gets "expected " prepended if it reads as a bare noun phrase (token's toString tk, "identifier", …, all lowercase-led), or is shown verbatim if it already reads as a full sentence — either the library's own char/chars/ Unicode.* (withErrorMessage s!"expected {repr tk}", already "expected "-led) or fugue's own direct, capitalized messages ("Operator conflict …", checkConflicts) — the one place these three uses of the same expected : List String field are told apart.

Equations

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

def throwExpected {σ : Type (max u_1 u_2)} {τ : Type u_1} {m : Type (max u_1 u_2) → Type u_3} {α : Type (max u_2 u_1)} [Parser.Stream σ τ] [Monad m] (tok : Option τ) (items : List String) : ParserT (ParseError σ τ) σ τ m α

Fail with tok unexpected and items (bare noun phrases) as the full expected set — a peek-dispatch catch-all's way to name every alternative a match itself cannot state, since Parser.Error.addMessage only ever replaces expected with one string at a time.

Equations

• throwExpected tok items s = pure (Parser.Result.error s { pos := Parser.Stream.getPosition s, unexpected := tok, expected := items })

def ParserT.mapStream {τ₁ τ₂ α : Type u_1} {m : Type u_1 → Type u_2} [Monad m] (f : τ₂ → Option τ₁) (g : τ₁ → τ₂) (p : ParserT (ParseError (TokenStream τ₁) τ₁) (TokenStream τ₁) τ₁ m α) : ParserT (ParseError (TokenStream τ₂) τ₂) (TokenStream τ₂) τ₂ m α

Run a parser written against one token type inside a parser over another. f maps an outer token to an inner one (returning none at the first token the inner parser has no business seeing); g maps back. The inner parser sees the maximal f-mapped prefix of the tokens not yet consumed, indexed from 0, so mapError shifts its reported positions back by the number of tokens already consumed. Only the cursor moves in the outer stream — its token array is untouched, so the outer tokens g would have reconstructed are the originals.

Equations

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

def Parser.Result.isOk {ε σ α : Type u_1} : Parser.Result ε σ α → Bool

Equations

• (Parser.Result.ok a a_1).isOk = true
• (Parser.Result.error a a_1).isOk = false

@[unbox]

structure PositionedSlice : Type

• slice : String.Slice
• position : Cursor

@[implicit_reducible]

instance instInhabitedPositionedSlice : Inhabited PositionedSlice

Equations

• instInhabitedPositionedSlice = { default := instInhabitedPositionedSlice.default }

@[implicit_reducible]

instance instLTPositionedSlice : LT PositionedSlice

Equations

• instLTPositionedSlice = { lt := Function.onFun (fun (x1 x2 : Cursor) => x1 < x2) PositionedSlice.position }

@[implicit_reducible]

instance instLEPositionedSlice : LE PositionedSlice

Equations

• instLEPositionedSlice = { le := Function.onFun (fun (x1 x2 : Cursor) => x1 ≤ x2) PositionedSlice.position }

@[implicit_reducible]

instance instBEqPositionedSlice : BEq PositionedSlice

Equations

• instBEqPositionedSlice = { beq := Function.onFun (fun (x1 x2 : Cursor) => x1 == x2) PositionedSlice.position }

@[implicit_reducible]

instance instDecidableLTPositionedSlice : DecidableLT PositionedSlice

Equations

• instDecidableLTPositionedSlice p₁ p₂ = inferInstance

@[implicit_reducible]

instance instDecidableLEPositionedSlice : DecidableLE PositionedSlice

Equations

• instDecidableLEPositionedSlice p₁ p₂ = inferInstance

@[implicit_reducible]

instance instStreamPositionedSliceChar : Parser.Stream PositionedSlice Char

Equations

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

@[implicit_reducible]

instance instInhabitedPositionPositionedSliceChar : Inhabited (Parser.Stream.Position PositionedSlice)

Equations

• instInhabitedPositionPositionedSliceChar = { default := instInhabitedPositionedSlice.default }

@[implicit_reducible]

instance instBEqPositionPositionedSliceChar : BEq (Parser.Stream.Position PositionedSlice)

Equations

• instBEqPositionPositionedSliceChar = { beq := Function.onFun (fun (x1 x2 : Cursor) => x1 == x2) PositionedSlice.position }

@[implicit_reducible]

instance instLTPositionPositionedSliceChar : LT (Parser.Stream.Position PositionedSlice)

Equations

• instLTPositionPositionedSliceChar = { lt := Function.onFun (fun (x1 x2 : Cursor) => x1 < x2) PositionedSlice.position }

@[implicit_reducible]

instance instLEPositionPositionedSliceChar : LE (Parser.Stream.Position PositionedSlice)

Equations

• instLEPositionPositionedSliceChar = { le := Function.onFun (fun (x1 x2 : Cursor) => x1 ≤ x2) PositionedSlice.position }

@[implicit_reducible]

instance instDecidableLTPositionPositionedSliceChar : DecidableLT (Parser.Stream.Position PositionedSlice)

Equations

• instDecidableLTPositionPositionedSliceChar = instDecidableLTPositionedSlice

@[implicit_reducible]

instance instDecidableLEPositionPositionedSliceChar : DecidableLE (Parser.Stream.Position PositionedSlice)

Equations

• instDecidableLEPositionPositionedSliceChar = instDecidableLEPositionedSlice

@[implicit_reducible]

instance instReprSegmentOfPosition_parser_ {σ : Type u_1} {τ : Type u_2} [Parser.Stream σ τ] [Repr (Parser.Stream.Position σ)] : Repr (Parser.Stream.Segment σ)

Equations

• instReprSegmentOfPosition_parser_ = { reprPrec := instReprSegmentOfPosition_parser_._aux_1 }

structure Located (α : Type u_1) : Type u_1

• segment : Parser.Stream.Segment PositionedSlice
• data : α

@[implicit_reducible]

instance instReprLocatedOfSegmentCharPositionedSlice {α : Type u_1} [Repr (Parser.Stream.Segment PositionedSlice)] [Repr α] : Repr (Located α)

Equations

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

@[implicit_reducible]

instance instInhabitedLocated {α : Type u_1} [Inhabited α] : Inhabited (Located α)

Equations

• instInhabitedLocated = { default := { segment := (Inhabited.default, Inhabited.default), data := Inhabited.default } }

@[unbox]

structure Located' (α : Type u_1) : Type u_1

A piece of data is located if its span in the stream is fully known.

• segment : SourceSpan
• data : α

def instReprLocated'.repr {α✝ : Type u_1} [Repr α✝] : Located' α✝ → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance instReprLocated' {α✝ : Type u_1} [Repr α✝] : Repr (Located' α✝)

Equations

• instReprLocated' = { reprPrec := instReprLocated'.repr }

@[implicit_reducible]

instance instInhabitedLocated' {a✝ : Type u_1} [Inhabited a✝] : Inhabited (Located' a✝)

Equations

• instInhabitedLocated' = { default := instInhabitedLocated'.default }

def instDecidableEqLocated'.decEq {α✝ : Type u_1} [DecidableEq α✝] (x✝ x✝¹ : Located' α✝) : Decidable (x✝ = x✝¹)

Equations

• instDecidableEqLocated'.decEq { segment := a, data := a_1 } { segment := b, data := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[implicit_reducible]

instance instDecidableEqLocated' {α✝ : Type u_1} [DecidableEq α✝] : DecidableEq (Located' α✝)

Equations

• instDecidableEqLocated' = instDecidableEqLocated'.decEq

@[implicit_reducible]

instance instBEqLocated' {α✝ : Type u_1} [BEq α✝] : BEq (Located' α✝)

Equations

• instBEqLocated' = { beq := instBEqLocated'.beq }

def instBEqLocated'.beq {α✝ : Type u_1} [BEq α✝] : Located' α✝ → Located' α✝ → Bool

Equations

• instBEqLocated'.beq { segment := a, data := a_1 } { segment := b, data := b_1 } = (a == b && a_1 == b_1)
• instBEqLocated'.beq x✝¹ x✝ = false

@[implicit_reducible]

instance instToStringLocated' {α : Type u_1} [ToString α] : ToString (Located' α)

Describes the payload, position dropped — a located value reads the same as its data wherever only a human-facing description is wanted (Parser_.token's "expected" hints).

Equations

• instToStringLocated' = { toString := fun (x : Located' α) => toString x.data }

structure Unexpected (α : Type u_1) : Type u_1

• token : Option α
• pos : SourceSpan
• hints : List String

def instReprUnexpected.repr {α✝ : Type u_1} [Repr α✝] : Unexpected α✝ → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance instReprUnexpected {α✝ : Type u_1} [Repr α✝] : Repr (Unexpected α✝)

Equations

• instReprUnexpected = { reprPrec := instReprUnexpected.repr }

@[implicit_reducible]

instance instInhabitedUnexpected {a✝ : Type u_1} : Inhabited (Unexpected a✝)

Equations

• instInhabitedUnexpected = { default := instInhabitedUnexpected.default }

@[implicit_reducible]

instance instToStringUnexpected {α : Type u_1} [ToString α] : ToString (Unexpected α)

Equations

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

@[implicit_reducible]

instance instCompilerDiagnosticUnexpectedStringOfToString {α : Type u_1} [ToString α] : CompilerDiagnostic (Unexpected α) String

Equations

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

inductive ParserWarning : Type

Warnings raised by the parser itself, as opposed to hard errors (Unexpected). Collected out-of-band during parsing (ParserWarningM, below) rather than emitted immediately, and filtered/printed by the compiler driver once parsing returns.

• fairIgnored (pos : SourceSpan) : ParserWarning

  fair process/fair+ was parsed and round-tripped, but is never acted on.

• unusedAnnotation (pos : SourceSpan) : ParserWarning

  A comment parses as a well-formed annotation (@type/@mailbox/@parameter) but sits where no call site consumes it, so it is silently ignored. Distinct from a misplaced annotation (captured, but attached to the wrong role), which is a hard error.

def instReprParserWarning.repr : ParserWarning → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance instReprParserWarning : Repr ParserWarning

Equations

• instReprParserWarning = { reprPrec := instReprParserWarning.repr }

@[implicit_reducible]

instance instInhabitedParserWarning : Inhabited ParserWarning

Equations

• instInhabitedParserWarning = { default := instInhabitedParserWarning.default }

def instBEqParserWarning.beq : ParserWarning → ParserWarning → Bool

Equations

• instBEqParserWarning.beq (ParserWarning.fairIgnored a) (ParserWarning.fairIgnored b) = (a == b)
• instBEqParserWarning.beq (ParserWarning.unusedAnnotation a) (ParserWarning.unusedAnnotation b) = (a == b)
• instBEqParserWarning.beq x✝¹ x✝ = false

@[implicit_reducible]

instance instBEqParserWarning : BEq ParserWarning

Equations

• instBEqParserWarning = { beq := instBEqParserWarning.beq }

def ParserWarning.name : ParserWarning → String

The -W<name>/-Wno-<name> name a given warning is filtered under.

Equations

• (ParserWarning.fairIgnored a).name = "fair"
• (ParserWarning.unusedAnnotation a).name = "unused-annotation"

@[implicit_reducible]

instance instCompilerDiagnosticParserWarningString : CompilerDiagnostic ParserWarning String

Equations

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

@[reducible, inline]

abbrev ParserWarningM (α : Type) : Type

The base monad every parser in Parser_ runs against: Id plus a List ParserWarning accumulator.

Equations

• ParserWarningM = StateT (List ParserWarning) Id

class MonadParserBacktrack (m : Type → Type u_1) : Type (max 1 u_1)

The base-monad state a backtrack has to undo, alongside the stream position. For a parser over ParserWarningM that is the accumulated ParserWarning list: a warning emitted inside an alternative that is then abandoned must not survive. Id has no such state, so its instance is a no-op and the lexer pays nothing.

• Saved : Type

  The part of m's state to snapshot and restore.

• save : m (Saved m)

  Take a snapshot.

• restore : Saved m → m PUnit.{1}

  Restore a snapshot.

@[implicit_reducible]

instance instMonadParserBacktrackId : MonadParserBacktrack Id

Equations

• instMonadParserBacktrackId = { Saved := Unit, save := pure (), restore := fun (x : Unit) => pure () }

@[implicit_reducible]

instance instMonadParserBacktrackParserWarningM : MonadParserBacktrack ParserWarningM

Equations

• instMonadParserBacktrackParserWarningM = { Saved := List ParserWarning, save := get, restore := set }

@[never_extract, macro_inline, specialize #[]]

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

debug name p runs p unchanged. It is the single seam parser tracing is inserted at, and name is the label such a trace would carry; call sites tag themselves once and stay tagged.

Equations

• debug _name p s = do let res ← p.run s pure res

@[specialize #[]]

def eoption {ε σ : Type} {τ : Type u_1} {m : Type → Type u_2} {α : Type} [Parser.Stream σ τ] [Parser.Error ε σ τ] [Monad m] [MonadParserBacktrack m] [BEq (Parser.Stream.Position σ)] (p : ParserT ε σ τ m α) : ParserT ε σ τ m (Option α)

Tries to execute a parser p and returns its result. If p fails without consuming tokens, returns none and rolls back any warnings p emitted before failing; if p fails after consuming input, that failure propagates unchanged.

Equations

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

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

takeMany1 p applies p at least once, collecting the results. Fails if p cannot be applied at least once, or if p fails while consuming input. Warnings emitted by the final, failed (non-consuming) application of p are rolled back; warnings from the applications that succeeded are kept.

Equations

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

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

takeMany p tries to repeatedly apply p until it does not parse, collecting its results. Fails if p fails while consuming input at some point. Warnings from the final, failed (non-consuming) application are rolled back.

Equations

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

Strict (megaparsec) choice combinators

fgdorais/Parser's OrElse, first, sepBy* reset the stream position on every failure, so p <|> q is really try p <|> q and every first alternative is implicitly atomic. These shadow them with megaparsec semantics: a failure that consumed input propagates, and only a failure at the entry position falls through to the next alternative. withBacktracking (a.k.a. try) is the one sanctioned opt-out, and it now also rolls back base-monad warnings.

Kept in namespace Parser_ so a parser namespace opts in with open Parser_ while the lexer, which still wants the library's backtracking first/<|> for its symbol trie, simply does not.

@[specialize #[]]

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

withBacktracking p runs p and, if p fails, rewinds the stream position and any warnings p emitted back to the entry point, so a failed p leaves no trace. Shadows the library's, which rewinds the position only. This is megaparsec try.

Equations

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

@[specialize #[]]

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

tokenMap test reads one token and maps it through test. On none it fails without consuming — the library's tokenCore advances the stream before the test runs, which turns every rejected token into a phantom consumption and makes strict alt/first commit to the wrong branch. Shadows Parser.tokenMap; tokenFilter/token/anyToken sit on top of it.

Equations

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

@[inline]

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

tokenFilter test accepts and returns a token satisfying test, failing without consuming otherwise.

Equations

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

@[inline]

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

token tk accepts and returns tk, failing without consuming otherwise.

Equations

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

@[inline]

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

anyToken consumes and returns one token, failing (without consuming) only at end of input.

Equations

• Parser_.anyToken = Parser_.tokenMap some

@[specialize #[]]

def Parser_.alt {ε σ : Type} {τ : Type u_1} {m : Type → Type u_2} {α : Type} [Parser.Stream σ τ] [Parser.Error ε σ τ] [Monad m] [MonadParserBacktrack m] [BEq (Parser.Stream.Position σ)] [ErrorCombine ε] (p q : ParserT ε σ τ m α) : ParserT ε σ τ m α

alt p q: run p; if it fails without consuming input, roll its warnings back and run q; if p consumed input before failing, that failure propagates and q is never tried. This is megaparsec <|> — wrap p in withBacktracking to get the retry-after-consumption the library's <|> always gives. When q also fails at that same entry position, the two errors combine (ErrorCombine) rather than p's being silently dropped — p <||> q failing means "neither matched", and the report should say what either would have accepted.

Equations

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

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

alt p q: run p; if it fails without consuming input, roll its warnings back and run q; if p consumed input before failing, that failure propagates and q is never tried. This is megaparsec <|> — wrap p in withBacktracking to get the retry-after-consumption the library's <|> always gives. When q also fails at that same entry position, the two errors combine (ErrorCombine) rather than p's being silently dropped — p <||> q failing means "neither matched", and the report should say what either would have accepted.

Equations

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

@[specialize #[]]

def Parser_.first {ε σ : Type} {τ : Type u_1} {α : Type} {m : Type → Type u_2} [Parser.Stream σ τ] [Parser.Error ε σ τ] [Monad m] [MonadParserBacktrack m] [BEq (Parser.Stream.Position σ)] [ErrorCombine ε] (ps : List (ParserT ε σ τ m α)) : ParserT ε σ τ m α

first ps tries the alternatives in order with megaparsec semantics (see alt): the first that consumes input commits, and only same-position failures fall through. On total failure every alternative's expected is merged into the one reported error.

Equations

• Parser_.first [] = fun (s : σ) => pure (Parser.Result.error s (Parser.Error.unexpected (Parser.Stream.getPosition s) none))
• Parser_.first [p] = p
• Parser_.first (p :: ps_2) = (p <||> Parser_.first ps_2)

@[specialize #[]]

def Parser_.withErrorMessage {ε σ : Type u_1} {τ : Type u_2} {m : Type u_1 → Type u_3} {α : Type u_1} [Parser.Stream σ τ] [Parser.Error ε σ τ] [Monad m] [BEq (Parser.Stream.Position σ)] (msg : String) (p : ParserT ε σ τ m α) : ParserT ε σ τ m α

withErrorMessage msg p: if p fails without consuming input, replace whatever it expected with msg (megaparsec's <?>/label); a failure that consumed input propagates untouched. Shadows the library's withErrorMessage, which wraps unconditionally: used directly on a recursive-descent parser like parseExpression, every nested call would re-wrap whatever the previous level had already wrapped, repeating "expected expression" once per level.

Equations

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

@[specialize #[]]

def Parser_.sepAccBy1 {ε σ : Type} {τ : Type u_1} {α β : Type} {m : Type → Type u_2} [Monad m] [Parser.Stream σ τ] [Parser.Error ε σ τ] [MonadParserBacktrack m] [BEq (Parser.Stream.Position σ)] (sep : ParserT ε σ τ m α) (p : ParserT ε σ τ m β) : ParserT ε σ τ m (List β × List α)

A variant of sepBy1 sep p which also returns the collected results of the parser sep.

Equations

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

@[specialize #[]]

def Parser_.sepBy1 {ε σ : Type} {τ : Type u_1} {α β : Type} {m : Type → Type u_2} [Monad m] [Parser.Stream σ τ] [Parser.Error ε σ τ] [MonadParserBacktrack m] [BEq (Parser.Stream.Position σ)] (sep : ParserT ε σ τ m β) (p : ParserT ε σ τ m α) : ParserT ε σ τ m (Array α)

sepBy1 sep p parses one or more p separated by sep, megaparsec-style: sep is a probe (a sep that consumes then fails — e.g. its whitespace/comment skip runs before the token check misses — ends the list cleanly), but once sep is in, a p that fails after consuming propagates its error rather than being silently dropped. No trailing sep is consumed.

Equations

• Parser_.sepBy1 sep p = do let x ← p let xs ← takeMany (Parser_.withBacktracking sep *> p) pure (#[x] ++ xs)

@[specialize #[]]

def Parser_.sepBy {ε σ : Type} {τ : Type u_1} {α β : Type} {m : Type → Type u_2} [Monad m] [Parser.Stream σ τ] [Parser.Error ε σ τ] [MonadParserBacktrack m] [BEq (Parser.Stream.Position σ)] (sep : ParserT ε σ τ m β) (p : ParserT ε σ τ m α) : ParserT ε σ τ m (Array α)

sepBy sep p parses zero or more p separated by sep. Same strictness as sepBy1 once the first p is in.

Equations

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

@[specialize #[]]

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

Alias: under strict semantics sepBy1 already refuses a trailing sep.

Equations

• Parser_.sepNoEndBy1 sep p = Parser_.sepBy1 sep p

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

sepEndBy1 sep p parses one or more p separated by sep with an optional trailing sep — the case where sep doubles as a terminator (PlusCal's statement ;). A sep with a non-p after it ends the list; a p that fails after consuming still propagates its error.

Equations

• Parser_.sepEndBy1 sep p = do let x ← p Parser_.sepEndBy1.loop✝ sep p #[x]