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