1 (* Title: tests for Interpret/mathengine.sml
2 Author: Walther Neuper 2000, 2006
3 (c) due to copyright terms
5 theory Test_Some imports Build_Thydata begin
6 ML {* KEStore_Elems.set_ref_thy @{theory};
7 fun autoCalculate' cI auto = autoCalculate cI auto |> Future.join *}
8 ML_file "~~/test/Tools/isac/Interpret/mathengine.sml"
10 "--------------------------------------------------------";
11 "table of contents --------------------------------------";
12 "--------------------------------------------------------";
13 "----------- change to parse ctxt -----------------------";
14 "----------- debugging setContext..pbl_ -----------------";
15 "----------- tryrefine ----------------------------------";
16 "---------- mini-subpbl isac-java 3992e3bd1948: initial <NEXT> ---------------";
17 "----------- fun step: Apply_Method without init_form ---";
18 "----------- fun step -----------------------------------";
19 "----------- fun autocalc -------------------------------";
20 "----------- fun autoCalculate --------------------------";
21 "----------- fun autoCalculate..CompleteCalc ------------";
22 "----------- search for Or_to_List ----------------------";
23 "----------- check thy in CalcTreeTEST ------------------";
24 "----------- identified error in fun getTactic, string_of_thmI ---------------";
25 "----------- improved fun getTactic for interSteps and numeral calculations --";
26 "--------------------------------------------------------";
27 "--------------------------------------------------------";
28 "--------------------------------------------------------";
30 "----------- change to parse ctxt -----------------------";
31 "----------- change to parse ctxt -----------------------";
32 "----------- change to parse ctxt -----------------------";
33 "===== start calculation: from problem description (fmz) to origin";
34 val fmz = ["realTestGiven (((1+2)*4/3)^^^2)","realTestFind s"];
35 val (thyID, pblID, metID) =
36 ("Test", ["calculate", "test"], ["Test", "test_calculate"]);
37 (*======= Isabelle2013-2 --> Isabelle2014: unclear, why this test ever run ========================
38 val (p,_,_,nxt,_,pt) = CalcTreeTEST [(fmz, (thyID, pblID, metID))];
40 (* call sequence: CalcTreeTEST
41 > nxt_specify_init_calc
44 val (thy, pbt) = (Thy_Info.get_theory thyID, (#ppc o get_pbt) pblID);
46 val ctxt = Proof_Context.init_global thy;
48 val ctopts = map (parseNEW ctxt) fmz;
49 val dts = map (split_dts o the) ctopts;
51 (term * term list) list
52 formulas: e.g. ((1+2)*4/3)^^^2
53 description: e.g. realTestGiven
58 string list -> theory -> (string * (term * 'a)) list -> ori list
61 string list -> theory -> (string * (term * 'a)) list -> (ori list * ctxt)
63 FROM val oris = prep_ori...
64 TO val (oris, _) = prep_ori...
66 "----- insert ctxt in ctree";
68 FROM loc : istate option * istate option,
69 TO loc : (istate * ctxt) option * (istate * ctxt) option,
71 FROM val pt = Nd (PblObj
72 {.., loc = (SOME (ScrState ([], [], NONE, Const ("empty", "'a"), Sundef, false)),
74 TO val pt = Nd (PblObj
76 ((SOME (ScrState ([], [], NONE, Const ("empty", "'a"), Sundef, false)), ctxt),
80 "===== interactive specification: from origin to specification (probl)";
81 val (p,_,_,nxt,_,pt) = me nxt p [1] pt;
82 (*nxt =("Add_Given", Model_Problem)*)
83 val (p,_,_,nxt,_,pt) = me nxt p [1] pt;
84 (*nxt = ("Add_Find",Add_Find "realTestFind s") : string * tac*)
86 (* call sequence: me Model_Problem
87 > me ("Add_Given", Add_Given "realTestGiven (((1 + 2) * 4 / 3) ^^^ 2)")
90 > specify GET ctxt (stored in ctree)
101 val (p,_,_,nxt,_,pt) = me nxt p [1] pt;
102 (*nxt = ("Specify_Theory",Specify_Theory "Test") : string * tac*)
103 val (p,_,_,nxt,_,pt) = me nxt p [1] pt;
104 (*nxt = ("Specify_Problem",Specify_Problem ["calculate","test"])*)
106 "===== end specify: from specification (probl) to guard (method)";
107 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
108 (*nxt = ("Specify_Method",Specify_Method ("Test","test_calculate"))*)
110 "===== start interpretation: from guard to environment";
111 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
112 (*nxt = ("Apply_Method",Apply_Method ("Test","test_calculate"))*)
114 (* call sequence: me ("Apply_Method",...
117 > solve ("Apply_Method",...
119 val ((_,tac), ptp) = (nxt, (pt, p));
120 locatetac tac (pt,p);
121 val (mI, m) = mk_tac'_ tac;
122 val Appl m = applicable_in p pt m;
123 member op = specsteps mI;
124 loc_solve_ (mI,m) ptp;
125 val (m, (pt, pos)) = ((mI,m), ptp);
127 val ((_, m as Apply_Method' (mI, _, _, _)), (pt, (pos as (p,_)))) =
129 val {srls,...} = get_met mI;
130 val PblObj{meth=itms,...} = get_obj I pt p;
131 val thy' = get_obj g_domID pt p;
132 val thy = assoc_thy thy';
133 val (is as ScrState (env,_,_,_,_,_), ctxt, sc) = init_scrstate thy itms mI;
135 "----- go on in the calculation";
136 val (p,_,f,nxt,_,pt) = me nxt pos [1] pt;
137 (*nxt = ("Calculate",Calculate "PLUS")*)
138 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
139 (*nxt = ("Calculate",Calculate "TIMES")*)
141 "===== input a formula to be derived from previous istate";
142 "----- appendFormula TODO: first repair error";
143 val cs = ((pt,p),[]);
144 val ("ok", cs' as (_,_,(pt,p))) = step p cs;
145 val ifo = (* encode "4^^^2" \<longrightarrow>*) "4^2";
147 val ("no derivation found", (_,_,(pt, p))) = inform cs' ((*encode*) ifo);
148 here ^^^^^^^^^^^^^^^^^^^^^ should be "ok"
151 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
152 (*nxt = ("Calculate",Calculate "DIVIDE")*)
153 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
154 (*nxt = ("Calculate",Calculate "POWER")*)
155 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
156 (*nxt = ("Check_Postcond",Check_Postcond ["calculate","test"])*)
157 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
158 (*nxt = ("End_Proof'",End_Proof')*)
159 if f = Form' (FormKF (~1,EdUndef,0,Nundef,"16")) then ()
160 else error "calculate.sml: script test_calculate changed behaviour";
162 "===== tactic Subproblem: from environment to origin";
164 ======= Isabelle2013-2 --> Isabelle2014: unclear, why this test ever run ========================*)
167 "----------- debugging setContext..pbl_ -----------------";
168 "----------- debugging setContext..pbl_ -----------------";
169 "----------- debugging setContext..pbl_ -----------------";
171 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
172 ("Test", ["sqroot-test","univariate","equation","test"],
173 ["Test","squ-equ-test-subpbl1"]))];
175 moveActiveRoot 1; modelProblem 1;
177 val pos as (p,_) = ([],Pbl);
178 val guh = "pbl_equ_univ";
179 checkContext 1 pos guh;
180 val ((pt,_),_) = get_calc 1;
181 val pp = par_pblobj pt p;
182 val keID = guh2kestoreID guh;
183 case context_pbl keID pt pp of (true,["univariate", "equation"],_,_,_)=>()
184 | _ => error "mathengine.sml: context_pbl .. pbl_equ_univ checked";
186 case get_obj g_spec pt p of (_, ["e_pblID"], _) => ()
187 | _ => error "mathengine.sml: context_pbl .. pbl still empty";
188 setContext 1 pos guh;
189 val ((pt,_),_) = get_calc 1;
190 case get_obj g_spec pt p of (_, ["univariate", "equation"], _) => ()
191 | _ => error "mathengine.sml: context_pbl .. pbl set";
194 setContext 1 pos "met_eq_lin";
195 val ((pt,_),_) = get_calc 1;
196 case get_obj g_spec pt p of (_, _, ["LinEq", "solve_lineq_equation"]) => ()
197 | _ => error "mathengine.sml: context_pbl .. pbl set";
200 "----------- tryrefine ----------------------------------";
201 "----------- tryrefine ----------------------------------";
202 "----------- tryrefine ----------------------------------";
204 CalcTree [(["equality (x/(x^2 - 6*x+9) - 1/(x^2 - 3*x) =1/x)",
205 "solveFor x", "solutions L"],
206 ("RatEq",["univariate","equation"],["no_met"]))];
208 moveActiveRoot 1; autoCalculate 1 CompleteCalc;
210 refineProblem 1 ([1],Res) "pbl_equ_univ"
211 (*gives "pbl_equ_univ_rat" correct*);
213 refineProblem 1 ([1],Res) (pblID2guh ["LINEAR","univariate","equation"])
214 (*gives "pbl_equ_univ_lin" incorrect*);
216 "---------- mini-subpbl isac-java 3992e3bd1948: initial <NEXT> ---------------";
217 "---------- mini-subpbl isac-java 3992e3bd1948: initial <NEXT> ---------------";
218 "---------- mini-subpbl isac-java 3992e3bd1948: initial <NEXT> ---------------";
220 (*this is the exact sequence of input provided by isac-java 3992e3bd1948;
221 Surrounding ML { * ... * } are omitted.
222 The multiple calls suggest to replicate the CalcTree in the Dialogue.
224 CalcTree [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
225 ("Test",["sqroot-test","univariate","equation","test"],["Test","squ-equ-test-subpbl1"]))];
228 getFormulaeFromTo 1 ([],Pbl) ([],Pbl) 0 false;
229 getFormulaeFromTo 1 ([],Pbl) ([],Pbl) 0 false;
230 (*completeCalcHead*)autoCalculate 1 CompleteCalcHead;
231 (*completeCalcHead*)getActiveFormula 1 ;
232 (*completeCalcHead*)refFormula 1 ([],Met);
233 refFormula 1 ([],Pbl);
234 (*<REFFORMULA> <CALCID> 1 </CALCID> <CALCHEAD status = "correct"> *)
235 fetchProposedTactic 1;
236 (*-> <STRINGLISTTACTIC name="Apply_Method">
238 <STRING> Test </STRING>
239 <STRING> squ-equ-test-subpbl1 </STRING>
240 WAS PREVIOUSLY: <SYSERROR> <CALCID> 1 </CALCID> <ERROR> error in kernel </ERROR></SYSERROR>*)
241 "~~~~~ fun fetchProposedTactic, args:"; val (cI) = (1);
242 val ("ok", (tacis, _, _)) = step (get_pos cI 1) (get_calc cI)
243 val _= upd_tacis cI tacis
244 val (tac,_,_) = last_elem tacis;
245 (*fetchproposedtacticOK2xml cI tac (fetchErrorpatterns tac);
246 fetchErrorpatterns tac
247 WAS PREVIOUSLY ERROR: app_py: not found: ["IsacKnowledge","KEStore","Rulesets","e_rls"]*)
248 "~~~~~ fun fetchErrorpatterns, args:"; val (tac) = (tac);
250 val (part, thyID) = thy_containing_rls "Build_Thydata" rlsID;
251 if part = "IsacScripts" andalso thyID = "KEStore" then ()
252 else error "fetchErrorpatterns .. e_rls changed";
253 val Hrls {thy_rls = (_, rls), ...} = get_the [part, thyID, "Rulesets", rlsID];
254 (* WAS PREVIOUSLY ERROR app_py: not found: ["IsacKnowledge","KEStore","Rulesets","e_rls"]*)
256 Rls {id = "e_rls", ...} => ()
257 | _ => error "thy_containing_rls changed for e_rls"
259 "----------- fun step: Apply_Method without init_form ---";
260 "----------- fun step: Apply_Method without init_form ---";
261 "----------- fun step: Apply_Method without init_form ---";
262 val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
264 ("Test", ["sqroot-test","univariate","equation","test"],
265 ["Test","squ-equ-test-subpbl1"]);
266 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
267 "~~~~~ fun me, args:"; val (_,tac) = nxt;
268 val ("ok", (_, _, (pt, p))) = locatetac tac (pt,p);
269 "~~~~~ fun step, args:"; val (ip as (_,p_), ptp as (pt,p), tacis) = (p, (pt, e_pos'), []);
270 val pIopt = get_pblID (pt,ip);
271 ip = ([],Res) (*false*);
273 member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p));
274 (*^^^^^^^^: Apply_Method without init_form*)
276 "----------- fun step -----------------------------------";
277 "----------- fun step -----------------------------------";
278 "----------- fun step -----------------------------------";
279 val p = e_pos'; val c = [];
280 val (p,_,f,nxt,_,pt) =
282 [(["functionTerm (x^^^2 + 1)", "integrateBy x", "antiDerivative FF"],
283 ("Integrate", ["integrate","function"], ["diff","integration"]))];
284 "----- step 1: returns tac = Model_Problem ---";
285 val (str, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);
286 "----- step 2: returns tac = ---";
287 val (str, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);
288 "----- step 3: returns tac = ---";
289 val (str, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);
290 "----- step 4: returns tac = ---";
291 val (str, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);
292 "----- step 5: returns tac = ---";
294 (*========== inhibit exn AK110718 ==============================================
295 2002 stops here as well: TODO review actual arguments:
296 val (str, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);
297 "----- step 6: returns tac = ---";
298 val (str, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);
299 "----- step 7: returns tac = ---";
300 val (str, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);
301 "----- step 8: returns tac = ---";
302 val (str, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);
303 ========== inhibit exn AK110718 ==============================================*)
306 "----------- fun autocalc -------------------------------";
307 "----------- fun autocalc -------------------------------";
308 "----------- fun autocalc -------------------------------";
309 val p = e_pos'; val c = [];
310 val (p,_,f,nxt,_,pt) =
312 [(["functionTerm (x^^^2 + 1)", "integrateBy x", "antiDerivative FF"],
313 ("Integrate",["integrate","function"], ["diff","integration"]))];
314 (*-----since Model_Problem + complete_mod_ in case cas of SOME-----*
315 modeling is skipped FIXME
316 *-----since Model_Problem + complete_mod_ in case cas of SOME-----*)
317 tracing "----- step 1 ---";
318 val (str, cut, (pt, p)) = autocalc [] p ((pt, e_pos'),[]) (Step 1); show_pt pt;
319 tracing "----- step 2 ---";
320 val (str, cut, (pt, p)) = autocalc [] p ((pt, e_pos'),[]) (Step 1); show_pt pt;
321 tracing "----- step 3 ---";
322 val (str, cut, (pt, p)) = autocalc [] p ((pt, e_pos'),[]) (Step 1); show_pt pt;
323 tracing "----- step 4 ---";
324 val (str, cut, (pt, p)) = autocalc [] p ((pt, e_pos'),[]) (Step 1); show_pt pt;
325 tracing "----- step 5 ---";
326 val (str, cut, (pt, p)) = autocalc [] p ((pt, e_pos'),[]) (Step 1); show_pt pt;
327 tracing "----- step 6 ---";
328 val (str, cut, (pt, p)) = autocalc [] p ((pt, e_pos'),[]) (Step 1); show_pt pt;
329 tracing "----- step 7 ---";
330 val (str, cut, (pt, p)) = autocalc [] p ((pt, e_pos'),[]) (Step 1); show_pt pt;
331 tracing "----- step 8 ---";
332 val (str, cut, (pt, p)) = autocalc [] p ((pt, e_pos'),[]) (Step 1); show_pt pt;
333 (*========== inhibit exn AK110718 ==============================================
334 WN110628: Integration does not work, see Knowledge/integrate.sml
336 if str = "end-of-calculation" andalso
337 term2str (get_obj g_res pt (fst p)) = "c + x + 1 / 3 * x ^^^ 3" then ()
338 else error "mathengine.sml -- fun autocalc -- end";
339 ========== inhibit exn AK110718 ==============================================*)
342 "----------- fun autoCalculate -----------------------------------";
343 "----------- fun autoCalculate -----------------------------------";
344 "----------- fun autoCalculate -----------------------------------";
346 CalcTree (*ATTENTION: encode_fmz ... unlike CalcTreeTEST*)
347 [(["functionTerm (x^2 + 1)", "integrateBy x", "antiDerivative FF"],
348 ("Integrate", ["integrate", "function"], ["diff", "integration"]))];
351 (*-----since Model_Problem + complete_mod_ in case cas of SOME-----*
352 modeling is skipped FIXME
353 see test/../interface -- solve_linear as rootpbl FE -- for OTHER expl:
354 setNextTactic 1 (Add_Given "equality (1 + -1 * 2 + x = 0)");
355 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); (*equality added*);
357 fetchProposedTactic 1;
358 setNextTactic 1 (Add_Given "solveFor x");
359 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
361 fetchProposedTactic 1;
362 setNextTactic 1 (Add_Find "solutions L");
363 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
365 fetchProposedTactic 1;
366 setNextTactic 1 (Specify_Theory "Test");
367 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
368 *-----since Model_Problem + complete_mod_ in case cas of SOME-----*)
369 autoCalculate 1 (Step 1);
371 autoCalculate 1 (Step 1);
373 autoCalculate 1 (Step 1);
375 autoCalculate 1 (Step 1);
377 autoCalculate 1 (Step 1);
379 autoCalculate 1 (Step 1);
381 autoCalculate 1 (Step 1);
383 autoCalculate 1 (Step 1);
385 autoCalculate 1 (Step 1);
386 val (ptp as (_, p), _) = get_calc 1;
387 val (Form t,_,_) = pt_extract ptp;
389 if term2str t = "c + x + 1 / 3 * x ^^^ 3" andalso p = ([], Res) then ()
390 else error "mathengine.sml -- fun autoCalculate -- end";
392 "----------- fun autoCalculate..CompleteCalc ------------";
393 "----------- fun autoCalculate..CompleteCalc ------------";
394 "----------- fun autoCalculate..CompleteCalc ------------";
396 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
397 ("Test", ["sqroot-test","univariate","equation","test"],
398 ["Test","squ-equ-test-subpbl1"]))];
401 (*autoCalculate 1 CompleteCalc; (*WAS <SYSERROR>..<ERROR> error in kernel </ERROR>*)*)
402 "~~~~~ fun autoCalculate, args:"; val (cI, auto) = (1, CompleteCalc);
403 val pold = get_pos cI 1;
404 (*autocalc [] pold (get_calc cI) auto; (*WAS Type unification failed
405 Type error in application: incompatible operand type
406 Operator: solveFor :: real \<Rightarrow> una
407 Operand: x :: 'a *)*)
408 "~~~~~ fun autocalc, args:"; val (c, (pos as (_,p_)), ((pt,_), _), auto)
409 = ([] : pos' list, pold, (get_calc cI), auto);
410 autoord auto > 3 andalso just_created (pt, pos); (*true*)
411 val ptp = all_modspec (pt, pos);
412 "TODO all_modspec: preconds for rootpbl";
413 (*all_solve auto c ptp; (*WAS Type unification failed...*)*)
414 "~~~~~ and all_solve, args:"; val (auto, c, (ptp as (pt, pos as (p,_)))) =
416 val (_,_,mI) = get_obj g_spec pt p
417 val ctxt = get_ctxt pt pos
418 val (ttt, c', ptp) = nxt_solv (Apply_Method' (mI, NONE, e_istate, ctxt)) (e_istate, ctxt) ptp;
419 (* complete_solve auto (c @ c') ptp; (*WAS Type unification failed...*) pos = ([], Met)*)
420 "~~~~~ fun complete_solve, args:"; val (auto, c, (ptp as (_, p as (_,p_)))) =
421 (auto, (c @ c'), ptp);
422 p = ([], Res) (*false p = ([1], Frm)*);
423 member op = [Pbl,Met] p_ (*false*);
424 val (ttt, c', ptp') = nxt_solve_ ptp; (*ttt = Rewrite_Set "norm_equation"*)
425 (* complete_solve auto (c @ c') ptp'; (*WAS Type unification failed...*) pos = ([], Met)*)
426 "~~~~~ fun complete_solve, args:"; val (auto, c, (ptp as (_, p as (_,p_)))) =
427 (auto, (c @ c'), ptp');
428 p = ([], Res) (*false p = ([1], Res)*);
429 member op = [Pbl,Met] p_ (*false*);
430 val (ttt, c', ptp') = nxt_solve_ ptp; (*ttt = Rewrite_Set "Test_simplify"*)
431 (* complete_solve auto (c @ c') ptp'; (*WAS Type unification failed...*) pos = ([], Met)*)
432 "~~~~~ fun complete_solve, args:"; val (auto, c, (ptp as (_, p as (_,p_)))) =
433 (auto, (c @ c'), ptp');
434 p = ([], Res) (*false p = ([2], Res)*);
435 member op = [Pbl,Met] p_ (*false*);
436 val ((Subproblem _, tac_, (_, is))::_, c', ptp') = nxt_solve_ ptp;
437 autoord auto < 5 (*false*);
438 (* val ptp = all_modspec ptp' (*WAS Type unification failed...*)*)
439 "~~~~~ fun all_modspec, args:"; val (pt, pos as (p,_)) = (ptp');
440 val (PblObj {fmz = (fmz_, _), origin = (pors, spec as (dI,pI,mI), hdl), ...}) = get_obj I pt p;
441 val thy = assoc_thy dI;
442 val {ppc, ...} = get_met mI;
443 (* val (mors, ctxt) = prep_ori fmz_ thy ppc; WAS Type unification failed because
444 val ctxt' = dI |> Thy_Info.get_theory |> Proof_Context.init_global;
445 (parseNEW ctxt' "x" |> the |> type_of) = TFree ("'a",[]);
447 (*vvv from: | assod pt _ (Subproblem'...*)
448 val (fmz_, vals) = oris2fmz_vals pors;
450 val ctxt = dI |> Thy_Info.get_theory |> Proof_Context.init_global
451 |> declare_constraints' vals
453 (*^^^ from: | assod pt _ (Subproblem'...*)
454 val [(1, [1], "#Given", dsc_eq, [equality]),
455 (2, [1], "#Given", dsc_solvefor, [xxx]),
456 (3, [1], "#Find", dsc_solutions, [x_i])] = pors;
457 if term2str xxx = "x" andalso type_of xxx = HOLogic.realT then ()
458 else error "autoCalculate..CompleteCalc: SubProblem broken 1";
459 val pt = update_pblppc pt p (map (ori2Coritm ppc) pors);
460 val pt = update_metppc pt p (map (ori2Coritm ppc) pors);
461 val pt = update_spec pt p (dI,pI,mI);
462 val pt = update_ctxt pt p ctxt;
463 "~~~~~ return to complete_solve, args:"; val (ptp) = (pt, (p,Met));
464 val (msg, c, (pt, p)) = complete_solve auto (c @ c') ptp;
465 if msg = "end-of-calculation" andalso c = [] andalso p = ([], Res) then ()
466 else error "autoCalculate..CompleteCalc: final result";
467 if terms2strs (get_assumptions_ pt p) =
468 ["matches (?a = ?b) (-1 + x = 0)", (*precond of submet*)
469 "x = 1", (*result of subpbl and rootpbl*)
470 "precond_rootmet x"] (*precond of rootmet*)
471 then () else error "autoCalculate..CompleteCalc: ctxt at final result";
474 "--------- search for Or_to_List ------------------------";
475 "--------- search for Or_to_List ------------------------";
476 "--------- search for Or_to_List ------------------------";
477 val fmz = ["equality (x^^^2 + 4*x + 5 = (2::real))", "solveFor x","solutions L"];
478 val (dI',pI',mI') = ("Isac", ["univariate","equation"], ["no_met"])
479 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
480 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
481 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
482 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
483 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
484 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
485 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
486 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
487 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
488 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
489 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Subproblem"*)
490 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
491 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
492 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
493 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
494 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
495 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
496 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
497 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
498 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
499 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
500 "~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), (_:NEW(*remove*)), (pt:ctree)) =
502 val ("ok", (_, _, ptp)) = locatetac tac (pt,p)
504 "~~~~~ fun step, args:"; val (((ip as (_,p_)):pos'), ((ptp as (pt,p), tacis):calcstate)) =
505 (p, ((pt, e_pos'),[]));
506 val pIopt = get_pblID (pt,ip);
507 ip = ([],Res); (*false*)
509 member op = [Pbl,Met] p_; (*false*)
510 "~~~~~ fun nxt_solve_, args:"; val (ptp as (pt, pos as (p,p_))) = (pt,ip);
511 e_metID = get_obj g_metID pt (par_pblobj pt p); (*false*)
512 val thy' = get_obj g_domID pt (par_pblobj pt p);
513 val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
514 val (tac_,is,(t,_)) = next_tac (thy',srls) (pt,pos) sc is; (*WAS Empty_Tac_: tac_*)
515 case tac_ of Or_to_List' _ => ()
516 | _ => error "Or_to_List broken ?"
519 "----------- check thy in CalcTreeTEST ------------------";
520 "----------- check thy in CalcTreeTEST ------------------";
521 "----------- check thy in CalcTreeTEST ------------------";
522 "WN1109 with Inverse_Z_Transform.thy when starting tests with CalcTreeTEST \n" ^
523 "we got the message: ME_Isa: thy 'Build_Inverse_Z_Transform' not in system \n" ^
524 "Below there are the steps which found out the reason: \n" ^
525 "store_pbt mistakenly stored that theory.";
526 val ctxt = Proof_Context.init_global @{theory Isac};
527 val SOME t = parseNEW ctxt "filterExpression (X = 3 / (z - 1/4 + -1/8 * (1/(z::real))))";
528 val SOME t = parseNEW ctxt "stepResponse (x[n::real]::bool)";
530 val fmz = ["filterExpression (X = 3 / (z - 1/4 + -1/8 * (1/(z::real))))",
531 "stepResponse (x[n::real]::bool)"];
532 val (dI,pI,mI) = ("Isac", ["Inverse", "Z_Transform", "SignalProcessing"],
533 ["SignalProcessing","Z_Transform","Inverse"]);
535 val (p,_,fb,nxt,_,pt) = CalcTreeTEST [(fmz, (dI,pI,mI))];
536 (*WAS ME_Isa: thy 'Build_Inverse_Z_Transform' not in system*)
538 "~~~~~ T fun CalcTreeTEST, args:"; val [(fmz, sp):fmz] = [(fmz, (dI,pI,mI))];
539 "~~~~~ fun nxt_specify_init_calc, args:"; val (fmz, (dI, pI, mI)) = (fmz, sp);
540 val thy = assoc_thy dI;
541 mI = ["no_met"]; (*false*)
542 val (pI, (pors, pctxt), mI) = (pI, get_pbt pI |> #ppc |> prep_ori fmz thy, mI)
543 val {cas, ppc, thy=thy',...} = get_pbt pI; (*take dI from _refined_ pbl*)
544 "tracing bottom up"; Context.theory_name thy' = "Build_Inverse_Z_Transform"; (*WAS true*)
545 val dI = theory2theory' (maxthy thy thy');
546 "tracing bottom up"; dI = "Build_Inverse_Z_Transform"; (*WAS true*)
548 val hdl = pblterm dI pI;
549 val (pt, _) = cappend_problem e_ctree [] (e_istate, pctxt) (fmz, (dI, pI, mI))
550 (pors, (dI, pI, mI), hdl)
551 val pt = update_ctxt pt [] pctxt;
553 "~~~~~ fun nxt_specif, args:"; val ((tac as Model_Problem), (pt, pos as (p,p_))) = (Model_Problem, (pt, ([], Pbl)));
554 val PblObj {origin = (oris, ospec, _), probl, spec, ctxt, ...} = get_obj I pt p;
555 "tracing bottom up"; #1(ospec) = "Build_Inverse_Z_Transform"; (*WAS true*)
557 "~~~~~ fun some_spec, args:"; val ((odI, opI, omI), (dI, pI, mI)) = (ospec, spec);
558 dI = e_domID; (*true*)
559 odI = "Build_Inverse_Z_Transform"; (*true*)
560 dI = "e_domID"; (*true*)
561 "~~~~~ after fun some_spec:";
562 val (dI, pI, mI) = some_spec ospec spec;
563 "tracing bottom up"; dI = "Build_Inverse_Z_Transform"; (*WAS true*)
564 val thy = assoc_thy dI; (*caused ME_Isa: thy 'Build_Inverse_Z_Transform' not in system*)
566 "----------- identified error in fun getTactic, string_of_thmI ---------------";
567 "----------- identified error in fun getTactic, string_of_thmI ---------------";
568 "----------- identified error in fun getTactic, string_of_thmI ---------------";
570 CalcTree [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
571 ("Test",["sqroot-test","univariate","equation","test"],["Test","squ-equ-test-subpbl1"]))];
573 autoCalculate 1 CompleteCalcHead;
574 autoCalculate 1 (Step 1);
575 autoCalculate 1 (Step 1);
576 autoCalculate 1 (Step 1);
577 getTactic 1 ([1],Frm); (*<RULESET> norm_equation </RULESET>*)
578 interSteps 1 ([1],Res);
579 "~~~~~ fun interSteps, args:"; val (cI, ip) = (1, ([1],Res));
580 val ((pt,p), tacis) = get_calc cI;
581 (not o is_interpos) ip = false;
582 val ip' = lev_pred' pt ip;
583 "~~~~~ fun detailstep, args:"; val (pt, (pos as (p,p_):pos')) = (pt, ip);
584 (* ^^^^^^^^^ not in test/../ *)
586 val cn = children nd;
588 (is_rewset o (get_obj g_tac nd)) [(*root of nd*)] = true;
589 "~~~~~ fun detailrls, args:"; val (pt, (pos as (p,p_):pos')) = (pt, pos);
590 (* ^^^^^^^^^ only once in test/../solve.sml*)
591 val t = get_obj g_form pt p
592 val tac = get_obj g_tac pt p
593 val rls = (assoc_rls o rls_of) tac
594 val ctxt = get_ctxt pt pos
595 (*rls = Rls {calc = [], erls = ...*)
596 val is = init_istate tac t
597 (*TODO.WN060602 ScrState (["(t_, Problem (Isac,[equation,univar]))"]
598 is wrong for simpl, but working ?!? *)
599 val tac_ = Apply_Method' (e_metID(*WN0402: see generate1 !?!*), SOME t, is, ctxt)
600 val pos' = ((lev_on o lev_dn) p, Frm)
601 val thy = assoc_thy "Isac"
602 val (_,_,_,pt') = (*implicit Take*)generate1 thy tac_ (is, ctxt) pos' pt;
603 (*val (_,_,(pt'',_)) = *)complete_solve CompleteSubpbl [] (pt',pos');
604 (* ^^^^^^^^^^^^^^ in test/../mathengine.sml*)
605 (* in pt'': tac = Rewrite ("rnorm_equation_add", "Test.rnorm_equation_add")},
606 ^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
607 "~~~~~ fun complete_solve, args:"; val (auto, c, (ptp as (_, p as (_,p_)): ctree * pos')) =
608 (CompleteSubpbl, [], (pt',pos'));
609 p = ([], Res) = false;
610 member op = [Pbl,Met] p_ = false;
611 val (_, c', ptp') = nxt_solve_ ptp;
612 (* in pt': tac = Rewrite ("rnorm_equation_add", "Test.rnorm_equation_add")},
613 ^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
614 "~~~~~ fun nxt_solve_, args:"; val ((ptp as (pt, pos as (p,p_)))) = (ptp);
615 e_metID = get_obj g_metID pt (par_pblobj pt p) = false;
616 val thy' = get_obj g_domID pt (par_pblobj pt p);
617 val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
618 val (tac_,is,(t,_)) = next_tac (thy',srls) (pt,pos) sc is;
619 (*tac_ = Rewrite' (..., ("rnorm_equation_add", "Test.rnorm_equation_add"), ...) !!!!!!!!!!!!!!!!*)
620 "~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt, pos as (p, _)):ctree * pos'),
621 (sc as Prog (h $ body)), (ScrState (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is);
623 nstep_up thy ptp sc E l Skip_ a v (*--> Appy (Rewrite' (.., (.., "Test.rnorm_equation_add"), ...)
624 BUT WE FIND IN THE CODE ABOVE IN next_tac:*)
626 (*----------------------------------------------------------------------------------------------*)
627 if string_of_thmI @{thm rnorm_equation_add} = "~ ?b =!= 0 ==> (?a = ?b) = (?a + - 1 * ?b = 0)"
628 then () else error "string_of_thmI changed";
629 if string_of_thm @{thm rnorm_equation_add} = "~ ?b =!= 0 ==> (?a = ?b) = (?a + - 1 * ?b = 0)"
630 then () else error "string_of_thm changed";
631 (*----------------------------------------------------------------------------------------------*)
633 (*SEARCH FOR THE ERROR WENT DOWN TO THE END OF THIS TEST, AND THEN UP TO HERE AGAIN*)
634 "~~~~~ fun nxt_solv, args:"; val (tac_, is, (pt, pos as (p,p_))) = (tac_, is, ptp);
637 (p, Met) => ((lev_on o lev_dn) p, Frm)(*begin script*)
638 | (p, Res) => (lev_on p,Res) (*somewhere in script*)
640 generate1 (assoc_thy "Isac") tac_ is pos pt;
641 (* tac = Rewrite ("rnorm_equation_add", "Test.rnorm_equation_add")},
642 ^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
643 "~~~~~ fun generate1, args:"; val (thy, (Rewrite' (thy',ord',rls',pa,thm',f,(f',asm))),
644 (is, ctxt), (p,p_), pt) = ((assoc_thy "Isac"), tac_, is, pos, pt);
645 val (pt,c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f
646 (Rewrite thm') (f',asm) Complete;
647 (* in pt: tac = Rewrite ("rnorm_equation_add", "Test.rnorm_equation_add")},
648 ^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
649 "~~~~~ fun cappend_atomic, args:"; val (pt, p, ist_res, f, r, f', s) =
650 (pt, p, (is, insert_assumptions asm ctxt), f, (Rewrite thm'), (f',asm), Complete);
651 existpt p pt andalso is_empty_tac (get_obj g_tac pt p) = false;
652 apfst (append_atomic p ist_res f r f' s) (cut_tree pt (p,Frm));
653 apfst : ('a -> 'b) -> 'a * 'c -> 'b * 'c;
654 (append_atomic p ist_res f r f' s) : ctree -> ctree;
656 (* HERE THE ERROR OCCURED IN THE FIRST APPROACH
657 getTactic 1 ([1,1],Frm); <ERROR> syserror in getTactic </ERROR> <<<<<=========================*)
658 "~~~~~ fun getTactic, args:"; val (cI, (p:pos')) = (1, ([1,1],Frm));
659 val ((pt,_),_) = get_calc cI
660 val (form, tac, asms) = pt_extract (pt, p)
662 "~~~~~ fun gettacticOK2xml, args:"; val ((cI:calcID), tac) = (cI, ta);
664 "~~~~~ fun tac2xml, args:"; val (j, (Rewrite thm')) = (i, tac);
665 "~~~~~ fun thm'2xml, args:"; val (j, ((ID, form) : thm'')) = ((j+i), thm');
666 ID = "rnorm_equation_add";
667 @{thm rnorm_equation_add};
668 (term2str o Thm.prop_of) form = "~ ?b =!= 0 ==> (?a = ?b) = (?a + -1 * ?b = 0)"
669 (*?!? should be "\<not> ?b =!= 0 \<Longrightarrow> (?a = ?b) = (?a + -1 * ?b = 0)"*)
670 (*thmstr2xml (j+i) form;
671 ERROR Undeclared constant: "Test.rnorm_equation_add" ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
675 (([], Frm), solve (x + 1 = 2, x)),
676 (([1], Frm), x + 1 = 2),
677 (([1,1], Frm), x + 1 = 2),
678 (([1,1], Res), x + 1 + -1 * 2 = 0),
679 (([1], Res), x + 1 + -1 * 2 = 0),
680 (([2], Res), -1 + x = 0)]
682 pt; --> tac = Rewrite ("rnorm_equation_add", "Test.rnorm_equation_add")*)
684 "----------- improved fun getTactic for interSteps and numeral calculations --";
685 "----------- improved fun getTactic for interSteps and numeral calculations --";
686 "----------- improved fun getTactic for interSteps and numeral calculations --";
687 reset_states (); val cI = 1;
688 CalcTree [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
689 ("Test",["sqroot-test","univariate","equation","test"],["Test","squ-equ-test-subpbl1"]))];
691 autoCalculate 1 CompleteCalcHead;
692 autoCalculate 1 (Step 1);
694 val cs = get_calc cI (* we improve from the calcstate here [*] *);
695 val pos as (_,p_) = get_pos cI 1 (* we improve from the calcstate here [*] *);
697 appendFormula 1 "x + 4 + -3 = 2" (*|> Future.join*);
698 interSteps 1 ([1],Res); (* already done by appendFormula, now showed to frontend *)
699 getTactic 1 ([1,1], Res);
700 (*<ID> sym_#add_Float ((~3,0), (0,0)) __ ((4,0), (0,0)) </ID> <<<<<================== to improve
701 <ISA> 1 + x = -3 + (4 + x) </ISA>*)
703 val ((pt''',p'''), tacis''') = get_calc cI;
706 (([], Frm), solve (x + 1 = 2, x)),
707 (([1], Frm), x + 1 = 2),
708 (([1,1], Frm), x + 1 = 2),
709 (([1,1], Res), 1 + x = 2),
710 (([1,2], Res), -3 + (4 + x) = 2),
711 (([1,3], Res), -3 + (x + 4) = 2),
712 (([1,4], Res), x + 4 + -3 = 2),
713 (([1], Res), x + 4 + -3 = 2)]*)
715 "~~~~~ fun appendFormula', args:"; val (cI, ifo) = (1, "x + 4 + -3 = 2");
716 (* val cs = get_calc cI (* we improve from the calcstate here [*] *);
717 val pos as (_,p_) = get_pos cI 1 (* we improve from the calcstate here [*] *);*)
718 val ("ok", cs') = step pos cs;
719 (*val ("ok", (_, c, ptp as (_,p))) = *)inform cs' (encode ifo);
720 "~~~~~ fun inform, args:"; val (cs as (_, _, ptp as (pt, pos as (p, p_))), istr) =
722 val SOME f_in = parse (assoc_thy "Isac") istr
723 val f_in = Thm.term_of f_in
724 val f_succ = get_curr_formula (pt, pos);
725 f_succ = f_in = false;
726 val NONE = cas_input f_in
727 val pos_pred = lev_back' pos
728 (* f_pred ---"step pos cs"---> f_succ in appendFormula *)
729 val f_pred = get_curr_formula (pt, pos_pred);
730 (*val msg_calcstate' = *)compare_step ([], [], (pt, pos_pred)) f_in (*<<=====*);
731 "~~~~~ fun compare_step, args:"; val (((tacis, c, ptp as (pt, pos as (p,p_)))), ifo) =
732 (([], [], (pt, pos_pred)), f_in);
735 Frm => get_obj g_form pt p
736 | Res => (fst o (get_obj g_result pt)) p
737 | _ => e_term (*on PblObj is fo <> ifo*);
738 val {nrls, ...} = get_met (get_obj g_metID pt (par_pblobj pt p))
739 val {rew_ord, erls, rules, ...} = rep_rls nrls;
740 (*val (found, der) = *)concat_deriv rew_ord erls rules fo ifo; (*<---------------*)
741 "~~~~~ fun concat_deriv, args:"; val (rew_ord, erls, rules, fo, ifo) =
742 (rew_ord, erls, rules, fo, ifo);
743 fun derivat ([]:(term * rule * (term * term list)) list) = e_term
744 | derivat dt = (#1 o #3 o last_elem) dt
745 fun equal (_,_,(t1, _)) (_,_,(t2, _)) = t1=t2
746 (*val fod = *)make_deriv (Isac"") erls rules (snd rew_ord) NONE fo;
747 (*val ifod = *)make_deriv (Isac"") erls rules (snd rew_ord) NONE ifo;