prep. cleanup LItool.resume_prog
1 (* Title: tests for MathEngine/mathengine-stateless.sml
2 Author: Walther Neuper 2000, 2006, 2020
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.do_next: Apply_Method without init_form ---";
18 "----------- fun Step.do_next -----------------------------------";
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 =====================*)
39 "----------- debugging setContext..pbl_ -----------------";
40 "----------- debugging setContext..pbl_ -----------------";
41 "----------- debugging setContext..pbl_ -----------------";
43 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
44 ("Test", ["sqroot-test","univariate","equation","test"],
45 ["Test","squ-equ-test-subpbl1"]))];
47 moveActiveRoot 1; modelProblem 1;
49 val pos as (p,_) = ([],Pbl);
50 val guh = "pbl_equ_univ";
51 checkContext 1 pos guh;
52 val ((pt,_),_) = get_calc 1;
53 val pp = par_pblobj pt p;
54 val keID = guh2kestoreID guh;
55 case context_pbl keID pt pp of (true,["univariate","equation"],_,_,_)=>()
56 | _ => error "mathengine.sml: context_pbl .. pbl_equ_univ checked";
58 case get_obj g_spec pt p of (_, ["e_pblID"], _) => ()
59 | _ => error "mathengine.sml: context_pbl .. pbl still empty";
61 val ((pt,_),_) = get_calc 1;
62 case get_obj g_spec pt p of (_, ["univariate","equation"], _) => ()
63 | _ => error "mathengine.sml: context_pbl .. pbl set";
66 setContext 1 pos "met_eq_lin";
67 val ((pt,_),_) = get_calc 1;
68 case get_obj g_spec pt p of (_, _, ["LinEq", "solve_lineq_equation"]) => ()
69 | _ => error "mathengine.sml: context_pbl .. pbl set";
72 "----------- tryrefine ----------------------------------";
73 "----------- tryrefine ----------------------------------";
74 "----------- tryrefine ----------------------------------";
76 CalcTree [(["equality (x/(x^2 - 6*x+9) - 1/(x^2 - 3*x) =1/x)",
77 "solveFor x", "solutions L"],
78 ("RatEq",["univariate","equation"],["no_met"]))];
80 moveActiveRoot 1; autoCalculate 1 CompleteCalc;
82 refineProblem 1 ([1],Res) "pbl_equ_univ"
83 (*gives "pbl_equ_univ_rat" correct*);
85 refineProblem 1 ([1],Res) (pblID2guh ["LINEAR","univariate","equation"])
86 (*gives "pbl_equ_univ_lin" incorrect*);
88 "---------- mini-subpbl isac-java 3992e3bd1948: initial <NEXT> ---------------";
89 "---------- mini-subpbl isac-java 3992e3bd1948: initial <NEXT> ---------------";
90 "---------- mini-subpbl isac-java 3992e3bd1948: initial <NEXT> ---------------";
92 (*this is the exact sequence of input provided by isac-java 3992e3bd1948;
93 Surrounding ML { * ... * } are omitted.
94 The multiple calls suggest to replicate the CalcTree in the Dialogue.
96 CalcTree [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
97 ("Test",["sqroot-test","univariate","equation","test"],["Test","squ-equ-test-subpbl1"]))];
100 getFormulaeFromTo 1 ([],Pbl) ([],Pbl) 0 false;
101 getFormulaeFromTo 1 ([],Pbl) ([],Pbl) 0 false;
102 (*completeCalcHead*)autoCalculate 1 CompleteCalcHead;
103 (*completeCalcHead*)getActiveFormula 1 ;
104 (*completeCalcHead*)refFormula 1 ([],Met);
105 refFormula 1 ([],Pbl);
106 (*<REFFORMULA> <CALCID> 1 </CALCID> <CALCHEAD status = "correct"> *)
107 fetchProposedTactic 1;
108 (*-> <STRINGLISTTACTIC name="Apply_Method">
110 <STRING> Test </STRING>
111 <STRING> squ-equ-test-subpbl1 </STRING>
112 WAS PREVIOUSLY: <SYSERROR> <CALCID> 1 </CALCID> <ERROR> error in kernel </ERROR></SYSERROR>*)
113 "~~~~~ fun fetchProposedTactic, args:"; val (cI) = (1);
114 val ("ok", (tacis, _, _)) = Step.do_next (get_pos cI 1) (get_calc cI)
115 val _= upd_tacis cI tacis
116 val (tac,_,_) = last_elem tacis;
117 (*fetchproposedtacticOK2xml cI tac (fetchErrorpatterns tac);
118 fetchErrorpatterns tac
119 WAS PREVIOUSLY ERROR: app_py: not found: ["IsacKnowledge","KEStore","Rulesets","e_rls"]*)
120 "~~~~~ fun fetchErrorpatterns, args:"; val (tac) = (tac);
122 val (part, thyID) = thy_containing_rls "Build_Thydata" rlsID;
123 if part = "IsacScripts" andalso thyID = "KEStore" then ()
124 else error "fetchErrorpatterns .. e_rls changed";
125 val Hrls {thy_rls = (_, rls), ...} = get_the [part, thyID, "Rulesets", rlsID];
126 (* WAS PREVIOUSLY ERROR app_py: not found: ["IsacKnowledge","KEStore","Rulesets","e_rls"]*)
128 Rls {id = "e_rls", ...} => ()
129 | _ => error "thy_containing_rls changed for e_rls"
131 "----------- fun Step.do_next: Apply_Method without init_form ---";
132 "----------- fun Step.do_next: Apply_Method without init_form ---";
133 "----------- fun Step.do_next: Apply_Method without init_form ---";
134 val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
136 ("Test", ["sqroot-test","univariate","equation","test"],
137 ["Test","squ-equ-test-subpbl1"]);
138 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
139 "~~~~~ fun me, args:"; val tac = nxt;
140 val ("ok", (_, _, (pt, p))) = Step.by_tactic tac (pt,p);
141 "~~~~~ fun Step.do_next, args:"; val (ip as (_,p_), ptp as (pt,p), tacis) = (p, (pt, e_pos'), []);
142 val pIopt = get_pblID (pt,ip);
143 ip = ([],Res) (*false*);
145 member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p));
146 (*^^^^^^^^: Apply_Method without init_form*)
148 "----------- fun Step.do_next -----------------------------------";
149 "----------- fun Step.do_next -----------------------------------";
150 "----------- fun Step.do_next -----------------------------------";
151 val p = e_pos'; val c = [];
152 val (p,_,f,nxt,_,pt) =
154 [(["functionTerm (x^^^2 + 1)", "integrateBy x", "antiDerivative FF"],
155 ("Integrate", ["integrate","function"], ["diff","integration"]))];
156 "----- step 1: returns tac = Model_Problem ---";
157 val (str, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);
158 "----- step 2: returns tac = ---";
159 val (str, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);
160 "----- step 3: returns tac = ---";
161 val (str, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);
162 "----- step 4: returns tac = ---";
163 val (str, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);
164 "----- step 5: returns tac = ---";
166 (*========== inhibit exn AK110718 ==============================================
167 2002 stops here as well: TODO review actual arguments:
168 val (str, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);
169 "----- step 6: returns tac = ---";
170 val (str, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);
171 "----- step 7: returns tac = ---";
172 val (str, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);
173 "----- step 8: returns tac = ---";
174 val (str, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);
175 ========== inhibit exn AK110718 ==============================================*)
178 "----------- fun autocalc -------------------------------";
179 "----------- fun autocalc -------------------------------";
180 "----------- fun autocalc -------------------------------";
181 val p = e_pos'; val c = [];
182 val (p,_,f,nxt,_,pt) =
184 [(["functionTerm (x^^^2 + 1)", "integrateBy x", "antiDerivative FF"],
185 ("Integrate",["integrate","function"], ["diff","integration"]))];
186 (*-----since Model_Problem + complete_mod_ in case cas of SOME-----*
187 modeling is skipped FIXME
188 *-----since Model_Problem + complete_mod_ in case cas of SOME-----*)
189 tracing "----- step 1 ---";
190 val (str, cut, (pt, p)) = autocalc [] p ((pt, e_pos'),[]) (Steps 1); show_pt pt;
191 tracing "----- step 2 ---";
192 val (str, cut, (pt, p)) = autocalc [] p ((pt, e_pos'),[]) (Steps 1); show_pt pt;
193 tracing "----- step 3 ---";
194 val (str, cut, (pt, p)) = autocalc [] p ((pt, e_pos'),[]) (Steps 1); show_pt pt;
195 tracing "----- step 4 ---";
196 val (str, cut, (pt, p)) = autocalc [] p ((pt, e_pos'),[]) (Steps 1); show_pt pt;
197 tracing "----- step 5 ---";
198 val (str, cut, (pt, p)) = autocalc [] p ((pt, e_pos'),[]) (Steps 1); show_pt pt;
199 tracing "----- step 6 ---";
200 val (str, cut, (pt, p)) = autocalc [] p ((pt, e_pos'),[]) (Steps 1); show_pt pt;
201 tracing "----- step 7 ---";
202 val (str, cut, (pt, p)) = autocalc [] p ((pt, e_pos'),[]) (Steps 1); show_pt pt;
203 tracing "----- step 8 ---";
204 val (str, cut, (pt, p)) = autocalc [] p ((pt, e_pos'),[]) (Steps 1); show_pt pt;
205 (*========== inhibit exn AK110718 ==============================================
206 WN110628: Integration does not work, see Knowledge/integrate.sml
208 if str = "end-of-calculation" andalso
209 term2str (get_obj g_res pt (fst p)) = "c + x + 1 / 3 * x ^^^ 3" then ()
210 else error "mathengine.sml -- fun autocalc -- end";
211 ========== inhibit exn AK110718 ==============================================*)
214 "----------- fun autoCalculate -----------------------------------";
215 "----------- fun autoCalculate -----------------------------------";
216 "----------- fun autoCalculate -----------------------------------";
218 CalcTree (*ATTENTION: encode_fmz ... unlike CalcTreeTEST*)
219 [(["functionTerm (x^2 + 1)", "integrateBy x", "antiDerivative FF"],
220 ("Integrate", ["integrate", "function"], ["diff", "integration"]))];
223 autoCalculate 1 (Steps 1);
225 autoCalculate 1 (Steps 1);
227 autoCalculate 1 (Steps 1);
229 autoCalculate 1 (Steps 1);
231 autoCalculate 1 (Steps 1);
233 autoCalculate 1 (Steps 1);
235 autoCalculate 1 (Steps 1);
237 autoCalculate 1 (Steps 1);
239 autoCalculate 1 (Steps 1);
240 val (ptp as (_, p), _) = get_calc 1;
241 val (Form t,_,_) = pt_extract ptp;
243 if term2str t = "c + x + 1 / 3 * x ^^^ 3" andalso p = ([], Res) then ()
244 else error "mathengine.sml -- fun autoCalculate -- end";
246 "----------- fun autoCalculate..CompleteCalc ------------";
247 "----------- fun autoCalculate..CompleteCalc ------------";
248 "----------- fun autoCalculate..CompleteCalc ------------";
250 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
251 ("Test", ["sqroot-test","univariate","equation","test"],
252 ["Test","squ-equ-test-subpbl1"]))];
255 (*autoCalculate 1 CompleteCalc; (*WAS <SYSERROR>..<ERROR> error in kernel </ERROR>*)*)
256 "~~~~~ fun autoCalculate, args:"; val (cI, auto) = (1, CompleteCalc);
257 val pold = get_pos cI 1;
258 (*autocalc [] pold (get_calc cI) auto; (*WAS Type unification failed
259 Type error in application: incompatible operand type
260 Operator: solveFor :: real \<Rightarrow> una
261 Operand: x :: 'a *)*)
262 "~~~~~ fun autocalc, args:"; val (c, (pos as (_,p_)), ((pt,_), _), auto)
263 = ([] : pos' list, pold, (get_calc cI), auto);
264 autoord auto > 3 andalso just_created (pt, pos); (*true*)
265 val ptp = all_modspec (pt, pos);
266 "TODO all_modspec: preconds for rootpbl";
267 (*all_solve auto c ptp; (*WAS Type unification failed...*)*)
268 "~~~~~ and all_solve, args:"; val (auto, c, (ptp as (pt, pos as (p,_)))) =
270 val (_,_,mI) = get_obj g_spec pt p
271 val ctxt = get_ctxt pt pos
272 val (_, (ttt, c', ptp)) = LI.by_tactic (Apply_Method' (mI, NONE, e_istate, ctxt)) (e_istate, ctxt) ptp;
273 (* complete_solve auto (c @ c') ptp; (*WAS Type unification failed...*) pos = ([], Met)*)
274 "~~~~~ fun complete_solve, args:"; val (auto, c, (ptp as (_, p as (_,p_)))) =
275 (auto, (c @ c'), ptp);
276 p = ([], Res) (*false p = ([1], Frm)*);
277 member op = [Pbl,Met] p_ (*false*);
278 val (_, (ttt, c', ptp')) = Step_Solve.do_next ptp; (*ttt = Rewrite_Set "norm_equation"*)
279 (* complete_solve auto (c @ c') ptp'; (*WAS Type unification failed...*) pos = ([], Met)*)
280 "~~~~~ fun complete_solve, args:"; val (auto, c, (ptp as (_, p as (_,p_)))) =
281 (auto, (c @ c'), ptp');
282 p = ([], Res) (*false p = ([1], Res)*);
283 member op = [Pbl,Met] p_ (*false*);
284 val (_, (ttt, c', ptp')) = Step_Solve.do_next ptp; (*ttt = Rewrite_Set "Test_simplify"*)
285 (* complete_solve auto (c @ c') ptp'; (*WAS Type unification failed...*) pos = ([], Met)*)
286 "~~~~~ fun complete_solve, args:"; val (auto, c, (ptp as (_, p as (_,p_)))) =
287 (auto, (c @ c'), ptp');
288 p = ([], Res) (*false p = ([2], Res)*);
289 member op = [Pbl,Met] p_ (*false*);
290 val (_, ((Subproblem _, tac_, (_, is)) ::_, c', ptp')) = Step_Solve.do_next ptp;
291 autoord auto < 5 (*false*);
292 (* val ptp = all_modspec ptp' (*WAS Type unification failed...*)*)
293 "~~~~~ fun all_modspec , args:"; val (pt, pos as (p,_)) = (ptp');
294 val (PblObj {fmz = (fmz_, _), origin = (pors, spec as (dI,pI,mI), hdl), ...}) = get_obj I pt p;
295 val {ppc, ...} = get_met mI;
296 (* val (mors, ctxt) = prep_ori fmz_ thy ppc; WAS Type unification failed because
297 val ctxt' = dI |> Thy_Info_get_theory |> Proof_Context.init_global;
298 (parseNEW ctxt' "x" |> the |> type_of) = TFree ("'a",[]);
300 (*vvv from: | associate pt _ (Subproblem'...*)
301 val (_, vals) = oris2fmz_vals pors;
303 val ctxt = ContextC.initialise dI vals
305 (*^^^ from: | associate pt _ (Subproblem'...*)
306 val [(1, [1], "#Given", dsc_eq, [equality]),
307 (2, [1], "#Given", dsc_solvefor, [xxx]),
308 (3, [1], "#Find", dsc_solutions, [x_i])] = pors;
309 if term2str xxx = "x" andalso type_of xxx = HOLogic.realT then ()
310 else error "autoCalculate..CompleteCalc: SubProblem broken 1";
312 val (pt, _) = cupdate_problem pt p ((dI, pI, mI),
313 map (ori2Coritm ppc) pors, map (ori2Coritm ppc) pors, ctxt)
315 "~~~~~ return to complete_solve, args:"; val (ptp) = (pt, (p,Met));
316 val (msg, c, (pt, p)) = complete_solve auto (c @ c') ptp;
317 if msg = "end-of-calculation" andalso c = [] andalso p = ([], Res) then ()
318 else error "autoCalculate..CompleteCalc: final result";
319 if eq_set op = (terms2strs (get_assumptions_ pt p),
320 ["precond_rootmet 1", "matches (?a = ?b) (-1 + x = 0)", "x = 1", "precond_rootmet x"])
321 (* assumptions are handled by Proof.context now:
322 ["matches (?a = ?b) (-1 + x = 0)", (*precond of submet*)
323 "x = 1", (*result of subpbl and rootpbl*)
324 "precond_rootmet x"] (*precond of rootmet*) *)
325 then () else error "autoCalculate..CompleteCalc: ctxt at final result";
328 "--------- search for Or_to_List ------------------------";
329 "--------- search for Or_to_List ------------------------";
330 "--------- search for Or_to_List ------------------------";
331 val fmz = ["equality (x^^^2 + 4*x + 5 = (2::real))", "solveFor x","solutions L"];
332 val (dI',pI',mI') = ("Isac_Knowledge", ["univariate","equation"], ["no_met"])
333 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
334 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
335 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
336 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
337 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
338 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
339 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
340 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
341 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
342 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
343 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Subproblem"*)
344 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
345 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
346 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
347 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
348 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
349 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
350 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
351 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
352 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
353 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
354 "~~~~~ fun me, args:"; val (tac, (p:pos'), (_:NEW(*remove*)), (pt:ctree)) =
356 val ("ok", (_, _, ptp)) = Step.by_tactic tac (pt,p)
358 "~~~~~ fun Step.do_next, args:"; val (((ip as (_,p_)):pos'), ((ptp as (pt,p), tacis):calcstate)) =
359 (p, ((pt, e_pos'),[]));
360 val pIopt = get_pblID (pt,ip);
361 ip = ([],Res); (*false*)
363 member op = [Pbl,Met] p_; (*false*)
364 "~~~~~ fun do_next, args:"; val (ptp as (pt, pos as (p,p_))) = (pt,ip);
365 e_metID = get_obj g_metID pt (par_pblobj pt p); (*false*)
366 val thy' = get_obj g_domID pt (par_pblobj pt p);
367 val ((ist, ctxt), sc) = resume_prog thy' (p,p_) pt;
368 val Next_Step (istate, ctxt, tac) = LI.find_next_step sc (pt,pos) ist ctxt; (*WAS Empty_Tac_: tac_*)
369 case tac of Or_to_List' _ => ()
370 | _ => error "Or_to_List broken ?"
373 "----------- check thy in CalcTreeTEST ------------------";
374 "----------- check thy in CalcTreeTEST ------------------";
375 "----------- check thy in CalcTreeTEST ------------------";
376 "WN1109 with Inverse_Z_Transform.thy when starting tests with CalcTreeTEST \n" ^
377 "we got the message: ME_Isa: thy 'Build_Inverse_Z_Transform' not in system \n" ^
378 "Below there are the steps which found out the reason: \n" ^
379 "store_pbt mistakenly stored that theory.";
380 val ctxt = Proof_Context.init_global @{theory Isac_Knowledge};
381 val SOME t = parseNEW ctxt "filterExpression (X = 3 / (z - 1/4 + -1/8 * (1/(z::real))))";
382 val SOME t = parseNEW ctxt "stepResponse (x[n::real]::bool)";
384 val fmz = ["filterExpression (X = 3 / (z - 1/4 + -1/8 * (1/(z::real))))", "boundVariable z",
385 "stepResponse (x[n::real]::bool)"];
386 val (dI,pI,mI) = ("Isac_Knowledge", ["Inverse", "Z_Transform", "SignalProcessing"],
387 ["SignalProcessing","Z_Transform","Inverse"]);
389 val (p,_,fb,nxt,_,pt) = CalcTreeTEST [(fmz, (dI,pI,mI))];
390 (*WAS ME_Isa: thy 'Build_Inverse_Z_Transform' not in system*)
392 "~~~~~ T fun CalcTreeTEST, args:"; val [(fmz, sp):fmz] = [(fmz, (dI,pI,mI))];
393 "~~~~~ fun nxt_specify_init_calc, args:"; val (fmz, (dI, pI, mI)) = (fmz, sp);
394 val thy = assoc_thy dI;
395 mI = ["no_met"]; (*false*)
396 val (pI, (pors, pctxt), mI) = (pI, get_pbt pI |> #ppc |> prep_ori fmz thy, mI)
397 val {cas, ppc, thy=thy',...} = get_pbt pI; (*take dI from _refined_ pbl*)
398 "tracing bottom up"; Context.theory_name thy' = "Build_Inverse_Z_Transform"; (*WAS true*)
399 val dI = theory2theory' (maxthy thy thy');
400 "tracing bottom up"; dI = "Build_Inverse_Z_Transform"; (*WAS true*)
402 val hdl = pblterm dI pI;
403 val (pt, _) = cappend_problem e_ctree [] (e_istate, pctxt) (fmz, (dI, pI, mI))
404 (pors, (dI, pI, mI), hdl, ContextC.e_ctxt)
406 "~~~~~ fun Step_Specify.by_tactic_input, args:"; val ((tac as Model_Problem), (pt, pos as (p,p_))) = (Model_Problem, (pt, ([], Pbl)));
407 val PblObj {origin = (oris, ospec, _), probl, spec, ctxt, ...} = get_obj I pt p;
408 "tracing bottom up"; #1(ospec) = "Build_Inverse_Z_Transform"; (*WAS true*)
410 "~~~~~ fun some_spec, args:"; val ((odI, opI, omI), (dI, pI, mI)) = (ospec, spec);
411 dI = e_domID; (*true*)
412 odI = "Build_Inverse_Z_Transform"; (*true*)
413 dI = "e_domID"; (*true*)
414 "~~~~~ after fun some_spec:";
415 val (dI, pI, mI) = some_spec ospec spec;
416 "tracing bottom up"; dI = "Build_Inverse_Z_Transform"; (*WAS true*)
417 val thy = assoc_thy dI; (*caused ME_Isa: thy 'Build_Inverse_Z_Transform' not in system*)
419 "----------- identified error in fun getTactic, string_of_thmI ---------------";
420 "----------- identified error in fun getTactic, string_of_thmI ---------------";
421 "----------- identified error in fun getTactic, string_of_thmI ---------------";
423 CalcTree [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
424 ("Test",["sqroot-test","univariate","equation","test"],["Test","squ-equ-test-subpbl1"]))];
426 autoCalculate 1 CompleteCalcHead;
427 autoCalculate 1 (Steps 1);
428 autoCalculate 1 (Steps 1);
429 autoCalculate 1 (Steps 1);
430 getTactic 1 ([1],Frm); (*<RULESET> norm_equation </RULESET>*)
431 interSteps 1 ([1],Res);
432 "~~~~~ fun interSteps, args:"; val (cI, ip) = (1, ([1],Res));
433 val ((pt,p), tacis) = get_calc cI;
434 (not o is_interpos) ip = false;
435 val ip' = lev_pred' pt ip;
436 "~~~~~ fun detailstep, args:"; val (pt, (pos as (p,p_):pos')) = (pt, ip);
437 (* ^^^^^^^^^ not in test/../ *)
439 val cn = children nd;
441 (is_rewset o (get_obj g_tac nd)) [(*root of nd*)] = true;
442 "~~~~~ fun detailrls, args:"; val (pt, (pos as (p,p_):pos')) = (pt, pos);
443 (* ^^^^^^^^^ only once in test/../solve.sml*)
444 val t = get_obj g_form pt p
445 val tac = get_obj g_tac pt p
446 val rls = (assoc_rls o rls_of) tac
447 val ctxt = get_ctxt pt pos
448 (*rls = Rls {calc = [], erls = ...*)
449 val is = init_istate tac t
450 (*TODO.WN060602 Pstate (["(t_, Problem (Isac,[equation,univar]))"]
451 is wrong for simpl, but working ?!? *)
452 val tac_ = Apply_Method' (e_metID(*WN0402: see generate1 !?!*), SOME t, is, ctxt)
453 val pos' = ((lev_on o lev_dn) p, Frm)
454 val thy = assoc_thy "Isac_Knowledge"
455 val (_,_,_,pt') = (*implicit Take*)generate1 tac_ (is, ctxt) (pt, pos');
456 (*val (_,_,(pt'',_)) = *)complete_solve CompleteSubpbl [] (pt',pos');
457 (* ^^^^^^^^^^^^^^ in test/../mathengine.sml*)
458 (* in pt'': tac = Rewrite ("rnorm_equation_add", "Test.rnorm_equation_add")},
459 ^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
460 "~~~~~ fun complete_solve , args:"; val (auto, c, (ptp as (_, p as (_,p_)): ctree * pos')) =
461 (CompleteSubpbl, [], (pt',pos'));
462 p = ([], Res) = false;
463 member op = [Pbl,Met] p_ = false;
464 val (_, (_, c', ptp')) = Step_Solve.do_next ptp;
465 (* in pt': tac = Rewrite ("rnorm_equation_add", "Test.rnorm_equation_add")},
466 ^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
467 "~~~~~ fun do_next , args:"; val ((ptp as (pt, pos as (p,p_)))) = (ptp);
468 e_metID = get_obj g_metID pt (par_pblobj pt p) = false;
469 val thy' = get_obj g_domID pt (par_pblobj pt p);
470 val ((ist, ctxt), sc) = resume_prog thy' (p,p_) pt;
471 val Next_Step (is, ctxt, tac_) = LI.find_next_step sc (pt,pos) ist ctxt;
472 (*tac_ = Rewrite' (..., ("rnorm_equation_add", "Test.rnorm_equation_add"), ...) !!!!!!!!!!!!!!!!*)
474 (*----- outcommented during cleanup of args in lucas-interpreter.sml ------------------------\\* )
475 "~~~~~ fun find_next_step , args:"; val (thy, (ptp as (pt, pos as (p, _)):ctree * pos'),
476 (sc as Prog (h $ body)), (Pstate (ist as (E,l,rls,a,v,s,b)), ctxt)) = ((thy',srls), (pt,pos), sc, is);
478 go_scan_up thy ptp sc ist true (*--> Accept_Tac (Rewrite' (.., (.., "Test.rnorm_equation_add"), ...)
479 BUT WE FIND IN THE CODE ABOVE IN find_next_step:*)
481 (*----------------------------------------------------------------------------------------------*)
482 if string_of_thmI @{thm rnorm_equation_add} = "\<not> ?b =!= 0 \<Longrightarrow> (?a = ?b) = (?a + - 1 * ?b = 0)"
483 then () else error "string_of_thmI changed";
484 if string_of_thm @{thm rnorm_equation_add} = "\<not> ?b =!= 0 \<Longrightarrow> (?a = ?b) = (?a + - 1 * ?b = 0)"
485 then () else error "string_of_thm changed";
486 (*----------------------------------------------------------------------------------------------*)
488 (*SEARCH FOR THE ERROR WENT DOWN TO THE END OF THIS TEST, AND THEN UP TO HERE AGAIN*)
489 "~~~~~ fun begin_end_prog, args:"; val (tac_, is, (pt, pos as (p,p_))) = (tac_, is, ptp);
492 (p, Met) => ((lev_on o lev_dn) p, Frm)(*begin script*)
493 | (p, Res) => (lev_on p,Res) (*somewhere in script*)
495 generate1 tac_ is pos pt;
496 (* tac = Rewrite ("rnorm_equation_add", "Test.rnorm_equation_add")},
497 ^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
498 "~~~~~ fun generate1, args:"; val (thy, (Rewrite' (thy',ord',rls',pa,thm',f,(f',asm))),
499 (is, ctxt), (p,p_), pt) = ((assoc_thy "Isac_Knowledge"), tac_, is, pos, pt);
500 val (pt,c) = cappend_atomic pt p (is, ContextC.insert_assumptions asm ctxt) f
501 (Rewrite thm') (f',asm) Complete;
502 (* in pt: tac = Rewrite ("rnorm_equation_add", "Test.rnorm_equation_add")},
503 ^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
504 "~~~~~ fun cappend_atomic, args:"; val (pt, p, ist_res, f, r, f', s) =
505 (pt, p, (is, ContextC.insert_assumptions asm ctxt), f, (Rewrite thm'), (f',asm), Complete);
506 existpt p pt andalso is_empty_tac (get_obj g_tac pt p) = false;
507 apfst (append_atomic p ist_res f r f' s) (cut_tree pt (p,Frm));
508 apfst : ('a -> 'b) -> 'a * 'c -> 'b * 'c;
509 (append_atomic p ist_res f r f' s) : ctree -> ctree;
511 (* HERE THE ERROR OCCURED IN THE FIRST APPROACH
512 getTactic 1 ([1,1],Frm); <ERROR> syserror in getTactic </ERROR> <<<<<=========================*)
513 "~~~~~ fun getTactic, args:"; val (cI, (p:pos')) = (1, ([1,1],Frm));
514 val ((pt,_),_) = get_calc cI
515 val (form, tac, asms) = pt_extract (pt, p)
517 "~~~~~ fun gettacticOK2xml, args:"; val ((cI:calcID), tac) = (cI, ta);
519 "~~~~~ fun tac2xml, args:"; val (j, (Rewrite thm')) = (i, tac);
520 "~~~~~ fun thm'2xml, args:"; val (j, ((ID, form) : thm'')) = ((j+i), thm');
521 ID = "rnorm_equation_add";
522 @{thm rnorm_equation_add};
523 (term2str o Thm.prop_of) form = "~ ?b =!= 0 ==> (?a = ?b) = (?a + -1 * ?b = 0)"
524 (*?!? should be "\<not> ?b =!= 0 \<Longrightarrow> (?a = ?b) = (?a + -1 * ?b = 0)"*)
525 (*thmstr2xml (j+i) form;
526 ERROR Undeclared constant: "Test.rnorm_equation_add" ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
530 (([], Frm), solve (x + 1 = 2, x)),
531 (([1], Frm), x + 1 = 2),
532 (([1,1], Frm), x + 1 = 2),
533 (([1,1], Res), x + 1 + -1 * 2 = 0),
534 (([1], Res), x + 1 + -1 * 2 = 0),
535 (([2], Res), -1 + x = 0)]
537 pt; --> tac = Rewrite ("rnorm_equation_add", "Test.rnorm_equation_add")*)
538 ( *----- outcommented during cleanup of args in lucas-interpreter.sml ------------------------//*)
540 "----------- improved fun getTactic for interSteps and numeral calculations --";
541 "----------- improved fun getTactic for interSteps and numeral calculations --";
542 "----------- improved fun getTactic for interSteps and numeral calculations --";
543 reset_states (); val cI = 1;
544 CalcTree [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
545 ("Test",["sqroot-test","univariate","equation","test"],["Test","squ-equ-test-subpbl1"]))];
547 autoCalculate 1 CompleteCalcHead;
548 autoCalculate 1 (Steps 1);
550 val cs = get_calc cI (* we improve from the calcstate here [*] *);
551 val pos as (_,p_) = get_pos cI 1 (* we improve from the calcstate here [*] *);
553 appendFormula 1 "x + 4 + -3 = 2" (*|> Future.join*);
554 interSteps 1 ([1],Res); (* already done by appendFormula, now showed to frontend *)
555 getTactic 1 ([1,1], Res);
556 (*<ID> sym_#add_Float ((~3,0), (0,0)) __ ((4,0), (0,0)) </ID> <<<<<================== to improve
557 <ISA> 1 + x = -3 + (4 + x) </ISA>*)
559 val ((pt''',p'''), tacis''') = get_calc cI;
562 (([], Frm), solve (x + 1 = 2, x)),
563 (([1], Frm), x + 1 = 2),
564 (([1,1], Frm), x + 1 = 2),
565 (([1,1], Res), 1 + x = 2),
566 (([1,2], Res), -3 + (4 + x) = 2),
567 (([1,3], Res), -3 + (x + 4) = 2),
568 (([1,4], Res), x + 4 + -3 = 2),
569 (([1], Res), x + 4 + -3 = 2)]*)
571 "~~~~~ fun appendFormula', args:"; val (cI, ifo) = (1, "x + 4 + -3 = 2");
572 (* val cs = get_calc cI (* we improve from the calcstate here [*] *);
573 val pos as (_,p_) = get_pos cI 1 (* we improve from the calcstate here [*] *);*)
574 val ("ok", cs' as (_, _, ptp')) = Step.do_next pos cs;
575 (*val ("ok", (_, c, ptp as (_,p))) = *)Step_Solve.by_term ptp' (encode ifo);
576 "~~~~~ fun Step_Solve.by_term , args:"; val (cs as (_, _, ptp as (pt, pos as (p, p_))), istr) =
578 val SOME f_in = parse (assoc_thy "Isac_Knowledge") istr
579 val f_in = Thm.term_of f_in
580 val f_succ = get_curr_formula (pt, pos);
581 f_succ = f_in = false;
582 val NONE = cas_input f_in
583 val pos_pred = lev_back' pos
584 (* f_pred ---"step pos cs"---> f_succ in appendFormula *)
585 val f_pred = get_curr_formula (pt, pos_pred);
586 (*val msg_calcstate' = *)compare_step ([], [], (pt, pos_pred)) f_in (*<<=====*);
587 "~~~~~ fun compare_step, args:"; val (((tacis, c, ptp as (pt, pos as (p,p_)))), ifo) =
588 (([], [], (pt, pos_pred)), f_in);
591 Frm => get_obj g_form pt p
592 | Res => (fst o (get_obj g_result pt)) p
593 | _ => e_term (*on PblObj is fo <> ifo*);
594 val {nrls, ...} = get_met (get_obj g_metID pt (par_pblobj pt p))
595 val {rew_ord, erls, rules, ...} = rep_rls nrls;
596 (*val (found, der) = *)concat_deriv rew_ord erls rules fo ifo; (*<---------------*)
597 "~~~~~ fun concat_deriv, args:"; val (rew_ord, erls, rules, fo, ifo) =
598 (rew_ord, erls, rules, fo, ifo);
599 fun derivat ([]:(term * rule * (term * term list)) list) = e_term
600 | derivat dt = (#1 o #3 o last_elem) dt
601 fun equal (_,_,(t1, _)) (_,_,(t2, _)) = t1=t2
602 (*val fod = *)make_deriv (Isac"") erls rules (snd rew_ord) NONE fo;
603 (*val ifod = *)make_deriv (Isac"") erls rules (snd rew_ord) NONE ifo;