|
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 |
"-----------------------------------------------------------------";
|
|
wneuper@59213
|
10 |
"--------- fun xml_of_term_NEW, xml_to_term_NEW ------------------";
|
|
wneuper@59214
|
11 |
"--------- create testdata for TestPIDE.java#testTermTransfer ----";
|
|
neuper@37906
|
12 |
"-----------------------------------------------------------------";
|
|
neuper@37906
|
13 |
"exported from struct --------------------------------------------";
|
|
neuper@37906
|
14 |
"-----------------------------------------------------------------";
|
|
neuper@37906
|
15 |
"--------- ... ---------------------------------------------------";
|
|
neuper@37906
|
16 |
"-----------------------------------------------------------------";
|
|
neuper@37906
|
17 |
|
|
neuper@37906
|
18 |
|
|
neuper@37906
|
19 |
|
|
neuper@37906
|
20 |
"-----------------------------------------------------------------";
|
|
neuper@37906
|
21 |
"within struct ---------------------------------------------------";
|
|
neuper@37906
|
22 |
"-----------------------------------------------------------------";
|
|
neuper@37906
|
23 |
(*==================================================================*)
|
|
neuper@37906
|
24 |
|
|
wneuper@59177
|
25 |
|
|
wneuper@59224
|
26 |
"--------- fun xmlstr --------------------------------------------";
|
|
wneuper@59224
|
27 |
"--------- fun xmlstr --------------------------------------------";
|
|
wneuper@59224
|
28 |
"--------- fun xmlstr --------------------------------------------";
|
|
wneuper@59224
|
29 |
val term = @{term "aaa + bbb::real"};
|
|
wneuper@59224
|
30 |
val str = term |> xml_of_term_NEW |> xmlstr 0;
|
|
wneuper@59224
|
31 |
if str =
|
|
walther@59617
|
32 |
"(FORMULA)\n. (ISA)\n. . aaa + bbb\n. (/ISA)\n. (TERM)\n aaa + bbb\n(/TERM)\n(/FORMULA)\n"
|
|
wneuper@59224
|
33 |
then () else error "term |> xml_of_term_NEW |> xmlstr ..changed";
|
|
wneuper@59224
|
34 |
writeln str;
|
|
wneuper@59224
|
35 |
|
|
wneuper@59213
|
36 |
"--------- fun xml_of_term_NEW, xml_to_term_NEW ------------------";
|
|
wneuper@59213
|
37 |
"--------- fun xml_of_term_NEW, xml_to_term_NEW ------------------";
|
|
wneuper@59213
|
38 |
"--------- fun xml_of_term_NEW, xml_to_term_NEW ------------------";
|
|
wneuper@59224
|
39 |
(* xml_of_term_NEW o xml_to_term_NEW = id ... not valid,
|
|
wneuper@59224
|
40 |
as long as the latter (going: frontend \<longrightarrow> kernel) does only carry "ISA" string.
|
|
wneuper@59213
|
41 |
val t = @{term "aaa + bbb::real"};
|
|
wneuper@59213
|
42 |
if t = (t |> xml_of_term_NEW |> xml_to_term_NEW) then ()
|
|
wneuper@59213
|
43 |
else error "xml_of_term_NEW |> xml_to_term_NEW changed"
|
|
wneuper@59224
|
44 |
*)
|
|
wneuper@59214
|
45 |
|
|
wneuper@59214
|
46 |
"--------- create testdata for TestPIDE.java#testTermTransfer ----";
|
|
wneuper@59214
|
47 |
"--------- create testdata for TestPIDE.java#testTermTransfer ----";
|
|
wneuper@59214
|
48 |
"--------- create testdata for TestPIDE.java#testTermTransfer ----";
|
|
wneuper@59214
|
49 |
val t = @{term "aaa + bbb::real"};
|
|
wneuper@59214
|
50 |
val ttt = HOLogic.mk_eq (t, Const ("processed_by_Isabelle_Isac", type_of t))
|
|
wneuper@59214
|
51 |
(* check the term structure *)
|
|
wenzelm@60309
|
52 |
val Const (\<^const_name>\<open>HOL.eq\<close>, T1) $
|
|
wenzelm@60309
|
53 |
(Const (\<^const_name>\<open>plus\<close>, T2) $
|
|
wneuper@59214
|
54 |
Free ("aaa", T3) $
|
|
wneuper@59214
|
55 |
Free ("bbb", _)) $
|
|
wneuper@59214
|
56 |
Const ("processed_by_Isabelle_Isac", _) = ttt;
|
|
wneuper@59214
|
57 |
|
|
wneuper@59214
|
58 |
(* check the type structure *)
|
|
Walther@60650
|
59 |
TermC.atom_typ @{context} T3;
|
|
wenzelm@60309
|
60 |
Type (\<^type_name>\<open>real\<close>, []);
|
|
wneuper@59214
|
61 |
|
|
Walther@60650
|
62 |
TermC.atom_typ @{context} T2;
|
|
wneuper@59214
|
63 |
(*
|
|
wneuper@59214
|
64 |
*** Type (fun,[
|
|
wneuper@59214
|
65 |
*** . Type (Real.real,[])
|
|
wneuper@59214
|
66 |
*** . Type (fun,[
|
|
wneuper@59214
|
67 |
*** . . Type (Real.real,[])
|
|
wneuper@59214
|
68 |
*** . . Type (Real.real,[])
|
|
wneuper@59214
|
69 |
*** . . ]
|
|
wneuper@59214
|
70 |
*** . ]
|
|
walther@60242
|
71 |
with this \<up> build the typ ...*)
|
|
wenzelm@60309
|
72 |
Type (\<^type_name>\<open>fun\<close>, [
|
|
wenzelm@60309
|
73 |
Type (\<^type_name>\<open>real\<close>, []),
|
|
wenzelm@60309
|
74 |
Type (\<^type_name>\<open>fun\<close>, [
|
|
wenzelm@60309
|
75 |
Type (\<^type_name>\<open>real\<close>, []),
|
|
wenzelm@60309
|
76 |
Type (\<^type_name>\<open>real\<close>, [])])]);
|
|
wneuper@59214
|
77 |
|
|
Walther@60650
|
78 |
TermC.atom_typ @{context} T1;
|
|
wneuper@59214
|
79 |
(*
|
|
wneuper@59214
|
80 |
*** Type (fun,[
|
|
wneuper@59214
|
81 |
*** . Type (Real.real,[])
|
|
wneuper@59214
|
82 |
*** . Type (fun,[
|
|
wneuper@59214
|
83 |
*** . . Type (Real.real,[])
|
|
wneuper@59214
|
84 |
*** . . Type (HOL.bool,[])
|
|
wneuper@59214
|
85 |
*** . . ]
|
|
wneuper@59214
|
86 |
*** . ]
|
|
walther@60242
|
87 |
with this \<up> build the typ ...*)
|
|
wenzelm@60309
|
88 |
Type (\<^type_name>\<open>fun\<close>, [
|
|
wenzelm@60309
|
89 |
Type (\<^type_name>\<open>real\<close>, []),
|
|
wenzelm@60309
|
90 |
Type (\<^type_name>\<open>fun\<close>, [
|
|
wenzelm@60309
|
91 |
Type (\<^type_name>\<open>real\<close>, []),
|
|
wenzelm@60309
|
92 |
Type (\<^type_name>\<open>bool\<close>, [])])]);
|
|
wneuper@59214
|
93 |
|
|
wneuper@59214
|
94 |
(* now compose term + typ *)
|
|
wenzelm@60309
|
95 |
val Const (\<^const_name>\<open>HOL.eq\<close>, Type (\<^type_name>\<open>fun\<close>, [
|
|
wenzelm@60309
|
96 |
Type (\<^type_name>\<open>real\<close>, []),
|
|
wenzelm@60309
|
97 |
Type (\<^type_name>\<open>fun\<close>, [
|
|
wenzelm@60309
|
98 |
Type (\<^type_name>\<open>real\<close>, []),
|
|
wenzelm@60309
|
99 |
Type (\<^type_name>\<open>bool\<close>, [])])])) $
|
|
wenzelm@60309
|
100 |
(Const (\<^const_name>\<open>plus\<close>, Type (\<^type_name>\<open>fun\<close>, [
|
|
wenzelm@60309
|
101 |
Type (\<^type_name>\<open>real\<close>, []),
|
|
wenzelm@60309
|
102 |
Type (\<^type_name>\<open>fun\<close>, [
|
|
wenzelm@60309
|
103 |
Type (\<^type_name>\<open>real\<close>, []),
|
|
wenzelm@60309
|
104 |
Type (\<^type_name>\<open>real\<close>, [])])])) $
|
|
wenzelm@60309
|
105 |
Free ("aaa", Type (\<^type_name>\<open>real\<close>, [])) $
|
|
wenzelm@60309
|
106 |
Free ("bbb", Type (\<^type_name>\<open>real\<close>, []))) $
|
|
wenzelm@60309
|
107 |
Const ("processed_by_Isabelle_Isac", Type (\<^type_name>\<open>real\<close>, [])) = ttt;
|
|
wneuper@59214
|
108 |
|
|
wneuper@59214
|
109 |
(* match out the original term from result*)
|
|
wenzelm@60309
|
110 |
val Const (\<^const_name>\<open>HOL.eq\<close>, Type (\<^type_name>\<open>fun\<close>, [
|
|
wenzelm@60309
|
111 |
Type (\<^type_name>\<open>real\<close>, []),
|
|
wenzelm@60309
|
112 |
Type (\<^type_name>\<open>fun\<close>, [
|
|
wenzelm@60309
|
113 |
Type (\<^type_name>\<open>real\<close>, []),
|
|
wenzelm@60309
|
114 |
Type (\<^type_name>\<open>bool\<close>, [])])])) $
|
|
wneuper@59214
|
115 |
t' $
|
|
wenzelm@60309
|
116 |
Const ("processed_by_Isabelle_Isac", Type (\<^type_name>\<open>real\<close>, [])) = ttt;
|
|
wneuper@59214
|
117 |
if t = t' then () else error "something with test_term changed"
|