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