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