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