/*

 * @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.xml.DataTypes;

import isac.bridge.xml.DataTypesCompanion;

import isac.bridge.xml.IsaToJava;

import isac.bridge.xml.TestsDATA;

import isac.gui.mawen.syntax.Ast;

import isac.util.formulae.CalcHead;

import isac.util.formulae.CalcHeadSimpleID;

import isac.util.formulae.Formula;

import isac.util.formulae.HierarchyKey;

import isac.util.formulae.Model;

import isac.util.formulae.ModelItem;

import isac.util.formulae.ModelItemList;

import isac.util.formulae.Specification;

import isac.util.Formalization;

import isac.util.Variant;

import isac.util.tactics.Rewrite;

import isac.util.tactics.RewriteInst;

import isac.util.tactics.StringListTactic;

import isac.util.tactics.Tactic;

import isac.util.tactics.Theorem;

import edu.tum.cs.isabelle.api.XML;

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

import java.util.Vector;

import junit.framework.TestCase;

/**

 * @author Walther Neuper Jul 21, 2015

 * 

 * Test conversion of relevant Objects to/from XML.Tree. 

 * This file tests isac.bridge.xml.Dataypes (which is not yet activated)

 * and is analogous to isabisac/src/Tools/isac/xmlsrc/datatypes.sml.

 * 

 * Legend:

 * / * ERROR * / marks initial occurrence before start of investigation.

 * / * ERR? * / marks lines inappropriate red [x] on the left margin,

 *              although the code compiles correctly.

 */

public class TestDataTypes extends TestCase {

    public void testSpecification() throws Exception {

        System.out.println("  ---------------------------------------------");

        System.out.println("/--BEGIN isac.bridge.xml.DataTypes#testSpecification");

        XML.Tree REF_FORMULA_out = TestDataTypesDATA.create_REF_FORMULA_out();

        System.out.println("REF_FORMULA_out = " + REF_FORMULA_out);

        XML.Tree xml_spec = TestDataTypesDATA.create_xml_spec(REF_FORMULA_out);

        System.out.println("xml_spec = " + xml_spec);

        Specification spec = null;

        spec = DataTypes.xml_to_Specification(xml_spec);

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

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

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

        ///-------------------------------------------------------------------

        // follow scala code in IsaToJava.xml_to_Specification as close as possible

        XML.Tree xml_thy = TestDataTypesDATA.create_xml_thy(xml_spec);

        System.out.println("xml_thy (created in Scala) = " + xml_thy);//XML.Tree!!!

        CalcHeadSimpleID thy_key = new CalcHeadSimpleID();

        thy_key.setID(DataTypes.xml_to_String(xml_thy));

        XML.Tree xml_pbl = TestDataTypesDATA.create_xml_pbl(xml_spec);

        System.out.println("xml_pbl (created in Scala) = " + xml_pbl);

        HierarchyKey pbl_key = new HierarchyKey();

/*ERR?*/pbl_key.setID(DataTypes.xml_to_VectorString(xml_pbl));

        XML.Tree xml_met = TestDataTypesDATA.create_xml_met(xml_spec);

        System.out.println("xml_met (created in Scala) = " + xml_met);

        HierarchyKey met_key = new HierarchyKey();

/*ERR?*/met_key.setID(DataTypes.xml_to_VectorString(xml_met));

        spec = new Specification(thy_key, pbl_key, met_key);

        System.out.println("\\--END isac.bridge.DataTypes#testSpecification");

    }

	/**

	 * 

	 */

    public void test_xml_to_Formula_NEW() throws Exception {

        System.out.println("  ---------------------------------------------");

        System.out.println("/--BEGIN isac.bridge.xml.DataTypes#test_xml_to_Formula_NEW");

        Term t = TestsDATA.term_mini_subpbl_1();

        XML.Tree xml_tree = TestDataTypesDATA.create_Formula_NEW(t);

        Formula f = DataTypes.xml_to_Formula_NEW(xml_tree);

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

/*ERR?*/assertEquals(Ast.math_string_of(f.getTerm()), "solve (x + 1 = 2, x)");

        System.out.println("\\--END isac.bridge.DataTypes#test_xml_to_Formula_NEW");

    }

    /**

     * Components of isac.util.formulae.CalcHead,

     * investigated wrt. error found in 

     * https://intra.ist.tugraz.at/hg/isac/rev/9b6d305fb011: 

     * with (outcommented)

     *   // * ERROR * /IntFormHead calcid_formhead = ... ((blanks "* /" due to parsing comment))

     * reaches tracing at

     * https://intra.ist.tugraz.at/hg/isac/file/9b6d305fb011/isac-java/src/java-tests/isac/bridge/TestPIDE.java#l141

     * https://intra.ist.tugraz.at/hg/isac/file/9b6d305fb011/isac-java/src/java/isac/bridge/xml/IsaToJava.scala#l244

     * but with (NOT outcommented)

     *    / * ERROR * /IntFormHead calcid_formhead = ... ((blanks "* /" due to parsing comment))

     * GIVES NO OUTPUT FROM THE WHOLE TEST CASE, NOT EVEN

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

     */

