138 fetchProposedTactic 1; |
138 fetchProposedTactic 1; |
139 (*========== inhibit exn 110310 ================================================ |
139 (*========== inhibit exn 110310 ================================================ |
140 val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1; |
140 val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1; |
141 |
141 |
142 setNextTactic 1 (Apply_Method ["Test","solve_linear"]); |
142 setNextTactic 1 (Apply_Method ["Test","solve_linear"]); |
|
143 (*ERROR.110620 <SETNEXTTACTIC>..<MESSAGE> end-of-calculation*) |
143 val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1; |
144 val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1; |
144 is_complete_mod ptp; |
145 is_complete_mod ptp; |
145 is_complete_spec ptp; |
146 is_complete_spec ptp; |
146 |
147 |
147 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); |
148 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); |
165 val ip = get_pos 1 1; |
166 val ip = get_pos 1 1; |
166 val (Form f, tac, asms) = pt_extract (pt, ip); |
167 val (Form f, tac, asms) = pt_extract (pt, ip); |
167 (*exception just above means: 'ModSpec' has been returned: error anyway*) |
168 (*exception just above means: 'ModSpec' has been returned: error anyway*) |
168 if term2str f = "[x = 1]" then () else |
169 if term2str f = "[x = 1]" then () else |
169 error "FE-Kernel-interface.sml: diff.behav. in solve_linear as rootpbl"; |
170 error "FE-Kernel-interface.sml: diff.behav. in solve_linear as rootpbl"; |
170 |
171 ============ inhibit exn 110310 ==============================================*) |
171 |
172 |
|
173 (*========== inhibit exn 110620 ================================================ |
172 "--------- inspect the CalcTree No.1 with Iterator No.2 -"; |
174 "--------- inspect the CalcTree No.1 with Iterator No.2 -"; |
173 "--------- inspect the CalcTree No.1 with Iterator No.2 -"; |
175 "--------- inspect the CalcTree No.1 with Iterator No.2 -"; |
174 "--------- inspect the CalcTree No.1 with Iterator No.2 -"; |
176 "--------- inspect the CalcTree No.1 with Iterator No.2 -"; |
175 (*WN041118: inspection shifted to Iterator No.1, because others need pos'*) |
177 (*WN041118: inspection shifted to Iterator No.1, because others need pos'*) |
176 moveActiveRoot 1; |
178 moveActiveRoot 1; |
189 error "FE-interface.sml: diff.behav. in a inspect 1 with Iterator 2"; |
191 error "FE-interface.sml: diff.behav. in a inspect 1 with Iterator 2"; |
190 moveActiveDown 1; refFormula 1 ([], Res); |
192 moveActiveDown 1; refFormula 1 ([], Res); |
191 if get_pos 1 1 = ([], Res) then () else |
193 if get_pos 1 1 = ([], Res) then () else |
192 error "FE-interface.sml: diff.behav. in b inspect 1 with Iterator 2"; |
194 error "FE-interface.sml: diff.behav. in b inspect 1 with Iterator 2"; |
193 moveActiveCalcHead 1; refFormula 1 ([],Pbl); |
195 moveActiveCalcHead 1; refFormula 1 ([],Pbl); |
194 |
196 ============ inhibit exn 110620 ==============================================*) |
195 |
197 |
196 "--------- miniscript with mini-subpbl ------------------"; |
198 "--------- miniscript with mini-subpbl ------------------"; |
197 "--------- miniscript with mini-subpbl ------------------"; |
199 "--------- miniscript with mini-subpbl ------------------"; |
198 "--------- miniscript with mini-subpbl ------------------"; |
200 "--------- miniscript with mini-subpbl ------------------"; |
199 states:=[]; (*start of calculation, return No.1*) |
201 states:=[]; (*start of calculation, return No.1*) |
314 if term2str f = "[x = 1]" then () else |
316 if term2str f = "[x = 1]" then () else |
315 error "FE-interface.sml: diff.behav. in miniscript with mini-subpb"; |
317 error "FE-interface.sml: diff.behav. in miniscript with mini-subpb"; |
316 |
318 |
317 DEconstrCalcTree 1; |
319 DEconstrCalcTree 1; |
318 |
320 |
319 |
|
320 "--------- mini-subpbl AUTOCALCULATE Step 1 -------------"; |
321 "--------- mini-subpbl AUTOCALCULATE Step 1 -------------"; |
321 "--------- mini-subpbl AUTOCALCULATE Step 1 -------------"; |
322 "--------- mini-subpbl AUTOCALCULATE Step 1 -------------"; |
322 "--------- mini-subpbl AUTOCALCULATE Step 1 -------------"; |
323 "--------- mini-subpbl AUTOCALCULATE Step 1 -------------"; |
323 states:=[]; |
324 states:=[]; |
324 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], |
325 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], |
367 if term2str f = "[x = 1]" andalso p = ([], Res) then () else |
368 if term2str f = "[x = 1]" andalso p = ([], Res) then () else |
368 error "FE-interface.sml: diff.behav. in miniscript with mini-subpb"; |
369 error "FE-interface.sml: diff.behav. in miniscript with mini-subpb"; |
369 |
370 |
370 DEconstrCalcTree 1; |
371 DEconstrCalcTree 1; |
371 |
372 |
|
373 (*========== inhibit exn 110620 ================================================ |
372 "--------- solve_linear as rootpbl AUTO CompleteCalc ----"; |
374 "--------- solve_linear as rootpbl AUTO CompleteCalc ----"; |
373 "--------- solve_linear as rootpbl AUTO CompleteCalc ----"; |
375 "--------- solve_linear as rootpbl AUTO CompleteCalc ----"; |
374 "--------- solve_linear as rootpbl AUTO CompleteCalc ----"; |
376 "--------- solve_linear as rootpbl AUTO CompleteCalc ----"; |
375 states:=[]; |
377 states:=[]; |
376 CalcTree |
378 CalcTree |
390 val p = get_pos 1 1; |
392 val p = get_pos 1 1; |
391 val (Form f, tac, asms) = pt_extract (pt, p); |
393 val (Form f, tac, asms) = pt_extract (pt, p); |
392 if term2str f = "[x = 1]" andalso p = ([], Res) then () else |
394 if term2str f = "[x = 1]" andalso p = ([], Res) then () else |
393 error "FE-interface.sml: diff.behav. in solve_linear/rt AUTOCALCULATE "; |
395 error "FE-interface.sml: diff.behav. in solve_linear/rt AUTOCALCULATE "; |
394 |
396 |
395 |
|
396 "--------- solve_linear as rootpbl AUTO CompleteHead/Calc "; |
397 "--------- solve_linear as rootpbl AUTO CompleteHead/Calc "; |
397 "--------- solve_linear as rootpbl AUTO CompleteHead/Calc "; |
398 "--------- solve_linear as rootpbl AUTO CompleteHead/Calc "; |
398 "--------- solve_linear as rootpbl AUTO CompleteHead/Calc "; |
399 "--------- solve_linear as rootpbl AUTO CompleteHead/Calc "; |
399 states:=[]; |
400 states:=[]; |
400 CalcTree |
401 CalcTree |
406 moveActiveRoot 1; |
407 moveActiveRoot 1; |
407 autoCalculate 1 CompleteCalcHead; |
408 autoCalculate 1 CompleteCalcHead; |
408 refFormula 1 (get_pos 1 1); |
409 refFormula 1 (get_pos 1 1); |
409 val ((pt,p),_) = get_calc 1; |
410 val ((pt,p),_) = get_calc 1; |
410 |
411 |
411 |
|
412 |
|
413 autoCalculate 1 CompleteCalc; |
412 autoCalculate 1 CompleteCalc; |
414 val ((pt,p),_) = get_calc 1; |
413 val ((pt,p),_) = get_calc 1; |
415 if p=([], Res) then () else |
414 if p=([], Res) then () else |
416 error "FE-interface.sml: diff.behav. in solve_linear AUTOC Head/Calc "; |
415 error "FE-interface.sml: diff.behav. in solve_linear AUTOC Head/Calc "; |
417 |
416 ============ inhibit exn 110620 ==============================================*) |
418 |
417 |
419 "--------- mini-subpbl AUTOCALCULATE CompleteCalc -------"; |
418 "--------- mini-subpbl AUTOCALCULATE CompleteCalc -------"; |
420 "--------- mini-subpbl AUTOCALCULATE CompleteCalc -------"; |
419 "--------- mini-subpbl AUTOCALCULATE CompleteCalc -------"; |
421 "--------- mini-subpbl AUTOCALCULATE CompleteCalc -------"; |
420 "--------- mini-subpbl AUTOCALCULATE CompleteCalc -------"; |
422 states:=[]; |
421 states:=[]; |
439 getFormulaeFromTo 1 unc gen 1 (*only level 1*) false; |
438 getFormulaeFromTo 1 unc gen 1 (*only level 1*) false; |
440 getFormulaeFromTo 1 unc gen 99999 (*all levels*) false; |
439 getFormulaeFromTo 1 unc gen 99999 (*all levels*) false; |
441 |
440 |
442 val ((pt,_),_) = get_calc 1; |
441 val ((pt,_),_) = get_calc 1; |
443 val p = get_pos 1 1; |
442 val p = get_pos 1 1; |
444 val (Form f, tac, asms) = pt_extract (pt, p); |
443 (*========== inhibit exn 110620 ================================================ |
|
444 val (Form f, tac, asms) = pt_extract (pt, p); |
|
445 (* ModSpec........... = ...................DIFFERENT !*) |
445 if term2str f = "[x = 1]" andalso p = ([], Res) then () else |
446 if term2str f = "[x = 1]" andalso p = ([], Res) then () else |
446 error "FE-interface.sml: diff.behav. in mini-subpbl AUTOCALCULATE 6"; |
447 error "FE-interface.sml: diff.behav. in mini-subpbl AUTOCALCULATE 6"; |
447 |
448 ============ inhibit exn 110620 ==============================================*) |
448 |
449 |
|
450 |
|
451 (*=== inhibit exn ?============================================================= |
449 "--------- mini-subpbl AUTO CompleteCalcHead ------------"; |
452 "--------- mini-subpbl AUTO CompleteCalcHead ------------"; |
450 "--------- mini-subpbl AUTO CompleteCalcHead ------------"; |
453 "--------- mini-subpbl AUTO CompleteCalcHead ------------"; |
451 "--------- mini-subpbl AUTO CompleteCalcHead ------------"; |
454 "--------- mini-subpbl AUTO CompleteCalcHead ------------"; |
452 states:=[]; |
455 states:=[]; |
453 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], |
456 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], |
454 ("Test", ["sqroot-test","univariate","equation","test"], |
457 ("Test", ["sqroot-test","univariate","equation","test"], |
455 ["Test","squ-equ-test-subpbl1"]))]; |
458 ["Test","squ-equ-test-subpbl1"]))]; |
456 Iterator 1; |
459 Iterator 1; |
|
460 moveActiveRoot 1; |
457 (* doesn't terminate !!! |
461 (* doesn't terminate !!! |
458 autoCalculate 1 CompleteCalcHead; |
462 autoCalculate 1 CompleteCalcHead; |
459 *) |
463 *) |
460 |
464 |
461 "--------- solve_linear as rootpbl AUTO CompleteModel ---"; |
465 "--------- solve_linear as rootpbl AUTO CompleteModel ---"; |
1312 val p = get_pos 1 1; |
1316 val p = get_pos 1 1; |
1313 val (Form f, tac, asms) = pt_extract (pt, p); |
1317 val (Form f, tac, asms) = pt_extract (pt, p); |
1314 if term2str f = "-1 + x = 0" andalso p = ([2], Res) then () else |
1318 if term2str f = "-1 + x = 0" andalso p = ([2], Res) then () else |
1315 error "FE-interface.sml: diff.behav. in FORMULA:replace} NOTok"; |
1319 error "FE-interface.sml: diff.behav. in FORMULA:replace} NOTok"; |
1316 |
1320 |
1317 ============ inhibit exn 110310 ==============================================*) |
1321 ===== inhibit exn ?===========================================================*) |
|
1322 |