/* 

 * @author Walther Neuper

 * Copyright (c) due to license terms

 * Created on Jul 14, 2015

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

 * 

 * From now on isac-java is a Scala Project.

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

 * off and on again helped.

 */

package isac.bridge.xml

import isac.bridge.CChanged

import isac.util.formulae.Position

import isac.util.formulae.Specification

import isac.util.Variant

import isac.util.Formalization

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

import scala.collection.JavaConversions._

object JavaToIsa {

  //===== convert arguments of JSystem.invoke(Operations.*

  // Conversions are all done in Scala (has specific methods), not in Java.

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

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

  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 ?

  }

  //----- step 1 -----------------------

  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(

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

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

        ConvertXML.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(

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

      xml_of_Specification(vat.getSpecification())))

  }

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

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

  }

  /*isabelle.XML.Tree = 

      <FORMALIZATION>

        <VARIANT>

          <STRINGLIST>      

            <STRING>equality (x+1=(2::real))</STRING>

            <STRING>solveFor x</STRING>

            <STRING>solutions L</STRING>

          </STRINGLIST>

          <SPECIFICATION>

            <THEORYID>Test</THEORYID>

            <PROBLEMID>

              <STRINGLIST>

                <STRING>sqroot-test</STRING>

                <STRING>univariate</STRING>

                <STRING>equation</STRING>

                <STRING>test</STRING></STRINGLIST>

            </PROBLEMID>

            <METHODID>

              <STRINGLIST>

                <STRING>Test</STRING>

                <STRING>squ-equ-test-subpbl1</STRING>

              </STRINGLIST>

            </METHODID>

          </SPECIFICATION>

        </VARIANT>

      </FORMALIZATION>

  */

  //----- step 4 -----------------------

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

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

    ConvertXML.xml_of_pos(List(1: java.lang.Integer) map Integer_to_BigInt, pos.getKind())

  }

  //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/*?*/: String): XML.Tree =

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

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

      xml_of_Position(from),

      xml_of_Position(to),

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

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

  } 

  //----- step 6 -----------------------

  //def ref_formula(calcid: scala.math.BigInt, pos: ICalcIterator,  //NOT RESOLVED BY sbt  

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

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

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

      xml_of_Position(pos)))

  }  

  //----- step 7 -----------------------

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

  {    

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

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

      XML.Elem(Markup("AUTO", Nil), List(XML.Text(auto)))))

  }

}