package isac.bridge;

import isac.bridge.xml.IntCalcFormula;

import isac.bridge.xml.IntCChanged;

import isac.bridge.xml.IntIntCompound;

import isac.bridge.xml.IntFormHead;

import isac.bridge.xml.IntFormulas;

import isac.bridge.xml.IntPosition;

import isac.bridge.xml.DataTypes;  //.scala

import isac.bridge.xml.JavaToIsa;  //.scala

import isac.bridge.xml.IsaToJava;  //.scala

import isac.util.formulae.CalcFormula;

import isac.util.formulae.CalcHead;

import isac.util.formulae.CalcHeadSimpleID;

import isac.util.formulae.HierarchyKey;

import isac.util.formulae.Model;

import isac.util.formulae.ModelItem;

import isac.util.formulae.Position;

import isac.util.formulae.Specification;

import isac.util.Formalization;

import isac.util.Variant;

import edu.tum.cs.isabelle.japi.JSystem;

import edu.tum.cs.isabelle.japi.Operations;

import isabelle.XML;

import java.io.File;

import java.math.BigInteger;

import java.util.Vector;

import junit.framework.TestCase;

public class TestPIDE extends TestCase {

	/* 

	 * ISABELLE_HOME is set by "isabelle.Isabelle_System.init",

	 * the connection to Isabelle/Isac by "JSystem.instance". 

	 */

    public void testConnection() {

        System.out.println("/--BEGIN isac.bridge.TestPIDE#testConnection");

		System.out.println("---1 isac.bridge.TestPIDE#testConnection");        

        isabelle.Isabelle_System.init("/usr/local/isabisac", "");

        System.out.println("---2 isac.bridge.TestPIDE#testConnection");        

        JSystem sys = JSystem.instance(new File("/home/wneuper/proto4/libisabelle/."), "Protocol");

		System.out.println("---3 isac.bridge.TestPIDE#testConnection");        

		String hello_out = sys.invoke(Operations.HELLO, "should-be-returned");

		System.out.println("---4 isac.bridge.TestPIDE#testConnection");        

		assertEquals(hello_out,"Hello should-be-returned");

		System.out.println("---5 isac.bridge.TestPIDE#testConnection");        

	    sys.dispose();

	    System.out.println("\\--END isac.bridge.TestPIDE#testConnection");        

	}

    /*

     * transfer the minimal test from libisabelle to isac-java:

     * https://github.com/wneuper/libisabelle/blob/master/examples/src/main/java/Mini_Test.java

     * which has been derived from:

     * https://github.com/wneuper/libisabelle/blob/master/doc/test--isac-Java--isac-kernel.txt

     */

