src/Pure/Thy/export_theory.scala
changeset 68267 6a29709906c6
parent 68264 bb9a3be6952a
child 68295 781a98696638
     1.1 --- a/src/Pure/Thy/export_theory.scala	Thu May 24 21:21:26 2018 +0200
     1.2 +++ b/src/Pure/Thy/export_theory.scala	Thu May 24 21:36:39 2018 +0200
     1.3 @@ -30,7 +30,8 @@
     1.4      axioms: Boolean = true,
     1.5      facts: Boolean = true,
     1.6      classes: Boolean = true,
     1.7 -    typedefs: Boolean = true): Session =
     1.8 +    typedefs: Boolean = true,
     1.9 +    cache: Term.Cache = Term.make_cache()): Session =
    1.10    {
    1.11      val thys =
    1.12        using(store.open_database(session_name))(db =>
    1.13 @@ -38,7 +39,8 @@
    1.14          db.transaction {
    1.15            Export.read_theory_names(db, session_name).map((theory_name: String) =>
    1.16              read_theory(db, session_name, theory_name, types = types, consts = consts,
    1.17 -              axioms = axioms, facts = facts, classes = classes, typedefs = typedefs))
    1.18 +              axioms = axioms, facts = facts, classes = classes, typedefs = typedefs,
    1.19 +              cache = Some(cache)))
    1.20          }
    1.21        })
    1.22  
    1.23 @@ -65,6 +67,16 @@
    1.24      typedefs: List[Typedef])
    1.25    {
    1.26      override def toString: String = name
    1.27 +
    1.28 +    def cache(cache: Term.Cache): Theory =
    1.29 +      Theory(cache.string(name),
    1.30 +        parents.map(cache.string(_)),
    1.31 +        types.map(_.cache(cache)),
    1.32 +        consts.map(_.cache(cache)),
    1.33 +        axioms.map(_.cache(cache)),
    1.34 +        facts.map(_.cache(cache)),
    1.35 +        classes.map(_.cache(cache)),
    1.36 +        typedefs.map(_.cache(cache)))
    1.37    }
    1.38  
    1.39    def empty_theory(name: String): Theory = Theory(name, Nil, Nil, Nil, Nil, Nil, Nil, Nil)
    1.40 @@ -75,7 +87,8 @@
    1.41      axioms: Boolean = true,
    1.42      facts: Boolean = true,
    1.43      classes: Boolean = true,
    1.44 -    typedefs: Boolean = true): Theory =
    1.45 +    typedefs: Boolean = true,
    1.46 +    cache: Option[Term.Cache] = None): Theory =
    1.47    {
    1.48      val parents =
    1.49        Export.read_entry(db, session_name, theory_name, "theory/parents") match {
    1.50 @@ -84,13 +97,15 @@
    1.51            error("Missing theory export in session " + quote(session_name) + ": " +
    1.52              quote(theory_name))
    1.53        }
    1.54 -    Theory(theory_name, parents,
    1.55 -      if (types) read_types(db, session_name, theory_name) else Nil,
    1.56 -      if (consts) read_consts(db, session_name, theory_name) else Nil,
    1.57 -      if (axioms) read_axioms(db, session_name, theory_name) else Nil,
    1.58 -      if (facts) read_facts(db, session_name, theory_name) else Nil,
    1.59 -      if (classes) read_classes(db, session_name, theory_name) else Nil,
    1.60 -      if (typedefs) read_typedefs(db, session_name, theory_name) else Nil)
    1.61 +    val theory =
    1.62 +      Theory(theory_name, parents,
    1.63 +        if (types) read_types(db, session_name, theory_name) else Nil,
    1.64 +        if (consts) read_consts(db, session_name, theory_name) else Nil,
    1.65 +        if (axioms) read_axioms(db, session_name, theory_name) else Nil,
    1.66 +        if (facts) read_facts(db, session_name, theory_name) else Nil,
    1.67 +        if (classes) read_classes(db, session_name, theory_name) else Nil,
    1.68 +        if (typedefs) read_typedefs(db, session_name, theory_name) else Nil)
    1.69 +    if (cache.isDefined) theory.cache(cache.get) else theory
    1.70    }
    1.71  
    1.72  
    1.73 @@ -99,6 +114,9 @@
    1.74    sealed case class Entity(name: String, serial: Long, pos: Position.T)
    1.75    {
    1.76      override def toString: String = name
    1.77 +
    1.78 +    def cache(cache: Term.Cache): Entity =
    1.79 +      Entity(cache.string(name), serial, cache.position(pos))
    1.80    }
    1.81  
    1.82    def decode_entity(tree: XML.Tree): (Entity, XML.Body) =
    1.83 @@ -135,6 +153,12 @@
    1.84    /* types */
    1.85  
    1.86    sealed case class Type(entity: Entity, args: List[String], abbrev: Option[Term.Typ])
    1.87 +  {
    1.88 +    def cache(cache: Term.Cache): Type =
    1.89 +      Type(entity.cache(cache),
    1.90 +        args.map(cache.string(_)),
    1.91 +        abbrev.map(cache.typ(_)))
    1.92 +  }
    1.93  
    1.94    def read_types(db: SQL.Database, session_name: String, theory_name: String): List[Type] =
    1.95      read_entities(db, session_name, theory_name, "types",
    1.96 @@ -154,6 +178,13 @@
    1.97  
    1.98    sealed case class Const(
    1.99      entity: Entity, typargs: List[String], typ: Term.Typ, abbrev: Option[Term.Term])
   1.100 +  {
   1.101 +    def cache(cache: Term.Cache): Const =
   1.102 +      Const(entity.cache(cache),
   1.103 +        typargs.map(cache.string(_)),
   1.104 +        cache.typ(typ),
   1.105 +        abbrev.map(cache.term(_)))
   1.106 +  }
   1.107  
   1.108    def read_consts(db: SQL.Database, session_name: String, theory_name: String): List[Const] =
   1.109      read_entities(db, session_name, theory_name, "consts",
   1.110 @@ -184,6 +215,13 @@
   1.111      typargs: List[(String, Term.Sort)],
   1.112      args: List[(String, Term.Typ)],
   1.113      prop: Term.Term)
   1.114 +  {
   1.115 +    def cache(cache: Term.Cache): Axiom =
   1.116 +      Axiom(entity.cache(cache),
   1.117 +        typargs.map({ case (name, sort) => (cache.string(name), cache.sort(sort)) }),
   1.118 +        args.map({ case (name, typ) => (cache.string(name), cache.typ(typ)) }),
   1.119 +        cache.term(prop))
   1.120 +  }
   1.121  
   1.122    def read_axioms(db: SQL.Database, session_name: String, theory_name: String): List[Axiom] =
   1.123      read_entities(db, session_name, theory_name, "axioms",
   1.124 @@ -199,6 +237,13 @@
   1.125      typargs: List[(String, Term.Sort)],
   1.126      args: List[(String, Term.Typ)],
   1.127      props: List[Term.Term])
   1.128 +  {
   1.129 +    def cache(cache: Term.Cache): Fact =
   1.130 +      Fact(entity.cache(cache),
   1.131 +        typargs.map({ case (name, sort) => (cache.string(name), cache.sort(sort)) }),
   1.132 +        args.map({ case (name, typ) => (cache.string(name), cache.typ(typ)) }),
   1.133 +        props.map(cache.term(_)))
   1.134 +  }
   1.135  
   1.136    def read_facts(db: SQL.Database, session_name: String, theory_name: String): List[Fact] =
   1.137      read_entities(db, session_name, theory_name, "facts",
   1.138 @@ -214,6 +259,12 @@
   1.139  
   1.140    sealed case class Class(
   1.141      entity: Entity, params: List[(String, Term.Typ)], axioms: List[Term.Term])
   1.142 +  {
   1.143 +    def cache(cache: Term.Cache): Class =
   1.144 +      Class(entity.cache(cache),
   1.145 +        params.map({ case (name, typ) => (cache.string(name), cache.typ(typ)) }),
   1.146 +        axioms.map(cache.term(_)))
   1.147 +  }
   1.148  
   1.149    def read_classes(db: SQL.Database, session_name: String, theory_name: String): List[Class] =
   1.150      read_entities(db, session_name, theory_name, "classes",
   1.151 @@ -234,6 +285,15 @@
   1.152  
   1.153    sealed case class Typedef(name: String,
   1.154      rep_type: Term.Typ, abs_type: Term.Typ, rep_name: String, abs_name: String, axiom_name: String)
   1.155 +  {
   1.156 +    def cache(cache: Term.Cache): Typedef =
   1.157 +      Typedef(cache.string(name),
   1.158 +        cache.typ(rep_type),
   1.159 +        cache.typ(abs_type),
   1.160 +        cache.string(rep_name),
   1.161 +        cache.string(abs_name),
   1.162 +        cache.string(axiom_name))
   1.163 +  }
   1.164  
   1.165    def read_typedefs(db: SQL.Database, session_name: String, theory_name: String): List[Typedef] =
   1.166      read_export(db, session_name, theory_name, "typedefs",