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