Shared IO-loader parsing utilities

This module contains the small pieces shared by the CSV and NPY loaders:

• ASCII digit/sign parsing used by numeric CSV cells and NPY headers; and
• small string helpers for parsing Python/NumPy-style header fragments.

The helpers are intentionally modest. They support TorchLean examples and regression tests, not a full data-ingestion framework.

def Runtime.Autograd.Train.IoLoader.Internal.maxNumericCellChars : ℕ

Maximum number of characters accepted for a numeric CSV cell or numeric NPY header atom.

Decimal scanning

def Runtime.Autograd.Train.IoLoader.Internal.isDigit (c : Char) : Bool

ASCII digit test used by the numeric parser.

def Runtime.Autograd.Train.IoLoader.Internal.digitVal? (c : Char) : Option ℕ

Convert a digit character to its numeric value, or return none if not a digit.

def Runtime.Autograd.Train.IoLoader.Internal.digitsToNat (ds : List ℕ) : ℕ

Interpret a list of base-10 digits as a natural number.

def Runtime.Autograd.Train.IoLoader.Internal.takeDigits (cs : List Char) : List ℕ × List Char

Consume a maximal prefix of digits from a character list.

def Runtime.Autograd.Train.IoLoader.Internal.takeDigits.go (acc : List ℕ) (cs : List Char) : List ℕ × List Char

def Runtime.Autograd.Train.IoLoader.Internal.parseSign (cs : List Char) : Bool × List Char

Parse an optional leading sign, returning whether the number is negative plus the remaining characters.

def Runtime.Autograd.Train.IoLoader.Internal.parseNatValue (s : String) : Option ℕ

Parse a natural number header value (expects a pure digit string).

Header string helpers

def Runtime.Autograd.Train.IoLoader.Internal.dropUntil (p : Char → Bool) : List Char → List Char

Drop characters until predicate p becomes true.

def Runtime.Autograd.Train.IoLoader.Internal.takeUntilChar (stop : Char) : List Char → List Char × List Char

Take characters until stop is encountered (not including stop).

def Runtime.Autograd.Train.IoLoader.Internal.parseQuotedValue (s : String) : Option String

Parse a quoted value '...' or \"...\" from a header fragment (best-effort).

def Runtime.Autograd.Train.IoLoader.Internal.parseBoolValue (s : String) : Option Bool

Parse a boolean header value (expects True or False).

def Runtime.Autograd.Train.IoLoader.Internal.fieldAfter (hdr key : String) : Option String

Find the substring after key in a header string, if present.

def Runtime.Autograd.Train.IoLoader.Internal.findField (hdr key : String) : Option String

Find a header field value by key name (handles both 'key': and \"key\": spellings).