Isabelle2015->17: completed "normalise" cf. fb6f5ef2c647
1 (* export problem-data and method-data to xml
2 author: Walther Neuper 2004
6 fun file2str (path : path) (fnm : filename) =
8 val file = TextIO.openIn (path ^ fnm)
9 val str = TextIO.inputAll file
10 in TextIO.closeIn file; str end
12 fun str2file (fnm : filename) (str : string) =
13 let val file = TextIO.openOut fnm
15 TextIO.output (file, str);
19 fun pos2filename [] = error "pos2filename called with []"
20 | pos2filename [i] = "_" ^ string_of_int i ^ ".xml"
21 | pos2filename (i::is) = "_" ^ string_of_int i ^ pos2filename is;
22 (* pos2filename [1,22,3];
23 val it = "_1_22_3.xml" : string
25 fun id2filename [] = error "id2filename called with []"
26 | id2filename [s] = s ^ ".xml"
27 | id2filename (s::ss) = s ^ "_" ^ id2filename ss;
28 (* id2filename ["linear","univariate","equation"];
29 val it = "linear_univariate_equation.xml" : string
32 (*ad DTD: a NODE contains an ID and zero or more NODEs*)
33 (*old version with pos2filename*)
34 fun hierarchy pm(*"pbl" | "met"*) h =
35 let val j = indentation
36 fun nd i p (Ptyp (id,_,ns)) =
37 let val p' = Ctree.lev_on p
38 in (indt i) ^ "<NODE>\n" ^
39 (indt (i+j)) ^ "<ID> " ^ id ^ " </ID>\n" ^
40 (indt (i+j)) ^ "<NO> " (*on this level*) ^
41 (string_of_int o last_elem) p' ^ " </NO>\n" ^
42 (indt (i+j)) ^ "<CONTENTREF> " ^ pm ^ pos2filename p' ^
44 (nds (i+j) (Ctree.lev_dn p') ns) ^
45 (indt i) ^ "</NODE>\n"
48 | nds i p (n::ns) = (nd i p n) ^ (nds i (Ctree.lev_on p) ns);
50 (*.create a hierarchy with references to the guh's.*)
52 let val j = indentation
53 fun nd i p (Ptyp (id,[n as {guh,...} : pbt],ns)) =
54 let val p' = Ctree.lev_on p
55 in (indt i) ^ "<NODE>\n" ^
56 (indt (i+j)) ^ "<ID> " ^ id ^ " </ID>\n" ^
57 (indt (i+j)) ^ "<NO> " (*on this level*) ^
58 (string_of_int o last_elem) p' ^ " </NO>\n" ^
59 (indt (i+j)) ^ "<CONTENTREF> " ^ guh ^
61 (nds (i+j) (Ctree.lev_dn p') ns) ^
62 (indt i) ^ "</NODE>\n"
65 | nds i p (n::ns) = (nd i p n) ^ (nds i (Ctree.lev_on p) ns);
66 in nds j [0] h : xml end;
68 let val j = indentation
69 fun nd i p (Ptyp (id,[n as {guh,...} : met],ns)) =
70 let val p' = Ctree.lev_on p
71 in (indt i) ^ "<NODE>\n" ^
72 (indt (i+j)) ^ "<ID> " ^ id ^ " </ID>\n" ^
73 (indt (i+j)) ^ "<NO> " (*on this level*) ^
74 (string_of_int o last_elem) p' ^ " </NO>\n" ^
75 (indt (i+j)) ^ "<CONTENTREF> " ^ guh ^
77 (nds (i+j) (Ctree.lev_dn p') ns) ^
78 (indt i) ^ "</NODE>\n"
81 | nds i p (n::ns) = (nd i p n) ^ (nds i (Ctree.lev_on p) ns);
82 in nds j [0] h : xml end;
83 (* (writeln o hierarchy_pbl) (!ptyps);
86 fun pbl_hierarchy2file (path:path) =
87 str2file (path ^ "pbl_hierarchy.xml")
89 " <ID> problem hierarchy </ID>\n" ^
91 " <CONTENTREF> pbl_ROOT </CONTENTREF>\n" ^
92 (hierarchy_pbl (get_ptyps ())) ^
95 fun met_hierarchy2file (path:path) =
96 str2file (path ^ "met_hierarchy.xml")
98 " <ID> method hierarchy </ID>\n" ^
100 " <CONTENTREF> met_ROOT </CONTENTREF>\n" ^
101 (hierarchy_met (get_mets ())) ^
104 (**.create the xml-files for the pbls, mets from the hierarchy.**)
106 (*.format a problem in xml for presentation on the problem browser;
107 new version with <KESTOREREF>s -- not used because linking
108 requires elements (rls, calc, ...) to be reorganized.*)
109 (*######## ATTENTION: THIS IS not THE ACTUAL VERSION ################*)
110 fun pbl2term thy (pblRD: Specify.pblRD) = (*WN120405.TODO.txt*)
111 str2term ("Problem (" ^ (get_thy o theory2domID) thy ^ "', " ^ (strs2str' o rev) pblRD ^ ")");
112 (* term2str (pbl2term (Thy_Info_get_theory "Isac") ["equations","univariate","normalise"]);
113 val it = "Problem (Isac, [normalise, univariate, equations])" : string
117 (* new version with <KESTOREREF>s -- not used *)
118 fun pbl2xml (id:(*pblRD*)pblID) ({guh,mathauthors,init,cas,met,ppc,prls,
120 let val thy' = theory2theory' thy
121 val prls' = (#id o rep_rls) prls
122 in "<NODECONTENT>\n" ^
123 indt i ^ "<GUH> " ^ guh ^ " </GUH>\n" ^
124 (((id2xml i)(* o rev*)) id) ^
125 indt i ^ "<META> </META>\n" ^
126 (*--------------- begin display ------------------------------*)
127 indt i ^ "<HEADLINE>\n" ^
128 (case cas of NONE => term2xml i (pbl2term thy id)
129 | SOME t => term2xml i t) ^ "\n" ^
130 indt i ^ "</HEADLINE>\n" ^
131 (*--------------- hline --------------------------------------*)
132 pattern2xml i ppc where_ ^
133 (*--------------- hline --------------------------------------*)
134 indt i ^ "<EXPLANATIONS> </EXPLANATIONS>\n"
135 (*--------------- end display --------------------------------*)
137 indt i ^ "<THEORY>\n" ^
138 theref2xml (i+i) thy' "Theorems" "" ^
139 indt i ^ "</THEORY>\n" ^
140 (case met of [] => (indt i) ^ "<METHODS> </METHODS>\n"
141 | _ => (indt i) ^ "<METHODS>\n" ^
142 foldl op^ ("", map (keref2xml (i+i) Met_) met) ^
143 (indt i) ^ "</METHODS>\n") ^
144 indt i ^ "<EVALPRECOND>\n" ^
145 theref2xml (i+i) (snd (Rtools.thy_containing_rls thy' prls')) "Rulesets" prls'^
146 indt i ^ "</EVALPRECOND>\n" ^
147 authors2xml i "MATHAUTHORS" mathauthors ^
148 authors2xml i "COURSEDESIGNS" ["isac team 2006"] ^
149 "</NODECONTENT>" : xml
151 (* old version with 'dead' strings for rls, calc, ....* *)
152 fun pbl2xml (id:(*pblRD*)pblID) ({guh,mathauthors,init,cas,met,ppc,prls,
155 indt i ^ "<GUH> " ^ guh ^ " </GUH>\n" ^
156 (((id2xml i)(* o rev*)) id) ^
157 indt i ^ "<META> </META>\n" ^
158 (*--------------- begin display ------------------------------*)
159 indt i ^ "<HEADLINE>\n" ^
160 (case cas of NONE => term2xml i (pbl2term thy id)
161 | SOME t => term2xml i t) ^ "\n" ^
162 indt i ^ "</HEADLINE>\n" ^
163 (*--------------- hline --------------------------------------*)
164 pattern2xml i ppc where_ ^
165 (*--------------- hline --------------------------------------*)
166 indt i ^ "<EXPLANATIONS> </EXPLANATIONS>\n"
167 (*--------------- end display --------------------------------*)
169 indt i ^ "<THEORY>\n" ^
170 theref2xml (i+i) (theory2theory' thy) "Theorems" "" ^
171 indt i ^ "</THEORY>\n" ^
172 (case met of [] => (indt i) ^ "<METHODS> </METHODS>\n"
173 | _ => (indt i) ^ "<METHODS>\n" ^
174 foldl op^ ("", map (keref2xml (i+i) Met_) met) ^
175 (indt i) ^ "</METHODS>\n") ^
176 indt i ^ "<EVALPRECOND> " ^ (#id o rep_rls)
177 prls ^ " </EVALPRECOND>\n" ^
178 authors2xml i "MATHAUTHORS" mathauthors ^
179 authors2xml i "COURSEDESIGNS" ["isac team 2006"] ^
180 "</NODECONTENT>" : xml;
183 (**. write pbls from hierarchy to files.**)
184 fun pbl2file (path:path) (pos: Ctree.pos) (id:metID) (pbl as {guh,...}) =
185 (writeln ("### pbl2file: id = " ^ strs2str id ^ ", pos = " ^ Ctree.pos2str pos);
186 ((str2file (path ^ Rtools.guh2filename guh)) o (pbl2xml id)) pbl
189 (**. write mets from hierarchy to files.**)
190 (*.format a method in xml for presentation on the method browser;
191 new version with <KESTOREREF>s -- not used because linking
192 requires elements (rls, calc, ...) to be reorganized.*)
193 (*######## ATTENTION: THIS IS not THE ACTUAL VERSION ################*)
194 fun met2xml (id:metID) ({guh,mathauthors,init,ppc,pre,scr,calc,
195 crls,erls,errpats,nrls,prls,srls,rew_ord'}:met) =
196 let val thy' = "Isac" (*FIXME.WN0607 get thy from met ?!?*)
197 val crls' = (#id o rep_rls) crls
198 val erls' = (#id o rep_rls) erls
199 val nrls' = (#id o rep_rls) nrls
200 val prls' = (#id o rep_rls) prls
201 val srls' = (#id o rep_rls) srls
202 in "<NODECONTENT>\n" ^
203 indt i ^ "<GUH> " ^ guh ^ " </GUH>\n" ^
205 indt i ^ "<META> </META>\n" ^
207 pattern2xml i ppc pre ^
208 indt i ^ "<EXPLANATIONS> </EXPLANATIONS>\n" ^
209 indt i ^ "<EVALPRECOND>\n" ^
210 theref2xml (i+i) (snd (Rtools.thy_containing_rls thy' prls')) "Rulesets" prls'^
211 indt i ^ "</EVALPRECOND>\n" ^
212 indt i ^ "<EVALCOND>\n" ^
213 theref2xml (i+i) (snd (Rtools.thy_containing_rls thy' erls')) "Rulesets" erls'^
214 indt i ^ "</EVALCOND>\n" ^
215 indt i ^ "<EVALLISTEXPR>\n"^
216 theref2xml (i+i) (snd (Rtools.thy_containing_rls thy' srls')) "Rulesets" srls'^
217 indt i ^ "</EVALLISTEXPR>\n" ^
218 indt i ^ "<CHECKELEMENTWISE>\n" ^
219 theref2xml (i+i) (snd (Rtools.thy_containing_rls thy' crls')) "Rulesets" crls'^
220 indt i ^ "</CHECKELEMENTWISE>\n" ^
221 indt i ^ "<NORMALFORM>\n" ^
222 theref2xml (i+i) (snd (Rtools.thy_containing_rls thy' nrls')) "Rulesets" nrls'^
223 indt i ^ "</NORMALFORM>\n" ^
224 indt i ^ "<REWORDER> " ^ rew_ord' ^ " </REWORDER>\n" ^
225 calcs2xmlOLD i calc ^
226 authors2xml i "MATHAUTHORS" mathauthors ^
227 authors2xml i "COURSEDESIGNS" ["isac team 2006"] ^
228 "</NODECONTENT>" : xml
230 (*.format a method in xml for presentation on the method browser;
231 old version with 'dead' strings for rls, calc, ....*)
232 fun met2xml (id:metID) ({guh,mathauthors,init,ppc,pre,scr,calc,
233 crls,erls,errpats,nrls,prls,srls,rew_ord'}:met) =
235 indt i ^ "<GUH> " ^ guh ^ " </GUH>\n" ^
237 indt i ^ "<META> </META>\n" ^
239 pattern2xml i ppc pre ^
240 indt i ^ "<EXPLANATIONS> </EXPLANATIONS>\n" ^
241 indt i ^ "<EVALPRECOND> " ^ (#id o rep_rls) prls ^ " </EVALPRECOND>\n" ^
242 indt i ^ "<EVALCOND> " ^ (#id o rep_rls) erls ^ " </EVALCOND>\n" ^
243 indt i ^ "<EVALLISTEXPR> "^ (#id o rep_rls) srls ^ " </EVALLISTEXPR>\n" ^
244 indt i ^ "<CHECKELEMENTWISE> " ^ (#id o rep_rls)
245 crls ^ " </CHECKELEMENTWISE>\n" ^
246 indt i ^ "<NORMALFORM> " ^ (#id o rep_rls) nrls ^ " </NORMALFORM>\n" ^
247 indt i ^ "<REWORDER> " ^ rew_ord' ^ " </REWORDER>\n" ^
248 calcs2xmlOLD i calc ^
249 authors2xml i "MATHAUTHORS" mathauthors ^
250 authors2xml i "COURSEDESIGNS" ["isac team 2006"] ^
251 "</NODECONTENT>" : xml;
252 (* writeln (met2xml ["Test", "solve_linear"]
253 (get_met ["Test", "solve_linear"]));
256 (*.write the files using an int-key (pos') as filename.*)
257 fun met2file (path:path) (pos: Ctree.pos) (id:metID) met =
258 (writeln ("### met2file: id = " ^ strs2str id);
259 ((str2file (path ^ "met" ^ pos2filename pos)) o (met2xml id)) met);
261 (*.write the files using the guh as filename.*)
262 fun met2file (path:path) (pos: Ctree.pos) (id:metID) (met as {guh,...}) =
263 (writeln ("### met2file: id = " ^ strs2str id);
264 ((str2file (path ^ Rtools.guh2filename guh)) o (met2xml id)) met);
266 (*.scan the mtree Ptyp and print the nodes using wfn.*)
267 fun node (pa:path) ids po wfn (Ptyp (id,[n],ns)) =
268 let val po' = Ctree.lev_on po
270 wfn pa po' (ids@[id]) n;
271 nodes pa (ids@[id]) (Ctree.lev_dn po') wfn ns
273 and nodes _ _ _ _ [] = ()
274 | nodes pa ids po wfn (n::ns) =
275 (node pa ids po wfn n; nodes pa ids (Ctree.lev_on po) wfn ns);
277 fun pbls2file (p:path) = nodes p [] [0] pbl2file (get_ptyps ());
278 fun mets2file (p:path) = nodes p [] [0] met2file (get_mets ());
280 val path = "/home/neuper/proto2/isac/xmldata/";
281 val path = "/home/neuper/tmp/";
283 pbl_hierarchy2file (path ^ "pbl/");
284 pbls2file (path ^ "pbl/");
286 met_hierarchy2file (path ^ "met/");
287 mets2file (path ^ "met/");
289 thy_hierarchy2file (path ^ "thy/");
290 thes2file (path ^ "thy/");
294 ({guh, mathauthors, init, rew_ord', erls, srls, prls, crls, nrls, calc, ppc, pre, scr, ...}: met)
296 {guh = guh, mathauthors = mathauthors, init = init, rew_ord' = rew_ord', erls = erls,
297 srls = srls, prls = prls, crls = crls, nrls = nrls, calc = calc,
298 ppc = ppc, pre = pre, scr = scr, errpats = errpats'}: met
300 (* interface for dialog-authoring: call in Buld_Thydata.thy only ! *)
301 fun update_metpair thy metID errpats = let
302 val ret = (update_metdata (Specify.get_met' thy metID) errpats, metID)
303 handle ERROR _ => error ("update_metpair: " ^ (strs2str metID) ^ " must address a method");