|
1 (* convert sml-datatypes to xml |
|
2 authors: Walther Neuper 2003 |
|
3 (c) due to copyright terms |
|
4 |
|
5 use"xmlsrc/datatypes.sml"; |
|
6 use"datatypes.sml"; |
|
7 *) |
|
8 |
|
9 signature DATATYPES = |
|
10 sig |
|
11 val authors2xml : int -> string -> string list -> xml |
|
12 val calc2xml : int -> thyID * calc -> xml |
|
13 val calcrefs2xml : int -> thyID * calc list -> xml |
|
14 val contthy2xml : int -> contthy -> xml |
|
15 val extref2xml : int -> string -> string -> xml |
|
16 val filterpbl : |
|
17 ''a -> (''a * (Term.term * Term.term)) list -> Term.term list |
|
18 val formula2xml : int -> Term.term -> xml |
|
19 val formulae2xml : int -> Term.term list -> xml |
|
20 val i : int |
|
21 val id2xml : int -> string list -> string |
|
22 val ints2xml : int -> int list -> string |
|
23 val itm_2xml : int -> SpecifyTools.itm_ -> xml |
|
24 val itms2xml : |
|
25 int -> |
|
26 (int * SpecifyTools.vats * bool * string * SpecifyTools.itm_) list -> |
|
27 string |
|
28 val keref2xml : int -> ketype -> kestoreID -> xml |
|
29 val model2xml : |
|
30 int -> SpecifyTools.itm list -> (bool * Term.term) list -> xml |
|
31 val modspec2xml : int -> ocalhd -> xml |
|
32 val pattern2xml : |
|
33 int -> |
|
34 (string * (Term.term * Term.term)) list -> Term.term list -> string |
|
35 val pos'2xml : int -> string * (int list * pos_) -> string |
|
36 val pos'calchead2xml : int -> pos' * ocalhd -> xml |
|
37 val pos_2xml : int -> pos_ -> string |
|
38 val posform2xml : int -> pos' * Term.term -> xml |
|
39 val posformhead2xml : int -> pos' * ptform -> string |
|
40 val posformheads2xml : int -> (pos' * ptform) list -> xml |
|
41 val posforms2xml : int -> (pos' * Term.term) list -> xml |
|
42 val posterms2xml : int -> (pos' * term) list -> xml |
|
43 val precond2xml : int -> bool * Term.term -> xml |
|
44 val preconds2xml : int -> (bool * Term.term) list -> xml |
|
45 val rls2xml : int -> thyID * rls -> xml |
|
46 val rule2xml : int -> guh -> rule -> xml |
|
47 val rules2xml : int -> guh -> rule list -> xml |
|
48 val scr2xml : int -> scr -> xml |
|
49 val spec2xml : int -> spec -> xml |
|
50 val sub2xml : int -> Term.term * Term.term -> xml |
|
51 val subs2xml : int -> subs -> xml |
|
52 val subst2xml : int -> subst -> xml |
|
53 val tac2xml : int -> tac -> xml |
|
54 val tacs2xml : int -> tac list -> xml |
|
55 val theref2xml : int -> thyID -> string -> xstring -> string |
|
56 val thm'2xml : int -> thm' -> xml |
|
57 val thm''2xml : int -> thm -> xml |
|
58 val thmstr2xml : int -> string -> xml |
|
59 end |
|
60 |
|
61 |
|
62 |
|
63 (*------------------------------------------------------------------*) |
|
64 structure datatypes:DATATYPES = |
|
65 struct |
|
66 (*------------------------------------------------------------------*) |
|
67 |
|
68 val i = indentation; |
|
69 |
|
70 (** general types: lists, **) |
|
71 |
|
72 (*.handles string list like 'fun id2xml'.*) |
|
73 fun authors2xml j str auts = |
|
74 let fun autx _ [] = "" |
|
75 | autx j (s::ss) = (indt j) ^ "<STRING> " ^ s ^ " </STRING>\n" ^ |
|
76 (autx j ss) |
|
77 in indt j ^ "<"^str^">\n" ^ |
|
78 autx (j + i) auts ^ |
|
79 indt j ^ "</"^str^">\n" : xml |
|
80 end; |
|
81 (* writeln(authors2xml 2 "MATHAUTHORS" []); |
|
82 writeln(authors2xml 2 "MATHAUTHORS" |
|
83 ["isac-team 2001", "Richard Lang 2003"]); |
|
84 *) |
|
85 |
|
86 fun id2xml j ids = |
|
87 let fun id2x _ [] = "" |
|
88 | id2x j (s::ss) = (indt j) ^ "<STRING> " ^ s ^ " </STRING>\n" ^ |
|
89 (id2x j ss) |
|
90 in (indt j) ^ "<STRINGLIST>\n" ^ |
|
91 (id2x (j + indentation) ids) ^ |
|
92 (indt j) ^ "</STRINGLIST>\n" end; |
|
93 (* writeln(id2xml 8 ["linear","univariate","equation"]); |
|
94 <STRINGLIST> |
|
95 <STRING>linear</STRING> |
|
96 <STRING>univariate</STRING> |
|
97 <STRING>equation</STRING> |
|
98 </STRINGLIST>*) |
|
99 |
|
100 fun ints2xml j ids = |
|
101 let fun int2x _ [] = "" |
|
102 | int2x j (s::ss) = (indt j) ^"<INT> "^ string_of_int s ^" </INT>\n"^ |
|
103 (int2x j ss) |
|
104 in (indt j) ^ "<INTLIST>\n" ^ |
|
105 (int2x (j + i) ids) ^ |
|
106 (indt j) ^ "</INTLIST>\n" end; |
|
107 (* writeln(ints2xml 3 [1,2,3]); |
|
108 *) |
|
109 |
|
110 |
|
111 (** isac datatypes **) |
|
112 |
|
113 fun pos_2xml j pos_ = |
|
114 (indt j) ^ "<POS> " ^ pos_2str pos_ ^ " </POS>\n"; |
|
115 |
|
116 (*.due to specialties of isac/util/parser/XMLParseDigest.java |
|
117 pos' requires different tags.*) |
|
118 fun pos'2xml j (tag, (pos, pos_)) = |
|
119 indt (j) ^ "<" ^ tag ^ ">\n" ^ |
|
120 ints2xml (j+i) pos ^ |
|
121 pos_2xml (j+i) pos_ ^ |
|
122 indt (j) ^ "</" ^ tag ^ ">\n"; |
|
123 (* writeln(pos'2xml 3 ("POSITION", ([1,2,3], Pbl))); |
|
124 *) |
|
125 |
|
126 fun formula2xml j term = (*TODO.WN050211: use for _all_ <FORMULA>*) |
|
127 indt j ^ "<FORMULA>\n"^ |
|
128 term2xml j term ^"\n"^ |
|
129 indt j ^ "</FORMULA>\n" : xml; |
|
130 (* writeln(formula2xml 6 (str2term "1+1=2")); |
|
131 *) |
|
132 fun formulae2xml j [] = ("":xml) |
|
133 | formulae2xml j (r::rs) = formula2xml j r ^ formulae2xml j rs; |
|
134 (* writeln(formulae2xml 6 [str2term "1+1=2", str2term "1+1+1=3"]); |
|
135 *) |
|
136 |
|
137 (*WN0502 @see ME/ctree: type asms: illdesigned, thus not used*) |
|
138 fun posform2xml j (p:pos', term) = |
|
139 indt j ^ "<POSFORM>\n" ^ |
|
140 pos'2xml (j+i) ("POSITION", p) ^ |
|
141 indt (j+i) ^ "<FORMULA>\n"^ |
|
142 term2xml (j+i) term ^"\n"^ |
|
143 indt (j+i) ^ "</FORMULA>\n"^ |
|
144 indt j ^ "</POSFORM>\n" : xml; |
|
145 (* writeln(posform2xml 6 (([1,2],Frm), str2term "1+1=2")); |
|
146 *) |
|
147 fun posforms2xml j [] = ("":xml) |
|
148 | posforms2xml j (r::rs) = posform2xml j r ^ posforms2xml j rs; |
|
149 (* writeln(posforms2xml 6 [(([1],Res), str2term "1+1=2"),(([2],Res), str2term "1+1+1=3")]); |
|
150 *) |
|
151 |
|
152 fun calcref2xml j (thyID:thyID, (scrop, (rewop, _)):calc) = |
|
153 indt j ^ "<CALCREF>\n" ^ |
|
154 indt (j+i) ^ "<STRING> " ^ scrop ^ "</STRING>\n" ^ |
|
155 indt (j+i) ^ "<GUH> " ^ cal2guh ("IsacKnowledge", |
|
156 thyID) scrop ^ " </GUH>\n" ^ |
|
157 indt j ^ "</CALCREF>\n" : xml; |
|
158 fun calcrefs2xml _ (_,[]) = "":xml |
|
159 | calcrefs2xml j (thyID, cal::cs) = |
|
160 calcref2xml j (thyID, cal) ^ calcrefs2xml j (thyID, cs); |
|
161 |
|
162 fun calc2xml j (thyID:thyID, (scrop, (rewop, _)):calc) = |
|
163 indt j ^ "<CALC>\n" ^ |
|
164 indt (j+i) ^ "<STRING>\n" ^ scrop ^ "</STRING>\n" ^ |
|
165 indt (j+i) ^ "<GUH>\n" ^ cal2guh ("IsacKnowledge", |
|
166 thyID) scrop ^ "</GUH>\n" ^ |
|
167 indt (j+i) ^ "<TERMOP>\n" ^ rewop ^ "</TERMOP>\n" ^ |
|
168 indt j ^ "</CALC>\n" : xml; |
|
169 |
|
170 (*.for creating a href for a rule within an rls's rule list; |
|
171 the guh points to the thy of definition of the rule, NOT of use in rls.*) |
|
172 fun rule2xml j (thyID:thyID) Erule = |
|
173 raise error "rule2xml called with 'Erule'" |
|
174 (* val (j, thyID, Thm (thmID, thm)) = (j+i, thyID, nth 1 rules); |
|
175 val (j, thyID, Thm (thmID, thm)) = (j, thyID,r); |
|
176 *) |
|
177 | rule2xml j thyID (Thm (thmID, thm)) = |
|
178 indt j ^ "<RULE>\n" ^ |
|
179 indt (j+i) ^ "<TAG> Theorem </TAG>\n" ^ |
|
180 indt (j+i) ^ "<STRING> " ^ thmID ^ " </STRING>\n" ^ |
|
181 indt (j+i) ^ "<GUH> " ^ thm2guh (thy_containing_thm thyID thmID) |
|
182 thmID ^ " </GUH>\n" ^ |
|
183 indt j ^ "</RULE>\n" : xml |
|
184 (* val (j, thyID, Calc (termop, _)) = (j+i, thyID, nth 42 rules); |
|
185 val (j, thyID, Calc (termop, _)) = (j+i, thyID, nth 43 rules); |
|
186 *) |
|
187 | rule2xml j thyID (Calc (termop, _)) = "" |
|
188 (*FIXXXXXXXME.WN060714 in rls make Calc : calc -> rule [add scriptop!] |
|
189 see smltest/../datatypes.sml ! |
|
190 indt j ^ "<RULE>\n" ^ |
|
191 indt (j+i) ^ "<STRING> " ^ termop ^ " </STRING>\n" ^ |
|
192 indt (j+i) ^ "<GUH> " ^ cal2guh (thy_containing_cal thyID termop) |
|
193 termop ^ " </GUH>\n" ^ |
|
194 indt j ^ "</RULE>\n" |
|
195 *) |
|
196 | rule2xml j thyID (Cal1 (termop, _)) = "" |
|
197 | rule2xml j thyID (Rls_ rls) = |
|
198 let val rls' = (#id o rep_rls) rls |
|
199 in indt j ^ "<RULE>\n" ^ |
|
200 indt (j+i) ^ "<TAG> Ruleset </TAG>\n" ^ |
|
201 indt (j+i) ^ "<STRING> " ^ rls' ^ " </STRING>\n" ^ |
|
202 indt (j+i) ^ "<GUH> " ^ rls2guh (thy_containing_rls thyID rls') |
|
203 rls' ^ " </GUH>\n" ^ |
|
204 indt j ^ "</RULE>\n" |
|
205 end; |
|
206 (* val (j, thyID, r::rs) = (2, "Test", rules); |
|
207 *) |
|
208 fun rules2xml j thyID [] = ("":xml) |
|
209 | rules2xml j thyID (r::rs) = rule2xml j thyID r ^ rules2xml j thyID rs; |
|
210 |
|
211 fun filterpbl str = |
|
212 let fun filt [] = [] |
|
213 | filt ((s, (t1, t2)) :: ps) = |
|
214 if str = s then (t1 $ t2) :: filt ps else filt ps |
|
215 in filt end; |
|
216 |
|
217 (*FIXME.WN040831 model2xml <--?--> pattern2xml*) |
|
218 (*WN.25.8.03: pattern2xml different output with TextIO | writeln !!! |
|
219 the version below is for TextIO: terms2xml makes \n !*) |
|
220 (* val (j, p, where_) = (i, ppc, where_); |
|
221 *) |
|
222 fun pattern2xml j p where_ = |
|
223 (case filterpbl "#Given" p of |
|
224 [] => (indt j) ^ "<GIVEN> </GIVEN>\n" |
|
225 (* val gis = filterpbl "#Given" p; |
|
226 *) |
|
227 | gis => (indt j) ^ "<GIVEN>\n" ^ terms2xml' j gis ^ |
|
228 (indt j) ^ "</GIVEN>\n") |
|
229 ^ |
|
230 (case where_ of |
|
231 [] => (indt j) ^ "<WHERE> </WHERE>\n" |
|
232 | whs => (indt j) ^ "<WHERE>\n" ^ terms2xml' j whs ^ |
|
233 (indt j) ^ "</WHERE>\n") |
|
234 ^ |
|
235 (case filterpbl "#Find" p of |
|
236 [] => (indt j) ^ "<FIND> </FIND>\n" |
|
237 | fis => (indt j) ^ "<FIND>\n" ^ terms2xml' j fis ^ |
|
238 (indt j) ^ "</FIND>\n") |
|
239 ^ |
|
240 (case filterpbl "#Relate" p of |
|
241 [] => (indt j) ^ "<RELATE> </RELATE>\n" |
|
242 | res => (indt j) ^ "<RELATE>\n" ^ terms2xml' j res ^ |
|
243 (indt j) ^ "</RELATE>\n"); |
|
244 (* |
|
245 writeln(pattern2xml 3 ((#ppc o get_pbt) |
|
246 ["squareroot","univariate","equation","test"]) []); |
|
247 *) |
|
248 |
|
249 (*see itm_2item*) |
|
250 fun itm_2xml j (Cor (dts,_))= |
|
251 (indt j ^"<ITEM status=\"correct\">\n"^ |
|
252 term2xml (j) (comp_dts' dts)^"\n"^ |
|
253 indt j ^"</ITEM>\n"):xml |
|
254 | itm_2xml j (Syn c) = |
|
255 indt j ^"<ITEM status=\"syntaxerror\">\n"^ |
|
256 indt (j) ^c^ |
|
257 indt j ^"</ITEM>\n" |
|
258 | itm_2xml j (Typ c) = |
|
259 indt j ^"<ITEM status=\"typeerror\">\n"^ |
|
260 indt (j) ^c^ |
|
261 indt j ^"</ITEM>\n" |
|
262 (*type item also has 'False of cterm' set in preconds2xml WN 050618*) |
|
263 | itm_2xml j (Inc (dts,_)) = |
|
264 indt j ^"<ITEM status=\"incomplete\">\n"^ |
|
265 term2xml (j) (comp_dts' dts)^"\n"^ |
|
266 indt j ^"</ITEM>\n" |
|
267 | itm_2xml j (Sup dts) = |
|
268 indt j ^"<ITEM status=\"superfluous\">\n"^ |
|
269 term2xml (j) (comp_dts' dts)^"\n"^ |
|
270 indt j ^"</ITEM>\n" |
|
271 | itm_2xml j (Mis (d,pid)) = |
|
272 indt j ^"<ITEM status=\"missing\">\n"^ |
|
273 term2xml (j) (d $ pid)^"\n"^ |
|
274 indt j ^"</ITEM>\n"; |
|
275 |
|
276 (*see terms2xml' fpr \n*) |
|
277 fun itms2xml _ [] = "" |
|
278 | itms2xml j [(_,_,_,_,itm_)] = itm_2xml j itm_ |
|
279 | itms2xml j (((_,_,_,_,itm_):itm)::itms) = |
|
280 itm_2xml j itm_ ^ itms2xml j itms; |
|
281 |
|
282 fun precond2xml j (true, term) = |
|
283 (indt j ^"<ITEM status=\"correct\">\n"^ |
|
284 term2xml (j) term^"\n"^ |
|
285 indt j ^"</ITEM>\n"):xml |
|
286 | precond2xml j (false, term) = |
|
287 indt j ^"<ITEM status=\"false\">\n"^ |
|
288 term2xml (j+i) term^"\n"^ |
|
289 indt j ^"</ITEM>\n"; |
|
290 |
|
291 fun preconds2xml _ [] = ("":xml) |
|
292 | preconds2xml j (p::ps) = precond2xml j p ^ preconds2xml j ps; |
|
293 |
|
294 (*FIXME.WN040831 model2xml <--?--> pattern2xml*) |
|
295 fun model2xml j (itms:itm list) where_ = |
|
296 let fun eq4 str (_,_,_,field,_) = str = field |
|
297 in (indt j ^"<MODEL>\n"^ |
|
298 (case filter (eq4 "#Given") itms of |
|
299 [] => (indt (j+i)) ^ "<GIVEN> </GIVEN>\n" |
|
300 | gis => (indt (j+i)) ^ "<GIVEN>\n" ^ itms2xml (j+2*i) gis ^ |
|
301 (indt (j+i)) ^ "</GIVEN>\n") |
|
302 ^ |
|
303 (case where_ of |
|
304 [] => (indt (j+i)) ^ "<WHERE> </WHERE>\n" |
|
305 | whs => (indt (j+i)) ^ "<WHERE>\n" ^ preconds2xml (j+2*i) whs ^ |
|
306 (indt (j+i)) ^ "</WHERE>\n") |
|
307 ^ |
|
308 (case filter (eq4 "#Find") itms of |
|
309 [] => (indt (j+i)) ^ "<FIND> </FIND>\n" |
|
310 | fis => (indt (j+i)) ^ "<FIND>\n" ^ itms2xml (j+2*i) fis ^ |
|
311 (indt (j+i)) ^ "</FIND>\n") |
|
312 ^ |
|
313 (case filter (eq4 "#Relate") itms of |
|
314 [] => (indt (j+i)) ^ "<RELATE> </RELATE>\n" |
|
315 | res => (indt (j+i)) ^ "<RELATE>\n" ^ itms2xml (j+2*i) res ^ |
|
316 (indt (j+i)) ^ "</RELATE>\n")^ |
|
317 indt j ^"</MODEL>\n"):xml |
|
318 end; |
|
319 (* writeln(model2xml 3 itms []); |
|
320 *) |
|
321 |
|
322 fun spec2xml j ((dI,pI,mI):spec) = |
|
323 (indt j ^"<SPECIFICATION>\n"^ |
|
324 indt (j+i) ^"<THEORYID> "^ dI ^" </THEORYID>\n"^ |
|
325 indt (j+i) ^"<PROBLEMID>\n"^ |
|
326 id2xml (j+2*i) pI ^ |
|
327 indt (j+i) ^"</PROBLEMID>\n"^ |
|
328 indt (j+i) ^"<METHODID>\n"^ |
|
329 id2xml (j+2*i) mI ^ |
|
330 indt (j+i) ^"</METHODID>\n"^ |
|
331 indt j ^"</SPECIFICATION>\n"):xml; |
|
332 |
|
333 fun modspec2xml j ((b, p_, head, gfr, pre, spec): ocalhd) = |
|
334 (indt j ^"<CALCHEAD status = "^ |
|
335 quote (if b then "correct" else "incorrect")^">\n"^ |
|
336 indt (j+i) ^"<HEAD>\n"^ |
|
337 term2xml (j+i) head^"\n"^ |
|
338 indt (j+i) ^"</HEAD>\n"^ |
|
339 model2xml (j+i) gfr pre ^ |
|
340 indt (j+i) ^"<BELONGSTO> "^(case p_ of Pbl => "Pbl" |
|
341 | Met => "Met" |
|
342 | _ => "Und")^" </BELONGSTO>\n"^ |
|
343 spec2xml (j+i) spec ^ |
|
344 indt j ^"</CALCHEAD>\n"):xml; |
|
345 (* writeln (modspec2xml 2 e_ocalhd); |
|
346 *) |
|
347 fun pos'calchead2xml j (p:pos', (b, p_, head, gfr, pre, spec): ocalhd) = |
|
348 (indt j ^"<CALCHEAD status = "^ |
|
349 quote (if b then "correct" else "incorrect")^">\n"^ |
|
350 pos'2xml (j+i) ("POSITION", p) ^ |
|
351 indt (j+i) ^"<HEAD>\n"^ |
|
352 term2xml (j+i) head^"\n"^ |
|
353 indt (j+i) ^"</HEAD>\n"^ |
|
354 model2xml (j+i) gfr pre ^ |
|
355 indt (j+i) ^"<BELONGSTO> "^(case p_ of Pbl => "Pbl" |
|
356 | Met => "Met" |
|
357 | _ => "Und")^" </BELONGSTO>\n"^ |
|
358 spec2xml (j+i) spec ^ |
|
359 indt j ^"</CALCHEAD>\n"):xml; |
|
360 |
|
361 fun sub2xml j (id, value) = |
|
362 (indt j ^"<PAIR>\n"^ |
|
363 indt j ^" <VARIABLE>\n"^ |
|
364 term2xml (j+i) id ^ "\n" ^ |
|
365 indt j ^" </VARIABLE>\n" ^ |
|
366 indt j ^" <VALUE>\n"^ |
|
367 term2xml (j+i) value ^ "\n" ^ |
|
368 indt j ^" </VALUE>\n" ^ |
|
369 indt j ^"</PAIR>\n"):xml; |
|
370 fun subs2xml j (subs:subs) = |
|
371 (indt j ^"<SUBSTITUTION>\n"^ |
|
372 foldl op^ ("", map (sub2xml (j+i)) |
|
373 (subs2subst (assoc_thy "Isac.thy") subs)) ^ |
|
374 indt j ^"</SUBSTITUTION>\n"):xml; |
|
375 (* val subs = [(str2term "bdv", str2term "x")]; |
|
376 val subs = ["(bdv, x)"]; |
|
377 writeln(subs2xml 0 subs); |
|
378 *) |
|
379 fun subst2xml j (subst:subst) = |
|
380 (indt j ^"<SUBSTITUTION>\n"^ |
|
381 foldl op^ ("", map (sub2xml (j+i)) subst) ^ |
|
382 indt j ^"</SUBSTITUTION>\n"):xml; |
|
383 (* val subst = [(str2term "bdv", str2term "x")]; |
|
384 writeln(subst2xml 0 subst); |
|
385 *) |
|
386 |
|
387 (* val (j, str) = ((j+i), form); |
|
388 *) |
|
389 fun thmstr2xml j str = ((((term2xml j) o str2term) str)^"\n"):xml; |
|
390 |
|
391 (* val (j, ((ID, form):thm')) = ((j+i), thm'); |
|
392 *) |
|
393 fun thm'2xml j ((ID, form):thm') = |
|
394 (indt j ^"<THEOREM>\n"^ |
|
395 indt (j+i) ^"<ID> "^ID^" </ID>\n"^ |
|
396 indt (j+i) ^"<FORMULA>\n"^ |
|
397 thmstr2xml (j+i) form^ |
|
398 indt (j+i) ^"</FORMULA>\n"^ |
|
399 indt j ^"</THEOREM>\n"):xml; |
|
400 |
|
401 (*WN060627 scope of thy's not considered ?!?*) |
|
402 fun thm''2xml j (thm:thm) = |
|
403 indt j ^"<THEOREM>\n"^ |
|
404 indt (j+i) ^"<ID> "^ (strip_thy o Thm.name_of_thm) thm ^" </ID>\n"^ |
|
405 term2xml j ((#prop o rep_thm) thm) ^ "\n" ^ |
|
406 indt j ^"</THEOREM>\n":xml; |
|
407 |
|
408 |
|
409 fun scr2xml j EmptyScr = |
|
410 indt j ^"<SCRIPT> </SCRIPT>\n" : xml |
|
411 | scr2xml j (Script term) = |
|
412 if term = e_term |
|
413 then indt j ^"<SCRIPT> </SCRIPT>\n" |
|
414 else indt j ^"<SCRIPT>\n"^ |
|
415 term2xml j (inst_abs (assoc_thy "Isac.thy") term) ^ "\n" ^ |
|
416 indt j ^"</SCRIPT>\n" |
|
417 | scr2xml j (Rfuns _) = |
|
418 indt j ^"<REVERSREWRITE> reverse rewrite functions </REVERSREWRITE>\n"; |
|
419 |
|
420 fun prepa12xml j (terms, term) = |
|
421 indt j ^"<PREPAT>\n"^ |
|
422 indt (j+i) ^"<PRECONDS>\n"^ |
|
423 terms2xml (j+2*i) terms ^ |
|
424 indt (j+i) ^"</PRECONDS>\n"^ |
|
425 indt (j+i) ^"<PATTERN>\n"^ |
|
426 term2xml (j+2*i) term ^ |
|
427 indt (j+i) ^"</PATTERN>\n"^ |
|
428 indt j ^"</PREPAT>\n" : xml; |
|
429 |
|
430 fun prepat2xml j [] = "" |
|
431 | prepat2xml j (p::ps) = prepa12xml j p ^ prepat2xml j ps : xml; |
|
432 |
|
433 (* val (j, (thyID, seqrls, {id, preconds, rew_ord=(ord,_), erls, |
|
434 srls, calc, rules, scr})) = |
|
435 (j, (thyID, "Seq", data)); |
|
436 *) |
|
437 fun rls2xm j (thyID, seqrls, {id, preconds, rew_ord=(ord,_), erls, |
|
438 srls, calc, rules, scr}) = |
|
439 indt j ^"<RULESET>\n"^ |
|
440 indt (j+i) ^"<ID> "^ id ^" </ID>\n"^ |
|
441 indt (j+i) ^"<TYPE> "^ seqrls ^" </TYPE>\n"^ |
|
442 indt (j+i) ^"<RULES>\n" ^ |
|
443 rules2xml (j+2*i) thyID rules ^ |
|
444 indt (j+i) ^"</RULES>\n" ^ |
|
445 indt (j+i) ^"<PRECONDS> " ^ |
|
446 terms2xml' (j+2*i) preconds ^ |
|
447 indt (j+i) ^"</PRECONDS>\n" ^ |
|
448 indt (j+i) ^"<ORDER>\n" ^ |
|
449 indt (j+2*i) ^ "<STRING> " ^ ord ^ " </STRING>\n" ^ |
|
450 (*WN060714 thy_isac_*-ord-*.xml not yet generated ................ |
|
451 indt (j+2*i) ^ "<GUH> " ^ ord2guh ("IsacKnowledge", |
|
452 thyID) ord ^ " </GUH>\n" ^ |
|
453 ..................................................................*) |
|
454 indt (j+i) ^"</ORDER>\n" ^ |
|
455 indt (j+i) ^"<ERLS>\n" ^ |
|
456 indt (j+2*i) ^ "<TAG> Ruleset </TAG>\n" ^ |
|
457 indt (j+2*i) ^ "<STRING> " ^ id_rls erls ^ " </STRING>\n" ^ |
|
458 indt (j+2*i) ^ "<GUH> " ^ rls2guh ("IsacKnowledge", thyID) |
|
459 (id_rls erls) ^ " </GUH>\n" ^ |
|
460 indt (j+i) ^"</ERLS>\n" ^ |
|
461 indt (j+i) ^"<SRLS>\n" ^ |
|
462 indt (j+2*i) ^ "<TAG> Ruleset </TAG>\n" ^ |
|
463 indt (j+2*i) ^ "<STRING> " ^ id_rls erls ^ " </STRING>\n" ^ |
|
464 indt (j+2*i) ^ "<GUH> " ^ rls2guh ("IsacKnowledge", thyID) |
|
465 (id_rls srls) ^ " </GUH>\n" ^ |
|
466 indt (j+i) ^"</SRLS>\n" ^ |
|
467 calcrefs2xml (j+i) (thyID, calc) ^ |
|
468 scr2xml (j+i) scr ^ |
|
469 indt j ^"</RULESET>\n" : xml; |
|
470 |
|
471 fun rls2xml j (thyID, Erls) = rls2xml j (thyID, e_rls) |
|
472 (* rls2xml j (thyID, Rls {id=id, preconds=preconds, rew_ord=(ord,e_rew_ord), |
|
473 erls=erls,srls=srls,calc=calc,rules=rules,scr=scr}); |
|
474 val (j, (thyID, Rls {id, preconds, rew_ord=(ord,_), erls, |
|
475 srls, calc, rules, scr})) = (i, thy_rls); |
|
476 val (j, (thyID, Seq data)) = (i, thy_rls); |
|
477 *) |
|
478 | rls2xml j (thyID, Rls data) = rls2xm j (thyID, "Rls", data) |
|
479 (* val (j, (thyID, Seq data)) = (i, thy_rls); |
|
480 *) |
|
481 | rls2xml j (thyID, Seq data) = rls2xm j (thyID, "Seq", data) |
|
482 | rls2xml j (thyID, Rrls {id, prepat, rew_ord=(ord,_), erls, calc, scr}) = |
|
483 indt j ^"<RULESET>\n"^ |
|
484 indt (j+i) ^"<ID> "^ id ^" </ID>\n"^ |
|
485 indt (j+i) ^"<TYPE> Rrls </TYPE>\n"^ |
|
486 prepat2xml (j+i) prepat ^ |
|
487 indt (j+i) ^"<ORDER> " ^ |
|
488 indt (j+2*i) ^ "<TAG> Rewrite order </TAG>\n" ^ |
|
489 indt (j+2*i) ^ "<STRING> " ^ ord ^ " </STRING>\n" ^ |
|
490 (*WN060714 thy_isac_*-ord-*.xml not yet generated ................ |
|
491 indt (j+2*i) ^ "<GUH> " ^ ord2guh ("IsacKnowledge", |
|
492 thyID) ord ^ " </GUH>\n" ^ |
|
493 .................................................................*) |
|
494 indt (j+i) ^"</ORDER>\n" ^ |
|
495 indt (j+i) ^"<ERLS> " ^ |
|
496 indt (j+2*i) ^ "<TAG> Ruleset </TAG>\n" ^ |
|
497 indt (j+2*i) ^ "<STRING> " ^ id_rls erls ^ " </STRING>\n" ^ |
|
498 indt (j+2*i) ^ "<GUH> " ^ rls2guh ("IsacKnowledge", thyID) |
|
499 (id_rls erls) ^ " </GUH>\n" ^ |
|
500 indt (j+i) ^"</ERLS>\n" ^ |
|
501 calcrefs2xml (j+i) (thyID, calc) ^ |
|
502 indt (j+i) ^"<SCRIPT>\n"^ |
|
503 scr2xml (j+2*i) scr ^ |
|
504 indt (j+i) ^" </SCRIPT>\n"^ |
|
505 indt j ^"</RULESET>\n" : xml; |
|
506 |
|
507 |
|
508 (*.convert a tactic into xml-format |
|
509 ATTENTION: WN060513 detected faulty 'cterm2xml's with 'string's as args.*) |
|
510 fun tac2xml j (Subproblem (dI, pI)) = |
|
511 (indt j ^"<SUBPROBLEMTACTIC name=\"Subproblem\">\n"^ |
|
512 indt (j+i) ^"<THEORY> "^ dI ^" </THEORY>\n"^ |
|
513 indt (j+i) ^"<PROBLEM>\n"^ |
|
514 id2xml (j+2*i) pI^ |
|
515 indt (j+i) ^"</PROBLEM>\n"^ |
|
516 indt j ^"</SUBPROBLEMTACTIC>\n"):xml |
|
517 | tac2xml j Model_Problem = |
|
518 (indt j ^"<STRINGLISTTACTIC name=\"Model_Problem\">"^ |
|
519 indt j ^"</STRINGLISTTACTIC>\n"):xml |
|
520 | tac2xml j (Refine_Tacitly pI) = |
|
521 (indt j ^"<STRINGLISTTACTIC name=\"Refine_Tacitly\">\n"^ |
|
522 id2xml (j+i) pI^ |
|
523 indt j ^"</STRINGLISTTACTIC>\n"):xml |
|
524 |
|
525 | tac2xml j (Add_Given ct) = |
|
526 (indt j ^"<SIMPLETACTIC name=\"Add_Given\">\n"^ |
|
527 cterm2xml (j+i) ct^ |
|
528 indt j ^"</SIMPLETACTIC>\n"):xml |
|
529 | tac2xml j (Add_Find ct) = |
|
530 (indt j ^"<SIMPLETACTIC name=\"Add_Find\">\n"^ |
|
531 cterm2xml (j+i) ct^ |
|
532 indt j ^"</SIMPLETACTIC>\n"):xml |
|
533 | tac2xml j (Add_Relation ct) = |
|
534 (indt j ^"<SIMPLETACTIC name=\"Add_Relation\">\n"^ |
|
535 cterm2xml (j+i) ct^ |
|
536 indt j ^"</SIMPLETACTIC>\n"):xml |
|
537 |
|
538 | tac2xml j (Specify_Theory ct) = |
|
539 (indt j ^"<SIMPLETACTIC name=\"Specify_Theory\">\n"^ |
|
540 cterm2xml (j+i) ct^(*WN060513 Specify_Theory = fn : domID -> tac |
|
541 and domID is a string, not a cterm *) |
|
542 indt j ^"</SIMPLETACTIC>\n"):xml |
|
543 | tac2xml j (Specify_Problem ct) = |
|
544 (indt j ^"<STRINGLISTTACTIC name=\"Specify_Problem\">\n"^ |
|
545 id2xml (j+i) ct^ |
|
546 indt j ^"</STRINGLISTTACTIC>\n"):xml |
|
547 | tac2xml j (Specify_Method ct) = |
|
548 (indt j ^"<STRINGLISTTACTIC name=\"Specify_Method\">\n"^ |
|
549 id2xml (j+i) ct^ |
|
550 indt j ^"</STRINGLISTTACTIC>\n"):xml |
|
551 | tac2xml j (Apply_Method mI) = |
|
552 (indt j ^"<STRINGLISTTACTIC name=\"Apply_Method\">\n"^ |
|
553 id2xml (j+i) mI^ |
|
554 indt j ^"</STRINGLISTTACTIC>\n"):xml |
|
555 |
|
556 | tac2xml j (Take ct) = |
|
557 (indt j ^"<SIMPLETACTIC name=\"Take\">\n"^ |
|
558 cterm2xml (j+i) ct^ |
|
559 indt j ^"</SIMPLETACTIC>\n"):xml |
|
560 | tac2xml j (Calculate opstr) = |
|
561 (indt j ^"<SIMPLETACTIC name=\"Calculate\">\n"^ |
|
562 cterm2xml (j+i) opstr^(*WN060513 Calculate = fn : string -> tac |
|
563 'string', _NOT_ 'cterm' ..flaw from RG*) |
|
564 indt j ^"</SIMPLETACTIC>\n"):xml |
|
565 (* val (j, Rewrite thm') = (i, tac); |
|
566 *) |
|
567 | tac2xml j (Rewrite thm') = |
|
568 (indt j ^"<REWRITETACTIC name=\"Rewrite\">\n"^ |
|
569 thm'2xml (j+i) thm'^ |
|
570 indt j ^"</REWRITETACTIC>\n"):xml |
|
571 (* writeln (tac2xml 2 (Rewrite ("all_left", |
|
572 "~ ?b =!= 0 ==> (?a = ?b) = (?a - ?b = 0)"))); |
|
573 val (j, (Rewrite_Inst (subs, thm'))) = (i, tac); |
|
574 *) |
|
575 | tac2xml j (Rewrite_Inst (subs, thm')) = |
|
576 (indt j ^"<REWRITEINSTTACTIC name=\"Rewrite_Inst\">\n"^ |
|
577 subs2xml (j+i) subs^ |
|
578 thm'2xml (j+i) thm'^ |
|
579 indt j ^"</REWRITEINSTTACTIC>\n"):xml |
|
580 (* writeln (tac2xml 2 (Rewrite_Inst |
|
581 (["(bdv,x)"], |
|
582 ("all_left", |
|
583 "~ ?b =!= 0 ==> (?a = ?b) = (?a - ?b = 0)")))); |
|
584 *) |
|
585 | tac2xml j (Rewrite_Set rls') = |
|
586 (indt j ^"<REWRITESETTACTIC name=\"Rewrite_Set\">\n"^ |
|
587 indt (j+i) ^"<RULESET> "^ rls' ^" </RULESET>\n"^ |
|
588 indt j ^"</REWRITESETTACTIC>\n"):xml |
|
589 | tac2xml j (Rewrite_Set_Inst (subs, rls')) = |
|
590 (indt j ^"<REWRITESETINSTTACTIC name=\"Rewrite_Set_Inst\">\n"^ |
|
591 indt (j+i) ^"<RULESET> "^ rls' ^" </RULESET>\n"^ |
|
592 subs2xml (j+i) subs^ |
|
593 indt j ^"</REWRITESETINSTTACTIC>\n"):xml |
|
594 |
|
595 | tac2xml j (Or_to_List) = |
|
596 (indt j ^"<STRINGLISTTACTIC name=\"Or_to_List\"> \ |
|
597 \</STRINGLISTTACTIC>\n"):xml |
|
598 | tac2xml j (Check_elementwise ct) = |
|
599 (indt j ^"<SIMPLETACTIC name=\"Check_elementwise\">\n"^ |
|
600 cterm2xml (j+i) ct ^ "\n"^ |
|
601 indt j ^"</SIMPLETACTIC>\n"):xml |
|
602 (*WN0605 quick and dirty: cterms is _NOT_ a stringlist like pblID...*) |
|
603 | tac2xml j (Substitute cterms) = |
|
604 (indt j ^"<STRINGLISTTACTIC name=\"Substitute\">\n"^ |
|
605 (*cterms2xml (j+i) cterms^ ....should be WN060514: TODO TERMLISTTACTIC?*) |
|
606 id2xml (j+i) cterms^ |
|
607 indt j ^"</STRINGLISTTACTIC>\n"):xml |
|
608 | tac2xml j (Check_Postcond pI) = |
|
609 (indt j ^"<STRINGLISTTACTIC name=\"Check_Postcond\">\n"^ |
|
610 id2xml (j+i) pI^ |
|
611 indt j ^"</STRINGLISTTACTIC>\n"):xml |
|
612 |
|
613 | tac2xml j tac = raise error ("tac2xml: not impl. for "^tac2str tac); |
|
614 |
|
615 fun tacs2xml j [] = "":xml |
|
616 | tacs2xml j (t::ts) = tac2xml j t ^ tacs2xml j ts; |
|
617 |
|
618 |
|
619 fun posformhead2xml j (p:pos', Form f) = |
|
620 indt j ^"<CALCFORMULA>\n"^ |
|
621 pos'2xml (j+i) ("POSITION", p) ^ |
|
622 indt (j+i) ^"<FORMULA>\n"^ |
|
623 term2xml (j+i) f^"\n"^ |
|
624 indt (j+i) ^"</FORMULA>\n"^ |
|
625 indt j ^"</CALCFORMULA>\n" |
|
626 | posformhead2xml j (p, ModSpec c) = |
|
627 pos'calchead2xml (j) (p, c); |
|
628 |
|
629 fun posformheads2xml j [] = ("":xml) |
|
630 | posformheads2xml j (r::rs) = posformhead2xml j r ^ posformheads2xml j rs; |
|
631 |
|
632 val e_pblterm = (term_of o the o (parse (assoc_thy "Script.thy"))) |
|
633 ("Problem (" ^ e_domID ^ "," ^ strs2str' e_pblID ^ ")"); |
|
634 |
|
635 (*WN051224 minimal adaption to exporting Formulae _only_ by getFormulaeFromTo*) |
|
636 fun posterm2xml j (p:pos', t) = |
|
637 indt j ^"<CALCFORMULA>\n"^ |
|
638 pos'2xml (j+i) ("POSITION", p) ^ |
|
639 indt (j+i) ^"<FORMULA>\n"^ |
|
640 (if t = e_pblterm (*headline in pbl is e_ <- _root_pbl for CAS-command*) |
|
641 then cterm2xml (j+i) "________________________________________________" |
|
642 else term2xml (j+i) t)^"\n" ^ |
|
643 indt (j+i) ^"</FORMULA>\n"^ |
|
644 indt j ^"</CALCFORMULA>\n"; |
|
645 |
|
646 fun posterms2xml j [] = ("":xml) |
|
647 | posterms2xml j (r::rs) = posterm2xml j r ^ posterms2xml j rs; |
|
648 |
|
649 fun asm_val2xml j (asm, vl) = |
|
650 indt j ^ "<ASMEVALUATED>\n" ^ |
|
651 indt (j+i) ^ "<ASM>\n" ^ |
|
652 term2xml (j+i) asm ^ "\n" ^ |
|
653 indt (j+i) ^ "</ASM>\n" ^ |
|
654 indt (j+i) ^ "<VALUE>\n" ^ |
|
655 term2xml (j+i) vl ^ "\n" ^ |
|
656 indt (j+i) ^ "</VALUE>\n" ^ |
|
657 indt j ^ "</ASMEVALUATED>\n" : xml; |
|
658 |
|
659 fun asm_vals2xml j [] = ("":xml) |
|
660 | asm_vals2xml j (asm_val::avs) = asm_val2xml j asm_val ^ |
|
661 asm_vals2xml j avs; |
|
662 |
|
663 (*.a reference to an element in the theory hierarchy; |
|
664 compare 'fun keref2xml'.*) |
|
665 (* val (j, thyID, typ, xstring) = |
|
666 (i+i, snd (thy_containing_rls thy' prls'), "Rulesets", prls'); |
|
667 *) |
|
668 fun theref2xml j (thyID:thyID) typ (xstring:xstring) = |
|
669 let val guh = theID2guh ["IsacKnowledge", thyID, typ, xstring] |
|
670 val typ' = (implode o (drop_last_n 1) o explode) typ |
|
671 in indt j ^ "<KESTOREREF>\n" ^ |
|
672 indt (j+i) ^ "<TAG> " ^ typ' ^ " </TAG>\n" ^ |
|
673 indt (j+i) ^ "<ID> " ^ xstring ^ " </ID>\n" ^ |
|
674 indt (j+i) ^ "<GUH> " ^ guh ^ " </GUH>\n" ^ |
|
675 indt j ^ "</KESTOREREF>\n" : xml |
|
676 end; |
|
677 |
|
678 (*.a reference to an element in the kestore EXCEPT theory hierarchy; |
|
679 compare 'fun theref2xml'.*) |
|
680 (* val (j, typ, kestoreID) = (i+i, Met_, hd met); |
|
681 *) |
|
682 fun keref2xml j typ (kestoreID:kestoreID) = |
|
683 let val id = strs2str' kestoreID |
|
684 val guh = kestoreID2guh typ kestoreID |
|
685 in indt j ^ "<KESTOREREF>\n" ^ |
|
686 indt (j+i) ^ "<TAG> " ^ ketype2str' typ ^ "</TAG>\n" ^ |
|
687 indt (j+i) ^ "<ID> " ^ id ^ " </ID>\n" ^ |
|
688 indt (j+i) ^ "<GUH> " ^ guh ^ " </GUH>\n" ^ |
|
689 indt j ^ "</KESTOREREF>\n" : xml |
|
690 end; |
|
691 |
|
692 (*url to a source external to isac*) |
|
693 fun extref2xml j linktext url = |
|
694 indt j ^ "<EXTREF>\n" ^ |
|
695 indt (j+i) ^ "<TEXT> " ^ linktext ^ " </TEXT>\n" ^ |
|
696 indt (j+i) ^ "<URL> " ^ url ^ " </URL>\n" ^ |
|
697 indt j ^ "</EXTREF>\n" : xml; |
|
698 |
|
699 |
|
700 (* val (ContThmInst{thyID, thm, bdvs, thminst, applto, applat, reword, |
|
701 asms, lhs, rhs, result, resasms, asmrls}) = |
|
702 (context_thy (pt,pos) tac); |
|
703 writeln (contthy2xml 2 (context_thy (pt,pos) tac)); |
|
704 *) |
|
705 fun contthy2xml j EContThy = |
|
706 raise error "contthy2xml called with EContThy" |
|
707 | contthy2xml j (ContThm {thyID, thm, applto, applat, reword, |
|
708 asms,lhs, rhs, result, resasms, asmrls}) = |
|
709 indt j ^ "<GUH> " ^ thm ^ " </GUH>\n" ^ |
|
710 indt j ^ "<APPLTO>\n" ^ |
|
711 term2xml j applto ^ "\n" ^ |
|
712 indt j ^ "</APPLTO>\n" ^ |
|
713 indt j ^ "<APPLAT>\n" ^ |
|
714 term2xml j applat ^ "\n" ^ |
|
715 indt j ^ "</APPLAT>\n" ^ |
|
716 indt j ^ "<ORDER>\n" ^ (*should be a theref2xml*) |
|
717 indt (j+i) ^"<ID> " ^ reword ^ " </ID>\n" ^ |
|
718 indt j ^ "</ORDER>\n" ^ |
|
719 indt j ^ "<ASMSEVAL>\n" ^ |
|
720 asm_vals2xml (j+i) asms ^ |
|
721 indt j ^ "</ASMSEVAL>\n" ^ |
|
722 indt j ^ "<LHS>\n" ^ |
|
723 term2xml j (fst lhs) ^ "\n" ^ |
|
724 indt j ^ "</LHS>\n" ^ |
|
725 indt j ^ "<LHSINST>\n" ^ |
|
726 term2xml j (snd lhs) ^ "\n" ^ |
|
727 indt j ^ "</LHSINST>\n" ^ |
|
728 indt j ^ "<RHS>\n" ^ |
|
729 term2xml j (fst rhs) ^ "\n" ^ |
|
730 indt j ^ "</RHS>\n" ^ |
|
731 indt j ^ "<RHSINST>\n" ^ |
|
732 term2xml j (snd rhs) ^ "\n" ^ |
|
733 indt j ^ "</RHSINST>\n" ^ |
|
734 indt j ^ "<RESULT>\n" ^ |
|
735 term2xml j result ^ "\n" ^ |
|
736 indt j ^ "</RESULT>\n" ^ |
|
737 indt j ^ "<ASSUMPTIONS>\n" ^ |
|
738 terms2xml' j resasms ^ |
|
739 indt j ^ "</ASSUMPTIONS>\n" ^ |
|
740 indt j ^ "<EVALRLS>\n" ^ |
|
741 theref2xml j thyID "Rulesets" asmrls ^ |
|
742 indt j ^ "</EVALRLS>\n" |
|
743 |
|
744 | contthy2xml j (ContThmInst{thyID, thm, bdvs, thminst, applto, applat, |
|
745 reword, asms, lhs, rhs, result, resasms, |
|
746 asmrls}) = |
|
747 indt j ^ "<GUH> " ^ thm ^ " </GUH>\n" ^ |
|
748 indt j ^ "<SUBSLIST>\n" ^ (*should be an environment = substitution*) |
|
749 indt (j+i) ^ "<MATHML>\n" ^ |
|
750 indt (j+2*i) ^ "<ISA> " ^ subst2str' bdvs ^ " </ISA>\n" ^ |
|
751 indt (j+i) ^ "</MATHML>\n" ^ |
|
752 indt j ^ "</SUBSLIST>\n" ^ |
|
753 indt j ^ "<INSTANTIATED>\n" ^ |
|
754 term2xml j thminst ^ "\n" ^ |
|
755 indt j ^ "</INSTANTIATED>\n" ^ |
|
756 indt j ^ "<APPLTO>\n" ^ |
|
757 term2xml j applto ^ "\n" ^ |
|
758 indt j ^ "</APPLTO>\n" ^ |
|
759 indt j ^ "<APPLAT>\n" ^ |
|
760 term2xml j applat ^ "\n" ^ |
|
761 indt j ^ "</APPLAT>\n" ^ |
|
762 indt j ^ "<ORDER>\n" ^ (*should be a theref2xml*) |
|
763 indt (j+i) ^"<ID> " ^ reword ^ " </ID>\n" ^ |
|
764 indt j ^ "</ORDER>\n" ^ |
|
765 indt j ^ "<ASMSEVAL>\n" ^ |
|
766 asm_vals2xml (j+i) asms ^ |
|
767 indt j ^ "</ASMSEVAL>\n" ^ |
|
768 indt j ^ "<LHS>\n" ^ |
|
769 term2xml j (fst lhs) ^ "\n" ^ |
|
770 indt j ^ "</LHS>\n" ^ |
|
771 indt j ^ "<LHSINST>\n" ^ |
|
772 term2xml j (snd lhs) ^ "\n" ^ |
|
773 indt j ^ "</LHSINST>\n" ^ |
|
774 indt j ^ "<RHS>\n" ^ |
|
775 term2xml j (fst rhs) ^ "\n" ^ |
|
776 indt j ^ "</RHS>\n" ^ |
|
777 indt j ^ "<RHSINST>\n" ^ |
|
778 term2xml j (snd rhs) ^ "\n" ^ |
|
779 indt j ^ "</RHSINST>\n" ^ |
|
780 indt j ^ "<RESULT>\n" ^ |
|
781 term2xml j result ^ "\n" ^ |
|
782 indt j ^ "</RESULT>\n" ^ |
|
783 indt j ^ "<ASSUMPTOIONS>\n" ^ |
|
784 terms2xml' j resasms ^ |
|
785 indt j ^ "</ASSUMPTOIONS>\n" ^ |
|
786 indt j ^ "<EVALRLS>\n" ^ |
|
787 theref2xml j thyID "Rulesets" asmrls ^ |
|
788 indt j ^ "</EVALRLS>\n" |
|
789 |
|
790 | contthy2xml j (ContRls {thyID, rls, applto, result, asms}) = |
|
791 indt j ^ "<GUH> " ^ rls ^ " </GUH>\n" ^ |
|
792 indt j ^ "<APPLTO>\n" ^ |
|
793 term2xml j applto ^ "\n" ^ |
|
794 indt j ^ "</APPLTO>\n" ^ |
|
795 indt j ^ "<RESULT>\n" ^ |
|
796 term2xml j result ^ "\n" ^ |
|
797 indt j ^ "</RESULT>\n" ^ |
|
798 indt j ^ "<ASSUMPTOIONS>\n" ^ |
|
799 terms2xml' j asms ^ |
|
800 indt j ^ "</ASSUMPTOIONS>\n" |
|
801 |
|
802 | contthy2xml j (ContRlsInst {thyID, rls, bdvs, applto, result, asms}) = |
|
803 indt j ^ "<GUH> " ^ rls ^ " </GUH>\n" ^ |
|
804 indt j ^ "<SUBSLIST>\n" ^ (*should be an environment = substitution*) |
|
805 indt (j+i) ^ "<MATHML>\n" ^ |
|
806 indt (j+2*i) ^ "<ISA> " ^ subst2str' bdvs ^ " </ISA>\n" ^ |
|
807 indt (j+i) ^ "</MATHML>\n" ^ |
|
808 indt j ^ "</SUBSLIST>\n" ^ |
|
809 indt j ^ "<APPLTO>\n" ^ |
|
810 term2xml j applto ^ "\n" ^ |
|
811 indt j ^ "</APPLTO>\n" ^ |
|
812 indt j ^ "<RESULT>\n" ^ |
|
813 term2xml j result ^ "\n" ^ |
|
814 indt j ^ "</RESULT>\n" ^ |
|
815 indt j ^ "<ASSUMPTOIONS>\n" ^ |
|
816 terms2xml' j asms ^ |
|
817 indt j ^ "</ASSUMPTOIONS>\n" |
|
818 |
|
819 | contthy2xml j (ContNOrew {thyID, thm_rls, applto}) = |
|
820 indt j ^ "<GUH> " ^ thm_rls ^ " </GUH>\n" ^ |
|
821 indt j ^ "<APPLTO>\n" ^ |
|
822 term2xml j applto ^ "\n" ^ |
|
823 indt j ^ "</APPLTO>\n" |
|
824 |
|
825 | contthy2xml j (ContNOrewInst{thyID, thm_rls, bdvs, thminst, applto}) = |
|
826 indt j ^ "<GUH> " ^ thm_rls ^ " </GUH>\n" ^ |
|
827 indt j ^ "<SUBSLIST>\n" ^ (*should be an environment = substitution*) |
|
828 indt (j+i) ^ "<MATHML>\n" ^ |
|
829 indt (j+2*i) ^ "<ISA> " ^ subst2str' bdvs ^ " </ISA>\n" ^ |
|
830 indt (j+i) ^ "</MATHML>\n" ^ |
|
831 indt j ^ "</SUBSLIST>\n" ^ |
|
832 indt j ^ "<INSTANTIATED>\n" ^ |
|
833 term2xml j thminst ^ "\n" ^ |
|
834 indt j ^ "</INSTANTIATED>\n" ^ |
|
835 indt j ^ "<APPLTO>\n" ^ |
|
836 term2xml j applto ^ "\n" ^ |
|
837 indt j ^ "</APPLTO>\n" : xml; |
|
838 |
|
839 |
|
840 (*------------------------------------------------------------------*) |
|
841 end |
|
842 open datatypes; |
|
843 (*------------------------------------------------------------------*) |