    public void testCalcHead() throws Exception {

        System.out.println("  ---------------------------------------------");

        System.out.println("/--BEGIN isac.bridge.xml.DataTypes#testCalcHead");

        //top down for TestPIDE.java ----- step 6 -------------------------------------

        XML.Tree REF_FORMULA_out = TestDataTypesDATA.create_REF_FORMULA_out();

        System.out.println("REF_FORMULA_out = " + REF_FORMULA_out);

        XML.Tree xml_calchead = TestDataTypesDATA.create_xml_calchead(REF_FORMULA_out);

        System.out.println("xml_calchead (created in Scala) = " + xml_calchead);

        /*CalcHead calchead =*/ DataTypes.xml_to_CalcHead(xml_calchead);

        /*ERROR*/ IntFormHead calcid_formhead = IsaToJava.ref_formula_out(REF_FORMULA_out);

        //^^^^^^^ CONSOLE OUTPUT WAS:

        //# 6  --ref_formula_out: CALCHEAD before

        //11 xml_to_CalcHead before: new CalcHead

        /////////////////////////////////////////

        // asserts after successful tackling error bottom up below:

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

        ///-------------------------------------------------------------------

        // follow scala code in IsaToJava.xml_to_Specification as close as possible

        //--------- Model ------------------------------

        //create ModelItem ...

        XML.Tree xml_item = TestDataTypesDATA.create_xml_item();

        ModelItem mit = DataTypes.xml_to_ModelItem(xml_item);

        assertEquals(mit.getItemStatus(), "false");

        assertEquals(mit.getFormula().toSMLString(), "precond_rootpbl v_v");

        Vector<ModelItem> mits = new Vector<>();

        mits.add(mit);

        //test conversion SCala List <--> Java Vector: content is invariant ...

        mits = DataTypes.sList2jVectorModelItem(TestDataTypesDATA.jVector2sList(mits));

        mit = mits.get(0);

        assertEquals(mit.getItemStatus(), "false");

        assertEquals(mit.getFormula().toSMLString(), "precond_rootpbl v_v");

        //create Model bottom up ...

        XML.Tree xml_model = TestDataTypesDATA.create_xml_model(REF_FORMULA_out);

        System.out.println("xml_model (created in Scala) = " + xml_model);

        model = DataTypes.xml_to_Model(xml_model);

        Vector<ModelItem> givens = model.getGiven().getItems();

        assertEquals(givens.size(), 0);

        Vector<ModelItem> wheres = model.getWhere().getItems();

        assertEquals(wheres.size(), 1);

        assertEquals(wheres.elementAt(0).getItemStatus(), "false");

        assertEquals(wheres.elementAt(0).toSMLString(), "precond_rootpbl v_v");

        //another variant to create Model bottom up ...

        XML.Tree xml_given = TestDataTypesDATA.create_xml_given(xml_model); 

/*ERR?*/givens = DataTypes.xml_to_VectorModelItem(xml_given);

        assertEquals(givens.size(), 0);

        XML.Tree xml_where = TestDataTypesDATA.create_xml_where(xml_model); 

/*ERR?*/wheres = DataTypes.xml_to_VectorModelItem(xml_where);

        assertEquals(wheres.size(), 1);

        assertEquals(wheres.elementAt(0).getItemStatus(), "false");

        assertEquals(wheres.elementAt(0).toSMLString(), "precond_rootpbl v_v");

/*ERR?*/Vector<ModelItem> finds = DataTypes.xml_to_VectorModelItem(

          TestDataTypesDATA.create_xml_find(xml_model));

/*ERR?*/Vector<ModelItem> relates = DataTypes.xml_to_VectorModelItem(

          TestDataTypesDATA.create_xml_relate(xml_model));

        model = new Model(

          new ModelItemList(givens),

          new ModelItemList(wheres),

          new ModelItemList(finds),

          new ModelItemList(relates));

        assertEquals(model.toString(), 

          "\nModel:\nGiven:\n[]\nWhere:\n[\"false (precond_rootpbl v_v)\"]\nFind:\n[]\nRelate:\n[]");

        //--------- Specification ------------------------------

        XML.Tree xml_spec = TestDataTypesDATA.create_xml_spec(REF_FORMULA_out);

/*ERROR*/ spec = DataTypes.xml_to_Specification(xml_spec);

        System.out.println("\\--END isac.bridge.DataTypes#testCalcHead");

    }

