more general cache, also for term substructures;
authorwenzelm
Thu May 24 21:13:09 2018 +0200 (21 months ago)
changeset 68265f0899dad4877
parent 68264 bb9a3be6952a
child 68266 f13bb379c573
more general cache, also for term substructures;
src/Pure/General/cache.scala
src/Pure/PIDE/xml.scala
src/Pure/build-jars
src/Pure/term.scala
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/General/cache.scala	Thu May 24 21:13:09 2018 +0200
     1.3 @@ -0,0 +1,61 @@
     1.4 +/*  Title:      Pure/cache.scala
     1.5 +    Author:     Makarius
     1.6 +
     1.7 +cache for partial sharing (weak table).
     1.8 +*/
     1.9 +
    1.10 +package isabelle
    1.11 +
    1.12 +
    1.13 +import java.util.{Collections, WeakHashMap}
    1.14 +import java.lang.ref.WeakReference
    1.15 +
    1.16 +
    1.17 +class Cache(initial_size: Int = 131071, max_string: Int = 100)
    1.18 +{
    1.19 +  private val table =
    1.20 +    Collections.synchronizedMap(new WeakHashMap[Any, WeakReference[Any]](initial_size))
    1.21 +
    1.22 +  def size: Int = table.size
    1.23 +
    1.24 +  protected def lookup[A](x: A): Option[A] =
    1.25 +  {
    1.26 +    val ref = table.get(x)
    1.27 +    if (ref == null) None
    1.28 +    else {
    1.29 +      val y = ref.asInstanceOf[WeakReference[A]].get
    1.30 +      if (y == null) None
    1.31 +      else Some(y)
    1.32 +    }
    1.33 +  }
    1.34 +
    1.35 +  protected def store[A](x: A): A =
    1.36 +  {
    1.37 +    table.put(x, new WeakReference[Any](x))
    1.38 +    x
    1.39 +  }
    1.40 +
    1.41 +  protected def cache_int(x: Int): Int =
    1.42 +    lookup(x) getOrElse store(x)
    1.43 +
    1.44 +  protected def cache_string(x: String): String =
    1.45 +  {
    1.46 +    if (x == "") ""
    1.47 +    else if (x == "true") "true"
    1.48 +    else if (x == "false") "false"
    1.49 +    else if (x == "0.0") "0.0"
    1.50 +    else if (Library.is_small_int(x)) Library.signed_string_of_int(Integer.parseInt(x))
    1.51 +    else {
    1.52 +      lookup(x) match {
    1.53 +        case Some(y) => y
    1.54 +        case None =>
    1.55 +          val z = Library.isolate_substring(x)
    1.56 +          if (z.length > max_string) z else store(z)
    1.57 +      }
    1.58 +    }
    1.59 +  }
    1.60 +
    1.61 +  // main methods
    1.62 +  def int(x: Int): Int = synchronized { cache_int(x) }
    1.63 +  def string(x: String): String = synchronized { cache_string(x) }
    1.64 +}
     2.1 --- a/src/Pure/PIDE/xml.scala	Thu May 24 16:56:14 2018 +0200
     2.2 +++ b/src/Pure/PIDE/xml.scala	Thu May 24 21:13:09 2018 +0200
     2.3 @@ -7,11 +7,6 @@
     2.4  package isabelle
     2.5  
     2.6  
     2.7 -import java.util.{Collections, WeakHashMap}
     2.8 -import java.lang.ref.WeakReference
     2.9 -import javax.xml.parsers.DocumentBuilderFactory
    2.10 -
    2.11 -
    2.12  object XML
    2.13  {
    2.14    /** XML trees **/
    2.15 @@ -152,55 +147,26 @@
    2.16  
    2.17  
    2.18  
    2.19 -  /** cache for partial sharing (weak table) **/
    2.20 +  /** cache **/
    2.21  
    2.22    def make_cache(initial_size: Int = 131071, max_string: Int = 100): Cache =
    2.23      new Cache(initial_size, max_string)
    2.24  
    2.25    class Cache private[XML](initial_size: Int, max_string: Int)
    2.26 +    extends isabelle.Cache(initial_size, max_string)
    2.27    {
    2.28 -    private val table =
    2.29 -      Collections.synchronizedMap(new WeakHashMap[Any, WeakReference[Any]](initial_size))
    2.30 -
    2.31 -    def size: Int = table.size
    2.32 -
    2.33 -    private def lookup[A](x: A): Option[A] =
    2.34 -    {
    2.35 -      val ref = table.get(x)
    2.36 -      if (ref == null) None
    2.37 -      else {
    2.38 -        val y = ref.asInstanceOf[WeakReference[A]].get
    2.39 -        if (y == null) None
    2.40 -        else Some(y)
    2.41 -      }
    2.42 -    }
    2.43 -    private def store[A](x: A): A =
    2.44 +    protected def cache_props(x: Properties.T): Properties.T =
    2.45      {
    2.46 -      table.put(x, new WeakReference[Any](x))
    2.47 -      x
    2.48 -    }
    2.49 -
    2.50 -    private def cache_string(x: String): String =
    2.51 -      if (x == "") ""
    2.52 -      else if (x == "true") "true"
    2.53 -      else if (x == "false") "false"
    2.54 -      else if (x == "0.0") "0.0"
    2.55 -      else if (Library.is_small_int(x)) Library.signed_string_of_int(Integer.parseInt(x))
    2.56 -      else
    2.57 -        lookup(x) match {
    2.58 -          case Some(y) => y
    2.59 -          case None =>
    2.60 -            val z = Library.isolate_substring(x)
    2.61 -            if (z.length > max_string) z else store(z)
    2.62 -        }
    2.63 -    private def cache_props(x: Properties.T): Properties.T =
    2.64        if (x.isEmpty) x
    2.65        else
    2.66          lookup(x) match {
    2.67            case Some(y) => y
    2.68            case None => store(x.map(p => (Library.isolate_substring(p._1).intern, cache_string(p._2))))
    2.69          }
    2.70 -    private def cache_markup(x: Markup): Markup =
    2.71 +    }
    2.72 +
    2.73 +    protected def cache_markup(x: Markup): Markup =
    2.74 +    {
    2.75        lookup(x) match {
    2.76          case Some(y) => y
    2.77          case None =>
    2.78 @@ -209,7 +175,10 @@
    2.79                store(Markup(cache_string(name), cache_props(props)))
    2.80            }
    2.81        }
    2.82 -    private def cache_tree(x: XML.Tree): XML.Tree =
    2.83 +    }
    2.84 +
    2.85 +    protected def cache_tree(x: XML.Tree): XML.Tree =
    2.86 +    {
    2.87        lookup(x) match {
    2.88          case Some(y) => y
    2.89          case None =>
    2.90 @@ -219,16 +188,19 @@
    2.91              case XML.Text(text) => store(XML.Text(cache_string(text)))
    2.92            }
    2.93        }
    2.94 -    private def cache_body(x: XML.Body): XML.Body =
    2.95 +    }
    2.96 +
    2.97 +    protected def cache_body(x: XML.Body): XML.Body =
    2.98 +    {
    2.99        if (x.isEmpty) x
   2.100        else
   2.101          lookup(x) match {
   2.102            case Some(y) => y
   2.103            case None => x.map(cache_tree(_))
   2.104          }
   2.105 +    }
   2.106  
   2.107      // main methods
   2.108 -    def string(x: String): String = synchronized { cache_string(x) }
   2.109      def props(x: Properties.T): Properties.T = synchronized { cache_props(x) }
   2.110      def markup(x: Markup): Markup = synchronized { cache_markup(x) }
   2.111      def tree(x: XML.Tree): XML.Tree = synchronized { cache_tree(x) }
     3.1 --- a/src/Pure/build-jars	Thu May 24 16:56:14 2018 +0200
     3.2 +++ b/src/Pure/build-jars	Thu May 24 21:13:09 2018 +0200
     3.3 @@ -41,6 +41,7 @@
     3.4    GUI/wrap_panel.scala
     3.5    General/antiquote.scala
     3.6    General/bytes.scala
     3.7 +  General/cache.scala
     3.8    General/codepoint.scala
     3.9    General/comment.scala
    3.10    General/completion.scala
     4.1 --- a/src/Pure/term.scala	Thu May 24 16:56:14 2018 +0200
     4.2 +++ b/src/Pure/term.scala	Thu May 24 21:13:09 2018 +0200
     4.3 @@ -29,5 +29,63 @@
     4.4    case class Bound(index: Int) extends Term
     4.5    case class Abs(name: String, typ: Typ = dummyT, body: Term) extends Term
     4.6    case class App(fun: Term, arg: Term) extends Term
     4.7 +
     4.8 +
     4.9 +
    4.10 +  /** cache **/
    4.11 +
    4.12 +  def make_cache(initial_size: Int = 131071, max_string: Int = Integer.MAX_VALUE): Cache =
    4.13 +    new Cache(initial_size, max_string)
    4.14 +
    4.15 +  class Cache private[Term](initial_size: Int, max_string: Int)
    4.16 +    extends isabelle.Cache(initial_size, max_string)
    4.17 +  {
    4.18 +    protected def cache_indexname(x: Indexname): Indexname =
    4.19 +      lookup(x) getOrElse store(cache_string(x._1), cache_int(x._2))
    4.20 +
    4.21 +    protected def cache_sort(x: Sort): Sort =
    4.22 +      if (x == dummyS) dummyS
    4.23 +      else lookup(x) getOrElse store(x.map(cache_string(_)))
    4.24 +
    4.25 +    protected def cache_typ(x: Typ): Typ =
    4.26 +    {
    4.27 +      if (x == dummyT) dummyT
    4.28 +      else
    4.29 +        lookup(x) match {
    4.30 +          case Some(y) => y
    4.31 +          case None =>
    4.32 +            x match {
    4.33 +              case Type(name, args) => store(Type(cache_string(name), args.map(cache_typ(_))))
    4.34 +              case TFree(name, sort) => store(TFree(cache_string(name), cache_sort(sort)))
    4.35 +              case TVar(name, sort) => store(TVar(cache_indexname(name), cache_sort(sort)))
    4.36 +            }
    4.37 +        }
    4.38 +    }
    4.39 +
    4.40 +    protected def cache_term(x: Term): Term =
    4.41 +    {
    4.42 +      lookup(x) match {
    4.43 +        case Some(y) => y
    4.44 +        case None =>
    4.45 +          x match {
    4.46 +            case Const(name, typ) => store(Const(cache_string(name), cache_typ(typ)))
    4.47 +            case Free(name, typ) => store(Free(cache_string(name), cache_typ(typ)))
    4.48 +            case Var(name, typ) => store(Var(cache_indexname(name), cache_typ(typ)))
    4.49 +            case Bound(index) => store(Bound(cache_int(index)))
    4.50 +            case Abs(name, typ, body) =>
    4.51 +              store(Abs(cache_string(name), cache_typ(typ), cache_term(body)))
    4.52 +            case App(fun, arg) => store(App(cache_term(fun), cache_term(arg)))
    4.53 +          }
    4.54 +      }
    4.55 +    }
    4.56 +
    4.57 +    // main methods
    4.58 +    def indexname(x: Indexname): Indexname = synchronized { cache_indexname(x) }
    4.59 +    def sort(x: Sort): Sort = synchronized { cache_sort(x) }
    4.60 +    def typ(x: Typ): Typ = synchronized { cache_typ(x) }
    4.61 +    def term(x: Term): Term = synchronized { cache_term(x) }
    4.62 +
    4.63 +    def position(x: Position.T): Position.T =
    4.64 +      synchronized { x.map({ case (a, b) => (cache_string(a), cache_string(b)) }) }
    4.65 +  }
    4.66  }
    4.67 -