|
wneuper@825
|
1 |
(* use"xmlsrc/datatypes.sml";
|
|
wneuper@825
|
2 |
use"datatypes.sml";
|
|
wneuper@825
|
3 |
*)
|
|
wneuper@825
|
4 |
|
|
wneuper@825
|
5 |
val i = indentation;
|
|
wneuper@825
|
6 |
|
|
wneuper@825
|
7 |
(** general types: lists, **)
|
|
wneuper@825
|
8 |
|
|
wneuper@825
|
9 |
fun id2xml j ids =
|
|
wneuper@825
|
10 |
let fun id2x _ [] = ""
|
|
rgradisc@1114
|
11 |
| id2x j (s::ss) = (indt j) ^ "<STRING> " ^ s ^ " </STRING>\n" ^
|
|
wneuper@825
|
12 |
(id2x j ss)
|
|
rgradisc@1114
|
13 |
in (indt j) ^ "<STRINGLIST>\n" ^
|
|
wneuper@825
|
14 |
(id2x (j + indentation) ids) ^
|
|
rgradisc@1114
|
15 |
(indt j) ^ "</STRINGLIST>\n" end;
|
|
wneuper@825
|
16 |
(* writeln(id2xml 8 ["linear","univariate","equation"]);
|
|
rgradisc@1114
|
17 |
<STRINGLIST>
|
|
rgradisc@1114
|
18 |
<STRING>linear</STRING>
|
|
rgradisc@1114
|
19 |
<STRING>univariate</STRING>
|
|
rgradisc@1114
|
20 |
<STRING>equation</STRING>
|
|
rgradisc@1114
|
21 |
</STRINGLIST>*)
|
|
wneuper@825
|
22 |
|
|
wneuper@825
|
23 |
fun ints2xml j ids =
|
|
wneuper@825
|
24 |
let fun int2x _ [] = ""
|
|
wneuper@825
|
25 |
| int2x j (s::ss) = (indt j) ^"<INT> "^ string_of_int s ^" </INT>\n"^
|
|
wneuper@825
|
26 |
(int2x j ss)
|
|
wneuper@825
|
27 |
in (indt j) ^ "<INTLIST>\n" ^
|
|
wneuper@825
|
28 |
(int2x (j + i) ids) ^
|
|
wneuper@825
|
29 |
(indt j) ^ "</INTLIST>\n" end;
|
|
wneuper@825
|
30 |
(* writeln(ints2xml 3 [1,2,3]);
|
|
wneuper@825
|
31 |
*)
|
|
wneuper@825
|
32 |
|
|
wneuper@825
|
33 |
|
|
wneuper@825
|
34 |
(** isac datatypes **)
|
|
wneuper@825
|
35 |
|
|
wneuper@882
|
36 |
fun rule2xml j Erule =
|
|
wneuper@882
|
37 |
(indt j ^ "<RULE> empty_rule </RULE>\n"):xml
|
|
wneuper@882
|
38 |
| rule2xml j (Thm (thmID, thm)) =
|
|
wneuper@882
|
39 |
indt j ^ "<RULE>\n" ^
|
|
wneuper@882
|
40 |
indt (j+i) ^ "<THEOREMID>" ^ thmID ^ "</THEOREMID>\n" ^
|
|
wneuper@882
|
41 |
term2xml j ((#prop o rep_thm) thm) ^ "\n" ^
|
|
wneuper@882
|
42 |
indt j ^ "</RULE>\n"
|
|
wneuper@882
|
43 |
| rule2xml j (Calc (op_, _)) =
|
|
wneuper@882
|
44 |
indt j ^ "<RULE>\n" ^
|
|
wneuper@882
|
45 |
indt (j+i) ^"<CALCULATE> (" ^ op_ ^ ", eval_fun) </CALCULATE>\n" ^
|
|
wneuper@882
|
46 |
indt j ^ "</RULE>\n"
|
|
wneuper@882
|
47 |
| rule2xml j (Rls_ rls) =
|
|
wneuper@882
|
48 |
indt j ^ "<RULE>\n" ^
|
|
wneuper@882
|
49 |
indt (j+i) ^"<RULESET> " ^ ((#id o rep_rls) rls) ^ " </RULESET>\n" ^
|
|
wneuper@882
|
50 |
indt j ^ "</RULE>\n";
|
|
wneuper@882
|
51 |
fun rules2xml j [] = ("":xml)
|
|
wneuper@882
|
52 |
| rules2xml j (r::rs) = rule2xml j r ^ rules2xml j rs;
|
|
wneuper@882
|
53 |
|
|
wneuper@825
|
54 |
fun filterpbl str =
|
|
wneuper@825
|
55 |
let fun filt [] = []
|
|
wneuper@825
|
56 |
| filt ((s, (t1, t2)) :: ps) =
|
|
wneuper@825
|
57 |
if str = s then (t1 $ t2) :: filt ps else filt ps
|
|
wneuper@825
|
58 |
in filt end;
|
|
wneuper@825
|
59 |
|
|
wneuper@1782
|
60 |
(*FIXME.WN040831 model2xml <--?--> pattern2xml*)
|
|
wneuper@825
|
61 |
(*WN.25.8.03: pattern2xml different output with TextIO | writeln !!!
|
|
wneuper@825
|
62 |
the version below is for TextIO: terms2xml makes \n !*)
|
|
wneuper@825
|
63 |
fun pattern2xml j p where_ =
|
|
wneuper@825
|
64 |
(case filterpbl "#Given" p of
|
|
wneuper@825
|
65 |
[] => (indt j) ^ "<GIVEN> </GIVEN>\n"
|
|
wneuper@825
|
66 |
| gis => (indt j) ^ "<GIVEN>\n" ^ terms2xml j gis ^
|
|
wneuper@825
|
67 |
(indt j) ^ "</GIVEN>\n")
|
|
wneuper@825
|
68 |
^
|
|
wneuper@825
|
69 |
(case where_ of
|
|
wneuper@825
|
70 |
[] => (indt j) ^ "<WHERE> </WHERE>\n"
|
|
wneuper@825
|
71 |
| whs => (indt j) ^ "<WHERE>\n" ^ terms2xml j whs ^
|
|
wneuper@825
|
72 |
(indt j) ^ "</WHERE>\n")
|
|
wneuper@825
|
73 |
^
|
|
wneuper@825
|
74 |
(case filterpbl "#Find" p of
|
|
wneuper@825
|
75 |
[] => (indt j) ^ "<FIND> </FIND>\n"
|
|
wneuper@825
|
76 |
| fis => (indt j) ^ "<FIND>\n" ^ terms2xml j fis ^
|
|
wneuper@825
|
77 |
(indt j) ^ "</FIND>\n")
|
|
wneuper@825
|
78 |
^
|
|
wneuper@825
|
79 |
(case filterpbl "#Relate" p of
|
|
wneuper@825
|
80 |
[] => (indt j) ^ "<RELATE> </RELATE>\n"
|
|
wneuper@825
|
81 |
| res => (indt j) ^ "<RELATE>\n" ^ terms2xml j res ^
|
|
wneuper@825
|
82 |
(indt j) ^ "</RELATE>\n");
|
|
wneuper@825
|
83 |
(*
|
|
wneuper@825
|
84 |
writeln(pattern2xml 3 ((#ppc o get_pbt)
|
|
wneuper@825
|
85 |
["squareroot","univariate","equation","test"]) []);
|
|
wneuper@825
|
86 |
*)
|
|
wneuper@825
|
87 |
|
|
wneuper@825
|
88 |
(*see itm_2item*)
|
|
wneuper@825
|
89 |
fun itm_2xml j (Cor (dts,_))=
|
|
rgradisc@1038
|
90 |
(indt j ^"<ITEM status=\"correct\">\n"^
|
|
rgradisc@1037
|
91 |
term2xml (j) (comp_dts' dts)^"\n"^
|
|
wneuper@825
|
92 |
indt j ^"</ITEM>\n"):xml
|
|
wneuper@825
|
93 |
| itm_2xml j (Syn c) =
|
|
rgradisc@1038
|
94 |
indt j ^"<ITEM status=\"syntaxerror\">\n"^
|
|
rgradisc@1037
|
95 |
indt (j) ^c^
|
|
wneuper@825
|
96 |
indt j ^"</ITEM>\n"
|
|
wneuper@825
|
97 |
| itm_2xml j (Typ c) =
|
|
rgradisc@1038
|
98 |
indt j ^"<ITEM status=\"typeerror\">\n"^
|
|
rgradisc@1037
|
99 |
indt (j) ^c^
|
|
wneuper@825
|
100 |
indt j ^"</ITEM>\n"
|
|
wneuper@825
|
101 |
| itm_2xml j (Inc (dts,_)) =
|
|
rgradisc@1038
|
102 |
indt j ^"<ITEM status=\"incomplete\">\n"^
|
|
rgradisc@1037
|
103 |
term2xml (j) (comp_dts' dts)^"\n"^
|
|
wneuper@825
|
104 |
indt j ^"</ITEM>\n"
|
|
wneuper@825
|
105 |
| itm_2xml j (Sup dts) =
|
|
rgradisc@1038
|
106 |
indt j ^"<ITEM status=\"superfluous\">\n"^
|
|
rgradisc@1037
|
107 |
term2xml (j) (comp_dts' dts)^"\n"^
|
|
wneuper@825
|
108 |
indt j ^"</ITEM>\n"
|
|
wneuper@825
|
109 |
| itm_2xml j (Mis (d,pid)) =
|
|
rgradisc@1038
|
110 |
indt j ^"<ITEM status=\"superfluous\">\n"^
|
|
rgradisc@1037
|
111 |
term2xml (j) (d $ pid)^"\n"^
|
|
wneuper@825
|
112 |
indt j ^"</ITEM>\n";
|
|
wneuper@825
|
113 |
|
|
wneuper@825
|
114 |
(*see terms2xml' fpr \n*)
|
|
wneuper@825
|
115 |
fun itms2xml _ [] = ""
|
|
wneuper@825
|
116 |
| itms2xml j [(_,_,_,_,itm_)] = itm_2xml j itm_
|
|
wneuper@825
|
117 |
| itms2xml j (((_,_,_,_,itm_):itm)::itms) =
|
|
wneuper@825
|
118 |
itm_2xml j itm_ ^ itms2xml j itms;
|
|
wneuper@825
|
119 |
|
|
wneuper@825
|
120 |
fun precond2xml j (true, term) =
|
|
wneuper@1124
|
121 |
(indt j ^"<ITEM status=\"correct\">\n"^
|
|
rgradisc@1037
|
122 |
term2xml (j) term^"\n"^
|
|
wneuper@825
|
123 |
indt j ^"</ITEM>\n"):xml
|
|
wneuper@825
|
124 |
| precond2xml j (false, term) =
|
|
rgradisc@1038
|
125 |
indt j ^"<ITEM status=\"false\">\n"^
|
|
rgradisc@1037
|
126 |
term2xml (j+i) term^"\n"^
|
|
wneuper@825
|
127 |
indt j ^"</ITEM>\n";
|
|
wneuper@825
|
128 |
|
|
wneuper@882
|
129 |
fun preconds2xml _ [] = ("":xml)
|
|
wneuper@825
|
130 |
| preconds2xml j (p::ps) = precond2xml j p ^ preconds2xml j ps;
|
|
wneuper@825
|
131 |
|
|
wneuper@1782
|
132 |
(*FIXME.WN040831 model2xml <--?--> pattern2xml*)
|
|
wneuper@825
|
133 |
fun model2xml j (itms:itm list) where_ =
|
|
wneuper@825
|
134 |
let fun eq4 str (_,_,_,field,_) = str = field
|
|
wneuper@844
|
135 |
in (indt j ^"<MODEL>\n"^
|
|
wneuper@825
|
136 |
(case filter (eq4 "#Given") itms of
|
|
wneuper@844
|
137 |
[] => (indt (j+i)) ^ "<GIVEN> </GIVEN>\n"
|
|
wneuper@844
|
138 |
| gis => (indt (j+i)) ^ "<GIVEN>\n" ^ itms2xml (j+2*i) gis ^
|
|
wneuper@844
|
139 |
(indt (j+i)) ^ "</GIVEN>\n")
|
|
wneuper@825
|
140 |
^
|
|
wneuper@825
|
141 |
(case where_ of
|
|
wneuper@844
|
142 |
[] => (indt (j+i)) ^ "<WHERE> </WHERE>\n"
|
|
wneuper@844
|
143 |
| whs => (indt (j+i)) ^ "<WHERE>\n" ^ preconds2xml (j+2*i) whs ^
|
|
wneuper@844
|
144 |
(indt (j+i)) ^ "</WHERE>\n")
|
|
wneuper@825
|
145 |
^
|
|
wneuper@825
|
146 |
(case filter (eq4 "#Find") itms of
|
|
wneuper@844
|
147 |
[] => (indt (j+i)) ^ "<FIND> </FIND>\n"
|
|
wneuper@844
|
148 |
| fis => (indt (j+i)) ^ "<FIND>\n" ^ itms2xml (j+2*i) fis ^
|
|
wneuper@844
|
149 |
(indt (j+i)) ^ "</FIND>\n")
|
|
wneuper@825
|
150 |
^
|
|
wneuper@825
|
151 |
(case filter (eq4 "#Relate") itms of
|
|
wneuper@844
|
152 |
[] => (indt (j+i)) ^ "<RELATE> </RELATE>\n"
|
|
wneuper@844
|
153 |
| res => (indt (j+i)) ^ "<RELATE>\n" ^ itms2xml (j+2*i) res ^
|
|
wneuper@844
|
154 |
(indt (j+i)) ^ "</RELATE>\n")^
|
|
wneuper@844
|
155 |
indt j ^"</MODEL>\n"):xml
|
|
wneuper@825
|
156 |
end;
|
|
wneuper@825
|
157 |
(* writeln(model2xml 3 itms []);
|
|
wneuper@825
|
158 |
*)
|
|
wneuper@825
|
159 |
|
|
wneuper@825
|
160 |
fun spec2xml j ((dI,pI,mI):spec) =
|
|
wneuper@825
|
161 |
(indt j ^"<SPECIFICATION>\n"^
|
|
rgradisc@1114
|
162 |
indt (j+i) ^"<THEORYID> "^ dI ^" </THEORYID>\n"^
|
|
rgradisc@1114
|
163 |
indt (j+i) ^"<PROBLEMID>\n"^
|
|
wneuper@825
|
164 |
id2xml (j+2*i) pI ^
|
|
rgradisc@1114
|
165 |
indt (j+i) ^"</PROBLEMID>\n"^
|
|
rgradisc@1114
|
166 |
indt (j+i) ^"<METHODID>\n"^
|
|
wneuper@825
|
167 |
id2xml (j+2*i) mI ^
|
|
rgradisc@1114
|
168 |
indt (j+i) ^"</METHODID>\n"^
|
|
wneuper@825
|
169 |
indt j ^"</SPECIFICATION>\n"):xml;
|
|
wneuper@825
|
170 |
|
|
wneuper@1630
|
171 |
fun modspec2xml j ((b, p_, head, gfr, pre, spec): ocalhd) =
|
|
wneuper@1630
|
172 |
(indt j ^"<CALCHEAD status = "^
|
|
wneuper@1630
|
173 |
quote (if b then "correct" else "incorrect")^">\n"^
|
|
wneuper@971
|
174 |
indt (j+1) ^"<HEAD>\n"^
|
|
wneuper@971
|
175 |
term2xml (j+1) head^"\n"^
|
|
wneuper@1630
|
176 |
indt (j+1) ^"</HEAD>\n"^
|
|
wneuper@825
|
177 |
model2xml (j+i) gfr pre ^
|
|
rgradisc@1174
|
178 |
indt (j+i) ^"<BELONGSTO> "^(case p_ of Pbl => "Pbl"
|
|
wneuper@1630
|
179 |
| Met => "Met"
|
|
wneuper@1630
|
180 |
| _ => "Und")^" </BELONGSTO>\n"^
|
|
wneuper@844
|
181 |
spec2xml (j+i) spec ^
|
|
rgradisc@1114
|
182 |
indt j ^"</CALCHEAD>\n"):xml;
|
|
wneuper@1630
|
183 |
(* writeln (modspec2xml 2 e_ocalhd);
|
|
wneuper@1630
|
184 |
*)
|
|
wneuper@825
|
185 |
|
|
wneuper@856
|
186 |
fun sub2xml j (id, value) =
|
|
wneuper@856
|
187 |
(indt j ^"<PAIR>\n"^
|
|
wneuper@856
|
188 |
indt j ^" <VARIABLE>\n"^
|
|
wneuper@856
|
189 |
term2xml (j+i) id ^ "\n" ^
|
|
wneuper@856
|
190 |
indt j ^" </VARIABLE>\n" ^
|
|
wneuper@856
|
191 |
indt j ^" <VALUE>\n"^
|
|
wneuper@856
|
192 |
term2xml (j+i) value ^ "\n" ^
|
|
wneuper@856
|
193 |
indt j ^" </VALUE>\n" ^
|
|
wneuper@856
|
194 |
indt j ^"</PAIR>\n"):xml;
|
|
wneuper@825
|
195 |
|
|
wneuper@856
|
196 |
fun subs2xml j (subs:subs) =
|
|
wneuper@856
|
197 |
(indt j ^"<SUBSTITUTION>\n"^
|
|
wneuper@856
|
198 |
foldl op^ ("", map (sub2xml (j+i))
|
|
wneuper@856
|
199 |
(subs2subst (assoc_thy "Isac.thy") subs)) ^
|
|
wneuper@856
|
200 |
indt j ^"</SUBSTITUTION>\n"):xml;
|
|
wneuper@856
|
201 |
(* val subs = [(str2term "bdv", str2term "x")];
|
|
wneuper@856
|
202 |
writeln(subs2xml 0 subs);
|
|
wneuper@856
|
203 |
*)
|
|
wneuper@825
|
204 |
|
|
wneuper@825
|
205 |
fun pos_2xml j pos_ =
|
|
wneuper@825
|
206 |
(indt j) ^ "<POS> " ^ pos_2str pos_ ^ " </POS>\n";
|
|
wneuper@825
|
207 |
|
|
wneuper@1974
|
208 |
(*.due to specialties of isac/util/parser/XMLParseDigest.java
|
|
wneuper@1974
|
209 |
pos' requires different tags.*)
|
|
wneuper@1974
|
210 |
fun pos'2xml j (tag, (pos, pos_)) =
|
|
wneuper@1974
|
211 |
indt j ^ "<" ^ tag ^ ">\n" ^
|
|
wneuper@825
|
212 |
ints2xml (j + i) pos ^
|
|
wneuper@825
|
213 |
pos_2xml (j + i) pos_ ^
|
|
wneuper@1974
|
214 |
indt j ^ "</" ^ tag ^ ">\n";
|
|
wneuper@1974
|
215 |
(* writeln(pos'2xml 3 ("POSITION", ([1,2,3], Pbl)));
|
|
wneuper@825
|
216 |
*)
|
|
wneuper@825
|
217 |
|
|
wneuper@825
|
218 |
|
|
wneuper@825
|
219 |
|
|
wneuper@825
|
220 |
fun thmstr2xml j str = ((((term2xml j) o str2term) str)^"\n"):xml;
|
|
wneuper@825
|
221 |
|
|
wneuper@825
|
222 |
fun thm'2xml j ((ID, form):thm') =
|
|
wneuper@825
|
223 |
(indt j ^"<THEOREM>\n"^
|
|
wneuper@825
|
224 |
indt (j+i) ^"<ID> "^ID^" </ID>\n"^
|
|
wneuper@825
|
225 |
indt (j+i) ^"<FORMULA>\n"^
|
|
wneuper@825
|
226 |
thmstr2xml (j+i) form^
|
|
wneuper@825
|
227 |
indt (j+i) ^"</FORMULA>\n"^
|
|
wneuper@825
|
228 |
indt j ^"</THEOREM>\n"):xml;
|
|
wneuper@825
|
229 |
|
|
wneuper@825
|
230 |
fun tac2xml j (Subproblem (dI, pI)) =
|
|
rgradisc@1152
|
231 |
(indt j ^"<SUBPROBLEMTACTIC name=\"Subproblem\">\n"^
|
|
rgradisc@942
|
232 |
indt (j+i) ^"<THEORY> "^ dI ^" </THEORY>\n"^
|
|
rgradisc@942
|
233 |
indt (j+i) ^"<PROBLEM>\n"^
|
|
rgradisc@942
|
234 |
id2xml (j+2*i) pI^
|
|
rgradisc@942
|
235 |
indt (j+i) ^"</PROBLEM>\n"^
|
|
rgradisc@1152
|
236 |
indt j ^"</SUBPROBLEMTACTIC>\n"):xml
|
|
wneuper@825
|
237 |
| tac2xml j (Model_Problem pI) =
|
|
rgradisc@1154
|
238 |
(indt j ^"<STRINGLISTTACTIC name=\"Model_Problem\">\n"^
|
|
rgradisc@942
|
239 |
id2xml (j+i) pI^
|
|
rgradisc@1154
|
240 |
indt j ^"</STRINGLISTTACTIC>\n"):xml
|
|
wneuper@825
|
241 |
| tac2xml j (Refine_Tacitly pI) =
|
|
rgradisc@1154
|
242 |
(indt j ^"<STRINGLISTTACTIC name=\"Refine_Tacitly\">\n"^
|
|
rgradisc@957
|
243 |
id2xml (j+i) pI^
|
|
rgradisc@1154
|
244 |
indt j ^"</STRINGLISTTACTIC>\n"):xml
|
|
wneuper@825
|
245 |
|
|
wneuper@825
|
246 |
| tac2xml j (Add_Given ct) =
|
|
rgradisc@1114
|
247 |
(indt j ^"<SIMPLETACTIC name=\"Add_Given\">\n"^
|
|
rgradisc@942
|
248 |
cterm2xml (j+i) ct^
|
|
rgradisc@1114
|
249 |
indt j ^"</SIMPLETACTIC>\n"):xml
|
|
wneuper@825
|
250 |
| tac2xml j (Add_Find ct) =
|
|
rgradisc@1114
|
251 |
(indt j ^"<SIMPLETACTIC name=\"Add_Find\">\n"^
|
|
rgradisc@942
|
252 |
cterm2xml (j+i) ct^
|
|
rgradisc@1114
|
253 |
indt j ^"</SIMPLETACTIC>\n"):xml
|
|
wneuper@825
|
254 |
| tac2xml j (Add_Relation ct) =
|
|
rgradisc@1114
|
255 |
(indt j ^"<SIMPLETACTIC name=\"Add_Relation\">\n"^
|
|
rgradisc@942
|
256 |
cterm2xml (j+i) ct^
|
|
rgradisc@1114
|
257 |
indt j ^"</SIMPLETACTIC>\n"):xml
|
|
wneuper@825
|
258 |
|
|
wneuper@844
|
259 |
| tac2xml j (Specify_Theory ct) =
|
|
rgradisc@1114
|
260 |
(indt j ^"<SIMPLETACTIC name=\"Specify_Theory\">\n"^
|
|
rgradisc@942
|
261 |
cterm2xml (j+i) ct^
|
|
rgradisc@1114
|
262 |
indt j ^"</SIMPLETACTIC>\n"):xml
|
|
wneuper@825
|
263 |
| tac2xml j (Specify_Problem ct) =
|
|
rgradisc@1154
|
264 |
(indt j ^"<STRINGLISTTACTIC name=\"Specify_Problem\">\n"^
|
|
rgradisc@942
|
265 |
id2xml (j+i) ct^
|
|
rgradisc@1154
|
266 |
indt j ^"</STRINGLISTTACTIC>\n"):xml
|
|
wneuper@825
|
267 |
| tac2xml j (Specify_Method ct) =
|
|
rgradisc@1154
|
268 |
(indt j ^"<STRINGLISTTACTIC name=\"Specify_Method\">\n"^
|
|
rgradisc@942
|
269 |
id2xml (j+i) ct^
|
|
rgradisc@1154
|
270 |
indt j ^"</STRINGLISTTACTIC>\n"):xml
|
|
wneuper@856
|
271 |
| tac2xml j (Apply_Method mI) =
|
|
rgradisc@1154
|
272 |
(indt j ^"<STRINGLISTTACTIC name=\"Apply_Method\">\n"^
|
|
rgradisc@942
|
273 |
id2xml (j+i) mI^
|
|
rgradisc@1154
|
274 |
indt j ^"</STRINGLISTTACTIC>\n"):xml
|
|
wneuper@825
|
275 |
|
|
wneuper@825
|
276 |
| tac2xml j (Rewrite thm') =
|
|
wneuper@1782
|
277 |
(indt j ^"<REWRITETACTIC name=\"Rewrite\">\n"^
|
|
rgradisc@942
|
278 |
thm'2xml (j+i) thm'^
|
|
wneuper@1782
|
279 |
indt j ^"</REWRITETACTIC>\n"):xml
|
|
wneuper@1782
|
280 |
(* writeln (tac2xml 2 (Rewrite ("all_left",
|
|
wneuper@1782
|
281 |
"~ ?b =!= 0 ==> (?a = ?b) = (?a - ?b = 0)")));
|
|
wneuper@1782
|
282 |
*)
|
|
wneuper@825
|
283 |
| tac2xml j (Rewrite_Inst (subs, thm')) =
|
|
wneuper@1782
|
284 |
(indt j ^"<REWRITEINSTTACTIC name=\"Rewrite_Inst\">\n"^
|
|
rgradisc@942
|
285 |
subs2xml (j+i) subs^
|
|
rgradisc@942
|
286 |
thm'2xml (j+i) thm'^
|
|
wneuper@1782
|
287 |
indt j ^"</REWRITEINSTTACTIC>\n"):xml
|
|
wneuper@1782
|
288 |
(* writeln (tac2xml 2 (Rewrite_Inst
|
|
wneuper@1782
|
289 |
(["(bdv,x)"],
|
|
wneuper@1782
|
290 |
("all_left",
|
|
wneuper@1782
|
291 |
"~ ?b =!= 0 ==> (?a = ?b) = (?a - ?b = 0)"))));
|
|
wneuper@1782
|
292 |
*)
|
|
wneuper@825
|
293 |
| tac2xml j (Rewrite_Set rls') =
|
|
rgradisc@1114
|
294 |
(indt j ^"<REWRITESETTACTIC name=\"Rewrite_Set\">\n"^
|
|
rgradisc@942
|
295 |
indt (j+i) ^"<RULESET> "^ rls' ^" </RULESET>\n"^
|
|
rgradisc@1114
|
296 |
indt j ^"</REWRITESETTACTIC>\n"):xml
|
|
wneuper@825
|
297 |
| tac2xml j (Rewrite_Set_Inst (subs, rls')) =
|
|
rgradisc@1114
|
298 |
(indt j ^"<REWRITESETINSTTACTIC name=\"Rewrite_Set_Inst\">\n"^
|
|
rgradisc@942
|
299 |
indt (j+i) ^"<RULESET> "^ rls' ^" </RULESET>\n"^
|
|
rgradisc@942
|
300 |
subs2xml (j+i) subs^
|
|
rgradisc@1114
|
301 |
indt j ^"</REWRITESETINSTTACTIC>\n"):xml
|
|
wneuper@825
|
302 |
|
|
wneuper@1250
|
303 |
| tac2xml j (Or_to_List) =
|
|
wneuper@1250
|
304 |
(indt j ^"<STRINGLISTTACTIC name=\"Or_to_List\"> \
|
|
wneuper@1250
|
305 |
\</STRINGLISTTACTIC>\n"):xml
|
|
wneuper@856
|
306 |
| tac2xml j (Check_elementwise ct) =
|
|
rgradisc@1154
|
307 |
(indt j ^"<SIMPLETACTIC name=\"Check_elementwise\">\n"^
|
|
rgradisc@942
|
308 |
term2xml (j+i)
|
|
wneuper@856
|
309 |
(str2term ct
|
|
rgradisc@942
|
310 |
(*FIXME.WN.9.03: redesign cterm' for xml-output*)) ^ "\n"^
|
|
rgradisc@1154
|
311 |
indt j ^"</SIMPLETACTIC>\n"):xml
|
|
wneuper@856
|
312 |
| tac2xml j (Check_Postcond pI) =
|
|
rgradisc@1154
|
313 |
(indt j ^"<STRINGLISTTACTIC name=\"Check_Postcond\">\n"^
|
|
rgradisc@942
|
314 |
id2xml (j+i) pI^
|
|
rgradisc@1154
|
315 |
indt j ^"</STRINGLISTTACTIC>\n"):xml
|
|
wneuper@856
|
316 |
|
|
wneuper@825
|
317 |
| tac2xml j tac = raise error ("tac2xml: not impl. for "^tac2str tac);
|
|
wneuper@825
|
318 |
|
|
wneuper@1399
|
319 |
fun tacs2xml j [] = "":xml
|
|
wneuper@1399
|
320 |
| tacs2xml j (t::ts) = tac2xml j t ^ tacs2xml j ts;
|
|
wneuper@1399
|
321 |
|
|
wneuper@1399
|
322 |
|
|
wneuper@1974
|
323 |
fun pos'form2xml j ("stepform", p:string * pos', f) =
|
|
wneuper@1334
|
324 |
indt j ^"<STEPFORMULA>\n"^
|
|
wneuper@1334
|
325 |
pos'2xml (j+i) p ^
|
|
wneuper@1334
|
326 |
term2xml j f^"\n"^
|
|
wneuper@1334
|
327 |
indt j ^"</STEPFORMULA>\n"
|
|
wneuper@1334
|
328 |
| pos'form2xml j ("headline", p, f) =
|
|
wneuper@1334
|
329 |
indt j ^"<HEADLINE>\n"^
|
|
wneuper@1334
|
330 |
pos'2xml (j+i) p ^
|
|
wneuper@1334
|
331 |
term2xml j f^"\n"^
|
|
wneuper@1334
|
332 |
indt j ^"</HEADLINE>\n";
|
|
wneuper@1334
|
333 |
|
|
wneuper@1334
|
334 |
fun pos'forms2xml j [] = ("":xml)
|
|
wneuper@1334
|
335 |
| pos'forms2xml j (r::rs) = pos'form2xml j r ^ pos'forms2xml j rs;
|