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) : Nat

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) : Nat → Cursor → Cursor

Skip characters satisfying predicate, bounded by explicit recursion fuel.

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

Consume characters satisfying predicate, bounded by explicit recursion fuel.

def NN.Verification.Util.TextCursor.digitsToNat (digits : String) : Nat

Fold a string of decimal digits into a natural number; callers guarantee digit-only input.

This is deliberately not String.toNat?, whose grammar also accepts _ digit separators, which the ODE/PDE literal languages do not.

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

Convert decimal digits to a natural number, rejecting empty or nondigit input.

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

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

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

Parse a finite signed decimal Float without scientific notation.