Text cursor primitives for verification parsers

ODE and PINN certificates both contain small mathematical expression languages. This module owns their shared byte-position cursor, fuel-bounded scanning, and decimal literal parsing. Grammar and AST decisions remain in the respective verifier modules.

structure NN.Verification.Util.TextCursor.Cursor : Type

A source string paired with the current raw byte position.

• source : String

  Source text being scanned.

• position : String.Pos.Raw

  Current raw byte position in source.

@[inline]

def NN.Verification.Util.TextCursor.peek (cursor : Cursor) : Option Char

Inspect the current character without advancing the cursor.

@[inline]

def NN.Verification.Util.TextCursor.bump (cursor : Cursor) : Cursor

Advance by one character, preserving the source text.

@[inline]

def NN.Verification.Util.TextCursor.remainingFuel (cursor : Cursor) : ℕ

Remaining bytes plus one, suitable as a budget for a single linear scan.

@[inline]

def NN.Verification.Util.TextCursor.atEnd (cursor : Cursor) : Bool

Whether the cursor has reached or passed the source's raw end position.

def NN.Verification.Util.TextCursor.isWhitespace (char : Char) : Bool

ASCII whitespace accepted by the verification expression languages.

def NN.Verification.Util.TextCursor.skipWhileFuel (predicate : Char → Bool) : ℕ → Cursor → Cursor

Skip characters satisfying predicate, bounded by explicit recursion fuel.

def NN.Verification.Util.TextCursor.takeWhileFuel (fuel : ℕ) (predicate : Char → Bool) (accumulator : String) (cursor : Cursor) : String × Cursor

Consume characters satisfying predicate, bounded by explicit recursion fuel.

def NN.Verification.Util.TextCursor.decimalNat (text : String) : Except String ℕ

Convert a nonempty string of decimal digits to a natural number.

def NN.Verification.Util.TextCursor.parseNat (fuel : ℕ) (cursor : Cursor) : Except String (ℕ × Cursor)

Parse a whitespace-prefixed unsigned decimal natural using a caller-supplied scan budget.

def NN.Verification.Util.TextCursor.parseFloat (fuel : ℕ) (cursor : Cursor) : Except String (Float × Cursor)

Parse a signed decimal Float without scientific notation.