TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

NN.Data.IO.Parsing

Data-File Parsing #

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

The parser is deliberately small. It supports TorchLean examples and regression tests, not a full data-ingestion framework.

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

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

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

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

    Instances For

      Decimal scanning #

      source
      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.

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

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

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

          Consume a maximal prefix of digits from a character list.

          Instances For
            source
            def TorchLean.Data.IO.Internal.takeDigits.go (acc : List Nat) (cs : List Char) :
            List Nat × List Char
            Instances For
              source
              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.

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

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

                Instances For

                  Header string helpers #

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

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

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

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

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

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

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

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

                        Instances For
                          source
                          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).

                          Instances For