src/Pure/Thy/export_theory.scala

formal position for spec rule (not significant for equality);

/*  Title:      Pure/Thy/export_theory.scala
    Author:     Makarius

Export foundational theory content.
*/

package isabelle


import scala.collection.immutable.SortedMap


object Export_Theory
{
  /** session content **/

  sealed case class Session(name: String, theory_graph: Graph[String, Option[Theory]])
  {
    override def toString: String = name

    def theory(theory_name: String): Option[Theory] =
      if (theory_graph.defined(theory_name)) theory_graph.get_node(theory_name)
      else None

    def theories: List[Theory] =
      theory_graph.topological_order.flatMap(theory(_))
  }

  def read_session(
    store: Sessions.Store,
    sessions_structure: Sessions.Structure,
    session_name: String,
    progress: Progress = No_Progress,
    types: Boolean = true,
    consts: Boolean = true,
    axioms: Boolean = true,
    thms: Boolean = true,
    classes: Boolean = true,
    locales: Boolean = true,
    locale_dependencies: Boolean = true,
    classrel: Boolean = true,
    arities: Boolean = true,
    constdefs: Boolean = true,
    typedefs: Boolean = true,
    spec_rules: Boolean = true,
    cache: Term.Cache = Term.make_cache()): Session =
  {
    val thys =
      sessions_structure.build_requirements(List(session_name)).flatMap(session =>
        using(store.open_database(session))(db =>
        {
          db.transaction {
            for (theory <- Export.read_theory_names(db, session))
            yield {
              progress.echo("Reading theory " + theory)
              read_theory(Export.Provider.database(db, session, theory),
                session, theory, types = types, consts = consts,
                axioms = axioms, thms = thms, classes = classes, locales = locales,
                locale_dependencies = locale_dependencies, classrel = classrel, arities = arities,
                constdefs = constdefs, typedefs = typedefs,
                spec_rules = spec_rules, cache = Some(cache))
            }
          }
        }))

    val graph0 =
      (Graph.string[Option[Theory]] /: thys) {
        case (g, thy) => g.default_node(thy.name, Some(thy)) }
    val graph1 =
      (graph0 /: thys) { case (g0, thy) =>
        (g0 /: thy.parents) { case (g1, parent) =>
          g1.default_node(parent, None).add_edge_acyclic(parent, thy.name) } }

    Session(session_name, graph1)
  }



  /** theory content **/

  val export_prefix: String = "theory/"
  val export_prefix_proofs: String = "proofs/"

  sealed case class Theory(name: String, parents: List[String],
    types: List[Type],
    consts: List[Const],
    axioms: List[Axiom],
    thms: List[Thm],
    classes: List[Class],
    locales: List[Locale],
    locale_dependencies: List[Locale_Dependency],
    classrel: List[Classrel],
    arities: List[Arity],
    constdefs: List[Constdef],
    typedefs: List[Typedef],
    spec_rules: List[Spec_Rule])
  {
    override def toString: String = name

    def entity_iterator: Iterator[Entity] =
      types.iterator.map(_.entity) ++
      consts.iterator.map(_.entity) ++
      axioms.iterator.map(_.entity) ++
      thms.iterator.map(_.entity) ++
      classes.iterator.map(_.entity) ++
      locales.iterator.map(_.entity) ++
      locale_dependencies.iterator.map(_.entity)

    def cache(cache: Term.Cache): Theory =
      Theory(cache.string(name),
        parents.map(cache.string(_)),
        types.map(_.cache(cache)),
        consts.map(_.cache(cache)),
        axioms.map(_.cache(cache)),
        thms.map(_.cache(cache)),
        classes.map(_.cache(cache)),
        locales.map(_.cache(cache)),
        locale_dependencies.map(_.cache(cache)),
        classrel.map(_.cache(cache)),
        arities.map(_.cache(cache)),
        constdefs.map(_.cache(cache)),
        typedefs.map(_.cache(cache)),
        spec_rules.map(_.cache(cache)))
  }

  def read_theory(provider: Export.Provider, session_name: String, theory_name: String,
    types: Boolean = true,
    consts: Boolean = true,
    axioms: Boolean = true,
    thms: Boolean = true,
    classes: Boolean = true,
    locales: Boolean = true,
    locale_dependencies: Boolean = true,
    classrel: Boolean = true,
    arities: Boolean = true,
    constdefs: Boolean = true,
    typedefs: Boolean = true,
    spec_rules: Boolean = true,
    cache: Option[Term.Cache] = None): Theory =
  {
    val parents =
      if (theory_name == Thy_Header.PURE) Nil
      else {
        provider(export_prefix + "parents") match {
          case Some(entry) => split_lines(entry.uncompressed().text)
          case None =>
            error("Missing theory export in session " + quote(session_name) + ": " +
              quote(theory_name))
        }
      }
    val theory =
      Theory(theory_name, parents,
        if (types) read_types(provider) else Nil,
        if (consts) read_consts(provider) else Nil,
        if (axioms) read_axioms(provider) else Nil,
        if (thms) read_thms(provider) else Nil,
        if (classes) read_classes(provider) else Nil,
        if (locales) read_locales(provider) else Nil,
        if (locale_dependencies) read_locale_dependencies(provider) else Nil,
        if (classrel) read_classrel(provider) else Nil,
        if (arities) read_arities(provider) else Nil,
        if (constdefs) read_constdefs(provider) else Nil,
        if (typedefs) read_typedefs(provider) else Nil,
        if (spec_rules) read_spec_rules(provider) else Nil)
    if (cache.isDefined) theory.cache(cache.get) else theory
  }

  def read_pure[A](store: Sessions.Store, read: (Export.Provider, String, String) => A): A =
  {
    val session_name = Thy_Header.PURE
    val theory_name = Thy_Header.PURE

    using(store.open_database(session_name))(db =>
    {
      db.transaction {
        read(Export.Provider.database(db, session_name, theory_name), session_name, theory_name)
      }
    })
  }

  def read_pure_theory(store: Sessions.Store, cache: Option[Term.Cache] = None): Theory =
    read_pure(store, read_theory(_, _, _, cache = cache))

  def read_pure_proof(
      store: Sessions.Store, id: Thm_Id, cache: Option[Term.Cache] = None): Option[Proof] =
    read_pure(store, (provider, _, _) => read_proof(provider, id, cache = cache))


  /* entities */

  object Kind extends Enumeration
  {
    val TYPE = Value("type")
    val CONST = Value("const")
    val AXIOM = Value("axiom")
    val THM = Value("thm")
    val PROOF = Value("proof")
    val CLASS = Value("class")
    val LOCALE = Value("locale")
    val LOCALE_DEPENDENCY = Value("locale_dependency")
    val DOCUMENT_HEADING = Value("document_heading")
    val DOCUMENT_TEXT = Value("document_text")
    val PROOF_TEXT = Value("proof_text")
  }

  sealed case class Entity(
    kind: Kind.Value, name: String, xname: String, pos: Position.T, id: Option[Long], serial: Long)
  {
    override def toString: String = kind.toString + " " + quote(name)

    def cache(cache: Term.Cache): Entity =
      Entity(kind, cache.string(name), cache.string(xname), cache.position(pos), id, serial)
  }

  def decode_entity(kind: Kind.Value, tree: XML.Tree): (Entity, XML.Body) =
  {
    def err(): Nothing = throw new XML.XML_Body(List(tree))

    tree match {
      case XML.Elem(Markup(Markup.ENTITY, props), body) =>
        val name = Markup.Name.unapply(props) getOrElse err()
        val xname = Markup.XName.unapply(props) getOrElse err()
        val pos = props.filter({ case (a, _) => Markup.POSITION_PROPERTIES(a) && a != Markup.ID })
        val id = Position.Id.unapply(props)
        val serial = Markup.Serial.unapply(props) getOrElse err()
        (Entity(kind, name, xname, pos, id, serial), body)
      case _ => err()
    }
  }


  /* approximative syntax */

  object Assoc extends Enumeration
  {
    val NO_ASSOC, LEFT_ASSOC, RIGHT_ASSOC = Value
  }

  sealed abstract class Syntax
  case object No_Syntax extends Syntax
  case class Prefix(delim: String) extends Syntax
  case class Infix(assoc: Assoc.Value, delim: String, pri: Int) extends Syntax

