Mercurial Mercurial > wneuper > isac / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
isac-java/src/java/isac/bridge/xml/DataTypes.scala
author Walther Neuper <wneuper@ist.tugraz.at>
Fri, 20 May 2016 11:07:33 +0200
changeset 4916 0393704b8be8
parent 4892 abca3a75f79f
child 4917 15173b75ce2b
permissions -rw-r--r--
TERM: unify XML for Formula --> term

Notes
# cf. https://intra.ist.tugraz.at/hg/isa/rev/c8bdd2cadb16
# "TERM" marks work on switching to transport libisabelle's Term instead of String
# concerned is transport only Java/Isac <-- Isabelle/Isac,
because --> transports String from input to be parsed by Isabelle.
# notation: Java/Isac "Formula" == Isabelle/Isac "term" 
     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  */

    10 

    11 package isac.bridge.xml

    12 

    13 import isac.bridge.CChanged

    14 import isac.bridge.CEvent

    15 import isac.bridge.CMessage

    16 import isac.util.Formalization

    17 import isac.util.formulae.CalcFormula

    18 import isac.util.formulae.CalcHead

    19 import isac.util.formulae.CalcHeadSimpleID

    20 import isac.util.formulae.ContextMethod

    21 import isac.util.formulae.ContextProblem

    22 import isac.util.formulae.ContextTheory

    23 import isac.util.formulae.Formula

    24 import isac.util.formulae.FormulaPair

    25 import isac.util.formulae.HierarchyKey

    26 import isac.util.formulae.KEStoreKey

    27 import isac.util.formulae.ModelItem

    28 import isac.util.formulae.ModelItemList

    29 import isac.util.formulae.Model

    30 import isac.util.formulae.Position

    31 import isac.util.formulae.Reference

    32 import isac.util.formulae.Specification

    33 import isac.util.tactics.TermTactic

    34 import isac.util.tactics.Rewrite

    35 import isac.util.tactics.RewriteInst

    36 import isac.util.tactics.RewriteSet

    37 import isac.util.tactics.RewriteSetInst

    38 import isac.util.tactics.SimpleTactic

    39 import isac.util.tactics.StringListTactic

    40 import isac.util.tactics.SubProblemTactic

    41 import isac.util.tactics.SubstituteTactic

    42 import isac.util.tactics.Tactic

    43 import isac.util.tactics.Theorem

    44 import isac.util.Variant

    45 

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

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

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

    49 

    50 import java.util.ArrayList

    51 import java.util.Vector

    52 import java.math.BigInteger

    53 import scala.math.BigInt

    54 import scala.collection.JavaConverters._

    55 

    56 /**

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

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

    59  */

    60 object DataTypes {

    61   

    62   /** 

    63    *  auxiliary methods, both directions

    64    **/

    65 

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

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

    68   }  

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

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

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

    72   }

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

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

    75   }

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

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

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

    79   }

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

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

    82       xml_of_ints(ints),

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

    84   }

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

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

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

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

    89   } 

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

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

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

    93       is.foreach { 

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

    95           => v.add(str)

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

    97       }

    98       v

    99     }

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

   101   }

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

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

   104       strs.asScala.toList map xml_of_str)  

   105   }

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

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

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

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

   110       v

   111     }

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

   113   }

   114   

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

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

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

   118   }

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

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

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

   122   }

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

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

   125   }  

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

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

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

   129   }

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

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

   132   }

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

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

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

   136   } 

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

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

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

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

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

   142   }

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

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

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

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

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

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

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

   150   } 

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

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

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

   154       is.foreach { 

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

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

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

   158       }

   159       v

   160     }

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

   162   }

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

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

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

   166       v

   167   }

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

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

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

   171       v

   172   }

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

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

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

   176       v

   177   }

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

   179     case XML.Text(str) => str

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

   181     }

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

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

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

   185   }

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

   187     case

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

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

   190       => str

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

   192   }

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

   194     case

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

   196       => str

   197     case

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

   199       => xml_to_term(term_xml)

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

   201   }

   202   

   203   /** 

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

   205    **/

   206   

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

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

   209     case

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

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

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

   213       => new ModelItem(status, form_isa)

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

   215   }

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

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

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

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

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

   221   }

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

   223     val ivect = new Vector[ModelItem]

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

   225     ivect

   226   }

   227   //for test on console:

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

   229     val ivect = new Vector[Integer]

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

   231     ivect

   232   }

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

   234     case

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

   236       => sList2jVectorModelItem(list_xml map xml_to_ModelItem)

   237     case

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

   239       => sList2jVectorModelItem(list_xml map xml_to_ModelItem)

   240     case

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

   242       => sList2jVectorModelItem(list_xml map xml_to_ModelItem)

   243     case

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

   245       => sList2jVectorModelItem(list_xml map xml_to_ModelItem)

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

   247   }

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

   249     case

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

   251       => new Model(

   252           new ModelItemList(xml_to_VectorModelItem(xml_given)),

   253           new ModelItemList(xml_to_VectorModelItem(xml_where)),

   254           new ModelItemList(xml_to_VectorModelItem(xml_find)),

   255           new ModelItemList(xml_to_VectorModelItem(xml_relate)))

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

   257   }

   258   // 

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

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

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

   262       xml_of_term(item.getFormula.toString)))

   263   }

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

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

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

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

   268   }

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

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

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

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

   273       // xml_where, is never input by user

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

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

   276       ))

   277   }

   278 

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

   280     case

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

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

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

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

   285       => { val thy_key = new CalcHeadSimpleID

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

   287            val pbl_key = new HierarchyKey

   288              pbl_key.setID(xml_to_VectorString(xml_pbl))

   289            val met_key = new HierarchyKey

   290              met_key.setID(xml_to_VectorString(xml_met))

   291            new Specification(thy_key, pbl_key, met_key) 

   292         }

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

   294   }

   295   

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

   297     case

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

   299           xml_pos, xml_head, xml_model,

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

   301           xml_spec))

   302       => { 

   303         new CalcHead(DataTypes.xml_to_Position(xml_pos), 

   304           DataTypes.xml_to_Formula(xml_head), xml_to_Model(xml_model),

   305           pbl_met, xml_to_Specification(xml_spec), status)

   306       }

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

   308   }

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

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

   311       xml_of_Position(chead.getPosition), 

   312       xml_of_HeadForm(chead.getHeadLine),

   313       xml_of_Model(chead.getModel),

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

   315       xml_of_Specification(chead.getSpecification)))

   316   }

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

   318     case

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

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

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

   322       =>  new Formula(form_isa)

   323     case

   324       XML.Elem(("HEAD", Nil), List(

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

   326           XML.Elem(("ISA", Nil), List(XML.Text(head_isa)))))))

   327       =>  new Formula(head_isa)

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

   329   }

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

   331     case

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

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

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

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

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

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

   338   }

   339   /* 

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

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

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

   343    */

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

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

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

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

   348   }

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

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

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

   352   }

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

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

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

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

   357   }

   358   def xml_of_HeadForm(head_isa: Formula): XML.Tree = {

   359     XML.Elem(("HEAD", Nil), List(

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

   361         XML.Elem(("ISA", Nil), List(XML.Text(head_isa.toString)))))))

   362   }

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

   364     case

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

   366       => new CalcFormula(xml_to_Position(pos), xml_to_Formula(form))

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

   368   }

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

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

   371       xml_of_Position(calc_form.getPosition), 

   372       xml_of_Formula(calc_form.getFormula)))

   373   }

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

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

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

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

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

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

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

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

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

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

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

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

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

   387     } else {

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

   389     }

   390   }

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

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

   393     xml_of_pos(is map Integer_to_BigInt, pos.getKind)

   394   }

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

   396     case

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

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

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

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

   401   }

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

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

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

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

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

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

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

   409   }

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

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

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

   413       xml_of_Specification(vat.getSpecification)))

   414   }

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

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

   417   }

   418 

   419   // repair for MathML: use term instead String 

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

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

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

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

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

   425   }

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

   427     case 

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

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

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

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

   432       => new Theorem(id, form)

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

   434   }

   435 

   436   //----- FOR xml_of_Tactic --------------------------------------------*)

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

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

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

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

   441   }

   442   // Substitute see //----- STRINGLISTTACTIC below

   443 

   444   //----- Rewrite* -----------------------------------------------------*)

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

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

   447       xml_of_Theorem(tac.getTheorem)))

   448   }

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

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

   451       //this will be generalised at introduction of MathML

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

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

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

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

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

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

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

   459       xml_of_Theorem(tac.getTheorem)))

   460   }

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

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

   463       XML.Text(tac.getRuleSet)))

   464   }

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

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

   467       //this will be generalised at introduction of MathML

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

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

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

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

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

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

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

   475       XML.Text(tac.getRuleSet)))

   476   }

   477   

   478   //----- FORMTACTIC ---------------------------------------------------*)

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

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

   481       xml_of_term(formtac.getTerm)))

   482   }  

   483   //----- SIMPLETACTIC -------------------------------------------------*)

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

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

   486       xml_of_term(tac.getArgument)))

   487   }  

   488   //----- STRINGLISTTACTIC ---------------------------------------------*)

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

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

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

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

   493   }

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

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

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

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

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

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

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

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

   502   }

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

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

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

   506   }

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

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

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

   510       xml = xml_of_VectorString(strs_tac.getStrings)

   511     else

   512       xml = xml_of_VectorString(strs_tac.getStrings)

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

   514       xml))

   515   }

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

   517   //   was shifted to DataTypesCompanion.java

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

   519     case

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

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

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

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

   524     case

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

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

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

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

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

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

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

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

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

   534 

   535     //----- Rewrite* -----------------------------------------------------*)

   536     case

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

   538         thm))

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

   540     case // faked until introduction of MathML

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

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

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

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

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

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

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

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

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

   550           )))),

   551         thm))

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

   553     case

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

   555         XML.Text(rule_set)))

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   570 

   571     //----- FORMTACTIC ---------------------------------------------------*)

   572     case

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

   574         term))

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

   576     case

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

   578         term))

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

   580     case

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

   582         term))

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

   584     case

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

   586         term))

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

   588     case

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

   590         term))

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

   592 

   593     //----- SIMPLETACTIC -------------------------------------------------*)

   594     case

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

   596         XML.Text(_)))

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

   598     case

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

   600         XML.Text(str)))

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

   602 

   603     //----- STRINGLISTTACTIC ---------------------------------------------*)

   604     case

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

   606         strs))

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

   608     case

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

   610         strs))

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

   612     case

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

   614         strs))

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

   616     case

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

   618         strs))

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

   620     case

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

   622         strs))

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

   624     case

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

   626         strs))

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

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

   629   }

   630 

   631   //------- for xml_of_contthy

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

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

   634     case

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

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

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

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

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

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

   641   }

   642   

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

   644     case

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

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

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

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

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

   650   }

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

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

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

   654     case

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   670           null, null,

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

   672           reword,

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

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

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

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

   677           xml_to_Reference(rlskey_xml))

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

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

   680     case

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   700           reword,

   701           sListToVectorFormulaPair(asmevs_xml map xml_to_asm_val),

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

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

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

   705           xml_to_Reference(rlskey_xml))

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

   707     case

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

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

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

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

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

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

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

   715           null,

   716           null,

   717           null, null,

   718           null, null,

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

   720           null)

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

   722     case

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

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

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

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

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

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

   729         XML.Elem(("ASSUMPTIONS", Nil), List(asms_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)), null,

   733           null,

   734           null,

   735           null, null,

   736           null, null,

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

   738           null)

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

   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       => new ContextTheory(new KEStoreKey(guh), null, null,

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

   746           null,

   747           null,

   748           null, null,

   749           null, null,

   750           null, null,

   751           null)

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

   753     case

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

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

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

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

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

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

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

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

   762           null,

   763           null,

   764           null, null,

   765           null, null,

   766           null, null,

   767           null)

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

   769   }

   770 

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

   772     case

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

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

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

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

   777         model_xml))

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

   779           status, new Formula(xml_to_term(head_xml)), xml_to_Model(model_xml))

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

   781   }

   782 

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

   784     case

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

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

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

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

   789         model_xml))

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

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

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

   793   }

   794 

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

   796     case

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

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

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

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

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

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

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

   804       => new CChanged(

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

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

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

   808     case

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

   810       => new CMessage(msg)

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

   812   }

   813   

   814 }
wneuper/isac