Data-File Parsing

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 parser is deliberately small. It supports TorchLean examples and regression tests, not a full data-ingestion framework.

def TorchLean.Data.IO.Internal.maxNumericCellChars : Nat

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

def TorchLean.Data.IO.Internal.formatError (context message : String) : String

Prefix a parser error with the file format or field that produced it.

Decimal scanning

def TorchLean.Data.IO.Internal.isDigit (c : Char) : Bool

ASCII digit test used by the numeric parser.

def TorchLean.Data.IO.Internal.digitVal? (c : Char) : Option Nat

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

def TorchLean.Data.IO.Internal.digitsToNat (ds : List Nat) : Nat

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

def TorchLean.Data.IO.Internal.takeDigits (cs : List Char) : List Nat × List Char

Consume a maximal prefix of digits from a character list.

def TorchLean.Data.IO.Internal.takeDigits.go (acc : List Nat) (cs : List Char) : List Nat × List Char

def TorchLean.Data.IO.Internal.parseSign (cs : List Char) : Bool × List Char

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

def TorchLean.Data.IO.Internal.parseNatValue (s : String) : Option Nat

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

Header string helpers

def TorchLean.Data.IO.Internal.dropUntil (p : Char → Bool) : List Char → List Char

Drop characters until predicate p becomes true.

def TorchLean.Data.IO.Internal.takeUntilChar (stop : Char) : List Char → List Char × List Char

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

def TorchLean.Data.IO.Internal.isHeaderValueEnd (rest : List Char) : Bool

End of one field value in a NumPy header dictionary or standalone parser input.

def TorchLean.Data.IO.Internal.parseQuotedValue (s : String) : Option String

Parse a closed quoted value from a header fragment. Escaped strings are unsupported.

def TorchLean.Data.IO.Internal.parseBoolValue (s : String) : Option Bool

Parse a complete boolean header atom (True or False).

def TorchLean.Data.IO.Internal.fieldAfter (hdr key : String) : Option String

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

def TorchLean.Data.IO.Internal.findField (hdr key : String) : Option String

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