src/Pure/Thy/export_theory.scala
changeset 68264 bb9a3be6952a
parent 68232 4b93573ac5b4
child 68267 6a29709906c6
     1.1 --- a/src/Pure/Thy/export_theory.scala	Thu May 24 09:18:29 2018 +0200
     1.2 +++ b/src/Pure/Thy/export_theory.scala	Thu May 24 16:56:14 2018 +0200
     1.3 @@ -26,14 +26,19 @@
     1.4    def read_session(store: Sessions.Store,
     1.5      session_name: String,
     1.6      types: Boolean = true,
     1.7 -    consts: Boolean = true): Session =
     1.8 +    consts: Boolean = true,
     1.9 +    axioms: Boolean = true,
    1.10 +    facts: Boolean = true,
    1.11 +    classes: Boolean = true,
    1.12 +    typedefs: Boolean = true): Session =
    1.13    {
    1.14      val thys =
    1.15        using(store.open_database(session_name))(db =>
    1.16        {
    1.17          db.transaction {
    1.18            Export.read_theory_names(db, session_name).map((theory_name: String) =>
    1.19 -            read_theory(db, session_name, theory_name, types = types, consts = consts))
    1.20 +            read_theory(db, session_name, theory_name, types = types, consts = consts,
    1.21 +              axioms = axioms, facts = facts, classes = classes, typedefs = typedefs))
    1.22          }
    1.23        })
    1.24  
    1.25 @@ -55,18 +60,22 @@
    1.26      types: List[Type],
    1.27      consts: List[Const],
    1.28      axioms: List[Axiom],
    1.29 -    facts: List[Fact])
    1.30 +    facts: List[Fact],
    1.31 +    classes: List[Class],
    1.32 +    typedefs: List[Typedef])
    1.33    {
    1.34      override def toString: String = name
    1.35    }
    1.36  
    1.37 -  def empty_theory(name: String): Theory = Theory(name, Nil, Nil, Nil, Nil, Nil)
    1.38 +  def empty_theory(name: String): Theory = Theory(name, Nil, Nil, Nil, Nil, Nil, Nil, Nil)
    1.39  
    1.40    def read_theory(db: SQL.Database, session_name: String, theory_name: String,
    1.41      types: Boolean = true,
    1.42      consts: Boolean = true,
    1.43      axioms: Boolean = true,
    1.44 -    facts: Boolean = true): Theory =
    1.45 +    facts: Boolean = true,
    1.46 +    classes: Boolean = true,
    1.47 +    typedefs: Boolean = true): Theory =
    1.48    {
    1.49      val parents =
    1.50        Export.read_entry(db, session_name, theory_name, "theory/parents") match {
    1.51 @@ -79,7 +88,9 @@
    1.52        if (types) read_types(db, session_name, theory_name) else Nil,
    1.53        if (consts) read_consts(db, session_name, theory_name) else Nil,
    1.54        if (axioms) read_axioms(db, session_name, theory_name) else Nil,
    1.55 -      if (facts) read_facts(db, session_name, theory_name) else Nil)
    1.56 +      if (facts) read_facts(db, session_name, theory_name) else Nil,
    1.57 +      if (classes) read_classes(db, session_name, theory_name) else Nil,
    1.58 +      if (typedefs) read_typedefs(db, session_name, theory_name) else Nil)
    1.59    }
    1.60  
    1.61  
    1.62 @@ -104,13 +115,20 @@
    1.63      }
    1.64    }
    1.65  
    1.66 +  def read_export[A](db: SQL.Database, session_name: String, theory_name: String,
    1.67 +    export_name: String, decode: XML.Body => List[A]): List[A] =
    1.68 +  {
    1.69 +    Export.read_entry(db, session_name, theory_name, "theory/" + export_name) match {
    1.70 +      case Some(entry) => decode(entry.uncompressed_yxml())
    1.71 +      case None => Nil
    1.72 +    }
    1.73 +  }
    1.74 +
    1.75    def read_entities[A](db: SQL.Database, session_name: String, theory_name: String,
    1.76      export_name: String, decode: XML.Tree => A): List[A] =
    1.77    {
    1.78 -    Export.read_entry(db, session_name, theory_name, "theory/" + export_name) match {
    1.79 -      case Some(entry) => entry.uncompressed_yxml().map(decode(_))
    1.80 -      case None => Nil
    1.81 -    }
    1.82 +    read_export(db, session_name, theory_name, export_name,
    1.83 +      (body: XML.Body) => body.map(decode(_)))
    1.84    }
    1.85  
    1.86  
    1.87 @@ -190,4 +208,44 @@
    1.88            val (typargs, args, props) = decode_props(body)
    1.89            Fact(entity, typargs, args, props)
    1.90          })
    1.91 +
    1.92 +
    1.93 +  /* type classes */
    1.94 +
    1.95 +  sealed case class Class(
    1.96 +    entity: Entity, params: List[(String, Term.Typ)], axioms: List[Term.Term])
    1.97 +
    1.98 +  def read_classes(db: SQL.Database, session_name: String, theory_name: String): List[Class] =
    1.99 +    read_entities(db, session_name, theory_name, "classes",
   1.100 +      (tree: XML.Tree) =>
   1.101 +        {
   1.102 +          val (entity, body) = decode_entity(tree)
   1.103 +          val (params, axioms) =
   1.104 +          {
   1.105 +            import XML.Decode._
   1.106 +            import Term_XML.Decode._
   1.107 +            pair(list(pair(string, typ)), list(term))(body)
   1.108 +          }
   1.109 +          Class(entity, params, axioms)
   1.110 +        })
   1.111 +
   1.112 +
   1.113 +  /* HOL typedefs */
   1.114 +
   1.115 +  sealed case class Typedef(name: String,
   1.116 +    rep_type: Term.Typ, abs_type: Term.Typ, rep_name: String, abs_name: String, axiom_name: String)
   1.117 +
   1.118 +  def read_typedefs(db: SQL.Database, session_name: String, theory_name: String): List[Typedef] =
   1.119 +    read_export(db, session_name, theory_name, "typedefs",
   1.120 +      (body: XML.Body) =>
   1.121 +        {
   1.122 +          val typedefs =
   1.123 +          {
   1.124 +            import XML.Decode._
   1.125 +            import Term_XML.Decode._
   1.126 +            list(pair(string, pair(typ, pair(typ, pair(string, pair(string, string))))))(body)
   1.127 +          }
   1.128 +          for { (name, (rep_type, (abs_type, (rep_name, (abs_name, axiom_name))))) <- typedefs }
   1.129 +          yield Typedef(name, rep_type, abs_type, rep_name, abs_name, axiom_name)
   1.130 +        })
   1.131  }