CSV Loader

Small CSV helpers for TorchLean examples and regression tests.

The parser is kept narrow: unquoted delimiter-separated numeric cells only. It does not support quoted fields, escaped delimiters, locale-specific number formats, NaN, or inf. Keeping that grammar explicit is better than accidentally treating this as a production CSV library.

structure TorchLean.Data.IO.CsvOptions : Type

Options for the CSV parser in this module.

The parser accepts unquoted numeric fields with literal delimiters and locale-independent number syntax.

• delimiter : Char

  Delimiter character (default: ,).

• skipHeader : Bool

  If true, drop the first line before parsing rows.

• trimCells : Bool

  If true, trim ASCII whitespace around cells and around each row.

• allowEmptyLines : Bool

  If true, ignore empty lines (otherwise treat them as an error).

def TorchLean.Data.IO.Internal.parseExponent (tag : String) (cs : List Char) : Except String (Int × List Char)

Parse an optional exponent suffix of the form e±NNN or E±NNN.

Returns (exp, rest) where exp is an Int power-of-10 exponent to apply.

def TorchLean.Data.IO.Internal.parseFloatString (tag s : String) : Except String Float

Parse a numeric string into a Float.

Supported grammar:

• optional sign
• digits
• optional fractional part .digits
• optional scientific exponent e±digits

This parser rejects NaN, inf, locale separators, and quoted CSV cells.

def TorchLean.Data.IO.parseCsvLine (tag : String) (options : CsvOptions) (rowIdx : Nat) (line : String) : Except String (Option (Array Float))

Parse one CSV line into an array of floats.

Returns none for empty lines when allowEmptyLines = true.

def TorchLean.Data.IO.readCsvFloatRows (path : System.FilePath) (options : CsvOptions := { }) : IO (Except String (Array (Array Float)))

Read a CSV file into an array of float rows.

This helper is intended for compact example datasets and runtime checks, not a full CSV implementation.