wneuper/isac: isac-java/src/java/isac/bridge/xml/DataTypes.scala@b4e3883d7b66

     1 /*

     2  * @author Walther Neuper

     3  * Copyright (c) due to license terms

     4  * Created on Jul 14, 2015

     5  * Institute for Softwaretechnology, Graz University of Technology, Austria.

     6  *

     7  * When ConvertXML.scala was not recognized switiching "Scala Nature"

     8  * off and on again helped.

     9  */

    11 package isac.bridge.xml

    13 import isac.bridge.CChanged

    14 import isac.bridge.CEvent

    15 import isac.bridge.CMessage

    16 import isac.gui.mawen.scalaterm.Util

    17 import isac.gui.mawen.syntax.Syntax_Phases

    18 import isac.util.Formalization

    19 import isac.util.formulae.CalcFormula

    20 import isac.util.formulae.CalcHead

    21 import isac.util.formulae.CalcHeadSimpleID

    22 import isac.util.formulae.ContextMethod

    23 import isac.util.formulae.ContextProblem

    24 import isac.util.formulae.ContextTheory

    25 import isac.util.formulae.Formula

    26 import isac.util.formulae.FormulaPair

    27 import isac.util.formulae.HierarchyKey

    28 import isac.util.formulae.KEStoreKey

    29 import isac.util.formulae.ModelItem

    30 import isac.util.formulae.ModelItemList

    31 import isac.util.formulae.Model

    32 import isac.util.formulae.Position

    33 import isac.util.formulae.Reference

    34 import isac.util.formulae.Specification

    35 import isac.util.tactics.TermTactic

    36 import isac.util.tactics.Rewrite

    37 import isac.util.tactics.RewriteInst

    38 import isac.util.tactics.RewriteSet

    39 import isac.util.tactics.RewriteSetInst

    40 import isac.util.tactics.SimpleTactic

    41 import isac.util.tactics.StringListTactic

    42 import isac.util.tactics.SubProblemTactic

    43 import isac.util.tactics.SubstituteTactic

    44 import isac.util.tactics.Tactic

    45 import isac.util.tactics.Theorem

    46 import isac.util.Variant

    48 import edu.tum.cs.isabelle.api.XML

    49 import edu.tum.cs.isabelle.pure._  // for Term

    50 import edu.tum.cs.isabelle._       // for Codec

    52 import java.util.ArrayList

    53 import java.util.Vector

    54 import java.math.BigInteger

    55 import scala.math.BigInt

    56 import scala.collection.JavaConverters._

    58 /**

    59  * conversion XML <--> Java-objects in isac-java used by libisabelle;

    60  * analogous to isabisac/src/Tools/isac/xmlsrc/datatypes.sml.

    61  */

    62 object DataTypes {

    64   /**

    65    *  auxiliary methods, both directions

    66    **/

    68   def xml_of_int (i: scala.math.BigInt): XML.Tree = {

    69     XML.Elem(("INT", Nil), List(XML.Text(i.toString)))

    70   }

    71   def xml_to_int (t: XML.Tree): scala.math.BigInt = t match {

    72     case XML.Elem(("INT", Nil), List(XML.Text(i))) => BigInt(i)

    73     case _ => throw new IllegalArgumentException("xml_to_int exn")

    74   }

    75   def xml_of_ints (is: List[scala.math.BigInt]): XML.Tree = {

    76     XML.Elem(("INTLIST", Nil), is map xml_of_int)

    77   }

    78   def xml_to_ints (t: XML.Tree): List[scala.math.BigInt] = t match {

    79     case XML.Elem(("INTLIST", Nil), is) => is map xml_to_int

    80     case _ => throw new IllegalArgumentException("xml_to_ints exn")

    81   }

    82   def xml_of_pos (ints: List[scala.math.BigInt], kind: String ): XML.Tree = {

    83     XML.Elem(("POSITION", Nil), List(

    84       xml_of_ints(ints),

    85       XML.Elem(("POS", Nil), List(XML.Text(kind)))))

    86   }

    87   def xml_to_pos (t: XML.Tree): (List[scala.math.BigInt], String) = t match {

    88     case XML.Elem(("POSITION", Nil), List(

    89         is, XML.Elem(("POS", Nil), List(XML.Text(kind))))) => (xml_to_ints(is), kind)

    90     case _ => throw new IllegalArgumentException("xml_to_pos exn")

    91   }

    92   def xml_to_VectorString (t: XML.Tree): Vector[java.lang.String] = t match {

    93     case XML.Elem(("STRINGLIST", Nil), is) => {

    94       val v = new java.util.Vector[java.lang.String];

    95       is.foreach {

    96         case (XML.Elem(("STRING", Nil), List(XML.Text(str))))

    97           => v.add(str)

    98         case _ => throw new IllegalArgumentException("xml_to_VectorString 1 wrong arg: " + t)

    99       }

   100       v

   101     }

   102     case _ => throw new IllegalArgumentException("xml_to_VectorString 2 wrong arg: " + t)

   103   }

   104   def  xml_of_VectorString(strs: Vector[java.lang.String]): XML.Tree = {

   105     XML.Elem(("STRINGLIST", Nil),

   106       strs.asScala.toList map xml_of_str)

   107   }

   108   def xml_to_VectorTactic (t: XML.Tree): Vector[Tactic] = t match {

   109     case XML.Elem(("TACLIST", Nil), tacs_xml) => {

   110       val v = new java.util.Vector[Tactic];

   111       tacs_xml.foreach { tac_xml => v.add(xml_to_Tactic(tac_xml)) }

   112       v

   113     }

   114     case _ => throw new IllegalArgumentException("xml_to_VectorTactic wrong arg: " + t)

   115   }

   117   // Note: java.int-->scala.BigInt not done here, because "int" is unknown in Scala.

   118   def Integer_to_BigInt (i: java.lang.Integer): scala.math.BigInt = {

   119     new scala.math.BigInt(new BigInteger(i.toString)) //TODO: improve conversion ?

   120   }

   121   // UNUSED conversion scala.math.BigInt --> java.lang.Integer

   122   def BigInt_to_Integer (i: scala.math.BigInt): java.lang.Integer = {

   123     new java.lang.Integer(i.toString) //TODO: improve conversion ?

   124   }

   125   def xml_of_str (s: String): XML.Tree = {

   126     XML.Elem(("STRING", Nil), List(XML.Text(s)))

   127   }

   128   def xml_to_str (t: XML.Tree): String = t match {

   129     case XML.Elem(("STRING", Nil), List(XML.Text(s))) => s

   130     case _ => throw new IllegalArgumentException("xml_to_str exn")

   131   }

   132   def xml_of_strs (ss: List[String]): XML.Tree = {

   133     XML.Elem(("STRINGLIST", Nil), ss map xml_of_str)

   134   }

   135   def xml_to_strs (t: XML.Tree): List[String] = t match {

   136     case XML.Elem(("STRINGLIST", Nil), ss) => ss map xml_to_str

   137     case _ => throw new IllegalArgumentException("xml_to_strs exn")

   138   }

   139   def xml_of_spec (thy: String, pbl: ArrayList[String], met: ArrayList[String]): XML.Tree = {

   140     XML.Elem(("SPECIFICATION", Nil), List(

   141       XML.Elem(("THEORYID", Nil), List(XML.Text(thy))),

   142       XML.Elem(("PROBLEMID", Nil), List(xml_of_strs(pbl.asScala.toList))),

   143       XML.Elem(("METHODID", Nil), List(xml_of_strs(met.asScala.toList)))))

   144   }

   145   def xml_to_spec (t: XML.Tree) = t match {

   146     case XML.Elem(("SPECIFICATION", Nil), List(

   147       XML.Elem(("THEORYID", Nil), List(XML.Text(thy))),

   148       XML.Elem(("PROBLEMID", Nil), List(pbl)),

   149       XML.Elem(("METHODID", Nil), List(met)))) =>

   150         (thy, DataTypes.xml_to_strs(pbl), xml_to_strs(met))

   151     case _ => throw new IllegalArgumentException("xml_to_spec exn")

   152   }

   153   def xml_to_VectorInteger (t: XML.Tree): Vector[java.lang.Integer] = t match {

   154     case XML.Elem(("INTLIST", Nil), is) => {

   155       val v = new java.util.Vector[java.lang.Integer];

   156       is.foreach {

   157         case (XML.Elem(("INT", Nil), List(XML.Text(i))))

   158           => v.add(new java.lang.Integer(i))

   159         case _ => throw new IllegalArgumentException("xml_to_VectorInteger 1 wrong arg: " + t)

   160       }

   161       v

   162     }

   163     case _ => throw new IllegalArgumentException("xml_to_VectorInteger 2 wrong arg: " + t)

   164   }

   165   def sListToVectorCalcFormula (forms: List[CalcFormula]): Vector[CalcFormula] = {

   166       val v = new java.util.Vector[CalcFormula];

   167       forms.foreach { form => v.add(form) }

   168       v

   169   }

   170   def sListToVectorFormula (forms: List[Formula]): Vector[Formula] = {

   171       val v = new java.util.Vector[Formula];

   172       forms.foreach { form => v.add(form) }

   173       v

   174   }

   175   def sListToVectorFormulaPair (forms: List[FormulaPair]): Vector[FormulaPair] = {

   176       val v = new java.util.Vector[FormulaPair];

   177       forms.foreach { form => v.add(form) }

   178       v

   179   }

   180   def xml_to_String (t: XML.Tree): java.lang.String = t match {

   181     case XML.Text(str) => str

   182     case _ => throw new IllegalArgumentException("xml_to_String wrong arg: " + t)

   183     }

   184   def xml_of_term (str: String): XML.Tree = {

   185     XML.Elem(("MATHML", Nil), List(

   186         XML.Elem(("ISA", Nil), List(XML.Text(str)))))

   187   }

   188   def xml_to_term (t: XML.Tree): java.lang.String = t match {

   189     case

   190       XML.Elem(("MATHML", Nil), List(

   191           XML.Elem(("ISA", Nil), List(XML.Text(str)))))

   192       => str

   193     case _ => throw new IllegalArgumentException("xml_to_term wrong arg: " + t)

   194   }

   195   def xml_of_Term (t: Term): XML.Tree =

   196     XML.Elem(("MATHML", Nil), List(

   197       XML.Elem(("ISA", Nil), List(XML.Text(Util.string_of(t)))),

   198       XML.Elem(("TERM", Nil), List(Codec[Term].encode(t)))))

   200   def xml_to_prog (t: XML.Tree): java.lang.String = t match {

   201     case

   202       XML.Elem(("NOCODE", Nil), List(XML.Text(str)))

   203       => str

   204     case

   205       XML.Elem(("CODE", Nil), List(term_xml))

   206       => xml_to_term(term_xml)

   207     case _ => throw new IllegalArgumentException("xml_to_prog wrong arg: " + t)

   208   }

   210   /**

   211    *  conversion XML <--> Java-objects in isac-java used by libisabelle

   212    **/

   214    // <--ISA carries a "status" computed by Math_Engine

   215    def xml_to_ModelItem(t: XML.Tree): isac.util.formulae.ModelItem = t match {

   216     case

   217       XML.Elem(("ITEM", List(("status", status))), List(

   218         XML.Elem(("MATHML", Nil), List(

   219           XML.Elem(("ISA", Nil), List(XML.Text(form_isa)))))))

   220       => new ModelItem(status, form_isa)

   221     case _ => throw new IllegalArgumentException("xml_to_ModelItem wrong arg: " + t)

   222   }

   223    // -->ISA carries NO "status" coming from user.

   224   def xml_of_ModelItem(item: ModelItem): XML.Tree = {

   225     XML.Elem(("ITEM", Nil), List(

   226       XML.Elem(("MATHML", Nil), List(

   227         XML.Elem(("ISA", Nil), List(XML.Text(item.getFormula.toSMLString)))))))

   228   }

   229   def sList2jVectorModelItem(ilist: List[ModelItem]): Vector[ModelItem] = {

   230     val ivect = new Vector[ModelItem]

   231     for (n <- 0 to ilist.size - 1) ivect.add(ilist(n))

   232     ivect

   233   }

   234   //for test on console:

   235   def sList2jVector(ilist: List[Integer]): Vector[Integer] = {

   236     val ivect = new Vector[Integer]

   237     for (n <- 0 to ilist.size - 1) ivect.add(ilist(n))

   238     ivect

   239   }

   240   def xml_to_VectorModelItem(t: XML.Tree): java.util.Vector[ModelItem] = t match {

   241     case

   242       XML.Elem(("GIVEN", Nil), list_xml)

   243       => sList2jVectorModelItem(list_xml map xml_to_ModelItem)

   244     case

   245       XML.Elem(("WHERE", Nil), list_xml)

   246       => sList2jVectorModelItem(list_xml map xml_to_ModelItem)

   247     case

   248       XML.Elem(("FIND", Nil), list_xml)

   249       => sList2jVectorModelItem(list_xml map xml_to_ModelItem)

   250     case

   251       XML.Elem(("RELATE", Nil), list_xml)

   252       => sList2jVectorModelItem(list_xml map xml_to_ModelItem)

   253     case _ => throw new IllegalArgumentException("xml_to_VectorModelItem wrong arg: " + t)

   254   }

   255   def xml_to_Model(t: XML.Tree): Model = t match {

   256     case

   257       XML.Elem(("MODEL", Nil), List(xml_given, xml_where, xml_find, xml_relate))

   258       => new Model(

   259           new ModelItemList(xml_to_VectorModelItem(xml_given)),

   260           new ModelItemList(xml_to_VectorModelItem(xml_where)),

   261           new ModelItemList(xml_to_VectorModelItem(xml_find)),

   262           new ModelItemList(xml_to_VectorModelItem(xml_relate)))

   263     case _ => throw new IllegalArgumentException("xml_to_Model wrong arg: " + t)

   264   }

   265   //

   266   // status (coming from user) is irrelevant: status is computed by Math_Engine

   267   def xml_of_Item(item: ModelItem): XML.Tree = {

   268     XML.Elem(("ITEM", Nil), List(

   269       xml_of_term(item.getFormula.toString)))

   270   }

   271   def xml_of_items(tag: String, items: java.util.Vector[ModelItem]): XML.Tree = {

   272     var xml: List[XML.Tree] = List()

   273     for (n <- 0 to items.size - 1) { ((xml_of_Item(items.elementAt(n))) :: xml) }

   274     XML.Elem((tag, Nil), xml.reverse)

   275   }

   276   // status (coming from user) is irrelevant: status is computed by Math_Engine

   277   def xml_of_Model(model: Model): XML.Tree = {

   278     XML.Elem(("MODEL", Nil), List(

   279       xml_of_items("GIVEN", model.getGiven.getItems),

   280       // xml_where, is never input by user

   281       xml_of_items("FIND", model.getFind.getItems),

   282       xml_of_items("RELATE", model.getRelate.getItems)

   283       ))

   284   }

   286   def xml_to_Specification(t: XML.Tree): isac.util.formulae.Specification = t match {

   287     case

   288       XML.Elem(("SPECIFICATION", Nil), List(

   289         XML.Elem(("THEORYID", Nil), List(xml_thy)),

   290         XML.Elem(("PROBLEMID", Nil), List(xml_pbl)),

   291         XML.Elem(("METHODID", Nil), List(xml_met))))

   292       => { val thy_key = new CalcHeadSimpleID

   293              thy_key.setID(DataTypes.xml_to_String(xml_thy))

   294            val pbl_key = new HierarchyKey

   295              pbl_key.setID(xml_to_VectorString(xml_pbl))

   296            val met_key = new HierarchyKey

   297              met_key.setID(xml_to_VectorString(xml_met))

   298            new Specification(thy_key, pbl_key, met_key)

   299         }

   300     case _ => throw new IllegalArgumentException("xml_to_Specification wrong arg: " + t)

   301   }

   303   def xml_to_CalcHead(t: XML.Tree): CalcHead = t match {

   304     case

   305         XML.Elem(("CALCHEAD", List(("status", status))), List(

   306           xml_pos, xml_head, xml_model,

   307           XML.Elem(("BELONGSTO", Nil), List(XML.Text(pbl_met))),

   308           xml_spec))

   309       => {

   310         println("1a xml_to_CalcHead "+xml_head);

   311         println("1b xml_to_CalcHead "+DataTypes.xml_to_Head(xml_head));

   312         new CalcHead(DataTypes.xml_to_Position(xml_pos),

   313           DataTypes.xml_to_Head(xml_head), xml_to_Model(xml_model),

   314           pbl_met, xml_to_Specification(xml_spec), status)

   315       }

   316     case _ => throw new IllegalArgumentException("xml_to_CalcHead wrong arg: " + t)

   317   }

   318   def xml_of_CalcHead(chead: CalcHead):  XML.Tree = {

   319     XML.Elem(("CALCHEAD", List(("status", chead.getStatusString))), List(

   320       xml_of_Position(chead.getPosition),

   321       xml_of_Head(chead.getHeadLine),

   322       xml_of_Model(chead.getModel),

   323       XML.Elem(("BELONGSTO", Nil), List(XML.Text(chead.getBelongsTo))),

   324       xml_of_Specification(chead.getSpecification)))

   325   }

   326   def xml_to_Formula(t: XML.Tree): isac.util.formulae.Formula = t match {

   327     case

   328       XML.Elem(("FORMULA", Nil), List(

   329         XML.Elem(("MATHML", Nil), List(

   330           XML.Elem(("ISA", Nil), List(XML.Text(form_isa)))))))

   331       =>  new Formula(form_isa)

   332     case _ => throw new IllegalArgumentException("xml_to_Formula wrong arg: " + t)

   333   }

   334   def xml_to_Head(t: XML.Tree): isac.util.formulae.Formula = t match {

   335     case

   336       XML.Elem(("HEAD", Nil), List(form_xml)) => {

   337       println("2a xml_to_Head "+"found HEAD");

   338       xml_to_Formula_NEW(form_xml)

   339     }

   340     case _ => {

   341       println("2b xml_to_Head "+"Exception");

   342       throw new IllegalArgumentException("xml_to_Formula wrong arg: " + t)

   343     }

   344   }

   345   def xml_to_Formula_NEW(t: XML.Tree): isac.util.formulae.Formula = t match {

   346     case

   347         XML.Elem(("FORMULA", Nil), List(

   348           XML.Elem(("ISA", Nil), List(XML.Text(str))),

   349           XML.Elem(("TERM", Nil), List(term))))

   350       => new Formula(str, Syntax_Phases.term_to_ast(Codec[Term].decode(term).right.get))

   351       // TODO: catch exn which might be thrown by "right.get"

   352     case _ => throw new IllegalArgumentException("xml_to_Formula_NEW wrong arg: " + t)

   353   }

   354   // for test purposes

   355   def xml_to_Term(t: XML.Tree): Term = t match {

   356     case

   357       XML.Elem(("FORMULA", Nil), List(

   358         XML.Elem(("ISA", Nil), List(XML.Text(str))),

   359         XML.Elem(("TERM", Nil), List(term))))

   360       => Codec[Term].decode(term).right.get

   361       // TODO: catch exn which might be thrown by "right.get"

   362     case _ => throw new IllegalArgumentException("xml_to_Term wrong arg: " + t)

   363   }

   365   /*

   366    * WN160512 presently there is no transport of Terms from the GUI to the MathEngine

   367    * and it is questionable whether such transport will be implemented at all.

   368    * So this method might take a String as argument (and send no TERM), like xml_of_Formula.

   369    */

   370   def xml_of_Formula_UNUSED(form: Formula): XML.Tree = {

   371     XML.Elem(("MATHML", Nil), List(

   372       XML.Elem(("ISA", Nil), List(XML.Text("TODO form.getString() OR form.toSMLString()"))),

   373       XML.Elem(("TERM", Nil), List(Codec[Term].encode(Syntax_Phases.ast_to_term(form.getTerm))))))

   374   }

   375  /* TODO we plan to send both, String and Term to Isabelle_Isac.

   376    * In a later phase of development Isabelle_Isac will decide whether to use

   377    * either String or Term (after conversion from Ast).

   378    */

   379   def xml_of_Formula_NEW(form: Formula): XML.Tree = {

   380     XML.Elem(("FORMULA", Nil), List(

   381       XML.Elem(("ISA", Nil), List(XML.Text(form.toString)))//,

   382       //XML.Elem(("TERM", Nil), List(Codec[Term].encode(Syntax_Phases.ast_to_term(form.getTerm))))

   383       ))

   384   }

   385   def xml_of_Formula(form_isa: Formula): XML.Tree = {

   386     XML.Elem(("FORMULA", Nil), List(

   387       XML.Elem(("MATHML", Nil), List(

   388         XML.Elem(("ISA", Nil), List(XML.Text(form_isa.toString)))))))

   389   }

   390   def xml_of_Head(head_isa: Formula): XML.Tree = {

   391     XML.Elem(("HEAD", Nil), List(xml_of_Formula_NEW(head_isa)))

   392   }

   393   def xml_to_CalcFormula(t: XML.Tree): CalcFormula = t match {

   394     case

   395       XML.Elem(("CALCFORMULA", Nil), List(pos, form))

   396       => new CalcFormula(xml_to_Position(pos), xml_to_Formula_NEW(form))

   397     case _ => throw new IllegalArgumentException("xml_to_CalcFormula wrong arg: " + t)

   398   }

   399   def xml_of_CalcFormula(calc_form: CalcFormula): XML.Tree = {

   400     XML.Elem(("CALCFORMULA", Nil), List(

   401       xml_of_Position(calc_form.getPosition),

   402       xml_of_Formula(calc_form.getFormula)))

   403   }

   404   def xml_of_Formalization(fmz: Formalization): XML.Tree = {

   405     if (fmz.getVariants.size == 0) { //..from <NEW> on GUI, then Isabelle/Isac expects..

   406       XML.Elem(("FORMALIZATION", Nil), List(

   407         XML.Elem(("VARIANT", Nil), List(

   408           XML.Elem(("STRINGLIST", Nil), Nil),

   409           XML.Elem(("SPECIFICATION", Nil), List(

   410             XML.Elem(("THEORYID", Nil), List(XML.Text("e_domID"))),

   411             XML.Elem(("PROBLEMID", Nil), List(

   412               XML.Elem(("STRINGLIST", Nil), List(

   413                 XML.Elem(("STRING", Nil), List(XML.Text("e_pblID"))))))),

   414             XML.Elem(("METHODID", Nil), List(

   415               XML.Elem(("STRINGLIST", Nil), List(

   416                 XML.Elem(("STRING", Nil), List(XML.Text("e_metID")))))))))))))

   417     } else {

   418       XML.Elem(("FORMALIZATION", Nil), fmz.getVariants.asScala.toList map xml_of_Variant)

   419     }

   420   }

   421   def xml_of_Position(pos: Position): XML.Tree = {

   422     val is: List[Integer] = pos.getIntList.asInstanceOf[Vector[Integer]].asScala.toList

   423     xml_of_pos(is map Integer_to_BigInt, pos.getKind)

   424   }

   425   def xml_to_Position(t: XML.Tree): Position = t match {

   426     case

   427       XML.Elem(("POSITION", Nil), List(

   428         ints, XML.Elem(("POS", Nil), List(XML.Text(kind)))))

   429       => new Position(xml_to_VectorInteger(ints), kind)

   430     case _ => throw new IllegalArgumentException("xml_to_Position wrong arg: " + t)

   431   }

   432   def xml_of_Specification(spec: Specification): XML.Tree = {

   433     XML.Elem(("SPECIFICATION", Nil), List(

   434       XML.Elem(("THEORYID", Nil), List(XML.Text(spec.getTheory.getID))),

   435       XML.Elem(("PROBLEMID", Nil), List(

   436         DataTypes.xml_of_strs(spec.getProblem.getID.asScala.toList))),

   437       XML.Elem(("METHODID", Nil), List(

   438         DataTypes.xml_of_strs(spec.getMethod.getID.asScala.toList)))))

   439   }

   440   def xml_of_Variant(vat: isac.util.Variant): XML.Tree = {

   441     XML.Elem(("VARIANT", Nil), List(

   442       DataTypes.xml_of_strs(vat.getIsaStrings.asScala.toList),

   443       xml_of_Specification(vat.getSpecification)))

   444   }

   445   def xml_of_ContextType(ctxt_typ: isac.wsdialog.IContextProvider.ContextType): XML.Tree = {

   446     XML.Elem(("KETYPE", Nil), List(XML.Text(ctxt_typ.toString)))

   447   }

   449   // from isac-java to kernel goes only "ISA", no "TERM"

   450   // repair: replace "FORMULA" by "ISA"

   451   def xml_of_Theorem(thm: Theorem): XML.Tree = {

   452     XML.Elem(("THEOREM", Nil), List(

   453       XML.Elem(("ID", Nil), List(XML.Text(thm.getId))),

   454       XML.Elem(("FORMULA", Nil), List(

   455         XML.Text(thm.getFormula))))) // term instead String for MathML

   456   }

   457   // from isac-java to kernel goes only "ISA", no "TERM"

   458   // repair: replace "FORMULA" by "ISA"

   459   def xml_to_Theorem(t: XML.Tree): Theorem = t match {

   460     case

   461       XML.Elem(("THEOREM", Nil), List(

   462         XML.Elem(("ID", Nil), List(XML.Text(id))),

   463         XML.Elem(("FORMULA", Nil), List(

   464           XML.Text(form)))))  // term instead String for MathML

   465       => new Theorem(id, form)

   466     case x => throw new IllegalArgumentException("xml_to_Theorem WRONG arg = " + x)

   467   }

   469   //----- FOR xml_of_Tactic --------------------------------------------*)

   470   def xml_of_SubProblemTactic(tac: SubProblemTactic): XML.Tree = {

   471     XML.Elem(("SUBPROBLEMTACTIC", List(("name", tac.getName))), List(

   472       XML.Elem(("THEORY", Nil), List(XML.Text(tac.getTheoryID))),

   473       XML.Elem(("PROBLEM", Nil), List(xml_of_VectorString(tac.getProblemID)))))

   474   }

   475   // Substitute see //----- STRINGLISTTACTIC below

   477   //----- Rewrite* -----------------------------------------------------*)

   478   def xml_of_Rewrite(tac: Rewrite): XML.Tree = {

   479     XML.Elem(("REWRITETACTIC", List(("name", tac.getName))), List(

   480       xml_of_Theorem(tac.getTheorem)))

   481   }

   482   def xml_of_RewriteInst(tac: RewriteInst): XML.Tree = {

   483     XML.Elem(("REWRITEINSTTACTIC", List(("name", tac.getName))), List(

   484       //this will be generalised at introduction of MathML

   485       XML.Elem(("PAIR", Nil), List(

   486         XML.Elem(("VARIABLE", Nil), List(

   487           XML.Elem(("MATHML", Nil), List(

   488             XML.Elem(("ISA", Nil), List(XML.Text(tac.getVariable))))))),

   489         XML.Elem(("VALUE", Nil), List(

   490           XML.Elem(("MATHML", Nil), List(

   491             XML.Elem(("ISA", Nil), List(XML.Text(tac.getValue))))))))),

   492       xml_of_Theorem(tac.getTheorem)))

   493   }

   494   def xml_of_RewriteSet(tac: RewriteSet): XML.Tree = {

   495     XML.Elem(("REWRITESETTACTIC", List(("name", tac.getName))), List(

   496       XML.Text(tac.getRuleSet)))

   497   }

   498   def xml_of_RewriteSetInst(tac: RewriteSetInst): XML.Tree = {

   499     XML.Elem(("REWRITESETINSTTACTIC", List(("name", tac.getName))), List(

   500       //this will be generalised at introduction of MathML

   501       XML.Elem(("PAIR", Nil), List(

   502         XML.Elem(("VARIABLE", Nil), List(

   503           XML.Elem(("MATHML", Nil), List(

   504             XML.Elem(("ISA", Nil), List(XML.Text(tac.getVariable))))))),

   505         XML.Elem(("VALUE", Nil), List(

   506           XML.Elem(("MATHML", Nil), List(

   507             XML.Elem(("ISA", Nil), List(XML.Text(tac.getValue))))))))),

   508       XML.Text(tac.getRuleSet)))

   509   }

   511   //----- FORMTACTIC ---------------------------------------------------*)

   512   def xml_of_TermTactic(formtac: TermTactic): XML.Tree = {

   513     XML.Elem(("FORMTACTIC", List(("name", formtac.getName))), List(

   514       xml_of_term(formtac.getTerm)))

   515   }

   516   //----- SIMPLETACTIC -------------------------------------------------*)

   517   def xml_of_SimpleTactic(tac: SimpleTactic): XML.Tree = {

   518     XML.Elem(("SIMPLETACTIC", List(("name", tac.getName))), List(

   519       xml_of_term(tac.getArgument)))

   520   }

   521   //----- STRINGLISTTACTIC ---------------------------------------------*)

   522   def dest_eq(equality: String): (String, String) = {

   523     val pair = equality.split("=")

   524     if (pair.length == 2) (pair(0), pair(1))

   525     else throw new IllegalArgumentException("dest_eq WRONG arg = " + equality)

   526   }

   527   def xml_of_val_var_pair(vv: (String, String)): XML.Tree = {

   528     XML.Elem(("PAIR", Nil), List(

   529       XML.Elem(("VARIABLE", Nil), List(

   530         XML.Elem(("MATHML", Nil), List(

   531           XML.Elem(("ISA", Nil), List(XML.Text(vv._1))))))),

   532       XML.Elem(("VALUE", Nil), List(

   533         XML.Elem(("MATHML", Nil), List(

   534           XML.Elem(("ISA", Nil), List(XML.Text(vv._2)))))))))

   535   }

   536   def xml_of_sube(equs: Vector[String]): XML.Tree = {

   537     XML.Elem(("SUBSTITUTION", Nil),

   538       (equs.asScala.toList map dest_eq) map xml_of_val_var_pair)

   539   }

   540   def xml_of_StringListTactic(strs_tac: StringListTactic): XML.Tree = {

   541     var xml = XML.Text("DUMMY"): XML.Tree

   542     if (strs_tac.getName == "Substitute")

   543       xml = xml_of_VectorString(strs_tac.getStrings)

   544     else

   545       xml = xml_of_VectorString(strs_tac.getStrings)

   546     XML.Elem(("STRINGLISTTACTIC", List(("name", strs_tac.getName))), List(

   547       xml))

   548   }

   549   // def xml_of_Tactic(tac: Tactic): XML.Tree = tac.getClass match {

   550   //   was shifted to DataTypesCompanion.java

   551   def xml_to_Tactic(t: XML.Tree): Tactic = t match {

   552     case

   553       XML.Elem(("SUBPROBLEMTACTIC", List(("name", "Subproblem"))), List(

   554         XML.Elem(("THEORY", Nil), List(XML.Text(thy))),

   555         XML.Elem(("PROBLEM", Nil), List(pbl))))

   556       => new SubProblemTactic("Subproblem", thy, xml_to_VectorString(pbl))

   557     case

   558       XML.Elem(("STRINGLISTTACTIC", List(("name", "Substitute"))), List(

   559           XML.Elem(("PAIR", Nil), List(

   560             XML.Elem(("VARIABLE", Nil), List(

   561               XML.Elem(("MATHML", Nil), List(

   562                 XML.Elem(("ISA", Nil), List(XML.Text(variable))))))),

   563             XML.Elem(("VALUE", Nil), List(

   564               XML.Elem(("MATHML", Nil), List(

   565                 XML.Elem(("ISA", Nil), List(XML.Text(value)))))))))))

   566       => new SubstituteTactic("Substitute", variable, value)

   568     //----- Rewrite* -----------------------------------------------------*)

   569     case

   570       XML.Elem(("REWRITETACTIC", List(("name", "Rewrite"))), List(

   571         thm))

   572       => new Rewrite("Rewrite", xml_to_Theorem(thm))

   573     case // faked until introduction of MathML

   574       XML.Elem(("REWRITEINSTTACTIC", List(("name", "Rewrite_Inst"))), List(

   575         XML.Elem(("SUBSTITUTION", Nil), List(

   576           XML.Elem(("PAIR", Nil), List(

   577             XML.Elem(("VARIABLE", Nil), List(

   578               XML.Elem(("MATHML", Nil), List(

   579                 XML.Elem(("ISA", Nil), List(XML.Text(variable))))))),

   580             XML.Elem(("VALUE", Nil), List(

   581               XML.Elem(("MATHML", Nil), List(

   582                 XML.Elem(("ISA", Nil), List(XML.Text(value)))))))

   583           )))),

   584         thm))

   585       => new RewriteInst("Rewrite_Inst", variable, value, xml_to_Theorem(thm))

   586     case

   587       XML.Elem(("REWRITESETTACTIC", List(("name", "Rewrite_Set"))), List(

   588         XML.Text(rule_set)))

   589       => new RewriteSet("Rewrite_Set", rule_set)

   590     case // faked Term by String until introduction of MathML

   591       XML.Elem(("REWRITESETINSTTACTIC", List(("name", "Rewrite_Set_Inst"))), List(

   592         XML.Elem(("SUBSTITUTION", Nil), List(

   593           XML.Elem(("PAIR", Nil), List(

   594             XML.Elem(("VARIABLE", Nil), List(

   595               XML.Elem(("MATHML", Nil), List(

   596                 XML.Elem(("ISA", Nil), List(XML.Text(variable))))))),

   597             XML.Elem(("VALUE", Nil), List(

   598               XML.Elem(("MATHML", Nil), List(

   599                 XML.Elem(("ISA", Nil), List(XML.Text(value))))))))))),

   600         XML.Elem(("RULESET", Nil), List(XML.Text(rule_set)))))

   601         // ATTENTION: args--vv are shuffled wrt. RewriteInst

   602       => new RewriteSetInst("Rewrite_Set_Inst", rule_set, variable, value)

   604     //----- FORMTACTIC ---------------------------------------------------*)

   605     case

   606       XML.Elem(("FORMTACTIC", List(("name", "Add_Find"))), List(

   607         term))

   608       => new TermTactic("Add_Find", xml_to_term(term))

   609     case

   610       XML.Elem(("FORMTACTIC", List(("name", "Add_Given"))), List(

   611         term))

   612       => new TermTactic("Add_Given", xml_to_term(term))

   613     case

   614       XML.Elem(("FORMTACTIC", List(("name", "Add_Relation"))), List(

   615         term))

   616       => new TermTactic("Add_Relation", xml_to_term(term))

   617     case

   618       XML.Elem(("FORMTACTIC", List(("name", "Check_elementwise"))), List(

   619         term))

   620       => new TermTactic("Check_elementwise", xml_to_term(term))

   621     case

   622       XML.Elem(("FORMTACTIC", List(("name", "Take"))), List(

   623         term))

   624       => new TermTactic("Take", xml_to_term(term))

   626     //----- SIMPLETACTIC -------------------------------------------------*)

   627     case

   628       XML.Elem(("SIMPLETACTIC", List(("name", "Or_to_List"))), List(

   629         XML.Text(_)))

   630       => new SimpleTactic("Or_to_List", "DUMMY")

   631     case

   632       XML.Elem(("SIMPLETACTIC", List(("name", "Specify_Theory"))), List(

   633         XML.Text(str)))

   634       => new SimpleTactic("Specify_Theory", str)

   636     //----- STRINGLISTTACTIC ---------------------------------------------*)

   637     case

   638       XML.Elem(("STRINGLISTTACTIC", List(("name", "Apply_Method"))), List(

   639         strs))

   640       => new StringListTactic("Apply_Method", xml_to_VectorString(strs))

   641     case

   642       XML.Elem(("STRINGLISTTACTIC", List(("name", "Check_Postcond"))), List(

   643         strs))

   644       => new StringListTactic("Check_Postcond", xml_to_VectorString(strs))

   645     case

   646       XML.Elem(("STRINGLISTTACTIC", List(("name", "Model_Problem"))), List(

   647         strs))

   648       => new StringListTactic("Model_Problem", xml_to_VectorString(strs))

   649     case

   650       XML.Elem(("STRINGLISTTACTIC", List(("name", "Refine_Tacitly"))), List(

   651         strs))

   652       => new StringListTactic("Refine_Tacitly", xml_to_VectorString(strs))

   653     case

   654       XML.Elem(("STRINGLISTTACTIC", List(("name", "Specify_Method"))), List(

   655         strs))

   656       => new StringListTactic("Specify_Method", xml_to_VectorString(strs))

   657     case

   658       XML.Elem(("STRINGLISTTACTIC", List(("name", "Specify_Problem"))), List(

   659         strs))

   660       => new StringListTactic("Specify_Problem", xml_to_VectorString(strs))

   661     case x => throw new IllegalArgumentException("xml_to_Tactic WRONG arg = " + x)

   662   }

   664   //------- for xml_of_contthy

   665   //--- see Isabelle/Isac:../datatypes.sml

   666   def xml_to_Reference(t: XML.Tree): Reference = t match {

   667     case

   668       XML.Elem(("KESTOREREF", Nil), List(

   669         XML.Elem(("TAG", Nil), List(XML.Text(tag))),

   670         XML.Elem(("ID", Nil), List(XML.Text(xstring))),

   671         XML.Elem(("GUH", Nil), List(XML.Text(guh)))))

   672       => new Reference(tag, xstring, new KEStoreKey(guh))

   673     case t => throw new IllegalArgumentException("xml_to_Reference wrong arg: " + t)

   674   }

   676   def xml_to_asm_val(t: XML.Tree): FormulaPair = t match {

   677     case

   678       XML.Elem(("ASMEVALUATED", Nil), List(

   679         XML.Elem(("ASM", Nil), List(asm)),

   680         XML.Elem(("VALUE", Nil), List(vl))))

   681       => new FormulaPair(new Formula(xml_to_term(asm)), /*new Formula((xml_to_term(vl)))*/true)

   682     case t => throw new IllegalArgumentException("xml_to_asm_val wrong arg: " + t)

   683   }

   684   def xml_to_ContextTheory(t: XML.Tree): ContextTheory = t match {

   685     //  | xml_of_contthy (ContThm {thyID, thm, applto, applat, reword,

   686     //        asms,lhs, rhs, result, resasms, asmrls}) =

   687     case

   688       XML.Elem(("CONTEXTDATA", Nil), List(

   689         XML.Elem(("GUH", Nil), List(XML.Text(guh))),

   690         XML.Elem(("APPLTO", Nil), List(applto_xml)),

   691         XML.Elem(("APPLAT", Nil), List(applat_xml)),

   692         XML.Elem(("ORDER", Nil), List(

   693           XML.Elem(("ID", Nil), List(XML.Text(reword))))),

   694         XML.Elem(("ASMSEVAL", Nil), asmevs_xml),    //Nil is possible

   695         XML.Elem(("LHS", Nil), List(lhs_xml)),

   696         XML.Elem(("LHSINST", Nil), List(lhsinst_xml)),

   697         XML.Elem(("RHS", Nil), List(rhs_xml)),

   698         XML.Elem(("RHSINST", Nil), List(rhsinst_xml)),

   699         XML.Elem(("RESULT", Nil), List(result_xml)),

   700         XML.Elem(("ASSUMPTIONS", Nil), asms_xml),   //Nil is possible

   701         XML.Elem(("EVALRLS", Nil), List(rlskey_xml))))

   702       => new ContextTheory(new KEStoreKey(guh),

   703           null, null,

   704           new Formula(xml_to_term(applto_xml)), new Formula(xml_to_term(applat_xml)),

   705           reword,

   706           sListToVectorFormulaPair(asmevs_xml map xml_to_asm_val), //WN150820 bug: Boolean form_2

   707           new Formula(xml_to_term(lhs_xml)), new Formula(xml_to_term(lhsinst_xml)),

   708           new Formula(xml_to_term(rhs_xml)), new Formula(xml_to_term(rhsinst_xml)),

   709           new Formula(xml_to_term(result_xml)), "xml_to_ContextTheory: ASSUMPTIONS wrong type",

   710           xml_to_Reference(rlskey_xml))

   711     //  | xml_of_contthy (ContThmInst {thyID, thm, bdvs, thminst, applto, applat,

   712     //        reword, asms, lhs, rhs, result, resasms, asmrls}) =

   713     case

   714       XML.Elem(("CONTEXTDATA", Nil), List(

   715         XML.Elem(("GUH", Nil), List(XML.Text(guh))),

   716         XML.Elem(("SUBSLIST", Nil), List(subst_xml)), // WRONG type

   717         XML.Elem(("INSTANTIATED", Nil), List(thminst_xml)),

   718         XML.Elem(("APPLTO", Nil), List(applto_xml)),

   719         XML.Elem(("APPLAT", Nil), List(applat_xml)),

   720         XML.Elem(("ORDER", Nil), List(

   721           XML.Elem(("ID", Nil), List(XML.Text(reword))))),

   722         XML.Elem(("ASMSEVAL", Nil), asmevs_xml),    //Nil is possible

   723         XML.Elem(("LHS", Nil), List(lhs_xml)),

   724         XML.Elem(("LHSINST", Nil), List(lhsinst_xml)),

   725         XML.Elem(("RHS", Nil), List(rhs_xml)),

   726         XML.Elem(("RHSINST", Nil), List(rhsinst_xml)),

   727         XML.Elem(("RESULT", Nil), List(result_xml)),

   728         XML.Elem(("ASSUMPTIONS", Nil), asms_xml),   //Nil is possible

   729         XML.Elem(("EVALRLS", Nil), List(rlskey_xml))))

   730       => new ContextTheory(new KEStoreKey(guh),

   731           new Formula(xml_to_term(subst_xml)), new Formula(xml_to_term(thminst_xml)),

   732           new Formula(xml_to_term(applto_xml)), new Formula(xml_to_term(applat_xml)),

   733           reword,

   734           sListToVectorFormulaPair(asmevs_xml map xml_to_asm_val),

   735           new Formula(xml_to_term(lhs_xml)), new Formula(xml_to_term(lhsinst_xml)),

   736           new Formula(xml_to_term(rhs_xml)), new Formula(xml_to_term(rhsinst_xml)),

   737           new Formula(xml_to_term(result_xml)), "xml_to_ContextTheory: ASSUMPTIONS wrong type",

   738           xml_to_Reference(rlskey_xml))

   739     //  | xml_of_contthy (ContRls {thyID = _, rls, applto, result, asms}) =

   740     case

   741       XML.Elem(("CONTEXTDATA", Nil), List(

   742         XML.Elem(("GUH", Nil), List(XML.Text(guh))),

   743         XML.Elem(("APPLTO", Nil), List(applto_xml)),

   744         XML.Elem(("RESULT", Nil), List(result_xml)),

   745         XML.Elem(("ASSUMPTIONS", Nil), asms_xml)))   //Nil is possible

   746       => new ContextTheory(new KEStoreKey(guh), null, null,

   747           new Formula(xml_to_term(applto_xml)), null,

   748           null,

   749           null,

   750           null, null,

   751           null, null,

   752           new Formula(xml_to_term(result_xml)), "xml_to_ContextTheory: ASSUMPTIONS wrong type",

   753           null)

   754     //  | xml_of_contthy (ContRlsInst {thyID = _, rls, bdvs, applto, result, asms}) =

   755     case

   756       XML.Elem(("CONTEXTDATA", Nil), List(

   757         XML.Elem(("GUH", Nil), List(XML.Text(guh))),

   758         XML.Elem(("SUBSLIST", Nil), List(subst_xml)), // WRONG type

   759         XML.Elem(("INSTANTIATED", Nil), List(thminst_xml)),

   760         XML.Elem(("APPLTO", Nil), List(applto_xml)),

   761         XML.Elem(("RESULT", Nil), List(result_xml)),

   762         XML.Elem(("ASSUMPTIONS", Nil), List(asms_xml))))

   763       => new ContextTheory(new KEStoreKey(guh),

   764           new Formula(xml_to_term(subst_xml)), new Formula(xml_to_term(thminst_xml)),

   765           new Formula(xml_to_term(applto_xml)), null,

   766           null,

   767           null,

   768           null, null,

   769           null, null,

   770           new Formula(xml_to_term(result_xml)), "xml_to_ContextTheory: ASSUMPTIONS wrong type",

   771           null)

   772     //  | xml_of_contthy (ContNOrew {thyID = _, thm_rls, applto}) =

   773     case

   774       XML.Elem(("CONTEXTDATA", Nil), List(

   775         XML.Elem(("GUH", Nil), List(XML.Text(guh))),

   776         XML.Elem(("APPLTO", Nil), List(applto_xml))))

   777       => new ContextTheory(new KEStoreKey(guh), null, null,

   778           new Formula(xml_to_term(applto_xml)), null,

   779           null,

   780           null,

   781           null, null,

   782           null, null,

   783           null, null,

   784           null)

   785     //  | xml_of_contthy (ContNOrewInst{thyID = _, thm_rls, bdvs, thminst, applto}) =

   786     case

   787       XML.Elem(("CONTEXTDATA", Nil), List(

   788         XML.Elem(("GUH", Nil), List(XML.Text(guh))),

   789         XML.Elem(("SUBSLIST", Nil), List(subst_xml)), // WRONG type

   790         XML.Elem(("INSTANTIATED", Nil), List(thminst_xml)),

   791         XML.Elem(("APPLTO", Nil), List(applto_xml))))

   792       => new ContextTheory(new KEStoreKey(guh),

   793           new Formula(xml_to_term(subst_xml)), new Formula(xml_to_term(thminst_xml)),

   794           new Formula(xml_to_term(applto_xml)), null,

   795           null,

   796           null,

   797           null, null,

   798           null, null,

   799           null, null,

   800           null)

   801     case _ => throw new IllegalArgumentException("xml_to_ContextTheory wrong arg: " + t)

   802   }

   804   def xml_to_ContextProblem(t: XML.Tree): ContextProblem = t match {

   805     case

   806       XML.Elem(("CONTEXTDATA", Nil), List(

   807         XML.Elem(("GUH", Nil), List(XML.Text(guh))),

   808         XML.Elem(("STATUS", Nil), List(XML.Text(status))),

   809         XML.Elem(("HEAD", Nil), List(head_xml)),

   810         model_xml))

   811       => new ContextProblem(new KEStoreKey(guh),

   812           status, xml_to_Formula_NEW(head_xml), xml_to_Model(model_xml))

   813     case _ => throw new IllegalArgumentException("xml_to_ContextProblem wrong arg: " + t)

   814   }

   816   def xml_to_ContextMethod(t: XML.Tree): ContextMethod = t match {

   817     case

   818       XML.Elem(("CONTEXTDATA", Nil), List(

   819         XML.Elem(("GUH", Nil), List(XML.Text(guh))),

   820         XML.Elem(("STATUS", Nil), List(XML.Text(status))),

   821         XML.Elem(("PROGRAM", Nil), List(prog_xml)),

   822         model_xml))

   823       => new ContextMethod(new KEStoreKey(guh),

   824           status, new Formula(xml_to_prog(prog_xml)), xml_to_Model(model_xml))

   825     case _ => throw new IllegalArgumentException("xml_to_ContextMethod wrong arg: " + t)

   826   }

   828   def xml_to_CEvent(t: XML.Tree): CEvent = t match {

   829     case

   830       XML.Elem(("CALCCHANGED", Nil), List(

   831         XML.Elem(("UNCHANGED", Nil), List(

   832           unc_is, XML.Elem(("POS", Nil), List(XML.Text(unc_kind))))),

   833         XML.Elem(("DELETED", Nil), List(

   834           del_is, XML.Elem(("POS", Nil), List(XML.Text(del_kind))))),

   835         XML.Elem(("GENERATED", Nil), List(

   836           gen_is, XML.Elem(("POS", Nil), List(XML.Text(gen_kind)))))))

   837       => new CChanged(

   838            new Position(DataTypes.xml_to_VectorInteger(unc_is), unc_kind),

   839            new Position(DataTypes.xml_to_VectorInteger(del_is), del_kind),

   840            new Position(DataTypes.xml_to_VectorInteger(gen_is), gen_kind))

   841     case

   842       XML.Elem(("CALCMESSAGE", Nil), List(XML.Text(msg)))

   843       => new CMessage(msg)

   844     case _ => throw new IllegalArgumentException("xml_to_CChanged wrong arg: " + t)

   845   }

   847 }

author	Walther Neuper <walther.neuper@jku.at>
	Fri, 26 Mar 2021 10:45:05 +0100
changeset 5239	b4e3883d7b66
parent 5229	6bf0e95981e3
permissions	-rw-r--r--