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

 	}

 }