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 ------------------------------------------------------------------*)
70 (** general types: lists, **)
72 fun xml_of_bool b = XML.Elem (("BOOL", []), [XML.Text (bool2str b)])
73 fun xml_to_bool (XML.Elem (("BOOL", []), [XML.Text b])) = string_to_bool b
74 | xml_to_bool tree = raise ERROR ("xml_to_bool: wrong XML.tree \n" ^ xmlstr 0 tree)
76 fun xml_to_ketype (XML.Elem (("KETYPE", []), [XML.Text str])) = str2ketype' str
77 | xml_to_ketype tree = raise ERROR ("xml_to_ketype: wrong XML.tree \n" ^ xmlstr 0 tree)
79 (*.handles string list like 'fun id2xml'.*)
80 fun authors2xml j str auts =
81 let fun autx _ [] = ""
82 | autx j (s::ss) = (indt j) ^ "<STRING> " ^ s ^ " </STRING>\n" ^
84 in indt j ^ "<"^str^">\n" ^
86 indt j ^ "</"^str^">\n" : xml
88 (* writeln(authors2xml 2 "MATHAUTHORS" []);
89 writeln(authors2xml 2 "MATHAUTHORS"
90 ["isac-team 2001", "Richard Lang 2003"]);
94 let fun id2x _ [] = ""
95 | id2x j (s::ss) = (indt j) ^ "<STRING> " ^ s ^ " </STRING>\n" ^
97 in (indt j) ^ "<STRINGLIST>\n" ^
98 (id2x (j + indentation) ids) ^
99 (indt j) ^ "</STRINGLIST>\n" end;
100 (* writeln(id2xml 8 ["linear","univariate","equation"]);
102 <STRING>linear</STRING>
103 <STRING>univariate</STRING>
104 <STRING>equation</STRING>
107 fun xml_of_str str = XML.Elem (("STRING", []), [XML.Text str])
108 fun xml_of_strs strs = XML.Elem (("STRINGLIST", []), map xml_of_str strs)
110 fun xml_to_str (XML.Elem (("STRING", []), [XML.Text str])) = str
111 | xml_to_str tree = raise ERROR ("xml_to_str: wrong XML.tree \n" ^ xmlstr 0 tree)
112 fun xml_to_strs (XML.Elem (("STRINGLIST", []), strs)) = map xml_to_str strs
113 | xml_to_strs tree = raise ERROR ("xml_to_strs: wrong XML.tree \n" ^ xmlstr 0 tree)
116 let fun int2x _ [] = ""
117 | int2x j (s::ss) = (indt j) ^"<INT> "^ string_of_int s ^" </INT>\n"^
119 in (indt j) ^ "<INTLIST>\n" ^
120 (int2x (j + i) ids) ^
121 (indt j) ^ "</INTLIST>\n" end;
122 (* writeln(ints2xml 3 [1,2,3]);
124 fun xml_of_int i = XML.Elem (("INT", []), [XML.Text (string_of_int i)])
125 fun xml_of_ints is = (*xml/datatypes.sml: fun ints2xml*)
126 XML.Elem (("INTLIST", []), map xml_of_int is)
128 fun xml_to_int (XML.Elem (("INT", []), [XML.Text i])) =
129 (case int_of_str i of SOME i => i | _ => error "xml_to_int: int_of_str \<Rightarrow> NONE")
130 | xml_to_int tree = raise ERROR ("xml_to_int: wrong XML.tree \n" ^ xmlstr 0 tree)
131 fun xml_to_ints (XML.Elem (("INTLIST", []), is)) = map xml_to_int is
132 | xml_to_ints tree = raise ERROR ("xml_to_ints: wrong XML.tree \n" ^ xmlstr 0 tree)
135 (** isac datatypes **)
137 fun pos_2xml j pos_ =
138 (indt j) ^ "<POS> " ^ pos_2str pos_ ^ " </POS>\n";
140 (*.due to specialties of isac/util/parser/XMLParseDigest.java
141 pos' requires different tags.*)
142 fun pos'2xml j (tag, (pos, pos_)) =
143 indt (j) ^ "<" ^ tag ^ ">\n" ^
145 pos_2xml (j+i) pos_ ^
146 indt (j) ^ "</" ^ tag ^ ">\n";
147 (* writeln(pos'2xml 3 ("POSITION", ([1,2,3], Pbl)));
149 fun xml_of_pos tag (is, pp) = (*xml/datatypes.sml: fun pos'2xml*)
150 XML.Elem ((tag, []), [
152 XML.Elem (("POS", []), [XML.Text (pos_2str pp)])])
153 fun xml_to_pos_ (XML.Elem (("POS", []), [XML.Text pp])) = str2pos_ pp
154 | xml_to_pos_ tree = raise ERROR ("xml_to_pos_: wrong XML.tree \n" ^ xmlstr 0 tree)
155 fun xml_to_pos (XML.Elem (("POSITION", []), [is, pp])) = (xml_to_ints is, xml_to_pos_ pp) (*: pos'*)
156 | xml_to_pos tree = raise ERROR ("xml_to_pos: wrong XML.tree \n" ^ xmlstr 0 tree)
158 fun xml_of_auto (Step i) =
159 XML.Elem (("AUTO", []), [XML.Text "Step", XML.Text (string_of_int i)])
160 | xml_of_auto CompleteModel = XML.Elem (("AUTO", []), [XML.Text "CompleteModel"])
161 | xml_of_auto CompleteCalcHead = XML.Elem (("AUTO", []), [XML.Text "CompleteCalcHead"])
162 | xml_of_auto CompleteToSubpbl = XML.Elem (("AUTO", []), [XML.Text "CompleteToSubpbl"])
163 | xml_of_auto CompleteSubpbl = XML.Elem (("AUTO", []), [XML.Text "CompleteSubpbl"])
164 | xml_of_auto CompleteCalc = XML.Elem (("AUTO", []), [XML.Text "CompleteCalc"])
165 fun xml_to_auto (XML.Elem (("AUTO", []), [
166 XML.Elem (("STEP", []), [XML.Text i])])) = Step (int_of_str i |> the)
167 | xml_to_auto (XML.Elem (("AUTO", []), [XML.Text "CompleteModel"])) = CompleteModel
168 | xml_to_auto (XML.Elem (("AUTO", []), [XML.Text "CompleteCalcHead"])) = CompleteCalcHead
169 | xml_to_auto (XML.Elem (("AUTO", []), [XML.Text "CompleteToSubpbl"])) = CompleteToSubpbl
170 | xml_to_auto (XML.Elem (("AUTO", []), [XML.Text "CompleteSubpbl"])) = CompleteSubpbl
171 | xml_to_auto (XML.Elem (("AUTO", []), [XML.Text "CompleteCalc"])) = CompleteCalc
172 | xml_to_auto tree = raise ERROR ("xml_to_auto: wrong XML.tree \n" ^ xmlstr 0 tree)
174 fun formula2xml j term = (*TODO.WN050211: use for _all_ <FORMULA>*)
175 indt j ^ "<FORMULA>\n"^
176 term2xml j term ^"\n"^
177 indt j ^ "</FORMULA>\n" : xml;
178 fun xml_of_formula term =
179 XML.Elem (("FORMULA", []), [xml_of_term term])
181 (XML.Elem (("FORMULA", []), [form])) = xml_to_term form
182 | xml_to_formula x = raise ERROR ("xml_to_formula wrong arg: " ^ xmlstr 0 x)
183 (* TODO test/Tools/isac/xmlsrc/datatypes.sml*)
185 fun formulae2xml j [] = ("":xml)
186 | formulae2xml j (r::rs) = formula2xml j r ^ formulae2xml j rs;
187 (* writeln(formulae2xml 6 [str2term "1+1=2", str2term "1+1+1=3"]);
190 (*WN0502 @see ME/ctree: type asms: illdesigned, thus not used*)
191 fun posform2xml j (p:pos', term) =
192 indt j ^ "<POSFORM>\n" ^
193 pos'2xml (j+i) ("POSITION", p) ^
194 indt (j+i) ^ "<FORMULA>\n"^
195 term2xml (j+i) term ^"\n"^
196 indt (j+i) ^ "</FORMULA>\n"^
197 indt j ^ "</POSFORM>\n" : xml;
198 (* writeln(posform2xml 6 (([1,2],Frm), str2term "1+1=2"));
200 fun posforms2xml j [] = ("":xml)
201 | posforms2xml j (r::rs) = posform2xml j r ^ posforms2xml j rs;
202 (* writeln(posforms2xml 6 [(([1],Res), str2term "1+1=2"),(([2],Res), str2term "1+1+1=3")]);
205 fun calcref2xml j (thyID:thyID, (scrop, (rewop, _)):calc) =
206 indt j ^ "<CALCREF>\n" ^
207 indt (j+i) ^ "<STRING> " ^ scrop ^ "</STRING>\n" ^
208 indt (j+i) ^ "<GUH> " ^ cal2guh ("IsacKnowledge",
209 thyID) scrop ^ " </GUH>\n" ^
210 indt j ^ "</CALCREF>\n" : xml;
211 fun calcrefs2xml _ (_,[]) = "":xml
212 | calcrefs2xml j (thyID, cal::cs) =
213 calcref2xml j (thyID, cal) ^ calcrefs2xml j (thyID, cs);
215 fun calc2xml j (thyID:thyID, (scrop, (rewop, _)):calc) =
216 indt j ^ "<CALC>\n" ^
217 indt (j+i) ^ "<STRING>\n" ^ scrop ^ "</STRING>\n" ^
218 indt (j+i) ^ "<GUH>\n" ^ cal2guh ("IsacKnowledge",
219 thyID) scrop ^ "</GUH>\n" ^
220 indt (j+i) ^ "<TERMOP>\n" ^ rewop ^ "</TERMOP>\n" ^
221 indt j ^ "</CALC>\n" : xml;
223 (*.for creating a href for a rule within an rls's rule list;
224 the guh points to the thy of definition of the rule, NOT of use in rls.*)
225 fun rule2xml j (thyID:thyID) Erule =
226 error "rule2xml called with 'Erule'"
227 | rule2xml j thyID (Thm (thmDeriv, thm)) =
228 indt j ^ "<RULE>\n" ^
229 indt (j+i) ^ "<TAG> Theorem </TAG>\n" ^
230 indt (j+i) ^ "<STRING> " ^ thmID_of_derivation_name thmDeriv ^ " </STRING>\n" ^
231 indt (j+i) ^ "<GUH> " ^
232 thm2guh (thy_containing_thm thmDeriv) (thmID_of_derivation_name thmDeriv) ^ " </GUH>\n" ^
233 indt j ^ "</RULE>\n" : xml
234 | rule2xml j thyID (Calc (termop, _)) = ""
235 (*FIXXXXXXXME.WN060714 in rls make Calc : calc -> rule [add scriptop!]
236 see smltest/../datatypes.sml !
237 indt j ^ "<RULE>\n" ^
238 indt (j+i) ^ "<STRING> " ^ termop ^ " </STRING>\n" ^
239 indt (j+i) ^ "<GUH> " ^ cal2guh (thy_containing_cal thyID termop)
240 termop ^ " </GUH>\n" ^
243 | rule2xml j thyID (Cal1 (termop, _)) = ""
244 | rule2xml j thyID (Rls_ rls) =
245 let val rls' = (#id o rep_rls) rls
247 indt j ^ "<RULE>\n" ^
248 indt (j+i) ^ "<TAG> Ruleset </TAG>\n" ^
249 indt (j+i) ^ "<STRING> " ^ rls' ^ " </STRING>\n" ^
250 indt (j+i) ^ "<GUH> " ^ rls2guh (thy_containing_rls thyID rls') rls' ^ " </GUH>\n" ^
254 fun rules2xml j thyID [] = ("":xml)
255 | rules2xml j thyID (r::rs) = rule2xml j thyID r ^ rules2xml j thyID rs;
259 | filt ((s, (t1, t2)) :: ps) =
260 if str = s then (t1 $ t2) :: filt ps else filt ps
263 (*FIXME.WN040831 model2xml <--?--> pattern2xml*)
264 (*WN.25.8.03: pattern2xml different output with TextIO | writeln !!!
265 the version below is for TextIO: terms2xml makes \n !*)
266 (* val (j, p, where_) = (i, ppc, where_);
268 fun pattern2xml j p where_ =
269 (case filterpbl "#Given" p of
270 [] => (indt j) ^ "<GIVEN> </GIVEN>\n"
271 (* val gis = filterpbl "#Given" p;
273 | gis => (indt j) ^ "<GIVEN>\n" ^ terms2xml' j gis ^
274 (indt j) ^ "</GIVEN>\n")
277 [] => (indt j) ^ "<WHERE> </WHERE>\n"
278 | whs => (indt j) ^ "<WHERE>\n" ^ terms2xml' j whs ^
279 (indt j) ^ "</WHERE>\n")
281 (case filterpbl "#Find" p of
282 [] => (indt j) ^ "<FIND> </FIND>\n"
283 | fis => (indt j) ^ "<FIND>\n" ^ terms2xml' j fis ^
284 (indt j) ^ "</FIND>\n")
286 (case filterpbl "#Relate" p of
287 [] => (indt j) ^ "<RELATE> </RELATE>\n"
288 | res => (indt j) ^ "<RELATE>\n" ^ terms2xml' j res ^
289 (indt j) ^ "</RELATE>\n");
291 writeln(pattern2xml 3 ((#ppc o get_pbt)
292 ["squareroot","univariate","equation","test"]) []);
296 fun itm_2xml j (Cor (dts,_)) =
297 (indt j ^"<ITEM status=\"correct\">\n"^
298 term2xml (j) (comp_dts' dts)^"\n"^
299 indt j ^"</ITEM>\n"):xml
300 | itm_2xml j (Syn c) =
301 indt j ^"<ITEM status=\"syntaxerror\">\n"^
304 | itm_2xml j (Typ c) =
305 indt j ^"<ITEM status=\"typeerror\">\n"^
308 (*type item also has 'False of cterm' set in preconds2xml WN 050618*)
309 | itm_2xml j (Inc (dts,_)) =
310 indt j ^"<ITEM status=\"incomplete\">\n"^
311 term2xml (j) (comp_dts' dts)^"\n"^
313 | itm_2xml j (Sup dts) =
314 indt j ^"<ITEM status=\"superfluous\">\n"^
315 term2xml (j) (comp_dts' dts)^"\n"^
317 | itm_2xml j (Mis (d,pid)) =
318 indt j ^"<ITEM status=\"missing\">\n"^
319 term2xml (j) (d $ pid)^"\n"^
321 fun xml_of_itm_ (Cor (dts, _)) =
322 XML.Elem (("ITEM", [("status", "correct")]), [xml_of_term (comp_dts' dts)])
323 | xml_of_itm_ (Syn c) =
324 XML.Elem (("ITEM", [("status", "syntaxerror")]), [XML.Text c])
325 | xml_of_itm_ (Typ c) =
326 XML.Elem (("ITEM", [("status", "typeerror")]), [XML.Text c])
327 (*type item also has 'False of cterm' set in preconds2xml WN 050618*)
328 | xml_of_itm_ (Inc (dts, _)) =
329 XML.Elem (("ITEM", [("status", "incomplete")]), [xml_of_term (comp_dts' dts)])
330 | xml_of_itm_ (Sup dts) =
331 XML.Elem (("ITEM", [("status", "superfluous")]), [xml_of_term (comp_dts' dts)])
332 | xml_of_itm_ (Mis (d, pid)) =
333 XML.Elem (("ITEM", [("status", "missing")]), [xml_of_term (d $ pid)])
335 (*see terms2xml' fpr \n*)
336 fun itms2xml _ [] = ""
337 | itms2xml j [(_,_,_,_,itm_)] = itm_2xml j itm_
338 | itms2xml j (((_,_,_,_,itm_):itm)::itms) =
339 itm_2xml j itm_ ^ itms2xml j itms;
340 fun xml_of_itms itms =
342 fun extract (_, _, _, _, itm_) = itm_
343 | extract _ = error "xml_of_itms.extract: wrong argument"
344 in map (xml_of_itm_ o extract) itms end
346 fun precond2xml j (true, term) =
347 (indt j ^"<ITEM status=\"correct\">\n"^
348 term2xml (j) term^"\n"^
349 indt j ^"</ITEM>\n"):xml
350 | precond2xml j (false, term) =
351 indt j ^"<ITEM status=\"false\">\n"^
352 term2xml (j+i) term^"\n"^
354 fun xml_of_precond (status, term) =
355 XML.Elem (("ITEM", [("status", if status then "correct" else "false")]), [xml_of_term term])
357 fun preconds2xml _ [] = ("":xml)
358 | preconds2xml j (p::ps) = precond2xml j p ^ preconds2xml j ps;
359 fun xml_of_preconds ps = map xml_of_precond ps
361 (*FIXME.WN040831 model2xml <--?--> pattern2xml*)
362 fun model2xml j (itms:itm list) where_ =
363 let fun eq4 str (_,_,_,field,_) = str = field
364 in (indt j ^"<MODEL>\n"^
365 (case filter (eq4 "#Given") itms of
366 [] => (indt (j+i)) ^ "<GIVEN> </GIVEN>\n"
367 | gis => (indt (j+i)) ^ "<GIVEN>\n" ^ itms2xml (j+2*i) gis ^
368 (indt (j+i)) ^ "</GIVEN>\n")
371 [] => (indt (j+i)) ^ "<WHERE> </WHERE>\n"
372 | whs => (indt (j+i)) ^ "<WHERE>\n" ^ preconds2xml (j+2*i) whs ^
373 (indt (j+i)) ^ "</WHERE>\n")
375 (case filter (eq4 "#Find") itms of
376 [] => (indt (j+i)) ^ "<FIND> </FIND>\n"
377 | fis => (indt (j+i)) ^ "<FIND>\n" ^ itms2xml (j+2*i) fis ^
378 (indt (j+i)) ^ "</FIND>\n")
380 (case filter (eq4 "#Relate") itms of
381 [] => (indt (j+i)) ^ "<RELATE> </RELATE>\n"
382 | res => (indt (j+i)) ^ "<RELATE>\n" ^ itms2xml (j+2*i) res ^
383 (indt (j+i)) ^ "</RELATE>\n")^
384 indt j ^"</MODEL>\n"):xml
386 (* writeln(model2xml 3 itms []);
388 fun xml_of_model itms where_ =
390 fun eq str (_, _, _,field, _) = str = field
392 XML.Elem (("MODEL", []), [
393 XML.Elem (("GIVEN", []),
394 filter (eq "#Given") itms |> xml_of_itms),
395 XML.Elem (("WHERE", []),
396 xml_of_preconds where_),
397 XML.Elem (("FIND", []),
398 filter (eq "#Find") itms |> xml_of_itms),
399 XML.Elem (("RELATE", []),
400 filter (eq "#Relate") itms |> xml_of_itms)])
403 fun spec2xml j ((dI,pI,mI):spec) =
404 (indt j ^"<SPECIFICATION>\n"^
405 indt (j+i) ^"<THEORYID> "^ dI ^" </THEORYID>\n"^
406 indt (j+i) ^"<PROBLEMID>\n"^
408 indt (j+i) ^"</PROBLEMID>\n"^
409 indt (j+i) ^"<METHODID>\n"^
411 indt (j+i) ^"</METHODID>\n"^
412 indt j ^"</SPECIFICATION>\n"):xml;
413 fun xml_of_spec (thyID, pblID, metID) =
414 XML.Elem (("SPECIFICATION", []), [
415 XML.Elem (("THEORYID", []), [XML.Text thyID]),
416 XML.Elem (("PROBLEMID", []), [xml_of_strs pblID]),
417 XML.Elem (("METHODID", []), [xml_of_strs metID])])
418 fun xml_to_spec (XML.Elem (("SPECIFICATION", []), [
419 XML.Elem (("THEORYID", []), [XML.Text thyID]),
420 XML.Elem (("PROBLEMID", []), [ps]),
421 XML.Elem (("METHODID", []), [ms])])) = (thyID, xml_to_strs ps, xml_to_strs ms)
422 | xml_to_spec tree = raise ERROR ("xml_to_spec: wrong XML.tree \n" ^ xmlstr 0 tree)
424 fun xml_of_variant (items, spec) =
425 XML.Elem (("VARIANT", []), [xml_of_strs items, xml_of_spec spec])
426 fun xml_to_variant (XML.Elem (("VARIANT", []), [items, spec])) =
427 (xml_to_strs items, xml_to_spec spec)
428 | xml_to_variant tree = raise ERROR ("xml_to_variant: wrong XML.tree \n" ^ xmlstr 0 tree)
430 fun xml_of_fmz [] = xml_of_fmz [e_fmz]
431 | xml_of_fmz vs = XML.Elem (("FORMALIZATION", []), map xml_of_variant vs)
432 fun xml_to_fmz (XML.Elem (("FORMALIZATION", []), vars)) = map xml_to_variant vars
433 | xml_to_fmz tree = raise ERROR ("xml_to_fmz: wrong XML.tree \n" ^ xmlstr 0 tree)
435 fun modspec2xml j ((b, p_, head, gfr, pre, spec): ocalhd) =
436 (indt j ^"<CALCHEAD status = "^
437 quote (if b then "correct" else "incorrect")^">\n"^
438 indt (j+i) ^"<HEAD>\n"^
439 term2xml (j+i) head^"\n"^
440 indt (j+i) ^"</HEAD>\n"^
441 model2xml (j+i) gfr pre ^
442 indt (j+i) ^"<BELONGSTO> "^(case p_ of Pbl => "Pbl"
444 | _ => "Und")^" </BELONGSTO>\n"^
445 spec2xml (j+i) spec ^
446 indt j ^"</CALCHEAD>\n"):xml;
447 fun xml_of_modspec ((b, p_, head, gfr, pre, spec): ocalhd) =
448 XML.Elem (("CALCHEAD", [("status", if b then "correct" else "incorrect")]), [
449 XML.Elem (("HEAD", []), [xml_of_term head]),
450 xml_of_model gfr pre,
451 XML.Elem (("BELONGSTO", []), [
452 XML.Text (case p_ of Pbl => "Pbl" | Met => "Met" | _ => "Und")]),
455 fun pos'calchead2xml j (p:pos', (b, p_, head, gfr, pre, spec): ocalhd) =
456 (indt j ^"<CALCHEAD status = "^
457 quote (if b then "correct" else "incorrect")^">\n"^
458 pos'2xml (j+i) ("POSITION", p) ^
459 indt (j+i) ^"<HEAD>\n"^
460 term2xml (j+i) head^"\n"^
461 indt (j+i) ^"</HEAD>\n"^
462 model2xml (j+i) gfr pre ^
463 indt (j+i) ^"<BELONGSTO> "^(case p_ of Pbl => "Pbl"
465 | _ => "Und")^" </BELONGSTO>\n"^
466 spec2xml (j+i) spec ^
467 indt j ^"</CALCHEAD>\n"):xml;
468 fun xml_of_posmodspec ((p: pos', (b, p_, head, gfr, pre, spec): ocalhd)) =
469 XML.Elem (("CALCHEAD", [("status", if b then "correct" else "incorrect")]), [
470 xml_of_pos "POSITION" p,
471 XML.Elem (("HEAD", []), [xml_of_term head]),
472 xml_of_model gfr pre,
473 XML.Elem (("BELONGSTO", []), [
474 XML.Text (case p_ of Pbl => "Pbl" | Met => "Met" | _ => "Und")]),
477 (XML.Elem (("IMODEL", []), [
478 XML.Elem (("GIVEN", []), givens),
479 (*XML.Elem (("WHERE", []), wheres), ... Where is never input*)
480 XML.Elem (("FIND", []), finds),
481 XML.Elem (("RELATE", []), relates)])) =
482 ([Given (map xml_to_cterm givens),
483 Find (map xml_to_cterm finds),
484 Relate (map xml_to_cterm relates)]): imodel
485 | xml_to_imodel x = raise ERROR ("xml_to_imodel: WRONG arg = " ^ xmlstr 0 x)
487 (XML.Elem (("ICALCHEAD", []), [
488 pos as XML.Elem (("POSITION", []), _),
489 headln as XML.Elem (("MATHML", []), _),
490 imodel as XML.Elem (("MATHML", []), _), (* TODO WN150813 ?!?*)
491 XML.Elem (("POS", []), [XML.Text belongsto]),
492 spec as XML.Elem (("SPECIFICATION", []), _)])) =
493 (xml_to_pos pos, xml_to_cterm headln, xml_to_imodel imodel,
494 str2pos_ belongsto, xml_to_spec spec): icalhd
495 | xml_to_icalhd x = raise ERROR ("xml_to_icalhd: WRONG arg = " ^ xmlstr 0 x)
497 fun sub2xml j (id, value) =
499 indt j ^" <VARIABLE>\n"^
500 term2xml (j+i) id ^ "\n" ^
501 indt j ^" </VARIABLE>\n" ^
502 indt j ^" <VALUE>\n"^
503 term2xml (j+i) value ^ "\n" ^
504 indt j ^" </VALUE>\n" ^
505 indt j ^"</PAIR>\n"):xml;
506 fun xml_of_sub (id, value) =
507 XML.Elem (("PAIR", []), [
508 XML.Elem (("VARIABLE", []), [xml_of_term id]),
509 XML.Elem (("VALUE", []), [xml_of_term value])])
511 (XML.Elem (("PAIR", []), [
512 XML.Elem (("VARIABLE", []), [id]),
513 XML.Elem (("VALUE", []), [value])])) = (xml_to_term id, xml_to_term value)
514 | xml_to_sub x = raise ERROR ("xml_to_sub wrong arg: " ^ xmlstr 0 x)
515 fun subs2xml j (subs:subs) =
516 (indt j ^"<SUBSTITUTION>\n"^
517 foldl op^ ("", map (sub2xml (j+i))
518 (subs2subst (assoc_thy "Isac") subs)) ^
519 indt j ^"</SUBSTITUTION>\n"):xml;
520 fun xml_of_subs (subs : subs) =
521 XML.Elem (("SUBSTITUTION", []), map xml_of_sub (subs2subst (assoc_thy "Isac") subs))
523 (XML.Elem (("SUBSTITUTION", []),
524 subs)) = (subst2subs (map xml_to_sub subs) : subs)
525 | xml_to_subs x = raise ERROR ("xml_to_subs wrong arg: " ^ xmlstr 0 x)
526 fun xml_of_sube (sube : sube) =
527 XML.Elem (("SUBSTITUTION", []), map xml_of_sub (sube2subst (assoc_thy "Isac") sube))
529 (XML.Elem (("SUBSTITUTION", []),
530 xml_var_val_pairs)) = subst2sube (map xml_to_sub xml_var_val_pairs)
531 | xml_to_sube x = raise ERROR ("xml_to_sube wrong arg: " ^ xmlstr 0 x)
533 fun subst2xml j (subst:subst) =
534 (indt j ^"<SUBSTITUTION>\n"^
535 foldl op^ ("", map (sub2xml (j+i)) subst) ^
536 indt j ^"</SUBSTITUTION>\n"):xml;
537 (* val subst = [(str2term "bdv", str2term "x")];
538 writeln(subst2xml 0 subst);
541 (* val (j, str) = ((j+i), form);
543 fun thmstr2xml j str = ((((term2xml j) o str2term) str)^"\n"):xml;
545 (* val (j, ((ID, form):thm')) = ((j+i), thm');
547 fun thm'2xml j ((ID, form):thm') =
548 (indt j ^"<THEOREM>\n"^
549 indt (j+i) ^"<ID> "^ID^" </ID>\n"^
550 indt (j+i) ^"<FORMULA>\n"^
551 thmstr2xml (j+i) form^
552 indt (j+i) ^"</FORMULA>\n"^
553 indt j ^"</THEOREM>\n"):xml;
554 fun xml_of_thm' ((ID, form) : thm') =
555 XML.Elem (("THEOREM", []), [
556 XML.Elem (("ID", []), [XML.Text ID]),
557 XML.Elem (("FORMULA", []), [
558 XML.Text form])]) (* repair for MathML: use term instead String *)
560 (XML.Elem (("THEOREM", []), [
561 XML.Elem (("ID", []), [XML.Text ID]),
562 XML.Elem (("FORMULA", []), [(* repair for MathML: use term instead String *)
563 XML.Text form])])) = ((ID, form) : thm')
564 | xml_to_thm' x = raise ERROR ("xml_of_thm' wrong arg:" ^ xmlstr 0 x)
566 (*WN060627 scope of thy's not considered ?!?*)
567 fun thm''2xml j (thm : thm) =
568 indt j ^ "<THEOREM>\n" ^
569 indt (j+i) ^ "<ID> " ^ thmID_of_derivation_name' thm ^ " </ID>\n"^
570 term2xml j (Thm.prop_of thm) ^ "\n" ^
571 indt j ^ "</THEOREM>\n" : xml;
572 fun xml_of_thm (thm : thm) =
573 XML.Elem (("THEOREM", []), [
574 XML.Elem (("ID", []), [XML.Text (thmID_of_derivation_name' thm)]),
575 xml_of_term (Thm.prop_of thm)])
577 fun scr2xml j EmptyScr =
578 indt j ^"<SCRIPT> </SCRIPT>\n" : xml
579 | scr2xml j (Prog term) =
581 then indt j ^"<SCRIPT> </SCRIPT>\n"
582 else indt j ^"<SCRIPT>\n"^
583 term2xml j (inst_abs (assoc_thy "Isac") term) ^ "\n" ^
584 indt j ^"</SCRIPT>\n"
585 | scr2xml j (Rfuns _) =
586 indt j ^"<REVERSREWRITE> reverse rewrite functions </REVERSREWRITE>\n";
587 fun xml_of_src EmptyScr =
588 XML.Elem (("NOCODE", []), [XML.Text "empty"])
589 | xml_of_src (Prog term) =
590 XML.Elem (("CODE", []), [
591 if term = e_term then xml_of_src EmptyScr
592 else xml_of_term (inst_abs (assoc_thy "Isac") term)])
593 | xml_of_src (Rfuns _) =
594 XML.Elem (("NOCODE", []), [XML.Text "reverse rewrite functions"])
596 fun prepa12xml j (terms, term) =
597 indt j ^"<PREPAT>\n"^
598 indt (j+i) ^"<PRECONDS>\n"^
599 terms2xml (j+2*i) terms ^
600 indt (j+i) ^"</PRECONDS>\n"^
601 indt (j+i) ^"<PATTERN>\n"^
602 term2xml (j+2*i) term ^
603 indt (j+i) ^"</PATTERN>\n"^
604 indt j ^"</PREPAT>\n" : xml;
606 fun prepat2xml j [] = ""
607 | prepat2xml j (p::ps) = prepa12xml j p ^ prepat2xml j ps : xml;
609 (* val (j, (thyID, seqrls, {id, preconds, rew_ord=(ord,_), erls,
610 srls, calc, rules, scr})) =
611 (j, (thyID, "Seq", data));
613 fun rls2xm j (thyID, seqrls, {id, preconds, rew_ord=(ord,_), erls,
614 srls, calc, rules, errpatts, scr}) =
615 indt j ^"<RULESET>\n"^
616 indt (j+i) ^"<ID> "^ id ^" </ID>\n"^
617 indt (j+i) ^"<TYPE> "^ seqrls ^" </TYPE>\n"^
618 indt (j+i) ^"<RULES>\n" ^
619 rules2xml (j+2*i) thyID rules ^
620 indt (j+i) ^"</RULES>\n" ^
621 indt (j+i) ^"<PRECONDS> " ^
622 terms2xml' (j+2*i) preconds ^
623 indt (j+i) ^"</PRECONDS>\n" ^
624 indt (j+i) ^"<ORDER>\n" ^
625 indt (j+2*i) ^ "<STRING> " ^ ord ^ " </STRING>\n" ^
626 (*WN060714 thy_isac_*-ord-*.xml not yet generated ................
627 indt (j+2*i) ^ "<GUH> " ^ ord2guh ("IsacKnowledge",
628 thyID) ord ^ " </GUH>\n" ^
629 ..................................................................*)
630 indt (j+i) ^"</ORDER>\n" ^
631 indt (j+i) ^"<ERLS>\n" ^
632 indt (j+2*i) ^ "<TAG> Ruleset </TAG>\n" ^
633 indt (j+2*i) ^ "<STRING> " ^ id_rls erls ^ " </STRING>\n" ^
634 indt (j+2*i) ^ "<GUH> " ^ rls2guh ("IsacKnowledge", thyID)
635 (id_rls erls) ^ " </GUH>\n" ^
636 indt (j+i) ^"</ERLS>\n" ^
637 indt (j+i) ^"<SRLS>\n" ^
638 indt (j+2*i) ^ "<TAG> Ruleset </TAG>\n" ^
639 indt (j+2*i) ^ "<STRING> " ^ id_rls erls ^ " </STRING>\n" ^
640 indt (j+2*i) ^ "<GUH> " ^ rls2guh ("IsacKnowledge", thyID)
641 (id_rls srls) ^ " </GUH>\n" ^
642 indt (j+i) ^"</SRLS>\n" ^
643 calcrefs2xml (j+i) (thyID, calc) ^
645 indt j ^"</RULESET>\n" : xml;
647 fun rls2xml j (thyID, Erls) = rls2xml j (thyID, e_rls)
648 | rls2xml j (thyID, Rls data) = rls2xm j (thyID, "Rls", data)
649 | rls2xml j (thyID, Seq data) = rls2xm j (thyID, "Seq", data)
650 | rls2xml j (thyID, Rrls {id, prepat, rew_ord=(ord,_), erls, calc, errpatts, scr}) =
651 indt j ^"<RULESET>\n"^
652 indt (j+i) ^"<ID> "^ id ^" </ID>\n"^
653 indt (j+i) ^"<TYPE> Rrls </TYPE>\n"^
654 prepat2xml (j+i) prepat ^
655 indt (j+i) ^"<ORDER> " ^
656 indt (j+2*i) ^ "<TAG> Rewrite order </TAG>\n" ^
657 indt (j+2*i) ^ "<STRING> " ^ ord ^ " </STRING>\n" ^
658 (*WN060714 thy_isac_*-ord-*.xml not yet generated ................
659 indt (j+2*i) ^ "<GUH> " ^ ord2guh ("IsacKnowledge",
660 thyID) ord ^ " </GUH>\n" ^
661 .................................................................*)
662 indt (j+i) ^"</ORDER>\n" ^
663 indt (j+i) ^"<ERLS> " ^
664 indt (j+2*i) ^ "<TAG> Ruleset </TAG>\n" ^
665 indt (j+2*i) ^ "<STRING> " ^ id_rls erls ^ " </STRING>\n" ^
666 indt (j+2*i) ^ "<GUH> " ^ rls2guh ("IsacKnowledge", thyID) (id_rls erls) ^ " </GUH>\n" ^
667 indt (j+i) ^"</ERLS>\n" ^
668 calcrefs2xml (j+i) (thyID, calc) ^
669 indt (j+i) ^"<SCRIPT>\n"^
670 scr2xml (j+2*i) scr ^
671 indt (j+i) ^" </SCRIPT>\n"^
672 indt j ^"</RULESET>\n" : xml;
674 (*.convert a tactic into xml-format
675 ATTENTION: WN060513 detected faulty 'cterm2xml's with 'string's as args.*)
676 fun tac2xml j (Subproblem (dI, pI)) =
677 (indt j ^"<SUBPROBLEMTACTIC name=\"Subproblem\">\n"^
678 indt (j+i) ^"<THEORY> "^ dI ^" </THEORY>\n"^
679 indt (j+i) ^"<PROBLEM>\n"^
681 indt (j+i) ^"</PROBLEM>\n"^
682 indt j ^"</SUBPROBLEMTACTIC>\n"):xml
683 | tac2xml j Model_Problem =
684 (indt j ^"<STRINGLISTTACTIC name=\"Model_Problem\">"^
685 indt j ^"</STRINGLISTTACTIC>\n"):xml
686 | tac2xml j (Refine_Tacitly pI) =
687 (indt j ^"<STRINGLISTTACTIC name=\"Refine_Tacitly\">\n"^
689 indt j ^"</STRINGLISTTACTIC>\n"):xml
691 | tac2xml j (Add_Given ct) =
692 (indt j ^"<SIMPLETACTIC name=\"Add_Given\">\n"^
694 indt j ^"</SIMPLETACTIC>\n"):xml
695 | tac2xml j (Add_Find ct) =
696 (indt j ^"<SIMPLETACTIC name=\"Add_Find\">\n"^
698 indt j ^"</SIMPLETACTIC>\n"):xml
699 | tac2xml j (Add_Relation ct) =
700 (indt j ^"<SIMPLETACTIC name=\"Add_Relation\">\n"^
702 indt j ^"</SIMPLETACTIC>\n"):xml
704 | tac2xml j (Specify_Theory ct) =
705 (indt j ^"<SIMPLETACTIC name=\"Specify_Theory\">\n"^
706 cterm2xml (j+i) ct^(*WN060513 Specify_Theory = fn : domID -> tac
707 and domID is a string, not a cterm *)
708 indt j ^"</SIMPLETACTIC>\n"):xml
709 | tac2xml j (Specify_Problem ct) =
710 (indt j ^"<STRINGLISTTACTIC name=\"Specify_Problem\">\n"^
712 indt j ^"</STRINGLISTTACTIC>\n"):xml
713 | tac2xml j (Specify_Method ct) =
714 (indt j ^"<STRINGLISTTACTIC name=\"Specify_Method\">\n"^
716 indt j ^"</STRINGLISTTACTIC>\n"):xml
717 | tac2xml j (Apply_Method mI) =
718 (indt j ^"<STRINGLISTTACTIC name=\"Apply_Method\">\n"^
720 indt j ^"</STRINGLISTTACTIC>\n"):xml
722 | tac2xml j (Take ct) =
723 (indt j ^"<SIMPLETACTIC name=\"Take\">\n"^
725 indt j ^"</SIMPLETACTIC>\n"):xml
726 | tac2xml j (Calculate opstr) =
727 (indt j ^"<SIMPLETACTIC name=\"Calculate\">\n"^
728 cterm2xml (j+i) opstr^(*WN060513 Calculate = fn : string -> tac
729 'string', _NOT_ 'cterm' ..flaw from RG*)
730 indt j ^"</SIMPLETACTIC>\n"):xml
731 (* val (j, Rewrite thm') = (i, tac);
733 | tac2xml j (Rewrite thm') =
734 (indt j ^"<REWRITETACTIC name=\"Rewrite\">\n"^
736 indt j ^"</REWRITETACTIC>\n"):xml
737 (* writeln (tac2xml 2 (Rewrite ("all_left",
738 "~ ?b =!= 0 ==> (?a = ?b) = (?a - ?b = 0)")));
739 val (j, (Rewrite_Inst (subs, thm'))) = (i, tac);
741 | tac2xml j (Rewrite_Inst (subs, thm')) =
742 (indt j ^"<REWRITEINSTTACTIC name=\"Rewrite_Inst\">\n"^
745 indt j ^"</REWRITEINSTTACTIC>\n"):xml
746 (* writeln (tac2xml 2 (Rewrite_Inst
749 "~ ?b =!= 0 ==> (?a = ?b) = (?a - ?b = 0)"))));
751 | tac2xml j (Rewrite_Set rls') =
752 (indt j ^"<REWRITESETTACTIC name=\"Rewrite_Set\">\n"^
753 indt (j+i) ^"<RULESET> "^ rls' ^" </RULESET>\n"^
754 indt j ^"</REWRITESETTACTIC>\n"):xml
755 | tac2xml j (Rewrite_Set_Inst (subs, rls')) =
756 (indt j ^"<REWRITESETINSTTACTIC name=\"Rewrite_Set_Inst\">\n"^
757 indt (j+i) ^"<RULESET> "^ rls' ^" </RULESET>\n"^
759 indt j ^"</REWRITESETINSTTACTIC>\n"):xml
761 | tac2xml j (Or_to_List) =
762 (indt j ^"<STRINGLISTTACTIC name=\"Or_to_List\"> </STRINGLISTTACTIC>\n"):xml
763 | tac2xml j (Check_elementwise ct) =
764 (indt j ^"<SIMPLETACTIC name=\"Check_elementwise\">\n"^
765 cterm2xml (j+i) ct ^ "\n"^
766 indt j ^"</SIMPLETACTIC>\n"):xml
767 (*WN0605 quick and dirty: cterms is _NOT_ a stringlist like pblID...*)
768 | tac2xml j (Substitute cterms) =
769 (indt j ^"<STRINGLISTTACTIC name=\"Substitute\">\n"^
770 (*cterms2xml (j+i) cterms^ ....should be WN060514: TODO TERMLISTTACTIC?*)
772 indt j ^"</STRINGLISTTACTIC>\n"):xml
773 | tac2xml j (Check_Postcond pI) =
774 (indt j ^"<STRINGLISTTACTIC name=\"Check_Postcond\">\n"^
776 indt j ^"</STRINGLISTTACTIC>\n"):xml
777 | tac2xml j tac = error ("tac2xml: not impl. for "^tac2str tac);
778 fun xml_of_tac (Subproblem (dI, pI)) =
779 XML.Elem (("SUBPROBLEMTACTIC", [("name", "Subproblem")]), [
780 XML.Elem (("THEORY", []), [XML.Text dI]),
781 XML.Elem (("PROBLEM", []), [xml_of_strs pI])])
782 | xml_of_tac (Substitute cterms) =
783 (*Substitute: sube -> tac; e_sube: cterm' list; UNCLEAR HOW TO INPUT ON FRONTEND*)
784 XML.Elem (("STRINGLISTTACTIC", [("name", "Substitute")]), [xml_of_sube cterms])
785 (*----- Rewrite* -----------------------------------------------------*)
786 | xml_of_tac (Rewrite thm') =
787 XML.Elem (("REWRITETACTIC", [("name", "Rewrite")]), [xml_of_thm' thm'])
788 | xml_of_tac (Rewrite_Inst (subs, thm')) =
789 XML.Elem (("REWRITEINSTTACTIC", [("name", "Rewrite_Inst")]), (
791 xml_of_thm' thm' :: []))
792 | xml_of_tac (Rewrite_Set rls') =
793 XML.Elem (("REWRITESETTACTIC", [("name", "Rewrite_Set")]), [XML.Text rls'])
794 | xml_of_tac (Rewrite_Set_Inst (subs, rls')) =
795 XML.Elem (("REWRITESETINSTTACTIC", [("name", "Rewrite_Set_Inst")]), ([
797 XML.Elem (("RULESET", []), [XML.Text rls'])]))
798 (*----- FORMTACTIC ---------------------------------------------------*)
799 | xml_of_tac (Add_Find ct) =
800 XML.Elem (("FORMTACTIC", [("name", "Add_Find")]), [xml_of_cterm ct])
801 | xml_of_tac (Add_Given ct) =
802 XML.Elem (("FORMTACTIC", [("name", "Add_Given")]), [xml_of_cterm ct])
803 | xml_of_tac (Add_Relation ct) =
804 XML.Elem (("FORMTACTIC", [("name", "Add_Relation")]), [xml_of_cterm ct])
805 | xml_of_tac (Check_elementwise ct) =
806 XML.Elem (("FORMTACTIC", [("name", "Check_elementwise")]), [xml_of_cterm ct])
807 | xml_of_tac (Take ct) =
808 XML.Elem (("FORMTACTIC", [("name", "Take")]), [xml_of_cterm ct])
809 (*----- SIMPLETACTIC -------------------------------------------------*)
810 | xml_of_tac (Calculate opstr) =
811 XML.Elem (("SIMPLETACTIC", [("name", "Calculate")]), [XML.Text opstr])
812 | xml_of_tac (Or_to_List) =
813 XML.Elem (("SIMPLETACTIC", [("name", "Or_to_List")]), [(*//////////*)])
814 | xml_of_tac (Specify_Theory ct) =
815 XML.Elem (("SIMPLETACTIC", [("name", "Specify_Theory")]), [XML.Text ct])
816 (*----- STRINGLISTTACTIC ---------------------------------------------*)
817 | xml_of_tac (Apply_Method mI) =
818 XML.Elem (("STRINGLISTTACTIC", [("name", "Apply_Method")]), [xml_of_strs mI])
819 | xml_of_tac (Check_Postcond pI) =
820 XML.Elem (("STRINGLISTTACTIC", [("name", "Check_Postcond")]), [xml_of_strs pI])
821 | xml_of_tac Model_Problem =
822 XML.Elem (("STRINGLISTTACTIC", [("name", "Model_Problem")]), [])
823 | xml_of_tac (Refine_Tacitly pI) =
824 XML.Elem (("STRINGLISTTACTIC", [("name", "Refine_Tacitly")]), [xml_of_strs pI])
825 | xml_of_tac (Specify_Method ct) =
826 XML.Elem (("STRINGLISTTACTIC", [("name", "Specify_Method")]), [xml_of_strs ct])
827 | xml_of_tac (Specify_Problem ct) =
828 XML.Elem (("STRINGLISTTACTIC", [("name", "Specify_Problem")]), [xml_of_strs ct])
829 | xml_of_tac tac = raise ERROR ("xml_of_tac: not impl. for " ^ tac2str tac);
832 (XML.Elem (("SUBPROBLEMTACTIC", [("name", "Subproblem")]), [
833 XML.Elem (("THEORY", []), [XML.Text dI]),
834 XML.Elem (("PROBLEM", []), [pI])])) = Subproblem (dI, xml_to_strs pI)
836 (*Substitute: sube -> tac; e_sube: cterm' list; UNCLEAR HOW TO INPUT ON FRONTEND*)
837 (XML.Elem (("STRINGLISTTACTIC", [
838 ("name", "Substitute")]), [cterms])) = Substitute (xml_to_sube cterms)
839 (*----- Rewrite* -----------------------------------------------------*)
841 (XML.Elem (("REWRITETACTIC", [
842 ("name", "Rewrite")]), [thm'])) = Rewrite (xml_to_thm' thm')
844 (XML.Elem (("REWRITEINSTTACTIC", [
845 ("name", "Rewrite_Inst")]), [
846 subs, thm'])) = Rewrite_Inst (xml_to_subs subs, xml_to_thm' thm')
848 (XML.Elem (("REWRITESETTACTIC", [
849 ("name", "Rewrite_Set")]), [XML.Text rls'])) = Rewrite_Set (rls')
851 (XML.Elem (("REWRITESETINSTTACTIC", [
852 ("name", "Rewrite_Set_Inst")]), [
854 XML.Elem (("RULESET", []), [XML.Text rls'])])) = Rewrite_Set_Inst (xml_to_subs subs, rls')
855 (*----- FORMTACTIC ---------------------------------------------------*)
857 (XML.Elem (("FORMTACTIC", [
858 ("name", "Add_Find")]), [ct])) = Add_Find (xml_to_cterm ct)
860 (XML.Elem (("FORMTACTIC", [
861 ("name", "Add_Given")]), [ct])) = Add_Given (xml_to_cterm ct)
863 (XML.Elem (("FORMTACTIC", [
864 ("name", "Add_Relation")]), [ct])) = Add_Relation (xml_to_cterm ct)
866 (XML.Elem (("FORMTACTIC", [
867 ("name", "Take")]), [ct])) = Take (xml_to_cterm ct)
869 (XML.Elem (("FORMTACTIC", [
870 ("name", "Check_elementwise")]), [ct])) = Check_elementwise (xml_to_cterm ct)
871 (*----- SIMPLETACTIC -------------------------------------------------*)
873 (XML.Elem (("SIMPLETACTIC", [
874 ("name", "Calculate")]), [XML.Text opstr])) = Calculate opstr
876 (XML.Elem (("SIMPLETACTIC", [("name", "Or_to_List")]), [])) = Or_to_List
878 (XML.Elem (("SIMPLETACTIC", [
879 ("name", "Specify_Theory")]), [XML.Text ct])) = Specify_Theory ct
880 (*----- STRINGLISTTACTIC ---------------------------------------------*)
882 (XML.Elem (("STRINGLISTTACTIC", [
883 ("name", "Apply_Method")]), [mI])) = Apply_Method (xml_to_strs mI)
885 (XML.Elem (("STRINGLISTTACTIC", [
886 ("name", "Check_Postcond")]), [pI])) = Check_Postcond (xml_to_strs pI)
888 (XML.Elem (("STRINGLISTTACTIC", [
889 ("name", "Model_Problem")]), [])) = Model_Problem
891 (XML.Elem (("STRINGLISTTACTIC", [
892 ("name", "Refine_Tacitly")]), [pI])) = Refine_Tacitly (xml_to_strs pI)
894 (XML.Elem (("STRINGLISTTACTIC", [
895 ("name", "Specify_Method")]), [ct])) = Specify_Method (xml_to_strs ct)
897 (XML.Elem (("STRINGLISTTACTIC", [
898 ("name", "Specify_Problem")]), [ct])) = Specify_Problem (xml_to_strs ct)
899 | xml_to_tac x = raise ERROR ("xml_to_tac: not impl. for " ^ xmlstr 0 x);
901 fun tacs2xml j [] = "":xml
902 | tacs2xml j (t::ts) = tac2xml j t ^ tacs2xml j ts;
904 fun posformhead2xml j (p:pos', Form f) =
905 indt j ^"<CALCFORMULA>\n"^
906 pos'2xml (j+i) ("POSITION", p) ^
907 indt (j+i) ^"<FORMULA>\n"^
908 term2xml (j+i) f^"\n"^
909 indt (j+i) ^"</FORMULA>\n"^
910 indt j ^"</CALCFORMULA>\n"
911 | posformhead2xml j (p, ModSpec c) =
912 pos'calchead2xml (j) (p, c);
914 fun posformheads2xml j [] = ("":xml)
915 | posformheads2xml j (r::rs) = posformhead2xml j r ^ posformheads2xml j rs;
917 val e_pblterm = (term_of o the o (parse @{theory Script}))
918 ("Problem (" ^ e_domID ^ "," ^ strs2str' e_pblID ^ ")");
920 (*WN051224 minimal adaption to exporting Formulae _only_ by getFormulaeFromTo*)
921 fun posterm2xml j (p:pos', t) =
922 indt j ^"<CALCFORMULA>\n"^
923 pos'2xml (j+i) ("POSITION", p) ^
924 indt (j+i) ^"<FORMULA>\n"^
925 (if t = e_pblterm (*headline in pbl is e_ <- _root_pbl for CAS-command*)
926 then cterm2xml (j+i) "________________________________________________"
927 else term2xml (j+i) t)^"\n" ^
928 indt (j+i) ^"</FORMULA>\n"^
929 indt j ^"</CALCFORMULA>\n";
930 fun xml_of_posterm ((p : pos'), t) =
931 XML.Elem (("CALCFORMULA", []),
932 [xml_of_pos "POSITION" p,
933 XML.Elem (("FORMULA", []), [
934 if t = e_pblterm (*headline in pbl is e_ <- _root_pbl for CAS-command*)
935 then xml_of_cterm "________________________________________________"
936 else xml_of_term t])])
938 fun posterms2xml j [] = ("":xml)
939 | posterms2xml j (r::rs) = posterm2xml j r ^ posterms2xml j rs;
941 fun asm_val2xml j (asm, vl) =
942 indt j ^ "<ASMEVALUATED>\n" ^
943 indt (j+i) ^ "<ASM>\n" ^
944 term2xml (j+i) asm ^ "\n" ^
945 indt (j+i) ^ "</ASM>\n" ^
946 indt (j+i) ^ "<VALUE>\n" ^
947 term2xml (j+i) vl ^ "\n" ^
948 indt (j+i) ^ "</VALUE>\n" ^
949 indt j ^ "</ASMEVALUATED>\n" : xml;
950 fun xml_of_asm_val (asm, vl) =
951 XML.Elem (("ASMEVALUATED", []),[
952 XML.Elem (("ASM", []), [xml_of_term asm]),
953 XML.Elem (("VALUE", []), [xml_of_term vl])])
955 fun asm_vals2xml j [] = ("":xml)
956 | asm_vals2xml j (asm_val::avs) = asm_val2xml j asm_val ^
959 (*.a reference to an element in the theory hierarchy;
960 compare 'fun keref2xml'.*)
961 (* val (j, thyID, typ, xstring) =
962 (i+i, snd (thy_containing_rls thy' prls'), "Rulesets", prls');
964 fun theref2xml j (thyID:thyID) typ (xstring:xstring) =
965 let val guh = theID2guh ["IsacKnowledge", thyID, typ, xstring]
966 val typ' = (implode o (drop_last_n 1) o Symbol.explode) typ
967 in indt j ^ "<KESTOREREF>\n" ^
968 indt (j+i) ^ "<TAG> " ^ typ' ^ " </TAG>\n" ^
969 indt (j+i) ^ "<ID> " ^ xstring ^ " </ID>\n" ^
970 indt (j+i) ^ "<GUH> " ^ guh ^ " </GUH>\n" ^
971 indt j ^ "</KESTOREREF>\n" : xml
973 fun xml_of_theref (thyid : thyID) typ (xstring : xstring) =
975 val guh = theID2guh ["IsacKnowledge", thyid, typ, xstring]
976 val typ' = (implode o (drop_last_n 1) o Symbol.explode) typ
978 XML.Elem (("KESTOREREF", []),[
979 XML.Elem (("TAG", []), [XML.Text typ']),
980 XML.Elem (("ID", []), [XML.Text xstring]),
981 XML.Elem (("GUH", []), [XML.Text guh])])
983 (*.a reference to an element in the kestore EXCEPT theory hierarchy;
984 compare 'fun theref2xml'.*)
985 (* val (j, typ, kestoreID) = (i+i, Met_, hd met);
987 fun keref2xml j typ (kestoreID:kestoreID) =
988 let val id = strs2str' kestoreID
989 val guh = kestoreID2guh typ kestoreID
990 in indt j ^ "<KESTOREREF>\n" ^
991 indt (j+i) ^ "<TAG> " ^ ketype2str' typ ^ "</TAG>\n" ^
992 indt (j+i) ^ "<ID> " ^ id ^ " </ID>\n" ^
993 indt (j+i) ^ "<GUH> " ^ guh ^ " </GUH>\n" ^
994 indt j ^ "</KESTOREREF>\n" : xml
997 (*url to a source external to isac*)
998 fun extref2xml j linktext url =
999 indt j ^ "<EXTREF>\n" ^
1000 indt (j+i) ^ "<TEXT> " ^ linktext ^ " </TEXT>\n" ^
1001 indt (j+i) ^ "<URL> " ^ url ^ " </URL>\n" ^
1002 indt j ^ "</EXTREF>\n" : xml;
1004 (* val (ContThmInst{thyID, thm, bdvs, thminst, applto, applat, reword,
1005 asms, lhs, rhs, result, resasms, asmrls}) =
1006 (context_thy (pt,pos) tac);
1007 writeln (contthy2xml 2 (context_thy (pt,pos) tac));
1009 fun contthy2xml j EContThy =
1010 error "contthy2xml called with EContThy"
1011 | contthy2xml j (ContThm {thyID, thm, applto, applat, reword,
1012 asms,lhs, rhs, result, resasms, asmrls}) =
1013 indt j ^ "<GUH> " ^ thm ^ " </GUH>\n" ^
1015 indt j ^ "<APPLTO>\n" ^
1016 term2xml j applto ^ "\n" ^
1017 indt j ^ "</APPLTO>\n" ^
1018 indt j ^ "<APPLAT>\n" ^
1019 term2xml j applat ^ "\n" ^
1020 indt j ^ "</APPLAT>\n" ^
1021 indt j ^ "<ORDER>\n" ^ (*should be a theref2xml*)
1022 indt (j+i) ^"<ID> " ^ reword ^ " </ID>\n" ^
1023 indt j ^ "</ORDER>\n" ^
1024 indt j ^ "<ASMSEVAL>\n" ^
1025 asm_vals2xml (j+i) asms ^
1026 indt j ^ "</ASMSEVAL>\n" ^
1027 indt j ^ "<LHS>\n" ^
1028 term2xml j (fst lhs) ^ "\n" ^
1029 indt j ^ "</LHS>\n" ^
1030 indt j ^ "<LHSINST>\n" ^
1031 term2xml j (snd lhs) ^ "\n" ^
1032 indt j ^ "</LHSINST>\n" ^
1033 indt j ^ "<RHS>\n" ^
1034 term2xml j (fst rhs) ^ "\n" ^
1035 indt j ^ "</RHS>\n" ^
1036 indt j ^ "<RHSINST>\n" ^
1037 term2xml j (snd rhs) ^ "\n" ^
1038 indt j ^ "</RHSINST>\n" ^
1039 indt j ^ "<RESULT>\n" ^
1040 term2xml j result ^ "\n" ^
1041 indt j ^ "</RESULT>\n" ^
1042 indt j ^ "<ASSUMPTIONS>\n" ^
1043 terms2xml' j resasms ^
1044 indt j ^ "</ASSUMPTIONS>\n" ^
1045 indt j ^ "<EVALRLS>\n" ^
1046 theref2xml j thyID "Rulesets" asmrls ^
1047 indt j ^ "</EVALRLS>\n"
1048 | contthy2xml j (ContThmInst{thyID, thm, bdvs, thminst, applto, applat,
1049 reword, asms, lhs, rhs, result, resasms,
1051 indt j ^ "<GUH> " ^ thm ^ " </GUH>\n" ^
1052 indt j ^ "<SUBSLIST>\n" ^ (*should be an environment = substitution*)
1053 indt (j+i) ^ "<MATHML>\n" ^
1054 indt (j+2*i) ^ "<ISA> " ^ subst2str' bdvs ^ " </ISA>\n" ^
1055 indt (j+i) ^ "</MATHML>\n" ^
1056 indt j ^ "</SUBSLIST>\n" ^
1057 indt j ^ "<INSTANTIATED>\n" ^
1058 term2xml j thminst ^ "\n" ^
1059 indt j ^ "</INSTANTIATED>\n" ^
1060 indt j ^ "<APPLTO>\n" ^
1061 term2xml j applto ^ "\n" ^
1062 indt j ^ "</APPLTO>\n" ^
1063 indt j ^ "<APPLAT>\n" ^
1064 term2xml j applat ^ "\n" ^
1065 indt j ^ "</APPLAT>\n" ^
1066 indt j ^ "<ORDER>\n" ^ (*should be a theref2xml*)
1067 indt (j+i) ^"<ID> " ^ reword ^ " </ID>\n" ^
1068 indt j ^ "</ORDER>\n" ^
1069 indt j ^ "<ASMSEVAL>\n" ^
1070 asm_vals2xml (j+i) asms ^
1071 indt j ^ "</ASMSEVAL>\n" ^
1072 indt j ^ "<LHS>\n" ^
1073 term2xml j (fst lhs) ^ "\n" ^
1074 indt j ^ "</LHS>\n" ^
1075 indt j ^ "<LHSINST>\n" ^
1076 term2xml j (snd lhs) ^ "\n" ^
1077 indt j ^ "</LHSINST>\n" ^
1078 indt j ^ "<RHS>\n" ^
1079 term2xml j (fst rhs) ^ "\n" ^
1080 indt j ^ "</RHS>\n" ^
1081 indt j ^ "<RHSINST>\n" ^
1082 term2xml j (snd rhs) ^ "\n" ^
1083 indt j ^ "</RHSINST>\n" ^
1084 indt j ^ "<RESULT>\n" ^
1085 term2xml j result ^ "\n" ^
1086 indt j ^ "</RESULT>\n" ^
1087 indt j ^ "<ASSUMPTOIONS>\n" ^
1088 terms2xml' j resasms ^
1089 indt j ^ "</ASSUMPTOIONS>\n" ^
1090 indt j ^ "<EVALRLS>\n" ^
1091 theref2xml j thyID "Rulesets" asmrls ^
1092 indt j ^ "</EVALRLS>\n"
1094 | contthy2xml j (ContRls {thyID, rls, applto, result, asms}) =
1095 indt j ^ "<GUH> " ^ rls ^ " </GUH>\n" ^
1096 indt j ^ "<APPLTO>\n" ^
1097 term2xml j applto ^ "\n" ^
1098 indt j ^ "</APPLTO>\n" ^
1099 indt j ^ "<RESULT>\n" ^
1100 term2xml j result ^ "\n" ^
1101 indt j ^ "</RESULT>\n" ^
1102 indt j ^ "<ASSUMPTOIONS>\n" ^
1104 indt j ^ "</ASSUMPTOIONS>\n"
1106 | contthy2xml j (ContRlsInst {thyID, rls, bdvs, applto, result, asms}) =
1107 indt j ^ "<GUH> " ^ rls ^ " </GUH>\n" ^
1108 indt j ^ "<SUBSLIST>\n" ^ (*should be an environment = substitution*)
1109 indt (j+i) ^ "<MATHML>\n" ^
1110 indt (j+2*i) ^ "<ISA> " ^ subst2str' bdvs ^ " </ISA>\n" ^
1111 indt (j+i) ^ "</MATHML>\n" ^
1112 indt j ^ "</SUBSLIST>\n" ^
1113 indt j ^ "<APPLTO>\n" ^
1114 term2xml j applto ^ "\n" ^
1115 indt j ^ "</APPLTO>\n" ^
1116 indt j ^ "<RESULT>\n" ^
1117 term2xml j result ^ "\n" ^
1118 indt j ^ "</RESULT>\n" ^
1119 indt j ^ "<ASSUMPTOIONS>\n" ^
1121 indt j ^ "</ASSUMPTOIONS>\n"
1123 | contthy2xml j (ContNOrew {thyID, thm_rls, applto}) =
1124 indt j ^ "<GUH> " ^ thm_rls ^ " </GUH>\n" ^
1125 indt j ^ "<APPLTO>\n" ^
1126 term2xml j applto ^ "\n" ^
1127 indt j ^ "</APPLTO>\n"
1129 | contthy2xml j (ContNOrewInst{thyID, thm_rls, bdvs, thminst, applto}) =
1130 indt j ^ "<GUH> " ^ thm_rls ^ " </GUH>\n" ^
1131 indt j ^ "<SUBSLIST>\n" ^ (*should be an environment = substitution*)
1132 indt (j+i) ^ "<MATHML>\n" ^
1133 indt (j+2*i) ^ "<ISA> " ^ subst2str' bdvs ^ " </ISA>\n" ^
1134 indt (j+i) ^ "</MATHML>\n" ^
1135 indt j ^ "</SUBSLIST>\n" ^
1136 indt j ^ "<INSTANTIATED>\n" ^
1137 term2xml j thminst ^ "\n" ^
1138 indt j ^ "</INSTANTIATED>\n" ^
1139 indt j ^ "<APPLTO>\n" ^
1140 term2xml j applto ^ "\n" ^
1141 indt j ^ "</APPLTO>\n" : xml;
1142 fun xml_of_contthy EContThy =
1143 error "contthy2xml called with EContThy"
1145 | xml_of_contthy (ContThm {thyID, thm, applto, applat, reword,
1146 asms,lhs, rhs, result, resasms, asmrls}) =
1147 XML.Elem (("CONTEXTDATA", []), [
1148 XML.Elem (("GUH", []), [XML.Text thm]),
1149 XML.Elem (("APPLTO", []), [xml_of_term applto]),
1150 XML.Elem (("APPLAT", []), [xml_of_term applat]),
1151 XML.Elem (("ORDER", []), [ (* should be a theref2xml *)
1152 XML.Elem (("ID", []), [XML.Text reword])]),
1153 XML.Elem (("ASMSEVAL", []), map xml_of_asm_val asms),
1154 XML.Elem (("LHS", []), [xml_of_term (fst lhs)]),
1155 XML.Elem (("LHSINST", []), [xml_of_term (snd lhs)]),
1156 XML.Elem (("RHS", []), [xml_of_term (fst rhs)]),
1157 XML.Elem (("RHSINST", []), [xml_of_term (snd rhs)]),
1158 XML.Elem (("RESULT", []), [xml_of_term result]),
1159 XML.Elem (("ASSUMPTIONS", []), map xml_of_term resasms),
1160 XML.Elem (("EVALRLS", []), [xml_of_theref thyID "Rulesets" asmrls])])
1162 | xml_of_contthy (ContThmInst {thyID, thm, bdvs, thminst, applto, applat,
1163 reword, asms, lhs, rhs, result, resasms, asmrls}) =
1164 XML.Elem (("CONTEXTDATA", []), [
1165 XML.Elem (("GUH", []), [XML.Text thm]),
1166 XML.Elem (("SUBSLIST", []), [ (* should be an environment = substitution *)
1167 xml_of_cterm (subst2str' bdvs)]),
1168 XML.Elem (("INSTANTIATED", []), [xml_of_term thminst]),
1169 XML.Elem (("APPLTO", []), [xml_of_term applto]),
1170 XML.Elem (("APPLAT", []), [xml_of_term applat]),
1171 XML.Elem (("ORDER", []), [ (* should be a theref2xml *)
1172 XML.Elem (("ID", []), [XML.Text reword])]),
1173 XML.Elem (("ASMSEVAL", []), map xml_of_asm_val asms),
1174 XML.Elem (("LHS", []), [xml_of_term (fst lhs)]),
1175 XML.Elem (("LHSINST", []), [xml_of_term (snd lhs)]),
1176 XML.Elem (("RHS", []), [xml_of_term (fst rhs)]),
1177 XML.Elem (("RHSINST", []), [xml_of_term (snd rhs)]),
1178 XML.Elem (("RESULT", []), [xml_of_term result]),
1179 XML.Elem (("ASSUMPTIONS", []), map xml_of_term resasms),
1180 XML.Elem (("EVALRLS", []), [xml_of_theref thyID "Rulesets" asmrls])])
1182 | xml_of_contthy (ContRls {thyID = _, rls, applto, result, asms}) =
1183 XML.Elem (("CONTEXTDATA", []), [
1184 XML.Elem (("GUH", []), [XML.Text rls]),
1185 XML.Elem (("APPLTO", []), [xml_of_term applto]),
1186 XML.Elem (("RESULT", []), [xml_of_term result]),
1187 XML.Elem (("ASSUMPTIONS", []), map xml_of_term asms)])
1189 | xml_of_contthy (ContRlsInst {thyID = _, rls, bdvs, applto, result, asms}) =
1190 XML.Elem (("CONTEXTDATA", []), [
1191 XML.Elem (("GUH", []), [XML.Text rls]),
1192 XML.Elem (("SUBSLIST", []), [ (* should be an environment = substitution *)
1193 xml_of_cterm (subst2str' bdvs)]),
1194 XML.Elem (("INSTANTIATED", []), [xml_of_cterm (subst2str' bdvs)]),
1195 XML.Elem (("APPLTO", []), [xml_of_term applto]),
1196 XML.Elem (("RESULT", []), [xml_of_term result]),
1197 XML.Elem (("ASSUMPTIONS", []), map xml_of_term asms)])
1199 | xml_of_contthy (ContNOrew {thyID = _, thm_rls, applto}) =
1200 XML.Elem (("CONTEXTDATA", []), [
1201 XML.Elem (("GUH", []), [XML.Text thm_rls]),
1202 XML.Elem (("APPLTO", []), [xml_of_term applto])])
1204 | xml_of_contthy (ContNOrewInst{thyID = _, thm_rls, bdvs, thminst, applto}) =
1205 XML.Elem (("CONTEXTDATA", []), [
1206 XML.Elem (("GUH", []), [XML.Text thm_rls]),
1207 XML.Elem (("SUBSLIST", []), [ (* should be an environment = substitution *)
1208 xml_of_cterm (subst2str' bdvs)]),
1209 XML.Elem (("INSTANTIATED", []), [xml_of_term thminst]),
1210 XML.Elem (("APPLTO", []), [xml_of_term applto])])
1212 fun matchpbl2xml (cI:calcID) (model_ok, pI, hdl, pbl, pre) =
1213 writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
1215 " <GUH> " ^ pblID2guh pI ^ " </GUH>\n" ^
1216 " <STATUS> " ^ (if model_ok
1218 else "incorrect") ^ " </STATUS>\n" ^
1220 term2xml i hdl ^ "\n" ^
1222 model2xml i pbl pre ^
1225 fun xml_of_matchpbl (model_ok, pI, hdl, pbl, pre) =
1226 XML.Elem (("CONTEXTDATA", []), [
1227 XML.Elem (("GUH", []), [XML.Text (pblID2guh pI)]),
1228 XML.Elem (("STATUS", []), [
1229 XML.Text ((if model_ok then "correct" else "incorrect"))]),
1230 XML.Elem (("HEAD", []), [xml_of_term hdl]),
1231 xml_of_model pbl pre])
1233 fun matchmet2xml (cI:calcID) (model_ok, pI, scr, pbl, pre) =
1234 writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
1236 " <GUH> " ^ metID2guh pI ^ " </GUH>\n" ^
1237 " <STATUS> " ^ (if model_ok
1239 else "incorrect") ^ " </STATUS>\n" ^
1241 model2xml i pbl pre ^
1244 fun xml_of_matchmet (model_ok, pI, scr, pbl, pre) =
1245 XML.Elem (("CONTEXTDATA", []), [
1246 XML.Elem (("GUH", []), [XML.Text (metID2guh pI)]),
1247 XML.Elem (("STATUS", []), [
1248 XML.Text ((if model_ok then "correct" else "incorrect"))]),
1249 XML.Elem (("PROGRAM", []), [xml_of_src scr]),
1250 xml_of_model pbl pre])
1252 fun xml_of_calcchanged calcid tag old del new = (*TODO: make analogous to xml_to_calcchanged*)
1253 XML.Elem ((tag, []),[
1254 XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
1255 XML.Elem (("CALCCHANGED", []), [
1256 xml_of_pos "UNCHANGED" old,
1257 xml_of_pos "DELETED" del,
1258 xml_of_pos "GENERATED" new])])
1259 fun xml_to_calcchanged (XML.Elem (("CALCCHANGED", []), [old, del, new])) =
1260 (xml_to_pos old, xml_to_pos del, xml_to_pos new)
1261 | xml_to_calcchanged x = raise ERROR ("xml_to_calcchanged: WRONG arg = " ^ xmlstr 0 x)
1263 (* for checking output at Frontend *)
1264 fun cut_xml xml i = xml |> xmlstr 0 |> Symbol.explode |> curry take i |> implode
1265 (*------------------------------------------------------------------
1268 ------------------------------------------------------------------*)