  def decode_syntax: XML.Decode.T[Syntax] =
    XML.Decode.variant(List(
      { case (Nil, Nil) => No_Syntax },
      { case (List(delim), Nil) => Prefix(delim) },
      { case (Nil, body) =>
          import XML.Decode._
          val (ass, delim, pri) = triple(int, string, int)(body)
          Infix(Assoc(ass), delim, pri) }))


  /* types */

  sealed case class Type(
    entity: Entity, syntax: Syntax, args: List[String], abbrev: Option[Term.Typ])
  {
    def cache(cache: Term.Cache): Type =
      Type(entity.cache(cache),
        syntax,
        args.map(cache.string(_)),
        abbrev.map(cache.typ(_)))
  }

  def read_types(provider: Export.Provider): List[Type] =
    provider.uncompressed_yxml(export_prefix + "types").map((tree: XML.Tree) =>
      {
        val (entity, body) = decode_entity(Kind.TYPE, tree)
        val (syntax, args, abbrev) =
        {
          import XML.Decode._
          triple(decode_syntax, list(string), option(Term_XML.Decode.typ))(body)
        }
        Type(entity, syntax, args, abbrev)
      })


  /* consts */

  sealed case class Const(
    entity: Entity,
    syntax: Syntax,
    typargs: List[String],
    typ: Term.Typ,
    abbrev: Option[Term.Term],
    propositional: Boolean,
    primrec_types: List[String],
    corecursive: Boolean)
  {
    def cache(cache: Term.Cache): Const =
      Const(entity.cache(cache),
        syntax,
        typargs.map(cache.string(_)),
        cache.typ(typ),
        abbrev.map(cache.term(_)),
        propositional,
        primrec_types.map(cache.string(_)),
        corecursive)
  }

  def read_consts(provider: Export.Provider): List[Const] =
    provider.uncompressed_yxml(export_prefix + "consts").map((tree: XML.Tree) =>
      {
        val (entity, body) = decode_entity(Kind.CONST, tree)
        val (syntax, (args, (typ, (abbrev, (propositional, (primrec_types, corecursive)))))) =
        {
          import XML.Decode._
          pair(decode_syntax,
            pair(list(string),
              pair(Term_XML.Decode.typ,
                pair(option(Term_XML.Decode.term), pair(bool,
                  pair(list(string), bool))))))(body)
        }
        Const(entity, syntax, args, typ, abbrev, propositional, primrec_types, corecursive)
      })


  /* axioms */

  sealed case class Prop(
    typargs: List[(String, Term.Sort)],
    args: List[(String, Term.Typ)],
    term: Term.Term)
  {
    def cache(cache: Term.Cache): Prop =
      Prop(
        typargs.map({ case (name, sort) => (cache.string(name), cache.sort(sort)) }),
        args.map({ case (name, typ) => (cache.string(name), cache.typ(typ)) }),
        cache.term(term))
  }

  def decode_prop(body: XML.Body): Prop =
  {
    val (typargs, args, t) =
    {
      import XML.Decode._
      import Term_XML.Decode._
      triple(list(pair(string, sort)), list(pair(string, typ)), term)(body)
    }
    Prop(typargs, args, t)
  }

  sealed case class Axiom(entity: Entity, prop: Prop)
  {
    def cache(cache: Term.Cache): Axiom =
      Axiom(entity.cache(cache), prop.cache(cache))
  }

  def read_axioms(provider: Export.Provider): List[Axiom] =
    provider.uncompressed_yxml(export_prefix + "axioms").map((tree: XML.Tree) =>
      {
        val (entity, body) = decode_entity(Kind.AXIOM, tree)
        val prop = decode_prop(body)
        Axiom(entity, prop)
      })


  /* theorems */

  sealed case class Thm_Id(serial: Long, theory_name: String)
  {
    def pure: Boolean = theory_name == Thy_Header.PURE
  }

  sealed case class Thm(
    entity: Entity,
    prop: Prop,
    deps: List[String],
    proof: Term.Proof)
  {
    def cache(cache: Term.Cache): Thm =
      Thm(
        entity.cache(cache),
        prop.cache(cache),
        deps.map(cache.string _),
        cache.proof(proof))
  }

