/* 

 * @author Walther Neuper

 * Copyright (c) due to license terms

 * Created on Jul 14, 2015

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

 */

package isac.bridge.xml

import isac.bridge.CChanged

import isac.bridge.CEvent

import isac.bridge.CMessage

import isac.util.formulae.Assumptions

import isac.util.formulae.CalcFormula

import isac.util.formulae.CalcHead

import isac.util.formulae.CalcHeadSimpleID

import isac.util.formulae.Context

import isac.util.formulae.ContextTheory

import isac.util.formulae.Formula

import isac.util.formulae.HierarchyKey

import isac.util.formulae.KEStoreKey

import isac.util.formulae.Model

import isac.util.formulae.ModelItem

import isac.util.formulae.ModelItemList

import isac.util.formulae.Position

import isac.util.formulae.Specification

import isac.util.Message

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

import java.util.ArrayList

import java.util.Vector

import java.math.BigInteger

import scala.math.BigInt

import scala.collection.JavaConverters._

/**

 * Convert results of JSystem.invoke(Operations.* to Java-objects.

 * Conversions use Scala's pattern matching, which is not available in Java.

 * 

 * The sequence in the kernel's signature below is maintained.

 */

object IsaToJava {

  //is the tree (expected to contain data going to Dialog) a message ?

  //  CALCMESSAGE is excluded, because this goes to Dialog as CCEvent

  def is_message(t: XML.Tree): java.lang.Boolean = t match {

    case

      XML.Elem(("MESSAGE", Nil), List(

        XML.Elem(("CALCID", Nil), List(XML.Text (_))),

        XML.Elem(("STRING", Nil), List(XML.Text (_))))) => true

    case

      XML.Elem(("SYSERROR", Nil), List(

        XML.Elem(("CALCID", Nil), List(XML.Text (_))),

        XML.Elem(("ERROR", Nil), List(XML.Text (_))))) => true

    case

      XML.Elem((_/*"SETNEXTTACTIC"*/, Nil), List(

        XML.Elem(("CALCID", Nil), List(XML.Text (_))),

        XML.Elem(("MESSAGE", Nil), List(XML.Text (_))))) => true

    case _ => false //expected data going to Dialog

  }

