wneuper@59250
|
1 |
(* convert sml-datatypes to xml for libisabelle and for kbase.
|
wneuper@59250
|
2 |
authors: Walther Neuper 2003, 2016
|
neuper@37906
|
3 |
(c) due to copyright terms
|
walther@60257
|
4 |
|
walther@60258
|
5 |
This code remains in order to
|
walther@60258
|
6 |
keep tests of interaction Java-frontend <-> Kernel running.
|
neuper@37906
|
7 |
*)
|
neuper@37906
|
8 |
|
wneuper@59250
|
9 |
(*** convert sml-datatypes to xml for kbase ***)
|
wneuper@59250
|
10 |
|
wneuper@59405
|
11 |
fun calc2xml j (thyID, (scrop, (rewop, _))) =
|
wneuper@59250
|
12 |
indt j ^ "<CALC>\n" ^
|
wneuper@59250
|
13 |
indt (j+i) ^ "<STRING>\n" ^ scrop ^ "</STRING>\n" ^
|
walther@59917
|
14 |
indt (j+i) ^ "<GUH>\n" ^ Thy_Write.cal2guh ("IsacKnowledge",
|
wneuper@59250
|
15 |
thyID) scrop ^ "</GUH>\n" ^
|
wneuper@59250
|
16 |
indt (j+i) ^ "<TERMOP>\n" ^ rewop ^ "</TERMOP>\n" ^
|
wneuper@59405
|
17 |
indt j ^ "</CALC>\n";
|
wneuper@59250
|
18 |
|
wneuper@59250
|
19 |
fun filterpbl str =
|
wneuper@59250
|
20 |
let fun filt [] = []
|
wneuper@59250
|
21 |
| filt ((s, (t1, t2)) :: ps) =
|
wneuper@59250
|
22 |
if str = s then (t1 $ t2) :: filt ps else filt ps
|
wneuper@59250
|
23 |
in filt end;
|
wneuper@59250
|
24 |
fun pattern2xml j p where_ =
|
wneuper@59250
|
25 |
(case filterpbl "#Given" p of
|
wneuper@59250
|
26 |
[] => (indt j) ^ "<GIVEN> </GIVEN>\n"
|
wneuper@59250
|
27 |
(* val gis = filterpbl "#Given" p;
|
wneuper@59250
|
28 |
*)
|
wneuper@59250
|
29 |
| gis => (indt j) ^ "<GIVEN>\n" ^ terms2xml' j gis ^
|
wneuper@59250
|
30 |
(indt j) ^ "</GIVEN>\n")
|
wneuper@59250
|
31 |
^
|
wneuper@59250
|
32 |
(case where_ of
|
wneuper@59250
|
33 |
[] => (indt j) ^ "<WHERE> </WHERE>\n"
|
wneuper@59250
|
34 |
| whs => (indt j) ^ "<WHERE>\n" ^ terms2xml' j whs ^
|
wneuper@59250
|
35 |
(indt j) ^ "</WHERE>\n")
|
wneuper@59250
|
36 |
^
|
wneuper@59250
|
37 |
(case filterpbl "#Find" p of
|
wneuper@59250
|
38 |
[] => (indt j) ^ "<FIND> </FIND>\n"
|
wneuper@59250
|
39 |
| fis => (indt j) ^ "<FIND>\n" ^ terms2xml' j fis ^
|
wneuper@59250
|
40 |
(indt j) ^ "</FIND>\n")
|
wneuper@59250
|
41 |
^
|
wneuper@59250
|
42 |
(case filterpbl "#Relate" p of
|
wneuper@59250
|
43 |
[] => (indt j) ^ "<RELATE> </RELATE>\n"
|
wneuper@59250
|
44 |
| res => (indt j) ^ "<RELATE>\n" ^ terms2xml' j res ^
|
wneuper@59250
|
45 |
(indt j) ^ "</RELATE>\n");
|
wneuper@59250
|
46 |
|
wneuper@59405
|
47 |
fun calcref2xml j (thyID, (scrop, (_(*rewop*), _))) =
|
wneuper@59250
|
48 |
indt j ^ "<CALCREF>\n" ^
|
wneuper@59250
|
49 |
indt (j+i) ^ "<STRING> " ^ scrop ^ "</STRING>\n" ^
|
walther@59917
|
50 |
indt (j+i) ^ "<GUH> " ^ Thy_Write.cal2guh ("IsacKnowledge",
|
wneuper@59250
|
51 |
thyID) scrop ^ " </GUH>\n" ^
|
wneuper@59405
|
52 |
indt j ^ "</CALCREF>\n";
|
wneuper@59405
|
53 |
fun calcrefs2xml _ (_,[]) = ""
|
wneuper@59250
|
54 |
| calcrefs2xml j (thyID, cal::cs) =
|
wneuper@59250
|
55 |
calcref2xml j (thyID, cal) ^ calcrefs2xml j (thyID, cs);
|
wneuper@59250
|
56 |
|
wneuper@59250
|
57 |
fun prepa12xml j (terms, term) =
|
wneuper@59250
|
58 |
indt j ^"<PREPAT>\n"^
|
wneuper@59250
|
59 |
indt (j+i) ^"<PRECONDS>\n"^
|
wneuper@59250
|
60 |
terms2xml (j+2*i) terms ^
|
wneuper@59250
|
61 |
indt (j+i) ^"</PRECONDS>\n"^
|
wneuper@59250
|
62 |
indt (j+i) ^"<PATTERN>\n"^
|
wneuper@59250
|
63 |
term2xml (j+2*i) term ^
|
wneuper@59250
|
64 |
indt (j+i) ^"</PATTERN>\n"^
|
wneuper@59405
|
65 |
indt j ^"</PREPAT>\n";
|
wneuper@59250
|
66 |
fun prepat2xml _ [] = ""
|
wneuper@59405
|
67 |
| prepat2xml j (p::ps) = prepa12xml j p ^ prepat2xml j ps;
|
wneuper@59250
|
68 |
|
wneuper@59250
|
69 |
|
wneuper@59250
|
70 |
(*** convert sml-datatypes to xml for libisabelle ***)
|
wneuper@59250
|
71 |
|
walther@60258
|
72 |
(** general types: lists, etc **)
|
neuper@37906
|
73 |
|
wneuper@59124
|
74 |
fun xml_of_bool b = XML.Elem (("BOOL", []), [XML.Text (bool2str b)])
|
wneuper@59156
|
75 |
|
wneuper@59124
|
76 |
fun xml_of_str str = XML.Elem (("STRING", []), [XML.Text str])
|
wneuper@59124
|
77 |
fun xml_of_strs strs = XML.Elem (("STRINGLIST", []), map xml_of_str strs)
|
wneuper@59124
|
78 |
|
wneuper@59124
|
79 |
fun xml_of_int i = XML.Elem (("INT", []), [XML.Text (string_of_int i)])
|
wneuper@59250
|
80 |
fun xml_of_ints is =
|
wneuper@59124
|
81 |
XML.Elem (("INTLIST", []), map xml_of_int is)
|
wneuper@59124
|
82 |
|
neuper@37906
|
83 |
(** isac datatypes **)
|
walther@60258
|
84 |
|
wneuper@59249
|
85 |
fun xml_of_pos tag (is, pp) =
|
wneuper@59124
|
86 |
XML.Elem ((tag, []), [
|
wneuper@59124
|
87 |
xml_of_ints is,
|
walther@59694
|
88 |
XML.Elem (("POS", []), [XML.Text (Pos.pos_2str pp)])])
|
wneuper@59124
|
89 |
|
walther@59747
|
90 |
fun xml_of_auto (Solve.Steps i) =
|
wneuper@59124
|
91 |
XML.Elem (("AUTO", []), [XML.Text "Step", XML.Text (string_of_int i)])
|
walther@60258
|
92 |
| xml_of_auto Solve.CompleteModel = XML.Elem (("AUTO", []), [XML.Text "CompleteModel"])
|
walther@60258
|
93 |
| xml_of_auto Solve.CompleteCalcHead = XML.Elem (("AUTO", []), [XML.Text "CompleteCalcHead"])
|
walther@60258
|
94 |
| xml_of_auto Solve.CompleteToSubpbl = XML.Elem (("AUTO", []), [XML.Text "CompleteToSubpbl"])
|
walther@60258
|
95 |
| xml_of_auto Solve.CompleteSubpbl = XML.Elem (("AUTO", []), [XML.Text "CompleteSubpbl"])
|
walther@60258
|
96 |
| xml_of_auto Solve.CompleteCalc = XML.Elem (("AUTO", []), [XML.Text "CompleteCalc"])
|
neuper@37906
|
97 |
|
neuper@37906
|
98 |
fun filterpbl str =
|
neuper@37906
|
99 |
let fun filt [] = []
|
neuper@37906
|
100 |
| filt ((s, (t1, t2)) :: ps) =
|
neuper@37906
|
101 |
if str = s then (t1 $ t2) :: filt ps else filt ps
|
neuper@37906
|
102 |
in filt end;
|
neuper@37906
|
103 |
|
walther@59943
|
104 |
fun xml_of_itm_ (I_Model.Cor (dts, _)) =
|
walther@59953
|
105 |
XML.Elem (("ITEM", [("status", "correct")]), [xml_of_term (Input_Descript.join' dts)])
|
walther@59943
|
106 |
| xml_of_itm_ (I_Model.Syn c) =
|
wneuper@59127
|
107 |
XML.Elem (("ITEM", [("status", "syntaxerror")]), [XML.Text c])
|
walther@59943
|
108 |
| xml_of_itm_ (I_Model.Typ c) =
|
wneuper@59127
|
109 |
XML.Elem (("ITEM", [("status", "typeerror")]), [XML.Text c])
|
wneuper@59127
|
110 |
(*type item also has 'False of cterm' set in preconds2xml WN 050618*)
|
walther@59943
|
111 |
| xml_of_itm_ (I_Model.Inc (dts, _)) =
|
walther@59953
|
112 |
XML.Elem (("ITEM", [("status", "incomplete")]), [xml_of_term (Input_Descript.join' dts)])
|
walther@59943
|
113 |
| xml_of_itm_ (I_Model.Sup dts) =
|
walther@59953
|
114 |
XML.Elem (("ITEM", [("status", "superfluous")]), [xml_of_term (Input_Descript.join' dts)])
|
walther@59943
|
115 |
| xml_of_itm_ (I_Model.Mis (d, pid)) =
|
wneuper@59127
|
116 |
XML.Elem (("ITEM", [("status", "missing")]), [xml_of_term (d $ pid)])
|
walther@59962
|
117 |
| xml_of_itm_ _ = raise ERROR "xml_of_itm_: wrong argument"
|
wneuper@59127
|
118 |
fun xml_of_itms itms =
|
wneuper@59127
|
119 |
let
|
wneuper@59127
|
120 |
fun extract (_, _, _, _, itm_) = itm_
|
wneuper@59127
|
121 |
in map (xml_of_itm_ o extract) itms end
|
neuper@37906
|
122 |
|
wneuper@59127
|
123 |
fun xml_of_precond (status, term) =
|
wneuper@59127
|
124 |
XML.Elem (("ITEM", [("status", if status then "correct" else "false")]), [xml_of_term term])
|
wneuper@59127
|
125 |
fun xml_of_preconds ps = map xml_of_precond ps
|
neuper@37906
|
126 |
|
wneuper@59127
|
127 |
fun xml_of_model itms where_ =
|
wneuper@59127
|
128 |
let
|
wneuper@59127
|
129 |
fun eq str (_, _, _,field, _) = str = field
|
wneuper@59127
|
130 |
in
|
wneuper@59127
|
131 |
XML.Elem (("MODEL", []), [
|
wneuper@59127
|
132 |
XML.Elem (("GIVEN", []),
|
wneuper@59127
|
133 |
filter (eq "#Given") itms |> xml_of_itms),
|
wneuper@59127
|
134 |
XML.Elem (("WHERE", []),
|
wneuper@59127
|
135 |
xml_of_preconds where_),
|
wneuper@59127
|
136 |
XML.Elem (("FIND", []),
|
wneuper@59127
|
137 |
filter (eq "#Find") itms |> xml_of_itms),
|
wneuper@59127
|
138 |
XML.Elem (("RELATE", []),
|
wneuper@59127
|
139 |
filter (eq "#Relate") itms |> xml_of_itms)])
|
wneuper@59127
|
140 |
end
|
neuper@37906
|
141 |
|
wneuper@59124
|
142 |
fun xml_of_spec (thyID, pblID, metID) =
|
wneuper@59124
|
143 |
XML.Elem (("SPECIFICATION", []), [
|
wneuper@59124
|
144 |
XML.Elem (("THEORYID", []), [XML.Text thyID]),
|
wneuper@59124
|
145 |
XML.Elem (("PROBLEMID", []), [xml_of_strs pblID]),
|
wneuper@59124
|
146 |
XML.Elem (("METHODID", []), [xml_of_strs metID])])
|
neuper@37906
|
147 |
|
wneuper@59148
|
148 |
fun xml_of_variant (items, spec) =
|
wneuper@59148
|
149 |
XML.Elem (("VARIANT", []), [xml_of_strs items, xml_of_spec spec])
|
wneuper@59148
|
150 |
|
walther@59941
|
151 |
fun xml_of_fmz [] = xml_of_fmz [Formalise.empty]
|
wneuper@59148
|
152 |
| xml_of_fmz vs = XML.Elem (("FORMALIZATION", []), map xml_of_variant vs)
|
wneuper@59141
|
153 |
|
walther@60097
|
154 |
fun xml_of_modspec ((b, p_, head, gfr, pre, spec): SpecificationC.T) =
|
wneuper@59129
|
155 |
XML.Elem (("CALCHEAD", [("status", if b then "correct" else "incorrect")]), [
|
wneuper@59223
|
156 |
XML.Elem (("HEAD", []), [xml_of_term_NEW head]),
|
wneuper@59151
|
157 |
xml_of_model gfr pre,
|
wneuper@59129
|
158 |
XML.Elem (("BELONGSTO", []), [
|
walther@60258
|
159 |
XML.Text (case p_ of Pos.Pbl => "Pbl" | Pos.Met => "Met" | _ => "Und")]),
|
wneuper@59129
|
160 |
xml_of_spec spec])
|
wneuper@59129
|
161 |
|
walther@60097
|
162 |
fun xml_of_posmodspec ((p: Pos.pos', (b, p_, head, gfr, pre, spec): SpecificationC.T)) =
|
wneuper@59150
|
163 |
XML.Elem (("CALCHEAD", [("status", if b then "correct" else "incorrect")]), [
|
wneuper@59150
|
164 |
xml_of_pos "POSITION" p,
|
wneuper@59223
|
165 |
XML.Elem (("HEAD", []), [xml_of_term_NEW head]),
|
wneuper@59151
|
166 |
xml_of_model gfr pre,
|
wneuper@59150
|
167 |
XML.Elem (("BELONGSTO", []), [
|
walther@60258
|
168 |
XML.Text (case p_ of Pos.Pbl => "Pbl" | Pos.Met => "Met" | _ => "Und")]),
|
wneuper@59150
|
169 |
xml_of_spec spec])
|
neuper@37906
|
170 |
|
wneuper@59134
|
171 |
fun xml_of_sub (id, value) =
|
wneuper@59134
|
172 |
XML.Elem (("PAIR", []), [
|
wneuper@59134
|
173 |
XML.Elem (("VARIABLE", []), [xml_of_term id]),
|
wneuper@59134
|
174 |
XML.Elem (("VALUE", []), [xml_of_term value])])
|
walther@59911
|
175 |
fun xml_of_subs (subs : Subst.input) =
|
walther@59911
|
176 |
XML.Elem (("SUBSTITUTION", []), map xml_of_sub (Subst.T_from_input (ThyC.get_theory "Isac_Knowledge") subs))
|
wneuper@59301
|
177 |
fun xml_of_sube sube =
|
walther@59912
|
178 |
XML.Elem (("SUBSTITUTION", []), map xml_of_sub (Subst.T_from_string_eqs (ThyC.get_theory "Isac_Knowledge") sube))
|
wneuper@59134
|
179 |
|
wneuper@59250
|
180 |
fun thm''2xml j (thm : thm) =
|
wneuper@59250
|
181 |
indt j ^ "<THEOREM>\n" ^
|
walther@59876
|
182 |
indt (j+i) ^ "<ID> " ^ ThmC.id_of_thm thm ^ " </ID>\n"^
|
wneuper@59250
|
183 |
term2xml j (Thm.prop_of thm) ^ "\n" ^
|
wneuper@59405
|
184 |
indt j ^ "</THEOREM>\n";
|
wneuper@59405
|
185 |
fun xml_of_thm' (ID, form) =
|
wneuper@59134
|
186 |
XML.Elem (("THEOREM", []), [
|
wneuper@59134
|
187 |
XML.Elem (("ID", []), [XML.Text ID]),
|
wneuper@59158
|
188 |
XML.Elem (("FORMULA", []), [
|
wneuper@59158
|
189 |
XML.Text form])]) (* repair for MathML: use term instead String *)
|
wneuper@59250
|
190 |
(* at the front-end theorems can be shown by their term, so term is transported isac-java <--- ME *)
|
wneuper@59405
|
191 |
fun xml_of_thm'' (ID, thm) =
|
wneuper@59252
|
192 |
XML.Elem (("THEOREM", []), [
|
wneuper@59252
|
193 |
XML.Elem (("ID", []), [XML.Text ID]),
|
wneuper@59252
|
194 |
XML.Elem (("FORMULA", []), [
|
walther@59868
|
195 |
XML.Text ((UnparseC.term o Thm.prop_of) thm)])]) (* repair for MathML: use term instead String *)
|
wneuper@59252
|
196 |
|
walther@59878
|
197 |
fun xml_of_src Rule.Empty_Prog =
|
wneuper@59176
|
198 |
XML.Elem (("NOCODE", []), [XML.Text "empty"])
|
wneuper@59416
|
199 |
| xml_of_src (Rule.Prog term) =
|
wneuper@59176
|
200 |
XML.Elem (("CODE", []), [
|
walther@59878
|
201 |
if term = TermC.empty then xml_of_src Rule.Empty_Prog
|
wneuper@59393
|
202 |
else xml_of_term (TermC.inst_abs term)])
|
wneuper@59416
|
203 |
| xml_of_src (Rule.Rfuns _) =
|
wneuper@59176
|
204 |
XML.Elem (("NOCODE", []), [XML.Text "reverse rewrite functions"])
|
neuper@37906
|
205 |
|
wneuper@59249
|
206 |
(*.convert a tactic into xml-format .*)
|
wneuper@59571
|
207 |
fun xml_of_tac (Tactic.Subproblem (dI, pI)) =
|
wneuper@59134
|
208 |
XML.Elem (("SUBPROBLEMTACTIC", [("name", "Subproblem")]), [
|
wneuper@59134
|
209 |
XML.Elem (("THEORY", []), [XML.Text dI]),
|
wneuper@59134
|
210 |
XML.Elem (("PROBLEM", []), [xml_of_strs pI])])
|
wneuper@59571
|
211 |
| xml_of_tac (Tactic.Substitute cterms) =
|
walther@59912
|
212 |
(*Substitute: sube -> tac; Subst.string_eqs_empty: cterm' list; UNCLEAR HOW TO INPUT ON FRONTEND*)
|
wneuper@59162
|
213 |
XML.Elem (("STRINGLISTTACTIC", [("name", "Substitute")]), [xml_of_sube cterms])
|
wneuper@59160
|
214 |
(*----- Rewrite* -----------------------------------------------------*)
|
wneuper@59571
|
215 |
| xml_of_tac (Tactic.Rewrite thm'') =
|
wneuper@59250
|
216 |
XML.Elem (("REWRITETACTIC", [("name", "Rewrite")]), [xml_of_thm'' thm''])
|
wneuper@59571
|
217 |
| xml_of_tac (Tactic.Rewrite_Inst (subs, thm'')) =
|
wneuper@59134
|
218 |
XML.Elem (("REWRITEINSTTACTIC", [("name", "Rewrite_Inst")]), (
|
wneuper@59134
|
219 |
xml_of_subs subs ::
|
wneuper@59250
|
220 |
xml_of_thm'' thm'' :: []))
|
wneuper@59571
|
221 |
| xml_of_tac (Tactic.Rewrite_Set rls') =
|
wneuper@59134
|
222 |
XML.Elem (("REWRITESETTACTIC", [("name", "Rewrite_Set")]), [XML.Text rls'])
|
wneuper@59571
|
223 |
| xml_of_tac (Tactic.Rewrite_Set_Inst (subs, rls')) =
|
wneuper@59161
|
224 |
XML.Elem (("REWRITESETINSTTACTIC", [("name", "Rewrite_Set_Inst")]), ([
|
wneuper@59161
|
225 |
xml_of_subs subs,
|
wneuper@59161
|
226 |
XML.Elem (("RULESET", []), [XML.Text rls'])]))
|
wneuper@59161
|
227 |
(*----- FORMTACTIC ---------------------------------------------------*)
|
wneuper@59571
|
228 |
| xml_of_tac (Tactic.Add_Find ct) =
|
wneuper@59161
|
229 |
XML.Elem (("FORMTACTIC", [("name", "Add_Find")]), [xml_of_cterm ct])
|
wneuper@59571
|
230 |
| xml_of_tac (Tactic.Add_Given ct) =
|
wneuper@59161
|
231 |
XML.Elem (("FORMTACTIC", [("name", "Add_Given")]), [xml_of_cterm ct])
|
wneuper@59571
|
232 |
| xml_of_tac (Tactic.Add_Relation ct) =
|
wneuper@59161
|
233 |
XML.Elem (("FORMTACTIC", [("name", "Add_Relation")]), [xml_of_cterm ct])
|
wneuper@59571
|
234 |
| xml_of_tac (Tactic.Check_elementwise ct) =
|
wneuper@59161
|
235 |
XML.Elem (("FORMTACTIC", [("name", "Check_elementwise")]), [xml_of_cterm ct])
|
wneuper@59571
|
236 |
| xml_of_tac (Tactic.Take ct) =
|
wneuper@59161
|
237 |
XML.Elem (("FORMTACTIC", [("name", "Take")]), [xml_of_cterm ct])
|
wneuper@59160
|
238 |
(*----- SIMPLETACTIC -------------------------------------------------*)
|
wneuper@59571
|
239 |
| xml_of_tac (Tactic.Calculate opstr) =
|
wneuper@59160
|
240 |
XML.Elem (("SIMPLETACTIC", [("name", "Calculate")]), [XML.Text opstr])
|
wneuper@59571
|
241 |
| xml_of_tac (Tactic.Or_to_List) =
|
wneuper@59160
|
242 |
XML.Elem (("SIMPLETACTIC", [("name", "Or_to_List")]), [(*//////////*)])
|
wneuper@59571
|
243 |
| xml_of_tac (Tactic.Specify_Theory ct) =
|
wneuper@59160
|
244 |
XML.Elem (("SIMPLETACTIC", [("name", "Specify_Theory")]), [XML.Text ct])
|
wneuper@59160
|
245 |
(*----- STRINGLISTTACTIC ---------------------------------------------*)
|
wneuper@59571
|
246 |
| xml_of_tac (Tactic.Apply_Method mI) =
|
wneuper@59160
|
247 |
XML.Elem (("STRINGLISTTACTIC", [("name", "Apply_Method")]), [xml_of_strs mI])
|
wneuper@59571
|
248 |
| xml_of_tac (Tactic.Check_Postcond pI) =
|
wneuper@59160
|
249 |
XML.Elem (("STRINGLISTTACTIC", [("name", "Check_Postcond")]), [xml_of_strs pI])
|
walther@60258
|
250 |
| xml_of_tac Tactic.Model_Problem =
|
wneuper@59160
|
251 |
XML.Elem (("STRINGLISTTACTIC", [("name", "Model_Problem")]), [])
|
wneuper@59571
|
252 |
| xml_of_tac (Tactic.Refine_Tacitly pI) =
|
wneuper@59160
|
253 |
XML.Elem (("STRINGLISTTACTIC", [("name", "Refine_Tacitly")]), [xml_of_strs pI])
|
wneuper@59571
|
254 |
| xml_of_tac (Tactic.Specify_Method ct) =
|
wneuper@59160
|
255 |
XML.Elem (("STRINGLISTTACTIC", [("name", "Specify_Method")]), [xml_of_strs ct])
|
wneuper@59571
|
256 |
| xml_of_tac (Tactic.Specify_Problem ct) =
|
wneuper@59160
|
257 |
XML.Elem (("STRINGLISTTACTIC", [("name", "Specify_Problem")]), [xml_of_strs ct])
|
walther@59846
|
258 |
| xml_of_tac tac = raise ERROR ("xml_of_tac: not impl. for " ^ Tactic.input_to_string tac);
|
wneuper@59160
|
259 |
|
walther@60339
|
260 |
val e_pblterm = TermC.parseNEW'' @{theory Prog_Tac}
|
walther@59997
|
261 |
("Problem (" ^ ThyC.id_empty ^ ", " ^ strs2str' Problem.id_empty ^ ")");
|
neuper@37906
|
262 |
|
neuper@37906
|
263 |
(*WN051224 minimal adaption to exporting Formulae _only_ by getFormulaeFromTo*)
|
wneuper@59516
|
264 |
fun xml_of_posterm (p, t, _) =
|
wneuper@59225
|
265 |
let val input_request = Free ("________________________________________________", dummyT)
|
wneuper@59225
|
266 |
in
|
wneuper@59225
|
267 |
XML.Elem (("CALCFORMULA", []),
|
wneuper@59225
|
268 |
[xml_of_pos "POSITION" p,
|
wneuper@59225
|
269 |
if t = e_pblterm (*headline in pbl is e_ <- _root_pbl for CAS-command*)
|
wneuper@59225
|
270 |
then xml_of_term_NEW input_request
|
wneuper@59225
|
271 |
else xml_of_term_NEW t])
|
wneuper@59225
|
272 |
end
|
neuper@37906
|
273 |
|
wneuper@59133
|
274 |
fun xml_of_asm_val (asm, vl) =
|
wneuper@59133
|
275 |
XML.Elem (("ASMEVALUATED", []),[
|
wneuper@59133
|
276 |
XML.Elem (("ASM", []), [xml_of_term asm]),
|
wneuper@59133
|
277 |
XML.Elem (("VALUE", []), [xml_of_term vl])])
|
neuper@37906
|
278 |
|
walther@60257
|
279 |
(* reference to an element in the theory hierarchy *)
|
wneuper@59405
|
280 |
fun theref2xml j thyID typ xstring =
|
walther@59917
|
281 |
let val guh = Thy_Write.theID2guh ["IsacKnowledge", thyID, typ, xstring]
|
neuper@40836
|
282 |
val typ' = (implode o (drop_last_n 1) o Symbol.explode) typ
|
neuper@37906
|
283 |
in indt j ^ "<KESTOREREF>\n" ^
|
neuper@37906
|
284 |
indt (j+i) ^ "<TAG> " ^ typ' ^ " </TAG>\n" ^
|
neuper@37906
|
285 |
indt (j+i) ^ "<ID> " ^ xstring ^ " </ID>\n" ^
|
neuper@37906
|
286 |
indt (j+i) ^ "<GUH> " ^ guh ^ " </GUH>\n" ^
|
wneuper@59405
|
287 |
indt j ^ "</KESTOREREF>\n"
|
neuper@37906
|
288 |
end;
|
wneuper@59405
|
289 |
fun xml_of_theref thyid typ xstring =
|
wneuper@59133
|
290 |
let
|
walther@59917
|
291 |
val guh = Thy_Write.theID2guh ["IsacKnowledge", thyid, typ, xstring]
|
wneuper@59133
|
292 |
val typ' = (implode o (drop_last_n 1) o Symbol.explode) typ
|
wneuper@59133
|
293 |
in
|
wneuper@59133
|
294 |
XML.Elem (("KESTOREREF", []),[
|
wneuper@59133
|
295 |
XML.Elem (("TAG", []), [XML.Text typ']),
|
wneuper@59133
|
296 |
XML.Elem (("ID", []), [XML.Text xstring]),
|
wneuper@59133
|
297 |
XML.Elem (("GUH", []), [XML.Text guh])])
|
wneuper@59133
|
298 |
end
|
neuper@37906
|
299 |
|
wneuper@59172
|
300 |
fun xml_of_matchpbl (model_ok, pI, hdl, pbl, pre) =
|
wneuper@59172
|
301 |
XML.Elem (("CONTEXTDATA", []), [
|
walther@59974
|
302 |
XML.Elem (("GUH", []), [XML.Text (Ptool.pblID2guh pI)]),
|
wneuper@59172
|
303 |
XML.Elem (("STATUS", []), [
|
wneuper@59172
|
304 |
XML.Text ((if model_ok then "correct" else "incorrect"))]),
|
wneuper@59223
|
305 |
XML.Elem (("HEAD", []), [xml_of_term_NEW hdl]),
|
wneuper@59172
|
306 |
xml_of_model pbl pre])
|
wneuper@59172
|
307 |
|
wneuper@59172
|
308 |
fun xml_of_matchmet (model_ok, pI, scr, pbl, pre) =
|
wneuper@59172
|
309 |
XML.Elem (("CONTEXTDATA", []), [
|
walther@59974
|
310 |
XML.Elem (("GUH", []), [XML.Text (Ptool.metID2guh pI)]),
|
wneuper@59172
|
311 |
XML.Elem (("STATUS", []), [
|
wneuper@59172
|
312 |
XML.Text ((if model_ok then "correct" else "incorrect"))]),
|
wneuper@59172
|
313 |
XML.Elem (("PROGRAM", []), [xml_of_src scr]),
|
wneuper@59172
|
314 |
xml_of_model pbl pre])
|
neuper@37906
|
315 |
|
walther@59616
|
316 |
fun xml_of_calcchanged calcid tag old del new =
|
wneuper@59131
|
317 |
XML.Elem ((tag, []),[
|
wneuper@59131
|
318 |
XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
|
wneuper@59131
|
319 |
XML.Elem (("CALCCHANGED", []), [
|
wneuper@59131
|
320 |
xml_of_pos "UNCHANGED" old,
|
wneuper@59131
|
321 |
xml_of_pos "DELETED" del,
|
wneuper@59131
|
322 |
xml_of_pos "GENERATED" new])])
|
wneuper@59175
|
323 |
|
wneuper@59175
|
324 |
(* for checking output at Frontend *)
|
wneuper@59175
|
325 |
fun cut_xml xml i = xml |> xmlstr 0 |> Symbol.explode |> curry take i |> implode
|