|
wneuper@4733
|
1 |
/*
|
|
wneuper@4733
|
2 |
* @author Walther Neuper
|
|
wneuper@4733
|
3 |
* Copyright (c) due to license terms
|
|
wneuper@4733
|
4 |
* Created on Jul 14, 2015
|
|
wneuper@4733
|
5 |
* Institute for Softwaretechnology, Graz University of Technology, Austria.
|
|
wneuper@4733
|
6 |
*/
|
|
wneuper@4733
|
7 |
package isac.bridge.xml
|
|
wneuper@4733
|
8 |
|
|
wneuper@4733
|
9 |
import isac.util.formulae.ModelItem
|
|
wneuper@4928
|
10 |
import isac.gui.mawen.scalaterm.Util
|
|
wneuper@4733
|
11 |
|
|
walther@5239
|
12 |
import edu.tum.cs.isabelle._ // for Codec
|
|
walther@5239
|
13 |
import edu.tum.cs.isabelle.api.XML
|
|
walther@5239
|
14 |
import edu.tum.cs.isabelle.pure._ // DEFINES type Term
|
|
wneuper@4733
|
15 |
|
|
wneuper@4733
|
16 |
import java.util.Vector
|
|
wneuper@4733
|
17 |
import scala.collection.JavaConverters._
|
|
wneuper@4733
|
18 |
import scala.collection.JavaConversions._
|
|
wneuper@4733
|
19 |
|
|
wneuper@4733
|
20 |
/*
|
|
wneuper@4733
|
21 |
* Compile test data for TestDataTypes.java.
|
|
wneuper@4733
|
22 |
*
|
|
wneuper@4733
|
23 |
* This setup has been chosen after <Run As> <Scala JUnit Test> could not
|
|
wneuper@4733
|
24 |
* made working with standard examples neither from within Eclipse
|
|
wneuper@4733
|
25 |
* * http://scala-ide.org/docs/2.0.x/testingframeworks.html
|
|
wneuper@4733
|
26 |
* * http://scala-ide.org/docs/current-user-doc/features/test-finder/index.html
|
|
wneuper@4733
|
27 |
* nor with ScalaTest
|
|
wneuper@4733
|
28 |
* * http://www.scalatest.org/download
|
|
wneuper@4733
|
29 |
* * http://www.scalatest.org/user_guide/using_scalatest_with_eclipse
|
|
wneuper@4733
|
30 |
*/
|
|
wneuper@4733
|
31 |
object TestDataTypesDATA {
|
|
wneuper@4733
|
32 |
|
|
wneuper@4733
|
33 |
//---------------------------------- for TestDataTypes.java#testCalcHead
|
|
wneuper@4733
|
34 |
def create_REF_FORMULA_out (): XML.Tree = {
|
|
wneuper@4733
|
35 |
val REF_FORMULA_out =
|
|
wneuper@4848
|
36 |
XML.Elem(("REFFORMULA", Nil), List(
|
|
wneuper@4848
|
37 |
XML.Elem(("CALCID", Nil), List(XML.Text ("1"))),
|
|
wneuper@4848
|
38 |
XML.Elem(("CALCHEAD", List(("status", "incorrect"))), List(
|
|
wneuper@4848
|
39 |
XML.Elem(("POSITION", Nil), List(
|
|
wneuper@4848
|
40 |
XML.Elem(("INTLIST", Nil), Nil),
|
|
wneuper@4848
|
41 |
XML.Elem(("POS", Nil), List(XML.Text("Pbl"))))),
|
|
wneuper@4848
|
42 |
XML.Elem(("HEAD", Nil), List(
|
|
wneuper@4928
|
43 |
XML.Elem(("FORMULA", Nil), List(
|
|
wneuper@4928
|
44 |
XML.Elem(("ISA", Nil), List(XML.Text("solve (x + 1 = 2, x)"))),
|
|
wneuper@4928
|
45 |
XML.Elem(("TERM", Nil), List(Codec[Term].encode(TestsDATA.term_mini_subpbl_1())) ))) )),
|
|
wneuper@4848
|
46 |
XML.Elem(("MODEL", Nil), List(
|
|
wneuper@4848
|
47 |
XML.Elem(("GIVEN", Nil), Nil),
|
|
wneuper@4848
|
48 |
XML.Elem(("WHERE", Nil), List(
|
|
wneuper@4848
|
49 |
XML.Elem(("ITEM", List(("status", "false"))), List(
|
|
wneuper@4848
|
50 |
XML.Elem(("MATHML", Nil), List(
|
|
wneuper@4848
|
51 |
XML.Elem(("ISA", Nil), List(XML.Text("precond_rootpbl v_v"))))))))),
|
|
wneuper@4848
|
52 |
XML.Elem(("FIND", Nil), Nil),
|
|
wneuper@4848
|
53 |
XML.Elem(("RELATE", Nil), Nil))),
|
|
wneuper@4848
|
54 |
XML.Elem(("BELONGSTO", Nil), List(XML.Text("Pbl"))),
|
|
wneuper@4848
|
55 |
XML.Elem(("SPECIFICATION", Nil), List(
|
|
wneuper@4848
|
56 |
XML.Elem(("THEORYID", Nil), List(XML.Text("e_domID"))),
|
|
wneuper@4848
|
57 |
XML.Elem(("PROBLEMID", Nil), List(
|
|
wneuper@4848
|
58 |
XML.Elem(("STRINGLIST", Nil), List(
|
|
wneuper@4848
|
59 |
XML.Elem(("STRING", Nil), List(XML.Text("e_pblID"))))))),
|
|
wneuper@4848
|
60 |
XML.Elem(("METHODID", Nil), List(
|
|
wneuper@4848
|
61 |
XML.Elem(("STRINGLIST", Nil), List(
|
|
wneuper@4848
|
62 |
XML.Elem(("STRING", Nil), List(XML.Text("e_metID")))))))))))));
|
|
wneuper@4733
|
63 |
REF_FORMULA_out
|
|
wneuper@4733
|
64 |
}
|
|
wneuper@4733
|
65 |
def create_xml_model (REF_FORMULA_out: XML.Tree): XML.Tree = REF_FORMULA_out match {
|
|
wneuper@4733
|
66 |
case
|
|
wneuper@4848
|
67 |
XML.Elem(("REFFORMULA", Nil), List(
|
|
wneuper@4848
|
68 |
XML.Elem(("CALCID", Nil), List(XML.Text ("1"))),
|
|
wneuper@4848
|
69 |
XML.Elem(("CALCHEAD", List(("status", "incorrect"))), List(
|
|
wneuper@4848
|
70 |
XML.Elem(("POSITION", Nil), List(
|
|
wneuper@4848
|
71 |
XML.Elem(("INTLIST", Nil), Nil),
|
|
wneuper@4848
|
72 |
XML.Elem(("POS", Nil), List(XML.Text("Pbl"))))),
|
|
wneuper@4848
|
73 |
XML.Elem(("HEAD", Nil), List(
|
|
wneuper@4928
|
74 |
XML.Elem(("FORMULA", Nil), List(
|
|
wneuper@4928
|
75 |
XML.Elem(("ISA", Nil), List(XML.Text("solve (x + 1 = 2, x)"))),
|
|
wneuper@4928
|
76 |
XML.Elem(("TERM", Nil), _ ))) )),
|
|
wneuper@4733
|
77 |
xml_model,
|
|
wneuper@4848
|
78 |
XML.Elem(("BELONGSTO", Nil), List(XML.Text("Pbl"))),
|
|
wneuper@4848
|
79 |
XML.Elem(("SPECIFICATION", Nil), List(
|
|
wneuper@4848
|
80 |
XML.Elem(("THEORYID", Nil), List(XML.Text("e_domID"))),
|
|
wneuper@4848
|
81 |
XML.Elem(("PROBLEMID", Nil), List(
|
|
wneuper@4848
|
82 |
XML.Elem(("STRINGLIST", Nil), List(
|
|
wneuper@4848
|
83 |
XML.Elem(("STRING", Nil), List(XML.Text("e_pblID"))))))),
|
|
wneuper@4848
|
84 |
XML.Elem(("METHODID", Nil), List(
|
|
wneuper@4848
|
85 |
XML.Elem(("STRINGLIST", Nil), List(
|
|
wneuper@4848
|
86 |
XML.Elem(("STRING", Nil), List(XML.Text("e_metID")))))))))))))
|
|
wneuper@4733
|
87 |
=> xml_model
|
|
wneuper@4733
|
88 |
case _ => throw new IllegalArgumentException("create_xml_model exn")
|
|
wneuper@4733
|
89 |
}
|
|
wneuper@4734
|
90 |
def create_xml_given (xml_model: XML.Tree): XML.Tree = xml_model match {
|
|
wneuper@4733
|
91 |
case
|
|
wneuper@4848
|
92 |
XML.Elem(("MODEL", Nil), List(
|
|
wneuper@4734
|
93 |
xml_given,
|
|
wneuper@4848
|
94 |
XML.Elem(("WHERE", Nil), List(
|
|
wneuper@4848
|
95 |
XML.Elem(("ITEM", List(("status", "false"))), List(
|
|
wneuper@4848
|
96 |
XML.Elem(("MATHML", Nil), List(
|
|
wneuper@4848
|
97 |
XML.Elem(("ISA", Nil), List(XML.Text("precond_rootpbl v_v"))))))))),
|
|
wneuper@4848
|
98 |
XML.Elem(("FIND", Nil), Nil),
|
|
wneuper@4848
|
99 |
XML.Elem(("RELATE", Nil), Nil)))
|
|
wneuper@4733
|
100 |
=> xml_given
|
|
wneuper@4733
|
101 |
case _ => throw new IllegalArgumentException("create_xml_given exn")
|
|
wneuper@4733
|
102 |
}
|
|
wneuper@4734
|
103 |
def create_xml_where (xml_model: XML.Tree): XML.Tree = xml_model match {
|
|
wneuper@4733
|
104 |
case
|
|
wneuper@4848
|
105 |
XML.Elem(("MODEL", Nil), List(
|
|
wneuper@4848
|
106 |
XML.Elem(("GIVEN", Nil), Nil),
|
|
wneuper@4734
|
107 |
xml_where,
|
|
wneuper@4848
|
108 |
XML.Elem(("FIND", Nil), Nil),
|
|
wneuper@4848
|
109 |
XML.Elem(("RELATE", Nil), Nil)))
|
|
wneuper@4733
|
110 |
=> xml_where
|
|
wneuper@4733
|
111 |
case _ => throw new IllegalArgumentException("create_xml_where exn")
|
|
wneuper@4733
|
112 |
}
|
|
wneuper@4734
|
113 |
def create_xml_find (xml_model: XML.Tree): XML.Tree = xml_model match {
|
|
wneuper@4734
|
114 |
case
|
|
wneuper@4848
|
115 |
XML.Elem(("MODEL", Nil), List(
|
|
wneuper@4848
|
116 |
XML.Elem(("GIVEN", Nil), Nil),
|
|
wneuper@4848
|
117 |
XML.Elem(("WHERE", Nil), List(
|
|
wneuper@4848
|
118 |
XML.Elem(("ITEM", List(("status", "false"))), List(
|
|
wneuper@4848
|
119 |
XML.Elem(("MATHML", Nil), List(
|
|
wneuper@4848
|
120 |
XML.Elem(("ISA", Nil), List(XML.Text("precond_rootpbl v_v"))))))))),
|
|
wneuper@4734
|
121 |
xml_find,
|
|
wneuper@4848
|
122 |
XML.Elem(("RELATE", Nil), Nil)))
|
|
wneuper@4734
|
123 |
=> xml_find
|
|
wneuper@4734
|
124 |
case _ => throw new IllegalArgumentException("create_xml_find exn")
|
|
wneuper@4734
|
125 |
}
|
|
wneuper@4734
|
126 |
def create_xml_relate (xml_model: XML.Tree): XML.Tree = xml_model match {
|
|
wneuper@4734
|
127 |
case
|
|
wneuper@4848
|
128 |
XML.Elem(("MODEL", Nil), List(
|
|
wneuper@4848
|
129 |
XML.Elem(("GIVEN", Nil), Nil),
|
|
wneuper@4848
|
130 |
XML.Elem(("WHERE", Nil), List(
|
|
wneuper@4848
|
131 |
XML.Elem(("ITEM", List(("status", "false"))), List(
|
|
wneuper@4848
|
132 |
XML.Elem(("MATHML", Nil), List(
|
|
wneuper@4848
|
133 |
XML.Elem(("ISA", Nil), List(XML.Text("precond_rootpbl v_v"))))))))),
|
|
wneuper@4848
|
134 |
XML.Elem(("FIND", Nil), Nil),
|
|
wneuper@4734
|
135 |
xml_relate))
|
|
wneuper@4734
|
136 |
=> xml_relate
|
|
wneuper@4734
|
137 |
case _ => throw new IllegalArgumentException("create_xml_relate exn")
|
|
wneuper@4734
|
138 |
}
|
|
wneuper@4733
|
139 |
def create_xml_item (): XML.Tree = {
|
|
wneuper@4848
|
140 |
XML.Elem(("ITEM", List(("status", "false"))), List(
|
|
wneuper@4848
|
141 |
XML.Elem(("MATHML", Nil), List(
|
|
wneuper@4848
|
142 |
XML.Elem(("ISA", Nil), List(XML.Text("precond_rootpbl v_v")))))))
|
|
wneuper@4733
|
143 |
}
|
|
wneuper@4733
|
144 |
def jVector2sList(ivect: Vector[ModelItem]): List[ModelItem] = {
|
|
wneuper@4733
|
145 |
ivect.asScala.toList
|
|
wneuper@4733
|
146 |
}
|
|
wneuper@4735
|
147 |
def create_xml_calchead (REF_FORMULA_out: XML.Tree): XML.Tree = REF_FORMULA_out match {
|
|
wneuper@4735
|
148 |
case
|
|
wneuper@4848
|
149 |
XML.Elem(("REFFORMULA", Nil), List(
|
|
wneuper@4848
|
150 |
XML.Elem(("CALCID", Nil), List(XML.Text ("1"))),
|
|
wneuper@4735
|
151 |
xml_calchead)) => xml_calchead
|
|
wneuper@4735
|
152 |
case _ => throw new IllegalArgumentException("create_xml_calchead exn")
|
|
wneuper@4735
|
153 |
}
|
|
wneuper@4736
|
154 |
def create_xml_spec (REF_FORMULA_out: XML.Tree): XML.Tree = REF_FORMULA_out match {
|
|
wneuper@4736
|
155 |
case
|
|
wneuper@4848
|
156 |
XML.Elem(("REFFORMULA", Nil), List(
|
|
wneuper@4848
|
157 |
XML.Elem(("CALCID", Nil), List(XML.Text ("1"))),
|
|
wneuper@4848
|
158 |
XML.Elem(("CALCHEAD", List(("status", "incorrect"))), List(
|
|
wneuper@4848
|
159 |
XML.Elem(("POSITION", Nil), List(
|
|
wneuper@4848
|
160 |
XML.Elem(("INTLIST", Nil), Nil),
|
|
wneuper@4848
|
161 |
XML.Elem(("POS", Nil), List(XML.Text("Pbl"))))),
|
|
wneuper@4848
|
162 |
XML.Elem(("HEAD", Nil), List(
|
|
wneuper@4928
|
163 |
XML.Elem(("FORMULA", Nil), List(
|
|
wneuper@4928
|
164 |
XML.Elem(("ISA", Nil), List(XML.Text("solve (x + 1 = 2, x)"))),
|
|
wneuper@4928
|
165 |
XML.Elem(("TERM", Nil), _ ))) )),
|
|
wneuper@4848
|
166 |
XML.Elem(("MODEL", Nil), List(
|
|
wneuper@4848
|
167 |
XML.Elem(("GIVEN", Nil), Nil),
|
|
wneuper@4848
|
168 |
XML.Elem(("WHERE", Nil), List(
|
|
wneuper@4848
|
169 |
XML.Elem(("ITEM", List(("status", "false"))), List(
|
|
wneuper@4848
|
170 |
XML.Elem(("MATHML", Nil), List(
|
|
wneuper@4848
|
171 |
XML.Elem(("ISA", Nil), List(XML.Text("precond_rootpbl v_v"))))))))),
|
|
wneuper@4848
|
172 |
XML.Elem(("FIND", Nil), Nil),
|
|
wneuper@4848
|
173 |
XML.Elem(("RELATE", Nil), Nil))),
|
|
wneuper@4848
|
174 |
XML.Elem(("BELONGSTO", Nil), List(XML.Text("Pbl"))),
|
|
wneuper@4928
|
175 |
xml_spec ))))
|
|
wneuper@4736
|
176 |
=> xml_spec
|
|
wneuper@4736
|
177 |
case _ => throw new IllegalArgumentException("create_xml_spec exn")
|
|
wneuper@4736
|
178 |
}
|
|
wneuper@4746
|
179 |
def create_xml_thy (xml_spec: XML.Tree): XML.Tree = xml_spec match {
|
|
wneuper@4746
|
180 |
case
|
|
wneuper@4848
|
181 |
XML.Elem(("SPECIFICATION", Nil), List(
|
|
wneuper@4848
|
182 |
XML.Elem(("THEORYID", Nil), List(xml_thy)),
|
|
wneuper@4848
|
183 |
XML.Elem(("PROBLEMID", Nil), List(
|
|
wneuper@4848
|
184 |
XML.Elem(("STRINGLIST", Nil), List(
|
|
wneuper@4848
|
185 |
XML.Elem(("STRING", Nil), List(XML.Text("e_pblID"))))))),
|
|
wneuper@4848
|
186 |
XML.Elem(("METHODID", Nil), List(
|
|
wneuper@4848
|
187 |
XML.Elem(("STRINGLIST", Nil), List(
|
|
wneuper@4848
|
188 |
XML.Elem(("STRING", Nil), List(XML.Text("e_metID")))))))))
|
|
wneuper@4746
|
189 |
=> xml_thy
|
|
wneuper@4746
|
190 |
case _ => throw new IllegalArgumentException("create_xml_thy exn")
|
|
wneuper@4746
|
191 |
}
|
|
wneuper@4746
|
192 |
def create_xml_pbl (xml_spec: XML.Tree): XML.Tree = xml_spec match {
|
|
wneuper@4746
|
193 |
case
|
|
wneuper@4848
|
194 |
XML.Elem(("SPECIFICATION", Nil), List(
|
|
wneuper@4848
|
195 |
XML.Elem(("THEORYID", Nil), List(XML.Text("e_domID"))),
|
|
wneuper@4848
|
196 |
XML.Elem(("PROBLEMID", Nil), List(xml_pbl)),
|
|
wneuper@4848
|
197 |
XML.Elem(("METHODID", Nil), List(
|
|
wneuper@4848
|
198 |
XML.Elem(("STRINGLIST", Nil), List(
|
|
wneuper@4848
|
199 |
XML.Elem(("STRING", Nil), List(XML.Text("e_metID")))))))))
|
|
wneuper@4746
|
200 |
=> xml_pbl
|
|
wneuper@4746
|
201 |
case _ => throw new IllegalArgumentException("create_xml_pbl exn")
|
|
wneuper@4746
|
202 |
}
|
|
wneuper@4746
|
203 |
def create_xml_met (xml_spec: XML.Tree): XML.Tree = xml_spec match {
|
|
wneuper@4746
|
204 |
case
|
|
wneuper@4848
|
205 |
XML.Elem(("SPECIFICATION", Nil), List(
|
|
wneuper@4848
|
206 |
XML.Elem(("THEORYID", Nil), List(XML.Text("e_domID"))),
|
|
wneuper@4848
|
207 |
XML.Elem(("PROBLEMID", Nil), List(
|
|
wneuper@4848
|
208 |
XML.Elem(("STRINGLIST", Nil), List(
|
|
wneuper@4848
|
209 |
XML.Elem(("STRING", Nil), List(XML.Text("e_pblID"))))))),
|
|
wneuper@4848
|
210 |
XML.Elem(("METHODID", Nil), List(xml_met))))
|
|
wneuper@4746
|
211 |
=> xml_met
|
|
wneuper@4746
|
212 |
case _ => throw new IllegalArgumentException("create_xml_met exn")
|
|
wneuper@4746
|
213 |
}
|
|
wneuper@4928
|
214 |
//TODO: vvvvvvvvvvvvvv should exist with another identifier
|
|
wneuper@4928
|
215 |
def create_Formula_NEW (term: Term): XML.Tree = {
|
|
wneuper@4928
|
216 |
XML.Elem(("FORMULA", Nil), List(
|
|
wneuper@4928
|
217 |
XML.Elem(("ISA", Nil), List(XML.Text(Util.string_of(term)))),
|
|
wneuper@4928
|
218 |
XML.Elem(("TERM", Nil), List(Codec[Term].encode(term)))))
|
|
wneuper@4928
|
219 |
}
|
|
wneuper@4928
|
220 |
|
|
wneuper@4733
|
221 |
}
|