1 (* Title: tests for mathml.sml
2 Author: Walther Neuper 060311
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 "-----------------------------------------------------------------";
24 "-----------------------------------------------------------------";
25 "within struct ---------------------------------------------------";
26 "-----------------------------------------------------------------";
27 (*==================================================================*)
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 ^^^ -> ^";
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 '>'";
43 (*========== inhibit exn AK110725 ================================================
44 "----- check 'manually' the xml-output of calling functions ------";
45 formula2xml 1 (TermC.str2term str);
48 (*TermC.str2term str; (* ERROR: Inner syntax error at "; 0 < ?n |] ==> ?a / ?b ^ ?n = ?a * ?b ^ - ?n"
49 Failed to TermC.parse term*)*)
50 "~~~~~ fun TermC.str2term, args:"; val (str) = (str);
51 ThyC.get_theory "Isac_Knowledge";
54 TermC.parse_patt (ThyC.get_theory "Isac_Knowledge");
55 (*TermC.parse_patt (ThyC.get_theory "Isac_Knowledge") str; (* ERROR: Inner syntax error at "; 0 < ?n |] ==> ?a / ?b ^ ?n = ?a * ?b ^ - ?n"
56 Failed to TermC.parse term*)*)
58 "~~~~~ fun TermC.parse_patt, args:"; val (thy, str) = ((ThyC.get_theory "Isac_Knowledge"), str);
61 (*|-> Proof_Context.read_term_pattern (*ERROR: Inner syntax error at "; 0 < ?n |] ==> ?a / ?b ^ ?n = ?a * ?b ^ - ?n"
62 Failed to TermC.parse term*)*)
64 Proof_Context.read_term_pattern;
65 (@{theory "Isac_Knowledge"}, str) |>> ThyC.to_ctxt;
66 "~~~~~ fun Proof_Context.read_term_pattern, args:"; val () = ();
67 (*AK110725 To be continued...*)
69 (*==================================================================*)
70 "-----------------------------------------------------------------";
71 "exported from struct --------------------------------------------";
72 "-----------------------------------------------------------------";
73 ========== inhibit exn AK110725 ================================================*)
75 "--------- fun rm_doublets '-4 * b ^^^^^^^^^ 2 / (...' -----------";
76 "--------- fun rm_doublets '-4 * b ^^^^^^^^^ 2 / (...' -----------";
77 "--------- fun rm_doublets '-4 * b ^^^^^^^^^ 2 / (...' -----------";
79 val cs = ["^", "^", "^", "d", "e"];
80 if rm_doublets c [] cs = Symbol.explode "^de"
81 then () else error "rm_doublets '^^^de' CHANGED";
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";
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";
94 "--------- fun decode '-4 * b ^^^^^^^^^ 2 / (...' ----------------";
95 "--------- fun decode '-4 * b ^^^^^^^^^ 2 / (...' ----------------";
96 "--------- fun decode '-4 * b ^^^^^^^^^ 2 / (...' ----------------";
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";
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;
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";
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"
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) $
131 Const ("processed_by_Isabelle_Isac", _) = ttt;
133 (* check the type structure *)
135 Type ("Real.real", []);
140 *** . Type (Real.real,[])
142 *** . . Type (Real.real,[])
143 *** . . Type (Real.real,[])
146 with this ^^^ build the typ ...*)
148 Type ("Real.real", []),
150 Type ("Real.real", []),
151 Type ("Real.real", [])])]);
156 *** . Type (Real.real,[])
158 *** . . Type (Real.real,[])
159 *** . . Type (HOL.bool,[])
162 with this ^^^ build the typ ...*)
164 Type ("Real.real", []),
166 Type ("Real.real", []),
167 Type ("HOL.bool", [])])]);
169 (* now compose term + typ *)
170 val Const ("HOL.eq", Type ("fun", [
171 Type ("Real.real", []),
173 Type ("Real.real", []),
174 Type ("HOL.bool", [])])])) $
175 (Const ("Groups.plus_class.plus", Type ("fun", [
176 Type ("Real.real", []),
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;
184 (* match out the original term from result*)
185 val Const ("HOL.eq", Type ("fun", [
186 Type ("Real.real", []),
188 Type ("Real.real", []),
189 Type ("HOL.bool", [])])])) $
191 Const ("processed_by_Isabelle_Isac", Type ("Real.real", [])) = ttt;
192 if t = t' then () else error "something with test_term changed"