    public void testFormalization() throws Exception {

        System.out.println("  ---------------------------------------------");

        System.out.println("/--BEGIN isac.bridge.xml.DataTypes#testFormalization");

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

        XML.Tree intree = DataTypes.xml_of_Formalization(fmz);

        assertEquals(intree.toString().substring(0,150),

          "Elem((FORMALIZATION,List()),List(Elem((VARIANT,List()),List(Elem((STRINGLIST,List()),List(Elem((STRING,List()),List(Text(equality (x+1=(2::real))))), ");

        System.out.println("\\--END isac.bridge.DataTypes#testFormalization");

    }

	/* 

	 * from hitting <NEW>button on <code>WindowApplication</code> Isabelle/Isac expects

	 * -->ISA: CalcTree [([], ("e_domID", ["e_pblID"], ["e_metID"]))];

	 */

    public void testEmptyFormalization() throws Exception {

        System.out.println("  ---------------------------------------------");

        System.out.println("/--BEGIN isac.bridge.xml.DataTypes#testEmptyFormalization");

        Formalization fmz = new Formalization();

        XML.Tree intree = DataTypes.xml_of_Formalization(fmz);

        String intree_cut = "Elem((FORMALIZATION,List()),List(Elem((VARIANT,List()),List(Elem((STRINGLIST,List()),List()), Elem((SPECIFICATION,List()),List(Elem((" 

          + "THEORYID,List()),List(Text(e_domID)))"; //.. etc.

        assertEquals(intree.toString().substring(0,170), intree_cut);

        // this fmz is now created by DataTypes.xml_of_Formalization:

        fmz = new Formalization();

	    CalcHeadSimpleID thy = new CalcHeadSimpleID();

	    thy.setID("e_domID");

	    HierarchyKey pbl = new HierarchyKey();

	    pbl.addString("e_pblID");

	    HierarchyKey met = new HierarchyKey();

	    met.addString("e_metID");

	    Specification spec = new Specification();

	    spec.setTheory(thy);

	    spec.setProblem(pbl);

	    spec.setMethod(met);

	    Variant vat = new Variant();

	    vat.setSpecification(spec);

	    fmz.addNewVariant(vat);

        intree = DataTypes.xml_of_Formalization(fmz);

        assertEquals(intree.toString().substring(0,170), intree_cut);

        System.out.println("\\--END isac.bridge.DataTypes#testEmptyFormalization");

    }

