/* 

 * @author Walther Neuper

 * Copyright (c) due to license terms

 * Created on Jul 14, 2015

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

 * 

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

 * off and on again helped.

 */

package isac.bridge.xml

import isac.bridge.CChanged

import isac.bridge.CEvent

import isac.bridge.CMessage

import isac.util.Formalization

import isac.util.formulae.CalcFormula

import isac.util.formulae.CalcHead

import isac.util.formulae.CalcHeadSimpleID

import isac.util.formulae.ContextMethod

import isac.util.formulae.ContextProblem

import isac.util.formulae.ContextTheory

import isac.util.formulae.Formula

import isac.util.formulae.FormulaPair

import isac.util.formulae.HierarchyKey

import isac.util.formulae.KEStoreKey

import isac.util.formulae.ModelItem

import isac.util.formulae.ModelItemList

import isac.util.formulae.Model

import isac.util.formulae.Position

import isac.util.formulae.Reference

import isac.util.formulae.Specification

import isac.util.tactics.TermTactic

import isac.util.tactics.Rewrite

import isac.util.tactics.RewriteInst

import isac.util.tactics.RewriteSet

import isac.util.tactics.RewriteSetInst

import isac.util.tactics.SimpleTactic

import isac.util.tactics.StringListTactic

import isac.util.tactics.SubProblemTactic

import isac.util.tactics.SubstituteTactic

import isac.util.tactics.Tactic

import isac.util.tactics.Theorem

import isabelle.XML

import isabelle.Markup

import java.util.ArrayList

import java.util.Vector

import java.math.BigInteger

import scala.math.BigInt

import scala.collection.JavaConverters._

/**

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

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

 */

object DataTypes {

