TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

NN.Tensor.Internal.Syntax.UnicodeData

Generated Python Unicode properties #

This file is generated by scripts/generate_unicode_table.py; do not edit it by hand. It freezes the CPython 3.12.13 character predicates for Unicode 15.0.0 that the einops lexer reproduces.

The table lists the maximal runs of code points sharing the same nonzero property flags, in ascending order and pairwise disjoint. Bit 0 records str.isalnum, bit 1 records str.isidentifier on the single character, bit 2 records whether the character may continue an identifier, and bit 3 records str.isdecimal. Every decimal run covers exactly the ten digits of one decimal alphabet in order, so the digit value of a decimal character is its offset from the start of its run.

source
structure TorchLean.Tensor.Internal.Syntax.PythonUnicode.Interval :
Type

A maximal run of code points sharing the same Python property flags.

  • lo : UInt32

    The first code point of the run.

  • hi : UInt32

    The last code point of the run.

  • flags : UInt8

    The property flags shared by every code point of the run.

Instances For
    source
    @[instance_reducible]
    instance TorchLean.Tensor.Internal.Syntax.PythonUnicode.instReprInterval :
    Repr Interval
    source
    def TorchLean.Tensor.Internal.Syntax.PythonUnicode.instReprInterval.repr :
    Interval → Nat → Std.Format
    Instances For
      source
      def TorchLean.Tensor.Internal.Syntax.PythonUnicode.instDecidableEqInterval.decEq (x✝ x✝¹ : Interval) :
      Decidable (x✝ = x✝¹)
      Instances For
        source
        @[instance_reducible]
        instance TorchLean.Tensor.Internal.Syntax.PythonUnicode.instDecidableEqInterval :
        DecidableEq Interval
        source
        def TorchLean.Tensor.Internal.Syntax.PythonUnicode.alphanumericFlag :
        UInt8

        Flag bit recording str.isalnum.

        Instances For
          source
          def TorchLean.Tensor.Internal.Syntax.PythonUnicode.identifierStartFlag :
          UInt8

          Flag bit recording that the character may start an identifier.

          Instances For
            source
            def TorchLean.Tensor.Internal.Syntax.PythonUnicode.identifierContinueFlag :
            UInt8

            Flag bit recording that the character may continue an identifier.

            Instances For
              source
              def TorchLean.Tensor.Internal.Syntax.PythonUnicode.decimalFlag :
              UInt8

              Flag bit recording str.isdecimal.

              Instances For
                source
                def TorchLean.Tensor.Internal.Syntax.PythonUnicode.intervalsPart0 :
                List Interval

                Part 0 of intervals, split to stay within elaborator limits.

                Instances For
                  source
                  def TorchLean.Tensor.Internal.Syntax.PythonUnicode.intervalsPart1 :
                  List Interval

                  Part 1 of intervals, split to stay within elaborator limits.

                  Instances For
                    source
                    def TorchLean.Tensor.Internal.Syntax.PythonUnicode.intervalsPart2 :
                    List Interval

                    Part 2 of intervals, split to stay within elaborator limits.

                    Instances For
                      source
                      def TorchLean.Tensor.Internal.Syntax.PythonUnicode.intervals :
                      Array Interval

                      The 1147 property runs of Unicode 15.0.0, ascending and disjoint.

                      Instances For
                        source
                        def TorchLean.Tensor.Internal.Syntax.PythonUnicode.search (codepoint : UInt32) (fuel lo hi : Nat) :
                        Option Interval

                        Binary search for the run containing codepoint within the index range [lo, hi) of intervals. The fuel argument bounds the recursion so the definition is structural and reduces inside the kernel.

                        Instances For
                          source
                          def TorchLean.Tensor.Internal.Syntax.PythonUnicode.lookup? (char : Char) :
                          Option Interval

                          The property run containing a character, if it has any recorded property.

                          Instances For
                            source
                            def TorchLean.Tensor.Internal.Syntax.PythonUnicode.hasFlag (char : Char) (flag : UInt8) :
                            Bool

                            Whether a character carries the given property flag.

                            Instances For
                              source
                              def TorchLean.Tensor.Internal.Syntax.PythonUnicode.decimalValue? (char : Char) :
                              Option Nat

                              The digit value of a str.isdecimal character.

                              Instances For