314 setNextTactic 1 (Check_Postcond |
314 setNextTactic 1 (Check_Postcond |
315 ["sqroot-test","univariate","equation","test"]); |
315 ["sqroot-test","univariate","equation","test"]); |
316 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); |
316 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); |
317 |
317 |
318 val ((pt,_),_) = get_calc 1; |
318 val ((pt,_),_) = get_calc 1; |
319 val str = pr_ptree pr_short pt; |
319 val str = pr_ctree pr_short pt; |
320 writeln str; |
320 writeln str; |
321 val ip = get_pos 1 1; |
321 val ip = get_pos 1 1; |
322 val (Form f, tac, asms) = pt_extract (pt, ip); |
322 val (Form f, tac, asms) = pt_extract (pt, ip); |
323 (*exception just above means: 'ModSpec' has been returned: error anyway*) |
323 (*exception just above means: 'ModSpec' has been returned: error anyway*) |
324 if term2str f = "[x = 1]" then () else |
324 if term2str f = "[x = 1]" then () else |
555 ["Test","squ-equ-test-subpbl1"]))]; |
555 ["Test","squ-equ-test-subpbl1"]))]; |
556 Iterator 1; moveActiveRoot 1; |
556 Iterator 1; moveActiveRoot 1; |
557 autoCalculate 1 CompleteToSubpbl; |
557 autoCalculate 1 CompleteToSubpbl; |
558 refFormula 1 (get_pos 1 1); (*<ISA> -1 + x = 0 </ISA>*); |
558 refFormula 1 (get_pos 1 1); (*<ISA> -1 + x = 0 </ISA>*); |
559 val ((pt,_),_) = get_calc 1; |
559 val ((pt,_),_) = get_calc 1; |
560 val str = pr_ptree pr_short pt; |
560 val str = pr_ctree pr_short pt; |
561 writeln str; |
561 writeln str; |
562 if str = ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + -1 * 2 = 0\n" |
562 if str = ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + -1 * 2 = 0\n" |
563 then () else |
563 then () else |
564 error "FE-interface.sml: diff.behav. in mini-subpbl CompleteToSubpbl-1"; |
564 error "FE-interface.sml: diff.behav. in mini-subpbl CompleteToSubpbl-1"; |
565 |
565 |
566 autoCalculate 1 (Step 1); (*proceeds only, of NOT 1 step before subplb*) |
566 autoCalculate 1 (Step 1); (*proceeds only, of NOT 1 step before subplb*) |
567 autoCalculate 1 CompleteToSubpbl; |
567 autoCalculate 1 CompleteToSubpbl; |
568 val ((pt,_),_) = get_calc 1; |
568 val ((pt,_),_) = get_calc 1; |
569 val str = pr_ptree pr_short pt; |
569 val str = pr_ctree pr_short pt; |
570 writeln str; |
570 writeln str; |
571 autoCalculate 1 CompleteCalc; (*das geht ohnehin !*); |
571 autoCalculate 1 CompleteCalc; (*das geht ohnehin !*); |
572 val ((pt,_),_) = get_calc 1; |
572 val ((pt,_),_) = get_calc 1; |
573 val p = get_pos 1 1; |
573 val p = get_pos 1 1; |
574 |
574 |