|
wneuper@4834
|
1 |
/**
|
|
wneuper@4834
|
2 |
* @author Walther Neuper
|
|
wneuper@4834
|
3 |
* Created on Sep 25, 2015
|
|
wneuper@4834
|
4 |
* (c) copyright due to license terms
|
|
wneuper@4834
|
5 |
*/
|
|
wneuper@4834
|
6 |
|
|
wneuper@4834
|
7 |
package isac.gui.mawen
|
|
wneuper@4834
|
8 |
|
|
wneuper@5088
|
9 |
import isac.gui.mawen.syntax.Ast._ //"._" simplifies "Ast.Ast" to "Ast"
|
|
walther@5239
|
10 |
import edu.tum.cs.isabelle.api.XML
|
|
wneuper@4834
|
11 |
|
|
wneuper@4834
|
12 |
/*
|
|
wneuper@4834
|
13 |
* terms for tests
|
|
wneuper@4834
|
14 |
*/
|
|
wneuper@4834
|
15 |
object TestDATA {
|
|
wneuper@4834
|
16 |
|
|
wneuper@4834
|
17 |
//---------------------------- for <code>TestXml</code>
|
|
wneuper@4834
|
18 |
// the priorities of the operators are from ~~/src/HOL/Groups.thy, Fields.thy, Power.thy, ...
|
|
wneuper@4834
|
19 |
|
|
wneuper@4867
|
20 |
// "1 + (2 * x * (y + 3)) / (4 * z * (y + 3)) + 5" ... Isabelle's + is left-associative:
|
|
wneuper@4867
|
21 |
// "(1 + (2 * x * (y + 3)) / (4 * z * (y + 3))) + 5"
|
|
wneuper@4834
|
22 |
def term_1(): XML.Tree = {
|
|
wneuper@4848
|
23 |
XML.Elem(("OP", List(("id", "+"), ("args", "2"), ("prior", "65"), ("fix", "in"))), List(
|
|
wneuper@4848
|
24 |
XML.Elem(("OP", List(("id", "+"), ("args", "2"), ("prior", "65"), ("fix", "in"))), List(
|
|
wneuper@4867
|
25 |
XML.Elem(("NUM", Nil), List(XML.Text ("1"))),
|
|
wneuper@4867
|
26 |
XML.Elem(("OP", List(("id", "/"), ("args", "2"), ("prior", "70"), ("fix", "in"))), List(
|
|
wneuper@4867
|
27 |
XML.Elem(("OP", List(("id", "*"), ("args", "2"), ("prior", "70"), ("fix", "in"))), List(
|
|
wneuper@4867
|
28 |
XML.Elem(("OP", List(("id", "*"), ("args", "2"), ("prior", "70"), ("fix", "in"))), List(
|
|
wneuper@4867
|
29 |
XML.Elem(("NUM", Nil), List(XML.Text ("2"))),
|
|
wneuper@4867
|
30 |
XML.Elem(("VAR", Nil), List(XML.Text ("x")))
|
|
wneuper@4867
|
31 |
) ),
|
|
wneuper@4867
|
32 |
XML.Elem(("OP", List(("id", "+"), ("args", "2"), ("prior", "65"), ("fix", "in"))), List(
|
|
wneuper@4867
|
33 |
XML.Elem(("VAR", Nil), List(XML.Text ("y"))),
|
|
wneuper@4867
|
34 |
XML.Elem(("NUM", Nil), List(XML.Text ("3")))
|
|
wneuper@4867
|
35 |
) )
|
|
wneuper@4867
|
36 |
) ),
|
|
wneuper@4867
|
37 |
XML.Elem(("OP", List(("id", "*"), ("args", "2"), ("prior", "70"), ("fix", "in"))), List(
|
|
wneuper@4867
|
38 |
XML.Elem(("OP", List(("id", "*"), ("args", "2"), ("prior", "70"), ("fix", "in"))), List(
|
|
wneuper@4867
|
39 |
XML.Elem(("NUM", Nil), List(XML.Text ("4"))),
|
|
wneuper@4867
|
40 |
XML.Elem(("VAR", Nil), List(XML.Text ("y")))
|
|
wneuper@4867
|
41 |
) ),
|
|
wneuper@4867
|
42 |
XML.Elem(("OP", List(("id", "+"), ("args", "2"), ("prior", "65"), ("fix", "in"))), List(
|
|
wneuper@4867
|
43 |
XML.Elem(("VAR", Nil), List(XML.Text ("y"))),
|
|
wneuper@4867
|
44 |
XML.Elem(("NUM", Nil), List(XML.Text ("3")))
|
|
wneuper@4867
|
45 |
) )
|
|
wneuper@4867
|
46 |
) )
|
|
wneuper@4867
|
47 |
) )
|
|
wneuper@4867
|
48 |
) ),
|
|
wneuper@4867
|
49 |
XML.Elem(("NUM", Nil), List(XML.Text ("5")))
|
|
wneuper@4867
|
50 |
) )
|
|
wneuper@4867
|
51 |
}
|
|
wneuper@4867
|
52 |
// the above term cancelled
|
|
wneuper@4867
|
53 |
// "1 + (2 * x) / (4 * z) + 5" ... Isabelle's + is left-associative, thus () omitted:
|
|
wneuper@4867
|
54 |
// "(1 + (2 * x) / (4 * z)) + 5"
|
|
wneuper@4867
|
55 |
def term_2(): XML.Tree = {
|
|
wneuper@4867
|
56 |
XML.Elem(("OP", List(("id", "+"), ("args", "2"), ("prior", "65"), ("fix", "in"))), List(
|
|
wneuper@4867
|
57 |
XML.Elem(("OP", List(("id", "+"), ("args", "2"), ("prior", "65"), ("fix", "in"))), List(
|
|
wneuper@4867
|
58 |
XML.Elem(("NUM", Nil), List(XML.Text ("1"))),
|
|
wneuper@4867
|
59 |
XML.Elem(("OP", List(("id", "/"), ("args", "2"), ("prior", "70"), ("fix", "in"))), List(
|
|
wneuper@4867
|
60 |
XML.Elem(("OP", List(("id", "*"), ("args", "2"), ("prior", "70"), ("fix", "in"))), List(
|
|
wneuper@4867
|
61 |
XML.Elem(("NUM", Nil), List(XML.Text ("2"))),
|
|
wneuper@4867
|
62 |
XML.Elem(("VAR", Nil), List(XML.Text ("x")))
|
|
wneuper@4867
|
63 |
) ),
|
|
wneuper@4867
|
64 |
XML.Elem(("OP", List(("id", "*"), ("args", "2"), ("prior", "70"), ("fix", "in"))), List(
|
|
wneuper@4867
|
65 |
XML.Elem(("NUM", Nil), List(XML.Text ("4"))),
|
|
wneuper@4867
|
66 |
XML.Elem(("VAR", Nil), List(XML.Text ("y")))
|
|
wneuper@4867
|
67 |
) )
|
|
wneuper@4867
|
68 |
) )
|
|
wneuper@4867
|
69 |
) ),
|
|
wneuper@4867
|
70 |
XML.Elem(("NUM", Nil), List(XML.Text ("5")))
|
|
wneuper@4867
|
71 |
) )
|
|
wneuper@4834
|
72 |
}
|
|
wneuper@4834
|
73 |
|
|
wneuper@4835
|
74 |
//---------------------------- for <code>TestWorksheetForMawen</code>
|
|
wneuper@4835
|
75 |
// "Diff (x + sin (x ^ 2), x)"
|
|
wneuper@4835
|
76 |
def term_Nil_Frm(): XML.Tree = {
|
|
wneuper@4848
|
77 |
XML.Elem(("CASCMD", List(("id", "Diff"), ("args", "2"))), List(
|
|
wneuper@4848
|
78 |
XML.Elem(("OP", List(("id", "+"), ("args", "2"), ("prior", "65"), ("fix", "in"))), List(
|
|
wneuper@4848
|
79 |
XML.Elem(("VAR", Nil), List(XML.Text ("x"))),
|
|
wneuper@4848
|
80 |
XML.Elem(("OP", List(("id", "sin"), ("args", "1"), ("prior", "99"), ("fix", "pre"))), List(
|
|
wneuper@4848
|
81 |
XML.Elem(("OP", List(("id", "^"), ("args", "2"), ("prior", "80"), ("fix", "in"))), List(
|
|
wneuper@4848
|
82 |
XML.Elem(("VAR", Nil), List(XML.Text ("x"))),
|
|
wneuper@4848
|
83 |
XML.Elem(("NUM", Nil), List(XML.Text ("2"))))))))),
|
|
wneuper@4848
|
84 |
XML.Elem(("VAR", Nil), List(XML.Text ("x")))))
|
|
wneuper@4835
|
85 |
}
|
|
wneuper@4835
|
86 |
|
|
wneuper@4838
|
87 |
// "d_d x (x + sin (x ^ 2))" as it comes from Isabelle (as SMLString)
|
|
wneuper@4838
|
88 |
def term_1_Frm_from_ISA(): XML.Tree = { // vvvvvvvvvvv--- enforces (term)
|
|
wneuper@4848
|
89 |
XML.Elem(("OP", List(("id", "d_d"), ("args", "2"), ("prior", "99"), ("fix", "pre"))), List(
|
|
wneuper@4848
|
90 |
XML.Elem(("VAR", Nil), List(XML.Text ("x"))),
|
|
wneuper@4848
|
91 |
XML.Elem(("OP", List(("id", "+"), ("args", "2"), ("prior", "65"), ("fix", "in"))), List(
|
|
wneuper@4848
|
92 |
XML.Elem(("VAR", Nil), List(XML.Text ("x"))),
|
|
wneuper@4848
|
93 |
XML.Elem(("OP", List(("id", "sin"), ("args", "1"), ("prior", "99"), ("fix", "pre"))), List(
|
|
wneuper@4848
|
94 |
XML.Elem(("OP", List(("id", "^"), ("args", "2"), ("prior", "80"), ("fix", "in"))), List(
|
|
wneuper@4848
|
95 |
XML.Elem(("VAR", Nil), List(XML.Text ("x"))),
|
|
wneuper@4848
|
96 |
XML.Elem(("NUM", Nil), List(XML.Text ("2")))))))))))
|
|
wneuper@4838
|
97 |
}
|
|
wneuper@4838
|
98 |
// "d_d x (x + sin (x ^ 2))" as presented to the gui ??????????????????????????????????????????????????
|
|
wneuper@4839
|
99 |
// version a: involves not-clarified mixfix notation
|
|
wneuper@4838
|
100 |
def term_1_Frm(): XML.Tree = {
|
|
wneuper@4838
|
101 |
// ambiguous..: no division -------v vvv vvv--- like "=" in HOL.thy ?????????
|
|
wneuper@4848
|
102 |
XML.Elem(("OP", List(("id", "/"), ("args", "3"), ("prior", "50"), ("fix", "mixfix"))), List(
|
|
wneuper@4848
|
103 |
XML.Elem(("CONST", Nil), List(XML.Text ("d"))), // CONST or OP or VAR ??????????????????????
|
|
wneuper@4848
|
104 |
XML.Elem(("VAR", Nil), List(XML.Text ("x"))),
|
|
wneuper@4848
|
105 |
XML.Elem(("OP", List(("id", "+"), ("args", "2"), ("prior", "65"), ("fix", "in"))), List(
|
|
wneuper@4848
|
106 |
XML.Elem(("VAR", Nil), List(XML.Text ("x"))),
|
|
wneuper@4848
|
107 |
XML.Elem(("OP", List(("id", "sin"), ("args", "1"), ("prior", "99"), ("fix", "pre"))), List(
|
|
wneuper@4848
|
108 |
XML.Elem(("OP", List(("id", "^"), ("args", "2"), ("prior", "80"), ("fix", "in"))), List(
|
|
wneuper@4848
|
109 |
XML.Elem(("VAR", Nil), List(XML.Text ("x"))),
|
|
wneuper@4848
|
110 |
XML.Elem(("NUM", Nil), List(XML.Text ("2")))))))))))
|
|
wneuper@4838
|
111 |
} // if ("args", "2") then we have no root for "/ d x" and "(x + sin (x ^ 2))" ????????????????????????
|
|
wneuper@4838
|
112 |
// but we could treat this as fraction --------^^^^^^^ and ^^^^^^^^^^^^^^^^^^^ is dangling without root
|
|
wneuper@4839
|
113 |
|
|
wneuper@4839
|
114 |
// "d_d x (x + sin (x ^ 2))" as presented to the gui ??????????????????????????????????????????????????
|
|
wneuper@4839
|
115 |
// version b: allows to represent "d_d x" as a normal fraction, but introduces additional TERM
|
|
wneuper@4839
|
116 |
def term_1_Frmb(): XML.Tree = {
|
|
wneuper@4848
|
117 |
XML.Elem(("TERM", List(("args", "2"))), List(
|
|
wneuper@4848
|
118 |
XML.Elem(("OP", List(("id", "/"), ("args", "2"), ("prior", "70"), ("fix", "in"))), List(
|
|
wneuper@4848
|
119 |
XML.Elem(("CONST", Nil), List(XML.Text ("d"))), // CONST or OP or VAR ????????????????????
|
|
wneuper@4848
|
120 |
XML.Elem(("TERM", List(("args", "2"))), List( // "d x" in the denominator have no root otherwise !!!!!!!!
|
|
wneuper@4848
|
121 |
XML.Elem(("CONST", Nil), List(XML.Text ("d"))),
|
|
wneuper@4848
|
122 |
XML.Elem(("VAR", Nil), List(XML.Text ("x"))))))),
|
|
wneuper@4848
|
123 |
XML.Elem(("OP", List(("id", "+"), ("args", "2"), ("prior", "65"), ("fix", "in"))), List(
|
|
wneuper@4848
|
124 |
XML.Elem(("VAR", Nil), List(XML.Text ("x"))),
|
|
wneuper@4848
|
125 |
XML.Elem(("OP", List(("id", "sin"), ("args", "1"), ("prior", "99"), ("fix", "pre"))), List(
|
|
wneuper@4848
|
126 |
XML.Elem(("OP", List(("id", "^"), ("args", "2"), ("prior", "80"), ("fix", "in"))), List(
|
|
wneuper@4848
|
127 |
XML.Elem(("VAR", Nil), List(XML.Text ("x"))),
|
|
wneuper@4848
|
128 |
XML.Elem(("NUM", Nil), List(XML.Text ("2")))))))))))
|
|
wneuper@4839
|
129 |
}
|
|
wneuper@4838
|
130 |
// CONCLUSION: either d_d as mixfix (with fraction?), or introduce TERM as root, or ???????????????????
|
|
s1520454056@5223
|
131 |
|
|
s1520454056@5223
|
132 |
// TestData from TestUseCases.testUC_userguide()
|
|
s1520454056@5223
|
133 |
def ast_05() : Ast =
|
|
s1520454056@5223
|
134 |
Appl(List(
|
|
s1520454056@5223
|
135 |
Constant("Groups.plus_class.plus"),
|
|
s1520454056@5223
|
136 |
Appl(List(
|
|
s1520454056@5223
|
137 |
Constant("Diff.d_d"),
|
|
s1520454056@5223
|
138 |
Variable("x"),
|
|
s1520454056@5223
|
139 |
Variable("x"))),
|
|
s1520454056@5223
|
140 |
Appl(List(
|
|
s1520454056@5223
|
141 |
Constant("Diff.d_d"),
|
|
s1520454056@5223
|
142 |
Variable("x"),
|
|
s1520454056@5223
|
143 |
Appl(List( //added to above
|
|
s1520454056@5223
|
144 |
Constant("BOX.1"), //added to above
|
|
s1520454056@5223
|
145 |
Appl(List(
|
|
s1520454056@5223
|
146 |
Constant("Transcendental.sin"),
|
|
s1520454056@5223
|
147 |
Appl(List( //added to above
|
|
s1520454056@5223
|
148 |
Constant("BOX.2"), //added to above
|
|
s1520454056@5223
|
149 |
Appl(List(
|
|
s1520454056@5223
|
150 |
Constant("Power.power_class.power"),
|
|
s1520454056@5223
|
151 |
Variable("x"),
|
|
s1520454056@5223
|
152 |
Variable("2")))))))))))))
|
|
s1520454056@5223
|
153 |
|
|
s1520454056@5223
|
154 |
def ast_06() : Ast =
|
|
s1520454056@5223
|
155 |
Appl(List(
|
|
s1520454056@5223
|
156 |
Constant("HOL.eq"),
|
|
s1520454056@5223
|
157 |
Appl(List(
|
|
s1520454056@5223
|
158 |
Constant("Diff.d_d"),
|
|
s1520454056@5223
|
159 |
Variable("bdv"),
|
|
s1520454056@5223
|
160 |
Appl(List( //added to above
|
|
s1520454056@5223
|
161 |
Constant("BOX.1"), //added to above
|
|
s1520454056@5223
|
162 |
Appl(List(
|
|
s1520454056@5223
|
163 |
Constant("Transcendental.sin"),
|
|
s1520454056@5223
|
164 |
Appl(List( //added to above
|
|
s1520454056@5223
|
165 |
Constant("BOX.2"), //added to above
|
|
s1520454056@5223
|
166 |
Variable("u"))))))))),
|
|
s1520454056@5223
|
167 |
Appl(List(
|
|
s1520454056@5223
|
168 |
Constant("Groups.times_class.times"),
|
|
s1520454056@5223
|
169 |
Appl(List( //added to above
|
|
s1520454056@5223
|
170 |
Constant("BOX.3"), //added to above
|
|
s1520454056@5223
|
171 |
Appl(List(
|
|
s1520454056@5223
|
172 |
Constant("Transcendental.cos"),
|
|
s1520454056@5223
|
173 |
Variable("u"))))),
|
|
s1520454056@5223
|
174 |
Appl(List(
|
|
s1520454056@5223
|
175 |
Constant("Diff.d_d"),
|
|
s1520454056@5223
|
176 |
Variable("bdv"),
|
|
s1520454056@5223
|
177 |
Appl(List( //added to above
|
|
s1520454056@5223
|
178 |
Constant("BOX.4"), //added to above
|
|
s1520454056@5223
|
179 |
Variable("u")))))))))
|
|
s1520454056@5223
|
180 |
|
|
s1520454056@5223
|
181 |
def ast_07() : Ast =
|
|
s1520454056@5223
|
182 |
Appl(List(
|
|
s1520454056@5223
|
183 |
Constant("Groups.plus_class.plus"),
|
|
s1520454056@5223
|
184 |
Appl(List(
|
|
s1520454056@5223
|
185 |
Constant("Diff.d_d"),
|
|
s1520454056@5223
|
186 |
Variable("x"),
|
|
s1520454056@5223
|
187 |
Variable("x"))),
|
|
s1520454056@5223
|
188 |
Appl(List(
|
|
s1520454056@5223
|
189 |
Constant("Groups.times_class.times"),
|
|
s1520454056@5223
|
190 |
Appl(List( //added to above
|
|
s1520454056@5223
|
191 |
Constant("BOX.3"), //added to above
|
|
s1520454056@5223
|
192 |
Appl(List(
|
|
s1520454056@5223
|
193 |
Constant("Transcendental.cos"),
|
|
s1520454056@5223
|
194 |
Appl(List(
|
|
s1520454056@5223
|
195 |
Constant("Power.power_class.power"),
|
|
s1520454056@5223
|
196 |
Variable("x"),
|
|
s1520454056@5223
|
197 |
Variable("2"))))))),
|
|
s1520454056@5223
|
198 |
Appl(List(
|
|
s1520454056@5223
|
199 |
Constant("Diff.d_d"),
|
|
s1520454056@5223
|
200 |
Variable("x"),
|
|
s1520454056@5223
|
201 |
Appl(List( //added to above
|
|
s1520454056@5223
|
202 |
Constant("BOX.4"), //added to above
|
|
s1520454056@5223
|
203 |
Variable("GAP")))))))))
|
|
wneuper@5087
|
204 |
|
|
walther@5239
|
205 |
}
|