  /** 

   *  auxiliary methods, both directions

   **/

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

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

  }  

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

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

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

  }

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

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

  }

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

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

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

  }

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

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

      xml_of_ints(ints),

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

  }

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

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

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

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

  } 

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

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

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

      is.foreach { 

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

          => v.add(str)

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

      }

      v

    }

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

  }

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

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

      strs.asScala.toList map xml_of_str)  

  }

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

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

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

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

      v

    }

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

  }

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

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

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

  }

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

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

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

  }

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

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

  }  

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

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

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

  }

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

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

  }

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

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

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

  } 

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

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

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

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

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

  }

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

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

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

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

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

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

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

  } 

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

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

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

      is.foreach { 

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

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

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

      }

      v

    }

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

  }

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

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

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

      v

  }

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

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

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

      v

  }

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

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

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

      v

  }

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

    case XML.Text(str) => str

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

    }

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

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

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

  }

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

    case

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

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

      => str

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

  }

  /** 

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

   **/

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

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

    case

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

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

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

      => new ModelItem(status, form_isa)

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

  }

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

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

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

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

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

  }

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

    val ivect = new Vector[ModelItem]

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

    ivect

  }

  //for test on console:

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

    val ivect = new Vector[Integer]

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

    ivect

  }

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

    case

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

      => sList2jVectorModelItem(list_xml map xml_to_ModelItem)

    case

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

      => sList2jVectorModelItem(list_xml map xml_to_ModelItem)

    case

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

      => sList2jVectorModelItem(list_xml map xml_to_ModelItem)

    case

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

      => sList2jVectorModelItem(list_xml map xml_to_ModelItem)

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

  }

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

    case

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

      => new Model(

          new ModelItemList(xml_to_VectorModelItem(xml_given)),

          new ModelItemList(xml_to_VectorModelItem(xml_where)),

          new ModelItemList(xml_to_VectorModelItem(xml_find)),

          new ModelItemList(xml_to_VectorModelItem(xml_relate)))

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

  }

  // 

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

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

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

      xml_of_term(item.getFormula.toString)))

  }

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

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

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

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

  }

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

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

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

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

      // xml_where, is never input by user

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

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

      ))

  }

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

    case

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

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

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

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

      => { val thy_key = new CalcHeadSimpleID

             thy_key.setID(DataTypes.xml_to_String(xml_thy))

           val pbl_key = new HierarchyKey

             pbl_key.setID(xml_to_VectorString(xml_pbl))

           val met_key = new HierarchyKey

             met_key.setID(xml_to_VectorString(xml_met))

           new Specification(thy_key, pbl_key, met_key) 

        }

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

  }

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

    case

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

          xml_pos, xml_head, xml_model,

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

          xml_spec))

      => { 

        new CalcHead(DataTypes.xml_to_Position(xml_pos), 

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

          pbl_met, xml_to_Specification(xml_spec), status)

      }

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

  }

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

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

      xml_of_Position(chead.getPosition), 

      xml_of_HeadForm(chead.getHeadLine),

      xml_of_Model(chead.getModel),

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

      xml_of_Specification(chead.getSpecification)))

  }

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

    case

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

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

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

      =>  new Formula(form_isa)

    case

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

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

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

      =>  new Formula(head_isa)

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

  }

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

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

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

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

  }

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

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

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

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

  }

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

    case

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

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

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

  }

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

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

      xml_of_Position(calc_form.getPosition), 

      xml_of_Formula(calc_form.getFormula)))

  }

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

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

  }

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

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

    xml_of_pos(is map Integer_to_BigInt, pos.getKind)

  }

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

    case

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

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

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

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

  }

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

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

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

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

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

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

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

  }

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

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

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

      xml_of_Specification(vat.getSpecification)))

  }

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

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

  }

  // repair for MathML: use term instead String 

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

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

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

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

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

  }

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

    case 

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

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

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

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

      => new Theorem(id, form)

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

  }

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

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

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

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

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

  }

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

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

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

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

      xml_of_Theorem(tac.getTheorem)))

  }

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

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

      //this will be generalised at introduction of MathML

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

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

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

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

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

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

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

      xml_of_Theorem(tac.getTheorem)))

  }

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

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

      XML.Text(tac.getRuleSet)))

  }

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

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

      //this will be generalised at introduction of MathML

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

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

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

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

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

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

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

      XML.Text(tac.getRuleSet)))

  }

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

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

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

      xml_of_term(formtac.getTerm)))

  }  

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

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

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

      xml_of_term(tac.getArgument)))

  }  

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

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

    val pair = equality.split("=")

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

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

  }

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

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

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

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

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

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

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

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

  }

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

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

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

  }

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

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

    if (strs_tac.getName == "Substitute")

      xml = xml_of_VectorString(strs_tac.getStrings)

    else

      xml = xml_of_VectorString(strs_tac.getStrings)

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

      xml))

  }

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

  //   was shifted to DataTypesCompanion.java

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

    case

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

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

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

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

    case

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

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

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

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

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

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

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

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

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

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

    case

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

        thm))

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

    case // faked until introduction of MathML

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

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

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

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

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

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

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

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

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

          )))),

        thm))

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

    case

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

        XML.Text(rule_set)))

      => new RewriteSet("Rewrite_Set", rule_set)

    case // faked Term by String until introduction of MathML

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

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

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

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

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

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

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

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

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

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

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

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

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

    case

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

        term))

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

    case

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

        term))

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

    case

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

        term))

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

    case

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

        term))

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

    case

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

        term))

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

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

    case

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

        XML.Text(_)))

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

    case

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

        XML.Text(str)))

      => new SimpleTactic("Specify_Theory", str)

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

    case

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

        strs))

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

    case

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

        strs))

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

    case

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

        strs))

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

    case

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

        strs))

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

    case

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

        strs))

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

    case

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

        strs))

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

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

  }

  //------- for xml_of_contthy

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

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

    case

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

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

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

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

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

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

  }

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

    case

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

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

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

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

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

  }

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

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

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

    case

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

        XML.Elem(Markup("GUH", Nil), List(XML.Text(thm))),

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

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

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

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

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

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

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

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

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

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

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

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

      => new ContextTheory(/*WN150820 GUH unused?!?*/

          null, null,

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

          reword,

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

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

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

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

          xml_to_Reference(rlskey_xml))

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

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

    case

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

        XML.Elem(Markup("GUH", Nil), List(XML.Text(thm))),

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

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

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

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

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

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

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

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

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

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

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

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

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

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

      => new ContextTheory(/*WN150820 GUH unused?!?*/

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

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

          reword,

          sListToVectorFormulaPair(asmevs_xml map xml_to_asm_val),

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

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

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

          xml_to_Reference(rlskey_xml))

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

    case

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

        XML.Elem(Markup("GUH", Nil), List(XML.Text(thm))),

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

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

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

      => new ContextTheory(/*WN150820 GUH unused?!?*/

          null, null,

          new Formula(xml_to_term(applto_xml)), null,

          null,

          null,

          null, null,

          null, null,

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

          null)

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

    case

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

        XML.Elem(Markup("GUH", Nil), List(XML.Text(thm))),

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

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

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

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

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

      => new ContextTheory(/*WN150820 GUH unused?!?*/

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

          new Formula(xml_to_term(applto_xml)), null,

          null,

          null,

          null, null,

          null, null,

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

          null)

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

    case

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

        XML.Elem(Markup("GUH", Nil), List(XML.Text(thm))),

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

      => new ContextTheory(/*WN150820 GUH unused?!?*/

          null, null,

          new Formula(xml_to_term(applto_xml)), null,

          null,

          null,

          null, null,

          null, null,

          null, null,

          null)

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

    case

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

        XML.Elem(Markup("GUH", Nil), List(XML.Text(thm))),

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

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

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

      => new ContextTheory(/*WN150820 GUH unused?!?*/

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

          new Formula(xml_to_term(applto_xml)), null,

          null,

          null,

          null, null,

          null, null,

          null, null,

          null)

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

  }

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

    case

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

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

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

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

        model_xml))

      => new ContextProblem(/*WN150820 GUH unused?!?*/

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

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

  }

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

    case

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

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

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

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

        model_xml))

      => new ContextMethod(/*WN150820 GUH unused?!?*/

          status, new Formula(xml_to_term(prog_xml)), xml_to_Model(model_xml))

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

  }

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

    case

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

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

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

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

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

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

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

      => new CChanged(

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

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

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

    case

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

      => new CMessage(msg)

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

  }

}