1.1 --- a/isac-java/src/java-tests/isac/bridge/xml/TestDataTypes.java Sat Aug 01 13:16:41 2015 +0200
1.2 +++ b/isac-java/src/java-tests/isac/bridge/xml/TestDataTypes.java Mon Aug 03 08:07:05 2015 +0200
1.3 @@ -6,21 +6,18 @@
1.4 */
1.5 package isac.bridge.xml;
1.6
1.7 +import isac.util.formulae.CalcHead;
1.8 +import isac.util.formulae.CalcHeadSimpleID;
1.9 +import isac.util.formulae.HierarchyKey;
1.10 import isac.util.formulae.Model;
1.11 import isac.util.formulae.ModelItem;
1.12 import isac.util.formulae.ModelItemList;
1.13 -import isac.util.formulae.CalcHead;
1.14 import isac.util.formulae.Specification;
1.15 import isac.bridge.xml.IsaToJava;
1.16
1.17 import isabelle.XML;
1.18
1.19 import java.util.Vector;
1.20 -
1.21 -
1.22 -
1.23 -//import scala.List; ..ERROR cannot be resolved.
1.24 -//WIE KRIEGE ICH List[ModelItem] | Vector[ModelItem] ?!?
1.25 import junit.framework.TestCase;
1.26
1.27 /**
1.28 @@ -30,9 +27,49 @@
1.29 * This file tests isac.bridge.xml.Dataypes (which is not yet activated)
1.30 * and is analogous to isabisac/src/Tools/isac/xmlsrc/datatypes.sml.
1.31 *
1.32 + * Legend:
1.33 + * / * ERROR * / marks initial occurrence before start of investigation.
1.34 + * / * ERR? * / marks lines inappropriate red [x] on the left margin,
1.35 + * although the code compiles correctly.
1.36 */
1.37 public class TestDataTypes extends TestCase {
1.38
1.39 + public void testSpecification() throws Exception {
1.40 + System.out.println(" ---------------------------------------------");
1.41 + System.out.println("/--BEGIN isac.bridge.xml.DataTypes#testSpecification");
1.42 +
1.43 + XML.Tree REF_FORMULA_out = TestDataTypesDATA.create_REF_FORMULA_out();
1.44 + System.out.println("REF_FORMULA_out = " + REF_FORMULA_out);
1.45 + XML.Tree xml_spec = TestDataTypesDATA.create_xml_spec(REF_FORMULA_out);
1.46 + System.out.println("xml_spec = " + xml_spec);
1.47 + Specification spec = null;
1.48 + /*ERROR*/ spec = IsaToJava.xml_to_Specification(xml_spec);
1.49 + assertEquals(spec.getTheory().toString(), "e_domID\n");
1.50 + assertEquals(spec.getProblem().toSMLString(), "[\"e_pblID\"]");
1.51 + assertEquals(spec.getMethod().toSMLString(), "[\"e_metID\"]");
1.52 +
1.53 + ///-------------------------------------------------------------------
1.54 + // follow scala code in IsaToJava.xml_to_Specification as close as possible
1.55 + XML.Tree xml_thy = TestDataTypesDATA.create_xml_thy(xml_spec);
1.56 + System.out.println("xml_thy (created in Scala) = " + xml_thy);//XML.Tree!!!
1.57 + CalcHeadSimpleID thy_key = new CalcHeadSimpleID();
1.58 + thy_key.setID(IsaToJava.xml_to_String(xml_thy));
1.59 +
1.60 + XML.Tree xml_pbl = TestDataTypesDATA.create_xml_pbl(xml_spec);
1.61 + System.out.println("xml_pbl (created in Scala) = " + xml_pbl);
1.62 + HierarchyKey pbl_key = new HierarchyKey();
1.63 +/*ERR?*/pbl_key.setID(IsaToJava.xml_to_VectorString(xml_pbl));
1.64 +
1.65 + XML.Tree xml_met = TestDataTypesDATA.create_xml_met(xml_spec);
1.66 + System.out.println("xml_met (created in Scala) = " + xml_met);
1.67 + HierarchyKey met_key = new HierarchyKey();
1.68 +/*ERR?*/met_key.setID(IsaToJava.xml_to_VectorString(xml_met));
1.69 +
1.70 + spec = new Specification(thy_key, pbl_key, met_key);
1.71 +
1.72 + System.out.println("\\--END isac.bridge.DataTypes#testSpecification");
1.73 + }
1.74 +
1.75 /**
1.76 * Components of isac.util.formulae.CalcHead,
1.77 * investigated wrt. error found in
1.78 @@ -46,27 +83,25 @@
1.79 * / * ERROR * /IntFormHead calcid_formhead = ... ((blanks "* /" due to parsing comment))
1.80 * GIVES NO OUTPUT FROM THE WHOLE TEST CASE, NOT EVEN
1.81 * System.out.println("/--BEGIN isac.bridge.TestPIDE#testMini_Test");
1.82 - *
1.83 - * Legend:
1.84 - * / * ERROR * / marks initial occurrence before bottom up construction
1.85 - * / * ERR? * / marks lines inappropriate red [x] on the left margin,
1.86 - * although the code compiles correctly.
1.87 */
1.88 public void testCalcHead() throws Exception {
1.89 + System.out.println(" ---------------------------------------------");
1.90 System.out.println("/--BEGIN isac.bridge.xml.DataTypes#testCalcHead");
1.91
1.92 - //top down for TestPIDE.java ----- step 6 -------------------------------------
1.93 + //top down for TestPIDE.java ----- step 6 -------------------------------------
1.94 XML.Tree REF_FORMULA_out = TestDataTypesDATA.create_REF_FORMULA_out();
1.95 System.out.println("REF_FORMULA_out = " + REF_FORMULA_out);
1.96 XML.Tree xml_calchead = TestDataTypesDATA.create_xml_calchead(REF_FORMULA_out);
1.97 - System.out.println("xml_calchead = " + xml_calchead);
1.98 -//GOON CalcHead calchead = IsaToJava.xml_to_CalcHead(xml_calchead);
1.99 -//GOON //*ERROR*/IntFormHead calcid_formhead = IsaToJava.ref_formula_out(REF_FORMULA_out);
1.100 + System.out.println("xml_calchead (created in Scala) = " + xml_calchead);
1.101 + /*ERROR*/ CalcHead calchead = IsaToJava.xml_to_CalcHead(xml_calchead);
1.102 + /*ERROR*/ IntFormHead calcid_formhead = IsaToJava.ref_formula_out(REF_FORMULA_out);
1.103 //^^^^^^^ CONSOLE OUTPUT WAS:
1.104 //# 6 --ref_formula_out: CALCHEAD before
1.105 //11 xml_to_CalcHead before: new CalcHead
1.106 + /////////////////////////////////////////
1.107
1.108 - //---------------- bottom up construction ------------------------------
1.109 + ///-------------------------------------------------------------------
1.110 + // follow scala code in IsaToJava.xml_to_Specification as close as possible
1.111 //--------- Model ------------------------------
1.112 //create ModelItem ...
1.113 XML.Tree xml_item = TestDataTypesDATA.create_xml_item();
1.114 @@ -84,8 +119,8 @@
1.115
1.116 //create Model bottom up ...
1.117 XML.Tree xml_model = TestDataTypesDATA.create_xml_model(REF_FORMULA_out);
1.118 - System.out.println("xml_model (decomposed) = " + xml_model);
1.119 - /*ERROR*/Model model = IsaToJava.xml_to_Model(xml_model);
1.120 + System.out.println("xml_model (created in Scala) = " + xml_model);
1.121 + /*ERROR*/ Model model = IsaToJava.xml_to_Model(xml_model);
1.122
1.123 Vector<ModelItem> givens = model.getGiven().getItems();
1.124 assertEquals(givens.size(), 0);
1.125 @@ -117,11 +152,8 @@
1.126 "\nModel:\nGiven:\n[]\nWhere:\n[\"false (precond_rootpbl v_v)\"]\nFind:\n[]\nRelate:\n[]");
1.127
1.128 //--------- Specification ------------------------------
1.129 - //create HierarchyKey bottom up ...
1.130 -//GOON
1.131 -
1.132 XML.Tree xml_spec = TestDataTypesDATA.create_xml_spec(REF_FORMULA_out);
1.133 -//GOON Specification spec = IsaToJava.xml_to_Specification(xml_spec);
1.134 + /*ERROR*/ Specification spec = IsaToJava.xml_to_Specification(xml_spec);
1.135
1.136 System.out.println("\\--END isac.bridge.DataTypes#testCalcHead");
1.137 }