1 (* Title: "BridgeLibisabelle/thy-hierarchy.sml"
2 Authors: Walther Neuper 060113
3 (c) due to copyright terms
5 theory Test_Some imports Isac.Build_Thydata begin
6 ML_file "~~/test/Tools/isac/ADDTESTS/accumulate-val/lucas_interpreter.sml"
7 ML_file "xmlsrc/thy-hierarchy.sml"
9 CAUTION with testing *2file functions -- they are actually writing to ~/tmp
12 val thy = @{theory "Isac_Knowledge"};
14 "-----------------------------------------------------------------";
15 "table of contents -----------------------------------------------";
16 "-----------------------------------------------------------------";
17 "----------- fun thms_of -----------------------------------------";
18 "----------- ### thes2file ... Exception- Match raised -----------";
19 "----------- search for data error in thes2file ------------------";
20 "----------- thes2file: thy_containing_rls : rls '...' not in ! --";
21 "----------- fun Thm.make_thm ------------------------------------";
22 "----------- correct theIDs for Rule_Set.empty -------------------";
23 "----------- fun revert_sym_rule --------------------------------------";
24 "----------- fun thms_of_rlss ------------------------------------";
25 "----------- repair thydata2xml for rls --------------------------";
26 "-----------------------------------------------------------------";
27 "----------- gen.minimal KEStore_Elems from Test_Build_Thydata.thy";
28 "----------- ..CONTINUED: we adapt some required MINIfunctions ---";
29 "----------- ..CONTINUED: xml from Test_Build_Thydata.thy --------";
30 "----------- ..CONTINUED: repair xml-format of thy_*-thm-*.xml ---";
31 "-----------------------------------------------------------------";
32 "-----------------------------------------------------------------";
33 "-----------------------------------------------------------------";
36 "----------- fun thms_of -----------------------------------------";
37 "----------- fun thms_of -----------------------------------------";
38 "----------- fun thms_of -----------------------------------------";
39 (*WN160112 WE REPLACED vvv BY "fun thms_of" in src/../thy-hierarchy.sml
40 val ths = MutabelleExtra.thms_of false @{theory Biegelinie};
42 ["Q' ?x = - qq ?x", "- qq ?x = Q' ?x", "\<not> ?a =!= 0 \<Longrightarrow> (?a * ?f ?x = ?b) = (?f ?x = 1 / ?a * ?b)",
43 "Q ?x = M_b' ?x", "M_b' ?x = Q ?x", "y'' ?x = - M_b ?x / EI", "M_b ?x = - EI * y'' ?x"]*)
44 map ThmC.id_of_thm (thms_of thy) =
45 ["Querkraft_Belastung", "Belastung_Querkraft", "make_fun_explicit",
46 "Querkraft_Moment", "Moment_Querkraft", "Neigung_Moment", "Moment_Neigung"]
48 val thy = @{theory Biegelinie};
49 val thms = thms_of thy;
50 if map ThmC.id_of_thm thms =
51 ["Querkraft_Belastung", "Belastung_Querkraft", "make_fun_explicit", "Querkraft_Moment",
52 "Moment_Querkraft", "Neigung_Moment", "Moment_Neigung"] then ()
53 else error "fun thms_of ...changed";
55 val without_partial_functions = thms_of @{theory Biegelinie};
56 if length without_partial_functions = 7 then () else error "thms_of Biegelinie changed";
58 "----------- ### thes2file ... Exception- Match raised -----------";
59 "----------- ### thes2file ... Exception- Match raised -----------";
60 "----------- ### thes2file ... Exception- Match raised -----------";
61 writeln "what to do when you get, e.g. \n\
62 \### thes2file: id = [\"IsacKnowledge\",\"Integrate\",\"Rulesets\"]\n\
63 \### thes2file: id = [\"IsacKnowledge\",\"Integrate\",\"Rulesets\",\"integration_rules\"]\n\
64 \### thes2file: id = [\"IsacKnowledge\",\"Integrate\",\"Rulesets\",\"add_new_c\"]\n\
65 \Exception- Match raised\n";
67 val theID = ["IsacKnowledge","Integrate","Rulesets","add_new_c"];
68 val thydata = get_the theID;
70 (* HERE WE DO NOT create a file ...
71 thydata2file "/tmp/" [] theID thydata (*reports Exception- Match in question*);
74 thydata2xml (theID, thydata) (*reported Exception- Match in question*);
77 val (theID:theID, Hrls {guh, coursedesign, mathauthors, thy_rls}) = (theID, thydata);
78 rls2xml i thy_rls (*reported Exception- Match in question*);
80 val (j, (thyID, Rule_Set.Sequence data)) = (i, thy_rls);
81 rls2xml j (thyID, Rule_Set.Sequence data) (*reported Exception- Match in question*);
83 val (j, (thyID, Rule_Set.Sequence {id, preconds, rew_ord=(ord,_), erls, errpatts, srls, calc, rules, scr})) =
84 (j, (thyID, Rule_Set.Sequence data));
86 rules2xml (j+2*i) thyID rules (*reports Exception- Match in question*);
87 (*TODO: Eval + Cal1 in datatypes.sml *)
89 "----------- search for data error in thes2file ------------------";
90 "----------- search for data error in thes2file ------------------";
91 "----------- search for data error in thes2file ------------------";
92 val TESTdump = Unsynchronized.ref
93 ("path": filepath, ["ids"]: theID, []: pos, thydata2file, Store.Node ("xxx", [], []): thydata Store.node);
95 fun TESTthenode (pa:filepath) ids po wfn (Store.Node (id, [n], ns)) TESTids =
96 let val po' = lev_on po
98 if (ids@[id]) = TESTids
100 (TESTdump := (pa, ids, po', wfn, (Store.Node (id, [n], ns)));
101 error "stopped before error, created TESTdump") (* this exn creates right signature*)
103 wfn pa po' (ids @ [id]) n; TESTthenodes pa (ids @ [id]) ((lev_dn po'): pos) wfn ns TESTids
105 and TESTthenodes _ _ _ _ [] _ = ()
106 | TESTthenodes pa ids po wfn (n::ns) TESTids =
107 (TESTthenode pa ids po wfn n TESTids; TESTthenodes pa ids (lev_on po) wfn ns TESTids);
109 (* /--- side effects from previous test files ---\*)
112 (* \--- side effects from previous test files ---/*)
114 "~~~~~ fun thes2file, args:"; val (p : filepath) = ("/tmp/");
115 (* recursively descend into thehier just before the error
116 by setting TESTids according to the last line in ouput
117 ### thes2file: id = : *)
118 (TESTthenodes p [] [0] thydata2file (get_thes ())
119 ["IsacKnowledge","Rational","Rulesets","norm_Rational_parenthesized"]
120 handle _(* "stopped before error, created TESTdump" *) => ());
122 (* /----- uncomment in case of "data error in thes2file" ----------------------------(*1*)-----\*)
123 val (pa, ids, po', wfn, (Store.Node (id, [n], ns))) = ! TESTdump;
125 "~~~~~ fun thydata2file, args:"; val ((xmldata:filepath), (pos:pos), (theID:theID), thydata) =
126 (pa, po', (ids@[id]), n);
127 "~~~~~ fun thydata2xml, args:"; val (theID, Hrls {guh, coursedesign, mathauthors, thy_rls}) =
128 (theID:theID, thydata);
129 "~~~~~ fun rls2xml, args:"; val (j, (thyID, Rule_Set.Sequence data)) = (i, thy_rls);
130 "~~~~~ fun rls2xm, args:"; val (j, (thyID, seqrls, {id, preconds, rew_ord=(ord,_), erls,
131 srls, calc, errpatts, rules, scr})) = (j, (thyID, "Rule_Set.Sequence", data));
132 "~~~~~ fun rules2xml, args:"; val (j, thyID, (r::rs)) = ((j+2*i), thyID, rules);
133 "~~~~~ fun rule2xml, args:"; val (j, thyID, (Rls_ rls)) = (j, thyID, r);
134 val rls' = (#id o Rule_Set.rep) rls;
135 (* \----- uncomment in case of "data error in thes2file" ----------------------------(*1*)-----/
136 another way to tackle this kind of error is shown in
137 "----------- thes2file: thy_containing_rls : rls '...' not in ! --"; ------------------------*)
139 "----------- thes2file: thy_containing_rls : rls '...' not in ! --";
140 "----------- thes2file: thy_containing_rls : rls '...' not in ! --";
141 "----------- thes2file: thy_containing_rls : rls '...' not in ! --";
142 val theID = ["IsacKnowledge","Rational","Rulesets","norm_Rational_parenthesized"]
143 val thydata = get_the theID
145 thydata2xml (theID, thydata);
147 "----------- fun ThmC_Def.make_thm ------------------------------------";
148 "----------- fun ThmC_Def.make_thm ------------------------------------";
149 "----------- fun ThmC_Def.make_thm ------------------------------------";
150 "~~~~~ fun ThmC_Def.make_thm, args:"; val (thy, part, (thmID : ThmC.id, thm), (mathauthors : authors)) =
151 (@{theory "Biegelinie"}, "IsacKnowledge",
152 ("Belastung_Querkraft", Thm.prop_of @{thm Belastung_Querkraft}),
153 ["Walther Neuper 2005 supported by a grant from NMI Austria"]);
154 val guh = thm2guh (part, Context.theory_name thy) thmID
155 val theID = guh2theID guh;
156 if guh = "thy_isac_Biegelinie-thm-Belastung_Querkraft" andalso
157 theID = ["IsacKnowledge", "Biegelinie", "Theorems", "Belastung_Querkraft"]
158 then () else error "store_thm: guh | theID changed";
160 "----------- correct theIDs for Rule_Set.empty ----------------------------";
161 "----------- correct theIDs for Rule_Set.empty ----------------------------";
162 "----------- correct theIDs for Rule_Set.empty ----------------------------";
163 if thy_containing_rls "Build_Thydata" "empty" = ("IsacScripts", "Know_Store") then ()
164 else error "thy_containing_rls Rule_Set.empty changed";
166 (*shows different assignment for "empty"...
168 ["IsacScripts", "Know_Store", "Rulesets", "empty"],
171 "----------- fun revert_sym_rule --------------------------------------";
172 "----------- fun revert_sym_rule --------------------------------------";
173 "----------- fun revert_sym_rule --------------------------------------";
174 val thy = @{theory Isac_Knowledge}
175 val (Thm (thmID, thm)) = ThmC.revert_sym_rule thy
176 (Thm ("sym_real_mult_minus1", ThmC.numerals_to_Free (@{thm real_mult_minus1} RS @{thm sym})))
178 if thmID = "Poly.real_mult_minus1" andalso ThmC.string_of_thm thm = "-1 * ?z = - ?z"
179 then () else error "fun revert_sym_rule changed 1";
181 val (Thm (thmID, thm)) = ThmC.revert_sym_rule thy
182 (Thm ("real_diff_minus", ThmC.numerals_to_Free @{thm real_diff_minus}))
184 if thmID = "Root.real_diff_minus" andalso ThmC.string_of_thm thm = "?a - ?b = ?a + -1 * ?b"
185 then () else error "fun revert_sym_rule changed 2"
187 "----------- fun thms_of_rlss ------------------------------------";
188 "----------- fun thms_of_rlss ------------------------------------";
189 "----------- fun thms_of_rlss ------------------------------------";
191 [("empty" : Rule_Set.id, ("Know_Store": ThyC.id, Rule_Set.empty)),
192 ("discard_minus" : Rule_Set.id, ("Poly": ThyC.id, discard_minus))]
194 val [_, (thmID, term)] = thms_of_rlss thy rlss;
196 if thmID = "real_mult_minus1" (* WAS "??.unknown" *)
197 then () else error "thms_of_rlss changed"
200 "~~~~~ fun thms_of_rlss, args:"; val (thy, rlss) = (@{theory Isac_Knowledge}, rlss);
201 val rlss' = (rlss : (Rule_Set.id * (ThyC.id * Rule_Set.T)) list)
202 |> map (thms_of_rls o #2 o #2)
203 (* = [[], [Thm ("real_diff_minus", "?a - ?b = ?a + -1 * ?b"),
204 Thm ("sym_real_mult_minus1", "- ?z1 = -1 * ?z1")]]*)
206 (* = [Thm ("real_diff_minus", "?a - ?b = ?a + -1 * ?b"),
207 Thm ("sym_real_mult_minus1", "- ?z1 = -1 * ?z1")]*)
208 |> map (ThmC.revert_sym_rule thy)
209 (* = [Thm ("Poly.real_diff_minus", "?a - ?b = ?a + -1 * ?b"),
210 Thm ("Delete.real_mult_minus1", "-1 * ?z = - ?z")] : rule list*)
211 |> map (fn Thm (thmID, thm) => (thmID, Thm.prop_of thm))
212 (* = [("Poly.real_diff_minus", Const ("HOL.Trueprop", "bool \<Rightarrow> prop") $ ...,
213 ("Delete.real_mult_minus1", Const ("HOL.Trueprop", ...)] : (string * term) list*)
214 |> gen_distinct (fn ((thmID1, thm1), (thmID2, thm2)) => thmID1 = thmID2);
216 "----------- repair thydata2xml for rls --------------------------";
217 "----------- repair thydata2xml for rls --------------------------";
218 "----------- repair thydata2xml for rls --------------------------";
219 val theID = ["IsacKnowledge", "Poly", "Rulesets", "expand"]
220 val hrls = get_the theID
222 if thydata2xml (theID, hrls) = (
224 " <GUH> thy_isac_Poly-rls-expand </GUH>\n" ^
226 " <STRING> IsacKnowledge </STRING>\n" ^
227 " <STRING> Poly </STRING>\n" ^
228 " <STRING> Rulesets </STRING>\n" ^
229 " <STRING> expand </STRING>\n" ^
230 " </STRINGLIST>\n <RULESET>\n" ^
231 " <ID> expand </ID>\n" ^
232 " <TYPE> Rls </TYPE>\n" ^
235 " <TAG> Theorem </TAG>\n" ^
236 " <STRING> distrib_right </STRING>\n" ^
237 " <GUH> thy_isac_distrib_right-thm-distrib_right </GUH>\n" ^
240 " <TAG> Theorem </TAG>\n" ^
241 " <STRING> distrib_left </STRING>\n" ^
242 " <GUH> thy_isac_distrib_left-thm-distrib_left </GUH>\n" ^
248 " <STRING> dummy_ord </STRING>\n" ^
251 " <TAG> Ruleset </TAG>\n" ^
252 " <STRING> empty </STRING>\n" ^
253 " <GUH> thy_isac_Poly-rls-empty </GUH>\n" ^
256 " <TAG> Ruleset </TAG>\n" ^
257 " <STRING> empty </STRING>\n" ^
258 " <GUH> thy_isac_Poly-rls-empty </GUH>\n" ^
260 " <SCRIPT> </SCRIPT>\n" ^
264 " <ISA> auto_generated t_t =\nRepeat\n ((Try (Repeat (Rewrite ''distrib_right'')) #>\n Try (Repeat (Rewrite ''distrib_left'')))\n ??.empty) </ISA>\n" ^
269 " <EXPLANATIONS> </EXPLANATIONS>\n" ^
271 " <STRING> isac-team </STRING>\n" ^
272 " </MATHAUTHORS>\n" ^
273 " <COURSEDESIGNS>\n" ^
274 " </COURSEDESIGNS>\n" ^
275 "</RULESETDATA>\n") then ()
276 else error "thydata2xml for rls changed";
278 "----------- gen.minimal KEStore_Elems from Test_Build_Thydata.thy";
279 "----------- gen.minimal KEStore_Elems from Test_Build_Thydata.thy";
280 "----------- gen.minimal KEStore_Elems from Test_Build_Thydata.thy";
281 val isacrlsthms = KEStore_Elems.get_rlss @{theory Test_Build_Thydata}
282 (* CHANGE FOR CODE ^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
283 |> remove (fn (rlsID, (rls', (_, _))) => rlsID = rls') "prog_expr" (*unpleasant in test*)
284 |> remove (fn (rlsID, (rls', (_, _))) => rlsID = rls') "e_rrls" (*unpleasant in test*)
285 |> remove (fn (rlsID, (rls', (_, _))) => rlsID = rls') "empty" (*unpleasant in test*)
286 |> thms_of_rlss @{theory} (*length = 4*)
288 val rlsthmsNOTisac = isacrlsthms (*length = 2*)
289 |> filter (fn (deriv, _) =>
290 member op= (map Context.theory_name isabthys') (ThyC.cut_id deriv))
292 val (knowthys', progthys') = ([@{theory Test_Build_Thydata}], [@{theory Test_Build_Thydata}])
295 collect_part "IsacKnowledge" knowledge_parent knowthys' @
296 (map (collect_isab "Isabelle") rlsthmsNOTisac) @
297 collect_part "IsacScripts" proglang_parent progthys' (* only the thms, no rls *)
299 case thydata_list of (*length = 8*)
300 [(["IsacKnowledge", "Test_Build_Thydata", "Theorems", "thm111"],
301 Hthm {coursedesign = [], fillpats = [], guh = "thy_isac_Test_Build_Thydata-thm-thm111",
302 mathauthors = ["isac-team"], thm = _}),
303 (["IsacKnowledge", "Test_Build_Thydata", "Theorems", "thm222"],
304 Hthm {coursedesign = [], fillpats = [], guh = "thy_isac_Test_Build_Thydata-thm-thm222",
305 mathauthors = ["isac-team"], thm = _}),
306 (["IsacKnowledge", "Test_Build_Thydata", "Rulesets", "rls111"],
307 Hrls {coursedesign = [], guh = "thy_isac_Test_Build_Thydata-rls-rls111",
308 mathauthors = ["isac-team"], thy_rls = ("Test_Build_Thydata", Rule_Set.Repeat _)}),
309 (["IsacKnowledge", "Test_Build_Thydata", "Rulesets", "rls222"],
310 Hrls {coursedesign = [], guh = "thy_isac_Test_Build_Thydata-rls-rls222",
311 mathauthors = ["isac-team"], thy_rls = ("Test_Build_Thydata", Rule_Set.Repeat _)}),
312 (["Isabelle", "HOL", "Theorems", "refl"],
313 Hthm {coursedesign = [], fillpats = [], guh = "thy_isab_HOL-thm-refl",
314 mathauthors = ["Isabelle team, TU Munich"], thm = _}),
315 (["Isabelle", "Fun", "Theorems", "o_def"], Hthm {coursedesign = [], fillpats = [],
316 guh = "thy_isab_Fun-thm-o_def", mathauthors = ["Isabelle team, TU Munich"], thm = _}),
317 (["IsacScripts", "Test_Build_Thydata", "Theorems", "thm111"],
318 Hthm {coursedesign = [], fillpats = [], guh = "thy_scri_Test_Build_Thydata-thm-thm111",
319 mathauthors = ["isac-team"], thm = _}),
320 (["IsacScripts", "Test_Build_Thydata", "Theorems", "thm222"],
321 Hthm {coursedesign = [], fillpats = [], guh = "thy_scri_Test_Build_Thydata-thm-thm222",
322 mathauthors = ["isac-team"], thm = _})] => ()
323 | _ => error "collect thydata from Test_Build_Thydata changed";
325 (* we store locally on MINIthehier instead on Know_Store, see Know_Store: *)
326 fun add_the (thydata, theID) = add_thydata ([], theID) thydata;
327 val thes = map (fn (a, b) => (b, a)) thydata_list
328 val MINIthehier = (fold add_the thes) (KEStore_Elems.get_thes @{theory Test_Build_Thydata});
330 "----------- ..CONTINUED: we adapt some required MINIfunctions ---";
331 "----------- ..CONTINUED: we adapt some required MINIfunctions ---";
332 "----------- ..CONTINUED: we adapt some required MINIfunctions ---";
333 fun MINIget_the (theID : theID) = get_py MINIthehier theID theID (*see ptyps.sml*)
334 fun MINIthy_hierarchy2file (path:filepath) =
335 str2file (path ^ "thy_hierarchy.xml")
337 " <ID> theory hierarchy </ID>\n" ^
339 " <CONTENTREF> thy_ROOT </CONTENTREF>\n" ^
340 (hierarchy_guh MINIthehier) ^
342 fun MINIthes2file (p : filepath) = thenodes p [] [0] thydata2file MINIthehier;
344 "----------- ..CONTINUED: xml from Test_Build_Thydata.thy --------";
345 "----------- ..CONTINUED: xml from Test_Build_Thydata.thy --------";
346 "----------- ..CONTINUED: xml from Test_Build_Thydata.thy --------";
347 case MINIget_the ["IsacScripts", "Test_Build_Thydata", "Theorems", "thm111"] of
348 Hthm {guh = "thy_scri_Test_Build_Thydata-thm-thm111", ...} => ()
349 | _ => error "MINIget_the thm111 changed"
353 MINIthy_hierarchy2file path (* ---> /tmp/thy_hierarchy.xml *);
354 writeln (file2str path "thy_hierarchy.xml") (* better check in editor *)
356 MINIthes2file path (* ---> /tmp/thy_... *);
358 "----------- ..CONTINUED: repair xml-format of thy_*-thm-*.xml ---";
359 "----------- ..CONTINUED: repair xml-format of thy_*-thm-*.xml ---";
360 "----------- ..CONTINUED: repair xml-format of thy_*-thm-*.xml ---";
361 "~~~~~ fun MINIthes2file, args:"; val (path) = ("/tmp/");
362 "~~~~~ and thenodes, args:"; val (pa, ids, po, wfn, (n::ns)) =
363 (path, [], [0], thydata2file, MINIthehier);
364 "~~~~~ fun thenode, args:"; val ((pa : filepath), ids, po, wfn, (Store.Node (id, [n], ns))) =
365 (pa, ids, po, wfn, n);
367 (*wfn pa po' (ids @ [id]) n -------------> writes xml to file; we want xml before written: *)
369 (* we take (theID, thydata) from thydata_list ABOVE: *)
370 case hd thydata_list of
371 (["IsacKnowledge", "Test_Build_Thydata", "Theorems", "thm111"],
372 Hthm {guh = "thy_isac_Test_Build_Thydata-thm-thm111", mathauthors = ["isac-team"], ...}) => ()
373 | _ => error "a change inhibits successful continuation of this test";
374 val (theID, thydata) = hd thydata_list;
375 "~~~~~ fun thydata2file, args:"; val ((path : filepath), (pos : pos), (theID : theID), thydata) =
376 (pa, po', (*ids @ [id]*)theID, (*n*)thydata);
377 "~~~~~ fun thydata2xml, args:"; val ((theID, Hthm {guh, coursedesign, mathauthors, fillpats, thm}))=
379 "~~~~~ to str2file return val:"; val (xml) =
381 indt i ^ "<GUH> "^ guh ^" </GUH>\n" ^
384 indt i ^ "<PROOF>\n" ^
385 extref2xml (i+i) "Proof of the theorem"
386 ("http://www.ist.tugraz.at/projects/isac/www/kbase/thy/browser_info/HOL/HOL-Real/Isac/" ^
387 nth 2 theID ^ ".html") ^
388 indt i ^ "</PROOF>\n" ^
389 indt i ^ "<EXPLANATIONS> </EXPLANATIONS>\n" ^
390 authors2xml i "MATHAUTHORS" mathauthors ^
391 authors2xml i "COURSEDESIGNS" coursedesign ^
394 if xml = ("<THEOREMDATA>\n" ^
395 " <GUH> thy_isac_Test_Build_Thydata-thm-thm111 </GUH>\n" ^
397 " <STRING> IsacKnowledge </STRING>\n" ^
398 " <STRING> Test_Build_Thydata </STRING>\n" ^
399 " <STRING> Theorems </STRING>\n" ^
400 " <STRING> thm111 </STRING>\n" ^
403 " <ID> thm111 </ID>\n" ^
405 " <ISA> ?thm111.0 = ?thm111.0 + 111 </ISA>\n" ^
410 " <TEXT> Proof of the theorem </TEXT>\n" ^
411 " <URL> http://www.ist.tugraz.at/projects/isac/www/kbase/thy/browser_info/HOL/HOL-Real/Isac/Test_Build_Thydata.html </URL>\n" ^
414 " <EXPLANATIONS> </EXPLANATIONS>\n" ^
416 " <STRING> isac-team </STRING>\n" ^
417 " </MATHAUTHORS>\n" ^
418 " <COURSEDESIGNS>\n" ^
419 " </COURSEDESIGNS>\n" ^
420 "</THEOREMDATA>\n") then () else error "thy_isac_Test_Build_Thydata-thm-thm111.xml changed"