1 (* Title: BaseDefinitions/calcelems.sml
2 Author: Walther Neuper 060113
3 (c) due to copyright terms
6 "--------------------------------------------------------";
7 "--------------------------------------------------------";
8 "table of contents --------------------------------------";
9 "--------------------------------------------------------";
10 "-------- Unsynchronized.ref doesn't work any more ------";
11 "-------- fun ThmC.cut_id ------------------";
12 "-------- fun UnparseC.term ----------------------------------";
13 "-------- fun ThmC.cut_id 000---------------";
14 "-------- fun Rule_Set.merge -----------------------------------------------------";
15 "-------- fun update_ptyps --------------------------------------------------";
16 "-------- fun subst2str' -----------------------------------------------------------------------";
17 "--------------------------------------------------------";
18 "--------------------------------------------------------";
19 "--------------------------------------------------------";
21 "-------- Unsynchronized.ref doesn't work any more ------";
22 "-------- Unsynchronized.ref doesn't work any more ------";
23 "-------- Unsynchronized.ref doesn't work any more ------";
24 (* this code resembles what would be needed to intermediately save original data ... *)
26 val ref_ = Unsynchronized.ref "original-data";
27 (* save intermediately *) val val_ = ! ref_;
29 (* restore original *) ref_ := val_;
30 if ! ref_ = "original-data"
31 then writeln "~~~~~ that's what we want"
32 else writeln "===== why not original ?";
34 (* ... which works in this simple case. But the same did not work with
35 --- fun insert_errpats ---, see changeset 90f3855dee3b *)
38 "-------- fun ThmC.cut_id ----------------";
39 "-------- fun ThmC.cut_id ----------------";
40 "-------- fun ThmC.cut_id ----------------";
41 val thm = @{thm radd_0};
42 val dn = Thm.derivation_name thm;
43 if dn = "Test.radd_0" then ()
44 else error "calcelems.sml Thm.derivation_name changed 1";
46 val thmID = ThmC.cut_id dn;
47 val thyID = ThyC.cut_id dn;
48 if thmID = "radd_0" andalso thyID = "Test" then ()
49 else error "calcelems.sml Thm.derivation_name changed 2";
52 val thm = @{thm add_divide_distrib}
53 val dn = Thm.derivation_name thm;
54 val thmID = ThmC.cut_id dn;
55 val thyID = ThyC.cut_id dn;
56 if thmID = "add_divide_distrib" andalso thyID = "Fields" then ()
57 else error "calcelems.sml Thm.derivation_name changed 3";
59 "-------- fun UnparseC.term ----------------------------------";
60 "-------- fun UnparseC.term ----------------------------------";
61 "-------- fun UnparseC.term ----------------------------------";
62 (*Quick notes from Makarius.1003
66 term "(1.24444) :: real"
68 ThmC_Def.num_to_Free @{term "%x. (-9993::int) + x + 1"}
70 Toplevel.debug := true;
73 PolyML.addPrettyPrinter
74 (fn _ => fn _ => ml_pretty o Pretty.to_ML o raw_pp_typ);
77 PolyML.addPrettyPrinter
78 (fn _ => fn _ => ml_pretty o Pretty.to_ML o Proof_Display.pp_typ Pure.thy);
79 (*default_print_depth 3;*)
82 "-------- fun ThmC.cut_id 000---------------";
83 "-------- fun ThmC.cut_id 000---------------";
84 "-------- fun ThmC.cut_id 000---------------";
85 val long_id = Thm.get_name_hint @{thm mult_1_left};
86 if long_id = "Groups.monoid_mult_class.mult_1_left" then ()
87 else error "fun Thm.get_name_hint or @{thm mult_1_left} changed";
89 if ThmC.cut_id long_id = "mult_1_left" then ()
90 else error "fun ThmC.cut_id broken";
92 if ThyC.cut_id long_id = "Groups" then ()
93 else error "fun ThyC.cut_id broken";
95 "-------- fun Rule_Set.merge -----------------------------------------------------";
96 "-------- fun Rule_Set.merge -----------------------------------------------------";
97 "-------- fun Rule_Set.merge -----------------------------------------------------";
98 (*theory Thy_2 imports Thy_1*)
99 val rlss2 = [("test_list_rls", (Context.theory_name @{theory},
100 Rule_Set.append_rules "test_list_rls" Rule_Set.empty [Thm ("refl", @{thm refl}), Thm ("subst", @{thm subst})]))]
101 (*theory Thy_2b imports Thy_1*)
102 val rlss2b = [("test_list_rls", (Context.theory_name @{theory},
103 Rule_Set.append_rules "test_list_rls" Rule_Set.empty [Thm ("False_def", @{thm False_def})]))]
105 val [(_, (_, Rule_Set.Repeat {rules, ...}))] = Rule_Set.to_kestore (rlss2, rlss2b)
108 [Thm ("subst", _), Thm ("refl", _), Thm ("False_def", _)] => ()
109 | _ => error "Rule_Set.merge changed"
111 "-------- fun update_ptyps --------------------------------------------------";
112 "-------- fun update_ptyps --------------------------------------------------";
113 "-------- fun update_ptyps --------------------------------------------------";
115 Store.Node ("aaa", [1], [
116 Store.Node ("aaa-1", [11], [])]),
117 Store.Node ("bbb", [2], [
118 Store.Node ("bbb-1", [21], []),
119 Store.Node ("bbb-2", [22], [
120 Store.Node ("bbb-21", [221], []),
121 Store.Node ("bbb-22", [222], [])])]),
122 Store.Node ("ccc", [3], [])] : int Store.T
125 (*update_ptyps ID ID 99999 pty; ERROR update_ptyps: [aaa] does not exist*)
128 if Store.update ID ID 99999 pty =
129 [Store.Node ("aaa", [1], [Store.Node ("aaa-1", [11], [])]),
130 Store.Node ("bbb", [2], [Store.Node ("bbb-1", [21], []),
131 Store.Node ("bbb-2", [22], [Store.Node ("bbb-21", [221], []), Store.Node ("bbb-22", [222], [])])]),
132 Store.Node ("ccc", [99999], [])]
133 then () else error "update_ptyps has changed 1";
136 (*update_ptyps ID ID 99999 pty; ERROR update_ptyps: [aaa] has descendants*)
138 val ID = ["bbb", "bbb-2", "bbb-21"];
139 if Store.update ID ID 99999 pty =
140 [Store.Node ("aaa", [1], [Store.Node ("aaa-1", [11], [])]),
141 Store.Node ("bbb", [2], [Store.Node ("bbb-1", [21], []), Store.Node ("bbb-2", [22],
142 [Store.Node ("bbb-21", [99999], []), Store.Node ("bbb-22", [222], [])])]),
143 Store.Node ("ccc", [3], [])]
144 then () else error "update_ptyps has changed 2";
146 val ID = ["bbb", "bbb-2", "bbb-22"];
147 if Store.update ID ID 99999 pty =
148 [Store.Node ("aaa", [1], [Store.Node ("aaa-1", [11], [])]),
149 Store.Node ("bbb", [2], [Store.Node ("bbb-1", [21], []),
150 Store.Node ("bbb-2", [22], [Store.Node ("bbb-21", [221], []), Store.Node ("bbb-22", [99999], [])])]),
151 Store.Node ("ccc", [3], [])]
152 then () else error "update_ptyps has changed 3";
154 "----------- fun subst2str' --------------------------------------------------------------------";
155 "----------- fun subst2str' --------------------------------------------------------------------";
156 "----------- fun subst2str' --------------------------------------------------------------------";
157 (*> subst2str' [(TermC.parse_test @{context} "bdv", TermC.parse_test @{context} "x"),
158 (TermC.parse_test @{context} "bdv_2", TermC.parse_test @{context} "y")];
159 val it = "[(bdv, x)]" : string