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