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