2 * @author Walther Neuper
3 * Copyright (c) due to license terms
4 * Created on Jul 14, 2015
5 * Institute for Softwaretechnology, Graz University of Technology, Austria.
7 package isac.bridge.xml;
9 import isac.bridge.xml.DataTypes;
10 import isac.bridge.xml.DataTypesCompanion;
11 import isac.bridge.xml.IsaToJava;
12 import isac.bridge.xml.TestsDATA;
13 import isac.gui.mawen.syntax.Ast;
14 import isac.util.formulae.CalcHead;
15 import isac.util.formulae.CalcHeadSimpleID;
16 import isac.util.formulae.Formula;
17 import isac.util.formulae.HierarchyKey;
18 import isac.util.formulae.Model;
19 import isac.util.formulae.ModelItem;
20 import isac.util.formulae.ModelItemList;
21 import isac.util.formulae.Specification;
22 import isac.util.Formalization;
23 import isac.util.Variant;
24 import isac.util.tactics.Rewrite;
25 import isac.util.tactics.RewriteInst;
26 import isac.util.tactics.StringListTactic;
27 import isac.util.tactics.Tactic;
28 import isac.util.tactics.Theorem;
29 import edu.tum.cs.isabelle.api.XML;
30 import edu.tum.cs.isabelle.pure.*; // DEFINES type Term
32 import java.util.Vector;
34 import junit.framework.TestCase;
37 * @author Walther Neuper Jul 21, 2015
39 * Test conversion of relevant Objects to/from XML.Tree.
40 * This file tests isac.bridge.xml.Dataypes (which is not yet activated)
41 * and is analogous to isabisac/src/Tools/isac/xmlsrc/datatypes.sml.
44 * / * ERROR * / marks initial occurrence before start of investigation.
45 * / * ERR? * / marks lines inappropriate red [x] on the left margin,
46 * although the code compiles correctly.
48 public class TestDataTypes extends TestCase {
50 public void testSpecification() throws Exception {
51 System.out.println(" ---------------------------------------------");
52 System.out.println("/--BEGIN isac.bridge.xml.DataTypes#testSpecification");
54 XML.Tree REF_FORMULA_out = TestDataTypesDATA.create_REF_FORMULA_out();
55 System.out.println("REF_FORMULA_out = " + REF_FORMULA_out);
56 XML.Tree xml_spec = TestDataTypesDATA.create_xml_spec(REF_FORMULA_out);
57 System.out.println("xml_spec = " + xml_spec);
58 Specification spec = null;
59 spec = DataTypes.xml_to_Specification(xml_spec);
60 assertEquals(spec.getTheory().toString(), "e_domID\n");
61 assertEquals(spec.getProblem().toSMLString(), "[\"e_pblID\"]");
62 assertEquals(spec.getMethod().toSMLString(), "[\"e_metID\"]");
64 ///-------------------------------------------------------------------
65 // follow scala code in IsaToJava.xml_to_Specification as close as possible
66 XML.Tree xml_thy = TestDataTypesDATA.create_xml_thy(xml_spec);
67 System.out.println("xml_thy (created in Scala) = " + xml_thy);//XML.Tree!!!
68 CalcHeadSimpleID thy_key = new CalcHeadSimpleID();
69 thy_key.setID(DataTypes.xml_to_String(xml_thy));
71 XML.Tree xml_pbl = TestDataTypesDATA.create_xml_pbl(xml_spec);
72 System.out.println("xml_pbl (created in Scala) = " + xml_pbl);
73 HierarchyKey pbl_key = new HierarchyKey();
74 /*ERR?*/pbl_key.setID(DataTypes.xml_to_VectorString(xml_pbl));
76 XML.Tree xml_met = TestDataTypesDATA.create_xml_met(xml_spec);
77 System.out.println("xml_met (created in Scala) = " + xml_met);
78 HierarchyKey met_key = new HierarchyKey();
79 /*ERR?*/met_key.setID(DataTypes.xml_to_VectorString(xml_met));
81 spec = new Specification(thy_key, pbl_key, met_key);
83 System.out.println("\\--END isac.bridge.DataTypes#testSpecification");
89 public void test_xml_to_Formula_NEW() throws Exception {
90 System.out.println(" ---------------------------------------------");
91 System.out.println("/--BEGIN isac.bridge.xml.DataTypes#test_xml_to_Formula_NEW");
93 Term t = TestsDATA.term_mini_subpbl_1();
94 XML.Tree xml_tree = TestDataTypesDATA.create_Formula_NEW(t);
95 Formula f = DataTypes.xml_to_Formula_NEW(xml_tree);
96 assertEquals(f.toSMLString(), "solve (x + 1 = 2, x)");
97 /*ERR?*/assertEquals(Ast.math_string_of(f.getTerm()), "solve (x + 1 = 2, x)");
99 System.out.println("\\--END isac.bridge.DataTypes#test_xml_to_Formula_NEW");
103 * Components of isac.util.formulae.CalcHead,
104 * investigated wrt. error found in
105 * https://intra.ist.tugraz.at/hg/isac/rev/9b6d305fb011:
106 * with (outcommented)
107 * // * ERROR * /IntFormHead calcid_formhead = ... ((blanks "* /" due to parsing comment))
109 * https://intra.ist.tugraz.at/hg/isac/file/9b6d305fb011/isac-java/src/java-tests/isac/bridge/TestPIDE.java#l141
110 * https://intra.ist.tugraz.at/hg/isac/file/9b6d305fb011/isac-java/src/java/isac/bridge/xml/IsaToJava.scala#l244
111 * but with (NOT outcommented)
112 * / * ERROR * /IntFormHead calcid_formhead = ... ((blanks "* /" due to parsing comment))
113 * GIVES NO OUTPUT FROM THE WHOLE TEST CASE, NOT EVEN
114 * System.out.println("/--BEGIN isac.bridge.TestPIDE#testMini_Test");
116 public void testCalcHead() throws Exception {
117 System.out.println(" ---------------------------------------------");
118 System.out.println("/--BEGIN isac.bridge.xml.DataTypes#testCalcHead");
120 //top down for TestPIDE.java ----- step 6 -------------------------------------
121 XML.Tree REF_FORMULA_out = TestDataTypesDATA.create_REF_FORMULA_out();
122 System.out.println("REF_FORMULA_out = " + REF_FORMULA_out);
123 XML.Tree xml_calchead = TestDataTypesDATA.create_xml_calchead(REF_FORMULA_out);
124 System.out.println("xml_calchead (created in Scala) = " + xml_calchead);
125 /*CalcHead calchead =*/ DataTypes.xml_to_CalcHead(xml_calchead);
126 /*ERROR*/ IntFormHead calcid_formhead = IsaToJava.ref_formula_out(REF_FORMULA_out);
127 //^^^^^^^ CONSOLE OUTPUT WAS:
128 //# 6 --ref_formula_out: CALCHEAD before
129 //11 xml_to_CalcHead before: new CalcHead
130 /////////////////////////////////////////
131 // asserts after successful tackling error bottom up below:
132 CalcHead ch = (CalcHead)(calcid_formhead.getFormHead());
133 assertEquals(ch.getPosition().toSMLString(), "([],Pbl)");
134 assertEquals(ch.getHeadLine().toSMLString(), "solve (x + 1 = 2, x)");
136 Model model = ch.getModel();
137 assertEquals(model.getGiven().getItems().size(), 0);
138 assertEquals(model.getWhere().getItems().size(), 1);
139 assertEquals(((ModelItem)model.getWhere().getItems().elementAt(0)).getItemStatus(), "false");
140 assertEquals(((ModelItem)model.getWhere().getItems().elementAt(0)).toSMLString(), "precond_rootpbl v_v");
142 assertEquals(ch.getBelongsTo(), "Pbl");
144 Specification spec = ch.getSpecification();
145 assertEquals(spec.getTheory().toString(), "e_domID\n");
146 assertEquals(spec.getProblem().toSMLString(), "[\"e_pblID\"]");
147 assertEquals(spec.getMethod().toSMLString(), "[\"e_metID\"]");
149 ///-------------------------------------------------------------------
150 // follow scala code in IsaToJava.xml_to_Specification as close as possible
151 //--------- Model ------------------------------
152 //create ModelItem ...
153 XML.Tree xml_item = TestDataTypesDATA.create_xml_item();
154 ModelItem mit = DataTypes.xml_to_ModelItem(xml_item);
155 assertEquals(mit.getItemStatus(), "false");
156 assertEquals(mit.getFormula().toSMLString(), "precond_rootpbl v_v");
158 Vector<ModelItem> mits = new Vector<>();
160 //test conversion SCala List <--> Java Vector: content is invariant ...
161 mits = DataTypes.sList2jVectorModelItem(TestDataTypesDATA.jVector2sList(mits));
163 assertEquals(mit.getItemStatus(), "false");
164 assertEquals(mit.getFormula().toSMLString(), "precond_rootpbl v_v");
166 //create Model bottom up ...
167 XML.Tree xml_model = TestDataTypesDATA.create_xml_model(REF_FORMULA_out);
168 System.out.println("xml_model (created in Scala) = " + xml_model);
169 model = DataTypes.xml_to_Model(xml_model);
171 Vector<ModelItem> givens = model.getGiven().getItems();
172 assertEquals(givens.size(), 0);
173 Vector<ModelItem> wheres = model.getWhere().getItems();
174 assertEquals(wheres.size(), 1);
175 assertEquals(wheres.elementAt(0).getItemStatus(), "false");
176 assertEquals(wheres.elementAt(0).toSMLString(), "precond_rootpbl v_v");
178 //another variant to create Model bottom up ...
179 XML.Tree xml_given = TestDataTypesDATA.create_xml_given(xml_model);
180 /*ERR?*/givens = DataTypes.xml_to_VectorModelItem(xml_given);
181 assertEquals(givens.size(), 0);
182 XML.Tree xml_where = TestDataTypesDATA.create_xml_where(xml_model);
183 /*ERR?*/wheres = DataTypes.xml_to_VectorModelItem(xml_where);
184 assertEquals(wheres.size(), 1);
185 assertEquals(wheres.elementAt(0).getItemStatus(), "false");
186 assertEquals(wheres.elementAt(0).toSMLString(), "precond_rootpbl v_v");
187 /*ERR?*/Vector<ModelItem> finds = DataTypes.xml_to_VectorModelItem(
188 TestDataTypesDATA.create_xml_find(xml_model));
189 /*ERR?*/Vector<ModelItem> relates = DataTypes.xml_to_VectorModelItem(
190 TestDataTypesDATA.create_xml_relate(xml_model));
193 new ModelItemList(givens),
194 new ModelItemList(wheres),
195 new ModelItemList(finds),
196 new ModelItemList(relates));
197 assertEquals(model.toString(),
198 "\nModel:\nGiven:\n[]\nWhere:\n[\"false (precond_rootpbl v_v)\"]\nFind:\n[]\nRelate:\n[]");
200 //--------- Specification ------------------------------
201 XML.Tree xml_spec = TestDataTypesDATA.create_xml_spec(REF_FORMULA_out);
202 /*ERROR*/ spec = DataTypes.xml_to_Specification(xml_spec);
204 System.out.println("\\--END isac.bridge.DataTypes#testCalcHead");
207 public void testFormalization() throws Exception {
208 System.out.println(" ---------------------------------------------");
209 System.out.println("/--BEGIN isac.bridge.xml.DataTypes#testFormalization");
211 Formalization fmz = isac.TESTUTIL.Formalization.solve_x_plus_1_equ_2();
212 XML.Tree intree = DataTypes.xml_of_Formalization(fmz);
213 assertEquals(intree.toString().substring(0,150),
214 "Elem((FORMALIZATION,List()),List(Elem((VARIANT,List()),List(Elem((STRINGLIST,List()),List(Elem((STRING,List()),List(Text(equality (x+1=(2::real))))), ");
216 System.out.println("\\--END isac.bridge.DataTypes#testFormalization");
220 * from hitting <NEW>button on <code>WindowApplication</code> Isabelle/Isac expects
221 * -->ISA: CalcTree [([], ("e_domID", ["e_pblID"], ["e_metID"]))];
223 public void testEmptyFormalization() throws Exception {
224 System.out.println(" ---------------------------------------------");
225 System.out.println("/--BEGIN isac.bridge.xml.DataTypes#testEmptyFormalization");
227 Formalization fmz = new Formalization();
228 XML.Tree intree = DataTypes.xml_of_Formalization(fmz);
229 String intree_cut = "Elem((FORMALIZATION,List()),List(Elem((VARIANT,List()),List(Elem((STRINGLIST,List()),List()), Elem((SPECIFICATION,List()),List(Elem(("
230 + "THEORYID,List()),List(Text(e_domID)))"; //.. etc.
231 assertEquals(intree.toString().substring(0,170), intree_cut);
233 // this fmz is now created by DataTypes.xml_of_Formalization:
234 fmz = new Formalization();
235 CalcHeadSimpleID thy = new CalcHeadSimpleID();
236 thy.setID("e_domID");
237 HierarchyKey pbl = new HierarchyKey();
238 pbl.addString("e_pblID");
239 HierarchyKey met = new HierarchyKey();
240 met.addString("e_metID");
241 Specification spec = new Specification();
243 spec.setProblem(pbl);
245 Variant vat = new Variant();
246 vat.setSpecification(spec);
247 fmz.addNewVariant(vat);
249 intree = DataTypes.xml_of_Formalization(fmz);
250 assertEquals(intree.toString().substring(0,170), intree_cut);
252 System.out.println("\\--END isac.bridge.DataTypes#testEmptyFormalization");
255 public void testTactic() throws Exception {
256 System.out.println(" ---------------------------------------------");
257 System.out.println("/--BEGIN isac.bridge.xml.DataTypes#testTactic");
259 //from java-tests-isacutil.parser.TestTactic
260 //------- Rewrite ----------------------------------------------
261 Tactic tac_built = new Rewrite();
262 tac_built.setName("Rewrite");
263 Theorem thm = new Theorem();
264 thm.setId("pythagoras");
265 Formula form = new Formula();
266 form.setText("[| ?l is_const; ?m is_const |] ==> "
267 + "?l * ?n + ?m * ?n = (?l + ?m) * ?n");
268 form.setText("a^2 + b^2 = c^2");
269 thm.setFormula(form);
270 ((Rewrite) tac_built).setTheorem(thm);
272 System.out.println("tac_built = " + ((Rewrite) tac_built).toSMLString());
273 XML.Tree tac_out = DataTypesCompanion.xml_of_Tactic(tac_built);
274 System.out.println("Tree tac_out = " + tac_out);
275 //<REWRITETACTIC name="Rewrite">
277 // <ID>pythagoras</ID>
278 // <FORMULA>a^2 + b^2 = c^2</FORMULA> !!!different from Parser
281 Tactic tac_in = (Tactic)DataTypes.xml_to_Tactic(tac_out);
282 System.out.println("Tactic tac_in = " + tac_in.toSMLString());
283 assertEquals(tac_built.toSMLString(), tac_in.toSMLString());
284 //from java-tests-isacutil.parser.TestXMLParserDigest
285 @SuppressWarnings("unused") // as data to remember
286 String xmlString = "@@@@@begin@@@@@"// .................................
287 + " 1"// ......................................................
288 + " <GETTACTIC>"// ...........................................
289 + " <CALCID> 1 </CALCID>"// ..................................
290 + " <REWRITETACTIC name=\"Rewrite\">"// .............
291 + " <THEOREM>"// .......................................
292 + " <ID> Belastung_Querkraft </ID>"// ..................
293 + " <FORMULA>"// .........................!!!different from XML
294 + " <MATHML>"// ........................!!!different from XML
295 + " <ISA> - q ?x = Q' ?x </ISA>"// ...!!!different from XML
296 + " </MATHML>"// .......................!!!different from XML
297 + " </FORMULA>"// ........................!!!different from XML
298 + " </THEOREM>"// .......................................
299 + " </REWRITETACTIC>"// ...................................
300 + " </GETTACTIC>" // ........................................
303 //------- RewriteInst ------------------------------------------
305 form.setText("?a = ?a");
306 thm.setFormula(form);
307 ((Rewrite) tac_built).setTheorem(thm);
308 assertEquals("a = a", tac_built.showToBeginner());
311 tac_built = new RewriteInst();
312 form.setText("(?k + ?bdv = ?m) = (?bdv = ?m + -1 * ?k)");
313 thm.setFormula(form);
314 ((RewriteInst) tac_built).setTheorem(thm);
315 assertEquals("(k + bdv = m) = (bdv = m + -1 * k)", tac_built.showToBeginner());
317 //------- RewriteSet -------------------------------------------
319 //from java-tests-isacutil.parser.TestXMLParserDigest
320 xmlString = "@@@@@begin@@@@@"// .................................
321 + " 1"// ......................................................
322 + " <GETTACTIC>"// ...........................................
323 + " <CALCID> 1 </CALCID>"// ..................................
324 + " <REWRITESETTACTIC name= \"Rewrite_Set\">"// .............
325 + " <RULESET> Test_simplify </RULESET>"// ....................
326 + " </REWRITESETTACTIC>"// ...................................
327 + " </GETTACTIC>" // ........................................
331 //------- StringListTactic -------------------------------------
332 Vector<String> keylist = new Vector<>();
333 keylist.add("normalize");
334 keylist.add("polynomial");
335 keylist.add("univariate");
336 keylist.add("equation");
337 tac_built = new StringListTactic("Specify_Problem", keylist);
338 System.out.println(tac_built.toSMLString());
339 assertEquals("Specify_Problem [\"normalize\",\"polynomial\","
340 + "\"univariate\",\"equation\"]", tac_built.toSMLString());
342 System.out.println("\\--END isac.bridge.DataTypes#testTactic");
345 public void testTactics() throws Exception {
346 System.out.println(" ---------------------------------------------");
347 System.out.println("/--BEGIN isac.bridge.xml.DataTypes#testTactics");
349 //from java-tests-isacutil.parser.TestXMLParserDigest
350 @SuppressWarnings("unused") // as data to remember
351 String xmlString = "> @@@@@begin@@@@@" // ...........................
352 + " 1 " // ......................................................
353 + "<APPLICABLETACTICS>" // .......................................
354 + " <CALCID> 1 </CALCID>" // ....................................
355 + " <TACLIST>" // ...............................................
356 + " <REWRITESETTACTIC name=\"Rewrite_Set\">"// .................
357 + " <RULESET> norm_equation </RULESET>"// ....................
358 + " </REWRITESETTACTIC>"// .....................................
359 + " <REWRITESETTACTIC name=\"Rewrite_Set\">"// .................
360 + " <RULESET> Test_simplify </RULESET>"// ....................
361 + " </REWRITESETTACTIC>"// .....................................
362 + " <SUBPROBLEMTACTIC name=\"Subproblem\">"// ..................
363 + " <THEORY> Test.thy </THEORY>"// ...........................
364 + " <PROBLEM>"// .............................................
365 + " <STRINGLIST>"// ........................................
366 + " <STRING> linear </STRING>"// .........................
367 + " <STRING> univariate </STRING>"// .....................
368 + " <STRING> equation </STRING>"// .......................
369 + " <STRING> test </STRING>"// ...........................
370 + " </STRINGLIST>"// .......................................
371 + " </PROBLEM>"// ............................................
372 + " </SUBPROBLEMTACTIC>"// .....................................
373 + " <SIMPLETACTIC name=\"Check_elementwise\">"// ...............
374 + " <MATHML>"// ............................................
375 + " <ISA> Assumptions </ISA>"// ..........................
376 + " </MATHML>"// ...........................................
377 + " </SIMPLETACTIC>"// .........................................
378 + " </TACLIST>"// ................................................
379 + "</APPLICABLETACTICS>"// ........................................
381 // wrapper_ = xml_parser_digest_.parse(xmlString);
382 // tac = (Tactic) ((TacticsContainer) wrapper_.getResponse()).getTactics().elementAt(3);
383 // assertEquals(tac.toSMLString(), "Check_elementwise \"Assumptions\"");
385 System.out.println("\\--END isac.bridge.DataTypes#testTactics");