neuper@37906: (* tests the interface of isac's SML-kernel in accordance to 
neuper@37906:    java-tests/isac.bridge.
neuper@37906: 
neuper@37906: WN050707 ... if true, the test ist marked with a \label referring
neuper@37906: to the same UC in isac-docu.tex as the JUnit testcase.
neuper@37906: use"../smltest/FE-interface/interface.sml";
neuper@37906: use"interface.sml";
neuper@37906:  *)
neuper@37906: 
neuper@37906:  print_depth 3;
neuper@37906: 
neuper@37906: "-----------------------------------------------------------------";
neuper@37906: "table of contents -----------------------------------------------";
neuper@37906: "-----------------------------------------------------------------";
neuper@37906: "within struct ---------------------------------------------------";
neuper@37906: "-----------------------------------------------------------------";
neuper@37906: "--------- encode ^ -> ^^^ ---------------------------------------";
neuper@37906: "-----------------------------------------------------------------";
neuper@37906: "exported from struct --------------------------------------------";
neuper@37906: "-----------------------------------------------------------------";
neuper@37906: "---------------- empty rootpbl ----------------------------------";
neuper@37906: "---------------- solve_linear as rootpbl FE ---------------------";
neuper@37906: "--------- inspect the CalcTree No.1 with Iterator No.2 ----------";
neuper@37906: "---------------- miniscript with mini-subpbl --------------------";
neuper@37906: "--------- miniscript with mini-subpbl AUTOCALCULATE Step 1-------";
neuper@37906: "--------- solve_linear as rootpbl AUTOCALCULATE CompleteCalc ----";
neuper@37906: "--------- solve_linear as rootpbl AUTOCALC CompleteHead/Calc ----";
neuper@37906: "--------- miniscript with mini-subpbl AUTOCALCULATE CompleteCalc-";
neuper@37906: "--------- miniscript with mini-subpbl AUTO CompleteCalcHead------";
neuper@37906: "--------- solve_linear as rootpbl AUTOCALCULATE CompleteModel ---";
neuper@37906: "--------- setContext..Thy ---------------------------------------";
neuper@37906: "--------- miniscript with mini-subpbl AUTOCALC CompleteToSubpbl -";
neuper@37906: "---------------- rat-eq + subpbl: no_met, NO solution dropped ---";
neuper@37906: "--------- tryMatchProblem, tryRefineProblem -------------------UC";
neuper@37906: "--------- modifyCalcHead, resetCalcHead, modelProblem ------------";
neuper@37906: "--------- maximum-example, UC: Modeling an example --------------";
neuper@37906: "--------- solve_linear from pbl-hierarchy -----------------------";
neuper@37906: "--------- solve_linear as in an algebra system (CAS)-------------";
neuper@37906: "--------- interSteps: on 'miniscript with mini-subpbl' ----------";
neuper@37906: "--------- getTactic, fetchApplicableTactics ---------------------";
neuper@37906: "--------- getAssumptions, getAccumulatedAsms --------------------";
neuper@37906: "--------- arbitrary combinations of steps -----------------------";
neuper@37906: "--------- appendFormula label{SOLVE:MANUAL:FORMULA:enter} right--";
neuper@37906: "--------- appendFormula label{SOLVE:MANUAL:FORMULA:enter} other--";
neuper@37906: "--------- appendFormula label{SOLVE:MANUAL:FORMULA:enter} oth 2--";
neuper@37906: "--------- appendFormula label{SOLVE:MANUAL:FORMULA:enter} NOTok--";
neuper@37906: "--------- replaceFormula {SOLVE:MANUAL:FORMULA:replace} right----";
neuper@37906: "--------- replaceFormula {SOLVE:MANUAL:FORMULA:replace} other----";
neuper@37906: "--------- replaceFormula {SOLVE:MANUAL:FORMULA:replace} other 2--";
neuper@37906: "--------- replaceFormula {SOLVE:MANUAL:FORMULA:replace} NOTok----";
neuper@37906: "-----------------------------------------------------------------";
neuper@37906: 
neuper@37906: "within struct ---------------------------------------------------";
neuper@37906: "within struct ---------------------------------------------------";
neuper@37906: "within struct ---------------------------------------------------";
neuper@37906: (*==================================================================
neuper@37906: 
neuper@37906: 
neuper@37906: "--------- encode ^ -> ^^^ ---------------------------------------";
neuper@37906: "--------- encode ^ -> ^^^ ---------------------------------------";
neuper@37906: "--------- encode ^ -> ^^^ ---------------------------------------";
neuper@37906: if encode "a^2+b^2=c^2" = "a^^^2+b^^^2=c^^^2" then ()
neuper@38031: else error "interface.sml: diff.behav. in encode ^ -> ^^^ ";
neuper@37906: 
neuper@37906: if (decode o encode) "a^2+b^2=c^2" = "a^2+b^2=c^2" then ()
neuper@38031: else error "interface.sml: diff.behav. in de/encode ^ <-> ^^^ ";
neuper@37906: 
neuper@37906: ==================================================================*)
neuper@37906: "exported from struct --------------------------------------------";
neuper@37906: "exported from struct --------------------------------------------";
neuper@37906: "exported from struct --------------------------------------------";
neuper@37906: 
neuper@37906: 
neuper@37906: (*------------ set at startup of the Kernel --------------------------*)
neuper@37906:  states:= [];  (*resets all state information in Kernel               *)
neuper@37906: (*----------------------------------------------------------------*)
neuper@37906: 
neuper@37906: "---------------- empty rootpbl ----------------------------------";
neuper@37906: "---------------- empty rootpbl ----------------------------------";
neuper@37906: "---------------- empty rootpbl ----------------------------------";
neuper@37906:  CalcTree [([], ("", [], []))];
neuper@37906:  Iterator 1;
neuper@37906:  moveActiveRoot 1;
neuper@37906:  refFormula 1 (get_pos 1 1);
neuper@37906: (*WN.040222: stoert das sehr, dass e_domID etc. statt leer kommt ???*)
neuper@37906: 
neuper@37906: 
neuper@37906: "---------------- solve_linear as rootpbl FE ---------------------";
neuper@37906: "---------------- solve_linear as rootpbl FE ---------------------";
neuper@37906: "---------------- solve_linear as rootpbl FE ---------------------";
neuper@37906:  states := [];
neuper@37906:  CalcTree      (*start of calculation, return No.1*)
neuper@37906:      [(["equality (1+-1*2+x=0)", "solveFor x","solutions L"],
neuper@37906:        ("Test.thy", 
neuper@37906: 	["linear","univariate","equation","test"],
neuper@37906: 	["Test","solve_linear"]))];
neuper@37906:  Iterator 1;     (*create an active Iterator on CalcTree No.1*)
neuper@37906:  
neuper@37906:  moveActiveRoot 1;(*sets the CalcIterator No.1 at the root of CalcTree No.1*);
neuper@37906:  refFormula 1 (get_pos 1 1)  (*gets CalcHead; model is still empty*);
neuper@37906:  
neuper@37906:  fetchProposedTactic 1 (*by using Iterator No.1*);
neuper@37906:  setNextTactic 1 (Model_Problem (*["linear","univariate","equation","test"]*));
neuper@37906:                         (*by using Iterator No.1*)
neuper@37906:  autoCalculate 1 (Step 1);
neuper@37906:  refFormula 1 (get_pos 1 1)  (*model contains descriptions for all items*);
neuper@37906:  autoCalculate 1 (Step 1);
neuper@37926: (*-----since Model_Problem + complete_mod_ in case cas of SOME-----*
neuper@37906:  fetchProposedTactic 1;
neuper@37906:  setNextTactic 1 (Add_Given "equality (1 + -1 * 2 + x = 0)");
neuper@37906:  autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); (*equality added*);
neuper@37906: 
neuper@37906:  fetchProposedTactic 1;
neuper@37906:  setNextTactic 1 (Add_Given "solveFor x");
neuper@37906:  autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
neuper@37906: 
neuper@37906:  fetchProposedTactic 1;
neuper@37906:  setNextTactic 1 (Add_Find "solutions L");
neuper@37906:  autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
neuper@37906: 
neuper@37906:  fetchProposedTactic 1;
neuper@37906:  setNextTactic 1 (Specify_Theory "Test.thy");
neuper@37906:  autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
neuper@37926: *-----since Model_Problem + complete_mod_ in case cas of SOME-----*)
neuper@37906: 
neuper@37906:  fetchProposedTactic 1;
neuper@37906:  setNextTactic 1 (Specify_Problem ["linear","univariate","equation","test"]);
neuper@37906:  autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
neuper@37906: (*-------------------------------------------------------------------------*)
neuper@37906:  fetchProposedTactic 1;
neuper@37906:  val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;
neuper@37906: 
neuper@37906:  setNextTactic 1 (Specify_Method ["Test","solve_linear"]);
neuper@37906:  val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;
neuper@37906: 
neuper@37906:  autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
neuper@37906:  val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;
neuper@37906: 
neuper@37906: (*-------------------------------------------------------------------------*)
neuper@37906:  fetchProposedTactic 1;
neuper@37906:  val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;
neuper@37906: 
neuper@37906:  setNextTactic 1 (Apply_Method ["Test","solve_linear"]);
neuper@37906:  val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;
neuper@37906:  is_complete_mod ptp;
neuper@37906:  is_complete_spec ptp;
neuper@37906: 
neuper@37906:  autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
neuper@37906:  val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;
neuper@37906:  (*term2str (get_obj g_form pt [1]);*)
neuper@37906: (*-------------------------------------------------------------------------*)
neuper@37906: 
neuper@37906:  fetchProposedTactic 1;
neuper@37906:  setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "isolate_bdv"));
neuper@37906:  autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
neuper@37906: 
neuper@37906:  fetchProposedTactic 1;
neuper@37906:  setNextTactic 1 (Rewrite_Set "Test_simplify");
neuper@37906:  autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
neuper@37906: 
neuper@37906:  fetchProposedTactic 1;
neuper@37906:  setNextTactic 1 (Check_Postcond ["linear","univariate","equation","test"]);
neuper@37906:  autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
neuper@37906: 
neuper@37906:  val ((pt,_),_) = get_calc 1;
neuper@37906:  val ip = get_pos 1 1;
neuper@37906:  val (Form f, tac, asms) = pt_extract (pt, ip);
neuper@37906:      (*exception just above means: 'ModSpec' has been returned: error anyway*)
neuper@37906:  if term2str f = "[x = 1]" then () else 
neuper@38031:  error "FE-Kernel-interface.sml: diff.behav. in solve_linear as rootpbl";
neuper@37906: 
neuper@37906: 
neuper@37906: 
neuper@37906: "--------- inspect the CalcTree No.1 with Iterator No.2 ---------";
neuper@37906: "--------- inspect the CalcTree No.1 with Iterator No.2 ---------";
neuper@37906: "--------- inspect the CalcTree No.1 with Iterator No.2 ---------";
neuper@37906: (*WN041118: inspection shifted to Iterator No.1, because others need pos'*)
neuper@37906:  moveActiveRoot 1; 
neuper@37906:  refFormula 1 ([],Pbl); getTactic 1 ([],Pbl);(*Error*)
neuper@37906:  moveActiveDown 1; 
neuper@37906:  refFormula 1 ([1],Frm); getTactic 1 ([1],Frm);(*Error*)
neuper@37906:  moveActiveDown 1 ; 
neuper@37906:  refFormula 1 ([1],Res); getTactic 1 ([1],Res);(*OK*) 
neuper@37906:  (*getAssumption 1 ([1],Res); TODO.WN041217*)
neuper@37906:  moveActiveDown 1 ; refFormula 1 ([2],Res);
neuper@37906:  moveActiveCalcHead 1; refFormula 1 ([],Pbl);
neuper@37906:  moveActiveDown 1;
neuper@37906:  moveActiveDown 1;
neuper@37906:  moveActiveDown 1;
neuper@37906:  if get_pos 1 1 = ([2], Res) then () else 
neuper@38031:  error "FE-interface.sml: diff.behav. in a inspect 1 with Iterator 2";
neuper@37906:  moveActiveDown 1; refFormula 1 ([], Res);
neuper@37906:  if get_pos 1 1 = ([], Res) then () else 
neuper@38031:  error "FE-interface.sml: diff.behav. in b inspect 1 with Iterator 2";
neuper@37906:  moveActiveCalcHead 1; refFormula 1 ([],Pbl);
neuper@37906: 
neuper@37906: 
neuper@37906: 
neuper@37906: "---------------- miniscript with mini-subpbl --------------------";
neuper@37906: "---------------- miniscript with mini-subpbl --------------------";
neuper@37906: "---------------- miniscript with mini-subpbl --------------------";
neuper@37906:  states:=[];
neuper@37906:  CalcTree      (*start of calculation, return No.1*)
neuper@37906:  [(["equality (x+1=2)", "solveFor x","solutions L"], 
neuper@37906:    ("Test.thy", 
neuper@37906:     ["sqroot-test","univariate","equation","test"],
neuper@37906:     ["Test","squ-equ-test-subpbl1"]))];
neuper@37906:  Iterator 1;
neuper@37906: 
neuper@37906:  moveActiveRoot 1; 
neuper@37906:  refFormula 1 (get_pos 1 1);
neuper@37906:  fetchProposedTactic 1;
neuper@37906:  setNextTactic 1 (Model_Problem);
neuper@37906:  autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*gets ModSpec;model is still empty*)
neuper@37906: 
neuper@37906:  fetchProposedTactic 1;
neuper@37906:  setNextTactic 1 (Add_Given "equality (x + 1 = 2)");
neuper@37906:  autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
neuper@37906: 
neuper@37906:  fetchProposedTactic 1;
neuper@37906:  setNextTactic 1 (Add_Given "solveFor x");
neuper@37906:  autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
neuper@37906: 
neuper@37906:  fetchProposedTactic 1;
neuper@37906:  setNextTactic 1 (Add_Find "solutions L");
neuper@37906:  autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
neuper@37906: 
neuper@37906:  fetchProposedTactic 1;
neuper@37906:  setNextTactic 1 (Specify_Theory "Test.thy");
neuper@37906:  autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
neuper@37906: 
neuper@37906:  fetchProposedTactic 1;
neuper@37906:  setNextTactic 1 (Specify_Problem 
neuper@37906: 		      ["sqroot-test","univariate","equation","test"]);
neuper@37906:  autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
neuper@37906: "1-----------------------------------------------------------------";
neuper@37906: 
neuper@37906:  fetchProposedTactic 1;
neuper@37906:  setNextTactic 1 (Specify_Method ["Test","squ-equ-test-subpbl1"]);
neuper@37906:  autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
neuper@37906: 
neuper@37906:  fetchProposedTactic 1;
neuper@37906:  setNextTactic 1 (Apply_Method ["Test","squ-equ-test-subpbl1"]);
neuper@37906:  autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
neuper@37906: 
neuper@37906:  fetchProposedTactic 1;
neuper@37906:  setNextTactic 1 (Rewrite_Set "norm_equation");
neuper@37906:  autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
neuper@37906: 
neuper@37906:  fetchProposedTactic 1;
neuper@37906:  setNextTactic 1 (Rewrite_Set "Test_simplify");
neuper@37906:  autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
neuper@37906: 
neuper@37906:  fetchProposedTactic 1;(*----------------Subproblem--------------------*);
neuper@37906:  setNextTactic 1 (Subproblem ("Test.thy",
neuper@37906: 			      ["linear","univariate","equation","test"]));
neuper@37906:  autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
neuper@37906: 
neuper@37906:  fetchProposedTactic 1;
neuper@37906:  setNextTactic 1 (Model_Problem );
neuper@37906:  autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
neuper@37906: 
neuper@37906:  fetchProposedTactic 1;
neuper@37906:  setNextTactic 1 (Add_Given "equality (-1 + x = 0)");
neuper@37906:  autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
neuper@37906: 
neuper@37906:  fetchProposedTactic 1;
neuper@37906:  setNextTactic 1 (Add_Given "solveFor x");
neuper@37906:  autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
neuper@37906: 
neuper@37906:  fetchProposedTactic 1;
neuper@37906:  setNextTactic 1 (Add_Find "solutions x_i");
neuper@37906:  autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
neuper@37906: 
neuper@37906:  fetchProposedTactic 1;
neuper@37906:  setNextTactic 1 (Specify_Theory "Test.thy");
neuper@37906:  autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
neuper@37906: 
neuper@37906:  fetchProposedTactic 1;
neuper@37906:  setNextTactic 1 (Specify_Problem ["linear","univariate","equation","test"]);
neuper@37906:  autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
neuper@37906: "2-----------------------------------------------------------------";
neuper@37906: 
neuper@37906:  fetchProposedTactic 1;
neuper@37906:  setNextTactic 1 (Specify_Method ["Test","solve_linear"]);
neuper@37906:  autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
neuper@37906: 
neuper@37906:  fetchProposedTactic 1;
neuper@37906:  setNextTactic 1 (Apply_Method ["Test","solve_linear"]);
neuper@37906:  autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
neuper@37906: 
neuper@37906:  fetchProposedTactic 1;
neuper@37906:  setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "isolate_bdv"));
neuper@37906:  autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
neuper@37906: 
neuper@37906:  fetchProposedTactic 1;
neuper@37906:  setNextTactic 1 (Rewrite_Set "Test_simplify");
neuper@37906:  autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
neuper@37906: 
neuper@37906:  fetchProposedTactic 1;
neuper@37906:  setNextTactic 1 (Check_Postcond ["linear","univariate","equation","test"]);
neuper@37906:  autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
neuper@37906: 
neuper@37906:  fetchProposedTactic 1;
neuper@37906:  setNextTactic 1 (Check_elementwise "Assumptions");
neuper@37906:  autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
neuper@37906: 
neuper@37906:  val xml = fetchProposedTactic 1;
neuper@37906:  setNextTactic 1 (Check_Postcond 
neuper@37906: 		      ["sqroot-test","univariate","equation","test"]);
neuper@37906:  autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
neuper@37906: 
neuper@37906:  val ((pt,_),_) = get_calc 1;
neuper@37906:  val str = pr_ptree pr_short pt;
neuper@37906:  writeln str;
neuper@37906:  val ip = get_pos 1 1;
neuper@37906:  val (Form f, tac, asms) = pt_extract (pt, ip);
neuper@37906:      (*exception just above means: 'ModSpec' has been returned: error anyway*)
neuper@37906:  if term2str f = "[x = 1]" then () else 
neuper@38031:  error "FE-interface.sml: diff.behav. in miniscript with mini-subpb";
neuper@37906: 
neuper@37906:  DEconstrCalcTree 1;
neuper@37906: 
neuper@37906: 
neuper@37906: "--------- miniscript with mini-subpbl AUTOCALCULATE Step 1-------";
neuper@37906: "--------- miniscript with mini-subpbl AUTOCALCULATE Step 1-------";
neuper@37906: "--------- miniscript with mini-subpbl AUTOCALCULATE Step 1-------";
neuper@37906:  states:=[];
neuper@37906:  CalcTree
neuper@37906:  [(["equality (x+1=2)", "solveFor x","solutions L"], 
neuper@37906:    ("Test.thy", 
neuper@37906:     ["sqroot-test","univariate","equation","test"],
neuper@37906:     ["Test","squ-equ-test-subpbl1"]))];
neuper@37906:  Iterator 1;
neuper@37906:  moveActiveRoot 1;
neuper@37906:  autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
neuper@37906:  autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
neuper@37906:  autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
neuper@37906:  autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
neuper@37906:  autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
neuper@37906:  autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
neuper@37906:  autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
neuper@37906:  autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
neuper@37906:  (*here the solve-phase starts*)
neuper@37906:  autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
neuper@37906:  autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
neuper@37906:  autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
neuper@37906:  (*------------------------------------*)
neuper@37906: (* print_depth 13; get_calc 1;
neuper@37906:    *)
neuper@37906:  autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
neuper@37906:  (*calc-head of subproblem*)
neuper@37906:  autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
neuper@37906:  autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
neuper@37906:  autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
neuper@37906:  autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
neuper@37906:  autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
neuper@37906:  autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
neuper@37906:  autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
neuper@37906:  (*solve-phase of the subproblem*)
neuper@37906:  autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
neuper@37906:  autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
neuper@37906:  autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
neuper@37906:  autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
neuper@37906:  (*finish subproblem*)
neuper@37906:  autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
neuper@37906:  (*finish problem*)
neuper@37906:  autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); 
neuper@37906: 
neuper@37906:  (*this checks the test for correctness..*)
neuper@37906:  val ((pt,_),_) = get_calc 1;
neuper@37906:  val p = get_pos 1 1;
neuper@37906:  val (Form f, tac, asms) = pt_extract (pt, p);
neuper@37906:  if term2str f = "[x = 1]" andalso p = ([], Res) then () else 
neuper@38031:  error "FE-interface.sml: diff.behav. in miniscript with mini-subpb";
neuper@37906: 
neuper@37906:  DEconstrCalcTree 1;
neuper@37906: 
neuper@37906: "--------- solve_linear as rootpbl AUTOCALCULATE CompleteCalc ----";
neuper@37906: "--------- solve_linear as rootpbl AUTOCALCULATE CompleteCalc ----";
neuper@37906: "--------- solve_linear as rootpbl AUTOCALCULATE CompleteCalc ----";
neuper@37906:  states:=[];
neuper@37906:  CalcTree
neuper@37906:      [(["equality (1+-1*2+x=0)", "solveFor x","solutions L"],
neuper@37906:        ("Test.thy", 
neuper@37906: 	["linear","univariate","equation","test"],
neuper@37906: 	["Test","solve_linear"]))];
neuper@37906:  Iterator 1;
neuper@37906:  moveActiveRoot 1;
neuper@37906: getFormulaeFromTo 1 ([],Pbl) ([],Pbl) 999 false;
neuper@37906: 
neuper@37906:  autoCalculate 1 CompleteCalc; 
neuper@37906:  val (unc, del, gen) = (([],Pbl), ([],Pbl), ([],Res));
neuper@37906:  getFormulaeFromTo 1 unc gen 1 (*only level 1*) false;
neuper@37906: 
neuper@37906:  val ((pt,_),_) = get_calc 1;
neuper@37906:  val p = get_pos 1 1;
neuper@37906:  val (Form f, tac, asms) = pt_extract (pt, p);
neuper@37906:  if term2str f = "[x = 1]" andalso p = ([], Res) then () else 
neuper@38031:  error "FE-interface.sml: diff.behav. in solve_linear/rt AUTOCALCULATE ";
neuper@37906: 
neuper@37906: 
neuper@37906: "--------- solve_linear as rootpbl AUTOCALC CompleteHead/Calc ----";
neuper@37906: "--------- solve_linear as rootpbl AUTOCALC CompleteHead/Calc ----";
neuper@37906: "--------- solve_linear as rootpbl AUTOCALC CompleteHead/Calc ----";
neuper@37906:  states:=[];
neuper@37906:  CalcTree
neuper@37906:      [(["equality (1+-1*2+x=0)", "solveFor x","solutions L"],
neuper@37906:        ("Test.thy", 
neuper@37906: 	["linear","univariate","equation","test"],
neuper@37906: 	["Test","solve_linear"]))];
neuper@37906:  Iterator 1;
neuper@37906:  moveActiveRoot 1;
neuper@37906:  autoCalculate 1 CompleteCalcHead;
neuper@37906:  refFormula 1 (get_pos 1 1);
neuper@37906:  val ((pt,p),_) = get_calc 1;
neuper@37906: 
neuper@37906: 
neuper@37906: 
neuper@37906:  autoCalculate 1 CompleteCalc; 
neuper@37906:  val ((pt,p),_) = get_calc 1;
neuper@37906:  if p=([], Res) then () else 
neuper@38031:  error "FE-interface.sml: diff.behav. in solve_linear AUTOC Head/Calc ";
neuper@37906: 
neuper@37906: 
neuper@37906: "--------- miniscript with mini-subpbl AUTOCALCULATE CompleteCalc-";
neuper@37906: "--------- miniscript with mini-subpbl AUTOCALCULATE CompleteCalc-";
neuper@37906: "--------- miniscript with mini-subpbl AUTOCALCULATE CompleteCalc-";
neuper@37906:  states:=[];
neuper@37906:  CalcTree
neuper@37906:  [(["equality (x+1=2)", "solveFor x","solutions L"], 
neuper@37906:    ("Test.thy", 
neuper@37906:     ["sqroot-test","univariate","equation","test"],
neuper@37906:     ["Test","squ-equ-test-subpbl1"]))];
neuper@37906:  Iterator 1;
neuper@37906:  moveActiveRoot 1;
neuper@37906:  autoCalculate 1 CompleteCalc;
neuper@37906: 
neuper@37906: (*
neuper@37906: getTactic 1 ([1],Frm);
neuper@37906: getTactic 1 ([1],Res);
neuper@37906: initContext 1 Thy_ ([1],Res);
neuper@37906: *)
neuper@37906: 
neuper@37906:  (*... returns calcChangedEvent with*)
neuper@37906:  val (unc, del, gen) = (([],Pbl), ([],Pbl), ([],Res));
neuper@37906:  getFormulaeFromTo 1 unc gen 0 (*only result*) false;
neuper@37906:  getFormulaeFromTo 1 unc gen 1 (*only level 1*) false;
neuper@37906:  getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
neuper@37906: 
neuper@37906:  val ((pt,_),_) = get_calc 1;
neuper@37906:  val p = get_pos 1 1;
neuper@37906:  val (Form f, tac, asms) = pt_extract (pt, p);
neuper@37906:  if term2str f = "[x = 1]" andalso p = ([], Res) then () else 
neuper@38031:  error "FE-interface.sml: diff.behav. in mini-subpbl AUTOCALCULATE 6";
neuper@37906: 
neuper@37906: 
neuper@37906: "--------- miniscript with mini-subpbl AUTO CompleteCalcHead------";
neuper@37906: "--------- miniscript with mini-subpbl AUTO CompleteCalcHead------";
neuper@37906: "--------- miniscript with mini-subpbl AUTO CompleteCalcHead------";
neuper@37906:  states:=[];
neuper@37906:  CalcTree
neuper@37906:  [(["equality (x+1=2)", "solveFor x","solutions L"], 
neuper@37906:    ("Test.thy", 
neuper@37906:     ["sqroot-test","univariate","equation","test"],
neuper@37906:     ["Test","squ-equ-test-subpbl1"]))];
neuper@37906:  Iterator 1;
neuper@37906: (* doesn't terminate !!!
neuper@37906:  autoCalculate 1 CompleteCalcHead; 
neuper@37906: *)
neuper@37906: 
neuper@37906: "--------- solve_linear as rootpbl AUTOCALCULATE CompleteModel ---";
neuper@37906: "--------- solve_linear as rootpbl AUTOCALCULATE CompleteModel ---";
neuper@37906: "--------- solve_linear as rootpbl AUTOCALCULATE CompleteModel ---";
neuper@37906:  states:=[];
neuper@37906:  CalcTree
neuper@37906:      [(["equality (1+-1*2+x=0)", "solveFor x","solutions L"],
neuper@37906:        ("Test.thy", 
neuper@37906: 	["linear","univariate","equation","test"],
neuper@37906: 	["Test","solve_linear"]))];
neuper@37906:  Iterator 1;
neuper@37906:  moveActiveRoot 1;
neuper@37906:  autoCalculate 1 CompleteModel; 
neuper@37906:  refFormula 1 (get_pos 1 1);
neuper@37906: 
neuper@37906: setProblem 1 ["linear","univariate","equation","test"];
neuper@37906: val pos = get_pos 1 1;
neuper@37906: setContext 1 pos (kestoreID2guh Pbl_["linear","univariate","equation","test"]);
neuper@37906:  refFormula 1 (get_pos 1 1);
neuper@37906: 
neuper@37906: setMethod 1 ["Test","solve_linear"];
neuper@37906: setContext 1 pos (kestoreID2guh Met_ ["Test","solve_linear"]);
neuper@37906:  refFormula 1 (get_pos 1 1);
neuper@37906:  val ((pt,_),_) = get_calc 1;
neuper@37906:  if get_obj g_spec pt [] = ("e_domID", 
neuper@37906: 			    ["linear", "univariate","equation","test"],
neuper@37906: 			    ["Test","solve_linear"]) then ()
neuper@38031:  else error "FE-interface.sml: diff.behav. in setProblem, setMethod";
neuper@37906: 
neuper@37906:  autoCalculate 1 CompleteCalcHead;
neuper@37906:  refFormula 1 (get_pos 1 1); 
neuper@37906:  autoCalculate 1 CompleteCalc; 
neuper@37906:  moveActiveDown 1;
neuper@37906:  moveActiveDown 1;
neuper@37906:  moveActiveDown 1;
neuper@37906:  refFormula 1 (get_pos 1 1); 
neuper@37906:  val ((pt,_),_) = get_calc 1;
neuper@37906:  val p = get_pos 1 1;
neuper@37906:  val (Form f, tac, asms) = pt_extract (pt, p);
neuper@37906:  if term2str f = "[x = 1]" andalso p = ([], Res) then () else 
neuper@38031:  error "FE-interface.sml: diff.behav. in mini-subpbl AUTOCALCULATE 6";
neuper@37906: 
neuper@37906: 
neuper@37906: "--------- setContext..Thy ---------------------------------------";
neuper@37906: "--------- setContext..Thy ---------------------------------------";
neuper@37906: "--------- setContext..Thy ---------------------------------------";
neuper@37906: states:=[];
neuper@37906: CalcTree
neuper@37906: [(["equality (x+1=2)", "solveFor x","solutions L"], 
neuper@37906:   ("Test.thy", 
neuper@37906:    ["sqroot-test","univariate","equation","test"],
neuper@37906:    ["Test","squ-equ-test-subpbl1"]))];
neuper@37906: Iterator 1; moveActiveRoot 1;
neuper@37906: autoCalculate 1 CompleteCalcHead;
neuper@37906: autoCalculate 1 (Step 1);
neuper@37906: val ((pt,p),_) = get_calc 1;  show_pt pt;
neuper@37906: (*
neuper@37906: setNextTactic 1 (Rewrite_Set "Test_simplify");
neuper@37906: autoCalculate 1 (Step 1);
neuper@37906: val ((pt,p),_) = get_calc 1;  show_pt pt;
neuper@37906: *)
neuper@37906: "-----^^^^^ and vvvvv do the same -----";
neuper@37906: setContext 1 p "thy_isac_Test-rls-Test_simplify";
neuper@37906: val ((pt,p),_) = get_calc 1;  show_pt pt;
neuper@37906: 
neuper@37906: autoCalculate 1 (Step 1);
neuper@37906: setContext 1 p "thy_isac_Test-rls-Test_simplify";
neuper@37906: val ((pt,p),_) = get_calc 1;  show_pt pt;
neuper@37906: 
neuper@37906: autoCalculate 1 CompleteCalc;
neuper@37906: 
neuper@37906: 
neuper@37906: 
neuper@37906: "--------- miniscript with mini-subpbl AUTOCALC CompleteToSubpbl -";
neuper@37906: "--------- miniscript with mini-subpbl AUTOCALC CompleteToSubpbl -";
neuper@37906: "--------- miniscript with mini-subpbl AUTOCALC CompleteToSubpbl -";
neuper@37906:  states:=[];
neuper@37906:  CalcTree
neuper@37906:  [(["equality (x+1=2)", "solveFor x","solutions L"], 
neuper@37906:    ("Test.thy", 
neuper@37906:     ["sqroot-test","univariate","equation","test"],
neuper@37906:     ["Test","squ-equ-test-subpbl1"]))];
neuper@37906:  Iterator 1; moveActiveRoot 1;
neuper@37906:  autoCalculate 1 CompleteToSubpbl;
neuper@37906:  refFormula 1 (get_pos 1 1); (*<ISA> -1 + x = 0 </ISA>*);
neuper@37906:  val ((pt,_),_) = get_calc 1;
neuper@37906:  val str = pr_ptree pr_short pt;
neuper@37906:  writeln str;
neuper@37906:  if str = ".    ----- pblobj -----\n1.   x + 1 = 2\n2.   x + 1 + -1 * 2 = 0\n"
neuper@37906:  then () else 
neuper@38031:  error "FE-interface.sml: diff.behav. in mini-subpbl CompleteToSubpbl-1";
neuper@37906: 
neuper@37906:  autoCalculate 1 (Step 1); (*proceeds only, of NOT 1 step before subplb*)
neuper@37906:  autoCalculate 1 CompleteToSubpbl;
neuper@37906:  val ((pt,_),_) = get_calc 1;
neuper@37906:  val str = pr_ptree pr_short pt;
neuper@37906:  writeln str;
neuper@37906:  autoCalculate 1 CompleteCalc; (*das geht ohnehin !*);
neuper@37906:  val ((pt,_),_) = get_calc 1;
neuper@37906:  val p = get_pos 1 1;
neuper@37906:  val (Form f, tac, asms) = pt_extract (pt, p);
neuper@37906:  if term2str f = "[x = 1]" andalso p = ([], Res) then () else 
neuper@38031:  error "FE-interface.sml: diff.behav. in mini-subpbl CompleteToSubpbl 1";
neuper@37906: 
neuper@37906: 
neuper@37906: 
neuper@37906: "---------------- rat-eq + subpbl: no_met, NO solution dropped ---";
neuper@37906: "---------------- rat-eq + subpbl: no_met, NO solution dropped ---";
neuper@37906: "---------------- rat-eq + subpbl: no_met, NO solution dropped ---";
neuper@37906:  states:=[];
neuper@37906:  CalcTree
neuper@37906:  [(["equality ((5*x)/(x - 2) - x/(x+2)=4)", "solveFor x","solutions L"],
neuper@37906:    ("RatEq.thy", ["univariate","equation"], ["no_met"]))];
neuper@37906:  Iterator 1;
neuper@37906:  moveActiveRoot 1; 
neuper@37906:  fetchProposedTactic 1;
neuper@37906:  setNextTactic 1 (Model_Problem );
neuper@37906:  autoCalculate 1 (Step 1); fetchProposedTactic 1;
neuper@37926: (*-----since Model_Problem + complete_mod_ in case cas of SOME-----*
neuper@37906:  setNextTactic 1 (Add_Given "equality (5 * x / (x - 2) - x / (x + 2) = 4)");
neuper@37906:  autoCalculate 1 (Step 1); fetchProposedTactic 1;
neuper@37906:  setNextTactic 1 (Add_Given "solveFor x");
neuper@37906:  autoCalculate 1 (Step 1); fetchProposedTactic 1;
neuper@37906:  setNextTactic 1 (Add_Find "solutions L");
neuper@37906:  autoCalculate 1 (Step 1); fetchProposedTactic 1;
neuper@37926: *-----since Model_Problem + complete_mod_ in case cas of SOME-----*)
neuper@37906:  setNextTactic 1 (Specify_Theory "RatEq.thy");
neuper@37906:  autoCalculate 1 (Step 1); fetchProposedTactic 1;
neuper@37906:  setNextTactic 1 (Specify_Problem ["rational","univariate","equation"]);
neuper@37906:  autoCalculate 1 (Step 1); fetchProposedTactic 1;
neuper@37906:  setNextTactic 1 (Specify_Method ["RatEq","solve_rat_equation"]);
neuper@37906:  autoCalculate 1 (Step 1); fetchProposedTactic 1;
neuper@37906:  setNextTactic 1 (Apply_Method ["RatEq","solve_rat_equation"]);
neuper@37906:  autoCalculate 1 (Step 1); fetchProposedTactic 1;
neuper@37906:  setNextTactic 1 (Rewrite_Set "RatEq_simplify");
neuper@37906:  autoCalculate 1 (Step 1); fetchProposedTactic 1;
neuper@37906:  setNextTactic 1 (Rewrite_Set "norm_Rational");
neuper@37906:  autoCalculate 1 (Step 1); fetchProposedTactic 1;
neuper@37906:  setNextTactic 1 (Rewrite_Set "RatEq_eliminate");
neuper@37906:  autoCalculate 1 (Step 1); fetchProposedTactic 1;
neuper@37906:  (*               __________ for "12 * x + 4 * x ^^^ 2 = 4 * (-4 + x ^^^ 2)"*)
neuper@37906:  setNextTactic 1 (Subproblem ("PolyEq.thy", ["normalize","polynomial",
neuper@37906: 					    "univariate","equation"]));
neuper@37906:  autoCalculate 1 (Step 1); fetchProposedTactic 1;
neuper@37906:  setNextTactic 1 (Model_Problem );
neuper@37906:  autoCalculate 1 (Step 1); fetchProposedTactic 1;
neuper@37926: (*-----since Model_Problem + complete_mod_ in case cas of SOME-----*
neuper@37906:  setNextTactic 1 (Add_Given 
neuper@37906: 		      "equality (12 * x + 4 * x ^^^ 2 = 4 * (-4 + x ^^^ 2))");
neuper@37906:  autoCalculate 1 (Step 1); fetchProposedTactic 1;
neuper@37906:  setNextTactic 1 (Add_Given "solveFor x");
neuper@37906:  autoCalculate 1 (Step 1); fetchProposedTactic 1;
neuper@37906:  setNextTactic 1 (Add_Find "solutions x_i");
neuper@37906:  autoCalculate 1 (Step 1); fetchProposedTactic 1;
neuper@37926: *-----since Model_Problem + complete_mod_ in case cas of SOME-----*)
neuper@37906:  setNextTactic 1 (Specify_Theory "PolyEq.thy");
neuper@37906:  autoCalculate 1 (Step 1); fetchProposedTactic 1;
neuper@37906:  setNextTactic 1 (Specify_Problem ["normalize","polynomial",
neuper@37906: 				   "univariate","equation"]);
neuper@37906:  autoCalculate 1 (Step 1); fetchProposedTactic 1;
neuper@37906:  setNextTactic 1 (Specify_Method ["PolyEq","normalize_poly"]);
neuper@37906:  autoCalculate 1 (Step 1); fetchProposedTactic 1;
neuper@37906:  setNextTactic 1 (Apply_Method ["PolyEq","normalize_poly"]);
neuper@37906:  autoCalculate 1 (Step 1); fetchProposedTactic 1;
neuper@37906:  setNextTactic 1 (Rewrite ("all_left",""));
neuper@37906:  autoCalculate 1 (Step 1); fetchProposedTactic 1;
neuper@37906:  setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "make_ratpoly_in"));
neuper@37906:  autoCalculate 1 (Step 1); fetchProposedTactic 1;
neuper@37906:  (*               __________ for "16 + 12 * x = 0"*)
neuper@37906:  setNextTactic 1 (Subproblem ("PolyEq.thy",
neuper@37906: 			 ["degree_1","polynomial","univariate","equation"]));
neuper@37906:  autoCalculate 1 (Step 1); fetchProposedTactic 1;
neuper@37906:  setNextTactic 1 (Model_Problem );
neuper@37906:  autoCalculate 1 (Step 1); fetchProposedTactic 1;
neuper@37926: (*-----since Model_Problem + complete_mod_ in case cas of SOME-----*
neuper@37906:  setNextTactic 1 (Add_Given 
neuper@37906: 		      "equality (16 + 12 * x = 0)");
neuper@37906:  autoCalculate 1 (Step 1); fetchProposedTactic 1;
neuper@37906:  setNextTactic 1 (Add_Given "solveFor x");
neuper@37906:  autoCalculate 1 (Step 1); fetchProposedTactic 1;
neuper@37906:  setNextTactic 1 (Add_Find "solutions x_i");
neuper@37906:  autoCalculate 1 (Step 1); fetchProposedTactic 1;
neuper@37926: *-----since Model_Problem + complete_mod_ in case cas of SOME-----*)
neuper@37906:  setNextTactic 1 (Specify_Theory "PolyEq.thy");
neuper@37906:  (*------------- some trials in the problem-hierarchy ---------------*)
neuper@37906:  setNextTactic 1 (Specify_Problem ["linear","univariate","equation"]);
neuper@37906:  autoCalculate 1 (Step 1); fetchProposedTactic 1; (*<ERROR> helpless </ERROR> !!!*)
neuper@37906:  setNextTactic 1 (Refine_Problem ["univariate","equation"]);
neuper@37906: 
neuper@37906: 
neuper@37906: 
neuper@37906: 
neuper@37906: 
neuper@37906:  (*------------------------------------------------------------------*)
neuper@37906:  autoCalculate 1 (Step 1); fetchProposedTactic 1;
neuper@37906:  setNextTactic 1 (Specify_Method ["PolyEq","solve_d1_polyeq_equation"]);
neuper@37906:  autoCalculate 1 (Step 1); fetchProposedTactic 1;
neuper@37906:  setNextTactic 1 (Apply_Method ["PolyEq","solve_d1_polyeq_equation"]);
neuper@37906:  autoCalculate 1 (Step 1); fetchProposedTactic 1;
neuper@37906:  setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "d1_polyeq_simplify"));
neuper@37906:  autoCalculate 1 (Step 1); fetchProposedTactic 1;
neuper@37906:  setNextTactic 1 (Rewrite_Set "polyeq_simplify");
neuper@37906:  autoCalculate 1 (Step 1); fetchProposedTactic 1;
neuper@37906:  (*==================================================================*)
neuper@37906:  setNextTactic 1 Or_to_List;
neuper@37906:  autoCalculate 1 (Step 1); fetchProposedTactic 1;
neuper@37906:  setNextTactic 1 (Check_elementwise "Assumptions");
neuper@37906:  autoCalculate 1 (Step 1); fetchProposedTactic 1;
neuper@37906:  setNextTactic 1 (Check_Postcond ["degree_1","polynomial",
neuper@37906: 				 "univariate","equation"]);
neuper@37906:  autoCalculate 1 (Step 1); fetchProposedTactic 1;
neuper@37906:  setNextTactic 1 (Check_Postcond ["normalize","polynomial",
neuper@37906: 				   "univariate","equation"]);
neuper@37906:  autoCalculate 1 (Step 1); fetchProposedTactic 1;
neuper@37906:  setNextTactic 1 (Check_elementwise "Assumptions");
neuper@37906:  autoCalculate 1 (Step 1); fetchProposedTactic 1;
neuper@37906:  setNextTactic 1 (Check_Postcond ["rational","univariate","equation"]);
neuper@37906:  val (ptp,_) = get_calc 1;
neuper@37906:  val (Form t,_,_) = pt_extract ptp;
neuper@37906:  if get_pos 1 1 = ([], Res) andalso term2str t = "[x = -4 / 3]" then ()
neuper@37906:  else writeln "FE-inteface.sml: diff.behav. in rat-eq + subpbl: no_met, NO ..";
neuper@37906: 
neuper@37906: 
neuper@37906: "---------------- tryMatchProblem, tryRefineProblem --------------";
neuper@37906: "---------------- tryMatchProblem, tryRefineProblem --------------";
neuper@37906: "---------------- tryMatchProblem, tryRefineProblem --------------";
neuper@37906: (*{\bf\UC{Having \isac{} Refine the Problem
neuper@37906:  * Automatically}\label{SPECIFY:refine-auto}\\} test match and refine with
neuper@37906:  * x^^^2 + 4*x + 5 = 2
neuper@37906: see isac.bridge.TestSpecify#testMatchRefine*)
neuper@37906:  DEconstrCalcTree 1;
neuper@37906:  CalcTree
neuper@37906:  [(["equality (x^2 + 4*x + 5 = 2)", "solveFor x","solutions L"],
neuper@37906:    ("Isac.thy", 
neuper@37906:     ["univariate","equation"],
neuper@37906:     ["no_met"]))];
neuper@37906:  Iterator 1;
neuper@37906:  moveActiveRoot 1; 
neuper@37906: 
neuper@37906:  fetchProposedTactic 1;
neuper@37906:  setNextTactic 1 (Model_Problem );
neuper@37906:  (*..this tactic should be done 'tacitly', too !*)
neuper@37906: 
neuper@37906: (*
neuper@37906: autoCalculate 1 CompleteCalcHead; 
neuper@37906: checkContext 1 ([],Pbl) "pbl_equ_univ";
neuper@37906: checkContext 1 ([],Pbl) (kestoreID2guh Pbl_ ["univariate","equation"]);
neuper@37906: *)
neuper@37906: 
neuper@37906:  autoCalculate 1 (Step 1); 
neuper@37906: 
neuper@37906:  fetchProposedTactic 1;
neuper@37906:  setNextTactic 1 (Add_Given "equality (x ^^^ 2 + 4 * x + 5 = 2)");
neuper@37906:  autoCalculate 1 (Step 1); 
neuper@37906: 
neuper@37906:  "--------- we go into the ProblemBrowser (_NO_ pblID selected) -";
neuper@37906: initContext 1 Pbl_ ([],Pbl);
neuper@37906: initContext 1 Met_ ([],Pbl);
neuper@37906: 
neuper@37906:  "--------- this match will show some incomplete items: ---------";
neuper@37906: checkContext 1 ([],Pbl) (kestoreID2guh Pbl_ ["univariate","equation"]);
neuper@37906: checkContext 1 ([],Pbl) (kestoreID2guh Met_ ["LinEq", "solve_lineq_equation"]);
neuper@37906: 
neuper@37906: 
neuper@37906:  fetchProposedTactic 1;
neuper@37906:  setNextTactic 1 (Add_Given "solveFor x"); autoCalculate 1 (Step 1);
neuper@37906: 
neuper@37906:  fetchProposedTactic 1;
neuper@37906:  setNextTactic 1 (Add_Find "solutions L"); autoCalculate 1 (Step 1);
neuper@37906: 
neuper@37906:  "--------- this is a matching model (all items correct): -------";
neuper@37906: checkContext 1  ([],Pbl) (kestoreID2guh Pbl_ ["univariate","equation"]);
neuper@37906:  "--------- this is a NOT matching model (some 'false': ---------";
neuper@37906: checkContext 1  ([],Pbl)(kestoreID2guh Pbl_["linear","univariate","equation"]);
neuper@37906: 
neuper@37906:  "--------- find out a matching problem: ------------------------";
neuper@37906:  "--------- find out a matching problem (FAILING: no new pbl) ---";
neuper@37906:  refineProblem 1([],Pbl)(pblID2guh ["linear","univariate","equation"]);
neuper@37906: 
neuper@37906:  "--------- find out a matching problem (SUCCESSFUL) ------------";
neuper@37906:  refineProblem 1 ([],Pbl) (pblID2guh ["univariate","equation"]);
neuper@37906: 
neuper@37906:  "--------- tryMatch, tryRefine did not change the calculation -";
neuper@37906:  "--------- this is done by <TRANSFER> on the pbl-browser: ------";
neuper@37906:  setNextTactic 1 (Specify_Problem ["normalize","polynomial",
neuper@37906: 				 "univariate","equation"]);
neuper@37906:  autoCalculate 1 (Step 1);
neuper@37906: (*WN050904 fetchProposedTactic again --> Specify_Problem ["normalize",...
neuper@37906:   and Specify_Theory skipped in comparison to below ---^^^-inserted      *)
neuper@37906: (*------------vvv-inserted-----------------------------------------------*)
neuper@37906:  fetchProposedTactic 1;
neuper@37906:  setNextTactic 1 (Specify_Problem ["normalize","polynomial",
neuper@37906: 				 "univariate","equation"]);
neuper@37906:  autoCalculate 1 (Step 1);
neuper@37906: 
neuper@37906: (*and Specify_Theory skipped by fetchProposedTactic ?!?*)
neuper@37906: 
neuper@37906:  fetchProposedTactic 1;
neuper@37906:  setNextTactic 1 (Specify_Method ["PolyEq","normalize_poly"]);
neuper@37906:  autoCalculate 1 (Step 1);
neuper@37906: 
neuper@37906:  fetchProposedTactic 1;
neuper@37906:  setNextTactic 1 (Apply_Method ["PolyEq","normalize_poly"]);
neuper@37906:  autoCalculate 1 CompleteCalc;
neuper@37906:  val ((pt,_),_) = get_calc 1;
neuper@37906:  show_pt pt;
neuper@37906:  val p = get_pos 1 1;
neuper@37906:  val (Form f, tac, asms) = pt_extract (pt, p);
neuper@37906:  if term2str f = "[x = -1, x = -3]" andalso p = ([], Res) then () else 
neuper@38031:  error "FE-interface.sml: diff.behav. in tryMatchProblem, tryRefine";
neuper@37906: 
neuper@37906: (*------------^^^-inserted-----------------------------------------------*)
neuper@37906: (*WN050904 the fetchProposedTactic's below may not have worked like that
neuper@37906:   before, too, because there was no check*)
neuper@37906:  fetchProposedTactic 1;
neuper@37906:  setNextTactic 1 (Specify_Theory "PolyEq.thy");
neuper@37906:  autoCalculate 1 (Step 1);
neuper@37906: 
neuper@37906:  fetchProposedTactic 1;
neuper@37906:  setNextTactic 1 (Specify_Method ["PolyEq","normalize_poly"]);
neuper@37906:  autoCalculate 1 (Step 1);
neuper@37906: 
neuper@37906:  fetchProposedTactic 1;
neuper@37906:  "--------- now the calc-header is ready for enter 'solving' ----";
neuper@37906:  autoCalculate 1 CompleteCalc;
neuper@37906: 
neuper@37906:  val ((pt,_),_) = get_calc 1;
neuper@37906: rootthy pt;
neuper@37906:  show_pt pt;
neuper@37906:  val p = get_pos 1 1;
neuper@37906:  val (Form f, tac, asms) = pt_extract (pt, p);
neuper@37906:  if term2str f = "[x = -1, x = -3]" andalso p = ([], Res) then () else 
neuper@38031:  error "FE-interface.sml: diff.behav. in tryMatchProblem, tryRefine";
neuper@37906: 
neuper@37906: 
neuper@37906: "--------- modifyCalcHead, resetCalcHead, modelProblem ------------";
neuper@37906: "--------- modifyCalcHead, resetCalcHead, modelProblem ------------";
neuper@37906: "--------- modifyCalcHead, resetCalcHead, modelProblem ------------";
neuper@37906: 
neuper@37906:  states:=[]; 
neuper@37906:  DEconstrCalcTree 1;
neuper@37906:  CalcTree
neuper@37906:  [(["equality (x+1=2)", "solveFor x","solutions L"], 
neuper@37906:    ("Test.thy", 
neuper@37906:     ["sqroot-test","univariate","equation","test"],
neuper@37906:     ["Test","squ-equ-test-subpbl1"]))];
neuper@37906:  Iterator 1;
neuper@37906:  moveActiveRoot 1; 
neuper@37906: 
neuper@37906:  modifyCalcHead 1 (([],Pbl),(*the position from refFormula*)
neuper@37906: 		  "solve (x+1=2, x)",(*the headline*)
neuper@37906: 		  [Given ["equality (x+1=2)", "solveFor x"],
neuper@37906: 		   Find ["solutions L"](*,Relate []*)],
neuper@37906: 		  Pbl, 
neuper@37906: 		  ("Test.thy", 
neuper@37906: 		   ["sqroot-test","univariate","equation","test"],
neuper@37906: 		   ["Test","squ-equ-test-subpbl1"]));
neuper@37906: resetCalcHead 1;
neuper@37906: modelProblem 1;
neuper@37906: 
neuper@37906: 
neuper@37906: "---------------- maximum-example, UC: Modeling an example -------";
neuper@37906: "---------------- maximum-example, UC: Modeling an example -------";
neuper@37906: "---------------- maximum-example, UC: Modeling an example -------";
neuper@37906: (* {\bf\UC{Editing the Model}\label{SPECIFY:enter}\label{SPECIFY:check}\\}
neuper@37906: see isac.bridge.TestModel#testEditItems
neuper@37906: *)
neuper@37906:  val elems = ["fixedValues [r=Arbfix]","maximum A","valuesFor [a,b]",
neuper@37906: 	      "relations [A=a*b, (a/2)^2 + (b/2)^2 = r^2]",
neuper@37906: 	      "relations [A=a*b, (a/2)^2 + (b/2)^2 = r^2]",
neuper@37906: 	      "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]",
neuper@37906: 	      (*^^^ these are the elements for the root-problem (in variants)*)
neuper@37906:               (*vvv these are elements required for subproblems*)
neuper@37906: 	      "boundVariable a","boundVariable b","boundVariable alpha",
neuper@37906: 	      "interval {x::real. 0 <= x & x <= 2*r}",
neuper@37906: 	      "interval {x::real. 0 <= x & x <= 2*r}",
neuper@37906: 	      "interval {x::real. 0 <= x & x <= pi}",
neuper@37906: 	      "errorBound (eps=(0::real))"]
neuper@37906:  (*specifying is not interesting for this example*)
neuper@37906:  val spec = ("DiffApp.thy", ["maximum_of","function"], 
neuper@37906: 	     ["DiffApp","max_by_calculus"]);
neuper@37906:  (*the empty model with descriptions for user-guidance by Model_Problem*)
neuper@37906:  val empty_model = [Given ["fixedValues []"],
neuper@37906: 		    Find ["maximum", "valuesFor"],
neuper@37906: 		    Relate ["relations []"]];
neuper@37906:  states:=[];
neuper@37906:  DEconstrCalcTree 1;
neuper@37906:  CalcTree [(elems, spec)];
neuper@37906:  Iterator 1;
neuper@37906:  moveActiveRoot 1; 
neuper@37906:  refFormula 1 (get_pos 1 1);
neuper@37906:  (*this gives a completely empty model*) 
neuper@37906: 
neuper@37906:  fetchProposedTactic 1;
neuper@37906: (*fill the CalcHead with Descriptions...*)
neuper@37906:  setNextTactic 1 (Model_Problem );
neuper@37906:  autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
neuper@37906: 
neuper@37906:  (*user input is !!!!!EITHER!!!!! _some_ (at least one) items of the model 
neuper@37906:  !!!!!OR!!!!! _one_ part of the specification !!!!!!!!!!!!!*)
neuper@37906:  (*input of two items, 'fixedValues [r=Arbfix]' and 'maximum b'...*)
neuper@37906:  modifyCalcHead 1 (([],Pbl) (*position, from previous refFormula*),
neuper@37906: 		  "Problem (DiffApp.thy, [maximum_of, function])",
neuper@37906: 		  (*the head-form ^^^ is not used for input here*)
neuper@37906: 		  [Given ["fixedValues [r=Arbfix]"(*new input*)],
neuper@37906: 		   Find ["maximum b"(*new input*), "valuesFor"], 
neuper@37906: 		   Relate ["relations"]],
neuper@37906: 		  (*input (Arbfix will dissappear soon)*)
neuper@37906: 		  Pbl (*belongsto*),
neuper@37906: 		  e_spec (*no input to the specification*));
neuper@37906: 
neuper@37906:  (*the user does not know, what 'superfluous' for 'maximum b' may mean
neuper@37906:   and asks what to do next*)
neuper@37906:  fetchProposedTactic 1;
neuper@37906:  (*the student follows the advice*)
neuper@37906:  setNextTactic 1 (Add_Find "maximum A"); (*FIXME.17.11.03: does not yet work*)
neuper@37906:   autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
neuper@37906:  
neuper@37906:  (*this input completes the model*)
neuper@37906:  modifyCalcHead 1 (([],Pbl), "not used here",
neuper@37906: 		  [Given ["fixedValues [r=Arbfix]"],
neuper@37906: 		   Find ["maximum A", "valuesFor [a,b]"(*new input*)], 
neuper@37906: 		   Relate ["relations [A=a*b, \
neuper@37906: 			   \(a/2)^2 + (b/2)^2 = r^2]"]], Pbl, e_spec);
neuper@37906: 
neuper@37906:  (*specification is not interesting an should be skipped by the dialogguide;
neuper@37906:    !!!!!!!!!!!!!!!!!!!! input of ONE part at a time !!!!!!!!!!!!!!!!!!!!!!*)
neuper@37906:  modifyCalcHead 1 (([],Pbl), "not used here",
neuper@37906: 		  [Given ["fixedValues [r=Arbfix]"],
neuper@37906: 		   Find ["maximum A", "valuesFor [a,b]"(*new input*)], 
neuper@37906: 		   Relate ["relations [A=a*b, \
neuper@37906: 			   \(a/2)^2 + (b/2)^2 = r^2]"]], Pbl, 
neuper@37906: 		  ("DiffApp.thy", ["e_pblID"], ["e_metID"]));
neuper@37906:  modifyCalcHead 1 (([],Pbl), "not used here",
neuper@37906: 		  [Given ["fixedValues [r=Arbfix]"],
neuper@37906: 		   Find ["maximum A", "valuesFor [a,b]"(*new input*)], 
neuper@37906: 		   Relate ["relations [A=a*b, \
neuper@37906: 			   \(a/2)^2 + (b/2)^2 = r^2]"]], Pbl, 
neuper@37906: 		  ("DiffApp.thy", ["maximum_of","function"], 
neuper@37906: 		   ["e_metID"]));
neuper@37906:  modifyCalcHead 1 (([],Pbl), "not used here",
neuper@37906: 		  [Given ["fixedValues [r=Arbfix]"],
neuper@37906: 		   Find ["maximum A", "valuesFor [a,b]"(*new input*)], 
neuper@37906: 		   Relate ["relations [A=a*b, \
neuper@37906: 			   \(a/2)^2 + (b/2)^2 = r^2]"]], Pbl, 
neuper@37906: 		  ("DiffApp.thy", ["maximum_of","function"], 
neuper@37906: 		   ["DiffApp","max_by_calculus"]));
neuper@37906:  (*this final calcHead now has STATUS 'complete' !*)
neuper@37906:  DEconstrCalcTree 1;
neuper@37906: 
neuper@37906: 
neuper@37906: "--------- solve_linear from pbl-hierarchy -----------------------";
neuper@37906: "--------- solve_linear from pbl-hierarchy -----------------------";
neuper@37906: "--------- solve_linear from pbl-hierarchy -----------------------";
neuper@37906:  states:=[];
neuper@37906:  val (fmz, sp) = ([], ("", ["linear","univariate","equation","test"], []));
neuper@37906:  CalcTree [(fmz, sp)];
neuper@37906:  Iterator 1; moveActiveRoot 1;
neuper@37906:  refFormula 1 (get_pos 1 1);
neuper@37906:  modifyCalcHead 1 (([],Pbl),"solve (1+-1*2+x=0)",
neuper@37906: 		  [Given ["equality (1+-1*2+x=0)", "solveFor x"],
neuper@37906: 		   Find ["solutions L"]],
neuper@37906: 		  Pbl, 
neuper@37906: 		  ("Test.thy", ["linear","univariate","equation","test"],
neuper@37906: 		   ["Test","solve_linear"]));
neuper@37906:  autoCalculate 1 CompleteCalc;
neuper@37906:  refFormula 1 (get_pos 1 1);
neuper@37906:  val ((pt,_),_) = get_calc 1;
neuper@37906:  val p = get_pos 1 1;
neuper@37906:  val (Form f, tac, asms) = pt_extract (pt, p);
neuper@37906:  if term2str f = "[x = 1]" andalso p = ([], Res) then () else 
neuper@38031:  error "FE-interface.sml: diff.behav. in from pbl-hierarchy";
neuper@37906:  
neuper@37906: 
neuper@37906: 
neuper@37906: "--------- solve_linear as in an algebra system (CAS)-------------";
neuper@37906: "--------- solve_linear as in an algebra system (CAS)-------------";
neuper@37906: "--------- solve_linear as in an algebra system (CAS)-------------";
neuper@37906:  states:=[];
neuper@37906:  val (fmz, sp) = ([], ("", [], []));
neuper@37906:  CalcTree [(fmz, sp)];
neuper@37906:  Iterator 1; moveActiveRoot 1;
neuper@37906:  modifyCalcHead 1 (([],Pbl),"solveTest (1+-1*2+x=0,x)", [], Pbl, ("", [], []));
neuper@37906:  autoCalculate 1 CompleteCalc;
neuper@37906:  refFormula 1 (get_pos 1 1);
neuper@37906:  val ((pt,_),_) = get_calc 1;
neuper@37906:  val p = get_pos 1 1;
neuper@37906:  val (Form f, tac, asms) = pt_extract (pt, p);
neuper@37906:  if term2str f = "[x = 1]" andalso p = ([], Res) then () else 
neuper@38031:  error "FE-interface.sml: diff.behav. in algebra system";
neuper@37906: 
neuper@37906: 
neuper@37906: 
neuper@37906: "--------- interSteps: on 'miniscript with mini-subpbl' ----------";
neuper@37906: "--------- interSteps: on 'miniscript with mini-subpbl' ----------";
neuper@37906: "--------- interSteps: on 'miniscript with mini-subpbl' ----------";
neuper@37906:  states:=[];
neuper@37906:  CalcTree
neuper@37906:  [(["equality (x+1=2)", "solveFor x","solutions L"], 
neuper@37906:    ("Test.thy", 
neuper@37906:     ["sqroot-test","univariate","equation","test"],
neuper@37906:     ["Test","squ-equ-test-subpbl1"]))];
neuper@37906:  Iterator 1;
neuper@37906:  moveActiveRoot 1;
neuper@37906:  autoCalculate 1 CompleteCalc; 
neuper@37906:  val ((pt,_),_) = get_calc 1;
neuper@37906:  show_pt pt;
neuper@37906: 
neuper@37906:  (*UC\label{SOLVE:INFO:intermediate-steps}*)
neuper@37906:  interSteps 1 ([2],Res);
neuper@37906:  val ((pt,_),_) = get_calc 1; show_pt pt (*new ([2,1],Frm)..([2,6],Res)*);
neuper@37906:  val (unc, del, gen) = (([1],Res),([1],Res),([2,6],Res));
neuper@37906:  getFormulaeFromTo 1 unc gen 1 false; 
neuper@37906: 
neuper@37906:  (*UC\label{SOLVE:INFO:intermediate-steps}*)
neuper@37906:  interSteps 1 ([3,2],Res);
neuper@37906:  val ((pt,_),_) = get_calc 1; show_pt pt (*new ([3,2,1],Frm)..([3,2,2],Res)*);
neuper@37906:  val (unc, del, gen) = (([3,1],Res),([3,1],Res),([3,2,2],Res));
neuper@37906:  getFormulaeFromTo 1 unc gen 1 false; 
neuper@37906: 
neuper@37906:  (*UC\label{SOLVE:INFO:intermediate-steps}*)
neuper@37906:  interSteps 1 ([3],Res)  (*no new steps in subproblems*);
neuper@37906:  val (unc, del, gen) = (([3],Pbl),([3],Pbl),([3,2],Res));
neuper@37906:  getFormulaeFromTo 1 unc gen 1 false; 
neuper@37906: 
neuper@37906:  (*UC\label{SOLVE:INFO:intermediate-steps}*)
neuper@37906:  interSteps 1 ([],Res)  (*no new steps in subproblems*);
neuper@37906:  val (unc, del, gen) = (([],Pbl),([],Pbl),([4],Res));
neuper@37906:  getFormulaeFromTo 1 unc gen 1 false; 
neuper@37906: 
neuper@37906: 
neuper@37906: "--------- getTactic, fetchApplicableTactics ---------------------";
neuper@37906: "--------- getTactic, fetchApplicableTactics ---------------------";
neuper@37906: "--------- getTactic, fetchApplicableTactics ---------------------";
neuper@37906:  states:=[];
neuper@37906:  CalcTree
neuper@37906:  [(["equality (x+1=2)", "solveFor x","solutions L"], 
neuper@37906:    ("Test.thy", 
neuper@37906:     ["sqroot-test","univariate","equation","test"],
neuper@37906:     ["Test","squ-equ-test-subpbl1"]))];
neuper@37906:  Iterator 1; moveActiveRoot 1;
neuper@37906:  autoCalculate 1 CompleteCalc;
neuper@37906:  val ((pt,_),_) = get_calc 1;
neuper@37906:  show_pt pt;
neuper@37906: 
neuper@37906:  (*UC\label{SOLVE:HIDE:getTactic}*)
neuper@37906:  getTactic 1 ([],Pbl);
neuper@37906:  getTactic 1 ([1],Res);
neuper@37906:  getTactic 1 ([3],Pbl);
neuper@37906:  getTactic 1 ([3,1],Frm);
neuper@37906:  getTactic 1 ([3],Res);
neuper@37906:  getTactic 1 ([],Res);
neuper@37906: 
neuper@37906: (*UC\label{SOLVE:MANUAL:TACTIC:listall}*)
neuper@37906:  fetchApplicableTactics 1 99999 ([],Pbl);
neuper@37906:  fetchApplicableTactics 1 99999 ([1],Res);
neuper@37906:  fetchApplicableTactics 1 99999 ([3],Pbl);
neuper@37906:  fetchApplicableTactics 1 99999 ([3,1],Res);
neuper@37906:  fetchApplicableTactics 1 99999 ([3],Res);
neuper@37906:  fetchApplicableTactics 1 99999 ([],Res);
neuper@37906: 
neuper@37906: 
neuper@37906: "--------- getAssumptions, getAccumulatedAsms --------------------";
neuper@37906: "--------- getAssumptions, getAccumulatedAsms --------------------";
neuper@37906: "--------- getAssumptions, getAccumulatedAsms --------------------";
neuper@37906: states:=[];
neuper@37906: CalcTree
neuper@37906: [(["equality (x/(x^2 - 6*x+9) - 1/(x^2 - 3*x) =1/x)",
neuper@37906: 	   "solveFor x","solutions L"], 
neuper@37906:   ("RatEq.thy",["univariate","equation"],["no_met"]))];
neuper@37906: Iterator 1; moveActiveRoot 1;
neuper@37906: autoCalculate 1 CompleteCalc; 
neuper@37906: val ((pt,_),_) = get_calc 1;
neuper@37906: show_pt pt;
neuper@37906: 
neuper@37906: (*UC\label{SOLVE:HELP:assumptions}*)
neuper@37906: getAssumptions 1 ([3], Res);
neuper@37906: getAssumptions 1 ([5], Res);
neuper@37906: (*UC\label{SOLVE:HELP:assumptions-origin} WN0502 still without positions*)
neuper@37906: getAccumulatedAsms 1 ([3], Res);
neuper@37906: getAccumulatedAsms 1 ([5], Res);
neuper@37906: 
neuper@37906: 
neuper@37906: "--------- arbitrary combinations of steps -----------------------";
neuper@37906: "--------- arbitrary combinations of steps -----------------------";
neuper@37906: "--------- arbitrary combinations of steps -----------------------";
neuper@37906:  states:=[];
neuper@37906:  CalcTree      (*start of calculation, return No.1*)
neuper@37906:      [(["equality (1+-1*2+x=0)", "solveFor x","solutions L"],
neuper@37906:        ("Test.thy", 
neuper@37906: 	["linear","univariate","equation","test"],
neuper@37906: 	["Test","solve_linear"]))];
neuper@37906:  Iterator 1; moveActiveRoot 1;
neuper@37906: 
neuper@37906:  fetchProposedTactic 1;
neuper@37906:  setNextTactic 1 (Model_Problem );
neuper@37906:  autoCalculate 1 (Step 1); 
neuper@37906: 
neuper@37906:  fetchProposedTactic 1;
neuper@37906:  fetchProposedTactic 1;
neuper@37906: 
neuper@37906:  setNextTactic 1 (Add_Find "solutions L");
neuper@37906:  setNextTactic 1 (Add_Find "solutions L");
neuper@37906: 
neuper@37906:  autoCalculate 1 (Step 1); 
neuper@37906:  autoCalculate 1 (Step 1); 
neuper@37906: 
neuper@37906:  setNextTactic 1 (Specify_Theory "Test.thy");
neuper@37906:  fetchProposedTactic 1;
neuper@37906:  autoCalculate 1 (Step 1); 
neuper@37906: 
neuper@37906:  autoCalculate 1 (Step 1); 
neuper@37906:  autoCalculate 1 (Step 1); 
neuper@37906:  autoCalculate 1 (Step 1); 
neuper@37906:  autoCalculate 1 (Step 1); 
neuper@37906: (*------------------------- end calc-head*)
neuper@37906: 
neuper@37906:  fetchProposedTactic 1;
neuper@37906:  setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "isolate_bdv"));
neuper@37906:  autoCalculate 1 (Step 1); 
neuper@37906: 
neuper@37906:  setNextTactic 1 (Rewrite_Set "Test_simplify");
neuper@37906:  fetchProposedTactic 1;
neuper@37906:  autoCalculate 1 (Step 1); 
neuper@37906: 
neuper@37906:  autoCalculate 1 CompleteCalc; 
neuper@37906:  val ((pt,_),_) = get_calc 1;
neuper@37906:  val p = get_pos 1 1;
neuper@37906:  val (Form f, tac, asms) = pt_extract (pt, p);
neuper@37906:  if term2str f = "[x = 1]" andalso p = ([], Res) then () else 
neuper@38031:  error "FE-interface.sml: diff.behav. in combinations of steps";
neuper@37906: 
neuper@37906: 
neuper@37906: "--------- appendFormula label{SOLVE:MANUAL:FORMULA:enter} right--";
neuper@37906: "--------- appendFormula label{SOLVE:MANUAL:FORMULA:enter} right--";
neuper@37906: "--------- appendFormula label{SOLVE:MANUAL:FORMULA:enter} right--";
neuper@37906:  states:=[];
neuper@37906:  CalcTree
neuper@37906:  [(["equality (x+1=2)", "solveFor x","solutions L"], 
neuper@37906:    ("Test.thy", 
neuper@37906:     ["sqroot-test","univariate","equation","test"],
neuper@37906:     ["Test","squ-equ-test-subpbl1"]))];
neuper@37906:  Iterator 1;
neuper@37906:  moveActiveRoot 1;
neuper@37906:  autoCalculate 1 CompleteCalcHead;
neuper@37906:  autoCalculate 1 (Step 1);
neuper@37906:  autoCalculate 1 (Step 1);
neuper@37906:  appendFormula 1 "-1 + x = 0";  
neuper@37906:  (*... returns calcChangedEvent with*)
neuper@37906:  val (unc, del, gen) = (([1],Res), ([1],Res), ([2],Res));
neuper@37906:  getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
neuper@37906: 
neuper@37906:  val ((pt,_),_) = get_calc 1;
neuper@37906:  val p = get_pos 1 1;
neuper@37906:  val (Form f, tac, asms) = pt_extract (pt, p);
neuper@37906:  if term2str f = "-1 + x = 0" andalso p = ([2], Res) then () else 
neuper@38031:  error "FE-interface.sml: diff.behav. in FORMULA:enter} right";
neuper@37906: 
neuper@37906: "--------- appendFormula label{SOLVE:MANUAL:FORMULA:enter} other--";
neuper@37906: "--------- appendFormula label{SOLVE:MANUAL:FORMULA:enter} other--";
neuper@37906: "--------- appendFormula label{SOLVE:MANUAL:FORMULA:enter} other--";
neuper@37906:  states:=[];
neuper@37906:  CalcTree
neuper@37906:  [(["equality (x+1=2)", "solveFor x","solutions L"], 
neuper@37906:    ("Test.thy", 
neuper@37906:     ["sqroot-test","univariate","equation","test"],
neuper@37906:     ["Test","squ-equ-test-subpbl1"]))];
neuper@37906:  Iterator 1;
neuper@37906:  moveActiveRoot 1;
neuper@37906:  autoCalculate 1 CompleteCalcHead;
neuper@37906:  autoCalculate 1 (Step 1);
neuper@37906:  autoCalculate 1 (Step 1);
neuper@37906:  appendFormula 1 "x - 1 = 0"; 
neuper@37906:  val (unc, del, gen) = (([1],Res), ([1],Res), ([2],Res));
neuper@37906:  getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
neuper@37906:  (*11 elements !!!*)
neuper@37906: 
neuper@37906:  val ((pt,_),_) = get_calc 1;
neuper@37906:  val p = get_pos 1 1;
neuper@37906:  val (Form f, tac, asms) = pt_extract (pt, p);
neuper@37906:  if term2str f = "x - 1 = 0" andalso p = ([2], Res) then () else 
neuper@38031:  error "FE-interface.sml: diff.behav. in FORMULA:enter} other";
neuper@37906: 
neuper@37906: "--------- appendFormula label{SOLVE:MANUAL:FORMULA:enter} oth 2--";
neuper@37906: "--------- appendFormula label{SOLVE:MANUAL:FORMULA:enter} oth 2--";
neuper@37906: "--------- appendFormula label{SOLVE:MANUAL:FORMULA:enter} oth 2--";
neuper@37906:  states:=[];
neuper@37906:  CalcTree
neuper@37906:  [(["equality (x+1=2)", "solveFor x","solutions L"], 
neuper@37906:    ("Test.thy", 
neuper@37906:     ["sqroot-test","univariate","equation","test"],
neuper@37906:     ["Test","squ-equ-test-subpbl1"]))];
neuper@37906:  Iterator 1;
neuper@37906:  moveActiveRoot 1;
neuper@37906:  autoCalculate 1 CompleteCalcHead;
neuper@37906:  autoCalculate 1 (Step 1);
neuper@37906:  autoCalculate 1 (Step 1);
neuper@37906:  appendFormula 1 "x = 1"; 
neuper@37906:  (*... returns calcChangedEvent with*)
neuper@37906:  val (unc, del, gen) = (([1],Res), ([1],Res), ([3,2],Res));
neuper@37906:  getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
neuper@37906:  (*6 elements !!!*)
neuper@37906: 
neuper@37906:  val ((pt,_),_) = get_calc 1;
neuper@37906:  val p = get_pos 1 1;
neuper@37906:  val (Form f, tac, asms) = pt_extract (pt, p);
neuper@37906:  if term2str f = "x = 1" andalso p = ([3,2], Res) then () else 
neuper@38031:  error "FE-interface.sml: diff.behav. in FORMULA:enter} oth 2";
neuper@37906: 
neuper@37906: 
neuper@37906: "--------- appendFormula label{SOLVE:MANUAL:FORMULA:enter} NOTok--";
neuper@37906: "--------- appendFormula label{SOLVE:MANUAL:FORMULA:enter} NOTok--";
neuper@37906: "--------- appendFormula label{SOLVE:MANUAL:FORMULA:enter} NOTok--";
neuper@37906:  states:=[];
neuper@37906:  CalcTree
neuper@37906:  [(["equality (x+1=2)", "solveFor x","solutions L"], 
neuper@37906:    ("Test.thy", 
neuper@37906:     ["sqroot-test","univariate","equation","test"],
neuper@37906:     ["Test","squ-equ-test-subpbl1"]))];
neuper@37906:  Iterator 1;
neuper@37906:  moveActiveRoot 1;
neuper@37906:  autoCalculate 1 CompleteCalcHead;
neuper@37906:  autoCalculate 1 (Step 1);
neuper@37906:  autoCalculate 1 (Step 1);
neuper@37906:  appendFormula 1 "x - 4711 = 0"; 
neuper@37906:  (*... returns <ERROR> no derivation found </ERROR>*)
neuper@37906: 
neuper@37906:  val ((pt,_),_) = get_calc 1;
neuper@37906:  val p = get_pos 1 1;
neuper@37906:  val (Form f, tac, asms) = pt_extract (pt, p);
neuper@37906:  if term2str f = "x + 1 + -1 * 2 = 0" andalso p = ([1], Res) then () else 
neuper@38031:  error "FE-interface.sml: diff.behav. in FORMULA:enter} NOTok";
neuper@37906: 
neuper@37906: 
neuper@37906: "--------- replaceFormula {SOLVE:MANUAL:FORMULA:replace} right----";
neuper@37906: "--------- replaceFormula {SOLVE:MANUAL:FORMULA:replace} right----";
neuper@37906: "--------- replaceFormula {SOLVE:MANUAL:FORMULA:replace} right----";
neuper@37906:  states:=[];
neuper@37906:  CalcTree
neuper@37906:  [(["equality (x+1=2)", "solveFor x","solutions L"], 
neuper@37906:    ("Test.thy", 
neuper@37906:     ["sqroot-test","univariate","equation","test"],
neuper@37906:     ["Test","squ-equ-test-subpbl1"]))];
neuper@37906:  Iterator 1;
neuper@37906:  moveActiveRoot 1;
neuper@37906:  autoCalculate 1 CompleteCalc;
neuper@37906:  moveActiveFormula 1 ([2],Res);
neuper@37906:  replaceFormula 1 "-1 + x = 0" (*i.e. repeats input*);
neuper@37906:  (*... returns <ERROR> formula not changed </ERROR>*)
neuper@37906: 
neuper@37906:  val ((pt,_),_) = get_calc 1;
neuper@37906:  val p = get_pos 1 1;
neuper@37906:  val (Form f, tac, asms) = pt_extract (pt, p);
neuper@37906:  if term2str f = "-1 + x = 0" andalso p = ([2], Res) then () else 
neuper@38031:  error "FE-interface.sml: diff.behav. in FORMULA:replace} right 1";
neuper@37906:  if map fst (get_interval ([2],Res) ([],Res) 9999 pt) = 
neuper@37906:     [([2], Res), ([3], Pbl), ([3, 1], Frm), ([3, 1], Res), ([3, 2], Res),
neuper@37906:      ([3], Res), ([4], Res), ([], Res)] then () (*nothing deleted!*) else
neuper@38031:  error "FE-interface.sml: diff.behav. in FORMULA:replace} right 2";
neuper@37906:  
neuper@37906: (*WN050211 replaceFormula didn't work on second ctree: thus now tested...*)
neuper@37906:  CalcTree
neuper@37906:  [(["equality (x+1=2)", "solveFor x","solutions L"], 
neuper@37906:    ("Test.thy", 
neuper@37906:     ["sqroot-test","univariate","equation","test"],
neuper@37906:     ["Test","squ-equ-test-subpbl1"]))];
neuper@37906:  Iterator 2;
neuper@37906:  moveActiveRoot 2;
neuper@37906:  autoCalculate 2 CompleteCalc;
neuper@37906:  moveActiveFormula 2 ([2],Res);
neuper@37906:  replaceFormula 2 "-1 + x = 0" (*i.e. repeats input*);
neuper@37906:  (*... returns <ERROR> formula not changed </ERROR>*)
neuper@37906: 
neuper@37906:  val ((pt,_),_) = get_calc 2;
neuper@37906:  val p = get_pos 2 1;
neuper@37906:  val (Form f, tac, asms) = pt_extract (pt, p);
neuper@37906:  if term2str f = "-1 + x = 0" andalso p = ([2], Res) then () else 
neuper@38031:  error "FE-interface.sml: diff.behav. in FORMULA:replace} right 1";
neuper@37906:  if map fst (get_interval ([2],Res) ([],Res) 9999 pt) = 
neuper@37906:     [([2], Res), ([3], Pbl), ([3, 1], Frm), ([3, 1], Res), ([3, 2], Res),
neuper@37906:      ([3], Res), ([4], Res), ([], Res)] then () (*nothing deleted!*) else
neuper@38031:  error "FE-interface.sml: diff.behav. in FORMULA:replace} right 2b";
neuper@37906: 
neuper@37906: "--------- replaceFormula {SOLVE:MANUAL:FORMULA:replace} other----";
neuper@37906: "--------- replaceFormula {SOLVE:MANUAL:FORMULA:replace} other----";
neuper@37906: "--------- replaceFormula {SOLVE:MANUAL:FORMULA:replace} other----";
neuper@37906:  states:=[];
neuper@37906:  CalcTree
neuper@37906:  [(["equality (x+1=2)", "solveFor x","solutions L"], 
neuper@37906:    ("Test.thy", 
neuper@37906:     ["sqroot-test","univariate","equation","test"],
neuper@37906:     ["Test","squ-equ-test-subpbl1"]))];
neuper@37906:  Iterator 1;
neuper@37906:  moveActiveRoot 1;
neuper@37906:  autoCalculate 1 CompleteCalc;
neuper@37906:  moveActiveFormula 1 ([2],Res); (*there is "-1 + x = 0"*)
neuper@37906:  replaceFormula 1 "x - 1 = 0"; (*<-------------------------------------*)
neuper@37906:  (*... returns calcChangedEvent with*)
neuper@37906:  val (unc, del, gen) = (([1],Res), ([4],Res), ([2],Res));
neuper@37906:  getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
neuper@37906: 
neuper@37906:  val ((pt,_),_) = get_calc 1;
neuper@37906:  show_pt pt;
neuper@37906:  val p = get_pos 1 1;
neuper@37906:  val (Form f, tac, asms) = pt_extract (pt, p);
neuper@37906:  if term2str f = "x - 1 = 0" andalso p = ([2], Res) then () else 
neuper@38031:  error "FE-interface.sml: diff.behav. in FORMULA:replace} other 1";
neuper@37906: (* for getting the list in whole length ...
neuper@37906: print_depth 99;map fst (get_interval ([1],Res) ([],Res) 9999 pt);print_depth 3;
neuper@37906:    *)
neuper@37906:  if map fst (get_interval ([1],Res) ([],Res) 9999 pt) = 
neuper@37906:     [([1], Res), ([2, 1], Frm), ([2, 1], Res), ([2, 2], Res), ([2, 3], Res),
neuper@37906:       ([2, 4], Res), ([2, 5], Res), ([2, 6], Res), ([2, 7], Res),
neuper@37906:       ([2, 8], Res), ([2, 9], Res), ([2], Res)
neuper@37906: (*WN060727 {cutlevup->test_trans} removed: , 
neuper@37906:       ([], Res)(*dropped, if test_trans doesnt stop at PblNd*)*)] then () else
neuper@38031:  error "FE-interface.sml: diff.behav. in FORMULA:replace} other 2";
neuper@37906: 
neuper@37906: 
neuper@37906: 
neuper@37906: "--------- replaceFormula {SOLVE:MANUAL:FORMULA:replace} other 2--";
neuper@37906: "--------- replaceFormula {SOLVE:MANUAL:FORMULA:replace} other 2--";
neuper@37906: "--------- replaceFormula {SOLVE:MANUAL:FORMULA:replace} other 2--";
neuper@37906:  states:=[];
neuper@37906:  CalcTree
neuper@37906:  [(["equality (x+1=2)", "solveFor x","solutions L"], 
neuper@37906:    ("Test.thy", 
neuper@37906:     ["sqroot-test","univariate","equation","test"],
neuper@37906:     ["Test","squ-equ-test-subpbl1"]))];
neuper@37906:  Iterator 1;
neuper@37906:  moveActiveRoot 1;
neuper@37906:  autoCalculate 1 CompleteCalc;
neuper@37906:  moveActiveFormula 1 ([2],Res); (*there is "-1 + x = 0"*)
neuper@37906:  replaceFormula 1 "x = 1"; (*<-------------------------------------*)
neuper@37906:  (*... returns calcChangedEvent with ...*)
neuper@37906:  val (unc, del, gen) = (([1],Res), ([4],Res), ([3,2],Res));
neuper@37906:  getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
neuper@37906:  (*9 elements !!!*)
neuper@37906: 
neuper@37906:  val ((pt,_),_) = get_calc 1;
neuper@37906:  show_pt pt; (*error: ...get_interval drops ([3,2],Res) ...*)
neuper@37906:  val (t,_) = get_obj g_result pt [3,2]; term2str t;
neuper@37906:   if map fst (get_interval ([1],Res) ([],Res) 9999 pt) = 
neuper@37906:     [([1], Res), ([2], Res), ([3], Pbl), ([3, 1], Frm), ([3, 1], Res),
neuper@37906:       ([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res), 
neuper@37906:       ([3,2],Res)] then () else
neuper@38031:  error "FE-interface.sml: diff.behav. in FORMULA:replace} oth2 1";
neuper@37906: 
neuper@37906:  val p = get_pos 1 1;
neuper@37906:  val (Form f, tac, asms) = pt_extract (pt, p);
neuper@37906:  if term2str f = "x = 1" andalso p = ([3,2], Res) then () else 
neuper@38031:  error "FE-interface.sml: diff.behav. in FORMULA:replace} oth2 2";
neuper@37906: 
neuper@37906: 
neuper@37906: 
neuper@37906: "--------- replaceFormula {SOLVE:MANUAL:FORMULA:replace} NOTok----";
neuper@37906: "--------- replaceFormula {SOLVE:MANUAL:FORMULA:replace} NOTok----";
neuper@37906: "--------- replaceFormula {SOLVE:MANUAL:FORMULA:replace} NOTok----";
neuper@37906:  states:=[];
neuper@37906:  CalcTree
neuper@37906:  [(["equality (x+1=2)", "solveFor x","solutions L"], 
neuper@37906:    ("Test.thy", 
neuper@37906:     ["sqroot-test","univariate","equation","test"],
neuper@37906:     ["Test","squ-equ-test-subpbl1"]))];
neuper@37906:  Iterator 1;
neuper@37906:  moveActiveRoot 1;
neuper@37906:  autoCalculate 1 CompleteCalc;
neuper@37906:  moveActiveFormula 1 ([2],Res); (*there is "-1 + x = 0"*)
neuper@37906:  replaceFormula 1 "x - 4711 = 0"; 
neuper@37906:  (*... returns <ERROR> no derivation found </ERROR>*)
neuper@37906: 
neuper@37906:  val ((pt,_),_) = get_calc 1;
neuper@37906:  show_pt pt;
neuper@37906:  val p = get_pos 1 1;
neuper@37906:  val (Form f, tac, asms) = pt_extract (pt, p);
neuper@37906:  if term2str f = "-1 + x = 0" andalso p = ([2], Res) then () else 
neuper@38031:  error "FE-interface.sml: diff.behav. in FORMULA:replace} NOTok";
neuper@37906: 
neuper@37906: