1 (*.export theory-data to xml
2 author: Walther Neuper 0601
5 FIXME.WN0602: re-engineer this file for analogy to pbl-met-hierarchy
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'
13 use"xmlsrc/thy-hierarchy.sml";
14 use"thy-hierarchy.sml";
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 .**)
23 (*.collect all theorems defined in in a theory and insert the guh.*)
24 fun makeHthm (part:string, thyID:thyID) (thmID:thmID, thm:term) =
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})
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})
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})
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})
46 fun collect_thms' (part, thy') =
47 let val thy = assoc_thy (thyID2theory' thy')
48 in map (makeHthm (part, thy')) (Theory.axioms_of thy) end;
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'))
55 in map (makeHrls part) rlss end;
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;
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;
68 (*.collect all data for a thy TODO.WN060120 rew_ord, Calc.*)
69 (* val thy' = nth 1 scri_thys;
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;
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"],
84 val isabelle_page = (["Isabelle"] : theID,
85 Html {guh = theID2guh ["Isabelle"],
87 mathauthors = ["Isabelle team, TU Munich"],
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)
95 subtract op = ["e_domID"] (map (get_thy o #1) (!script_thys))
97 subtract op = ["e_domID"]
98 (subtract op = scri_thys (map (get_thy o #1) (!theory')))
100 (map (collect_isab "Isabelle") isab_thms) @
101 ((flat o (map (collect_thy "IsacScripts"))) scri_thys) @
102 ((flat o (map (collect_thy "IsacKnowledge"))) isac_thys)
103 : (theID * thydata) list
106 fun show_thes () = (writeln o format_pblIDl o (scan [])) (!thehier);
110 (***.create the xml-format for the hierarchy.***)
112 (**.make a hierarchy from (theID * thydata) list created by 'fun collect_thy';
113 use the same mechanism as for pbl_hierarchy and met_hierarchy;
114 but check, if a thydata is already there (for auto-gen. Isabelle).**)
116 (*.for preserving elements created by 'fun store_thy'.*)
117 fun exist_the (theID:theID) (thy_hie:thehier) =
118 let fun node theID ids (Ptyp (id,_,ns)) =
119 if theID = ids @ [id] then true
120 else nodes theID (ids @ [id]) ns
121 and nodes _ _ [] = false
122 | nodes theID ids (n::ns) = if node theID ids n then true
123 else nodes theID ids ns
124 in nodes theID [] thy_hie end;
126 (*.insrt requires a parent; see 'fun fill_parents'.*)
127 fun can_insert (theID:theID) (thy_hie:thehier) =
128 (insrt theID e_thydata theID thy_hie; true)
131 (*.cut 'theID', the ID of theory elements from tail to head
132 until insertion into the hierarchy of theory elements 'th' is possible
133 (the hierarchy requires the parentnode to exist for insertion).*)
134 fun cut_theID th ([]:theID) =
135 error "could not insert into thy-hierarchy"
136 | cut_theID th theID =
137 if can_insert theID th
138 then theID else cut_theID th (drop_last theID);
140 (*.insert empty parents 'Html' into the hierarchy of theory elements 'th'
141 until the actual node can be inserted with key 'theID'.*)
142 (* val (th, cutID, theID) = (th, theID, theID);
143 val (th, cutID, theID) = (th', cutID_, theID);
145 fun fill_parents th cutID theID =
146 let val cutID' = cut_theID th cutID
149 else let val th' = insrt cutID' (Html {guh=theID2guh theID,
150 coursedesign=["isac team 2006"],
153 val cutID_ = cutID' @ [nth ((length cutID') + 1) theID]
154 in fill_parents th' cutID_ theID end
157 (*.create the hierarchy from a list (generated automatically);
158 thus, missing parents of list-elems are inserted
159 (causing msgs '*** insert: not found');
160 elemes already store_*d in some *.ML are NOT overwritten.*)
161 fun the_hier th ([]: (theID * thydata) list) = th
162 (* val (th, (theID, thydata)::ths) = (!thehier, collect_thydata ());
164 | the_hier th ((theID, thydata)::ths) =
165 if can_insert theID th
166 then let val th' = if exist_the theID th
167 then (writeln ("*** insert: preserved "^strs2str theID);
169 else insrt theID thydata theID th
170 in the_hier th' ths end
171 else let val th' = fill_parents th theID theID (*..*** insert: not found*)
172 val th' = insrt theID thydata theID th'
173 in the_hier th' ths end;
176 (*these files shall contain 'invisible' html
177 val thydatafilename = "thy_datafile.xml"; (*for "Theorems"|...*)
178 fun partfilename str = "thy_" ^ str ^ ".xml"; (*for "Isabelle"|...*)*)
180 (*.create an xml-hierarchy where the filname is created from the guh.*)
181 (*ad DTD: a NODE contains an ID and zero or more NODEs*)
182 fun hierarchy_guh h =
183 let val i = indentation
185 fun node i p theID (Ptyp (id,_,ns)) =
186 let val p' = lev_on p
187 val theID' = theID @ [id]
188 in (indt i) ^ "<NODE>\n" ^
189 (indt (i+j)) ^ "<ID> " ^ id ^ " </ID>\n" ^
190 (indt (i+j)) ^ "<NO> " (*on this level*) ^
191 (string_of_int o last_elem) p' ^ " </NO>\n" ^
192 (indt (i+j)) ^ "<CONTENTREF> " ^ theID2guh theID' ^
194 (nodes (i+j) (lev_dn p') theID' ns) ^
195 (indt i) ^ "</NODE>\n"
197 and nodes _ _ _ [] = ""
198 | nodes i p theID (n::ns) = (node i p theID n)
199 ^ (nodes i (lev_on p) theID ns);
200 in nodes j [0] [] h end;
202 fun thy_hierarchy2file (path:path) =
203 str2file (path ^ "thy_hierarchy.xml")
205 " <ID> theory hierarchy </ID>\n" ^
207 " <CONTENTREF> thy_ROOT </CONTENTREF>\n" ^
208 (hierarchy_guh (!thehier)) ^
212 (**.create the xml-files for the theory-data from the hierarchy.**)
215 (*.analoguous to 'fun met2xml'.*)
216 fun thydata2xml (theID:theID, Html {guh, coursedesign, mathauthors, html}) =
218 indt i ^ "<GUH> "^ guh ^" </GUH>\n" ^
220 indt i ^ "<EXPLANATIONS> " ^ html ^ "</EXPLANATIONS>\n" ^
221 authors2xml i "MATHAUTHORS" mathauthors ^
222 authors2xml i "COURSEDESIGNS" coursedesign ^
223 "</HTMLDATA>\n" : xml
224 | thydata2xml (theID:theID, Hthm {guh, coursedesign, mathauthors, thm}) =
226 indt i ^ "<GUH> "^ guh ^" </GUH>\n" ^
229 indt i ^ "<PROOF>\n" ^
230 extref2xml (i+i) "Proof of the theorem"
231 ("http://www.ist.tugraz.at/projects/isac/www/\
232 \kbase/thy/browser_info/HOL/HOL-Real/Isac/" ^
233 nth 2 theID ^ ".html") ^
234 indt i ^ "</PROOF>\n" ^
235 indt i ^ "<EXPLANATIONS> </EXPLANATIONS>\n" ^
236 authors2xml i "MATHAUTHORS" mathauthors ^
237 authors2xml i "COURSEDESIGNS" coursedesign ^
239 (* val (theID:theID, Hrls {guh, coursedesign, mathauthors, thy_rls}) =
242 | thydata2xml (theID, Hrls {guh, coursedesign, mathauthors, thy_rls}) =
244 indt i ^ "<GUH> "^ guh ^" </GUH>\n" ^
247 indt i ^ "<EXPLANATIONS> </EXPLANATIONS>\n" ^
248 authors2xml i "MATHAUTHORS" mathauthors ^
249 authors2xml i "COURSEDESIGNS" coursedesign ^
251 (* val (theID:theID, Hcal {guh, coursedesign, mathauthors, calc}) =
254 | thydata2xml (theID, Hcal {guh, coursedesign, mathauthors, calc}) =
256 indt i ^ "<GUH> "^ guh ^" </GUH>\n" ^
258 calc2xml i (theID2thyID theID, calc) ^
259 indt i ^ "<EXPLANATIONS> </EXPLANATIONS>\n" ^
260 authors2xml i "MATHAUTHORS" mathauthors ^
261 authors2xml i "COURSEDESIGNS" coursedesign ^
263 | thydata2xml (theID, _) =
264 error ("thydata2xml: not implemented for "^ strs2str' theID);
266 (*.analoguous to 'fun met2file'.*)
267 fun thydata2file (xmldata:path) (pos:pos) (theID:theID) thydata =
268 (writeln ("### thes2file: id = " ^ strs2str theID);
269 str2file (xmldata ^ theID2filename theID)
270 (thydata2xml (theID:theID, thydata)));
272 (*.analoguous to 'fun node'; here we scan ??????????.*)
273 (* val (pa, ids, po, wfn, (Ptyp (id,[n],ns))) =
274 (pa, ids, po, wfn, n);
276 fun thenode (pa:path) ids po wfn (Ptyp (id,[n],ns)) =
277 let val po' = lev_on po
278 in wfn pa po' (ids@[id]) n;
279 thenodes pa (ids@[id]) ((lev_dn po'):pos) wfn ns end
280 (* val (pa, ids, po, wfn, (n::ns)) =
281 (path, []:string list, [0], thydata2file, (!thehier));
283 and thenodes _ _ _ _ [] = ()
284 | thenodes pa ids po wfn (n::ns) = (thenode pa ids po wfn n;
285 thenodes pa ids (lev_on po) wfn ns);
287 (*..analoguous to 'fun mets2file'*)
288 fun thes2file (p : path) =
289 thenodes p [] [0] thydata2file (!thehier);
292 (***.store a single theory element in the hierarchy.***)
294 (*.for mathauthors only, other html is added to xml exported from here.*)
295 (* val (theID, mathauthors) =
296 (["IsacKnowledge", theory2thyID Biegelinie.thy, "Theorems"],
297 ["Walther Neuper 2005 supported by a grant from NMI Austria"]);
299 fun store_isa (theID : theID) (mathauthors : authors) =
300 let val guh = case theID of
301 [part] => part2guh theID
302 | [part, thyID, thypart] => thypart2guh theID
303 val theID = guh2theID guh
304 val the = Html {guh = guh,
306 mathauthors = mathauthors,
308 in (*needs no (!check_guhs_unique) because guh is generated automatically*)
309 thehier := insrt theID the theID (!thehier) end;
311 fun store_thy thy (mathauthors : authors) =
312 let val guh = thy2guh ["IsacKnowledge", theory2thyID thy]
313 val theID = guh2theID guh
314 val the = Html {guh = guh,
316 mathauthors = mathauthors,
318 in (*needs no (!check_guhs_unique) because guh is generated automatically*)
319 thehier := insrt theID the theID (!thehier) end;
321 fun store_thm thy (thmID : thmID, thm) (mathauthors : authors) =
322 let val guh = thm2guh ("IsacKnowledge", theory2thyID thy) thmID
323 val theID = guh2theID guh
324 val the = Hthm {guh = guh,
325 coursedesign = [], (*done at xml exported from here*)
326 mathauthors=mathauthors,
328 in (*needs no (!check_guhs_unique) because guh is generated automatically*)
329 thehier := insrt theID the theID (!thehier) end;
331 fun store_rls thy rls (mathauthors : authors) =
332 let val guh = rls2guh ("IsacKnowledge", theory2thyID thy)
333 ((#id o rep_rls) rls)
334 val theID = guh2theID guh
335 val the = Hrls {guh = guh,
337 mathauthors = mathauthors,
338 thy_rls=(theory2thyID thy, rls)}
339 in (*needs no (!check_guhs_unique) because guh is generated automatically*)
340 thehier := insrt theID the theID (!thehier) end;
342 fun store_cal thy cal (mathauthors : authors) =
343 let val guh = cal2guh ("IsacKnowledge", theory2thyID thy)
345 val theID = guh2theID guh
346 val the = Hcal {guh = guh,
348 mathauthors = mathauthors,
350 in (*needs no (!check_guhs_unique) because guh is generated automatically*)
351 thehier := insrt theID the theID (!thehier) end;
353 fun store_ord thy ord (mathauthors : authors) =
354 let val guh = ord2guh ("IsacKnowledge", theory2thyID thy)
356 val theID = guh2theID guh
357 val the = Hord {guh = guh,
359 mathauthors = mathauthors,
361 in (*needs no (!check_guhs_unique) because guh is generated automatically*)
362 thehier := insrt theID the theID (!thehier) end;