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 ------------------------------------------------------------------*)
73 fun indent i = fold (curry op ^) (replicate i ". ") ""
75 fun xmlstr i (XML.Text str) = indent i ^ str ^ "\n"
76 | xmlstr i (XML.Elem ((str, []), trees)) =
77 indent i ^ "<" ^ str ^ ">" ^ "\n" ^
78 List.foldr op ^ "" (map (xmlstr (i + 1)) trees) ^
79 indent i ^ "</" ^ str ^ ">" ^ "\n"
80 | xmlstr i (XML.Elem ((str, [("status", a)]), trees)) =
81 indent i ^ "<" ^ str ^ " status " ^ a ^ ">" ^ "\n" ^
82 List.foldr op ^ "" (map (xmlstr (i + 1)) trees) ^
83 indent i ^ "</" ^ str ^ ">" ^ "\n"
84 | xmlstr _ (XML.Elem ((_, (_ :: _)), _)) =
85 error "xmlstr: TODO review attribute \"status\" etc";
88 (** general types: lists, **)
90 fun xml_of_bool b = XML.Elem (("BOOL", []), [XML.Text (bool2str b)])
91 fun xml_to_bool (XML.Elem (("BOOL", []), [XML.Text b])) = string_to_bool b
92 | xml_to_bool tree = error ("xml_to_int: wrong XML.tree " ^ xmlstr 0 tree)
94 (*.handles string list like 'fun id2xml'.*)
95 fun authors2xml j str auts =
96 let fun autx _ [] = ""
97 | autx j (s::ss) = (indt j) ^ "<STRING> " ^ s ^ " </STRING>\n" ^
99 in indt j ^ "<"^str^">\n" ^
101 indt j ^ "</"^str^">\n" : xml
103 (* writeln(authors2xml 2 "MATHAUTHORS" []);
104 writeln(authors2xml 2 "MATHAUTHORS"
105 ["isac-team 2001", "Richard Lang 2003"]);
109 let fun id2x _ [] = ""
110 | id2x j (s::ss) = (indt j) ^ "<STRING> " ^ s ^ " </STRING>\n" ^
112 in (indt j) ^ "<STRINGLIST>\n" ^
113 (id2x (j + indentation) ids) ^
114 (indt j) ^ "</STRINGLIST>\n" end;
115 (* writeln(id2xml 8 ["linear","univariate","equation"]);
117 <STRING>linear</STRING>
118 <STRING>univariate</STRING>
119 <STRING>equation</STRING>
122 fun xml_of_str str = XML.Elem (("STRING", []), [XML.Text str])
123 fun xml_of_strs strs = XML.Elem (("STRINGLIST", []), map xml_of_str strs)
125 fun xml_to_str (XML.Elem (("STRING", []), [XML.Text str])) = str
126 | xml_to_str tree = error ("xml_to_str: wrong XML.tree " ^ xmlstr 0 tree)
127 fun xml_to_strs (XML.Elem (("STRINGLIST", []), strs)) = map xml_to_str strs
128 | xml_to_strs tree = error ("xml_to_strs: wrong XML.tree " ^ xmlstr 0 tree)
131 let fun int2x _ [] = ""
132 | int2x j (s::ss) = (indt j) ^"<INT> "^ string_of_int s ^" </INT>\n"^
134 in (indt j) ^ "<INTLIST>\n" ^
135 (int2x (j + i) ids) ^
136 (indt j) ^ "</INTLIST>\n" end;
137 (* writeln(ints2xml 3 [1,2,3]);
139 fun xml_of_int i = XML.Elem (("INT", []), [XML.Text (string_of_int i)])
140 fun xml_of_ints is = (*xml/datatypes.sml: fun ints2xml*)
141 XML.Elem (("INTLIST", []), map xml_of_int is)
143 fun xml_to_int (XML.Elem (("INT", []), [XML.Text i])) =
144 (case int_of_str i of SOME i => i | _ => error "xml_to_int: int_of_str \<Rightarrow> NONE")
145 | xml_to_int tree = error ("xml_to_int: wrong XML.tree " ^ xmlstr 0 tree)
146 fun xml_to_ints (XML.Elem (("INTLIST", []), is)) = map xml_to_int is
147 | xml_to_ints tree = error ("xml_to_ints: wrong XML.tree " ^ xmlstr 0 tree)
150 (** isac datatypes **)
152 fun pos_2xml j pos_ =
153 (indt j) ^ "<POS> " ^ pos_2str pos_ ^ " </POS>\n";
155 (*.due to specialties of isac/util/parser/XMLParseDigest.java
156 pos' requires different tags.*)
157 fun pos'2xml j (tag, (pos, pos_)) =
158 indt (j) ^ "<" ^ tag ^ ">\n" ^
160 pos_2xml (j+i) pos_ ^
161 indt (j) ^ "</" ^ tag ^ ">\n";
162 (* writeln(pos'2xml 3 ("POSITION", ([1,2,3], Pbl)));
164 fun xml_of_pos tag (is, pp) = (*xml/datatypes.sml: fun pos'2xml*)
165 XML.Elem ((tag, []), [
167 XML.Elem (("POS", []), [XML.Text (pos_2str pp)])])
169 fun xml_to_pos_ (XML.Elem (("POS", []), [XML.Text pp])) = str2pos_ pp
170 | xml_to_pos_ tree = error ("xml_to_pos_: wrong XML.tree " ^ xmlstr 0 tree)
171 fun xml_to_pos (XML.Elem (("POSITION", []), [is, pp])) = (xml_to_ints is, xml_to_pos_ pp) (*: pos'*)
172 | xml_to_pos tree = error ("xml_to_pos: wrong XML.tree " ^ xmlstr 0 tree)
174 fun xml_of_auto (Step i) =
175 XML.Elem (("AUTO", []), [XML.Text "Step", XML.Text (string_of_int i)])
176 | xml_of_auto CompleteModel = XML.Elem (("AUTO", []), [XML.Text "CompleteModel"])
177 | xml_of_auto CompleteCalcHead = XML.Elem (("AUTO", []), [XML.Text "CompleteCalcHead"])
178 | xml_of_auto CompleteToSubpbl = XML.Elem (("AUTO", []), [XML.Text "CompleteToSubpbl"])
179 | xml_of_auto CompleteSubpbl = XML.Elem (("AUTO", []), [XML.Text "CompleteSubpbl"])
180 | xml_of_auto CompleteCalc = XML.Elem (("AUTO", []), [XML.Text "CompleteCalc"])
181 fun xml_to_auto (XML.Elem (("AUTO", []), [XML.Text "Step", XML.Text i])) = Step (int_of_str i |>the)
182 | xml_to_auto (XML.Elem (("AUTO", []), [XML.Text "CompleteModel"])) = CompleteModel
183 | xml_to_auto (XML.Elem (("AUTO", []), [XML.Text "CompleteCalcHead"])) = CompleteCalcHead
184 | xml_to_auto (XML.Elem (("AUTO", []), [XML.Text "CompleteToSubpbl"])) = CompleteToSubpbl
185 | xml_to_auto (XML.Elem (("AUTO", []), [XML.Text "CompleteSubpbl"])) = CompleteSubpbl
186 | xml_to_auto (XML.Elem (("AUTO", []), [XML.Text "CompleteCalc"])) = CompleteCalc
187 | xml_to_auto tree = error ("xml_to_auto: wrong XML.tree " ^ xmlstr 0 tree)
189 fun formula2xml j term = (*TODO.WN050211: use for _all_ <FORMULA>*)
190 indt j ^ "<FORMULA>\n"^
191 term2xml j term ^"\n"^
192 indt j ^ "</FORMULA>\n" : xml;
193 fun xml_of_formula term =
194 XML.Elem (("FORMULA", []), [
195 XML.Elem (("CALCID", []), [xml_of_term term])])
197 fun formulae2xml j [] = ("":xml)
198 | formulae2xml j (r::rs) = formula2xml j r ^ formulae2xml j rs;
199 (* writeln(formulae2xml 6 [str2term "1+1=2", str2term "1+1+1=3"]);
202 (*WN0502 @see ME/ctree: type asms: illdesigned, thus not used*)
203 fun posform2xml j (p:pos', term) =
204 indt j ^ "<POSFORM>\n" ^
205 pos'2xml (j+i) ("POSITION", p) ^
206 indt (j+i) ^ "<FORMULA>\n"^
207 term2xml (j+i) term ^"\n"^
208 indt (j+i) ^ "</FORMULA>\n"^
209 indt j ^ "</POSFORM>\n" : xml;
210 (* writeln(posform2xml 6 (([1,2],Frm), str2term "1+1=2"));
212 fun posforms2xml j [] = ("":xml)
213 | posforms2xml j (r::rs) = posform2xml j r ^ posforms2xml j rs;
214 (* writeln(posforms2xml 6 [(([1],Res), str2term "1+1=2"),(([2],Res), str2term "1+1+1=3")]);
217 fun calcref2xml j (thyID:thyID, (scrop, (rewop, _)):calc) =
218 indt j ^ "<CALCREF>\n" ^
219 indt (j+i) ^ "<STRING> " ^ scrop ^ "</STRING>\n" ^
220 indt (j+i) ^ "<GUH> " ^ cal2guh ("IsacKnowledge",
221 thyID) scrop ^ " </GUH>\n" ^
222 indt j ^ "</CALCREF>\n" : xml;
223 fun calcrefs2xml _ (_,[]) = "":xml
224 | calcrefs2xml j (thyID, cal::cs) =
225 calcref2xml j (thyID, cal) ^ calcrefs2xml j (thyID, cs);
227 fun calc2xml j (thyID:thyID, (scrop, (rewop, _)):calc) =
228 indt j ^ "<CALC>\n" ^
229 indt (j+i) ^ "<STRING>\n" ^ scrop ^ "</STRING>\n" ^
230 indt (j+i) ^ "<GUH>\n" ^ cal2guh ("IsacKnowledge",
231 thyID) scrop ^ "</GUH>\n" ^
232 indt (j+i) ^ "<TERMOP>\n" ^ rewop ^ "</TERMOP>\n" ^
233 indt j ^ "</CALC>\n" : xml;
235 (*.for creating a href for a rule within an rls's rule list;
236 the guh points to the thy of definition of the rule, NOT of use in rls.*)
237 fun rule2xml j (thyID:thyID) Erule =
238 error "rule2xml called with 'Erule'"
239 | rule2xml j thyID (Thm (thmDeriv, thm)) =
240 indt j ^ "<RULE>\n" ^
241 indt (j+i) ^ "<TAG> Theorem </TAG>\n" ^
242 indt (j+i) ^ "<STRING> " ^ thmID_of_derivation_name thmDeriv ^ " </STRING>\n" ^
243 indt (j+i) ^ "<GUH> " ^
244 thm2guh (thy_containing_thm thmDeriv) (thmID_of_derivation_name thmDeriv) ^ " </GUH>\n" ^
245 indt j ^ "</RULE>\n" : xml
246 | rule2xml j thyID (Calc (termop, _)) = ""
247 (*FIXXXXXXXME.WN060714 in rls make Calc : calc -> rule [add scriptop!]
248 see smltest/../datatypes.sml !
249 indt j ^ "<RULE>\n" ^
250 indt (j+i) ^ "<STRING> " ^ termop ^ " </STRING>\n" ^
251 indt (j+i) ^ "<GUH> " ^ cal2guh (thy_containing_cal thyID termop)
252 termop ^ " </GUH>\n" ^
255 | rule2xml j thyID (Cal1 (termop, _)) = ""
256 | rule2xml j thyID (Rls_ rls) =
257 let val rls' = (#id o rep_rls) rls
259 indt j ^ "<RULE>\n" ^
260 indt (j+i) ^ "<TAG> Ruleset </TAG>\n" ^
261 indt (j+i) ^ "<STRING> " ^ rls' ^ " </STRING>\n" ^
262 indt (j+i) ^ "<GUH> " ^ rls2guh (thy_containing_rls thyID rls') rls' ^ " </GUH>\n" ^
266 fun rules2xml j thyID [] = ("":xml)
267 | rules2xml j thyID (r::rs) = rule2xml j thyID r ^ rules2xml j thyID rs;
271 | filt ((s, (t1, t2)) :: ps) =
272 if str = s then (t1 $ t2) :: filt ps else filt ps
275 (*FIXME.WN040831 model2xml <--?--> pattern2xml*)
276 (*WN.25.8.03: pattern2xml different output with TextIO | writeln !!!
277 the version below is for TextIO: terms2xml makes \n !*)
278 (* val (j, p, where_) = (i, ppc, where_);
280 fun pattern2xml j p where_ =
281 (case filterpbl "#Given" p of
282 [] => (indt j) ^ "<GIVEN> </GIVEN>\n"
283 (* val gis = filterpbl "#Given" p;
285 | gis => (indt j) ^ "<GIVEN>\n" ^ terms2xml' j gis ^
286 (indt j) ^ "</GIVEN>\n")
289 [] => (indt j) ^ "<WHERE> </WHERE>\n"
290 | whs => (indt j) ^ "<WHERE>\n" ^ terms2xml' j whs ^
291 (indt j) ^ "</WHERE>\n")
293 (case filterpbl "#Find" p of
294 [] => (indt j) ^ "<FIND> </FIND>\n"
295 | fis => (indt j) ^ "<FIND>\n" ^ terms2xml' j fis ^
296 (indt j) ^ "</FIND>\n")
298 (case filterpbl "#Relate" p of
299 [] => (indt j) ^ "<RELATE> </RELATE>\n"
300 | res => (indt j) ^ "<RELATE>\n" ^ terms2xml' j res ^
301 (indt j) ^ "</RELATE>\n");
303 writeln(pattern2xml 3 ((#ppc o get_pbt)
304 ["squareroot","univariate","equation","test"]) []);
308 fun itm_2xml j (Cor (dts,_)) =
309 (indt j ^"<ITEM status=\"correct\">\n"^
310 term2xml (j) (comp_dts' dts)^"\n"^
311 indt j ^"</ITEM>\n"):xml
312 | itm_2xml j (Syn c) =
313 indt j ^"<ITEM status=\"syntaxerror\">\n"^
316 | itm_2xml j (Typ c) =
317 indt j ^"<ITEM status=\"typeerror\">\n"^
320 (*type item also has 'False of cterm' set in preconds2xml WN 050618*)
321 | itm_2xml j (Inc (dts,_)) =
322 indt j ^"<ITEM status=\"incomplete\">\n"^
323 term2xml (j) (comp_dts' dts)^"\n"^
325 | itm_2xml j (Sup dts) =
326 indt j ^"<ITEM status=\"superfluous\">\n"^
327 term2xml (j) (comp_dts' dts)^"\n"^
329 | itm_2xml j (Mis (d,pid)) =
330 indt j ^"<ITEM status=\"missing\">\n"^
331 term2xml (j) (d $ pid)^"\n"^
333 fun xml_of_itm_ (Cor (dts, _)) =
334 XML.Elem (("ITEM", [("status", "correct")]), [xml_of_term (comp_dts' dts)])
335 | xml_of_itm_ (Syn c) =
336 XML.Elem (("ITEM", [("status", "syntaxerror")]), [XML.Text c])
337 | xml_of_itm_ (Typ c) =
338 XML.Elem (("ITEM", [("status", "typeerror")]), [XML.Text c])
339 (*type item also has 'False of cterm' set in preconds2xml WN 050618*)
340 | xml_of_itm_ (Inc (dts, _)) =
341 XML.Elem (("ITEM", [("status", "incomplete")]), [xml_of_term (comp_dts' dts)])
342 | xml_of_itm_ (Sup dts) =
343 XML.Elem (("ITEM", [("status", "superfluous")]), [xml_of_term (comp_dts' dts)])
344 | xml_of_itm_ (Mis (d, pid)) =
345 XML.Elem (("ITEM", [("status", "missing")]), [xml_of_term (d $ pid)])
347 (*see terms2xml' fpr \n*)
348 fun itms2xml _ [] = ""
349 | itms2xml j [(_,_,_,_,itm_)] = itm_2xml j itm_
350 | itms2xml j (((_,_,_,_,itm_):itm)::itms) =
351 itm_2xml j itm_ ^ itms2xml j itms;
352 fun xml_of_itms itms =
354 fun extract (_, _, _, _, itm_) = itm_
355 | extract _ = error "xml_of_itms.extract: wrong argument"
356 in map (xml_of_itm_ o extract) itms end
358 fun precond2xml j (true, term) =
359 (indt j ^"<ITEM status=\"correct\">\n"^
360 term2xml (j) term^"\n"^
361 indt j ^"</ITEM>\n"):xml
362 | precond2xml j (false, term) =
363 indt j ^"<ITEM status=\"false\">\n"^
364 term2xml (j+i) term^"\n"^
366 fun xml_of_precond (status, term) =
367 XML.Elem (("ITEM", [("status", if status then "correct" else "false")]), [xml_of_term term])
369 fun preconds2xml _ [] = ("":xml)
370 | preconds2xml j (p::ps) = precond2xml j p ^ preconds2xml j ps;
371 fun xml_of_preconds ps = map xml_of_precond ps
373 (*FIXME.WN040831 model2xml <--?--> pattern2xml*)
374 fun model2xml j (itms:itm list) where_ =
375 let fun eq4 str (_,_,_,field,_) = str = field
376 in (indt j ^"<MODEL>\n"^
377 (case filter (eq4 "#Given") itms of
378 [] => (indt (j+i)) ^ "<GIVEN> </GIVEN>\n"
379 | gis => (indt (j+i)) ^ "<GIVEN>\n" ^ itms2xml (j+2*i) gis ^
380 (indt (j+i)) ^ "</GIVEN>\n")
383 [] => (indt (j+i)) ^ "<WHERE> </WHERE>\n"
384 | whs => (indt (j+i)) ^ "<WHERE>\n" ^ preconds2xml (j+2*i) whs ^
385 (indt (j+i)) ^ "</WHERE>\n")
387 (case filter (eq4 "#Find") itms of
388 [] => (indt (j+i)) ^ "<FIND> </FIND>\n"
389 | fis => (indt (j+i)) ^ "<FIND>\n" ^ itms2xml (j+2*i) fis ^
390 (indt (j+i)) ^ "</FIND>\n")
392 (case filter (eq4 "#Relate") itms of
393 [] => (indt (j+i)) ^ "<RELATE> </RELATE>\n"
394 | res => (indt (j+i)) ^ "<RELATE>\n" ^ itms2xml (j+2*i) res ^
395 (indt (j+i)) ^ "</RELATE>\n")^
396 indt j ^"</MODEL>\n"):xml
398 (* writeln(model2xml 3 itms []);
400 fun xml_of_model itms where_ =
402 fun eq str (_, _, _,field, _) = str = field
404 XML.Elem (("MODEL", []), [
405 XML.Elem (("GIVEN", []),
406 filter (eq "#Given") itms |> xml_of_itms),
407 XML.Elem (("WHERE", []),
408 xml_of_preconds where_),
409 XML.Elem (("FIND", []),
410 filter (eq "#Find") itms |> xml_of_itms),
411 XML.Elem (("RELATE", []),
412 filter (eq "#Relate") itms |> xml_of_itms)])
415 fun spec2xml j ((dI,pI,mI):spec) =
416 (indt j ^"<SPECIFICATION>\n"^
417 indt (j+i) ^"<THEORYID> "^ dI ^" </THEORYID>\n"^
418 indt (j+i) ^"<PROBLEMID>\n"^
420 indt (j+i) ^"</PROBLEMID>\n"^
421 indt (j+i) ^"<METHODID>\n"^
423 indt (j+i) ^"</METHODID>\n"^
424 indt j ^"</SPECIFICATION>\n"):xml;
425 fun xml_of_spec (thyID, pblID, metID) =
426 XML.Elem (("SPECIFICATION", []), [
427 XML.Elem (("THEORYID", []), [XML.Text thyID]),
428 XML.Elem (("PROBLEMID", []), [xml_of_strs pblID]),
429 XML.Elem (("METHODID", []), [xml_of_strs metID])])
430 fun xml_to_spec (XML.Elem (("SPECIFICATION", []), [
431 XML.Elem (("THEORYID", []), [XML.Text thyID]),
432 XML.Elem (("PROBLEMID", []), ps),
433 XML.Elem (("METHODID", []), ms)])) = (thyID, map xml_to_strs ps, map xml_to_strs ms)
434 | xml_to_spec tree = error ("xml_to_spec: wrong XML.tree " ^ xmlstr 0 tree)
436 fun modspec2xml j ((b, p_, head, gfr, pre, spec): ocalhd) =
437 (indt j ^"<CALCHEAD status = "^
438 quote (if b then "correct" else "incorrect")^">\n"^
439 indt (j+i) ^"<HEAD>\n"^
440 term2xml (j+i) head^"\n"^
441 indt (j+i) ^"</HEAD>\n"^
442 model2xml (j+i) gfr pre ^
443 indt (j+i) ^"<BELONGSTO> "^(case p_ of Pbl => "Pbl"
445 | _ => "Und")^" </BELONGSTO>\n"^
446 spec2xml (j+i) spec ^
447 indt j ^"</CALCHEAD>\n"):xml;
448 fun xml_of_modspec ((b, p_, head, gfr, pre, spec): ocalhd) =
449 XML.Elem (("CALCHEAD", [("status", if b then "correct" else "incorrect")]), [
450 XML.Elem (("HEAD", []), [xml_of_term head]),
451 XML.Elem (("BELONGSTO", []), [
452 XML.Text (case p_ of Pbl => "Pbl" | Met => "Met" | _ => "Und")]),
453 xml_of_model gfr pre,
456 fun pos'calchead2xml j (p:pos', (b, p_, head, gfr, pre, spec): ocalhd) =
457 (indt j ^"<CALCHEAD status = "^
458 quote (if b then "correct" else "incorrect")^">\n"^
459 pos'2xml (j+i) ("POSITION", p) ^
460 indt (j+i) ^"<HEAD>\n"^
461 term2xml (j+i) head^"\n"^
462 indt (j+i) ^"</HEAD>\n"^
463 model2xml (j+i) gfr pre ^
464 indt (j+i) ^"<BELONGSTO> "^(case p_ of Pbl => "Pbl"
466 | _ => "Und")^" </BELONGSTO>\n"^
467 spec2xml (j+i) spec ^
468 indt j ^"</CALCHEAD>\n"):xml;
470 fun sub2xml j (id, value) =
472 indt j ^" <VARIABLE>\n"^
473 term2xml (j+i) id ^ "\n" ^
474 indt j ^" </VARIABLE>\n" ^
475 indt j ^" <VALUE>\n"^
476 term2xml (j+i) value ^ "\n" ^
477 indt j ^" </VALUE>\n" ^
478 indt j ^"</PAIR>\n"):xml;
479 fun xml_of_sub (id, value) =
480 XML.Elem (("PAIR", []), [
481 XML.Elem (("VARIABLE", []), [xml_of_term id]),
482 XML.Elem (("VALUE", []), [xml_of_term value])])
483 fun subs2xml j (subs:subs) =
484 (indt j ^"<SUBSTITUTION>\n"^
485 foldl op^ ("", map (sub2xml (j+i))
486 (subs2subst (assoc_thy "Isac") subs)) ^
487 indt j ^"</SUBSTITUTION>\n"):xml;
488 fun xml_of_subs (subs : subs) =
489 XML.Elem (("SUBSTITUTION", []), map xml_of_sub (subs2subst (assoc_thy "Isac") subs))
491 fun subst2xml j (subst:subst) =
492 (indt j ^"<SUBSTITUTION>\n"^
493 foldl op^ ("", map (sub2xml (j+i)) subst) ^
494 indt j ^"</SUBSTITUTION>\n"):xml;
495 (* val subst = [(str2term "bdv", str2term "x")];
496 writeln(subst2xml 0 subst);
499 (* val (j, str) = ((j+i), form);
501 fun thmstr2xml j str = ((((term2xml j) o str2term) str)^"\n"):xml;
503 (* val (j, ((ID, form):thm')) = ((j+i), thm');
505 fun thm'2xml j ((ID, form):thm') =
506 (indt j ^"<THEOREM>\n"^
507 indt (j+i) ^"<ID> "^ID^" </ID>\n"^
508 indt (j+i) ^"<FORMULA>\n"^
509 thmstr2xml (j+i) form^
510 indt (j+i) ^"</FORMULA>\n"^
511 indt j ^"</THEOREM>\n"):xml;
512 fun xml_of_thm' ((ID, form) : thm') =
513 XML.Elem (("THEOREM", []), [
514 XML.Elem (("ID", []), [XML.Text ID]),
515 XML.Elem (("FORMULA", []), [XML.Text form])])
517 (*WN060627 scope of thy's not considered ?!?*)
518 fun thm''2xml j (thm : thm) =
519 indt j ^ "<THEOREM>\n" ^
520 indt (j+i) ^ "<ID> " ^ thmID_of_derivation_name' thm ^ " </ID>\n"^
521 term2xml j (prop_of thm) ^ "\n" ^
522 indt j ^ "</THEOREM>\n" : xml;
523 fun xml_of_thm (thm : thm) =
524 XML.Elem (("THEOREM", []), [
525 XML.Elem (("ID", []), [XML.Text (thmID_of_derivation_name' thm)]),
526 xml_of_term (prop_of thm)])
528 fun scr2xml j EmptyScr =
529 indt j ^"<SCRIPT> </SCRIPT>\n" : xml
530 | scr2xml j (Prog term) =
532 then indt j ^"<SCRIPT> </SCRIPT>\n"
533 else indt j ^"<SCRIPT>\n"^
534 term2xml j (inst_abs (assoc_thy "Isac") term) ^ "\n" ^
535 indt j ^"</SCRIPT>\n"
536 | scr2xml j (Rfuns _) =
537 indt j ^"<REVERSREWRITE> reverse rewrite functions </REVERSREWRITE>\n";
538 fun xml_of_src EmptyScr =
539 XML.Elem (("SCRIPT", []), [XML.Text "empty_script"])
540 | xml_of_src (Prog term) =
541 XML.Elem (("SCRIPT", []), [
542 if term = e_term then xml_of_src EmptyScr
543 else XML.Elem (("SCRIPT", []), [xml_of_term (inst_abs (assoc_thy "Isac") term)])])
544 | xml_of_src (Rfuns _) =
545 XML.Elem (("REVERSREWRITE", []), [XML.Text "reverse rewrite functions"])
547 fun prepa12xml j (terms, term) =
548 indt j ^"<PREPAT>\n"^
549 indt (j+i) ^"<PRECONDS>\n"^
550 terms2xml (j+2*i) terms ^
551 indt (j+i) ^"</PRECONDS>\n"^
552 indt (j+i) ^"<PATTERN>\n"^
553 term2xml (j+2*i) term ^
554 indt (j+i) ^"</PATTERN>\n"^
555 indt j ^"</PREPAT>\n" : xml;
557 fun prepat2xml j [] = ""
558 | prepat2xml j (p::ps) = prepa12xml j p ^ prepat2xml j ps : xml;
560 (* val (j, (thyID, seqrls, {id, preconds, rew_ord=(ord,_), erls,
561 srls, calc, rules, scr})) =
562 (j, (thyID, "Seq", data));
564 fun rls2xm j (thyID, seqrls, {id, preconds, rew_ord=(ord,_), erls,
565 srls, calc, rules, errpatts, scr}) =
566 indt j ^"<RULESET>\n"^
567 indt (j+i) ^"<ID> "^ id ^" </ID>\n"^
568 indt (j+i) ^"<TYPE> "^ seqrls ^" </TYPE>\n"^
569 indt (j+i) ^"<RULES>\n" ^
570 rules2xml (j+2*i) thyID rules ^
571 indt (j+i) ^"</RULES>\n" ^
572 indt (j+i) ^"<PRECONDS> " ^
573 terms2xml' (j+2*i) preconds ^
574 indt (j+i) ^"</PRECONDS>\n" ^
575 indt (j+i) ^"<ORDER>\n" ^
576 indt (j+2*i) ^ "<STRING> " ^ ord ^ " </STRING>\n" ^
577 (*WN060714 thy_isac_*-ord-*.xml not yet generated ................
578 indt (j+2*i) ^ "<GUH> " ^ ord2guh ("IsacKnowledge",
579 thyID) ord ^ " </GUH>\n" ^
580 ..................................................................*)
581 indt (j+i) ^"</ORDER>\n" ^
582 indt (j+i) ^"<ERLS>\n" ^
583 indt (j+2*i) ^ "<TAG> Ruleset </TAG>\n" ^
584 indt (j+2*i) ^ "<STRING> " ^ id_rls erls ^ " </STRING>\n" ^
585 indt (j+2*i) ^ "<GUH> " ^ rls2guh ("IsacKnowledge", thyID)
586 (id_rls erls) ^ " </GUH>\n" ^
587 indt (j+i) ^"</ERLS>\n" ^
588 indt (j+i) ^"<SRLS>\n" ^
589 indt (j+2*i) ^ "<TAG> Ruleset </TAG>\n" ^
590 indt (j+2*i) ^ "<STRING> " ^ id_rls erls ^ " </STRING>\n" ^
591 indt (j+2*i) ^ "<GUH> " ^ rls2guh ("IsacKnowledge", thyID)
592 (id_rls srls) ^ " </GUH>\n" ^
593 indt (j+i) ^"</SRLS>\n" ^
594 calcrefs2xml (j+i) (thyID, calc) ^
596 indt j ^"</RULESET>\n" : xml;
598 fun rls2xml j (thyID, Erls) = rls2xml j (thyID, e_rls)
599 | rls2xml j (thyID, Rls data) = rls2xm j (thyID, "Rls", data)
600 | rls2xml j (thyID, Seq data) = rls2xm j (thyID, "Seq", data)
601 | rls2xml j (thyID, Rrls {id, prepat, rew_ord=(ord,_), erls, calc, errpatts, scr}) =
602 indt j ^"<RULESET>\n"^
603 indt (j+i) ^"<ID> "^ id ^" </ID>\n"^
604 indt (j+i) ^"<TYPE> Rrls </TYPE>\n"^
605 prepat2xml (j+i) prepat ^
606 indt (j+i) ^"<ORDER> " ^
607 indt (j+2*i) ^ "<TAG> Rewrite order </TAG>\n" ^
608 indt (j+2*i) ^ "<STRING> " ^ ord ^ " </STRING>\n" ^
609 (*WN060714 thy_isac_*-ord-*.xml not yet generated ................
610 indt (j+2*i) ^ "<GUH> " ^ ord2guh ("IsacKnowledge",
611 thyID) ord ^ " </GUH>\n" ^
612 .................................................................*)
613 indt (j+i) ^"</ORDER>\n" ^
614 indt (j+i) ^"<ERLS> " ^
615 indt (j+2*i) ^ "<TAG> Ruleset </TAG>\n" ^
616 indt (j+2*i) ^ "<STRING> " ^ id_rls erls ^ " </STRING>\n" ^
617 indt (j+2*i) ^ "<GUH> " ^ rls2guh ("IsacKnowledge", thyID) (id_rls erls) ^ " </GUH>\n" ^
618 indt (j+i) ^"</ERLS>\n" ^
619 calcrefs2xml (j+i) (thyID, calc) ^
620 indt (j+i) ^"<SCRIPT>\n"^
621 scr2xml (j+2*i) scr ^
622 indt (j+i) ^" </SCRIPT>\n"^
623 indt j ^"</RULESET>\n" : xml;
625 (*.convert a tactic into xml-format
626 ATTENTION: WN060513 detected faulty 'cterm2xml's with 'string's as args.*)
627 fun tac2xml j (Subproblem (dI, pI)) =
628 (indt j ^"<SUBPROBLEMTACTIC name=\"Subproblem\">\n"^
629 indt (j+i) ^"<THEORY> "^ dI ^" </THEORY>\n"^
630 indt (j+i) ^"<PROBLEM>\n"^
632 indt (j+i) ^"</PROBLEM>\n"^
633 indt j ^"</SUBPROBLEMTACTIC>\n"):xml
634 | tac2xml j Model_Problem =
635 (indt j ^"<STRINGLISTTACTIC name=\"Model_Problem\">"^
636 indt j ^"</STRINGLISTTACTIC>\n"):xml
637 | tac2xml j (Refine_Tacitly pI) =
638 (indt j ^"<STRINGLISTTACTIC name=\"Refine_Tacitly\">\n"^
640 indt j ^"</STRINGLISTTACTIC>\n"):xml
642 | tac2xml j (Add_Given ct) =
643 (indt j ^"<SIMPLETACTIC name=\"Add_Given\">\n"^
645 indt j ^"</SIMPLETACTIC>\n"):xml
646 | tac2xml j (Add_Find ct) =
647 (indt j ^"<SIMPLETACTIC name=\"Add_Find\">\n"^
649 indt j ^"</SIMPLETACTIC>\n"):xml
650 | tac2xml j (Add_Relation ct) =
651 (indt j ^"<SIMPLETACTIC name=\"Add_Relation\">\n"^
653 indt j ^"</SIMPLETACTIC>\n"):xml
655 | tac2xml j (Specify_Theory ct) =
656 (indt j ^"<SIMPLETACTIC name=\"Specify_Theory\">\n"^
657 cterm2xml (j+i) ct^(*WN060513 Specify_Theory = fn : domID -> tac
658 and domID is a string, not a cterm *)
659 indt j ^"</SIMPLETACTIC>\n"):xml
660 | tac2xml j (Specify_Problem ct) =
661 (indt j ^"<STRINGLISTTACTIC name=\"Specify_Problem\">\n"^
663 indt j ^"</STRINGLISTTACTIC>\n"):xml
664 | tac2xml j (Specify_Method ct) =
665 (indt j ^"<STRINGLISTTACTIC name=\"Specify_Method\">\n"^
667 indt j ^"</STRINGLISTTACTIC>\n"):xml
668 | tac2xml j (Apply_Method mI) =
669 (indt j ^"<STRINGLISTTACTIC name=\"Apply_Method\">\n"^
671 indt j ^"</STRINGLISTTACTIC>\n"):xml
673 | tac2xml j (Take ct) =
674 (indt j ^"<SIMPLETACTIC name=\"Take\">\n"^
676 indt j ^"</SIMPLETACTIC>\n"):xml
677 | tac2xml j (Calculate opstr) =
678 (indt j ^"<SIMPLETACTIC name=\"Calculate\">\n"^
679 cterm2xml (j+i) opstr^(*WN060513 Calculate = fn : string -> tac
680 'string', _NOT_ 'cterm' ..flaw from RG*)
681 indt j ^"</SIMPLETACTIC>\n"):xml
682 (* val (j, Rewrite thm') = (i, tac);
684 | tac2xml j (Rewrite thm') =
685 (indt j ^"<REWRITETACTIC name=\"Rewrite\">\n"^
687 indt j ^"</REWRITETACTIC>\n"):xml
688 (* writeln (tac2xml 2 (Rewrite ("all_left",
689 "~ ?b =!= 0 ==> (?a = ?b) = (?a - ?b = 0)")));
690 val (j, (Rewrite_Inst (subs, thm'))) = (i, tac);
692 | tac2xml j (Rewrite_Inst (subs, thm')) =
693 (indt j ^"<REWRITEINSTTACTIC name=\"Rewrite_Inst\">\n"^
696 indt j ^"</REWRITEINSTTACTIC>\n"):xml
697 (* writeln (tac2xml 2 (Rewrite_Inst
700 "~ ?b =!= 0 ==> (?a = ?b) = (?a - ?b = 0)"))));
702 | tac2xml j (Rewrite_Set rls') =
703 (indt j ^"<REWRITESETTACTIC name=\"Rewrite_Set\">\n"^
704 indt (j+i) ^"<RULESET> "^ rls' ^" </RULESET>\n"^
705 indt j ^"</REWRITESETTACTIC>\n"):xml
706 | tac2xml j (Rewrite_Set_Inst (subs, rls')) =
707 (indt j ^"<REWRITESETINSTTACTIC name=\"Rewrite_Set_Inst\">\n"^
708 indt (j+i) ^"<RULESET> "^ rls' ^" </RULESET>\n"^
710 indt j ^"</REWRITESETINSTTACTIC>\n"):xml
712 | tac2xml j (Or_to_List) =
713 (indt j ^"<STRINGLISTTACTIC name=\"Or_to_List\"> </STRINGLISTTACTIC>\n"):xml
714 | tac2xml j (Check_elementwise ct) =
715 (indt j ^"<SIMPLETACTIC name=\"Check_elementwise\">\n"^
716 cterm2xml (j+i) ct ^ "\n"^
717 indt j ^"</SIMPLETACTIC>\n"):xml
718 (*WN0605 quick and dirty: cterms is _NOT_ a stringlist like pblID...*)
719 | tac2xml j (Substitute cterms) =
720 (indt j ^"<STRINGLISTTACTIC name=\"Substitute\">\n"^
721 (*cterms2xml (j+i) cterms^ ....should be WN060514: TODO TERMLISTTACTIC?*)
723 indt j ^"</STRINGLISTTACTIC>\n"):xml
724 | tac2xml j (Check_Postcond pI) =
725 (indt j ^"<STRINGLISTTACTIC name=\"Check_Postcond\">\n"^
727 indt j ^"</STRINGLISTTACTIC>\n"):xml
728 | tac2xml j tac = error ("tac2xml: not impl. for "^tac2str tac);
729 fun xml_of_tac (Subproblem (dI, pI)) =
730 XML.Elem (("SUBPROBLEMTACTIC", [("name", "Subproblem")]), [
731 XML.Elem (("THEORY", []), [XML.Text dI]),
732 XML.Elem (("PROBLEM", []), [xml_of_strs pI])])
733 | xml_of_tac Model_Problem =
734 XML.Elem (("STRINGLISTTACTIC", [("name", "Model_Problem")]), [])
735 | xml_of_tac (Refine_Tacitly pI) =
736 XML.Elem (("STRINGLISTTACTIC", [("name", "Refine_Tacitly")]), [xml_of_strs pI])
737 | xml_of_tac (Add_Given ct) =
738 XML.Elem (("SIMPLETACTIC", [("name", "Add_Given")]), [xml_of_cterm ct])
739 | xml_of_tac (Add_Find ct) =
740 XML.Elem (("SIMPLETACTIC", [("name", "Add_Find")]), [xml_of_cterm ct])
741 | xml_of_tac (Add_Relation ct) =
742 XML.Elem (("SIMPLETACTIC", [("name", "Add_Relation")]), [xml_of_cterm ct])
743 | xml_of_tac (Specify_Theory ct) =
744 (*WN060513 Specify_Theory = fn : domID -> tac and domID is a string, not a cterm *)
745 XML.Elem (("SIMPLETACTIC", [("name", "Specify_Theory")]), [xml_of_cterm ct])
746 | xml_of_tac (Specify_Problem ct) =
747 XML.Elem (("STRINGLISTTACTIC", [("name", "Specify_Problem")]), [xml_of_strs ct])
748 | xml_of_tac (Specify_Method ct) =
749 XML.Elem (("STRINGLISTTACTIC", [("name", "Specify_Method")]), [xml_of_strs ct])
750 | xml_of_tac (Apply_Method mI) =
751 XML.Elem (("STRINGLISTTACTIC", [("name", "Specify_Method")]), [xml_of_strs mI])
752 | xml_of_tac (Take ct) =
753 XML.Elem (("SIMPLETACTIC", [("name", "Take")]), [xml_of_cterm ct])
754 | xml_of_tac (Calculate opstr) =
755 (*WN060513 Calculate = fn : string -> tac 'string', _NOT_ 'cterm' ..flaw from RG*)
756 XML.Elem (("SIMPLETACTIC", [("name", "Take")]), [xml_of_cterm opstr])
757 | xml_of_tac (Rewrite thm') =
758 XML.Elem (("REWRITETACTIC", [("name", "Rewrite")]), [xml_of_thm' thm'])
759 | xml_of_tac (Rewrite_Inst (subs, thm')) =
760 XML.Elem (("REWRITEINSTTACTIC", [("name", "Rewrite_Inst")]), (
762 xml_of_thm' thm' :: []))
763 | xml_of_tac (Rewrite_Set rls') =
764 XML.Elem (("REWRITESETTACTIC", [("name", "Rewrite_Set")]), [XML.Text rls'])
765 | xml_of_tac (Rewrite_Set_Inst (subs, rls')) =
766 XML.Elem (("REWRITESETINSTTACTIC", [("name", "Rewrite_Set_Inst")]), (
767 XML.Elem (("RULESET", []), [XML.Text rls']) ::
768 xml_of_subs subs ::[]))
769 | xml_of_tac (Or_to_List) =
770 XML.Elem (("STRINGLISTTACTIC", [("name", "Or_to_List")]), [])
771 | xml_of_tac (Check_elementwise ct) =
772 XML.Elem (("SIMPLETACTIC", [("name", "Check_elementwise")]), [xml_of_cterm ct])
773 | xml_of_tac (Substitute cterms) =
774 (*WN0605 quick and dirty: cterms is _NOT_ a stringlist like pblID...
775 cterms2xml (j+i) cterms^ ....should be WN060514: TODO TERMLISTTACTIC?*)
776 XML.Elem (("STRINGLISTTACTIC", [("name", "Substitute")]), [xml_of_strs cterms])
777 | xml_of_tac (Check_Postcond pI) =
778 XML.Elem (("STRINGLISTTACTIC", [("name", "Or_to_List")]), [xml_of_strs pI])
779 | xml_of_tac tac = error ("xml_of_tac: not impl. for " ^ tac2str tac);
781 fun tacs2xml j [] = "":xml
782 | tacs2xml j (t::ts) = tac2xml j t ^ tacs2xml j ts;
785 fun posformhead2xml j (p:pos', Form f) =
786 indt j ^"<CALCFORMULA>\n"^
787 pos'2xml (j+i) ("POSITION", p) ^
788 indt (j+i) ^"<FORMULA>\n"^
789 term2xml (j+i) f^"\n"^
790 indt (j+i) ^"</FORMULA>\n"^
791 indt j ^"</CALCFORMULA>\n"
792 | posformhead2xml j (p, ModSpec c) =
793 pos'calchead2xml (j) (p, c);
795 fun posformheads2xml j [] = ("":xml)
796 | posformheads2xml j (r::rs) = posformhead2xml j r ^ posformheads2xml j rs;
798 val e_pblterm = (term_of o the o (parse @{theory Script}))
799 ("Problem (" ^ e_domID ^ "," ^ strs2str' e_pblID ^ ")");
801 (*WN051224 minimal adaption to exporting Formulae _only_ by getFormulaeFromTo*)
802 fun posterm2xml j (p:pos', t) =
803 indt j ^"<CALCFORMULA>\n"^
804 pos'2xml (j+i) ("POSITION", p) ^
805 indt (j+i) ^"<FORMULA>\n"^
806 (if t = e_pblterm (*headline in pbl is e_ <- _root_pbl for CAS-command*)
807 then cterm2xml (j+i) "________________________________________________"
808 else term2xml (j+i) t)^"\n" ^
809 indt (j+i) ^"</FORMULA>\n"^
810 indt j ^"</CALCFORMULA>\n";
811 fun xml_of_posterm ((p : pos'), t) =
812 XML.Elem (("CALCFORMULA", []),
813 [xml_of_pos "POSITION" p,
814 XML.Elem (("FORMULA", []), [
815 if t = e_pblterm (*headline in pbl is e_ <- _root_pbl for CAS-command*)
816 then xml_of_cterm "________________________________________________"
817 else xml_of_term t])])
819 fun posterms2xml j [] = ("":xml)
820 | posterms2xml j (r::rs) = posterm2xml j r ^ posterms2xml j rs;
822 fun asm_val2xml j (asm, vl) =
823 indt j ^ "<ASMEVALUATED>\n" ^
824 indt (j+i) ^ "<ASM>\n" ^
825 term2xml (j+i) asm ^ "\n" ^
826 indt (j+i) ^ "</ASM>\n" ^
827 indt (j+i) ^ "<VALUE>\n" ^
828 term2xml (j+i) vl ^ "\n" ^
829 indt (j+i) ^ "</VALUE>\n" ^
830 indt j ^ "</ASMEVALUATED>\n" : xml;
831 fun xml_of_asm_val (asm, vl) =
832 XML.Elem (("ASMEVALUATED", []),[
833 XML.Elem (("ASM", []), [xml_of_term asm]),
834 XML.Elem (("VALUE", []), [xml_of_term vl])])
836 fun asm_vals2xml j [] = ("":xml)
837 | asm_vals2xml j (asm_val::avs) = asm_val2xml j asm_val ^
840 (*.a reference to an element in the theory hierarchy;
841 compare 'fun keref2xml'.*)
842 (* val (j, thyID, typ, xstring) =
843 (i+i, snd (thy_containing_rls thy' prls'), "Rulesets", prls');
845 fun theref2xml j (thyID:thyID) typ (xstring:xstring) =
846 let val guh = theID2guh ["IsacKnowledge", thyID, typ, xstring]
847 val typ' = (implode o (drop_last_n 1) o Symbol.explode) typ
848 in indt j ^ "<KESTOREREF>\n" ^
849 indt (j+i) ^ "<TAG> " ^ typ' ^ " </TAG>\n" ^
850 indt (j+i) ^ "<ID> " ^ xstring ^ " </ID>\n" ^
851 indt (j+i) ^ "<GUH> " ^ guh ^ " </GUH>\n" ^
852 indt j ^ "</KESTOREREF>\n" : xml
854 fun xml_of_theref (thyid : thyID) typ (xstring : xstring) =
856 val guh = theID2guh ["IsacKnowledge", thyid, typ, xstring]
857 val typ' = (implode o (drop_last_n 1) o Symbol.explode) typ
859 XML.Elem (("KESTOREREF", []),[
860 XML.Elem (("TAG", []), [XML.Text typ']),
861 XML.Elem (("ID", []), [XML.Text xstring]),
862 XML.Elem (("GUH", []), [XML.Text guh])])
864 (*.a reference to an element in the kestore EXCEPT theory hierarchy;
865 compare 'fun theref2xml'.*)
866 (* val (j, typ, kestoreID) = (i+i, Met_, hd met);
868 fun keref2xml j typ (kestoreID:kestoreID) =
869 let val id = strs2str' kestoreID
870 val guh = kestoreID2guh typ kestoreID
871 in indt j ^ "<KESTOREREF>\n" ^
872 indt (j+i) ^ "<TAG> " ^ ketype2str' typ ^ "</TAG>\n" ^
873 indt (j+i) ^ "<ID> " ^ id ^ " </ID>\n" ^
874 indt (j+i) ^ "<GUH> " ^ guh ^ " </GUH>\n" ^
875 indt j ^ "</KESTOREREF>\n" : xml
878 (*url to a source external to isac*)
879 fun extref2xml j linktext url =
880 indt j ^ "<EXTREF>\n" ^
881 indt (j+i) ^ "<TEXT> " ^ linktext ^ " </TEXT>\n" ^
882 indt (j+i) ^ "<URL> " ^ url ^ " </URL>\n" ^
883 indt j ^ "</EXTREF>\n" : xml;
885 (* val (ContThmInst{thyID, thm, bdvs, thminst, applto, applat, reword,
886 asms, lhs, rhs, result, resasms, asmrls}) =
887 (context_thy (pt,pos) tac);
888 writeln (contthy2xml 2 (context_thy (pt,pos) tac));
890 fun contthy2xml j EContThy =
891 error "contthy2xml called with EContThy"
892 | contthy2xml j (ContThm {thyID, thm, applto, applat, reword,
893 asms,lhs, rhs, result, resasms, asmrls}) =
894 indt j ^ "<GUH> " ^ thm ^ " </GUH>\n" ^
896 indt j ^ "<APPLTO>\n" ^
897 term2xml j applto ^ "\n" ^
898 indt j ^ "</APPLTO>\n" ^
899 indt j ^ "<APPLAT>\n" ^
900 term2xml j applat ^ "\n" ^
901 indt j ^ "</APPLAT>\n" ^
902 indt j ^ "<ORDER>\n" ^ (*should be a theref2xml*)
903 indt (j+i) ^"<ID> " ^ reword ^ " </ID>\n" ^
904 indt j ^ "</ORDER>\n" ^
905 indt j ^ "<ASMSEVAL>\n" ^
906 asm_vals2xml (j+i) asms ^
907 indt j ^ "</ASMSEVAL>\n" ^
909 term2xml j (fst lhs) ^ "\n" ^
910 indt j ^ "</LHS>\n" ^
911 indt j ^ "<LHSINST>\n" ^
912 term2xml j (snd lhs) ^ "\n" ^
913 indt j ^ "</LHSINST>\n" ^
915 term2xml j (fst rhs) ^ "\n" ^
916 indt j ^ "</RHS>\n" ^
917 indt j ^ "<RHSINST>\n" ^
918 term2xml j (snd rhs) ^ "\n" ^
919 indt j ^ "</RHSINST>\n" ^
920 indt j ^ "<RESULT>\n" ^
921 term2xml j result ^ "\n" ^
922 indt j ^ "</RESULT>\n" ^
923 indt j ^ "<ASSUMPTIONS>\n" ^
924 terms2xml' j resasms ^
925 indt j ^ "</ASSUMPTIONS>\n" ^
926 indt j ^ "<EVALRLS>\n" ^
927 theref2xml j thyID "Rulesets" asmrls ^
928 indt j ^ "</EVALRLS>\n"
929 | contthy2xml j (ContThmInst{thyID, thm, bdvs, thminst, applto, applat,
930 reword, asms, lhs, rhs, result, resasms,
932 indt j ^ "<GUH> " ^ thm ^ " </GUH>\n" ^
933 indt j ^ "<SUBSLIST>\n" ^ (*should be an environment = substitution*)
934 indt (j+i) ^ "<MATHML>\n" ^
935 indt (j+2*i) ^ "<ISA> " ^ subst2str' bdvs ^ " </ISA>\n" ^
936 indt (j+i) ^ "</MATHML>\n" ^
937 indt j ^ "</SUBSLIST>\n" ^
938 indt j ^ "<INSTANTIATED>\n" ^
939 term2xml j thminst ^ "\n" ^
940 indt j ^ "</INSTANTIATED>\n" ^
941 indt j ^ "<APPLTO>\n" ^
942 term2xml j applto ^ "\n" ^
943 indt j ^ "</APPLTO>\n" ^
944 indt j ^ "<APPLAT>\n" ^
945 term2xml j applat ^ "\n" ^
946 indt j ^ "</APPLAT>\n" ^
947 indt j ^ "<ORDER>\n" ^ (*should be a theref2xml*)
948 indt (j+i) ^"<ID> " ^ reword ^ " </ID>\n" ^
949 indt j ^ "</ORDER>\n" ^
950 indt j ^ "<ASMSEVAL>\n" ^
951 asm_vals2xml (j+i) asms ^
952 indt j ^ "</ASMSEVAL>\n" ^
954 term2xml j (fst lhs) ^ "\n" ^
955 indt j ^ "</LHS>\n" ^
956 indt j ^ "<LHSINST>\n" ^
957 term2xml j (snd lhs) ^ "\n" ^
958 indt j ^ "</LHSINST>\n" ^
960 term2xml j (fst rhs) ^ "\n" ^
961 indt j ^ "</RHS>\n" ^
962 indt j ^ "<RHSINST>\n" ^
963 term2xml j (snd rhs) ^ "\n" ^
964 indt j ^ "</RHSINST>\n" ^
965 indt j ^ "<RESULT>\n" ^
966 term2xml j result ^ "\n" ^
967 indt j ^ "</RESULT>\n" ^
968 indt j ^ "<ASSUMPTOIONS>\n" ^
969 terms2xml' j resasms ^
970 indt j ^ "</ASSUMPTOIONS>\n" ^
971 indt j ^ "<EVALRLS>\n" ^
972 theref2xml j thyID "Rulesets" asmrls ^
973 indt j ^ "</EVALRLS>\n"
975 | contthy2xml j (ContRls {thyID, rls, applto, result, asms}) =
976 indt j ^ "<GUH> " ^ rls ^ " </GUH>\n" ^
977 indt j ^ "<APPLTO>\n" ^
978 term2xml j applto ^ "\n" ^
979 indt j ^ "</APPLTO>\n" ^
980 indt j ^ "<RESULT>\n" ^
981 term2xml j result ^ "\n" ^
982 indt j ^ "</RESULT>\n" ^
983 indt j ^ "<ASSUMPTOIONS>\n" ^
985 indt j ^ "</ASSUMPTOIONS>\n"
987 | contthy2xml j (ContRlsInst {thyID, rls, bdvs, applto, result, asms}) =
988 indt j ^ "<GUH> " ^ rls ^ " </GUH>\n" ^
989 indt j ^ "<SUBSLIST>\n" ^ (*should be an environment = substitution*)
990 indt (j+i) ^ "<MATHML>\n" ^
991 indt (j+2*i) ^ "<ISA> " ^ subst2str' bdvs ^ " </ISA>\n" ^
992 indt (j+i) ^ "</MATHML>\n" ^
993 indt j ^ "</SUBSLIST>\n" ^
994 indt j ^ "<APPLTO>\n" ^
995 term2xml j applto ^ "\n" ^
996 indt j ^ "</APPLTO>\n" ^
997 indt j ^ "<RESULT>\n" ^
998 term2xml j result ^ "\n" ^
999 indt j ^ "</RESULT>\n" ^
1000 indt j ^ "<ASSUMPTOIONS>\n" ^
1002 indt j ^ "</ASSUMPTOIONS>\n"
1004 | contthy2xml j (ContNOrew {thyID, thm_rls, applto}) =
1005 indt j ^ "<GUH> " ^ thm_rls ^ " </GUH>\n" ^
1006 indt j ^ "<APPLTO>\n" ^
1007 term2xml j applto ^ "\n" ^
1008 indt j ^ "</APPLTO>\n"
1010 | contthy2xml j (ContNOrewInst{thyID, thm_rls, bdvs, thminst, applto}) =
1011 indt j ^ "<GUH> " ^ thm_rls ^ " </GUH>\n" ^
1012 indt j ^ "<SUBSLIST>\n" ^ (*should be an environment = substitution*)
1013 indt (j+i) ^ "<MATHML>\n" ^
1014 indt (j+2*i) ^ "<ISA> " ^ subst2str' bdvs ^ " </ISA>\n" ^
1015 indt (j+i) ^ "</MATHML>\n" ^
1016 indt j ^ "</SUBSLIST>\n" ^
1017 indt j ^ "<INSTANTIATED>\n" ^
1018 term2xml j thminst ^ "\n" ^
1019 indt j ^ "</INSTANTIATED>\n" ^
1020 indt j ^ "<APPLTO>\n" ^
1021 term2xml j applto ^ "\n" ^
1022 indt j ^ "</APPLTO>\n" : xml;
1023 fun xml_of_contthy EContThy =
1024 error "contthy2xml called with EContThy"
1026 | xml_of_contthy (ContThm {thyID, thm, applto, applat, reword,
1027 asms,lhs, rhs, result, resasms, asmrls}) =
1028 [XML.Elem (("GUH", []), [XML.Text thm]),
1029 XML.Elem (("APPLTO", []), [xml_of_term applto]),
1030 XML.Elem (("APPLAT", []), [xml_of_term applat]),
1031 XML.Elem (("ORDER", []), [ (* should be a theref2xml *)
1032 XML.Elem (("ID", []), [XML.Text reword])]),
1033 XML.Elem (("ASMSEVAL", []), map xml_of_asm_val asms),
1034 XML.Elem (("LHS", []), [xml_of_term (fst lhs)]),
1035 XML.Elem (("LHSINST", []), [xml_of_term (snd lhs)]),
1036 XML.Elem (("RHS", []), [xml_of_term (fst rhs)]),
1037 XML.Elem (("RHSINST", []), [xml_of_term (snd rhs)]),
1038 XML.Elem (("RESULT", []), [xml_of_term result]),
1039 XML.Elem (("ASSUMPTIONS", []), map xml_of_term resasms),
1040 XML.Elem (("EVALRLS", []), [xml_of_theref thyID "Rulesets" asmrls])]
1042 | xml_of_contthy (ContThmInst {thyID, thm, bdvs, thminst, applto, applat,
1043 reword, asms, lhs, rhs, result, resasms, asmrls}) =
1044 [XML.Elem (("GUH", []), [XML.Text thm]),
1045 XML.Elem (("SUBSLIST", []), [ (* should be an environment = substitution *)
1046 xml_of_cterm (subst2str' bdvs)]),
1047 XML.Elem (("INSTANTIATED", []), [xml_of_term thminst]),
1048 XML.Elem (("APPLTO", []), [xml_of_term applto]),
1049 XML.Elem (("APPLAT", []), [xml_of_term applat]),
1050 XML.Elem (("ORDER", []), [ (* should be a theref2xml *)
1051 XML.Elem (("ID", []), [XML.Text reword])]),
1052 XML.Elem (("ASMSEVAL", []), map xml_of_asm_val asms),
1053 XML.Elem (("LHS", []), [xml_of_term (fst lhs)]),
1054 XML.Elem (("LHSINST", []), [xml_of_term (snd lhs)]),
1055 XML.Elem (("RHS", []), [xml_of_term (fst rhs)]),
1056 XML.Elem (("RHSINST", []), [xml_of_term (snd rhs)]),
1057 XML.Elem (("RESULT", []), [xml_of_term result]),
1058 XML.Elem (("ASSUMPTIONS", []), map xml_of_term resasms),
1059 XML.Elem (("EVALRLS", []), [xml_of_theref thyID "Rulesets" asmrls])]
1061 | xml_of_contthy (ContRls {thyID = _, rls, applto, result, asms}) =
1062 [XML.Elem (("GUH", []), [XML.Text rls]),
1063 XML.Elem (("APPLTO", []), [xml_of_term applto]),
1064 XML.Elem (("RESULT", []), [xml_of_term result]),
1065 XML.Elem (("ASSUMPTIONS", []), map xml_of_term asms)]
1067 | xml_of_contthy (ContRlsInst {thyID = _, rls, bdvs, applto, result, asms}) =
1068 [XML.Elem (("GUH", []), [XML.Text rls]),
1069 XML.Elem (("SUBSLIST", []), [ (* should be an environment = substitution *)
1070 xml_of_cterm (subst2str' bdvs)]),
1071 XML.Elem (("INSTANTIATED", []), [xml_of_cterm (subst2str' bdvs)]),
1072 XML.Elem (("APPLTO", []), [xml_of_term applto]),
1073 XML.Elem (("RESULT", []), [xml_of_term result]),
1074 XML.Elem (("ASSUMPTIONS", []), map xml_of_term asms)]
1076 | xml_of_contthy (ContNOrew {thyID = _, thm_rls, applto}) =
1077 [XML.Elem (("GUH", []), [XML.Text thm_rls]),
1078 XML.Elem (("APPLTO", []), [xml_of_term applto])]
1080 | xml_of_contthy (ContNOrewInst{thyID = _, thm_rls, bdvs, thminst, applto}) =
1081 [XML.Elem (("GUH", []), [XML.Text thm_rls]),
1082 XML.Elem (("SUBSLIST", []), [ (* should be an environment = substitution *)
1083 xml_of_cterm (subst2str' bdvs)]),
1084 XML.Elem (("INSTANTIATED", []), [xml_of_term thminst]),
1085 XML.Elem (("APPLTO", []), [xml_of_term applto])]
1087 fun xml_of_calcchanged calcid tag old del new =
1088 XML.Elem ((tag, []),[
1089 XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
1090 XML.Elem (("CALCCHANGED", []), [
1091 xml_of_pos "UNCHANGED" old,
1092 xml_of_pos "DELETED" del,
1093 xml_of_pos "GENERATED" new])])
1094 (*------------------------------------------------------------------
1097 ------------------------------------------------------------------*)