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 ------------------";
|
neuper@37906
|
15 |
"-----------------------------------------------------------------";
|
neuper@37906
|
16 |
"exported from struct --------------------------------------------";
|
neuper@37906
|
17 |
"-----------------------------------------------------------------";
|
neuper@37906
|
18 |
"--------- ... ---------------------------------------------------";
|
neuper@37906
|
19 |
"-----------------------------------------------------------------";
|
neuper@37906
|
20 |
|
neuper@37906
|
21 |
|
neuper@37906
|
22 |
|
neuper@37906
|
23 |
"-----------------------------------------------------------------";
|
neuper@37906
|
24 |
"within struct ---------------------------------------------------";
|
neuper@37906
|
25 |
"-----------------------------------------------------------------";
|
neuper@37906
|
26 |
(*==================================================================*)
|
neuper@37906
|
27 |
|
neuper@37906
|
28 |
"--------- encode ^^^ -> ^ ---------------------------------------";
|
neuper@37906
|
29 |
"--------- encode ^^^ -> ^ ---------------------------------------";
|
neuper@37906
|
30 |
"--------- encode ^^^ -> ^ ---------------------------------------";
|
neuper@37906
|
31 |
val str = "a^^^2+b^^^2=c^^^2";
|
neuper@37906
|
32 |
if decode str = "a^2+b^2=c^2" then ()
|
neuper@38031
|
33 |
else error "mathml.sml: diff.behav. in encode ^^^ -> ^";
|
neuper@37906
|
34 |
|
akargl@42176
|
35 |
"--------- encode < -> < and > -> > --------------------------";
|
akargl@42176
|
36 |
"--------- encode < -> < and > -> > --------------------------";
|
akargl@42176
|
37 |
"--------- encode < -> < and > -> > --------------------------";
|
neuper@37906
|
38 |
val str = "?bdv occurs_in ?b; 0 < ?n |] ==> ?a / ?b ^ ?n = ?a * ?b ^ - ?n";
|
akargl@42176
|
39 |
if decode str = "?bdv occurs_in ?b; 0 < ?n |] ==> ?a / ?b ^ ?n = ?a * ?b ^ - ?n" then ()
|
akargl@42176
|
40 |
else error "mathml.sml: diff.behav. in encode '<' and '>'";
|
neuper@37906
|
41 |
|
akargl@42176
|
42 |
(*========== inhibit exn AK110725 ================================================
|
neuper@37906
|
43 |
"----- check 'manually' the xml-output of calling functions ------";
|
akargl@42176
|
44 |
formula2xml 1 (str2term str);
|
neuper@37906
|
45 |
|
akargl@42176
|
46 |
(* AK110725
|
akargl@42176
|
47 |
(*str2term str; (* ERROR: Inner syntax error at "; 0 < ?n |] ==> ?a / ?b ^ ?n = ?a * ?b ^ - ?n"
|
akargl@42176
|
48 |
Failed to parse term*)*)
|
akargl@42176
|
49 |
"~~~~~ fun str2term, args:"; val (str) = (str);
|
akargl@42176
|
50 |
Thy_Info.get_theory "Isac";
|
akargl@42176
|
51 |
|
akargl@42176
|
52 |
parse_patt;
|
akargl@42176
|
53 |
parse_patt (Thy_Info.get_theory "Isac");
|
akargl@42176
|
54 |
(*parse_patt (Thy_Info.get_theory "Isac") str; (* ERROR: Inner syntax error at "; 0 < ?n |] ==> ?a / ?b ^ ?n = ?a * ?b ^ - ?n"
|
akargl@42176
|
55 |
Failed to parse term*)*)
|
akargl@42176
|
56 |
|
akargl@42176
|
57 |
"~~~~~ fun parse_patt, args:"; val (thy, str) = ((Thy_Info.get_theory "Isac"), str);
|
akargl@42176
|
58 |
(thy, str)
|
akargl@42176
|
59 |
|>> thy2ctxt
|
neuper@48761
|
60 |
(*|-> Proof_Context.read_term_pattern (*ERROR: Inner syntax error at "; 0 < ?n |] ==> ?a / ?b ^ ?n = ?a * ?b ^ - ?n"
|
akargl@42176
|
61 |
Failed to parse term*)*)
|
akargl@42176
|
62 |
|
neuper@48761
|
63 |
Proof_Context.read_term_pattern;
|
akargl@42176
|
64 |
(@{theory "Isac"}, str) |>> thy2ctxt;
|
neuper@48761
|
65 |
"~~~~~ fun Proof_Context.read_term_pattern, args:"; val () = ();
|
akargl@42176
|
66 |
(*AK110725 To be continued...*)
|
akargl@42176
|
67 |
*)
|
neuper@37906
|
68 |
(*==================================================================*)
|
neuper@37906
|
69 |
"-----------------------------------------------------------------";
|
neuper@37906
|
70 |
"exported from struct --------------------------------------------";
|
neuper@37906
|
71 |
"-----------------------------------------------------------------";
|
akargl@42176
|
72 |
========== inhibit exn AK110725 ================================================*)
|
wneuper@59177
|
73 |
|
wneuper@59177
|
74 |
"--------- fun rm_doublets '-4 * b ^^^^^^^^^ 2 / (...' -----------";
|
wneuper@59177
|
75 |
"--------- fun rm_doublets '-4 * b ^^^^^^^^^ 2 / (...' -----------";
|
wneuper@59177
|
76 |
"--------- fun rm_doublets '-4 * b ^^^^^^^^^ 2 / (...' -----------";
|
wneuper@59177
|
77 |
val c = "^";
|
wneuper@59177
|
78 |
val cs = ["^","^","^","d","e"];
|
wneuper@59177
|
79 |
if rm_doublets c [] cs = Symbol.explode "^de"
|
wneuper@59177
|
80 |
then () else error "rm_doublets '^^^de' CHANGED";
|
wneuper@59177
|
81 |
|
wneuper@59177
|
82 |
val cs = ["a","b","^","^","^","d","e"];
|
wneuper@59177
|
83 |
if rm_doublets c [] cs = Symbol.explode "ab^de"
|
wneuper@59177
|
84 |
then () else error "rm_doublets 'ab^^^de' CHANGED";
|
wneuper@59177
|
85 |
|
wneuper@59177
|
86 |
val cstr =
|
wneuper@59177
|
87 |
"-4 * b ^^^^^^^^^ 2 / (a + b) + 4 * a ^^^^^^^^^ 2 / (a + b) -4 * b ^ 2 / (a + b) + 4 * a ^ 2 / (a + b)";
|
wneuper@59177
|
88 |
val cs = Symbol.explode cstr;
|
wneuper@59177
|
89 |
if rm_doublets c [] cs = Symbol.explode
|
wneuper@59177
|
90 |
"-4 * b ^ 2 / (a + b) + 4 * a ^ 2 / (a + b) -4 * b ^ 2 / (a + b) + 4 * a ^ 2 / (a + b)"
|
wneuper@59177
|
91 |
then () else error "rm_doublets '-4 * b ^^^^^..' CHANGED";
|
wneuper@59177
|
92 |
|
wneuper@59177
|
93 |
"--------- fun decode '-4 * b ^^^^^^^^^ 2 / (...' ----------------";
|
wneuper@59177
|
94 |
"--------- fun decode '-4 * b ^^^^^^^^^ 2 / (...' ----------------";
|
wneuper@59177
|
95 |
"--------- fun decode '-4 * b ^^^^^^^^^ 2 / (...' ----------------";
|
wneuper@59177
|
96 |
if encode cstr =
|
wneuper@59177
|
97 |
"-4 * b ^^^ 2 / (a + b) + 4 * a ^^^ 2 / (a + b) -4 * b ^^^ 2 / (a + b) + 4 * a ^^^ 2 / (a + b)"
|
wneuper@59177
|
98 |
then () else error "encode '-4 * b ^^^^^..' CHANGED";
|
wneuper@59177
|
99 |
|
wneuper@59213
|
100 |
"--------- fun xml_of_term_NEW, xml_to_term_NEW ------------------";
|
wneuper@59213
|
101 |
"--------- fun xml_of_term_NEW, xml_to_term_NEW ------------------";
|
wneuper@59213
|
102 |
"--------- fun xml_of_term_NEW, xml_to_term_NEW ------------------";
|
wneuper@59213
|
103 |
val t = @{term "aaa + bbb::real"};
|
wneuper@59213
|
104 |
if t = (t |> xml_of_term_NEW |> xml_to_term_NEW) then ()
|
wneuper@59213
|
105 |
else error "xml_of_term_NEW |> xml_to_term_NEW changed"
|