|
1 (* export problem-data and method-data to xml |
|
2 author: Walther Neuper |
|
3 (c) isac-team |
|
4 |
|
5 use"xmlsrc/pbl-met-hierarchy.sml"; |
|
6 use"pbl-met-hierarchy.sml"; |
|
7 *) |
|
8 |
|
9 fun str2file (fnm:filename) (str:string) = |
|
10 let val file = TextIO.openOut fnm |
|
11 in (TextIO.output (file, str); |
|
12 TextIO.flushOut file; |
|
13 TextIO.closeOut file) end; |
|
14 fun pos2filename [] = raise error "pos2filename called with []" |
|
15 | pos2filename [i] = "_" ^ string_of_int i ^ ".xml" |
|
16 | pos2filename (i::is) = "_" ^ string_of_int i ^ pos2filename is; |
|
17 (* pos2filename [1,22,3]; |
|
18 val it = "_1_22_3.xml" : string |
|
19 *) |
|
20 fun id2filename [] = raise error "id2filename called with []" |
|
21 | id2filename [s] = s ^ ".xml" |
|
22 | id2filename (s::ss) = s ^ "_" ^ id2filename ss; |
|
23 (* id2filename ["linear","univariate","equation"]; |
|
24 val it = "linear_univariate_equation.xml" : string |
|
25 *) |
|
26 |
|
27 |
|
28 |
|
29 (*ad DTD: a NODE contains an ID and zero or more NODEs*) |
|
30 (*old version with pos2filename*) |
|
31 fun hierarchy pm(*"pbl" | "met"*) h = |
|
32 let val j = indentation |
|
33 fun nd i p (Ptyp (id,_,ns)) = |
|
34 let val p' = lev_on p |
|
35 in (indt i) ^ "<NODE>\n" ^ |
|
36 (indt (i+j)) ^ "<ID> " ^ id ^ " </ID>\n" ^ |
|
37 (indt (i+j)) ^ "<NO> " (*on this level*) ^ |
|
38 (string_of_int o last_elem) p' ^ " </NO>\n" ^ |
|
39 (indt (i+j)) ^ "<CONTENTREF> " ^ pm ^ pos2filename p' ^ |
|
40 " </CONTENTREF>\n" ^ |
|
41 (nds (i+j) (lev_dn p') ns) ^ |
|
42 (indt i) ^ "</NODE>\n" |
|
43 end |
|
44 and nds _ _ [] = "" |
|
45 | nds i p (n::ns) = (nd i p n) ^ (nds i (lev_on p) ns); |
|
46 in nds j [0] h end; |
|
47 (*.create a hierarchy with references to the guh's.*) |
|
48 fun hierarchy_pbl h = |
|
49 let val j = indentation |
|
50 fun nd i p (Ptyp (id,[n as {guh,...} : pbt],ns)) = |
|
51 let val p' = lev_on p |
|
52 in (indt i) ^ "<NODE>\n" ^ |
|
53 (indt (i+j)) ^ "<ID> " ^ id ^ " </ID>\n" ^ |
|
54 (indt (i+j)) ^ "<NO> " (*on this level*) ^ |
|
55 (string_of_int o last_elem) p' ^ " </NO>\n" ^ |
|
56 (indt (i+j)) ^ "<CONTENTREF> " ^ guh ^ |
|
57 " </CONTENTREF>\n" ^ |
|
58 (nds (i+j) (lev_dn p') ns) ^ |
|
59 (indt i) ^ "</NODE>\n" |
|
60 end |
|
61 and nds _ _ [] = "" |
|
62 | nds i p (n::ns) = (nd i p n) ^ (nds i (lev_on p) ns); |
|
63 in nds j [0] h : xml end; |
|
64 fun hierarchy_met h = |
|
65 let val j = indentation |
|
66 fun nd i p (Ptyp (id,[n as {guh,...} : met],ns)) = |
|
67 let val p' = lev_on p |
|
68 in (indt i) ^ "<NODE>\n" ^ |
|
69 (indt (i+j)) ^ "<ID> " ^ id ^ " </ID>\n" ^ |
|
70 (indt (i+j)) ^ "<NO> " (*on this level*) ^ |
|
71 (string_of_int o last_elem) p' ^ " </NO>\n" ^ |
|
72 (indt (i+j)) ^ "<CONTENTREF> " ^ guh ^ |
|
73 " </CONTENTREF>\n" ^ |
|
74 (nds (i+j) (lev_dn p') ns) ^ |
|
75 (indt i) ^ "</NODE>\n" |
|
76 end |
|
77 and nds _ _ [] = "" |
|
78 | nds i p (n::ns) = (nd i p n) ^ (nds i (lev_on p) ns); |
|
79 in nds j [0] h : xml end; |
|
80 (* (writeln o hierarchy_pbl) (!ptyps); |
|
81 *) |
|
82 |
|
83 fun pbl_hierarchy2file (path:path) = |
|
84 str2file (path ^ "pbl_hierarchy.xml") |
|
85 ("<NODE>\n" ^ |
|
86 " <ID> problem hierarchy </ID>\n" ^ |
|
87 " <NO> 1 </NO>\n" ^ |
|
88 " <CONTENTREF> pbl_ROOT </CONTENTREF>\n" ^ |
|
89 (hierarchy_pbl (!ptyps)) ^ |
|
90 "</NODE>"); |
|
91 |
|
92 fun met_hierarchy2file (path:path) = |
|
93 str2file (path ^ "met_hierarchy.xml") |
|
94 ("<NODE>\n" ^ |
|
95 " <ID> method hierarchy </ID>\n" ^ |
|
96 " <NO> 1 </NO>\n" ^ |
|
97 " <CONTENTREF> met_ROOT </CONTENTREF>\n" ^ |
|
98 (hierarchy_met (!mets)) ^ |
|
99 "</NODE>"); |
|
100 |
|
101 |
|
102 |
|
103 (**.create the xml-files for the pbls, mets from the hierarchy.**) |
|
104 |
|
105 val i = indentation; |
|
106 |
|
107 fun pbl2term thy (pblRD:pblRD) = |
|
108 str2term ("Problem (" ^ |
|
109 (get_thy o theory2domID) thy ^ "_, " ^ |
|
110 (strs2str' o rev) pblRD ^ ")"); |
|
111 (* term2str (pbl2term Isac.thy ["equations","univariate","normalize"]); |
|
112 val it = "Problem (Isac, [normalize, univariate, equations])" : string |
|
113 *) |
|
114 |
|
115 |
|
116 (*.format a problem in xml for presentation on the problem browser; |
|
117 new version with <KESTOREREF>s -- not used because linking |
|
118 requires elements (rls, calc, ...) to be reorganized.*) |
|
119 (*######## ATTENTION: THIS IS not THE ACTUAL VERSION ################*) |
|
120 fun pbl2xml (id:(*pblRD*)pblID) ({guh,mathauthors,init,cas,met,ppc,prls, |
|
121 thy,where_}:pbt) = |
|
122 let val thy' = theory2theory' thy |
|
123 val prls' = (#id o rep_rls) prls |
|
124 in "<NODECONTENT>\n" ^ |
|
125 indt i ^ "<GUH> " ^ guh ^ " </GUH>\n" ^ |
|
126 (((id2xml i)(* o rev*)) id) ^ |
|
127 indt i ^ "<META> </META>\n" ^ |
|
128 (*--------------- begin display ------------------------------*) |
|
129 indt i ^ "<HEADLINE>\n" ^ |
|
130 (case cas of None => term2xml i (pbl2term thy id) |
|
131 | Some t => term2xml i t) ^ "\n" ^ |
|
132 indt i ^ "</HEADLINE>\n" ^ |
|
133 (*--------------- hline --------------------------------------*) |
|
134 pattern2xml i ppc where_ ^ |
|
135 (*--------------- hline --------------------------------------*) |
|
136 indt i ^ "<EXPLANATIONS> </EXPLANATIONS>\n" |
|
137 (*--------------- end display --------------------------------*) |
|
138 ^ |
|
139 indt i ^ "<THEORY>\n" ^ |
|
140 theref2xml (i+i) thy' "Theorems" "" ^ |
|
141 indt i ^ "</THEORY>\n" ^ |
|
142 (case met of [] => (indt i) ^ "<METHODS> </METHODS>\n" |
|
143 | _ => (indt i) ^ "<METHODS>\n" ^ |
|
144 foldl op^ ("", map (keref2xml (i+i) Met_) met) ^ |
|
145 (indt i) ^ "</METHODS>\n") ^ |
|
146 indt i ^ "<EVALPRECOND>\n" ^ |
|
147 theref2xml (i+i) (snd (thy_containing_rls thy' prls')) "Rulesets" prls'^ |
|
148 indt i ^ "</EVALPRECOND>\n" ^ |
|
149 authors2xml i "MATHAUTHORS" mathauthors ^ |
|
150 authors2xml i "COURSEDESIGNS" ["isac team 2006"] ^ |
|
151 "</NODECONTENT>" : xml |
|
152 end; |
|
153 |
|
154 (*.format a problem in xml for presentation on the problem browser; |
|
155 old version with 'dead' strings for rls, calc, ....*) |
|
156 (* |
|
157 val pblID = ["linear","univariate","equation"]; |
|
158 val pblID = ["degree_4","polynomial","univariate","equation"]; |
|
159 val pblID = rev ["tool","find_values"]; |
|
160 val (id, {guh,mathauthors,init,cas,met,ppc,prls,thy,where_}:pbt) = |
|
161 (pblID, get_pbt pblID); |
|
162 *) |
|
163 fun pbl2xml (id:(*pblRD*)pblID) ({guh,mathauthors,init,cas,met,ppc,prls, |
|
164 thy,where_}:pbt) = |
|
165 "<NODECONTENT>\n" ^ |
|
166 indt i ^ "<GUH> " ^ guh ^ " </GUH>\n" ^ |
|
167 (((id2xml i)(* o rev*)) id) ^ |
|
168 indt i ^ "<META> </META>\n" ^ |
|
169 (*--------------- begin display ------------------------------*) |
|
170 indt i ^ "<HEADLINE>\n" ^ |
|
171 (case cas of None => term2xml i (pbl2term thy id) |
|
172 | Some t => term2xml i t) ^ "\n" ^ |
|
173 indt i ^ "</HEADLINE>\n" ^ |
|
174 (*--------------- hline --------------------------------------*) |
|
175 pattern2xml i ppc where_ ^ |
|
176 (*--------------- hline --------------------------------------*) |
|
177 indt i ^ "<EXPLANATIONS> </EXPLANATIONS>\n" |
|
178 (*--------------- end display --------------------------------*) |
|
179 ^ |
|
180 indt i ^ "<THEORY>\n" ^ |
|
181 theref2xml (i+i) (theory2theory' thy) "Theorems" "" ^ |
|
182 indt i ^ "</THEORY>\n" ^ |
|
183 (case met of [] => (indt i) ^ "<METHODS> </METHODS>\n" |
|
184 | _ => (indt i) ^ "<METHODS>\n" ^ |
|
185 foldl op^ ("", map (keref2xml (i+i) Met_) met) ^ |
|
186 (indt i) ^ "</METHODS>\n") ^ |
|
187 indt i ^ "<EVALPRECOND> " ^ (#id o rep_rls) |
|
188 prls ^ " </EVALPRECOND>\n" ^ |
|
189 authors2xml i "MATHAUTHORS" mathauthors ^ |
|
190 authors2xml i "COURSEDESIGNS" ["isac team 2006"] ^ |
|
191 "</NODECONTENT>" : xml; |
|
192 (* |
|
193 val pblID = ["linear","univariate","equation"]; |
|
194 val pblID = ["degree_4","polynomial","univariate","equation"]; |
|
195 writeln (pbl2xml pblID (get_pbt pblID)); |
|
196 *) |
|
197 |
|
198 (*replace by 'fun calc2xml' as developed for thy in 0607*) |
|
199 fun calc2xmlOLD j ((scr_op, (isa_op, _)):calc) = |
|
200 indt i ^ "<CALCULATE> (" ^ scr_op ^ ", (" ^ isa_op ^ ")) </CALCULATE>\n"; |
|
201 fun calcs2xmlOLD j [] = ("":xml) (*TODO replace with 'strs2xml'*) |
|
202 | calcs2xmlOLD j (r::rs) = calc2xmlOLD j r ^ calcs2xmlOLD j rs; |
|
203 |
|
204 (* val (id, {guh,mathauthors,init,ppc,pre,scr,calc, |
|
205 crls,erls,nrls,prls,srls,rew_ord'}) = |
|
206 (["Test", "solve_linear"], |
|
207 get_met ["Test", "solve_linear"]); |
|
208 *) |
|
209 |
|
210 (*.format a method in xml for presentation on the method browser; |
|
211 new version with <KESTOREREF>s -- not used because linking |
|
212 requires elements (rls, calc, ...) to be reorganized.*) |
|
213 (*######## ATTENTION: THIS IS not THE ACTUAL VERSION ################*) |
|
214 fun met2xml (id:metID) ({guh,mathauthors,init,ppc,pre,scr,calc, |
|
215 crls,erls,nrls,prls,srls,rew_ord'}:met) = |
|
216 let val thy' = "Isac.thy" (*FIXME.WN0607 get thy from met ?!?*) |
|
217 val crls' = (#id o rep_rls) crls |
|
218 val erls' = (#id o rep_rls) erls |
|
219 val nrls' = (#id o rep_rls) nrls |
|
220 val prls' = (#id o rep_rls) prls |
|
221 val srls' = (#id o rep_rls) srls |
|
222 in "<NODECONTENT>\n" ^ |
|
223 indt i ^ "<GUH> " ^ guh ^ " </GUH>\n" ^ |
|
224 id2xml i id ^ |
|
225 indt i ^ "<META> </META>\n" ^ |
|
226 scr2xml i scr ^ |
|
227 pattern2xml i ppc pre ^ |
|
228 indt i ^ "<EXPLANATIONS> </EXPLANATIONS>\n" ^ |
|
229 indt i ^ "<EVALPRECOND>\n" ^ |
|
230 theref2xml (i+i) (snd (thy_containing_rls thy' prls')) "Rulesets" prls'^ |
|
231 indt i ^ "</EVALPRECOND>\n" ^ |
|
232 indt i ^ "<EVALCOND>\n" ^ |
|
233 theref2xml (i+i) (snd (thy_containing_rls thy' erls')) "Rulesets" erls'^ |
|
234 indt i ^ "</EVALCOND>\n" ^ |
|
235 indt i ^ "<EVALLISTEXPR>\n"^ |
|
236 theref2xml (i+i) (snd (thy_containing_rls thy' srls')) "Rulesets" srls'^ |
|
237 indt i ^ "</EVALLISTEXPR>\n" ^ |
|
238 indt i ^ "<CHECKELEMENTWISE>\n" ^ |
|
239 theref2xml (i+i) (snd (thy_containing_rls thy' crls')) "Rulesets" crls'^ |
|
240 indt i ^ "</CHECKELEMENTWISE>\n" ^ |
|
241 indt i ^ "<NORMALFORM>\n" ^ |
|
242 theref2xml (i+i) (snd (thy_containing_rls thy' nrls')) "Rulesets" nrls'^ |
|
243 indt i ^ "</NORMALFORM>\n" ^ |
|
244 indt i ^ "<REWORDER> " ^ rew_ord' ^ " </REWORDER>\n" ^ |
|
245 calcs2xmlOLD i calc ^ |
|
246 authors2xml i "MATHAUTHORS" mathauthors ^ |
|
247 authors2xml i "COURSEDESIGNS" ["isac team 2006"] ^ |
|
248 "</NODECONTENT>" : xml |
|
249 end; |
|
250 (*.format a method in xml for presentation on the method browser; |
|
251 old version with 'dead' strings for rls, calc, ....*) |
|
252 fun met2xml (id:metID) ({guh,mathauthors,init,ppc,pre,scr,calc, |
|
253 crls,erls,nrls,prls,srls,rew_ord'}:met) = |
|
254 "<NODECONTENT>\n" ^ |
|
255 indt i ^ "<GUH> " ^ guh ^ " </GUH>\n" ^ |
|
256 id2xml i id ^ |
|
257 indt i ^ "<META> </META>\n" ^ |
|
258 scr2xml i scr ^ |
|
259 pattern2xml i ppc pre ^ |
|
260 indt i ^ "<EXPLANATIONS> </EXPLANATIONS>\n" ^ |
|
261 indt i ^ "<EVALPRECOND> " ^ (#id o rep_rls) prls ^ " </EVALPRECOND>\n" ^ |
|
262 indt i ^ "<EVALCOND> " ^ (#id o rep_rls) erls ^ " </EVALCOND>\n" ^ |
|
263 indt i ^ "<EVALLISTEXPR> "^ (#id o rep_rls) srls ^ " </EVALLISTEXPR>\n" ^ |
|
264 indt i ^ "<CHECKELEMENTWISE> " ^ (#id o rep_rls) |
|
265 crls ^ " </CHECKELEMENTWISE>\n" ^ |
|
266 indt i ^ "<NORMALFORM> " ^ (#id o rep_rls) nrls ^ " </NORMALFORM>\n" ^ |
|
267 indt i ^ "<REWORDER> " ^ rew_ord' ^ " </REWORDER>\n" ^ |
|
268 calcs2xmlOLD i calc ^ |
|
269 authors2xml i "MATHAUTHORS" mathauthors ^ |
|
270 authors2xml i "COURSEDESIGNS" ["isac team 2006"] ^ |
|
271 "</NODECONTENT>" : xml; |
|
272 |
|
273 (* writeln (met2xml ["Test", "solve_linear"] |
|
274 (get_met ["Test", "solve_linear"])); |
|
275 *) |
|
276 |
|
277 (**. write pbls from hierarchy to files.**) |
|
278 |
|
279 (*.write the files using an int-key (pos') as filename.*) |
|
280 fun pbl2file (path:path) (pos:pos) (id:metID) (pbl as {guh,...}) = |
|
281 (writeln ("### pbl2file: id = " ^ strs2str id); |
|
282 ((str2file (path ^ pos2filename pos)) o (pbl2xml id)) pbl |
|
283 ); |
|
284 |
|
285 (*.write the files using the guh as filename.*) |
|
286 (* *) |
|
287 fun pbl2file (path:path) (pos:pos) (id:metID) (pbl as {guh,...}) = |
|
288 (writeln ("### pbl2file: id = " ^ strs2str id ^ ", pos = " ^ pos2str pos); |
|
289 ((str2file (path ^ guh2filename guh)) o (pbl2xml id)) pbl |
|
290 ); |
|
291 |
|
292 (**. write mets from hierarchy to files.**) |
|
293 |
|
294 (*.write the files using an int-key (pos') as filename.*) |
|
295 fun met2file (path:path) (pos:pos) (id:metID) met = |
|
296 (writeln ("### met2file: id = " ^ strs2str id); |
|
297 ((str2file (path ^ "met" ^ pos2filename pos)) o (met2xml id)) met); |
|
298 |
|
299 (*.write the files using the guh as filename.*) |
|
300 fun met2file (path:path) (pos:pos) (id:metID) (met as {guh,...}) = |
|
301 (writeln ("### met2file: id = " ^ strs2str id); |
|
302 ((str2file (path ^ guh2filename guh)) o (met2xml id)) met); |
|
303 |
|
304 |
|
305 (*.scan the mtree Ptyp and and print the nodes using wfn.*) |
|
306 fun node (pa:path) ids po wfn (Ptyp (id,[n],ns)) = |
|
307 let val po' = lev_on po |
|
308 in wfn pa po' (ids@[id]) n; |
|
309 nodes pa (ids@[id]) ((lev_dn po'):pos) wfn ns end |
|
310 and nodes _ _ _ _ [] = () |
|
311 | nodes pa ids po wfn (n::ns) = (node pa ids po wfn n; |
|
312 nodes pa ids (lev_on po) wfn ns); |
|
313 |
|
314 |
|
315 fun pbls2file (p:path) = nodes p [] [0] pbl2file (!ptyps); |
|
316 fun mets2file (p:path) = nodes p [] [0] met2file (!mets); |
|
317 (* |
|
318 val path = "/home/neuper/proto2/isac/xmldata/"; |
|
319 val path = "/home/neuper/tmp/"; |
|
320 |
|
321 pbl_hierarchy2file (path ^ "pbl/"); |
|
322 pbls2file (path ^ "pbl/"); |
|
323 |
|
324 met_hierarchy2file (path ^ "met/"); |
|
325 mets2file (path ^ "met/"); |
|
326 |
|
327 thy_hierarchy2file (path ^ "thy/"); |
|
328 thes2file (path ^ "thy/"); |
|
329 *) |