7 "--------- solve_linear as rootpbl AUTOCALCULATE CompleteCalcHead-"; |
7 "--------- solve_linear as rootpbl AUTOCALCULATE CompleteCalcHead-"; |
8 "--------- maximum-example: complete_metitms ---------------------"; |
8 "--------- maximum-example: complete_metitms ---------------------"; |
9 "--------- maximum-example: complete_mod -------------------------"; |
9 "--------- maximum-example: complete_mod -------------------------"; |
10 "appendForm with miniscript with mini-subpbl:"; |
10 "appendForm with miniscript with mini-subpbl:"; |
11 "--------- appendFormula: on Res + equ_nrls ----------------------"; |
11 "--------- appendFormula: on Res + equ_nrls ----------------------"; |
12 "--------- appendFormula: on Frm + equ_nrls ----------------------X"; |
12 "--------- appendFormula: on Frm + equ_nrls ----------------------"; |
13 "--------- appendFormula: on Res + NO deriv ----------------------"; |
13 "--------- appendFormula: on Res + NO deriv ----------------------"; |
14 "--------- appendFormula: on Res + late deriv --------------------"; |
14 "--------- appendFormula: on Res + late deriv --------------------"; |
15 "--------- appendFormula: on Res + late deriv [x = 3 + -2]---///--"; |
15 "--------- appendFormula: on Res + late deriv [x = 3 + -2]---///--"; |
16 "replaceForm with miniscript with mini-subpbl:"; |
16 "replaceForm with miniscript with mini-subpbl:"; |
17 "--------- replaceFormula: on Res + = ----------------------------"; |
17 "--------- replaceFormula: on Res + = ----------------------------"; |
18 "--------- replaceFormula: on Res + = 1st Nd ---------------------X"; |
18 "--------- replaceFormula: on Res + = 1st Nd ---------------------"; |
19 "--------- replaceFormula: on Frm + = 1st Nd ---------------------"; |
19 "--------- replaceFormula: on Frm + = 1st Nd ---------------------"; |
20 "--------- replaceFormula: cut calculation -----------------------X"; |
20 "--------- replaceFormula: cut calculation -----------------------"; |
21 |
21 |
22 |
22 |
23 |
23 |
24 |
24 |
25 "--------- solve_linear as rootpbl AUTOCALCULATE CompleteModel ---"; |
25 "--------- solve_linear as rootpbl AUTOCALCULATE CompleteModel ---"; |
307 ["sqroot-test","univariate","equation","test"], |
307 ["sqroot-test","univariate","equation","test"], |
308 ["Test","squ-equ-test-subpbl1"]))]; |
308 ["Test","squ-equ-test-subpbl1"]))]; |
309 Iterator 1; moveActiveRoot 1; |
309 Iterator 1; moveActiveRoot 1; |
310 autoCalculate 1 CompleteCalcHead; |
310 autoCalculate 1 CompleteCalcHead; |
311 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1) (*x + 1 = 2*); |
311 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1) (*x + 1 = 2*); |
312 (*> ###generate1 Apply_Method': pos = ([1], Frm) |
312 |
313 ###generate1 Apply_Method': topt= Some x + 1 = 2 |
|
314 ###generate1 Apply_Method': is = ScrState ([" |
|
315 (e_, x + 1 = 2)"," |
|
316 (v_, x)"], |
|
317 [], None, |
|
318 ??.empty, Safe, true) |
|
319 ##@cappend_form: pos =[1] |
|
320 ##@cappend_form before cut_tree: loc =ScrState ([" |
|
321 (e_, x + 1 = 2)"," |
|
322 (v_, x)"], |
|
323 [], None, |
|
324 ??.empty, Safe, true) |
|
325 ##@append_form: pos =[1] |
|
326 ##@cappend_form after append: loc =(#Some ScrState ([" |
|
327 (e_, x + 1 = 2)"," |
|
328 (v_, x)"], |
|
329 [], None, |
|
330 ??.empty, Safe, true), |
|
331 #None) |
|
332 ###generate1 Apply_Method: after cappend |
|
333 *) |
|
334 appendFormula 1 "2+ -1 + x = 2"; refFormula 1 (get_pos 1 1); |
313 appendFormula 1 "2+ -1 + x = 2"; refFormula 1 (get_pos 1 1); |
335 (**)@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@;(**) |
|
336 (* |
|
337 > appendFormula 1 "2+ -1 + x = 2"; |
|
338 ###generate1 Rewrite_Set': pos= ([1], Frm) |
|
339 ##@cappend_atomic: pos =[1] |
|
340 ##@cappend_atomic before cut_tree: loc =ScrState ([" |
|
341 (e_, x + 1 = 2)"," |
|
342 (v_, x)"], |
|
343 [R,L,R,L,L,R,R], Some e_, |
|
344 x + 1 + -1 * 2 = 0, Sundef, false) |
|
345 #@append_atomic: pos =[1] |
|
346 ##@cappend_atomic after append: loc =(#None, |
|
347 #Some ScrState ([" |
|
348 (e_, x + 1 = 2)"," |
|
349 (v_, x)"], |
|
350 [R,L,R,L,L,R,R], Some e_, |
|
351 x + 1 + -1 * 2 = 0, Sundef, false)) |
|
352 Exception- Bind raised |
|
353 *) |
|
354 |
|
355 |
314 |
356 moveDown 1 ([],Pbl); refFormula 1 ([1],Frm) (*x + 1 = 2*); |
315 moveDown 1 ([],Pbl); refFormula 1 ([1],Frm) (*x + 1 = 2*); |
357 >>>>>>> 1.8 |
316 >>>>>>> 1.8 |
358 |
317 |
359 moveDown 1 ([1 ],Frm); refFormula 1 ([1,1],Frm); |
318 moveDown 1 ([1 ],Frm); refFormula 1 ([1,1],Frm); |
373 else raise error "auto-inform.sml: diff.behav.appendFormula: on Frm + equ 2"; |
332 else raise error "auto-inform.sml: diff.behav.appendFormula: on Frm + equ 2"; |
374 autoCalculate 1 CompleteCalc; |
333 autoCalculate 1 CompleteCalc; |
375 val ((pt,_),_) = get_calc 1; |
334 val ((pt,_),_) = get_calc 1; |
376 if "[x = 1]" = term2str (fst (get_obj g_result pt [])) then () |
335 if "[x = 1]" = term2str (fst (get_obj g_result pt [])) then () |
377 else raise error "auto-inform.sml: diff.behav.appendFormula: on Frm + equ 3"; |
336 else raise error "auto-inform.sml: diff.behav.appendFormula: on Frm + equ 3"; |
378 (**@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@**) |
|
379 |
|
380 |
337 |
381 |
338 |
382 "--------- appendFormula: on Res + NO deriv ----------------------"; |
339 "--------- appendFormula: on Res + NO deriv ----------------------"; |
383 "--------- appendFormula: on Res + NO deriv ----------------------"; |
340 "--------- appendFormula: on Res + NO deriv ----------------------"; |
384 "--------- appendFormula: on Res + NO deriv ----------------------"; |
341 "--------- appendFormula: on Res + NO deriv ----------------------"; |
484 replaceFormula 1 "-2 * 1 + (1 + x) = 0"; refFormula 1 (get_pos 1 1); |
441 replaceFormula 1 "-2 * 1 + (1 + x) = 0"; refFormula 1 (get_pos 1 1); |
485 val ((pt,_),_) = get_calc 1; |
442 val ((pt,_),_) = get_calc 1; |
486 val str = pr_ptree pr_short pt; |
443 val str = pr_ptree pr_short pt; |
487 writeln str; |
444 writeln str; |
488 if str=". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + -1 * 2 = 0\n2.1. x + 1 + -1 * 2 = 0\n2.2. -1 * 2 + (x + 1) = 0\n2.3. -1 * 2 + (1 + x) = 0\n2.4. 1 + (-1 * 2 + x) = 0\n2.5. 1 + (-2 + x) = 0\n2.6. 1 + (-2 * 1 + x) = 0\n" then() |
445 if str=". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + -1 * 2 = 0\n2.1. x + 1 + -1 * 2 = 0\n2.2. -1 * 2 + (x + 1) = 0\n2.3. -1 * 2 + (1 + x) = 0\n2.4. 1 + (-1 * 2 + x) = 0\n2.5. 1 + (-2 + x) = 0\n2.6. 1 + (-2 * 1 + x) = 0\n" then() |
489 else raise error "auto-inform.sml: diff.behav.replaceFormula: on Res + = 1"; |
446 else raise error "auto-inform.sml: diff.behav.replaceFormula: on Res += 1"; |
490 autoCalculate 1 CompleteCalc; |
447 autoCalculate 1 CompleteCalc; |
491 val ((pt,pos as(p,_)),_) = get_calc 1; |
448 val ((pt,pos as(p,_)),_) = get_calc 1; |
492 if pos=([],Res)andalso"[x = 1]"=(term2str o fst)(get_obj g_result pt p)then() |
449 if pos=([],Res)andalso"[x = 1]"=(term2str o fst)(get_obj g_result pt p)then() |
493 else raise error "auto-inform.sml: diff.behav.replaceFormula: on Res + = 2"; |
450 else raise error "auto-inform.sml: diff.behav.replaceFormula: on Res + = 2"; |
494 |
451 |
495 |
452 |
496 "--------- replaceFormula: on Res + = 1st Nd ---------------------"; |
453 "--------- replaceFormula: on Res + = 1st Nd ---------------------"; |
497 "--------- replaceFormula: on Res + = 1st Nd ---------------------"; |
454 "--------- replaceFormula: on Res + = 1st Nd ---------------------"; |
498 "--------- replaceFormula: on Res + = 1st Nd ---------------------"; |
455 "--------- replaceFormula: on Res + = 1st Nd ---------------------"; |
499 (**@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@(**) |
|
500 states:=[]; |
456 states:=[]; |
501 CalcTree [(["equality (x+1=2)", "solveFor x","solutions L"], |
457 CalcTree [(["equality (x+1=2)", "solveFor x","solutions L"], |
502 ("Test.thy", |
458 ("Test.thy", |
503 ["sqroot-test","univariate","equation","test"], |
459 ["sqroot-test","univariate","equation","test"], |
504 ["Test","squ-equ-test-subpbl1"]))]; |
460 ["Test","squ-equ-test-subpbl1"]))]; |
515 else raise error "auto-inform.sml: diff.behav.replaceFormula: on Res 1 + = 1"; |
471 else raise error "auto-inform.sml: diff.behav.replaceFormula: on Res 1 + = 1"; |
516 autoCalculate 1 CompleteCalc; |
472 autoCalculate 1 CompleteCalc; |
517 val ((pt,pos as(p,_)),_) = get_calc 1; |
473 val ((pt,pos as(p,_)),_) = get_calc 1; |
518 if pos=([],Res)andalso"[x = 1]"=(term2str o fst)(get_obj g_result pt p)then() |
474 if pos=([],Res)andalso"[x = 1]"=(term2str o fst)(get_obj g_result pt p)then() |
519 else raise error "auto-inform.sml: diff.behav.replaceFormula: on Res + = 2"; |
475 else raise error "auto-inform.sml: diff.behav.replaceFormula: on Res + = 2"; |
520 (**)@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@**) |
|
521 |
476 |
522 |
477 |
523 "--------- replaceFormula: on Frm + = 1st Nd ---------------------"; |
478 "--------- replaceFormula: on Frm + = 1st Nd ---------------------"; |
524 "--------- replaceFormula: on Frm + = 1st Nd ---------------------"; |
479 "--------- replaceFormula: on Frm + = 1st Nd ---------------------"; |
525 "--------- replaceFormula: on Frm + = 1st Nd ---------------------"; |
480 "--------- replaceFormula: on Frm + = 1st Nd ---------------------"; |
545 |
500 |
546 |
501 |
547 "--------- replaceFormula: cut calculation -----------------------"; |
502 "--------- replaceFormula: cut calculation -----------------------"; |
548 "--------- replaceFormula: cut calculation -----------------------"; |
503 "--------- replaceFormula: cut calculation -----------------------"; |
549 "--------- replaceFormula: cut calculation -----------------------"; |
504 "--------- replaceFormula: cut calculation -----------------------"; |
550 (**@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@(**) |
|
551 states:=[]; |
505 states:=[]; |
552 CalcTree [(["equality (x+1=2)", "solveFor x","solutions L"], |
506 CalcTree [(["equality (x+1=2)", "solveFor x","solutions L"], |
553 ("Test.thy", |
507 ("Test.thy", |
554 ["sqroot-test","univariate","equation","test"], |
508 ["sqroot-test","univariate","equation","test"], |
555 ["Test","squ-equ-test-subpbl1"]))]; |
509 ["Test","squ-equ-test-subpbl1"]))]; |