more abstract Export.Provider;
authorwenzelm
Mon Jun 11 18:05:43 2018 +0200 (13 months ago)
changeset 68418366e43cddd20
parent 68417 21465884037a
child 68419 a1f43b4f984d
more abstract Export.Provider;
src/Pure/Thy/export.scala
src/Pure/Thy/export_theory.scala
     1.1 --- a/src/Pure/Thy/export.scala	Mon Jun 11 17:37:44 2018 +0200
     1.2 +++ b/src/Pure/Thy/export.scala	Mon Jun 11 18:05:43 2018 +0200
     1.3 @@ -185,6 +185,35 @@
     1.4    }
     1.5  
     1.6  
     1.7 +  /* abstract provider */
     1.8 +
     1.9 +  object Provider
    1.10 +  {
    1.11 +    def database(db: SQL.Database, session_name: String, theory_name: String): Provider =
    1.12 +      new Provider {
    1.13 +        def apply(export_name: String): Option[Entry] =
    1.14 +          read_entry(db, session_name, theory_name, export_name)
    1.15 +      }
    1.16 +
    1.17 +    def snapshot(snapshot: Document.Snapshot): Provider =
    1.18 +      new Provider {
    1.19 +        def apply(export_name: String): Option[Entry] =
    1.20 +          snapshot.exports_map.get(export_name)
    1.21 +      }
    1.22 +  }
    1.23 +
    1.24 +  trait Provider
    1.25 +  {
    1.26 +    def apply(export_name: String): Option[Entry]
    1.27 +
    1.28 +    def uncompressed_yxml(export_name: String, cache: XZ.Cache = XZ.cache()): XML.Body =
    1.29 +      apply(export_name) match {
    1.30 +        case Some(entry) => entry.uncompressed_yxml(cache = cache)
    1.31 +        case None => Nil
    1.32 +      }
    1.33 +  }
    1.34 +
    1.35 +
    1.36    /* export to file-system */
    1.37  
    1.38    def export_files(
     2.1 --- a/src/Pure/Thy/export_theory.scala	Mon Jun 11 17:37:44 2018 +0200
     2.2 +++ b/src/Pure/Thy/export_theory.scala	Mon Jun 11 18:05:43 2018 +0200
     2.3 @@ -40,7 +40,8 @@
     2.4        {
     2.5          db.transaction {
     2.6            Export.read_theory_names(db, session_name).map((theory_name: String) =>
     2.7 -            read_theory(db, session_name, theory_name, types = types, consts = consts,
     2.8 +            read_theory(Export.Provider.database(db, session_name, theory_name),
     2.9 +              session_name, theory_name, types = types, consts = consts,
    2.10                axioms = axioms, facts = facts, classes = classes, typedefs = typedefs,
    2.11                cache = Some(cache)))
    2.12          }
    2.13 @@ -90,7 +91,7 @@
    2.14    def empty_theory(name: String): Theory =
    2.15      Theory(name, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil)
    2.16  
    2.17 -  def read_theory(db: SQL.Database, session_name: String, theory_name: String,
    2.18 +  def read_theory(provider: Export.Provider, session_name: String, theory_name: String,
    2.19      types: Boolean = true,
    2.20      consts: Boolean = true,
    2.21      axioms: Boolean = true,
    2.22 @@ -102,7 +103,7 @@
    2.23      cache: Option[Term.Cache] = None): Theory =
    2.24    {
    2.25      val parents =
    2.26 -      Export.read_entry(db, session_name, theory_name, export_prefix + "parents") match {
    2.27 +      provider(export_prefix + "parents") match {
    2.28          case Some(entry) => split_lines(entry.uncompressed().text)
    2.29          case None =>
    2.30            error("Missing theory export in session " + quote(session_name) + ": " +
    2.31 @@ -110,14 +111,14 @@
    2.32        }
    2.33      val theory =
    2.34        Theory(theory_name, parents,
    2.35 -        if (types) read_types(db, session_name, theory_name) else Nil,
    2.36 -        if (consts) read_consts(db, session_name, theory_name) else Nil,
    2.37 -        if (axioms) read_axioms(db, session_name, theory_name) else Nil,
    2.38 -        if (facts) read_facts(db, session_name, theory_name) else Nil,
    2.39 -        if (classes) read_classes(db, session_name, theory_name) else Nil,
    2.40 -        if (typedefs) read_typedefs(db, session_name, theory_name) else Nil,
    2.41 -        if (classrel) read_classrel(db, session_name, theory_name) else Nil,
    2.42 -        if (arities) read_arities(db, session_name, theory_name) else Nil)
    2.43 +        if (types) read_types(provider) else Nil,
    2.44 +        if (consts) read_consts(provider) else Nil,
    2.45 +        if (axioms) read_axioms(provider) else Nil,
    2.46 +        if (facts) read_facts(provider) else Nil,
    2.47 +        if (classes) read_classes(provider) else Nil,
    2.48 +        if (typedefs) read_typedefs(provider) else Nil,
    2.49 +        if (classrel) read_classrel(provider) else Nil,
    2.50 +        if (arities) read_arities(provider) else Nil)
    2.51      if (cache.isDefined) theory.cache(cache.get) else theory
    2.52    }
    2.53  
    2.54 @@ -146,22 +147,6 @@
    2.55      }
    2.56    }
    2.57  
    2.58 -  def read_export[A](db: SQL.Database, session_name: String, theory_name: String,
    2.59 -    export_name: String, decode: XML.Body => List[A]): List[A] =
    2.60 -  {
    2.61 -    Export.read_entry(db, session_name, theory_name, export_prefix + export_name) match {
    2.62 -      case Some(entry) => decode(entry.uncompressed_yxml())
    2.63 -      case None => Nil
    2.64 -    }
    2.65 -  }
    2.66 -
    2.67 -  def read_entities[A](db: SQL.Database, session_name: String, theory_name: String,
    2.68 -    export_name: String, decode: XML.Tree => A): List[A] =
    2.69 -  {
    2.70 -    read_export(db, session_name, theory_name, export_name,
    2.71 -      (body: XML.Body) => body.map(decode(_)))
    2.72 -  }
    2.73 -
    2.74  
    2.75    /* types */
    2.76  
    2.77 @@ -173,18 +158,17 @@
    2.78          abbrev.map(cache.typ(_)))
    2.79    }
    2.80  
    2.81 -  def read_types(db: SQL.Database, session_name: String, theory_name: String): List[Type] =
    2.82 -    read_entities(db, session_name, theory_name, "types",
    2.83 -      (tree: XML.Tree) =>
    2.84 +  def read_types(provider: Export.Provider): List[Type] =
    2.85 +    provider.uncompressed_yxml(export_prefix + "types").map((tree: XML.Tree) =>
    2.86 +      {
    2.87 +        val (entity, body) = decode_entity(tree)
    2.88 +        val (args, abbrev) =
    2.89          {
    2.90 -          val (entity, body) = decode_entity(tree)
    2.91 -          val (args, abbrev) =
    2.92 -          {
    2.93 -            import XML.Decode._
    2.94 -            pair(list(string), option(Term_XML.Decode.typ))(body)
    2.95 -          }
    2.96 -          Type(entity, args, abbrev)
    2.97 -        })
    2.98 +          import XML.Decode._
    2.99 +          pair(list(string), option(Term_XML.Decode.typ))(body)
   2.100 +        }
   2.101 +        Type(entity, args, abbrev)
   2.102 +      })
   2.103  
   2.104  
   2.105    /* consts */
   2.106 @@ -199,18 +183,17 @@
   2.107          abbrev.map(cache.term(_)))
   2.108    }
   2.109  
   2.110 -  def read_consts(db: SQL.Database, session_name: String, theory_name: String): List[Const] =
   2.111 -    read_entities(db, session_name, theory_name, "consts",
   2.112 -      (tree: XML.Tree) =>
   2.113 +  def read_consts(provider: Export.Provider): List[Const] =
   2.114 +    provider.uncompressed_yxml(export_prefix + "consts").map((tree: XML.Tree) =>
   2.115 +      {
   2.116 +        val (entity, body) = decode_entity(tree)
   2.117 +        val (args, typ, abbrev) =
   2.118          {
   2.119 -          val (entity, body) = decode_entity(tree)
   2.120 -          val (args, typ, abbrev) =
   2.121 -          {
   2.122 -            import XML.Decode._
   2.123 -            triple(list(string), Term_XML.Decode.typ, option(Term_XML.Decode.term))(body)
   2.124 -          }
   2.125 -          Const(entity, args, typ, abbrev)
   2.126 -        })
   2.127 +          import XML.Decode._
   2.128 +          triple(list(string), Term_XML.Decode.typ, option(Term_XML.Decode.term))(body)
   2.129 +        }
   2.130 +        Const(entity, args, typ, abbrev)
   2.131 +      })
   2.132  
   2.133  
   2.134    /* axioms and facts */
   2.135 @@ -236,14 +219,13 @@
   2.136          cache.term(prop))
   2.137    }
   2.138  
   2.139 -  def read_axioms(db: SQL.Database, session_name: String, theory_name: String): List[Axiom] =
   2.140 -    read_entities(db, session_name, theory_name, "axioms",
   2.141 -      (tree: XML.Tree) =>
   2.142 -        {
   2.143 -          val (entity, body) = decode_entity(tree)
   2.144 -          val (typargs, args, List(prop)) = decode_props(body)
   2.145 -          Axiom(entity, typargs, args, prop)
   2.146 -        })
   2.147 +  def read_axioms(provider: Export.Provider): List[Axiom] =
   2.148 +    provider.uncompressed_yxml(export_prefix + "axioms").map((tree: XML.Tree) =>
   2.149 +      {
   2.150 +        val (entity, body) = decode_entity(tree)
   2.151 +        val (typargs, args, List(prop)) = decode_props(body)
   2.152 +        Axiom(entity, typargs, args, prop)
   2.153 +      })
   2.154  
   2.155    sealed case class Fact(
   2.156      entity: Entity,
   2.157 @@ -258,14 +240,13 @@
   2.158          props.map(cache.term(_)))
   2.159    }
   2.160  
   2.161 -  def read_facts(db: SQL.Database, session_name: String, theory_name: String): List[Fact] =
   2.162 -    read_entities(db, session_name, theory_name, "facts",
   2.163 -      (tree: XML.Tree) =>
   2.164 -        {
   2.165 -          val (entity, body) = decode_entity(tree)
   2.166 -          val (typargs, args, props) = decode_props(body)
   2.167 -          Fact(entity, typargs, args, props)
   2.168 -        })
   2.169 +  def read_facts(provider: Export.Provider): List[Fact] =
   2.170 +    provider.uncompressed_yxml(export_prefix + "facts").map((tree: XML.Tree) =>
   2.171 +      {
   2.172 +        val (entity, body) = decode_entity(tree)
   2.173 +        val (typargs, args, props) = decode_props(body)
   2.174 +        Fact(entity, typargs, args, props)
   2.175 +      })
   2.176  
   2.177  
   2.178    /* type classes */
   2.179 @@ -279,19 +260,18 @@
   2.180          axioms.map(cache.term(_)))
   2.181    }
   2.182  
   2.183 -  def read_classes(db: SQL.Database, session_name: String, theory_name: String): List[Class] =
   2.184 -    read_entities(db, session_name, theory_name, "classes",
   2.185 -      (tree: XML.Tree) =>
   2.186 +  def read_classes(provider: Export.Provider): List[Class] =
   2.187 +    provider.uncompressed_yxml(export_prefix + "classes").map((tree: XML.Tree) =>
   2.188 +      {
   2.189 +        val (entity, body) = decode_entity(tree)
   2.190 +        val (params, axioms) =
   2.191          {
   2.192 -          val (entity, body) = decode_entity(tree)
   2.193 -          val (params, axioms) =
   2.194 -          {
   2.195 -            import XML.Decode._
   2.196 -            import Term_XML.Decode._
   2.197 -            pair(list(pair(string, typ)), list(term))(body)
   2.198 -          }
   2.199 -          Class(entity, params, axioms)
   2.200 -        })
   2.201 +          import XML.Decode._
   2.202 +          import Term_XML.Decode._
   2.203 +          pair(list(pair(string, typ)), list(term))(body)
   2.204 +        }
   2.205 +        Class(entity, params, axioms)
   2.206 +      })
   2.207  
   2.208  
   2.209    /* sort algebra */
   2.210 @@ -302,17 +282,16 @@
   2.211        Classrel(cache.string(class_name), super_names.map(cache.string(_)))
   2.212    }
   2.213  
   2.214 -  def read_classrel(db: SQL.Database, session_name: String, theory_name: String): List[Classrel] =
   2.215 -    read_export(db, session_name, theory_name, "classrel",
   2.216 -      (body: XML.Body) =>
   2.217 -        {
   2.218 -          val classrel =
   2.219 -          {
   2.220 -            import XML.Decode._
   2.221 -            list(pair(string, list(string)))(body)
   2.222 -          }
   2.223 -          for ((c, cs) <- classrel) yield Classrel(c, cs)
   2.224 -        })
   2.225 +  def read_classrel(provider: Export.Provider): List[Classrel] =
   2.226 +  {
   2.227 +    val body = provider.uncompressed_yxml(export_prefix + "classrel")
   2.228 +    val classrel =
   2.229 +    {
   2.230 +      import XML.Decode._
   2.231 +      list(pair(string, list(string)))(body)
   2.232 +    }
   2.233 +    for ((c, cs) <- classrel) yield Classrel(c, cs)
   2.234 +  }
   2.235  
   2.236    sealed case class Arity(type_name: String, domain: List[Term.Sort], codomain: String)
   2.237    {
   2.238 @@ -320,18 +299,17 @@
   2.239        Arity(cache.string(type_name), domain.map(cache.sort(_)), cache.string(codomain))
   2.240    }
   2.241  
   2.242 -  def read_arities(db: SQL.Database, session_name: String, theory_name: String): List[Arity] =
   2.243 -    read_export(db, session_name, theory_name, "arities",
   2.244 -      (body: XML.Body) =>
   2.245 -        {
   2.246 -          val arities =
   2.247 -          {
   2.248 -            import XML.Decode._
   2.249 -            import Term_XML.Decode._
   2.250 -            list(triple(string, list(sort), string))(body)
   2.251 -          }
   2.252 -          for ((a, b, c) <- arities) yield Arity(a, b, c)
   2.253 -        })
   2.254 +  def read_arities(provider: Export.Provider): List[Arity] =
   2.255 +  {
   2.256 +    val body = provider.uncompressed_yxml(export_prefix + "arities")
   2.257 +    val arities =
   2.258 +    {
   2.259 +      import XML.Decode._
   2.260 +      import Term_XML.Decode._
   2.261 +      list(triple(string, list(sort), string))(body)
   2.262 +    }
   2.263 +    for ((a, b, c) <- arities) yield Arity(a, b, c)
   2.264 +  }
   2.265  
   2.266  
   2.267    /* HOL typedefs */
   2.268 @@ -348,17 +326,16 @@
   2.269          cache.string(axiom_name))
   2.270    }
   2.271  
   2.272 -  def read_typedefs(db: SQL.Database, session_name: String, theory_name: String): List[Typedef] =
   2.273 -    read_export(db, session_name, theory_name, "typedefs",
   2.274 -      (body: XML.Body) =>
   2.275 -        {
   2.276 -          val typedefs =
   2.277 -          {
   2.278 -            import XML.Decode._
   2.279 -            import Term_XML.Decode._
   2.280 -            list(pair(string, pair(typ, pair(typ, pair(string, pair(string, string))))))(body)
   2.281 -          }
   2.282 -          for { (name, (rep_type, (abs_type, (rep_name, (abs_name, axiom_name))))) <- typedefs }
   2.283 -          yield Typedef(name, rep_type, abs_type, rep_name, abs_name, axiom_name)
   2.284 -        })
   2.285 +  def read_typedefs(provider: Export.Provider): List[Typedef] =
   2.286 +  {
   2.287 +    val body = provider.uncompressed_yxml(export_prefix + "typedefs")
   2.288 +    val typedefs =
   2.289 +    {
   2.290 +      import XML.Decode._
   2.291 +      import Term_XML.Decode._
   2.292 +      list(pair(string, pair(typ, pair(typ, pair(string, pair(string, string))))))(body)
   2.293 +    }
   2.294 +    for { (name, (rep_type, (abs_type, (rep_name, (abs_name, axiom_name))))) <- typedefs }
   2.295 +    yield Typedef(name, rep_type, abs_type, rep_name, abs_name, axiom_name)
   2.296 +  }
   2.297  }