akargl@42176
|
1 |
(* Title: tests for mathml.sml
|
akargl@42176
|
2 |
Author: Walther Neuper 060311
|
neuper@37906
|
3 |
(c) isac-team 2006
|
neuper@37906
|
4 |
*)
|
neuper@37906
|
5 |
"-----------------------------------------------------------------";
|
neuper@37906
|
6 |
"table of contents -----------------------------------------------";
|
neuper@37906
|
7 |
"-----------------------------------------------------------------";
|
neuper@37906
|
8 |
"within struct ---------------------------------------------------";
|
neuper@37906
|
9 |
"-----------------------------------------------------------------";
|
neuper@37906
|
10 |
"--------- encode ^^^ -> ^ ---------------------------------------";
|
neuper@37906
|
11 |
"--------- encode < -> < and > -> > --------------------------";
|
wneuper@59177
|
12 |
"--------- fun rm_doublets '-4 * b ^^^^^^^^^ 2 / (...' -----------";
|
wneuper@59177
|
13 |
"--------- fun decode '-4 * b ^^^^^^^^^ 2 / (...' ----------------";
|
wneuper@59213
|
14 |
"--------- fun xml_of_term_NEW, xml_to_term_NEW ------------------";
|
wneuper@59214
|
15 |
"--------- create testdata for TestPIDE.java#testTermTransfer ----";
|
neuper@37906
|
16 |
"-----------------------------------------------------------------";
|
neuper@37906
|
17 |
"exported from struct --------------------------------------------";
|
neuper@37906
|
18 |
"-----------------------------------------------------------------";
|
neuper@37906
|
19 |
"--------- ... ---------------------------------------------------";
|
neuper@37906
|
20 |
"-----------------------------------------------------------------";
|
neuper@37906
|
21 |
|
neuper@37906
|
22 |
|
neuper@37906
|
23 |
|
neuper@37906
|
24 |
"-----------------------------------------------------------------";
|
neuper@37906
|
25 |
"within struct ---------------------------------------------------";
|
neuper@37906
|
26 |
"-----------------------------------------------------------------";
|
neuper@37906
|
27 |
(*==================================================================*)
|
neuper@37906
|
28 |
|
neuper@37906
|
29 |
"--------- encode ^^^ -> ^ ---------------------------------------";
|
neuper@37906
|
30 |
"--------- encode ^^^ -> ^ ---------------------------------------";
|
neuper@37906
|
31 |
"--------- encode ^^^ -> ^ ---------------------------------------";
|
neuper@37906
|
32 |
val str = "a^^^2+b^^^2=c^^^2";
|
neuper@37906
|
33 |
if decode str = "a^2+b^2=c^2" then ()
|
neuper@38031
|
34 |
else error "mathml.sml: diff.behav. in encode ^^^ -> ^";
|
neuper@37906
|
35 |
|
akargl@42176
|
36 |
"--------- encode < -> < and > -> > --------------------------";
|
akargl@42176
|
37 |
"--------- encode < -> < and > -> > --------------------------";
|
akargl@42176
|
38 |
"--------- encode < -> < and > -> > --------------------------";
|
neuper@37906
|
39 |
val str = "?bdv occurs_in ?b; 0 < ?n |] ==> ?a / ?b ^ ?n = ?a * ?b ^ - ?n";
|
akargl@42176
|
40 |
if decode str = "?bdv occurs_in ?b; 0 < ?n |] ==> ?a / ?b ^ ?n = ?a * ?b ^ - ?n" then ()
|
akargl@42176
|
41 |
else error "mathml.sml: diff.behav. in encode '<' and '>'";
|
neuper@37906
|
42 |
|
akargl@42176
|
43 |
(*========== inhibit exn AK110725 ================================================
|
neuper@37906
|
44 |
"----- check 'manually' the xml-output of calling functions ------";
|
akargl@42176
|
45 |
formula2xml 1 (str2term str);
|
neuper@37906
|
46 |
|
akargl@42176
|
47 |
(* AK110725
|
akargl@42176
|
48 |
(*str2term str; (* ERROR: Inner syntax error at "; 0 < ?n |] ==> ?a / ?b ^ ?n = ?a * ?b ^ - ?n"
|
akargl@42176
|
49 |
Failed to parse term*)*)
|
akargl@42176
|
50 |
"~~~~~ fun str2term, args:"; val (str) = (str);
|
walther@59879
|
51 |
ThyC.get_theory "Isac_Knowledge";
|
akargl@42176
|
52 |
|
akargl@42176
|
53 |
parse_patt;
|
walther@59879
|
54 |
parse_patt (ThyC.get_theory "Isac_Knowledge");
|
walther@59879
|
55 |
(*parse_patt (ThyC.get_theory "Isac_Knowledge") str; (* ERROR: Inner syntax error at "; 0 < ?n |] ==> ?a / ?b ^ ?n = ?a * ?b ^ - ?n"
|
akargl@42176
|
56 |
Failed to parse term*)*)
|
akargl@42176
|
57 |
|
walther@59879
|
58 |
"~~~~~ fun parse_patt, args:"; val (thy, str) = ((ThyC.get_theory "Isac_Knowledge"), str);
|
akargl@42176
|
59 |
(thy, str)
|
walther@59879
|
60 |
|>> ThyC.to_ctxt
|
neuper@48761
|
61 |
(*|-> Proof_Context.read_term_pattern (*ERROR: Inner syntax error at "; 0 < ?n |] ==> ?a / ?b ^ ?n = ?a * ?b ^ - ?n"
|
akargl@42176
|
62 |
Failed to parse term*)*)
|
akargl@42176
|
63 |
|
neuper@48761
|
64 |
Proof_Context.read_term_pattern;
|
walther@59879
|
65 |
(@{theory "Isac_Knowledge"}, str) |>> ThyC.to_ctxt;
|
neuper@48761
|
66 |
"~~~~~ fun Proof_Context.read_term_pattern, args:"; val () = ();
|
akargl@42176
|
67 |
(*AK110725 To be continued...*)
|
akargl@42176
|
68 |
*)
|
neuper@37906
|
69 |
(*==================================================================*)
|
neuper@37906
|
70 |
"-----------------------------------------------------------------";
|
neuper@37906
|
71 |
"exported from struct --------------------------------------------";
|
neuper@37906
|
72 |
"-----------------------------------------------------------------";
|
akargl@42176
|
73 |
========== inhibit exn AK110725 ================================================*)
|
wneuper@59177
|
74 |
|
wneuper@59177
|
75 |
"--------- fun rm_doublets '-4 * b ^^^^^^^^^ 2 / (...' -----------";
|
wneuper@59177
|
76 |
"--------- fun rm_doublets '-4 * b ^^^^^^^^^ 2 / (...' -----------";
|
wneuper@59177
|
77 |
"--------- fun rm_doublets '-4 * b ^^^^^^^^^ 2 / (...' -----------";
|
wneuper@59177
|
78 |
val c = "^";
|
walther@59997
|
79 |
val cs = ["^", "^", "^", "d", "e"];
|
wneuper@59177
|
80 |
if rm_doublets c [] cs = Symbol.explode "^de"
|
wneuper@59177
|
81 |
then () else error "rm_doublets '^^^de' CHANGED";
|
wneuper@59177
|
82 |
|
walther@59997
|
83 |
val cs = ["a", "b", "^", "^", "^", "d", "e"];
|
wneuper@59177
|
84 |
if rm_doublets c [] cs = Symbol.explode "ab^de"
|
wneuper@59177
|
85 |
then () else error "rm_doublets 'ab^^^de' CHANGED";
|
wneuper@59177
|
86 |
|
wneuper@59177
|
87 |
val cstr =
|
wneuper@59177
|
88 |
"-4 * b ^^^^^^^^^ 2 / (a + b) + 4 * a ^^^^^^^^^ 2 / (a + b) -4 * b ^ 2 / (a + b) + 4 * a ^ 2 / (a + b)";
|
wneuper@59177
|
89 |
val cs = Symbol.explode cstr;
|
wneuper@59177
|
90 |
if rm_doublets c [] cs = Symbol.explode
|
wneuper@59177
|
91 |
"-4 * b ^ 2 / (a + b) + 4 * a ^ 2 / (a + b) -4 * b ^ 2 / (a + b) + 4 * a ^ 2 / (a + b)"
|
wneuper@59177
|
92 |
then () else error "rm_doublets '-4 * b ^^^^^..' CHANGED";
|
wneuper@59177
|
93 |
|
wneuper@59177
|
94 |
"--------- fun decode '-4 * b ^^^^^^^^^ 2 / (...' ----------------";
|
wneuper@59177
|
95 |
"--------- fun decode '-4 * b ^^^^^^^^^ 2 / (...' ----------------";
|
wneuper@59177
|
96 |
"--------- fun decode '-4 * b ^^^^^^^^^ 2 / (...' ----------------";
|
wneuper@59177
|
97 |
if encode cstr =
|
wneuper@59177
|
98 |
"-4 * b ^^^ 2 / (a + b) + 4 * a ^^^ 2 / (a + b) -4 * b ^^^ 2 / (a + b) + 4 * a ^^^ 2 / (a + b)"
|
wneuper@59177
|
99 |
then () else error "encode '-4 * b ^^^^^..' CHANGED";
|
wneuper@59177
|
100 |
|
wneuper@59224
|
101 |
"--------- fun xmlstr --------------------------------------------";
|
wneuper@59224
|
102 |
"--------- fun xmlstr --------------------------------------------";
|
wneuper@59224
|
103 |
"--------- fun xmlstr --------------------------------------------";
|
wneuper@59224
|
104 |
val term = @{term "aaa + bbb::real"};
|
wneuper@59224
|
105 |
val str = term |> xml_of_term_NEW |> xmlstr 0;
|
wneuper@59224
|
106 |
if str =
|
walther@59617
|
107 |
"(FORMULA)\n. (ISA)\n. . aaa + bbb\n. (/ISA)\n. (TERM)\n aaa + bbb\n(/TERM)\n(/FORMULA)\n"
|
wneuper@59224
|
108 |
then () else error "term |> xml_of_term_NEW |> xmlstr ..changed";
|
wneuper@59224
|
109 |
writeln str;
|
wneuper@59224
|
110 |
|
wneuper@59213
|
111 |
"--------- fun xml_of_term_NEW, xml_to_term_NEW ------------------";
|
wneuper@59213
|
112 |
"--------- fun xml_of_term_NEW, xml_to_term_NEW ------------------";
|
wneuper@59213
|
113 |
"--------- fun xml_of_term_NEW, xml_to_term_NEW ------------------";
|
wneuper@59224
|
114 |
(* xml_of_term_NEW o xml_to_term_NEW = id ... not valid,
|
wneuper@59224
|
115 |
as long as the latter (going: frontend \<longrightarrow> kernel) does only carry "ISA" string.
|
wneuper@59213
|
116 |
val t = @{term "aaa + bbb::real"};
|
wneuper@59213
|
117 |
if t = (t |> xml_of_term_NEW |> xml_to_term_NEW) then ()
|
wneuper@59213
|
118 |
else error "xml_of_term_NEW |> xml_to_term_NEW changed"
|
wneuper@59224
|
119 |
*)
|
wneuper@59214
|
120 |
|
wneuper@59214
|
121 |
"--------- create testdata for TestPIDE.java#testTermTransfer ----";
|
wneuper@59214
|
122 |
"--------- create testdata for TestPIDE.java#testTermTransfer ----";
|
wneuper@59214
|
123 |
"--------- create testdata for TestPIDE.java#testTermTransfer ----";
|
wneuper@59214
|
124 |
val t = @{term "aaa + bbb::real"};
|
wneuper@59214
|
125 |
val ttt = HOLogic.mk_eq (t, Const ("processed_by_Isabelle_Isac", type_of t))
|
wneuper@59214
|
126 |
(* check the term structure *)
|
wneuper@59214
|
127 |
val Const ("HOL.eq", T1) $
|
wneuper@59214
|
128 |
(Const ("Groups.plus_class.plus", T2) $
|
wneuper@59214
|
129 |
Free ("aaa", T3) $
|
wneuper@59214
|
130 |
Free ("bbb", _)) $
|
wneuper@59214
|
131 |
Const ("processed_by_Isabelle_Isac", _) = ttt;
|
wneuper@59214
|
132 |
|
wneuper@59214
|
133 |
(* check the type structure *)
|
wneuper@59214
|
134 |
atomtyp T3;
|
wneuper@59214
|
135 |
Type ("Real.real", []);
|
wneuper@59214
|
136 |
|
wneuper@59214
|
137 |
atomtyp T2;
|
wneuper@59214
|
138 |
(*
|
wneuper@59214
|
139 |
*** Type (fun,[
|
wneuper@59214
|
140 |
*** . Type (Real.real,[])
|
wneuper@59214
|
141 |
*** . Type (fun,[
|
wneuper@59214
|
142 |
*** . . Type (Real.real,[])
|
wneuper@59214
|
143 |
*** . . Type (Real.real,[])
|
wneuper@59214
|
144 |
*** . . ]
|
wneuper@59214
|
145 |
*** . ]
|
wneuper@59214
|
146 |
with this ^^^ build the typ ...*)
|
wneuper@59214
|
147 |
Type ("fun", [
|
wneuper@59214
|
148 |
Type ("Real.real", []),
|
wneuper@59214
|
149 |
Type ("fun", [
|
wneuper@59214
|
150 |
Type ("Real.real", []),
|
wneuper@59214
|
151 |
Type ("Real.real", [])])]);
|
wneuper@59214
|
152 |
|
wneuper@59214
|
153 |
atomtyp T1;
|
wneuper@59214
|
154 |
(*
|
wneuper@59214
|
155 |
*** Type (fun,[
|
wneuper@59214
|
156 |
*** . Type (Real.real,[])
|
wneuper@59214
|
157 |
*** . Type (fun,[
|
wneuper@59214
|
158 |
*** . . Type (Real.real,[])
|
wneuper@59214
|
159 |
*** . . Type (HOL.bool,[])
|
wneuper@59214
|
160 |
*** . . ]
|
wneuper@59214
|
161 |
*** . ]
|
wneuper@59214
|
162 |
with this ^^^ build the typ ...*)
|
wneuper@59214
|
163 |
Type ("fun", [
|
wneuper@59214
|
164 |
Type ("Real.real", []),
|
wneuper@59214
|
165 |
Type ("fun", [
|
wneuper@59214
|
166 |
Type ("Real.real", []),
|
wneuper@59214
|
167 |
Type ("HOL.bool", [])])]);
|
wneuper@59214
|
168 |
|
wneuper@59214
|
169 |
(* now compose term + typ *)
|
wneuper@59214
|
170 |
val Const ("HOL.eq", Type ("fun", [
|
wneuper@59214
|
171 |
Type ("Real.real", []),
|
wneuper@59214
|
172 |
Type ("fun", [
|
wneuper@59214
|
173 |
Type ("Real.real", []),
|
wneuper@59214
|
174 |
Type ("HOL.bool", [])])])) $
|
wneuper@59214
|
175 |
(Const ("Groups.plus_class.plus", Type ("fun", [
|
wneuper@59214
|
176 |
Type ("Real.real", []),
|
wneuper@59214
|
177 |
Type ("fun", [
|
wneuper@59214
|
178 |
Type ("Real.real", []),
|
wneuper@59214
|
179 |
Type ("Real.real", [])])])) $
|
wneuper@59214
|
180 |
Free ("aaa", Type ("Real.real", [])) $
|
wneuper@59214
|
181 |
Free ("bbb", Type ("Real.real", []))) $
|
wneuper@59214
|
182 |
Const ("processed_by_Isabelle_Isac", Type ("Real.real", [])) = ttt;
|
wneuper@59214
|
183 |
|
wneuper@59214
|
184 |
(* match out the original term from result*)
|
wneuper@59214
|
185 |
val Const ("HOL.eq", Type ("fun", [
|
wneuper@59214
|
186 |
Type ("Real.real", []),
|
wneuper@59214
|
187 |
Type ("fun", [
|
wneuper@59214
|
188 |
Type ("Real.real", []),
|
wneuper@59214
|
189 |
Type ("HOL.bool", [])])])) $
|
wneuper@59214
|
190 |
t' $
|
wneuper@59214
|
191 |
Const ("processed_by_Isabelle_Isac", Type ("Real.real", [])) = ttt;
|
wneuper@59214
|
192 |
if t = t' then () else error "something with test_term changed"
|