package isac.bridge;

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

import isac.bridge.IsacOperations;

import isac.bridge.xml.IntCEvent;

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.Formula;

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 edu.tum.cs.isabelle.api.*;

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

//import edu.tum.cs.isabelle.*;    // OVERWRITES System.out.println

import edu.tum.cs.isabelle.pure.*; // DEFINES type Term

import edu.tum.cs.isabelle.setup.Setup;

import java.io.FileNotFoundException;

import java.io.IOException;

import java.io.InputStream;

import java.nio.file.Paths;

import java.math.BigInteger;

import java.util.Properties;

import java.util.Vector;

import junit.framework.TestCase;

public class TestPIDE extends TestCase {

	String isabelle_home_;

	public void setUp() {	          

	  InputStream inputStream = null;

	  try {

	    Properties prop = new Properties();

	    String propFileName = "./properties/BridgeMain.properties";

	    inputStream = getClass().getClassLoader().getResourceAsStream(propFileName);

	    if (inputStream != null) {

	      prop.load(inputStream);

	    } else {

	      throw new FileNotFoundException("property file '" + propFileName + "' not found in the classpath");

	    }

	    // get the property value and print it out

	    isabelle_home_ = prop.getProperty("ISABELLE_HOME");

        } catch (Exception e) {

	      System.out.println("Exception: " + e);

	    } finally {

	      try { inputStream.close();

			} catch (IOException e) { e.printStackTrace(); }

	    }

      }

	/* 

	 * 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");        

		Setup setup = new Setup(Paths.get(isabelle_home_), JPlatform.guess(),

          new Version("2015"), Setup.defaultPackageName());

        Environment env = JSetup.makeEnvironment(setup); // ohne Duration

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

/*Error*/Configuration config = Configuration.fromBuiltin("libisabelle_Isac");

	    JSystem sys = JSystem.create(env, config);

		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");

		Setup setup = new Setup(Paths.get(isabelle_home_), JPlatform.guess(),

          new Version("2015"), Setup.defaultPackageName());

        Environment env = JSetup.makeEnvironment(setup); // ohne Duration

	    Configuration config = Configuration.fromBuiltin("libisabelle_Isac");

	    JSystem sys = JSystem.create(env, config);

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

	    //build Formalization in Java and then convert to XML

	    Formalization fmz = isac.TESTUTIL.Formalization.solve_x_plus_1_equ_2();

	    XML.Tree CALC_TREE_out = sys.invoke(IsacOperations.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(IsacOperations.ITERATOR,

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

	    IntIntCompound int_int = IsaToJava.iterator_out(ITERATOR_out);

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

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

		assertEquals(calcid, 1);

		assertEquals(userid, 1);

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

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

	    XML.Tree MOVE_ACTIVE_ROOT_out = sys.invoke(IsacOperations.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.getPosition();

		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(IsacOperations.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().toString(), "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(IsacOperations.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");

        Specification 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(IsacOperations.AUTO_CALC,

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

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

	    IntCEvent calcid_cc = IsaToJava.auto_calc_out(AUTO_CALC_out);

	    calcid = calcid_cc.getCalcId();

	    CChanged cc = (CChanged)calcid_cc.getCEvent();

		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(IsacOperations.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(IsacOperations.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");

	}

    /*

     * transfer a term to Isabelle/Isac, let the term process there

     * and transfer the processed term back to here.

     * 

     * Note: this test probably goes beyond what is required by Isac:

     * 

     * Terms isac-java --> Isabelle/Isac are mostly input by user, 

     * thus may contain different kinds of errors;

     * their format is still to be determined (String ?).

     * 

     * Terms isac-java <-- Isabelle/Isac the other way round pack two formats,

     * edu.tum.cs.isabelle.pure.Term and String.

     */

	public void testTermTransfer() {

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

		Setup setup = new Setup(Paths.get(isabelle_home_), JPlatform.guess(),

           new Version("2015"), Setup.defaultPackageName());

        Environment env = JSetup.makeEnvironment(setup); // ohne Duration

	    Configuration config = Configuration.fromBuiltin("libisabelle_Isac");

	    JSystem sys = JSystem.create(env, config);

	    //----- create test_term ------------------------------------------------------

	    Term test_term = TestsDATA.test_term();

	    XML.Tree wrapped_term = DataTypes.xml_of_Term(test_term);

	    //----- transfer test_term to Isabelle/Isac and back again --------------------

	    /*XML.Tree processed_test_term =*/ sys.invoke(IsacOperations.TEST_TERM_TRANSFER, wrapped_term);

	    //----- check result ----------------------------------------------------------

	    // TODO

	    sys.dispose();

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

	}

    /*

     * transfer a String to Isabelle/Isac, let it parse there

     * and transfer the processed term back to here.

     * 

     * Terms isac-java --> Isabelle/Isac are mostly input by user, 

     * their format is String most likely during the next phase of devel.

     * 

     * Terms isac-java <-- Isabelle/Isac the other way round pack two formats,

     * edu.tum.cs.isabelle.pure.Term and String.

     */

	public void testTermOneWay() {

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

		Setup setup = new Setup(Paths.get(isabelle_home_), JPlatform.guess(),

           new Version("2015"), Setup.defaultPackageName());

        Environment env = JSetup.makeEnvironment(setup); // ohne Duration

	    Configuration config = Configuration.fromBuiltin("libisabelle_Isac");

	    JSystem sys = JSystem.create(env, config);

	    //----- create test_term ------------------------------------------------------

	    String term_str = "aaa + bbb::real";

	    //----- transfer test_term to Isabelle/Isac and back again --------------------

	    XML.Tree processed_test_term = sys.invoke(IsacOperations.TEST_TERM_ONE_WAY, term_str);

	    Formula form = DataTypes.xml_to_Formula_NEW(processed_test_term);

	    //----- check result ----------------------------------------------------------

	    assertEquals(form.toString(), "aaa + bbb = ??.processed_by_Isabelle_Isac");

	    //TODO Util#string_of(Term)

	    //assertEquals(Util.string_of(form.getTerm()), "aaa + bbb = ??.processed_by_Isabelle_Isac");

	    sys.dispose();

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

	}

}