Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/Pure/General/   (Beweissystem Isabelle Version 2025-1©)  Datei vom 16.11.2025 mit Größe 1 kB image not shown  

Quelle  cache.scala   Sprache: Scala

 
/*  Title:      Pure/General/cache.scala
    Author:     Makarius

Cache for partial sharing (weak table).
*/


package isabelle


import java.util.{Collections, WeakHashMap, Map => JMap}
import java.lang.ref.WeakReference


object Cache {
  val default_max_string = 100
  val default_initial_size = 131071

  def make(
      max_string: Int = default_max_string,
      initial_size: Int = default_initial_size): Cache =
    new Cache(max_string, initial_size)

  val none: Cache = make(max_string = 0)
}

class Cache(max_string: Int, initial_size: Int) {
  val no_cache: Boolean = max_string == 0

  protected val table: JMap[Any, WeakReference[Any]] =
    if (max_string == 0) null
    else Collections.synchronizedMap(new WeakHashMap[Any, WeakReference[Any]](initial_size))

  override def toString: String =
    if (no_cache) "Cache.none" else "Cache(size = " + table.size + ")"

  protected def lookup[A](x: A): Option[A] = {
    if (table == null) None
    else {
      val ref = table.get(x)
      if (ref == null) None
      else Option(ref.asInstanceOf[WeakReference[A]].get)
    }
  }

  protected def store[A](x: A): A = {
    if (table == null || x == null) x
    else {
      table.put(x, new WeakReference[Any](x))
      x
    }
  }

  protected def cache_string(x: String): String = {
    if (x == nullnull
    else if (x == """"
    else if (x == "true""true"
    else if (x == "false""false"
    else if (x == "0.0""0.0"
    else if (Symbol.is_static_spaces(x)) Symbol.spaces(x.length)
    else if (Library.is_small_int(x)) Library.signed_string_of_int(Integer.parseInt(x))
    else {
      lookup(x) match {
        case Some(y) => y
        case None =>
          val z = Library.isolate_substring(x)
          if (z.length > max_string) z else store(z)
      }
    }
  }

  // main methods
  def string(x: String): String =
    if (no_cache) x else synchronized { cache_string(x) }
}

100%


¤ Dauer der Verarbeitung: 0.12 Sekunden  (vorverarbeitet)  ¤

*© Formatika GbR, Deutschland






Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.