src/Pure/Thy/export_theory.scala
changeset 68418 366e43cddd20
parent 68346 b44010800a19
child 68710 3db37e950118
     1.1 --- a/src/Pure/Thy/export_theory.scala	Mon Jun 11 17:37:44 2018 +0200
     1.2 +++ b/src/Pure/Thy/export_theory.scala	Mon Jun 11 18:05:43 2018 +0200
     1.3 @@ -40,7 +40,8 @@
     1.4        {
     1.5          db.transaction {
     1.6            Export.read_theory_names(db, session_name).map((theory_name: String) =>
     1.7 -            read_theory(db, session_name, theory_name, types = types, consts = consts,
     1.8 +            read_theory(Export.Provider.database(db, session_name, theory_name),
     1.9 +              session_name, theory_name, types = types, consts = consts,
    1.10                axioms = axioms, facts = facts, classes = classes, typedefs = typedefs,
    1.11                cache = Some(cache)))
    1.12          }
    1.13 @@ -90,7 +91,7 @@
    1.14    def empty_theory(name: String): Theory =
    1.15      Theory(name, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil)
    1.16  
    1.17 -  def read_theory(db: SQL.Database, session_name: String, theory_name: String,
    1.18 +  def read_theory(provider: Export.Provider, session_name: String, theory_name: String,
    1.19      types: Boolean = true,
    1.20      consts: Boolean = true,
    1.21      axioms: Boolean = true,
    1.22 @@ -102,7 +103,7 @@
    1.23      cache: Option[Term.Cache] = None): Theory =
    1.24    {
    1.25      val parents =
    1.26 -      Export.read_entry(db, session_name, theory_name, export_prefix + "parents") match {
    1.27 +      provider(export_prefix + "parents") match {
    1.28          case Some(entry) => split_lines(entry.uncompressed().text)
    1.29          case None =>
    1.30            error("Missing theory export in session " + quote(session_name) + ": " +
    1.31 @@ -110,14 +111,14 @@
    1.32        }
    1.33      val theory =
    1.34        Theory(theory_name, parents,
    1.35 -        if (types) read_types(db, session_name, theory_name) else Nil,
    1.36 -        if (consts) read_consts(db, session_name, theory_name) else Nil,
    1.37 -        if (axioms) read_axioms(db, session_name, theory_name) else Nil,
    1.38 -        if (facts) read_facts(db, session_name, theory_name) else Nil,
    1.39 -        if (classes) read_classes(db, session_name, theory_name) else Nil,
    1.40 -        if (typedefs) read_typedefs(db, session_name, theory_name) else Nil,
    1.41 -        if (classrel) read_classrel(db, session_name, theory_name) else Nil,
    1.42 -        if (arities) read_arities(db, session_name, theory_name) else Nil)
    1.43 +        if (types) read_types(provider) else Nil,
    1.44 +        if (consts) read_consts(provider) else Nil,
    1.45 +        if (axioms) read_axioms(provider) else Nil,
    1.46 +        if (facts) read_facts(provider) else Nil,
    1.47 +        if (classes) read_classes(provider) else Nil,
    1.48 +        if (typedefs) read_typedefs(provider) else Nil,
    1.49 +        if (classrel) read_classrel(provider) else Nil,
    1.50 +        if (arities) read_arities(provider) else Nil)
    1.51      if (cache.isDefined) theory.cache(cache.get) else theory
    1.52    }
    1.53  
    1.54 @@ -146,22 +147,6 @@
    1.55      }
    1.56    }
    1.57  
    1.58 -  def read_export[A](db: SQL.Database, session_name: String, theory_name: String,
    1.59 -    export_name: String, decode: XML.Body => List[A]): List[A] =
    1.60 -  {
    1.61 -    Export.read_entry(db, session_name, theory_name, export_prefix + export_name) match {
    1.62 -      case Some(entry) => decode(entry.uncompressed_yxml())
    1.63 -      case None => Nil
    1.64 -    }
    1.65 -  }
    1.66 -
    1.67 -  def read_entities[A](db: SQL.Database, session_name: String, theory_name: String,
    1.68 -    export_name: String, decode: XML.Tree => A): List[A] =
    1.69 -  {
    1.70 -    read_export(db, session_name, theory_name, export_name,
    1.71 -      (body: XML.Body) => body.map(decode(_)))
    1.72 -  }
    1.73 -
    1.74  
    1.75    /* types */
    1.76  
    1.77 @@ -173,18 +158,17 @@
    1.78          abbrev.map(cache.typ(_)))
    1.79    }
    1.80  
    1.81 -  def read_types(db: SQL.Database, session_name: String, theory_name: String): List[Type] =
    1.82 -    read_entities(db, session_name, theory_name, "types",
    1.83 -      (tree: XML.Tree) =>
    1.84 +  def read_types(provider: Export.Provider): List[Type] =
    1.85 +    provider.uncompressed_yxml(export_prefix + "types").map((tree: XML.Tree) =>
    1.86 +      {
    1.87 +        val (entity, body) = decode_entity(tree)
    1.88 +        val (args, abbrev) =
    1.89          {
    1.90 -          val (entity, body) = decode_entity(tree)
    1.91 -          val (args, abbrev) =
    1.92 -          {
    1.93 -            import XML.Decode._
    1.94 -            pair(list(string), option(Term_XML.Decode.typ))(body)
    1.95 -          }
    1.96 -          Type(entity, args, abbrev)
    1.97 -        })
    1.98 +          import XML.Decode._
    1.99 +          pair(list(string), option(Term_XML.Decode.typ))(body)
   1.100 +        }
   1.101 +        Type(entity, args, abbrev)
   1.102 +      })
   1.103  
   1.104  
   1.105    /* consts */
   1.106 @@ -199,18 +183,17 @@
   1.107          abbrev.map(cache.term(_)))
   1.108    }
   1.109  
   1.110 -  def read_consts(db: SQL.Database, session_name: String, theory_name: String): List[Const] =
   1.111 -    read_entities(db, session_name, theory_name, "consts",
   1.112 -      (tree: XML.Tree) =>
   1.113 +  def read_consts(provider: Export.Provider): List[Const] =
   1.114 +    provider.uncompressed_yxml(export_prefix + "consts").map((tree: XML.Tree) =>
   1.115 +      {
   1.116 +        val (entity, body) = decode_entity(tree)
   1.117 +        val (args, typ, abbrev) =
   1.118          {
   1.119 -          val (entity, body) = decode_entity(tree)
   1.120 -          val (args, typ, abbrev) =
   1.121 -          {
   1.122 -            import XML.Decode._
   1.123 -            triple(list(string), Term_XML.Decode.typ, option(Term_XML.Decode.term))(body)
   1.124 -          }
   1.125 -          Const(entity, args, typ, abbrev)
   1.126 -        })
   1.127 +          import XML.Decode._
   1.128 +          triple(list(string), Term_XML.Decode.typ, option(Term_XML.Decode.term))(body)
   1.129 +        }
   1.130 +        Const(entity, args, typ, abbrev)
   1.131 +      })
   1.132  
   1.133  
   1.134    /* axioms and facts */
   1.135 @@ -236,14 +219,13 @@
   1.136          cache.term(prop))
   1.137    }
   1.138  
   1.139 -  def read_axioms(db: SQL.Database, session_name: String, theory_name: String): List[Axiom] =
   1.140 -    read_entities(db, session_name, theory_name, "axioms",
   1.141 -      (tree: XML.Tree) =>
   1.142 -        {
   1.143 -          val (entity, body) = decode_entity(tree)
   1.144 -          val (typargs, args, List(prop)) = decode_props(body)
   1.145 -          Axiom(entity, typargs, args, prop)
   1.146 -        })
   1.147 +  def read_axioms(provider: Export.Provider): List[Axiom] =
   1.148 +    provider.uncompressed_yxml(export_prefix + "axioms").map((tree: XML.Tree) =>
   1.149 +      {
   1.150 +        val (entity, body) = decode_entity(tree)
   1.151 +        val (typargs, args, List(prop)) = decode_props(body)
   1.152 +        Axiom(entity, typargs, args, prop)
   1.153 +      })
   1.154  
   1.155    sealed case class Fact(
   1.156      entity: Entity,
   1.157 @@ -258,14 +240,13 @@
   1.158          props.map(cache.term(_)))
   1.159    }
   1.160  
   1.161 -  def read_facts(db: SQL.Database, session_name: String, theory_name: String): List[Fact] =
   1.162 -    read_entities(db, session_name, theory_name, "facts",
   1.163 -      (tree: XML.Tree) =>
   1.164 -        {
   1.165 -          val (entity, body) = decode_entity(tree)
   1.166 -          val (typargs, args, props) = decode_props(body)
   1.167 -          Fact(entity, typargs, args, props)
   1.168 -        })
   1.169 +  def read_facts(provider: Export.Provider): List[Fact] =
   1.170 +    provider.uncompressed_yxml(export_prefix + "facts").map((tree: XML.Tree) =>
   1.171 +      {
   1.172 +        val (entity, body) = decode_entity(tree)
   1.173 +        val (typargs, args, props) = decode_props(body)
   1.174 +        Fact(entity, typargs, args, props)
   1.175 +      })
   1.176  
   1.177  
   1.178    /* type classes */
   1.179 @@ -279,19 +260,18 @@
   1.180          axioms.map(cache.term(_)))
   1.181    }
   1.182  
   1.183 -  def read_classes(db: SQL.Database, session_name: String, theory_name: String): List[Class] =
   1.184 -    read_entities(db, session_name, theory_name, "classes",
   1.185 -      (tree: XML.Tree) =>
   1.186 +  def read_classes(provider: Export.Provider): List[Class] =
   1.187 +    provider.uncompressed_yxml(export_prefix + "classes").map((tree: XML.Tree) =>
   1.188 +      {
   1.189 +        val (entity, body) = decode_entity(tree)
   1.190 +        val (params, axioms) =
   1.191          {
   1.192 -          val (entity, body) = decode_entity(tree)
   1.193 -          val (params, axioms) =
   1.194 -          {
   1.195 -            import XML.Decode._
   1.196 -            import Term_XML.Decode._
   1.197 -            pair(list(pair(string, typ)), list(term))(body)
   1.198 -          }
   1.199 -          Class(entity, params, axioms)
   1.200 -        })
   1.201 +          import XML.Decode._
   1.202 +          import Term_XML.Decode._
   1.203 +          pair(list(pair(string, typ)), list(term))(body)
   1.204 +        }
   1.205 +        Class(entity, params, axioms)
   1.206 +      })
   1.207  
   1.208  
   1.209    /* sort algebra */
   1.210 @@ -302,17 +282,16 @@
   1.211        Classrel(cache.string(class_name), super_names.map(cache.string(_)))
   1.212    }
   1.213  
   1.214 -  def read_classrel(db: SQL.Database, session_name: String, theory_name: String): List[Classrel] =
   1.215 -    read_export(db, session_name, theory_name, "classrel",
   1.216 -      (body: XML.Body) =>
   1.217 -        {
   1.218 -          val classrel =
   1.219 -          {
   1.220 -            import XML.Decode._
   1.221 -            list(pair(string, list(string)))(body)
   1.222 -          }
   1.223 -          for ((c, cs) <- classrel) yield Classrel(c, cs)
   1.224 -        })
   1.225 +  def read_classrel(provider: Export.Provider): List[Classrel] =
   1.226 +  {
   1.227 +    val body = provider.uncompressed_yxml(export_prefix + "classrel")
   1.228 +    val classrel =
   1.229 +    {
   1.230 +      import XML.Decode._
   1.231 +      list(pair(string, list(string)))(body)
   1.232 +    }
   1.233 +    for ((c, cs) <- classrel) yield Classrel(c, cs)
   1.234 +  }
   1.235  
   1.236    sealed case class Arity(type_name: String, domain: List[Term.Sort], codomain: String)
   1.237    {
   1.238 @@ -320,18 +299,17 @@
   1.239        Arity(cache.string(type_name), domain.map(cache.sort(_)), cache.string(codomain))
   1.240    }
   1.241  
   1.242 -  def read_arities(db: SQL.Database, session_name: String, theory_name: String): List[Arity] =
   1.243 -    read_export(db, session_name, theory_name, "arities",
   1.244 -      (body: XML.Body) =>
   1.245 -        {
   1.246 -          val arities =
   1.247 -          {
   1.248 -            import XML.Decode._
   1.249 -            import Term_XML.Decode._
   1.250 -            list(triple(string, list(sort), string))(body)
   1.251 -          }
   1.252 -          for ((a, b, c) <- arities) yield Arity(a, b, c)
   1.253 -        })
   1.254 +  def read_arities(provider: Export.Provider): List[Arity] =
   1.255 +  {
   1.256 +    val body = provider.uncompressed_yxml(export_prefix + "arities")
   1.257 +    val arities =
   1.258 +    {
   1.259 +      import XML.Decode._
   1.260 +      import Term_XML.Decode._
   1.261 +      list(triple(string, list(sort), string))(body)
   1.262 +    }
   1.263 +    for ((a, b, c) <- arities) yield Arity(a, b, c)
   1.264 +  }
   1.265  
   1.266  
   1.267    /* HOL typedefs */
   1.268 @@ -348,17 +326,16 @@
   1.269          cache.string(axiom_name))
   1.270    }
   1.271  
   1.272 -  def read_typedefs(db: SQL.Database, session_name: String, theory_name: String): List[Typedef] =
   1.273 -    read_export(db, session_name, theory_name, "typedefs",
   1.274 -      (body: XML.Body) =>
   1.275 -        {
   1.276 -          val typedefs =
   1.277 -          {
   1.278 -            import XML.Decode._
   1.279 -            import Term_XML.Decode._
   1.280 -            list(pair(string, pair(typ, pair(typ, pair(string, pair(string, string))))))(body)
   1.281 -          }
   1.282 -          for { (name, (rep_type, (abs_type, (rep_name, (abs_name, axiom_name))))) <- typedefs }
   1.283 -          yield Typedef(name, rep_type, abs_type, rep_name, abs_name, axiom_name)
   1.284 -        })
   1.285 +  def read_typedefs(provider: Export.Provider): List[Typedef] =
   1.286 +  {
   1.287 +    val body = provider.uncompressed_yxml(export_prefix + "typedefs")
   1.288 +    val typedefs =
   1.289 +    {
   1.290 +      import XML.Decode._
   1.291 +      import Term_XML.Decode._
   1.292 +      list(pair(string, pair(typ, pair(typ, pair(string, pair(string, string))))))(body)
   1.293 +    }
   1.294 +    for { (name, (rep_type, (abs_type, (rep_name, (abs_name, axiom_name))))) <- typedefs }
   1.295 +    yield Typedef(name, rep_type, abs_type, rep_name, abs_name, axiom_name)
   1.296 +  }
   1.297  }