1 (* title: "xmlsrc/thy-hierarchy.sml"
2 export theory-data "thehier" to xml
3 author: Walther Neuper 0601
7 open TermC (* allows contains_one_of to be infix *)
9 (* copy from mutabelle_extra.ML, fun thms_of *)
10 fun thms_of thy = (* das ist zu verbessern *)
12 val fun_ids = Specify.get_fun_ids thy
14 filter (fn thm => Context.theory_name (Thm.theory_of_thm thm) = Context.theory_name thy
15 andalso not (thm contains_one_of fun_ids)
16 andalso not (Celem.thmID_of_derivation_name' thm = "mono"))
17 (* created in Biegelinie by partial_function ^^^^^^*)
18 (map snd (Global_Theory.all_thms_of thy false))
21 (* wrap theory-data into the uniform type thydata *)
23 fun makeHthm (part : string, thyID : Rule.thyID) (thm : thm) =
24 let val theID = [part, thyID, "Theorems"] @ [Celem.thmID_of_derivation_name' thm] : Celem.theID
25 in (theID, Celem.Hthm {guh = Celem.theID2guh theID, coursedesign = [],
26 mathauthors = ["isac-team"], fillpats = [], thm = thm})
28 fun makeHrls (part : string) (rls' : Rule.rls', thy_rls as (thyID, rls): Rule.thyID * Rule.rls) =
29 let val theID = [part, thyID,"Rulesets"] @ [rls'] : Celem.theID
30 in (theID, Celem.Hrls {guh = Celem.theID2guh theID, coursedesign = [],
31 mathauthors = ["isac-team"], thy_rls = thy_rls})
33 fun makeHcal (part : string, thyID : Rule.thyID) (calID, cal) =
34 let val theID = [part, thyID,"Operations"] @ [calID] : Celem.theID
35 in (theID, Celem.Hcal {guh = Celem.theID2guh theID, coursedesign=[],
36 mathauthors = ["isac-team"], calc = cal})
38 fun makeHord (part : string, thyID : Rule.thyID) (ordID, ord) =
39 let val theID = [part, thyID,"TODO-Orders"] @ [ordID] : Celem.theID
40 in (theID, Celem.Hord {guh = Celem.theID2guh theID, coursedesign=[],
41 mathauthors = ["isac-team"], ord = ord})
44 fun revert_sym thy (Rule.Thm (thmID, thm)) =
45 if (Rtools.is_sym o Celem.thmID_of_derivation_name) thmID
48 val thmID' = Rtools.sym_drop thmID
49 val thm' = Rewrite.assoc_thm' thy (thmID',"")
50 val thmDeriv' = Thm.get_name_hint thm'
51 in Rule.Thm (thmDeriv', thm') end
52 else Rule.Thm (Thm.get_name_hint thm, thm)
54 (* get all theorems from the list of rule-sets (defined in Knowledge) *)
55 fun thms_of_rlss thy rlss = (rlss : (Rule.rls' * (Rule.theory' * Rule.rls)) list)
56 |> map (Rtools.thms_of_rls o #2 o #2)
58 |> map (revert_sym thy)
59 |> map (fn Rule.Thm (thmID, thm) => (thmID, thm))
60 |> gen_distinct (fn ((thmID1, _), (thmID2, _)) => thmID1 = thmID2)
61 : (Celem.thmID * thm) list
63 (* collect all thydata defined in in a theory *)
65 fun collect_thms part thy =
66 map (makeHthm (part, Context.theory_name thy)) (rev (thms_of thy))
67 fun collect_rlss part rlss thys = (rlss : (Rule.rls' * (Rule.thyID * Rule.rls)) list)
68 |> filter (fn (_, (thyID, _)) => member (op=) (map Context.theory_name thys) thyID)
69 |> map (makeHrls part)
70 fun collect_cals (part, thy') =
71 let val cals = [] (*FIXXXXXXXXXXME.WN060713 add thyID: (thyID, cal)*)
72 in map (makeHcal (part, thy')) cals end;
73 fun collect_ords (part, thy') =
74 let val thy = Celem.assoc_thy (Rule.thyID2theory' thy')
75 in [(*TODO.WN060120 rew_ord, Calc*)]:(Celem.theID * Celem.thydata) list end;
77 (* parts are: Isabelle | IsacKnowledge | IsacScripts, see KEStore.thy *)
78 fun collect_part part parent thys =
79 (flat (map (collect_thms part) thys)) @
80 (collect_rlss part (KEStore_Elems.get_rlss parent) thys) @
81 [(*TODO: collect_cals, collect_ords*)]
83 (* collect theorems defined in Isabelle *)
84 fun collect_isab isa (thmDeriv, thm) =
86 [isa, Celem.thyID_of_derivation_name thmDeriv, "Theorems", Celem.thmID_of_derivation_name thmDeriv]
88 (theID: Celem.theID, Celem.Hthm {guh = Celem.theID2guh theID,
89 mathauthors = ["Isabelle team, TU Munich"],
95 fun show_thes () = (writeln o Specify.format_pblIDl o (Specify.scan [])) (get_thes ());
98 (** create an xml representation for thehier: hierarchy of entries + files per entry **)
100 (* create an xml-hierarchy where the filname is created from the guh;
101 ad DTD: a NODE contains an ID and zero or more NODEs*)
102 fun hierarchy_guh h =
106 fun node i p theID (Celem.Ptyp (id, _, ns)) =
108 val p' = Ctree.lev_on p
109 val theID' = theID @ [id]
111 (indt i) ^ "<NODE>\n" ^
112 (indt (i+j)) ^ "<ID> " ^ id ^ " </ID>\n" ^
113 (indt (i+j)) ^ "<NO> " (*on this level*) ^ (string_of_int o last_elem) p' ^ " </NO>\n" ^
114 (indt (i+j)) ^ "<CONTENTREF> " ^ Celem.theID2guh theID' ^ " </CONTENTREF>\n" ^
115 (nodes (i+j) (Ctree.lev_dn p') theID' ns) ^
116 (indt i) ^ "</NODE>\n"
118 and nodes _ _ _ [] = ""
119 | nodes i p theID (n :: ns) = (node i p theID n) ^ (nodes i (Ctree.lev_on p) theID ns);
120 in nodes j [0] [] h end;
122 fun thy_hierarchy2file (path: Celem.path) =
123 str2file (path ^ "thy_hierarchy.xml")
125 " <ID> theory hierarchy </ID>\n" ^
127 " <CONTENTREF> thy_ROOT </CONTENTREF>\n" ^
128 (hierarchy_guh (get_thes ())) ^
131 (* create the xml-files for the thydata in the hierarchy *)
133 (* analoguous to 'fun met2xml' *)
134 fun thydata2xml (theID: Celem.theID, Celem.Html {guh, coursedesign, mathauthors, html}) =
136 indt i ^ "<GUH> "^ guh ^" </GUH>\n" ^
138 indt i ^ "<EXPLANATIONS> " ^ html ^ "</EXPLANATIONS>\n" ^
139 authors2xml i "MATHAUTHORS" mathauthors ^
140 authors2xml i "COURSEDESIGNS" coursedesign ^
141 "</HTMLDATA>\n" : Celem.xml
142 | thydata2xml (theID, Celem.Hthm {guh, coursedesign, mathauthors, fillpats(*TODO?*), thm}) =
144 indt i ^ "<GUH> "^ guh ^" </GUH>\n" ^
147 indt i ^ "<PROOF>\n" ^
148 extref2xml (i+i) "Proof of the theorem" (* TODO "Unsorted"vvv: distinguish Isabelle | Isac *)
149 ("http://www.ist.tugraz.at/projects/isac/www/kbase/thy/browser_info/HOL/HOL-Real/Isac/" ^
150 nth 2 theID ^ ".html") ^
151 indt i ^ "</PROOF>\n" ^
152 indt i ^ "<EXPLANATIONS> </EXPLANATIONS>\n" ^
153 authors2xml i "MATHAUTHORS" mathauthors ^
154 authors2xml i "COURSEDESIGNS" coursedesign ^
156 | thydata2xml (theID, Celem.Hrls {guh, coursedesign, mathauthors, thy_rls}) =
158 indt i ^ "<GUH> "^ guh ^" </GUH>\n" ^
161 indt i ^ "<EXPLANATIONS> </EXPLANATIONS>\n" ^
162 authors2xml i "MATHAUTHORS" mathauthors ^
163 authors2xml i "COURSEDESIGNS" coursedesign ^
165 | thydata2xml (theID, Celem.Hcal {guh, coursedesign, mathauthors, calc}) =
167 indt i ^ "<GUH> "^ guh ^" </GUH>\n" ^
169 calc2xml i (Celem.theID2thyID theID, calc) ^
170 indt i ^ "<EXPLANATIONS> </EXPLANATIONS>\n" ^
171 authors2xml i "MATHAUTHORS" mathauthors ^
172 authors2xml i "COURSEDESIGNS" coursedesign ^
174 | thydata2xml (theID, _) =
175 error ("thydata2xml: not implemented for "^ strs2str' theID);
177 (* analoguous to 'fun met2file' *)
178 fun thydata2file (path : Celem.path) (pos : Ctree.pos) (theID : Celem.theID) thydata =
179 (writeln ("### thes2file: id = " ^ strs2str theID);
180 str2file (path ^ Rtools.theID2filename theID) (thydata2xml (theID, thydata)));
182 (* analoguous to 'fun node' *)
183 fun thenode (pa : Celem.path) ids po wfn (Celem.Ptyp (id, [n], ns)) =
184 let val po' = Ctree.lev_on po
185 in wfn pa po' (ids @ [id]) n; thenodes pa (ids @ [id]) (Ctree.lev_dn po') wfn ns end
186 and thenodes _ _ _ _ [] = ()
187 | thenodes pa ids po wfn (n::ns) =
188 (thenode pa ids po wfn n; thenodes pa ids (Ctree.lev_on po) wfn ns);
190 (* analoguous to 'fun mets2file' *)
191 fun thes2file (p : Celem.path) = thenodes p [] [0] thydata2file (get_thes ());
194 (***.store a single theory element in the hierarchy.***)
196 (*.for mathauthors only, other html is added to xml exported from here.*)
197 fun make_isa thy (part, thypart) (mathauthors : Celem.authors) =
199 val theID = [part, Rule.string_of_thy thy, thypart]
200 val guh = case theID of
201 [part] => Celem.part2guh theID
202 | [part, thyID, thypart] => Celem.thypart2guh theID
203 val theID = Rtools.guh2theID guh
204 val the = Celem.Html {guh = guh, coursedesign = [], mathauthors = mathauthors, html = ""}
207 fun make_thy thy (mathauthors : Celem.authors) =
209 val guh = Celem.thy2guh ["IsacKnowledge", Rule.theory2thyID thy]
210 val theID = Rtools.guh2theID guh
211 val the = Celem.Html {guh = guh, coursedesign = [], mathauthors = mathauthors, html = ""}
214 fun make_thm thy part (thmID : Celem.thmID, thm) (mathauthors : Celem.authors) =
216 val guh = Celem.thm2guh (part, Rule.theory2thyID thy) thmID
217 val theID = Rtools.guh2theID guh
218 val the = Celem.Hthm {guh = guh, coursedesign = [(*inserted in xml after export*)],
219 mathauthors = mathauthors, fillpats = [], thm = thm}
222 fun make_rls thy rls (mathauthors : Celem.authors) =
224 val guh = Celem.rls2guh ("IsacKnowledge", Rule.theory2thyID thy) ((#id o Rule.rep_rls) rls)
225 val theID = Rtools.guh2theID guh
226 val the = Celem.Hrls {guh = guh, coursedesign = [], mathauthors = mathauthors,
227 thy_rls = (Rule.theory2thyID thy, rls)}
228 (*needs no (!check_guhs_unique) because guh is generated automatically*)
231 fun make_cal thy cal (mathauthors : Celem.authors) =
233 val guh = Celem.cal2guh ("IsacKnowledge", Rule.theory2thyID thy) ("TODO store_cal")
234 val theID = Rtools.guh2theID guh
235 val the = Celem.Hcal {guh = guh, coursedesign = [], mathauthors = mathauthors, calc = cal}
238 fun make_ord thy ord (mathauthors : Celem.authors) =
240 val guh = Celem.ord2guh ("IsacKnowledge", Rule.theory2thyID thy) ("TODO store_ord")
241 val theID = Rtools.guh2theID guh
242 val the = Celem.Hord {guh = guh, coursedesign = [], mathauthors = mathauthors, ord = ord}
245 fun insert_errpatIDs thy theID errpatIDs = (* TODO: redo like insert_fillpatts *)
247 val hrls = Specify.get_the theID
248 val hrls' = Celem.update_hrls hrls errpatIDs
249 handle ERROR _ => error ("insert_errpatIDs: " ^ strs2str theID ^ "must address a rule-set")
250 in (hrls', theID) end