  def is_syserror(t: XML.Tree): java.lang.Boolean = t match {

    case

      XML.Elem(("SYSERROR", Nil), List(

        XML.Elem(("CALCID", Nil), List(XML.Text (_))),

        XML.Elem(("ERROR", Nil), List(XML.Text (_))))) => true

    case _ => false

  }

/* from isabisac/src/Tools/Frontend/interface.sml + XML generation

signature MATH_ENGINE =

  sig

    val appendFormula : calcID -> cterm' -> XML.tree

          appendformulaOK2xml

          appendformulaERROR2xml

          sysERROR2xml

    val autoCalculate : calcID -> auto -> XML.tree

          autocalculateOK2xml

          autocalculateERROR2xml

          sysERROR2xml

    val applyTactic : calcID -> pos' -> tac -> XML.tree

          autocalculateOK2xml

          autocalculateERROR2xml

    val CalcTree : fmz list -> XML.tree

          calctreeOK2xml

          sysERROR2xml

    val checkContext : calcID -> pos' -> guh -> XML.tree

          message2xml

          contextthyOK2xml

          sysERROR2xml

    val DEconstrCalcTree : calcID -> XML.tree

          deconstructcalctreeOK2xml

    val fetchApplicableTactics : calcID -> int -> pos' -> XML.tree

          applicabletacticsOK

          sysERROR2xml

    val fetchProposedTactic : calcID -> XML.tree

          fetchproposedtacticOK2xml

          fetchproposedtacticERROR2xml

          sysERROR2xml

    val findFillpatterns : calcID -> errpatID -> XML.tree

          findFillpatterns2xml

    val getAccumulatedAsms : calcID -> pos' -> XML.tree

          getasmsOK2xml

          sysERROR2xml

    val getActiveFormula : calcID -> XML.tree

          iteratorOK2xml

    val getAssumptions : calcID -> pos' -> XML.tree

          getasmsOK2xml

          sysERROR2xml

    val getFormulaeFromTo : calcID -> pos' -> pos' -> int -> bool -> XML.tree

          getintervalOK

          sysERROR2xml

    val getTactic : calcID -> pos' -> XML.tree

          gettacticOK2xml

          gettacticERROR2xml

          sysERROR2xml

    val initContext : calcID -> ketype -> pos' -> XML.tree

          message2xml

          contextthyOK2xml

          sysERROR2xml

    val inputFillFormula: calcID -> string -> XML.tree

          autocalculateOK2xml

          autocalculateERROR2xml

          message2xml

    val interSteps : calcID -> pos' -> XML.tree

          interStepsOK

          interStepsERROR

          sysERROR2xml

    val Iterator : calcID -> XML.tree

          adduserOK2xml

          sysERROR2xml

    val IteratorTEST : calcID -> iterID

    val modelProblem : calcID -> XML.tree

          modifycalcheadOK2xml

          sysERROR2xml

    val modifyCalcHead : calcID -> icalhd -> XML.tree

          modifycalcheadOK2xml

          sysERROR2xml

    val moveActiveCalcHead : calcID -> XML.tree

          iteratorOK2xml

          sysERROR2xml

    val moveActiveDown : calcID -> XML.tree

          iteratorOK2xml

          iteratorERROR2xml

          sysERROR2xml

    val moveActiveFormula : calcID -> pos' -> XML.tree

          iteratorOK2xml

          sysERROR2xml

    val moveActiveLevelDown : calcID -> XML.tree

          iteratorOK2xml

          iteratorERROR2xml

          sysERROR2xml

    val moveActiveLevelUp : calcID -> XML.tree

          iteratorOK2xml

          iteratorERROR2xml

          sysERROR2xml

    val moveActiveRoot : calcID -> XML.tree

          iteratorOK2xml

          sysERROR2xml

    val moveActiveRootTEST : calcID -> XML.tree

    val moveActiveUp : calcID -> XML.tree

          iteratorOK2xml

          iteratorERROR2xml

          sysERROR2xml

    val moveCalcHead : calcID -> pos' -> XML.tree

          iteratorOK2xml

          iteratorERROR2xml

          sysERROR2xml

    val moveDown : calcID -> pos' -> XML.tree

          iteratorOK2xml

          iteratorERROR2xml

          sysERROR2xml

    val moveLevelDown : calcID -> pos' -> XML.tree

          iteratorOK2xml

          iteratorERROR2xml

          sysERROR2xml

    val moveLevelUp : calcID -> pos' -> XML.tree

          iteratorOK2xml

          iteratorERROR2xml

          sysERROR2xml

    val moveRoot : calcID -> XML.tree

          iteratorOK2xml

          sysERROR2xml

    val moveUp : calcID -> pos' -> XML.tree

          iteratorOK2xml

          iteratorERROR2xml

          sysERROR2xml

    val refFormula : calcID -> pos' -> XML.tree

          refformulaOK2xml

          sysERROR2xml

    val refineProblem : calcID -> pos' -> guh -> XML.tree

          xml_of_matchpbl

          sysERROR2xml

    val replaceFormula : calcID -> cterm' -> XML.tree

          replaceformulaOK2xml

          replaceformulaERROR2xml

          sysERROR2xml

    val requestFillformula : calcID -> errpatID * fillpatID -> XML.tree

          autocalculateOK2xml

          autocalculateERROR2xml

    val resetCalcHead : calcID -> XML.tree

          modifycalcheadOK2xml

          sysERROR2xml

    val setContext : calcID -> pos' -> guh -> XML.tree

          message2xml

          autocalculateOK2xml

          sysERROR2xml

    val setMethod : calcID -> metID -> XML.tree

          modifycalcheadOK2xml

          sysERROR2xml

    val setNextTactic : calcID -> tac -> XML.tree

          setnexttactic2xml

          sysERROR2xml

    val setProblem : calcID -> pblID -> XML.tree

          modifycalcheadOK2xml

          sysERROR2xml

    val setTheory : calcID -> thyID -> XML.tree

          modifycalcheadOK2xml

          sysERROR2xml

  end

*/

