88 |
88 |
89 "----------- search for data error in thes2file ------------------"; |
89 "----------- search for data error in thes2file ------------------"; |
90 "----------- search for data error in thes2file ------------------"; |
90 "----------- search for data error in thes2file ------------------"; |
91 "----------- search for data error in thes2file ------------------"; |
91 "----------- search for data error in thes2file ------------------"; |
92 val TESTdump = Unsynchronized.ref |
92 val TESTdump = Unsynchronized.ref |
93 ("path": filepath, ["ids"]: theID, []: pos, thydata2file, Ptyp ("xxx", [], []): thydata ptyp); |
93 ("path": filepath, ["ids"]: theID, []: pos, thydata2file, Celem1.Ptyp ("xxx", [], []): thydata Celem1.ptyp); |
94 |
94 |
95 fun TESTthenode (pa:filepath) ids po wfn (Ptyp (id, [n], ns)) TESTids = |
95 fun TESTthenode (pa:filepath) ids po wfn (Celem1.Ptyp (id, [n], ns)) TESTids = |
96 let val po' = lev_on po |
96 let val po' = lev_on po |
97 in |
97 in |
98 if (ids@[id]) = TESTids |
98 if (ids@[id]) = TESTids |
99 then |
99 then |
100 (TESTdump := (pa, ids, po', wfn, (Ptyp (id, [n], ns))); |
100 (TESTdump := (pa, ids, po', wfn, (Celem1.Ptyp (id, [n], ns))); |
101 error "stopped before error, created TESTdump") (* this exn creates right signature*) |
101 error "stopped before error, created TESTdump") (* this exn creates right signature*) |
102 else |
102 else |
103 wfn pa po' (ids @ [id]) n; TESTthenodes pa (ids @ [id]) ((lev_dn po'): pos) wfn ns TESTids |
103 wfn pa po' (ids @ [id]) n; TESTthenodes pa (ids @ [id]) ((lev_dn po'): pos) wfn ns TESTids |
104 end |
104 end |
105 and TESTthenodes _ _ _ _ [] _ = () |
105 and TESTthenodes _ _ _ _ [] _ = () |
118 (TESTthenodes p [] [0] thydata2file (get_thes ()) |
118 (TESTthenodes p [] [0] thydata2file (get_thes ()) |
119 ["IsacKnowledge","Rational","Rulesets","norm_Rational_parenthesized"] |
119 ["IsacKnowledge","Rational","Rulesets","norm_Rational_parenthesized"] |
120 handle _(* "stopped before error, created TESTdump" *) => ()); |
120 handle _(* "stopped before error, created TESTdump" *) => ()); |
121 ; |
121 ; |
122 (* /----- uncomment in case of "data error in thes2file" ----------------------------(*1*)-----\*) |
122 (* /----- uncomment in case of "data error in thes2file" ----------------------------(*1*)-----\*) |
123 val (pa, ids, po', wfn, (Ptyp (id, [n], ns))) = ! TESTdump; |
123 val (pa, ids, po', wfn, (Celem1.Ptyp (id, [n], ns))) = ! TESTdump; |
124 ; |
124 ; |
125 "~~~~~ fun thydata2file, args:"; val ((xmldata:filepath), (pos:pos), (theID:theID), thydata) = |
125 "~~~~~ fun thydata2file, args:"; val ((xmldata:filepath), (pos:pos), (theID:theID), thydata) = |
126 (pa, po', (ids@[id]), n); |
126 (pa, po', (ids@[id]), n); |
127 "~~~~~ fun thydata2xml, args:"; val (theID, Hrls {guh, coursedesign, mathauthors, thy_rls}) = |
127 "~~~~~ fun thydata2xml, args:"; val (theID, Hrls {guh, coursedesign, mathauthors, thy_rls}) = |
128 (theID:theID, thydata); |
128 (theID:theID, thydata); |
158 then () else error "store_thm: guh | theID changed"; |
158 then () else error "store_thm: guh | theID changed"; |
159 |
159 |
160 "----------- correct theIDs for Rule_Set.empty ----------------------------"; |
160 "----------- correct theIDs for Rule_Set.empty ----------------------------"; |
161 "----------- correct theIDs for Rule_Set.empty ----------------------------"; |
161 "----------- correct theIDs for Rule_Set.empty ----------------------------"; |
162 "----------- correct theIDs for Rule_Set.empty ----------------------------"; |
162 "----------- correct theIDs for Rule_Set.empty ----------------------------"; |
163 if thy_containing_rls "Build_Thydata" "empty" = ("IsacScripts", "KEStore") then () |
163 if thy_containing_rls "Build_Thydata" "empty" = ("IsacScripts", "Know_Store") then () |
164 else error "thy_containing_rls Rule_Set.empty changed"; |
164 else error "thy_containing_rls Rule_Set.empty changed"; |
165 show_thes (); |
165 show_thes (); |
166 (*shows different assignment for "empty"... |
166 (*shows different assignment for "empty"... |
167 : |
167 : |
168 ["IsacScripts", "KEStore", "Rulesets", "empty"], |
168 ["IsacScripts", "Know_Store", "Rulesets", "empty"], |
169 :*) |
169 :*) |
170 |
170 |
171 "----------- fun revert_sym_rule --------------------------------------"; |
171 "----------- fun revert_sym_rule --------------------------------------"; |
172 "----------- fun revert_sym_rule --------------------------------------"; |
172 "----------- fun revert_sym_rule --------------------------------------"; |
173 "----------- fun revert_sym_rule --------------------------------------"; |
173 "----------- fun revert_sym_rule --------------------------------------"; |
186 |
186 |
187 "----------- fun thms_of_rlss ------------------------------------"; |
187 "----------- fun thms_of_rlss ------------------------------------"; |
188 "----------- fun thms_of_rlss ------------------------------------"; |
188 "----------- fun thms_of_rlss ------------------------------------"; |
189 "----------- fun thms_of_rlss ------------------------------------"; |
189 "----------- fun thms_of_rlss ------------------------------------"; |
190 val rlss = |
190 val rlss = |
191 [("empty" : Rule_Set.id, ("KEStore": ThyC.id, Rule_Set.empty)), |
191 [("empty" : Rule_Set.id, ("Know_Store": ThyC.id, Rule_Set.empty)), |
192 ("discard_minus" : Rule_Set.id, ("Poly": ThyC.id, discard_minus))] |
192 ("discard_minus" : Rule_Set.id, ("Poly": ThyC.id, discard_minus))] |
193 ; |
193 ; |
194 val [_, (thmID, term)] = thms_of_rlss thy rlss; |
194 val [_, (thmID, term)] = thms_of_rlss thy rlss; |
195 (* |
195 (* |
196 if thmID = "real_mult_minus1" (* WAS "??.unknown" *) |
196 if thmID = "real_mult_minus1" (* WAS "??.unknown" *) |
320 (["IsacScripts", "Test_Build_Thydata", "Theorems", "thm222"], |
320 (["IsacScripts", "Test_Build_Thydata", "Theorems", "thm222"], |
321 Hthm {coursedesign = [], fillpats = [], guh = "thy_scri_Test_Build_Thydata-thm-thm222", |
321 Hthm {coursedesign = [], fillpats = [], guh = "thy_scri_Test_Build_Thydata-thm-thm222", |
322 mathauthors = ["isac-team"], thm = _})] => () |
322 mathauthors = ["isac-team"], thm = _})] => () |
323 | _ => error "collect thydata from Test_Build_Thydata changed"; |
323 | _ => error "collect thydata from Test_Build_Thydata changed"; |
324 ; |
324 ; |
325 (* we store locally on MINIthehier instead on KEStore, see KEStore: *) |
325 (* we store locally on MINIthehier instead on Know_Store, see Know_Store: *) |
326 fun add_the (thydata, theID) = add_thydata ([], theID) thydata; |
326 fun add_the (thydata, theID) = add_thydata ([], theID) thydata; |
327 val thes = map (fn (a, b) => (b, a)) thydata_list |
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}); |
328 val MINIthehier = (fold add_the thes) (KEStore_Elems.get_thes @{theory Test_Build_Thydata}); |
329 |
329 |
330 "----------- ..CONTINUED: we adapt some required MINIfunctions ---"; |
330 "----------- ..CONTINUED: we adapt some required MINIfunctions ---"; |
359 "----------- ..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 ---"; |
360 "----------- ..CONTINUED: repair xml-format of thy_*-thm-*.xml ---"; |
361 "~~~~~ fun MINIthes2file, args:"; val (path) = ("/tmp/"); |
361 "~~~~~ fun MINIthes2file, args:"; val (path) = ("/tmp/"); |
362 "~~~~~ and thenodes, args:"; val (pa, ids, po, wfn, (n::ns)) = |
362 "~~~~~ and thenodes, args:"; val (pa, ids, po, wfn, (n::ns)) = |
363 (path, [], [0], thydata2file, MINIthehier); |
363 (path, [], [0], thydata2file, MINIthehier); |
364 "~~~~~ fun thenode, args:"; val ((pa : filepath), ids, po, wfn, (Ptyp (id, [n], ns))) = |
364 "~~~~~ fun thenode, args:"; val ((pa : filepath), ids, po, wfn, (Celem1.Ptyp (id, [n], ns))) = |
365 (pa, ids, po, wfn, n); |
365 (pa, ids, po, wfn, n); |
366 val po' = lev_on po; |
366 val po' = lev_on po; |
367 (*wfn pa po' (ids @ [id]) n -------------> writes xml to file; we want xml before written: *) |
367 (*wfn pa po' (ids @ [id]) n -------------> writes xml to file; we want xml before written: *) |
368 |
368 |
369 (* we take (theID, thydata) from thydata_list ABOVE: *) |
369 (* we take (theID, thydata) from thydata_list ABOVE: *) |