akargl@42176
|
1 |
(* Title: tests for sml/xmlsrc/pbl-met-hierarchy.sml
|
akargl@42176
|
2 |
Author: Walther Neuper 060209
|
neuper@37906
|
3 |
(c) isac-team 2006
|
neuper@37906
|
4 |
|
neuper@37906
|
5 |
use"../smltest/xmlsrc/pbl-met-hierarchy.sml";
|
neuper@37906
|
6 |
use"pbl-met-hierarchy.sml";
|
neuper@37906
|
7 |
|
neuper@37906
|
8 |
CAUTION with testing *2file functions -- they are actually writing !!!
|
neuper@37906
|
9 |
*)
|
neuper@37906
|
10 |
|
wneuper@59592
|
11 |
val thy = @{theory "Isac_Knowledge"};
|
neuper@37906
|
12 |
|
neuper@37906
|
13 |
"-----------------------------------------------------------------";
|
neuper@37906
|
14 |
"table of contents -----------------------------------------------";
|
neuper@37906
|
15 |
"-----------------------------------------------------------------";
|
neuper@42404
|
16 |
"----- pbl2xml ---------------------------------------------------";
|
neuper@42404
|
17 |
"----- ERROR Illegal reference to internal variable: 'Pure_' -----";
|
neuper@42404
|
18 |
"----- fun pbl2term ----------------------------------------------";
|
neuper@42453
|
19 |
"----- fun insert_errpats ----------------------------------------";
|
neuper@37906
|
20 |
"-----------------------------------------------------------------";
|
neuper@37906
|
21 |
"-----------------------------------------------------------------";
|
neuper@37906
|
22 |
"-----------------------------------------------------------------";
|
neuper@37906
|
23 |
|
neuper@37906
|
24 |
|
neuper@37906
|
25 |
|
neuper@42404
|
26 |
"----- pbl2xml ---------------------------------------------------";
|
neuper@42404
|
27 |
"----- pbl2xml ---------------------------------------------------";
|
neuper@42404
|
28 |
"----- pbl2xml ---------------------------------------------------";
|
neuper@37906
|
29 |
(*what to do if from 'pbls2file "../../xmldata/pbl/";' you get the error
|
neuper@37906
|
30 |
|
neuper@37906
|
31 |
### pbl2file: id = ["Biegelinie"]
|
wneuper@59585
|
32 |
*** Type unification failed: Clash of types "fun" and "Program.ID".
|
neuper@37906
|
33 |
*** Type error in application: Incompatible operand type.
|
neuper@37906
|
34 |
***
|
neuper@37906
|
35 |
*** Operator: Problem :: ID * ID list => ??'a
|
neuper@37906
|
36 |
*** Operand: (Biegelinie, [Biegelinie]) ::
|
neuper@37906
|
37 |
*** ((real => real) => una) * ((real => real) => una) list
|
neuper@37906
|
38 |
***
|
neuper@37906
|
39 |
Exception- OPTION raised
|
neuper@37906
|
40 |
*)
|
akargl@42176
|
41 |
|
neuper@42406
|
42 |
if pbl2xml ["Biegelinien"] (get_pbt ["Biegelinien"]) =
|
neuper@42406
|
43 |
"<NODECONTENT>\n"^
|
neuper@42406
|
44 |
" <GUH> pbl_bieg </GUH>\n"^
|
neuper@42406
|
45 |
" <STRINGLIST>\n"^
|
neuper@42406
|
46 |
" <STRING> Biegelinien </STRING>\n"^
|
neuper@42406
|
47 |
" </STRINGLIST>\n <META> </META>\n"^
|
neuper@42406
|
48 |
" <HEADLINE>\n"^
|
neuper@42406
|
49 |
" <MATHML>\n"^
|
neuper@42406
|
50 |
" <ISA> Problem (Biegelinie', [Biegelinien]) </ISA>\n"^
|
neuper@42406
|
51 |
" </MATHML>\n"^
|
neuper@42406
|
52 |
" </HEADLINE>\n"^
|
wneuper@59252
|
53 |
|
neuper@42406
|
54 |
" <GIVEN>\n"^
|
neuper@42406
|
55 |
" <MATHML>\n"^
|
neuper@42406
|
56 |
" <ISA> Traegerlaenge l_l </ISA>\n"^
|
neuper@42406
|
57 |
" </MATHML>\n"^
|
neuper@42406
|
58 |
" <MATHML>\n"^
|
neuper@42406
|
59 |
" <ISA> Streckenlast q_q </ISA>\n"^
|
neuper@42406
|
60 |
" </MATHML> </GIVEN>\n <WHERE> </WHERE>\n"^
|
neuper@42406
|
61 |
" <FIND>\n"^
|
neuper@42406
|
62 |
" <MATHML>\n"^
|
neuper@42406
|
63 |
" <ISA> Biegelinie b_b </ISA>\n"^
|
neuper@42406
|
64 |
" </MATHML> </FIND>\n"^
|
neuper@42406
|
65 |
" <RELATE>\n"^
|
neuper@42406
|
66 |
" <MATHML>\n"^
|
neuper@42406
|
67 |
" <ISA> Randbedingungen r_b </ISA>\n"^
|
neuper@42406
|
68 |
" </MATHML> </RELATE>\n"^
|
wneuper@59252
|
69 |
|
neuper@42406
|
70 |
" <EXPLANATIONS> </EXPLANATIONS>\n"^
|
neuper@42406
|
71 |
" <THEORY>\n"^
|
neuper@42406
|
72 |
" <KESTOREREF>\n"^
|
neuper@42406
|
73 |
" <TAG> Theorem </TAG>\n"^
|
neuper@42406
|
74 |
" <ID> </ID>\n"^
|
neuper@42406
|
75 |
" <GUH> thy_isac_Biegelinie-thm- </GUH>\n"^
|
neuper@42406
|
76 |
" </KESTOREREF>\n"^
|
neuper@42406
|
77 |
" </THEORY>\n"^
|
wneuper@59252
|
78 |
|
neuper@42406
|
79 |
" <METHODS>\n"^
|
neuper@42406
|
80 |
" <KESTOREREF>\n"^
|
neuper@42406
|
81 |
" <TAG> Method</TAG>\n"^
|
neuper@42406
|
82 |
" <ID> [IntegrierenUndKonstanteBestimmen2] </ID>\n"^
|
neuper@42406
|
83 |
" <GUH> met_biege_2 </GUH>\n"^
|
neuper@42406
|
84 |
" </KESTOREREF>\n"^
|
neuper@42406
|
85 |
" </METHODS>\n"^
|
wneuper@59252
|
86 |
|
walther@59852
|
87 |
" <EVALPRECOND> empty </EVALPRECOND>\n"^
|
neuper@42406
|
88 |
" <MATHAUTHORS>\n"^
|
neuper@42406
|
89 |
" </MATHAUTHORS>\n"^
|
neuper@42406
|
90 |
" <COURSEDESIGNS>\n"^
|
neuper@42406
|
91 |
" <STRING> isac team 2006 </STRING>\n"^
|
neuper@42406
|
92 |
" </COURSEDESIGNS>\n"^
|
neuper@42406
|
93 |
"</NODECONTENT>"
|
neuper@42406
|
94 |
then () else error "fun pbl2xml 'Biegelinien' changed";
|
akargl@42176
|
95 |
|
neuper@37906
|
96 |
(* val id = ["Biegelinie"];
|
neuper@37906
|
97 |
val {(*guh,*)cas,met,ppc,prls,thy,where_} = get_pbt ["Biegelinie"];
|
neuper@37906
|
98 |
AND STEP THROUGH pbl2xml ...
|
neuper@37906
|
99 |
|
neuper@37906
|
100 |
term2xml i (pbl2term thy id);
|
neuper@37906
|
101 |
pbl2term thy id;
|
neuper@37906
|
102 |
*)
|
neuper@37906
|
103 |
(* val (thy, pblRD) = (thy, id);
|
neuper@37906
|
104 |
AND STEP THROUGH pbl2term...
|
neuper@37906
|
105 |
|
neuper@37906
|
106 |
val str = ("Problem (" ^
|
neuper@37906
|
107 |
(get_thy o theory2domID) thy ^ ", " ^
|
neuper@37906
|
108 |
(strs2str' o rev) pblRD ^ ")");
|
neuper@37906
|
109 |
str2term str;
|
neuper@37906
|
110 |
str2term "Biegelinie";
|
neuper@37906
|
111 |
str2term "Biegelinien";
|
neuper@37906
|
112 |
*)
|
neuper@37906
|
113 |
(*Const
|
neuper@37906
|
114 |
("Biegelinie.Biegelinie",
|
neuper@55279
|
115 |
"("Real.real => "Real.real) => Tools.una") : Term.term
|
wneuper@59585
|
116 |
..I.E. THE "Program.ID" _WAS_ ALREADY OCCUPIED BY A 'description'*)
|
neuper@37906
|
117 |
|
akargl@42176
|
118 |
|
neuper@42404
|
119 |
"----- ERROR Illegal reference to internal variable: 'Pure_' -----";
|
neuper@42404
|
120 |
"----- ERROR Illegal reference to internal variable: 'Pure_' -----";
|
neuper@42404
|
121 |
"----- ERROR Illegal reference to internal variable: 'Pure_' -----";
|
neuper@42404
|
122 |
val path = "/tmp/";
|
walther@59687
|
123 |
"~~~~~ fun pbls2file, args:"; val (p:filepath) = (path ^ "pbl/");
|
s1210629013@55354
|
124 |
get_ptyps (); (*not = []*)
|
neuper@42404
|
125 |
"~~~~~ fun nodes, args:"; val (pa, ids, po, wfn, (n::ns)) =
|
s1210629013@55354
|
126 |
(p, []: string list, [0], pbl2file, (get_ptyps ()));
|
walther@59897
|
127 |
"~~~~~ fun node, args:"; val (pa:filepath, ids, po, wfn, Store.Node (id,[n],ns)) = (pa, ids, po, wfn, n);
|
neuper@42404
|
128 |
val po' = lev_on po;
|
neuper@42404
|
129 |
wfn (*= pbl2file*)
|
walther@59898
|
130 |
"~~~~~ fun pbl2file, args:"; val ((path:filepath), (pos:pos), (id: Spec.metID), (pbl as {guh,...})) =
|
neuper@42404
|
131 |
(pa, po', (ids@[id]), n);
|
neuper@42404
|
132 |
strs2str id = "[\"e_pblID\"]"; (*true*)
|
neuper@42404
|
133 |
pos2str pos = "[1]"; (*true*)
|
neuper@42404
|
134 |
path ^ guh2filename guh = "/tmp/pbl/pbl_empty.xml"; (*true*)
|
walther@59898
|
135 |
"~~~~~ fun pbl2xml, args:"; val (id: Spec.pblID, {guh,mathauthors,init,cas,met,ppc,prls,thy,where_}) =
|
neuper@42404
|
136 |
(id, pbl);
|
neuper@42404
|
137 |
"~~~~~ fun pbl2term, args:"; val (thy, (pblRD:pblRD)) = (thy, id);
|
walther@59881
|
138 |
if ("Problem (" ^ Context.theory_name thy ^ "', " ^ (strs2str' o rev) pblRD ^ ")") =
|
neuper@42404
|
139 |
"Problem (Pure', [e_pblID])"
|
neuper@42404
|
140 |
then () else error "fun pbl2term changed";
|
neuper@42404
|
141 |
|
neuper@42406
|
142 |
|
neuper@42404
|
143 |
"----- fun pbl2term ----------------------------------------------";
|
neuper@42404
|
144 |
"----- fun pbl2term ----------------------------------------------";
|
neuper@42404
|
145 |
"----- fun pbl2term ----------------------------------------------";
|
neuper@42404
|
146 |
(*see WN120405a.TODO.txt*)
|
walther@59879
|
147 |
if UnparseC.term (pbl2term (ThyC.get_theory "Isac_Knowledge") ["equations","univariate","normalise"]) =
|
wneuper@59592
|
148 |
"Problem (Isac_Knowledge', [normalise, univariate, equations])"
|
neuper@42404
|
149 |
then () else error "fun pbl2term changed";
|
neuper@42404
|
150 |
|
neuper@42453
|
151 |
"----- fun insert_errpats ----------------------------------------";
|
neuper@42453
|
152 |
"----- fun insert_errpats ----------------------------------------";
|
neuper@42453
|
153 |
"----- fun insert_errpats ----------------------------------------";
|
neuper@42456
|
154 |
(* vv--- here intermediate save/restore does not work and affects other tests ---vv
|
neuper@42456
|
155 |
see test/../calcelems.sml --- Unsynchronized.ref doesn't work any more ---
|
neuper@42456
|
156 |
|
neuper@42453
|
157 |
val errpatstest =
|
neuper@42453
|
158 |
[("chain-rule-diff-both",
|
neuper@42453
|
159 |
[parse_patt @{theory} "d_d ?bdv (sin ?u) = cos (d_d ?bdv ?u)",
|
neuper@42453
|
160 |
parse_patt @{theory} "d_d ?bdv (cos ?u) = - sin (d_d ?bdv ?u)",
|
neuper@42453
|
161 |
parse_patt @{theory} "d_d ?bdv (?u ^^^ ?n) = ?n * ?u ^^^ (?n - 1)",
|
neuper@42453
|
162 |
parse_patt @{theory} "d_d ?bdv (LogExp.ln ?u) = 1 / ?u",
|
neuper@42453
|
163 |
parse_patt @{theory} "d_d ?bdv (LogExp.ln ?u) = 1 / d_d ?bdv ?u"],
|
neuper@42453
|
164 |
[@{thm diff_sin_chain}, @{thm diff_cos_chain}, @{thm diff_pow_chain},
|
neuper@42453
|
165 |
@{thm diff_ln_chain}, @{thm diff_exp_chain}])];
|
neuper@42453
|
166 |
|
neuper@42453
|
167 |
insert_errpats ["diff","differentiate_on_R"] errpatstest;
|
neuper@42453
|
168 |
|
neuper@42453
|
169 |
val {errpats, ...} = get_met ["diff","differentiate_on_R"];
|
neuper@42453
|
170 |
case errpats of
|
neuper@42453
|
171 |
("chain-rule-diff-both", _, _) :: _ => ()
|
neuper@42456
|
172 |
| _ => error "insert_errpats chain-rule-diff-both changed";
|
neuper@42456
|
173 |
^^^^^--- here intermediate save/restore does not work and affects other tests ---^^*)
|
neuper@42453
|
174 |
|