merged
authorwenzelm
Thu May 24 22:28:26 2018 +0200 (21 months ago)
changeset 682695ff0ccc74884
parent 68263 e4e536a71e3d
parent 68268 38b4d4f39434
child 68270 2bc921b2159b
child 68271 77f6fa78b6e1
child 68283 e2f235b9662a
merged
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/Admin/Windows/Cygwin/setup_server	Thu May 24 22:28:26 2018 +0200
     1.3 @@ -0,0 +1,26 @@
     1.4 +#!/usr/bin/env bash
     1.5 +
     1.6 +CYGWIN_MAIN="https://cygwin.com"
     1.7 +CYGWIN_MIRROR="https://ftp.eq.uc.pt/software/pc/prog/cygwin"
     1.8 +
     1.9 +function fail()
    1.10 +{
    1.11 +  echo "$1" >&2
    1.12 +  exit 2
    1.13 +}
    1.14 +
    1.15 +function download()
    1.16 +{
    1.17 +  local URL="$1"
    1.18 +  local DIR="${2:-.}"
    1.19 +  mkdir -p "$DIR" || fail "Cannot create directory: \"$DIR\""
    1.20 +  echo "Downloading $URL ..."
    1.21 +  curl --fail --silent "$URL" > "$DIR"/"$(basename "$URL")" || fail "FAILED"
    1.22 +}
    1.23 +
    1.24 +download "$CYGWIN_MAIN/setup-x86.exe"
    1.25 +download "$CYGWIN_MAIN/setup-x86_64.exe"
    1.26 +download "$CYGWIN_MIRROR/x86/setup.xz" "x86"
    1.27 +download "$CYGWIN_MIRROR/x86/setup.xz.sig" "x86"
    1.28 +download "$CYGWIN_MIRROR/x86_64/setup.xz" "x86_64"
    1.29 +download "$CYGWIN_MIRROR/x86_64/setup.xz.sig" "x86_64"
     2.1 --- a/src/HOL/Tools/typedef.ML	Thu May 24 17:06:39 2018 +0200
     2.2 +++ b/src/HOL/Tools/typedef.ML	Thu May 24 22:28:26 2018 +0200
     2.3 @@ -348,4 +348,27 @@
     2.4  
     2.5  val overloaded = typedef_overloaded;
     2.6  
     2.7 +
     2.8 +
     2.9 +(** theory export **)
    2.10 +
    2.11 +val _ = Export_Theory.setup_presentation (fn _ => fn thy =>
    2.12 +  let
    2.13 +    val parent_spaces = map Sign.type_space (Theory.parents_of thy);
    2.14 +    val typedefs =
    2.15 +      Name_Space.dest_table (#types (Type.rep_tsig (Sign.tsig_of thy)))
    2.16 +      |> maps (fn (name, _) =>
    2.17 +          if exists (fn space => Name_Space.declared space name) parent_spaces then []
    2.18 +          else
    2.19 +            get_info_global thy name
    2.20 +            |> map (fn ({rep_type, abs_type, Rep_name, Abs_name, axiom_name}, _) =>
    2.21 +              (name, (rep_type, (abs_type, (Rep_name, (Abs_name, axiom_name)))))));
    2.22 +  in
    2.23 +    if null typedefs then ()
    2.24 +    else
    2.25 +      Export_Theory.export_body thy "typedefs"
    2.26 +        let open XML.Encode Term_XML.Encode
    2.27 +        in list (pair string (pair typ (pair typ (pair string (pair string string))))) typedefs end
    2.28 +  end);
    2.29 +
    2.30  end;
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/Pure/General/cache.scala	Thu May 24 22:28:26 2018 +0200
     3.3 @@ -0,0 +1,63 @@
     3.4 +/*  Title:      Pure/cache.scala
     3.5 +    Author:     Makarius
     3.6 +
     3.7 +cache for partial sharing (weak table).
     3.8 +*/
     3.9 +
    3.10 +package isabelle
    3.11 +
    3.12 +
    3.13 +import java.util.{Collections, WeakHashMap}
    3.14 +import java.lang.ref.WeakReference
    3.15 +
    3.16 +
    3.17 +class Cache(initial_size: Int = 131071, max_string: Int = 100)
    3.18 +{
    3.19 +  private val table =
    3.20 +    Collections.synchronizedMap(new WeakHashMap[Any, WeakReference[Any]](initial_size))
    3.21 +
    3.22 +  def size: Int = table.size
    3.23 +
    3.24 +  override def toString: String = "Cache(" + size + ")"
    3.25 +
    3.26 +  protected def lookup[A](x: A): Option[A] =
    3.27 +  {
    3.28 +    val ref = table.get(x)
    3.29 +    if (ref == null) None
    3.30 +    else {
    3.31 +      val y = ref.asInstanceOf[WeakReference[A]].get
    3.32 +      if (y == null) None
    3.33 +      else Some(y)
    3.34 +    }
    3.35 +  }
    3.36 +
    3.37 +  protected def store[A](x: A): A =
    3.38 +  {
    3.39 +    table.put(x, new WeakReference[Any](x))
    3.40 +    x
    3.41 +  }
    3.42 +
    3.43 +  protected def cache_int(x: Int): Int =
    3.44 +    lookup(x) getOrElse store(x)
    3.45 +
    3.46 +  protected def cache_string(x: String): String =
    3.47 +  {
    3.48 +    if (x == "") ""
    3.49 +    else if (x == "true") "true"
    3.50 +    else if (x == "false") "false"
    3.51 +    else if (x == "0.0") "0.0"
    3.52 +    else if (Library.is_small_int(x)) Library.signed_string_of_int(Integer.parseInt(x))
    3.53 +    else {
    3.54 +      lookup(x) match {
    3.55 +        case Some(y) => y
    3.56 +        case None =>
    3.57 +          val z = Library.isolate_substring(x)
    3.58 +          if (z.length > max_string) z else store(z)
    3.59 +      }
    3.60 +    }
    3.61 +  }
    3.62 +
    3.63 +  // main methods
    3.64 +  def int(x: Int): Int = synchronized { cache_int(x) }
    3.65 +  def string(x: String): String = synchronized { cache_string(x) }
    3.66 +}
     4.1 --- a/src/Pure/PIDE/xml.scala	Thu May 24 17:06:39 2018 +0200
     4.2 +++ b/src/Pure/PIDE/xml.scala	Thu May 24 22:28:26 2018 +0200
     4.3 @@ -7,11 +7,6 @@
     4.4  package isabelle
     4.5  
     4.6  
     4.7 -import java.util.{Collections, WeakHashMap}
     4.8 -import java.lang.ref.WeakReference
     4.9 -import javax.xml.parsers.DocumentBuilderFactory
    4.10 -
    4.11 -
    4.12  object XML
    4.13  {
    4.14    /** XML trees **/
    4.15 @@ -152,55 +147,26 @@
    4.16  
    4.17  
    4.18  
    4.19 -  /** cache for partial sharing (weak table) **/
    4.20 +  /** cache **/
    4.21  
    4.22    def make_cache(initial_size: Int = 131071, max_string: Int = 100): Cache =
    4.23      new Cache(initial_size, max_string)
    4.24  
    4.25    class Cache private[XML](initial_size: Int, max_string: Int)
    4.26 +    extends isabelle.Cache(initial_size, max_string)
    4.27    {
    4.28 -    private val table =
    4.29 -      Collections.synchronizedMap(new WeakHashMap[Any, WeakReference[Any]](initial_size))
    4.30 -
    4.31 -    def size: Int = table.size
    4.32 -
    4.33 -    private def lookup[A](x: A): Option[A] =
    4.34 -    {
    4.35 -      val ref = table.get(x)
    4.36 -      if (ref == null) None
    4.37 -      else {
    4.38 -        val y = ref.asInstanceOf[WeakReference[A]].get
    4.39 -        if (y == null) None
    4.40 -        else Some(y)
    4.41 -      }
    4.42 -    }
    4.43 -    private def store[A](x: A): A =
    4.44 +    protected def cache_props(x: Properties.T): Properties.T =
    4.45      {
    4.46 -      table.put(x, new WeakReference[Any](x))
    4.47 -      x
    4.48 -    }
    4.49 -
    4.50 -    private def cache_string(x: String): String =
    4.51 -      if (x == "") ""
    4.52 -      else if (x == "true") "true"
    4.53 -      else if (x == "false") "false"
    4.54 -      else if (x == "0.0") "0.0"
    4.55 -      else if (Library.is_small_int(x)) Library.signed_string_of_int(Integer.parseInt(x))
    4.56 -      else
    4.57 -        lookup(x) match {
    4.58 -          case Some(y) => y
    4.59 -          case None =>
    4.60 -            val z = Library.isolate_substring(x)
    4.61 -            if (z.length > max_string) z else store(z)
    4.62 -        }
    4.63 -    private def cache_props(x: Properties.T): Properties.T =
    4.64        if (x.isEmpty) x
    4.65        else
    4.66          lookup(x) match {
    4.67            case Some(y) => y
    4.68            case None => store(x.map(p => (Library.isolate_substring(p._1).intern, cache_string(p._2))))
    4.69          }
    4.70 -    private def cache_markup(x: Markup): Markup =
    4.71 +    }
    4.72 +
    4.73 +    protected def cache_markup(x: Markup): Markup =
    4.74 +    {
    4.75        lookup(x) match {
    4.76          case Some(y) => y
    4.77          case None =>
    4.78 @@ -209,7 +175,10 @@
    4.79                store(Markup(cache_string(name), cache_props(props)))
    4.80            }
    4.81        }
    4.82 -    private def cache_tree(x: XML.Tree): XML.Tree =
    4.83 +    }
    4.84 +
    4.85 +    protected def cache_tree(x: XML.Tree): XML.Tree =
    4.86 +    {
    4.87        lookup(x) match {
    4.88          case Some(y) => y
    4.89          case None =>
    4.90 @@ -219,16 +188,19 @@
    4.91              case XML.Text(text) => store(XML.Text(cache_string(text)))
    4.92            }
    4.93        }
    4.94 -    private def cache_body(x: XML.Body): XML.Body =
    4.95 +    }
    4.96 +
    4.97 +    protected def cache_body(x: XML.Body): XML.Body =
    4.98 +    {
    4.99        if (x.isEmpty) x
   4.100        else
   4.101          lookup(x) match {
   4.102            case Some(y) => y
   4.103            case None => x.map(cache_tree(_))
   4.104          }
   4.105 +    }
   4.106  
   4.107      // main methods
   4.108 -    def string(x: String): String = synchronized { cache_string(x) }
   4.109      def props(x: Properties.T): Properties.T = synchronized { cache_props(x) }
   4.110      def markup(x: Markup): Markup = synchronized { cache_markup(x) }
   4.111      def tree(x: XML.Tree): XML.Tree = synchronized { cache_tree(x) }
     5.1 --- a/src/Pure/Thy/export_theory.ML	Thu May 24 17:06:39 2018 +0200
     5.2 +++ b/src/Pure/Thy/export_theory.ML	Thu May 24 22:28:26 2018 +0200
     5.3 @@ -27,6 +27,9 @@
     5.4  
     5.5  val _ = setup_presentation (fn {adjust_pos, ...} => fn thy =>
     5.6    let
     5.7 +    val rep_tsig = Type.rep_tsig (Sign.tsig_of thy);
     5.8 +
     5.9 +
    5.10      (* parents *)
    5.11  
    5.12      val parents = Theory.parents_of thy;
    5.13 @@ -76,7 +79,7 @@
    5.14  
    5.15      val _ =
    5.16        export_entities "types" (K export_type) Sign.type_space
    5.17 -        (Name_Space.dest_table (#types (Type.rep_tsig (Sign.tsig_of thy))));
    5.18 +        (Name_Space.dest_table (#types rep_tsig));
    5.19  
    5.20  
    5.21      (* consts *)
    5.22 @@ -120,6 +123,24 @@
    5.23        export_entities "facts" (K (SOME o export_fact)) (Facts.space_of o Global_Theory.facts_of)
    5.24          (Facts.dest_static true [] (Global_Theory.facts_of thy));
    5.25  
    5.26 +
    5.27 +    (* type classes *)
    5.28 +
    5.29 +    val encode_class =
    5.30 +      let open XML.Encode Term_XML.Encode
    5.31 +      in pair (list (pair string typ)) (list term) end;
    5.32 +
    5.33 +    fun export_class name =
    5.34 +      (case try (Axclass.get_info thy) name of
    5.35 +        NONE => ([], [])
    5.36 +      | SOME {params, axioms, ...} =>
    5.37 +          (params, map (Logic.unvarify_global o Thm.full_prop_of) axioms))
    5.38 +      |> encode_class |> SOME;
    5.39 +
    5.40 +    val _ =
    5.41 +      export_entities "classes" (fn name => fn () => export_class name)
    5.42 +        Sign.class_space (map (rpair ()) (Graph.keys (Sorts.classes_of (#2 (#classes rep_tsig)))));
    5.43 +
    5.44      in () end);
    5.45  
    5.46  end;
     6.1 --- a/src/Pure/Thy/export_theory.scala	Thu May 24 17:06:39 2018 +0200
     6.2 +++ b/src/Pure/Thy/export_theory.scala	Thu May 24 22:28:26 2018 +0200
     6.3 @@ -26,14 +26,21 @@
     6.4    def read_session(store: Sessions.Store,
     6.5      session_name: String,
     6.6      types: Boolean = true,
     6.7 -    consts: Boolean = true): Session =
     6.8 +    consts: Boolean = true,
     6.9 +    axioms: Boolean = true,
    6.10 +    facts: Boolean = true,
    6.11 +    classes: Boolean = true,
    6.12 +    typedefs: Boolean = true,
    6.13 +    cache: Term.Cache = Term.make_cache()): Session =
    6.14    {
    6.15      val thys =
    6.16        using(store.open_database(session_name))(db =>
    6.17        {
    6.18          db.transaction {
    6.19            Export.read_theory_names(db, session_name).map((theory_name: String) =>
    6.20 -            read_theory(db, session_name, theory_name, types = types, consts = consts))
    6.21 +            read_theory(db, session_name, theory_name, types = types, consts = consts,
    6.22 +              axioms = axioms, facts = facts, classes = classes, typedefs = typedefs,
    6.23 +              cache = Some(cache)))
    6.24          }
    6.25        })
    6.26  
    6.27 @@ -55,18 +62,33 @@
    6.28      types: List[Type],
    6.29      consts: List[Const],
    6.30      axioms: List[Axiom],
    6.31 -    facts: List[Fact])
    6.32 +    facts: List[Fact],
    6.33 +    classes: List[Class],
    6.34 +    typedefs: List[Typedef])
    6.35    {
    6.36      override def toString: String = name
    6.37 +
    6.38 +    def cache(cache: Term.Cache): Theory =
    6.39 +      Theory(cache.string(name),
    6.40 +        parents.map(cache.string(_)),
    6.41 +        types.map(_.cache(cache)),
    6.42 +        consts.map(_.cache(cache)),
    6.43 +        axioms.map(_.cache(cache)),
    6.44 +        facts.map(_.cache(cache)),
    6.45 +        classes.map(_.cache(cache)),
    6.46 +        typedefs.map(_.cache(cache)))
    6.47    }
    6.48  
    6.49 -  def empty_theory(name: String): Theory = Theory(name, Nil, Nil, Nil, Nil, Nil)
    6.50 +  def empty_theory(name: String): Theory = Theory(name, Nil, Nil, Nil, Nil, Nil, Nil, Nil)
    6.51  
    6.52    def read_theory(db: SQL.Database, session_name: String, theory_name: String,
    6.53      types: Boolean = true,
    6.54      consts: Boolean = true,
    6.55      axioms: Boolean = true,
    6.56 -    facts: Boolean = true): Theory =
    6.57 +    facts: Boolean = true,
    6.58 +    classes: Boolean = true,
    6.59 +    typedefs: Boolean = true,
    6.60 +    cache: Option[Term.Cache] = None): Theory =
    6.61    {
    6.62      val parents =
    6.63        Export.read_entry(db, session_name, theory_name, "theory/parents") match {
    6.64 @@ -75,11 +97,15 @@
    6.65            error("Missing theory export in session " + quote(session_name) + ": " +
    6.66              quote(theory_name))
    6.67        }
    6.68 -    Theory(theory_name, parents,
    6.69 -      if (types) read_types(db, session_name, theory_name) else Nil,
    6.70 -      if (consts) read_consts(db, session_name, theory_name) else Nil,
    6.71 -      if (axioms) read_axioms(db, session_name, theory_name) else Nil,
    6.72 -      if (facts) read_facts(db, session_name, theory_name) else Nil)
    6.73 +    val theory =
    6.74 +      Theory(theory_name, parents,
    6.75 +        if (types) read_types(db, session_name, theory_name) else Nil,
    6.76 +        if (consts) read_consts(db, session_name, theory_name) else Nil,
    6.77 +        if (axioms) read_axioms(db, session_name, theory_name) else Nil,
    6.78 +        if (facts) read_facts(db, session_name, theory_name) else Nil,
    6.79 +        if (classes) read_classes(db, session_name, theory_name) else Nil,
    6.80 +        if (typedefs) read_typedefs(db, session_name, theory_name) else Nil)
    6.81 +    if (cache.isDefined) theory.cache(cache.get) else theory
    6.82    }
    6.83  
    6.84  
    6.85 @@ -88,6 +114,9 @@
    6.86    sealed case class Entity(name: String, serial: Long, pos: Position.T)
    6.87    {
    6.88      override def toString: String = name
    6.89 +
    6.90 +    def cache(cache: Term.Cache): Entity =
    6.91 +      Entity(cache.string(name), serial, cache.position(pos))
    6.92    }
    6.93  
    6.94    def decode_entity(tree: XML.Tree): (Entity, XML.Body) =
    6.95 @@ -104,19 +133,32 @@
    6.96      }
    6.97    }
    6.98  
    6.99 +  def read_export[A](db: SQL.Database, session_name: String, theory_name: String,
   6.100 +    export_name: String, decode: XML.Body => List[A]): List[A] =
   6.101 +  {
   6.102 +    Export.read_entry(db, session_name, theory_name, "theory/" + export_name) match {
   6.103 +      case Some(entry) => decode(entry.uncompressed_yxml())
   6.104 +      case None => Nil
   6.105 +    }
   6.106 +  }
   6.107 +
   6.108    def read_entities[A](db: SQL.Database, session_name: String, theory_name: String,
   6.109      export_name: String, decode: XML.Tree => A): List[A] =
   6.110    {
   6.111 -    Export.read_entry(db, session_name, theory_name, "theory/" + export_name) match {
   6.112 -      case Some(entry) => entry.uncompressed_yxml().map(decode(_))
   6.113 -      case None => Nil
   6.114 -    }
   6.115 +    read_export(db, session_name, theory_name, export_name,
   6.116 +      (body: XML.Body) => body.map(decode(_)))
   6.117    }
   6.118  
   6.119  
   6.120    /* types */
   6.121  
   6.122    sealed case class Type(entity: Entity, args: List[String], abbrev: Option[Term.Typ])
   6.123 +  {
   6.124 +    def cache(cache: Term.Cache): Type =
   6.125 +      Type(entity.cache(cache),
   6.126 +        args.map(cache.string(_)),
   6.127 +        abbrev.map(cache.typ(_)))
   6.128 +  }
   6.129  
   6.130    def read_types(db: SQL.Database, session_name: String, theory_name: String): List[Type] =
   6.131      read_entities(db, session_name, theory_name, "types",
   6.132 @@ -136,6 +178,13 @@
   6.133  
   6.134    sealed case class Const(
   6.135      entity: Entity, typargs: List[String], typ: Term.Typ, abbrev: Option[Term.Term])
   6.136 +  {
   6.137 +    def cache(cache: Term.Cache): Const =
   6.138 +      Const(entity.cache(cache),
   6.139 +        typargs.map(cache.string(_)),
   6.140 +        cache.typ(typ),
   6.141 +        abbrev.map(cache.term(_)))
   6.142 +  }
   6.143  
   6.144    def read_consts(db: SQL.Database, session_name: String, theory_name: String): List[Const] =
   6.145      read_entities(db, session_name, theory_name, "consts",
   6.146 @@ -166,6 +215,13 @@
   6.147      typargs: List[(String, Term.Sort)],
   6.148      args: List[(String, Term.Typ)],
   6.149      prop: Term.Term)
   6.150 +  {
   6.151 +    def cache(cache: Term.Cache): Axiom =
   6.152 +      Axiom(entity.cache(cache),
   6.153 +        typargs.map({ case (name, sort) => (cache.string(name), cache.sort(sort)) }),
   6.154 +        args.map({ case (name, typ) => (cache.string(name), cache.typ(typ)) }),
   6.155 +        cache.term(prop))
   6.156 +  }
   6.157  
   6.158    def read_axioms(db: SQL.Database, session_name: String, theory_name: String): List[Axiom] =
   6.159      read_entities(db, session_name, theory_name, "axioms",
   6.160 @@ -181,6 +237,13 @@
   6.161      typargs: List[(String, Term.Sort)],
   6.162      args: List[(String, Term.Typ)],
   6.163      props: List[Term.Term])
   6.164 +  {
   6.165 +    def cache(cache: Term.Cache): Fact =
   6.166 +      Fact(entity.cache(cache),
   6.167 +        typargs.map({ case (name, sort) => (cache.string(name), cache.sort(sort)) }),
   6.168 +        args.map({ case (name, typ) => (cache.string(name), cache.typ(typ)) }),
   6.169 +        props.map(cache.term(_)))
   6.170 +  }
   6.171  
   6.172    def read_facts(db: SQL.Database, session_name: String, theory_name: String): List[Fact] =
   6.173      read_entities(db, session_name, theory_name, "facts",
   6.174 @@ -190,4 +253,59 @@
   6.175            val (typargs, args, props) = decode_props(body)
   6.176            Fact(entity, typargs, args, props)
   6.177          })
   6.178 +
   6.179 +
   6.180 +  /* type classes */
   6.181 +
   6.182 +  sealed case class Class(
   6.183 +    entity: Entity, params: List[(String, Term.Typ)], axioms: List[Term.Term])
   6.184 +  {
   6.185 +    def cache(cache: Term.Cache): Class =
   6.186 +      Class(entity.cache(cache),
   6.187 +        params.map({ case (name, typ) => (cache.string(name), cache.typ(typ)) }),
   6.188 +        axioms.map(cache.term(_)))
   6.189 +  }
   6.190 +
   6.191 +  def read_classes(db: SQL.Database, session_name: String, theory_name: String): List[Class] =
   6.192 +    read_entities(db, session_name, theory_name, "classes",
   6.193 +      (tree: XML.Tree) =>
   6.194 +        {
   6.195 +          val (entity, body) = decode_entity(tree)
   6.196 +          val (params, axioms) =
   6.197 +          {
   6.198 +            import XML.Decode._
   6.199 +            import Term_XML.Decode._
   6.200 +            pair(list(pair(string, typ)), list(term))(body)
   6.201 +          }
   6.202 +          Class(entity, params, axioms)
   6.203 +        })
   6.204 +
   6.205 +
   6.206 +  /* HOL typedefs */
   6.207 +
   6.208 +  sealed case class Typedef(name: String,
   6.209 +    rep_type: Term.Typ, abs_type: Term.Typ, rep_name: String, abs_name: String, axiom_name: String)
   6.210 +  {
   6.211 +    def cache(cache: Term.Cache): Typedef =
   6.212 +      Typedef(cache.string(name),
   6.213 +        cache.typ(rep_type),
   6.214 +        cache.typ(abs_type),
   6.215 +        cache.string(rep_name),
   6.216 +        cache.string(abs_name),
   6.217 +        cache.string(axiom_name))
   6.218 +  }
   6.219 +
   6.220 +  def read_typedefs(db: SQL.Database, session_name: String, theory_name: String): List[Typedef] =
   6.221 +    read_export(db, session_name, theory_name, "typedefs",
   6.222 +      (body: XML.Body) =>
   6.223 +        {
   6.224 +          val typedefs =
   6.225 +          {
   6.226 +            import XML.Decode._
   6.227 +            import Term_XML.Decode._
   6.228 +            list(pair(string, pair(typ, pair(typ, pair(string, pair(string, string))))))(body)
   6.229 +          }
   6.230 +          for { (name, (rep_type, (abs_type, (rep_name, (abs_name, axiom_name))))) <- typedefs }
   6.231 +          yield Typedef(name, rep_type, abs_type, rep_name, abs_name, axiom_name)
   6.232 +        })
   6.233  }
     7.1 --- a/src/Pure/build-jars	Thu May 24 17:06:39 2018 +0200
     7.2 +++ b/src/Pure/build-jars	Thu May 24 22:28:26 2018 +0200
     7.3 @@ -41,6 +41,7 @@
     7.4    GUI/wrap_panel.scala
     7.5    General/antiquote.scala
     7.6    General/bytes.scala
     7.7 +  General/cache.scala
     7.8    General/codepoint.scala
     7.9    General/comment.scala
    7.10    General/completion.scala
     8.1 --- a/src/Pure/term.scala	Thu May 24 17:06:39 2018 +0200
     8.2 +++ b/src/Pure/term.scala	Thu May 24 22:28:26 2018 +0200
     8.3 @@ -29,5 +29,63 @@
     8.4    case class Bound(index: Int) extends Term
     8.5    case class Abs(name: String, typ: Typ = dummyT, body: Term) extends Term
     8.6    case class App(fun: Term, arg: Term) extends Term
     8.7 +
     8.8 +
     8.9 +
    8.10 +  /** cache **/
    8.11 +
    8.12 +  def make_cache(initial_size: Int = 131071, max_string: Int = Integer.MAX_VALUE): Cache =
    8.13 +    new Cache(initial_size, max_string)
    8.14 +
    8.15 +  class Cache private[Term](initial_size: Int, max_string: Int)
    8.16 +    extends isabelle.Cache(initial_size, max_string)
    8.17 +  {
    8.18 +    protected def cache_indexname(x: Indexname): Indexname =
    8.19 +      lookup(x) getOrElse store(cache_string(x._1), cache_int(x._2))
    8.20 +
    8.21 +    protected def cache_sort(x: Sort): Sort =
    8.22 +      if (x == dummyS) dummyS
    8.23 +      else lookup(x) getOrElse store(x.map(cache_string(_)))
    8.24 +
    8.25 +    protected def cache_typ(x: Typ): Typ =
    8.26 +    {
    8.27 +      if (x == dummyT) dummyT
    8.28 +      else
    8.29 +        lookup(x) match {
    8.30 +          case Some(y) => y
    8.31 +          case None =>
    8.32 +            x match {
    8.33 +              case Type(name, args) => store(Type(cache_string(name), args.map(cache_typ(_))))
    8.34 +              case TFree(name, sort) => store(TFree(cache_string(name), cache_sort(sort)))
    8.35 +              case TVar(name, sort) => store(TVar(cache_indexname(name), cache_sort(sort)))
    8.36 +            }
    8.37 +        }
    8.38 +    }
    8.39 +
    8.40 +    protected def cache_term(x: Term): Term =
    8.41 +    {
    8.42 +      lookup(x) match {
    8.43 +        case Some(y) => y
    8.44 +        case None =>
    8.45 +          x match {
    8.46 +            case Const(name, typ) => store(Const(cache_string(name), cache_typ(typ)))
    8.47 +            case Free(name, typ) => store(Free(cache_string(name), cache_typ(typ)))
    8.48 +            case Var(name, typ) => store(Var(cache_indexname(name), cache_typ(typ)))
    8.49 +            case Bound(index) => store(Bound(cache_int(index)))
    8.50 +            case Abs(name, typ, body) =>
    8.51 +              store(Abs(cache_string(name), cache_typ(typ), cache_term(body)))
    8.52 +            case App(fun, arg) => store(App(cache_term(fun), cache_term(arg)))
    8.53 +          }
    8.54 +      }
    8.55 +    }
    8.56 +
    8.57 +    // main methods
    8.58 +    def indexname(x: Indexname): Indexname = synchronized { cache_indexname(x) }
    8.59 +    def sort(x: Sort): Sort = synchronized { cache_sort(x) }
    8.60 +    def typ(x: Typ): Typ = synchronized { cache_typ(x) }
    8.61 +    def term(x: Term): Term = synchronized { cache_term(x) }
    8.62 +
    8.63 +    def position(x: Position.T): Position.T =
    8.64 +      synchronized { x.map({ case (a, b) => (cache_string(a), cache_string(b)) }) }
    8.65 +  }
    8.66  }
    8.67 -