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 -> ThyC.id * Rule_Def.calc -> xml
10 val calcrefs2xml : int -> ThyC.id * Rule_Def.calc list -> xml
11 val extref2xml : int -> string -> string -> xml
13 ''a -> (''a * (Term.term * Term.term)) list -> Term.term list
14 val formula2xml : int -> Term.term -> xml
15 val formulae2xml : int -> Term.term list -> xml
17 val id2xml : int -> string list -> string
18 val ints2xml : int -> int list -> string
19 val itm_2xml : int -> I_Model.feedback -> xml
20 val itms2xml : int -> I_Model.T -> string
21 val keref2xml : int -> Ptool.ketype -> Ptool.kestoreID -> xml
23 int -> I_Model.T -> (bool * Term.term) list -> xml
24 val modspec2xml : int -> SpecificationC.T -> xml
25 val pattern2xml : int -> Model_Pattern.T -> Term.term list -> string
26 val pos'2xml : int -> string * Pos.pos' -> string
27 val pos'calchead2xml : int -> Pos.pos' * SpecificationC.T -> xml
28 val pos_2xml : int -> Pos.pos_ -> string
29 val posform2xml : int -> Pos.pos' * Term.term -> xml
30 val posformhead2xml : int -> Pos.pos' * Ctree.ptform -> string
31 val posformheads2xml : int -> (Pos.pos' * Ctree.ptform) list -> xml
32 val posforms2xml : int -> (Pos.pos' * Term.term) list -> xml
33 val posterms2xml : int -> (Pos.pos' * term) list -> xml
34 val precond2xml : int -> bool * Term.term -> xml
35 val preconds2xml : int -> (bool * Term.term) list -> xml
36 val rls2xml : int -> ThyC.id * Rule_Set.T -> xml
37 val rule2xml : int -> Check_Unique.id -> Rule.rule -> xml
38 val rules2xml : int -> Check_Unique.id -> Rule.rule list -> xml
39 val scr2xml : int -> Program.T -> xml
40 val spec2xml : int -> References.T -> xml
41 val sub2xml : int -> Term.term * Term.term -> xml
42 val subs2xml : int -> Subst.input -> xml
43 val subst2xml : int -> subst -> xml
44 val tac2xml : int -> Tactic.input -> xml
45 val tacs2xml : int -> Tactic.input list -> xml
46 val theref2xml : int -> ThyC.id -> string -> xstring -> string
47 val thm''2xml : int -> thm -> xml
48 val thmstr2xml : int -> string -> xml
51 (*------------------------------------------------------------------
52 structure datatypes:DATATYPES =
53 (*structure datatypes =*)
55 ------------------------------------------------------------------*)
57 (*** convert sml-datatypes to xml for kbase ***)
58 (* NOTE: funs with siblings in xml_of_* are together with them in 'xml for libisabelle' *)
63 let fun id2x _ [] = ""
64 | id2x j (s::ss) = (indt j) ^ "<STRING> " ^ s ^ " </STRING>\n" ^
66 in (indt j) ^ "<STRINGLIST>\n" ^
67 (id2x (j + indentation) ids) ^
68 (indt j) ^ "</STRINGLIST>\n" end;
69 (* writeln(id2xml 8 ["linear", "univariate", "equation"]);
71 <STRING>linear</STRING>
72 <STRING>univariate</STRING>
73 <STRING>equation</STRING>
75 fun calc2xml j (thyID, (scrop, (rewop, _))) =
77 indt (j+i) ^ "<STRING>\n" ^ scrop ^ "</STRING>\n" ^
78 indt (j+i) ^ "<GUH>\n" ^ Thy_Write.cal2guh ("IsacKnowledge",
79 thyID) scrop ^ "</GUH>\n" ^
80 indt (j+i) ^ "<TERMOP>\n" ^ rewop ^ "</TERMOP>\n" ^
82 (*replace by 'fun calc2xml' as developed for thy in 0607*)
83 fun calc2xmlOLD _ (scr_op, (isa_op, _)) =
84 indt i ^ "<CALCULATE> (" ^ scr_op ^ ", (" ^ isa_op ^ ")) </CALCULATE>\n";
85 fun calcs2xmlOLD _ [] = "" (*TODO replace with 'strs2xml'*)
86 | calcs2xmlOLD j (r::rs) = calc2xmlOLD j r ^ calcs2xmlOLD j rs;
88 (*.for creating a href for a rule within an rls's rule list;
89 the guh points to the thy of definition of the rule, NOT of use in rls.*)
90 fun rule2xml _ _ Rule.Erule =
91 raise ERROR "rule2xml called with 'Erule'"
92 | rule2xml j _ (Rule.Thm (thmDeriv, _)) =
94 indt (j+i) ^ "<TAG> Theorem </TAG>\n" ^
95 indt (j+i) ^ "<STRING> " ^ ThmC.cut_id thmDeriv ^ " </STRING>\n" ^
96 indt (j+i) ^ "<GUH> " ^
97 Thy_Write.thm2guh (Thy_Read.thy_containing_thm thmDeriv) (ThmC.cut_id thmDeriv) ^ " </GUH>\n" ^
99 | rule2xml _ _ (Rule.Eval (_(*termop*), _)) = ""
100 (*FIXXXXXXXME.WN060714 in rls make Eval : calc -> rule [add scriptop!]
101 see smltest/../datatypes.sml !
102 indt j ^ "<RULE>\n" ^
103 indt (j+i) ^ "<STRING> " ^ termop ^ " </STRING>\n" ^
104 indt (j+i) ^ "<GUH> " ^ cal2guh (thy_containing_cal thyID termop)
105 termop ^ " </GUH>\n" ^
108 | rule2xml _ _ (Rule.Cal1 (_(*termop*), _)) = ""
109 | rule2xml j thyID (Rule.Rls_ rls) =
110 let val rls' = (#id o Rule_Set.rep) rls
112 indt j ^ "<RULE>\n" ^
113 indt (j+i) ^ "<TAG> Ruleset </TAG>\n" ^
114 indt (j+i) ^ "<STRING> " ^ rls' ^ " </STRING>\n" ^
115 indt (j+i) ^ "<GUH> " ^ Thy_Write.rls2guh (Thy_Read.thy_containing_rls thyID rls') rls' ^ " </GUH>\n" ^
118 fun rules2xml _ _ [] = ""
119 | rules2xml j thyID (r::rs) = rule2xml j thyID r ^ rules2xml j thyID rs;
123 | filt ((s, (t1, t2)) :: ps) =
124 if str = s then (t1 $ t2) :: filt ps else filt ps
126 fun pattern2xml j p where_ =
127 (case filterpbl "#Given" p of
128 [] => (indt j) ^ "<GIVEN> </GIVEN>\n"
129 (* val gis = filterpbl "#Given" p;
131 | gis => (indt j) ^ "<GIVEN>\n" ^ terms2xml' j gis ^
132 (indt j) ^ "</GIVEN>\n")
135 [] => (indt j) ^ "<WHERE> </WHERE>\n"
136 | whs => (indt j) ^ "<WHERE>\n" ^ terms2xml' j whs ^
137 (indt j) ^ "</WHERE>\n")
139 (case filterpbl "#Find" p of
140 [] => (indt j) ^ "<FIND> </FIND>\n"
141 | fis => (indt j) ^ "<FIND>\n" ^ terms2xml' j fis ^
142 (indt j) ^ "</FIND>\n")
144 (case filterpbl "#Relate" p of
145 [] => (indt j) ^ "<RELATE> </RELATE>\n"
146 | res => (indt j) ^ "<RELATE>\n" ^ terms2xml' j res ^
147 (indt j) ^ "</RELATE>\n");
149 writeln(pattern2xml 3 ((#ppc o get_pbt)
150 ["squareroot", "univariate", "equation", "test"]) []);
153 (*url to a source external to isac*)
154 fun extref2xml j linktext url =
155 indt j ^ "<EXTREF>\n" ^
156 indt (j+i) ^ "<TEXT> " ^ linktext ^ " </TEXT>\n" ^
157 indt (j+i) ^ "<URL> " ^ url ^ " </URL>\n" ^
158 indt j ^ "</EXTREF>\n";
159 fun theref2xml j thyID typ xstring =
160 let val guh = Thy_Write.theID2guh ["IsacKnowledge", thyID, typ, xstring]
161 val typ' = (implode o (drop_last_n 1) o Symbol.explode) typ
162 in indt j ^ "<KESTOREREF>\n" ^
163 indt (j+i) ^ "<TAG> " ^ typ' ^ " </TAG>\n" ^
164 indt (j+i) ^ "<ID> " ^ xstring ^ " </ID>\n" ^
165 indt (j+i) ^ "<GUH> " ^ guh ^ " </GUH>\n" ^
166 indt j ^ "</KESTOREREF>\n"
168 fun keref2xml j typ kestoreID =
169 let val id = strs2str' kestoreID
170 val guh = Ptool.kestoreID2guh typ kestoreID
171 in indt j ^ "<KESTOREREF>\n" ^
172 indt (j+i) ^ "<TAG> " ^ Ptool.ketype2str' typ ^ "</TAG>\n" ^
173 indt (j+i) ^ "<ID> " ^ id ^ " </ID>\n" ^
174 indt (j+i) ^ "<GUH> " ^ guh ^ " </GUH>\n" ^
175 indt j ^ "</KESTOREREF>\n"
177 fun authors2xml j str auts =
178 let fun autx _ [] = ""
179 | autx j (s::ss) = (indt j) ^ "<STRING> " ^ s ^ " </STRING>\n" ^
181 in indt j ^ "<"^str^">\n" ^
183 indt j ^ "</"^str^">\n"
185 (* writeln(authors2xml 2 "MATHAUTHORS" []);
186 writeln(authors2xml 2 "MATHAUTHORS"
187 ["isac-team 2001", "Richard Lang 2003"]);
189 fun scr2xml j Rule.Empty_Prog =
190 indt j ^"<SCRIPT> </SCRIPT>\n"
191 | scr2xml j (Rule.Prog term) =
192 if term = TermC.empty
193 then indt j ^"<SCRIPT> </SCRIPT>\n"
194 else indt j ^"<SCRIPT>\n"^
195 term2xml j (TermC.inst_abs term) ^ "\n" ^
196 indt j ^"</SCRIPT>\n"
197 | scr2xml j (Rule.Rfuns _) =
198 indt j ^"<REVERSREWRITE> reverse rewrite functions </REVERSREWRITE>\n";
200 fun calcref2xml j (thyID, (scrop, (_(*rewop*), _))) =
201 indt j ^ "<CALCREF>\n" ^
202 indt (j+i) ^ "<STRING> " ^ scrop ^ "</STRING>\n" ^
203 indt (j+i) ^ "<GUH> " ^ Thy_Write.cal2guh ("IsacKnowledge",
204 thyID) scrop ^ " </GUH>\n" ^
205 indt j ^ "</CALCREF>\n";
206 fun calcrefs2xml _ (_,[]) = ""
207 | calcrefs2xml j (thyID, cal::cs) =
208 calcref2xml j (thyID, cal) ^ calcrefs2xml j (thyID, cs);
210 fun prepa12xml j (terms, term) =
211 indt j ^"<PREPAT>\n"^
212 indt (j+i) ^"<PRECONDS>\n"^
213 terms2xml (j+2*i) terms ^
214 indt (j+i) ^"</PRECONDS>\n"^
215 indt (j+i) ^"<PATTERN>\n"^
216 term2xml (j+2*i) term ^
217 indt (j+i) ^"</PATTERN>\n"^
218 indt j ^"</PREPAT>\n";
219 fun prepat2xml _ [] = ""
220 | prepat2xml j (p::ps) = prepa12xml j p ^ prepat2xml j ps;
222 fun rls2xm j (thyID, seqrls, {id, preconds, rew_ord=(ord,_), erls,
223 srls, calc, rules, errpatts, scr}) =
224 indt j ^"<RULESET>\n"^
225 indt (j+i) ^"<ID> "^ id ^" </ID>\n"^
226 indt (j+i) ^"<TYPE> "^ seqrls ^" </TYPE>\n"^
227 indt (j+i) ^"<RULES>\n" ^
228 rules2xml (j+2*i) thyID rules ^
229 indt (j+i) ^"</RULES>\n" ^
230 indt (j+i) ^"<PRECONDS> " ^
231 terms2xml' (j+2*i) preconds ^
232 indt (j+i) ^"</PRECONDS>\n" ^
233 indt (j+i) ^"<ORDER>\n" ^
234 indt (j+2*i) ^ "<STRING> " ^ ord ^ " </STRING>\n" ^
235 (*WN060714 thy_isac_*-ord-*.xml not yet generated ................
236 indt (j+2*i) ^ "<GUH> " ^ ord2guh ("IsacKnowledge",
237 thyID) ord ^ " </GUH>\n" ^
238 ..................................................................*)
239 indt (j+i) ^"</ORDER>\n" ^
240 indt (j+i) ^"<ERLS>\n" ^
241 indt (j+2*i) ^ "<TAG> Ruleset </TAG>\n" ^
242 indt (j+2*i) ^ "<STRING> " ^ Rule_Set.id erls ^ " </STRING>\n" ^
243 indt (j+2*i) ^ "<GUH> " ^ Thy_Write.rls2guh ("IsacKnowledge", thyID)
244 (Rule_Set.id erls) ^ " </GUH>\n" ^
245 indt (j+i) ^"</ERLS>\n" ^
246 indt (j+i) ^"<SRLS>\n" ^
247 indt (j+2*i) ^ "<TAG> Ruleset </TAG>\n" ^
248 indt (j+2*i) ^ "<STRING> " ^ Rule_Set.id erls ^ " </STRING>\n" ^
249 indt (j+2*i) ^ "<GUH> " ^ Thy_Write.rls2guh ("IsacKnowledge", thyID)
250 (Rule_Set.id srls) ^ " </GUH>\n" ^
251 indt (j+i) ^"</SRLS>\n" ^
252 calcrefs2xml (j+i) (thyID, calc) ^
254 indt j ^"</RULESET>\n";
255 fun rls2xml j (thyID, Rule_Set.Empty) = rls2xml j (thyID, Rule_Set.empty)
256 | rls2xml j (thyID, Rule_Def.Repeat data) = rls2xm j (thyID, "Rls", data)
257 | rls2xml j (thyID, Rule_Set.Sequence data) = rls2xm j (thyID, "Seq", data)
258 | rls2xml j (thyID, Rule_Set.Rrls {id, prepat, rew_ord=(ord,_), erls, calc, errpatts, scr}) =
259 indt j ^"<RULESET>\n"^
260 indt (j+i) ^"<ID> "^ id ^" </ID>\n"^
261 indt (j+i) ^"<TYPE> Rrls </TYPE>\n"^
262 prepat2xml (j+i) prepat ^
263 indt (j+i) ^"<ORDER> " ^
264 indt (j+2*i) ^ "<TAG> Rewrite order </TAG>\n" ^
265 indt (j+2*i) ^ "<STRING> " ^ ord ^ " </STRING>\n" ^
266 (*WN060714 thy_isac_*-ord-*.xml not yet generated ................
267 indt (j+2*i) ^ "<GUH> " ^ ord2guh ("IsacKnowledge",
268 thyID) ord ^ " </GUH>\n" ^
269 .................................................................*)
270 indt (j+i) ^"</ORDER>\n" ^
271 indt (j+i) ^"<ERLS> " ^
272 indt (j+2*i) ^ "<TAG> Ruleset </TAG>\n" ^
273 indt (j+2*i) ^ "<STRING> " ^ Rule_Set.id erls ^ " </STRING>\n" ^
274 indt (j+2*i) ^ "<GUH> " ^ Thy_Write.rls2guh ("IsacKnowledge", thyID) (Rule_Set.id erls) ^ " </GUH>\n" ^
275 indt (j+i) ^"</ERLS>\n" ^
276 calcrefs2xml (j+i) (thyID, calc) ^
277 indt (j+i) ^"<SCRIPT>\n"^
278 scr2xml (j+2*i) scr ^
279 indt (j+i) ^" </SCRIPT>\n"^
280 indt j ^"</RULESET>\n";
282 (*** convert sml-datatypes to xml for libisabelle ***)
284 (** general types: lists, **)
286 fun xml_of_bool b = XML.Elem (("BOOL", []), [XML.Text (bool2str b)])
287 fun xml_to_bool (XML.Elem (("BOOL", []), [XML.Text b])) = string_to_bool b
288 | xml_to_bool tree = raise ERROR ("xml_to_bool: wrong XML.tree \n" ^ xmlstr 0 tree)
290 fun xml_to_ketype (XML.Elem (("KETYPE", []), [XML.Text str])) = Ptool.str2ketype' str
291 | xml_to_ketype tree = raise ERROR ("xml_to_ketype: wrong XML.tree \n" ^ xmlstr 0 tree)
293 fun xml_of_str str = XML.Elem (("STRING", []), [XML.Text str])
294 fun xml_of_strs strs = XML.Elem (("STRINGLIST", []), map xml_of_str strs)
296 fun xml_to_str (XML.Elem (("STRING", []), [XML.Text str])) = str
297 | xml_to_str tree = raise ERROR ("xml_to_str: wrong XML.tree \n" ^ xmlstr 0 tree)
298 fun xml_to_strs (XML.Elem (("STRINGLIST", []), strs)) = map xml_to_str strs
299 | xml_to_strs tree = raise ERROR ("xml_to_strs: wrong XML.tree \n" ^ xmlstr 0 tree)
301 fun xml_of_int i = XML.Elem (("INT", []), [XML.Text (string_of_int i)])
303 XML.Elem (("INTLIST", []), map xml_of_int is)
305 fun xml_to_int (XML.Elem (("INT", []), [XML.Text i])) =
306 (case TermC.int_opt_of_string i of SOME i => i | _ => raise ERROR "xml_to_int: int_of_str \<Rightarrow> NONE")
307 | xml_to_int tree = raise ERROR ("xml_to_int: wrong XML.tree \n" ^ xmlstr 0 tree)
308 fun xml_to_ints (XML.Elem (("INTLIST", []), is)) = map xml_to_int is
309 | xml_to_ints tree = raise ERROR ("xml_to_ints: wrong XML.tree \n" ^ xmlstr 0 tree)
311 (** isac datatypes **)
312 fun xml_of_pos tag (is, pp) =
313 XML.Elem ((tag, []), [
315 XML.Elem (("POS", []), [XML.Text (Pos.pos_2str pp)])])
316 fun xml_to_pos_ (XML.Elem (("POS", []), [XML.Text pp])) = Pos.str2pos_ pp
317 | xml_to_pos_ tree = raise ERROR ("xml_to_pos_: wrong XML.tree \n" ^ xmlstr 0 tree)
318 fun xml_to_pos (XML.Elem (("POSITION", []), [is, pp])) = (xml_to_ints is, xml_to_pos_ pp) (*: pos'*)
319 | xml_to_pos tree = raise ERROR ("xml_to_pos: wrong XML.tree \n" ^ xmlstr 0 tree)
321 fun xml_of_auto (Solve.Steps i) =
322 XML.Elem (("AUTO", []), [XML.Text "Step", XML.Text (string_of_int i)])
323 | xml_of_auto CompleteModel = XML.Elem (("AUTO", []), [XML.Text "CompleteModel"])
324 | xml_of_auto CompleteCalcHead = XML.Elem (("AUTO", []), [XML.Text "CompleteCalcHead"])
325 | xml_of_auto CompleteToSubpbl = XML.Elem (("AUTO", []), [XML.Text "CompleteToSubpbl"])
326 | xml_of_auto CompleteSubpbl = XML.Elem (("AUTO", []), [XML.Text "CompleteSubpbl"])
327 | xml_of_auto CompleteCalc = XML.Elem (("AUTO", []), [XML.Text "CompleteCalc"])
328 fun xml_to_auto (XML.Elem (("AUTO", []), [
329 XML.Elem (("STEP", []), [XML.Text i])])) = Solve.Steps (TermC.int_opt_of_string i |> the)
330 | xml_to_auto (XML.Elem (("AUTO", []), [XML.Text "CompleteModel"])) = Solve.CompleteModel
331 | xml_to_auto (XML.Elem (("AUTO", []), [XML.Text "CompleteCalcHead"])) = Solve.CompleteCalcHead
332 | xml_to_auto (XML.Elem (("AUTO", []), [XML.Text "CompleteToSubpbl"])) = Solve.CompleteToSubpbl
333 | xml_to_auto (XML.Elem (("AUTO", []), [XML.Text "CompleteSubpbl"])) = Solve.CompleteSubpbl
334 | xml_to_auto (XML.Elem (("AUTO", []), [XML.Text "CompleteCalc"])) = Solve.CompleteCalc
335 | xml_to_auto tree = raise ERROR ("xml_to_auto: wrong XML.tree \n" ^ xmlstr 0 tree)
339 | filt ((s, (t1, t2)) :: ps) =
340 if str = s then (t1 $ t2) :: filt ps else filt ps
343 fun xml_of_itm_ (I_Model.Cor (dts, _)) =
344 XML.Elem (("ITEM", [("status", "correct")]), [xml_of_term (Input_Descript.join' dts)])
345 | xml_of_itm_ (I_Model.Syn c) =
346 XML.Elem (("ITEM", [("status", "syntaxerror")]), [XML.Text c])
347 | xml_of_itm_ (I_Model.Typ c) =
348 XML.Elem (("ITEM", [("status", "typeerror")]), [XML.Text c])
349 (*type item also has 'False of cterm' set in preconds2xml WN 050618*)
350 | xml_of_itm_ (I_Model.Inc (dts, _)) =
351 XML.Elem (("ITEM", [("status", "incomplete")]), [xml_of_term (Input_Descript.join' dts)])
352 | xml_of_itm_ (I_Model.Sup dts) =
353 XML.Elem (("ITEM", [("status", "superfluous")]), [xml_of_term (Input_Descript.join' dts)])
354 | xml_of_itm_ (I_Model.Mis (d, pid)) =
355 XML.Elem (("ITEM", [("status", "missing")]), [xml_of_term (d $ pid)])
356 | xml_of_itm_ _ = raise ERROR "xml_of_itm_: wrong argument"
357 fun xml_of_itms itms =
359 fun extract (_, _, _, _, itm_) = itm_
360 | extract _ = raise ERROR "xml_of_itms.extract: wrong argument"
361 in map (xml_of_itm_ o extract) itms end
363 fun xml_of_precond (status, term) =
364 XML.Elem (("ITEM", [("status", if status then "correct" else "false")]), [xml_of_term term])
365 fun xml_of_preconds ps = map xml_of_precond ps
367 fun xml_of_model itms where_ =
369 fun eq str (_, _, _,field, _) = str = field
371 XML.Elem (("MODEL", []), [
372 XML.Elem (("GIVEN", []),
373 filter (eq "#Given") itms |> xml_of_itms),
374 XML.Elem (("WHERE", []),
375 xml_of_preconds where_),
376 XML.Elem (("FIND", []),
377 filter (eq "#Find") itms |> xml_of_itms),
378 XML.Elem (("RELATE", []),
379 filter (eq "#Relate") itms |> xml_of_itms)])
382 fun xml_of_spec (thyID, pblID, metID) =
383 XML.Elem (("SPECIFICATION", []), [
384 XML.Elem (("THEORYID", []), [XML.Text thyID]),
385 XML.Elem (("PROBLEMID", []), [xml_of_strs pblID]),
386 XML.Elem (("METHODID", []), [xml_of_strs metID])])
387 fun xml_to_spec (XML.Elem (("SPECIFICATION", []), [
388 XML.Elem (("THEORYID", []), [XML.Text thyID]),
389 XML.Elem (("PROBLEMID", []), [ps]),
390 XML.Elem (("METHODID", []), [ms])])) = (thyID, xml_to_strs ps, xml_to_strs ms)
391 | xml_to_spec tree = raise ERROR ("xml_to_spec: wrong XML.tree \n" ^ xmlstr 0 tree)
393 fun xml_of_variant (items, spec) =
394 XML.Elem (("VARIANT", []), [xml_of_strs items, xml_of_spec spec])
395 fun xml_to_variant (XML.Elem (("VARIANT", []), [items, spec])) =
396 (xml_to_strs items, xml_to_spec spec)
397 | xml_to_variant tree = raise ERROR ("xml_to_variant: wrong XML.tree \n" ^ xmlstr 0 tree)
399 fun xml_of_fmz [] = xml_of_fmz [Formalise.empty]
400 | xml_of_fmz vs = XML.Elem (("FORMALIZATION", []), map xml_of_variant vs)
401 fun xml_to_fmz (XML.Elem (("FORMALIZATION", []), vars)) = map xml_to_variant vars
402 | xml_to_fmz tree = raise ERROR ("xml_to_fmz: wrong XML.tree \n" ^ xmlstr 0 tree)
404 fun xml_of_modspec ((b, p_, head, gfr, pre, spec): SpecificationC.T) =
405 XML.Elem (("CALCHEAD", [("status", if b then "correct" else "incorrect")]), [
406 XML.Elem (("HEAD", []), [xml_of_term_NEW head]),
407 xml_of_model gfr pre,
408 XML.Elem (("BELONGSTO", []), [
409 XML.Text (case p_ of Pbl => "Pbl" | Met => "Met" | _ => "Und")]),
412 fun xml_of_posmodspec ((p: Pos.pos', (b, p_, head, gfr, pre, spec): SpecificationC.T)) =
413 XML.Elem (("CALCHEAD", [("status", if b then "correct" else "incorrect")]), [
414 xml_of_pos "POSITION" p,
415 XML.Elem (("HEAD", []), [xml_of_term_NEW head]),
416 xml_of_model gfr pre,
417 XML.Elem (("BELONGSTO", []), [
418 XML.Text (case p_ of Pbl => "Pbl" | Met => "Met" | _ => "Und")]),
421 (XML.Elem (("IMODEL", []), [
422 XML.Elem (("GIVEN", []), givens),
423 (*XML.Elem (("WHERE", []), wheres), ... Where is never input*)
424 XML.Elem (("FIND", []), finds),
425 XML.Elem (("RELATE", []), relates)])) =
426 ([P_Spec.Given (map xml_to_cterm givens),
427 P_Spec.Find (map xml_to_cterm finds),
428 P_Spec.Relate (map xml_to_cterm relates)]) : P_Spec.imodel
429 | xml_to_imodel x = raise ERROR ("xml_to_imodel: WRONG arg = " ^ xmlstr 0 x)
431 (XML.Elem (( "ICALCHEAD", []), [
432 pos as XML.Elem (( "POSITION", []), _),
433 XML.Elem (( "HEAD", []), [form]),
434 imodel as XML.Elem (("MATHML", []), _), (* TODO WN150813 ?!?*)
435 XML.Elem (( "POS", []), [XML.Text belongsto]),
436 spec as XML.Elem (( "SPECIFICATION", []), _)])) =
437 (xml_to_pos pos, xml_to_term_NEW form |> UnparseC.term, xml_to_imodel imodel,
438 Pos.str2pos_ belongsto, xml_to_spec spec) : P_Spec.icalhd
439 | xml_to_icalhd x = raise ERROR ("xml_to_icalhd: WRONG arg = " ^ xmlstr 0 x)
441 fun xml_of_sub (id, value) =
442 XML.Elem (("PAIR", []), [
443 XML.Elem (("VARIABLE", []), [xml_of_term id]),
444 XML.Elem (("VALUE", []), [xml_of_term value])])
446 (XML.Elem (("PAIR", []), [
447 XML.Elem (("VARIABLE", []), [id]),
448 XML.Elem (("VALUE", []), [value])])) = (xml_to_term id, xml_to_term value)
449 | xml_to_sub x = raise ERROR ("xml_to_sub wrong arg: " ^ xmlstr 0 x)
450 fun xml_of_subs (subs : Subst.input) =
451 XML.Elem (("SUBSTITUTION", []), map xml_of_sub (Subst.T_from_input (ThyC.get_theory "Isac_Knowledge") subs))
453 (XML.Elem (("SUBSTITUTION", []),
454 subs)) = Subst.T_to_input (map xml_to_sub subs)
455 | xml_to_subs x = raise ERROR ("xml_to_subs wrong arg: " ^ xmlstr 0 x)
456 fun xml_of_sube sube =
457 XML.Elem (("SUBSTITUTION", []), map xml_of_sub (Subst.T_from_string_eqs (ThyC.get_theory "Isac_Knowledge") sube))
459 (XML.Elem (("SUBSTITUTION", []),
460 xml_var_val_pairs)) = Subst.T_to_string_eqs (map xml_to_sub xml_var_val_pairs)
461 | xml_to_sube x = raise ERROR ("xml_to_sube wrong arg: " ^ xmlstr 0 x)
463 fun thm''2xml j (thm : thm) =
464 indt j ^ "<THEOREM>\n" ^
465 indt (j+i) ^ "<ID> " ^ ThmC.id_of_thm thm ^ " </ID>\n"^
466 term2xml j (Thm.prop_of thm) ^ "\n" ^
467 indt j ^ "</THEOREM>\n";
468 fun xml_of_thm' (ID, form) =
469 XML.Elem (("THEOREM", []), [
470 XML.Elem (("ID", []), [XML.Text ID]),
471 XML.Elem (("FORMULA", []), [
472 XML.Text form])]) (* repair for MathML: use term instead String *)
473 (* at the front-end theorems can be shown by their term, so term is transported isac-java <--- ME *)
474 fun xml_of_thm'' (ID, thm) =
475 (*---xml_of_thm''------------------------------------------thm'_to_thm''--------------
476 XML.Elem (("THEOREM", []), [
477 XML.Elem (("ID", []), [XML.Text ID]),
478 xml_of_term_NEW term])
479 -----xml_of_thm''------------------------------------------thm'_to_thm''------------*)
480 XML.Elem (("THEOREM", []), [
481 XML.Elem (("ID", []), [XML.Text ID]),
482 XML.Elem (("FORMULA", []), [
483 XML.Text ((UnparseC.term o Thm.prop_of) thm)])]) (* repair for MathML: use term instead String *)
486 (XML.Elem (("THEOREM", []), [
487 XML.Elem (("ID", []), [XML.Text ID]),
488 XML.Elem (("FORMULA", []), [XML.Text "NO_ad_hoc_thm_FROM_FRONTEND = True"])])) =
489 (ID, "NO_ad_hoc_thm_FROM_GUI = True")
490 | xml_to_thm' x = raise ERROR ("xml_of_thm' wrong arg:\n" ^ xmlstr 0 x)
491 (* at the front-end theorems are identified only by their name, so NO isac-java \<longrightarrow> ME *)
493 (*---xml_of_thm''------------------------------------------thm'_to_thm''--------------
494 (XML.Elem (("THEOREM", []), [
495 XML.Elem (("ID", []), [XML.Text ID]),
497 (ID, xml_to_term_NEW xterm) : thm''
498 | xml_to_thm'' x = raise ERROR ("xml_to_thm'' wrong arg:\n" ^ xmlstr 0 x)
499 -----xml_of_thm''------------------------------------------thm'_to_thm''------------*)
500 (XML.Elem (("THEOREM", []), [
501 XML.Elem (("ID", []), [XML.Text ID]),
502 XML.Elem (("FORMULA", []), [
503 XML.Text term])])) = (ID, ThmC.thm_from_thy (ThyC.Isac ()) ID)
504 | xml_to_thm'' x = raise ERROR ("xml_of_thm' wrong arg:" ^ xmlstr 0 x)
506 fun xml_of_src Rule.Empty_Prog =
507 XML.Elem (("NOCODE", []), [XML.Text "empty"])
508 | xml_of_src (Rule.Prog term) =
509 XML.Elem (("CODE", []), [
510 if term = TermC.empty then xml_of_src Rule.Empty_Prog
511 else xml_of_term (TermC.inst_abs term)])
512 | xml_of_src (Rule.Rfuns _) =
513 XML.Elem (("NOCODE", []), [XML.Text "reverse rewrite functions"])
515 (*.convert a tactic into xml-format .*)
516 fun xml_of_tac (Tactic.Subproblem (dI, pI)) =
517 XML.Elem (("SUBPROBLEMTACTIC", [("name", "Subproblem")]), [
518 XML.Elem (("THEORY", []), [XML.Text dI]),
519 XML.Elem (("PROBLEM", []), [xml_of_strs pI])])
520 | xml_of_tac (Tactic.Substitute cterms) =
521 (*Substitute: sube -> tac; Subst.string_eqs_empty: cterm' list; UNCLEAR HOW TO INPUT ON FRONTEND*)
522 XML.Elem (("STRINGLISTTACTIC", [("name", "Substitute")]), [xml_of_sube cterms])
523 (*----- Rewrite* -----------------------------------------------------*)
524 | xml_of_tac (Tactic.Rewrite thm'') =
525 XML.Elem (("REWRITETACTIC", [("name", "Rewrite")]), [xml_of_thm'' thm''])
526 | xml_of_tac (Tactic.Rewrite_Inst (subs, thm'')) =
527 XML.Elem (("REWRITEINSTTACTIC", [("name", "Rewrite_Inst")]), (
529 xml_of_thm'' thm'' :: []))
530 | xml_of_tac (Tactic.Rewrite_Set rls') =
531 XML.Elem (("REWRITESETTACTIC", [("name", "Rewrite_Set")]), [XML.Text rls'])
532 | xml_of_tac (Tactic.Rewrite_Set_Inst (subs, rls')) =
533 XML.Elem (("REWRITESETINSTTACTIC", [("name", "Rewrite_Set_Inst")]), ([
535 XML.Elem (("RULESET", []), [XML.Text rls'])]))
536 (*----- FORMTACTIC ---------------------------------------------------*)
537 | xml_of_tac (Tactic.Add_Find ct) =
538 XML.Elem (("FORMTACTIC", [("name", "Add_Find")]), [xml_of_cterm ct])
539 | xml_of_tac (Tactic.Add_Given ct) =
540 XML.Elem (("FORMTACTIC", [("name", "Add_Given")]), [xml_of_cterm ct])
541 | xml_of_tac (Tactic.Add_Relation ct) =
542 XML.Elem (("FORMTACTIC", [("name", "Add_Relation")]), [xml_of_cterm ct])
543 | xml_of_tac (Tactic.Check_elementwise ct) =
544 XML.Elem (("FORMTACTIC", [("name", "Check_elementwise")]), [xml_of_cterm ct])
545 | xml_of_tac (Tactic.Take ct) =
546 XML.Elem (("FORMTACTIC", [("name", "Take")]), [xml_of_cterm ct])
547 (*----- SIMPLETACTIC -------------------------------------------------*)
548 | xml_of_tac (Tactic.Calculate opstr) =
549 XML.Elem (("SIMPLETACTIC", [("name", "Calculate")]), [XML.Text opstr])
550 | xml_of_tac (Tactic.Or_to_List) =
551 XML.Elem (("SIMPLETACTIC", [("name", "Or_to_List")]), [(*//////////*)])
552 | xml_of_tac (Tactic.Specify_Theory ct) =
553 XML.Elem (("SIMPLETACTIC", [("name", "Specify_Theory")]), [XML.Text ct])
554 (*----- STRINGLISTTACTIC ---------------------------------------------*)
555 | xml_of_tac (Tactic.Apply_Method mI) =
556 XML.Elem (("STRINGLISTTACTIC", [("name", "Apply_Method")]), [xml_of_strs mI])
557 | xml_of_tac (Tactic.Check_Postcond pI) =
558 XML.Elem (("STRINGLISTTACTIC", [("name", "Check_Postcond")]), [xml_of_strs pI])
559 | xml_of_tac Model_Problem =
560 XML.Elem (("STRINGLISTTACTIC", [("name", "Model_Problem")]), [])
561 | xml_of_tac (Tactic.Refine_Tacitly pI) =
562 XML.Elem (("STRINGLISTTACTIC", [("name", "Refine_Tacitly")]), [xml_of_strs pI])
563 | xml_of_tac (Tactic.Specify_Method ct) =
564 XML.Elem (("STRINGLISTTACTIC", [("name", "Specify_Method")]), [xml_of_strs ct])
565 | xml_of_tac (Tactic.Specify_Problem ct) =
566 XML.Elem (("STRINGLISTTACTIC", [("name", "Specify_Problem")]), [xml_of_strs ct])
567 | xml_of_tac tac = raise ERROR ("xml_of_tac: not impl. for " ^ Tactic.input_to_string tac);
570 (XML.Elem (("SUBPROBLEMTACTIC", [("name", "Subproblem")]), [
571 XML.Elem (("THEORY", []), [XML.Text dI]),
572 XML.Elem (("PROBLEM", []), [pI])])) = Tactic.Subproblem (dI, xml_to_strs pI)
574 (*Substitute: sube -> tac; Subst.string_eqs_empty: cterm' list; UNCLEAR HOW TO INPUT ON FRONTEND*)
575 (XML.Elem (("STRINGLISTTACTIC", [
576 ("name", "Substitute")]), [cterms])) = Tactic.Substitute (xml_to_sube cterms)
577 (*----- Rewrite* -----------------------------------------------------*)
579 (XML.Elem (("REWRITETACTIC", [
580 ("name", "Rewrite")]), [thm])) = Tactic.Rewrite (xml_to_thm'' thm)
582 (XML.Elem (("REWRITEINSTTACTIC", [
583 ("name", "Rewrite_Inst")]), [
584 subs, thm])) = Tactic.Rewrite_Inst (xml_to_subs subs, xml_to_thm'' thm)
586 (XML.Elem (("REWRITESETTACTIC", [
587 ("name", "Rewrite_Set")]), [XML.Text rls'])) = Tactic.Rewrite_Set (rls')
589 (XML.Elem (("REWRITESETINSTTACTIC", [
590 ("name", "Rewrite_Set_Inst")]), [
592 XML.Elem (("RULESET", []), [XML.Text rls'])])) = Tactic.Rewrite_Set_Inst (xml_to_subs subs, rls')
593 (*----- FORMTACTIC ---------------------------------------------------*)
595 (XML.Elem (("FORMTACTIC", [
596 ("name", "Add_Find")]), [ct])) = Tactic.Add_Find (xml_to_cterm ct)
598 (XML.Elem (("FORMTACTIC", [
599 ("name", "Add_Given")]), [ct])) = Tactic.Add_Given (xml_to_cterm ct)
601 (XML.Elem (("FORMTACTIC", [
602 ("name", "Add_Relation")]), [ct])) = Tactic.Add_Relation (xml_to_cterm ct)
604 (XML.Elem (("FORMTACTIC", [
605 ("name", "Take")]), [ct])) = Tactic.Take (xml_to_cterm ct)
607 (XML.Elem (("FORMTACTIC", [
608 ("name", "Check_elementwise")]), [ct])) = Tactic.Check_elementwise (xml_to_cterm ct)
609 (*----- SIMPLETACTIC -------------------------------------------------*)
611 (XML.Elem (("SIMPLETACTIC", [
612 ("name", "Calculate")]), [XML.Text opstr])) = Tactic.Calculate opstr
614 (XML.Elem (("SIMPLETACTIC", [("name", "Or_to_List")]), [])) = Tactic.Or_to_List
616 (XML.Elem (("SIMPLETACTIC", [
617 ("name", "Specify_Theory")]), [XML.Text ct])) = Tactic.Specify_Theory ct
618 (*----- STRINGLISTTACTIC ---------------------------------------------*)
620 (XML.Elem (("STRINGLISTTACTIC", [
621 ("name", "Apply_Method")]), [mI])) = Tactic.Apply_Method (xml_to_strs mI)
623 (XML.Elem (("STRINGLISTTACTIC", [
624 ("name", "Check_Postcond")]), [pI])) = Tactic.Check_Postcond (xml_to_strs pI)
626 (XML.Elem (("STRINGLISTTACTIC", [
627 ("name", "Model_Problem")]), [])) = Tactic.Model_Problem
629 (XML.Elem (("STRINGLISTTACTIC", [
630 ("name", "Refine_Tacitly")]), [pI])) = Tactic.Refine_Tacitly (xml_to_strs pI)
632 (XML.Elem (("STRINGLISTTACTIC", [
633 ("name", "Specify_Method")]), [ct])) = Tactic.Specify_Method (xml_to_strs ct)
635 (XML.Elem (("STRINGLISTTACTIC", [
636 ("name", "Specify_Problem")]), [ct])) = Tactic.Specify_Problem (xml_to_strs ct)
637 | xml_to_tac x = raise ERROR ("xml_to_tac: not impl. for " ^ xmlstr 0 x);
639 val e_pblterm = (Thm.term_of o the o (TermC.parse @{theory Prog_Tac}))
640 ("Problem (" ^ ThyC.id_empty ^ ", " ^ strs2str' Problem.id_empty ^ ")");
642 (*WN051224 minimal adaption to exporting Formulae _only_ by getFormulaeFromTo*)
643 fun xml_of_posterm (p, t, _) =
644 let val input_request = Free ("________________________________________________", dummyT)
646 XML.Elem (("CALCFORMULA", []),
647 [xml_of_pos "POSITION" p,
648 if t = e_pblterm (*headline in pbl is e_ <- _root_pbl for CAS-command*)
649 then xml_of_term_NEW input_request
650 else xml_of_term_NEW t])
653 fun xml_of_asm_val (asm, vl) =
654 XML.Elem (("ASMEVALUATED", []),[
655 XML.Elem (("ASM", []), [xml_of_term asm]),
656 XML.Elem (("VALUE", []), [xml_of_term vl])])
658 (*.a reference to an element in the theory hierarchy;
659 compare 'fun keref2xml'.*)
660 (* val (j, thyID, typ, xstring) =
661 (i+i, snd (thy_containing_rls thy' prls'), "Rulesets", prls');
663 fun theref2xml j thyID typ xstring =
664 let val guh = Thy_Write.theID2guh ["IsacKnowledge", thyID, typ, xstring]
665 val typ' = (implode o (drop_last_n 1) o Symbol.explode) typ
666 in indt j ^ "<KESTOREREF>\n" ^
667 indt (j+i) ^ "<TAG> " ^ typ' ^ " </TAG>\n" ^
668 indt (j+i) ^ "<ID> " ^ xstring ^ " </ID>\n" ^
669 indt (j+i) ^ "<GUH> " ^ guh ^ " </GUH>\n" ^
670 indt j ^ "</KESTOREREF>\n"
672 fun xml_of_theref thyid typ xstring =
674 val guh = Thy_Write.theID2guh ["IsacKnowledge", thyid, typ, xstring]
675 val typ' = (implode o (drop_last_n 1) o Symbol.explode) typ
677 XML.Elem (("KESTOREREF", []),[
678 XML.Elem (("TAG", []), [XML.Text typ']),
679 XML.Elem (("ID", []), [XML.Text xstring]),
680 XML.Elem (("GUH", []), [XML.Text guh])])
684 fun xml_of_matchpbl (model_ok, pI, hdl, pbl, pre) =
685 XML.Elem (("CONTEXTDATA", []), [
686 XML.Elem (("GUH", []), [XML.Text (Ptool.pblID2guh pI)]),
687 XML.Elem (("STATUS", []), [
688 XML.Text ((if model_ok then "correct" else "incorrect"))]),
689 XML.Elem (("HEAD", []), [xml_of_term_NEW hdl]),
690 xml_of_model pbl pre])
692 fun xml_of_matchmet (model_ok, pI, scr, pbl, pre) =
693 XML.Elem (("CONTEXTDATA", []), [
694 XML.Elem (("GUH", []), [XML.Text (Ptool.metID2guh pI)]),
695 XML.Elem (("STATUS", []), [
696 XML.Text ((if model_ok then "correct" else "incorrect"))]),
697 XML.Elem (("PROGRAM", []), [xml_of_src scr]),
698 xml_of_model pbl pre])
700 fun xml_of_calcchanged calcid tag old del new =
701 (*TODO: make analogous to xml_to_calcchanged*)
702 XML.Elem ((tag, []),[
703 XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
704 XML.Elem (("CALCCHANGED", []), [
705 xml_of_pos "UNCHANGED" old,
706 xml_of_pos "DELETED" del,
707 xml_of_pos "GENERATED" new])])
708 fun xml_to_calcchanged (XML.Elem (("CALCCHANGED", []), [old, del, new])) =
709 (xml_to_pos old, xml_to_pos del, xml_to_pos new)
710 | xml_to_calcchanged x = raise ERROR ("xml_to_calcchanged: WRONG arg = " ^ xmlstr 0 x)
712 (* for checking output at Frontend *)
713 fun cut_xml xml i = xml |> xmlstr 0 |> Symbol.explode |> curry take i |> implode
714 (*------------------------------------------------------------------
717 ------------------------------------------------------------------*)