src/Pure/Thy/export_theory.scala
author wenzelm
Sun, 13 May 2018 20:04:59 +0200
changeset 68171 13162bb3a677
child 68172 0f14cf9c632f
permissions -rw-r--r--
export foundational theory content in Scala;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
68171
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/Thy/export_theory.scala
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
     3
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
     4
Export foundational theory content.
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
     5
*/
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
     6
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
     7
package isabelle
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
     8
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
     9
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
    10
object Export_Theory
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
    11
{
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
    12
  /* entities */
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
    13
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
    14
  sealed case class Entity(name: String, kind: String, serial: Long, pos: Position.T)
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
    15
  {
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
    16
    override def toString: String = name
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
    17
  }
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
    18
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
    19
  def decode_entity(tree: XML.Tree): (Entity, XML.Body) =
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
    20
  {
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
    21
    def err(): Nothing = throw new XML.XML_Body(List(tree))
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
    22
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
    23
    tree match {
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
    24
      case XML.Elem(Markup(Markup.ENTITY, props), body) =>
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
    25
        val name = Markup.Name.unapply(props) getOrElse err()
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
    26
        val kind = Markup.Kind.unapply(props) getOrElse err()
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
    27
        val serial = Markup.Serial.unapply(props) getOrElse err()
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
    28
        val pos = props.filter({ case (a, _) => Markup.POSITION_PROPERTIES(a) })
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
    29
        (Entity(name, kind, serial, pos), body)
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
    30
      case _ => err()
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
    31
    }
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
    32
  }
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
    33
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
    34
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
    35
  /* types */
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
    36
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
    37
  sealed case class Type(entity: Entity, args: List[String], abbrev: Option[Term.Typ])
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
    38
  {
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
    39
    def arity: Int = args.length
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
    40
  }
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
    41
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
    42
  def decode_type(tree: XML.Tree): Type =
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
    43
  {
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
    44
    val (entity, body) = decode_entity(tree)
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
    45
    val (args, abbrev) =
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
    46
    {
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
    47
      import XML.Decode._
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
    48
      pair(list(string), option(Term_XML.Decode.typ))(body)
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
    49
    }
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
    50
    Type(entity, args, abbrev)
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
    51
  }
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
    52
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
    53
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
    54
  /* consts */
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
    55
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
    56
  sealed case class Const(entity: Entity, typ: Term.Typ, abbrev: Option[Term.Term])
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
    57
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
    58
  def decode_const(tree: XML.Tree): Const =
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
    59
  {
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
    60
    val (entity, body) = decode_entity(tree)
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
    61
    val (typ, abbrev) =
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
    62
    {
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
    63
      import XML.Decode._
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
    64
      pair(Term_XML.Decode.typ, option(Term_XML.Decode.term))(body)
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
    65
    }
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
    66
    Const(entity, typ, abbrev)
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
    67
  }
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
    68
}