|
1 (*.export theory-data to xml |
|
2 author: Walther Neuper 0601 |
|
3 (c) isac-team |
|
4 |
|
5 FIXME.WN0602: re-engineer this file for analogy to pbl-met-hierarchy |
|
6 as follows: |
|
7 # 'fun collect_thydata': unit -> string list * thydata list |
|
8 ^^^^^^^^^^^ hierarchy-key |
|
9 # 'fun thys2file': from this ^^^ datastructure (^^^^^^^^^^^ for free!) |
|
10 # map 'fun store_pbt' (NEW!) over ^^^ into 'thy_data ptyp' |
|
11 # from 'thy_data ptyp' create 'thy_hierarchy' |
|
12 |
|
13 use"xmlsrc/thy-hierarchy.sml"; |
|
14 use"thy-hierarchy.sml"; |
|
15 .*) |
|
16 |
|
17 |
|
18 (**.collect data and build intermediate structure for hierarchy: |
|
19 theorems, rulesets and Calc's, (TODO rew_ord's etc) defined in isac |
|
20 and Isabelle-thms used in rulesets; |
|
21 this code binds ref-var's and must be after IsacKnowledge .**) |
|
22 |
|
23 (*.collect all theorems defined in in a theory and insert the guh.*) |
|
24 fun makeHthm (part:string, thyID:thyID) (thmID:thmID, thm:thm) = |
|
25 let val theID = [part, thyID, "Theorems"] @ [strip_thy thmID] : theID |
|
26 in (theID, Hthm {guh = theID2guh theID, coursedesign = [], |
|
27 mathauthors = ["isac-team"], thm = thm}) |
|
28 end; |
|
29 fun makeHrls (part:string) (rls':rls', thy_rls as (thyID, rls): thyID * rls) = |
|
30 let val theID = [part, thyID,"Rulesets"] @ [rls'] : theID |
|
31 in (theID, Hrls {guh = theID2guh theID, coursedesign=[], |
|
32 mathauthors=["isac-team"], thy_rls = thy_rls}) |
|
33 end; |
|
34 fun makeHcal (part:string, thyID:thyID) (calID, cal) = |
|
35 let val theID = [part, thyID,"Operations"] @ [calID] : theID |
|
36 in (theID, Hcal {guh = theID2guh theID, coursedesign=[], |
|
37 mathauthors=["isac-team"], calc = cal}) |
|
38 end; |
|
39 fun makeHord (part:string, thyID:thyID) (ordID, ord) = |
|
40 let val theID = [part, thyID,"TODO-Orders"] @ [ordID] : theID |
|
41 in (theID, Hord {guh = theID2guh theID, coursedesign=[], |
|
42 mathauthors=["isac-team"], ord = ord}) |
|
43 end; |
|
44 |
|
45 |
|
46 fun collect_thms' (part, thy') = |
|
47 let val thy = assoc_thy (thyID2theory' thy') |
|
48 in map (makeHthm (part, thy')) (thms_of thy) end; |
|
49 |
|
50 (*.collect all rulesets defined in in a theory and insert the guh.*) |
|
51 fun collect_rlss (part, thy') = |
|
52 let val rlss = filter ((curry op= thy') o |
|
53 ((#1 o #2):(rls' * (theory' * rls)) -> theory')) |
|
54 (!ruleset') |
|
55 in map (makeHrls part) rlss end; |
|
56 |
|
57 (*.collect all calcs defined in in a theory.*) |
|
58 fun collect_cals (part, thy') = |
|
59 let val cals = [] (*FIXXXXXXXXXXME.WN060713 add thyID: (thyID, cal)*) |
|
60 in map (makeHcal (part, thy')) cals end; |
|
61 |
|
62 |
|
63 (*.collect all rew_ord's defined in in a theory.*) |
|
64 fun collect_ords (part, thy') = |
|
65 let val thy = assoc_thy (thyID2theory' thy') |
|
66 in [(*TODO.WN060120 rew_ord, Calc*)]:(theID * thydata) list end; |
|
67 |
|
68 (*.collect all data for a thy TODO.WN060120 rew_ord, Calc.*) |
|
69 (* val thy' = nth 1 scri_thys; |
|
70 *) |
|
71 fun collect_thy part(*IsacScripts|IsacKnowledge*) (thy': theory') = |
|
72 ((collect_thms' (part, thy')) @ (collect_rlss (part, thy')) @ |
|
73 (collect_cals (part, thy')) @ (collect_ords (part, thy'))) |
|
74 : (theID * thydata) list; |
|
75 |
|
76 (*.collect theorems defined in Isabelle (before Isac is evaluated above).*) |
|
77 fun collect_isab isa (thyID, (thmID, thm)) = |
|
78 let val theID = [isa, thyID, "Theorems", thmID] |
|
79 in (theID:theID, Hthm {guh = theID2guh theID, |
|
80 mathauthors = ["Isabelle team, TU Munich"], |
|
81 coursedesign = [], |
|
82 thm = thm}) end; |
|
83 |
|
84 val isabelle_page = (["Isabelle"] : theID, |
|
85 Html {guh = theID2guh ["Isabelle"], |
|
86 html = "", |
|
87 mathauthors = ["Isabelle team, TU Munich"], |
|
88 coursedesign = []}); |
|
89 |
|
90 (*.create a list with all thydata=thyelements=the; |
|
91 this list is used by 'fun the_hier' to create the hierarchy .*) |
|
92 fun collect_thydata () = |
|
93 let val isab_thms = map rearrange_inv (!isab_thm_thy) |
|
94 val scri_thys = (map (get_thy o #1) (!script_thys)) |
|
95 \\ ["e_domID"] |
|
96 val isac_thys = (map (get_thy o #1) |
|
97 (!theory')) \\ scri_thys \\ ["e_domID"] |
|
98 in [isabelle_page] @ |
|
99 (map (collect_isab "Isabelle") isab_thms) @ |
|
100 ((flat o (map (collect_thy "IsacScripts"))) scri_thys) @ |
|
101 ((flat o (map (collect_thy "IsacKnowledge"))) isac_thys) |
|
102 : (theID * thydata) list |
|
103 end; |
|
104 |
|
105 fun show_thes () = (writeln o format_pblIDl o (scan [])) (!thehier); |
|
106 |
|
107 |
|
108 |
|
109 (***.create the xml-format for the hierarchy.***) |
|
110 |
|
111 (**.make a hierarchy from (theID * thydata) list created by 'fun collect_thy'; |
|
112 use the same mechanism as for pbl_hierarchy and met_hierarchy; |
|
113 but check, if a thydata is already there (for auto-gen. Isabelle).**) |
|
114 |
|
115 (*.for preserving elements created by 'fun store_thy'.*) |
|
116 fun exist_the (theID:theID) (thy_hie:thehier) = |
|
117 let fun node theID ids (Ptyp (id,_,ns)) = |
|
118 if theID = ids @ [id] then true |
|
119 else nodes theID (ids @ [id]) ns |
|
120 and nodes _ _ [] = false |
|
121 | nodes theID ids (n::ns) = if node theID ids n then true |
|
122 else nodes theID ids ns |
|
123 in nodes theID [] thy_hie end; |
|
124 |
|
125 (*.insrt requires a parent; see 'fun fill_parents'.*) |
|
126 fun can_insert (theID:theID) (thy_hie:thehier) = |
|
127 (insrt theID e_thydata theID thy_hie; true) |
|
128 handle _ => false; |
|
129 |
|
130 (*.cut 'theID', the ID of theory elements from tail to head |
|
131 until insertion into the hierarchy of theory elements 'th' is possible |
|
132 (the hierarchy requires the parentnode to exist for insertion).*) |
|
133 fun cut_theID th ([]:theID) = |
|
134 raise error "could not insert into thy-hierarchy" |
|
135 | cut_theID th theID = |
|
136 if can_insert theID th |
|
137 then theID else cut_theID th (drop_last theID); |
|
138 |
|
139 (*.insert empty parents 'Html' into the hierarchy of theory elements 'th' |
|
140 until the actual node can be inserted with key 'theID'.*) |
|
141 (* val (th, cutID, theID) = (th, theID, theID); |
|
142 val (th, cutID, theID) = (th', cutID_, theID); |
|
143 *) |
|
144 fun fill_parents th cutID theID = |
|
145 let val cutID' = cut_theID th cutID |
|
146 in if cutID' = theID |
|
147 then th |
|
148 else let val th' = insrt cutID' (Html {guh=theID2guh theID, |
|
149 coursedesign=["isac team 2006"], |
|
150 mathauthors=[], |
|
151 html=""}) cutID' th |
|
152 val cutID_ = cutID' @ [nth ((length cutID') + 1) theID] |
|
153 in fill_parents th' cutID_ theID end |
|
154 end; |
|
155 |
|
156 (*.create the hierarchy from a list (generated automatically); |
|
157 thus, missing parents of list-elems are inserted |
|
158 (causing msgs '*** insert: not found'); |
|
159 elemes already store_*d in some *.ML are NOT overwritten.*) |
|
160 fun the_hier th ([]: (theID * thydata) list) = th |
|
161 (* val (th, (theID, thydata)::ths) = (!thehier, collect_thydata ()); |
|
162 *) |
|
163 | the_hier th ((theID, thydata)::ths) = |
|
164 if can_insert theID th |
|
165 then let val th' = if exist_the theID th |
|
166 then (writeln ("*** insert: preserved "^strs2str theID); |
|
167 th) |
|
168 else insrt theID thydata theID th |
|
169 in the_hier th' ths end |
|
170 else let val th' = fill_parents th theID theID (*..*** insert: not found*) |
|
171 val th' = insrt theID thydata theID th' |
|
172 in the_hier th' ths end; |
|
173 |
|
174 |
|
175 (*these files shall contain 'invisible' html |
|
176 val thydatafilename = "thy_datafile.xml"; (*for "Theorems"|...*) |
|
177 fun partfilename str = "thy_" ^ str ^ ".xml"; (*for "Isabelle"|...*)*) |
|
178 |
|
179 (*.create an xml-hierarchy where the filname is created from the guh.*) |
|
180 (*ad DTD: a NODE contains an ID and zero or more NODEs*) |
|
181 fun hierarchy_guh h = |
|
182 let val i = indentation |
|
183 val j = indentation |
|
184 fun node i p theID (Ptyp (id,_,ns)) = |
|
185 let val p' = lev_on p |
|
186 val theID' = theID @ [id] |
|
187 in (indt i) ^ "<NODE>\n" ^ |
|
188 (indt (i+j)) ^ "<ID> " ^ id ^ " </ID>\n" ^ |
|
189 (indt (i+j)) ^ "<NO> " (*on this level*) ^ |
|
190 (string_of_int o last_elem) p' ^ " </NO>\n" ^ |
|
191 (indt (i+j)) ^ "<CONTENTREF> " ^ theID2guh theID' ^ |
|
192 " </CONTENTREF>\n" ^ |
|
193 (nodes (i+j) (lev_dn p') theID' ns) ^ |
|
194 (indt i) ^ "</NODE>\n" |
|
195 end |
|
196 and nodes _ _ _ [] = "" |
|
197 | nodes i p theID (n::ns) = (node i p theID n) |
|
198 ^ (nodes i (lev_on p) theID ns); |
|
199 in nodes j [0] [] h end; |
|
200 |
|
201 fun thy_hierarchy2file (path:path) = |
|
202 str2file (path ^ "thy_hierarchy.xml") |
|
203 ("<NODE>\n" ^ |
|
204 " <ID> theory hierarchy </ID>\n" ^ |
|
205 " <NO> 1 </NO>\n" ^ |
|
206 " <CONTENTREF> thy_ROOT </CONTENTREF>\n" ^ |
|
207 (hierarchy_guh (!thehier)) ^ |
|
208 "</NODE>"); |
|
209 |
|
210 |
|
211 (**.create the xml-files for the theory-data from the hierarchy.**) |
|
212 |
|
213 val i = indentation; |
|
214 (*.analoguous to 'fun met2xml'.*) |
|
215 fun thydata2xml (theID:theID, Html {guh, coursedesign, mathauthors, html}) = |
|
216 "<HTMLDATA>\n" ^ |
|
217 indt i ^ "<GUH> "^ guh ^" </GUH>\n" ^ |
|
218 id2xml i theID ^ |
|
219 indt i ^ "<EXPLANATIONS> " ^ html ^ "</EXPLANATIONS>\n" ^ |
|
220 authors2xml i "MATHAUTHORS" mathauthors ^ |
|
221 authors2xml i "COURSEDESIGNS" coursedesign ^ |
|
222 "</HTMLDATA>\n" : xml |
|
223 | thydata2xml (theID:theID, Hthm {guh, coursedesign, mathauthors, thm}) = |
|
224 "<THEOREMDATA>\n" ^ |
|
225 indt i ^ "<GUH> "^ guh ^" </GUH>\n" ^ |
|
226 id2xml i theID ^ |
|
227 thm''2xml i thm ^ |
|
228 indt i ^ "<PROOF>\n" ^ |
|
229 extref2xml (i+i) "Proof of the theorem" |
|
230 ("http://www.ist.tugraz.at/projects/isac/www/\ |
|
231 \kbase/thy/browser_info/HOL/HOL-Real/Isac/" ^ |
|
232 nth 2 theID ^ ".html") ^ |
|
233 indt i ^ "</PROOF>\n" ^ |
|
234 indt i ^ "<EXPLANATIONS> </EXPLANATIONS>\n" ^ |
|
235 authors2xml i "MATHAUTHORS" mathauthors ^ |
|
236 authors2xml i "COURSEDESIGNS" coursedesign ^ |
|
237 "</THEOREMDATA>\n" |
|
238 (* val (theID:theID, Hrls {guh, coursedesign, mathauthors, thy_rls}) = |
|
239 (theID, thydata); |
|
240 *) |
|
241 | thydata2xml (theID, Hrls {guh, coursedesign, mathauthors, thy_rls}) = |
|
242 "<RULESETDATA>\n" ^ |
|
243 indt i ^ "<GUH> "^ guh ^" </GUH>\n" ^ |
|
244 id2xml i theID ^ |
|
245 rls2xml i thy_rls ^ |
|
246 indt i ^ "<EXPLANATIONS> </EXPLANATIONS>\n" ^ |
|
247 authors2xml i "MATHAUTHORS" mathauthors ^ |
|
248 authors2xml i "COURSEDESIGNS" coursedesign ^ |
|
249 "</RULESETDATA>\n" |
|
250 (* val (theID:theID, Hcal {guh, coursedesign, mathauthors, calc}) = |
|
251 (theID, rlsdata); |
|
252 *) |
|
253 | thydata2xml (theID, Hcal {guh, coursedesign, mathauthors, calc}) = |
|
254 "<RULESETDATA>\n" ^ |
|
255 indt i ^ "<GUH> "^ guh ^" </GUH>\n" ^ |
|
256 id2xml i theID ^ |
|
257 calc2xml i (theID2thyID theID, calc) ^ |
|
258 indt i ^ "<EXPLANATIONS> </EXPLANATIONS>\n" ^ |
|
259 authors2xml i "MATHAUTHORS" mathauthors ^ |
|
260 authors2xml i "COURSEDESIGNS" coursedesign ^ |
|
261 "</RULESETDATA>\n" |
|
262 | thydata2xml (theID, _) = |
|
263 raise error ("thydata2xml: not implemented for "^ strs2str' theID); |
|
264 |
|
265 (*.analoguous to 'fun met2file'.*) |
|
266 fun thydata2file (xmldata:path) (pos:pos) (theID:theID) thydata = |
|
267 (writeln ("### thes2file: id = " ^ strs2str theID); |
|
268 str2file (xmldata ^ theID2filename theID) |
|
269 (thydata2xml (theID:theID, thydata))); |
|
270 |
|
271 (*.analoguous to 'fun node'; here we scan ??????????.*) |
|
272 (* val (pa, ids, po, wfn, (Ptyp (id,[n],ns))) = |
|
273 (pa, ids, po, wfn, n); |
|
274 *) |
|
275 fun thenode (pa:path) ids po wfn (Ptyp (id,[n],ns)) = |
|
276 let val po' = lev_on po |
|
277 in wfn pa po' (ids@[id]) n; |
|
278 thenodes pa (ids@[id]) ((lev_dn po'):pos) wfn ns end |
|
279 (* val (pa, ids, po, wfn, (n::ns)) = |
|
280 (path, []:string list, [0], thydata2file, (!thehier)); |
|
281 *) |
|
282 and thenodes _ _ _ _ [] = () |
|
283 | thenodes pa ids po wfn (n::ns) = (thenode pa ids po wfn n; |
|
284 thenodes pa ids (lev_on po) wfn ns); |
|
285 |
|
286 (*..analoguous to 'fun mets2file'*) |
|
287 fun thes2file (p : path) = |
|
288 thenodes p [] [0] thydata2file (!thehier); |
|
289 |
|
290 |
|
291 (***.store a single theory element in the hierarchy.***) |
|
292 |
|
293 (*.for mathauthors only, other html is added to xml exported from here.*) |
|
294 (* val (theID, mathauthors) = |
|
295 (["IsacKnowledge", theory2thyID Biegelinie.thy, "Theorems"], |
|
296 ["Walther Neuper 2005 supported by a grant from NMI Austria"]); |
|
297 *) |
|
298 fun store_isa (theID : theID) (mathauthors : authors) = |
|
299 let val guh = case theID of |
|
300 [part] => part2guh theID |
|
301 | [part, thyID, thypart] => thypart2guh theID |
|
302 val theID = guh2theID guh |
|
303 val the = Html {guh = guh, |
|
304 coursedesign = [], |
|
305 mathauthors = mathauthors, |
|
306 html = ""} |
|
307 in (*needs no (!check_guhs_unique) because guh is generated automatically*) |
|
308 thehier := insrt theID the theID (!thehier) end; |
|
309 |
|
310 fun store_thy thy (mathauthors : authors) = |
|
311 let val guh = thy2guh ["IsacKnowledge", theory2thyID thy] |
|
312 val theID = guh2theID guh |
|
313 val the = Html {guh = guh, |
|
314 coursedesign = [], |
|
315 mathauthors = mathauthors, |
|
316 html = ""} |
|
317 in (*needs no (!check_guhs_unique) because guh is generated automatically*) |
|
318 thehier := insrt theID the theID (!thehier) end; |
|
319 |
|
320 fun store_thm thy (thmID : thmID, thm) (mathauthors : authors) = |
|
321 let val guh = thm2guh ("IsacKnowledge", theory2thyID thy) thmID |
|
322 val theID = guh2theID guh |
|
323 val the = Hthm {guh = guh, |
|
324 coursedesign = [], (*done at xml exported from here*) |
|
325 mathauthors=mathauthors, |
|
326 thm = thm} |
|
327 in (*needs no (!check_guhs_unique) because guh is generated automatically*) |
|
328 thehier := insrt theID the theID (!thehier) end; |
|
329 |
|
330 fun store_rls thy rls (mathauthors : authors) = |
|
331 let val guh = rls2guh ("IsacKnowledge", theory2thyID thy) |
|
332 ((#id o rep_rls) rls) |
|
333 val theID = guh2theID guh |
|
334 val the = Hrls {guh = guh, |
|
335 coursedesign = [], |
|
336 mathauthors = mathauthors, |
|
337 thy_rls=(theory2thyID thy, rls)} |
|
338 in (*needs no (!check_guhs_unique) because guh is generated automatically*) |
|
339 thehier := insrt theID the theID (!thehier) end; |
|
340 |
|
341 fun store_cal thy cal (mathauthors : authors) = |
|
342 let val guh = cal2guh ("IsacKnowledge", theory2thyID thy) |
|
343 ("TODO store_cal") |
|
344 val theID = guh2theID guh |
|
345 val the = Hcal {guh = guh, |
|
346 coursedesign = [], |
|
347 mathauthors = mathauthors, |
|
348 calc = cal} |
|
349 in (*needs no (!check_guhs_unique) because guh is generated automatically*) |
|
350 thehier := insrt theID the theID (!thehier) end; |
|
351 |
|
352 fun store_ord thy ord (mathauthors : authors) = |
|
353 let val guh = ord2guh ("IsacKnowledge", theory2thyID thy) |
|
354 ("TODO store_ord") |
|
355 val theID = guh2theID guh |
|
356 val the = Hord {guh = guh, |
|
357 coursedesign = [], |
|
358 mathauthors = mathauthors, |
|
359 ord = ord} |
|
360 in (*needs no (!check_guhs_unique) because guh is generated automatically*) |
|
361 thehier := insrt theID the theID (!thehier) end; |