| changeset 59921 | 0766dade4a78 |
| parent 59920 | 33913fe24685 |
| child 59932 | 87336f3b021f |
| 59920:33913fe24685 | 59921:0766dade4a78 |
|---|---|
188 = "Pstate ([\"\n(e_e, 1 + -1 * 2 + x = 0)\",\"\n(v_v, x)\"], [R,L,R,L,R,L,R], empty, SOME e_e, \nx = 0 + -1 * (1 + -1 * 2), ORundef, true, true)" |
188 = "Pstate ([\"\n(e_e, 1 + -1 * 2 + x = 0)\",\"\n(v_v, x)\"], [R,L,R,L,R,L,R], empty, SOME e_e, \nx = 0 + -1 * (1 + -1 * 2), ORundef, true, true)" |
189 then () else error "from Step.by_tactic return --- changed 2"; |
189 then () else error "from Step.by_tactic return --- changed 2"; |
190 (*\\******************* Step.by_tactic returns tac_ + istate + cstate *****************************//*) |
190 (*\\******************* Step.by_tactic returns tac_ + istate + cstate *****************************//*) |
191 |
191 |
192 "~~~~~ fun Step.by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt'''''_', ip'''''_')); |
192 "~~~~~ fun Step.by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt'''''_', ip'''''_')); |
193 val Applicable.Yes m = (*case*) ApplicableOLD.applicable_in p pt tac (*of*); |
193 val Applicable.Yes m = (*case*) Step.check tac (pt, p) (*of*); |
194 (*if*) Tactic.for_specify' m; (*false*) |
194 (*if*) Tactic.for_specify' m; (*false*) |
195 |
195 |
196 Step_Solve.by_tactic m (pt, p); |
196 Step_Solve.by_tactic m (pt, p); |
197 "~~~~~ fun by_tactic , args:"; val (m, (pt, po as (p, p_))) = (m, (pt, p)); |
197 "~~~~~ fun by_tactic , args:"; val (m, (pt, po as (p, p_))) = (m, (pt, p)); |
198 (*if*) Method.id_empty = get_obj g_metID pt (par_pblobj pt p); (*else*) |
198 (*if*) Method.id_empty = get_obj g_metID pt (par_pblobj pt p); (*else*) |
306 refFormula 1 (get_pos 1 1); |
306 refFormula 1 (get_pos 1 1); |
307 fetchProposedTactic 1; |
307 fetchProposedTactic 1; |
308 setNextTactic 1 (Model_Problem); |
308 setNextTactic 1 (Model_Problem); |
309 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*gets ModSpec;model is still empty*) |
309 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*gets ModSpec;model is still empty*) |
310 |
310 |
311 fetchProposedTactic 1; |
311 fetchProposedTactic 1; (*<SYSERROR><CALCID>1</CALCID><ERROR>error in kernel 3</ERROR></SYSERROR>* ) |
312 setNextTactic 1 (Add_Given "equality (x + 1 = 2)"); |
312 setNextTactic 1 (Add_Given "equality (x + 1 = 2)"); |
313 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1); |
313 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1); |
314 |
314 |
315 fetchProposedTactic 1; |
315 fetchProposedTactic 1; |
316 setNextTactic 1 (Add_Given "solveFor x"); |
316 setNextTactic 1 (Add_Given "solveFor x"); |
411 val ip = get_pos 1 1; |
411 val ip = get_pos 1 1; |
412 val (Form f, tac, asms) = pt_extract (pt, ip); |
412 val (Form f, tac, asms) = pt_extract (pt, ip); |
413 (*exception just above means: 'ModSpec' has been returned: error anyway*) |
413 (*exception just above means: 'ModSpec' has been returned: error anyway*) |
414 if UnparseC.term f = "[x = 1]" then () else |
414 if UnparseC.term f = "[x = 1]" then () else |
415 error "FE-interface.sml: diff.behav. in miniscript with mini-subpb"; |
415 error "FE-interface.sml: diff.behav. in miniscript with mini-subpb"; |
416 (**)-------------------------------------------------------------------------------------------*) |
|
416 DEconstrCalcTree 1; |
417 DEconstrCalcTree 1; |
417 |
418 |
418 "--------- mini-subpbl AUTOCALCULATE Steps 1 -------------"; |
419 "--------- mini-subpbl AUTOCALCULATE Steps 1 -------------"; |
419 "--------- mini-subpbl AUTOCALCULATE Steps 1 -------------"; |
420 "--------- mini-subpbl AUTOCALCULATE Steps 1 -------------"; |
420 "--------- mini-subpbl AUTOCALCULATE Steps 1 -------------"; |
421 "--------- mini-subpbl AUTOCALCULATE Steps 1 -------------"; |
831 autoCalculate 1 (Steps 1); |
832 autoCalculate 1 (Steps 1); |
832 (*WN050904 fetchProposedTactic again --> Specify_Problem ["normalise",... |
833 (*WN050904 fetchProposedTactic again --> Specify_Problem ["normalise",... |
833 and Specify_Theory skipped in comparison to below ---^^^-inserted *) |
834 and Specify_Theory skipped in comparison to below ---^^^-inserted *) |
834 (*------------vvv-inserted-----------------------------------------------*) |
835 (*------------vvv-inserted-----------------------------------------------*) |
835 fetchProposedTactic 1; |
836 fetchProposedTactic 1; |
837 (*/-----ERROR INTRODUCED BY CHILD OF 33913fe24685 --------------------------------------------\* ) |
|
836 setNextTactic 1 (Specify_Problem ["normalise","polynomial", |
838 setNextTactic 1 (Specify_Problem ["normalise","polynomial", |
837 "univariate","equation"]); |
839 "univariate","equation"]); |
838 autoCalculate 1 (Steps 1); |
840 autoCalculate 1 (Steps 1); |
839 |
841 |
840 (*and Specify_Theory skipped by fetchProposedTactic ?!?*) |
842 (*and Specify_Theory skipped by fetchProposedTactic ?!?*) |
876 val p = get_pos 1 1; |
878 val p = get_pos 1 1; |
877 val (Form f, tac, asms) = pt_extract (pt, p); |
879 val (Form f, tac, asms) = pt_extract (pt, p); |
878 if UnparseC.term f = "[x = -1, x = -3]" andalso p = ([], Res) then () else |
880 if UnparseC.term f = "[x = -1, x = -3]" andalso p = ([], Res) then () else |
879 error "FE-interface.sml: diff.behav. in tryMatchProblem, tryRefine"; |
881 error "FE-interface.sml: diff.behav. in tryMatchProblem, tryRefine"; |
880 DEconstrCalcTree 1; |
882 DEconstrCalcTree 1; |
883 ( *\-----ERROR INTRODUCED BY CHILD OF 33913fe24685 --------------------------------------------/*) |
|
881 |
884 |
882 "--------- modifyCalcHead, resetCalcHead, modelProblem --"; |
885 "--------- modifyCalcHead, resetCalcHead, modelProblem --"; |
883 "--------- modifyCalcHead, resetCalcHead, modelProblem --"; |
886 "--------- modifyCalcHead, resetCalcHead, modelProblem --"; |
884 "--------- modifyCalcHead, resetCalcHead, modelProblem --"; |
887 "--------- modifyCalcHead, resetCalcHead, modelProblem --"; |
885 reset_states (); |
888 reset_states (); |