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
6 use"Frontend/interface.sml";
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
58 (*------------------------------------------------------------------*)
59 structure interface : INTERFACE =
61 (*------------------------------------------------------------------*)
63 (*.encode "Isabelle"-strings as seen by the user to the
64 format accepted by Isabelle.
65 encode "^" ---> "^^^"; see Knowledge/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') =
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;
85 (** add and delete users **)
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);*)
99 (*.create a calc-tree; for calls from java: thus ^^^ decoded to ^;
100 compare "fun CalcTreeTEST" which does NOT decode.*)
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"]))];
116 (let val cs = nxt_specify_init_calc (encode_fmz (fmz, sp))
117 (*FIXME.WN.8.03: error-handling missing*)
119 in calctreeOK2xml cI end)
120 handle _ => sysERROR2xml 0 "error in kernel";
122 fun DEconstrCalcTree (cI:calcID) =
123 deconstructcalctreeOK2xml (del_calc cI);
126 fun getActiveFormula (cI:calcID) = iteratorOK2xml cI (get_pos cI 1);
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;
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");
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);
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"
163 (*. apply a tactic at a position and update the calc-tree if applicable .*)
164 (*WN080226 java-code is missing, errors smltest/Knowledge/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)));
168 fun applyTactic (cI:calcID) ip tac =
169 let val ((pt, _), _) = get_calc cI
171 in case locatetac tac (pt, ip) of
172 (* val ("ok", (tacis, c, (pt',p'))) = locatetac tac (pt, ip);
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')
188 | (str,_) => autocalculateERROR2xml cI "failure"
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";
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);
223 (let val pold = get_pos cI 1
224 val x = autocalc [] pold (get_calc cI) auto
227 (* val (str, c, ptp as (_,p)) = x;
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
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
237 | (str, _, _) => autocalculateERROR2xml cI str
239 handle _ => sysERROR2xml cI "error in kernel";
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"]],
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));
261 fun getTactic cI (p:pos') =
262 (let val ((pt,_),_) = get_calc cI
263 val (form, tac, asms) = pt_extract (pt, p)
265 (* val SOME ta = tac;
267 SOME ta => gettacticOK2xml cI ta
268 | NONE => gettacticERROR2xml cI ("no tactic at position "^pos'2str p)
270 handle _ => sysERROR2xml cI "syserror in getTactic";
272 (*. see ICalcIterator#fetchApplicableTactics
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
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
292 handle _ => sysERROR2xml cI "error in kernel";
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";
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";
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);
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";
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);
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")
334 | getFormulaeFromTo cI (from as ([],Pbl):pos') (to as ([],Met):pos')_ false =
335 getFormulaeFromTo cI ([],Pbl) ([],Pbl) (~00000) false
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);
342 (if from = to then sysERROR2xml cI "getFormulaeFromTo: From = To"
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")
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";
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));
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;
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
384 handle _ => sysERROR2xml cI "error in kernel";
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";
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";
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";
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
421 (* val (cI, ip as (_,p_), guh) = (1, p, "thy_isac_Test-rls-Test_simplify");
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 '"^
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);
436 (upd_calc cI ((pt,p), []);
437 autocalculateOK2xml cI pold (if null c then pold
439 | ("unsafe-ok", (tacis, c, ptp as (_,p))) =>
440 (upd_calc cI ((pt,p), []);
441 autocalculateOK2xml cI pold (if null c then pold
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
449 Notappl e => message2xml cI ("'" ^ tac2str tac ^
452 let val (p,c,_,pt) = generate1 (assoc_thy"Isac.thy")
454 in upd_calc cI ((pt,p),[]);
455 autocalculateOK2xml cI pold (if null c then pold
459 (* val (cI, ip as (_,p_), guh) = (1, pos, guh);
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 \
472 (* val (cI, ip as (_,p_), guh) = (1, pos, "met_eq_lin");
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 \
484 handle _ => sysERROR2xml cI "error in kernel";
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"]);
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"
501 handle _ => sysERROR2xml cI "error in kernel";
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"
515 handle _ => sysERROR2xml cI "error in kernel";
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"
529 handle _ => sysERROR2xml cI "error in kernel";
532 (**. without update of CalcTree .**)
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
539 val chd = trymatch pblID pt p
540 in trymatchOK2xml cI chd end)
541 handle _ => sysERROR2xml cI "error in kernel";*)
543 (*.refinement for the parent-problem of the position.*)
544 (* val (cI, (p,p_), guh) = (1, ([1],Res), "pbl_equ_univ");
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";
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");
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;
571 (case inform cs' (encode ifo) of
572 (* val (str, (_, c, ptp as (_,p))) = inform cs' (encode ifo);
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
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
582 | (msg, _) => appendformulaERROR2xml cI msg)
583 | (msg, cs') => appendformulaERROR2xml cI msg
585 handle _ => sysERROR2xml cI "error in kernel";
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)");
599 fun replaceFormula cI (ifo:cterm') =
600 (let val ((pt, _), _) = get_calc cI
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);
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
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
617 handle _ => sysERROR2xml cI "error in kernel";
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
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";
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";
640 (* val (cI, uI) = (1,1);
641 val (cI, uI) = (1,2);
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);
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);
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)
671 val _ = upd_ipos cI 1 ip'
672 in (*iteratorOK2xml cI uI*)() end;
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";
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";
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";
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";
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));
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'
748 then contextthyOK2xml cI (context_thy (pt,pos) tac)
749 else message2xml cI ("no thy-context at tac '" ^
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;
757 ("ok", (tacis, _, (pt,_))) =>
758 let val tac = fst3 (last_elem tacis)
760 then contextthyOK2xml
761 cI (context_thy ptp tac)
762 else message2xml cI ("no thy-context at tac '" ^
765 | (msg, _) => message2xml cI msg
766 else message2xml cI "no thy-context at this position"
768 handle _ => sysERROR2xml cI "error in kernel")
770 (* val (cI, Pbl_, pos as (p,p_)) = (1, Pbl_, ([],Pbl));
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")
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");
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/Knowledge/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");
799 fun checkContext (cI:calcID) (pos:pos' as (p,p_)) (guh:guh) =
800 (case (implode o (take_fromto 1 4) o explode) guh of
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 '"^
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
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");
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"]);
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";
840 (*------------------------------------------------------------------*)
843 (*------------------------------------------------------------------*)