  def read_thms(provider: Export.Provider): List[Thm] =
    provider.uncompressed_yxml(export_prefix + "thms").map((tree: XML.Tree) =>
      {
        val (entity, body) = decode_entity(Kind.THM, tree)
        val (prop, deps, prf) =
        {
          import XML.Decode._
          import Term_XML.Decode._
          triple(decode_prop, list(string), proof)(body)
        }
        Thm(entity, prop, deps, prf)
      })

  sealed case class Proof(
    typargs: List[(String, Term.Sort)],
    args: List[(String, Term.Typ)],
    term: Term.Term,
    proof: Term.Proof)
  {
    def prop: Prop = Prop(typargs, args, term)

    def cache(cache: Term.Cache): Proof =
      Proof(
        typargs.map({ case (name, sort) => (cache.string(name), cache.sort(sort)) }),
        args.map({ case (name, typ) => (cache.string(name), cache.typ(typ)) }),
        cache.term(term),
        cache.proof(proof))
  }

  def read_proof(
    provider: Export.Provider, id: Thm_Id, cache: Option[Term.Cache] = None): Option[Proof] =
  {
    for { entry <- provider.focus(id.theory_name)(export_prefix_proofs + id.serial) }
    yield {
      val body = entry.uncompressed_yxml()
      val (typargs, (args, (prop_body, proof_body))) =
      {
        import XML.Decode._
        import Term_XML.Decode._
        pair(list(pair(string, sort)), pair(list(pair(string, typ)), pair(x => x, x => x)))(body)
      }
      val env = args.toMap
      val prop = Term_XML.Decode.term_env(env)(prop_body)
      val proof = Term_XML.Decode.proof_env(env)(proof_body)

      val result = Proof(typargs, args, prop, proof)
      cache.map(result.cache(_)) getOrElse result
    }
  }

  def read_proof_boxes(
    store: Sessions.Store,
    provider: Export.Provider,
    proof: Term.Proof,
    suppress: Thm_Id => Boolean = _ => false,
    cache: Option[Term.Cache] = None): List[(Thm_Id, Proof)] =
  {
    var seen = Set.empty[Long]
    var result = SortedMap.empty[Long, (Thm_Id, Proof)]

    def boxes(context: Option[(Long, Term.Proof)], prf: Term.Proof)
    {
      prf match {
        case Term.Abst(_, _, p) => boxes(context, p)
        case Term.AbsP(_, _, p) => boxes(context, p)
        case Term.Appt(p, _) => boxes(context, p)
        case Term.AppP(p, q) => boxes(context, p); boxes(context, q)
        case thm: Term.PThm if !seen(thm.serial) =>
          seen += thm.serial
          val id = Thm_Id(thm.serial, thm.theory_name)
          if (!suppress(id)) {
            val read =
              if (id.pure) Export_Theory.read_pure_proof(store, id, cache = cache)
              else Export_Theory.read_proof(provider, id, cache = cache)
            read match {
              case Some(p) =>
                result += (thm.serial -> (id -> p))
                boxes(Some((thm.serial, p.proof)), p.proof)
              case None =>
                error("Missing proof " + thm.serial + " (theory " + quote (thm.theory_name) + ")" +
                  (context match {
                    case None => ""
                    case Some((i, p)) => " in proof " + i + ":\n" + p
                  }))
            }
          }
        case _ =>
      }
    }

    boxes(None, proof)
    result.iterator.map(_._2).toList
  }


  /* type classes */

  sealed case class Class(
    entity: Entity, params: List[(String, Term.Typ)], axioms: List[Prop])
  {
    def cache(cache: Term.Cache): Class =
      Class(entity.cache(cache),
        params.map({ case (name, typ) => (cache.string(name), cache.typ(typ)) }),
        axioms.map(_.cache(cache)))
  }

  def read_classes(provider: Export.Provider): List[Class] =
    provider.uncompressed_yxml(export_prefix + "classes").map((tree: XML.Tree) =>
      {
        val (entity, body) = decode_entity(Kind.CLASS, tree)
        val (params, axioms) =
        {
          import XML.Decode._
          import Term_XML.Decode._
          pair(list(pair(string, typ)), list(decode_prop))(body)
        }
        Class(entity, params, axioms)
      })


  /* locales */

