src/Pure/Thy/export_theory.scala
changeset 68295 781a98696638
parent 68267 6a29709906c6
child 68346 b44010800a19
     1.1 --- a/src/Pure/Thy/export_theory.scala	Sat May 26 21:24:07 2018 +0200
     1.2 +++ b/src/Pure/Thy/export_theory.scala	Sat May 26 22:02:25 2018 +0200
     1.3 @@ -31,6 +31,8 @@
     1.4      facts: Boolean = true,
     1.5      classes: Boolean = true,
     1.6      typedefs: Boolean = true,
     1.7 +    classrel: Boolean = true,
     1.8 +    arities: Boolean = true,
     1.9      cache: Term.Cache = Term.make_cache()): Session =
    1.10    {
    1.11      val thys =
    1.12 @@ -64,7 +66,9 @@
    1.13      axioms: List[Axiom],
    1.14      facts: List[Fact],
    1.15      classes: List[Class],
    1.16 -    typedefs: List[Typedef])
    1.17 +    typedefs: List[Typedef],
    1.18 +    classrel: List[Classrel],
    1.19 +    arities: List[Arity])
    1.20    {
    1.21      override def toString: String = name
    1.22  
    1.23 @@ -76,10 +80,13 @@
    1.24          axioms.map(_.cache(cache)),
    1.25          facts.map(_.cache(cache)),
    1.26          classes.map(_.cache(cache)),
    1.27 -        typedefs.map(_.cache(cache)))
    1.28 +        typedefs.map(_.cache(cache)),
    1.29 +        classrel.map(_.cache(cache)),
    1.30 +        arities.map(_.cache(cache)))
    1.31    }
    1.32  
    1.33 -  def empty_theory(name: String): Theory = Theory(name, Nil, Nil, Nil, Nil, Nil, Nil, Nil)
    1.34 +  def empty_theory(name: String): Theory =
    1.35 +    Theory(name, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil)
    1.36  
    1.37    def read_theory(db: SQL.Database, session_name: String, theory_name: String,
    1.38      types: Boolean = true,
    1.39 @@ -88,6 +95,8 @@
    1.40      facts: Boolean = true,
    1.41      classes: Boolean = true,
    1.42      typedefs: Boolean = true,
    1.43 +    classrel: Boolean = true,
    1.44 +    arities: Boolean = true,
    1.45      cache: Option[Term.Cache] = None): Theory =
    1.46    {
    1.47      val parents =
    1.48 @@ -104,7 +113,9 @@
    1.49          if (axioms) read_axioms(db, session_name, theory_name) else Nil,
    1.50          if (facts) read_facts(db, session_name, theory_name) else Nil,
    1.51          if (classes) read_classes(db, session_name, theory_name) else Nil,
    1.52 -        if (typedefs) read_typedefs(db, session_name, theory_name) else Nil)
    1.53 +        if (typedefs) read_typedefs(db, session_name, theory_name) else Nil,
    1.54 +        if (classrel) read_classrel(db, session_name, theory_name) else Nil,
    1.55 +        if (arities) read_arities(db, session_name, theory_name) else Nil)
    1.56      if (cache.isDefined) theory.cache(cache.get) else theory
    1.57    }
    1.58  
    1.59 @@ -281,6 +292,46 @@
    1.60          })
    1.61  
    1.62  
    1.63 +  /* sort algebra */
    1.64 +
    1.65 +  sealed case class Classrel(class_name: String, super_names: List[String])
    1.66 +  {
    1.67 +    def cache(cache: Term.Cache): Classrel =
    1.68 +      Classrel(cache.string(class_name), super_names.map(cache.string(_)))
    1.69 +  }
    1.70 +
    1.71 +  def read_classrel(db: SQL.Database, session_name: String, theory_name: String): List[Classrel] =
    1.72 +    read_export(db, session_name, theory_name, "classrel",
    1.73 +      (body: XML.Body) =>
    1.74 +        {
    1.75 +          val classrel =
    1.76 +          {
    1.77 +            import XML.Decode._
    1.78 +            list(pair(string, list(string)))(body)
    1.79 +          }
    1.80 +          for ((c, cs) <- classrel) yield Classrel(c, cs)
    1.81 +        })
    1.82 +
    1.83 +  sealed case class Arity(type_name: String, domain: List[Term.Sort], codomain: String)
    1.84 +  {
    1.85 +    def cache(cache: Term.Cache): Arity =
    1.86 +      Arity(cache.string(type_name), domain.map(cache.sort(_)), cache.string(codomain))
    1.87 +  }
    1.88 +
    1.89 +  def read_arities(db: SQL.Database, session_name: String, theory_name: String): List[Arity] =
    1.90 +    read_export(db, session_name, theory_name, "arities",
    1.91 +      (body: XML.Body) =>
    1.92 +        {
    1.93 +          val arities =
    1.94 +          {
    1.95 +            import XML.Decode._
    1.96 +            import Term_XML.Decode._
    1.97 +            list(triple(string, list(sort), string))(body)
    1.98 +          }
    1.99 +          for ((a, b, c) <- arities) yield Arity(a, b, c)
   1.100 +        })
   1.101 +
   1.102 +
   1.103    /* HOL typedefs */
   1.104  
   1.105    sealed case class Typedef(name: String,