/* 

 * @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.util.formulae.CalcFormula

import isac.util.formulae.CalcHead

import isac.util.formulae.Formula

import isac.util.formulae.Position

import isac.util.formulae.Specification

import isac.util.tactics.Tactic

import isac.util.Variant

import isac.util.Formalization

import isac.wsdialog.IContextProvider.ContextType;

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._

import scala.collection.JavaConversions._

/**

 * Convert arguments of JSystem.invoke(Operations.* to XML;

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

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

 */

object JavaToIsa {

/* from isabisac/src/Tools/Frontend/interface.sml

signature MATH_ENGINE =

  sig

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

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

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

    val CalcTree : fmz list -> XML.tree

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

    val DEconstrCalcTree : calcID -> XML.tree

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

    val fetchProposedTactic : calcID -> XML.tree

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

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

    val getActiveFormula : calcID -> XML.tree

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

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

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

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

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

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

    val Iterator : calcID -> XML.tree

    val IteratorTEST : calcID -> iterID

    val modelProblem : calcID -> XML.tree

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

    val moveActiveCalcHead : calcID -> XML.tree

    val moveActiveDown : calcID -> XML.tree

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

    val moveActiveLevelDown : calcID -> XML.tree

    val moveActiveLevelUp : calcID -> XML.tree

    val moveActiveRoot : calcID -> XML.tree

    val moveActiveRootTEST : calcID -> XML.tree

    val moveActiveUp : calcID -> XML.tree

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

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

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

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

    val moveRoot : calcID -> XML.tree

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

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

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

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

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

    val resetCalcHead : calcID -> XML.tree

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

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

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

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

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

  end

*/

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

  def append_form(calcid: scala.math.BigInt, form: Formula): XML.Tree =

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

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

