neuper@37906
|
1 |
(* convert sml-datatypes to xml
|
neuper@37906
|
2 |
authors: Walther Neuper 2003
|
neuper@37906
|
3 |
(c) due to copyright terms
|
neuper@37906
|
4 |
|
neuper@37906
|
5 |
use"xmlsrc/datatypes.sml";
|
neuper@37906
|
6 |
use"datatypes.sml";
|
neuper@37906
|
7 |
*)
|
neuper@37906
|
8 |
|
neuper@37940
|
9 |
|
neuper@37906
|
10 |
signature DATATYPES =
|
neuper@37906
|
11 |
sig
|
neuper@37906
|
12 |
val authors2xml : int -> string -> string list -> xml
|
neuper@37906
|
13 |
val calc2xml : int -> thyID * calc -> xml
|
neuper@37906
|
14 |
val calcrefs2xml : int -> thyID * calc list -> xml
|
neuper@37906
|
15 |
val contthy2xml : int -> contthy -> xml
|
neuper@37906
|
16 |
val extref2xml : int -> string -> string -> xml
|
neuper@37906
|
17 |
val filterpbl :
|
neuper@37906
|
18 |
''a -> (''a * (Term.term * Term.term)) list -> Term.term list
|
neuper@37906
|
19 |
val formula2xml : int -> Term.term -> xml
|
neuper@37906
|
20 |
val formulae2xml : int -> Term.term list -> xml
|
neuper@37906
|
21 |
val i : int
|
neuper@37906
|
22 |
val id2xml : int -> string list -> string
|
neuper@37906
|
23 |
val ints2xml : int -> int list -> string
|
neuper@37906
|
24 |
val itm_2xml : int -> SpecifyTools.itm_ -> xml
|
neuper@37906
|
25 |
val itms2xml :
|
neuper@37906
|
26 |
int ->
|
neuper@37906
|
27 |
(int * SpecifyTools.vats * bool * string * SpecifyTools.itm_) list ->
|
neuper@37906
|
28 |
string
|
neuper@37906
|
29 |
val keref2xml : int -> ketype -> kestoreID -> xml
|
neuper@37906
|
30 |
val model2xml :
|
neuper@37906
|
31 |
int -> SpecifyTools.itm list -> (bool * Term.term) list -> xml
|
neuper@37906
|
32 |
val modspec2xml : int -> ocalhd -> xml
|
neuper@37906
|
33 |
val pattern2xml :
|
neuper@37906
|
34 |
int ->
|
neuper@37906
|
35 |
(string * (Term.term * Term.term)) list -> Term.term list -> string
|
neuper@37906
|
36 |
val pos'2xml : int -> string * (int list * pos_) -> string
|
neuper@37906
|
37 |
val pos'calchead2xml : int -> pos' * ocalhd -> xml
|
neuper@37906
|
38 |
val pos_2xml : int -> pos_ -> string
|
neuper@37906
|
39 |
val posform2xml : int -> pos' * Term.term -> xml
|
neuper@37906
|
40 |
val posformhead2xml : int -> pos' * ptform -> string
|
neuper@37906
|
41 |
val posformheads2xml : int -> (pos' * ptform) list -> xml
|
neuper@37906
|
42 |
val posforms2xml : int -> (pos' * Term.term) list -> xml
|
neuper@37906
|
43 |
val posterms2xml : int -> (pos' * term) list -> xml
|
neuper@37906
|
44 |
val precond2xml : int -> bool * Term.term -> xml
|
neuper@37906
|
45 |
val preconds2xml : int -> (bool * Term.term) list -> xml
|
neuper@37906
|
46 |
val rls2xml : int -> thyID * rls -> xml
|
neuper@37906
|
47 |
val rule2xml : int -> guh -> rule -> xml
|
neuper@37906
|
48 |
val rules2xml : int -> guh -> rule list -> xml
|
neuper@37906
|
49 |
val scr2xml : int -> scr -> xml
|
neuper@37906
|
50 |
val spec2xml : int -> spec -> xml
|
neuper@37906
|
51 |
val sub2xml : int -> Term.term * Term.term -> xml
|
neuper@37906
|
52 |
val subs2xml : int -> subs -> xml
|
neuper@37906
|
53 |
val subst2xml : int -> subst -> xml
|
neuper@37906
|
54 |
val tac2xml : int -> tac -> xml
|
neuper@37906
|
55 |
val tacs2xml : int -> tac list -> xml
|
neuper@37906
|
56 |
val theref2xml : int -> thyID -> string -> xstring -> string
|
neuper@37906
|
57 |
val thm'2xml : int -> thm' -> xml
|
neuper@37906
|
58 |
val thm''2xml : int -> thm -> xml
|
neuper@37906
|
59 |
val thmstr2xml : int -> string -> xml
|
neuper@37906
|
60 |
end
|
neuper@37906
|
61 |
|
neuper@37906
|
62 |
|
neuper@37906
|
63 |
|
wneuper@59124
|
64 |
(*------------------------------------------------------------------
|
neuper@37906
|
65 |
structure datatypes:DATATYPES =
|
neuper@37940
|
66 |
(*structure datatypes =*)
|
neuper@37906
|
67 |
struct
|
wneuper@59124
|
68 |
------------------------------------------------------------------*)
|
neuper@37906
|
69 |
|
neuper@37906
|
70 |
val i = indentation;
|
neuper@37906
|
71 |
|
wneuper@59124
|
72 |
local
|
wneuper@59127
|
73 |
fun indent i = fold (curry op ^) (replicate i ". ") ""
|
wneuper@59124
|
74 |
in
|
wneuper@59124
|
75 |
fun xmlstr i (XML.Text str) = indent i ^ str ^ "\n"
|
wneuper@59124
|
76 |
| xmlstr i (XML.Elem ((str, []), trees)) =
|
wneuper@59124
|
77 |
indent i ^ "<" ^ str ^ ">" ^ "\n" ^
|
wneuper@59124
|
78 |
List.foldr op ^ "" (map (xmlstr (i + 1)) trees) ^
|
wneuper@59124
|
79 |
indent i ^ "</" ^ str ^ ">" ^ "\n"
|
wneuper@59124
|
80 |
| xmlstr i (XML.Elem ((str, [("status", a)]), trees)) =
|
wneuper@59124
|
81 |
indent i ^ "<" ^ str ^ " status " ^ a ^ ">" ^ "\n" ^
|
wneuper@59124
|
82 |
List.foldr op ^ "" (map (xmlstr (i + 1)) trees) ^
|
wneuper@59124
|
83 |
indent i ^ "</" ^ str ^ ">" ^ "\n"
|
wneuper@59124
|
84 |
| xmlstr _ (XML.Elem ((_, (_ :: _)), _)) =
|
wneuper@59124
|
85 |
error "xmlstr: TODO review attribute \"status\" etc";
|
wneuper@59124
|
86 |
end
|
wneuper@59124
|
87 |
|
neuper@37906
|
88 |
(** general types: lists, **)
|
neuper@37906
|
89 |
|
wneuper@59124
|
90 |
fun xml_of_bool b = XML.Elem (("BOOL", []), [XML.Text (bool2str b)])
|
wneuper@59124
|
91 |
fun xml_to_bool (XML.Elem (("BOOL", []), [XML.Text b])) = string_to_bool b
|
wneuper@59124
|
92 |
| xml_to_bool tree = error ("xml_to_int: wrong XML.tree " ^ xmlstr 0 tree)
|
wneuper@59124
|
93 |
|
neuper@37906
|
94 |
(*.handles string list like 'fun id2xml'.*)
|
neuper@37906
|
95 |
fun authors2xml j str auts =
|
neuper@37906
|
96 |
let fun autx _ [] = ""
|
neuper@37906
|
97 |
| autx j (s::ss) = (indt j) ^ "<STRING> " ^ s ^ " </STRING>\n" ^
|
neuper@37906
|
98 |
(autx j ss)
|
neuper@37906
|
99 |
in indt j ^ "<"^str^">\n" ^
|
neuper@37906
|
100 |
autx (j + i) auts ^
|
neuper@37906
|
101 |
indt j ^ "</"^str^">\n" : xml
|
neuper@37906
|
102 |
end;
|
neuper@38031
|
103 |
(* writeln(authors2xml 2 "MATHAUTHORS" []);
|
neuper@38031
|
104 |
writeln(authors2xml 2 "MATHAUTHORS"
|
neuper@37906
|
105 |
["isac-team 2001", "Richard Lang 2003"]);
|
neuper@37906
|
106 |
*)
|
neuper@37906
|
107 |
|
neuper@37906
|
108 |
fun id2xml j ids =
|
neuper@37906
|
109 |
let fun id2x _ [] = ""
|
neuper@37906
|
110 |
| id2x j (s::ss) = (indt j) ^ "<STRING> " ^ s ^ " </STRING>\n" ^
|
neuper@37906
|
111 |
(id2x j ss)
|
neuper@37906
|
112 |
in (indt j) ^ "<STRINGLIST>\n" ^
|
neuper@37906
|
113 |
(id2x (j + indentation) ids) ^
|
neuper@37906
|
114 |
(indt j) ^ "</STRINGLIST>\n" end;
|
neuper@38031
|
115 |
(* writeln(id2xml 8 ["linear","univariate","equation"]);
|
neuper@37906
|
116 |
<STRINGLIST>
|
neuper@37906
|
117 |
<STRING>linear</STRING>
|
neuper@37906
|
118 |
<STRING>univariate</STRING>
|
neuper@37906
|
119 |
<STRING>equation</STRING>
|
neuper@37906
|
120 |
</STRINGLIST>*)
|
neuper@37906
|
121 |
|
wneuper@59124
|
122 |
fun xml_of_str str = XML.Elem (("STRING", []), [XML.Text str])
|
wneuper@59124
|
123 |
fun xml_of_strs strs = XML.Elem (("STRINGLIST", []), map xml_of_str strs)
|
wneuper@59124
|
124 |
|
wneuper@59124
|
125 |
fun xml_to_str (XML.Elem (("STRING", []), [XML.Text str])) = str
|
wneuper@59124
|
126 |
| xml_to_str tree = error ("xml_to_str: wrong XML.tree " ^ xmlstr 0 tree)
|
wneuper@59124
|
127 |
fun xml_to_strs (XML.Elem (("STRINGLIST", []), strs)) = map xml_to_str strs
|
wneuper@59124
|
128 |
| xml_to_strs tree = error ("xml_to_strs: wrong XML.tree " ^ xmlstr 0 tree)
|
wneuper@59124
|
129 |
|
neuper@37906
|
130 |
fun ints2xml j ids =
|
neuper@37906
|
131 |
let fun int2x _ [] = ""
|
neuper@37906
|
132 |
| int2x j (s::ss) = (indt j) ^"<INT> "^ string_of_int s ^" </INT>\n"^
|
neuper@37906
|
133 |
(int2x j ss)
|
neuper@37906
|
134 |
in (indt j) ^ "<INTLIST>\n" ^
|
neuper@37906
|
135 |
(int2x (j + i) ids) ^
|
neuper@37906
|
136 |
(indt j) ^ "</INTLIST>\n" end;
|
neuper@38031
|
137 |
(* writeln(ints2xml 3 [1,2,3]);
|
neuper@37906
|
138 |
*)
|
wneuper@59124
|
139 |
fun xml_of_int i = XML.Elem (("INT", []), [XML.Text (string_of_int i)])
|
wneuper@59124
|
140 |
fun xml_of_ints is = (*xml/datatypes.sml: fun ints2xml*)
|
wneuper@59124
|
141 |
XML.Elem (("INTLIST", []), map xml_of_int is)
|
wneuper@59124
|
142 |
|
wneuper@59124
|
143 |
fun xml_to_int (XML.Elem (("INT", []), [XML.Text i])) =
|
wneuper@59124
|
144 |
(case int_of_str i of SOME i => i | _ => error "xml_to_int: int_of_str \<Rightarrow> NONE")
|
wneuper@59124
|
145 |
| xml_to_int tree = error ("xml_to_int: wrong XML.tree " ^ xmlstr 0 tree)
|
wneuper@59124
|
146 |
fun xml_to_ints (XML.Elem (("INTLIST", []), is)) = map xml_to_int is
|
wneuper@59124
|
147 |
| xml_to_ints tree = error ("xml_to_ints: wrong XML.tree " ^ xmlstr 0 tree)
|
neuper@37906
|
148 |
|
neuper@37906
|
149 |
|
neuper@37906
|
150 |
(** isac datatypes **)
|
neuper@37906
|
151 |
|
neuper@37906
|
152 |
fun pos_2xml j pos_ =
|
neuper@37906
|
153 |
(indt j) ^ "<POS> " ^ pos_2str pos_ ^ " </POS>\n";
|
neuper@37906
|
154 |
|
neuper@37906
|
155 |
(*.due to specialties of isac/util/parser/XMLParseDigest.java
|
neuper@37906
|
156 |
pos' requires different tags.*)
|
neuper@37906
|
157 |
fun pos'2xml j (tag, (pos, pos_)) =
|
neuper@37906
|
158 |
indt (j) ^ "<" ^ tag ^ ">\n" ^
|
neuper@37906
|
159 |
ints2xml (j+i) pos ^
|
neuper@37906
|
160 |
pos_2xml (j+i) pos_ ^
|
neuper@37906
|
161 |
indt (j) ^ "</" ^ tag ^ ">\n";
|
neuper@38031
|
162 |
(* writeln(pos'2xml 3 ("POSITION", ([1,2,3], Pbl)));
|
neuper@37906
|
163 |
*)
|
wneuper@59124
|
164 |
fun xml_of_pos tag (is, pp) = (*xml/datatypes.sml: fun pos'2xml*)
|
wneuper@59124
|
165 |
XML.Elem ((tag, []), [
|
wneuper@59124
|
166 |
xml_of_ints is,
|
wneuper@59124
|
167 |
XML.Elem (("POS", []), [XML.Text (pos_2str pp)])])
|
wneuper@59124
|
168 |
|
wneuper@59124
|
169 |
fun xml_to_pos_ (XML.Elem (("POS", []), [XML.Text pp])) = str2pos_ pp
|
wneuper@59124
|
170 |
| xml_to_pos_ tree = error ("xml_to_pos_: wrong XML.tree " ^ xmlstr 0 tree)
|
wneuper@59124
|
171 |
fun xml_to_pos (XML.Elem (("POSITION", []), [is, pp])) = (xml_to_ints is, xml_to_pos_ pp) (*: pos'*)
|
wneuper@59124
|
172 |
| xml_to_pos tree = error ("xml_to_pos: wrong XML.tree " ^ xmlstr 0 tree)
|
wneuper@59124
|
173 |
|
wneuper@59124
|
174 |
fun xml_of_auto (Step i) =
|
wneuper@59124
|
175 |
XML.Elem (("AUTO", []), [XML.Text "Step", XML.Text (string_of_int i)])
|
wneuper@59124
|
176 |
| xml_of_auto CompleteModel = XML.Elem (("AUTO", []), [XML.Text "CompleteModel"])
|
wneuper@59124
|
177 |
| xml_of_auto CompleteCalcHead = XML.Elem (("AUTO", []), [XML.Text "CompleteCalcHead"])
|
wneuper@59124
|
178 |
| xml_of_auto CompleteToSubpbl = XML.Elem (("AUTO", []), [XML.Text "CompleteToSubpbl"])
|
wneuper@59124
|
179 |
| xml_of_auto CompleteSubpbl = XML.Elem (("AUTO", []), [XML.Text "CompleteSubpbl"])
|
wneuper@59124
|
180 |
| xml_of_auto CompleteCalc = XML.Elem (("AUTO", []), [XML.Text "CompleteCalc"])
|
wneuper@59124
|
181 |
fun xml_to_auto (XML.Elem (("AUTO", []), [XML.Text "Step", XML.Text i])) = Step (int_of_str i |>the)
|
wneuper@59124
|
182 |
| xml_to_auto (XML.Elem (("AUTO", []), [XML.Text "CompleteModel"])) = CompleteModel
|
wneuper@59124
|
183 |
| xml_to_auto (XML.Elem (("AUTO", []), [XML.Text "CompleteCalcHead"])) = CompleteCalcHead
|
wneuper@59124
|
184 |
| xml_to_auto (XML.Elem (("AUTO", []), [XML.Text "CompleteToSubpbl"])) = CompleteToSubpbl
|
wneuper@59124
|
185 |
| xml_to_auto (XML.Elem (("AUTO", []), [XML.Text "CompleteSubpbl"])) = CompleteSubpbl
|
wneuper@59124
|
186 |
| xml_to_auto (XML.Elem (("AUTO", []), [XML.Text "CompleteCalc"])) = CompleteCalc
|
wneuper@59124
|
187 |
| xml_to_auto tree = error ("xml_to_auto: wrong XML.tree " ^ xmlstr 0 tree)
|
neuper@37906
|
188 |
|
neuper@37906
|
189 |
fun formula2xml j term = (*TODO.WN050211: use for _all_ <FORMULA>*)
|
neuper@37906
|
190 |
indt j ^ "<FORMULA>\n"^
|
neuper@37906
|
191 |
term2xml j term ^"\n"^
|
neuper@37906
|
192 |
indt j ^ "</FORMULA>\n" : xml;
|
neuper@38031
|
193 |
(* writeln(formula2xml 6 (str2term "1+1=2"));
|
neuper@37906
|
194 |
*)
|
neuper@37906
|
195 |
fun formulae2xml j [] = ("":xml)
|
neuper@37906
|
196 |
| formulae2xml j (r::rs) = formula2xml j r ^ formulae2xml j rs;
|
neuper@38031
|
197 |
(* writeln(formulae2xml 6 [str2term "1+1=2", str2term "1+1+1=3"]);
|
neuper@37906
|
198 |
*)
|
neuper@37906
|
199 |
|
neuper@37906
|
200 |
(*WN0502 @see ME/ctree: type asms: illdesigned, thus not used*)
|
neuper@37906
|
201 |
fun posform2xml j (p:pos', term) =
|
neuper@37906
|
202 |
indt j ^ "<POSFORM>\n" ^
|
neuper@37906
|
203 |
pos'2xml (j+i) ("POSITION", p) ^
|
neuper@37906
|
204 |
indt (j+i) ^ "<FORMULA>\n"^
|
neuper@37906
|
205 |
term2xml (j+i) term ^"\n"^
|
neuper@37906
|
206 |
indt (j+i) ^ "</FORMULA>\n"^
|
neuper@37906
|
207 |
indt j ^ "</POSFORM>\n" : xml;
|
neuper@38031
|
208 |
(* writeln(posform2xml 6 (([1,2],Frm), str2term "1+1=2"));
|
neuper@37906
|
209 |
*)
|
neuper@37906
|
210 |
fun posforms2xml j [] = ("":xml)
|
neuper@37906
|
211 |
| posforms2xml j (r::rs) = posform2xml j r ^ posforms2xml j rs;
|
neuper@38031
|
212 |
(* writeln(posforms2xml 6 [(([1],Res), str2term "1+1=2"),(([2],Res), str2term "1+1+1=3")]);
|
neuper@37906
|
213 |
*)
|
neuper@37906
|
214 |
|
neuper@37906
|
215 |
fun calcref2xml j (thyID:thyID, (scrop, (rewop, _)):calc) =
|
neuper@37906
|
216 |
indt j ^ "<CALCREF>\n" ^
|
neuper@37906
|
217 |
indt (j+i) ^ "<STRING> " ^ scrop ^ "</STRING>\n" ^
|
neuper@37906
|
218 |
indt (j+i) ^ "<GUH> " ^ cal2guh ("IsacKnowledge",
|
neuper@37906
|
219 |
thyID) scrop ^ " </GUH>\n" ^
|
neuper@37906
|
220 |
indt j ^ "</CALCREF>\n" : xml;
|
neuper@37906
|
221 |
fun calcrefs2xml _ (_,[]) = "":xml
|
neuper@37906
|
222 |
| calcrefs2xml j (thyID, cal::cs) =
|
neuper@37906
|
223 |
calcref2xml j (thyID, cal) ^ calcrefs2xml j (thyID, cs);
|
neuper@37906
|
224 |
|
neuper@37906
|
225 |
fun calc2xml j (thyID:thyID, (scrop, (rewop, _)):calc) =
|
neuper@37906
|
226 |
indt j ^ "<CALC>\n" ^
|
neuper@37906
|
227 |
indt (j+i) ^ "<STRING>\n" ^ scrop ^ "</STRING>\n" ^
|
neuper@37906
|
228 |
indt (j+i) ^ "<GUH>\n" ^ cal2guh ("IsacKnowledge",
|
neuper@37906
|
229 |
thyID) scrop ^ "</GUH>\n" ^
|
neuper@37906
|
230 |
indt (j+i) ^ "<TERMOP>\n" ^ rewop ^ "</TERMOP>\n" ^
|
neuper@37906
|
231 |
indt j ^ "</CALC>\n" : xml;
|
neuper@37906
|
232 |
|
neuper@37906
|
233 |
(*.for creating a href for a rule within an rls's rule list;
|
neuper@37906
|
234 |
the guh points to the thy of definition of the rule, NOT of use in rls.*)
|
neuper@37906
|
235 |
fun rule2xml j (thyID:thyID) Erule =
|
neuper@42407
|
236 |
error "rule2xml called with 'Erule'"
|
neuper@42400
|
237 |
| rule2xml j thyID (Thm (thmDeriv, thm)) =
|
neuper@42407
|
238 |
indt j ^ "<RULE>\n" ^
|
neuper@42407
|
239 |
indt (j+i) ^ "<TAG> Theorem </TAG>\n" ^
|
neuper@42407
|
240 |
indt (j+i) ^ "<STRING> " ^ thmID_of_derivation_name thmDeriv ^ " </STRING>\n" ^
|
neuper@42407
|
241 |
indt (j+i) ^ "<GUH> " ^
|
neuper@42407
|
242 |
thm2guh (thy_containing_thm thmDeriv) (thmID_of_derivation_name thmDeriv) ^ " </GUH>\n" ^
|
neuper@42407
|
243 |
indt j ^ "</RULE>\n" : xml
|
neuper@37906
|
244 |
| rule2xml j thyID (Calc (termop, _)) = ""
|
neuper@37906
|
245 |
(*FIXXXXXXXME.WN060714 in rls make Calc : calc -> rule [add scriptop!]
|
neuper@37906
|
246 |
see smltest/../datatypes.sml !
|
neuper@37906
|
247 |
indt j ^ "<RULE>\n" ^
|
neuper@37906
|
248 |
indt (j+i) ^ "<STRING> " ^ termop ^ " </STRING>\n" ^
|
neuper@37906
|
249 |
indt (j+i) ^ "<GUH> " ^ cal2guh (thy_containing_cal thyID termop)
|
neuper@37906
|
250 |
termop ^ " </GUH>\n" ^
|
neuper@37906
|
251 |
indt j ^ "</RULE>\n"
|
neuper@37906
|
252 |
*)
|
neuper@37906
|
253 |
| rule2xml j thyID (Cal1 (termop, _)) = ""
|
neuper@37906
|
254 |
| rule2xml j thyID (Rls_ rls) =
|
neuper@42407
|
255 |
let val rls' = (#id o rep_rls) rls
|
neuper@42407
|
256 |
in
|
neuper@42407
|
257 |
indt j ^ "<RULE>\n" ^
|
neuper@42407
|
258 |
indt (j+i) ^ "<TAG> Ruleset </TAG>\n" ^
|
neuper@42407
|
259 |
indt (j+i) ^ "<STRING> " ^ rls' ^ " </STRING>\n" ^
|
neuper@42407
|
260 |
indt (j+i) ^ "<GUH> " ^ rls2guh (thy_containing_rls thyID rls') rls' ^ " </GUH>\n" ^
|
neuper@42407
|
261 |
indt j ^ "</RULE>\n"
|
neuper@42407
|
262 |
end;
|
neuper@42407
|
263 |
|
neuper@37906
|
264 |
fun rules2xml j thyID [] = ("":xml)
|
neuper@37906
|
265 |
| rules2xml j thyID (r::rs) = rule2xml j thyID r ^ rules2xml j thyID rs;
|
neuper@37906
|
266 |
|
neuper@37906
|
267 |
fun filterpbl str =
|
neuper@37906
|
268 |
let fun filt [] = []
|
neuper@37906
|
269 |
| filt ((s, (t1, t2)) :: ps) =
|
neuper@37906
|
270 |
if str = s then (t1 $ t2) :: filt ps else filt ps
|
neuper@37906
|
271 |
in filt end;
|
neuper@37906
|
272 |
|
neuper@37906
|
273 |
(*FIXME.WN040831 model2xml <--?--> pattern2xml*)
|
neuper@38031
|
274 |
(*WN.25.8.03: pattern2xml different output with TextIO | writeln !!!
|
neuper@37906
|
275 |
the version below is for TextIO: terms2xml makes \n !*)
|
neuper@37906
|
276 |
(* val (j, p, where_) = (i, ppc, where_);
|
neuper@37906
|
277 |
*)
|
neuper@37906
|
278 |
fun pattern2xml j p where_ =
|
neuper@37906
|
279 |
(case filterpbl "#Given" p of
|
neuper@37906
|
280 |
[] => (indt j) ^ "<GIVEN> </GIVEN>\n"
|
neuper@37906
|
281 |
(* val gis = filterpbl "#Given" p;
|
neuper@37906
|
282 |
*)
|
neuper@37906
|
283 |
| gis => (indt j) ^ "<GIVEN>\n" ^ terms2xml' j gis ^
|
neuper@37906
|
284 |
(indt j) ^ "</GIVEN>\n")
|
neuper@37906
|
285 |
^
|
neuper@37906
|
286 |
(case where_ of
|
neuper@37906
|
287 |
[] => (indt j) ^ "<WHERE> </WHERE>\n"
|
neuper@37906
|
288 |
| whs => (indt j) ^ "<WHERE>\n" ^ terms2xml' j whs ^
|
neuper@37906
|
289 |
(indt j) ^ "</WHERE>\n")
|
neuper@37906
|
290 |
^
|
neuper@37906
|
291 |
(case filterpbl "#Find" p of
|
neuper@37906
|
292 |
[] => (indt j) ^ "<FIND> </FIND>\n"
|
neuper@37906
|
293 |
| fis => (indt j) ^ "<FIND>\n" ^ terms2xml' j fis ^
|
neuper@37906
|
294 |
(indt j) ^ "</FIND>\n")
|
neuper@37906
|
295 |
^
|
neuper@37906
|
296 |
(case filterpbl "#Relate" p of
|
neuper@37906
|
297 |
[] => (indt j) ^ "<RELATE> </RELATE>\n"
|
neuper@37906
|
298 |
| res => (indt j) ^ "<RELATE>\n" ^ terms2xml' j res ^
|
neuper@37906
|
299 |
(indt j) ^ "</RELATE>\n");
|
neuper@37906
|
300 |
(*
|
neuper@38031
|
301 |
writeln(pattern2xml 3 ((#ppc o get_pbt)
|
neuper@37906
|
302 |
["squareroot","univariate","equation","test"]) []);
|
neuper@37906
|
303 |
*)
|
neuper@37906
|
304 |
|
neuper@37906
|
305 |
(*see itm_2item*)
|
wneuper@59127
|
306 |
fun itm_2xml j (Cor (dts,_)) =
|
neuper@37906
|
307 |
(indt j ^"<ITEM status=\"correct\">\n"^
|
neuper@37906
|
308 |
term2xml (j) (comp_dts' dts)^"\n"^
|
neuper@37906
|
309 |
indt j ^"</ITEM>\n"):xml
|
neuper@37906
|
310 |
| itm_2xml j (Syn c) =
|
neuper@37906
|
311 |
indt j ^"<ITEM status=\"syntaxerror\">\n"^
|
neuper@37906
|
312 |
indt (j) ^c^
|
neuper@37906
|
313 |
indt j ^"</ITEM>\n"
|
neuper@37906
|
314 |
| itm_2xml j (Typ c) =
|
neuper@37906
|
315 |
indt j ^"<ITEM status=\"typeerror\">\n"^
|
neuper@37906
|
316 |
indt (j) ^c^
|
neuper@37906
|
317 |
indt j ^"</ITEM>\n"
|
neuper@37906
|
318 |
(*type item also has 'False of cterm' set in preconds2xml WN 050618*)
|
neuper@37906
|
319 |
| itm_2xml j (Inc (dts,_)) =
|
neuper@37906
|
320 |
indt j ^"<ITEM status=\"incomplete\">\n"^
|
neuper@37906
|
321 |
term2xml (j) (comp_dts' dts)^"\n"^
|
neuper@37906
|
322 |
indt j ^"</ITEM>\n"
|
neuper@37906
|
323 |
| itm_2xml j (Sup dts) =
|
neuper@37906
|
324 |
indt j ^"<ITEM status=\"superfluous\">\n"^
|
neuper@37906
|
325 |
term2xml (j) (comp_dts' dts)^"\n"^
|
neuper@37906
|
326 |
indt j ^"</ITEM>\n"
|
neuper@37906
|
327 |
| itm_2xml j (Mis (d,pid)) =
|
neuper@37906
|
328 |
indt j ^"<ITEM status=\"missing\">\n"^
|
neuper@37906
|
329 |
term2xml (j) (d $ pid)^"\n"^
|
neuper@37906
|
330 |
indt j ^"</ITEM>\n";
|
wneuper@59127
|
331 |
fun xml_of_itm_ (Cor (dts, _)) =
|
wneuper@59127
|
332 |
XML.Elem (("ITEM", [("status", "correct")]), [xml_of_term (comp_dts' dts)])
|
wneuper@59127
|
333 |
| xml_of_itm_ (Syn c) =
|
wneuper@59127
|
334 |
XML.Elem (("ITEM", [("status", "syntaxerror")]), [XML.Text c])
|
wneuper@59127
|
335 |
| xml_of_itm_ (Typ c) =
|
wneuper@59127
|
336 |
XML.Elem (("ITEM", [("status", "typeerror")]), [XML.Text c])
|
wneuper@59127
|
337 |
(*type item also has 'False of cterm' set in preconds2xml WN 050618*)
|
wneuper@59127
|
338 |
| xml_of_itm_ (Inc (dts, _)) =
|
wneuper@59127
|
339 |
XML.Elem (("ITEM", [("status", "incomplete")]), [xml_of_term (comp_dts' dts)])
|
wneuper@59127
|
340 |
| xml_of_itm_ (Sup dts) =
|
wneuper@59127
|
341 |
XML.Elem (("ITEM", [("status", "superfluous")]), [xml_of_term (comp_dts' dts)])
|
wneuper@59127
|
342 |
| xml_of_itm_ (Mis (d, pid)) =
|
wneuper@59127
|
343 |
XML.Elem (("ITEM", [("status", "missing")]), [xml_of_term (d $ pid)])
|
neuper@37906
|
344 |
|
neuper@37906
|
345 |
(*see terms2xml' fpr \n*)
|
neuper@37906
|
346 |
fun itms2xml _ [] = ""
|
neuper@37906
|
347 |
| itms2xml j [(_,_,_,_,itm_)] = itm_2xml j itm_
|
neuper@37906
|
348 |
| itms2xml j (((_,_,_,_,itm_):itm)::itms) =
|
neuper@37906
|
349 |
itm_2xml j itm_ ^ itms2xml j itms;
|
wneuper@59127
|
350 |
fun xml_of_itms itms =
|
wneuper@59127
|
351 |
let
|
wneuper@59127
|
352 |
fun extract (_, _, _, _, itm_) = itm_
|
wneuper@59127
|
353 |
| extract _ = error "xml_of_itms.extract: wrong argument"
|
wneuper@59127
|
354 |
in map (xml_of_itm_ o extract) itms end
|
neuper@37906
|
355 |
|
neuper@37906
|
356 |
fun precond2xml j (true, term) =
|
neuper@37906
|
357 |
(indt j ^"<ITEM status=\"correct\">\n"^
|
neuper@37906
|
358 |
term2xml (j) term^"\n"^
|
neuper@37906
|
359 |
indt j ^"</ITEM>\n"):xml
|
neuper@37906
|
360 |
| precond2xml j (false, term) =
|
neuper@37906
|
361 |
indt j ^"<ITEM status=\"false\">\n"^
|
neuper@37906
|
362 |
term2xml (j+i) term^"\n"^
|
neuper@37906
|
363 |
indt j ^"</ITEM>\n";
|
wneuper@59127
|
364 |
fun xml_of_precond (status, term) =
|
wneuper@59127
|
365 |
XML.Elem (("ITEM", [("status", if status then "correct" else "false")]), [xml_of_term term])
|
neuper@37906
|
366 |
|
neuper@37906
|
367 |
fun preconds2xml _ [] = ("":xml)
|
neuper@37906
|
368 |
| preconds2xml j (p::ps) = precond2xml j p ^ preconds2xml j ps;
|
wneuper@59127
|
369 |
fun xml_of_preconds ps = map xml_of_precond ps
|
neuper@37906
|
370 |
|
neuper@37906
|
371 |
(*FIXME.WN040831 model2xml <--?--> pattern2xml*)
|
neuper@37906
|
372 |
fun model2xml j (itms:itm list) where_ =
|
wneuper@59127
|
373 |
let fun eq4 str (_,_,_,field,_) = str = field
|
wneuper@59127
|
374 |
in (indt j ^"<MODEL>\n"^
|
wneuper@59127
|
375 |
(case filter (eq4 "#Given") itms of
|
wneuper@59127
|
376 |
[] => (indt (j+i)) ^ "<GIVEN> </GIVEN>\n"
|
wneuper@59127
|
377 |
| gis => (indt (j+i)) ^ "<GIVEN>\n" ^ itms2xml (j+2*i) gis ^
|
wneuper@59127
|
378 |
(indt (j+i)) ^ "</GIVEN>\n")
|
wneuper@59127
|
379 |
^
|
wneuper@59127
|
380 |
(case where_ of
|
wneuper@59127
|
381 |
[] => (indt (j+i)) ^ "<WHERE> </WHERE>\n"
|
wneuper@59127
|
382 |
| whs => (indt (j+i)) ^ "<WHERE>\n" ^ preconds2xml (j+2*i) whs ^
|
wneuper@59127
|
383 |
(indt (j+i)) ^ "</WHERE>\n")
|
wneuper@59127
|
384 |
^
|
wneuper@59127
|
385 |
(case filter (eq4 "#Find") itms of
|
wneuper@59127
|
386 |
[] => (indt (j+i)) ^ "<FIND> </FIND>\n"
|
wneuper@59127
|
387 |
| fis => (indt (j+i)) ^ "<FIND>\n" ^ itms2xml (j+2*i) fis ^
|
wneuper@59127
|
388 |
(indt (j+i)) ^ "</FIND>\n")
|
wneuper@59127
|
389 |
^
|
wneuper@59127
|
390 |
(case filter (eq4 "#Relate") itms of
|
wneuper@59127
|
391 |
[] => (indt (j+i)) ^ "<RELATE> </RELATE>\n"
|
wneuper@59127
|
392 |
| res => (indt (j+i)) ^ "<RELATE>\n" ^ itms2xml (j+2*i) res ^
|
wneuper@59127
|
393 |
(indt (j+i)) ^ "</RELATE>\n")^
|
wneuper@59127
|
394 |
indt j ^"</MODEL>\n"):xml
|
wneuper@59127
|
395 |
end;
|
neuper@38031
|
396 |
(* writeln(model2xml 3 itms []);
|
neuper@37906
|
397 |
*)
|
wneuper@59127
|
398 |
fun xml_of_model itms where_ =
|
wneuper@59127
|
399 |
let
|
wneuper@59127
|
400 |
fun eq str (_, _, _,field, _) = str = field
|
wneuper@59127
|
401 |
in
|
wneuper@59127
|
402 |
XML.Elem (("MODEL", []), [
|
wneuper@59127
|
403 |
XML.Elem (("GIVEN", []),
|
wneuper@59127
|
404 |
filter (eq "#Given") itms |> xml_of_itms),
|
wneuper@59127
|
405 |
XML.Elem (("WHERE", []),
|
wneuper@59127
|
406 |
xml_of_preconds where_),
|
wneuper@59127
|
407 |
XML.Elem (("FIND", []),
|
wneuper@59127
|
408 |
filter (eq "#Find") itms |> xml_of_itms),
|
wneuper@59127
|
409 |
XML.Elem (("RELATE", []),
|
wneuper@59127
|
410 |
filter (eq "#Relate") itms |> xml_of_itms)])
|
wneuper@59127
|
411 |
end
|
neuper@37906
|
412 |
|
neuper@37906
|
413 |
fun spec2xml j ((dI,pI,mI):spec) =
|
neuper@37906
|
414 |
(indt j ^"<SPECIFICATION>\n"^
|
neuper@37906
|
415 |
indt (j+i) ^"<THEORYID> "^ dI ^" </THEORYID>\n"^
|
neuper@37906
|
416 |
indt (j+i) ^"<PROBLEMID>\n"^
|
neuper@37906
|
417 |
id2xml (j+2*i) pI ^
|
neuper@37906
|
418 |
indt (j+i) ^"</PROBLEMID>\n"^
|
neuper@37906
|
419 |
indt (j+i) ^"<METHODID>\n"^
|
neuper@37906
|
420 |
id2xml (j+2*i) mI ^
|
neuper@37906
|
421 |
indt (j+i) ^"</METHODID>\n"^
|
neuper@37906
|
422 |
indt j ^"</SPECIFICATION>\n"):xml;
|
wneuper@59124
|
423 |
fun xml_of_spec (thyID, pblID, metID) =
|
wneuper@59124
|
424 |
XML.Elem (("SPECIFICATION", []), [
|
wneuper@59124
|
425 |
XML.Elem (("THEORYID", []), [XML.Text thyID]),
|
wneuper@59124
|
426 |
XML.Elem (("PROBLEMID", []), [xml_of_strs pblID]),
|
wneuper@59124
|
427 |
XML.Elem (("METHODID", []), [xml_of_strs metID])])
|
wneuper@59124
|
428 |
fun xml_to_spec (XML.Elem (("SPECIFICATION", []), [
|
wneuper@59124
|
429 |
XML.Elem (("THEORYID", []), [XML.Text thyID]),
|
wneuper@59124
|
430 |
XML.Elem (("PROBLEMID", []), ps),
|
wneuper@59124
|
431 |
XML.Elem (("METHODID", []), ms)])) = (thyID, map xml_to_strs ps, map xml_to_strs ms)
|
wneuper@59124
|
432 |
| xml_to_spec tree = error ("xml_to_spec: wrong XML.tree " ^ xmlstr 0 tree)
|
neuper@37906
|
433 |
|
neuper@37906
|
434 |
fun modspec2xml j ((b, p_, head, gfr, pre, spec): ocalhd) =
|
neuper@37906
|
435 |
(indt j ^"<CALCHEAD status = "^
|
neuper@37906
|
436 |
quote (if b then "correct" else "incorrect")^">\n"^
|
neuper@37906
|
437 |
indt (j+i) ^"<HEAD>\n"^
|
neuper@37906
|
438 |
term2xml (j+i) head^"\n"^
|
neuper@37906
|
439 |
indt (j+i) ^"</HEAD>\n"^
|
neuper@37906
|
440 |
model2xml (j+i) gfr pre ^
|
neuper@37906
|
441 |
indt (j+i) ^"<BELONGSTO> "^(case p_ of Pbl => "Pbl"
|
neuper@37906
|
442 |
| Met => "Met"
|
neuper@37906
|
443 |
| _ => "Und")^" </BELONGSTO>\n"^
|
neuper@37906
|
444 |
spec2xml (j+i) spec ^
|
neuper@37906
|
445 |
indt j ^"</CALCHEAD>\n"):xml;
|
wneuper@59129
|
446 |
fun xml_of_modspec j ((b, p_, head, gfr, pre, spec): ocalhd) =
|
wneuper@59129
|
447 |
XML.Elem (("CALCHEAD", [("status", if b then "correct" else "incorrect")]), [
|
wneuper@59129
|
448 |
XML.Elem (("HEAD", []), [xml_of_term head]),
|
wneuper@59129
|
449 |
XML.Elem (("BELONGSTO", []), [
|
wneuper@59129
|
450 |
XML.Text (case p_ of Pbl => "Pbl" | Met => "Met" | _ => "Und")]),
|
wneuper@59129
|
451 |
xml_of_model gfr pre,
|
wneuper@59129
|
452 |
xml_of_spec spec])
|
wneuper@59129
|
453 |
|
neuper@37906
|
454 |
fun pos'calchead2xml j (p:pos', (b, p_, head, gfr, pre, spec): ocalhd) =
|
neuper@37906
|
455 |
(indt j ^"<CALCHEAD status = "^
|
neuper@37906
|
456 |
quote (if b then "correct" else "incorrect")^">\n"^
|
neuper@37906
|
457 |
pos'2xml (j+i) ("POSITION", p) ^
|
neuper@37906
|
458 |
indt (j+i) ^"<HEAD>\n"^
|
neuper@37906
|
459 |
term2xml (j+i) head^"\n"^
|
neuper@37906
|
460 |
indt (j+i) ^"</HEAD>\n"^
|
neuper@37906
|
461 |
model2xml (j+i) gfr pre ^
|
neuper@37906
|
462 |
indt (j+i) ^"<BELONGSTO> "^(case p_ of Pbl => "Pbl"
|
neuper@37906
|
463 |
| Met => "Met"
|
neuper@37906
|
464 |
| _ => "Und")^" </BELONGSTO>\n"^
|
neuper@37906
|
465 |
spec2xml (j+i) spec ^
|
neuper@37906
|
466 |
indt j ^"</CALCHEAD>\n"):xml;
|
neuper@37906
|
467 |
|
neuper@37906
|
468 |
fun sub2xml j (id, value) =
|
neuper@37906
|
469 |
(indt j ^"<PAIR>\n"^
|
neuper@37906
|
470 |
indt j ^" <VARIABLE>\n"^
|
neuper@37906
|
471 |
term2xml (j+i) id ^ "\n" ^
|
neuper@37906
|
472 |
indt j ^" </VARIABLE>\n" ^
|
neuper@37906
|
473 |
indt j ^" <VALUE>\n"^
|
neuper@37906
|
474 |
term2xml (j+i) value ^ "\n" ^
|
neuper@37906
|
475 |
indt j ^" </VALUE>\n" ^
|
neuper@37906
|
476 |
indt j ^"</PAIR>\n"):xml;
|
neuper@37906
|
477 |
fun subs2xml j (subs:subs) =
|
neuper@37906
|
478 |
(indt j ^"<SUBSTITUTION>\n"^
|
neuper@37906
|
479 |
foldl op^ ("", map (sub2xml (j+i))
|
neuper@38050
|
480 |
(subs2subst (assoc_thy "Isac") subs)) ^
|
neuper@37906
|
481 |
indt j ^"</SUBSTITUTION>\n"):xml;
|
neuper@37906
|
482 |
(* val subs = [(str2term "bdv", str2term "x")];
|
neuper@37906
|
483 |
val subs = ["(bdv, x)"];
|
neuper@38031
|
484 |
writeln(subs2xml 0 subs);
|
neuper@37906
|
485 |
*)
|
neuper@37906
|
486 |
fun subst2xml j (subst:subst) =
|
neuper@37906
|
487 |
(indt j ^"<SUBSTITUTION>\n"^
|
neuper@37906
|
488 |
foldl op^ ("", map (sub2xml (j+i)) subst) ^
|
neuper@37906
|
489 |
indt j ^"</SUBSTITUTION>\n"):xml;
|
neuper@37906
|
490 |
(* val subst = [(str2term "bdv", str2term "x")];
|
neuper@38031
|
491 |
writeln(subst2xml 0 subst);
|
neuper@37906
|
492 |
*)
|
neuper@37906
|
493 |
|
neuper@37906
|
494 |
(* val (j, str) = ((j+i), form);
|
neuper@37906
|
495 |
*)
|
neuper@37906
|
496 |
fun thmstr2xml j str = ((((term2xml j) o str2term) str)^"\n"):xml;
|
neuper@37906
|
497 |
|
neuper@37906
|
498 |
(* val (j, ((ID, form):thm')) = ((j+i), thm');
|
neuper@37906
|
499 |
*)
|
neuper@37906
|
500 |
fun thm'2xml j ((ID, form):thm') =
|
neuper@37906
|
501 |
(indt j ^"<THEOREM>\n"^
|
neuper@37906
|
502 |
indt (j+i) ^"<ID> "^ID^" </ID>\n"^
|
neuper@37906
|
503 |
indt (j+i) ^"<FORMULA>\n"^
|
neuper@37906
|
504 |
thmstr2xml (j+i) form^
|
neuper@37906
|
505 |
indt (j+i) ^"</FORMULA>\n"^
|
neuper@37906
|
506 |
indt j ^"</THEOREM>\n"):xml;
|
neuper@37906
|
507 |
|
neuper@37906
|
508 |
(*WN060627 scope of thy's not considered ?!?*)
|
neuper@55490
|
509 |
fun thm''2xml j (thm : thm) =
|
neuper@55490
|
510 |
indt j ^ "<THEOREM>\n" ^
|
neuper@55490
|
511 |
indt (j+i) ^ "<ID> " ^ thmID_of_derivation_name' thm ^ " </ID>\n"^
|
neuper@55489
|
512 |
term2xml j (prop_of thm) ^ "\n" ^
|
neuper@55490
|
513 |
indt j ^ "</THEOREM>\n" : xml;
|
neuper@37906
|
514 |
|
neuper@37906
|
515 |
fun scr2xml j EmptyScr =
|
neuper@37906
|
516 |
indt j ^"<SCRIPT> </SCRIPT>\n" : xml
|
neuper@48763
|
517 |
| scr2xml j (Prog term) =
|
neuper@37906
|
518 |
if term = e_term
|
neuper@37906
|
519 |
then indt j ^"<SCRIPT> </SCRIPT>\n"
|
neuper@37906
|
520 |
else indt j ^"<SCRIPT>\n"^
|
neuper@38050
|
521 |
term2xml j (inst_abs (assoc_thy "Isac") term) ^ "\n" ^
|
neuper@37906
|
522 |
indt j ^"</SCRIPT>\n"
|
neuper@37906
|
523 |
| scr2xml j (Rfuns _) =
|
neuper@37906
|
524 |
indt j ^"<REVERSREWRITE> reverse rewrite functions </REVERSREWRITE>\n";
|
neuper@37906
|
525 |
|
neuper@37906
|
526 |
fun prepa12xml j (terms, term) =
|
neuper@37906
|
527 |
indt j ^"<PREPAT>\n"^
|
neuper@37906
|
528 |
indt (j+i) ^"<PRECONDS>\n"^
|
neuper@37906
|
529 |
terms2xml (j+2*i) terms ^
|
neuper@37906
|
530 |
indt (j+i) ^"</PRECONDS>\n"^
|
neuper@37906
|
531 |
indt (j+i) ^"<PATTERN>\n"^
|
neuper@37906
|
532 |
term2xml (j+2*i) term ^
|
neuper@37906
|
533 |
indt (j+i) ^"</PATTERN>\n"^
|
neuper@37906
|
534 |
indt j ^"</PREPAT>\n" : xml;
|
neuper@37906
|
535 |
|
neuper@37906
|
536 |
fun prepat2xml j [] = ""
|
neuper@37906
|
537 |
| prepat2xml j (p::ps) = prepa12xml j p ^ prepat2xml j ps : xml;
|
neuper@37906
|
538 |
|
neuper@37906
|
539 |
(* val (j, (thyID, seqrls, {id, preconds, rew_ord=(ord,_), erls,
|
neuper@37906
|
540 |
srls, calc, rules, scr})) =
|
neuper@37906
|
541 |
(j, (thyID, "Seq", data));
|
neuper@37906
|
542 |
*)
|
neuper@37906
|
543 |
fun rls2xm j (thyID, seqrls, {id, preconds, rew_ord=(ord,_), erls,
|
neuper@42451
|
544 |
srls, calc, rules, errpatts, scr}) =
|
neuper@37906
|
545 |
indt j ^"<RULESET>\n"^
|
neuper@37906
|
546 |
indt (j+i) ^"<ID> "^ id ^" </ID>\n"^
|
neuper@37906
|
547 |
indt (j+i) ^"<TYPE> "^ seqrls ^" </TYPE>\n"^
|
neuper@37906
|
548 |
indt (j+i) ^"<RULES>\n" ^
|
neuper@37906
|
549 |
rules2xml (j+2*i) thyID rules ^
|
neuper@37906
|
550 |
indt (j+i) ^"</RULES>\n" ^
|
neuper@37906
|
551 |
indt (j+i) ^"<PRECONDS> " ^
|
neuper@37906
|
552 |
terms2xml' (j+2*i) preconds ^
|
neuper@37906
|
553 |
indt (j+i) ^"</PRECONDS>\n" ^
|
neuper@37906
|
554 |
indt (j+i) ^"<ORDER>\n" ^
|
neuper@37906
|
555 |
indt (j+2*i) ^ "<STRING> " ^ ord ^ " </STRING>\n" ^
|
neuper@37906
|
556 |
(*WN060714 thy_isac_*-ord-*.xml not yet generated ................
|
neuper@37906
|
557 |
indt (j+2*i) ^ "<GUH> " ^ ord2guh ("IsacKnowledge",
|
neuper@37906
|
558 |
thyID) ord ^ " </GUH>\n" ^
|
neuper@37906
|
559 |
..................................................................*)
|
neuper@37906
|
560 |
indt (j+i) ^"</ORDER>\n" ^
|
neuper@37906
|
561 |
indt (j+i) ^"<ERLS>\n" ^
|
neuper@37906
|
562 |
indt (j+2*i) ^ "<TAG> Ruleset </TAG>\n" ^
|
neuper@37906
|
563 |
indt (j+2*i) ^ "<STRING> " ^ id_rls erls ^ " </STRING>\n" ^
|
neuper@37906
|
564 |
indt (j+2*i) ^ "<GUH> " ^ rls2guh ("IsacKnowledge", thyID)
|
neuper@37906
|
565 |
(id_rls erls) ^ " </GUH>\n" ^
|
neuper@37906
|
566 |
indt (j+i) ^"</ERLS>\n" ^
|
neuper@37906
|
567 |
indt (j+i) ^"<SRLS>\n" ^
|
neuper@37906
|
568 |
indt (j+2*i) ^ "<TAG> Ruleset </TAG>\n" ^
|
neuper@37906
|
569 |
indt (j+2*i) ^ "<STRING> " ^ id_rls erls ^ " </STRING>\n" ^
|
neuper@37906
|
570 |
indt (j+2*i) ^ "<GUH> " ^ rls2guh ("IsacKnowledge", thyID)
|
neuper@37906
|
571 |
(id_rls srls) ^ " </GUH>\n" ^
|
neuper@37906
|
572 |
indt (j+i) ^"</SRLS>\n" ^
|
neuper@37906
|
573 |
calcrefs2xml (j+i) (thyID, calc) ^
|
neuper@37906
|
574 |
scr2xml (j+i) scr ^
|
neuper@37906
|
575 |
indt j ^"</RULESET>\n" : xml;
|
neuper@37906
|
576 |
|
neuper@37906
|
577 |
fun rls2xml j (thyID, Erls) = rls2xml j (thyID, e_rls)
|
neuper@37906
|
578 |
| rls2xml j (thyID, Rls data) = rls2xm j (thyID, "Rls", data)
|
neuper@37906
|
579 |
| rls2xml j (thyID, Seq data) = rls2xm j (thyID, "Seq", data)
|
neuper@42451
|
580 |
| rls2xml j (thyID, Rrls {id, prepat, rew_ord=(ord,_), erls, calc, errpatts, scr}) =
|
neuper@37906
|
581 |
indt j ^"<RULESET>\n"^
|
neuper@37906
|
582 |
indt (j+i) ^"<ID> "^ id ^" </ID>\n"^
|
neuper@37906
|
583 |
indt (j+i) ^"<TYPE> Rrls </TYPE>\n"^
|
neuper@37906
|
584 |
prepat2xml (j+i) prepat ^
|
neuper@37906
|
585 |
indt (j+i) ^"<ORDER> " ^
|
neuper@37906
|
586 |
indt (j+2*i) ^ "<TAG> Rewrite order </TAG>\n" ^
|
neuper@37906
|
587 |
indt (j+2*i) ^ "<STRING> " ^ ord ^ " </STRING>\n" ^
|
neuper@37906
|
588 |
(*WN060714 thy_isac_*-ord-*.xml not yet generated ................
|
neuper@37906
|
589 |
indt (j+2*i) ^ "<GUH> " ^ ord2guh ("IsacKnowledge",
|
neuper@37906
|
590 |
thyID) ord ^ " </GUH>\n" ^
|
neuper@37906
|
591 |
.................................................................*)
|
neuper@37906
|
592 |
indt (j+i) ^"</ORDER>\n" ^
|
neuper@37906
|
593 |
indt (j+i) ^"<ERLS> " ^
|
neuper@37906
|
594 |
indt (j+2*i) ^ "<TAG> Ruleset </TAG>\n" ^
|
neuper@37906
|
595 |
indt (j+2*i) ^ "<STRING> " ^ id_rls erls ^ " </STRING>\n" ^
|
neuper@55490
|
596 |
indt (j+2*i) ^ "<GUH> " ^ rls2guh ("IsacKnowledge", thyID) (id_rls erls) ^ " </GUH>\n" ^
|
neuper@37906
|
597 |
indt (j+i) ^"</ERLS>\n" ^
|
neuper@37906
|
598 |
calcrefs2xml (j+i) (thyID, calc) ^
|
neuper@37906
|
599 |
indt (j+i) ^"<SCRIPT>\n"^
|
neuper@37906
|
600 |
scr2xml (j+2*i) scr ^
|
neuper@37906
|
601 |
indt (j+i) ^" </SCRIPT>\n"^
|
neuper@37906
|
602 |
indt j ^"</RULESET>\n" : xml;
|
neuper@37906
|
603 |
|
neuper@37906
|
604 |
(*.convert a tactic into xml-format
|
neuper@37906
|
605 |
ATTENTION: WN060513 detected faulty 'cterm2xml's with 'string's as args.*)
|
neuper@37906
|
606 |
fun tac2xml j (Subproblem (dI, pI)) =
|
neuper@37906
|
607 |
(indt j ^"<SUBPROBLEMTACTIC name=\"Subproblem\">\n"^
|
neuper@37906
|
608 |
indt (j+i) ^"<THEORY> "^ dI ^" </THEORY>\n"^
|
neuper@37906
|
609 |
indt (j+i) ^"<PROBLEM>\n"^
|
neuper@37906
|
610 |
id2xml (j+2*i) pI^
|
neuper@37906
|
611 |
indt (j+i) ^"</PROBLEM>\n"^
|
neuper@37906
|
612 |
indt j ^"</SUBPROBLEMTACTIC>\n"):xml
|
neuper@37906
|
613 |
| tac2xml j Model_Problem =
|
neuper@37906
|
614 |
(indt j ^"<STRINGLISTTACTIC name=\"Model_Problem\">"^
|
neuper@37906
|
615 |
indt j ^"</STRINGLISTTACTIC>\n"):xml
|
neuper@37906
|
616 |
| tac2xml j (Refine_Tacitly pI) =
|
neuper@37906
|
617 |
(indt j ^"<STRINGLISTTACTIC name=\"Refine_Tacitly\">\n"^
|
neuper@37906
|
618 |
id2xml (j+i) pI^
|
neuper@37906
|
619 |
indt j ^"</STRINGLISTTACTIC>\n"):xml
|
neuper@37906
|
620 |
|
neuper@37906
|
621 |
| tac2xml j (Add_Given ct) =
|
neuper@37906
|
622 |
(indt j ^"<SIMPLETACTIC name=\"Add_Given\">\n"^
|
neuper@37906
|
623 |
cterm2xml (j+i) ct^
|
neuper@37906
|
624 |
indt j ^"</SIMPLETACTIC>\n"):xml
|
neuper@37906
|
625 |
| tac2xml j (Add_Find ct) =
|
neuper@37906
|
626 |
(indt j ^"<SIMPLETACTIC name=\"Add_Find\">\n"^
|
neuper@37906
|
627 |
cterm2xml (j+i) ct^
|
neuper@37906
|
628 |
indt j ^"</SIMPLETACTIC>\n"):xml
|
neuper@37906
|
629 |
| tac2xml j (Add_Relation ct) =
|
neuper@37906
|
630 |
(indt j ^"<SIMPLETACTIC name=\"Add_Relation\">\n"^
|
neuper@37906
|
631 |
cterm2xml (j+i) ct^
|
neuper@37906
|
632 |
indt j ^"</SIMPLETACTIC>\n"):xml
|
neuper@37906
|
633 |
|
neuper@37906
|
634 |
| tac2xml j (Specify_Theory ct) =
|
neuper@37906
|
635 |
(indt j ^"<SIMPLETACTIC name=\"Specify_Theory\">\n"^
|
neuper@37906
|
636 |
cterm2xml (j+i) ct^(*WN060513 Specify_Theory = fn : domID -> tac
|
neuper@37906
|
637 |
and domID is a string, not a cterm *)
|
neuper@37906
|
638 |
indt j ^"</SIMPLETACTIC>\n"):xml
|
neuper@37906
|
639 |
| tac2xml j (Specify_Problem ct) =
|
neuper@37906
|
640 |
(indt j ^"<STRINGLISTTACTIC name=\"Specify_Problem\">\n"^
|
neuper@37906
|
641 |
id2xml (j+i) ct^
|
neuper@37906
|
642 |
indt j ^"</STRINGLISTTACTIC>\n"):xml
|
neuper@37906
|
643 |
| tac2xml j (Specify_Method ct) =
|
neuper@37906
|
644 |
(indt j ^"<STRINGLISTTACTIC name=\"Specify_Method\">\n"^
|
neuper@37906
|
645 |
id2xml (j+i) ct^
|
neuper@37906
|
646 |
indt j ^"</STRINGLISTTACTIC>\n"):xml
|
neuper@37906
|
647 |
| tac2xml j (Apply_Method mI) =
|
neuper@37906
|
648 |
(indt j ^"<STRINGLISTTACTIC name=\"Apply_Method\">\n"^
|
neuper@37906
|
649 |
id2xml (j+i) mI^
|
neuper@37906
|
650 |
indt j ^"</STRINGLISTTACTIC>\n"):xml
|
neuper@37906
|
651 |
|
neuper@37906
|
652 |
| tac2xml j (Take ct) =
|
neuper@37906
|
653 |
(indt j ^"<SIMPLETACTIC name=\"Take\">\n"^
|
neuper@37906
|
654 |
cterm2xml (j+i) ct^
|
neuper@37906
|
655 |
indt j ^"</SIMPLETACTIC>\n"):xml
|
neuper@37906
|
656 |
| tac2xml j (Calculate opstr) =
|
neuper@37906
|
657 |
(indt j ^"<SIMPLETACTIC name=\"Calculate\">\n"^
|
neuper@37906
|
658 |
cterm2xml (j+i) opstr^(*WN060513 Calculate = fn : string -> tac
|
neuper@37906
|
659 |
'string', _NOT_ 'cterm' ..flaw from RG*)
|
neuper@37906
|
660 |
indt j ^"</SIMPLETACTIC>\n"):xml
|
neuper@37906
|
661 |
(* val (j, Rewrite thm') = (i, tac);
|
neuper@37906
|
662 |
*)
|
neuper@37906
|
663 |
| tac2xml j (Rewrite thm') =
|
neuper@37906
|
664 |
(indt j ^"<REWRITETACTIC name=\"Rewrite\">\n"^
|
neuper@37906
|
665 |
thm'2xml (j+i) thm'^
|
neuper@37906
|
666 |
indt j ^"</REWRITETACTIC>\n"):xml
|
neuper@38031
|
667 |
(* writeln (tac2xml 2 (Rewrite ("all_left",
|
neuper@37906
|
668 |
"~ ?b =!= 0 ==> (?a = ?b) = (?a - ?b = 0)")));
|
neuper@37906
|
669 |
val (j, (Rewrite_Inst (subs, thm'))) = (i, tac);
|
neuper@37906
|
670 |
*)
|
neuper@37906
|
671 |
| tac2xml j (Rewrite_Inst (subs, thm')) =
|
neuper@37906
|
672 |
(indt j ^"<REWRITEINSTTACTIC name=\"Rewrite_Inst\">\n"^
|
neuper@37906
|
673 |
subs2xml (j+i) subs^
|
neuper@37906
|
674 |
thm'2xml (j+i) thm'^
|
neuper@37906
|
675 |
indt j ^"</REWRITEINSTTACTIC>\n"):xml
|
neuper@38031
|
676 |
(* writeln (tac2xml 2 (Rewrite_Inst
|
neuper@37906
|
677 |
(["(bdv,x)"],
|
neuper@37906
|
678 |
("all_left",
|
neuper@37906
|
679 |
"~ ?b =!= 0 ==> (?a = ?b) = (?a - ?b = 0)"))));
|
neuper@37906
|
680 |
*)
|
neuper@37906
|
681 |
| tac2xml j (Rewrite_Set rls') =
|
neuper@37906
|
682 |
(indt j ^"<REWRITESETTACTIC name=\"Rewrite_Set\">\n"^
|
neuper@37906
|
683 |
indt (j+i) ^"<RULESET> "^ rls' ^" </RULESET>\n"^
|
neuper@37906
|
684 |
indt j ^"</REWRITESETTACTIC>\n"):xml
|
neuper@37906
|
685 |
| tac2xml j (Rewrite_Set_Inst (subs, rls')) =
|
neuper@37906
|
686 |
(indt j ^"<REWRITESETINSTTACTIC name=\"Rewrite_Set_Inst\">\n"^
|
neuper@37906
|
687 |
indt (j+i) ^"<RULESET> "^ rls' ^" </RULESET>\n"^
|
neuper@37906
|
688 |
subs2xml (j+i) subs^
|
neuper@37906
|
689 |
indt j ^"</REWRITESETINSTTACTIC>\n"):xml
|
neuper@37906
|
690 |
|
neuper@37906
|
691 |
| tac2xml j (Or_to_List) =
|
neuper@37940
|
692 |
(indt j ^"<STRINGLISTTACTIC name=\"Or_to_List\"> </STRINGLISTTACTIC>\n"):xml
|
neuper@37906
|
693 |
| tac2xml j (Check_elementwise ct) =
|
neuper@37906
|
694 |
(indt j ^"<SIMPLETACTIC name=\"Check_elementwise\">\n"^
|
neuper@37906
|
695 |
cterm2xml (j+i) ct ^ "\n"^
|
neuper@37906
|
696 |
indt j ^"</SIMPLETACTIC>\n"):xml
|
neuper@37906
|
697 |
(*WN0605 quick and dirty: cterms is _NOT_ a stringlist like pblID...*)
|
neuper@37906
|
698 |
| tac2xml j (Substitute cterms) =
|
neuper@37906
|
699 |
(indt j ^"<STRINGLISTTACTIC name=\"Substitute\">\n"^
|
neuper@37906
|
700 |
(*cterms2xml (j+i) cterms^ ....should be WN060514: TODO TERMLISTTACTIC?*)
|
neuper@37906
|
701 |
id2xml (j+i) cterms^
|
neuper@37906
|
702 |
indt j ^"</STRINGLISTTACTIC>\n"):xml
|
neuper@37906
|
703 |
| tac2xml j (Check_Postcond pI) =
|
neuper@37906
|
704 |
(indt j ^"<STRINGLISTTACTIC name=\"Check_Postcond\">\n"^
|
neuper@37906
|
705 |
id2xml (j+i) pI^
|
neuper@37906
|
706 |
indt j ^"</STRINGLISTTACTIC>\n"):xml
|
neuper@37906
|
707 |
|
neuper@38031
|
708 |
| tac2xml j tac = error ("tac2xml: not impl. for "^tac2str tac);
|
neuper@37906
|
709 |
|
neuper@37906
|
710 |
fun tacs2xml j [] = "":xml
|
neuper@37906
|
711 |
| tacs2xml j (t::ts) = tac2xml j t ^ tacs2xml j ts;
|
neuper@37906
|
712 |
|
neuper@37906
|
713 |
|
neuper@37906
|
714 |
fun posformhead2xml j (p:pos', Form f) =
|
neuper@37906
|
715 |
indt j ^"<CALCFORMULA>\n"^
|
neuper@37906
|
716 |
pos'2xml (j+i) ("POSITION", p) ^
|
neuper@37906
|
717 |
indt (j+i) ^"<FORMULA>\n"^
|
neuper@37906
|
718 |
term2xml (j+i) f^"\n"^
|
neuper@37906
|
719 |
indt (j+i) ^"</FORMULA>\n"^
|
neuper@37906
|
720 |
indt j ^"</CALCFORMULA>\n"
|
neuper@37906
|
721 |
| posformhead2xml j (p, ModSpec c) =
|
neuper@37906
|
722 |
pos'calchead2xml (j) (p, c);
|
neuper@37906
|
723 |
|
neuper@37906
|
724 |
fun posformheads2xml j [] = ("":xml)
|
neuper@37906
|
725 |
| posformheads2xml j (r::rs) = posformhead2xml j r ^ posformheads2xml j rs;
|
neuper@37906
|
726 |
|
neuper@48763
|
727 |
val e_pblterm = (term_of o the o (parse @{theory Script}))
|
neuper@37906
|
728 |
("Problem (" ^ e_domID ^ "," ^ strs2str' e_pblID ^ ")");
|
neuper@37906
|
729 |
|
neuper@37906
|
730 |
(*WN051224 minimal adaption to exporting Formulae _only_ by getFormulaeFromTo*)
|
neuper@37906
|
731 |
fun posterm2xml j (p:pos', t) =
|
neuper@37906
|
732 |
indt j ^"<CALCFORMULA>\n"^
|
neuper@37906
|
733 |
pos'2xml (j+i) ("POSITION", p) ^
|
neuper@37906
|
734 |
indt (j+i) ^"<FORMULA>\n"^
|
neuper@37906
|
735 |
(if t = e_pblterm (*headline in pbl is e_ <- _root_pbl for CAS-command*)
|
neuper@37906
|
736 |
then cterm2xml (j+i) "________________________________________________"
|
neuper@37906
|
737 |
else term2xml (j+i) t)^"\n" ^
|
neuper@37906
|
738 |
indt (j+i) ^"</FORMULA>\n"^
|
neuper@37906
|
739 |
indt j ^"</CALCFORMULA>\n";
|
wneuper@59127
|
740 |
fun xml_of_posterm ((p : pos'), t) =
|
wneuper@59127
|
741 |
XML.Elem (("CALCFORMULA", []),
|
wneuper@59127
|
742 |
[xml_of_pos "POSITION" p,
|
wneuper@59127
|
743 |
XML.Elem (("FORMULA", []), [
|
wneuper@59127
|
744 |
if t = e_pblterm (*headline in pbl is e_ <- _root_pbl for CAS-command*)
|
wneuper@59127
|
745 |
then xml_of_cterm "________________________________________________"
|
wneuper@59127
|
746 |
else xml_of_term t])])
|
neuper@37906
|
747 |
|
neuper@37906
|
748 |
fun posterms2xml j [] = ("":xml)
|
neuper@37906
|
749 |
| posterms2xml j (r::rs) = posterm2xml j r ^ posterms2xml j rs;
|
neuper@37906
|
750 |
|
neuper@37906
|
751 |
fun asm_val2xml j (asm, vl) =
|
neuper@37906
|
752 |
indt j ^ "<ASMEVALUATED>\n" ^
|
neuper@37906
|
753 |
indt (j+i) ^ "<ASM>\n" ^
|
neuper@37906
|
754 |
term2xml (j+i) asm ^ "\n" ^
|
neuper@37906
|
755 |
indt (j+i) ^ "</ASM>\n" ^
|
neuper@37906
|
756 |
indt (j+i) ^ "<VALUE>\n" ^
|
neuper@37906
|
757 |
term2xml (j+i) vl ^ "\n" ^
|
neuper@37906
|
758 |
indt (j+i) ^ "</VALUE>\n" ^
|
neuper@37906
|
759 |
indt j ^ "</ASMEVALUATED>\n" : xml;
|
neuper@37906
|
760 |
|
neuper@37906
|
761 |
fun asm_vals2xml j [] = ("":xml)
|
neuper@37906
|
762 |
| asm_vals2xml j (asm_val::avs) = asm_val2xml j asm_val ^
|
neuper@37906
|
763 |
asm_vals2xml j avs;
|
neuper@37906
|
764 |
|
neuper@37906
|
765 |
(*.a reference to an element in the theory hierarchy;
|
neuper@37906
|
766 |
compare 'fun keref2xml'.*)
|
neuper@37906
|
767 |
(* val (j, thyID, typ, xstring) =
|
neuper@37906
|
768 |
(i+i, snd (thy_containing_rls thy' prls'), "Rulesets", prls');
|
neuper@37906
|
769 |
*)
|
neuper@37906
|
770 |
fun theref2xml j (thyID:thyID) typ (xstring:xstring) =
|
neuper@37906
|
771 |
let val guh = theID2guh ["IsacKnowledge", thyID, typ, xstring]
|
neuper@40836
|
772 |
val typ' = (implode o (drop_last_n 1) o Symbol.explode) typ
|
neuper@37906
|
773 |
in indt j ^ "<KESTOREREF>\n" ^
|
neuper@37906
|
774 |
indt (j+i) ^ "<TAG> " ^ typ' ^ " </TAG>\n" ^
|
neuper@37906
|
775 |
indt (j+i) ^ "<ID> " ^ xstring ^ " </ID>\n" ^
|
neuper@37906
|
776 |
indt (j+i) ^ "<GUH> " ^ guh ^ " </GUH>\n" ^
|
neuper@37906
|
777 |
indt j ^ "</KESTOREREF>\n" : xml
|
neuper@37906
|
778 |
end;
|
neuper@37906
|
779 |
|
neuper@37906
|
780 |
(*.a reference to an element in the kestore EXCEPT theory hierarchy;
|
neuper@37906
|
781 |
compare 'fun theref2xml'.*)
|
neuper@37906
|
782 |
(* val (j, typ, kestoreID) = (i+i, Met_, hd met);
|
neuper@37906
|
783 |
*)
|
neuper@37906
|
784 |
fun keref2xml j typ (kestoreID:kestoreID) =
|
neuper@37906
|
785 |
let val id = strs2str' kestoreID
|
neuper@37906
|
786 |
val guh = kestoreID2guh typ kestoreID
|
neuper@37906
|
787 |
in indt j ^ "<KESTOREREF>\n" ^
|
neuper@37906
|
788 |
indt (j+i) ^ "<TAG> " ^ ketype2str' typ ^ "</TAG>\n" ^
|
neuper@37906
|
789 |
indt (j+i) ^ "<ID> " ^ id ^ " </ID>\n" ^
|
neuper@37906
|
790 |
indt (j+i) ^ "<GUH> " ^ guh ^ " </GUH>\n" ^
|
neuper@37906
|
791 |
indt j ^ "</KESTOREREF>\n" : xml
|
neuper@37906
|
792 |
end;
|
neuper@37906
|
793 |
|
neuper@37906
|
794 |
(*url to a source external to isac*)
|
neuper@37906
|
795 |
fun extref2xml j linktext url =
|
neuper@37906
|
796 |
indt j ^ "<EXTREF>\n" ^
|
neuper@37906
|
797 |
indt (j+i) ^ "<TEXT> " ^ linktext ^ " </TEXT>\n" ^
|
neuper@37906
|
798 |
indt (j+i) ^ "<URL> " ^ url ^ " </URL>\n" ^
|
neuper@37906
|
799 |
indt j ^ "</EXTREF>\n" : xml;
|
neuper@37906
|
800 |
|
neuper@37906
|
801 |
(* val (ContThmInst{thyID, thm, bdvs, thminst, applto, applat, reword,
|
neuper@37906
|
802 |
asms, lhs, rhs, result, resasms, asmrls}) =
|
neuper@37906
|
803 |
(context_thy (pt,pos) tac);
|
neuper@38031
|
804 |
writeln (contthy2xml 2 (context_thy (pt,pos) tac));
|
neuper@37906
|
805 |
*)
|
neuper@37906
|
806 |
fun contthy2xml j EContThy =
|
neuper@38031
|
807 |
error "contthy2xml called with EContThy"
|
neuper@37906
|
808 |
| contthy2xml j (ContThm {thyID, thm, applto, applat, reword,
|
neuper@37906
|
809 |
asms,lhs, rhs, result, resasms, asmrls}) =
|
neuper@37906
|
810 |
indt j ^ "<GUH> " ^ thm ^ " </GUH>\n" ^
|
neuper@37940
|
811 |
|
neuper@37906
|
812 |
indt j ^ "<APPLTO>\n" ^
|
neuper@37906
|
813 |
term2xml j applto ^ "\n" ^
|
neuper@37906
|
814 |
indt j ^ "</APPLTO>\n" ^
|
neuper@37906
|
815 |
indt j ^ "<APPLAT>\n" ^
|
neuper@37906
|
816 |
term2xml j applat ^ "\n" ^
|
neuper@37906
|
817 |
indt j ^ "</APPLAT>\n" ^
|
neuper@37906
|
818 |
indt j ^ "<ORDER>\n" ^ (*should be a theref2xml*)
|
neuper@37906
|
819 |
indt (j+i) ^"<ID> " ^ reword ^ " </ID>\n" ^
|
neuper@37906
|
820 |
indt j ^ "</ORDER>\n" ^
|
neuper@37906
|
821 |
indt j ^ "<ASMSEVAL>\n" ^
|
neuper@37906
|
822 |
asm_vals2xml (j+i) asms ^
|
neuper@37906
|
823 |
indt j ^ "</ASMSEVAL>\n" ^
|
neuper@37906
|
824 |
indt j ^ "<LHS>\n" ^
|
neuper@37906
|
825 |
term2xml j (fst lhs) ^ "\n" ^
|
neuper@37906
|
826 |
indt j ^ "</LHS>\n" ^
|
neuper@37906
|
827 |
indt j ^ "<LHSINST>\n" ^
|
neuper@37906
|
828 |
term2xml j (snd lhs) ^ "\n" ^
|
neuper@37906
|
829 |
indt j ^ "</LHSINST>\n" ^
|
neuper@37906
|
830 |
indt j ^ "<RHS>\n" ^
|
neuper@37906
|
831 |
term2xml j (fst rhs) ^ "\n" ^
|
neuper@37906
|
832 |
indt j ^ "</RHS>\n" ^
|
neuper@37906
|
833 |
indt j ^ "<RHSINST>\n" ^
|
neuper@37906
|
834 |
term2xml j (snd rhs) ^ "\n" ^
|
neuper@37906
|
835 |
indt j ^ "</RHSINST>\n" ^
|
neuper@37906
|
836 |
indt j ^ "<RESULT>\n" ^
|
neuper@37906
|
837 |
term2xml j result ^ "\n" ^
|
neuper@37906
|
838 |
indt j ^ "</RESULT>\n" ^
|
neuper@37906
|
839 |
indt j ^ "<ASSUMPTIONS>\n" ^
|
neuper@37906
|
840 |
terms2xml' j resasms ^
|
neuper@37906
|
841 |
indt j ^ "</ASSUMPTIONS>\n" ^
|
neuper@37906
|
842 |
indt j ^ "<EVALRLS>\n" ^
|
neuper@37906
|
843 |
theref2xml j thyID "Rulesets" asmrls ^
|
neuper@37906
|
844 |
indt j ^ "</EVALRLS>\n"
|
neuper@37906
|
845 |
| contthy2xml j (ContThmInst{thyID, thm, bdvs, thminst, applto, applat,
|
neuper@37906
|
846 |
reword, asms, lhs, rhs, result, resasms,
|
neuper@37906
|
847 |
asmrls}) =
|
neuper@37906
|
848 |
indt j ^ "<GUH> " ^ thm ^ " </GUH>\n" ^
|
neuper@37906
|
849 |
indt j ^ "<SUBSLIST>\n" ^ (*should be an environment = substitution*)
|
neuper@37906
|
850 |
indt (j+i) ^ "<MATHML>\n" ^
|
neuper@37906
|
851 |
indt (j+2*i) ^ "<ISA> " ^ subst2str' bdvs ^ " </ISA>\n" ^
|
neuper@37906
|
852 |
indt (j+i) ^ "</MATHML>\n" ^
|
neuper@37906
|
853 |
indt j ^ "</SUBSLIST>\n" ^
|
neuper@37906
|
854 |
indt j ^ "<INSTANTIATED>\n" ^
|
neuper@37906
|
855 |
term2xml j thminst ^ "\n" ^
|
neuper@37906
|
856 |
indt j ^ "</INSTANTIATED>\n" ^
|
neuper@37906
|
857 |
indt j ^ "<APPLTO>\n" ^
|
neuper@37906
|
858 |
term2xml j applto ^ "\n" ^
|
neuper@37906
|
859 |
indt j ^ "</APPLTO>\n" ^
|
neuper@37906
|
860 |
indt j ^ "<APPLAT>\n" ^
|
neuper@37906
|
861 |
term2xml j applat ^ "\n" ^
|
neuper@37906
|
862 |
indt j ^ "</APPLAT>\n" ^
|
neuper@37906
|
863 |
indt j ^ "<ORDER>\n" ^ (*should be a theref2xml*)
|
neuper@37906
|
864 |
indt (j+i) ^"<ID> " ^ reword ^ " </ID>\n" ^
|
neuper@37906
|
865 |
indt j ^ "</ORDER>\n" ^
|
neuper@37906
|
866 |
indt j ^ "<ASMSEVAL>\n" ^
|
neuper@37906
|
867 |
asm_vals2xml (j+i) asms ^
|
neuper@37906
|
868 |
indt j ^ "</ASMSEVAL>\n" ^
|
neuper@37906
|
869 |
indt j ^ "<LHS>\n" ^
|
neuper@37906
|
870 |
term2xml j (fst lhs) ^ "\n" ^
|
neuper@37906
|
871 |
indt j ^ "</LHS>\n" ^
|
neuper@37906
|
872 |
indt j ^ "<LHSINST>\n" ^
|
neuper@37906
|
873 |
term2xml j (snd lhs) ^ "\n" ^
|
neuper@37906
|
874 |
indt j ^ "</LHSINST>\n" ^
|
neuper@37906
|
875 |
indt j ^ "<RHS>\n" ^
|
neuper@37906
|
876 |
term2xml j (fst rhs) ^ "\n" ^
|
neuper@37906
|
877 |
indt j ^ "</RHS>\n" ^
|
neuper@37906
|
878 |
indt j ^ "<RHSINST>\n" ^
|
neuper@37906
|
879 |
term2xml j (snd rhs) ^ "\n" ^
|
neuper@37906
|
880 |
indt j ^ "</RHSINST>\n" ^
|
neuper@37906
|
881 |
indt j ^ "<RESULT>\n" ^
|
neuper@37906
|
882 |
term2xml j result ^ "\n" ^
|
neuper@37906
|
883 |
indt j ^ "</RESULT>\n" ^
|
neuper@37906
|
884 |
indt j ^ "<ASSUMPTOIONS>\n" ^
|
neuper@37906
|
885 |
terms2xml' j resasms ^
|
neuper@37906
|
886 |
indt j ^ "</ASSUMPTOIONS>\n" ^
|
neuper@37906
|
887 |
indt j ^ "<EVALRLS>\n" ^
|
neuper@37906
|
888 |
theref2xml j thyID "Rulesets" asmrls ^
|
neuper@37906
|
889 |
indt j ^ "</EVALRLS>\n"
|
neuper@37906
|
890 |
|
neuper@37906
|
891 |
| contthy2xml j (ContRls {thyID, rls, applto, result, asms}) =
|
neuper@37906
|
892 |
indt j ^ "<GUH> " ^ rls ^ " </GUH>\n" ^
|
neuper@37906
|
893 |
indt j ^ "<APPLTO>\n" ^
|
neuper@37906
|
894 |
term2xml j applto ^ "\n" ^
|
neuper@37906
|
895 |
indt j ^ "</APPLTO>\n" ^
|
neuper@37906
|
896 |
indt j ^ "<RESULT>\n" ^
|
neuper@37906
|
897 |
term2xml j result ^ "\n" ^
|
neuper@37906
|
898 |
indt j ^ "</RESULT>\n" ^
|
neuper@37906
|
899 |
indt j ^ "<ASSUMPTOIONS>\n" ^
|
neuper@37906
|
900 |
terms2xml' j asms ^
|
neuper@37906
|
901 |
indt j ^ "</ASSUMPTOIONS>\n"
|
neuper@37906
|
902 |
|
neuper@37906
|
903 |
| contthy2xml j (ContRlsInst {thyID, rls, bdvs, applto, result, asms}) =
|
neuper@37906
|
904 |
indt j ^ "<GUH> " ^ rls ^ " </GUH>\n" ^
|
neuper@37906
|
905 |
indt j ^ "<SUBSLIST>\n" ^ (*should be an environment = substitution*)
|
neuper@37906
|
906 |
indt (j+i) ^ "<MATHML>\n" ^
|
neuper@37906
|
907 |
indt (j+2*i) ^ "<ISA> " ^ subst2str' bdvs ^ " </ISA>\n" ^
|
neuper@37906
|
908 |
indt (j+i) ^ "</MATHML>\n" ^
|
neuper@37906
|
909 |
indt j ^ "</SUBSLIST>\n" ^
|
neuper@37906
|
910 |
indt j ^ "<APPLTO>\n" ^
|
neuper@37906
|
911 |
term2xml j applto ^ "\n" ^
|
neuper@37906
|
912 |
indt j ^ "</APPLTO>\n" ^
|
neuper@37906
|
913 |
indt j ^ "<RESULT>\n" ^
|
neuper@37906
|
914 |
term2xml j result ^ "\n" ^
|
neuper@37906
|
915 |
indt j ^ "</RESULT>\n" ^
|
neuper@37906
|
916 |
indt j ^ "<ASSUMPTOIONS>\n" ^
|
neuper@37906
|
917 |
terms2xml' j asms ^
|
neuper@37906
|
918 |
indt j ^ "</ASSUMPTOIONS>\n"
|
neuper@37906
|
919 |
|
neuper@37906
|
920 |
| contthy2xml j (ContNOrew {thyID, thm_rls, applto}) =
|
neuper@37906
|
921 |
indt j ^ "<GUH> " ^ thm_rls ^ " </GUH>\n" ^
|
neuper@37906
|
922 |
indt j ^ "<APPLTO>\n" ^
|
neuper@37906
|
923 |
term2xml j applto ^ "\n" ^
|
neuper@37906
|
924 |
indt j ^ "</APPLTO>\n"
|
neuper@37906
|
925 |
|
neuper@37906
|
926 |
| contthy2xml j (ContNOrewInst{thyID, thm_rls, bdvs, thminst, applto}) =
|
neuper@37906
|
927 |
indt j ^ "<GUH> " ^ thm_rls ^ " </GUH>\n" ^
|
neuper@37906
|
928 |
indt j ^ "<SUBSLIST>\n" ^ (*should be an environment = substitution*)
|
neuper@37906
|
929 |
indt (j+i) ^ "<MATHML>\n" ^
|
neuper@37906
|
930 |
indt (j+2*i) ^ "<ISA> " ^ subst2str' bdvs ^ " </ISA>\n" ^
|
neuper@37906
|
931 |
indt (j+i) ^ "</MATHML>\n" ^
|
neuper@37906
|
932 |
indt j ^ "</SUBSLIST>\n" ^
|
neuper@37906
|
933 |
indt j ^ "<INSTANTIATED>\n" ^
|
neuper@37906
|
934 |
term2xml j thminst ^ "\n" ^
|
neuper@37906
|
935 |
indt j ^ "</INSTANTIATED>\n" ^
|
neuper@37906
|
936 |
indt j ^ "<APPLTO>\n" ^
|
neuper@37906
|
937 |
term2xml j applto ^ "\n" ^
|
neuper@37906
|
938 |
indt j ^ "</APPLTO>\n" : xml;
|
neuper@37906
|
939 |
|
wneuper@59124
|
940 |
(*------------------------------------------------------------------
|
neuper@37906
|
941 |
end
|
neuper@37906
|
942 |
open datatypes;
|
wneuper@59124
|
943 |
------------------------------------------------------------------*)
|
neuper@37940
|
944 |
|
neuper@37940
|
945 |
|