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