src/Pure/General/bytes.scala
author wenzelm
Thu, 14 Nov 2013 16:55:32 +0100
changeset 54439 621a155c7715
child 54440 2c4940d2edf7
permissions -rw-r--r--
immutable byte vectors versus UTF8 strings;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
54439
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/General/bytes.scala
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
     2
    Module:     PIDE
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
     3
    Author:     Makarius
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
     4
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
     5
Immutable byte vectors versus UTF8 strings.
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
     6
*/
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
     7
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
     8
package isabelle
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
     9
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
    10
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
    11
object Bytes
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
    12
{
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
    13
  val empty: Bytes = new Bytes(Array[Byte](), 0, 0)
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
    14
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
    15
  def apply(s: CharSequence): Bytes =
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
    16
  {
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
    17
    val str = s.toString
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
    18
    if (str.isEmpty) empty
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
    19
    else {
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
    20
      val bytes = UTF8.string_bytes(str)
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
    21
      new Bytes(bytes, 0, bytes.length)
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
    22
    }
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
    23
  }
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
    24
}
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
    25
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
    26
final class Bytes private(
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
    27
  protected val bytes: Array[Byte],
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
    28
  protected val offset: Int,
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
    29
  val length: Int)
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
    30
{
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
    31
  /* equality */
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
    32
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
    33
  private lazy val hash: Int =
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
    34
  {
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
    35
    var h = 0
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
    36
    for (i <- offset until offset + length) {
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
    37
      val b = bytes(i).asInstanceOf[Int] & 0xFF
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
    38
      h = 31 * h + b
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
    39
    }
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
    40
    h
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
    41
  }
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
    42
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
    43
  override def hashCode(): Int = hash
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
    44
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
    45
  override def equals(that: Any): Boolean =
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
    46
  {
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
    47
    that match {
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
    48
      case other: Bytes =>
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
    49
        if (this eq other) true
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
    50
        else if (length != other.length) false
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
    51
        else (0 until length).forall(i => bytes(offset + i) == other.bytes(other.offset + i))
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
    52
      case _ => false
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
    53
    }
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
    54
  }
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
    55
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
    56
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
    57
  /* content */
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
    58
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
    59
  override def toString: String = new String(bytes, offset, length, UTF8.charset)
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
    60
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
    61
  def is_empty: Boolean = length == 0
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
    62
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
    63
  def +(other: Bytes): Bytes =
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
    64
    if (other.is_empty) this
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
    65
    else if (is_empty) other
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
    66
    else {
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
    67
      val new_bytes = new Array[Byte](length + other.length)
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
    68
      java.lang.System.arraycopy(bytes, offset, new_bytes, 0, length)
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
    69
      java.lang.System.arraycopy(other.bytes, other.offset, new_bytes, length, other.length)
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
    70
      new Bytes(new_bytes, 0, new_bytes.length)
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
    71
    }
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
    72
}
621a155c7715 immutable byte vectors versus UTF8 strings;
wenzelm
parents:
diff changeset
    73