      DataTypes.xml_of_Formula_NEW(form)))

  }

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

  def auto_calculate(calcid: scala.math.BigInt, scope: String, steps: scala.math.BigInt): XML.Tree =

  { //ATTENTION the "if" below is according to "fun xml_to_auto" in datatypes.sml, 

    //but NOT according to "if/else if" in BridgeRMI#autoCalculate for "isabelle tty".

    if (steps == 0)

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

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

        XML.Elem(("AUTO", Nil), List(XML.Text(scope)))))

    else

      //dataypes.sml:

      //xml_to_auto (XML.Elem (("AUTO", []), [XML.Text "Step", XML.Text i])) = Step (int_of_str i |>the)

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

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

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

          XML.Elem(("STEP", Nil), List(XML.Text(steps.toString()))) )) ))

  }

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

  //fun CalcTree : fmz list -> XML.tree                  ...uses only DataTypes..fmz..

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

  def   check_ctxt(calcid: scala.math.BigInt, from: Position, kestore_key: String): XML.Tree =

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

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

      DataTypes.xml_of_Position(from),

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

  } 

  //fun DEconstrCalcTree : calcID -> XML.tree    ...no further ado: scala.math.BigInt

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

  def   fetch_applicable_tacs(calcid: scala.math.BigInt, scope: scala.math.BigInt, pos: Position): XML.Tree =

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

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

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

      DataTypes.xml_of_Position(pos)))

  } 

  //fun fetchProposedTactic : calcID -> XML.tree

  def   fetch_proposed_tac(calcid: scala.math.BigInt): XML.Tree =

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

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

  } 

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

  //... only implemented in Math_Engine

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

  def   get_accumulated_asms(calcid: scala.math.BigInt, pos: Position): XML.Tree =

  { XML.Elem(("GETASSUMPTIONS", Nil), List(

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

      DataTypes.xml_of_Position(pos)))

  } 

  //fun getActiveFormula : calcID -> XML.tree

  def   get_active_form(calcid: scala.math.BigInt): XML.Tree =

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

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

  } 

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

  def   get_asms(calcid: scala.math.BigInt, pos: Position): XML.Tree =

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

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

      DataTypes.xml_of_Position(pos)))

  } 

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

  //def get_formulae(calcid: scala.math.BigInt, from: ICalcIterator,to: ICalcIterator,

  def   get_formulae(calcid: scala.math.BigInt, from: Position,     to: Position,

    level: scala.math.BigInt, rules: Boolean): XML.Tree =

  { XML.Elem(("GETFORMULAEFROMTO", Nil), List(

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

      DataTypes.xml_of_Position(from), //Isabelle/Isac needs no further data from ICalcIterator

      DataTypes.xml_of_Position(to),

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

      XML.Elem(("BOOL", Nil), List(XML.Text(rules.toString)))))

  } 

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

  def   get_tac(calcid: scala.math.BigInt, pos: Position): XML.Tree =

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

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

      DataTypes.xml_of_Position(pos)))

  } 

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

  def   init_ctxt(calcid: scala.math.BigInt, ketype: ContextType, pos: Position): XML.Tree =

  { XML.Elem(("INITCONTEXT", Nil), List(

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

      DataTypes.xml_of_ContextType(ketype),

      DataTypes.xml_of_Position(pos) ))

  }

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

  //... ONLY IMPL. IN Math_Engine

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

  def   inter_steps(calcid: scala.math.BigInt, pos: Position): XML.Tree =

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

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

      DataTypes.xml_of_Position(pos)))

  } 

  //fun Iterator : calcID -> XML.tree                ...IS ONLY A scala.math.BigInt

  //fun IteratorTEST : calcID -> iterID              ... only relevant for Isabelle/Isac

  //fun modelProblem : calcID -> XML.tree            ...IS ONLY A scala.math.BigInt

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

  def   modify_calchead(calcid: scala.math.BigInt, calchead: CalcHead): XML.Tree =

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

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

      DataTypes.xml_of_CalcHead(calchead)))

  } 

  //fun moveActiveCalcHead : calcID -> XML.tree

  def   move_active_calchead(calcid: scala.math.BigInt): XML.Tree =

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

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

  } 

  // BridgeRMI#moveActiveDown needs Protocol#move_active_down + Protocol#move_down

  //fun moveActiveDown : calcID -> XML.tree

  def   move_active_down(calcid: scala.math.BigInt): XML.Tree =

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

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

  } 

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

  def   move_active_form(calcid: scala.math.BigInt, pos: Position): XML.Tree =

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

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

      DataTypes.xml_of_Position(pos)))

  } 

  //fun moveActiveLevelDown : calcID -> XML.tree

  def   move_active_levdown(calcid: scala.math.BigInt): XML.Tree =

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

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

  } 

  //fun moveActiveLevelUp : calcID -> XML.tree

  def   move_active_levup(calcid: scala.math.BigInt): XML.Tree =

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

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

  } 

  //fun moveActiveRoot : calcID -> XML.tree

  //  uses only an BigInt, not an XML.Tree

  //fun moveActiveRootTEST : calcID -> XML.tree

  //... only relevant for Isabelle/Isac

  //fun moveActiveUp : calcID -> XML.tree

  def   move_active_up(calcid: scala.math.BigInt): XML.Tree =

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

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

  } 

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

  def   move_calchead(calcid: scala.math.BigInt, pos: Position): XML.Tree =

  { XML.Elem(("GETTACTIC"/*shortcut in coding*/, Nil), List(

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

      DataTypes.xml_of_Position(pos)))

  } 

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

  def   move_down(calcid: scala.math.BigInt, pos: Position): XML.Tree =

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

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

      DataTypes.xml_of_Position(pos)))

  } 

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

  def   move_levdn(calcid: scala.math.BigInt, pos: Position): XML.Tree =

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

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

      DataTypes.xml_of_Position(pos)))

  } 

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

  def   move_levup(calcid: scala.math.BigInt, pos: Position): XML.Tree =

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

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

      DataTypes.xml_of_Position(pos)))

  } 

  //fun moveRoot : calcID -> XML.tree

  def   move_root(calcid: scala.math.BigInt): XML.Tree =

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

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

  } 

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

  def   move_up(calcid: scala.math.BigInt, pos: Position): XML.Tree =

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

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

      DataTypes.xml_of_Position(pos)))

  } 

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

  //def ref_formula(calcid: scala.math.BigInt, pos: ICalcIterator 

  def   ref_formula(calcid: scala.math.BigInt, pos: Position): XML.Tree =

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

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

      DataTypes.xml_of_Position(pos)))

  }  

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

  def   refine_pbl(calcid: scala.math.BigInt, from: Position, kestore_key: String): XML.Tree =

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

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

      DataTypes.xml_of_Position(from),

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

  } 

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

  def replace_form(calcid: scala.math.BigInt, form: Formula): XML.Tree =

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

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

      DataTypes.xml_of_Formula_NEW(form)))

  }

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

  //...ONLY IMPLEMENTED IN Math_Engine

  //fun resetCalcHead : calcID -> XML.tree

  def reset_calchead(calcid: scala.math.BigInt): XML.Tree =

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

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

  }

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

  def   set_ctxt(calcid: scala.math.BigInt, pos: Position, kestore_key: String): XML.Tree =

  { XML.Elem(("CONTEXT", Nil), List(

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

      DataTypes.xml_of_Position(pos),

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

  } 

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

  def   set_met(calcid: scala.math.BigInt, met_key: java.util.Vector[String]): XML.Tree =

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

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

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

        DataTypes.xml_of_VectorString(met_key)))))

  } 

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

  def   set_next_tac(calcid: scala.math.BigInt, tac: Tactic): XML.Tree =

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

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

      DataTypesCompanion.xml_of_Tactic(tac)))

  } 

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

  def   set_pbl(calcid: scala.math.BigInt, pbl_key: java.util.Vector[String]): XML.Tree =

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

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

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

        DataTypes.xml_of_VectorString(pbl_key)))))

  } 

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

  def   set_thy(calcid: scala.math.BigInt, thy_id: String): XML.Tree =

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

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

      XML.Elem(("THEORYID", Nil), List(XML.Text(calcid.toString())))))

  } 

}