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