  //fun appendFormula : calcID -> cterm' -> XML.tree

  def append_form_out(t: XML.Tree): IntCEvent = t match {

    case

      XML.Elem(("APPENDFORMULA", Nil), List(

        XML.Elem(("CALCID", Nil), List(XML.Text (calcid))),

        cevent_xml))

      => new IntCEvent(new java.lang.Integer(calcid), 

           DataTypes.xml_to_CEvent(cevent_xml))

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

  }

  //fun autoCalculate : calcID -> auto -> XML.tree

  def auto_calc_out(t: XML.Tree): IntCEvent = t match {

    case

      XML.Elem(("AUTOCALC", Nil), List(

        XML.Elem(("CALCID", Nil), List(XML.Text (calcid))),

        cevent_xml))

      => new IntCEvent(new java.lang.Integer(calcid), 

           DataTypes.xml_to_CEvent(cevent_xml))

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

  }

  //fun applyTactic : calcID -> pos' -> tac -> XML.tree  ...NOT IMPL. IN isac-java WN150813

  //fun CalcTree : fmz list -> XML.tree

  def calc_tree_out(t: XML.Tree): java.lang.Integer = t match {

    case

       XML.Elem(("CALCTREE", Nil), List(

         XML.Elem(("CALCID", Nil), List(XML.Text(i)))))

      => new Integer(i)

    case //TODO catch in Java

       XML.Elem(("SYSERROR", Nil), List(

         XML.Elem(("CALCID", Nil), List(XML.Text(i))),

         XML.Elem(("ERROR", Nil), List(XML.Text(msg)))))

      => throw new IllegalArgumentException("calc_tree_out SYSERROR wrong arg: " + t)

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

  }

  //fun checkContext : calcID -> pos' -> guh -> XML.tree

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

    case

      XML.Elem(("CONTEXTTHY", Nil), List(

        XML.Elem(("CALCID", Nil), List(XML.Text(calcid))),

        contthy_xml))

