neuper@37871
|
1 |
(* tests for sml/xmlsrc/thy-hierarchy.sml
|
neuper@37871
|
2 |
authors: Walther Neuper 060113
|
neuper@37871
|
3 |
(c) due to copyright terms
|
neuper@37871
|
4 |
|
neuper@37871
|
5 |
use"../smltest/xmlsrc/thy-hierarchy.sml";
|
neuper@37871
|
6 |
use"thy-hierarchy.sml";
|
neuper@37871
|
7 |
|
neuper@37871
|
8 |
CAUTION with testing *2file functions -- they are actually writing to ~/tmp
|
neuper@37871
|
9 |
*)
|
neuper@37871
|
10 |
|
neuper@37871
|
11 |
val thy = Isac.thy;
|
neuper@37871
|
12 |
|
neuper@37871
|
13 |
"-----------------------------------------------------------------";
|
neuper@37871
|
14 |
"table of contents -----------------------------------------------";
|
neuper@37871
|
15 |
"-----------------------------------------------------------------";
|
neuper@37871
|
16 |
"----------- assoc_rls -------------------------------------------";
|
neuper@37871
|
17 |
"----------- thm_hier --------------------------------------------";
|
neuper@37871
|
18 |
"----------- fun thydata2xml -------------------------------------";
|
neuper@37871
|
19 |
"----------- write xml to tmp ------------------------------------";
|
neuper@37871
|
20 |
"----------- the_hier [] (collect_thyda.. NOT overwriting store_ -";
|
neuper@37871
|
21 |
"----------- ### thes2file ... Exception- Match raised -----------";
|
neuper@37871
|
22 |
"-----------------------------------------------------------------";
|
neuper@37871
|
23 |
"-----------------------------------------------------------------";
|
neuper@37871
|
24 |
"-----------------------------------------------------------------";
|
neuper@37871
|
25 |
|
neuper@37871
|
26 |
|
neuper@37871
|
27 |
"----------- assoc_rls -------------------------------------------";
|
neuper@37871
|
28 |
"----------- assoc_rls -------------------------------------------";
|
neuper@37871
|
29 |
"----------- assoc_rls -------------------------------------------";
|
neuper@37871
|
30 |
val al = [(1,11),(2,22),(3,33)];
|
neuper@37871
|
31 |
overwrite (al, (2,2222));
|
neuper@37871
|
32 |
(*val it = [(1, 11), (2, 2222), (3, 33)] : (int * int) list*)
|
neuper@37871
|
33 |
|
neuper@37871
|
34 |
val al = [("e_rls",("Atools",e_rls)),("e_rrls",("Atools",e_rrls))];
|
neuper@37871
|
35 |
val bl = [("e_rls",e_rls),("e_rrls",e_rrls)];
|
neuper@37871
|
36 |
val b = ("e_rls",("Atools",e_rrls));
|
neuper@37871
|
37 |
overwrite (al, b);
|
neuper@37871
|
38 |
overwritelthy thy (al, bl);
|
neuper@37871
|
39 |
|
neuper@37871
|
40 |
assoc' (!ruleset',"e_rls");
|
neuper@37871
|
41 |
assoc_rls "e_rls";
|
neuper@37871
|
42 |
|
neuper@37871
|
43 |
|
neuper@37871
|
44 |
"----------- thm_hier --------------------------------------------";
|
neuper@37871
|
45 |
"----------- thm_hier --------------------------------------------";
|
neuper@37871
|
46 |
"----------- thm_hier --------------------------------------------";
|
neuper@37871
|
47 |
(curry op:: "xxx") ["yyy","yyy","yyy"];
|
neuper@37871
|
48 |
map (curry op:: "xxx") [["yyy1"],["yyy2"],["yyy3"]];
|
neuper@37871
|
49 |
|
neuper@37871
|
50 |
val thy' = "Integrate";
|
neuper@37871
|
51 |
val thy = assoc_thy (thyID2theory' thy');
|
neuper@37871
|
52 |
|
neuper@37871
|
53 |
"collect_thms thy'------------------------------------------------";
|
neuper@37871
|
54 |
(thms_of thy);
|
neuper@37871
|
55 |
|
neuper@37871
|
56 |
(apfst single) ("Integrate.integral_var", integral_var);
|
neuper@37871
|
57 |
|
neuper@37871
|
58 |
(strip_thy o #1) ("Integrate.integral_var", integral_var);
|
neuper@37871
|
59 |
|
neuper@37871
|
60 |
(*cannot get this as arg from arg ^^^^^^^^^^^^^^^^*)
|
neuper@37871
|
61 |
("Integrate.integral_var", integral_var);
|
neuper@37871
|
62 |
(*thus new fun....*)
|
neuper@37871
|
63 |
|
neuper@37871
|
64 |
makeHthm ("IsacKnowledge",thy') ("Integrate.integral_var", integral_var);
|
neuper@37871
|
65 |
(makeHthm ("IsacKnowledge",thy')) ("Integrate.integral_var", integral_var);
|
neuper@37871
|
66 |
map (makeHthm ("IsacKnowledge",thy')) (thms_of thy);
|
neuper@37871
|
67 |
collect_thms' ("IsacKnowledge",thy');
|
neuper@37871
|
68 |
|
neuper@37871
|
69 |
"collect_rlss thy'------------------------------------------------";
|
neuper@37871
|
70 |
makeHrls "IsacKnowledge" ("integration_rules", (thy', integration_rules));
|
neuper@37871
|
71 |
|
neuper@37871
|
72 |
val thy' = "Test";
|
neuper@37871
|
73 |
val rlss = filter ((curry op= thy') o
|
neuper@37871
|
74 |
((#1 o #2):(rls' * (theory' * rls)) -> theory'))
|
neuper@37871
|
75 |
(!ruleset');
|
neuper@37871
|
76 |
collect_rlss ("IsacKnowledge",thy');
|
neuper@37871
|
77 |
|
neuper@37871
|
78 |
"collect_thy thy-------------------------------------------------";
|
neuper@37871
|
79 |
val thy' = "ListG.thy";
|
neuper@37871
|
80 |
val thy = assoc_thy (thyID2theory' thy');
|
neuper@37871
|
81 |
((collect_thms' ("IsacKnowledge",thy')) @
|
neuper@37871
|
82 |
(collect_rlss ("IsacKnowledge",thy')) @
|
neuper@37871
|
83 |
(collect_cals ("IsacKnowledge",thy')) @
|
neuper@37871
|
84 |
(collect_ords ("IsacKnowledge",thy')));
|
neuper@37871
|
85 |
collect_thy "IsacKnowledge" thy';
|
neuper@37871
|
86 |
|
neuper@37871
|
87 |
"collect_thydata -------------------------------------------------";
|
neuper@37871
|
88 |
(!isab_thm_thy);
|
neuper@37871
|
89 |
map rearrange_inv (!isab_thm_thy);
|
neuper@37871
|
90 |
(map ((apfst ((curry op:: "Isabelle") o single)) o rearrange_inv));
|
neuper@37871
|
91 |
(map ((apfst ((curry op:: "Isabelle") o single)) o rearrange_inv))
|
neuper@37871
|
92 |
(!isab_thm_thy);
|
neuper@37871
|
93 |
|
neuper@37871
|
94 |
|
neuper@37871
|
95 |
"thy_hierarchy ---------------------------------------------------";
|
neuper@37871
|
96 |
val theID = ["IsacScripts", "ListG", "Theorems", "append_Cons"]:theID;
|
neuper@37871
|
97 |
val thydat as (theID, thydata) =
|
neuper@37871
|
98 |
(theID, Hthm {guh=theID2guh theID, mathauthors=[],
|
neuper@37871
|
99 |
coursedesign=[], thm=append_Cons});
|
neuper@37871
|
100 |
|
neuper@37871
|
101 |
val th = [] : thehier;
|
neuper@37871
|
102 |
val theID' = cut_theID th theID;
|
neuper@37871
|
103 |
val th = fill_parents th theID' theID;
|
neuper@37871
|
104 |
(* val th =
|
neuper@37871
|
105 |
[Ptyp ("IsacScripts",
|
neuper@37871
|
106 |
[Html {guh = "thy_ListG-thm-append_Cons", html = "", ...}],
|
neuper@37871
|
107 |
[Ptyp ("ListG", ...)])] : thehier *)
|
neuper@37871
|
108 |
(*show_thes*)(writeln o format_pblIDl o (scan [])) th;
|
neuper@37871
|
109 |
writeln (hierarchy_guh th);
|
neuper@37871
|
110 |
|
neuper@37871
|
111 |
val th = [] : thehier;
|
neuper@37871
|
112 |
val thydats = collect_thydata ();
|
neuper@37871
|
113 |
val th1 = the_hier th thydats (**** insert: not found [".. from fill_parents*);
|
neuper@37871
|
114 |
(*show_thes*)(writeln o format_pblIDl o (scan [])) th1;
|
neuper@37871
|
115 |
|
neuper@37871
|
116 |
writeln (hierarchy_guh th);
|
neuper@37871
|
117 |
writeln (hierarchy_guh th1);
|
neuper@37871
|
118 |
|
neuper@37871
|
119 |
"thy_hierarchy2file ----------------------------------------------";
|
neuper@37871
|
120 |
show_thes();
|
neuper@37871
|
121 |
(*
|
neuper@37871
|
122 |
val path = "/home/neuper/tmp/";
|
neuper@37871
|
123 |
thy_hierarchy2file path;
|
neuper@37871
|
124 |
*)
|
neuper@37871
|
125 |
|
neuper@37871
|
126 |
get_the ["IsacKnowledge"];
|
neuper@37871
|
127 |
get_the ["IsacKnowledge", "Test"];
|
neuper@37871
|
128 |
get_the ["IsacKnowledge", "Test", "Theorems"];
|
neuper@37871
|
129 |
get_the ["IsacKnowledge", "Test", "Theorems", "exp_pow"];
|
neuper@37871
|
130 |
|
neuper@37871
|
131 |
get_the ["IsacKnowledge", "Test", "Rulesets"];
|
neuper@37871
|
132 |
|
neuper@37871
|
133 |
(* FIXXXXXXXXXME.WN060713 guh -- theID
|
neuper@37871
|
134 |
case get_the ["IsacKnowledge", "Test", "Rulesets", "Test_simplify"] of
|
neuper@37871
|
135 |
Hrls {guh = "thy_Test-rls-Test_simplify",thy_rls = ("Test", _),
|
neuper@37871
|
136 |
mathauthors = _,coursedesign = _} => ()
|
neuper@37871
|
137 |
| _ => raise error "thy-hierarchy.sml: [IsacKnowledge,Test,Rulesets]";
|
neuper@37871
|
138 |
*)
|
neuper@37871
|
139 |
|
neuper@37871
|
140 |
|
neuper@37871
|
141 |
"----------- fun thydata2xml -------------------------------------";
|
neuper@37871
|
142 |
"----------- fun thydata2xml -------------------------------------";
|
neuper@37871
|
143 |
"----------- fun thydata2xml -------------------------------------";
|
neuper@37871
|
144 |
val theID = ["IsacScripts", "ListG", "Theorems", "append_Cons"];
|
neuper@37871
|
145 |
val thmdata = get_the theID;
|
neuper@37871
|
146 |
writeln(thydata2xml (theID, thmdata));
|
neuper@37871
|
147 |
|
neuper@37871
|
148 |
val theID = ["IsacKnowledge", "Poly", "Rulesets", "norm_Poly"];
|
neuper@37871
|
149 |
val rlsdata = get_the theID;
|
neuper@37871
|
150 |
writeln(thydata2xml (theID, rlsdata));
|
neuper@37871
|
151 |
|
neuper@37871
|
152 |
(*FIXXXXXXXME.WN060714 in rls make Calc : calc -> rule [add scriptop!]
|
neuper@37871
|
153 |
see sml/../datatypes.sml !
|
neuper@37871
|
154 |
val (thy', rls') = ("DiffApp.thy", "Tools.rhs");
|
neuper@37871
|
155 |
thy_containing_rls thy' rls';
|
neuper@37871
|
156 |
print_depth 99; map #1 startsearch; print_depth 3;
|
neuper@37871
|
157 |
*)
|
neuper@37871
|
158 |
|
neuper@37871
|
159 |
(*
|
neuper@37871
|
160 |
val path = "/home/neuper/tmp/";
|
neuper@37871
|
161 |
thes2file path;
|
neuper@37871
|
162 |
*)
|
neuper@37871
|
163 |
|
neuper@37871
|
164 |
"----------- write xml to tmp ------------------------------------";
|
neuper@37871
|
165 |
"----------- write xml to tmp ------------------------------------";
|
neuper@37871
|
166 |
"----------- write xml to tmp ------------------------------------";
|
neuper@37871
|
167 |
(*
|
neuper@37871
|
168 |
val path = "/home/neuper/tmp/";
|
neuper@37871
|
169 |
|
neuper@37871
|
170 |
pbl_hierarchy2file (path ^ "pbl/");
|
neuper@37871
|
171 |
pbls2file (path ^ "pbl/");
|
neuper@37871
|
172 |
|
neuper@37871
|
173 |
met_hierarchy2file (path ^ "met/");
|
neuper@37871
|
174 |
mets2file (path ^ "met/");
|
neuper@37871
|
175 |
|
neuper@37871
|
176 |
thy_hierarchy2file (path ^ "thy/");
|
neuper@37871
|
177 |
thes2file (path ^ "thy/");
|
neuper@37871
|
178 |
*)
|
neuper@37871
|
179 |
|
neuper@37871
|
180 |
|
neuper@37871
|
181 |
"----------- the_hier [] (collect_thyda.. NOT overwriting store_ -";
|
neuper@37871
|
182 |
"----------- the_hier [] (collect_thyda.. NOT overwriting store_ -";
|
neuper@37871
|
183 |
"----------- the_hier [] (collect_thyda.. NOT overwriting store_ -";
|
neuper@37871
|
184 |
(*
|
neuper@37871
|
185 |
store_isa ["Isabelle"] ["THIS SHOULD not BE OBERWRITTEN below"];
|
neuper@37871
|
186 |
print_depth 99; get_the ["Isabelle"]; print_depth 3;
|
neuper@37871
|
187 |
print_depth 5; thehier; print_depth 3;
|
neuper@37871
|
188 |
|
neuper@37871
|
189 |
thehier := the_hier (!thehier) (collect_thydata ());
|
neuper@37871
|
190 |
print_depth 99; get_the ["Isabelle"]; print_depth 3;
|
neuper@37871
|
191 |
print_depth 5; thehier; print_depth 3;
|
neuper@37871
|
192 |
*)
|
neuper@37871
|
193 |
|
neuper@37871
|
194 |
case get_the ["IsacKnowledge", "Biegelinie", "Theorems"] of
|
neuper@37871
|
195 |
Html {mathauthors =
|
neuper@37871
|
196 |
["Walther Neuper 2005 supported by a grant from NMI Austria"],...}=>()
|
neuper@37871
|
197 |
| _ => raise error "thy-hierarchy.sml: store_isa overwritten";
|
neuper@37871
|
198 |
|
neuper@37871
|
199 |
case get_the ["IsacKnowledge","Biegelinie","Theorems","Belastung_Querkraft"] of
|
neuper@37871
|
200 |
Hthm {mathauthors =
|
neuper@37871
|
201 |
["Walther Neuper 2005 supported by a grant from NMI Austria"],...}=>()
|
neuper@37871
|
202 |
| _ => raise error "thy-hierarchy.sml: store_isa overwritten";
|
neuper@37871
|
203 |
|
neuper@37871
|
204 |
(*
|
neuper@37871
|
205 |
print_depth 7;
|
neuper@37871
|
206 |
get_the ["IsacKnowledge","Biegelinie","Theorems","Belastung_Querkraft"];
|
neuper@37871
|
207 |
print_depth 3;
|
neuper@37871
|
208 |
*)
|
neuper@37871
|
209 |
|
neuper@37871
|
210 |
(*WN060728 strange behaviour:
|
neuper@37871
|
211 |
### fun the_hier reports these not overwritten ?!?...(stored twice ?!?) ...
|
neuper@37871
|
212 |
|
neuper@37871
|
213 |
val it = () : unit
|
neuper@37871
|
214 |
*** insert: preserved ["Isabelle","RealDef","Theorems","real_mult_assoc"]
|
neuper@37871
|
215 |
*** insert: preserved ["Isabelle","RealDef","Theorems","real_add_assoc"]
|
neuper@37871
|
216 |
*** insert: preserved ["Isabelle","RealBin","Theorems","real_mult_minus1"]
|
neuper@37871
|
217 |
*** insert: preserved ["Isabelle","RealBin","Theorems","real_mult_2"]
|
neuper@37871
|
218 |
*** insert: preserved ["Isabelle","RealDef","Theorems","real_mult_assoc"]
|
neuper@37871
|
219 |
*** insert: preserved ["Isabelle","RealDef","Theorems","real_mult_minus_eq1"]
|
neuper@37871
|
220 |
*** insert: preserved ["Isabelle","RealDef","Theorems","real_add_assoc"]
|
neuper@37871
|
221 |
*** insert: preserved ["Isabelle","RealDef","Theorems","real_minus_divide_eq"]
|
neuper@37871
|
222 |
*** insert: preserved ["IsacScripts","ListG","Theorems","induct"]
|
neuper@37871
|
223 |
*** insert: preserved ["IsacScripts","ListG","Theorems","simps_1"]
|
neuper@37871
|
224 |
*** insert: preserved ["IsacScripts","ListG","Theorems","simps_2"]
|
neuper@37871
|
225 |
val it = () : unit
|
neuper@37871
|
226 |
|
neuper@37871
|
227 |
### but those store_*d in Biegelinie.ML are NOT reported !?!?!?!?!?!?!
|
neuper@37871
|
228 |
### however, '*** insert: not found' is NOT reported below, too....
|
neuper@37871
|
229 |
|
neuper@37871
|
230 |
----------------------------------
|
neuper@37871
|
231 |
*** insert: not found ... IS OK :
|
neuper@37871
|
232 |
comes from fill_parents
|
neuper@37871
|
233 |
----------------------------------
|
neuper@37871
|
234 |
|
neuper@37871
|
235 |
val it = () : unit
|
neuper@37871
|
236 |
*** insert: not found ["Isabelle","NatDef","Theorems","le_refl"]
|
neuper@37871
|
237 |
*** insert: not found ["Isabelle","NatDef","Theorems","le_refl"]*)
|
neuper@37871
|
238 |
|
neuper@37871
|
239 |
"----------- ### thes2file ... Exception- Match raised -----------";
|
neuper@37871
|
240 |
"----------- ### thes2file ... Exception- Match raised -----------";
|
neuper@37871
|
241 |
"----------- ### thes2file ... Exception- Match raised -----------";
|
neuper@37871
|
242 |
writeln "what to do when you get,e.g. \n\
|
neuper@37871
|
243 |
\### thes2file: id = [\"IsacKnowledge\",\"Integrate\",\"Rulesets\"]\n\
|
neuper@37871
|
244 |
\### thes2file: id = [\"IsacKnowledge\",\"Integrate\",\"Rulesets\",\"integration_rules\"]\n\
|
neuper@37871
|
245 |
\### thes2file: id = [\"IsacKnowledge\",\"Integrate\",\"Rulesets\",\"add_new_c\"]\n\
|
neuper@37871
|
246 |
\Exception- Match raised";
|
neuper@37871
|
247 |
|
neuper@37871
|
248 |
val ptyp = hd (!thehier);
|
neuper@37871
|
249 |
val theID = ["IsacKnowledge","Integrate","Rulesets","add_new_c"];
|
neuper@37871
|
250 |
val thydata = get_the theID;
|
neuper@37871
|
251 |
(* creates a file ...
|
neuper@37871
|
252 |
thydata2file "~/tmp/"[] theID thydata (*reports Exception- Match in question*);
|
neuper@37871
|
253 |
*)
|
neuper@37871
|
254 |
thydata2xml (theID, thydata) (*reports Exception- Match in question*);
|
neuper@37871
|
255 |
val (theID:theID, Hrls {guh, coursedesign, mathauthors, thy_rls}) =
|
neuper@37871
|
256 |
(theID, thydata);
|
neuper@37871
|
257 |
rls2xml i thy_rls (*reports Exception- Match in question*);
|
neuper@37871
|
258 |
val (j, (thyID, Seq data)) = (i, thy_rls);
|
neuper@37871
|
259 |
(* evaluate this local fun ...
|
neuper@37871
|
260 |
rls2xm j (thyID, "Seq", data) (*reports Exception- Match in question*);
|
neuper@37871
|
261 |
*)
|
neuper@37871
|
262 |
val (j, (thyID, seqrls, {id, preconds, rew_ord=(ord,_), erls,
|
neuper@37871
|
263 |
srls, calc, rules, scr})) =
|
neuper@37871
|
264 |
(j, (thyID, "Seq", data));
|
neuper@37871
|
265 |
rules2xml (j+2*i) thyID rules (*reports Exception- Match in question*);
|
neuper@37871
|
266 |
|