neuper@52113: (* Title: tests the interface of isac's SML-kernel in accordance to neuper@52113: java-tests/isac.bridge. neuper@52113: Author: Walther Neuper neuper@52113: (c) copyright due to lincense terms. neuper@52113: neuper@52113: WN050707 ... if true, the test ist marked with a \label referring neuper@52113: to the same UC in isac-docu.tex as the JUnit testcase. neuper@52113: WN120210?not ME: added some labels, which are not among the above, neuper@52113: repaired lost \label (s). wneuper@59127: wneuper@59127: theory Test_Some imports Build_Thydata begin wneuper@59127: ML {* KEStore_Elems.set_ref_thy @{theory}; wneuper@59127: fun autoCalculate' cI auto = autoCalculate cI auto (*|> Future.join*) *} wneuper@59127: ML_file "Frontend/use-cases.sml" neuper@52113: *) neuper@52113: neuper@52113: "--------------------------------------------------------"; neuper@52113: "table of contents --------------------------------------"; neuper@52113: "--------------------------------------------------------"; neuper@52113: "within struct ------------------------------------------"; neuper@52113: "--------------------------------------------------------"; neuper@52113: "--------- encode ^ -> ^^^ ------------------------------"; neuper@52113: "--------------------------------------------------------"; neuper@52113: "exported from struct -----------------------------------"; neuper@52113: "--------------------------------------------------------"; neuper@52113: "--------- empty rootpbl --------------------------------"; neuper@52113: "--------- solve_linear as rootpbl FE -------------------"; neuper@52113: "--------- inspect the CalcTree No.1 with Iterator No.2 -"; neuper@52113: "--------- miniscript with mini-subpbl ------------------"; neuper@52113: "--------- mini-subpbl AUTOCALCULATE Step 1 -------------"; neuper@52113: "--------- solve_linear as rootpbl AUTO CompleteCalc ----"; neuper@52113: "--------- solve_linear as rootpbl AUTO CompleteHead/Calc "; neuper@52113: "--------- mini-subpbl AUTOCALCULATE CompleteCalc -------"; neuper@52113: "--------- mini-subpbl AUTO CompleteCalcHead ------------"; neuper@52113: "--------- solve_linear as rootpbl AUTO CompleteModel ---"; neuper@52113: "--------- setContext..Thy ------------------------------"; neuper@52113: "--------- mini-subpbl AUTOCALC CompleteToSubpbl --------"; neuper@52113: "--------- rat-eq + subpbl: no_met, NO solution dropped -"; neuper@52113: "--------- tryMatchProblem, tryRefineProblem ------------"; neuper@52113: "--------- modifyCalcHead, resetCalcHead, modelProblem --"; neuper@52113: "--------- maximum-example, UC: Modeling an example -----"; neuper@52113: "--------- solve_linear from pbl-hierarchy --------------"; neuper@52113: "--------- solve_linear as in an algebra system (CAS)----"; neuper@52113: "--------- interSteps: on 'miniscript with mini-subpbl' -"; neuper@52113: "--------- getTactic, fetchApplicableTactics ------------"; neuper@52113: "--------- getAssumptions, getAccumulatedAsms -----------"; neuper@52113: "--------- arbitrary combinations of steps --------------"; neuper@52113: "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}right"; neuper@52113: "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}other"; neuper@52113: "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}oth 2"; neuper@52113: "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}NOTok"; neuper@52113: "--------- replaceFormula {SOL:MAN:FOR:replace} right----"; neuper@52113: "--------- replaceFormula {SOL:MAN:FOR:replace} other----"; neuper@52113: "--------- replaceFormula {SOL:MAN:FOR:replace} other 2--"; neuper@52113: "--------- replaceFormula {SOL:MAN:FOR:replace} NOTok----"; neuper@52113: "--------- UC errpat chain-rule-diff-both, fillpat by input ------"; neuper@52113: "--------- UC errpat add-fraction, fillpat by input --------------"; neuper@52113: "--------- UC errpat, fillpat step to Rewrite --------------------"; neuper@52113: "--------- UC errpat, fillpat step to Rewrite_Set ----------------"; neuper@52113: "--------------------------------------------------------"; neuper@52113: neuper@52113: "within struct ---------------------------------------------------"; neuper@52113: "within struct ---------------------------------------------------"; neuper@52113: "within struct ---------------------------------------------------"; neuper@52113: (*================================================================== neuper@52113: neuper@52113: neuper@52113: "--------- encode ^ -> ^^^ ------------------------------"; neuper@52113: "--------- encode ^ -> ^^^ ------------------------------"; neuper@52113: "--------- encode ^ -> ^^^ ------------------------------"; neuper@52113: if encode "a^2+b^2=c^2" = "a^^^2+b^^^2=c^^^2" then () neuper@52113: else error "interface.sml: diff.behav. in encode ^ -> ^^^ "; neuper@52113: neuper@52113: if (decode o encode) "a^2+b^2=c^2" = "a^2+b^2=c^2" then () neuper@52113: else error "interface.sml: diff.behav. in de/encode ^ <-> ^^^ "; neuper@52113: neuper@52113: ==================================================================*) neuper@52113: "exported from struct --------------------------------------------"; neuper@52113: "exported from struct --------------------------------------------"; neuper@52113: "exported from struct --------------------------------------------"; neuper@52113: neuper@52113: neuper@52113: (*------------ set at startup of the Kernel ----------------------*) wneuper@59253: reset_states (); (*resets all state information in Kernel *) neuper@52113: (*----------------------------------------------------------------*) neuper@52113: neuper@52113: "--------- empty rootpbl --------------------------------"; neuper@52113: "--------- empty rootpbl --------------------------------"; neuper@52113: "--------- empty rootpbl --------------------------------"; neuper@52113: CalcTree [([], ("", [], []))]; neuper@52113: Iterator 1; neuper@52113: moveActiveRoot 1; neuper@52113: refFormula 1 (get_pos 1 1); neuper@52113: (*WN.040222: stoert das sehr, dass e_domID etc. statt leer kommt ???*) neuper@52113: DEconstrCalcTree 1; neuper@52113: neuper@52113: "--------- solve_linear as rootpbl FE -------------------"; neuper@52113: "--------- solve_linear as rootpbl FE -------------------"; neuper@52113: "--------- solve_linear as rootpbl FE -------------------"; neuper@52113: CalcTree (*start of calculation, return No.1*) neuper@52113: [(["equality (1+-1*2+x=(0::real))", "solveFor x","solutions L"], neuper@52113: ("Test", neuper@55279: ["LINEAR","univariate","equation","test"], neuper@52113: ["Test","solve_linear"]))]; neuper@52113: Iterator 1; (*create an active Iterator on CalcTree No.1*) neuper@52113: neuper@52113: moveActiveRoot 1;(*sets the CalcIterator No.1 at the root of CalcTree No.1*); neuper@52113: refFormula 1 (get_pos 1 1) (*gets CalcHead; model is still empty*); neuper@52113: neuper@52113: neuper@52113: fetchProposedTactic 1 (*by using Iterator No.1*); neuper@52113: setNextTactic 1 (Model_Problem); (*by using Iterator No.1*) wneuper@59248: autoCalculate 1 (Step 1); neuper@52113: refFormula 1 (get_pos 1 1) (*model contains descriptions for all items*); wneuper@59248: autoCalculate 1 (Step 1); neuper@52113: (*-----since Model_Problem + complete_mod_ in case cas of SOME-----* neuper@52113: fetchProposedTactic 1; neuper@52113: setNextTactic 1 (Add_Given "equality (1 + -1 * 2 + x = 0)"); wneuper@59248: autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); (*equality added*); neuper@52113: neuper@52113: fetchProposedTactic 1; neuper@52113: setNextTactic 1 (Add_Given "solveFor x"); wneuper@59248: autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); neuper@52113: neuper@52113: fetchProposedTactic 1; neuper@52113: setNextTactic 1 (Add_Find "solutions L"); wneuper@59248: autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); neuper@52113: neuper@52113: fetchProposedTactic 1; neuper@52113: setNextTactic 1 (Specify_Theory "Test"); wneuper@59248: autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); neuper@52113: *-----since Model_Problem + complete_mod_ in case cas of SOME-----*) neuper@52113: neuper@52113: fetchProposedTactic 1; neuper@55279: setNextTactic 1 (Specify_Problem ["LINEAR","univariate","equation","test"]); wneuper@59248: autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); neuper@52113: (*-------------------------------------------------------------------------*) neuper@52113: fetchProposedTactic 1; neuper@52113: val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1; neuper@52113: neuper@52113: setNextTactic 1 (Specify_Method ["Test","solve_linear"]); neuper@52113: val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1; neuper@52113: wneuper@59248: autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); neuper@52113: val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1; neuper@52113: neuper@52113: (*-------------------------------------------------------------------------*) neuper@52113: fetchProposedTactic 1; neuper@52113: val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1; neuper@52113: neuper@52113: setNextTactic 1 (Apply_Method ["Test","solve_linear"]); neuper@52113: (*ERROR.110620 .. end-of-calculation*) neuper@52113: val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1; neuper@52113: is_complete_mod ptp; neuper@52113: is_complete_spec ptp; neuper@52113: wneuper@59248: autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); neuper@52113: val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1; neuper@52113: (*term2str (get_obj g_form pt [1]);*) neuper@52113: (*-------------------------------------------------------------------------*) neuper@52113: neuper@52113: fetchProposedTactic 1; neuper@52113: setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "isolate_bdv")); wneuper@59248: autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); neuper@52113: neuper@52113: fetchProposedTactic 1; neuper@52113: setNextTactic 1 (Rewrite_Set "Test_simplify"); wneuper@59248: autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); neuper@52113: neuper@52113: fetchProposedTactic 1; neuper@55279: setNextTactic 1 (Check_Postcond ["LINEAR","univariate","equation","test"]); wneuper@59248: autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); neuper@52113: neuper@52113: val ((pt,_),_) = get_calc 1; neuper@52113: val ip = get_pos 1 1; neuper@52113: val (Form f, tac, asms) = pt_extract (pt, ip); neuper@52113: (*exception just above means: 'ModSpec' has been returned: error anyway*) neuper@52113: if term2str f = "[x = 1]" then () else neuper@52113: error "FE-Kernel-interface.sml: diff.behav. in solve_linear as rootpbl"; neuper@52113: neuper@52113: "--------- inspect the CalcTree No.1 with Iterator No.2 -"; neuper@52113: "--------- inspect the CalcTree No.1 with Iterator No.2 -"; neuper@52113: "--------- inspect the CalcTree No.1 with Iterator No.2 -"; neuper@52113: (*WN041118: inspection shifted to Iterator No.1, because others need pos'*) neuper@52113: moveActiveRoot 1; neuper@52113: refFormula 1 ([],Pbl); getTactic 1 ([],Pbl);(*Error*) neuper@52113: moveActiveDown 1; neuper@52113: refFormula 1 ([1],Frm); getTactic 1 ([1],Frm);(*Error*) neuper@52113: moveActiveDown 1 ; neuper@52113: refFormula 1 ([1],Res); getTactic 1 ([1],Res);(*OK*) neuper@52113: (*getAssumption 1 ([1],Res); TODO.WN041217*) neuper@52113: moveActiveDown 1 ; refFormula 1 ([2],Res); neuper@52113: moveActiveCalcHead 1; refFormula 1 ([],Pbl); neuper@52113: moveActiveDown 1; neuper@52113: moveActiveDown 1; neuper@52113: moveActiveDown 1; neuper@52113: if get_pos 1 1 = ([2], Res) then () else neuper@52113: error "FE-interface.sml: diff.behav. in a inspect 1 with Iterator 2"; neuper@52113: moveActiveDown 1; refFormula 1 ([], Res); neuper@52113: if get_pos 1 1 = ([], Res) then () else neuper@52113: error "FE-interface.sml: diff.behav. in b inspect 1 with Iterator 2"; neuper@52113: moveActiveCalcHead 1; refFormula 1 ([],Pbl); neuper@52113: DEconstrCalcTree 1; neuper@52113: neuper@52113: "--------- miniscript with mini-subpbl ------------------"; neuper@52113: "--------- miniscript with mini-subpbl ------------------"; neuper@52113: "--------- miniscript with mini-subpbl ------------------"; neuper@52113: (*WN120210?not ME:\label{SOLVE:MANUAL:TACTIC:enter} UC 30.3.2.1 p.175 !!!!!NOT IMPL IN FE*) neuper@52113: "=== this sequence of fun-calls resembles fun me ==="; neuper@52113: CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], neuper@52113: ("Test", ["sqroot-test","univariate","equation","test"], neuper@52113: ["Test","squ-equ-test-subpbl1"]))]; neuper@52113: Iterator 1; neuper@52113: neuper@52113: moveActiveRoot 1; neuper@52113: refFormula 1 (get_pos 1 1); neuper@52113: fetchProposedTactic 1; neuper@52113: setNextTactic 1 (Model_Problem); wneuper@59248: autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*gets ModSpec;model is still empty*) neuper@52113: neuper@52113: fetchProposedTactic 1; neuper@52113: setNextTactic 1 (Add_Given "equality (x + 1 = 2)"); wneuper@59248: autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); neuper@52113: neuper@52113: fetchProposedTactic 1; neuper@52113: setNextTactic 1 (Add_Given "solveFor x"); wneuper@59248: autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); neuper@52113: neuper@52113: fetchProposedTactic 1; neuper@52113: setNextTactic 1 (Add_Find "solutions L"); wneuper@59248: autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); neuper@52113: neuper@52113: fetchProposedTactic 1; neuper@52113: setNextTactic 1 (Specify_Theory "Test"); wneuper@59248: autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); neuper@52113: neuper@52113: fetchProposedTactic 1; neuper@52113: setNextTactic 1 (Specify_Problem neuper@52113: ["sqroot-test","univariate","equation","test"]); wneuper@59248: autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); neuper@52113: "1-----------------------------------------------------------------"; neuper@52113: neuper@52113: fetchProposedTactic 1; neuper@52113: setNextTactic 1 (Specify_Method ["Test","squ-equ-test-subpbl1"]); wneuper@59248: autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); neuper@52113: neuper@52113: fetchProposedTactic 1; neuper@52113: setNextTactic 1 (Apply_Method ["Test","squ-equ-test-subpbl1"]); wneuper@59248: autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); neuper@52113: neuper@52113: fetchProposedTactic 1; neuper@52113: setNextTactic 1 (Rewrite_Set "norm_equation"); wneuper@59248: autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); neuper@52113: neuper@52113: fetchProposedTactic 1; neuper@52113: setNextTactic 1 (Rewrite_Set "Test_simplify"); wneuper@59248: autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); neuper@52113: neuper@52113: fetchProposedTactic 1;(*----------------Subproblem--------------------*); neuper@52113: setNextTactic 1 (Subproblem ("Test", neuper@55279: ["LINEAR","univariate","equation","test"])); wneuper@59248: autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); neuper@52113: neuper@52113: fetchProposedTactic 1; neuper@52113: setNextTactic 1 (Model_Problem ); wneuper@59248: autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); neuper@52113: neuper@52113: fetchProposedTactic 1; neuper@52113: setNextTactic 1 (Add_Given "equality (-1 + x = 0)"); wneuper@59248: autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); neuper@52113: neuper@52113: fetchProposedTactic 1; neuper@52113: setNextTactic 1 (Add_Given "solveFor x"); wneuper@59248: autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); neuper@52113: neuper@52113: fetchProposedTactic 1; neuper@52113: setNextTactic 1 (Add_Find "solutions x_i"); wneuper@59248: autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); neuper@52113: neuper@52113: fetchProposedTactic 1; neuper@52113: setNextTactic 1 (Specify_Theory "Test"); wneuper@59248: autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); neuper@52113: neuper@52113: fetchProposedTactic 1; neuper@55279: setNextTactic 1 (Specify_Problem ["LINEAR","univariate","equation","test"]); wneuper@59248: autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); neuper@52113: "2-----------------------------------------------------------------"; neuper@52113: neuper@52113: fetchProposedTactic 1; neuper@52113: setNextTactic 1 (Specify_Method ["Test","solve_linear"]); wneuper@59248: autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); neuper@52113: neuper@52113: fetchProposedTactic 1; neuper@52113: setNextTactic 1 (Apply_Method ["Test","solve_linear"]); wneuper@59248: autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); neuper@52113: neuper@52113: fetchProposedTactic 1; neuper@52113: setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "isolate_bdv")); wneuper@59248: autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); neuper@52113: neuper@52113: fetchProposedTactic 1; neuper@52113: setNextTactic 1 (Rewrite_Set "Test_simplify"); wneuper@59248: autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); neuper@52113: neuper@52113: fetchProposedTactic 1; neuper@55279: setNextTactic 1 (Check_Postcond ["LINEAR","univariate","equation","test"]); wneuper@59248: autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); neuper@52113: neuper@52113: fetchProposedTactic 1; neuper@52113: setNextTactic 1 (Check_elementwise "Assumptions"); wneuper@59248: autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); neuper@52113: neuper@52113: val xml = fetchProposedTactic 1; neuper@52113: setNextTactic 1 (Check_Postcond neuper@52113: ["sqroot-test","univariate","equation","test"]); wneuper@59248: autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); neuper@52113: neuper@52113: val ((pt,_),_) = get_calc 1; wneuper@59279: val str = pr_ctree pr_short pt; neuper@52113: writeln str; neuper@52113: val ip = get_pos 1 1; neuper@52113: val (Form f, tac, asms) = pt_extract (pt, ip); neuper@52113: (*exception just above means: 'ModSpec' has been returned: error anyway*) neuper@52113: if term2str f = "[x = 1]" then () else neuper@52113: error "FE-interface.sml: diff.behav. in miniscript with mini-subpb"; neuper@52113: DEconstrCalcTree 1; neuper@52113: neuper@52113: "--------- mini-subpbl AUTOCALCULATE Step 1 -------------"; neuper@52113: "--------- mini-subpbl AUTOCALCULATE Step 1 -------------"; neuper@52113: "--------- mini-subpbl AUTOCALCULATE Step 1 -------------"; neuper@52113: (*WN120210?not ME:\label{SOLVE:AUTO:one} UC 30.3.3.2 p.176*) neuper@52113: CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], neuper@52113: ("Test", ["sqroot-test","univariate","equation","test"], neuper@52113: ["Test","squ-equ-test-subpbl1"]))]; neuper@52113: Iterator 1; neuper@52113: moveActiveRoot 1; wneuper@59248: autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); wneuper@59248: autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); wneuper@59248: autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); wneuper@59248: autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); wneuper@59248: autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); wneuper@59248: autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); wneuper@59248: autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); wneuper@59248: autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); neuper@52113: (*here the solve-phase starts*) wneuper@59248: autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); wneuper@59248: autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); wneuper@59248: autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); neuper@52113: (*------------------------------------*) wneuper@59111: (* default_print_depth 13; get_calc 1; neuper@52113: *) wneuper@59248: autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); neuper@52113: (*calc-head of subproblem*) wneuper@59248: autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); wneuper@59248: autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); wneuper@59248: autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); wneuper@59248: autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); wneuper@59248: autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); wneuper@59248: autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); wneuper@59248: autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); neuper@52113: (*solve-phase of the subproblem*) wneuper@59248: autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); wneuper@59248: autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); wneuper@59248: autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); wneuper@59248: autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); neuper@52113: (*finish subproblem*) wneuper@59248: autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); neuper@52113: (*finish problem*) wneuper@59248: autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); neuper@52113: neuper@52113: (*this checks the test for correctness..*) neuper@52113: val ((pt,_),_) = get_calc 1; neuper@52113: val p = get_pos 1 1; neuper@52113: val (Form f, tac, asms) = pt_extract (pt, p); neuper@52113: if term2str f = "[x = 1]" andalso p = ([], Res) then () else neuper@52113: error "FE-interface.sml: diff.behav. in miniscript with mini-subpb"; neuper@52113: DEconstrCalcTree 1; neuper@52113: neuper@52113: neuper@52113: "--------- solve_linear as rootpbl AUTO CompleteCalc ----"; neuper@52113: "--------- solve_linear as rootpbl AUTO CompleteCalc ----"; neuper@52113: "--------- solve_linear as rootpbl AUTO CompleteCalc ----"; neuper@52113: (*WN120210?not ME:\label{SPECIFY:START:auto} UC 30.2.4.2 p.174*) neuper@52113: CalcTree neuper@52113: [(["equality (1+-1*2+x=(0::real))", "solveFor x","solutions L"], neuper@52113: ("Test", neuper@55279: ["LINEAR","univariate","equation","test"], neuper@52113: ["Test","solve_linear"]))]; neuper@52113: Iterator 1; neuper@52113: moveActiveRoot 1; neuper@52113: getFormulaeFromTo 1 ([],Pbl) ([],Pbl) 999 false; neuper@52113: wneuper@59248: autoCalculate 1 CompleteCalc; neuper@52113: val (unc, del, gen) = (([],Pbl), ([],Pbl), ([],Res)); neuper@52113: getFormulaeFromTo 1 unc gen 1 (*only level 1*) false; neuper@52113: neuper@52113: val ((pt,_),_) = get_calc 1; neuper@52113: val p = get_pos 1 1; neuper@52113: val (Form f, tac, asms) = pt_extract (pt, p); neuper@52113: if term2str f = "[x = 1]" andalso p = ([], Res) then () else neuper@52113: error "FE-interface.sml: diff.behav. in solve_linear/rt AUTOCALCULATE "; neuper@52113: DEconstrCalcTree 1; neuper@52113: neuper@52113: "--------- solve_linear as rootpbl AUTO CompleteHead/Calc "; neuper@52113: "--------- solve_linear as rootpbl AUTO CompleteHead/Calc "; neuper@52113: "--------- solve_linear as rootpbl AUTO CompleteHead/Calc "; neuper@52113: (* ERROR: error in kernel ?? *) neuper@52113: CalcTree neuper@52113: [(["equality (1+-1*2+x=(0::real))", "solveFor x","solutions L"], neuper@52113: ("Test", neuper@55279: ["LINEAR","univariate","equation","test"], neuper@52113: ["Test","solve_linear"]))]; neuper@52113: Iterator 1; neuper@52113: moveActiveRoot 1; neuper@52113: wneuper@59248: autoCalculate 1 CompleteCalcHead; neuper@52113: refFormula 1 (get_pos 1 1); neuper@52113: val ((pt,p),_) = get_calc 1; neuper@52113: wneuper@59248: autoCalculate 1 CompleteCalc; neuper@52113: val ((pt,p),_) = get_calc 1; neuper@52113: if p=([], Res) then () else neuper@52113: error "FE-interface.sml: diff.behav. in solve_linear AUTOC Head/Calc "; neuper@52113: DEconstrCalcTree 1; neuper@52113: neuper@52113: "--------- mini-subpbl AUTOCALCULATE CompleteCalc -------"; neuper@52113: "--------- mini-subpbl AUTOCALCULATE CompleteCalc -------"; neuper@52113: "--------- mini-subpbl AUTOCALCULATE CompleteCalc -------"; neuper@52113: (*WN120210?not ME:\label{SPECIFY:START:auto} UC 30.2.4.2 p.174*) neuper@52113: CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], neuper@52113: ("Test", ["sqroot-test","univariate","equation","test"], neuper@52113: ["Test","squ-equ-test-subpbl1"]))]; neuper@52113: Iterator 1; neuper@52113: moveActiveRoot 1; wneuper@59248: autoCalculate 1 CompleteCalc; neuper@52113: val ((pt,p),_) = get_calc 1; show_pt pt; neuper@52113: (* neuper@52113: getTactic 1 ([1],Frm); neuper@52113: getTactic 1 ([1],Res); neuper@52113: initContext 1 Thy_ ([1],Res); neuper@52113: *) neuper@52113: (*... returns calcChangedEvent with*) neuper@52113: val (unc, del, gen) = (([],Pbl), ([],Pbl), ([],Res)); neuper@52113: getFormulaeFromTo 1 unc gen 0 (*only result*) false; neuper@52113: getFormulaeFromTo 1 unc gen 1 (*only level 1*) false; neuper@52113: getFormulaeFromTo 1 unc gen 99999 (*all levels*) false; neuper@52113: neuper@52113: val ((pt,_),_) = get_calc 1; neuper@52113: val p = get_pos 1 1; neuper@52113: val (Form f, tac, asms) = pt_extract (pt, p); neuper@52113: if term2str f = "[x = 1]" andalso p = ([], Res) then () else neuper@52113: error "FE-interface.sml: diff.behav. in mini-subpbl AUTOCALCULATE 6"; wneuper@59253: DEconstrCalcTree 1; neuper@52113: neuper@52113: "--------- mini-subpbl AUTO CompleteCalcHead ------------"; neuper@52113: "--------- mini-subpbl AUTO CompleteCalcHead ------------"; neuper@52113: "--------- mini-subpbl AUTO CompleteCalcHead ------------"; neuper@52113: CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], neuper@52113: ("Test", ["sqroot-test","univariate","equation","test"], neuper@52113: ["Test","squ-equ-test-subpbl1"]))]; neuper@52113: Iterator 1; neuper@52113: moveActiveRoot 1; wneuper@59248: autoCalculate 1 CompleteCalcHead; neuper@52113: neuper@52113: val ((Nd (PblObj {env = NONE, fmz = (fm, ("Test", pblID, metID)), loc = (SOME (env, ctxt1), NONE), neuper@52113: cell = NONE, ctxt = ctxt2, meth, neuper@52113: spec = ("Test", ["sqroot-test", "univariate", "equation", "test"], neuper@52113: ["Test", "squ-equ-test-subpbl1"]), neuper@52113: probl, branch = TransitiveB, origin, ostate = Incomplete, result}, []), neuper@52113: ([], Met)), []) = get_calc 1; neuper@52113: if length meth = 3 andalso length probl = 3 (*just some items tested*) then () neuper@52113: else error "--- mini-subpbl AUTO CompleteCalcHead ---"; neuper@52113: DEconstrCalcTree 1; neuper@52113: neuper@52113: "--------- solve_linear as rootpbl AUTO CompleteModel ---"; neuper@52113: "--------- solve_linear as rootpbl AUTO CompleteModel ---"; neuper@52113: "--------- solve_linear as rootpbl AUTO CompleteModel ---"; neuper@52113: CalcTree neuper@52113: [(["equality (1+-1*2+x=(0::real))", "solveFor x","solutions L"], neuper@52113: ("Test", neuper@55279: ["LINEAR","univariate","equation","test"], neuper@52113: ["Test","solve_linear"]))]; neuper@52113: Iterator 1; neuper@52113: moveActiveRoot 1; wneuper@59248: autoCalculate 1 CompleteModel; neuper@52113: refFormula 1 (get_pos 1 1); neuper@52113: neuper@55279: setProblem 1 ["LINEAR","univariate","equation","test"]; neuper@52113: val pos = get_pos 1 1; neuper@55279: setContext 1 pos (kestoreID2guh Pbl_["LINEAR","univariate","equation","test"]); neuper@52113: refFormula 1 (get_pos 1 1); neuper@52113: neuper@52113: setMethod 1 ["Test","solve_linear"]; neuper@52113: setContext 1 pos (kestoreID2guh Met_ ["Test","solve_linear"]); neuper@52113: refFormula 1 (get_pos 1 1); neuper@52113: val ((pt,_),_) = get_calc 1; neuper@52113: if get_obj g_spec pt [] = ("e_domID", neuper@55279: ["LINEAR", "univariate","equation","test"], neuper@52113: ["Test","solve_linear"]) then () neuper@52113: else error "FE-interface.sml: diff.behav. in setProblem, setMethod"; neuper@52113: wneuper@59248: autoCalculate 1 CompleteCalcHead; neuper@52113: refFormula 1 (get_pos 1 1); wneuper@59248: autoCalculate 1 CompleteCalc; neuper@52113: moveActiveDown 1; neuper@52113: moveActiveDown 1; neuper@52113: moveActiveDown 1; neuper@52113: refFormula 1 (get_pos 1 1); neuper@52113: val ((pt,_),_) = get_calc 1; neuper@52113: val p = get_pos 1 1; neuper@52113: val (Form f, tac, asms) = pt_extract (pt, p); neuper@52113: if term2str f = "[x = 1]" andalso p = ([], Res) then () else neuper@52113: error "FE-interface.sml: diff.behav. in mini-subpbl AUTOCALCULATE 6"; wneuper@59253: DEconstrCalcTree 1; neuper@52113: neuper@52113: "--------- setContext..Thy ------------------------------"; neuper@52113: "--------- setContext..Thy ------------------------------"; neuper@52113: "--------- setContext..Thy ------------------------------"; neuper@52113: CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], neuper@52113: ("Test", ["sqroot-test","univariate","equation","test"], neuper@52113: ["Test","squ-equ-test-subpbl1"]))]; neuper@52113: Iterator 1; moveActiveRoot 1; wneuper@59248: autoCalculate 1 CompleteCalcHead; wneuper@59248: autoCalculate 1 (Step 1); neuper@52113: val ((pt,p),_) = get_calc 1; show_pt pt; (*2 lines, OK*) neuper@52113: (* neuper@52113: setNextTactic 1 (Rewrite_Set "Test_simplify"); (*--> "thy_isac_Test-rls-Test_simplify"*) wneuper@59248: autoCalculate 1 (Step 1); neuper@52113: val ((pt,p),_) = get_calc 1; show_pt pt; neuper@52113: *) neuper@52113: "-----^^^^^ and vvvvv do the same -----"; neuper@52113: setContext 1 p "thy_isac_Test-rls-Test_simplify"; neuper@52113: val ((pt,p),_) = get_calc 1; show_pt pt; (*2 lines, OK*) neuper@52113: wneuper@59248: autoCalculate 1 (Step 1); neuper@52113: setContext 1 p "thy_isac_Test-rls-Test_simplify"; neuper@52113: val (((pt,_),_), p) = (get_calc 1, get_pos 1 1); neuper@52113: val (Form f, tac, asms) = pt_extract (pt, p); neuper@52113: if p = ([1], Res) andalso term2str (get_obj g_res pt (fst p)) = "x + 1 + -1 * 2 = 0" wneuper@59248: then () else error "--- setContext..Thy --- autoCalculate 1 (Step 1) #1"; neuper@52113: wneuper@59248: autoCalculate 1 CompleteCalc; neuper@52113: val (((pt,_),_), p) = (get_calc 1, get_pos 1 1); neuper@52113: val (Form f, tac, asms) = pt_extract (pt, p); neuper@52113: neuper@52113: if term2str f = "[x = 1]" andalso p = ([], Res) then () wneuper@59248: else error "--- setContext..Thy --- autoCalculate CompleteCalc"; neuper@52113: DEconstrCalcTree 1; neuper@52113: neuper@52113: "--------- mini-subpbl AUTOCALC CompleteToSubpbl --------"; neuper@52113: "--------- mini-subpbl AUTOCALC CompleteToSubpbl --------"; neuper@52113: "--------- mini-subpbl AUTOCALC CompleteToSubpbl --------"; neuper@52113: CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], neuper@52113: ("Test", ["sqroot-test","univariate","equation","test"], neuper@52113: ["Test","squ-equ-test-subpbl1"]))]; neuper@52113: Iterator 1; moveActiveRoot 1; wneuper@59248: autoCalculate 1 CompleteToSubpbl; neuper@52113: refFormula 1 (get_pos 1 1); (* -1 + x = 0 *); neuper@52113: val ((pt,_),_) = get_calc 1; wneuper@59279: val str = pr_ctree pr_short pt; neuper@52113: writeln str; neuper@52113: if str = ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + -1 * 2 = 0\n" neuper@52113: then () else neuper@52113: error "FE-interface.sml: diff.behav. in mini-subpbl CompleteToSubpbl-1"; neuper@52113: wneuper@59248: autoCalculate 1 (Step 1); (*proceeds only, of NOT 1 step before subplb*) wneuper@59248: autoCalculate 1 CompleteToSubpbl; neuper@52113: val ((pt,_),_) = get_calc 1; wneuper@59279: val str = pr_ctree pr_short pt; neuper@52113: writeln str; wneuper@59248: autoCalculate 1 CompleteCalc; (*das geht ohnehin !*); neuper@52113: val ((pt,_),_) = get_calc 1; neuper@52113: val p = get_pos 1 1; neuper@52113: neuper@52113: val (Form f, tac, asms) = pt_extract (pt, p); neuper@52113: if term2str f = "[x = 1]" andalso p = ([], Res) then () else neuper@52113: error "FE-interface.sml: diff.behav. in mini-subpbl CompleteToSubpbl 1"; wneuper@59253: DEconstrCalcTree 1; neuper@52113: neuper@52113: "--------- rat-eq + subpbl: no_met, NO solution dropped -"; neuper@52113: "--------- rat-eq + subpbl: no_met, NO solution dropped -"; neuper@52113: "--------- rat-eq + subpbl: no_met, NO solution dropped -"; neuper@52113: CalcTree neuper@52113: [(["equality ((5*x)/(x - 2) - x/(x+2)=(4::real))", "solveFor x","solutions L"], neuper@52113: ("RatEq", ["univariate","equation"], ["no_met"]))]; neuper@52113: Iterator 1; neuper@52113: moveActiveRoot 1; neuper@52113: fetchProposedTactic 1; neuper@52113: neuper@52113: setNextTactic 1 (Model_Problem); wneuper@59248: autoCalculate 1 (Step 1); fetchProposedTactic 1; neuper@52113: neuper@52113: setNextTactic 1 (Specify_Theory "RatEq"); wneuper@59248: autoCalculate 1 (Step 1); fetchProposedTactic 1; neuper@52113: setNextTactic 1 (Specify_Problem ["rational","univariate","equation"]); wneuper@59248: autoCalculate 1 (Step 1); fetchProposedTactic 1; neuper@52113: setNextTactic 1 (Specify_Method ["RatEq","solve_rat_equation"]); wneuper@59248: autoCalculate 1 (Step 1); fetchProposedTactic 1; neuper@52113: setNextTactic 1 (Apply_Method ["RatEq","solve_rat_equation"]); wneuper@59248: autoCalculate 1 (Step 1); fetchProposedTactic 1; neuper@52113: setNextTactic 1 (Rewrite_Set "RatEq_simplify"); wneuper@59248: autoCalculate 1 (Step 1); fetchProposedTactic 1; neuper@52113: setNextTactic 1 (Rewrite_Set "norm_Rational"); wneuper@59248: autoCalculate 1 (Step 1); fetchProposedTactic 1; neuper@52113: setNextTactic 1 (Rewrite_Set "RatEq_eliminate"); wneuper@59248: autoCalculate 1 (Step 1); fetchProposedTactic 1; neuper@52113: (* __________ for "12 * x + 4 * x ^^^ 2 = 4 * (-4 + x ^^^ 2)"*) neuper@52113: setNextTactic 1 (Subproblem ("PolyEq", ["normalize","polynomial", neuper@52113: "univariate","equation"])); wneuper@59248: autoCalculate 1 (Step 1); fetchProposedTactic 1; neuper@52113: setNextTactic 1 (Model_Problem ); wneuper@59248: autoCalculate 1 (Step 1); fetchProposedTactic 1; neuper@52113: setNextTactic 1 (Specify_Theory "PolyEq"); wneuper@59248: autoCalculate 1 (Step 1); fetchProposedTactic 1; neuper@52113: setNextTactic 1 (Specify_Problem ["normalize","polynomial", neuper@52113: "univariate","equation"]); wneuper@59248: autoCalculate 1 (Step 1); fetchProposedTactic 1; neuper@52113: setNextTactic 1 (Specify_Method ["PolyEq","normalize_poly"]); wneuper@59248: autoCalculate 1 (Step 1); fetchProposedTactic 1; neuper@52113: setNextTactic 1 (Apply_Method ["PolyEq","normalize_poly"]); wneuper@59248: autoCalculate 1 (Step 1); fetchProposedTactic 1; wneuper@59254: setNextTactic 1 (Rewrite ("all_left", num_str @{thm all_left})); wneuper@59248: autoCalculate 1 (Step 1); fetchProposedTactic 1; neuper@52113: setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "make_ratpoly_in")); wneuper@59248: autoCalculate 1 (Step 1); fetchProposedTactic 1; neuper@52113: (* __________ for "16 + 12 * x = 0"*) neuper@52113: setNextTactic 1 (Subproblem ("PolyEq", neuper@52113: ["degree_1","polynomial","univariate","equation"])); wneuper@59248: autoCalculate 1 (Step 1); fetchProposedTactic 1; neuper@52113: setNextTactic 1 (Model_Problem ); wneuper@59248: autoCalculate 1 (Step 1); fetchProposedTactic 1; neuper@52113: setNextTactic 1 (Specify_Theory "PolyEq"); neuper@52113: (*------------- some trials in the problem-hierarchy ---------------*) neuper@55279: setNextTactic 1 (Specify_Problem ["LINEAR","univariate","equation"]); wneuper@59248: autoCalculate 1 (Step 1); fetchProposedTactic 1; (* helpless !!!*) neuper@52113: setNextTactic 1 (Refine_Problem ["univariate","equation"]); neuper@52113: (*------------------------------------------------------------------*) wneuper@59248: autoCalculate 1 (Step 1); fetchProposedTactic 1; neuper@52113: setNextTactic 1 (Specify_Method ["PolyEq","solve_d1_polyeq_equation"]); wneuper@59248: autoCalculate 1 (Step 1); fetchProposedTactic 1; neuper@52113: setNextTactic 1 (Apply_Method ["PolyEq","solve_d1_polyeq_equation"]); wneuper@59248: autoCalculate 1 (Step 1); fetchProposedTactic 1; neuper@52113: setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "d1_polyeq_simplify")); wneuper@59248: autoCalculate 1 (Step 1); fetchProposedTactic 1; neuper@52113: setNextTactic 1 (Rewrite_Set "polyeq_simplify"); wneuper@59248: autoCalculate 1 (Step 1); fetchProposedTactic 1; neuper@52113: setNextTactic 1 Or_to_List; wneuper@59248: autoCalculate 1 (Step 1); fetchProposedTactic 1; neuper@52113: setNextTactic 1 (Check_elementwise "Assumptions"); wneuper@59248: autoCalculate 1 (Step 1); fetchProposedTactic 1; neuper@52113: setNextTactic 1 (Check_Postcond ["degree_1","polynomial", neuper@52113: "univariate","equation"]); wneuper@59248: autoCalculate 1 (Step 1); fetchProposedTactic 1; neuper@52113: setNextTactic 1 (Check_Postcond ["normalize","polynomial", neuper@52113: "univariate","equation"]); wneuper@59248: autoCalculate 1 (Step 1); fetchProposedTactic 1; neuper@52113: setNextTactic 1 (Check_Postcond ["rational","univariate","equation"]); neuper@52113: val (ptp,_) = get_calc 1; neuper@52113: val (Form t,_,_) = pt_extract ptp; neuper@52113: if get_pos 1 1 = ([], Res) andalso term2str t = "[x = -4 / 3]" then () neuper@52113: else writeln "FE-inteface.sml: diff.behav. in rat-eq + subpbl: no_met, NO .."; wneuper@59253: DEconstrCalcTree 1; neuper@52113: neuper@52113: "--------- tryMatchProblem, tryRefineProblem ------------"; neuper@52113: "--------- tryMatchProblem, tryRefineProblem ------------"; neuper@52113: "--------- tryMatchProblem, tryRefineProblem ------------"; neuper@52113: (*{\bf\UC{Having \isac{} Refine the Problem neuper@52113: * Automatically}\label{SPECIFY:refine-auto}\\} test match and refine with neuper@52113: * x^^^2 + 4*x + 5 = 2 neuper@52113: see isac.bridge.TestSpecify#testMatchRefine*) neuper@52113: CalcTree neuper@52113: [(["equality (x^2 + 4*x + 5 = (2::real))", "solveFor x","solutions L"], neuper@52113: ("Isac", neuper@52113: ["univariate","equation"], neuper@52113: ["no_met"]))]; neuper@52113: Iterator 1; neuper@52113: moveActiveRoot 1; neuper@52113: neuper@52113: fetchProposedTactic 1; neuper@52113: setNextTactic 1 (Model_Problem ); neuper@52113: (*..this tactic should be done 'tacitly', too !*) neuper@52113: neuper@52113: (* wneuper@59248: autoCalculate 1 CompleteCalcHead; neuper@52113: checkContext 1 ([],Pbl) "pbl_equ_univ"; neuper@52113: checkContext 1 ([],Pbl) (kestoreID2guh Pbl_ ["univariate","equation"]); neuper@52113: *) neuper@52113: wneuper@59248: autoCalculate 1 (Step 1); neuper@52113: neuper@52113: fetchProposedTactic 1; neuper@52113: setNextTactic 1 (Add_Given "equality (x ^^^ 2 + 4 * x + 5 = (2::real))"); wneuper@59248: autoCalculate 1 (Step 1); neuper@52113: neuper@52113: "--------- we go into the ProblemBrowser (_NO_ pblID selected) -"; neuper@52113: initContext 1 Pbl_ ([],Pbl); wneuper@59173: (* this would break if a calculation would be inserted before: CALCID... wneuper@59173: and pattern matching is not available in *.java. wneuper@59173: if cut_xml xml = "(CONTEXTPBL)\n. (CALCID)\n. . 1\n. (/CALCID)\n. (CONTEXTDATA)\n. . (GUH)\n. . . pbl_equ_univ\n. . (/GUH)\n. . (STATUS)\n. . . correct\n. . (/STATUS)\n. . (HEAD)\n. . . (MATHML)\n. . . . (ISA)\n. . . . . solve (x ^ 2 + 4 * x + 5 = 2, x)\n. . . . (/ISA)\n. . . (/MATHML)\n. . (/HEAD)\n. . (MODEL)\n. . . (GIVEN)\n. . . . (ITEM status=correct)\n. . . . . (MATHML)\n. . . . . . (ISA)\n. . . . . . . equality (x ^ 2 + 4 * x + 5 = 2)\n. . . . . . (/ISA)\n. . . . . (/MATHML)\n. . . . (/ITEM)\n. . . . (ITEM status=correct)\n. . . . . (MATHML)\n. . . . . . (ISA)\n. . . . . . . solveFor x\n. . . . . . (/ISA)\n. . . . . (/MATHML)\n. . . . (/ITEM)\n. . . (/GIVEN)\n. . . (WHERE)\n. . . . (ITEM status=correct)\n. . . . . (MATHML)\n. . . . . . (ISA)\n. . . . . . . matches (?a = ?b) (x ^ 2 + 4 * x + 5 = 2)\n. . . . . . (/ISA)\n. . . . . (/MATHML)\n. . . . (/ITEM)\n. . . (/WHERE)\n. . . (FIND)\n. . . . (ITEM status=correct)\n. . . . . (MATHML)\n. . . . . . (ISA)\n. . . . . . . solutions L\n. . . . . . (/ISA)\n. . . . . (/MATHML)\n. . . . (/ITEM)\n. . . (/FI" wneuper@59173: then () else error "--- tryMatchProblem, tryRefineProblem: initContext 1 Pbl_ ([],Pbl); CHANGED"; wneuper@59173: *) neuper@52113: initContext 1 Met_ ([],Pbl); wneuper@59173: (*1error in kernel 33*) neuper@52113: neuper@52113: "--------- this match will show some incomplete items: ---------"; neuper@52113: neuper@52113: checkContext 1 ([],Pbl) (kestoreID2guh Pbl_ ["univariate","equation"]); neuper@52113: checkContext 1 ([],Pbl) (kestoreID2guh Met_ ["LinEq", "solve_lineq_equation"]); neuper@52113: neuper@52113: neuper@52113: fetchProposedTactic 1; wneuper@59248: setNextTactic 1 (Add_Given "solveFor x"); autoCalculate 1 (Step 1); neuper@52113: neuper@52113: fetchProposedTactic 1; wneuper@59248: setNextTactic 1 (Add_Find "solutions L"); autoCalculate 1 (Step 1); neuper@52113: neuper@52113: "--------- this is a matching model (all items correct): -------"; neuper@52113: checkContext 1 ([],Pbl) (kestoreID2guh Pbl_ ["univariate","equation"]); neuper@52113: "--------- this is a NOT matching model (some 'false': ---------"; neuper@55279: checkContext 1 ([],Pbl)(kestoreID2guh Pbl_ ["LINEAR","univariate","equation"]); neuper@52113: neuper@52113: "--------- find out a matching problem: ------------------------"; neuper@52113: "--------- find out a matching problem (FAILING: no new pbl) ---"; neuper@55279: refineProblem 1([],Pbl)(pblID2guh ["LINEAR","univariate","equation"]); neuper@52113: neuper@52113: "--------- find out a matching problem (SUCCESSFUL) ------------"; neuper@52113: refineProblem 1 ([],Pbl) (pblID2guh ["univariate","equation"]); neuper@52113: neuper@52113: "--------- tryMatch, tryRefine did not change the calculation -"; neuper@52113: "--------- this is done by on the pbl-browser: ------"; neuper@52113: setNextTactic 1 (Specify_Problem ["normalize","polynomial", neuper@52113: "univariate","equation"]); wneuper@59248: autoCalculate 1 (Step 1); neuper@52113: (*WN050904 fetchProposedTactic again --> Specify_Problem ["normalize",... neuper@52113: and Specify_Theory skipped in comparison to below ---^^^-inserted *) neuper@52113: (*------------vvv-inserted-----------------------------------------------*) neuper@52113: fetchProposedTactic 1; neuper@52113: setNextTactic 1 (Specify_Problem ["normalize","polynomial", neuper@52113: "univariate","equation"]); wneuper@59248: autoCalculate 1 (Step 1); neuper@52113: neuper@52113: (*and Specify_Theory skipped by fetchProposedTactic ?!?*) neuper@52113: neuper@52113: fetchProposedTactic 1; neuper@52113: setNextTactic 1 (Specify_Method ["PolyEq","normalize_poly"]); wneuper@59248: autoCalculate 1 (Step 1); neuper@52113: neuper@52113: fetchProposedTactic 1; neuper@52113: setNextTactic 1 (Apply_Method ["PolyEq","normalize_poly"]); neuper@52113: wneuper@59248: autoCalculate 1 CompleteCalc; neuper@52113: neuper@52113: val ((pt,_),_) = get_calc 1; neuper@52113: show_pt pt; neuper@52113: val p = get_pos 1 1; neuper@52113: val (Form f, tac, asms) = pt_extract (pt, p); neuper@52113: if term2str f = "[x = -1, x = -3]" andalso p = ([], Res) then () else neuper@52113: error "FE-interface.sml: diff.behav. in tryMatchProblem, tryRefine"; neuper@52113: neuper@52113: (*------------^^^-inserted-----------------------------------------------*) neuper@52113: (*WN050904 the fetchProposedTactic's below may not have worked like that neuper@52113: before, too, because there was no check*) neuper@52113: fetchProposedTactic 1; neuper@52113: setNextTactic 1 (Specify_Theory "PolyEq"); wneuper@59248: autoCalculate 1 (Step 1); neuper@52113: neuper@52113: fetchProposedTactic 1; neuper@52113: setNextTactic 1 (Specify_Method ["PolyEq","normalize_poly"]); wneuper@59248: autoCalculate 1 (Step 1); neuper@52113: neuper@52113: fetchProposedTactic 1; neuper@52113: "--------- now the calc-header is ready for enter 'solving' ----"; wneuper@59248: autoCalculate 1 CompleteCalc; neuper@52113: neuper@52113: val ((pt,_),_) = get_calc 1; neuper@52113: rootthy pt; neuper@52113: show_pt pt; neuper@52113: val p = get_pos 1 1; neuper@52113: val (Form f, tac, asms) = pt_extract (pt, p); neuper@52113: if term2str f = "[x = -1, x = -3]" andalso p = ([], Res) then () else neuper@52113: error "FE-interface.sml: diff.behav. in tryMatchProblem, tryRefine"; wneuper@59253: DEconstrCalcTree 1; neuper@52113: neuper@52113: "--------- modifyCalcHead, resetCalcHead, modelProblem --"; neuper@52113: "--------- modifyCalcHead, resetCalcHead, modelProblem --"; neuper@52113: "--------- modifyCalcHead, resetCalcHead, modelProblem --"; neuper@52113: CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], neuper@52113: ("Test", ["sqroot-test","univariate","equation","test"], neuper@52113: ["Test","squ-equ-test-subpbl1"]))]; neuper@52113: Iterator 1; neuper@52113: moveActiveRoot 1; neuper@52113: neuper@52113: modifyCalcHead 1 (([],Pbl),(*the position from refFormula*) neuper@52113: "solve (x+1=2, x)",(*the headline*) neuper@52113: [Given ["equality (x+1=(2::real))", "solveFor x"], neuper@52113: Find ["solutions L"](*,Relate []*)], neuper@52113: Pbl, neuper@52113: ("Test", neuper@52113: ["sqroot-test","univariate","equation","test"], neuper@52113: ["Test","squ-equ-test-subpbl1"])); neuper@52113: neuper@52113: val ((Nd (PblObj {env = NONE, neuper@52113: fmz = (fm, tpm), neuper@52113: loc = (SOME scrst_ctxt, NONE), neuper@52113: ctxt, neuper@52113: cell = NONE, neuper@52113: meth, neuper@52113: spec = (thy, neuper@52113: ["sqroot-test", "univariate", "equation", "test"], neuper@52113: ["Test", "squ-equ-test-subpbl1"]), neuper@52113: probl, neuper@52113: branch = TransitiveB, neuper@52113: origin, neuper@52113: ostate = Incomplete, neuper@52113: result}, neuper@52113: []), neuper@52113: ([], Pbl)), neuper@52113: []) = get_calc 1; neuper@52113: (*WN110622: is the same as in 2002, but shouldn't be probl = [3 items?]*) neuper@52113: if length meth = 0 andalso length probl = 0 (*just some items tested*) then () neuper@52113: else error "--- modifyCalcHead, resetCalcHead, modelProblem 1 --"; neuper@52113: neuper@52113: resetCalcHead 1; neuper@52113: modelProblem 1; neuper@52113: neuper@52113: get_calc 1; neuper@52113: val ((Nd (PblObj {env = NONE, neuper@52113: fmz = (fm, tpm), neuper@52113: loc = (SOME scrst_ctxt, NONE), neuper@52113: ctxt, neuper@52113: cell = NONE, neuper@52113: meth, neuper@52113: spec = ("e_domID", ["e_pblID"], ["e_metID"]), neuper@52113: probl, neuper@52113: branch = TransitiveB, neuper@52113: origin, neuper@52113: ostate = Incomplete, neuper@52113: result}, neuper@52113: []), neuper@52113: ([], Pbl)), neuper@52113: []) = get_calc 1; neuper@52113: if length meth = 3 andalso length probl = 3 (*just some items tested*) then () neuper@52113: else error "--- modifyCalcHead, resetCalcHead, modelProblem 2 --"; neuper@52113: neuper@52113: "--------- maximum-example, UC: Modeling an example -----"; neuper@52113: "--------- maximum-example, UC: Modeling an example -----"; neuper@52113: "--------- maximum-example, UC: Modeling an example -----"; neuper@52113: (* {\bf\UC{Editing the Model}\label{SPECIFY:enter}\label{SPECIFY:check}\\} neuper@52113: see isac.bridge.TestModel#testEditItems neuper@52113: *) neuper@52113: val elems = ["fixedValues [r=Arbfix]","maximum A","valuesFor [a,b]", neuper@52113: "relations [A=a*b, (a/2)^2 + (b/2)^2 = r^2]", neuper@52113: "relations [A=a*b, (a/2)^2 + (b/2)^2 = r^2]", neuper@52113: "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]", neuper@52113: (*^^^ these are the elements for the root-problem (in variants)*) neuper@52113: (*vvv these are elements required for subproblems*) neuper@52113: "boundVariable a","boundVariable b","boundVariable alpha", neuper@52113: "interval {x::real. 0 <= x & x <= 2*r}", neuper@52113: "interval {x::real. 0 <= x & x <= 2*r}", neuper@52113: "interval {x::real. 0 <= x & x <= pi}", neuper@52113: "errorBound (eps=(0::real))"] neuper@52113: (*specifying is not interesting for this example*) neuper@52113: val spec = ("DiffApp", ["maximum_of","function"], neuper@52113: ["DiffApp","max_by_calculus"]); neuper@52113: (*the empty model with descriptions for user-guidance by Model_Problem*) neuper@52113: val empty_model = [Given ["fixedValues []"], neuper@52113: Find ["maximum", "valuesFor"], neuper@52113: Relate ["relations []"]]; neuper@52113: DEconstrCalcTree 1; neuper@52113: neuper@52113: "#################################################################"; neuper@52113: neuper@52113: CalcTree [(elems, spec)]; neuper@52113: Iterator 1; neuper@52113: moveActiveRoot 1; neuper@52113: refFormula 1 (get_pos 1 1); neuper@52113: (*this gives a completely empty model*) neuper@52113: neuper@52113: fetchProposedTactic 1; neuper@52113: (*fill the CalcHead with Descriptions...*) neuper@52113: setNextTactic 1 (Model_Problem ); wneuper@59248: autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); neuper@52113: neuper@52113: (*user input is !!!!!EITHER!!!!! _some_ (at least one) items of the model neuper@52113: !!!!!OR!!!!! _one_ part of the specification !!!!!!!!!!!!!*) neuper@52113: (*input of two items, 'fixedValues [r=Arbfix]' and 'maximum b'...*) neuper@52113: modifyCalcHead 1 (([],Pbl) (*position, from previous refFormula*), neuper@52113: "Problem (DiffApp.thy, [maximum_of, function])", neuper@52113: (*the head-form ^^^ is not used for input here*) neuper@52113: [Given ["fixedValues [r=Arbfix]"(*new input*)], neuper@52113: Find ["maximum b"(*new input*), "valuesFor"], neuper@52113: Relate ["relations"]], neuper@52113: (*input (Arbfix will dissappear soon)*) neuper@52113: Pbl (*belongsto*), neuper@52113: e_spec (*no input to the specification*)); neuper@52113: neuper@52113: (*the user does not know, what 'superfluous' for 'maximum b' may mean neuper@52113: and asks what to do next*) neuper@52113: fetchProposedTactic 1; neuper@52113: (*the student follows the advice*) neuper@52113: setNextTactic 1 (Add_Find "maximum A"); (*FIXME.17.11.03: does not yet work*) wneuper@59248: autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); neuper@52113: neuper@52113: (*this input completes the model*) neuper@52113: modifyCalcHead 1 (([],Pbl), "not used here", neuper@52113: [Given ["fixedValues [r=Arbfix]"], neuper@52113: Find ["maximum A", "valuesFor [a,b]"(*new input*)], neuper@52113: Relate ["relations [A=a*b, \ neuper@52113: \(a/2)^2 + (b/2)^2 = r^2]"]], Pbl, e_spec); neuper@52113: neuper@52113: (*specification is not interesting and should be skipped by the dialogguide; neuper@52113: !!!!!!!!!!!!!!!!!!!! input of ONE part at a time !!!!!!!!!!!!!!!!!!!!!!*) neuper@52113: modifyCalcHead 1 (([],Pbl), "not used here", neuper@52113: [Given ["fixedValues [r=Arbfix]"], neuper@52113: Find ["maximum A", "valuesFor [a,b]"(*new input*)], neuper@52113: Relate ["relations [A=a*b, \ neuper@52113: \(a/2)^2 + (b/2)^2 = r^2]"]], Pbl, neuper@52113: ("DiffApp", ["e_pblID"], ["e_metID"])); neuper@52113: modifyCalcHead 1 (([],Pbl), "not used here", neuper@52113: [Given ["fixedValues [r=Arbfix]"], neuper@52113: Find ["maximum A", "valuesFor [a,b]"(*new input*)], neuper@52113: Relate ["relations [A=a*b, \ neuper@52113: \(a/2)^2 + (b/2)^2 = r^2]"]], Pbl, neuper@52113: ("DiffApp", ["maximum_of","function"], neuper@52113: ["e_metID"])); neuper@52113: modifyCalcHead 1 (([],Pbl), "not used here", neuper@52113: [Given ["fixedValues [r=Arbfix]"], neuper@52113: Find ["maximum A", "valuesFor [a,b]"(*new input*)], neuper@52113: Relate ["relations [A=a*b, \ neuper@52113: \(a/2)^2 + (b/2)^2 = r^2]"]], Pbl, neuper@52113: ("DiffApp", ["maximum_of","function"], neuper@52113: ["DiffApp","max_by_calculus"])); neuper@52113: (*this final calcHead now has STATUS 'complete' !*) neuper@52113: DEconstrCalcTree 1; neuper@52113: neuper@52113: "--------- solve_linear from pbl-hierarchy --------------"; neuper@52113: "--------- solve_linear from pbl-hierarchy --------------"; neuper@52113: "--------- solve_linear from pbl-hierarchy --------------"; neuper@55279: val (fmz, sp) = ([], ("", ["LINEAR","univariate","equation","test"], [])); neuper@52113: CalcTree [(fmz, sp)]; neuper@52113: Iterator 1; moveActiveRoot 1; neuper@52113: refFormula 1 (get_pos 1 1); neuper@52113: modifyCalcHead 1 (([],Pbl),"solve (1+-1*2+x=(0::real))", neuper@52113: [Given ["equality (1+-1*2+x=(0::real))", "solveFor x"], neuper@52113: Find ["solutions L"]], neuper@52113: Pbl, neuper@55279: ("Test", ["LINEAR","univariate","equation","test"], neuper@52113: ["Test","solve_linear"])); wneuper@59248: autoCalculate 1 CompleteCalc; neuper@52113: refFormula 1 (get_pos 1 1); neuper@52113: val ((pt,_),_) = get_calc 1; neuper@52113: val p = get_pos 1 1; neuper@52113: val (Form f, tac, asms) = pt_extract (pt, p); neuper@52113: if term2str f = "[x = 1]" andalso p = ([], Res) neuper@52113: andalso terms2str asms = "[\"matches (?a = ?b) (1 + -1 * 2 + x = 0)\"]" then () neuper@52113: else error "FE-interface.sml: diff.behav. in from pbl -hierarchy"; neuper@52113: DEconstrCalcTree 1; neuper@52113: neuper@52113: "--------- solve_linear as in an algebra system (CAS)----"; neuper@52113: "--------- solve_linear as in an algebra system (CAS)----"; neuper@52113: "--------- solve_linear as in an algebra system (CAS)----"; neuper@52113: (*WN120210?not ME:\label{UC:cas-input} UC 30.1.2.5 p.168*) neuper@52113: val (fmz, sp) = ([], ("", [], [])); neuper@52113: CalcTree [(fmz, sp)]; neuper@52113: Iterator 1; moveActiveRoot 1; neuper@52113: modifyCalcHead 1 (([],Pbl),"solveTest (1+-1*2+x=0,x)", [], Pbl, ("", [], [])); wneuper@59248: autoCalculate 1 CompleteCalc; neuper@52113: refFormula 1 (get_pos 1 1); neuper@52113: val ((pt,_),_) = get_calc 1; neuper@52113: val p = get_pos 1 1; neuper@52113: val (Form f, tac, asms) = pt_extract (pt, p); neuper@52113: if term2str f = "[x = 1]" andalso p = ([], Res) neuper@52113: andalso terms2str asms = "[\"matches (?a = ?b) (1 + -1 * 2 + x = 0)\"]" then () neuper@52113: else error "FE-interface.sml: diff.behav. in from pbl -hierarchy"; neuper@52113: DEconstrCalcTree 1; neuper@52113: neuper@52113: "--------- interSteps: on 'miniscript with mini-subpbl' -"; neuper@52113: "--------- interSteps: on 'miniscript with mini-subpbl' -"; neuper@52113: "--------- interSteps: on 'miniscript with mini-subpbl' -"; neuper@52113: CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], neuper@52113: ("Test", ["sqroot-test","univariate","equation","test"], neuper@52113: ["Test","squ-equ-test-subpbl1"]))]; neuper@52113: Iterator 1; neuper@52113: moveActiveRoot 1; wneuper@59248: autoCalculate 1 CompleteCalc; neuper@52113: val ((pt,_),_) = get_calc 1; neuper@52113: show_pt pt; neuper@52113: neuper@52113: (*UC\label{UC:inter-steps} UC 30.3.5.5 p.178*) neuper@52113: interSteps 1 ([2],Res); neuper@52113: val ((pt,_),_) = get_calc 1; show_pt pt (*new ([2,1],Frm)..([2,6],Res)*); neuper@52113: val (unc, del, gen) = (([1],Res),([1],Res),([2,6],Res)); neuper@52113: getFormulaeFromTo 1 unc gen 1 false; neuper@52113: neuper@52113: (*UC\label{UC:inter-steps} UC 30.3.5.5 p.178*) neuper@52113: interSteps 1 ([3,2],Res); neuper@52113: val ((pt,_),_) = get_calc 1; show_pt pt (*new ([3,2,1],Frm)..([3,2,2],Res)*); neuper@52113: val (unc, del, gen) = (([3,1],Res),([3,1],Res),([3,2,2],Res)); neuper@52113: getFormulaeFromTo 1 unc gen 1 false; neuper@52113: neuper@52113: (*UC\label{UC:inter-steps} UC 30.3.5.5 p.178*) neuper@52113: interSteps 1 ([3],Res) (*no new steps in subproblems*); neuper@52113: val (unc, del, gen) = (([3],Pbl),([3],Pbl),([3,2],Res)); neuper@52113: getFormulaeFromTo 1 unc gen 1 false; neuper@52113: neuper@52113: (*UC\label{UC:inter-steps} UC 30.3.5.5 p.178*) neuper@52113: interSteps 1 ([],Res) (*no new steps in subproblems*); neuper@52113: val (unc, del, gen) = (([],Pbl),([],Pbl),([4],Res)); neuper@52113: getFormulaeFromTo 1 unc gen 1 false; neuper@52113: DEconstrCalcTree 1; neuper@52113: neuper@52113: "--------- getTactic, fetchApplicableTactics ------------"; neuper@52113: "--------- getTactic, fetchApplicableTactics ------------"; neuper@52113: "--------- getTactic, fetchApplicableTactics ------------"; neuper@52113: (* compare test/../script.sml neuper@52113: "----------- fun sel_rules ---------------------------------------"; neuper@52113: *) neuper@52113: CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], neuper@52113: ("Test", ["sqroot-test","univariate","equation","test"], neuper@52113: ["Test","squ-equ-test-subpbl1"]))]; neuper@52113: Iterator 1; moveActiveRoot 1; wneuper@59248: autoCalculate 1 CompleteCalc; neuper@52113: val ((pt,_),_) = get_calc 1; neuper@52113: show_pt pt; neuper@52113: neuper@52113: (*UC\label{SOLVE:HIDE:getTactic} \label{SOLVE:AUTO:tactic} UC 30.3.3.1 p.176 neuper@52113: WN120210 not impl. in FE*) neuper@52113: getTactic 1 ([],Pbl); neuper@52113: getTactic 1 ([1],Res); neuper@52113: getTactic 1 ([3],Pbl); neuper@52113: getTactic 1 ([3,1],Frm); neuper@52113: getTactic 1 ([3],Res); neuper@52113: getTactic 1 ([],Res); neuper@52113: neuper@52113: (*UC\label{SOLVE:MANUAL:TACTIC:listall} UC 30.3.2.2 p.175*) neuper@52113: fetchApplicableTactics 1 99999 ([],Pbl); neuper@52113: fetchApplicableTactics 1 99999 ([1],Res); neuper@52113: fetchApplicableTactics 1 99999 ([3],Pbl); neuper@52113: fetchApplicableTactics 1 99999 ([3,1],Res); neuper@52113: fetchApplicableTactics 1 99999 ([3],Res); neuper@52113: fetchApplicableTactics 1 99999 ([],Res); neuper@52113: DEconstrCalcTree 1; neuper@52113: neuper@52113: "--------- getAssumptions, getAccumulatedAsms -----------"; neuper@52113: "--------- getAssumptions, getAccumulatedAsms -----------"; neuper@52113: "--------- getAssumptions, getAccumulatedAsms -----------"; neuper@52113: CalcTree neuper@52113: [(["equality (x/(x^2 - 6*x+9) - 1/(x^2 - 3*x) =1/x)", neuper@52113: "solveFor x","solutions L"], neuper@52113: ("RatEq",["univariate","equation"],["no_met"]))]; neuper@52113: Iterator 1; moveActiveRoot 1; wneuper@59248: autoCalculate 1 CompleteCalc; neuper@52113: val ((pt,_),_) = get_calc 1; neuper@52113: val p = get_pos 1 1; neuper@52113: val (Form f, tac, asms) = pt_extract (pt, p); neuper@52113: (*============ inhibit exn WN120316 compare 2002--2011 =========================== neuper@52113: if map term2str asms = neuper@52113: ["True |\n~ lhs ((3 + -1 * x + x ^^^ 2) * x =\n" ^ neuper@52113: " 1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)) is_poly_in x", "-6 * x + 5 * x ^^^ 2 = 0", neuper@52113: "lhs (-6 * x + 5 * x ^^^ 2 = 0) is_poly_in x", neuper@52113: "lhs (-6 * x + 5 * x ^^^ 2 = 0) has_degree_in x = 2", neuper@52113: "9 * x + -6 * x ^^^ 2 + x ^^^ 3 ~= 0"] neuper@52113: andalso term2str f = "[-6 * x + 5 * x ^^^ 2 = 0]" andalso p = ([], Res) then () neuper@52113: else error "TODO compare 2002--2011"; (*...data during test --- x / (x ^ 2 - 6 * x + 9) - 1...*) neuper@52113: ============ inhibit exn WN120316 compare 2002--2011 ===========================*) neuper@52113: if p = ([], Res) andalso term2str f = "[]" (*see WN120317.TODO dropped rateq*) neuper@52113: andalso asms = [] (*STRANGE!, compare test --- x / (x ^ 2 - 6 * x + 9) - 1 / (x ^ 2 ...*) neuper@52113: then () else error "rlang.sml: diff.behav. in Schalk I s.87 Bsp 55b [x = 6 / 5]"; neuper@52113: neuper@52113: (*UC\label{SOLVE:HELP:assumptions} UC 30.3.5.1 p.178*) neuper@52113: getAssumptions 1 ([3], Res); neuper@52113: getAssumptions 1 ([5], Res); neuper@52113: (*UC\label{SOLVE:HELP:assumptions-origin} UC 30.3.5.2 p.178 neuper@52113: WN0502 still without positions*) neuper@52113: getAccumulatedAsms 1 ([3], Res); neuper@52113: getAccumulatedAsms 1 ([5], Res); neuper@52113: DEconstrCalcTree 1; neuper@52113: neuper@52113: "--------- arbitrary combinations of steps --------------"; neuper@52113: "--------- arbitrary combinations of steps --------------"; neuper@52113: "--------- arbitrary combinations of steps --------------"; neuper@52113: CalcTree (*start of calculation, return No.1*) neuper@52113: [(["equality (1+-1*2+x=(0::real))", "solveFor x","solutions L"], neuper@52113: ("Test", neuper@55279: ["LINEAR","univariate","equation","test"], neuper@52113: ["Test","solve_linear"]))]; neuper@52113: Iterator 1; moveActiveRoot 1; neuper@52113: neuper@52113: fetchProposedTactic 1; neuper@52113: (*ERROR get_calc 1 not existent*) neuper@52113: setNextTactic 1 (Model_Problem ); wneuper@59248: autoCalculate 1 (Step 1); neuper@52113: fetchProposedTactic 1; neuper@52113: fetchProposedTactic 1; neuper@52113: neuper@52113: setNextTactic 1 (Add_Find "solutions L"); neuper@52113: setNextTactic 1 (Add_Find "solutions L"); neuper@52113: wneuper@59248: autoCalculate 1 (Step 1); wneuper@59248: autoCalculate 1 (Step 1); neuper@52113: neuper@52113: setNextTactic 1 (Specify_Theory "Test"); neuper@52113: fetchProposedTactic 1; wneuper@59248: autoCalculate 1 (Step 1); neuper@52113: wneuper@59248: autoCalculate 1 (Step 1); wneuper@59248: autoCalculate 1 (Step 1); wneuper@59248: autoCalculate 1 (Step 1); wneuper@59248: autoCalculate 1 (Step 1); neuper@52113: (*------------------------- end calc-head*) neuper@52113: neuper@52113: fetchProposedTactic 1; neuper@52113: setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "isolate_bdv")); wneuper@59248: autoCalculate 1 (Step 1); neuper@52113: neuper@52113: setNextTactic 1 (Rewrite_Set "Test_simplify"); neuper@52113: fetchProposedTactic 1; wneuper@59248: autoCalculate 1 (Step 1); neuper@52113: wneuper@59248: autoCalculate 1 CompleteCalc; neuper@52113: val ((pt,_),_) = get_calc 1; neuper@52113: val p = get_pos 1 1; neuper@52113: val (Form f, tac, asms) = pt_extract (pt, p); neuper@52113: if term2str f = "[x = 1]" andalso p = ([], Res) then () else neuper@52113: error "FE-interface.sml: diff.behav. in combinations of steps"; neuper@52113: DEconstrCalcTree 1; neuper@52113: neuper@52113: "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}right"; (*UC 30.3.2.4 p.175*) neuper@52113: "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}right"; neuper@52113: "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}right"; neuper@52113: CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], neuper@52113: ("Test", ["sqroot-test","univariate","equation","test"], neuper@52113: ["Test","squ-equ-test-subpbl1"]))]; neuper@52113: Iterator 1; neuper@52113: moveActiveRoot 1; wneuper@59248: autoCalculate 1 CompleteCalcHead; wneuper@59248: autoCalculate 1 (Step 1); wneuper@59248: autoCalculate 1 (Step 1); wneuper@59123: appendFormula 1 "-1 + x = 0" (*|> Future.join*); neuper@52113: (*... returns calcChangedEvent with*) neuper@52113: val (unc, del, gen) = (([1],Res), ([1],Res), ([2],Res)); neuper@52113: getFormulaeFromTo 1 unc gen 99999 (*all levels*) false; neuper@52113: neuper@52113: val ((pt,_),_) = get_calc 1; neuper@52113: val p = get_pos 1 1; neuper@52113: val (Form f, tac, asms) = pt_extract (pt, p); neuper@52113: if term2str f = "-1 + x = 0" andalso p = ([2], Res) then () else neuper@52113: error "FE-interface.sml: diff.behav. in FORMULA:enter} right"; neuper@52113: DEconstrCalcTree 1; neuper@52113: neuper@52113: "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}other"; (*UC 30.3.2.4 p.175*) neuper@52113: "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}other"; neuper@52113: "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}other"; neuper@52113: CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], neuper@52113: ("Test", ["sqroot-test","univariate","equation","test"], neuper@52113: ["Test","squ-equ-test-subpbl1"]))]; neuper@52113: Iterator 1; neuper@52113: moveActiveRoot 1; wneuper@59248: autoCalculate 1 CompleteCalcHead; wneuper@59248: autoCalculate 1 (Step 1); wneuper@59248: autoCalculate 1 (Step 1); wneuper@59123: appendFormula 1 "x - 1 = 0" (*|> Future.join*); neuper@52113: val (unc, del, gen) = (([1],Res), ([1],Res), ([2],Res)); neuper@52113: getFormulaeFromTo 1 unc gen 99999 (*all levels*) false; neuper@52113: (*11 elements !!!*) neuper@52113: neuper@52113: val ((pt,_),_) = get_calc 1; neuper@52113: val p = get_pos 1 1; neuper@52113: val (Form f, tac, asms) = pt_extract (pt, p); neuper@52113: if term2str f = "x - 1 = 0" andalso p = ([2], Res) then () else neuper@52113: error "FE-interface.sml: diff.behav. in FORMULA:enter} other"; neuper@52113: DEconstrCalcTree 1; neuper@52113: neuper@52113: "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}oth 2"; (*UC 30.3.2.4 p.175*) neuper@52113: "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}oth 2"; neuper@52113: "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}oth 2"; neuper@52113: CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], neuper@52113: ("Test", ["sqroot-test","univariate","equation","test"], neuper@52113: ["Test","squ-equ-test-subpbl1"]))]; neuper@52113: Iterator 1; neuper@52113: moveActiveRoot 1; wneuper@59248: autoCalculate 1 CompleteCalcHead; wneuper@59248: autoCalculate 1 (Step 1); wneuper@59248: autoCalculate 1 (Step 1); wneuper@59123: appendFormula 1 "x = 1" (*|> Future.join*); neuper@52113: (*... returns calcChangedEvent with*) neuper@52113: val (unc, del, gen) = (([1],Res), ([1],Res), ([3,2],Res)); neuper@52113: getFormulaeFromTo 1 unc gen 99999 (*all levels*) false; neuper@52113: (*6 elements !!!*) neuper@52113: neuper@52113: val ((pt,_),_) = get_calc 1; neuper@52113: val p = get_pos 1 1; neuper@52113: val (Form f, tac, asms) = pt_extract (pt, p); neuper@52113: if term2str f = "x = 1" andalso p = ([3,2], Res) then () else neuper@52113: error "FE-interface.sml: diff.behav. in FORMULA:enter} oth 2"; neuper@52113: DEconstrCalcTree 1; neuper@52113: neuper@52113: "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}NOTok"; (*UC 30.3.2.4 p.175*) neuper@52113: "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}NOTok"; neuper@52113: "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}NOTok"; neuper@52113: CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], neuper@52113: ("Test", ["sqroot-test","univariate","equation","test"], neuper@52113: ["Test","squ-equ-test-subpbl1"]))]; neuper@52113: Iterator 1; neuper@52113: moveActiveRoot 1; wneuper@59248: autoCalculate 1 CompleteCalcHead; wneuper@59248: autoCalculate 1 (Step 1); wneuper@59248: autoCalculate 1 (Step 1); wneuper@59123: appendFormula 1 "x - 4711 = 0" (*|> Future.join*); neuper@52113: (*... returns no derivation found *) neuper@52113: neuper@52113: val ((pt,_),_) = get_calc 1; neuper@52113: val p = get_pos 1 1; neuper@52113: val (Form f, tac, asms) = pt_extract (pt, p); neuper@52113: if term2str f = "x + 1 + -1 * 2 = 0" andalso p = ([1], Res) then () else neuper@52113: error "FE-interface.sml: diff.behav. in FORMULA:enter} NOTok"; neuper@52113: DEconstrCalcTree 1; neuper@52113: neuper@52113: "--------- replaceFormula {SOL:MAN:FOR:replace} right----"; (*UC 30.3.2.5 p.176*) neuper@52113: "--------- replaceFormula {SOL:MAN:FOR:replace} right----"; neuper@52113: "--------- replaceFormula {SOL:MAN:FOR:replace} right----"; neuper@52113: (*\label{SOLVE:MANUAL:FORMULA:replace}*) neuper@52113: CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], neuper@52113: ("Test", ["sqroot-test","univariate","equation","test"], neuper@52113: ["Test","squ-equ-test-subpbl1"]))]; neuper@52113: Iterator 1; neuper@52113: moveActiveRoot 1; wneuper@59248: autoCalculate 1 CompleteCalc; neuper@52113: moveActiveFormula 1 ([2],Res); neuper@52113: replaceFormula 1 "-1 + x = 0" (*i.e. repeats input*); neuper@52113: (*... returns formula not changed *) neuper@52113: neuper@52113: val ((pt,_),_) = get_calc 1; neuper@52113: val p = get_pos 1 1; neuper@52113: val (Form f, tac, asms) = pt_extract (pt, p); neuper@52113: if term2str f = "-1 + x = 0" andalso p = ([2], Res) then () else neuper@52113: error "FE-interface.sml: diff.behav. in FORMULA:replace} right 1"; neuper@52113: if map fst (get_interval ([2],Res) ([],Res) 9999 pt) = neuper@52113: [([2], Res), ([3], Pbl), ([3, 1], Frm), ([3, 1], Res), ([3, 2], Res), neuper@52113: ([3], Res), ([4], Res), ([], Res)] then () (*nothing deleted!*) else neuper@52113: error "FE-interface.sml: diff.behav. in FORMULA:replace} right 2"; neuper@52113: neuper@52113: (*WN050211 replaceFormula didn't work on second ctree: thus now tested...*) neuper@52113: CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], neuper@52113: ("Test", ["sqroot-test","univariate","equation","test"], neuper@52113: ["Test","squ-equ-test-subpbl1"]))]; neuper@52113: Iterator 2; neuper@52113: moveActiveRoot 2; wneuper@59248: autoCalculate 2 CompleteCalc; neuper@52113: moveActiveFormula 2 ([2],Res); neuper@52113: replaceFormula 2 "-1 + x = 0" (*i.e. repeats input*); neuper@52113: (*... returns formula not changed *) neuper@52113: neuper@52113: val ((pt,_),_) = get_calc 2; neuper@52113: val p = get_pos 2 1; neuper@52113: val (Form f, tac, asms) = pt_extract (pt, p); neuper@52113: if term2str f = "-1 + x = 0" andalso p = ([2], Res) then () else neuper@52113: error "FE-interface.sml: diff.behav. in FORMULA:replace} right 1"; neuper@52113: if map fst (get_interval ([2],Res) ([],Res) 9999 pt) = neuper@52113: [([2], Res), ([3], Pbl), ([3, 1], Frm), ([3, 1], Res), ([3, 2], Res), neuper@52113: ([3], Res), ([4], Res), ([], Res)] then () (*nothing deleted!*) else neuper@52113: error "FE-interface.sml: diff.behav. in FORMULA:replace} right 2b"; neuper@52113: DEconstrCalcTree 1; neuper@52113: neuper@52113: "--------- replaceFormula {SOL:MAN:FOR:replace} other----"; (*UC 30.3.2.5 p.176*) neuper@52113: "--------- replaceFormula {SOL:MAN:FOR:replace} other----"; neuper@52113: "--------- replaceFormula {SOL:MAN:FOR:replace} other----"; neuper@52113: (*\label{SOLVE:MANUAL:FORMULA:replace}*) neuper@52113: CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], neuper@52113: ("Test", ["sqroot-test","univariate","equation","test"], neuper@52113: ["Test","squ-equ-test-subpbl1"]))]; neuper@52113: Iterator 1; neuper@52113: moveActiveRoot 1; wneuper@59248: autoCalculate 1 CompleteCalc; neuper@52113: moveActiveFormula 1 ([2],Res); (*there is "-1 + x = 0"*) neuper@52113: replaceFormula 1 "x - 1 = 0"; (*<-------------------------------------*) neuper@52113: (*... returns calcChangedEvent with*) neuper@52113: val (unc, del, gen) = (([1],Res), ([4],Res), ([2],Res)); neuper@52113: getFormulaeFromTo 1 unc gen 99999 (*all levels*) false; neuper@52113: neuper@52113: val ((pt,_),_) = get_calc 1; neuper@52113: show_pt pt; neuper@52113: val p = get_pos 1 1; neuper@52113: val (Form f, tac, asms) = pt_extract (pt, p); neuper@52113: if term2str f = "x - 1 = 0" andalso p = ([2], Res) then () else neuper@52113: error "FE-interface.sml: diff.behav. in FORMULA:replace} other 1"; neuper@52113: (* for getting the list in whole length ... wneuper@59111: default_print_depth 99;map fst (get_interval ([1],Res) ([],Res) 9999 pt);default_print_depth 3; neuper@52113: *) neuper@52113: if map fst (get_interval ([1],Res) ([],Res) 9999 pt) = neuper@52113: [([1], Res), ([2, 1], Frm), ([2, 1], Res), ([2, 2], Res), ([2, 3], Res), neuper@52113: ([2, 4], Res), ([2, 5], Res), ([2, 6], Res), ([2, 7], Res), neuper@52113: ([2, 8], Res), ([2, 9], Res), ([2], Res) neuper@52113: (*WN060727 {cutlevup->test_trans} removed: , neuper@52113: ([], Res)(*dropped, if test_trans doesnt stop at PblNd*)*)] then () else neuper@52113: error "FE-interface.sml: diff.behav. in FORMULA:replace} other 2"; neuper@52113: DEconstrCalcTree 1; neuper@52113: neuper@52113: "--------- replaceFormula {SOL:MAN:FOR:replace} other 2--"; (*UC 30.3.2.5 p.176*) neuper@52113: "--------- replaceFormula {SOL:MAN:FOR:replace} other 2--"; neuper@52113: "--------- replaceFormula {SOL:MAN:FOR:replace} other 2--"; neuper@52113: (*\label{SOLVE:MANUAL:FORMULA:replace}*) neuper@52113: CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], neuper@52113: ("Test", ["sqroot-test","univariate","equation","test"], neuper@52113: ["Test","squ-equ-test-subpbl1"]))]; neuper@52113: Iterator 1; neuper@52113: moveActiveRoot 1; wneuper@59248: autoCalculate 1 CompleteCalc; neuper@52113: moveActiveFormula 1 ([2],Res); (*there is "-1 + x = 0"*) neuper@52113: replaceFormula 1 "x = 1"; (*<-------------------------------------*) neuper@52113: (*... returns calcChangedEvent with ...*) neuper@52113: val (unc, del, gen) = (([1],Res), ([4],Res), ([3,2],Res)); neuper@52113: getFormulaeFromTo 1 unc gen 99999 (*all levels*) false; neuper@52113: (*9 elements !!!*) neuper@52113: neuper@52113: val ((pt,_),_) = get_calc 1; neuper@52113: show_pt pt; (*error: ...get_interval drops ([3,2],Res) ...*) neuper@52113: val (t,_) = get_obj g_result pt [3,2]; term2str t; neuper@52113: if map fst (get_interval ([1],Res) ([],Res) 9999 pt) = neuper@52113: [([1], Res), ([2], Res), ([3], Pbl), ([3, 1], Frm), ([3, 1], Res), neuper@52113: ([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res), neuper@52113: ([3,2],Res)] then () else neuper@52113: error "FE-interface.sml: diff.behav. in FORMULA:replace} oth2 1"; neuper@52113: neuper@52113: val p = get_pos 1 1; neuper@52113: val (Form f, tac, asms) = pt_extract (pt, p); neuper@52113: if term2str f = "x = 1" andalso p = ([3,2], Res) then () else neuper@52113: error "FE-interface.sml: diff.behav. in FORMULA:replace} oth2 2"; neuper@52113: DEconstrCalcTree 1; neuper@52113: neuper@52113: "--------- replaceFormula {SOL:MAN:FOR:replace} NOTok----"; (*UC 30.3.2.5 p.176*) neuper@52113: "--------- replaceFormula {SOL:MAN:FOR:replace} NOTok----"; neuper@52113: "--------- replaceFormula {SOL:MAN:FOR:replace} NOTok----"; neuper@52113: (*\label{SOLVE:MANUAL:FORMULA:replace}*) neuper@52113: CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], neuper@52113: ("Test", ["sqroot-test","univariate","equation","test"], neuper@52113: ["Test","squ-equ-test-subpbl1"]))]; neuper@52113: Iterator 1; neuper@52113: moveActiveRoot 1; wneuper@59248: autoCalculate 1 CompleteCalc; neuper@52113: moveActiveFormula 1 ([2],Res); (*there is "-1 + x = 0"*) neuper@52113: replaceFormula 1 "x - 4711 = 0"; neuper@52113: (*... returns no derivation found *) neuper@52113: neuper@52113: val ((pt,_),_) = get_calc 1; neuper@52113: show_pt pt; neuper@52113: val p = get_pos 1 1; neuper@52113: val (Form f, tac, asms) = pt_extract (pt, p); neuper@52113: if term2str f = "-1 + x = 0" andalso p = ([2], Res) then () else neuper@52113: error "FE-interface.sml: diff.behav. in FORMULA:replace} NOTok"; wneuper@59254: DEconstrCalcTree 1; neuper@52113: neuper@52113: "--------- UC errpat chain-rule-diff-both, fillpat by input ------"; neuper@52113: "--------- UC errpat chain-rule-diff-both, fillpat by input ------"; neuper@52113: "--------- UC errpat chain-rule-diff-both, fillpat by input ------"; neuper@52113: CalcTree neuper@52113: [(["functionTerm (x ^ 2 + sin (x ^ 4))", "differentiateFor x", "derivative f_f'"], neuper@52113: ("Isac", ["derivative_of","function"], ["diff","differentiate_on_R"]))]; neuper@52113: Iterator 1; neuper@52113: moveActiveRoot 1; wneuper@59248: autoCalculate 1 CompleteCalcHead; wneuper@59248: autoCalculate 1 (Step 1); wneuper@59248: autoCalculate 1 (Step 1);(*([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))*) wneuper@59123: appendFormula 1 "d_d x (x ^ 2) + cos (4 * x ^ 3)" (*|> Future.join*); (*<<<<<<<=========================*) neuper@52113: (* the check for errpat is maximally liberal (whole term modulo "nrls" from "type met"), neuper@52113: would recognize "cos (4 * x ^ (4 - 1)) + 2 * x" as well. neuper@52113: results in error pattern #chain-rule-diff-both# neuper@52113: instead of no derivation found *) neuper@52113: val ((pt,pos), _) = get_calc 1; neuper@52113: val p = get_pos 1 1; neuper@52113: val (Form f, _, asms) = pt_extract (pt, p); neuper@52113: wneuper@59254: if p = ([1], Res) andalso term2str f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" wneuper@59253: then case get_obj g_tac pt (fst p) of Rewrite_Inst (["(bdv, x)"], wneuper@59253: ("diff_sum", thm)) => () | _ => error "embed fun get_fillform changed 0" wneuper@59253: | _ => error "embed fun get_fillform changed 1" wneuper@59253: else error "embed fun get_fillform changed 2"; neuper@52113: neuper@52113: (*========== inhibit exn WN1130621 Isabelle2012-->13 !thehier! ==================== neuper@52113: findFillpatterns 1 "chain-rule-diff-both"; (*<<<<<<<=================================*) neuper@52113: (* fill patterns #fill-d_d-arg#d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) = neuper@52113: d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x ?_dummy_1#fill-both-args#...#...#... *) neuper@52113: val ((pt,pos),_) = get_calc 1; neuper@52113: val p = get_pos 1 1; neuper@52113: neuper@52113: val (Form f, _, asms) = pt_extract (pt, p); neuper@52113: if p = ([1], Res) andalso term2str f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" andalso neuper@52113: get_obj g_tac pt (fst p) = Rewrite_Inst (["(bdv, x)"], ("diff_sum", "Diff.diff_sum"(*?!?*))) neuper@52113: then () neuper@52113: else error "embed fun get_fillform changed 2"; neuper@52113: neuper@52113: (* if we assume, that the fill-patterns are ordered such that the 1st has large gaps neuper@52113: and the last has no gaps, then the number of fill-patterns would suffice neuper@52113: for the DialogGuide to select appropriately. *) neuper@52113: requestFillformula 1 ("chain-rule-diff-both", "fill-both-args");(*<<<<<<<============*) neuper@52113: (* ([1], Res) ([2], Res) ([2], Res) *) neuper@52113: val ((pt,pos),_) = get_calc 1; neuper@52113: val p = get_pos 1 1; neuper@52113: val (Form f, _, asms) = pt_extract (pt, p); neuper@52113: if p = ([1], Res) andalso existpt [2] pt andalso neuper@52113: term2str f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" andalso neuper@52113: get_obj g_tac pt (fst p) = Rewrite_Inst (["(bdv, x)"], ("diff_sum", "Diff.diff_sum")) neuper@52113: then () else error "embed fun get_fillform changed 3"; neuper@52113: neuper@52113: inputFillFormula 1 "d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4)";(*<<<<<<<=====*) neuper@52113: val ((pt, _),_) = get_calc 1; neuper@52113: val p = get_pos 1 1; neuper@52113: val (Form f, _, asms) = pt_extract (pt, p); neuper@52113: if p = ([2], Res) andalso neuper@52113: term2str f = "d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4)" andalso neuper@52113: get_obj g_tac pt (fst p) = Rewrite_Inst (["(bdv, x)"], ("diff_sin_chain", "")) neuper@52113: then () else error "inputFillFormula changed 11"; neuper@52113: wneuper@59248: autoCalculate 1 CompleteCalc; neuper@52113: neuper@52113: "~~~~~ final check: the input formula is inserted as it would have been correct from beginning"; neuper@52113: val ((pt, _),_) = get_calc 1; neuper@52113: val p = get_pos 1 1; neuper@52113: val (Form f, _, asms) = pt_extract (pt, p); neuper@52113: if p = ([], Res) andalso term2str f = "2 * x + cos (x ^^^ 4) * 4 * x ^^^ 3" neuper@52113: then () else error "inputFillFormula changed 12"; neuper@52113: show_pt pt; neuper@52113: (*[ neuper@52113: (([], Frm), Diff (x ^^^ 2 + sin (x ^^^ 4), x)), neuper@52113: (([1], Frm), d_d x (x ^^^ 2 + sin (x ^^^ 4))), neuper@52113: (([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))), neuper@52113: (([2], Res), d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4)), (*<<<<<<<=====*) neuper@52113: (([3], Res), d_d x (x ^^^ 2) + cos (x ^^^ 4) * (4 * x ^^^ (4 - 1))), neuper@52113: (([4], Res), 2 * x ^^^ (2 - 1) + cos (x ^^^ 4) * (4 * x ^^^ (4 - 1))), neuper@52113: (([5], Res), 2 * x + cos (x ^^^ 4) * 4 * x ^^^ 3), neuper@52113: (([], Res), 2 * x + cos (x ^^^ 4) * 4 * x ^^^ 3)] *) neuper@52113: ============ inhibit exn WN1130621 Isabelle2012-->13 !thehier! ==================*) wneuper@59253: DEconstrCalcTree 1; neuper@52113: neuper@52113: "--------- UC errpat add-fraction, fillpat by input --------------"; neuper@52113: "--------- UC errpat add-fraction, fillpat by input --------------"; neuper@52113: "--------- UC errpat add-fraction, fillpat by input --------------"; neuper@52113: (*cp from BridgeLog Java <=> SML*) wneuper@59254: CalcTree [([], ("e_domID", ["e_pblID"], ["e_metID"]))]; neuper@52113: Iterator 1; neuper@52113: moveActiveRoot 1; neuper@52113: moveActiveFormula 1 ([],Pbl); neuper@52113: replaceFormula 1 "Simplify (5 * x / (4 * y) + 3 * x / (4 * y))"; wneuper@59248: autoCalculate 1 CompleteCalcHead; wneuper@59248: autoCalculate 1 (Step 1); wneuper@59123: appendFormula 1 "8 * x / (8 * y)" (*|> Future.join*); neuper@52113: (* no derivation found neuper@52113: --- but in BridgeLog Java <=> SML: neuper@52113: error pattern #addition-of-fractions# *) wneuper@59253: DEconstrCalcTree 1; neuper@52113: neuper@52113: "--------- UC errpat, fillpat step to Rewrite --------------------"; neuper@52113: "--------- UC errpat, fillpat step to Rewrite --------------------"; neuper@52113: "--------- UC errpat, fillpat step to Rewrite --------------------"; neuper@52113: (*TODO*) wneuper@59254: CalcTree neuper@52113: [(["functionTerm ((x ^ 2) ^ 3 + sin (x ^ 4))", neuper@52113: "differentiateFor x", "derivative f_f'"], neuper@52113: ("Isac", ["derivative_of","function"], neuper@52113: ["diff","differentiate_on_R"]))]; (*<<<======= EP is directly in script*) neuper@52113: Iterator 1; neuper@52113: moveActiveRoot 1; wneuper@59248: autoCalculate 1 CompleteCalc; neuper@52113: val ((pt,p),_) = get_calc 1; show_pt pt; wneuper@59253: DEconstrCalcTree 1; neuper@52113: neuper@52113: "--------- UC errpat, fillpat step to Rewrite_Set ----------------"; neuper@52113: "--------- UC errpat, fillpat step to Rewrite_Set ----------------"; neuper@52113: "--------- UC errpat, fillpat step to Rewrite_Set ----------------"; neuper@52113: CalcTree neuper@52113: [(["functionTerm ((x ^ 2) ^ 3 + sin (x ^ 4))", neuper@52113: "differentiateFor x", "derivative f_f'"], neuper@52113: ("Isac", ["derivative_of","function"], neuper@52113: ["diff","after_simplification"]))]; (*<<<======= EP is in a ruleset*) neuper@52113: Iterator 1; neuper@52113: moveActiveRoot 1; wneuper@59248: autoCalculate 1 CompleteCalcHead; wneuper@59248: autoCalculate 1 (Step 1); fetchProposedTactic 1; wneuper@59248: autoCalculate 1 (Step 1); fetchProposedTactic 1; neuper@52113: (* neuper@52113: neuper@52113: 1 neuper@52113: neuper@52113: neuper@52113: chain-rule-diff-both neuper@52113: cancel neuper@52113: neuper@52113: neuper@52113: norm_diff neuper@52113: neuper@52113: neuper@52113: neuper@52113: neuper@52113: bdv neuper@52113: neuper@52113: neuper@52113: neuper@52113: neuper@52113: x neuper@52113: neuper@52113: neuper@52113: neuper@52113: neuper@52113: neuper@52113: neuper@52113: neuper@52113: neuper@52113: neuper@52113: (*WN1208 postponed due to efforts required for stepToErrorPatterns (NEW rewrite_set_)*) neuper@52113: stepToErrorPatterns 1; (*--> calcChanged, rule immediately calls... *) neuper@52113: stepOnErrorPatterns 1; (*--> calcChanged, rule calls getTactic and displays it *) neuper@52113: (* then --- UC errpat, fillpat by input ---*) neuper@52113: *) wneuper@59248: autoCalculate 1 CompleteCalc; neuper@52113: val ((pt,p),_) = get_calc 1; show_pt pt; neuper@52113: (*WN1208 postponed due to efforts required for stepToErrorPatterns (NEW rewrite_set_)*) wneuper@59253: DEconstrCalcTree 1; neuper@52113: