1 (* the interface between the isac-kernel and the java-frontend; |
|
2 the isac-kernel holds calc-trees; stdout in XML-format. |
|
3 authors: Walther Neuper 2002 |
|
4 (c) due to copyright terms |
|
5 |
|
6 use"FE-interface/interface.sml"; |
|
7 use"interface.sml"; |
|
8 *) |
|
9 |
|
10 signature INTERFACE = |
|
11 sig |
|
12 val CalcTree : fmz list -> unit |
|
13 val DEconstrCalcTree : calcID -> unit |
|
14 val Iterator : calcID -> unit |
|
15 val IteratorTEST : calcID -> iterID |
|
16 val appendFormula : calcID -> cterm' -> unit |
|
17 val autoCalculate : calcID -> auto -> unit |
|
18 val checkContext : calcID -> pos' -> guh -> unit |
|
19 val fetchApplicableTactics : calcID -> int -> pos' -> unit |
|
20 val fetchProposedTactic : calcID -> unit |
|
21 val applyTactic : calcID -> pos' -> tac -> unit |
|
22 val getAccumulatedAsms : calcID -> pos' -> unit |
|
23 val getActiveFormula : calcID -> unit |
|
24 val getAssumptions : calcID -> pos' -> unit |
|
25 val initContext : calcID -> ketype -> pos' -> unit |
|
26 val getFormulaeFromTo : calcID -> pos' -> pos' -> int -> bool -> unit |
|
27 val getTactic : calcID -> pos' -> unit |
|
28 val interSteps : calcID -> pos' -> unit |
|
29 val modifyCalcHead : calcID -> icalhd -> unit |
|
30 val moveActiveCalcHead : calcID -> unit |
|
31 val moveActiveDown : calcID -> unit |
|
32 val moveActiveDownTEST : calcID -> unit |
|
33 val moveActiveFormula : calcID -> pos' -> unit |
|
34 val moveActiveLevelDown : calcID -> unit |
|
35 val moveActiveLevelUp : calcID -> unit |
|
36 val moveActiveRoot : calcID -> unit |
|
37 val moveActiveRootTEST : calcID -> unit |
|
38 val moveActiveUp : calcID -> unit |
|
39 val moveCalcHead : calcID -> pos' -> unit |
|
40 val moveDown : calcID -> pos' -> unit |
|
41 val moveLevelDown : calcID -> pos' -> unit |
|
42 val moveLevelUp : calcID -> pos' -> unit |
|
43 val moveRoot : calcID -> unit |
|
44 val moveUp : calcID -> pos' -> unit |
|
45 val refFormula : calcID -> pos' -> unit |
|
46 val replaceFormula : calcID -> cterm' -> unit |
|
47 val resetCalcHead : calcID -> unit |
|
48 val modelProblem : calcID -> unit |
|
49 val refineProblem : calcID -> pos' -> guh -> unit |
|
50 val setContext : calcID -> pos' -> guh -> unit |
|
51 val setMethod : calcID -> metID -> unit |
|
52 val setNextTactic : calcID -> tac -> unit |
|
53 val setProblem : calcID -> pblID -> unit |
|
54 val setTheory : calcID -> thyID -> unit |
|
55 end |
|
56 |
|
57 |
|
58 (*------------------------------------------------------------------*) |
|
59 structure interface : INTERFACE = |
|
60 struct |
|
61 (*------------------------------------------------------------------*) |
|
62 |
|
63 (*.encode "Isabelle"-strings as seen by the user to the |
|
64 format accepted by Isabelle. |
|
65 encode "^" ---> "^^^"; see IsacKnowledge/Atools.thy; |
|
66 called for each cterm', icalhd, fmz in this interface; |
|
67 + see "fun decode" in xmlsrc/mathml.sml.*) |
|
68 fun encode (str:cterm') = |
|
69 let fun enc [] = [] |
|
70 | enc ("^"::cs) = "^"::"^"::"^"::(enc cs) |
|
71 | enc (c::cs) = c::(enc cs) |
|
72 in (implode o enc o explode) str:cterm' end; |
|
73 fun encode_imodel (imodel:imodel) = |
|
74 let fun enc (Given ifos) = Given (map encode ifos) |
|
75 | enc (Find ifos) = Find (map encode ifos) |
|
76 | enc (Relate ifos) = Relate (map encode ifos) |
|
77 in map enc imodel:imodel end; |
|
78 fun encode_icalhd ((pos', headl, imodel, pos_, spec):icalhd) = |
|
79 (pos', encode headl, encode_imodel imodel, pos_, spec):icalhd; |
|
80 fun encode_fmz ((ifos, spec):fmz) = (map encode ifos, spec):fmz; |
|
81 |
|
82 |
|
83 (***. CalcTree .***) |
|
84 |
|
85 (** add and delete users **) |
|
86 |
|
87 (*.'Iterator 1' must exist with each CalcTree; |
|
88 the only for updating the calc-tree |
|
89 WN.0411: only 'Iterator 1' is stored, |
|
90 all others are just calculated on the fly |
|
91 TODO: adapt Iterator, add_user(= add_iterator!),etc. accordingly .*) |
|
92 fun Iterator (cI:calcID) = (*returned ID unnecessary after WN.0411*) |
|
93 (adduserOK2xml cI (add_user (cI:calcID))) |
|
94 handle _ => sysERROR2xml cI "error in kernel"; |
|
95 fun IteratorTEST (cI:calcID) = add_user (cI:calcID); |
|
96 (*fun DEconstructIterator (cI:calcID) (uI:iterID) = |
|
97 deluserOK2xml (del_user cI uI);*) |
|
98 |
|
99 (*.create a calc-tree; for calls from java: thus ^^^ decoded to ^; |
|
100 compare "fun CalcTreeTEST" which does NOT decode.*) |
|
101 fun CalcTree |
|
102 [(fmz, sp):fmz] (*for several variants lateron*) = |
|
103 (* val[(fmz,sp):fmz]=[(["fixedValues [r=Arbfix]","maximum A","valuesFor [a,b]", |
|
104 "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]", |
|
105 "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]", |
|
106 "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]", |
|
107 "boundVariable a","boundVariable b","boundVariable alpha", |
|
108 "interval {x::real. 0 <= x & x <= 2*r}", |
|
109 "interval {x::real. 0 <= x & x <= 2*r}", |
|
110 "interval {x::real. 0 <= x & x <= pi}", |
|
111 "errorBound (eps=(0::real))"], |
|
112 ("DiffApp.thy", ["maximum_of","function"], |
|
113 ["DiffApp","max_by_calculus"]))]; |
|
114 |
|
115 *) |
|
116 (let val cs = nxt_specify_init_calc (encode_fmz (fmz, sp)) |
|
117 (*FIXME.WN.8.03: error-handling missing*) |
|
118 val cI = add_calc cs |
|
119 in calctreeOK2xml cI end) |
|
120 handle _ => sysERROR2xml 0 "error in kernel"; |
|
121 |
|
122 fun DEconstrCalcTree (cI:calcID) = |
|
123 deconstructcalctreeOK2xml (del_calc cI); |
|
124 |
|
125 |
|
126 fun getActiveFormula (cI:calcID) = iteratorOK2xml cI (get_pos cI 1); |
|
127 |
|
128 fun moveActiveFormula (cI:calcID) (p:pos') = |
|
129 let val ((pt,_),_) = get_calc cI |
|
130 in if existpt' p pt then (upd_ipos cI 1 p; iteratorOK2xml cI p) |
|
131 else sysERROR2xml cI "frontend sends a non-existing pos" end; |
|
132 |
|
133 (*. set the next tactic to be applied: dont't change the calc-tree, |
|
134 but remember the envisaged changes for fun autoCalculate; |
|
135 compare force NextTactic .*) |
|
136 (* val (cI, tac) = (1, Add_Given "equality (x ^^^ 2 + 4 * x + 3 = 0)"); |
|
137 val (cI, tac) = (1, Specify_Theory "PolyEq.thy"); |
|
138 val (cI, tac) = (1, Specify_Problem ["normalize","polynomial", |
|
139 "univariate","equation"]); |
|
140 val (cI, tac) = (1, Subproblem ("Poly.thy", |
|
141 ["polynomial","univariate","equation"])); |
|
142 val (cI, tac) = (1, Model_Problem["linear","univariate","equation","test"]); |
|
143 val (cI, tac) = (1, Detail_Set "Test_simplify"); |
|
144 val (cI, tac) = (1, Apply_Method ["Test", "solve_linear"]); |
|
145 val (cI, tac) = (1, Rewrite_Set "Test_simplify"); |
|
146 *) |
|
147 fun setNextTactic (cI:calcID) tac = |
|
148 let val ((pt, _), _) = get_calc cI |
|
149 val ip = get_pos cI 1 |
|
150 in case locatetac tac (pt, ip) of |
|
151 (* val ("ok", (tacis, c, (_,p'))) = locatetac tac (pt, ip); |
|
152 *) |
|
153 ("ok", (tacis, _, _)) => |
|
154 (upd_calc cI ((pt, ip), tacis); setnexttactic2xml cI "ok") |
|
155 | ("unsafe-ok", (tacis, _, _)) => |
|
156 (upd_calc cI ((pt, ip), tacis); setnexttactic2xml cI "unsafe-ok") |
|
157 | ("not-applicable",_) => setnexttactic2xml cI "not-applicable" |
|
158 | ("end-of-calculation",_) => |
|
159 setnexttactic2xml cI "end-of-calculation" |
|
160 | ("failure",_) => sysERROR2xml cI "failure" |
|
161 end; |
|
162 |
|
163 (*. apply a tactic at a position and update the calc-tree if applicable .*) |
|
164 (*WN080226 java-code is missing, errors smltest/IsacKnowledge/polyminus.sml*) |
|
165 (* val (cI, ip, tac) = (1, p, hd appltacs); |
|
166 val (cI, ip, tac) = (1, p, (hd (sel_appl_atomic_tacs pt p))); |
|
167 *) |
|
168 fun applyTactic (cI:calcID) ip tac = |
|
169 let val ((pt, _), _) = get_calc cI |
|
170 val p = get_pos cI 1 |
|
171 in case locatetac tac (pt, ip) of |
|
172 (* val ("ok", (tacis, c, (pt',p'))) = locatetac tac (pt, ip); |
|
173 *) |
|
174 ("ok", (_, c, ptp as (_,p'))) => |
|
175 (upd_calc cI (ptp, []); upd_ipos cI 1 p'; |
|
176 autocalculateOK2xml cI p (if null c then p' |
|
177 else last_elem c) p') |
|
178 | ("unsafe-ok", (_, c, ptp as (_,p'))) => |
|
179 (upd_calc cI (ptp, []); upd_ipos cI 1 p'; |
|
180 autocalculateOK2xml cI p (if null c then p' |
|
181 else last_elem c) p') |
|
182 | ("end-of-calculation", (_, c, ptp as (_,p'))) => |
|
183 (upd_calc cI (ptp, []); upd_ipos cI 1 p'; |
|
184 autocalculateOK2xml cI p (if null c then p' |
|
185 else last_elem c) p') |
|
186 |
|
187 |
|
188 | (str,_) => autocalculateERROR2xml cI "failure" |
|
189 end; |
|
190 |
|
191 |
|
192 |
|
193 (* val cI = 1; |
|
194 *) |
|
195 fun fetchProposedTactic (cI:calcID) = |
|
196 (case step (get_pos cI 1) (get_calc cI) of |
|
197 ("ok", (tacis, _, _)) => |
|
198 let val _= upd_tacis cI tacis |
|
199 val (tac,_,_) = last_elem tacis |
|
200 in fetchproposedtacticOK2xml cI tac end |
|
201 | ("helpless",_) => fetchproposedtacticERROR2xml cI "helpless" |
|
202 | ("no-fmz-spec",_) => fetchproposedtacticERROR2xml cI "no-fmz-spec" |
|
203 | ("end-of-calculation",_) => |
|
204 fetchproposedtacticERROR2xml cI "end-of-calculation") |
|
205 handle _ => sysERROR2xml cI "error in kernel"; |
|
206 |
|
207 (*datatype auto = FIXXXME040624: does NOT match interfaces/ITOCalc.java |
|
208 Step of int (*1 do #int steps (may stop in model/specify) |
|
209 IS VERY INEFFICIENT IN MODEL/SPECIY*) |
|
210 | CompleteModel (*2 complete modeling |
|
211 if model complete, finish specifying*) |
|
212 | CompleteCalcHead (*3 complete model/specify in one go*) |
|
213 | CompleteToSubpbl (*4 stop at the next begin of a subproblem, |
|
214 if none, complete the actual (sub)problem*) |
|
215 | CompleteSubpbl (*5 complete the actual (sub)problem (incl.ev.subproblems)*) |
|
216 | CompleteCalc; (*6 complete the calculation as a whole*)*) |
|
217 fun autoCalculate (cI:calcID) auto = |
|
218 (* val (cI, auto) = (1,CompleteCalc); |
|
219 val (cI, auto) = (1,CompleteModel); |
|
220 val (cI, auto) = (1,CompleteCalcHead); |
|
221 val (cI, auto) = (1,Step 1); |
|
222 *) |
|
223 (let val pold = get_pos cI 1 |
|
224 val x = autocalc [] pold (get_calc cI) auto |
|
225 in |
|
226 case x of |
|
227 (* val (str, c, ptp as (_,p)) = x; |
|
228 *) |
|
229 ("ok", c, ptp as (_,p)) => |
|
230 (upd_calc cI (ptp, []); upd_ipos cI 1 p; |
|
231 autocalculateOK2xml cI pold (if null c then pold |
|
232 else last_elem c) p) |
|
233 | ("end-of-calculation", c, ptp as (_,p)) => |
|
234 (upd_calc cI (ptp, []); upd_ipos cI 1 p; |
|
235 autocalculateOK2xml cI pold (if null c then pold |
|
236 else last_elem c) p) |
|
237 | (str, _, _) => autocalculateERROR2xml cI str |
|
238 end) |
|
239 handle _ => sysERROR2xml cI "error in kernel"; |
|
240 |
|
241 |
|
242 (* val (cI:calcID, ichd as ((p,_),_,_,_,_):icalhd) = |
|
243 (1, (([],Pbl), "not used here", |
|
244 [Given ["fixedValues [r=Arbfix]"], |
|
245 Find ["maximum A", "valuesFor [a,b]"(*new input*)], |
|
246 Relate ["relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]"]], Pbl, |
|
247 ("DiffApp.thy", ["maximum_of","function"], |
|
248 ["DiffApp","max_by_calculus"]))); |
|
249 val (cI:calcID, ichd as ((p,_),_,_,_,_):icalhd) = |
|
250 (1, (([],Pbl),"solve (x+1=2, x)", |
|
251 [Given ["equality (x+1=2)", "solveFor x"], |
|
252 Find ["solutions L"]], |
|
253 Pbl, |
|
254 ("Test.thy", ["linear","univariate","equation","test"], |
|
255 ["Test","solve_linear"]))); |
|
256 val (cI:calcID, ichd as ((p,_),_,_,_,_):icalhd) = |
|
257 (1, (([],Pbl),"solveTest (1+-1*2+x=0,x)", [], Pbl, ("", [], []))); |
|
258 val (cI, p:pos')=(1, ([1],Frm)); |
|
259 val (cI, p:pos')=(1, ([1,2,1,3],Res)); |
|
260 *) |
|
261 fun getTactic cI (p:pos') = |
|
262 (let val ((pt,_),_) = get_calc cI |
|
263 val (form, tac, asms) = pt_extract (pt, p) |
|
264 in case tac of |
|
265 (* val SOME ta = tac; |
|
266 *) |
|
267 SOME ta => gettacticOK2xml cI ta |
|
268 | NONE => gettacticERROR2xml cI ("no tactic at position "^pos'2str p) |
|
269 end) |
|
270 handle _ => sysERROR2xml cI "syserror in getTactic"; |
|
271 |
|
272 (*. see ICalcIterator#fetchApplicableTactics |
|
273 @see #TACTICS_ALL |
|
274 @see #TACTICS_CURRENT_THEORY |
|
275 @see #TACTICS_CURRENT_METHOD ..the only impl.WN040307.*) |
|
276 (*. fetch tactics to be applied to a particular step.*) |
|
277 (* WN071231 kept this version for later parametrisation*) |
|
278 (*.version 1: fetch _all_ tactics from script .*) |
|
279 fun fetchApplicableTactics cI (scope:int) (p:pos') = |
|
280 (let val ((pt, _), _) = get_calc cI |
|
281 in (applicabletacticsOK cI (sel_rules pt p)) |
|
282 handle PTREE str => sysERROR2xml cI str |
|
283 end) |
|
284 handle _ => sysERROR2xml cI "error in kernel"; |
|
285 (*.version 2: fetch _applicable_ _elementary_ (ie. recursively |
|
286 decompose rule-sets) Rewrite*, Calculate .*) |
|
287 fun fetchApplicableTactics cI (scope:int) (p:pos') = |
|
288 (let val ((pt, _), _) = get_calc cI |
|
289 in (applicabletacticsOK cI (sel_appl_atomic_tacs pt p)) |
|
290 handle PTREE str => sysERROR2xml cI str |
|
291 end) |
|
292 handle _ => sysERROR2xml cI "error in kernel"; |
|
293 |
|
294 fun getAssumptions cI (p:pos') = |
|
295 (let val ((pt,_),_) = get_calc cI |
|
296 val (_, _, asms) = pt_extract (pt, p) |
|
297 in getasmsOK2xml cI asms end) |
|
298 handle _ => sysERROR2xml cI "syserror in getAssumptions"; |
|
299 |
|
300 (*WN0502 @see ME/ctree: type asms: illdesigned, thus no positions returned*) |
|
301 fun getAccumulatedAsms cI (p:pos') = |
|
302 (let val ((pt, _), _) = get_calc cI |
|
303 val ass = map fst (get_assumptions_ pt p) |
|
304 in (*getaccuasmsOK2xml cI (get_assumptions_ pt p)*) |
|
305 getasmsOK2xml cI ass end) |
|
306 handle _ => sysERROR2xml cI "syserror in getAccumulatedAsms"; |
|
307 |
|
308 |
|
309 (*since moveActive* does NOT transfer pos java --> sml (only sml --> java) |
|
310 refFormula might become involved in far-off errors !!!*) |
|
311 fun refFormula cI (p:pos') = (*WN0501 rename to 'fun getElement' !*) |
|
312 (* val (cI, uI) = (1,1); |
|
313 *) |
|
314 (let val ((pt,_),_) = get_calc cI |
|
315 val (form, tac, asms) = pt_extract (pt, p) |
|
316 in refformulaOK2xml cI p form end) |
|
317 handle _ => sysERROR2xml cI "error in kernel"; |
|
318 |
|
319 (*.get formulae 'from' 'to' w.r.t. ordering in Position#compareTo(Position p); |
|
320 in case of CalcHeads only the headline is taken |
|
321 (the pos' allows distinction between PrfObj and PblObj anyway); |
|
322 'level' is adjusted such that an 'interval' of formulae is returned; |
|
323 'from' 'to' are designed for use by iterators of calcChangedEvent; |
|
324 thus 'from' is the last unchanged position.*) |
|
325 fun getFormulaeFromTo cI (from as ([],Pbl):pos') (to as ([],Pbl):pos')_ false = |
|
326 (*special case because 'from' is _before_ the first elements to be returned*) |
|
327 (* val (cI, from, to, level) = (1, ([],Pbl), ([],Pbl), 1); |
|
328 *) |
|
329 ((let val ((pt,_),_) = get_calc cI |
|
330 val (ModSpec (_,_,headline,_,_,_),_,_) = pt_extract (pt, to) |
|
331 in getintervalOK cI [(to, headline)] end) |
|
332 handle _ => sysERROR2xml cI "error in kernel") |
|
333 |
|
334 | getFormulaeFromTo cI (from as ([],Pbl):pos') (to as ([],Met):pos')_ false = |
|
335 getFormulaeFromTo cI ([],Pbl) ([],Pbl) (~00000) false |
|
336 |
|
337 | getFormulaeFromTo cI (from:pos') (to:pos') level false = |
|
338 (* val (cI, from, to, level) = (1, unc, gen, 0); |
|
339 val (cI, from, to, level) = (1, unc, gen, 1); |
|
340 val (cI, from, to, level) = (1, ([],Pbl), ([],Met), 1); |
|
341 *) |
|
342 (if from = to then sysERROR2xml cI "getFormulaeFromTo: From = To" |
|
343 else |
|
344 (case from of |
|
345 ([],Res) => sysERROR2xml cI "getFormulaeFromTo does: moveDown \ |
|
346 \from=([],Res) .. goes beyond result" |
|
347 | _ => let val ((pt,_),_) = get_calc cI |
|
348 val f = move_dn [] pt from |
|
349 fun max (a,b) = if a < b then b else a |
|
350 (*must reach margins ...*) |
|
351 val lev = max (level, max (lev_of from, lev_of to)) |
|
352 in getintervalOK cI (get_interval f to lev pt) end) |
|
353 handle _ => sysERROR2xml cI "error in getFormulaeFromTo") |
|
354 |
|
355 | getFormulaeFromTo cI from to level true = |
|
356 sysERROR2xml cI "getFormulaeFromTo impl.for formulae only,\ |
|
357 \i.e. last arg only impl. for false, _NOT_ true"; |
|
358 |
|
359 |
|
360 (* val (cI, ip) = (1, ([1,9], Res)); |
|
361 val (cI, ip) = (1, ([], Res)); |
|
362 val (cI, ip) = (1, ([2], Res)); |
|
363 val (cI, ip) = (1, ([3,1], Res)); |
|
364 val (cI, ip) = (1, ([1,2,1], Res)); |
|
365 *) |
|
366 fun interSteps cI ip = |
|
367 (let val ((pt,p), tacis) = get_calc cI |
|
368 in if (not o is_interpos) ip |
|
369 then interStepsERROR cI "only formulae with position (_,Res) \ |
|
370 \may have intermediate steps above them" |
|
371 else let val ip' = lev_pred' pt ip |
|
372 (* val (str, pt', lastpos) = detailstep pt ip; |
|
373 *) |
|
374 in case detailstep pt ip of |
|
375 ("detailrls", pt(*, pos'forms*), lastpos) => |
|
376 (upd_calc cI ((pt, p), tacis); |
|
377 interStepsOK cI (*pos'forms*) ip' ip' lastpos) |
|
378 | ("no-Rewrite_Set...", _, _) => |
|
379 sysERROR2xml cI "no Rewrite_Set..." |
|
380 | (_, _(*, pos'formshds*), lastpos) => |
|
381 interStepsOK cI (*pos'formshds*) ip' ip' lastpos |
|
382 end |
|
383 end) |
|
384 handle _ => sysERROR2xml cI "error in kernel"; |
|
385 |
|
386 fun modifyCalcHead (cI:calcID) (ichd as ((p,_),_,_,_,_):icalhd) = |
|
387 (let val ((pt,_),_) = get_calc cI |
|
388 val (pt, chd as (_,p_,_,_,_,_)) = input_icalhd pt ichd |
|
389 in (upd_calc cI ((pt, (p,p_)), []); |
|
390 modifycalcheadOK2xml cI chd) end) |
|
391 handle _ => sysERROR2xml cI "error in kernel"; |
|
392 |
|
393 (*.at the activeFormula set the Model, the Guard and the Specification |
|
394 to empty and return a CalcHead; |
|
395 the 'origin' remains (for reconstructing all that).*) |
|
396 fun resetCalcHead (cI:calcID) = |
|
397 (let val (ptp,_) = get_calc cI |
|
398 val ptp = reset_calchead ptp |
|
399 in (upd_calc cI (ptp, []); |
|
400 modifycalcheadOK2xml cI (get_ocalhd ptp)) end) |
|
401 handle _ => sysERROR2xml cI "error in kernel"; |
|
402 |
|
403 (*.at the activeFormula insert all the Descriptions in the Model |
|
404 (_not_ in the Guard) and return a CalcHead; |
|
405 the Descriptions are for user-guidance; the rest of the items |
|
406 are left empty for user-input; |
|
407 includes a resetCalcHead for the Model and the Guard.*) |
|
408 fun modelProblem (cI:calcID) = |
|
409 (let val (ptp, _) = get_calc cI |
|
410 val ptp = reset_calchead ptp |
|
411 val (_, _, ptp) = nxt_specif Model_Problem ptp |
|
412 in (upd_calc cI (ptp, []); |
|
413 modifycalcheadOK2xml cI (get_ocalhd ptp)) end) |
|
414 handle _ => sysERROR2xml cI "error in kernel"; |
|
415 |
|
416 |
|
417 (*.set the context determined on a knowledgebrowser to the current calc.*) |
|
418 fun setContext (cI:calcID) (ip as (_,p_):pos') (guh:guh) = |
|
419 (case (implode o (take_fromto 1 4) o explode) guh of |
|
420 "thy_" => |
|
421 (* val (cI, ip as (_,p_), guh) = (1, p, "thy_isac_Test-rls-Test_simplify"); |
|
422 *) |
|
423 if member op = [Pbl,Met] p_ |
|
424 then message2xml cI "thy-context not to calchead" |
|
425 else if ip = ([],Res) then message2xml cI "no thy-context at result" |
|
426 else if no_thycontext guh then message2xml cI ("no thy-context for '"^ |
|
427 guh ^ "'") |
|
428 else let val (ptp as (pt,pold),_) = get_calc cI |
|
429 val is = get_istate pt ip |
|
430 val subs = subs_from is "dummy" guh |
|
431 val tac = guh2rewtac guh subs |
|
432 in case locatetac tac (pt, ip) of (*='fun setNextTactic'+step*) |
|
433 ("ok", (tacis, c, ptp as (_,p))) => |
|
434 (* val (str, (tacis, c, ptp as (_,p))) = locatetac tac (pt, ip); |
|
435 *) |
|
436 (upd_calc cI ((pt,p), []); |
|
437 autocalculateOK2xml cI pold (if null c then pold |
|
438 else last_elem c) p) |
|
439 | ("unsafe-ok", (tacis, c, ptp as (_,p))) => |
|
440 (upd_calc cI ((pt,p), []); |
|
441 autocalculateOK2xml cI pold (if null c then pold |
|
442 else last_elem c) p) |
|
443 | ("end-of-calculation",_) => |
|
444 message2xml cI "end-of-calculation" |
|
445 | ("failure",_) => sysERROR2xml cI "failure" |
|
446 | ("not-applicable",_) => (*the rule comes from anywhere..*) |
|
447 (case applicable_in ip pt tac of |
|
448 |
|
449 Notappl e => message2xml cI ("'" ^ tac2str tac ^ |
|
450 "' not-applicable") |
|
451 | Appl m => |
|
452 let val (p,c,_,pt) = generate1 (assoc_thy"Isac.thy") |
|
453 m Uistate ip pt |
|
454 in upd_calc cI ((pt,p),[]); |
|
455 autocalculateOK2xml cI pold (if null c then pold |
|
456 else last_elem c) p |
|
457 end) |
|
458 end |
|
459 (* val (cI, ip as (_,p_), guh) = (1, pos, guh); |
|
460 *) |
|
461 | "pbl_" => |
|
462 let val pI = guh2kestoreID guh |
|
463 val ((pt, _), _) = get_calc cI |
|
464 (*val ip as (_, p_) = get_pos cI 1*) |
|
465 in if member op = [Pbl, Met] p_ |
|
466 then let val (pt, chd) = set_problem pI (pt, ip) |
|
467 in (upd_calc cI ((pt, ip), []); |
|
468 modifycalcheadOK2xml cI chd) end |
|
469 else sysERROR2xml cI "setContext for pbl requires ActiveFormula \ |
|
470 \on CalcHead" |
|
471 end |
|
472 (* val (cI, ip as (_,p_), guh) = (1, pos, "met_eq_lin"); |
|
473 *) |
|
474 | "met_" => |
|
475 let val mI = guh2kestoreID guh |
|
476 val ((pt, _), _) = get_calc cI |
|
477 in if member op = [Pbl, Met] p_ |
|
478 then let val (pt, chd) = set_method mI (pt, ip) |
|
479 in (upd_calc cI ((pt, ip), []); |
|
480 modifycalcheadOK2xml cI chd) end |
|
481 else sysERROR2xml cI "setContext for met requires ActiveFormula \ |
|
482 \on CalcHead" |
|
483 end) |
|
484 handle _ => sysERROR2xml cI "error in kernel"; |
|
485 |
|
486 |
|
487 (*.specify the Method at the activeFormula and return a CalcHead |
|
488 containing the Guard. |
|
489 WN0512 impl.incomplete, see 'nxt_specif (Specify_Method '.*) |
|
490 fun setMethod (cI:calcID) (mI:metID) = |
|
491 (* val (cI, mI) = (1, ["Test","solve_linear"]); |
|
492 *) |
|
493 (let val ((pt, _), _) = get_calc cI |
|
494 val ip as (_, p_) = get_pos cI 1 |
|
495 in if member op = [Pbl,Met] p_ |
|
496 then let val (pt, chd) = set_method mI (pt, ip) |
|
497 in (upd_calc cI ((pt, ip), []); |
|
498 modifycalcheadOK2xml cI chd) end |
|
499 else sysERROR2xml cI "setMethod requires ActiveFormula on CalcHead" |
|
500 end) |
|
501 handle _ => sysERROR2xml cI "error in kernel"; |
|
502 |
|
503 (*.specify the Problem at the activeFormula and return a CalcHead |
|
504 containing the Model; special case of checkContext; |
|
505 WN0512 impl.incomplete, see 'nxt_specif (Specify_Problem '.*) |
|
506 fun setProblem (cI:calcID) (pI:pblID) = |
|
507 (let val ((pt, _), _) = get_calc cI |
|
508 val ip as (_, p_) = get_pos cI 1 |
|
509 in if member op = [Pbl,Met] p_ |
|
510 then let val (pt, chd) = set_problem pI (pt, ip) |
|
511 in (upd_calc cI ((pt, ip), []); |
|
512 modifycalcheadOK2xml cI chd) end |
|
513 else sysERROR2xml cI "setProblem requires ActiveFormula on CalcHead" |
|
514 end) |
|
515 handle _ => sysERROR2xml cI "error in kernel"; |
|
516 |
|
517 (*.specify the Theory at the activeFormula and return a CalcHead; |
|
518 special case of checkContext; |
|
519 WN0512 impl.incomplete, see 'nxt_specif (Specify_Method '.*) |
|
520 fun setTheory (cI:calcID) (tI:thyID) = |
|
521 (let val ((pt, _), _) = get_calc cI |
|
522 val ip as (_, p_) = get_pos cI 1 |
|
523 in if member op = [Pbl,Met] p_ |
|
524 then let val (pt, chd) = set_theory tI (pt, ip) |
|
525 in (upd_calc cI ((pt, ip), []); |
|
526 modifycalcheadOK2xml cI chd) end |
|
527 else sysERROR2xml cI "setProblem requires ActiveFormula on CalcHead" |
|
528 end) |
|
529 handle _ => sysERROR2xml cI "error in kernel"; |
|
530 |
|
531 |
|
532 (**. without update of CalcTree .**) |
|
533 |
|
534 (*.match the model of a problem at pos p |
|
535 with the model-pattern of the problem with pblID*) |
|
536 (*fun tryMatchProblem cI pblID = |
|
537 (let val ((pt,_),_) = get_calc cI |
|
538 val p = get_pos cI 1 |
|
539 val chd = trymatch pblID pt p |
|
540 in trymatchOK2xml cI chd end) |
|
541 handle _ => sysERROR2xml cI "error in kernel";*) |
|
542 |
|
543 (*.refinement for the parent-problem of the position.*) |
|
544 (* val (cI, (p,p_), guh) = (1, ([1],Res), "pbl_equ_univ"); |
|
545 *) |
|
546 fun refineProblem cI ((p,p_) : pos') (guh : guh) = |
|
547 (let val pblID = guh2kestoreID guh |
|
548 val ((pt,_),_) = get_calc cI |
|
549 val pp = par_pblobj pt p |
|
550 val chd = tryrefine pblID pt (pp, p_) |
|
551 in matchpbl2xml cI chd end) |
|
552 handle _ => sysERROR2xml cI "error in kernel"; |
|
553 |
|
554 (* val (cI, ifo) = (1, "-2 * 1 + (1 + x) = 0"); |
|
555 val (cI, ifo) = (1, "x = 2"); |
|
556 val (cI, ifo) = (1, "[x = 3 + -2*1]"); |
|
557 val (cI, ifo) = (1, "-1 + x = 0"); |
|
558 val (cI, ifo) = (1, "x - 4711 = 0"); |
|
559 val (cI, ifo) = (1, "2+ -1 + x = 2"); |
|
560 val (cI, ifo) = (1, " x - "); |
|
561 val (cI, ifo) = (1, "(-3 * x + 4 * y + -1 * x * y) / (x * y)"); |
|
562 val (cI, ifo) = (1, "(4 * y + -3 * x) / (x * y) + -1"); |
|
563 *) |
|
564 fun appendFormula cI (ifo:cterm') = |
|
565 (let val cs = get_calc cI |
|
566 val pos as (_,p_) = get_pos cI 1 |
|
567 in case step pos cs of |
|
568 (* val (str, cs') = step pos cs; |
|
569 *) |
|
570 ("ok", cs') => |
|
571 (case inform cs' (encode ifo) of |
|
572 (* val (str, (_, c, ptp as (_,p))) = inform cs' (encode ifo); |
|
573 *) |
|
574 ("ok", (_(*use in DG !!!*), c, ptp as (_,p))) => |
|
575 (upd_calc cI (ptp, []); upd_ipos cI 1 p; |
|
576 appendformulaOK2xml cI pos (if null c then pos |
|
577 else last_elem c) p) |
|
578 | ("same-formula", (_, c, ptp as (_,p))) => |
|
579 (upd_calc cI (ptp, []); upd_ipos cI 1 p; |
|
580 appendformulaOK2xml cI pos (if null c then pos |
|
581 else last_elem c) p) |
|
582 | (msg, _) => appendformulaERROR2xml cI msg) |
|
583 | (msg, cs') => appendformulaERROR2xml cI msg |
|
584 end) |
|
585 handle _ => sysERROR2xml cI "error in kernel"; |
|
586 |
|
587 |
|
588 |
|
589 (*.replace a formula with_in_ a calculation; |
|
590 this situation applies for initial CAS-commands, too.*) |
|
591 (* val (cI, ifo) = (2, "-1 + x = 0"); |
|
592 val (cI, ifo) = (1, "-1 + x = 0"); |
|
593 val (cI, ifo) = (1, "x - 1 = 0"); |
|
594 val (cI, ifo) = (1, "x = 1"); |
|
595 val (cI, ifo) = (1, "solve(x+1=2,x)"); |
|
596 val (cI, ifo) = (1, "Simplify (2*a + 3*a)"); |
|
597 val (cI, ifo) = (1, "Diff (x^2 + x + 1, x)"); |
|
598 *) |
|
599 fun replaceFormula cI (ifo:cterm') = |
|
600 (let val ((pt, _), _) = get_calc cI |
|
601 val p = get_pos cI 1 |
|
602 in case inform (([], [], (pt, p)): calcstate') (encode ifo) of |
|
603 ("ok", (_(*tacs used for DG ?*), c, ptp' as (pt',p'))) => |
|
604 (* val (str, (_,c, ptp' as (pt',p')))= inform ([], [], (pt, p)) (encode ifo); |
|
605 *) |
|
606 let val unc = if null (fst p) then p else move_up [] pt p |
|
607 val _ = upd_calc cI (ptp', []) |
|
608 val _ = upd_ipos cI 1 p' |
|
609 in replaceformulaOK2xml cI unc |
|
610 (if null c then unc |
|
611 else last_elem c) p'(*' NEW*) end |
|
612 | ("same-formula", _) => |
|
613 (*TODO.WN0501 MESSAGE !*) |
|
614 replaceformulaERROR2xml cI "formula not changed" |
|
615 | (msg, _) => replaceformulaERROR2xml cI msg |
|
616 end) |
|
617 handle _ => sysERROR2xml cI "error in kernel"; |
|
618 |
|
619 |
|
620 |
|
621 (***. CalcIterator |
|
622 moveActive*: set the pos' of the active formula stored with the calctree |
|
623 could take pos' as argument for consistency checks |
|
624 move*: compute the new iterator from the old one on the fly |
|
625 |
|
626 .***) |
|
627 |
|
628 fun moveActiveRoot cI = |
|
629 (let val _ = upd_ipos cI 1 ([],Pbl) |
|
630 in iteratorOK2xml cI ([],Pbl) end) |
|
631 handle e => sysERROR2xml cI "error in kernel"; |
|
632 fun moveRoot cI = |
|
633 (iteratorOK2xml cI ([],Pbl)) |
|
634 handle e => sysERROR2xml cI ""; |
|
635 fun moveActiveRootTEST cI = |
|
636 (let val _ = upd_ipos cI 1 ([],Pbl) |
|
637 in (*iteratorOK2xml cI ([],Pbl)*)() end) |
|
638 handle e => sysERROR2xml cI "error in kernel"; |
|
639 |
|
640 (* val (cI, uI) = (1,1); |
|
641 val (cI, uI) = (1,2); |
|
642 *) |
|
643 fun moveActiveDown cI = |
|
644 ((let val ((pt,_),_) = get_calc cI |
|
645 (* val (P, (Nd (_, ns)), (p::(ps as (_::_)), p_)) =([]:pos, pt, get_pos cI uI); |
|
646 val (P, (Nd (c, ns)), ([p], p_)) =([]:pos, pt, get_pos cI uI); |
|
647 |
|
648 print_depth 7;pt |
|
649 *) |
|
650 val ip' = move_dn [] pt (get_pos cI 1) |
|
651 val _ = upd_ipos cI 1 ip' |
|
652 in iteratorOK2xml cI ip' end) |
|
653 handle (PTREE e) => iteratorERROR2xml cI) |
|
654 handle _ => sysERROR2xml cI "error in kernel"; |
|
655 fun moveDown cI (p:pos') = |
|
656 ((let val ((pt,_),_) = get_calc cI |
|
657 (* val (P, (Nd (_, ns)), (p::(ps as (_::_)), p_)) =([]:pos, pt, get_pos cI uI); |
|
658 val (P, (Nd (c, ns)), ([p], p_)) =([]:pos, pt, get_pos cI uI); |
|
659 |
|
660 print_depth 7;pt |
|
661 *) |
|
662 val ip' = move_dn [] pt p |
|
663 in iteratorOK2xml cI ip' end) |
|
664 handle (PTREE e) => iteratorERROR2xml cI) |
|
665 handle _ => sysERROR2xml cI "error in kernel"; |
|
666 fun moveActiveDownTEST cI = |
|
667 let val ((pt,_),_) = get_calc cI |
|
668 val ip = get_pos cI 1 |
|
669 val ip' = (move_dn [] pt ip) |
|
670 handle _ => ip |
|
671 val _ = upd_ipos cI 1 ip' |
|
672 in (*iteratorOK2xml cI uI*)() end; |
|
673 |
|
674 fun moveActiveLevelDown cI = |
|
675 ((let val ((pt,_),_) = get_calc cI |
|
676 val ip' = movelevel_dn [] pt (get_pos cI 1) |
|
677 val _ = upd_ipos cI 1 ip' |
|
678 in iteratorOK2xml cI ip' end) |
|
679 handle (PTREE e) => iteratorERROR2xml cI) |
|
680 handle _ => sysERROR2xml cI "error in kernel"; |
|
681 fun moveLevelDown cI (p:pos') = |
|
682 ((let val ((pt,_),_) = get_calc cI |
|
683 val ip' = movelevel_dn [] pt p |
|
684 in iteratorOK2xml cI ip' end) |
|
685 handle (PTREE e) => iteratorERROR2xml cI) |
|
686 handle _ => sysERROR2xml cI "error in kernel"; |
|
687 |
|
688 fun moveActiveUp cI = |
|
689 ((let val ((pt,_),_) = get_calc cI |
|
690 val ip' = move_up [] pt (get_pos cI 1) |
|
691 val _ = upd_ipos cI 1 ip' |
|
692 in iteratorOK2xml cI ip' end) |
|
693 handle PTREE e => iteratorERROR2xml cI) |
|
694 handle _ => sysERROR2xml cI "error in kernel"; |
|
695 fun moveUp cI (p:pos') = |
|
696 ((let val ((pt,_),_) = get_calc cI |
|
697 val ip' = move_up [] pt p |
|
698 in iteratorOK2xml cI ip' end) |
|
699 handle PTREE e => iteratorERROR2xml cI) |
|
700 handle _ => sysERROR2xml cI "error in kernel"; |
|
701 |
|
702 fun moveActiveLevelUp cI = |
|
703 ((let val ((pt,_),_) = get_calc cI |
|
704 val ip' = movelevel_up [] pt (get_pos cI 1) |
|
705 val _ = upd_ipos cI 1 ip' |
|
706 in iteratorOK2xml cI ip' end) |
|
707 handle PTREE e => iteratorERROR2xml cI) |
|
708 handle _ => sysERROR2xml cI "error in kernel"; |
|
709 fun moveLevelUp cI (p:pos') = |
|
710 ((let val ((pt,_),_) = get_calc cI |
|
711 val ip' = movelevel_up [] pt p |
|
712 in iteratorOK2xml cI ip' end) |
|
713 handle PTREE e => iteratorERROR2xml cI) |
|
714 handle _ => sysERROR2xml cI "error in kernel"; |
|
715 |
|
716 fun moveActiveCalcHead cI = |
|
717 ((let val ((pt,_),_) = get_calc cI |
|
718 val ip' = movecalchd_up pt (get_pos cI 1) |
|
719 val _ = upd_ipos cI 1 ip' |
|
720 in iteratorOK2xml cI ip' end) |
|
721 handle PTREE e => iteratorERROR2xml cI) |
|
722 handle _ => sysERROR2xml cI "error in kernel"; |
|
723 fun moveCalcHead cI (p:pos') = |
|
724 ((let val ((pt,_),_) = get_calc cI |
|
725 val ip' = movecalchd_up pt p |
|
726 in iteratorOK2xml cI ip' end) |
|
727 handle PTREE e => iteratorERROR2xml cI) |
|
728 handle _ => sysERROR2xml cI "error in kernel"; |
|
729 |
|
730 |
|
731 (*.initContext Thy_ is conceptually impossible at [Pbl,Met] |
|
732 and at positions with Check_Postcond and End_Trans; |
|
733 at possible pos's there can be NO rewrite (returned as a context, too).*) |
|
734 (* val (cI, Thy_, (pos as (p,p_):pos')) = (1, Thy_, ([1], Frm)); |
|
735 val (cI, Thy_, (pos as (p,p_):pos')) = (1, Thy_, ([], Res)); |
|
736 val (cI, Thy_, (pos as (p,p_):pos')) = (1, Thy_, ([2], Res)); |
|
737 val (cI, Thy_, (pos as (p,p_):pos')) = (1, Thy_, ([1,1], Frm)); |
|
738 *) |
|
739 fun initContext (cI:calcID) Thy_ (pos as (p,p_):pos') = |
|
740 ((if member op = [Pbl,Met] p_ |
|
741 then message2xml cI "thy-context not to calchead" |
|
742 else if pos = ([],Res) then message2xml cI "no thy-context at result" |
|
743 else let val cs as (ptp as (pt,_),_) = get_calc cI |
|
744 in if exist_lev_on' pt pos |
|
745 then let val pos' = lev_on' pt pos |
|
746 val tac = get_tac_checked pt pos' |
|
747 in if is_rewtac tac |
|
748 then contextthyOK2xml cI (context_thy (pt,pos) tac) |
|
749 else message2xml cI ("no thy-context at tac '" ^ |
|
750 tac2str tac ^ "'") |
|
751 end |
|
752 else if is_curr_endof_calc pt pos |
|
753 then case step pos cs of |
|
754 (* val (str, (tacis, _, (pt,_))) = step pos cs; |
|
755 val ("ok", (tacis, _, (pt,_))) = step pos cs; |
|
756 *) |
|
757 ("ok", (tacis, _, (pt,_))) => |
|
758 let val tac = fst3 (last_elem tacis) |
|
759 in if is_rewtac tac |
|
760 then contextthyOK2xml |
|
761 cI (context_thy ptp tac) |
|
762 else message2xml cI ("no thy-context at tac '" ^ |
|
763 tac2str tac ^ "'") |
|
764 end |
|
765 | (msg, _) => message2xml cI msg |
|
766 else message2xml cI "no thy-context at this position" |
|
767 end) |
|
768 handle _ => sysERROR2xml cI "error in kernel") |
|
769 |
|
770 (* val (cI, Pbl_, pos as (p,p_)) = (1, Pbl_, ([],Pbl)); |
|
771 *) |
|
772 | initContext cI Pbl_ (pos as (p,p_):pos') = |
|
773 ((let val ((pt,_),_) = get_calc cI |
|
774 val pp = par_pblobj pt p |
|
775 val chd = initcontext_pbl pt (pp,p_) |
|
776 in matchpbl2xml cI chd end) |
|
777 handle _ => sysERROR2xml cI "error in kernel") |
|
778 |
|
779 | initContext cI Met_ (pos as (p,p_):pos') = |
|
780 ((let val ((pt,_),_) = get_calc cI |
|
781 val pp = par_pblobj pt p |
|
782 val chd = initcontext_met pt (pp,p_) |
|
783 in matchmet2xml cI chd end) |
|
784 handle _ => sysERROR2xml cI "error in kernel"); |
|
785 |
|
786 |
|
787 |
|
788 (*.match a theorem, a ruleset (etc., selected in the knowledge-browser) |
|
789 with the formula in the focus on the worksheet; |
|
790 string contains the thy, thus it is unique as thmID, rlsID for this thy; |
|
791 take the substitution from the istate of the formula.*) |
|
792 (* use"../smltest/IsacKnowledge/poly.sml"; |
|
793 val (cI, pos as (p,p_), guh) = (1, ([1,1,1], Frm), |
|
794 "thy_Poly-thm-real_diff_minus"); |
|
795 val (cI, pos as (p,p_), guh) = (1, ([1,1], Frm), "norm_Poly"); |
|
796 val (cI, pos as (p,p_), guh) = |
|
797 (1, ([1], Res), "thy_isac_Test-rls-Test_simplify"); |
|
798 *) |
|
799 fun checkContext (cI:calcID) (pos:pos' as (p,p_)) (guh:guh) = |
|
800 (case (implode o (take_fromto 1 4) o explode) guh of |
|
801 "thy_" => |
|
802 if member op = [Pbl,Met] p_ |
|
803 then message2xml cI "thy-context not to calchead" |
|
804 else if pos = ([],Res) then message2xml cI "no thy-context at result" |
|
805 else if no_thycontext guh then message2xml cI ("no thy-context for '"^ |
|
806 guh ^ "'") |
|
807 else let val (ptp as (pt,_),_) = get_calc cI |
|
808 val is = get_istate pt pos |
|
809 val subs = subs_from is "dummy" guh |
|
810 val tac = guh2rewtac guh subs |
|
811 in contextthyOK2xml cI (context_thy (pt, pos) tac) end |
|
812 |
|
813 (*.match the model of a problem at pos p |
|
814 with the model-pattern of the problem with pblID.*) |
|
815 (* val (cI, pos:pos' as (p,p_), guh) = |
|
816 (1, p, kestoreID2guh Pbl_ ["univariate","equation"]); |
|
817 val (cI, pos:pos' as (p,p_), guh) = |
|
818 (1, ([],Pbl), kestoreID2guh Pbl_ ["univariate","equation"]); |
|
819 val (cI, pos:pos' as (p,p_), guh) = |
|
820 (1, ([],Pbl), "pbl_equ_univ"); |
|
821 *) |
|
822 | "pbl_" => |
|
823 let val ((pt,_),_) = get_calc cI |
|
824 val pp = par_pblobj pt p |
|
825 val keID = guh2kestoreID guh |
|
826 val chd = context_pbl keID pt pp |
|
827 in matchpbl2xml cI chd end |
|
828 (* val (cI, pos:pos' as (p,p_), guh) = |
|
829 (1, ([],Pbl), kestoreID2guh Met_ ["LinEq", "solve_lineq_equation"]); |
|
830 *) |
|
831 | "met_" => |
|
832 let val ((pt,_),_) = get_calc cI |
|
833 val pp = par_pblobj pt p |
|
834 val keID = guh2kestoreID guh |
|
835 val chd = context_met keID pt pp |
|
836 in matchmet2xml cI chd end) |
|
837 handle _ => sysERROR2xml cI "error in kernel"; |
|
838 |
|
839 |
|
840 (*------------------------------------------------------------------*) |
|
841 end |
|
842 open interface; |
|
843 (*------------------------------------------------------------------*) |
|