src/Pure/General/cache.scala
author wenzelm
Thu, 24 May 2018 21:21:26 +0200
changeset 68266 f13bb379c573
parent 68265 f0899dad4877
child 68396 7433ee1ed7e3
permissions -rw-r--r--
tuned output;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
68265
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/cache.scala
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents:
diff changeset
     3
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents:
diff changeset
     4
cache for partial sharing (weak table).
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents:
diff changeset
     5
*/
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents:
diff changeset
     6
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents:
diff changeset
     7
package isabelle
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents:
diff changeset
     8
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents:
diff changeset
     9
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents:
diff changeset
    10
import java.util.{Collections, WeakHashMap}
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents:
diff changeset
    11
import java.lang.ref.WeakReference
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents:
diff changeset
    12
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents:
diff changeset
    13
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents:
diff changeset
    14
class Cache(initial_size: Int = 131071, max_string: Int = 100)
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents:
diff changeset
    15
{
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents:
diff changeset
    16
  private val table =
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents:
diff changeset
    17
    Collections.synchronizedMap(new WeakHashMap[Any, WeakReference[Any]](initial_size))
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents:
diff changeset
    18
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents:
diff changeset
    19
  def size: Int = table.size
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents:
diff changeset
    20
68266
f13bb379c573 tuned output;
wenzelm
parents: 68265
diff changeset
    21
  override def toString: String = "Cache(" + size + ")"
f13bb379c573 tuned output;
wenzelm
parents: 68265
diff changeset
    22
68265
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents:
diff changeset
    23
  protected def lookup[A](x: A): Option[A] =
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents:
diff changeset
    24
  {
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents:
diff changeset
    25
    val ref = table.get(x)
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents:
diff changeset
    26
    if (ref == null) None
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents:
diff changeset
    27
    else {
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents:
diff changeset
    28
      val y = ref.asInstanceOf[WeakReference[A]].get
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents:
diff changeset
    29
      if (y == null) None
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents:
diff changeset
    30
      else Some(y)
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents:
diff changeset
    31
    }
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents:
diff changeset
    32
  }
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents:
diff changeset
    33
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents:
diff changeset
    34
  protected def store[A](x: A): A =
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents:
diff changeset
    35
  {
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents:
diff changeset
    36
    table.put(x, new WeakReference[Any](x))
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents:
diff changeset
    37
    x
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents:
diff changeset
    38
  }
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents:
diff changeset
    39
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents:
diff changeset
    40
  protected def cache_int(x: Int): Int =
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents:
diff changeset
    41
    lookup(x) getOrElse store(x)
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents:
diff changeset
    42
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents:
diff changeset
    43
  protected def cache_string(x: String): String =
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents:
diff changeset
    44
  {
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents:
diff changeset
    45
    if (x == "") ""
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents:
diff changeset
    46
    else if (x == "true") "true"
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents:
diff changeset
    47
    else if (x == "false") "false"
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents:
diff changeset
    48
    else if (x == "0.0") "0.0"
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents:
diff changeset
    49
    else if (Library.is_small_int(x)) Library.signed_string_of_int(Integer.parseInt(x))
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents:
diff changeset
    50
    else {
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents:
diff changeset
    51
      lookup(x) match {
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents:
diff changeset
    52
        case Some(y) => y
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents:
diff changeset
    53
        case None =>
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents:
diff changeset
    54
          val z = Library.isolate_substring(x)
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents:
diff changeset
    55
          if (z.length > max_string) z else store(z)
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents:
diff changeset
    56
      }
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents:
diff changeset
    57
    }
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents:
diff changeset
    58
  }
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents:
diff changeset
    59
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents:
diff changeset
    60
  // main methods
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents:
diff changeset
    61
  def int(x: Int): Int = synchronized { cache_int(x) }
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents:
diff changeset
    62
  def string(x: String): String = synchronized { cache_string(x) }
f0899dad4877 more general cache, also for term substructures;
wenzelm
parents:
diff changeset
    63
}