src/Pure/ML/ml_heap.scala
author wenzelm
Sun, 15 Jan 2023 20:38:27 +0100
changeset 76992 11c0747a87fc
parent 76991 6a078c80eab6
child 77206 6784eaef7d0c
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
76991
6a078c80eab6 clarified modules;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/ML/ml_heap.scala
6a078c80eab6 clarified modules;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
6a078c80eab6 clarified modules;
wenzelm
parents:
diff changeset
     3
6a078c80eab6 clarified modules;
wenzelm
parents:
diff changeset
     4
ML heap operations.
6a078c80eab6 clarified modules;
wenzelm
parents:
diff changeset
     5
*/
6a078c80eab6 clarified modules;
wenzelm
parents:
diff changeset
     6
6a078c80eab6 clarified modules;
wenzelm
parents:
diff changeset
     7
package isabelle
6a078c80eab6 clarified modules;
wenzelm
parents:
diff changeset
     8
6a078c80eab6 clarified modules;
wenzelm
parents:
diff changeset
     9
6a078c80eab6 clarified modules;
wenzelm
parents:
diff changeset
    10
import java.nio.ByteBuffer
6a078c80eab6 clarified modules;
wenzelm
parents:
diff changeset
    11
import java.nio.channels.FileChannel
6a078c80eab6 clarified modules;
wenzelm
parents:
diff changeset
    12
import java.nio.file.StandardOpenOption
6a078c80eab6 clarified modules;
wenzelm
parents:
diff changeset
    13
6a078c80eab6 clarified modules;
wenzelm
parents:
diff changeset
    14
6a078c80eab6 clarified modules;
wenzelm
parents:
diff changeset
    15
object ML_Heap {
6a078c80eab6 clarified modules;
wenzelm
parents:
diff changeset
    16
  /** heap file with SHA1 digest **/
6a078c80eab6 clarified modules;
wenzelm
parents:
diff changeset
    17
6a078c80eab6 clarified modules;
wenzelm
parents:
diff changeset
    18
  private val sha1_prefix = "SHA1:"
6a078c80eab6 clarified modules;
wenzelm
parents:
diff changeset
    19
6a078c80eab6 clarified modules;
wenzelm
parents:
diff changeset
    20
  def read_digest(heap: Path): Option[String] = {
6a078c80eab6 clarified modules;
wenzelm
parents:
diff changeset
    21
    if (heap.is_file) {
6a078c80eab6 clarified modules;
wenzelm
parents:
diff changeset
    22
      using(FileChannel.open(heap.java_path, StandardOpenOption.READ)) { file =>
6a078c80eab6 clarified modules;
wenzelm
parents:
diff changeset
    23
        val len = file.size
6a078c80eab6 clarified modules;
wenzelm
parents:
diff changeset
    24
        val n = sha1_prefix.length + SHA1.digest_length
6a078c80eab6 clarified modules;
wenzelm
parents:
diff changeset
    25
        if (len >= n) {
6a078c80eab6 clarified modules;
wenzelm
parents:
diff changeset
    26
          file.position(len - n)
6a078c80eab6 clarified modules;
wenzelm
parents:
diff changeset
    27
6a078c80eab6 clarified modules;
wenzelm
parents:
diff changeset
    28
          val buf = ByteBuffer.allocate(n)
6a078c80eab6 clarified modules;
wenzelm
parents:
diff changeset
    29
          var i = 0
6a078c80eab6 clarified modules;
wenzelm
parents:
diff changeset
    30
          var m = 0
6a078c80eab6 clarified modules;
wenzelm
parents:
diff changeset
    31
          while ({
6a078c80eab6 clarified modules;
wenzelm
parents:
diff changeset
    32
            m = file.read(buf)
6a078c80eab6 clarified modules;
wenzelm
parents:
diff changeset
    33
            if (m != -1) i += m
6a078c80eab6 clarified modules;
wenzelm
parents:
diff changeset
    34
            m != -1 && n > i
6a078c80eab6 clarified modules;
wenzelm
parents:
diff changeset
    35
          }) ()
6a078c80eab6 clarified modules;
wenzelm
parents:
diff changeset
    36
6a078c80eab6 clarified modules;
wenzelm
parents:
diff changeset
    37
          if (i == n) {
6a078c80eab6 clarified modules;
wenzelm
parents:
diff changeset
    38
            val prefix = new String(buf.array(), 0, sha1_prefix.length, UTF8.charset)
6a078c80eab6 clarified modules;
wenzelm
parents:
diff changeset
    39
            val s = new String(buf.array(), sha1_prefix.length, SHA1.digest_length, UTF8.charset)
6a078c80eab6 clarified modules;
wenzelm
parents:
diff changeset
    40
            if (prefix == sha1_prefix) Some(s) else None
6a078c80eab6 clarified modules;
wenzelm
parents:
diff changeset
    41
          }
6a078c80eab6 clarified modules;
wenzelm
parents:
diff changeset
    42
          else None
6a078c80eab6 clarified modules;
wenzelm
parents:
diff changeset
    43
        }
6a078c80eab6 clarified modules;
wenzelm
parents:
diff changeset
    44
        else None
6a078c80eab6 clarified modules;
wenzelm
parents:
diff changeset
    45
      }
6a078c80eab6 clarified modules;
wenzelm
parents:
diff changeset
    46
    }
6a078c80eab6 clarified modules;
wenzelm
parents:
diff changeset
    47
    else None
6a078c80eab6 clarified modules;
wenzelm
parents:
diff changeset
    48
  }
6a078c80eab6 clarified modules;
wenzelm
parents:
diff changeset
    49
6a078c80eab6 clarified modules;
wenzelm
parents:
diff changeset
    50
  def write_digest(heap: Path): String =
76992
wenzelm
parents: 76991
diff changeset
    51
    read_digest(heap) getOrElse {
wenzelm
parents: 76991
diff changeset
    52
      val s = SHA1.digest(heap).toString
wenzelm
parents: 76991
diff changeset
    53
      File.append(heap, sha1_prefix + s)
wenzelm
parents: 76991
diff changeset
    54
      s
76991
6a078c80eab6 clarified modules;
wenzelm
parents:
diff changeset
    55
    }
6a078c80eab6 clarified modules;
wenzelm
parents:
diff changeset
    56
}