wneuper@59216
|
1 |
theory Isac_Protocol
|
wneuper@59470
|
2 |
imports "~~/src/Tools/isac/Knowledge/Build_Thydata" Protocol.Protocol
|
wneuper@59216
|
3 |
begin
|
wneuper@59216
|
4 |
|
wneuper@59216
|
5 |
(* val appendFormula : calcID -> cterm' -> XML.tree *)
|
wneuper@59216
|
6 |
operation_setup (sequential, bracket, auto) append_form =
|
wneuper@59216
|
7 |
\<open>fn intree =>
|
wneuper@59216
|
8 |
(let
|
wneuper@59216
|
9 |
val (calcid, cterm') = case intree of
|
wneuper@59216
|
10 |
XML.Elem (("APPENDFORMULA", []), [
|
wneuper@59216
|
11 |
XML.Elem (("CALCID", []), [XML.Text ci]),
|
walther@59868
|
12 |
form]) => (ci |> TermC.int_of_str, form |> xml_to_term_NEW |> UnparseC.term)
|
wneuper@59216
|
13 |
| x => raise ERROR ("append_form: WRONG intree = " ^ xmlstr 0 x)
|
wneuper@59260
|
14 |
val result = Kernel.appendFormula calcid cterm'
|
wneuper@59216
|
15 |
in result end)
|
wneuper@59216
|
16 |
handle ERROR msg => appendformulaERROR2xml 4711 msg\<close>
|
wneuper@59216
|
17 |
|
wneuper@59216
|
18 |
(* val autoCalculate : calcID -> auto -> XML.tree *)
|
wneuper@59216
|
19 |
operation_setup autocalculate = \<open>
|
wneuper@59216
|
20 |
{from_lib = Codec.tree,
|
wneuper@59216
|
21 |
to_lib = Codec.tree,
|
wneuper@59216
|
22 |
action = (fn intree =>
|
wneuper@59216
|
23 |
(let
|
wneuper@59216
|
24 |
val (ci, a) = case intree of
|
wneuper@59216
|
25 |
XML.Elem (("AUTOCALC", []), [
|
wneuper@59216
|
26 |
XML.Elem (("CALCID", []), [XML.Text ci]), a]) => (ci, a)
|
wneuper@59216
|
27 |
| tree => raise ERROR ("autocalculate: WRONG intree = " ^ xmlstr 0 tree)
|
walther@59875
|
28 |
val SOME calcid = TermC.int_opt_of_string ci
|
wneuper@59216
|
29 |
val auto = xml_to_auto a
|
wneuper@59260
|
30 |
val result = Kernel.autoCalculate calcid auto
|
wneuper@59216
|
31 |
in result end)
|
wneuper@59216
|
32 |
handle ERROR msg => autocalculateERROR2xml 4711 msg)}\<close>
|
wneuper@59216
|
33 |
|
wneuper@59216
|
34 |
(* val applyTactic : calcID -> pos' -> tac -> XML.tree *)
|
wneuper@59216
|
35 |
operation_setup apply_tac = \<open>
|
wneuper@59216
|
36 |
{from_lib = Codec.tree,
|
wneuper@59216
|
37 |
to_lib = Codec.tree,
|
wneuper@59216
|
38 |
action = (fn intree =>
|
wneuper@59216
|
39 |
(let
|
wneuper@59216
|
40 |
val (ci, pos, tac) = case intree of
|
wneuper@59216
|
41 |
XML.Elem (("AUTOCALC", []), [
|
wneuper@59216
|
42 |
XML.Elem (("CALCID", []), [XML.Text ci]),
|
wneuper@59390
|
43 |
pos, tac]) => (TermC.int_of_str ci, xml_to_pos pos, xml_to_tac tac)
|
wneuper@59216
|
44 |
| tree => raise ERROR ("apply_tac: WRONG intree = " ^ xmlstr 0 tree)
|
wneuper@59260
|
45 |
val result = Kernel.applyTactic ci pos tac
|
wneuper@59216
|
46 |
in result end)
|
wneuper@59216
|
47 |
handle ERROR msg => autocalculateERROR2xml 4711 msg)}\<close>
|
wneuper@59216
|
48 |
|
wneuper@59216
|
49 |
(* val CalcTree : fmz list -> XML.tree *)
|
wneuper@59216
|
50 |
operation_setup calctree = \<open>
|
wneuper@59216
|
51 |
{from_lib = Codec.tree,
|
wneuper@59216
|
52 |
to_lib = Codec.tree,
|
wneuper@59216
|
53 |
action = (fn intree =>
|
wneuper@59216
|
54 |
(let
|
wneuper@59216
|
55 |
val fmz = case intree of
|
wneuper@59216
|
56 |
tree as XML.Elem (("FORMALIZATION", []), vars) => xml_to_fmz tree
|
wneuper@59216
|
57 |
| tree => raise ERROR ("calctree: WRONG intree = " ^ xmlstr 0 tree)
|
wneuper@59260
|
58 |
val result = Kernel.CalcTree fmz
|
wneuper@59216
|
59 |
in result end)
|
wneuper@59216
|
60 |
handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
|
wneuper@59216
|
61 |
|
wneuper@59216
|
62 |
(* val checkContext : calcID -> pos' -> guh -> XML.tree *)
|
wneuper@59216
|
63 |
operation_setup check_ctxt = \<open>
|
wneuper@59216
|
64 |
{from_lib = Codec.tree,
|
wneuper@59216
|
65 |
to_lib = Codec.tree,
|
wneuper@59216
|
66 |
action = (fn intree =>
|
wneuper@59216
|
67 |
(let
|
wneuper@59216
|
68 |
val (ci, pos, guh) = case intree of
|
wneuper@59216
|
69 |
XML.Elem (("CONTEXTTHY", []), [
|
wneuper@59216
|
70 |
XML.Elem (("CALCID", []), [XML.Text ci]),
|
wneuper@59216
|
71 |
pos as XML.Elem (("POSITION", []), _),
|
wneuper@59216
|
72 |
XML.Elem (("GUH", []), [XML.Text guh])])
|
wneuper@59390
|
73 |
=> (TermC.int_of_str ci, xml_to_pos pos, guh)
|
wneuper@59216
|
74 |
| tree => raise ERROR ("check_ctxt: WRONG intree = " ^ xmlstr 0 tree)
|
wneuper@59260
|
75 |
val result = Kernel.checkContext ci pos guh
|
wneuper@59216
|
76 |
in result end)
|
wneuper@59216
|
77 |
handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
|
wneuper@59216
|
78 |
|
wneuper@59216
|
79 |
(* val DEconstrCalcTree : calcID -> XML.tree *)
|
wneuper@59216
|
80 |
operation_setup deconstrcalctree = \<open>
|
wneuper@59216
|
81 |
{from_lib = Codec.int,
|
wneuper@59216
|
82 |
to_lib = Codec.tree,
|
wneuper@59216
|
83 |
action = (fn calcid =>
|
wneuper@59216
|
84 |
let
|
wneuper@59260
|
85 |
val result = Kernel.DEconstrCalcTree calcid
|
wneuper@59216
|
86 |
in result end)}\<close>
|
wneuper@59216
|
87 |
|
wneuper@59216
|
88 |
(* val fetchApplicableTactics : calcID -> int -> pos' -> XML.tree *)
|
wneuper@59216
|
89 |
operation_setup fetch_applicable_tacs = \<open>
|
wneuper@59216
|
90 |
{from_lib = Codec.tree,
|
wneuper@59216
|
91 |
to_lib = Codec.tree,
|
wneuper@59216
|
92 |
action = (fn intree =>
|
wneuper@59216
|
93 |
(let
|
wneuper@59216
|
94 |
val (ci, i, pos) = case intree of
|
wneuper@59216
|
95 |
XML.Elem (("APPLICABLETACTICS", []), [
|
wneuper@59216
|
96 |
XML.Elem (("CALCID", []), [XML.Text ci]),
|
wneuper@59216
|
97 |
XML.Elem (("INT", []), [XML.Text i]),
|
wneuper@59216
|
98 |
pos as XML.Elem (("POSITION", []), _)])
|
wneuper@59390
|
99 |
=> (TermC.int_of_str ci, TermC.int_of_str i, xml_to_pos pos)
|
wneuper@59216
|
100 |
| tree => raise ERROR ("fetch_applicable_tacs: WRONG intree = " ^ xmlstr 0 tree)
|
wneuper@59260
|
101 |
val result = Kernel.fetchApplicableTactics ci i pos
|
wneuper@59216
|
102 |
in result end)
|
wneuper@59216
|
103 |
handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
|
wneuper@59216
|
104 |
|
wneuper@59216
|
105 |
(* val fetchProposedTactic : calcID -> XML.tree *)
|
wneuper@59216
|
106 |
operation_setup fetch_proposed_tac = \<open>
|
wneuper@59216
|
107 |
{from_lib = Codec.tree,
|
wneuper@59216
|
108 |
to_lib = Codec.tree,
|
wneuper@59216
|
109 |
action = (fn intree =>
|
wneuper@59216
|
110 |
(let
|
wneuper@59216
|
111 |
val (ci) = case intree of
|
wneuper@59216
|
112 |
XML.Elem (("NEXTTAC", []), [
|
wneuper@59390
|
113 |
XML.Elem (("CALCID", []), [XML.Text ci])]) => (TermC.int_of_str ci)
|
wneuper@59216
|
114 |
| tree => raise ERROR ("fetch_proposed_tac: WRONG intree = " ^ xmlstr 0 tree)
|
wneuper@59260
|
115 |
val result = Kernel.fetchProposedTactic ci
|
wneuper@59216
|
116 |
in result end)
|
wneuper@59216
|
117 |
handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
|
wneuper@59216
|
118 |
|
wneuper@59216
|
119 |
(* val findFillpatterns : calcID -> errpatID -> XML.tree *)
|
wneuper@59216
|
120 |
operation_setup find_fill_patts = \<open>
|
wneuper@59216
|
121 |
{from_lib = Codec.tree,
|
wneuper@59216
|
122 |
to_lib = Codec.tree,
|
wneuper@59216
|
123 |
action = (fn intree =>
|
wneuper@59216
|
124 |
(let
|
wneuper@59216
|
125 |
val (ci, err_pat_id) = case intree of
|
wneuper@59216
|
126 |
XML.Elem (("FINDFILLPATTERNS", []), [
|
wneuper@59216
|
127 |
XML.Elem (("CALCID", []), [XML.Text ci]),
|
wneuper@59216
|
128 |
XML.Elem (("STRING", []), [XML.Text err_pat_id])])
|
wneuper@59390
|
129 |
=> (TermC.int_of_str ci, err_pat_id)
|
wneuper@59216
|
130 |
| tree => raise ERROR ("find_fill_patts: WRONG intree = " ^ xmlstr 0 tree)
|
wneuper@59260
|
131 |
val result = Kernel.findFillpatterns ci err_pat_id
|
wneuper@59216
|
132 |
in result end)
|
wneuper@59216
|
133 |
handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
|
wneuper@59216
|
134 |
|
wneuper@59216
|
135 |
(* val getAccumulatedAsms : calcID -> pos' -> XML.tree *)
|
wneuper@59216
|
136 |
operation_setup get_accumulated_asms = \<open>
|
wneuper@59216
|
137 |
{from_lib = Codec.tree,
|
wneuper@59216
|
138 |
to_lib = Codec.tree,
|
wneuper@59216
|
139 |
action = (fn intree =>
|
wneuper@59216
|
140 |
(let
|
wneuper@59216
|
141 |
val (ci, pos) = case intree of
|
wneuper@59216
|
142 |
XML.Elem (("GETASSUMPTIONS", []), [
|
wneuper@59216
|
143 |
XML.Elem (("CALCID", []), [XML.Text ci]),
|
wneuper@59216
|
144 |
pos as XML.Elem (("POSITION", []), _)])
|
wneuper@59390
|
145 |
=> (TermC.int_of_str ci, xml_to_pos pos)
|
wneuper@59216
|
146 |
| tree => raise ERROR ("autocalculate: WRONG intree = " ^ xmlstr 0 tree)
|
wneuper@59260
|
147 |
val result = Kernel.getAccumulatedAsms ci pos
|
wneuper@59216
|
148 |
in result end)
|
wneuper@59216
|
149 |
handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
|
wneuper@59216
|
150 |
|
wneuper@59216
|
151 |
(* val getActiveFormula : calcID -> XML.tree *)
|
wneuper@59216
|
152 |
operation_setup get_active_form = \<open>
|
wneuper@59216
|
153 |
{from_lib = Codec.tree,
|
wneuper@59216
|
154 |
to_lib = Codec.tree,
|
wneuper@59216
|
155 |
action = (fn intree =>
|
wneuper@59216
|
156 |
(let
|
wneuper@59216
|
157 |
val (ci) = case intree of
|
wneuper@59216
|
158 |
XML.Elem (("CALCITERATOR", []), [
|
wneuper@59216
|
159 |
XML.Elem (("CALCID", []), [XML.Text ci])])
|
wneuper@59390
|
160 |
=> (TermC.int_of_str ci)
|
wneuper@59216
|
161 |
| tree => raise ERROR ("get_active_form: WRONG intree = " ^ xmlstr 0 tree)
|
wneuper@59260
|
162 |
val result = Kernel.getActiveFormula ci
|
wneuper@59216
|
163 |
in result end)
|
wneuper@59216
|
164 |
handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
|
wneuper@59216
|
165 |
|
wneuper@59216
|
166 |
(* val getAssumptions : calcID -> pos' -> XML.tree *)
|
wneuper@59216
|
167 |
operation_setup get_asms = \<open>
|
wneuper@59216
|
168 |
{from_lib = Codec.tree,
|
wneuper@59216
|
169 |
to_lib = Codec.tree,
|
wneuper@59216
|
170 |
action = (fn intree =>
|
wneuper@59216
|
171 |
(let
|
wneuper@59216
|
172 |
val (ci, pos) = case intree of
|
wneuper@59216
|
173 |
XML.Elem (("APPLICABLETACTICS", []), [
|
wneuper@59216
|
174 |
XML.Elem (("CALCID", []), [XML.Text ci]),
|
wneuper@59216
|
175 |
pos as XML.Elem (("POSITION", []), _)])
|
wneuper@59390
|
176 |
=> (TermC.int_of_str ci, xml_to_pos pos)
|
wneuper@59216
|
177 |
| tree => raise ERROR ("get_asms: WRONG intree = " ^ xmlstr 0 tree)
|
wneuper@59260
|
178 |
val result = Kernel.getAssumptions ci pos
|
wneuper@59216
|
179 |
in result end)
|
wneuper@59216
|
180 |
handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
|
wneuper@59216
|
181 |
|
wneuper@59216
|
182 |
(* val getFormulaeFromTo : calcID -> pos' -> pos' -> int -> bool -> XML.tree *)
|
wneuper@59216
|
183 |
operation_setup getformulaefromto = \<open>
|
wneuper@59216
|
184 |
{from_lib = Codec.tree,
|
wneuper@59216
|
185 |
to_lib = Codec.tree,
|
wneuper@59216
|
186 |
action = (fn intree =>
|
wneuper@59216
|
187 |
(let
|
wneuper@59216
|
188 |
val (calcid, from, to, level, rules) = case intree of
|
wneuper@59216
|
189 |
XML.Elem (("GETFORMULAEFROMTO", []), [
|
wneuper@59216
|
190 |
XML.Elem (("CALCID", []), [XML.Text calcid]),
|
wneuper@59216
|
191 |
from as XML.Elem (("POSITION", []), [
|
wneuper@59216
|
192 |
XML.Elem (("INTLIST", []), _),
|
wneuper@59216
|
193 |
XML.Elem (("POS", []), [XML.Text _])]),
|
wneuper@59216
|
194 |
to as XML.Elem (("POSITION", []), [
|
wneuper@59216
|
195 |
XML.Elem (("INTLIST", []), _),
|
wneuper@59216
|
196 |
XML.Elem (("POS", []), [XML.Text _])]),
|
wneuper@59216
|
197 |
XML.Elem (("INT", []), [XML.Text level]),
|
wneuper@59216
|
198 |
XML.Elem (("BOOL", []), [XML.Text rules])])
|
wneuper@59390
|
199 |
=> (TermC.int_of_str calcid, xml_to_pos from, xml_to_pos to, TermC.int_of_str level, string_to_bool rules)
|
wneuper@59216
|
200 |
| tree => raise ERROR ("getformulaefromto: WRONG intree = " ^ xmlstr 0 tree)
|
wneuper@59260
|
201 |
val result = Kernel.getFormulaeFromTo calcid from to level rules
|
wneuper@59216
|
202 |
in result end)
|
wneuper@59216
|
203 |
handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
|
wneuper@59216
|
204 |
|
wneuper@59216
|
205 |
(* val getTactic : calcID -> pos' -> XML.tree *)
|
wneuper@59216
|
206 |
operation_setup get_tac = \<open>
|
wneuper@59216
|
207 |
{from_lib = Codec.tree,
|
wneuper@59216
|
208 |
to_lib = Codec.tree,
|
wneuper@59216
|
209 |
action = (fn intree =>
|
wneuper@59216
|
210 |
(let
|
wneuper@59216
|
211 |
val (ci, pos) = case intree of
|
wneuper@59216
|
212 |
XML.Elem (("GETTACTIC", []), [
|
wneuper@59216
|
213 |
XML.Elem (("CALCID", []), [XML.Text ci]),
|
wneuper@59216
|
214 |
pos as XML.Elem (("POSITION", []), _)])
|
wneuper@59390
|
215 |
=> (TermC.int_of_str ci, xml_to_pos pos)
|
wneuper@59216
|
216 |
| tree => raise ERROR ("get_tac: WRONG intree = " ^ xmlstr 0 tree)
|
wneuper@59260
|
217 |
val result = Kernel.getTactic ci pos
|
wneuper@59216
|
218 |
in result end)
|
wneuper@59216
|
219 |
handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
|
wneuper@59216
|
220 |
|
wneuper@59216
|
221 |
(* val initContext : calcID -> ketype -> pos' -> XML.tree *)
|
wneuper@59216
|
222 |
operation_setup init_ctxt = \<open>
|
wneuper@59216
|
223 |
{from_lib = Codec.tree,
|
wneuper@59216
|
224 |
to_lib = Codec.tree,
|
wneuper@59216
|
225 |
action = (fn intree =>
|
wneuper@59216
|
226 |
((let
|
wneuper@59216
|
227 |
val (ci, ketype, pos) = case intree of
|
wneuper@59216
|
228 |
XML.Elem (("INITCONTEXT", []), [
|
wneuper@59216
|
229 |
XML.Elem (("CALCID", []), [XML.Text ci]),
|
wneuper@59216
|
230 |
ketype as XML.Elem (("KETYPE", []), _),
|
wneuper@59216
|
231 |
pos as XML.Elem (("POSITION", []), _)])
|
wneuper@59390
|
232 |
=> (TermC.int_of_str ci, xml_to_ketype ketype, xml_to_pos pos)
|
wneuper@59216
|
233 |
| tree => raise ERROR ("init_ctxt: WRONG intree = " ^ xmlstr 0 tree)
|
wneuper@59260
|
234 |
val result = Kernel.initContext ci ketype pos
|
wneuper@59216
|
235 |
in result end)
|
wneuper@59216
|
236 |
handle ERROR msg => sysERROR2xml 4711 msg)
|
wneuper@59216
|
237 |
handle _ => sysERROR2xml 4711 "Protocol.operation_setup init_ctxt UNKNOWN exn")}\<close>
|
wneuper@59216
|
238 |
|
wneuper@59216
|
239 |
(* val inputFillFormula: calcID -> string -> XML.tree *)
|
wneuper@59216
|
240 |
operation_setup input_fill_form = \<open>
|
wneuper@59216
|
241 |
{from_lib = Codec.tree,
|
wneuper@59216
|
242 |
to_lib = Codec.tree,
|
wneuper@59216
|
243 |
action = (fn intree =>
|
wneuper@59216
|
244 |
(let
|
wneuper@59216
|
245 |
val (ci, str) = case intree of
|
wneuper@59216
|
246 |
XML.Elem (("AUTOCALC", []), [
|
wneuper@59216
|
247 |
XML.Elem (("CALCID", []), [XML.Text ci]),
|
wneuper@59216
|
248 |
XML.Elem (("STRING", []), [XML.Text str])])
|
wneuper@59390
|
249 |
=> (TermC.int_of_str ci, str)
|
wneuper@59216
|
250 |
| tree => raise ERROR ("input_fill_form: WRONG intree = " ^ xmlstr 0 tree)
|
wneuper@59260
|
251 |
val result = Kernel.inputFillFormula ci str
|
wneuper@59216
|
252 |
in result end)
|
wneuper@59216
|
253 |
handle ERROR msg => message2xml 4711 msg)}\<close>
|
wneuper@59216
|
254 |
|
wneuper@59216
|
255 |
(* val interSteps : calcID -> pos' -> XML.tree *)
|
wneuper@59216
|
256 |
operation_setup inter_steps = \<open>
|
wneuper@59216
|
257 |
{from_lib = Codec.tree,
|
wneuper@59216
|
258 |
to_lib = Codec.tree,
|
wneuper@59216
|
259 |
action = (fn intree =>
|
wneuper@59216
|
260 |
(let
|
wneuper@59216
|
261 |
val (ci, pos) = case intree of
|
wneuper@59216
|
262 |
XML.Elem (("INTERSTEPS", []), [
|
wneuper@59216
|
263 |
XML.Elem (("CALCID", []), [XML.Text ci]),
|
wneuper@59216
|
264 |
pos as XML.Elem (("POSITION", []), _)])
|
wneuper@59390
|
265 |
=> (TermC.int_of_str ci, xml_to_pos pos)
|
wneuper@59216
|
266 |
| tree => raise ERROR ("inter_steps: WRONG intree = " ^ xmlstr 0 tree)
|
wneuper@59260
|
267 |
val result = Kernel.interSteps ci pos
|
wneuper@59216
|
268 |
in result end)
|
wneuper@59216
|
269 |
handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
|
wneuper@59216
|
270 |
|
wneuper@59216
|
271 |
(* val Iterator : calcID -> XML.tree *)
|
wneuper@59216
|
272 |
operation_setup iterator = \<open>
|
wneuper@59216
|
273 |
{from_lib = Codec.int,
|
wneuper@59216
|
274 |
to_lib = Codec.tree,
|
wneuper@59216
|
275 |
action = (fn calcid =>
|
wneuper@59216
|
276 |
let
|
wneuper@59260
|
277 |
val result = Kernel.Iterator calcid
|
wneuper@59216
|
278 |
in result end)}\<close>
|
wneuper@59216
|
279 |
|
wneuper@59216
|
280 |
(* val IteratorTEST : calcID -> iterID *)
|
wneuper@59216
|
281 |
|
wneuper@59216
|
282 |
(* val modelProblem : calcID -> XML.tree *)
|
wneuper@59216
|
283 |
operation_setup model_pbl = \<open>
|
wneuper@59216
|
284 |
{from_lib = Codec.tree,
|
wneuper@59216
|
285 |
to_lib = Codec.tree,
|
wneuper@59216
|
286 |
action = (fn intree =>
|
wneuper@59216
|
287 |
(let
|
wneuper@59216
|
288 |
val (ci) = case intree of
|
wneuper@59216
|
289 |
XML.Elem (("MODIFYCALCHEAD", []), [
|
wneuper@59216
|
290 |
XML.Elem (("CALCID", []), [XML.Text ci])])
|
wneuper@59390
|
291 |
=> (TermC.int_of_str ci)
|
wneuper@59216
|
292 |
| tree => raise ERROR ("model_pbl: WRONG intree = " ^ xmlstr 0 tree)
|
wneuper@59260
|
293 |
val result = Kernel.modelProblem ci
|
wneuper@59216
|
294 |
in result end)
|
wneuper@59216
|
295 |
handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
|
wneuper@59216
|
296 |
|
wneuper@59216
|
297 |
(* val modifyCalcHead : calcID -> icalhd -> XML.tree *)
|
wneuper@59216
|
298 |
operation_setup modify_calchead = \<open>
|
wneuper@59216
|
299 |
{from_lib = Codec.tree,
|
wneuper@59216
|
300 |
to_lib = Codec.tree,
|
wneuper@59216
|
301 |
action = (fn intree =>
|
wneuper@59216
|
302 |
(let
|
wneuper@59216
|
303 |
val (ci, icalhd) = case intree of
|
wneuper@59216
|
304 |
XML.Elem (("MODIFYCALCHEAD", []), [
|
wneuper@59216
|
305 |
XML.Elem (("CALCID", []), [XML.Text ci]),
|
wneuper@59216
|
306 |
icalhd])
|
wneuper@59390
|
307 |
=> (TermC.int_of_str ci, xml_to_icalhd icalhd)
|
wneuper@59216
|
308 |
| tree => raise ERROR ("modify_calchead: WRONG intree = " ^ xmlstr 0 tree)
|
wneuper@59260
|
309 |
val result = Kernel.modifyCalcHead ci icalhd
|
wneuper@59216
|
310 |
in result end)
|
wneuper@59216
|
311 |
handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
|
wneuper@59216
|
312 |
|
wneuper@59216
|
313 |
(* val moveActiveCalcHead : calcID -> XML.tree *)
|
wneuper@59216
|
314 |
operation_setup move_active_calchead = \<open>
|
wneuper@59216
|
315 |
{from_lib = Codec.tree,
|
wneuper@59216
|
316 |
to_lib = Codec.tree,
|
wneuper@59216
|
317 |
action = (fn intree =>
|
wneuper@59216
|
318 |
(let
|
wneuper@59216
|
319 |
val (ci) = case intree of
|
wneuper@59216
|
320 |
XML.Elem (("CALCITERATOR", []), [
|
wneuper@59216
|
321 |
XML.Elem (("CALCID", []), [XML.Text ci])])
|
wneuper@59390
|
322 |
=> (TermC.int_of_str ci)
|
wneuper@59216
|
323 |
| tree => raise ERROR ("move_active_calchead: WRONG intree = " ^ xmlstr 0 tree)
|
wneuper@59260
|
324 |
val result = Kernel.moveActiveCalcHead ci
|
wneuper@59216
|
325 |
in result end)
|
wneuper@59216
|
326 |
handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
|
wneuper@59216
|
327 |
|
wneuper@59216
|
328 |
(* val moveActiveDown : calcID -> XML.tree *)
|
wneuper@59216
|
329 |
operation_setup move_active_down = \<open>
|
wneuper@59216
|
330 |
{from_lib = Codec.tree,
|
wneuper@59216
|
331 |
to_lib = Codec.tree,
|
wneuper@59216
|
332 |
action = (fn intree =>
|
wneuper@59216
|
333 |
(let
|
wneuper@59216
|
334 |
val (ci) = case intree of
|
wneuper@59216
|
335 |
XML.Elem (("CALCITERATOR", []), [
|
wneuper@59216
|
336 |
XML.Elem (("CALCID", []), [XML.Text ci])])
|
wneuper@59390
|
337 |
=> (TermC.int_of_str ci)
|
wneuper@59216
|
338 |
| tree => raise ERROR ("move_active_down: WRONG intree = " ^ xmlstr 0 tree)
|
wneuper@59260
|
339 |
val result = Kernel.moveActiveDown ci
|
wneuper@59216
|
340 |
in result end)
|
wneuper@59216
|
341 |
handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
|
wneuper@59216
|
342 |
|
wneuper@59216
|
343 |
(* val moveActiveFormula : calcID -> pos' -> XML.tree *)
|
wneuper@59216
|
344 |
operation_setup move_active_form = \<open>
|
wneuper@59216
|
345 |
{from_lib = Codec.tree,
|
wneuper@59216
|
346 |
to_lib = Codec.tree,
|
wneuper@59216
|
347 |
action = (fn intree =>
|
wneuper@59216
|
348 |
(let
|
wneuper@59216
|
349 |
val (ci, pos) = case intree of
|
wneuper@59216
|
350 |
XML.Elem (("CALCITERATOR", []), [
|
wneuper@59216
|
351 |
XML.Elem (("CALCID", []), [XML.Text ci]),
|
wneuper@59216
|
352 |
pos as XML.Elem (("POSITION", []), _)])
|
wneuper@59390
|
353 |
=> (TermC.int_of_str ci, xml_to_pos pos)
|
wneuper@59216
|
354 |
| tree => raise ERROR ("move_active_form: WRONG intree = " ^ xmlstr 0 tree)
|
wneuper@59260
|
355 |
val result = Kernel.moveActiveFormula ci pos
|
wneuper@59216
|
356 |
in result end)
|
wneuper@59216
|
357 |
handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
|
wneuper@59216
|
358 |
|
wneuper@59216
|
359 |
(* val moveActiveLevelDown : calcID -> XML.tree *)
|
wneuper@59216
|
360 |
operation_setup move_active_levdown = \<open>
|
wneuper@59216
|
361 |
{from_lib = Codec.tree,
|
wneuper@59216
|
362 |
to_lib = Codec.tree,
|
wneuper@59216
|
363 |
action = (fn intree =>
|
wneuper@59216
|
364 |
(let
|
wneuper@59216
|
365 |
val (ci) = case intree of
|
wneuper@59216
|
366 |
XML.Elem (("CALCITERATOR", []), [
|
wneuper@59216
|
367 |
XML.Elem (("CALCID", []), [XML.Text ci])])
|
wneuper@59390
|
368 |
=> (TermC.int_of_str ci)
|
wneuper@59216
|
369 |
| tree => raise ERROR ("move_active_levdown: WRONG intree = " ^ xmlstr 0 tree)
|
wneuper@59260
|
370 |
val result = Kernel.moveActiveLevelDown ci
|
wneuper@59216
|
371 |
in result end)
|
wneuper@59216
|
372 |
handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
|
wneuper@59216
|
373 |
|
wneuper@59216
|
374 |
(* val moveActiveLevelUp : calcID -> XML.tree *)
|
wneuper@59216
|
375 |
operation_setup move_active_levup = \<open>
|
wneuper@59216
|
376 |
{from_lib = Codec.tree,
|
wneuper@59216
|
377 |
to_lib = Codec.tree,
|
wneuper@59216
|
378 |
action = (fn intree =>
|
wneuper@59216
|
379 |
(let
|
wneuper@59216
|
380 |
val (ci) = case intree of
|
wneuper@59216
|
381 |
XML.Elem (("CALCITERATOR", []), [
|
wneuper@59216
|
382 |
XML.Elem (("CALCID", []), [XML.Text ci])])
|
wneuper@59390
|
383 |
=> (TermC.int_of_str ci)
|
wneuper@59216
|
384 |
| tree => raise ERROR ("move_active_levup: WRONG intree = " ^ xmlstr 0 tree)
|
wneuper@59260
|
385 |
val result = Kernel.moveActiveLevelUp ci
|
wneuper@59216
|
386 |
in result end)
|
wneuper@59216
|
387 |
handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
|
wneuper@59216
|
388 |
|
wneuper@59216
|
389 |
(* val moveActiveRoot : calcID -> XML.tree *)
|
wneuper@59216
|
390 |
operation_setup moveactiveroot = \<open>
|
wneuper@59216
|
391 |
{from_lib = Codec.int,
|
wneuper@59216
|
392 |
to_lib = Codec.tree,
|
wneuper@59216
|
393 |
action = (fn calcid =>
|
wneuper@59216
|
394 |
let
|
wneuper@59260
|
395 |
val result = Kernel.moveActiveRoot calcid
|
wneuper@59216
|
396 |
in result end)}\<close>
|
wneuper@59216
|
397 |
|
wneuper@59216
|
398 |
(* val moveActiveRootTEST : calcID -> XML.tree *)
|
wneuper@59216
|
399 |
|
wneuper@59216
|
400 |
(* val moveActiveUp : calcID -> XML.tree *)
|
wneuper@59216
|
401 |
operation_setup move_active_up = \<open>
|
wneuper@59216
|
402 |
{from_lib = Codec.tree,
|
wneuper@59216
|
403 |
to_lib = Codec.tree,
|
wneuper@59216
|
404 |
action = (fn intree =>
|
wneuper@59216
|
405 |
(let
|
wneuper@59216
|
406 |
val (ci) = case intree of
|
wneuper@59216
|
407 |
XML.Elem (("CALCITERATOR", []), [
|
wneuper@59216
|
408 |
XML.Elem (("CALCID", []), [XML.Text ci])])
|
wneuper@59390
|
409 |
=> (TermC.int_of_str ci)
|
wneuper@59216
|
410 |
| tree => raise ERROR ("move_active_up: WRONG intree = " ^ xmlstr 0 tree)
|
wneuper@59260
|
411 |
val result = Kernel.moveActiveUp ci
|
wneuper@59216
|
412 |
in result end)
|
wneuper@59216
|
413 |
handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
|
wneuper@59216
|
414 |
|
wneuper@59216
|
415 |
(* val moveCalcHead : calcID -> pos' -> XML.tree *)
|
wneuper@59216
|
416 |
operation_setup move_calchead = \<open>
|
wneuper@59216
|
417 |
{from_lib = Codec.tree,
|
wneuper@59216
|
418 |
to_lib = Codec.tree,
|
wneuper@59216
|
419 |
action = (fn intree =>
|
wneuper@59216
|
420 |
(let
|
wneuper@59216
|
421 |
val (ci, pos) = case intree of
|
wneuper@59216
|
422 |
XML.Elem (("CALCITERATOR", []), [
|
wneuper@59216
|
423 |
XML.Elem (("CALCID", []), [XML.Text ci]),
|
wneuper@59216
|
424 |
pos as XML.Elem (("POSITION", []), _)])
|
wneuper@59390
|
425 |
=> (TermC.int_of_str ci, xml_to_pos pos)
|
wneuper@59216
|
426 |
| tree => raise ERROR ("move_active_calchead: WRONG intree = " ^ xmlstr 0 tree)
|
wneuper@59260
|
427 |
val result = Kernel.moveCalcHead ci pos
|
wneuper@59216
|
428 |
in result end)
|
wneuper@59216
|
429 |
handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
|
wneuper@59216
|
430 |
|
wneuper@59216
|
431 |
(* val moveDown : calcID -> pos' -> XML.tree *)
|
wneuper@59216
|
432 |
operation_setup move_down = \<open>
|
wneuper@59216
|
433 |
{from_lib = Codec.tree,
|
wneuper@59216
|
434 |
to_lib = Codec.tree,
|
wneuper@59216
|
435 |
action = (fn intree =>
|
wneuper@59216
|
436 |
(let
|
wneuper@59216
|
437 |
val (ci, pos) = case intree of
|
wneuper@59216
|
438 |
XML.Elem (("CALCITERATOR", []), [
|
wneuper@59216
|
439 |
XML.Elem (("CALCID", []), [XML.Text ci]),
|
wneuper@59216
|
440 |
pos as XML.Elem (("POSITION", []), _)])
|
wneuper@59390
|
441 |
=> (TermC.int_of_str ci, xml_to_pos pos)
|
wneuper@59216
|
442 |
| tree => raise ERROR ("move_down: WRONG intree = " ^ xmlstr 0 tree)
|
wneuper@59260
|
443 |
val result = Kernel.moveDown ci pos
|
wneuper@59216
|
444 |
in result end)
|
wneuper@59216
|
445 |
handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
|
wneuper@59216
|
446 |
|
wneuper@59216
|
447 |
(* val moveLevelDown : calcID -> pos' -> XML.tree *)
|
wneuper@59216
|
448 |
operation_setup move_levdn = \<open>
|
wneuper@59216
|
449 |
{from_lib = Codec.tree,
|
wneuper@59216
|
450 |
to_lib = Codec.tree,
|
wneuper@59216
|
451 |
action = (fn intree =>
|
wneuper@59216
|
452 |
(let
|
wneuper@59216
|
453 |
val (ci, pos) = case intree of
|
wneuper@59216
|
454 |
XML.Elem (("CALCITERATOR", []), [
|
wneuper@59216
|
455 |
XML.Elem (("CALCID", []), [XML.Text ci]),
|
wneuper@59216
|
456 |
pos as XML.Elem (("POSITION", []), _)])
|
wneuper@59390
|
457 |
=> (TermC.int_of_str ci, xml_to_pos pos)
|
wneuper@59216
|
458 |
| tree => raise ERROR ("move_levdn: WRONG intree = " ^ xmlstr 0 tree)
|
wneuper@59260
|
459 |
val result = Kernel.moveLevelDown ci pos
|
wneuper@59216
|
460 |
in result end)
|
wneuper@59216
|
461 |
handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
|
wneuper@59216
|
462 |
|
wneuper@59216
|
463 |
(* val moveLevelUp : calcID -> pos' -> XML.tree *)
|
wneuper@59216
|
464 |
operation_setup move_levup = \<open>
|
wneuper@59216
|
465 |
{from_lib = Codec.tree,
|
wneuper@59216
|
466 |
to_lib = Codec.tree,
|
wneuper@59216
|
467 |
action = (fn intree =>
|
wneuper@59216
|
468 |
(let
|
wneuper@59216
|
469 |
val (ci, pos) = case intree of
|
wneuper@59216
|
470 |
XML.Elem (("CALCITERATOR", []), [
|
wneuper@59216
|
471 |
XML.Elem (("CALCID", []), [XML.Text ci]),
|
wneuper@59216
|
472 |
pos as XML.Elem (("POSITION", []), _)])
|
wneuper@59390
|
473 |
=> (TermC.int_of_str ci, xml_to_pos pos)
|
wneuper@59216
|
474 |
| tree => raise ERROR ("move_levup: WRONG intree = " ^ xmlstr 0 tree)
|
wneuper@59260
|
475 |
val result = Kernel.moveLevelUp ci pos
|
wneuper@59216
|
476 |
in result end)
|
wneuper@59216
|
477 |
handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
|
wneuper@59216
|
478 |
|
wneuper@59216
|
479 |
(* val moveRoot : calcID -> XML.tree *)
|
wneuper@59216
|
480 |
operation_setup move_root = \<open>
|
wneuper@59216
|
481 |
{from_lib = Codec.tree,
|
wneuper@59216
|
482 |
to_lib = Codec.tree,
|
wneuper@59216
|
483 |
action = (fn intree =>
|
wneuper@59216
|
484 |
(let
|
wneuper@59216
|
485 |
val (ci) = case intree of
|
wneuper@59216
|
486 |
XML.Elem (("CALCITERATOR", []), [
|
wneuper@59216
|
487 |
XML.Elem (("CALCID", []), [XML.Text ci])])
|
wneuper@59390
|
488 |
=> (TermC.int_of_str ci)
|
wneuper@59216
|
489 |
| tree => raise ERROR ("move_root: WRONG intree = " ^ xmlstr 0 tree)
|
wneuper@59260
|
490 |
val result = Kernel.moveRoot ci
|
wneuper@59216
|
491 |
in result end)
|
wneuper@59216
|
492 |
handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
|
wneuper@59216
|
493 |
|
wneuper@59216
|
494 |
(* val moveUp : calcID -> pos' -> XML.tree *)
|
wneuper@59216
|
495 |
operation_setup move_up = \<open>
|
wneuper@59216
|
496 |
{from_lib = Codec.tree,
|
wneuper@59216
|
497 |
to_lib = Codec.tree,
|
wneuper@59216
|
498 |
action = (fn intree =>
|
wneuper@59216
|
499 |
(let
|
wneuper@59216
|
500 |
val (ci, pos) = case intree of
|
wneuper@59216
|
501 |
XML.Elem (("CALCITERATOR", []), [
|
wneuper@59216
|
502 |
XML.Elem (("CALCID", []), [XML.Text ci]),
|
wneuper@59216
|
503 |
pos as XML.Elem (("POSITION", []), _)])
|
wneuper@59390
|
504 |
=> (TermC.int_of_str ci, xml_to_pos pos)
|
wneuper@59216
|
505 |
| tree => raise ERROR ("move_up: WRONG intree = " ^ xmlstr 0 tree)
|
wneuper@59260
|
506 |
val result = Kernel.moveUp ci pos
|
wneuper@59216
|
507 |
in result end)
|
wneuper@59216
|
508 |
handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
|
wneuper@59216
|
509 |
|
wneuper@59216
|
510 |
(* val refFormula : calcID -> pos' -> XML.tree *)
|
wneuper@59216
|
511 |
operation_setup refformula = \<open>
|
wneuper@59216
|
512 |
{from_lib = Codec.tree,
|
wneuper@59216
|
513 |
to_lib = Codec.tree,
|
wneuper@59216
|
514 |
action = (fn intree =>
|
wneuper@59216
|
515 |
(let
|
wneuper@59216
|
516 |
val (ci, p) = case intree of
|
wneuper@59216
|
517 |
XML.Elem (("REFFORMULA", []), [
|
wneuper@59216
|
518 |
XML.Elem (("CALCID", []), [XML.Text ci]), p])
|
wneuper@59216
|
519 |
=> (ci, p)
|
wneuper@59216
|
520 |
| tree => raise ERROR ("refformula: WRONG intree = " ^ xmlstr 0 tree)
|
walther@59875
|
521 |
val SOME calcid = TermC.int_opt_of_string ci
|
wneuper@59216
|
522 |
val pos = xml_to_pos p
|
wneuper@59260
|
523 |
val result = Kernel.refFormula calcid pos
|
wneuper@59216
|
524 |
in result end)
|
wneuper@59216
|
525 |
handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
|
wneuper@59216
|
526 |
|
walther@59960
|
527 |
(* Refine.problem
|
walther@59960
|
528 |
val refineProblem : calcID -> pos' -> guh -> XML.tree *)
|
wneuper@59216
|
529 |
operation_setup refine_pbl = \<open>
|
wneuper@59216
|
530 |
{from_lib = Codec.tree,
|
wneuper@59216
|
531 |
to_lib = Codec.tree,
|
wneuper@59216
|
532 |
action = (fn intree =>
|
wneuper@59216
|
533 |
(let
|
wneuper@59216
|
534 |
val (ci, pos, guh) = case intree of
|
wneuper@59216
|
535 |
XML.Elem (("CONTEXTPBL", []), [
|
wneuper@59216
|
536 |
XML.Elem (("CALCID", []), [XML.Text ci]),
|
wneuper@59216
|
537 |
pos as XML.Elem (("POSITION", []), _),
|
wneuper@59216
|
538 |
XML.Elem (("GUH", []), [XML.Text guh])])
|
wneuper@59390
|
539 |
=> (TermC.int_of_str ci, xml_to_pos pos, guh)
|
wneuper@59216
|
540 |
| tree => raise ERROR ("refine_pbl: WRONG intree = " ^ xmlstr 0 tree)
|
wneuper@59260
|
541 |
val result = Kernel.refineProblem ci pos guh
|
wneuper@59216
|
542 |
in result end)
|
wneuper@59216
|
543 |
handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
|
wneuper@59216
|
544 |
|
wneuper@59216
|
545 |
(* val replaceFormula : calcID -> cterm' -> XML.tree *)
|
wneuper@59216
|
546 |
operation_setup replace_form = \<open>
|
wneuper@59216
|
547 |
{from_lib = Codec.tree,
|
wneuper@59216
|
548 |
to_lib = Codec.tree,
|
wneuper@59216
|
549 |
action = (fn intree =>
|
wneuper@59216
|
550 |
(let
|
wneuper@59216
|
551 |
val (calcid, cterm') = case intree of
|
wneuper@59216
|
552 |
XML.Elem (("REPLACEFORMULA", []), [
|
wneuper@59216
|
553 |
XML.Elem (("CALCID", []), [XML.Text ci]), form])
|
walther@59868
|
554 |
=> (ci |> TermC.int_of_str, form |> xml_to_term_NEW |> UnparseC.term)
|
wneuper@59216
|
555 |
| tree => raise ERROR ("replace_form: WRONG intree = " ^ xmlstr 0 tree)
|
wneuper@59260
|
556 |
val result = Kernel.replaceFormula calcid cterm'
|
wneuper@59216
|
557 |
in result end)
|
wneuper@59216
|
558 |
handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
|
wneuper@59216
|
559 |
|
wneuper@59216
|
560 |
(* val requestFillformula : calcID -> errpatID * fillpatID -> XML.tree NOT IMPL. IN isac-java *)
|
wneuper@59216
|
561 |
operation_setup request_fill_form = \<open>
|
wneuper@59216
|
562 |
{from_lib = Codec.tree,
|
wneuper@59216
|
563 |
to_lib = Codec.tree,
|
wneuper@59216
|
564 |
action = (fn intree =>
|
wneuper@59216
|
565 |
(let
|
wneuper@59216
|
566 |
val (ci, errpat_id, fillpat_id) = case intree of
|
wneuper@59216
|
567 |
XML.Elem (("AUTOCALC", []), [
|
wneuper@59216
|
568 |
XML.Elem (("CALCID", []), [XML.Text ci]),
|
wneuper@59216
|
569 |
XML.Elem (("ERRPATTID", []), [XML.Text errpat_id]),
|
wneuper@59216
|
570 |
XML.Elem (("FILLPATTID", []), [XML.Text fillpat_id])])
|
wneuper@59390
|
571 |
=> (TermC.int_of_str ci, errpat_id, fillpat_id)
|
wneuper@59216
|
572 |
| tree => raise ERROR ("request_fill_form: WRONG intree = " ^ xmlstr 0 tree)
|
wneuper@59260
|
573 |
val result = Kernel.requestFillformula ci (errpat_id, fillpat_id)
|
wneuper@59216
|
574 |
in result end)
|
wneuper@59216
|
575 |
handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
|
wneuper@59216
|
576 |
|
wneuper@59216
|
577 |
(* val resetCalcHead : calcID -> XML.tree *)
|
wneuper@59216
|
578 |
operation_setup reset_calchead = \<open>
|
wneuper@59216
|
579 |
{from_lib = Codec.tree,
|
wneuper@59216
|
580 |
to_lib = Codec.tree,
|
wneuper@59216
|
581 |
action = (fn intree =>
|
wneuper@59216
|
582 |
(let
|
wneuper@59216
|
583 |
val (ci) = case intree of
|
wneuper@59216
|
584 |
XML.Elem (("MODIFYCALCHEAD", []), [
|
wneuper@59216
|
585 |
XML.Elem (("CALCID", []), [XML.Text ci])])
|
wneuper@59390
|
586 |
=> (TermC.int_of_str ci)
|
wneuper@59216
|
587 |
| tree => raise ERROR ("reset_calchead: WRONG intree = " ^ xmlstr 0 tree)
|
wneuper@59260
|
588 |
val result = Kernel.resetCalcHead ci
|
wneuper@59216
|
589 |
in result end)
|
wneuper@59216
|
590 |
handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
|
wneuper@59216
|
591 |
|
wneuper@59216
|
592 |
(* val setContext : calcID -> pos' -> guh -> XML.tree *)
|
wneuper@59216
|
593 |
operation_setup set_ctxt = \<open>
|
wneuper@59216
|
594 |
{from_lib = Codec.tree,
|
wneuper@59216
|
595 |
to_lib = Codec.tree,
|
wneuper@59216
|
596 |
action = (fn intree =>
|
wneuper@59216
|
597 |
(let
|
wneuper@59216
|
598 |
val (ci, pos, guh) = case intree of
|
wneuper@59216
|
599 |
XML.Elem (("CONTEXT", []), [
|
wneuper@59216
|
600 |
XML.Elem (("CALCID", []), [XML.Text ci]),
|
wneuper@59216
|
601 |
pos as XML.Elem (("POSITION", []), _),
|
wneuper@59216
|
602 |
XML.Elem (("GUH", []), [XML.Text guh])])
|
wneuper@59390
|
603 |
=> (TermC.int_of_str ci, xml_to_pos pos, guh)
|
wneuper@59216
|
604 |
| tree => raise ERROR ("set_ctxt: WRONG intree = " ^ xmlstr 0 tree)
|
wneuper@59260
|
605 |
val result = Kernel.setContext ci pos guh
|
wneuper@59216
|
606 |
in result end)
|
wneuper@59216
|
607 |
handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
|
wneuper@59216
|
608 |
|
wneuper@59216
|
609 |
(*//===vvv TODO ================================================================\\\\\\\\\\\\\\\\*)
|
wneuper@59216
|
610 |
|
wneuper@59216
|
611 |
(* val setMethod : calcID -> metID -> XML.tree *)
|
wneuper@59216
|
612 |
operation_setup set_met = \<open>
|
wneuper@59216
|
613 |
{from_lib = Codec.tree,
|
wneuper@59216
|
614 |
to_lib = Codec.tree,
|
wneuper@59216
|
615 |
action = (fn intree =>
|
wneuper@59216
|
616 |
(let
|
wneuper@59216
|
617 |
val (ci, met_id) = case intree of
|
wneuper@59216
|
618 |
XML.Elem (("MODIFYCALCHEAD", []), [
|
wneuper@59216
|
619 |
XML.Elem (("CALCID", []), [XML.Text ci]),
|
wneuper@59216
|
620 |
XML.Elem (("METHODID", []), [met_id])])
|
wneuper@59390
|
621 |
=> (TermC.int_of_str ci, xml_to_strs met_id)
|
wneuper@59216
|
622 |
| tree => raise ERROR ("set_met: WRONG intree = " ^ xmlstr 0 tree)
|
wneuper@59260
|
623 |
val result = Kernel.setMethod ci met_id
|
wneuper@59216
|
624 |
in result end)
|
wneuper@59216
|
625 |
handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
|
wneuper@59216
|
626 |
|
wneuper@59216
|
627 |
(* val setNextTactic : calcID -> tac -> XML.tree *)
|
wneuper@59216
|
628 |
operation_setup set_next_tac = \<open>
|
wneuper@59216
|
629 |
{from_lib = Codec.tree,
|
wneuper@59216
|
630 |
to_lib = Codec.tree,
|
wneuper@59216
|
631 |
action = (fn intree =>
|
wneuper@59216
|
632 |
(let
|
wneuper@59216
|
633 |
val (ci, tac) = case intree of
|
wneuper@59216
|
634 |
XML.Elem (("SETNEXTTACTIC", []), [
|
wneuper@59216
|
635 |
XML.Elem (("CALCID", []), [XML.Text ci]),
|
wneuper@59216
|
636 |
tac])
|
wneuper@59390
|
637 |
=> (TermC.int_of_str ci, xml_to_tac tac)
|
wneuper@59216
|
638 |
| tree => raise ERROR ("set_next_tac: WRONG intree = " ^ xmlstr 0 tree)
|
wneuper@59260
|
639 |
val result = Kernel.setNextTactic ci tac
|
wneuper@59216
|
640 |
in result end)
|
wneuper@59216
|
641 |
handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
|
wneuper@59216
|
642 |
|
wneuper@59216
|
643 |
(*\\===^^^ TODO ================================================================///////////////*)
|
wneuper@59216
|
644 |
|
wneuper@59216
|
645 |
(* val setProblem : calcID -> pblID -> XML.tree *)
|
wneuper@59216
|
646 |
operation_setup set_pbl = \<open>
|
wneuper@59216
|
647 |
{from_lib = Codec.tree,
|
wneuper@59216
|
648 |
to_lib = Codec.tree,
|
wneuper@59216
|
649 |
action = (fn intree =>
|
wneuper@59216
|
650 |
(let
|
wneuper@59216
|
651 |
val (ci, pbl_id) = case intree of
|
wneuper@59216
|
652 |
XML.Elem (("MODIFYCALCHEAD", []), [
|
wneuper@59216
|
653 |
XML.Elem (("CALCID", []), [XML.Text ci]),
|
wneuper@59216
|
654 |
XML.Elem (("PROBLEMID", []), [pbl_id])])
|
wneuper@59390
|
655 |
=> (TermC.int_of_str ci, xml_to_strs pbl_id)
|
wneuper@59216
|
656 |
| tree => raise ERROR ("set_pbl: WRONG intree = " ^ xmlstr 0 tree)
|
wneuper@59260
|
657 |
val result = Kernel.setProblem ci pbl_id
|
wneuper@59216
|
658 |
in result end)
|
wneuper@59216
|
659 |
handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
|
wneuper@59216
|
660 |
|
wneuper@59216
|
661 |
(* val setTheory : calcID -> thyID -> XML.tree *)
|
wneuper@59216
|
662 |
operation_setup set_thy = \<open>
|
wneuper@59216
|
663 |
{from_lib = Codec.tree,
|
wneuper@59216
|
664 |
to_lib = Codec.tree,
|
wneuper@59216
|
665 |
action = (fn intree =>
|
wneuper@59216
|
666 |
(let
|
wneuper@59216
|
667 |
val (ci, thy_id) = case intree of
|
wneuper@59216
|
668 |
XML.Elem (("MODIFYCALCHEAD", []), [
|
wneuper@59216
|
669 |
XML.Elem (("CALCID", []), [XML.Text ci]),
|
wneuper@59216
|
670 |
XML.Elem (("THEORYID", []), [XML.Text thy_id])])
|
wneuper@59390
|
671 |
=> (TermC.int_of_str ci, thy_id)
|
wneuper@59216
|
672 |
| tree => raise ERROR ("set_thy: WRONG intree = " ^ xmlstr 0 tree)
|
wneuper@59260
|
673 |
val result = Kernel.setTheory ci thy_id
|
wneuper@59216
|
674 |
in result end)
|
wneuper@59216
|
675 |
handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
|
wneuper@59216
|
676 |
|
wneuper@59218
|
677 |
(* for inital java-tests/isac/bridge/TestTerm.scala *)
|
wneuper@59216
|
678 |
operation_setup make_int = \<open>
|
wneuper@59216
|
679 |
{from_lib = Codec.unit,
|
wneuper@59216
|
680 |
to_lib = Codec.term,
|
wneuper@59216
|
681 |
action = (fn _ => HOLogic.mk_number @{typ int} 3)}
|
wneuper@59216
|
682 |
\<close>
|
wneuper@59216
|
683 |
|
wneuper@59218
|
684 |
(* passes libisabelle term in both directions;
|
wneuper@59218
|
685 |
the use of direction isac-java \<longrightarrow> Isabelle/Isac is a future design question *)
|
wneuper@59216
|
686 |
operation_setup test_term_transfer = \<open>
|
wneuper@59216
|
687 |
{from_lib = Codec.tree,
|
wneuper@59216
|
688 |
to_lib = Codec.tree,
|
wneuper@59216
|
689 |
action = (fn intree =>
|
wneuper@59216
|
690 |
(let
|
wneuper@59216
|
691 |
val t = case intree of
|
wneuper@59216
|
692 |
XML.Elem (("MATHML", []), [
|
wneuper@59216
|
693 |
XML.Elem (("ISA", []), [XML.Text _]),
|
wneuper@59216
|
694 |
XML.Elem (("TERM", []), [xt])])
|
wneuper@59216
|
695 |
=> xt |> Codec.decode Codec.term |> Codec.the_success
|
wneuper@59216
|
696 |
| tree => raise ERROR ("test_term_transfer: WRONG intree = " ^ xmlstr 0 tree)
|
wneuper@59216
|
697 |
val test_out = HOLogic.mk_eq (t, Const ("processed_by_Isabelle_Isac", type_of t))
|
wneuper@59216
|
698 |
in xml_of_term_NEW test_out end)
|
wneuper@59216
|
699 |
handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
|
wneuper@59216
|
700 |
|
wneuper@59216
|
701 |
operation_setup test_term_one_way = \<open>
|
wneuper@59216
|
702 |
{from_lib = Codec.string,
|
wneuper@59216
|
703 |
to_lib = Codec.tree,
|
wneuper@59216
|
704 |
action = (fn instr =>
|
wneuper@59216
|
705 |
(let
|
wneuper@59390
|
706 |
val t = instr |> TermC.parse @{theory} |> the |> Thm.term_of
|
wneuper@59216
|
707 |
val test_out = HOLogic.mk_eq (t, Const ("processed_by_Isabelle_Isac", type_of t))
|
wneuper@59216
|
708 |
in xml_of_term_NEW test_out end)
|
wneuper@59216
|
709 |
handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
|
wneuper@59216
|
710 |
|
wneuper@59218
|
711 |
(* tool for creating libisabelle's terms *)
|
wneuper@59218
|
712 |
operation_setup scalaterm_of_string = \<open>
|
wneuper@59218
|
713 |
{from_lib = Codec.string,
|
wneuper@59218
|
714 |
to_lib = Codec.tree,
|
wneuper@59218
|
715 |
action = (fn instr =>
|
wneuper@59218
|
716 |
(let
|
wneuper@59390
|
717 |
val termopt = TermC.parseNEW (Proof_Context.init_global @{theory}) instr
|
wneuper@59220
|
718 |
in
|
wneuper@59390
|
719 |
case TermC.parseNEW (Proof_Context.init_global @{theory}) instr of
|
wneuper@59220
|
720 |
SOME term => xml_of_term_NEW term
|
wneuper@59220
|
721 |
| NONE => sysERROR2xml 4711 ("*** syntax ERROR in: " ^ instr)
|
wneuper@59220
|
722 |
end))}\<close>
|
wneuper@59218
|
723 |
|
wneuper@59216
|
724 |
end |