src/Pure/Thy/export_theory.scala
changeset 68208 d9f2cf4fc002
parent 68206 dedf1a70d1fa
child 68209 aeffd8f1f079
equal deleted inserted replaced
68207:1463c4996fb2 68208:d9f2cf4fc002
    52 
    52 
    53 
    53 
    54 
    54 
    55   /** theory content **/
    55   /** theory content **/
    56 
    56 
    57   sealed case class Theory(
    57   sealed case class Theory(name: String, parents: List[String],
    58     name: String, parents: List[String], types: List[Type], consts: List[Const])
    58     types: List[Type],
       
    59     consts: List[Const],
       
    60     axioms: List[Axiom])
    59   {
    61   {
    60     override def toString: String = name
    62     override def toString: String = name
    61   }
    63   }
    62 
    64 
    63   def empty_theory(name: String): Theory = Theory(name, Nil, Nil, Nil)
    65   def empty_theory(name: String): Theory = Theory(name, Nil, Nil, Nil, Nil)
    64 
    66 
    65   def read_theory(db: SQL.Database, session_name: String, theory_name: String,
    67   def read_theory(db: SQL.Database, session_name: String, theory_name: String,
    66     types: Boolean = true,
    68     types: Boolean = true,
    67     consts: Boolean = true): Theory =
    69     consts: Boolean = true,
       
    70     axioms: Boolean = true): Theory =
    68   {
    71   {
    69     val parents =
    72     val parents =
    70       Export.read_entry(db, session_name, theory_name, "theory/parents") match {
    73       Export.read_entry(db, session_name, theory_name, "theory/parents") match {
    71         case Some(entry) =>
    74         case Some(entry) =>
    72           import XML.Decode._
    75           import XML.Decode._
    75           error("Missing theory export in session " + quote(session_name) + ": " +
    78           error("Missing theory export in session " + quote(session_name) + ": " +
    76             quote(theory_name))
    79             quote(theory_name))
    77       }
    80       }
    78     Theory(theory_name, parents,
    81     Theory(theory_name, parents,
    79       if (types) read_types(db, session_name, theory_name) else Nil,
    82       if (types) read_types(db, session_name, theory_name) else Nil,
    80       if (consts) read_consts(db, session_name, theory_name) else Nil)
    83       if (consts) read_consts(db, session_name, theory_name) else Nil,
       
    84       if (axioms) read_axioms(db, session_name, theory_name) else Nil)
    81   }
    85   }
    82 
    86 
    83 
    87 
    84   /* entities */
    88   /* entities */
    85 
    89 
   145             import XML.Decode._
   149             import XML.Decode._
   146             triple(list(string), Term_XML.Decode.typ, option(Term_XML.Decode.term))(body)
   150             triple(list(string), Term_XML.Decode.typ, option(Term_XML.Decode.term))(body)
   147           }
   151           }
   148           Const(entity, args, typ, abbrev)
   152           Const(entity, args, typ, abbrev)
   149         })
   153         })
       
   154 
       
   155 
       
   156   /* axioms */
       
   157 
       
   158   sealed case class Axiom(
       
   159     entity: Entity,
       
   160     typargs: List[(String, Term.Sort)],
       
   161     args: List[(String, Term.Typ)],
       
   162     prop: Term.Term)
       
   163 
       
   164   def read_axioms(db: SQL.Database, session_name: String, theory_name: String): List[Axiom] =
       
   165     read_entities(db, session_name, theory_name, "axioms",
       
   166       (tree: XML.Tree) =>
       
   167         {
       
   168           val (entity, body) = decode_entity(tree)
       
   169           val (typargs, args, prop) =
       
   170           {
       
   171             import XML.Decode._
       
   172             import Term_XML.Decode._
       
   173             triple(list(pair(string, sort)), list(pair(string, typ)), term)(body)
       
   174           }
       
   175           Axiom(entity, typargs, args, prop)
       
   176         })
   150 }
   177 }