	public void testMini_Test() {

		System.out.println("/--BEGIN isac.bridge.TestPIDE#testMini_Test");

	    isabelle.Isabelle_System.init("/usr/local/isabisac", "");

	    JSystem sys = JSystem.instance(new File("/home/wneuper/proto4/libisabelle/."), "Protocol");

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

	    //build Formalization in Java and then convert to XML

	    CalcHeadSimpleID thy = new CalcHeadSimpleID();

	    thy.setID("Test");

	    HierarchyKey pbl = new HierarchyKey();

	    pbl.addString("sqroot-test");

	    pbl.addString("univariate");

	    pbl.addString("equation");

	    pbl.addString("test");

	    HierarchyKey met = new HierarchyKey();

	    met.addString("Test");

	    met.addString("squ-equ-test-subpbl1");

	    Specification spec = new Specification();

	    spec.setTheory(thy);

	    spec.setProblem(pbl);

	    spec.setMethod(met);

	    Variant vat = new Variant();

	    vat.addNewIsaString("equality (x+1=(2::real))");

	    vat.addNewIsaString("solveFor x");

	    vat.addNewIsaString("solutions L");

	    vat.setSpecification(spec);

	    Formalization fmz = new Formalization();

	    fmz.addNewVariant(vat);

	    XML.Tree CALC_TREE_out = sys.invoke(Operations.CALC_TREE,

	      DataTypes.xml_of_Formalization(fmz));

	    int calcid = (IsaToJava.calc_tree_out(CALC_TREE_out)).intValue();

		assertEquals(calcid, 1);

	    System.out.println("# 1  # " + CALC_TREE_out);

	    //----- step 2 ----------------------------------------------------------------

	    XML.Tree ITERATOR_out = sys.invoke(Operations.ITERATOR,

	      new scala.math.BigInt(BigInteger.valueOf(calcid)));

	    IntIntCompound int_int = IsaToJava.iterator_out(ITERATOR_out);

	    calcid = int_int.get_calcid().intValue();

	    int userid = int_int.get_userid().intValue();

		assertEquals(calcid, 1);

		assertEquals(userid, 1);

	    System.out.println("# 2  # " + ITERATOR_out);

	    //----- step 3 ----------------------------------------------------------------

	    XML.Tree MOVE_ACTIVE_ROOT_out = sys.invoke(Operations.MOVE_ACTIVE_ROOT,

	      new scala.math.BigInt(BigInteger.valueOf(calcid)));

	    IntPosition calcid_pos = IsaToJava.move_active_root_out(MOVE_ACTIVE_ROOT_out);

	    calcid = calcid_pos.getCalcId();

	    Position pos = calcid_pos.getPos();

		assertEquals(pos.toSMLString(), "([],Pbl)");

	    System.out.println("# 3  # " + MOVE_ACTIVE_ROOT_out);

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

        Position from = new Position();

        from.setKind("Pbl");

        Position to = new Position();

        to.setKind("Pbl");

        int level = 0;

        boolean rules = false;

        XML.Tree GET_FORMULAE_out = sys.invoke(Operations.GET_FORMULAE,

          JavaToIsa.get_formulae(new scala.math.BigInt(BigInteger.valueOf(calcid)),

          from, to, new scala.math.BigInt(BigInteger.valueOf(level)), rules));

        IntFormulas calcid_forms = IsaToJava.get_formulae_out(GET_FORMULAE_out);

	    calcid = calcid_forms.getCalcId();

        Vector<CalcFormula> forms = calcid_forms.getCalcFormulas();

		assertEquals(forms.size(), 1);

		assertEquals(((CalcFormula)forms.elementAt(0)).getFormula(), "solve (x + 1 = 2, x)");

        System.out.println("# 4  # " + GET_FORMULAE_out);

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

        pos = new Position();

        pos.setKind("Pbl");

	    XML.Tree REF_FORMULA_out = sys.invoke(Operations.REF_FORMULA,

	      JavaToIsa.ref_formula(new scala.math.BigInt(BigInteger.valueOf(calcid)), pos));

	    System.out.println("# 6 before IsaToJava.ref_formula_out");

        IntFormHead calcid_formhead = IsaToJava.ref_formula_out(REF_FORMULA_out);

        calcid = calcid_formhead.getCalcId();

        assertEquals(calcid, 1);

        CalcHead ch = (CalcHead)(calcid_formhead.getFormHead());

        assertEquals(ch.getPosition().toSMLString(), "([],Pbl)");

        assertEquals(ch.getHeadLine().toSMLString(), "solve (x + 1 = 2, x)");

        Model model = ch.getModel();

        assertEquals(model.getGiven().getItems().size(), 0);

        assertEquals(model.getWhere().getItems().size(), 1);

        assertEquals(((ModelItem)model.getWhere().getItems().elementAt(0)).getItemStatus(), "false");

        assertEquals(((ModelItem)model.getWhere().getItems().elementAt(0)).toSMLString(), "precond_rootpbl v_v");

        assertEquals(ch.getBelongsTo(), "Pbl");

        spec = ch.getSpecification();

        assertEquals(spec.getTheory().toString(), "e_domID\n");

        assertEquals(spec.getProblem().toSMLString(), "[\"e_pblID\"]");

        assertEquals(spec.getMethod().toSMLString(), "[\"e_metID\"]");

	    System.out.println("# 6  # " + REF_FORMULA_out);

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

	    String scope = "CompleteCalc";

	    XML.Tree AUTO_CALC_out = sys.invoke(Operations.AUTO_CALC,

	      JavaToIsa.auto_calculate(new scala.math.BigInt(BigInteger.valueOf(calcid)), scope, 

	    	new scala.math.BigInt(BigInteger.valueOf(0))));

	    IntCChanged calcid_cc = IsaToJava.auto_calc_out(AUTO_CALC_out);

	    calcid = calcid_cc.getCalcId();

	    CChanged cc = calcid_cc.getCChanged();

		assertEquals(cc.getLastUnchanged().toSMLString(), "([],Pbl)");

		assertEquals(cc.getLastDeleted().toSMLString(), "([],Pbl)");

		assertEquals(cc.getLastGenerated().toSMLString(), "([],Res)");

	    System.out.println("# 7  # " + AUTO_CALC_out);

	    //----- step 10 ---------------------------------------------------------------

        pos = new Position();

        pos.setKind("Res");

	    REF_FORMULA_out = sys.invoke(Operations.REF_FORMULA,

	      JavaToIsa.ref_formula(new scala.math.BigInt(BigInteger.valueOf(calcid)), pos));

	    calcid_formhead = IsaToJava.ref_formula_out(REF_FORMULA_out);

	    calcid = calcid_formhead.getCalcId().intValue();

	    // later here we shall check for CalcFormula OR CalcHead

	    CalcFormula form = (CalcFormula)calcid_formhead.getFormHead();

	    form.getFormula();

	    assertEquals(form.getPosition().toSMLString(), "([],Res)");

	    assertEquals(form.toString(), "[x = 1]");

	    System.out.println("# 10 # " + REF_FORMULA_out);

	    //----- step 13 ---------------------------------------------------------------

	    XML.Tree DEL_CALC_out = sys.invoke(Operations.DEL_CALC,

	      new scala.math.BigInt(BigInteger.valueOf(calcid)));

	    calcid = IsaToJava.del_calc_out(DEL_CALC_out).intValue();

		assertEquals(calcid, 1);

	    System.out.println("# 13 # " + DEL_CALC_out);

	    sys.dispose();

		System.out.println("\\--END isac.bridge.TestPIDE##testMini_Test");

	}

}