1 (* Title: tests for Interpret/mathengine.sml
2 Author: Walther Neuper 2000, 2006
3 (c) due to copyright terms
5 "--------------------------------------------------------";
6 "table of contents --------------------------------------";
7 "--------------------------------------------------------";
8 "----------- change to parse ctxt -----------------------";
9 "----------- debugging setContext..pbl_ -----------------";
10 "----------- tryrefine ----------------------------------";
11 "---------- mini-subpbl isac-java 3992e3bd1948: initial <NEXT> ---------------";
12 "----------- fun step: Apply_Method without init_form ---";
13 "----------- fun step -----------------------------------";
14 "----------- fun autocalc -------------------------------";
15 "----------- fun autoCalculate' --------------------------";
16 "----------- fun autoCalculate..CompleteCalc ------------";
17 "----------- search for Or_to_List ----------------------";
18 "----------- check thy in CalcTreeTEST ------------------";
19 "--------------------------------------------------------";
20 "--------------------------------------------------------";
21 "--------------------------------------------------------";
23 "----------- change to parse ctxt -----------------------";
24 "----------- change to parse ctxt -----------------------";
25 "----------- change to parse ctxt -----------------------";
26 "===== start calculation: from problem description (fmz) to origin";
27 val fmz = ["realTestGiven (((1+2)*4/3)^^^2)","realTestFind s"];
28 val (thyID, pblID, metID) =
29 ("Test", ["calculate", "test"], ["Test", "test_calculate"]);
30 val (p,_,_,nxt,_,pt) = CalcTreeTEST [(fmz, (thyID, pblID, metID))];
32 (* call sequence: CalcTreeTEST
33 > nxt_specify_init_calc
36 val (thy, pbt) = (Thy_Info.get_theory thyID, (#ppc o get_pbt) pblID);
38 val ctxt = Proof_Context.init_global thy;
40 val ctopts = map (parseNEW ctxt) fmz;
41 val dts = map (split_dts o the) ctopts;
43 (term * term list) list
44 formulas: e.g. ((1+2)*4/3)^^^2
45 description: e.g. realTestGiven
50 string list -> theory -> (string * (term * 'a)) list -> ori list
53 string list -> theory -> (string * (term * 'a)) list -> (ori list * ctxt)
55 FROM val oris = prep_ori...
56 TO val (oris, _) = prep_ori...
58 "----- insert ctxt in ptree";
60 FROM loc : istate option * istate option,
61 TO loc : (istate * ctxt) option * (istate * ctxt) option,
63 FROM val pt = Nd (PblObj
64 {.., loc = (SOME (ScrState ([], [], NONE, Const ("empty", "'a"), Sundef, false)),
66 TO val pt = Nd (PblObj
68 ((SOME (ScrState ([], [], NONE, Const ("empty", "'a"), Sundef, false)), ctxt),
72 "===== interactive specification: from origin to specification (probl)";
73 val (p,_,_,nxt,_,pt) = me nxt p [1] pt;
74 (*nxt =("Add_Given", Model_Problem)*)
75 val (p,_,_,nxt,_,pt) = me nxt p [1] pt;
76 (*nxt = ("Add_Find",Add_Find "realTestFind s") : string * tac*)
78 (* call sequence: me Model_Problem
79 > me ("Add_Given", Add_Given "realTestGiven (((1 + 2) * 4 / 3) ^^^ 2)")
82 > specify GET ctxt (stored in ctree)
93 val (p,_,_,nxt,_,pt) = me nxt p [1] pt;
94 (*nxt = ("Specify_Theory",Specify_Theory "Test") : string * tac*)
95 val (p,_,_,nxt,_,pt) = me nxt p [1] pt;
96 (*nxt = ("Specify_Problem",Specify_Problem ["calculate","test"])*)
98 "===== end specify: from specification (probl) to guard (method)";
99 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
100 (*nxt = ("Specify_Method",Specify_Method ("Test","test_calculate"))*)
102 "===== start interpretation: from guard to environment";
103 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
104 (*nxt = ("Apply_Method",Apply_Method ("Test","test_calculate"))*)
106 (* call sequence: me ("Apply_Method",...
109 > solve ("Apply_Method",...
111 val ((_,tac), ptp) = (nxt, (pt, p));
112 locatetac tac (pt,p);
113 val (mI, m) = mk_tac'_ tac;
114 val Appl m = applicable_in p pt m;
115 member op = specsteps mI;
116 loc_solve_ (mI,m) ptp;
117 val (m, (pt, pos)) = ((mI,m), ptp);
119 val ((_, m as Apply_Method' (mI, _, _, _)), (pt, (pos as (p,_)))) =
121 val {srls,...} = get_met mI;
122 val PblObj{meth=itms,...} = get_obj I pt p;
123 val thy' = get_obj g_domID pt p;
124 val thy = assoc_thy thy';
125 val (is as ScrState (env,_,_,_,_,_), ctxt, sc) = init_scrstate thy itms mI;
127 "----- go on in the calculation";
128 val (p,_,f,nxt,_,pt) = me nxt pos [1] pt;
129 (*nxt = ("Calculate",Calculate "PLUS")*)
130 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
131 (*nxt = ("Calculate",Calculate "TIMES")*)
133 "===== input a formula to be derived from previous istate";
134 "----- appendFormula TODO: first repair error";
135 val cs = ((pt,p),[]);
136 val ("ok", cs' as (_,_,(pt,p))) = step p cs;
137 val ifo = (* encode "4^^^2" \<longrightarrow>*) "4^2";
139 val ("no derivation found", (_,_,(pt, p))) = inform cs' ((*encode*) ifo);
140 here ^^^^^^^^^^^^^^^^^^^^^ should be "ok"
143 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
144 (*nxt = ("Calculate",Calculate "DIVIDE")*)
145 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
146 (*nxt = ("Calculate",Calculate "POWER")*)
147 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
148 (*nxt = ("Check_Postcond",Check_Postcond ["calculate","test"])*)
149 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
150 (*nxt = ("End_Proof'",End_Proof')*)
151 if f = Form' (FormKF (~1,EdUndef,0,Nundef,"16")) then ()
152 else error "calculate.sml: script test_calculate changed behaviour";
154 "===== tactic Subproblem: from environment to origin";
158 "----------- debugging setContext..pbl_ -----------------";
159 "----------- debugging setContext..pbl_ -----------------";
160 "----------- debugging setContext..pbl_ -----------------";
162 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
163 ("Test", ["sqroot-test","univariate","equation","test"],
164 ["Test","squ-equ-test-subpbl1"]))];
166 moveActiveRoot 1; modelProblem 1;
168 val pos as (p,_) = ([],Pbl);
169 val guh = "pbl_equ_univ";
170 checkContext 1 pos guh;
171 val ((pt,_),_) = get_calc 1;
172 val pp = par_pblobj pt p;
173 val keID = guh2kestoreID guh;
174 case context_pbl keID pt pp of (true,["univariate", "equation"],_,_,_)=>()
175 | _ => error "mathengine.sml: context_pbl .. pbl_equ_univ checked";
177 case get_obj g_spec pt p of (_, ["e_pblID"], _) => ()
178 | _ => error "mathengine.sml: context_pbl .. pbl still empty";
179 setContext 1 pos guh;
180 val ((pt,_),_) = get_calc 1;
181 case get_obj g_spec pt p of (_, ["univariate", "equation"], _) => ()
182 | _ => error "mathengine.sml: context_pbl .. pbl set";
185 setContext 1 pos "met_eq_lin";
186 val ((pt,_),_) = get_calc 1;
187 case get_obj g_spec pt p of (_, _, ["LinEq", "solve_lineq_equation"]) => ()
188 | _ => error "mathengine.sml: context_pbl .. pbl set";
191 "----------- tryrefine ----------------------------------";
192 "----------- tryrefine ----------------------------------";
193 "----------- tryrefine ----------------------------------";
195 CalcTree [(["equality (x/(x^2 - 6*x+9) - 1/(x^2 - 3*x) =1/x)",
196 "solveFor x", "solutions L"],
197 ("RatEq",["univariate","equation"],["no_met"]))];
199 moveActiveRoot 1; autoCalculate' 1 CompleteCalc;
201 refineProblem 1 ([1],Res) "pbl_equ_univ"
202 (*gives "pbl_equ_univ_rat" correct*);
204 refineProblem 1 ([1],Res) (pblID2guh ["LINEAR","univariate","equation"])
205 (*gives "pbl_equ_univ_lin" incorrect*);
207 "---------- mini-subpbl isac-java 3992e3bd1948: initial <NEXT> ---------------";
208 "---------- mini-subpbl isac-java 3992e3bd1948: initial <NEXT> ---------------";
209 "---------- mini-subpbl isac-java 3992e3bd1948: initial <NEXT> ---------------";
211 (*this is the exact sequence of input provided by isac-java 3992e3bd1948;
212 Surrounding ML { * ... * } are omitted.
213 The multiple calls suggest to replicate the CalcTree in the Dialogue.
215 Reproduce error: On the newly opened Worksheet click <NEXT>.
216 The error indicates a problem with the hierarchy of theories.
218 CalcTree [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
219 ("Test",["sqroot-test","univariate","equation","test"],["Test","squ-equ-test-subpbl1"]))];
222 getFormulaeFromTo 1 ([],Pbl) ([],Pbl) 0 false;
223 getFormulaeFromTo 1 ([],Pbl) ([],Pbl) 0 false;
224 (*completeCalcHead*)autoCalculate' 1 CompleteCalcHead;
225 (*completeCalcHead*)getActiveFormula 1 ;
226 (*completeCalcHead*)refFormula 1 ([],Met);
227 refFormula 1 ([],Pbl);
228 (*<REFFORMULA> <CALCID> 1 </CALCID> <CALCHEAD status = "correct"> *)
229 (*fetchProposedTactic 1;
230 <SYSERROR> <CALCID> 1 </CALCID> <ERROR> error in kernel </ERROR></SYSERROR>*)
231 "~~~~~ fun fetchProposedTactic, args:"; val (cI) = (1);
232 val ("ok", (tacis, _, _)) = step (get_pos cI 1) (get_calc cI)
233 val _= upd_tacis cI tacis
234 val (tac,_,_) = last_elem tacis;
235 (*fetchproposedtacticOK2xml cI tac (fetchErrorpatterns tac);
236 fetchErrorpatterns tac
237 ERROR: app_py: not found: ["IsacKnowledge","KEStore","Rulesets","e_rls"]*)
238 "~~~~~ fun fetchErrorpatterns, args:"; val (tac) = (tac);
240 val (part, thyID) = thy_containing_rls "Build_Thydata" rlsID;
241 if part = "IsacKnowledge" andalso thyID = "KEStore" then ()
242 else error "fetchErrorpatterns .. e_rls changed";
243 (* val Hrls {thy_rls = (_, rls), ...} = get_the [part, thyID, "Rulesets", rlsID]
244 ERROR app_py: not found: ["IsacKnowledge","KEStore","Rulesets","e_rls"]*)
246 "----------- fun step: Apply_Method without init_form ---";
247 "----------- fun step: Apply_Method without init_form ---";
248 "----------- fun step: Apply_Method without init_form ---";
249 val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
251 ("Test", ["sqroot-test","univariate","equation","test"],
252 ["Test","squ-equ-test-subpbl1"]);
253 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
254 "~~~~~ fun me, args:"; val (_,tac) = nxt;
255 val ("ok", (_, _, (pt, p))) = locatetac tac (pt,p);
256 "~~~~~ fun step, args:"; val (ip as (_,p_), ptp as (pt,p), tacis) = (p, (pt, e_pos'), []);
257 val pIopt = get_pblID (pt,ip);
258 ip = ([],Res) (*false*);
260 member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p));
261 (*^^^^^^^^: Apply_Method without init_form*)
263 "----------- fun step -----------------------------------";
264 "----------- fun step -----------------------------------";
265 "----------- fun step -----------------------------------";
266 val p = e_pos'; val c = [];
267 val (p,_,f,nxt,_,pt) =
269 [(["functionTerm (x^^^2 + 1)", "integrateBy x", "antiDerivative FF"],
270 ("Integrate", ["integrate","function"], ["diff","integration"]))];
271 "----- step 1: returns tac = Model_Problem ---";
272 val (str, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);
273 "----- step 2: returns tac = ---";
274 val (str, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);
275 "----- step 3: returns tac = ---";
276 val (str, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);
277 "----- step 4: returns tac = ---";
278 val (str, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);
279 "----- step 5: returns tac = ---";
281 (*========== inhibit exn AK110718 ==============================================
282 2002 stops here as well: TODO review actual arguments:
283 val (str, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);
284 "----- step 6: returns tac = ---";
285 val (str, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);
286 "----- step 7: returns tac = ---";
287 val (str, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);
288 "----- step 8: returns tac = ---";
289 val (str, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);
290 ========== inhibit exn AK110718 ==============================================*)
293 "----------- fun autocalc -------------------------------";
294 "----------- fun autocalc -------------------------------";
295 "----------- fun autocalc -------------------------------";
296 val p = e_pos'; val c = [];
297 val (p,_,f,nxt,_,pt) =
299 [(["functionTerm (x^^^2 + 1)", "integrateBy x", "antiDerivative FF"],
300 ("Integrate",["integrate","function"], ["diff","integration"]))];
301 (*-----since Model_Problem + complete_mod_ in case cas of SOME-----*
302 modeling is skipped FIXME
303 *-----since Model_Problem + complete_mod_ in case cas of SOME-----*)
304 tracing "----- step 1 ---";
305 val (str, cut, (pt, p)) = autocalc [] p ((pt, e_pos'),[]) (Step 1); show_pt pt;
306 tracing "----- step 2 ---";
307 val (str, cut, (pt, p)) = autocalc [] p ((pt, e_pos'),[]) (Step 1); show_pt pt;
308 tracing "----- step 3 ---";
309 val (str, cut, (pt, p)) = autocalc [] p ((pt, e_pos'),[]) (Step 1); show_pt pt;
310 tracing "----- step 4 ---";
311 val (str, cut, (pt, p)) = autocalc [] p ((pt, e_pos'),[]) (Step 1); show_pt pt;
312 tracing "----- step 5 ---";
313 val (str, cut, (pt, p)) = autocalc [] p ((pt, e_pos'),[]) (Step 1); show_pt pt;
314 tracing "----- step 6 ---";
315 val (str, cut, (pt, p)) = autocalc [] p ((pt, e_pos'),[]) (Step 1); show_pt pt;
316 tracing "----- step 7 ---";
317 val (str, cut, (pt, p)) = autocalc [] p ((pt, e_pos'),[]) (Step 1); show_pt pt;
318 tracing "----- step 8 ---";
319 val (str, cut, (pt, p)) = autocalc [] p ((pt, e_pos'),[]) (Step 1); show_pt pt;
320 (*========== inhibit exn AK110718 ==============================================
321 WN110628: Integration does not work, see Knowledge/integrate.sml
323 if str = "end-of-calculation" andalso
324 term2str (get_obj g_res pt (fst p)) = "c + x + 1 / 3 * x ^^^ 3" then ()
325 else error "mathengine.sml -- fun autocalc -- end";
326 ========== inhibit exn AK110718 ==============================================*)
329 "----------- fun autoCalculate' -----------------------------------";
330 "----------- fun autoCalculate' -----------------------------------";
331 "----------- fun autoCalculate' -----------------------------------";
333 CalcTree (*ATTENTION: encode_fmz ... unlike CalcTreeTEST*)
334 [(["functionTerm (x^2 + 1)", "integrateBy x", "antiDerivative FF"],
335 ("Integrate", ["integrate", "function"], ["diff", "integration"]))];
338 (*-----since Model_Problem + complete_mod_ in case cas of SOME-----*
339 modeling is skipped FIXME
340 see test/../interface -- solve_linear as rootpbl FE -- for OTHER expl:
341 setNextTactic 1 (Add_Given "equality (1 + -1 * 2 + x = 0)");
342 autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1); (*equality added*);
344 fetchProposedTactic 1;
345 setNextTactic 1 (Add_Given "solveFor x");
346 autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
348 fetchProposedTactic 1;
349 setNextTactic 1 (Add_Find "solutions L");
350 autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
352 fetchProposedTactic 1;
353 setNextTactic 1 (Specify_Theory "Test");
354 autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
355 *-----since Model_Problem + complete_mod_ in case cas of SOME-----*)
356 autoCalculate' 1 (Step 1);
358 autoCalculate' 1 (Step 1);
360 autoCalculate' 1 (Step 1);
362 autoCalculate' 1 (Step 1);
364 autoCalculate' 1 (Step 1);
366 autoCalculate' 1 (Step 1);
368 autoCalculate' 1 (Step 1);
370 autoCalculate' 1 (Step 1);
372 autoCalculate' 1 (Step 1);
373 val (ptp as (_, p), _) = get_calc 1;
374 val (Form t,_,_) = pt_extract ptp;
376 if term2str t = "c + x + 1 / 3 * x ^^^ 3" andalso p = ([], Res) then ()
377 else error "mathengine.sml -- fun autoCalculate' -- end";
379 "----------- fun autoCalculate..CompleteCalc ------------";
380 "----------- fun autoCalculate..CompleteCalc ------------";
381 "----------- fun autoCalculate..CompleteCalc ------------";
383 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
384 ("Test", ["sqroot-test","univariate","equation","test"],
385 ["Test","squ-equ-test-subpbl1"]))];
388 (*autoCalculate' 1 CompleteCalc; (*WAS <SYSERROR>..<ERROR> error in kernel </ERROR>*)*)
389 "~~~~~ fun autoCalculate, args:"; val (cI, auto) = (1, CompleteCalc);
390 val pold = get_pos cI 1;
391 (*autocalc [] pold (get_calc cI) auto; (*WAS Type unification failed
392 Type error in application: incompatible operand type
393 Operator: solveFor :: real \<Rightarrow> una
394 Operand: x :: 'a *)*)
395 "~~~~~ fun autocalc, args:"; val (c, (pos as (_,p_)), ((pt,_), _), auto)
396 = ([] : pos' list, pold, (get_calc cI), auto);
397 autoord auto > 3 andalso just_created (pt, pos); (*true*)
398 val ptp = all_modspec (pt, pos);
399 "TODO all_modspec: preconds for rootpbl";
400 (*all_solve auto c ptp; (*WAS Type unification failed...*)*)
401 "~~~~~ and all_solve, args:"; val (auto, c, (ptp as (pt, pos as (p,_)))) =
403 val (_,_,mI) = get_obj g_spec pt p
404 val ctxt = get_ctxt pt pos
405 val (ttt, c', ptp) = nxt_solv (Apply_Method' (mI, NONE, e_istate, ctxt)) (e_istate, ctxt) ptp;
406 (* complete_solve auto (c @ c') ptp; (*WAS Type unification failed...*) pos = ([], Met)*)
407 "~~~~~ fun complete_solve, args:"; val (auto, c, (ptp as (_, p as (_,p_)))) =
408 (auto, (c @ c'), ptp);
409 p = ([], Res) (*false p = ([1], Frm)*);
410 member op = [Pbl,Met] p_ (*false*);
411 val (ttt, c', ptp') = nxt_solve_ ptp; (*ttt = Rewrite_Set "norm_equation"*)
412 (* complete_solve auto (c @ c') ptp'; (*WAS Type unification failed...*) pos = ([], Met)*)
413 "~~~~~ fun complete_solve, args:"; val (auto, c, (ptp as (_, p as (_,p_)))) =
414 (auto, (c @ c'), ptp');
415 p = ([], Res) (*false p = ([1], Res)*);
416 member op = [Pbl,Met] p_ (*false*);
417 val (ttt, c', ptp') = nxt_solve_ ptp; (*ttt = Rewrite_Set "Test_simplify"*)
418 (* complete_solve auto (c @ c') ptp'; (*WAS Type unification failed...*) pos = ([], Met)*)
419 "~~~~~ fun complete_solve, args:"; val (auto, c, (ptp as (_, p as (_,p_)))) =
420 (auto, (c @ c'), ptp');
421 p = ([], Res) (*false p = ([2], Res)*);
422 member op = [Pbl,Met] p_ (*false*);
423 val ((Subproblem _, tac_, (_, is))::_, c', ptp') = nxt_solve_ ptp;
424 autoord auto < 5 (*false*);
425 (* val ptp = all_modspec ptp' (*WAS Type unification failed...*)*)
426 "~~~~~ fun all_modspec, args:"; val (pt, pos as (p,_)) = (ptp');
427 val (PblObj {fmz = (fmz_, _), origin = (pors, spec as (dI,pI,mI), hdl), ...}) = get_obj I pt p;
428 val thy = assoc_thy dI;
429 val {ppc, ...} = get_met mI;
430 (* val (mors, ctxt) = prep_ori fmz_ thy ppc; WAS Type unification failed because
431 val ctxt' = dI |> Thy_Info.get_theory |> Proof_Context.init_global;
432 (parseNEW ctxt' "x" |> the |> type_of) = TFree ("'a",[]);
434 (*vvv from: | assod pt _ (Subproblem'...*)
435 val (fmz_, vals) = oris2fmz_vals pors;
437 val ctxt = dI |> Thy_Info.get_theory |> Proof_Context.init_global
438 |> declare_constraints' vals
440 (*^^^ from: | assod pt _ (Subproblem'...*)
441 val [(1, [1], "#Given", dsc_eq, [equality]),
442 (2, [1], "#Given", dsc_solvefor, [xxx]),
443 (3, [1], "#Find", dsc_solutions, [x_i])] = pors;
444 if term2str xxx = "x" andalso type_of xxx = HOLogic.realT then ()
445 else error "autoCalculate..CompleteCalc: SubProblem broken 1";
446 val pt = update_pblppc pt p (map (ori2Coritm ppc) pors);
447 val pt = update_metppc pt p (map (ori2Coritm ppc) pors);
448 val pt = update_spec pt p (dI,pI,mI);
449 val pt = update_ctxt pt p ctxt;
450 "~~~~~ return to complete_solve, args:"; val (ptp) = (pt, (p,Met));
451 val (msg, c, (pt, p)) = complete_solve auto (c @ c') ptp;
452 if msg = "end-of-calculation" andalso c = [] andalso p = ([], Res) then ()
453 else error "autoCalculate..CompleteCalc: final result";
454 if terms2strs (get_assumptions_ pt p) =
455 ["matches (?a = ?b) (-1 + x = 0)", (*precond of submet*)
456 "x = 1", (*result of subpbl and rootpbl*)
457 "precond_rootmet x"] (*precond of rootmet*)
458 then () else error "autoCalculate..CompleteCalc: ctxt at final result";
461 "--------- search for Or_to_List ------------------------";
462 "--------- search for Or_to_List ------------------------";
463 "--------- search for Or_to_List ------------------------";
464 val fmz = ["equality (x^^^2 + 4*x + 5 = (2::real))", "solveFor x","solutions L"];
465 val (dI',pI',mI') = ("Isac", ["univariate","equation"], ["no_met"])
466 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
467 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
468 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
469 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
470 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
471 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
472 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
473 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
474 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
475 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
476 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Subproblem"*)
477 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
478 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
479 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
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 "~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), (_:NEW(*remove*)), (pt:ptree)) =
489 val ("ok", (_, _, ptp)) = locatetac tac (pt,p)
491 "~~~~~ fun step, args:"; val (((ip as (_,p_)):pos'), ((ptp as (pt,p), tacis):calcstate)) =
492 (p, ((pt, e_pos'),[]));
493 val pIopt = get_pblID (pt,ip);
494 ip = ([],Res); (*false*)
496 member op = [Pbl,Met] p_; (*false*)
497 "~~~~~ fun nxt_solve_, args:"; val (ptp as (pt, pos as (p,p_))) = (pt,ip);
498 e_metID = get_obj g_metID pt (par_pblobj pt p); (*false*)
499 val thy' = get_obj g_domID pt (par_pblobj pt p);
500 val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
501 val (tac_,is,(t,_)) = next_tac (thy',srls) (pt,pos) sc is; (*WAS Empty_Tac_: tac_*)
502 case tac_ of Or_to_List' _ => ()
503 | _ => error "Or_to_List broken ?"
506 "----------- check thy in CalcTreeTEST ------------------";
507 "----------- check thy in CalcTreeTEST ------------------";
508 "----------- check thy in CalcTreeTEST ------------------";
509 "WN1109 with Inverse_Z_Transform.thy when starting tests with CalcTreeTEST \n" ^
510 "we got the message: ME_Isa: thy 'Build_Inverse_Z_Transform' not in system \n" ^
511 "Below there are the steps which found out the reason: \n" ^
512 "store_pbt mistakenly stored that theory.";
513 val ctxt = Proof_Context.init_global @{theory Isac};
514 val SOME t = parseNEW ctxt "filterExpression (X = 3 / (z - 1/4 + -1/8 * (1/(z::real))))";
515 val SOME t = parseNEW ctxt "stepResponse (x[n::real]::bool)";
517 val fmz = ["filterExpression (X = 3 / (z - 1/4 + -1/8 * (1/(z::real))))",
518 "stepResponse (x[n::real]::bool)"];
519 val (dI,pI,mI) = ("Isac", ["Inverse", "Z_Transform", "SignalProcessing"],
520 ["SignalProcessing","Z_Transform","Inverse"]);
522 val (p,_,fb,nxt,_,pt) = CalcTreeTEST [(fmz, (dI,pI,mI))];
523 (*WAS ME_Isa: thy 'Build_Inverse_Z_Transform' not in system*)
525 "~~~~~ T fun CalcTreeTEST, args:"; val [(fmz, sp):fmz] = [(fmz, (dI,pI,mI))];
526 "~~~~~ fun nxt_specify_init_calc, args:"; val (fmz, (dI, pI, mI)) = (fmz, sp);
527 val thy = assoc_thy dI;
528 mI = ["no_met"]; (*false*)
529 val (pI, (pors, pctxt), mI) = (pI, get_pbt pI |> #ppc |> prep_ori fmz thy, mI)
530 val {cas, ppc, thy=thy',...} = get_pbt pI; (*take dI from _refined_ pbl*)
531 "tracing bottom up"; Context.theory_name thy' = "Build_Inverse_Z_Transform"; (*WAS true*)
532 val dI = theory2theory' (maxthy thy thy');
533 "tracing bottom up"; dI = "Build_Inverse_Z_Transform"; (*WAS true*)
535 val hdl = pblterm dI pI;
536 val (pt, _) = cappend_problem e_ptree [] (e_istate, pctxt) (fmz, (dI, pI, mI))
537 (pors, (dI, pI, mI), hdl)
538 val pt = update_ctxt pt [] pctxt;
540 "~~~~~ fun nxt_specif, args:"; val ((tac as Model_Problem), (pt, pos as (p,p_))) = (Model_Problem, (pt, ([], Pbl)));
541 val PblObj {origin = (oris, ospec, _), probl, spec, ctxt, ...} = get_obj I pt p;
542 "tracing bottom up"; #1(ospec) = "Build_Inverse_Z_Transform"; (*WAS true*)
544 "~~~~~ fun some_spec, args:"; val ((odI, opI, omI), (dI, pI, mI)) = (ospec, spec);
545 dI = e_domID; (*true*)
546 odI = "Build_Inverse_Z_Transform"; (*true*)
547 dI = "e_domID"; (*true*)
548 "~~~~~ after fun some_spec:";
549 val (dI, pI, mI) = some_spec ospec spec;
550 "tracing bottom up"; dI = "Build_Inverse_Z_Transform"; (*WAS true*)
551 val thy = assoc_thy dI; (*caused ME_Isa: thy 'Build_Inverse_Z_Transform' not in system*)