|
wneuper@4804
|
1 |
/*
|
|
wneuper@4804
|
2 |
* @author Walther Neuper
|
|
wneuper@4804
|
3 |
* Copyright (c) due to license terms
|
|
wneuper@4804
|
4 |
* Created on Aug 28, 2015
|
|
wneuper@4804
|
5 |
* Institute for Softwaretechnology, Graz University of Technology, Austria.
|
|
wneuper@4804
|
6 |
*/
|
|
wneuper@4804
|
7 |
package isac.bridge.xml
|
|
wneuper@4804
|
8 |
|
|
walther@5239
|
9 |
import edu.tum.cs.isabelle.api.XML
|
|
walther@5239
|
10 |
import edu.tum.cs.isabelle.pure._ // DEFINES type Term
|
|
wneuper@4804
|
11 |
|
|
wneuper@4804
|
12 |
/*
|
|
wneuper@4804
|
13 |
* Compile test data for TestDataTypes.java.
|
|
wneuper@4804
|
14 |
*
|
|
wneuper@4804
|
15 |
* This setup has been chosen after <Run As> <Scala JUnit Test> could not
|
|
wneuper@4804
|
16 |
* made working with standard examples neither from within Eclipse
|
|
wneuper@4804
|
17 |
* * http://scala-ide.org/docs/2.0.x/testingframeworks.html
|
|
wneuper@4804
|
18 |
* * http://scala-ide.org/docs/current-user-doc/features/test-finder/index.html
|
|
wneuper@4804
|
19 |
* nor with ScalaTest
|
|
wneuper@4804
|
20 |
* * http://www.scalatest.org/download
|
|
wneuper@4804
|
21 |
* * http://www.scalatest.org/user_guide/using_scalatest_with_eclipse
|
|
wneuper@4804
|
22 |
*/
|
|
wneuper@4804
|
23 |
object TestsDATA {
|
|
wneuper@4804
|
24 |
|
|
wneuper@4804
|
25 |
//---------------------------------- for TestXMLout.java#test_match
|
|
wneuper@4804
|
26 |
def create_AAA (): XML.Tree =
|
|
wneuper@4848
|
27 |
XML.Elem(("AAA", Nil), Nil)
|
|
wneuper@4804
|
28 |
def create_BBB (): XML.Tree =
|
|
wneuper@4848
|
29 |
XML.Elem(("BBB", Nil), Nil)
|
|
wneuper@4804
|
30 |
def create_CCCddd (): XML.Tree =
|
|
wneuper@4848
|
31 |
XML.Elem(("CCC", Nil), List(
|
|
wneuper@4848
|
32 |
XML.Elem(("ddd", Nil), Nil)))
|
|
wneuper@4804
|
33 |
def create_DDDeeeFFF (): XML.Tree =
|
|
wneuper@4848
|
34 |
XML.Elem(("DDD", Nil), List(
|
|
wneuper@4848
|
35 |
XML.Elem(("eee", Nil), List(XML.Text("FFF")))))
|
|
wneuper@4804
|
36 |
def create_EEEfffGGGhhhIII (): XML.Tree =
|
|
wneuper@4848
|
37 |
XML.Elem(("EEE", Nil), List(
|
|
wneuper@4848
|
38 |
XML.Elem(("fff", Nil), List(XML.Text("GGG"))),
|
|
wneuper@4848
|
39 |
XML.Elem(("hhh", Nil), List(XML.Text("III")))))
|
|
wneuper@4804
|
40 |
|
|
wneuper@4804
|
41 |
def match_ABC(t: XML.Tree): java.lang.String = t match {
|
|
wneuper@4804
|
42 |
case
|
|
wneuper@4848
|
43 |
XML.Elem(("AAA", Nil), Nil) => "AAA"
|
|
wneuper@4804
|
44 |
case
|
|
wneuper@4848
|
45 |
XML.Elem(("BBB", Nil), Nil) => "BBB"
|
|
wneuper@4804
|
46 |
case
|
|
wneuper@4848
|
47 |
XML.Elem(("CCC", Nil), List(
|
|
wneuper@4848
|
48 |
XML.Elem(("ddd", Nil), Nil))) => "CCCddd"
|
|
wneuper@4804
|
49 |
case
|
|
wneuper@4848
|
50 |
XML.Elem(("DDD", Nil), List(
|
|
wneuper@4848
|
51 |
XML.Elem(("eee", Nil), List(XML.Text("FFF")))))
|
|
wneuper@4804
|
52 |
=> "DDDeeeFFF"
|
|
wneuper@4804
|
53 |
case
|
|
wneuper@4848
|
54 |
XML.Elem(("EEE", Nil), List(
|
|
wneuper@4848
|
55 |
XML.Elem(("fff", Nil), List(XML.Text("GGG"))),
|
|
wneuper@4848
|
56 |
XML.Elem(("hhh", Nil), List(XML.Text("III")))))
|
|
wneuper@4804
|
57 |
=> "EEEfffGGGhhhIII"
|
|
wneuper@4804
|
58 |
case
|
|
wneuper@4848
|
59 |
XML.Elem(("SYSERROR", Nil), List(
|
|
wneuper@4848
|
60 |
XML.Elem(("CALCID", Nil), List(XML.Text(_))),
|
|
wneuper@4848
|
61 |
XML.Elem(("ERROR", Nil), List(XML.Text(_)))))
|
|
wneuper@4804
|
62 |
=> "SYSERROR"
|
|
wneuper@4804
|
63 |
case _ => "no match"
|
|
wneuper@4804
|
64 |
}
|
|
wneuper@4804
|
65 |
|
|
wneuper@4804
|
66 |
//---------------------------------- for TestXMLout.java#test_is_message
|
|
wneuper@4804
|
67 |
def create_SYSERROR (): XML.Tree =
|
|
wneuper@4848
|
68 |
XML.Elem(("SYSERROR", Nil), List(
|
|
wneuper@4848
|
69 |
XML.Elem(("CALCID", Nil), List(XML.Text("1"))),
|
|
wneuper@4848
|
70 |
XML.Elem(("ERROR", Nil), List(XML.Text("no Rewrite_Set...")))))
|
|
wneuper@4804
|
71 |
/*
|
|
wneuper@4804
|
72 |
* intermediateSteps xml_out = <SYSERROR><CALCID>1</CALCID><ERROR>no Rewrite_Set...</ERROR></SYSERROR>
|
|
wneuper@4804
|
73 |
*/
|
|
wneuper@4804
|
74 |
|
|
wneuper@4851
|
75 |
|
|
wneuper@4851
|
76 |
//---------------------------------- for ../TestPIDE.java#testTermTransfer
|
|
wneuper@4851
|
77 |
//----- see Isabelle_Isac/test/../mathml.sml--- create testdata for TestPIDE.java#testTermTransfer ---
|
|
wneuper@4851
|
78 |
// https://intra.ist.tugraz.at/hg/isa/rev/5ce72a592f7f
|
|
wneuper@4851
|
79 |
// val t = @{term "aaa + bbb::real"}
|
|
wneuper@4851
|
80 |
// ... gives in SML:
|
|
wneuper@4851
|
81 |
// ( ( Const ("Groups.plus_class.plus", "real ⇒ real ⇒ real") $ Free ("aaa", "real") ) $ Free ("bbb", "real") )
|
|
wneuper@4851
|
82 |
// ... gives in SML with left-associativity:
|
|
wneuper@4851
|
83 |
// val
|
|
wneuper@4851
|
84 |
// (*App*) (
|
|
wneuper@4851
|
85 |
// (*App*) (
|
|
wneuper@4851
|
86 |
// Const ("Groups.plus_class.plus", _) $
|
|
wneuper@4851
|
87 |
// Free ("aaa", _) ) $
|
|
wneuper@4851
|
88 |
// Free ("bbb", _) ) = t
|
|
wneuper@4851
|
89 |
// ... gives in SML with explicit typ:
|
|
wneuper@4851
|
90 |
// (*App*) (
|
|
wneuper@4851
|
91 |
// (*App*) (
|
|
wneuper@4851
|
92 |
// Const ("Groups.plus_class.plus", Type ("fun", [
|
|
wneuper@4851
|
93 |
// Type ("Real.real", []),
|
|
wneuper@4851
|
94 |
// Type ("fun", [
|
|
wneuper@4851
|
95 |
// Type ("Real.real", []),
|
|
wneuper@4851
|
96 |
// Type ("Real.real", [])])])) $
|
|
wneuper@4851
|
97 |
// Free ("aaa", Type ("Real.real", [])) ) $
|
|
wneuper@4851
|
98 |
// Free ("bbb", Type ("Real.real", [])) )
|
|
wneuper@4851
|
99 |
def test_term (): Term =
|
|
wneuper@4851
|
100 |
App(
|
|
wneuper@4851
|
101 |
App(
|
|
wneuper@4851
|
102 |
Const ("Groups.plus_class.plus", Type("fun", List(
|
|
wneuper@4851
|
103 |
Type("Real.real", List()),
|
|
wneuper@4851
|
104 |
Type("fun", List(
|
|
wneuper@4851
|
105 |
Type("Real.real", List()),
|
|
wneuper@4851
|
106 |
Type("Real.real", List())))))),
|
|
wneuper@4851
|
107 |
Free ("aaa", Type ("Real.real", List()))),
|
|
wneuper@4851
|
108 |
Free ("bbb", Type ("Real.real", List())))
|
|
wneuper@4851
|
109 |
|
|
wneuper@4928
|
110 |
/*
|
|
wneuper@4928
|
111 |
* "solve (x + 1 = (2::real), (x::real))" parsed via <code>ScalaTermFromString</code> to
|
|
wneuper@4928
|
112 |
* App(Const("Equation.solve",Type("fun",List(Type("Product_Type.prod",List(Type("HOL.bool",List()), Type("Real.real",List()))), Type(List.list,List(Type("HOL.bool",List())))))),App(App(Const("Product_Type.Pair",Type("fun",List(Type("HOL.bool",List()), Type("fun",List(Type("Real.real",List()), Type("Product_Type.prod",List(Type("HOL.bool",List()), Type("Real.real",List())))))))),App(App(Const("HOL.eq",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("HOL.bool",List())))))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("x",Type("Real.real",List()))),Free("1",Type("Real.real",List())))),Free("2",Type(Real.real,List())))),Free("x",Type("Real.real",List()))))
|
|
wneuper@4928
|
113 |
*/
|
|
wneuper@4928
|
114 |
def term_mini_subpbl_1 (): Term = {
|
|
wneuper@4928
|
115 |
App(Const("Equation.solve",Type("fun",List(Type("Product_Type.prod",List(Type("HOL.bool",List()), Type("Real.real",List()))), Type("List.list",List(Type("HOL.bool",List())))))),App(App(Const("Product_Type.Pair",Type("fun",List(Type("HOL.bool",List()), Type("fun",List(Type("Real.real",List()), Type("Product_Type.prod",List(Type("HOL.bool",List()), Type("Real.real",List())))))))),App(App(Const("HOL.eq",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("HOL.bool",List())))))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("x",Type("Real.real",List()))),Free("1",Type("Real.real",List())))),Free("2",Type("Real.real",List())))),Free("x",Type("Real.real",List()))))
|
|
wneuper@4928
|
116 |
}
|
|
walther@5239
|
117 |
}
|