1 (* tests for sml/calcelems.sml
2 author: Walther Neuper 060113
5 "--------------------------------------------------------";
6 "--------------------------------------------------------";
7 "table of contents --------------------------------------";
8 "--------------------------------------------------------";
9 "-------- Unsynchronized.ref doesn't work any more ------";
10 "-------- fun thmID_of_derivation_name ------------------";
11 "-------- fun term2str ----------------------------------";
12 "-------- fun thmID_of_derivation_name 000---------------";
13 "-------- fun merge_rlss -----------------------------------------------------";
14 "-------- fun update_ptyps --------------------------------------------------";
15 "--------------------------------------------------------";
16 "--------------------------------------------------------";
17 "--------------------------------------------------------";
19 "-------- Unsynchronized.ref doesn't work any more ------";
20 "-------- Unsynchronized.ref doesn't work any more ------";
21 "-------- Unsynchronized.ref doesn't work any more ------";
22 (* this code resembles what would be needed to intermediately save original data ... *)
24 val ref_ = Unsynchronized.ref "original-data";
25 (* save intermediately *) val val_ = ! ref_;
27 (* restore original *) ref_ := val_;
28 if ! ref_ = "original-data"
29 then writeln "~~~~~ that's what we want"
30 else writeln "===== why not original ?";
32 (* ... which works in this simple case. But the same did not work with
33 --- fun insert_errpats ---, see changeset 90f3855dee3b *)
36 "-------- fun thmID_of_derivation_name ----------------";
37 "-------- fun thmID_of_derivation_name ----------------";
38 "-------- fun thmID_of_derivation_name ----------------";
39 val thm = @{thm radd_0};
40 val dn = Thm.derivation_name thm;
41 if dn = "Test.radd_0" then ()
42 else error "calcelems.sml Thm.derivation_name changed 1";
44 val thmID = thmID_of_derivation_name dn;
45 val thyID = thyID_of_derivation_name dn;
46 if thmID = "radd_0" andalso thyID = "Test" then ()
47 else error "calcelems.sml Thm.derivation_name changed 2";
50 val thm = @{thm add_divide_distrib}
51 val dn = Thm.derivation_name thm;
52 val thmID = thmID_of_derivation_name dn;
53 val thyID = thyID_of_derivation_name dn;
54 if thmID = "add_divide_distrib" andalso thyID = "Fields" then ()
55 else error "calcelems.sml Thm.derivation_name changed 3";
57 "-------- fun term2str ----------------------------------";
58 "-------- fun term2str ----------------------------------";
59 "-------- fun term2str ----------------------------------";
60 (*Quick notes from Makarius.1003
64 term "(1.24444) :: real"
66 numbers_to_string @{term "%x. (-9993::int) + x + 1"}
68 Toplevel.debug := true;
71 PolyML.addPrettyPrinter
72 (fn _ => fn _ => ml_pretty o Pretty.to_ML o raw_pp_typ);
75 PolyML.addPrettyPrinter
76 (fn _ => fn _ => ml_pretty o Pretty.to_ML o Proof_Display.pp_typ Pure.thy);
77 (*default_print_depth 3;*)
79 "===== extend parse to string with markup===";
82 (let val t = (typ_a2real o numbers_to_string)
83 (Syntax.read_term_global thy str)
84 in SOME (Thm.global_cterm_of thy t) end) (*FIXXXXME 10.8.02: return term !!!*)
88 "-------- fun thmID_of_derivation_name 000---------------";
89 "-------- fun thmID_of_derivation_name 000---------------";
90 "-------- fun thmID_of_derivation_name 000---------------";
91 val long_id = Thm.get_name_hint @{thm mult_1_left};
92 if long_id = "Groups.monoid_mult_class.mult_1_left" then ()
93 else error "fun Thm.get_name_hint or @{thm mult_1_left} changed";
95 if thmID_of_derivation_name long_id = "mult_1_left" then ()
96 else error "fun thmID_of_derivation_name broken";
98 if thyID_of_derivation_name long_id = "Groups" then ()
99 else error "fun thyID_of_derivation_name broken";
101 "-------- fun merge_rlss -----------------------------------------------------";
102 "-------- fun merge_rlss -----------------------------------------------------";
103 "-------- fun merge_rlss -----------------------------------------------------";
104 (*theory Thy_2 imports Thy_1*)
105 val rlss2 = [("test_list_rls", (Context.theory_name @{theory},
106 append_rls "test_list_rls" e_rls [Thm ("refl", @{thm refl}), Thm ("subst", @{thm subst})]))]
107 (*theory Thy_2b imports Thy_1*)
108 val rlss2b = [("test_list_rls", (Context.theory_name @{theory},
109 append_rls "test_list_rls" e_rls [Thm ("False_def", @{thm False_def})]))]
111 val [(_, (_, Rls {rules, ...}))] = merge_rlss (rlss2, rlss2b)
114 [Thm ("subst", _), Thm ("refl", _), Thm ("False_def", _)] => ()
115 | _ => error "merge_rlss changed"
117 "-------- fun update_ptyps --------------------------------------------------";
118 "-------- fun update_ptyps --------------------------------------------------";
119 "-------- fun update_ptyps --------------------------------------------------";
122 Ptyp ("aaa-1", [11], [])]),
124 Ptyp ("bbb-1", [21], []),
125 Ptyp ("bbb-2", [22], [
126 Ptyp ("bbb-21", [221], []),
127 Ptyp ("bbb-22", [222], [])])]),
128 Ptyp ("ccc", [3], [])] : int ptyp list
131 (*update_ptyps ID ID 99999 pty; ERROR update_ptyps: [aaa] does not exist*)
134 if update_ptyps ID ID 99999 pty =
135 [Ptyp ("aaa", [1], [Ptyp ("aaa-1", [11], [])]),
136 Ptyp ("bbb", [2], [Ptyp ("bbb-1", [21], []),
137 Ptyp ("bbb-2", [22], [Ptyp ("bbb-21", [221], []), Ptyp ("bbb-22", [222], [])])]),
138 Ptyp ("ccc", [99999], [])]
139 then () else error "update_ptyps has changed 1";
142 (*update_ptyps ID ID 99999 pty; ERROR update_ptyps: [aaa] has descendants*)
144 val ID = ["bbb", "bbb-2", "bbb-21"];
145 if update_ptyps ID ID 99999 pty =
146 [Ptyp ("aaa", [1], [Ptyp ("aaa-1", [11], [])]),
147 Ptyp ("bbb", [2], [Ptyp ("bbb-1", [21], []), Ptyp ("bbb-2", [22],
148 [Ptyp ("bbb-21", [99999], []), Ptyp ("bbb-22", [222], [])])]),
149 Ptyp ("ccc", [3], [])]
150 then () else error "update_ptyps has changed 2";
152 val ID = ["bbb", "bbb-2", "bbb-22"];
153 if update_ptyps ID ID 99999 pty =
154 [Ptyp ("aaa", [1], [Ptyp ("aaa-1", [11], [])]),
155 Ptyp ("bbb", [2], [Ptyp ("bbb-1", [21], []),
156 Ptyp ("bbb-2", [22], [Ptyp ("bbb-21", [221], []), Ptyp ("bbb-22", [99999], [])])]),
157 Ptyp ("ccc", [3], [])]
158 then () else error "update_ptyps has changed 3";