|
akargl@42176
|
1 |
(* Title: test for sml/xmlsrc/datatypes.sml
|
|
akargl@42176
|
2 |
Authors: Walther Neuper 2003
|
|
neuper@37906
|
3 |
(c) due to copyright terms
|
|
neuper@37906
|
4 |
|
|
neuper@37906
|
5 |
use"../smltest/xmlsrc/datatypes.sml";
|
|
neuper@37906
|
6 |
use"datatypes.sml";
|
|
neuper@37906
|
7 |
*)
|
|
neuper@37906
|
8 |
|
|
neuper@37906
|
9 |
"-----------------------------------------------------------------";
|
|
neuper@37906
|
10 |
"table of contents -----------------------------------------------";
|
|
neuper@37906
|
11 |
"-----------------------------------------------------------------";
|
|
neuper@37906
|
12 |
"----------- fun rules2xml ---------------------------------------";
|
|
neuper@37906
|
13 |
"----------- fun thm''2xml ---------------------------------------";
|
|
neuper@37906
|
14 |
"-----------------------------------------------------------------";
|
|
neuper@37906
|
15 |
"-----------------------------------------------------------------";
|
|
neuper@37906
|
16 |
"-----------------------------------------------------------------";
|
|
neuper@37906
|
17 |
|
|
neuper@37906
|
18 |
|
|
neuper@37906
|
19 |
|
|
neuper@37906
|
20 |
"----------- fun rules2xml ---------------------------------------";
|
|
neuper@37906
|
21 |
"----------- fun rules2xml ---------------------------------------";
|
|
neuper@37906
|
22 |
"----------- fun rules2xml ---------------------------------------";
|
|
akargl@42176
|
23 |
|
|
neuper@37906
|
24 |
show_thes();
|
|
neuper@37906
|
25 |
val thyID = "Test";
|
|
akargl@42176
|
26 |
|
|
akargl@42176
|
27 |
(*========== inhibit exn AK110725 ================================================
|
|
neuper@37906
|
28 |
val thydata = get_the ["IsacKnowledge", "Test", "Rulesets", "ac_plus_times"];
|
|
akargl@42176
|
29 |
(*AK110725
|
|
akargl@42176
|
30 |
(*val thydata = get_the ["IsacKnowledge", "Test", "Rulesets", "ac_plus_times"];
|
|
akargl@42176
|
31 |
(* ERROR: get_pbt not found: ["IsacKnowledge","Test","Rulesets","ac_plus_times"] *)*)
|
|
akargl@42176
|
32 |
"~~~~~ fun get_the, args:"; val (theID:theID) = (["IsacKnowledge", "Test", "Rulesets", "ac_plus_times"]);
|
|
akargl@42176
|
33 |
(*get_py (Thy_Info.get_theory "Pure") theID theID (! thehier);
|
|
akargl@42176
|
34 |
(* ERROR: get_pbt not found: ["IsacKnowledge","Test","Rulesets","ac_plus_times"] *)*)
|
|
akargl@42176
|
35 |
print_depth 999;
|
|
akargl@42176
|
36 |
(!thehier);
|
|
akargl@42176
|
37 |
|
|
akargl@42176
|
38 |
(*"~~~~~ fun get_py, args:"; val (thy, d, _, []) = ((Thy_Info.get_theory "Pure"), theID, theID, (! thehier));*)
|
|
akargl@42176
|
39 |
"~~~~~ fun get_py, args:"; val (thy, d, _, [_]) = ((Thy_Info.get_theory "Pure"), theID, theID, (!thehier));
|
|
akargl@42176
|
40 |
error ("get_pbt not found: "^(strs2str d));
|
|
akargl@42176
|
41 |
(*AK110725 To be continued...s*)
|
|
akargl@42176
|
42 |
*)
|
|
akargl@42176
|
43 |
|
|
akargl@42176
|
44 |
val Hrls {thy_rls = (_,Rls {rules = rules as rule::_,...}),...} = thydata;
|
|
neuper@37906
|
45 |
|
|
neuper@37906
|
46 |
(*for rule2xml...*)
|
|
neuper@37906
|
47 |
val (j, thyID, Thm (thmID, thm)) = (2, thyID, rule);
|
|
neuper@37906
|
48 |
val (isa, thyID') = thy_containing_thm thyID thmID;
|
|
neuper@37906
|
49 |
val guh = thm2guh (isa, thyID') thmID;
|
|
neuper@37906
|
50 |
writeln (rules2xml 2 "Test" rules);
|
|
neuper@37906
|
51 |
|
|
neuper@37906
|
52 |
|
|
neuper@37906
|
53 |
"----------- fun thm''2xml ---------------------------------------";
|
|
neuper@37906
|
54 |
"----------- fun thm''2xml ---------------------------------------";
|
|
neuper@37906
|
55 |
"----------- fun thm''2xml ---------------------------------------";
|
|
akargl@42176
|
56 |
|
|
neuper@37906
|
57 |
show_thes();
|
|
neuper@37906
|
58 |
val theID = ["IsacKnowledge", "Diff", "Theorems", "frac_conv"];
|
|
neuper@37906
|
59 |
val thydata = get_the theID;
|
|
neuper@37906
|
60 |
val Hthm {guh=guh, thm=thm, mathauthors=ma, coursedesign=co} = thydata;
|
|
neuper@37906
|
61 |
writeln(thydata2xml (theID, thydata));
|
|
neuper@37906
|
62 |
"----- check 'manually' ...0 < ?n |] ==> ?a... -----";
|
|
neuper@37906
|
63 |
"----------------------------^^^---------^^^------------";
|
|
neuper@37906
|
64 |
|
|
neuper@37906
|
65 |
|
|
neuper@37906
|
66 |
|
|
neuper@37906
|
67 |
(* use"../smltest/xmlsrc/datatypes.sml";
|
|
akargl@42176
|
68 |
*)
|
|
akargl@42176
|
69 |
============ inhibit exn AK110725 ==============================================*)
|