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 runs of code points sharing the same nonzero property flags, in ascending order and pairwise disjoint. Adjacent decimal alphabets remain separate even when their flags agree. 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 run with common Python property flags, split at decimal-alphabet boundaries.

  • 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.lookup? (char : Char) :
                        Option Interval

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

                        The structural fuel keeps lookup reducible in kernel proofs of the lexer. The pinned Array.binSearch implementation does not reduce through the imported module boundary.

                        Instances For
                          source
                          def TorchLean.Tensor.Internal.Syntax.PythonUnicode.lookup?.search (codepoint : UInt32) (fuel lo hi : Nat) :
                          Option Interval
                          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