1 (* export problem-data and method-data to xml |
1 (* ~/src/Tools/isac/BridgeLibisabelle/pbl-met-hierarchy.sml |
2 author: Walther Neuper 2004 |
2 author: Walther Neuper 2004 |
3 (c) isac-team |
3 (c) isac-team |
|
4 |
|
5 Create XML for the tree structure of problem-patterns and methods. |
|
6 This is kept as a model for some browsing facility, which is required |
|
7 in parallel to PIDE, because these structures are different |
|
8 from the dependency graph of Isabelle's theories. |
4 *) |
9 *) |
5 signature PROBLEM_METHOD_HIERARCHY = |
10 signature PROBLEM_METHOD_HIERARCHY = |
6 sig |
11 sig |
7 val format_pblIDl : string list list -> string |
12 val format_pblIDl : string list list -> string |
8 eqtype filepath |
13 eqtype filepath |
9 val file2str: filepath -> Thy_Present.filename -> string |
14 val file2str: filepath -> Thy_Present.filename -> string |
10 val hierarchy: string -> 'a Store.node list -> string |
|
11 val hierarchy_met: MethodC.T Store.node list -> xml |
15 val hierarchy_met: MethodC.T Store.node list -> xml |
12 val hierarchy_pbl: Problem.T Store.node list -> xml |
16 val hierarchy_pbl: Problem.T Store.node list -> xml |
13 val i: int |
17 val i: int |
14 val id2filename: string list -> string |
18 |
15 val met2file: filepath -> Pos.pos -> MethodC.id -> MethodC.T -> unit |
19 val pbl_hierarchy2file: filepath -> unit |
16 val met2xml: MethodC.id -> MethodC.T -> xml |
|
17 val met_hierarchy2file: filepath -> unit |
20 val met_hierarchy2file: filepath -> unit |
18 val mets2file: filepath -> unit |
21 |
19 val node: filepath -> string list -> Pos.pos -> (filepath -> Pos.pos -> string list -> 'a -> 'b) -> 'a Store.node -> unit |
|
20 val nodes: filepath -> string list -> Pos.pos -> (filepath -> Pos.pos -> string list -> 'a -> 'b) -> 'a Store.node list -> unit |
|
21 val pbl2file: filepath -> Pos.pos -> MethodC.id -> Problem.T -> unit |
|
22 val pbl2term: theory -> Problem.id -> term |
|
23 val pbl2xml: Problem.id -> Problem.T -> xml |
|
24 val pbl_hierarchy2file: filepath -> unit |
|
25 val pbls2file: filepath -> unit |
|
26 val pos2filename: int list -> string |
|
27 val str2file: Thy_Present.filename -> string -> unit |
22 val str2file: Thy_Present.filename -> string -> unit |
28 val update_metdata: MethodC.T -> Error_Pattern_Def.T list -> MethodC.T |
23 val update_metdata: MethodC.T -> Error_Pattern_Def.T list -> MethodC.T |
29 val update_metpair: theory -> MethodC.id -> Error_Pattern_Def.T list -> MethodC.T * MethodC.id |
24 val update_metpair: theory -> MethodC.id -> Error_Pattern_Def.T list -> MethodC.T * MethodC.id |
30 end |
25 end |
31 |
26 |
148 (* term2str (pbl2term (Thy_Info_get_theory "Isac_Knowledge") ["equations", "univariate", "normalise"]); |
115 (* term2str (pbl2term (Thy_Info_get_theory "Isac_Knowledge") ["equations", "univariate", "normalise"]); |
149 val it = "Problem (Isac, [normalise, univariate, equations])" : string |
116 val it = "Problem (Isac, [normalise, univariate, equations])" : string |
150 *) |
117 *) |
151 val i = indentation; |
118 val i = indentation; |
152 |
119 |
153 (* new version with <KESTOREREF>s -- not used *) |
|
154 fun pbl2xml (id:(*pblRD*)Problem.id) ({guh,mathauthors,init,cas,met,ppc,prls, |
|
155 thy,where_}:Problem.T) = |
|
156 let val thy' = Context.theory_name thy |
|
157 val prls' = (#id o Rule_Set.rep) prls |
|
158 in "<NODECONTENT>\n" ^ |
|
159 indt i ^ "<GUH> " ^ guh ^ " </GUH>\n" ^ |
|
160 (((id2xml i)(* o rev*)) id) ^ |
|
161 indt i ^ "<META> </META>\n" ^ |
|
162 (*--------------- begin display ------------------------------*) |
|
163 indt i ^ "<HEADLINE>\n" ^ |
|
164 (case cas of NONE => term2xml i (pbl2term thy id) |
|
165 | SOME t => term2xml i t) ^ "\n" ^ |
|
166 indt i ^ "</HEADLINE>\n" ^ |
|
167 (*--------------- hline --------------------------------------*) |
|
168 pattern2xml i ppc where_ ^ |
|
169 (*--------------- hline --------------------------------------*) |
|
170 indt i ^ "<EXPLANATIONS> </EXPLANATIONS>\n" |
|
171 (*--------------- end display --------------------------------*) |
|
172 ^ |
|
173 indt i ^ "<THEORY>\n" ^ |
|
174 theref2xml (i+i) thy' "Theorems" "" ^ |
|
175 indt i ^ "</THEORY>\n" ^ |
|
176 (case met of [] => (indt i) ^ "<METHODS> </METHODS>\n" |
|
177 | _ => (indt i) ^ "<METHODS>\n" ^ |
|
178 foldl op ^ ("", map (keref2xml (i+i) Ptool.Met_) met) ^ |
|
179 (indt i) ^ "</METHODS>\n") ^ |
|
180 indt i ^ "<EVALPRECOND>\n" ^ |
|
181 theref2xml (i+i) (snd (Thy_Read.thy_containing_rls thy' prls')) "Rulesets" prls'^ |
|
182 indt i ^ "</EVALPRECOND>\n" ^ |
|
183 authors2xml i "MATHAUTHORS" mathauthors ^ |
|
184 authors2xml i "COURSEDESIGNS" ["isac team 2006"] ^ |
|
185 "</NODECONTENT>" : xml |
|
186 end; |
|
187 (* old version with 'dead' strings for rls, calc, ....* *) |
|
188 fun pbl2xml (id:(*pblRD*)Problem.id) ({guh,mathauthors,init,cas,met,ppc,prls, |
|
189 thy,where_}:Problem.T) = |
|
190 "<NODECONTENT>\n" ^ |
|
191 indt i ^ "<GUH> " ^ guh ^ " </GUH>\n" ^ |
|
192 (((id2xml i)(* o rev*)) id) ^ |
|
193 indt i ^ "<META> </META>\n" ^ |
|
194 (*--------------- begin display ------------------------------*) |
|
195 indt i ^ "<HEADLINE>\n" ^ |
|
196 (case cas of NONE => term2xml i (pbl2term thy id) |
|
197 | SOME t => term2xml i t) ^ "\n" ^ |
|
198 indt i ^ "</HEADLINE>\n" ^ |
|
199 (*--------------- hline --------------------------------------*) |
|
200 pattern2xml i ppc where_ ^ |
|
201 (*--------------- hline --------------------------------------*) |
|
202 indt i ^ "<EXPLANATIONS> </EXPLANATIONS>\n" |
|
203 (*--------------- end display --------------------------------*) |
|
204 ^ |
|
205 indt i ^ "<THEORY>\n" ^ |
|
206 theref2xml (i+i) (Context.theory_name thy) "Theorems" "" ^ |
|
207 indt i ^ "</THEORY>\n" ^ |
|
208 (case met of [] => (indt i) ^ "<METHODS> </METHODS>\n" |
|
209 | _ => (indt i) ^ "<METHODS>\n" ^ |
|
210 foldl op^ ("", map (keref2xml (i+i) Ptool.Met_) met) ^ |
|
211 (indt i) ^ "</METHODS>\n") ^ |
|
212 indt i ^ "<EVALPRECOND> " ^ (#id o Rule_Set.rep) |
|
213 prls ^ " </EVALPRECOND>\n" ^ |
|
214 authors2xml i "MATHAUTHORS" mathauthors ^ |
|
215 authors2xml i "COURSEDESIGNS" ["isac team 2006"] ^ |
|
216 "</NODECONTENT>" : xml; |
|
217 |
|
218 |
|
219 (**. write pbls from hierarchy to files.**) |
|
220 fun pbl2file path (pos: Pos.pos) (id: MethodC.id) (pbl as {guh, ...}) = |
|
221 (writeln ("### pbl2file: id = " ^ strs2str id ^ ", pos = " ^ Pos.pos2str pos); |
|
222 ((str2file (path ^ Thy_Present.guh2filename guh)) o (pbl2xml id)) pbl |
|
223 ); |
|
224 |
|
225 (**. write mets from hierarchy to files.**) |
|
226 (*.format a method in xml for presentation on the method browser; |
|
227 new version with <KESTOREREF>s -- not used because linking |
|
228 requires elements (rls, calc, ...) to be reorganized.*) |
|
229 (*######## ATTENTION: THIS IS not THE ACTUAL VERSION ################*) |
|
230 fun met2xml (id: MethodC.id) ({guh,mathauthors,init,ppc,pre,scr,calc, |
|
231 crls,erls,errpats,nrls,prls,srls,rew_ord'}: MethodC.T) = |
|
232 let val thy' = "Isac_Knowledge" (*FIXME.WN0607 get thy from met ?!?*) |
|
233 val crls' = (#id o Rule_Set.rep) crls |
|
234 val erls' = (#id o Rule_Set.rep) erls |
|
235 val nrls' = (#id o Rule_Set.rep) nrls |
|
236 val prls' = (#id o Rule_Set.rep) prls |
|
237 val srls' = (#id o Rule_Set.rep) srls |
|
238 in "<NODECONTENT>\n" ^ |
|
239 indt i ^ "<GUH> " ^ guh ^ " </GUH>\n" ^ |
|
240 id2xml i id ^ |
|
241 indt i ^ "<META> </META>\n" ^ |
|
242 scr2xml i scr ^ |
|
243 pattern2xml i ppc pre ^ |
|
244 indt i ^ "<EXPLANATIONS> </EXPLANATIONS>\n" ^ |
|
245 indt i ^ "<EVALPRECOND>\n" ^ |
|
246 theref2xml (i+i) (snd (Thy_Read.thy_containing_rls thy' prls')) "Rulesets" prls'^ |
|
247 indt i ^ "</EVALPRECOND>\n" ^ |
|
248 indt i ^ "<EVALCOND>\n" ^ |
|
249 theref2xml (i+i) (snd (Thy_Read.thy_containing_rls thy' erls')) "Rulesets" erls'^ |
|
250 indt i ^ "</EVALCOND>\n" ^ |
|
251 indt i ^ "<EVALLISTEXPR>\n"^ |
|
252 theref2xml (i+i) (snd (Thy_Read.thy_containing_rls thy' srls')) "Rulesets" srls'^ |
|
253 indt i ^ "</EVALLISTEXPR>\n" ^ |
|
254 indt i ^ "<CHECKELEMENTWISE>\n" ^ |
|
255 theref2xml (i+i) (snd (Thy_Read.thy_containing_rls thy' crls')) "Rulesets" crls'^ |
|
256 indt i ^ "</CHECKELEMENTWISE>\n" ^ |
|
257 indt i ^ "<NORMALFORM>\n" ^ |
|
258 theref2xml (i+i) (snd (Thy_Read.thy_containing_rls thy' nrls')) "Rulesets" nrls'^ |
|
259 indt i ^ "</NORMALFORM>\n" ^ |
|
260 indt i ^ "<REWORDER> " ^ rew_ord' ^ " </REWORDER>\n" ^ |
|
261 calcs2xmlOLD i calc ^ |
|
262 authors2xml i "MATHAUTHORS" mathauthors ^ |
|
263 authors2xml i "COURSEDESIGNS" ["isac team 2006"] ^ |
|
264 "</NODECONTENT>" : xml |
|
265 end; |
|
266 (*.format a method in xml for presentation on the method browser; |
|
267 old version with 'dead' strings for rls, calc, ....*) |
|
268 fun met2xml (id: MethodC.id) ({guh,mathauthors,init,ppc,pre,scr,calc, |
|
269 crls,erls,errpats,nrls,prls,srls,rew_ord'}: MethodC.T) = |
|
270 "<NODECONTENT>\n" ^ |
|
271 indt i ^ "<GUH> " ^ guh ^ " </GUH>\n" ^ |
|
272 id2xml i id ^ |
|
273 indt i ^ "<META> </META>\n" ^ |
|
274 scr2xml i scr ^ |
|
275 pattern2xml i ppc pre ^ |
|
276 indt i ^ "<EXPLANATIONS> </EXPLANATIONS>\n" ^ |
|
277 indt i ^ "<EVALPRECOND> " ^ (#id o Rule_Set.rep) prls ^ " </EVALPRECOND>\n" ^ |
|
278 indt i ^ "<EVALCOND> " ^ (#id o Rule_Set.rep) erls ^ " </EVALCOND>\n" ^ |
|
279 indt i ^ "<EVALLISTEXPR> "^ (#id o Rule_Set.rep) srls ^ " </EVALLISTEXPR>\n" ^ |
|
280 indt i ^ "<CHECKELEMENTWISE> " ^ (#id o Rule_Set.rep) |
|
281 crls ^ " </CHECKELEMENTWISE>\n" ^ |
|
282 indt i ^ "<NORMALFORM> " ^ (#id o Rule_Set.rep) nrls ^ " </NORMALFORM>\n" ^ |
|
283 indt i ^ "<REWORDER> " ^ rew_ord' ^ " </REWORDER>\n" ^ |
|
284 calcs2xmlOLD i calc ^ |
|
285 authors2xml i "MATHAUTHORS" mathauthors ^ |
|
286 authors2xml i "COURSEDESIGNS" ["isac team 2006"] ^ |
|
287 "</NODECONTENT>" : xml; |
|
288 (* writeln (met2xml ["Test", "solve_linear"] |
|
289 (get_met ["Test", "solve_linear"])); |
|
290 *) |
|
291 |
|
292 (*.write the files using an int-key (pos') as filename.*) |
|
293 fun met2file path (pos: Pos.pos) (id: MethodC.id) met = |
|
294 (writeln ("### met2file: id = " ^ strs2str id); |
|
295 ((str2file (path ^ "met" ^ pos2filename pos)) o (met2xml id)) met); |
|
296 |
|
297 (*.write the files using the guh as filename.*) |
|
298 fun met2file path (pos: Pos.pos) (id: MethodC.id) (met as {guh,...}) = |
|
299 (writeln ("### met2file: id = " ^ strs2str id); |
|
300 ((str2file (path ^ Thy_Present.guh2filename guh)) o (met2xml id)) met); |
|
301 |
|
302 (*.scan the mtree Ptyp and print the nodes using wfn.*) |
|
303 fun node pa ids po wfn (Store.Node (id, [n], ns)) = |
|
304 let val po' = Pos.lev_on po |
|
305 in |
|
306 wfn pa po' (ids@[id]) n; |
|
307 nodes pa (ids@[id]) (Pos.lev_dn po') wfn ns |
|
308 end |
|
309 and nodes _ _ _ _ [] = () |
|
310 | nodes pa ids po wfn (n::ns) = |
|
311 (node pa ids po wfn n; nodes pa ids (Pos.lev_on po) wfn ns); |
|
312 |
|
313 fun pbls2file path = nodes path [] [0] pbl2file (get_ptyps ()); |
|
314 fun mets2file path = nodes path [] [0] met2file (get_mets ()); |
|
315 (* |
|
316 ~@wneuper-w541:~/tmp$ mkdir pbl |
|
317 ~@wneuper-w541:~/tmp$ mkdir met |
|
318 ~@wneuper-w541:~/tmp$ mkdir thy |
|
319 |
|
320 val path = "/home/wneuper/proto2/isac/xmldata/"; |
|
321 val path = "/home/wneuper/tmp/"; |
|
322 |
|
323 pbl_hierarchy2file (path ^ "pbl/"); |
|
324 pbls2file (path ^ "pbl/"); |
|
325 |
|
326 met_hierarchy2file (path ^ "met/"); |
|
327 mets2file (path ^ "met/"); |
|
328 |
|
329 thy_hierarchy2file (path ^ "thy/"); |
|
330 thes2file (path ^ "thy/"); |
|
331 *) |
|
332 |
|
333 fun update_metdata |
120 fun update_metdata |
334 ({guh, mathauthors, init, rew_ord', erls, srls, prls, crls, nrls, calc, ppc, pre, scr, ...}: MethodC.T) |
121 ({guh, mathauthors, init, rew_ord', erls, srls, prls, crls, nrls, calc, ppc, pre, scr, ...}: MethodC.T) |
335 errpats' = |
122 errpats' = |
336 {guh = guh, mathauthors = mathauthors, init = init, rew_ord' = rew_ord', erls = erls, |
123 {guh = guh, mathauthors = mathauthors, init = init, rew_ord' = rew_ord', erls = erls, |
337 srls = srls, prls = prls, crls = crls, nrls = nrls, calc = calc, |
124 srls = srls, prls = prls, crls = crls, nrls = nrls, calc = calc, |