    public void testTactic() throws Exception {

        System.out.println("  ---------------------------------------------");

        System.out.println("/--BEGIN isac.bridge.xml.DataTypes#testTactic");

        //from java-tests-isacutil.parser.TestTactic

        //------- Rewrite ----------------------------------------------

        Tactic tac_built = new Rewrite();

        tac_built.setName("Rewrite");

        Theorem thm = new Theorem();

        thm.setId("pythagoras");

        Formula form = new Formula();

        form.setText("[| ?l is_const; ?m is_const |] ==> "

                + "?l * ?n + ?m * ?n = (?l + ?m) * ?n");

        form.setText("a^2 + b^2 = c^2");

        thm.setFormula(form);

        ((Rewrite) tac_built).setTheorem(thm);

        System.out.println("tac_built     = " + ((Rewrite) tac_built).toSMLString());

        XML.Tree tac_out = DataTypesCompanion.xml_of_Tactic(tac_built);

        System.out.println("Tree tac_out  = " + tac_out);

		//<REWRITETACTIC name="Rewrite">

		//  <THEOREM>

		//    <ID>pythagoras</ID>

		//    <FORMULA>a^2 + b^2 = c^2</FORMULA>               !!!different from Parser

		//  </THEOREM>

		//</REWRITETACTIC>         

        Tactic tac_in = (Tactic)DataTypes.xml_to_Tactic(tac_out);

        System.out.println("Tactic tac_in = " + tac_in.toSMLString());

        assertEquals(tac_built.toSMLString(), tac_in.toSMLString());

        //from java-tests-isacutil.parser.TestXMLParserDigest

        @SuppressWarnings("unused") // as data to remember

        String xmlString = "@@@@@begin@@@@@"// .................................

                + " 1"// ......................................................

                + " <GETTACTIC>"// ...........................................

                + "   <CALCID> 1 </CALCID>"// ..................................

                + "   <REWRITETACTIC name=\"Rewrite\">"// .............

                + "     <THEOREM>"// .......................................

                + "       <ID> Belastung_Querkraft </ID>"// ..................

                + "       <FORMULA>"// .........................!!!different from XML

                + "         <MATHML>"// ........................!!!different from XML

                + "           <ISA> - q ?x = Q' ?x </ISA>"// ...!!!different from XML

                + "         </MATHML>"// .......................!!!different from XML

                + "       </FORMULA>"// ........................!!!different from XML

                + "     </THEOREM>"// .......................................

                + "   </REWRITETACTIC>"// ...................................

                + " </GETTACTIC>" // ........................................

                + " @@@@@end@@@@@";

        //------- RewriteInst ------------------------------------------

        form.setText("?a = ?a");

        thm.setFormula(form);

        ((Rewrite) tac_built).setTheorem(thm);

        assertEquals("a = a", tac_built.showToBeginner());

        tac_built = null;

        tac_built = new RewriteInst();

        form.setText("(?k + ?bdv = ?m) = (?bdv = ?m + -1 * ?k)");

        thm.setFormula(form);

        ((RewriteInst) tac_built).setTheorem(thm);

        assertEquals("(k + bdv = m) = (bdv = m + -1 * k)", tac_built.showToBeginner());

        //------- RewriteSet -------------------------------------------

        //from java-tests-isacutil.parser.TestXMLParserDigest

        xmlString = "@@@@@begin@@@@@"// .................................

                + " 1"// ......................................................

                + " <GETTACTIC>"// ...........................................

                + "   <CALCID> 1 </CALCID>"// ..................................

                + "   <REWRITESETTACTIC name= \"Rewrite_Set\">"// .............

                + "     <RULESET> Test_simplify </RULESET>"// ....................

                + "   </REWRITESETTACTIC>"// ...................................

                + " </GETTACTIC>" // ........................................

                + " @@@@@end@@@@@";

        //------- StringListTactic -------------------------------------

        Vector<String> keylist = new Vector<>();

        keylist.add("normalize");

        keylist.add("polynomial");

        keylist.add("univariate");

        keylist.add("equation");

        tac_built = new StringListTactic("Specify_Problem", keylist);

        System.out.println(tac_built.toSMLString());

        assertEquals("Specify_Problem [\"normalize\",\"polynomial\","

                + "\"univariate\",\"equation\"]", tac_built.toSMLString());

        System.out.println("\\--END isac.bridge.DataTypes#testTactic");

    }

    public void testTactics() throws Exception {

        System.out.println("  ---------------------------------------------");

        System.out.println("/--BEGIN isac.bridge.xml.DataTypes#testTactics");

        //from java-tests-isacutil.parser.TestXMLParserDigest        

        @SuppressWarnings("unused") // as data to remember

        String xmlString = "> @@@@@begin@@@@@" // ...........................

                + " 1 " // ......................................................

                + "<APPLICABLETACTICS>" // .......................................

                + "  <CALCID> 1 </CALCID>" // ....................................

                + "  <TACLIST>" // ...............................................

                + "    <REWRITESETTACTIC name=\"Rewrite_Set\">"// .................

                + "      <RULESET> norm_equation </RULESET>"// ....................

                + "    </REWRITESETTACTIC>"// .....................................

                + "    <REWRITESETTACTIC name=\"Rewrite_Set\">"// .................

                + "      <RULESET> Test_simplify </RULESET>"// ....................

                + "    </REWRITESETTACTIC>"// .....................................

                + "    <SUBPROBLEMTACTIC name=\"Subproblem\">"// ..................

                + "      <THEORY> Test.thy </THEORY>"// ...........................

                + "      <PROBLEM>"// .............................................

                + "        <STRINGLIST>"// ........................................

                + "          <STRING> linear </STRING>"// .........................

                + "          <STRING> univariate </STRING>"// .....................

                + "          <STRING> equation </STRING>"// .......................

                + "          <STRING> test </STRING>"// ...........................

                + "        </STRINGLIST>"// .......................................

                + "      </PROBLEM>"// ............................................

                + "    </SUBPROBLEMTACTIC>"// .....................................

                + "    <SIMPLETACTIC name=\"Check_elementwise\">"// ...............

                + "      <MATHML>"// ............................................

                + "        <ISA> Assumptions </ISA>"// ..........................

                + "      </MATHML>"// ...........................................

                + "    </SIMPLETACTIC>"// .........................................

                + "  </TACLIST>"// ................................................

                + "</APPLICABLETACTICS>"// ........................................

                + "@@@@@end@@@@@";

//        wrapper_ = xml_parser_digest_.parse(xmlString);

//        tac = (Tactic) ((TacticsContainer) wrapper_.getResponse()).getTactics().elementAt(3);

//        assertEquals(tac.toSMLString(), "Check_elementwise \"Assumptions\"");

        System.out.println("\\--END isac.bridge.DataTypes#testTactics");

    }

}