      => DataTypes.xml_to_ContextTheory(contthy_xml)

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

  }

  //fun DEconstrCalcTree : calcID -> XML.tree

  def del_calc_out(t: XML.Tree): java.lang.Integer = t match {

    case

      XML.Elem(("DELCALC", Nil), List(

        XML.Elem(("CALCID", Nil), List(XML.Text(calcid)))))

      => new java.lang.Integer(calcid)

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

  }

  //fun fetchApplicableTactics : calcID -> int -> pos' -> XML.tree

  def fetch_applicable_tacs_out(t: XML.Tree): IntTactics = t match {

    case

      XML.Elem(("APPLICABLETACTICS", Nil), List(

        XML.Elem(("CALCID", Nil), List(XML.Text(calcid))),

        tacs_xml))

      =>  new IntTactics(new java.lang.Integer(calcid), 

            DataTypes.xml_to_VectorTactic(tacs_xml))

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

  }

  //fun fetchProposedTactic : calcID -> XML.tree

  def fetch_proposed_tac_out(t: XML.Tree): IntTacticErrPats = t match {

    case

      XML.Elem(("NEXTTAC", Nil), List(

        XML.Elem(("CALCID", Nil), List(XML.Text(calcid))),

        XML.Elem(("TACTICERRORPATTERNS", Nil), List(errpat_ids)),

        tac))

      =>  new IntTacticErrPats(new java.lang.Integer(calcid), 

            DataTypes.xml_to_VectorString(errpat_ids), DataTypes.xml_to_Tactic(tac))

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

  }

  //fun findFillpatterns : calcID -> errpatID -> XML.tree

  //... only implemented in Math_Engine

  //fun getAccumulatedAsms : calcID -> pos' -> XML.tree

  def get_accumulated_asms_out(t: XML.Tree): IntAssumptions = t match {

    case

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

        XML.Elem(("CALCID", Nil), List(XML.Text(calcid))),

        XML.Elem(("ASMLIST", Nil), asms)))

       => new IntAssumptions(new java.lang.Integer(calcid), 

            new Assumptions(DataTypes.sListToVectorFormula(asms map DataTypes.xml_to_Formula_NEW)))

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

  }

  //fun getActiveFormula : calcID -> XML.tree

  def get_active_form_out(t: XML.Tree): IntPosition = t match {

    case

      XML.Elem(("CALCITERATOR", Nil), List(

        XML.Elem(("CALCID", Nil), List(XML.Text(calcid))),

        pos_xml))

       => new IntPosition(new java.lang.Integer(calcid), 

            DataTypes.xml_to_Position(pos_xml))

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

  }

  //fun getAssumptions : calcID -> pos' -> XML.tree

  def get_asms_out(t: XML.Tree): IntAssumptions = t match {

    case

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

        XML.Elem(("CALCID", Nil), List(XML.Text(calcid))),

        XML.Elem(("ASMLIST", Nil), asms)))

       => new IntAssumptions(new java.lang.Integer(calcid), 

            new Assumptions(DataTypes.sListToVectorFormula(asms map DataTypes.xml_to_Formula_NEW)))

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

  }

  //fun getFormulaeFromTo : calcID -> pos' -> pos' -> int -> bool -> XML.tree

  def get_formulae_out(t: XML.Tree): IntFormulas = t match {

    case

      XML.Elem(("GETELEMENTSFROMTO", Nil), List(

        XML.Elem(("CALCID", Nil), List(XML.Text(calcid))),

        XML.Elem(("FORMHEADS", Nil), forms)))

       => new IntFormulas(new java.lang.Integer(calcid), 

            DataTypes.sListToVectorCalcFormula(forms map DataTypes.xml_to_CalcFormula))

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

  }

  //fun getTactic : calcID -> pos' -> XML.tree

  def get_tac_out(t: XML.Tree): IntTactic = t match {

    case

      XML.Elem(("GETTACTIC", Nil), List(

        XML.Elem(("CALCID", Nil), List(XML.Text(calcid))),

        tac))

      => new IntTactic(new java.lang.Integer(calcid), 

           DataTypes.xml_to_Tactic(tac))

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

  }

  //fun initContext : calcID -> ketype -> pos' -> XML.tree

  def init_ctxt_out(t: XML.Tree): Context = t match {

    case

      XML.Elem(("CONTEXTTHY", Nil), List(

        XML.Elem(("CALCID", Nil), List(XML.Text(calcid))),

        contthy_xml))

      => DataTypes.xml_to_ContextTheory(contthy_xml)

    case

      XML.Elem(("CONTEXTPBL", Nil), List(

        XML.Elem(("CALCID", Nil), List(XML.Text(calcid))),

        contpbl_xml))

      => DataTypes.xml_to_ContextProblem(contpbl_xml)

    case

      XML.Elem(("CONTEXTMET", Nil), List(

        XML.Elem(("CALCID", Nil), List(XML.Text(calcid))),

        contmet_xml))

      => DataTypes.xml_to_ContextMethod(contmet_xml)

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

  }

  //fun inputFillFormula: calcID -> string -> XML.tree

  //... ONLY IMPL. IN Math_Engine

  //fun interSteps : calcID -> pos' -> XML.tree

  def inter_steps_out(t: XML.Tree): IntCEvent = t match {

    case

      XML.Elem(("INTERSTEPS", Nil), List(

        XML.Elem(("CALCID", Nil), List(XML.Text(calcid))),

        cevent_xml))

      => new IntCEvent(new java.lang.Integer(calcid), 

           DataTypes.xml_to_CEvent(cevent_xml))

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

  }

  //fun Iterator : calcID -> XML.tree

  def iterator_out(t: XML.Tree): IntIntCompound = t match {

    case

      XML.Elem(("ADDUSER", Nil), List(

        XML.Elem(("CALCID", Nil), List(XML.Text(calcid))),

        XML.Elem(("USERID", Nil), List(XML.Text(userid)))))

      => new IntIntCompound(new java.lang.Integer(calcid), new java.lang.Integer(userid))

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

  }

  //fun IteratorTEST : calcID -> iterID              

  //... only relevant for Isabelle/Isac

  //fun modelProblem : calcID -> XML.tree

  def modify_calchead_out(t: XML.Tree): IntCalcHead = t match {

    case

      XML.Elem(("MODIFYCALCHEAD", Nil), List(

        XML.Elem(("CALCID", Nil), List(XML.Text(calcid))),

        calchead_xml))

      => new IntCalcHead(new java.lang.Integer(calcid), 

           DataTypes.xml_to_CalcHead(calchead_xml))

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

  }

  //fun modifyCalcHead : calcID -> icalhd -> XML.tree

  def model_pbl_out(t: XML.Tree): IntCalcHead = modify_calchead_out(t)  

  //fun moveActiveCalcHead : calcID -> XML.tree

  def move_active_calchead_out(t: XML.Tree): IntPosition = get_active_form_out(t)    

  //fun moveActiveDown : calcID -> XML.tree

  def move_active_down_out(t: XML.Tree): IntPosition = get_active_form_out(t)  

  //fun moveActiveFormula : calcID -> pos' -> XML.tree

  def move_active_form_out(t: XML.Tree): IntPosition = get_active_form_out(t)  

  //fun moveActiveLevelDown : calcID -> XML.tree

  def move_active_levdown_out(t: XML.Tree): IntPosition = get_active_form_out(t)  

  //fun moveActiveLevelUp : calcID -> XML.tree

  def move_active_levup_out(t: XML.Tree): IntPosition = get_active_form_out(t)  

  //fun moveActiveRoot : calcID -> XML.tree

  def move_active_root_out(t: XML.Tree): IntPosition = get_active_form_out(t)

  //fun moveActiveRootTEST : calcID -> XML.tree

  //... only relevant for Isabelle/Isac

  //fun moveActiveUp : calcID -> XML.tree

  def move_active_up_out(t: XML.Tree): IntPosition = get_active_form_out(t)  

  //fun moveCalcHead : calcID -> pos' -> XML.tree

  def move_calchead_out(t: XML.Tree): IntPosition = get_active_form_out(t)  

  //fun moveDown : calcID -> pos' -> XML.tree

  def move_down_out(t: XML.Tree): IntPosition = get_active_form_out(t)  

  //fun moveLevelDown : calcID -> pos' -> XML.tree

  def move_levdn_out(t: XML.Tree): IntPosition = get_active_form_out(t)  

  //fun moveLevelUp : calcID -> pos' -> XML.tree

  def move_levup_out(t: XML.Tree): IntPosition = get_active_form_out(t)  

  //fun moveRoot : calcID -> XML.tree

  def move_root_out(t: XML.Tree): IntPosition = get_active_form_out(t)

  //fun moveUp : calcID -> pos' -> XML.tree

  def move_up_out(t: XML.Tree): IntPosition = get_active_form_out(t)

  //fun refFormula : calcID -> pos' -> XML.tree

  def ref_formula_out(t: XML.Tree): IntFormHead = t match {

    case

      XML.Elem(("REFFORMULA", Nil), List(

        XML.Elem(("CALCID", Nil), List(

          XML.Text (calcid))), 

           XML.Elem(("CALCFORMULA", Nil), cform_etc)))

      => new IntFormHead(new java.lang.Integer(calcid), 

             DataTypes.xml_to_CalcFormula(XML.Elem(("CALCFORMULA", Nil), cform_etc)))

    case

      XML.Elem(("REFFORMULA", Nil), List(

        XML.Elem(("CALCID", Nil), List(XML.Text (calcid))), 

        XML.Elem(("CALCHEAD", status), chead_etc)))

      => new IntFormHead(new java.lang.Integer(calcid), 

           DataTypes.xml_to_CalcHead(XML.Elem(("CALCHEAD", status), chead_etc)))

    case // singularity in error handling

      XML.Elem(("REFFORMULA", Nil), List(

        XML.Elem(("CALCID", Nil), List(XML.Text (calcid))), 

        XML.Elem(("ERROR", Nil), List(XML.Text(msg)))))

      => new IntFormHead(new java.lang.Integer(calcid), new Message(msg))

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

  }

  //fun refineProblem : calcID -> pos' -> guh -> XML.tree

    /* WN150824: isabisac ... isac-java seems to incompatible:

     * isabisac/../interface-xml.xml_of_matchpbl is incompatible with

     * isac.util.parser.XMLParserDigest //=== Rules for parsing Contexts.

     * 

     * Unfortunately there is no use-case and no test for refineProblem,

     * so the Context only gets the KEStoreKey ("GUH"), 

     * not the HierarchyKey.

     */

  def refine_pbl_out(t: XML.Tree): IntContext = t match {

    case

      XML.Elem(("CONTEXTPBL", Nil), List(

        // WN150530: calcid will be required for asynchronous communication *)

        // XML.Elem(("CALCID", Nil), List(XML.Text(calcid))),

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

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

        form_xml,

        model_xml))

      => new IntContext(/*new java.lang.Integer(calcid),*/ 

           new Context(null/*see WN150824*/, new KEStoreKey(guh)))

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

  }

  //fun replaceFormula : calcID -> cterm' -> XML.tree

  def replace_form_out(t: XML.Tree): IntCEvent = t match {

    case

      XML.Elem(("REPLACEFORMULA", Nil), List(

        XML.Elem(("CALCID", Nil), List(XML.Text (calcid))),

        cevent_xml))

      => new IntCEvent(new java.lang.Integer(calcid), 

           DataTypes.xml_to_CEvent(cevent_xml))

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

  }

  //fun requestFillformula : calcID -> errpatID * fillpatID -> XML.tree

  //...ONLY IMPLEMENTED IN Math_Engine

  //fun resetCalcHead : calcID -> XML.tree

  def reset_calchead_out(t: XML.Tree): IntCalcHead = modify_calchead_out(t)

  //fun setContext : calcID -> pos' -> guh -> XML.tree

  def set_ctxt_out(t: XML.Tree): IntCEvent = auto_calc_out(t)

  //fun setMethod : calcID -> metID -> XML.tree

  def set_met_out(t: XML.Tree): IntCalcHead = modify_calchead_out(t)

  //fun setNextTactic : calcID -> tac -> XML.tree

  def set_next_tac_out(t: XML.Tree): Message = t match {

    case

      XML.Elem(("SETNEXTTACTIC", Nil), List(

        XML.Elem(("CALCID", Nil), List(XML.Text (_))),

        XML.Elem(("MESSAGE", Nil), List(XML.Text (msg))))) 

      => new Message(msg) 

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

  }

  //fun setProblem : calcID -> pblID -> XML.tree

  def set_pbl_out(t: XML.Tree): IntCalcHead = modify_calchead_out(t)

  //fun setTheory : calcID -> thyID -> XML.tree

  def set_thy_out(t: XML.Tree): IntCalcHead = modify_calchead_out(t)

}