1 (* export problem-data and method-data to xml
5 use"xmlsrc/pbl-met-hierarchy.sml";
6 use"pbl-met-hierarchy.sml";
9 fun str2file (fnm:filename) (str:string) =
10 let val file = TextIO.openOut fnm
11 in (TextIO.output (file, str);
13 TextIO.closeOut file) end;
14 fun pos2filename [] = 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
20 fun id2filename [] = 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
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)) =
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' ^
41 (nds (i+j) (lev_dn p') ns) ^
42 (indt i) ^ "</NODE>\n"
45 | nds i p (n::ns) = (nd i p n) ^ (nds i (lev_on p) ns);
47 (*.create a hierarchy with references to the guh's.*)
49 let val j = indentation
50 fun nd i p (Ptyp (id,[n as {guh,...} : pbt],ns)) =
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 ^
58 (nds (i+j) (lev_dn p') ns) ^
59 (indt i) ^ "</NODE>\n"
62 | nds i p (n::ns) = (nd i p n) ^ (nds i (lev_on p) ns);
63 in nds j [0] h : xml end;
65 let val j = indentation
66 fun nd i p (Ptyp (id,[n as {guh,...} : met],ns)) =
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 ^
74 (nds (i+j) (lev_dn p') ns) ^
75 (indt i) ^ "</NODE>\n"
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);
83 fun pbl_hierarchy2file (path:path) =
84 str2file (path ^ "pbl_hierarchy.xml")
86 " <ID> problem hierarchy </ID>\n" ^
88 " <CONTENTREF> pbl_ROOT </CONTENTREF>\n" ^
89 (hierarchy_pbl (!ptyps)) ^
92 fun met_hierarchy2file (path:path) =
93 str2file (path ^ "met_hierarchy.xml")
95 " <ID> method hierarchy </ID>\n" ^
97 " <CONTENTREF> met_ROOT </CONTENTREF>\n" ^
98 (hierarchy_met (!mets)) ^
103 (**.create the xml-files for the pbls, mets from the hierarchy.**)
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
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,
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 --------------------------------*)
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
154 (*.format a problem in xml for presentation on the problem browser;
155 old version with 'dead' strings for rls, calc, ....*)
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);
163 fun pbl2xml (id:(*pblRD*)pblID) ({guh,mathauthors,init,cas,met,ppc,prls,
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 --------------------------------*)
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;
193 val pblID = ["linear","univariate","equation"];
194 val pblID = ["degree_4","polynomial","univariate","equation"];
195 writeln (pbl2xml pblID (get_pbt pblID));
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;
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"]);
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" ^
225 indt i ^ "<META> </META>\n" ^
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
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) =
255 indt i ^ "<GUH> " ^ guh ^ " </GUH>\n" ^
257 indt i ^ "<META> </META>\n" ^
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;
273 (* writeln (met2xml ["Test", "solve_linear"]
274 (get_met ["Test", "solve_linear"]));
277 (**. write pbls from hierarchy to files.**)
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
285 (*.write the files using the guh as filename.*)
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
292 (**. write mets from hierarchy to files.**)
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);
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);
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);
315 fun pbls2file (p:path) = nodes p [] [0] pbl2file (!ptyps);
316 fun mets2file (p:path) = nodes p [] [0] met2file (!mets);
318 val path = "/home/neuper/proto2/isac/xmldata/";
319 val path = "/home/neuper/tmp/";
321 pbl_hierarchy2file (path ^ "pbl/");
322 pbls2file (path ^ "pbl/");
324 met_hierarchy2file (path ^ "met/");
325 mets2file (path ^ "met/");
327 thy_hierarchy2file (path ^ "thy/");
328 thes2file (path ^ "thy/");