16 import isac.util.formulae.Model; |
16 import isac.util.formulae.Model; |
17 import isac.util.formulae.ModelItem; |
17 import isac.util.formulae.ModelItem; |
18 import isac.util.formulae.Position; |
18 import isac.util.formulae.Position; |
19 import isac.util.formulae.Specification; |
19 import isac.util.formulae.Specification; |
20 import isac.util.Formalization; |
20 import isac.util.Formalization; |
21 import info.hupel.isabelle.api.*; |
21 |
22 import info.hupel.isabelle.japi.*; |
22 import edu.tum.cs.isabelle.api.*; |
23 //import info.hupel.isabelle.*; // OVERWRITES System.out.println |
23 import edu.tum.cs.isabelle.japi.*; |
24 import info.hupel.isabelle.pure.*; // DEFINES type Term |
24 //import edu.tum.cs.isabelle.*; // OVERWRITES System.out.println |
25 import info.hupel.isabelle.setup.Setup; |
25 import edu.tum.cs.isabelle.pure.*; // DEFINES type Term |
|
26 import edu.tum.cs.isabelle.setup.Setup; |
26 |
27 |
27 import java.io.FileNotFoundException; |
28 import java.io.FileNotFoundException; |
28 import java.io.IOException; |
29 import java.io.IOException; |
29 import java.io.InputStream; |
30 import java.io.InputStream; |
30 import java.nio.file.Paths; |
31 import java.nio.file.Paths; |
64 */ |
65 */ |
65 public void testConnection() { |
66 public void testConnection() { |
66 System.out.println("/--BEGIN isac.bridge.TestPIDE#testConnection"); |
67 System.out.println("/--BEGIN isac.bridge.TestPIDE#testConnection"); |
67 |
68 |
68 System.out.println("---1 isac.bridge.TestPIDE#testConnection"); |
69 System.out.println("---1 isac.bridge.TestPIDE#testConnection"); |
69 JResources res = JResources.dumpIsabelleResources(); |
70 Setup setup = new Setup(Paths.get(isabelle_home_), JPlatform.guess(), |
70 Configuration config = Configuration.fromBuiltin("libisabelle_Isac"); |
71 new Version("2015"), Setup.defaultPackageName()); |
71 Environment env = JSetup.makeEnvironment(JSetup.defaultSetup(new Version.Stable("2018")), res); |
72 Environment env = JSetup.makeEnvironment(setup); // ohne Duration |
72 JSystem sys = JSystem.create(env, config); |
73 |
73 |
74 System.out.println("---2 isac.bridge.TestPIDE#testConnection"); |
|
75 /*Error*/Configuration config = Configuration.fromBuiltin("libisabelle_Isac"); |
|
76 JSystem sys = JSystem.create(env, config); |
|
77 |
74 System.out.println("---3 isac.bridge.TestPIDE#testConnection"); |
78 System.out.println("---3 isac.bridge.TestPIDE#testConnection"); |
75 String hello_out = sys.invoke(Operations.HELLO, "should-be-returned"); |
79 String hello_out = sys.invoke(Operations.HELLO, "should-be-returned"); |
76 |
80 |
77 System.out.println("---4 isac.bridge.TestPIDE#testConnection"); |
81 System.out.println("---4 isac.bridge.TestPIDE#testConnection"); |
78 assertEquals(hello_out,"Hello should-be-returned"); |
82 assertEquals(hello_out,"Hello should-be-returned"); |
90 * https://github.com/wneuper/libisabelle/blob/master/doc/test--isac-Java--isac-kernel.txt |
94 * https://github.com/wneuper/libisabelle/blob/master/doc/test--isac-Java--isac-kernel.txt |
91 */ |
95 */ |
92 public void testMini_Test() { |
96 public void testMini_Test() { |
93 System.out.println("/--BEGIN isac.bridge.TestPIDE#testMini_Test"); |
97 System.out.println("/--BEGIN isac.bridge.TestPIDE#testMini_Test"); |
94 |
98 |
95 JResources res = JResources.dumpIsabelleResources(); |
99 Setup setup = new Setup(Paths.get(isabelle_home_), JPlatform.guess(), |
96 Configuration config = Configuration.fromBuiltin("libisabelle_Isac"); |
100 new Version("2015"), Setup.defaultPackageName()); |
97 Environment env = JSetup.makeEnvironment(JSetup.defaultSetup(new Version.Stable("2018")), res); |
101 Environment env = JSetup.makeEnvironment(setup); // ohne Duration |
98 JSystem sys = JSystem.create(env, config); |
102 Configuration config = Configuration.fromBuiltin("libisabelle_Isac"); |
|
103 JSystem sys = JSystem.create(env, config); |
99 |
104 |
100 //----- step 1 ---------------------------------------------------------------- |
105 //----- step 1 ---------------------------------------------------------------- |
101 //build Formalization in Java and then convert to XML |
106 //build Formalization in Java and then convert to XML |
102 Formalization fmz = isac.TESTUTIL.Formalization.solve_x_plus_1_equ_2(); |
107 Formalization fmz = isac.TESTUTIL.Formalization.solve_x_plus_1_equ_2(); |
103 XML.Tree CALC_TREE_out = sys.invoke(IsacOperations.CALC_TREE, |
108 XML.Tree CALC_TREE_out = sys.invoke(IsacOperations.CALC_TREE, |
221 * Terms isac-java --> Isabelle/Isac are mostly input by user, |
226 * Terms isac-java --> Isabelle/Isac are mostly input by user, |
222 * thus may contain different kinds of errors; |
227 * thus may contain different kinds of errors; |
223 * their format is still to be determined (String ?). |
228 * their format is still to be determined (String ?). |
224 * |
229 * |
225 * Terms isac-java <-- Isabelle/Isac the other way round pack two formats, |
230 * Terms isac-java <-- Isabelle/Isac the other way round pack two formats, |
226 * info.hupel.isabelle.pure.Term and String. |
231 * edu.tum.cs.isabelle.pure.Term and String. |
227 */ |
232 */ |
228 public void testTermTransfer() { |
233 public void testTermTransfer() { |
229 System.out.println("/--BEGIN isac.bridge.TestPIDE#testTermTransfer"); |
234 System.out.println("/--BEGIN isac.bridge.TestPIDE#testTermTransfer"); |
230 |
235 |
231 JResources res = JResources.dumpIsabelleResources(); |
236 Setup setup = new Setup(Paths.get(isabelle_home_), JPlatform.guess(), |
232 Configuration config = Configuration.fromBuiltin("libisabelle_Isac"); |
237 new Version("2015"), Setup.defaultPackageName()); |
233 Environment env = JSetup.makeEnvironment(JSetup.defaultSetup(new Version.Stable("2018")), res); |
238 Environment env = JSetup.makeEnvironment(setup); // ohne Duration |
234 JSystem sys = JSystem.create(env, config); |
239 Configuration config = Configuration.fromBuiltin("libisabelle_Isac"); |
|
240 JSystem sys = JSystem.create(env, config); |
235 |
241 |
236 //----- create test_term ------------------------------------------------------ |
242 //----- create test_term ------------------------------------------------------ |
237 Term test_term = TestsDATA.test_term(); |
243 Term test_term = TestsDATA.test_term(); |
238 XML.Tree wrapped_term = DataTypes.xml_of_Term(test_term); |
244 XML.Tree wrapped_term = DataTypes.xml_of_Term(test_term); |
239 |
245 |
253 * |
259 * |
254 * Terms isac-java --> Isabelle/Isac are mostly input by user, |
260 * Terms isac-java --> Isabelle/Isac are mostly input by user, |
255 * their format is String most likely during the next phase of devel. |
261 * their format is String most likely during the next phase of devel. |
256 * |
262 * |
257 * Terms isac-java <-- Isabelle/Isac the other way round pack two formats, |
263 * Terms isac-java <-- Isabelle/Isac the other way round pack two formats, |
258 * info.hupel.isabelle.pure.Term and String. |
264 * edu.tum.cs.isabelle.pure.Term and String. |
259 */ |
265 */ |
260 public void testTermOneWay() { |
266 public void testTermOneWay() { |
261 System.out.println("/--BEGIN isac.bridge.TestPIDE#testTermOneWay"); |
267 System.out.println("/--BEGIN isac.bridge.TestPIDE#testTermOneWay"); |
262 |
268 |
263 JResources res = JResources.dumpIsabelleResources(); |
269 Setup setup = new Setup(Paths.get(isabelle_home_), JPlatform.guess(), |
264 Configuration config = Configuration.fromBuiltin("libisabelle_Isac"); |
270 new Version("2015"), Setup.defaultPackageName()); |
265 Environment env = JSetup.makeEnvironment(JSetup.defaultSetup(new Version.Stable("2018")), res); |
271 Environment env = JSetup.makeEnvironment(setup); // ohne Duration |
266 JSystem sys = JSystem.create(env, config); |
272 Configuration config = Configuration.fromBuiltin("libisabelle_Isac"); |
|
273 JSystem sys = JSystem.create(env, config); |
267 |
274 |
268 //----- create test_term ------------------------------------------------------ |
275 //----- create test_term ------------------------------------------------------ |
269 String term_str = "aaa + bbb::real"; |
276 String term_str = "aaa + bbb::real"; |
270 |
277 |
271 //----- transfer test_term to Isabelle/Isac and back again -------------------- |
278 //----- transfer test_term to Isabelle/Isac and back again -------------------- |