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: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})
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')) (thms_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)
94 val scri_thys = (map (get_thy o #1) (!script_thys))
96 val isac_thys = (map (get_thy o #1)
97 (!theory')) \\ scri_thys \\ ["e_domID"]
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
105 fun show_thes () = (writeln o format_pblIDl o (scan [])) (!thehier);
109 (***.create the xml-format for the hierarchy.***)
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).**)
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;
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)
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);
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);
144 fun fill_parents th cutID theID =
145 let val cutID' = cut_theID th cutID
148 else let val th' = insrt cutID' (Html {guh=theID2guh theID,
149 coursedesign=["isac team 2006"],
152 val cutID_ = cutID' @ [nth ((length cutID') + 1) theID]
153 in fill_parents th' cutID_ theID end
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 ());
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);
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;
175 (*these files shall contain 'invisible' html
176 val thydatafilename = "thy_datafile.xml"; (*for "Theorems"|...*)
177 fun partfilename str = "thy_" ^ str ^ ".xml"; (*for "Isabelle"|...*)*)
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
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' ^
193 (nodes (i+j) (lev_dn p') theID' ns) ^
194 (indt i) ^ "</NODE>\n"
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;
201 fun thy_hierarchy2file (path:path) =
202 str2file (path ^ "thy_hierarchy.xml")
204 " <ID> theory hierarchy </ID>\n" ^
206 " <CONTENTREF> thy_ROOT </CONTENTREF>\n" ^
207 (hierarchy_guh (!thehier)) ^
211 (**.create the xml-files for the theory-data from the hierarchy.**)
214 (*.analoguous to 'fun met2xml'.*)
215 fun thydata2xml (theID:theID, Html {guh, coursedesign, mathauthors, html}) =
217 indt i ^ "<GUH> "^ guh ^" </GUH>\n" ^
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}) =
225 indt i ^ "<GUH> "^ guh ^" </GUH>\n" ^
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 ^
238 (* val (theID:theID, Hrls {guh, coursedesign, mathauthors, thy_rls}) =
241 | thydata2xml (theID, Hrls {guh, coursedesign, mathauthors, thy_rls}) =
243 indt i ^ "<GUH> "^ guh ^" </GUH>\n" ^
246 indt i ^ "<EXPLANATIONS> </EXPLANATIONS>\n" ^
247 authors2xml i "MATHAUTHORS" mathauthors ^
248 authors2xml i "COURSEDESIGNS" coursedesign ^
250 (* val (theID:theID, Hcal {guh, coursedesign, mathauthors, calc}) =
253 | thydata2xml (theID, Hcal {guh, coursedesign, mathauthors, calc}) =
255 indt i ^ "<GUH> "^ guh ^" </GUH>\n" ^
257 calc2xml i (theID2thyID theID, calc) ^
258 indt i ^ "<EXPLANATIONS> </EXPLANATIONS>\n" ^
259 authors2xml i "MATHAUTHORS" mathauthors ^
260 authors2xml i "COURSEDESIGNS" coursedesign ^
262 | thydata2xml (theID, _) =
263 raise error ("thydata2xml: not implemented for "^ strs2str' theID);
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)));
271 (*.analoguous to 'fun node'; here we scan ??????????.*)
272 (* val (pa, ids, po, wfn, (Ptyp (id,[n],ns))) =
273 (pa, ids, po, wfn, n);
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));
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);
286 (*..analoguous to 'fun mets2file'*)
287 fun thes2file (p : path) =
288 thenodes p [] [0] thydata2file (!thehier);
291 (***.store a single theory element in the hierarchy.***)
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"]);
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,
305 mathauthors = mathauthors,
307 in (*needs no (!check_guhs_unique) because guh is generated automatically*)
308 thehier := insrt theID the theID (!thehier) end;
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,
315 mathauthors = mathauthors,
317 in (*needs no (!check_guhs_unique) because guh is generated automatically*)
318 thehier := insrt theID the theID (!thehier) end;
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,
327 in (*needs no (!check_guhs_unique) because guh is generated automatically*)
328 thehier := insrt theID the theID (!thehier) end;
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,
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;
341 fun store_cal thy cal (mathauthors : authors) =
342 let val guh = cal2guh ("IsacKnowledge", theory2thyID thy)
344 val theID = guh2theID guh
345 val the = Hcal {guh = guh,
347 mathauthors = mathauthors,
349 in (*needs no (!check_guhs_unique) because guh is generated automatically*)
350 thehier := insrt theID the theID (!thehier) end;
352 fun store_ord thy ord (mathauthors : authors) =
353 let val guh = ord2guh ("IsacKnowledge", theory2thyID thy)
355 val theID = guh2theID guh
356 val the = Hord {guh = guh,
358 mathauthors = mathauthors,
360 in (*needs no (!check_guhs_unique) because guh is generated automatically*)
361 thehier := insrt theID the theID (!thehier) end;