more exports;
authorwenzelm
Thu May 24 16:56:14 2018 +0200 (14 months ago)
changeset 68264bb9a3be6952a
parent 68260 61188c781cdd
child 68265 f0899dad4877
more exports;
read_session: proper signature;
src/HOL/Tools/typedef.ML
src/Pure/Thy/export_theory.ML
src/Pure/Thy/export_theory.scala
     1.1 --- a/src/HOL/Tools/typedef.ML	Thu May 24 09:18:29 2018 +0200
     1.2 +++ b/src/HOL/Tools/typedef.ML	Thu May 24 16:56:14 2018 +0200
     1.3 @@ -348,4 +348,27 @@
     1.4  
     1.5  val overloaded = typedef_overloaded;
     1.6  
     1.7 +
     1.8 +
     1.9 +(** theory export **)
    1.10 +
    1.11 +val _ = Export_Theory.setup_presentation (fn _ => fn thy =>
    1.12 +  let
    1.13 +    val parent_spaces = map Sign.type_space (Theory.parents_of thy);
    1.14 +    val typedefs =
    1.15 +      Name_Space.dest_table (#types (Type.rep_tsig (Sign.tsig_of thy)))
    1.16 +      |> maps (fn (name, _) =>
    1.17 +          if exists (fn space => Name_Space.declared space name) parent_spaces then []
    1.18 +          else
    1.19 +            get_info_global thy name
    1.20 +            |> map (fn ({rep_type, abs_type, Rep_name, Abs_name, axiom_name}, _) =>
    1.21 +              (name, (rep_type, (abs_type, (Rep_name, (Abs_name, axiom_name)))))));
    1.22 +  in
    1.23 +    if null typedefs then ()
    1.24 +    else
    1.25 +      Export_Theory.export_body thy "typedefs"
    1.26 +        let open XML.Encode Term_XML.Encode
    1.27 +        in list (pair string (pair typ (pair typ (pair string (pair string string))))) typedefs end
    1.28 +  end);
    1.29 +
    1.30  end;
     2.1 --- a/src/Pure/Thy/export_theory.ML	Thu May 24 09:18:29 2018 +0200
     2.2 +++ b/src/Pure/Thy/export_theory.ML	Thu May 24 16:56:14 2018 +0200
     2.3 @@ -27,6 +27,9 @@
     2.4  
     2.5  val _ = setup_presentation (fn {adjust_pos, ...} => fn thy =>
     2.6    let
     2.7 +    val rep_tsig = Type.rep_tsig (Sign.tsig_of thy);
     2.8 +
     2.9 +
    2.10      (* parents *)
    2.11  
    2.12      val parents = Theory.parents_of thy;
    2.13 @@ -76,7 +79,7 @@
    2.14  
    2.15      val _ =
    2.16        export_entities "types" (K export_type) Sign.type_space
    2.17 -        (Name_Space.dest_table (#types (Type.rep_tsig (Sign.tsig_of thy))));
    2.18 +        (Name_Space.dest_table (#types rep_tsig));
    2.19  
    2.20  
    2.21      (* consts *)
    2.22 @@ -120,6 +123,24 @@
    2.23        export_entities "facts" (K (SOME o export_fact)) (Facts.space_of o Global_Theory.facts_of)
    2.24          (Facts.dest_static true [] (Global_Theory.facts_of thy));
    2.25  
    2.26 +
    2.27 +    (* type classes *)
    2.28 +
    2.29 +    val encode_class =
    2.30 +      let open XML.Encode Term_XML.Encode
    2.31 +      in pair (list (pair string typ)) (list term) end;
    2.32 +
    2.33 +    fun export_class name =
    2.34 +      (case try (Axclass.get_info thy) name of
    2.35 +        NONE => ([], [])
    2.36 +      | SOME {params, axioms, ...} =>
    2.37 +          (params, map (Logic.unvarify_global o Thm.full_prop_of) axioms))
    2.38 +      |> encode_class |> SOME;
    2.39 +
    2.40 +    val _ =
    2.41 +      export_entities "classes" (fn name => fn () => export_class name)
    2.42 +        Sign.class_space (map (rpair ()) (Graph.keys (Sorts.classes_of (#2 (#classes rep_tsig)))));
    2.43 +
    2.44      in () end);
    2.45  
    2.46  end;
     3.1 --- a/src/Pure/Thy/export_theory.scala	Thu May 24 09:18:29 2018 +0200
     3.2 +++ b/src/Pure/Thy/export_theory.scala	Thu May 24 16:56:14 2018 +0200
     3.3 @@ -26,14 +26,19 @@
     3.4    def read_session(store: Sessions.Store,
     3.5      session_name: String,
     3.6      types: Boolean = true,
     3.7 -    consts: Boolean = true): Session =
     3.8 +    consts: Boolean = true,
     3.9 +    axioms: Boolean = true,
    3.10 +    facts: Boolean = true,
    3.11 +    classes: Boolean = true,
    3.12 +    typedefs: Boolean = true): Session =
    3.13    {
    3.14      val thys =
    3.15        using(store.open_database(session_name))(db =>
    3.16        {
    3.17          db.transaction {
    3.18            Export.read_theory_names(db, session_name).map((theory_name: String) =>
    3.19 -            read_theory(db, session_name, theory_name, types = types, consts = consts))
    3.20 +            read_theory(db, session_name, theory_name, types = types, consts = consts,
    3.21 +              axioms = axioms, facts = facts, classes = classes, typedefs = typedefs))
    3.22          }
    3.23        })
    3.24  
    3.25 @@ -55,18 +60,22 @@
    3.26      types: List[Type],
    3.27      consts: List[Const],
    3.28      axioms: List[Axiom],
    3.29 -    facts: List[Fact])
    3.30 +    facts: List[Fact],
    3.31 +    classes: List[Class],
    3.32 +    typedefs: List[Typedef])
    3.33    {
    3.34      override def toString: String = name
    3.35    }
    3.36  
    3.37 -  def empty_theory(name: String): Theory = Theory(name, Nil, Nil, Nil, Nil, Nil)
    3.38 +  def empty_theory(name: String): Theory = Theory(name, Nil, Nil, Nil, Nil, Nil, Nil, Nil)
    3.39  
    3.40    def read_theory(db: SQL.Database, session_name: String, theory_name: String,
    3.41      types: Boolean = true,
    3.42      consts: Boolean = true,
    3.43      axioms: Boolean = true,
    3.44 -    facts: Boolean = true): Theory =
    3.45 +    facts: Boolean = true,
    3.46 +    classes: Boolean = true,
    3.47 +    typedefs: Boolean = true): Theory =
    3.48    {
    3.49      val parents =
    3.50        Export.read_entry(db, session_name, theory_name, "theory/parents") match {
    3.51 @@ -79,7 +88,9 @@
    3.52        if (types) read_types(db, session_name, theory_name) else Nil,
    3.53        if (consts) read_consts(db, session_name, theory_name) else Nil,
    3.54        if (axioms) read_axioms(db, session_name, theory_name) else Nil,
    3.55 -      if (facts) read_facts(db, session_name, theory_name) else Nil)
    3.56 +      if (facts) read_facts(db, session_name, theory_name) else Nil,
    3.57 +      if (classes) read_classes(db, session_name, theory_name) else Nil,
    3.58 +      if (typedefs) read_typedefs(db, session_name, theory_name) else Nil)
    3.59    }
    3.60  
    3.61  
    3.62 @@ -104,13 +115,20 @@
    3.63      }
    3.64    }
    3.65  
    3.66 +  def read_export[A](db: SQL.Database, session_name: String, theory_name: String,
    3.67 +    export_name: String, decode: XML.Body => List[A]): List[A] =
    3.68 +  {
    3.69 +    Export.read_entry(db, session_name, theory_name, "theory/" + export_name) match {
    3.70 +      case Some(entry) => decode(entry.uncompressed_yxml())
    3.71 +      case None => Nil
    3.72 +    }
    3.73 +  }
    3.74 +
    3.75    def read_entities[A](db: SQL.Database, session_name: String, theory_name: String,
    3.76      export_name: String, decode: XML.Tree => A): List[A] =
    3.77    {
    3.78 -    Export.read_entry(db, session_name, theory_name, "theory/" + export_name) match {
    3.79 -      case Some(entry) => entry.uncompressed_yxml().map(decode(_))
    3.80 -      case None => Nil
    3.81 -    }
    3.82 +    read_export(db, session_name, theory_name, export_name,
    3.83 +      (body: XML.Body) => body.map(decode(_)))
    3.84    }
    3.85  
    3.86  
    3.87 @@ -190,4 +208,44 @@
    3.88            val (typargs, args, props) = decode_props(body)
    3.89            Fact(entity, typargs, args, props)
    3.90          })
    3.91 +
    3.92 +
    3.93 +  /* type classes */
    3.94 +
    3.95 +  sealed case class Class(
    3.96 +    entity: Entity, params: List[(String, Term.Typ)], axioms: List[Term.Term])
    3.97 +
    3.98 +  def read_classes(db: SQL.Database, session_name: String, theory_name: String): List[Class] =
    3.99 +    read_entities(db, session_name, theory_name, "classes",
   3.100 +      (tree: XML.Tree) =>
   3.101 +        {
   3.102 +          val (entity, body) = decode_entity(tree)
   3.103 +          val (params, axioms) =
   3.104 +          {
   3.105 +            import XML.Decode._
   3.106 +            import Term_XML.Decode._
   3.107 +            pair(list(pair(string, typ)), list(term))(body)
   3.108 +          }
   3.109 +          Class(entity, params, axioms)
   3.110 +        })
   3.111 +
   3.112 +
   3.113 +  /* HOL typedefs */
   3.114 +
   3.115 +  sealed case class Typedef(name: String,
   3.116 +    rep_type: Term.Typ, abs_type: Term.Typ, rep_name: String, abs_name: String, axiom_name: String)
   3.117 +
   3.118 +  def read_typedefs(db: SQL.Database, session_name: String, theory_name: String): List[Typedef] =
   3.119 +    read_export(db, session_name, theory_name, "typedefs",
   3.120 +      (body: XML.Body) =>
   3.121 +        {
   3.122 +          val typedefs =
   3.123 +          {
   3.124 +            import XML.Decode._
   3.125 +            import Term_XML.Decode._
   3.126 +            list(pair(string, pair(typ, pair(typ, pair(string, pair(string, string))))))(body)
   3.127 +          }
   3.128 +          for { (name, (rep_type, (abs_type, (rep_name, (abs_name, axiom_name))))) <- typedefs }
   3.129 +          yield Typedef(name, rep_type, abs_type, rep_name, abs_name, axiom_name)
   3.130 +        })
   3.131  }