1 (* the interface between the isac-kernel and the java-frontend;
2 the isac-kernel holds calc-trees; stdout in XML-format.
3 This is the only file which does not adhere to Isabelle coding standards,
4 rather the function names are according to the respective Java methods.
5 authors: Walther Neuper 2002
6 (c) due to copyright terms
8 use"Frontend/interface.sml";
14 val CalcTree : fmz list -> unit
15 val DEconstrCalcTree : calcID -> unit
16 val Iterator : calcID -> unit
17 val IteratorTEST : calcID -> iterID
18 val appendFormula : calcID -> cterm' -> unit (*future*)
19 val autoCalculate : calcID -> auto -> unit (*future*)
20 val checkContext : calcID -> pos' -> guh -> unit
21 val fetchApplicableTactics : calcID -> int -> pos' -> unit
22 val fetchProposedTactic : calcID -> unit
23 val applyTactic : calcID -> pos' -> tac -> unit
24 val getAccumulatedAsms : calcID -> pos' -> unit
25 val getActiveFormula : calcID -> unit
26 val getAssumptions : calcID -> pos' -> unit
27 val initContext : calcID -> ketype -> pos' -> unit
28 val getFormulaeFromTo : calcID -> pos' -> pos' -> int -> bool -> unit
29 val getTactic : calcID -> pos' -> unit
30 val interSteps : calcID -> pos' -> unit
31 val modifyCalcHead : calcID -> icalhd -> unit
32 val moveActiveCalcHead : calcID -> unit
33 val moveActiveDown : calcID -> unit
34 val moveActiveDownTEST : calcID -> unit
35 val moveActiveFormula : calcID -> pos' -> unit
36 val moveActiveLevelDown : calcID -> unit
37 val moveActiveLevelUp : calcID -> unit
38 val moveActiveRoot : calcID -> unit
39 val moveActiveRootTEST : calcID -> unit
40 val moveActiveUp : calcID -> unit
41 val moveCalcHead : calcID -> pos' -> unit
42 val moveDown : calcID -> pos' -> unit
43 val moveLevelDown : calcID -> pos' -> unit
44 val moveLevelUp : calcID -> pos' -> unit
45 val moveRoot : calcID -> unit
46 val moveUp : calcID -> pos' -> unit
47 val refFormula : calcID -> pos' -> unit
48 val replaceFormula : calcID -> cterm' -> unit
49 val resetCalcHead : calcID -> unit
50 val modelProblem : calcID -> unit
51 val refineProblem : calcID -> pos' -> guh -> unit
52 val setContext : calcID -> pos' -> guh -> unit
53 val setMethod : calcID -> metID -> unit
54 val setNextTactic : calcID -> tac -> unit
55 val setProblem : calcID -> pblID -> unit
56 val setTheory : calcID -> thyID -> unit
57 val findFillpatterns : calcID -> errpatID -> unit
58 val requestFillformula : calcID -> errpatID * fillpatID -> unit
59 val inputFillFormula: calcID -> string -> unit
60 (*------------ for tests*)
61 val encode: cterm' -> cterm'
62 val encode_fmz: fmz -> fmz
66 (*------------------------------------------------------------------*)
67 structure interface : INTERFACE =
69 (*------------------------------------------------------------------*)
71 (* encode "Isabelle"-strings as seen by the user to the
72 format accepted by Isabelle.
73 encode "^" ---> "^^^"; see Knowledge/Atools.thy;
74 called for each cterm', icalhd, fmz in this interface;
75 + see "fun decode" in xmlsrc/mathml.sml *)
76 fun encode (str : cterm') =
78 | enc ("^" :: cs) = "^" :: "^" :: "^" :: (enc cs)
79 | enc (c :: cs) = c :: (enc cs)
80 in (implode o enc o Symbol.explode) str:cterm' end;
81 fun encode_imodel (imodel:imodel) =
82 let fun enc (Given ifos) = Given (map encode ifos)
83 | enc (Find ifos) = Find (map encode ifos)
84 | enc (Relate ifos) = Relate (map encode ifos)
85 in map enc imodel:imodel end;
86 fun encode_icalhd ((pos', headl, imodel, pos_, spec):icalhd) =
87 (pos', encode headl, encode_imodel imodel, pos_, spec):icalhd;
88 fun encode_fmz ((ifos, spec) : fmz) = (map encode ifos, spec) : fmz;
93 (** add and delete users **)
95 (*.'Iterator 1' must exist with each CalcTree;
96 the only for updating the calc-tree
97 WN.0411: only 'Iterator 1' is stored,
98 all others are just calculated on the fly
99 TODO: adapt Iterator, add_user(= add_iterator!),etc. accordingly .*)
100 fun Iterator (cI:calcID) = (*returned ID unnecessary after WN.0411*)
101 (adduserOK2xml cI (add_user (cI:calcID)))
102 handle _ => sysERROR2xml cI "error in kernel";
103 fun IteratorTEST (cI:calcID) = add_user (cI:calcID);
104 (*fun DEconstructIterator (cI:calcID) (uI:iterID) =
105 deluserOK2xml (del_user cI uI);*)
107 (*.create a calc-tree; for calls from java: thus ^^^ decoded to ^;
108 compare "fun CalcTreeTEST" which does NOT decode.*)
109 fun CalcTree [(fmz, sp) : fmz] (*for several variants lateron*) =
110 (let val cs = nxt_specify_init_calc (encode_fmz (fmz, sp))
111 (*FIXME.WN.8.03: error-handling missing*)
113 in calctreeOK2xml cI end)
114 handle _ => sysERROR2xml 0 "error in kernel";
116 fun DEconstrCalcTree (cI:calcID) =
117 deconstructcalctreeOK2xml (del_calc cI);
120 fun getActiveFormula (cI:calcID) = iteratorOK2xml cI (get_pos cI 1);
122 fun moveActiveFormula (cI:calcID) (p:pos') =
123 let val ((pt,_),_) = get_calc cI
124 in if existpt' p pt then (upd_ipos cI 1 p; iteratorOK2xml cI p)
125 else sysERROR2xml cI "frontend sends a non-existing pos" end;
127 (*. set the next tactic to be applied: dont't change the calc-tree,
128 but remember the envisaged changes for fun autoCalculate;
129 compare force NextTactic .*)
130 (* val (cI, tac) = (1, Add_Given "equality (x ^^^ 2 + 4 * x + 3 = 0)");
131 val (cI, tac) = (1, Specify_Theory "PolyEq");
132 val (cI, tac) = (1, Specify_Problem ["normalize","polynomial",
133 "univariate","equation"]);
134 val (cI, tac) = (1, Subproblem ("Poly",
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 =
143 val ((pt, _), _) = get_calc cI
144 val ip = get_pos cI 1
145 in case locatetac tac (pt, ip) of
146 (* val ("ok", (tacis, c, (_,p'))) = locatetac tac (pt, ip);
148 ("ok", (tacis, _, _)) =>
149 (upd_calc cI ((pt, ip), tacis); setnexttactic2xml cI "ok")
150 | ("unsafe-ok", (tacis, _, _)) =>
151 (upd_calc cI ((pt, ip), tacis); setnexttactic2xml cI "unsafe-ok")
152 | ("not-applicable",_) => setnexttactic2xml cI "not-applicable"
153 | ("end-of-calculation",_) =>
154 setnexttactic2xml cI "end-of-calculation"
155 | ("failure",_) => sysERROR2xml cI "failure"
158 (*. apply a tactic at a position and update the calc-tree if applicable .*)
159 (*WN080226 java-code is missing, errors smltest/Knowledge/polyminus.sml*)
160 fun applyTactic (cI:calcID) ip tac =
162 val ((pt, _), _) = get_calc cI
165 case locatetac tac (pt, ip) of
166 ("ok", (_, c, ptp as (_,p'))) =>
167 (upd_calc cI (ptp, []);
169 autocalculateOK2xml cI p (if null c then p' else last_elem c) p')
170 | ("unsafe-ok", (_, c, ptp as (_,p'))) =>
171 (upd_calc cI (ptp, []);
173 autocalculateOK2xml cI p (if null c then p' else last_elem c) p')
174 | ("end-of-calculation", (_, c, ptp as (_,p'))) =>
175 (upd_calc cI (ptp, []);
177 autocalculateOK2xml cI p (if null c then p' else last_elem c) p')
178 | (str,_) => autocalculateERROR2xml cI "failure"
181 fun fetchProposedTactic (cI:calcID) =
182 (case step (get_pos cI 1) (get_calc cI) of
183 ("ok", (tacis, _, _)) =>
184 let val _= upd_tacis cI tacis
185 val (tac,_,_) = last_elem tacis
186 in fetchproposedtacticOK2xml cI tac (fetchErrorpatterns tac) end
187 | ("helpless",_) => fetchproposedtacticERROR2xml cI "helpless"
188 | ("no-fmz-spec",_) => fetchproposedtacticERROR2xml cI "no-fmz-spec"
189 | ("end-of-calculation",_) =>
190 fetchproposedtacticERROR2xml cI "end-of-calculation")
191 handle _ => sysERROR2xml cI "error in kernel";
193 (*original see ~~/src/Tools/isac/Interpret/solve.sml:
194 datatype auto = FIXXXME040624: does NOT match interfaces/ITOCalc.java
195 Step of int (*1 do #int steps (may stop in model/specify)
196 IS VERY INEFFICIENT IN MODEL/SPECIY*)
197 | CompleteModel (*2 complete modeling
198 if model complete, finish specifying*)
199 | CompleteCalcHead (*3 complete model/specify in one go*)
200 | CompleteToSubpbl (*4 stop at the next begin of a subproblem,
201 if none, complete the actual (sub)problem*)
202 | CompleteSubpbl (*5 complete the actual (sub)problem (incl.ev.subproblems)*)
203 | CompleteCalc; (*6 complete the calculation as a whole*)*)
205 fun autoCalculate (cI:calcID) auto = (*Future.fork
207 val pold = get_pos cI 1
208 val x = autocalc [] pold (get_calc cI) auto
211 ("ok", c, ptp as (_,p)) =>
212 (upd_calc cI (ptp, []); upd_ipos cI 1 p;
213 autocalculateOK2xml cI pold (if null c then pold else last_elem c) p)
214 | ("end-of-calculation", c, ptp as (_,p)) =>
215 (upd_calc cI (ptp, []); upd_ipos cI 1 p;
216 autocalculateOK2xml cI pold (if null c then pold else last_elem c) p)
217 | (str, _, _) => autocalculateERROR2xml cI str
219 handle ERROR msg => sysERROR2xml cI ("error in kernel: " ^ msg)(* )) *);
222 (* val (cI:calcID, ichd as ((p,_),_,_,_,_):icalhd) =
223 (1, (([],Pbl), "not used here",
224 [Given ["fixedValues [r=Arbfix]"],
225 Find ["maximum A", "valuesFor [a,b]"(*new input*)],
226 Relate ["relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]"]], Pbl,
227 ("DiffApp", ["maximum_of","function"],
228 ["DiffApp","max_by_calculus"])));
229 val (cI:calcID, ichd as ((p,_),_,_,_,_):icalhd) =
230 (1, (([],Pbl),"solve (x+1=2, x)",
231 [Given ["equality (x+1=2)", "solveFor x"],
232 Find ["solutions L"]],
234 ("Test", ["linear","univariate","equation","test"],
235 ["Test","solve_linear"])));
236 val (cI:calcID, ichd as ((p,_),_,_,_,_):icalhd) =
237 (1, (([],Pbl),"solveTest (1+-1*2+x=0,x)", [], Pbl, ("", [], [])));
238 val (cI, p:pos')=(1, ([1],Frm));
239 val (cI, p:pos')=(1, ([1,2,1,3],Res));
241 fun getTactic cI (p:pos') =
242 (let val ((pt,_),_) = get_calc cI
243 val (form, tac, asms) = pt_extract (pt, p)
245 SOME ta => gettacticOK2xml cI ta
246 | NONE => gettacticERROR2xml cI ("no tactic at position "^pos'2str p)
248 handle _ => sysERROR2xml cI "syserror in getTactic";
250 (*. see ICalcIterator#fetchApplicableTactics
252 @see #TACTICS_CURRENT_THEORY
253 @see #TACTICS_CURRENT_METHOD ..the only impl.WN040307.*)
254 (*. fetch tactics to be applied to a particular step.*)
255 (* WN071231 kept this version for later parametrisation*)
256 (*.version 1: fetch _all_ tactics from script .*)
257 fun fetchApplicableTactics cI (scope:int) (p:pos') =
258 (let val ((pt, _), _) = get_calc cI
259 in (applicabletacticsOK cI (sel_rules pt p))
260 handle PTREE str => sysERROR2xml cI str
262 handle _ => sysERROR2xml cI "error in kernel";
263 (*WN120611 took version 1 again
264 version 2: fetch _applicable_ _elementary_ (ie. recursively
265 decompose rule-sets) Rewrite*, Calculate
266 fun fetchApplicableTactics cI (scope:int) (p:pos') =
267 (let val ((pt, _), _) = get_calc cI
268 in (applicabletacticsOK cI (sel_appl_atomic_tacs pt p))
269 handle PTREE str => sysERROR2xml cI str
271 handle _ => sysERROR2xml cI "error in kernel";
273 fun getAssumptions cI (p:pos') =
274 (let val ((pt,_),_) = get_calc cI
275 val (_, _, asms) = pt_extract (pt, p)
276 in getasmsOK2xml cI asms end)
277 handle _ => sysERROR2xml cI "syserror in getAssumptions";
279 (*WN0502 @see ME/ctree: type asms: illdesigned, thus no positions returned*)
280 fun getAccumulatedAsms cI (p:pos') =
281 (let val ((pt, _), _) = get_calc cI
282 val ass = get_assumptions_ pt p
283 in (*getaccuasmsOK2xml cI (get_assumptions_ pt p)*)
284 getasmsOK2xml cI ass end)
285 handle _ => sysERROR2xml cI "syserror in getAccumulatedAsms";
288 (*since moveActive* does NOT transfer pos java --> sml (only sml --> java)
289 refFormula might become involved in far-off errors !!!*)
290 fun refFormula cI (p:pos') = (*WN0501 rename to 'fun getElement' !*)
291 (* val (cI, uI) = (1,1);
293 (let val ((pt,_),_) = get_calc cI
294 val (form, tac, asms) = pt_extract (pt, p)
295 in refformulaOK2xml cI p form end)
296 handle _ => sysERROR2xml cI "error in kernel";
298 (*.get formulae 'from' 'to' w.r.t. ordering in Position#compareTo(Position p);
299 in case of CalcHeads only the headline is taken
300 (the pos' allows distinction between PrfObj and PblObj anyway);
301 'level' is adjusted such that an 'interval' of formulae is returned;
302 'from' 'to' are designed for use by iterators of calcChangedEvent;
303 thus 'from' is the last unchanged position.*)
304 fun getFormulaeFromTo cI (from as ([],Pbl):pos') (to as ([],Pbl):pos')_ false =
305 (*special case because 'from' is _before_ the first elements to be returned*)
306 (* val (cI, from, to, level) = (1, ([],Pbl), ([],Pbl), 1);
308 ((let val ((pt,_),_) = get_calc cI
309 val (ModSpec (_,_,headline,_,_,_),_,_) = pt_extract (pt, to)
310 in getintervalOK cI [(to, headline)] end)
311 handle _ => sysERROR2xml cI "error in kernel")
313 | getFormulaeFromTo cI (from as ([],Pbl):pos') (to as ([],Met):pos')_ false =
314 getFormulaeFromTo cI ([],Pbl) ([],Pbl) (~00000) false
316 | getFormulaeFromTo cI (from:pos') (to:pos') level false =
317 (* val (cI, from, to, level) = (1, unc, gen, 0);
318 val (cI, from, to, level) = (1, unc, gen, 1);
319 val (cI, from, to, level) = (1, ([],Pbl), ([],Met), 1);
321 (if from = to then sysERROR2xml cI "getFormulaeFromTo: From = To"
324 ([],Res) => sysERROR2xml cI "getFormulaeFromTo does: moveDown \
325 \from=([],Res) .. goes beyond result"
326 | _ => let val ((pt,_),_) = get_calc cI
327 val f = move_dn [] pt from
328 fun max (a,b) = if a < b then b else a
329 (*must reach margins ...*)
330 val lev = max (level, max (lev_of from, lev_of to))
331 in getintervalOK cI (get_interval f to lev pt) end)
332 handle _ => sysERROR2xml cI "error in getFormulaeFromTo")
334 | getFormulaeFromTo cI from to level true =
335 sysERROR2xml cI "getFormulaeFromTo impl.for formulae only,\
336 \i.e. last arg only impl. for false, _NOT_ true";
338 fun interSteps cI ip =
339 (let val ((pt,p), tacis) = get_calc cI
341 if (not o is_interpos) ip
342 then interStepsERROR cI ("only formulae with position (_,Res) " ^
343 "may have intermediate steps above them")
345 let val ip' = lev_pred' pt ip
346 in case detailstep pt ip of
347 ("detailrls", pt, lastpos) => (upd_calc cI ((pt, p), tacis);
348 interStepsOK cI ip' ip' lastpos)
349 | ("no-Rewrite_Set...", _, _) => sysERROR2xml cI "no Rewrite_Set..."
350 | (_, _, lastpos) => interStepsOK cI ip' ip' lastpos
353 handle _ => sysERROR2xml cI "error in kernel";
355 fun modifyCalcHead (cI:calcID) (ichd as ((p,_),_,_,_,_):icalhd) =
356 (let val ((pt,_),_) = get_calc cI
357 val (pt, chd as (_,p_,_,_,_,_)) = input_icalhd pt ichd
358 in (upd_calc cI ((pt, (p,p_)), []);
359 modifycalcheadOK2xml cI chd) end)
360 handle _ => sysERROR2xml cI "error in kernel";
362 (*.at the activeFormula set the Model, the Guard and the Specification
363 to empty and return a CalcHead;
364 the 'origin' remains (for reconstructing all that).*)
365 fun resetCalcHead (cI:calcID) =
366 (let val (ptp,_) = get_calc cI
367 val ptp = reset_calchead ptp
368 in (upd_calc cI (ptp, []);
369 modifycalcheadOK2xml cI (get_ocalhd ptp)) end)
370 handle _ => sysERROR2xml cI "error in kernel";
372 (*.at the activeFormula insert all the Descriptions in the Model
373 (_not_ in the Guard) and return a CalcHead;
374 the Descriptions are for user-guidance; the rest of the items
375 are left empty for user-input;
376 includes a resetCalcHead for the Model and the Guard.*)
377 fun modelProblem (cI:calcID) =
378 (let val (ptp, _) = get_calc cI
379 val ptp = reset_calchead ptp
380 val (_, _, ptp) = nxt_specif Model_Problem ptp
381 in (upd_calc cI (ptp, []);
382 modifycalcheadOK2xml cI (get_ocalhd ptp)) end)
383 handle _ => sysERROR2xml cI "error in kernel";
386 (* set the UContext determined on a knowledgebrowser to the current calc *)
387 fun setContext (cI:calcID) (ip as (_,p_):pos') (guh:guh) =
388 (case (implode o (take_fromto 1 4) o Symbol.explode) guh of
390 if member op = [Pbl,Met] p_
391 then message2xml cI "thy-context not to calchead"
392 else if ip = ([],Res) then message2xml cI "no thy-context at result"
393 else if no_thycontext guh then message2xml cI ("no thy-context for '" ^ guh ^ "'")
396 val (ptp as (pt, pold), _) = get_calc cI
397 val is = get_istate pt ip
398 val subs = subs_from is "dummy" guh
399 val tac = guh2rewtac guh subs
401 case locatetac tac (pt, ip) of (*='fun setNextTactic'+step*)
402 ("ok", (tacis, c, ptp as (_,p))) =>
403 (upd_calc cI ((pt,p), []);
404 autocalculateOK2xml cI pold (if null c then pold else last_elem c) p)
405 | ("unsafe-ok", (tacis, c, ptp as (_,p))) =>
406 (upd_calc cI ((pt,p), []);
407 autocalculateOK2xml cI pold (if null c then pold else last_elem c) p)
408 | ("end-of-calculation",_) => message2xml cI "end-of-calculation"
409 | ("failure",_) => sysERROR2xml cI "failure"
410 | ("not-applicable",_) => (*the rule comes from anywhere..*)
411 (case applicable_in ip pt tac of
412 Notappl e => message2xml cI ("'" ^ tac2str tac ^ "' not-applicable")
415 val ctxt = get_ctxt pt pold
417 generate1 (assoc_thy "Isac") m (Uistate, ctxt) ip pt
418 in upd_calc cI ((pt,p),[]);
419 autocalculateOK2xml cI pold (if null c then pold else last_elem c) p
424 val pI = guh2kestoreID guh
425 val ((pt, _), _) = get_calc cI
427 if member op = [Pbl, Met] p_
429 let val (pt, chd) = set_problem pI (pt, ip)
430 in (upd_calc cI ((pt, ip), []); modifycalcheadOK2xml cI chd) end
431 else sysERROR2xml cI "setContext for pbl requires ActiveFormula on CalcHead"
435 val mI = guh2kestoreID guh
436 val ((pt, _), _) = get_calc cI
438 if member op = [Pbl, Met] p_
440 let val (pt, chd) = set_method mI (pt, ip)
441 in (upd_calc cI ((pt, ip), []); modifycalcheadOK2xml cI chd) end
442 else sysERROR2xml cI "setContext for met requires ActiveFormula on CalcHead"
444 handle _ => sysERROR2xml cI "error in kernel";
447 (*.specify the Method at the activeFormula and return a CalcHead
448 containing the Guard.
449 WN0512 impl.incomplete, see 'nxt_specif (Specify_Method '.*)
450 fun setMethod (cI:calcID) (mI:metID) =
451 (* val (cI, mI) = (1, ["Test","solve_linear"]);
453 (let val ((pt, _), _) = get_calc cI
454 val ip as (_, p_) = get_pos cI 1
455 in if member op = [Pbl,Met] p_
456 then let val (pt, chd) = set_method mI (pt, ip)
457 in (upd_calc cI ((pt, ip), []);
458 modifycalcheadOK2xml cI chd) end
459 else sysERROR2xml cI "setMethod requires ActiveFormula on CalcHead"
461 handle _ => sysERROR2xml cI "error in kernel";
463 (*.specify the Problem at the activeFormula and return a CalcHead
464 containing the Model; special case of checkContext;
465 WN0512 impl.incomplete, see 'nxt_specif (Specify_Problem '.*)
466 fun setProblem (cI:calcID) (pI:pblID) =
467 (let val ((pt, _), _) = get_calc cI
468 val ip as (_, p_) = get_pos cI 1
469 in if member op = [Pbl,Met] p_
470 then let val (pt, chd) = set_problem pI (pt, ip)
471 in (upd_calc cI ((pt, ip), []);
472 modifycalcheadOK2xml cI chd) end
473 else sysERROR2xml cI "setProblem requires ActiveFormula on CalcHead"
475 handle _ => sysERROR2xml cI "error in kernel";
477 (*.specify the Theory at the activeFormula and return a CalcHead;
478 special case of checkContext;
479 WN0512 impl.incomplete, see 'nxt_specif (Specify_Method '.*)
480 fun setTheory (cI:calcID) (tI:thyID) =
481 (let val ((pt, _), _) = get_calc cI
482 val ip as (_, p_) = get_pos cI 1
483 in if member op = [Pbl,Met] p_
484 then let val (pt, chd) = set_theory tI (pt, ip)
485 in (upd_calc cI ((pt, ip), []);
486 modifycalcheadOK2xml cI chd) end
487 else sysERROR2xml cI "setProblem requires ActiveFormula on CalcHead"
489 handle _ => sysERROR2xml cI "error in kernel";
492 (**. without update of CalcTree .**)
494 (*.match the model of a problem at pos p
495 with the model-pattern of the problem with pblID*)
496 (*fun tryMatchProblem cI pblID =
497 (let val ((pt,_),_) = get_calc cI
499 val chd = trymatch pblID pt p
500 in trymatchOK2xml cI chd end)
501 handle _ => sysERROR2xml cI "error in kernel";*)
503 (*.refinement for the parent-problem of the position.*)
504 (* val (cI, (p,p_), guh) = (1, ([1],Res), "pbl_equ_univ");
506 fun refineProblem cI ((p,p_) : pos') (guh : guh) =
507 (let val pblID = guh2kestoreID guh
508 val ((pt,_),_) = get_calc cI
509 val pp = par_pblobj pt p
510 val chd = tryrefine pblID pt (pp, p_)
511 in matchpbl2xml cI chd end)
512 handle _ => sysERROR2xml cI "error in kernel";
514 (* append a formula to the calculation *)
515 fun appendFormula' cI (ifo:cterm') =
518 val pos as (_,p_) = get_pos cI 1
522 (case inform cs' (encode ifo) of
523 ("ok", (_(*use in DG !!!*), c, ptp as (_,p))) =>
524 (upd_calc cI (ptp, []); upd_ipos cI 1 p;
525 appendformulaOK2xml cI pos (if null c then pos else last_elem c) p)
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 else last_elem c) p)
529 | (msg, _) => appendformulaERROR2xml cI msg)
530 | (msg, cs') => appendformulaERROR2xml cI msg
532 handle ERROR msg => sysERROR2xml cI ("error in kernel: " ^ msg);
534 fun appendFormula cI ifo = (*Future.fork (fn () => *)appendFormula' cI ifo(* ) *);
536 (* replace a formula with_in_ a calculation;
537 this situation applies for initial CAS-commands, too *)
538 fun replaceFormula cI (ifo:cterm') =
540 val ((pt, _), _) = get_calc cI
543 case inform (([], [], (pt, p)): calcstate') (encode ifo) of
544 ("ok", (_(*tacs used for DG ?*), c, ptp' as (pt',p'))) =>
546 val unc = if null (fst p) then p else move_up [] pt p
547 val _ = upd_calc cI (ptp', [])
548 val _ = upd_ipos cI 1 p'
549 in replaceformulaOK2xml cI unc (if null c then unc else last_elem c) p' end
550 | ("same-formula", _) => replaceformulaERROR2xml cI "formula not changed"
551 | (msg, _) => replaceformulaERROR2xml cI msg
553 handle _ => sysERROR2xml cI "error in kernel";
558 moveActive*: set the pos' of the active formula stored with the calctree
559 could take pos' as argument for consistency checks
560 move*: compute the new iterator from the old one on the fly
564 fun moveActiveRoot cI =
565 (let val _ = upd_ipos cI 1 ([],Pbl)
566 in iteratorOK2xml cI ([],Pbl) end)
567 handle e => sysERROR2xml cI "error in kernel";
569 (iteratorOK2xml cI ([],Pbl))
570 handle e => sysERROR2xml cI "";
571 fun moveActiveRootTEST cI =
572 (let val _ = upd_ipos cI 1 ([],Pbl)
573 in (*iteratorOK2xml cI ([],Pbl)*)() end)
574 handle e => sysERROR2xml cI "error in kernel";
576 (* val (cI, uI) = (1,1);
577 val (cI, uI) = (1,2);
579 fun moveActiveDown cI =
580 ((let val ((pt,_),_) = get_calc cI
581 (* val (P, (Nd (_, ns)), (p::(ps as (_::_)), p_)) =([]:pos, pt, get_pos cI uI);
582 val (P, (Nd (c, ns)), ([p], p_)) =([]:pos, pt, get_pos cI uI);
586 val ip' = move_dn [] pt (get_pos cI 1)
587 val _ = upd_ipos cI 1 ip'
588 in iteratorOK2xml cI ip' end)
589 handle (PTREE e) => iteratorERROR2xml cI)
590 handle _ => sysERROR2xml cI "error in kernel";
591 fun moveDown cI (p:pos') =
592 ((let val ((pt,_),_) = get_calc cI
593 (* val (P, (Nd (_, ns)), (p::(ps as (_::_)), p_)) =([]:pos, pt, get_pos cI uI);
594 val (P, (Nd (c, ns)), ([p], p_)) =([]:pos, pt, get_pos cI uI);
598 val ip' = move_dn [] pt p
599 in iteratorOK2xml cI ip' end)
600 handle (PTREE e) => iteratorERROR2xml cI)
601 handle _ => sysERROR2xml cI "error in kernel";
602 fun moveActiveDownTEST cI =
603 let val ((pt,_),_) = get_calc cI
604 val ip = get_pos cI 1
605 val ip' = (move_dn [] pt ip)
607 val _ = upd_ipos cI 1 ip'
608 in (*iteratorOK2xml cI uI*)() end;
610 fun moveActiveLevelDown cI =
611 ((let val ((pt,_),_) = get_calc cI
612 val ip' = movelevel_dn [] pt (get_pos cI 1)
613 val _ = upd_ipos cI 1 ip'
614 in iteratorOK2xml cI ip' end)
615 handle (PTREE e) => iteratorERROR2xml cI)
616 handle _ => sysERROR2xml cI "error in kernel";
617 fun moveLevelDown cI (p:pos') =
618 ((let val ((pt,_),_) = get_calc cI
619 val ip' = movelevel_dn [] pt p
620 in iteratorOK2xml cI ip' end)
621 handle (PTREE e) => iteratorERROR2xml cI)
622 handle _ => sysERROR2xml cI "error in kernel";
624 fun moveActiveUp cI =
625 ((let val ((pt,_),_) = get_calc cI
626 val ip' = move_up [] pt (get_pos cI 1)
627 val _ = upd_ipos cI 1 ip'
628 in iteratorOK2xml cI ip' end)
629 handle PTREE e => iteratorERROR2xml cI)
630 handle _ => sysERROR2xml cI "error in kernel";
631 fun moveUp cI (p:pos') =
632 ((let val ((pt,_),_) = get_calc cI
633 val ip' = move_up [] pt p
634 in iteratorOK2xml cI ip' end)
635 handle PTREE e => iteratorERROR2xml cI)
636 handle _ => sysERROR2xml cI "error in kernel";
638 fun moveActiveLevelUp cI =
639 ((let val ((pt,_),_) = get_calc cI
640 val ip' = movelevel_up [] pt (get_pos cI 1)
641 val _ = upd_ipos cI 1 ip'
642 in iteratorOK2xml cI ip' end)
643 handle PTREE e => iteratorERROR2xml cI)
644 handle _ => sysERROR2xml cI "error in kernel";
645 fun moveLevelUp cI (p:pos') =
646 ((let val ((pt,_),_) = get_calc cI
647 val ip' = movelevel_up [] pt p
648 in iteratorOK2xml cI ip' end)
649 handle PTREE e => iteratorERROR2xml cI)
650 handle _ => sysERROR2xml cI "error in kernel";
652 fun moveActiveCalcHead cI =
653 ((let val ((pt,_),_) = get_calc cI
654 val ip' = movecalchd_up pt (get_pos cI 1)
655 val _ = upd_ipos cI 1 ip'
656 in iteratorOK2xml cI ip' end)
657 handle PTREE e => iteratorERROR2xml cI)
658 handle _ => sysERROR2xml cI "error in kernel";
659 fun moveCalcHead cI (p:pos') =
660 ((let val ((pt,_),_) = get_calc cI
661 val ip' = movecalchd_up pt p
662 in iteratorOK2xml cI ip' end)
663 handle PTREE e => iteratorERROR2xml cI)
664 handle _ => sysERROR2xml cI "error in kernel";
667 (*.initContext Thy_ is conceptually impossible at [Pbl,Met]
668 and at positions with Check_Postcond and End_Trans;
669 at possible pos's there can be NO rewrite (returned as a context, too).*)
670 fun initContext (cI:calcID) Thy_ (pos as (p, p_):pos') =
671 ((if member op = [Pbl, Met] p_
672 then message2xml cI "thy-context not to calchead"
673 else if pos = ([], Res) then message2xml cI "no thy-context at result"
675 let val cs as (ptp as (pt, _), _) = get_calc cI
677 if exist_lev_on' pt pos
680 val pos' = lev_on' pt pos
681 val tac = get_tac_checked pt pos'
684 then contextthyOK2xml cI (context_thy (pt, pos) tac)
685 else message2xml cI ("no thy-context at tac '" ^ tac2str tac ^ "'")
687 else if is_curr_endof_calc pt pos
690 ("ok", (tacis, _, (pt, _))) =>
691 let val tac = fst3 (last_elem tacis)
694 then contextthyOK2xml cI (context_thy ptp tac)
695 else message2xml cI ("no thy-context at tac '" ^ tac2str tac ^ "'")
697 | (msg, _) => message2xml cI msg
698 else message2xml cI "no thy-context at this position"
700 handle _ => sysERROR2xml cI "error in kernel")
702 | initContext cI Pbl_ (pos as (p,p_):pos') =
703 ((let val ((pt,_),_) = get_calc cI
704 val pp = par_pblobj pt p
705 val chd = initcontext_pbl pt (pp,p_)
706 in matchpbl2xml cI chd end)
707 handle _ => sysERROR2xml cI "error in kernel")
709 | initContext cI Met_ (pos as (p,p_):pos') =
710 ((let val ((pt,_),_) = get_calc cI
711 val pp = par_pblobj pt p
712 val chd = initcontext_met pt (pp,p_)
713 in matchmet2xml cI chd end)
714 handle _ => sysERROR2xml cI "error in kernel");
716 (* match a theorem, a ruleset (etc., selected in the knowledge-browser)
717 with the formula in the focus on the worksheet;
718 string contains the thy, thus it is unique as thmID, rlsID for this thy;
719 take the substitution from the istate of the formula *)
720 fun checkContext (cI:calcID) (pos:pos' as (p,p_)) (guh:guh) =
721 (case (implode o (take_fromto 1 4) o Symbol.explode) guh of
723 if member op = [Pbl,Met] p_
724 then message2xml cI "thy-context not to calchead"
725 else if pos = ([],Res) then message2xml cI "no thy-context at result"
726 else if no_thycontext guh then message2xml cI ("no thy-context for '"^
728 else let val (ptp as (pt,_),_) = get_calc cI
729 val is = get_istate pt pos
730 val subs = subs_from is "dummy" guh
731 val tac = guh2rewtac guh subs
732 in contextthyOK2xml cI (context_thy (pt, pos) tac) end
734 (*.match the model of a problem at pos p
735 with the model-pattern of the problem with pblID.*)
736 (* val (cI, pos:pos' as (p,p_), guh) =
737 (1, p, kestoreID2guh Pbl_ ["univariate","equation"]);
738 val (cI, pos:pos' as (p,p_), guh) =
739 (1, ([],Pbl), kestoreID2guh Pbl_ ["univariate","equation"]);
740 val (cI, pos:pos' as (p,p_), guh) =
741 (1, ([],Pbl), "pbl_equ_univ");
744 let val ((pt,_),_) = get_calc cI
745 val pp = par_pblobj pt p
746 val keID = guh2kestoreID guh
747 val chd = context_pbl keID pt pp
748 in matchpbl2xml cI chd end
749 (* val (cI, pos:pos' as (p,p_), guh) =
750 (1, ([],Pbl), kestoreID2guh Met_ ["LinEq", "solve_lineq_equation"]);
753 let val ((pt,_),_) = get_calc cI
754 val pp = par_pblobj pt p
755 val keID = guh2kestoreID guh
756 val chd = context_met keID pt pp
757 in matchmet2xml cI chd end)
758 handle _ => sysERROR2xml cI "error in kernel";
760 (* for an errpatID find "(fillpatID, fillform)" list
761 which dedicated to this errpat and which is applicable at current formula*)
762 fun findFillpatterns cI errpatID =
764 val ((pt, _), _) = get_calc cI
765 val pos = get_pos cI 1;
766 val fillpats = find_fillpatterns (pt, pos) errpatID
767 in findFillpatterns2xml cI (map #1 fillpats) end;
769 (* given a fillpatID propose a fillform to the learner on the worksheet;
770 the "ctree" is extended with fillpat and "ostate Inconsistent",
771 the "istate" is copied and NOT updated;
773 arg errpatID: required because there is no dialog-related state in the math-kernel.
775 fun requestFillformula cI (errpatID, fillpatID) =
777 val ((pt, _), _) = get_calc cI
778 val pos = get_pos cI 1
779 val fillforms = find_fillpatterns (pt, pos) errpatID
781 case filter ((curry op = fillpatID) o
782 (#1: (fillpatID * term * thm * (subs option) -> fillpatID))) fillforms of
783 (_, fillform, thm, sube_opt) :: _ =>
785 val (pt, pos') = generate_inconsistent_rew (sube_opt, thm'_of_thm thm)
786 fillform (get_loc pt pos) pos pt
788 (upd_calc cI ((pt, pos'), []); (*upd_ipos cI 1 pos';*)
789 autocalculateOK2xml cI pos pos' pos')
791 | _ => autocalculateERROR2xml cI "no fillpattern found"
794 (* input a formula which exactly fills the gaps in a "fillformula"
795 presented to the learner immediately before by "requestFillformula (errpatID, fillpatID)":
796 errpatID: lhs of the respective thm = lhs of fillformula with fillpatID.
797 The respective thm is stored in the ctree. *)
798 fun inputFillFormula cI ifo =
800 val ((pt, _), _) = get_calc cI
801 val pos = get_pos cI 1;
803 case is_exactly_equal (pt, pos) ifo of
806 in (* cp from applyTactic *)
807 case locatetac tac (pt, pos) of
808 ("ok", (_, c, ptp as (_,p'))) =>
809 (upd_calc cI (ptp, []);
811 autocalculateOK2xml cI pos (if null c then p' else last_elem c) p')
812 | ("unsafe-ok", (_, c, ptp as (_,p'))) =>
813 (upd_calc cI (ptp, []);
815 autocalculateOK2xml cI pos (if null c then p' else last_elem c) p')
816 | ("end-of-calculation", (_, c, ptp as (_,p'))) =>
817 (upd_calc cI (ptp, []);
819 autocalculateOK2xml cI pos (if null c then p' else last_elem c) p')
820 | (str,_) => autocalculateERROR2xml cI "failure"
822 | (msg, _) => message2xml cI msg
825 (*------------------------------------------------------------------*)
828 (*------------------------------------------------------------------*)