3 import isac.util.formulae.Position;
4 import examples.src.main.java.ConvertXML;
5 import examples.src.main.java.IntIntCompound;
6 import examples.src.main.java.IntPosCompound;
7 import examples.src.main.java.IntCalcChangedCompound;
8 import examples.src.main.java.IntCalcFormCompound;
10 import edu.tum.cs.isabelle.japi.JSystem;
11 import edu.tum.cs.isabelle.japi.Operations;
15 import java.math.BigInteger;
16 import java.util.ArrayList;
17 import java.util.Vector;
18 import junit.framework.TestCase;
19 import org.junit.Test;
21 import static org.junit.Assert.*;
23 public class TestPIDE extends TestCase {
26 * NOTE: libisabelle.JSystem requires ISABELLE_HOME set,
27 * which is not yet done (waiting for a better solution in libisabelle).
28 * You can run this changeset within Eclipse if you outcomment all / *DEBUG* / --> // *DEBUG* /
29 * (spaces between "/" and "*" for not confusing the Java compiler)
31 public void testConnection() {
32 System.out.println("/--BEGIN isac.bridge.TestPIDE#testConnection");
34 System.out.println("---1 isac.bridge.TestPIDE#testConnection");
35 isabelle.Isabelle_System.init("/usr/local/isabisac", "");
36 JSystem sys = JSystem.instance(new File("/home/wneuper/proto4/libisabelle/."), "Protocol");
38 System.out.println("---2 isac.bridge.TestPIDE#testConnection");
39 String hello_out = sys.invoke(Operations.HELLO, "should-be-returned");
41 System.out.println("---3 isac.bridge.TestPIDE#testConnection");
42 assertEquals(hello_out,"Hello should-be-returned");
44 System.out.println("\\--END isac.bridge.TestPIDE#testConnection");
48 * transfer the minimal test from libisabelle to isac-java:
49 * https://github.com/wneuper/libisabelle/blob/master/examples/src/main/java/Mini_Test.java
50 * which has been derived from:
51 * https://github.com/wneuper/libisabelle/blob/master/doc/test--isac-Java--isac-kernel.txt
53 public void testMini_Test() {
54 System.out.println("/--BEGIN isac.bridge.TestPIDE#testMini_Test");
56 isabelle.Isabelle_System.init("/usr/local/isabisac", "");
57 JSystem sys = JSystem.instance(new File("/home/wneuper/proto4/libisabelle/."), "Protocol");
59 //----- step 1 ----------------------------------------------------------------
60 //List items = list("equality (x+1=(2::real))", "solveFor x", "solutions L");
61 ArrayList<String> items = new ArrayList<>();
62 items.add("equality (x+1=(2::real))");
63 items.add("solveFor x");
64 items.add("solutions L");
65 //List pbl = list("sqroot-test","univariate","equation","test");
66 ArrayList<String> pbl = new ArrayList<>();
67 pbl.add("sqroot-test");
68 pbl.add("univariate");
71 //List met = list("Test","squ-equ-test-subpbl1");
72 ArrayList<String> met = new ArrayList<>();
74 met.add("squ-equ-test-subpbl1");
75 XML.Tree CALC_TREE_out = sys.invoke(Operations.CALC_TREE,
76 ConvertXML.calc_tree(items, "Test", pbl, met));
77 int calcid = (ConvertXML.calc_tree_out(CALC_TREE_out)).intValue();
78 assertEquals(calcid, 1);
79 System.out.println("# 1 # " + CALC_TREE_out);
81 //----- step 2 ----------------------------------------------------------------
82 XML.Tree ITERATOR_out = sys.invoke(Operations.ITERATOR,
83 new scala.math.BigInt(BigInteger.valueOf(calcid)));
84 IntIntCompound int_int = ConvertXML.iterator_out(ITERATOR_out);
85 calcid = int_int.get_calcid().intValue();
86 int userid = int_int.get_userid().intValue();
87 assertEquals(calcid, 1);
88 assertEquals(userid, 1);
89 System.out.println("# 2 # " + ITERATOR_out);
91 //----- step 3 ----------------------------------------------------------------
92 XML.Tree MOVE_ACTIVE_ROOT_out = sys.invoke(Operations.MOVE_ACTIVE_ROOT,
93 new scala.math.BigInt(BigInteger.valueOf(calcid)));
94 IntPosCompound calcid_pos = ConvertXML.move_active_root_out(MOVE_ACTIVE_ROOT_out);
95 calcid = calcid_pos.get_calcid();
96 Vector<Integer> ints = calcid_pos.get_ints();
97 String kind = calcid_pos.get_kind();
98 Position pos = new Position(ints, kind);
99 assertEquals(pos.toSMLString(), "([],Pbl)");
100 System.out.println("# 3 # " + MOVE_ACTIVE_ROOT_out);
102 //----- step 4 ----------------------------------------------------------------
103 Vector<Integer> from_path = new Vector<>();
104 String from_kind = "Pbl";
105 Vector<Integer> to_path = new Vector<>();
106 String to_kind = "Pbl";
108 XML.Tree GET_FORMULAE_out = sys.invoke(Operations.GET_FORMULAE,
109 ConvertXML.get_formulae(new scala.math.BigInt(BigInteger.valueOf(calcid)),
110 from_path, from_kind, to_path, to_kind, new scala.math.BigInt(BigInteger.valueOf(level)), "false"));
111 //IntFormulaCompound ..POSTPONED TO shift ConvertXML into isac-java
112 System.out.println("# 4 # " + GET_FORMULAE_out);
114 //----- step 6 ----------------------------------------------------------------
115 Vector<Integer> pos_path = new Vector<>();
116 String pos_kind = "Pbl";
117 XML.Tree REF_FORMULA_out = sys.invoke(Operations.REF_FORMULA,
118 ConvertXML.ref_formula(new scala.math.BigInt(BigInteger.valueOf(calcid)), pos_path, pos_kind));
119 //^^^^^^^^^^ cumbersome without import CalcHead .. Model .. ModelItemList
120 System.out.println("# 6 # " + REF_FORMULA_out);
122 //----- step 7 ----------------------------------------------------------------
123 String auto = "CompleteCalc";
124 XML.Tree AUTO_CALC_out = sys.invoke(Operations.AUTO_CALC,
125 ConvertXML.auto_calculate(new scala.math.BigInt(BigInteger.valueOf(calcid)), auto));
126 IntCalcChangedCompound calcid_cc = ConvertXML.auto_calc_out(AUTO_CALC_out);
127 Vector<Integer> unc_ints = calcid_cc.get_unc_ints();
128 String unc_kind = calcid_cc.get_unc_kind();
129 //...del, gen are analogous
130 Position unc = new Position(unc_ints, unc_kind);
131 assertEquals(unc.toSMLString(), "([],Pbl)");
132 System.out.println("# 7 # " + AUTO_CALC_out);
134 //----- step 10 ---------------------------------------------------------------
135 pos_path = new Vector<>();
137 REF_FORMULA_out = sys.invoke(Operations.REF_FORMULA,
138 ConvertXML.ref_formula(new scala.math.BigInt(BigInteger.valueOf(calcid)), pos_path, pos_kind));
139 Object calcid_formhead = ConvertXML.ref_formula_out(REF_FORMULA_out);
140 // calcid = calcid_formhead.get_calcid().intValue();
141 //if (calcid_formhead.is_calchead()) {
142 // IntCalcHeadCompound calc_head = (IntCalcHeadCompound) calcid_formhead;
145 IntCalcFormCompound calc_form = (IntCalcFormCompound) calcid_formhead;
146 Vector<Integer> form_ints = calc_form.get_form_ints();
147 String form_kind = calc_form.get_form_kind();
148 String form_isa = calc_form.get_form_isa();
150 Position form_pos = new Position(form_ints, form_kind);
151 System.out.println(unc.toSMLString());
152 assertEquals(form_pos.toSMLString(), "([],Res)");
153 assertEquals(form_isa, "[x = 1]");
154 System.out.println("# 10 # " + REF_FORMULA_out);
156 //----- step 13 ---------------------------------------------------------------
157 XML.Tree DEL_CALC_out = sys.invoke(Operations.DEL_CALC,
158 new scala.math.BigInt(BigInteger.valueOf(calcid)));
159 calcid = ConvertXML.del_calc_out(DEL_CALC_out).intValue();
160 assertEquals(calcid, 1);
161 System.out.println("# 13 # " + DEL_CALC_out);
165 System.out.println("\\--END isac.bridge.TestPIDE##testMini_Test");