  sealed case class Locale(
    entity: Entity,
    typargs: List[(String, Term.Sort)],
    args: List[((String, Term.Typ), Syntax)],
    axioms: List[Prop])
  {
    def cache(cache: Term.Cache): Locale =
      Locale(entity.cache(cache),
        typargs.map({ case (name, sort) => (cache.string(name), cache.sort(sort)) }),
        args.map({ case ((name, typ), syntax) => ((cache.string(name), cache.typ(typ)), syntax) }),
        axioms.map(_.cache(cache)))
  }

  def read_locales(provider: Export.Provider): List[Locale] =
    provider.uncompressed_yxml(export_prefix + "locales").map((tree: XML.Tree) =>
      {
        val (entity, body) = decode_entity(Kind.LOCALE, tree)
        val (typargs, args, axioms) =
        {
          import XML.Decode._
          import Term_XML.Decode._
          triple(list(pair(string, sort)), list(pair(pair(string, typ), decode_syntax)),
            list(decode_prop))(body)
        }
        Locale(entity, typargs, args, axioms)
      })


  /* locale dependencies */

  sealed case class Locale_Dependency(
    entity: Entity,
    source: String,
    target: String,
    prefix: List[(String, Boolean)],
    subst_types: List[((String, Term.Sort), Term.Typ)],
    subst_terms: List[((String, Term.Typ), Term.Term)])
  {
    def cache(cache: Term.Cache): Locale_Dependency =
      Locale_Dependency(entity.cache(cache),
        cache.string(source),
        cache.string(target),
        prefix.map({ case (name, mandatory) => (cache.string(name), mandatory) }),
        subst_types.map({ case ((a, s), ty) => ((cache.string(a), cache.sort(s)), cache.typ(ty)) }),
        subst_terms.map({ case ((x, ty), t) => ((cache.string(x), cache.typ(ty)), cache.term(t)) }))

    def is_inclusion: Boolean =
      subst_types.isEmpty && subst_terms.isEmpty
  }

  def read_locale_dependencies(provider: Export.Provider): List[Locale_Dependency] =
    provider.uncompressed_yxml(export_prefix + "locale_dependencies").map((tree: XML.Tree) =>
      {
        val (entity, body) = decode_entity(Kind.LOCALE_DEPENDENCY, tree)
        val (source, (target, (prefix, (subst_types, subst_terms)))) =
        {
          import XML.Decode._
          import Term_XML.Decode._
          pair(string, pair(string, pair(list(pair(string, bool)),
            pair(list(pair(pair(string, sort), typ)), list(pair(pair(string, typ), term))))))(body)
        }
        Locale_Dependency(entity, source, target, prefix, subst_types, subst_terms)
      })


  /* sort algebra */

  sealed case class Classrel(class1: String, class2: String, prop: Prop)
  {
    def cache(cache: Term.Cache): Classrel =
      Classrel(cache.string(class1), cache.string(class2), prop.cache(cache))
  }

  def read_classrel(provider: Export.Provider): List[Classrel] =
  {
    val body = provider.uncompressed_yxml(export_prefix + "classrel")
    val classrel =
    {
      import XML.Decode._
      list(pair(decode_prop, pair(string, string)))(body)
    }
    for ((prop, (c1, c2)) <- classrel) yield Classrel(c1, c2, prop)
  }

  sealed case class Arity(type_name: String, domain: List[Term.Sort], codomain: String, prop: Prop)
  {
    def cache(cache: Term.Cache): Arity =
      Arity(cache.string(type_name), domain.map(cache.sort(_)), cache.string(codomain),
        prop.cache(cache))
  }

  def read_arities(provider: Export.Provider): List[Arity] =
  {
    val body = provider.uncompressed_yxml(export_prefix + "arities")
    val arities =
    {
      import XML.Decode._
      import Term_XML.Decode._
      list(pair(decode_prop, triple(string, list(sort), string)))(body)
    }
    for ((prop, (a, b, c)) <- arities) yield Arity(a, b, c, prop)
  }


  /* Pure constdefs */

  sealed case class Constdef(name: String, axiom_name: String)
  {
    def cache(cache: Term.Cache): Constdef =
      Constdef(cache.string(name), cache.string(axiom_name))
  }

  def read_constdefs(provider: Export.Provider): List[Constdef] =
  {
    val body = provider.uncompressed_yxml(export_prefix + "constdefs")
    val constdefs =
    {
      import XML.Decode._
      list(pair(string, string))(body)
    }
    for ((name, axiom_name) <- constdefs) yield Constdef(name, axiom_name)
  }


