1 (* Title: "xmlsrc/thy-hierarchy.sml"
2 tests for xmlsrc/thy-hierarchy.sml
3 Authors: Walther Neuper 060113
4 (c) due to copyright terms
6 theory Test_Some imports Isac.Build_Thydata begin
7 ML_file "~~/test/Tools/isac/ADDTESTS/accumulate-val/lucas_interpreter.sml"
8 ML_file "xmlsrc/thy-hierarchy.sml"
10 CAUTION with testing *2file functions -- they are actually writing to ~/tmp
13 val thy = @{theory "Isac"};
15 "-----------------------------------------------------------------";
16 "table of contents -----------------------------------------------";
17 "-----------------------------------------------------------------";
18 "----------- fun thms_of -----------------------------------------";
19 "----------- ### thes2file ... Exception- Match raised -----------";
20 "----------- search for data error in thes2file ------------------";
21 "----------- thes2file: thy_containing_rls : rls '...' not in ! --";
22 "----------- fun Thm.make_thm ------------------------------------";
23 "----------- correct theIDs for e_rls ----------------------------";
24 "----------- correct theIDs for list_rls -------------------------";
25 "----------- fun revert_sym --------------------------------------";
26 "----------- fun thms_of_rlss ------------------------------------";
27 "----------- repair thydata2xml for rls --------------------------";
28 "-----------------------------------------------------------------";
29 "----------- gen.minimal KEStore_Elems from Test_Build_Thydata.thy";
30 "----------- ..CONTINUED: we adapt some required MINIfunctions ---";
31 "----------- ..CONTINUED: xml from Test_Build_Thydata.thy --------";
32 "----------- ..CONTINUED: repair xml-format of thy_*-thm-*.xml ---";
33 "-----------------------------------------------------------------";
34 "-----------------------------------------------------------------";
35 "-----------------------------------------------------------------";
38 "----------- fun thms_of -----------------------------------------";
39 "----------- fun thms_of -----------------------------------------";
40 "----------- fun thms_of -----------------------------------------";
41 (*WN160112 WE REPLACED vvv BY "fun thms_of" in src/../thy-hierarchy.sml
42 val ths = MutabelleExtra.thms_of false @{theory Biegelinie};
44 ["Q' ?x = - qq ?x", "- qq ?x = Q' ?x", "\<not> ?a =!= 0 \<Longrightarrow> (?a * ?f ?x = ?b) = (?f ?x = 1 / ?a * ?b)",
45 "Q ?x = M_b' ?x", "M_b' ?x = Q ?x", "y'' ?x = - M_b ?x / EI", "M_b ?x = - EI * y'' ?x"]*)
46 map thmID_of_derivation_name' (thms_of thy) =
47 ["Querkraft_Belastung", "Belastung_Querkraft", "make_fun_explicit",
48 "Querkraft_Moment", "Moment_Querkraft", "Neigung_Moment", "Moment_Neigung"]
50 val thy = @{theory Biegelinie};
51 val thms = thms_of thy;
52 if map thmID_of_derivation_name' thms =
53 ["Querkraft_Belastung", "Belastung_Querkraft", "make_fun_explicit", "Querkraft_Moment",
54 "Moment_Querkraft", "Neigung_Moment", "Moment_Neigung"] then ()
55 else error "fun thms_of ...changed";
57 val without_partial_functions = thms_of @{theory Biegelinie};
58 if length without_partial_functions = 7 then () else error "thms_of Biegelinie changed";
60 "----------- ### thes2file ... Exception- Match raised -----------";
61 "----------- ### thes2file ... Exception- Match raised -----------";
62 "----------- ### thes2file ... Exception- Match raised -----------";
63 writeln "what to do when you get, e.g. \n\
64 \### thes2file: id = [\"IsacKnowledge\",\"Integrate\",\"Rulesets\"]\n\
65 \### thes2file: id = [\"IsacKnowledge\",\"Integrate\",\"Rulesets\",\"integration_rules\"]\n\
66 \### thes2file: id = [\"IsacKnowledge\",\"Integrate\",\"Rulesets\",\"add_new_c\"]\n\
67 \Exception- Match raised\n";
69 val theID = ["IsacKnowledge","Integrate","Rulesets","add_new_c"];
70 val thydata = get_the theID;
72 (* HERE WE DO NOT create a file ...
73 thydata2file "/tmp/" [] theID thydata (*reports Exception- Match in question*);
76 thydata2xml (theID, thydata) (*reported Exception- Match in question*);
79 val (theID:theID, Hrls {guh, coursedesign, mathauthors, thy_rls}) = (theID, thydata);
80 rls2xml i thy_rls (*reported Exception- Match in question*);
82 val (j, (thyID, Seq data)) = (i, thy_rls);
83 rls2xml j (thyID, Seq data) (*reported Exception- Match in question*);
85 val (j, (thyID, Seq {id, preconds, rew_ord=(ord,_), erls, errpatts, srls, calc, rules, scr})) =
86 (j, (thyID, Seq data));
88 rules2xml (j+2*i) thyID rules (*reports Exception- Match in question*);
89 (*TODO: Calc + Cal1 in datatypes.sml *)
91 "----------- search for data error in thes2file ------------------";
92 "----------- search for data error in thes2file ------------------";
93 "----------- search for data error in thes2file ------------------";
94 val TESTdump = Unsynchronized.ref
95 ("path": path, ["ids"]: theID, []: pos, thydata2file, Ptyp ("xxx", [], []): thydata ptyp);
97 fun TESTthenode (pa:path) ids po wfn (Ptyp (id, [n], ns)) TESTids =
98 let val po' = lev_on po
100 if (ids@[id]) = TESTids
102 (TESTdump := (pa, ids, po', wfn, (Ptyp (id, [n], ns)));
103 error "stopped before error, created TESTdump") (* this exn creates right signature*)
105 wfn pa po' (ids @ [id]) n; TESTthenodes pa (ids @ [id]) ((lev_dn po'): pos) wfn ns TESTids
107 and TESTthenodes _ _ _ _ [] _ = ()
108 | TESTthenodes pa ids po wfn (n::ns) TESTids =
109 (TESTthenode pa ids po wfn n TESTids; TESTthenodes pa ids (lev_on po) wfn ns TESTids);
111 (* /--- side effects from previous test files ---\*)
114 (* \--- side effects from previous test files ---/*)
116 "~~~~~ fun thes2file, args:"; val (p : path) = ("/tmp/");
117 (* recursively descend into thehier just before the error
118 by setting TESTids according to the last line in ouput
119 ### thes2file: id = : *)
120 (TESTthenodes p [] [0] thydata2file (get_thes ())
121 ["IsacKnowledge","Rational","Rulesets","norm_Rational_parenthesized"]
122 handle _(* "stopped before error, created TESTdump" *) => ());
124 (* /----- uncomment in case of "data error in thes2file" ----------------------------(*1*)-----\*)
125 val (pa, ids, po', wfn, (Ptyp (id, [n], ns))) = ! TESTdump;
127 "~~~~~ fun thydata2file, args:"; val ((xmldata:path), (pos:pos), (theID:theID), thydata) =
128 (pa, po', (ids@[id]), n);
129 "~~~~~ fun thydata2xml, args:"; val (theID, Hrls {guh, coursedesign, mathauthors, thy_rls}) =
130 (theID:theID, thydata);
131 "~~~~~ fun rls2xml, args:"; val (j, (thyID, Seq data)) = (i, thy_rls);
132 "~~~~~ fun rls2xm, args:"; val (j, (thyID, seqrls, {id, preconds, rew_ord=(ord,_), erls,
133 srls, calc, errpatts, rules, scr})) = (j, (thyID, "Seq", data));
134 "~~~~~ fun rules2xml, args:"; val (j, thyID, (r::rs)) = ((j+2*i), thyID, rules);
135 "~~~~~ fun rule2xml, args:"; val (j, thyID, (Rls_ rls)) = (j, thyID, r);
136 val rls' = (#id o rep_rls) rls;
137 (* \----- uncomment in case of "data error in thes2file" ----------------------------(*1*)-----/
138 another way to tackle this kind of error is shown in
139 "----------- thes2file: thy_containing_rls : rls '...' not in ! --"; ------------------------*)
141 "----------- thes2file: thy_containing_rls : rls '...' not in ! --";
142 "----------- thes2file: thy_containing_rls : rls '...' not in ! --";
143 "----------- thes2file: thy_containing_rls : rls '...' not in ! --";
144 val theID = ["IsacKnowledge","Rational","Rulesets","norm_Rational_parenthesized"]
145 val thydata = get_the theID
147 thydata2xml (theID, thydata);
149 "----------- fun Thm.make_thm ------------------------------------";
150 "----------- fun Thm.make_thm ------------------------------------";
151 "----------- fun Thm.make_thm ------------------------------------";
152 "~~~~~ fun Thm.make_thm, args:"; val (thy, part, (thmID : thmID, thm), (mathauthors : authors)) =
153 (@{theory "Biegelinie"}, "IsacKnowledge",
154 ("Belastung_Querkraft", Thm.prop_of @{thm Belastung_Querkraft}),
155 ["Walther Neuper 2005 supported by a grant from NMI Austria"]);
156 val guh = thm2guh (part, theory2thyID thy) thmID
157 val theID = guh2theID guh;
158 if guh = "thy_isac_Biegelinie-thm-Belastung_Querkraft" andalso
159 theID = ["IsacKnowledge", "Biegelinie", "Theorems", "Belastung_Querkraft"]
160 then () else error "store_thm: guh | theID changed";
162 "----------- correct theIDs for e_rls ----------------------------";
163 "----------- correct theIDs for e_rls ----------------------------";
164 "----------- correct theIDs for e_rls ----------------------------";
165 if thy_containing_rls "Build_Thydata" "e_rls" = ("IsacScripts", "KEStore") then ()
166 else error "thy_containing_rls e_rls changed";
168 (*shows different assignment for "e_rls"...
170 ["IsacScripts", "KEStore", "Rulesets", "e_rls"],
173 "----------- correct theIDs for list_rls -------------------------";
174 "----------- correct theIDs for list_rls -------------------------";
175 "----------- correct theIDs for list_rls -------------------------";
176 if thy_containing_rls "Build_Thydata" "list_rls" = ("IsacScripts", "Atools") then ()
177 else error "thy_containing_rls list_rls changed";
179 (*shows different assignment for "list_rls"...
181 ["IsacScripts", "Tools", "Rulesets", "list_rls"],
184 "----------- fun revert_sym --------------------------------------";
185 "----------- fun revert_sym --------------------------------------";
186 "----------- fun revert_sym --------------------------------------";
187 val thy = @{theory Isac}
188 val (Thm (thmID, thm)) =
189 revert_sym thy (Thm ("sym_real_mult_minus1", num_str (@{thm real_mult_minus1} RS @{thm sym})))
191 if thmID = "Delete.real_mult_minus1" andalso string_of_thmI thm = "-1 * ?z = - ?z"
192 then () else error "fun revert_sym changed 1";
194 val (Thm (thmID, thm)) =
195 revert_sym thy (Thm ("real_diff_minus", num_str @{thm real_diff_minus}))
197 if thmID = "Root.real_diff_minus" andalso string_of_thmI thm = "?a - ?b = ?a + -1 * ?b"
198 then () else error "fun revert_sym changed 2"
200 "----------- fun thms_of_rlss ------------------------------------";
201 "----------- fun thms_of_rlss ------------------------------------";
202 "----------- fun thms_of_rlss ------------------------------------";
204 [("e_rls" : rls', ("KEStore": theory', e_rls)),
205 ("discard_minus" : rls', ("Poly": theory', discard_minus))]
207 val [_, (thmID, term)] = thms_of_rlss thy rlss;
209 if thmID = "real_mult_minus1" (* WAS "??.unknown" *)
210 then () else error "thms_of_rlss changed"
213 "~~~~~ fun thms_of_rlss, args:"; val (thy, rlss) = (@{theory Isac}, rlss);
214 val rlss' = (rlss : (rls' * (theory' * rls)) list)
215 |> map (thms_of_rls o #2 o #2)
216 (* = [[], [Thm ("real_diff_minus", "?a - ?b = ?a + -1 * ?b"),
217 Thm ("sym_real_mult_minus1", "- ?z1 = -1 * ?z1")]]*)
219 (* = [Thm ("real_diff_minus", "?a - ?b = ?a + -1 * ?b"),
220 Thm ("sym_real_mult_minus1", "- ?z1 = -1 * ?z1")]*)
221 |> map (revert_sym thy)
222 (* = [Thm ("Poly.real_diff_minus", "?a - ?b = ?a + -1 * ?b"),
223 Thm ("Delete.real_mult_minus1", "-1 * ?z = - ?z")] : rule list*)
224 |> map (fn Thm (thmID, thm) => (thmID, Thm.prop_of thm))
225 (* = [("Poly.real_diff_minus", Const ("HOL.Trueprop", "bool \<Rightarrow> prop") $ ...,
226 ("Delete.real_mult_minus1", Const ("HOL.Trueprop", ...)] : (string * term) list*)
227 |> gen_distinct (fn ((thmID1, thm1), (thmID2, thm2)) => thmID1 = thmID2);
229 "----------- repair thydata2xml for rls --------------------------";
230 "----------- repair thydata2xml for rls --------------------------";
231 "----------- repair thydata2xml for rls --------------------------";
232 val theID = ["IsacKnowledge", "Poly", "Rulesets", "expand"]
233 val hrls = get_the theID
235 if thydata2xml (theID, hrls) = ("<RULESETDATA>\n" ^
236 " <GUH> thy_isac_Poly-rls-expand </GUH>\n" ^
238 " <STRING> IsacKnowledge </STRING>\n" ^
239 " <STRING> Poly </STRING>\n" ^
240 " <STRING> Rulesets </STRING>\n" ^
241 " <STRING> expand </STRING>\n" ^
242 " </STRINGLIST>\n <RULESET>\n" ^
243 " <ID> expand </ID>\n" ^
244 " <TYPE> Rls </TYPE>\n" ^
247 " <TAG> Theorem </TAG>\n" ^
248 " <STRING> distrib_right </STRING>\n" ^
249 " <GUH> thy_isac_distrib_right-thm-distrib_right </GUH>\n" ^
252 " <TAG> Theorem </TAG>\n" ^
253 " <STRING> distrib_left </STRING>\n" ^
254 " <GUH> thy_isac_distrib_left-thm-distrib_left </GUH>\n" ^
257 " <PRECONDS> </PRECONDS>\n" ^
259 " <STRING> dummy_ord </STRING>\n" ^
262 " <TAG> Ruleset </TAG>\n" ^
263 " <STRING> e_rls </STRING>\n" ^
264 " <GUH> thy_isac_Poly-rls-e_rls </GUH>\n" ^
267 " <TAG> Ruleset </TAG>\n" ^
268 " <STRING> e_rls </STRING>\n" ^
269 " <GUH> thy_isac_Poly-rls-e_rls </GUH>\n" ^
273 " <ISA> auto_generated t_t =\nRepeat\n" ^
274 " ((Try (Repeat (Rewrite ''distrib_right'' False)) @@\n" ^
275 " Try (Repeat (Rewrite ''distrib_left'' False)))\n" ^
276 " ??.empty) </ISA>\n" ^
280 " <EXPLANATIONS> </EXPLANATIONS>\n" ^
282 " <STRING> isac-team </STRING>\n" ^
283 " </MATHAUTHORS>\n" ^
284 " <COURSEDESIGNS>\n" ^
285 " </COURSEDESIGNS>\n" ^
286 "</RULESETDATA>\n") then ()
287 else error "thydata2xml for rls changed";
289 "----------- gen.minimal KEStore_Elems from Test_Build_Thydata.thy";
290 "----------- gen.minimal KEStore_Elems from Test_Build_Thydata.thy";
291 "----------- gen.minimal KEStore_Elems from Test_Build_Thydata.thy";
292 val isacrlsthms = KEStore_Elems.get_rlss @{theory Test_Build_Thydata}
293 (* CHANGE FOR CODE ^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
294 |> remove (fn (rlsID, (rls', (_, _))) => rlsID = rls') "list_rls" (*unpleasant in test*)
295 |> remove (fn (rlsID, (rls', (_, _))) => rlsID = rls') "e_rrls" (*unpleasant in test*)
296 |> remove (fn (rlsID, (rls', (_, _))) => rlsID = rls') "e_rls" (*unpleasant in test*)
297 |> thms_of_rlss @{theory} (*length = 4*)
299 val rlsthmsNOTisac = isacrlsthms (*length = 2*)
300 |> filter (fn (deriv, _) =>
301 member op= (map Context.theory_name isabthys') (thyID_of_derivation_name deriv))
303 val (knowthys', progthys') = ([@{theory Test_Build_Thydata}], [@{theory Test_Build_Thydata}])
306 collect_part "IsacKnowledge" knowledge_parent knowthys' @
307 (map (collect_isab "Isabelle") rlsthmsNOTisac) @
308 collect_part "IsacScripts" proglang_parent progthys' (* only the thms, no rls *)
310 case thydata_list of (*length = 8*)
311 [(["IsacKnowledge", "Test_Build_Thydata", "Theorems", "thm111"],
312 Hthm {coursedesign = [], fillpats = [], guh = "thy_isac_Test_Build_Thydata-thm-thm111",
313 mathauthors = ["isac-team"], thm = _}),
314 (["IsacKnowledge", "Test_Build_Thydata", "Theorems", "thm222"],
315 Hthm {coursedesign = [], fillpats = [], guh = "thy_isac_Test_Build_Thydata-thm-thm222",
316 mathauthors = ["isac-team"], thm = _}),
317 (["IsacKnowledge", "Test_Build_Thydata", "Rulesets", "rls111"],
318 Hrls {coursedesign = [], guh = "thy_isac_Test_Build_Thydata-rls-rls111",
319 mathauthors = ["isac-team"], thy_rls = ("Test_Build_Thydata", Rls _)}),
320 (["IsacKnowledge", "Test_Build_Thydata", "Rulesets", "rls222"],
321 Hrls {coursedesign = [], guh = "thy_isac_Test_Build_Thydata-rls-rls222",
322 mathauthors = ["isac-team"], thy_rls = ("Test_Build_Thydata", Rls _)}),
323 (["Isabelle", "HOL", "Theorems", "refl"],
324 Hthm {coursedesign = [], fillpats = [], guh = "thy_isab_HOL-thm-refl",
325 mathauthors = ["Isabelle team, TU Munich"], thm = _}),
326 (["Isabelle", "Fun", "Theorems", "o_def"], Hthm {coursedesign = [], fillpats = [],
327 guh = "thy_isab_Fun-thm-o_def", mathauthors = ["Isabelle team, TU Munich"], thm = _}),
328 (["IsacScripts", "Test_Build_Thydata", "Theorems", "thm111"],
329 Hthm {coursedesign = [], fillpats = [], guh = "thy_scri_Test_Build_Thydata-thm-thm111",
330 mathauthors = ["isac-team"], thm = _}),
331 (["IsacScripts", "Test_Build_Thydata", "Theorems", "thm222"],
332 Hthm {coursedesign = [], fillpats = [], guh = "thy_scri_Test_Build_Thydata-thm-thm222",
333 mathauthors = ["isac-team"], thm = _})] => ()
334 | _ => error "collect thydata from Test_Build_Thydata changed";
336 (* we store locally on MINIthehier instead on KEStore, see KEStore: *)
337 fun add_the (thydata, theID) = add_thydata ([], theID) thydata;
338 val thes = map (fn (a, b) => (b, a)) thydata_list
339 val MINIthehier = (fold add_the thes) (KEStore_Elems.get_thes @{theory Test_Build_Thydata});
341 "----------- ..CONTINUED: we adapt some required MINIfunctions ---";
342 "----------- ..CONTINUED: we adapt some required MINIfunctions ---";
343 "----------- ..CONTINUED: we adapt some required MINIfunctions ---";
344 fun MINIget_the (theID : theID) = get_py MINIthehier theID theID (*see ptyps.sml*)
345 fun MINIthy_hierarchy2file (path:path) =
346 str2file (path ^ "thy_hierarchy.xml")
348 " <ID> theory hierarchy </ID>\n" ^
350 " <CONTENTREF> thy_ROOT </CONTENTREF>\n" ^
351 (hierarchy_guh MINIthehier) ^
353 fun MINIthes2file (p : path) = thenodes p [] [0] thydata2file MINIthehier;
355 "----------- ..CONTINUED: xml from Test_Build_Thydata.thy --------";
356 "----------- ..CONTINUED: xml from Test_Build_Thydata.thy --------";
357 "----------- ..CONTINUED: xml from Test_Build_Thydata.thy --------";
358 case MINIget_the ["IsacScripts", "Test_Build_Thydata", "Theorems", "thm111"] of
359 Hthm {guh = "thy_scri_Test_Build_Thydata-thm-thm111", ...} => ()
360 | _ => error "MINIget_the thm111 changed"
364 MINIthy_hierarchy2file path (* ---> /tmp/thy_hierarchy.xml *);
365 writeln (file2str path "thy_hierarchy.xml") (* better check in editor *)
367 MINIthes2file path (* ---> /tmp/thy_... *);
369 "----------- ..CONTINUED: repair xml-format of thy_*-thm-*.xml ---";
370 "----------- ..CONTINUED: repair xml-format of thy_*-thm-*.xml ---";
371 "----------- ..CONTINUED: repair xml-format of thy_*-thm-*.xml ---";
372 "~~~~~ fun MINIthes2file, args:"; val (path) = ("/tmp/");
373 "~~~~~ and thenodes, args:"; val (pa, ids, po, wfn, (n::ns)) =
374 (path, [], [0], thydata2file, MINIthehier);
375 "~~~~~ fun thenode, args:"; val ((pa : path), ids, po, wfn, (Ptyp (id, [n], ns))) =
376 (pa, ids, po, wfn, n);
378 (*wfn pa po' (ids @ [id]) n -------------> writes xml to file; we want xml before written: *)
380 (* we take (theID, thydata) from thydata_list ABOVE: *)
381 case hd thydata_list of
382 (["IsacKnowledge", "Test_Build_Thydata", "Theorems", "thm111"],
383 Hthm {guh = "thy_isac_Test_Build_Thydata-thm-thm111", mathauthors = ["isac-team"], ...}) => ()
384 | _ => error "a change inhibits successful continuation of this test";
385 val (theID, thydata) = hd thydata_list;
386 "~~~~~ fun thydata2file, args:"; val ((path : path), (pos : pos), (theID : theID), thydata) =
387 (pa, po', (*ids @ [id]*)theID, (*n*)thydata);
388 "~~~~~ fun thydata2xml, args:"; val ((theID, Hthm {guh, coursedesign, mathauthors, fillpats, thm}))=
390 "~~~~~ to str2file return val:"; val (xml) =
392 indt i ^ "<GUH> "^ guh ^" </GUH>\n" ^
395 indt i ^ "<PROOF>\n" ^
396 extref2xml (i+i) "Proof of the theorem"
397 ("http://www.ist.tugraz.at/projects/isac/www/kbase/thy/browser_info/HOL/HOL-Real/Isac/" ^
398 nth 2 theID ^ ".html") ^
399 indt i ^ "</PROOF>\n" ^
400 indt i ^ "<EXPLANATIONS> </EXPLANATIONS>\n" ^
401 authors2xml i "MATHAUTHORS" mathauthors ^
402 authors2xml i "COURSEDESIGNS" coursedesign ^
405 if xml = ("<THEOREMDATA>\n" ^
406 " <GUH> thy_isac_Test_Build_Thydata-thm-thm111 </GUH>\n" ^
408 " <STRING> IsacKnowledge </STRING>\n" ^
409 " <STRING> Test_Build_Thydata </STRING>\n" ^
410 " <STRING> Theorems </STRING>\n" ^
411 " <STRING> thm111 </STRING>\n" ^
414 " <ID> thm111 </ID>\n" ^
416 " <ISA> ?thm111.0 = ?thm111.0 + 111 </ISA>\n" ^
421 " <TEXT> Proof of the theorem </TEXT>\n" ^
422 " <URL> http://www.ist.tugraz.at/projects/isac/www/kbase/thy/browser_info/HOL/HOL-Real/Isac/Test_Build_Thydata.html </URL>\n" ^
425 " <EXPLANATIONS> </EXPLANATIONS>\n" ^
427 " <STRING> isac-team </STRING>\n" ^
428 " </MATHAUTHORS>\n" ^
429 " <COURSEDESIGNS>\n" ^
430 " </COURSEDESIGNS>\n" ^
431 "</THEOREMDATA>\n") then () else error "thy_isac_Test_Build_Thydata-thm-thm111.xml changed"