1 (* convert sml-datatypes to xml for libisabelle and for kbase.
2 authors: Walther Neuper 2003, 2016
3 (c) due to copyright terms
6 signature DATATYPES = (*TODO: redo with xml_of/to *)
8 val authors2xml : int -> string -> string list -> Celem.xml
9 val calc2xml : int -> Rule.thyID * Rule.calc -> Celem.xml
10 val calcrefs2xml : int -> Rule.thyID * Rule.calc list -> Celem.xml
11 val contthy2xml : int -> Rtools.contthy -> Celem.xml
12 val extref2xml : int -> string -> string -> Celem.xml
14 ''a -> (''a * (Term.term * Term.term)) list -> Term.term list
15 val formula2xml : int -> Term.term -> Celem.xml
16 val formulae2xml : int -> Term.term list -> Celem.xml
18 val id2xml : int -> string list -> string
19 val ints2xml : int -> int list -> string
20 val itm_2xml : int -> Model.itm_ -> Celem.xml
21 val itms2xml : int -> (int * Model.vats * bool * string * Model.itm_) list ->
23 val keref2xml : int -> Celem.ketype -> Celem.kestoreID -> Celem.xml
25 int -> Model.itm list -> (bool * Term.term) list -> Celem.xml
26 val modspec2xml : int -> Ctree.ocalhd -> Celem.xml
29 (string * (Term.term * Term.term)) list -> Term.term list -> string
30 val pos'2xml : int -> string * (int list * Ctree.pos_) -> string
31 val pos'calchead2xml : int -> Ctree.pos' * Ctree.ocalhd -> Celem.xml
32 val pos_2xml : int -> Ctree.pos_ -> string
33 val posform2xml : int -> Ctree.pos' * Term.term -> Celem.xml
34 val posformhead2xml : int -> Ctree.pos' * Ctree.ptform -> string
35 val posformheads2xml : int -> (Ctree.pos' * Ctree.ptform) list -> Celem.xml
36 val posforms2xml : int -> (Ctree.pos' * Term.term) list -> Celem.xml
37 val posterms2xml : int -> (Ctree.pos' * term) list -> Celem.xml
38 val precond2xml : int -> bool * Term.term -> Celem.xml
39 val preconds2xml : int -> (bool * Term.term) list -> Celem.xml
40 val rls2xml : int -> Rule.thyID * Rule.rls -> Celem.xml
41 val rule2xml : int -> Celem.guh -> Rule.rule -> Celem.xml
42 val rules2xml : int -> Celem.guh -> Rule.rule list -> Celem.xml
43 val scr2xml : int -> Rule.program -> Celem.xml
44 val spec2xml : int -> Celem.spec -> Celem.xml
45 val sub2xml : int -> Term.term * Term.term -> Celem.xml
46 val subs2xml : int -> Selem.subs -> Celem.xml
47 val subst2xml : int -> Rule.subst -> Celem.xml
48 val tac2xml : int -> Tactic.input -> Celem.xml
49 val tacs2xml : int -> Tactic.input list -> Celem.xml
50 val theref2xml : int -> Rule.thyID -> string -> xstring -> string
51 val thm'2xml : int -> Celem.thm' -> Celem.xml
52 val thm''2xml : int -> thm -> Celem.xml
53 val thmstr2xml : int -> string -> Celem.xml
56 (*------------------------------------------------------------------
57 structure datatypes:DATATYPES =
58 (*structure datatypes =*)
60 ------------------------------------------------------------------*)
62 (*** convert sml-datatypes to xml for kbase ***)
63 (* NOTE: funs with siblings in xml_of_* are together with them in 'xml for libisabelle' *)
68 let fun id2x _ [] = ""
69 | id2x j (s::ss) = (indt j) ^ "<STRING> " ^ s ^ " </STRING>\n" ^
71 in (indt j) ^ "<STRINGLIST>\n" ^
72 (id2x (j + indentation) ids) ^
73 (indt j) ^ "</STRINGLIST>\n" end;
74 (* writeln(id2xml 8 ["linear","univariate","equation"]);
76 <STRING>linear</STRING>
77 <STRING>univariate</STRING>
78 <STRING>equation</STRING>
80 fun calc2xml j (thyID, (scrop, (rewop, _))) =
82 indt (j+i) ^ "<STRING>\n" ^ scrop ^ "</STRING>\n" ^
83 indt (j+i) ^ "<GUH>\n" ^ Celem.cal2guh ("IsacKnowledge",
84 thyID) scrop ^ "</GUH>\n" ^
85 indt (j+i) ^ "<TERMOP>\n" ^ rewop ^ "</TERMOP>\n" ^
87 (*replace by 'fun calc2xml' as developed for thy in 0607*)
88 fun calc2xmlOLD _ (scr_op, (isa_op, _)) =
89 indt i ^ "<CALCULATE> (" ^ scr_op ^ ", (" ^ isa_op ^ ")) </CALCULATE>\n";
90 fun calcs2xmlOLD _ [] = "" (*TODO replace with 'strs2xml'*)
91 | calcs2xmlOLD j (r::rs) = calc2xmlOLD j r ^ calcs2xmlOLD j rs;
93 (*.for creating a href for a rule within an rls's rule list;
94 the guh points to the thy of definition of the rule, NOT of use in rls.*)
95 fun rule2xml _ _ Rule.Erule =
96 error "rule2xml called with 'Erule'"
97 | rule2xml j _ (Rule.Thm (thmDeriv, _)) =
99 indt (j+i) ^ "<TAG> Theorem </TAG>\n" ^
100 indt (j+i) ^ "<STRING> " ^ Celem.thmID_of_derivation_name thmDeriv ^ " </STRING>\n" ^
101 indt (j+i) ^ "<GUH> " ^
102 Celem.thm2guh (Rtools.thy_containing_thm thmDeriv) (Celem.thmID_of_derivation_name thmDeriv) ^ " </GUH>\n" ^
104 | rule2xml _ _ (Rule.Calc (_(*termop*), _)) = ""
105 (*FIXXXXXXXME.WN060714 in rls make Calc : calc -> rule [add scriptop!]
106 see smltest/../datatypes.sml !
107 indt j ^ "<RULE>\n" ^
108 indt (j+i) ^ "<STRING> " ^ termop ^ " </STRING>\n" ^
109 indt (j+i) ^ "<GUH> " ^ cal2guh (thy_containing_cal thyID termop)
110 termop ^ " </GUH>\n" ^
113 | rule2xml _ _ (Rule.Cal1 (_(*termop*), _)) = ""
114 | rule2xml j thyID (Rule.Rls_ rls) =
115 let val rls' = (#id o Rule.rep_rls) rls
117 indt j ^ "<RULE>\n" ^
118 indt (j+i) ^ "<TAG> Ruleset </TAG>\n" ^
119 indt (j+i) ^ "<STRING> " ^ rls' ^ " </STRING>\n" ^
120 indt (j+i) ^ "<GUH> " ^ Celem.rls2guh (Rtools.thy_containing_rls thyID rls') rls' ^ " </GUH>\n" ^
123 fun rules2xml _ _ [] = ""
124 | rules2xml j thyID (r::rs) = rule2xml j thyID r ^ rules2xml j thyID rs;
128 | filt ((s, (t1, t2)) :: ps) =
129 if str = s then (t1 $ t2) :: filt ps else filt ps
131 fun pattern2xml j p where_ =
132 (case filterpbl "#Given" p of
133 [] => (indt j) ^ "<GIVEN> </GIVEN>\n"
134 (* val gis = filterpbl "#Given" p;
136 | gis => (indt j) ^ "<GIVEN>\n" ^ terms2xml' j gis ^
137 (indt j) ^ "</GIVEN>\n")
140 [] => (indt j) ^ "<WHERE> </WHERE>\n"
141 | whs => (indt j) ^ "<WHERE>\n" ^ terms2xml' j whs ^
142 (indt j) ^ "</WHERE>\n")
144 (case filterpbl "#Find" p of
145 [] => (indt j) ^ "<FIND> </FIND>\n"
146 | fis => (indt j) ^ "<FIND>\n" ^ terms2xml' j fis ^
147 (indt j) ^ "</FIND>\n")
149 (case filterpbl "#Relate" p of
150 [] => (indt j) ^ "<RELATE> </RELATE>\n"
151 | res => (indt j) ^ "<RELATE>\n" ^ terms2xml' j res ^
152 (indt j) ^ "</RELATE>\n");
154 writeln(pattern2xml 3 ((#ppc o get_pbt)
155 ["squareroot","univariate","equation","test"]) []);
158 (*url to a source external to isac*)
159 fun extref2xml j linktext url =
160 indt j ^ "<EXTREF>\n" ^
161 indt (j+i) ^ "<TEXT> " ^ linktext ^ " </TEXT>\n" ^
162 indt (j+i) ^ "<URL> " ^ url ^ " </URL>\n" ^
163 indt j ^ "</EXTREF>\n";
164 fun theref2xml j thyID typ xstring =
165 let val guh = Celem.theID2guh ["IsacKnowledge", thyID, typ, xstring]
166 val typ' = (implode o (drop_last_n 1) o Symbol.explode) typ
167 in indt j ^ "<KESTOREREF>\n" ^
168 indt (j+i) ^ "<TAG> " ^ typ' ^ " </TAG>\n" ^
169 indt (j+i) ^ "<ID> " ^ xstring ^ " </ID>\n" ^
170 indt (j+i) ^ "<GUH> " ^ guh ^ " </GUH>\n" ^
171 indt j ^ "</KESTOREREF>\n"
173 fun keref2xml j typ kestoreID =
174 let val id = strs2str' kestoreID
175 val guh = Specify.kestoreID2guh typ kestoreID
176 in indt j ^ "<KESTOREREF>\n" ^
177 indt (j+i) ^ "<TAG> " ^ Celem.ketype2str' typ ^ "</TAG>\n" ^
178 indt (j+i) ^ "<ID> " ^ id ^ " </ID>\n" ^
179 indt (j+i) ^ "<GUH> " ^ guh ^ " </GUH>\n" ^
180 indt j ^ "</KESTOREREF>\n"
182 fun authors2xml j str auts =
183 let fun autx _ [] = ""
184 | autx j (s::ss) = (indt j) ^ "<STRING> " ^ s ^ " </STRING>\n" ^
186 in indt j ^ "<"^str^">\n" ^
188 indt j ^ "</"^str^">\n"
190 (* writeln(authors2xml 2 "MATHAUTHORS" []);
191 writeln(authors2xml 2 "MATHAUTHORS"
192 ["isac-team 2001", "Richard Lang 2003"]);
194 fun scr2xml j Rule.EmptyScr =
195 indt j ^"<SCRIPT> </SCRIPT>\n"
196 | scr2xml j (Rule.Prog term) =
197 if term = Rule.e_term
198 then indt j ^"<SCRIPT> </SCRIPT>\n"
199 else indt j ^"<SCRIPT>\n"^
200 term2xml j (TermC.inst_abs term) ^ "\n" ^
201 indt j ^"</SCRIPT>\n"
202 | scr2xml j (Rule.Rfuns _) =
203 indt j ^"<REVERSREWRITE> reverse rewrite functions </REVERSREWRITE>\n";
205 fun calcref2xml j (thyID, (scrop, (_(*rewop*), _))) =
206 indt j ^ "<CALCREF>\n" ^
207 indt (j+i) ^ "<STRING> " ^ scrop ^ "</STRING>\n" ^
208 indt (j+i) ^ "<GUH> " ^ Celem.cal2guh ("IsacKnowledge",
209 thyID) scrop ^ " </GUH>\n" ^
210 indt j ^ "</CALCREF>\n";
211 fun calcrefs2xml _ (_,[]) = ""
212 | calcrefs2xml j (thyID, cal::cs) =
213 calcref2xml j (thyID, cal) ^ calcrefs2xml j (thyID, cs);
215 fun prepa12xml j (terms, term) =
216 indt j ^"<PREPAT>\n"^
217 indt (j+i) ^"<PRECONDS>\n"^
218 terms2xml (j+2*i) terms ^
219 indt (j+i) ^"</PRECONDS>\n"^
220 indt (j+i) ^"<PATTERN>\n"^
221 term2xml (j+2*i) term ^
222 indt (j+i) ^"</PATTERN>\n"^
223 indt j ^"</PREPAT>\n";
224 fun prepat2xml _ [] = ""
225 | prepat2xml j (p::ps) = prepa12xml j p ^ prepat2xml j ps;
227 fun rls2xm j (thyID, seqrls, {id, preconds, rew_ord=(ord,_), erls,
228 srls, calc, rules, errpatts, scr}) =
229 indt j ^"<RULESET>\n"^
230 indt (j+i) ^"<ID> "^ id ^" </ID>\n"^
231 indt (j+i) ^"<TYPE> "^ seqrls ^" </TYPE>\n"^
232 indt (j+i) ^"<RULES>\n" ^
233 rules2xml (j+2*i) thyID rules ^
234 indt (j+i) ^"</RULES>\n" ^
235 indt (j+i) ^"<PRECONDS> " ^
236 terms2xml' (j+2*i) preconds ^
237 indt (j+i) ^"</PRECONDS>\n" ^
238 indt (j+i) ^"<ORDER>\n" ^
239 indt (j+2*i) ^ "<STRING> " ^ ord ^ " </STRING>\n" ^
240 (*WN060714 thy_isac_*-ord-*.xml not yet generated ................
241 indt (j+2*i) ^ "<GUH> " ^ ord2guh ("IsacKnowledge",
242 thyID) ord ^ " </GUH>\n" ^
243 ..................................................................*)
244 indt (j+i) ^"</ORDER>\n" ^
245 indt (j+i) ^"<ERLS>\n" ^
246 indt (j+2*i) ^ "<TAG> Ruleset </TAG>\n" ^
247 indt (j+2*i) ^ "<STRING> " ^ Rule.id_rls erls ^ " </STRING>\n" ^
248 indt (j+2*i) ^ "<GUH> " ^ Celem.rls2guh ("IsacKnowledge", thyID)
249 (Rule.id_rls erls) ^ " </GUH>\n" ^
250 indt (j+i) ^"</ERLS>\n" ^
251 indt (j+i) ^"<SRLS>\n" ^
252 indt (j+2*i) ^ "<TAG> Ruleset </TAG>\n" ^
253 indt (j+2*i) ^ "<STRING> " ^ Rule.id_rls erls ^ " </STRING>\n" ^
254 indt (j+2*i) ^ "<GUH> " ^ Celem.rls2guh ("IsacKnowledge", thyID)
255 (Rule.id_rls srls) ^ " </GUH>\n" ^
256 indt (j+i) ^"</SRLS>\n" ^
257 calcrefs2xml (j+i) (thyID, calc) ^
259 indt j ^"</RULESET>\n";
260 fun rls2xml j (thyID, Rule.Erls) = rls2xml j (thyID, Rule.e_rls)
261 | rls2xml j (thyID, Rule.Rls data) = rls2xm j (thyID, "Rls", data)
262 | rls2xml j (thyID, Rule.Seq data) = rls2xm j (thyID, "Seq", data)
263 | rls2xml j (thyID, Rule.Rrls {id, prepat, rew_ord=(ord,_), erls, calc, errpatts, scr}) =
264 indt j ^"<RULESET>\n"^
265 indt (j+i) ^"<ID> "^ id ^" </ID>\n"^
266 indt (j+i) ^"<TYPE> Rrls </TYPE>\n"^
267 prepat2xml (j+i) prepat ^
268 indt (j+i) ^"<ORDER> " ^
269 indt (j+2*i) ^ "<TAG> Rewrite order </TAG>\n" ^
270 indt (j+2*i) ^ "<STRING> " ^ ord ^ " </STRING>\n" ^
271 (*WN060714 thy_isac_*-ord-*.xml not yet generated ................
272 indt (j+2*i) ^ "<GUH> " ^ ord2guh ("IsacKnowledge",
273 thyID) ord ^ " </GUH>\n" ^
274 .................................................................*)
275 indt (j+i) ^"</ORDER>\n" ^
276 indt (j+i) ^"<ERLS> " ^
277 indt (j+2*i) ^ "<TAG> Ruleset </TAG>\n" ^
278 indt (j+2*i) ^ "<STRING> " ^ Rule.id_rls erls ^ " </STRING>\n" ^
279 indt (j+2*i) ^ "<GUH> " ^ Celem.rls2guh ("IsacKnowledge", thyID) (Rule.id_rls erls) ^ " </GUH>\n" ^
280 indt (j+i) ^"</ERLS>\n" ^
281 calcrefs2xml (j+i) (thyID, calc) ^
282 indt (j+i) ^"<SCRIPT>\n"^
283 scr2xml (j+2*i) scr ^
284 indt (j+i) ^" </SCRIPT>\n"^
285 indt j ^"</RULESET>\n";
287 (*** convert sml-datatypes to xml for libisabelle ***)
289 (** general types: lists, **)
291 fun xml_of_bool b = XML.Elem (("BOOL", []), [XML.Text (bool2str b)])
292 fun xml_to_bool (XML.Elem (("BOOL", []), [XML.Text b])) = string_to_bool b
293 | xml_to_bool tree = raise ERROR ("xml_to_bool: wrong XML.tree \n" ^ xmlstr 0 tree)
295 fun xml_to_ketype (XML.Elem (("KETYPE", []), [XML.Text str])) = Celem.str2ketype' str
296 | xml_to_ketype tree = raise ERROR ("xml_to_ketype: wrong XML.tree \n" ^ xmlstr 0 tree)
298 fun xml_of_str str = XML.Elem (("STRING", []), [XML.Text str])
299 fun xml_of_strs strs = XML.Elem (("STRINGLIST", []), map xml_of_str strs)
301 fun xml_to_str (XML.Elem (("STRING", []), [XML.Text str])) = str
302 | xml_to_str tree = raise ERROR ("xml_to_str: wrong XML.tree \n" ^ xmlstr 0 tree)
303 fun xml_to_strs (XML.Elem (("STRINGLIST", []), strs)) = map xml_to_str strs
304 | xml_to_strs tree = raise ERROR ("xml_to_strs: wrong XML.tree \n" ^ xmlstr 0 tree)
306 fun xml_of_int i = XML.Elem (("INT", []), [XML.Text (string_of_int i)])
308 XML.Elem (("INTLIST", []), map xml_of_int is)
310 fun xml_to_int (XML.Elem (("INT", []), [XML.Text i])) =
311 (case TermC.int_of_str_opt i of SOME i => i | _ => error "xml_to_int: int_of_str \<Rightarrow> NONE")
312 | xml_to_int tree = raise ERROR ("xml_to_int: wrong XML.tree \n" ^ xmlstr 0 tree)
313 fun xml_to_ints (XML.Elem (("INTLIST", []), is)) = map xml_to_int is
314 | xml_to_ints tree = raise ERROR ("xml_to_ints: wrong XML.tree \n" ^ xmlstr 0 tree)
316 (** isac datatypes **)
317 fun xml_of_pos tag (is, pp) =
318 XML.Elem ((tag, []), [
320 XML.Elem (("POS", []), [XML.Text (Ctree.pos_2str pp)])])
321 fun xml_to_pos_ (XML.Elem (("POS", []), [XML.Text pp])) = Ctree.str2pos_ pp
322 | xml_to_pos_ tree = raise ERROR ("xml_to_pos_: wrong XML.tree \n" ^ xmlstr 0 tree)
323 fun xml_to_pos (XML.Elem (("POSITION", []), [is, pp])) = (xml_to_ints is, xml_to_pos_ pp) (*: pos'*)
324 | xml_to_pos tree = raise ERROR ("xml_to_pos: wrong XML.tree \n" ^ xmlstr 0 tree)
326 fun xml_of_auto (Solve.Step i) =
327 XML.Elem (("AUTO", []), [XML.Text "Step", XML.Text (string_of_int i)])
328 | xml_of_auto CompleteModel = XML.Elem (("AUTO", []), [XML.Text "CompleteModel"])
329 | xml_of_auto CompleteCalcHead = XML.Elem (("AUTO", []), [XML.Text "CompleteCalcHead"])
330 | xml_of_auto CompleteToSubpbl = XML.Elem (("AUTO", []), [XML.Text "CompleteToSubpbl"])
331 | xml_of_auto CompleteSubpbl = XML.Elem (("AUTO", []), [XML.Text "CompleteSubpbl"])
332 | xml_of_auto CompleteCalc = XML.Elem (("AUTO", []), [XML.Text "CompleteCalc"])
333 fun xml_to_auto (XML.Elem (("AUTO", []), [
334 XML.Elem (("STEP", []), [XML.Text i])])) = Solve.Step (TermC.int_of_str_opt i |> the)
335 | xml_to_auto (XML.Elem (("AUTO", []), [XML.Text "CompleteModel"])) = Solve.CompleteModel
336 | xml_to_auto (XML.Elem (("AUTO", []), [XML.Text "CompleteCalcHead"])) = Solve.CompleteCalcHead
337 | xml_to_auto (XML.Elem (("AUTO", []), [XML.Text "CompleteToSubpbl"])) = Solve.CompleteToSubpbl
338 | xml_to_auto (XML.Elem (("AUTO", []), [XML.Text "CompleteSubpbl"])) = Solve.CompleteSubpbl
339 | xml_to_auto (XML.Elem (("AUTO", []), [XML.Text "CompleteCalc"])) = Solve.CompleteCalc
340 | xml_to_auto tree = raise ERROR ("xml_to_auto: wrong XML.tree \n" ^ xmlstr 0 tree)
344 | filt ((s, (t1, t2)) :: ps) =
345 if str = s then (t1 $ t2) :: filt ps else filt ps
348 fun xml_of_itm_ (Model.Cor (dts, _)) =
349 XML.Elem (("ITEM", [("status", "correct")]), [xml_of_term (Model.comp_dts' dts)])
350 | xml_of_itm_ (Model.Syn c) =
351 XML.Elem (("ITEM", [("status", "syntaxerror")]), [XML.Text c])
352 | xml_of_itm_ (Model.Typ c) =
353 XML.Elem (("ITEM", [("status", "typeerror")]), [XML.Text c])
354 (*type item also has 'False of cterm' set in preconds2xml WN 050618*)
355 | xml_of_itm_ (Model.Inc (dts, _)) =
356 XML.Elem (("ITEM", [("status", "incomplete")]), [xml_of_term (Model.comp_dts' dts)])
357 | xml_of_itm_ (Model.Sup dts) =
358 XML.Elem (("ITEM", [("status", "superfluous")]), [xml_of_term (Model.comp_dts' dts)])
359 | xml_of_itm_ (Model.Mis (d, pid)) =
360 XML.Elem (("ITEM", [("status", "missing")]), [xml_of_term (d $ pid)])
361 | xml_of_itm_ _ = error "xml_of_itm_: wrong argument"
362 fun xml_of_itms itms =
364 fun extract (_, _, _, _, itm_) = itm_
365 | extract _ = error "xml_of_itms.extract: wrong argument"
366 in map (xml_of_itm_ o extract) itms end
368 fun xml_of_precond (status, term) =
369 XML.Elem (("ITEM", [("status", if status then "correct" else "false")]), [xml_of_term term])
370 fun xml_of_preconds ps = map xml_of_precond ps
372 fun xml_of_model itms where_ =
374 fun eq str (_, _, _,field, _) = str = field
376 XML.Elem (("MODEL", []), [
377 XML.Elem (("GIVEN", []),
378 filter (eq "#Given") itms |> xml_of_itms),
379 XML.Elem (("WHERE", []),
380 xml_of_preconds where_),
381 XML.Elem (("FIND", []),
382 filter (eq "#Find") itms |> xml_of_itms),
383 XML.Elem (("RELATE", []),
384 filter (eq "#Relate") itms |> xml_of_itms)])
387 fun xml_of_spec (thyID, pblID, metID) =
388 XML.Elem (("SPECIFICATION", []), [
389 XML.Elem (("THEORYID", []), [XML.Text thyID]),
390 XML.Elem (("PROBLEMID", []), [xml_of_strs pblID]),
391 XML.Elem (("METHODID", []), [xml_of_strs metID])])
392 fun xml_to_spec (XML.Elem (("SPECIFICATION", []), [
393 XML.Elem (("THEORYID", []), [XML.Text thyID]),
394 XML.Elem (("PROBLEMID", []), [ps]),
395 XML.Elem (("METHODID", []), [ms])])) = (thyID, xml_to_strs ps, xml_to_strs ms)
396 | xml_to_spec tree = raise ERROR ("xml_to_spec: wrong XML.tree \n" ^ xmlstr 0 tree)
398 fun xml_of_variant (items, spec) =
399 XML.Elem (("VARIANT", []), [xml_of_strs items, xml_of_spec spec])
400 fun xml_to_variant (XML.Elem (("VARIANT", []), [items, spec])) =
401 (xml_to_strs items, xml_to_spec spec)
402 | xml_to_variant tree = raise ERROR ("xml_to_variant: wrong XML.tree \n" ^ xmlstr 0 tree)
404 fun xml_of_fmz [] = xml_of_fmz [Selem.e_fmz]
405 | xml_of_fmz vs = XML.Elem (("FORMALIZATION", []), map xml_of_variant vs)
406 fun xml_to_fmz (XML.Elem (("FORMALIZATION", []), vars)) = map xml_to_variant vars
407 | xml_to_fmz tree = raise ERROR ("xml_to_fmz: wrong XML.tree \n" ^ xmlstr 0 tree)
409 fun xml_of_modspec ((b, p_, head, gfr, pre, spec): Ctree.ocalhd) =
410 XML.Elem (("CALCHEAD", [("status", if b then "correct" else "incorrect")]), [
411 XML.Elem (("HEAD", []), [xml_of_term_NEW head]),
412 xml_of_model gfr pre,
413 XML.Elem (("BELONGSTO", []), [
414 XML.Text (case p_ of Pbl => "Pbl" | Met => "Met" | _ => "Und")]),
417 fun xml_of_posmodspec ((p: Ctree.pos', (b, p_, head, gfr, pre, spec): Ctree.ocalhd)) =
418 XML.Elem (("CALCHEAD", [("status", if b then "correct" else "incorrect")]), [
419 xml_of_pos "POSITION" p,
420 XML.Elem (("HEAD", []), [xml_of_term_NEW head]),
421 xml_of_model gfr pre,
422 XML.Elem (("BELONGSTO", []), [
423 XML.Text (case p_ of Pbl => "Pbl" | Met => "Met" | _ => "Und")]),
426 (XML.Elem (("IMODEL", []), [
427 XML.Elem (("GIVEN", []), givens),
428 (*XML.Elem (("WHERE", []), wheres), ... Where is never input*)
429 XML.Elem (("FIND", []), finds),
430 XML.Elem (("RELATE", []), relates)])) =
431 ([Inform.Given (map xml_to_cterm givens),
432 Inform.Find (map xml_to_cterm finds),
433 Inform.Relate (map xml_to_cterm relates)]) : Inform.imodel
434 | xml_to_imodel x = raise ERROR ("xml_to_imodel: WRONG arg = " ^ xmlstr 0 x)
436 (XML.Elem (( "ICALCHEAD", []), [
437 pos as XML.Elem (( "POSITION", []), _),
438 XML.Elem (( "HEAD", []), [form]),
439 imodel as XML.Elem (("MATHML", []), _), (* TODO WN150813 ?!?*)
440 XML.Elem (( "POS", []), [XML.Text belongsto]),
441 spec as XML.Elem (( "SPECIFICATION", []), _)])) =
442 (xml_to_pos pos, xml_to_term_NEW form |> Rule.term2str, xml_to_imodel imodel,
443 Ctree.str2pos_ belongsto, xml_to_spec spec) : Inform.icalhd
444 | xml_to_icalhd x = raise ERROR ("xml_to_icalhd: WRONG arg = " ^ xmlstr 0 x)
446 fun xml_of_sub (id, value) =
447 XML.Elem (("PAIR", []), [
448 XML.Elem (("VARIABLE", []), [xml_of_term id]),
449 XML.Elem (("VALUE", []), [xml_of_term value])])
451 (XML.Elem (("PAIR", []), [
452 XML.Elem (("VARIABLE", []), [id]),
453 XML.Elem (("VALUE", []), [value])])) = (xml_to_term id, xml_to_term value)
454 | xml_to_sub x = raise ERROR ("xml_to_sub wrong arg: " ^ xmlstr 0 x)
455 fun xml_of_subs (subs : Selem.subs) =
456 XML.Elem (("SUBSTITUTION", []), map xml_of_sub (Selem.subs2subst (Celem.assoc_thy "Isac") subs))
458 (XML.Elem (("SUBSTITUTION", []),
459 subs)) = Selem.subst2subs (map xml_to_sub subs)
460 | xml_to_subs x = raise ERROR ("xml_to_subs wrong arg: " ^ xmlstr 0 x)
461 fun xml_of_sube sube =
462 XML.Elem (("SUBSTITUTION", []), map xml_of_sub (Selem.sube2subst (Celem.assoc_thy "Isac") sube))
464 (XML.Elem (("SUBSTITUTION", []),
465 xml_var_val_pairs)) = Selem.subst2sube (map xml_to_sub xml_var_val_pairs)
466 | xml_to_sube x = raise ERROR ("xml_to_sube wrong arg: " ^ xmlstr 0 x)
468 fun thm''2xml j (thm : thm) =
469 indt j ^ "<THEOREM>\n" ^
470 indt (j+i) ^ "<ID> " ^ Celem.thmID_of_derivation_name' thm ^ " </ID>\n"^
471 term2xml j (Thm.prop_of thm) ^ "\n" ^
472 indt j ^ "</THEOREM>\n";
473 fun xml_of_thm' (ID, form) =
474 XML.Elem (("THEOREM", []), [
475 XML.Elem (("ID", []), [XML.Text ID]),
476 XML.Elem (("FORMULA", []), [
477 XML.Text form])]) (* repair for MathML: use term instead String *)
478 (* at the front-end theorems can be shown by their term, so term is transported isac-java <--- ME *)
479 fun xml_of_thm'' (ID, thm) =
480 (*---xml_of_thm''------------------------------------------thm'_to_thm''--------------
481 XML.Elem (("THEOREM", []), [
482 XML.Elem (("ID", []), [XML.Text ID]),
483 xml_of_term_NEW term])
484 -----xml_of_thm''------------------------------------------thm'_to_thm''------------*)
485 XML.Elem (("THEOREM", []), [
486 XML.Elem (("ID", []), [XML.Text ID]),
487 XML.Elem (("FORMULA", []), [
488 XML.Text ((Rule.term2str o Thm.prop_of) thm)])]) (* repair for MathML: use term instead String *)
491 (XML.Elem (("THEOREM", []), [
492 XML.Elem (("ID", []), [XML.Text ID]),
493 XML.Elem (("FORMULA", []), [XML.Text "NO_ad_hoc_thm_FROM_FRONTEND = True"])])) =
494 (ID, "NO_ad_hoc_thm_FROM_GUI = True")
495 | xml_to_thm' x = raise ERROR ("xml_of_thm' wrong arg:\n" ^ xmlstr 0 x)
496 (* at the front-end theorems are identified only by their name, so NO isac-java \<longrightarrow> ME *)
498 (*---xml_of_thm''------------------------------------------thm'_to_thm''--------------
499 (XML.Elem (("THEOREM", []), [
500 XML.Elem (("ID", []), [XML.Text ID]),
502 (ID, xml_to_term_NEW xterm) : thm''
503 | xml_to_thm'' x = raise ERROR ("xml_to_thm'' wrong arg:\n" ^ xmlstr 0 x)
504 -----xml_of_thm''------------------------------------------thm'_to_thm''------------*)
505 (XML.Elem (("THEOREM", []), [
506 XML.Elem (("ID", []), [XML.Text ID]),
507 XML.Elem (("FORMULA", []), [
508 XML.Text term])])) = (ID, Rewrite.assoc_thm'' (Rule.Isac ()) ID)
509 | xml_to_thm'' x = raise ERROR ("xml_of_thm' wrong arg:" ^ xmlstr 0 x)
511 fun xml_of_src Rule.EmptyScr =
512 XML.Elem (("NOCODE", []), [XML.Text "empty"])
513 | xml_of_src (Rule.Prog term) =
514 XML.Elem (("CODE", []), [
515 if term = Rule.e_term then xml_of_src Rule.EmptyScr
516 else xml_of_term (TermC.inst_abs term)])
517 | xml_of_src (Rule.Rfuns _) =
518 XML.Elem (("NOCODE", []), [XML.Text "reverse rewrite functions"])
520 (*.convert a tactic into xml-format .*)
521 fun xml_of_tac (Tactic.Subproblem (dI, pI)) =
522 XML.Elem (("SUBPROBLEMTACTIC", [("name", "Subproblem")]), [
523 XML.Elem (("THEORY", []), [XML.Text dI]),
524 XML.Elem (("PROBLEM", []), [xml_of_strs pI])])
525 | xml_of_tac (Tactic.Substitute cterms) =
526 (*Substitute: sube -> tac; e_sube: cterm' list; UNCLEAR HOW TO INPUT ON FRONTEND*)
527 XML.Elem (("STRINGLISTTACTIC", [("name", "Substitute")]), [xml_of_sube cterms])
528 (*----- Rewrite* -----------------------------------------------------*)
529 | xml_of_tac (Tactic.Rewrite thm'') =
530 XML.Elem (("REWRITETACTIC", [("name", "Rewrite")]), [xml_of_thm'' thm''])
531 | xml_of_tac (Tactic.Rewrite_Inst (subs, thm'')) =
532 XML.Elem (("REWRITEINSTTACTIC", [("name", "Rewrite_Inst")]), (
534 xml_of_thm'' thm'' :: []))
535 | xml_of_tac (Tactic.Rewrite_Set rls') =
536 XML.Elem (("REWRITESETTACTIC", [("name", "Rewrite_Set")]), [XML.Text rls'])
537 | xml_of_tac (Tactic.Rewrite_Set_Inst (subs, rls')) =
538 XML.Elem (("REWRITESETINSTTACTIC", [("name", "Rewrite_Set_Inst")]), ([
540 XML.Elem (("RULESET", []), [XML.Text rls'])]))
541 (*----- FORMTACTIC ---------------------------------------------------*)
542 | xml_of_tac (Tactic.Add_Find ct) =
543 XML.Elem (("FORMTACTIC", [("name", "Add_Find")]), [xml_of_cterm ct])
544 | xml_of_tac (Tactic.Add_Given ct) =
545 XML.Elem (("FORMTACTIC", [("name", "Add_Given")]), [xml_of_cterm ct])
546 | xml_of_tac (Tactic.Add_Relation ct) =
547 XML.Elem (("FORMTACTIC", [("name", "Add_Relation")]), [xml_of_cterm ct])
548 | xml_of_tac (Tactic.Check_elementwise ct) =
549 XML.Elem (("FORMTACTIC", [("name", "Check_elementwise")]), [xml_of_cterm ct])
550 | xml_of_tac (Tactic.Take ct) =
551 XML.Elem (("FORMTACTIC", [("name", "Take")]), [xml_of_cterm ct])
552 (*----- SIMPLETACTIC -------------------------------------------------*)
553 | xml_of_tac (Tactic.Calculate opstr) =
554 XML.Elem (("SIMPLETACTIC", [("name", "Calculate")]), [XML.Text opstr])
555 | xml_of_tac (Tactic.Or_to_List) =
556 XML.Elem (("SIMPLETACTIC", [("name", "Or_to_List")]), [(*//////////*)])
557 | xml_of_tac (Tactic.Specify_Theory ct) =
558 XML.Elem (("SIMPLETACTIC", [("name", "Specify_Theory")]), [XML.Text ct])
559 (*----- STRINGLISTTACTIC ---------------------------------------------*)
560 | xml_of_tac (Tactic.Apply_Method mI) =
561 XML.Elem (("STRINGLISTTACTIC", [("name", "Apply_Method")]), [xml_of_strs mI])
562 | xml_of_tac (Tactic.Check_Postcond pI) =
563 XML.Elem (("STRINGLISTTACTIC", [("name", "Check_Postcond")]), [xml_of_strs pI])
564 | xml_of_tac Model_Problem =
565 XML.Elem (("STRINGLISTTACTIC", [("name", "Model_Problem")]), [])
566 | xml_of_tac (Tactic.Refine_Tacitly pI) =
567 XML.Elem (("STRINGLISTTACTIC", [("name", "Refine_Tacitly")]), [xml_of_strs pI])
568 | xml_of_tac (Tactic.Specify_Method ct) =
569 XML.Elem (("STRINGLISTTACTIC", [("name", "Specify_Method")]), [xml_of_strs ct])
570 | xml_of_tac (Tactic.Specify_Problem ct) =
571 XML.Elem (("STRINGLISTTACTIC", [("name", "Specify_Problem")]), [xml_of_strs ct])
572 | xml_of_tac tac = raise ERROR ("xml_of_tac: not impl. for " ^ Tactic.tac2str tac);
575 (XML.Elem (("SUBPROBLEMTACTIC", [("name", "Subproblem")]), [
576 XML.Elem (("THEORY", []), [XML.Text dI]),
577 XML.Elem (("PROBLEM", []), [pI])])) = Tactic.Subproblem (dI, xml_to_strs pI)
579 (*Substitute: sube -> tac; e_sube: cterm' list; UNCLEAR HOW TO INPUT ON FRONTEND*)
580 (XML.Elem (("STRINGLISTTACTIC", [
581 ("name", "Substitute")]), [cterms])) = Tactic.Substitute (xml_to_sube cterms)
582 (*----- Rewrite* -----------------------------------------------------*)
584 (XML.Elem (("REWRITETACTIC", [
585 ("name", "Rewrite")]), [thm])) = Tactic.Rewrite (xml_to_thm'' thm)
587 (XML.Elem (("REWRITEINSTTACTIC", [
588 ("name", "Rewrite_Inst")]), [
589 subs, thm])) = Tactic.Rewrite_Inst (xml_to_subs subs, xml_to_thm'' thm)
591 (XML.Elem (("REWRITESETTACTIC", [
592 ("name", "Rewrite_Set")]), [XML.Text rls'])) = Tactic.Rewrite_Set (rls')
594 (XML.Elem (("REWRITESETINSTTACTIC", [
595 ("name", "Rewrite_Set_Inst")]), [
597 XML.Elem (("RULESET", []), [XML.Text rls'])])) = Tactic.Rewrite_Set_Inst (xml_to_subs subs, rls')
598 (*----- FORMTACTIC ---------------------------------------------------*)
600 (XML.Elem (("FORMTACTIC", [
601 ("name", "Add_Find")]), [ct])) = Tactic.Add_Find (xml_to_cterm ct)
603 (XML.Elem (("FORMTACTIC", [
604 ("name", "Add_Given")]), [ct])) = Tactic.Add_Given (xml_to_cterm ct)
606 (XML.Elem (("FORMTACTIC", [
607 ("name", "Add_Relation")]), [ct])) = Tactic.Add_Relation (xml_to_cterm ct)
609 (XML.Elem (("FORMTACTIC", [
610 ("name", "Take")]), [ct])) = Tactic.Take (xml_to_cterm ct)
612 (XML.Elem (("FORMTACTIC", [
613 ("name", "Check_elementwise")]), [ct])) = Tactic.Check_elementwise (xml_to_cterm ct)
614 (*----- SIMPLETACTIC -------------------------------------------------*)
616 (XML.Elem (("SIMPLETACTIC", [
617 ("name", "Calculate")]), [XML.Text opstr])) = Tactic.Calculate opstr
619 (XML.Elem (("SIMPLETACTIC", [("name", "Or_to_List")]), [])) = Tactic.Or_to_List
621 (XML.Elem (("SIMPLETACTIC", [
622 ("name", "Specify_Theory")]), [XML.Text ct])) = Tactic.Specify_Theory ct
623 (*----- STRINGLISTTACTIC ---------------------------------------------*)
625 (XML.Elem (("STRINGLISTTACTIC", [
626 ("name", "Apply_Method")]), [mI])) = Tactic.Apply_Method (xml_to_strs mI)
628 (XML.Elem (("STRINGLISTTACTIC", [
629 ("name", "Check_Postcond")]), [pI])) = Tactic.Check_Postcond (xml_to_strs pI)
631 (XML.Elem (("STRINGLISTTACTIC", [
632 ("name", "Model_Problem")]), [])) = Tactic.Model_Problem
634 (XML.Elem (("STRINGLISTTACTIC", [
635 ("name", "Refine_Tacitly")]), [pI])) = Tactic.Refine_Tacitly (xml_to_strs pI)
637 (XML.Elem (("STRINGLISTTACTIC", [
638 ("name", "Specify_Method")]), [ct])) = Tactic.Specify_Method (xml_to_strs ct)
640 (XML.Elem (("STRINGLISTTACTIC", [
641 ("name", "Specify_Problem")]), [ct])) = Tactic.Specify_Problem (xml_to_strs ct)
642 | xml_to_tac x = raise ERROR ("xml_to_tac: not impl. for " ^ xmlstr 0 x);
644 val e_pblterm = (Thm.term_of o the o (TermC.parse @{theory Program}))
645 ("Problem (" ^ Rule.e_domID ^ "," ^ strs2str' Celem.e_pblID ^ ")");
647 (*WN051224 minimal adaption to exporting Formulae _only_ by getFormulaeFromTo*)
648 fun xml_of_posterm (p, t, _) =
649 let val input_request = Free ("________________________________________________", dummyT)
651 XML.Elem (("CALCFORMULA", []),
652 [xml_of_pos "POSITION" p,
653 if t = e_pblterm (*headline in pbl is e_ <- _root_pbl for CAS-command*)
654 then xml_of_term_NEW input_request
655 else xml_of_term_NEW t])
658 fun xml_of_asm_val (asm, vl) =
659 XML.Elem (("ASMEVALUATED", []),[
660 XML.Elem (("ASM", []), [xml_of_term asm]),
661 XML.Elem (("VALUE", []), [xml_of_term vl])])
663 (*.a reference to an element in the theory hierarchy;
664 compare 'fun keref2xml'.*)
665 (* val (j, thyID, typ, xstring) =
666 (i+i, snd (thy_containing_rls thy' prls'), "Rulesets", prls');
668 fun theref2xml j thyID typ xstring =
669 let val guh = Celem.theID2guh ["IsacKnowledge", thyID, typ, xstring]
670 val typ' = (implode o (drop_last_n 1) o Symbol.explode) typ
671 in indt j ^ "<KESTOREREF>\n" ^
672 indt (j+i) ^ "<TAG> " ^ typ' ^ " </TAG>\n" ^
673 indt (j+i) ^ "<ID> " ^ xstring ^ " </ID>\n" ^
674 indt (j+i) ^ "<GUH> " ^ guh ^ " </GUH>\n" ^
675 indt j ^ "</KESTOREREF>\n"
677 fun xml_of_theref thyid typ xstring =
679 val guh = Celem.theID2guh ["IsacKnowledge", thyid, typ, xstring]
680 val typ' = (implode o (drop_last_n 1) o Symbol.explode) typ
682 XML.Elem (("KESTOREREF", []),[
683 XML.Elem (("TAG", []), [XML.Text typ']),
684 XML.Elem (("ID", []), [XML.Text xstring]),
685 XML.Elem (("GUH", []), [XML.Text guh])])
688 fun xml_of_contthy Rtools.EContThy =
689 error "contthy2xml called with EContThy"
691 | xml_of_contthy (Rtools.ContThm {thyID, thm, applto, applat, reword,
692 asms,lhs, rhs, result, resasms, asmrls}) =
693 XML.Elem (("CONTEXTDATA", []), [
694 XML.Elem (("GUH", []), [XML.Text thm]),
695 XML.Elem (("APPLTO", []), [xml_of_term applto]),
696 XML.Elem (("APPLAT", []), [xml_of_term applat]),
697 XML.Elem (("ORDER", []), [ (* should be a theref2xml *)
698 XML.Elem (("ID", []), [XML.Text reword])]),
699 XML.Elem (("ASMSEVAL", []), map xml_of_asm_val asms),
700 XML.Elem (("LHS", []), [xml_of_term (fst lhs)]),
701 XML.Elem (("LHSINST", []), [xml_of_term (snd lhs)]),
702 XML.Elem (("RHS", []), [xml_of_term (fst rhs)]),
703 XML.Elem (("RHSINST", []), [xml_of_term (snd rhs)]),
704 XML.Elem (("RESULT", []), [xml_of_term result]),
705 XML.Elem (("ASSUMPTIONS", []), map xml_of_term resasms),
706 XML.Elem (("EVALRLS", []), [xml_of_theref thyID "Rulesets" asmrls])])
708 | xml_of_contthy (Rtools.ContThmInst {thyID, thm, bdvs, thminst, applto, applat,
709 reword, asms, lhs, rhs, result, resasms, asmrls}) =
710 XML.Elem (("CONTEXTDATA", []), [
711 XML.Elem (("GUH", []), [XML.Text thm]),
712 XML.Elem (("SUBSLIST", []), [ (* should be an environment = substitution *)
713 xml_of_cterm (Celem.subst2str' bdvs)]),
714 XML.Elem (("INSTANTIATED", []), [xml_of_term thminst]),
715 XML.Elem (("APPLTO", []), [xml_of_term applto]),
716 XML.Elem (("APPLAT", []), [xml_of_term applat]),
717 XML.Elem (("ORDER", []), [ (* should be a theref2xml *)
718 XML.Elem (("ID", []), [XML.Text reword])]),
719 XML.Elem (("ASMSEVAL", []), map xml_of_asm_val asms),
720 XML.Elem (("LHS", []), [xml_of_term (fst lhs)]),
721 XML.Elem (("LHSINST", []), [xml_of_term (snd lhs)]),
722 XML.Elem (("RHS", []), [xml_of_term (fst rhs)]),
723 XML.Elem (("RHSINST", []), [xml_of_term (snd rhs)]),
724 XML.Elem (("RESULT", []), [xml_of_term result]),
725 XML.Elem (("ASSUMPTIONS", []), map xml_of_term resasms),
726 XML.Elem (("EVALRLS", []), [xml_of_theref thyID "Rulesets" asmrls])])
728 | xml_of_contthy (Rtools.ContRls {thyID = _, rls, applto, result, asms}) =
729 XML.Elem (("CONTEXTDATA", []), [
730 XML.Elem (("GUH", []), [XML.Text rls]),
731 XML.Elem (("APPLTO", []), [xml_of_term applto]),
732 XML.Elem (("RESULT", []), [xml_of_term result]),
733 XML.Elem (("ASSUMPTIONS", []), map xml_of_term asms)])
735 | xml_of_contthy (Rtools.ContRlsInst {thyID = _, rls, bdvs, applto, result, asms}) =
736 XML.Elem (("CONTEXTDATA", []), [
737 XML.Elem (("GUH", []), [XML.Text rls]),
738 XML.Elem (("SUBSLIST", []), [ (* should be an environment = substitution *)
739 xml_of_cterm (Celem.subst2str' bdvs)]),
740 XML.Elem (("INSTANTIATED", []), [xml_of_cterm (Celem.subst2str' bdvs)]),
741 XML.Elem (("APPLTO", []), [xml_of_term applto]),
742 XML.Elem (("RESULT", []), [xml_of_term result]),
743 XML.Elem (("ASSUMPTIONS", []), map xml_of_term asms)])
745 | xml_of_contthy (Rtools.ContNOrew {thyID = _, thm_rls, applto}) =
746 XML.Elem (("CONTEXTDATA", []), [
747 XML.Elem (("GUH", []), [XML.Text thm_rls]),
748 XML.Elem (("APPLTO", []), [xml_of_term applto])])
750 | xml_of_contthy (Rtools.ContNOrewInst{thyID = _, thm_rls, bdvs, thminst, applto}) =
751 XML.Elem (("CONTEXTDATA", []), [
752 XML.Elem (("GUH", []), [XML.Text thm_rls]),
753 XML.Elem (("SUBSLIST", []), [ (* should be an environment = substitution *)
754 xml_of_cterm (Celem.subst2str' bdvs)]),
755 XML.Elem (("INSTANTIATED", []), [xml_of_term thminst]),
756 XML.Elem (("APPLTO", []), [xml_of_term applto])])
758 fun xml_of_matchpbl (model_ok, pI, hdl, pbl, pre) =
759 XML.Elem (("CONTEXTDATA", []), [
760 XML.Elem (("GUH", []), [XML.Text (Specify.pblID2guh pI)]),
761 XML.Elem (("STATUS", []), [
762 XML.Text ((if model_ok then "correct" else "incorrect"))]),
763 XML.Elem (("HEAD", []), [xml_of_term_NEW hdl]),
764 xml_of_model pbl pre])
766 fun xml_of_matchmet (model_ok, pI, scr, pbl, pre) =
767 XML.Elem (("CONTEXTDATA", []), [
768 XML.Elem (("GUH", []), [XML.Text (Specify.metID2guh pI)]),
769 XML.Elem (("STATUS", []), [
770 XML.Text ((if model_ok then "correct" else "incorrect"))]),
771 XML.Elem (("PROGRAM", []), [xml_of_src scr]),
772 xml_of_model pbl pre])
774 fun xml_of_calcchanged calcid tag old del new = (*TODO: make analogous to xml_to_calcchanged*)
775 XML.Elem ((tag, []),[
776 XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
777 XML.Elem (("CALCCHANGED", []), [
778 xml_of_pos "UNCHANGED" old,
779 xml_of_pos "DELETED" del,
780 xml_of_pos "GENERATED" new])])
781 fun xml_to_calcchanged (XML.Elem (("CALCCHANGED", []), [old, del, new])) =
782 (xml_to_pos old, xml_to_pos del, xml_to_pos new)
783 | xml_to_calcchanged x = raise ERROR ("xml_to_calcchanged: WRONG arg = " ^ xmlstr 0 x)
785 (* for checking output at Frontend *)
786 fun cut_xml xml i = xml |> xmlstr 0 |> Symbol.explode |> curry take i |> implode
787 (*------------------------------------------------------------------
790 ------------------------------------------------------------------*)