  /* HOL typedefs */

  sealed case class Typedef(name: String,
    rep_type: Term.Typ, abs_type: Term.Typ, rep_name: String, abs_name: String, axiom_name: String)
  {
    def cache(cache: Term.Cache): Typedef =
      Typedef(cache.string(name),
        cache.typ(rep_type),
        cache.typ(abs_type),
        cache.string(rep_name),
        cache.string(abs_name),
        cache.string(axiom_name))
  }

  def read_typedefs(provider: Export.Provider): List[Typedef] =
  {
    val body = provider.uncompressed_yxml(export_prefix + "typedefs")
    val typedefs =
    {
      import XML.Decode._
      import Term_XML.Decode._
      list(pair(string, pair(typ, pair(typ, pair(string, pair(string, string))))))(body)
    }
    for { (name, (rep_type, (abs_type, (rep_name, (abs_name, axiom_name))))) <- typedefs }
    yield Typedef(name, rep_type, abs_type, rep_name, abs_name, axiom_name)
  }


  /* Pure spec rules */

  sealed abstract class Recursion
  {
    def cache(cache: Term.Cache): Recursion =
      this match {
        case Primrec(types) => Primrec(types.map(cache.string))
        case Primcorec(types) => Primcorec(types.map(cache.string))
        case _ => this
      }
  }
  case class Primrec(types: List[String]) extends Recursion
  case object Recdef extends Recursion
  case class Primcorec(types: List[String]) extends Recursion
  case object Corec extends Recursion
  case object Unknown_Recursion extends Recursion

  val decode_recursion: XML.Decode.T[Recursion] =
  {
    import XML.Decode._
    variant(List(
      { case (Nil, a) => Primrec(list(string)(a)) },
      { case (Nil, Nil) => Recdef },
      { case (Nil, a) => Primcorec(list(string)(a)) },
      { case (Nil, Nil) => Corec },
      { case (Nil, Nil) => Unknown_Recursion }))
  }


  sealed abstract class Rough_Classification
  {
    def is_equational: Boolean = this.isInstanceOf[Equational]
    def is_inductive: Boolean = this == Inductive
    def is_co_inductive: Boolean = this == Co_Inductive
    def is_relational: Boolean = is_inductive || is_co_inductive
    def is_unknown: Boolean = this == Unknown

    def cache(cache: Term.Cache): Rough_Classification =
      this match {
        case Equational(recursion) => Equational(recursion.cache(cache))
        case _ => this
      }
  }
  case class Equational(recursion: Recursion) extends Rough_Classification
  case object Inductive extends Rough_Classification
  case object Co_Inductive extends Rough_Classification
  case object Unknown extends Rough_Classification

  val decode_rough_classification: XML.Decode.T[Rough_Classification] =
  {
    import XML.Decode._
    variant(List(
      { case (Nil, a) => Equational(decode_recursion(a)) },
      { case (Nil, Nil) => Inductive },
      { case (Nil, Nil) => Co_Inductive },
      { case (Nil, Nil) => Unknown }))
  }


  sealed case class Spec_Rule(
    pos: Position.T,
    name: String,
    rough_classification: Rough_Classification,
    terms: List[Term.Term],
    rules: List[Prop])
  {
    def id: Option[Long] = Position.Id.unapply(pos)

    def cache(cache: Term.Cache): Spec_Rule =
      Spec_Rule(
        cache.position(pos),
        cache.string(name),
        rough_classification.cache(cache),
        terms.map(cache.term(_)),
        rules.map(_.cache(cache)))
  }

  def read_spec_rules(provider: Export.Provider): List[Spec_Rule] =
  {
    val body = provider.uncompressed_yxml(export_prefix + "spec_rules")
    val spec_rules =
    {
      import XML.Decode._
      import Term_XML.Decode._
      list(
        pair(properties, pair(string, pair(decode_rough_classification,
        pair(list(term), list(decode_prop))))))(body)
    }
    for ((pos, (name, (rough_classification, (terms, rules)))) <- spec_rules)
      yield Spec_Rule(pos, name, rough_classification, terms, rules)
  }
}