1 (* Title: tests for mathml.sml
2 Author: Walther Neuper 060311
5 "-----------------------------------------------------------------";
6 "table of contents -----------------------------------------------";
7 "-----------------------------------------------------------------";
8 "within struct ---------------------------------------------------";
9 "-----------------------------------------------------------------";
10 "--------- fun xml_of_term_NEW, xml_to_term_NEW ------------------";
11 "--------- create testdata for TestPIDE.java#testTermTransfer ----";
12 "-----------------------------------------------------------------";
13 "exported from struct --------------------------------------------";
14 "-----------------------------------------------------------------";
15 "--------- ... ---------------------------------------------------";
16 "-----------------------------------------------------------------";
20 "-----------------------------------------------------------------";
21 "within struct ---------------------------------------------------";
22 "-----------------------------------------------------------------";
23 (*==================================================================*)
26 "--------- fun xmlstr --------------------------------------------";
27 "--------- fun xmlstr --------------------------------------------";
28 "--------- fun xmlstr --------------------------------------------";
29 val term = @{term "aaa + bbb::real"};
30 val str = term |> xml_of_term_NEW |> xmlstr 0;
32 "(FORMULA)\n. (ISA)\n. . aaa + bbb\n. (/ISA)\n. (TERM)\n aaa + bbb\n(/TERM)\n(/FORMULA)\n"
33 then () else error "term |> xml_of_term_NEW |> xmlstr ..changed";
36 "--------- fun xml_of_term_NEW, xml_to_term_NEW ------------------";
37 "--------- fun xml_of_term_NEW, xml_to_term_NEW ------------------";
38 "--------- fun xml_of_term_NEW, xml_to_term_NEW ------------------";
39 (* xml_of_term_NEW o xml_to_term_NEW = id ... not valid,
40 as long as the latter (going: frontend \<longrightarrow> kernel) does only carry "ISA" string.
41 val t = @{term "aaa + bbb::real"};
42 if t = (t |> xml_of_term_NEW |> xml_to_term_NEW) then ()
43 else error "xml_of_term_NEW |> xml_to_term_NEW changed"
46 "--------- create testdata for TestPIDE.java#testTermTransfer ----";
47 "--------- create testdata for TestPIDE.java#testTermTransfer ----";
48 "--------- create testdata for TestPIDE.java#testTermTransfer ----";
49 val t = @{term "aaa + bbb::real"};
50 val ttt = HOLogic.mk_eq (t, Const ("processed_by_Isabelle_Isac", type_of t))
51 (* check the term structure *)
52 val Const (\<^const_name>\<open>HOL.eq\<close>, T1) $
53 (Const (\<^const_name>\<open>plus\<close>, T2) $
56 Const ("processed_by_Isabelle_Isac", _) = ttt;
58 (* check the type structure *)
59 TermC.atom_typ @{context} T3;
60 Type (\<^type_name>\<open>real\<close>, []);
62 TermC.atom_typ @{context} T2;
65 *** . Type (Real.real,[])
67 *** . . Type (Real.real,[])
68 *** . . Type (Real.real,[])
71 with this \<up> build the typ ...*)
72 Type (\<^type_name>\<open>fun\<close>, [
73 Type (\<^type_name>\<open>real\<close>, []),
74 Type (\<^type_name>\<open>fun\<close>, [
75 Type (\<^type_name>\<open>real\<close>, []),
76 Type (\<^type_name>\<open>real\<close>, [])])]);
78 TermC.atom_typ @{context} T1;
81 *** . Type (Real.real,[])
83 *** . . Type (Real.real,[])
84 *** . . Type (HOL.bool,[])
87 with this \<up> build the typ ...*)
88 Type (\<^type_name>\<open>fun\<close>, [
89 Type (\<^type_name>\<open>real\<close>, []),
90 Type (\<^type_name>\<open>fun\<close>, [
91 Type (\<^type_name>\<open>real\<close>, []),
92 Type (\<^type_name>\<open>bool\<close>, [])])]);
94 (* now compose term + typ *)
95 val Const (\<^const_name>\<open>HOL.eq\<close>, Type (\<^type_name>\<open>fun\<close>, [
96 Type (\<^type_name>\<open>real\<close>, []),
97 Type (\<^type_name>\<open>fun\<close>, [
98 Type (\<^type_name>\<open>real\<close>, []),
99 Type (\<^type_name>\<open>bool\<close>, [])])])) $
100 (Const (\<^const_name>\<open>plus\<close>, Type (\<^type_name>\<open>fun\<close>, [
101 Type (\<^type_name>\<open>real\<close>, []),
102 Type (\<^type_name>\<open>fun\<close>, [
103 Type (\<^type_name>\<open>real\<close>, []),
104 Type (\<^type_name>\<open>real\<close>, [])])])) $
105 Free ("aaa", Type (\<^type_name>\<open>real\<close>, [])) $
106 Free ("bbb", Type (\<^type_name>\<open>real\<close>, []))) $
107 Const ("processed_by_Isabelle_Isac", Type (\<^type_name>\<open>real\<close>, [])) = ttt;
109 (* match out the original term from result*)
110 val Const (\<^const_name>\<open>HOL.eq\<close>, Type (\<^type_name>\<open>fun\<close>, [
111 Type (\<^type_name>\<open>real\<close>, []),
112 Type (\<^type_name>\<open>fun\<close>, [
113 Type (\<^type_name>\<open>real\<close>, []),
114 Type (\<^type_name>\<open>bool\<close>, [])])])) $
116 Const ("processed_by_Isabelle_Isac", Type (\<^type_name>\<open>real\<close>, [])) = ttt;
117 if t = t' then () else error "something with test_term changed"