(* tests the interface of isac's SML-kernel in accordance to 

   java-tests/isac.bridge.

WN050707 ... if true, the test ist marked with a \label referring

to the same UC in isac-docu.tex as the JUnit testcase.

use"../smltest/FE-interface/interface.sml";

use"interface.sml";

 *)

"--------------------------------------------------------";

"table of contents --------------------------------------";

"--------------------------------------------------------";

"within struct ------------------------------------------";

"--------------------------------------------------------";

"--------- encode ^ -> ^^^ ------------------------------";

"--------------------------------------------------------";

"exported from struct -----------------------------------";

"--------------------------------------------------------";

"--------- empty rootpbl --------------------------------";

"--------- solve_linear as rootpbl FE -------------------";

"--------- inspect the CalcTree No.1 with Iterator No.2 -";

"--------- miniscript with mini-subpbl ------------------";

"--------- mini-subpbl AUTOCALCULATE Step 1 -------------";

"--------- solve_linear as rootpbl AUTO CompleteCalc ----";

"--------- solve_linear as rootpbl AUTO CompleteHead/Calc ";

"--------- mini-subpbl AUTOCALCULATE CompleteCalc -------";

"--------- mini-subpbl AUTO CompleteCalcHead ------------";

"--------- solve_linear as rootpbl AUTO CompleteModel ---";

"--------- setContext..Thy ------------------------------";

"--------- mini-subpbl AUTOCALC CompleteToSubpbl --------";

"--------- rat-eq + subpbl: no_met, NO solution dropped -";

"--------- tryMatchProblem, tryRefineProblem ------------";

"--------- modifyCalcHead, resetCalcHead, modelProblem --";

"--------- maximum-example, UC: Modeling an example -----";

"--------- solve_linear from pbl-hierarchy --------------";

"--------- solve_linear as in an algebra system (CAS)----";

"--------- interSteps: on 'miniscript with mini-subpbl' -";

"--------- getTactic, fetchApplicableTactics ------------";

"--------- getAssumptions, getAccumulatedAsms -----------";

"--------- arbitrary combinations of steps --------------";

"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}right";

"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}other";

"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}oth 2";

"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}NOTok";

"--------- replaceFormula {SOL:MAN:FOR:replace} right----";

"--------- replaceFormula {SOL:MAN:FOR:replace} other----";

"--------- replaceFormula {SOL:MAN:FOR:replace} other 2--";

"--------- replaceFormula {SOL:MAN:FOR:replace} NOTok----";

"--------------------------------------------------------";

"within struct ---------------------------------------------------";

"within struct ---------------------------------------------------";

"within struct ---------------------------------------------------";

(*==================================================================

"--------- encode ^ -> ^^^ ------------------------------";

"--------- encode ^ -> ^^^ ------------------------------";

"--------- encode ^ -> ^^^ ------------------------------";

if encode "a^2+b^2=c^2" = "a^^^2+b^^^2=c^^^2" then ()

else error "interface.sml: diff.behav. in encode ^ -> ^^^ ";

if (decode o encode) "a^2+b^2=c^2" = "a^2+b^2=c^2" then ()

else error "interface.sml: diff.behav. in de/encode ^ <-> ^^^ ";

==================================================================*)

"exported from struct --------------------------------------------";

"exported from struct --------------------------------------------";

"exported from struct --------------------------------------------";

(*------------ set at startup of the Kernel --------------------------*)

 states:= [];  (*resets all state information in Kernel               *)

(*----------------------------------------------------------------*)

"--------- empty rootpbl --------------------------------";

"--------- empty rootpbl --------------------------------";

"--------- empty rootpbl --------------------------------";

 CalcTree [([], ("", [], []))];

 Iterator 1;

 moveActiveRoot 1;

 refFormula 1 (get_pos 1 1);

(*WN.040222: stoert das sehr, dass e_domID etc. statt leer kommt ???*)

"--------- solve_linear as rootpbl FE -------------------";

"--------- solve_linear as rootpbl FE -------------------";

"--------- solve_linear as rootpbl FE -------------------";

 states := [];

 CalcTree      (*start of calculation, return No.1*)

     [(["equality (1+-1*2+x=(0::real))", "solveFor x","solutions L"],

       ("Test", 

	["linear","univariate","equation","test"],

	["Test","solve_linear"]))];

 Iterator 1;     (*create an active Iterator on CalcTree No.1*)

 moveActiveRoot 1;(*sets the CalcIterator No.1 at the root of CalcTree No.1*);

 refFormula 1 (get_pos 1 1)  (*gets CalcHead; model is still empty*);

 fetchProposedTactic 1 (*by using Iterator No.1*);

 setNextTactic 1 (Model_Problem); (*by using Iterator No.1*)

 autoCalculate 1 (Step 1);

 refFormula 1 (get_pos 1 1)  (*model contains descriptions for all items*);

 autoCalculate 1 (Step 1);

(*-----since Model_Problem + complete_mod_ in case cas of SOME-----*

 fetchProposedTactic 1;

 setNextTactic 1 (Add_Given "equality (1 + -1 * 2 + x = 0)");

 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); (*equality added*);

 fetchProposedTactic 1;

 setNextTactic 1 (Add_Given "solveFor x");

 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);

 fetchProposedTactic 1;

 setNextTactic 1 (Add_Find "solutions L");

 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);

 fetchProposedTactic 1;

 setNextTactic 1 (Specify_Theory "Test");

 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);

*-----since Model_Problem + complete_mod_ in case cas of SOME-----*)

 fetchProposedTactic 1;

 setNextTactic 1 (Specify_Problem ["linear","univariate","equation","test"]);

 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);

(*-------------------------------------------------------------------------*)

 fetchProposedTactic 1;

 val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;

 setNextTactic 1 (Specify_Method ["Test","solve_linear"]);

 val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;

 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);

 val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;

(*-------------------------------------------------------------------------*)

 fetchProposedTactic 1;

(*========== inhibit exn 110310 ================================================

 val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;

 setNextTactic 1 (Apply_Method ["Test","solve_linear"]);

   (*ERROR.110620 <SETNEXTTACTIC>..<MESSAGE> end-of-calculation*)

 val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;

 is_complete_mod ptp;

 is_complete_spec ptp;

 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);

 val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;

 (*term2str (get_obj g_form pt [1]);*)

(*-------------------------------------------------------------------------*)

 fetchProposedTactic 1;

 setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "isolate_bdv"));

 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);

 fetchProposedTactic 1;

 setNextTactic 1 (Rewrite_Set "Test_simplify");

 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);

 fetchProposedTactic 1;

 setNextTactic 1 (Check_Postcond ["linear","univariate","equation","test"]);

 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);

 val ((pt,_),_) = get_calc 1;

 val ip = get_pos 1 1;

 val (Form f, tac, asms) = pt_extract (pt, ip);

     (*exception just above means: 'ModSpec' has been returned: error anyway*)

 if term2str f = "[x = 1]" then () else 

 error "FE-Kernel-interface.sml: diff.behav. in solve_linear as rootpbl";

============ inhibit exn 110310 ==============================================*)

(*========== inhibit exn 110620 ================================================

"--------- inspect the CalcTree No.1 with Iterator No.2 -";

"--------- inspect the CalcTree No.1 with Iterator No.2 -";

"--------- inspect the CalcTree No.1 with Iterator No.2 -";

(*WN041118: inspection shifted to Iterator No.1, because others need pos'*)

 moveActiveRoot 1; 

 refFormula 1 ([],Pbl); getTactic 1 ([],Pbl);(*Error*)

 moveActiveDown 1; 

 refFormula 1 ([1],Frm); getTactic 1 ([1],Frm);(*Error*)

 moveActiveDown 1 ; 

 refFormula 1 ([1],Res); getTactic 1 ([1],Res);(*OK*) 

 (*getAssumption 1 ([1],Res); TODO.WN041217*)

 moveActiveDown 1 ; refFormula 1 ([2],Res);

 moveActiveCalcHead 1; refFormula 1 ([],Pbl);

 moveActiveDown 1;

 moveActiveDown 1;

 moveActiveDown 1;

 if get_pos 1 1 = ([2], Res) then () else 

 error "FE-interface.sml: diff.behav. in a inspect 1 with Iterator 2";

 moveActiveDown 1; refFormula 1 ([], Res);

 if get_pos 1 1 = ([], Res) then () else 

 error "FE-interface.sml: diff.behav. in b inspect 1 with Iterator 2";

 moveActiveCalcHead 1; refFormula 1 ([],Pbl);

============ inhibit exn 110620 ==============================================*)

"--------- miniscript with mini-subpbl ------------------";

"--------- miniscript with mini-subpbl ------------------";

"--------- miniscript with mini-subpbl ------------------";

 states:=[]; (*start of calculation, return No.1*)

 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], 

   ("Test", ["sqroot-test","univariate","equation","test"],

    ["Test","squ-equ-test-subpbl1"]))];

 Iterator 1;

 moveActiveRoot 1; 

 refFormula 1 (get_pos 1 1);

 fetchProposedTactic 1;

 setNextTactic 1 (Model_Problem);

 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*gets ModSpec;model is still empty*)

 fetchProposedTactic 1;

 setNextTactic 1 (Add_Given "equality (x + 1 = 2)");

 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);

 fetchProposedTactic 1;

 setNextTactic 1 (Add_Given "solveFor x");

 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);

 fetchProposedTactic 1;

 setNextTactic 1 (Add_Find "solutions L");

 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);

 fetchProposedTactic 1;

 setNextTactic 1 (Specify_Theory "Test");

 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);

 fetchProposedTactic 1;

 setNextTactic 1 (Specify_Problem 

		      ["sqroot-test","univariate","equation","test"]);

 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);

"1-----------------------------------------------------------------";

 fetchProposedTactic 1;

 setNextTactic 1 (Specify_Method ["Test","squ-equ-test-subpbl1"]);

 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);

 fetchProposedTactic 1;

 setNextTactic 1 (Apply_Method ["Test","squ-equ-test-subpbl1"]);

 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);

 fetchProposedTactic 1;

 setNextTactic 1 (Rewrite_Set "norm_equation");

 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);

 fetchProposedTactic 1;

 setNextTactic 1 (Rewrite_Set "Test_simplify");

 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);

 fetchProposedTactic 1;(*----------------Subproblem--------------------*);

 setNextTactic 1 (Subproblem ("Test",

			      ["linear","univariate","equation","test"]));

 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);

 fetchProposedTactic 1;

 setNextTactic 1 (Model_Problem );

 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);

 fetchProposedTactic 1;

 setNextTactic 1 (Add_Given "equality (-1 + x = 0)");

 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);

 fetchProposedTactic 1;

 setNextTactic 1 (Add_Given "solveFor x");

 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);

 fetchProposedTactic 1;

 setNextTactic 1 (Add_Find "solutions x_i");

 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);

 fetchProposedTactic 1;

 setNextTactic 1 (Specify_Theory "Test");

 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);

 fetchProposedTactic 1;

 setNextTactic 1 (Specify_Problem ["linear","univariate","equation","test"]);

 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);

"2-----------------------------------------------------------------";

 fetchProposedTactic 1;

 setNextTactic 1 (Specify_Method ["Test","solve_linear"]);

 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);

 fetchProposedTactic 1;

 setNextTactic 1 (Apply_Method ["Test","solve_linear"]);

 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);

 fetchProposedTactic 1;

 setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "isolate_bdv"));

 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);

 fetchProposedTactic 1;

 setNextTactic 1 (Rewrite_Set "Test_simplify");

 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);

 fetchProposedTactic 1;

 setNextTactic 1 (Check_Postcond ["linear","univariate","equation","test"]);

 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);

 fetchProposedTactic 1;

 setNextTactic 1 (Check_elementwise "Assumptions");

 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);

 val xml = fetchProposedTactic 1;

 setNextTactic 1 (Check_Postcond 

		      ["sqroot-test","univariate","equation","test"]);

 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);

 val ((pt,_),_) = get_calc 1;

 val str = pr_ptree pr_short pt;

 writeln str;

 val ip = get_pos 1 1;

 val (Form f, tac, asms) = pt_extract (pt, ip);

     (*exception just above means: 'ModSpec' has been returned: error anyway*)

 if term2str f = "[x = 1]" then () else 

 error "FE-interface.sml: diff.behav. in miniscript with mini-subpb";

 DEconstrCalcTree 1;

"--------- mini-subpbl AUTOCALCULATE Step 1 -------------";

"--------- mini-subpbl AUTOCALCULATE Step 1 -------------";

"--------- mini-subpbl AUTOCALCULATE Step 1 -------------";

 states:=[];

 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], 

   ("Test", ["sqroot-test","univariate","equation","test"],

    ["Test","squ-equ-test-subpbl1"]))];

 Iterator 1;

 moveActiveRoot 1;

 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);

 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);

 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);

 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);

 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);

 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);

 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);

 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);

 (*here the solve-phase starts*)

 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);

 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);

 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);

 (*------------------------------------*)

(* print_depth 13; get_calc 1;

   *)

 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);

 (*calc-head of subproblem*)

 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);

 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);

 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);

 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);

 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);

 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);

 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);

 (*solve-phase of the subproblem*)

 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);

 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);

 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);

 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);

 (*finish subproblem*)

 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);

 (*finish problem*)

 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); 

 (*this checks the test for correctness..*)

 val ((pt,_),_) = get_calc 1;

 val p = get_pos 1 1;

 val (Form f, tac, asms) = pt_extract (pt, p);

 if term2str f = "[x = 1]" andalso p = ([], Res) then () else 

 error "FE-interface.sml: diff.behav. in miniscript with mini-subpb";

 DEconstrCalcTree 1;

(*========== inhibit exn 110620 ================================================

"--------- solve_linear as rootpbl AUTO CompleteCalc ----";

"--------- solve_linear as rootpbl AUTO CompleteCalc ----";

"--------- solve_linear as rootpbl AUTO CompleteCalc ----";

 states:=[];

 CalcTree

     [(["equality (1+-1*2+x=0)", "solveFor x","solutions L"],

       ("Test", 

	["linear","univariate","equation","test"],

	["Test","solve_linear"]))];

 Iterator 1;

 moveActiveRoot 1;

getFormulaeFromTo 1 ([],Pbl) ([],Pbl) 999 false;

 autoCalculate 1 CompleteCalc; 

 val (unc, del, gen) = (([],Pbl), ([],Pbl), ([],Res));

 getFormulaeFromTo 1 unc gen 1 (*only level 1*) false;

 val ((pt,_),_) = get_calc 1;

 val p = get_pos 1 1;

 val (Form f, tac, asms) = pt_extract (pt, p);

 if term2str f = "[x = 1]" andalso p = ([], Res) then () else 

 error "FE-interface.sml: diff.behav. in solve_linear/rt AUTOCALCULATE ";

"--------- solve_linear as rootpbl AUTO CompleteHead/Calc ";

"--------- solve_linear as rootpbl AUTO CompleteHead/Calc ";

"--------- solve_linear as rootpbl AUTO CompleteHead/Calc ";

 states:=[];

 CalcTree

     [(["equality (1+-1*2+x=0)", "solveFor x","solutions L"],

       ("Test", 

	["linear","univariate","equation","test"],

	["Test","solve_linear"]))];

 Iterator 1;

 moveActiveRoot 1;

 autoCalculate 1 CompleteCalcHead;

 refFormula 1 (get_pos 1 1);

 val ((pt,p),_) = get_calc 1;

 autoCalculate 1 CompleteCalc; 

 val ((pt,p),_) = get_calc 1;

 if p=([], Res) then () else 

 error "FE-interface.sml: diff.behav. in solve_linear AUTOC Head/Calc ";

============ inhibit exn 110620 ==============================================*)

"--------- mini-subpbl AUTOCALCULATE CompleteCalc -------";

"--------- mini-subpbl AUTOCALCULATE CompleteCalc -------";

"--------- mini-subpbl AUTOCALCULATE CompleteCalc -------";

 states:=[];

 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], 

   ("Test", ["sqroot-test","univariate","equation","test"],

    ["Test","squ-equ-test-subpbl1"]))];

 Iterator 1;

 moveActiveRoot 1;

 autoCalculate 1 CompleteCalc;

(*

getTactic 1 ([1],Frm);

getTactic 1 ([1],Res);

initContext 1 Thy_ ([1],Res);

*)

 (*... returns calcChangedEvent with*)

 val (unc, del, gen) = (([],Pbl), ([],Pbl), ([],Res));

 getFormulaeFromTo 1 unc gen 0 (*only result*) false;

 getFormulaeFromTo 1 unc gen 1 (*only level 1*) false;

 getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;

 val ((pt,_),_) = get_calc 1;

 val p = get_pos 1 1;

(*========== inhibit exn 110620 ================================================

 val (Form f, tac, asms) = pt_extract (pt, p);

(*    ModSpec........... =  ...................DIFFERENT !*)

 if term2str f = "[x = 1]" andalso p = ([], Res) then () else 

 error "FE-interface.sml: diff.behav. in mini-subpbl AUTOCALCULATE 6";

============ inhibit exn 110620 ==============================================*)

(*=== inhibit exn ?=============================================================

"--------- mini-subpbl AUTO CompleteCalcHead ------------";

"--------- mini-subpbl AUTO CompleteCalcHead ------------";

"--------- mini-subpbl AUTO CompleteCalcHead ------------";

 states:=[];

 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], 

   ("Test", ["sqroot-test","univariate","equation","test"],

    ["Test","squ-equ-test-subpbl1"]))];

 Iterator 1;

 moveActiveRoot 1;

(* doesn't terminate !!!

 autoCalculate 1 CompleteCalcHead; 

*)

"--------- solve_linear as rootpbl AUTO CompleteModel ---";

"--------- solve_linear as rootpbl AUTO CompleteModel ---";

"--------- solve_linear as rootpbl AUTO CompleteModel ---";

 states:=[];

 CalcTree

     [(["equality (1+-1*2+x=0)", "solveFor x","solutions L"],

       ("Test", 

	["linear","univariate","equation","test"],

	["Test","solve_linear"]))];

 Iterator 1;

 moveActiveRoot 1;

 autoCalculate 1 CompleteModel; 

 refFormula 1 (get_pos 1 1);

setProblem 1 ["linear","univariate","equation","test"];

val pos = get_pos 1 1;

setContext 1 pos (kestoreID2guh Pbl_["linear","univariate","equation","test"]);

 refFormula 1 (get_pos 1 1);

setMethod 1 ["Test","solve_linear"];

setContext 1 pos (kestoreID2guh Met_ ["Test","solve_linear"]);

 refFormula 1 (get_pos 1 1);

 val ((pt,_),_) = get_calc 1;

 if get_obj g_spec pt [] = ("e_domID", 

			    ["linear", "univariate","equation","test"],

			    ["Test","solve_linear"]) then ()

 else error "FE-interface.sml: diff.behav. in setProblem, setMethod";

 autoCalculate 1 CompleteCalcHead;

 refFormula 1 (get_pos 1 1); 

 autoCalculate 1 CompleteCalc; 

 moveActiveDown 1;

 moveActiveDown 1;

 moveActiveDown 1;

 refFormula 1 (get_pos 1 1); 

 val ((pt,_),_) = get_calc 1;

 val p = get_pos 1 1;

 val (Form f, tac, asms) = pt_extract (pt, p);

 if term2str f = "[x = 1]" andalso p = ([], Res) then () else 

 error "FE-interface.sml: diff.behav. in mini-subpbl AUTOCALCULATE 6";

"--------- setContext..Thy ------------------------------";

"--------- setContext..Thy ------------------------------";

"--------- setContext..Thy ------------------------------";

states:=[];

CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], 

  ("Test", ["sqroot-test","univariate","equation","test"],

   ["Test","squ-equ-test-subpbl1"]))];

Iterator 1; moveActiveRoot 1;

autoCalculate 1 CompleteCalcHead;

autoCalculate 1 (Step 1);

val ((pt,p),_) = get_calc 1;  show_pt pt;

(*

setNextTactic 1 (Rewrite_Set "Test_simplify");

autoCalculate 1 (Step 1);

val ((pt,p),_) = get_calc 1;  show_pt pt;

*)

"-----^^^^^ and vvvvv do the same -----";

setContext 1 p "thy_isac_Test-rls-Test_simplify";

val ((pt,p),_) = get_calc 1;  show_pt pt;

autoCalculate 1 (Step 1);

setContext 1 p "thy_isac_Test-rls-Test_simplify";

val ((pt,p),_) = get_calc 1;  show_pt pt;

autoCalculate 1 CompleteCalc;

"--------- mini-subpbl AUTOCALC CompleteToSubpbl --------";

"--------- mini-subpbl AUTOCALC CompleteToSubpbl --------";

"--------- mini-subpbl AUTOCALC CompleteToSubpbl --------";

 states:=[];

 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], 

   ("Test", ["sqroot-test","univariate","equation","test"],

    ["Test","squ-equ-test-subpbl1"]))];

 Iterator 1; moveActiveRoot 1;

 autoCalculate 1 CompleteToSubpbl;

 refFormula 1 (get_pos 1 1); (*<ISA> -1 + x = 0 </ISA>*);

 val ((pt,_),_) = get_calc 1;

 val str = pr_ptree pr_short pt;

 writeln str;

 if str = ".    ----- pblobj -----\n1.   x + 1 = 2\n2.   x + 1 + -1 * 2 = 0\n"

 then () else 

 error "FE-interface.sml: diff.behav. in mini-subpbl CompleteToSubpbl-1";

 autoCalculate 1 (Step 1); (*proceeds only, of NOT 1 step before subplb*)

 autoCalculate 1 CompleteToSubpbl;

 val ((pt,_),_) = get_calc 1;

 val str = pr_ptree pr_short pt;

 writeln str;

 autoCalculate 1 CompleteCalc; (*das geht ohnehin !*);

 val ((pt,_),_) = get_calc 1;

 val p = get_pos 1 1;

 val (Form f, tac, asms) = pt_extract (pt, p);

 if term2str f = "[x = 1]" andalso p = ([], Res) then () else 

 error "FE-interface.sml: diff.behav. in mini-subpbl CompleteToSubpbl 1";

"--------- rat-eq + subpbl: no_met, NO solution dropped -";

"--------- rat-eq + subpbl: no_met, NO solution dropped -";

"--------- rat-eq + subpbl: no_met, NO solution dropped -";

 states:=[];

 CalcTree

 [(["equality ((5*x)/(x - 2) - x/(x+2)=4)", "solveFor x","solutions L"],

   ("RatEq", ["univariate","equation"], ["no_met"]))];

 Iterator 1;

 moveActiveRoot 1; 

 fetchProposedTactic 1;

 setNextTactic 1 (Model_Problem );

autoCalculate 1 (Step 1); fetchProposedTactic 1;

(*-----since Model_Problem + complete_mod_ in case cas of SOME-----*

 setNextTactic 1 (Add_Given "equality (5 * x / (x - 2) - x / (x + 2) = 4)");

 autoCalculate 1 (Step 1); fetchProposedTactic 1;

 setNextTactic 1 (Add_Given "solveFor x");

 autoCalculate 1 (Step 1); fetchProposedTactic 1;

 setNextTactic 1 (Add_Find "solutions L");

 autoCalculate 1 (Step 1); fetchProposedTactic 1;

*-----since Model_Problem + complete_mod_ in case cas of SOME-----*)

 setNextTactic 1 (Specify_Theory "RatEq");

 autoCalculate 1 (Step 1); fetchProposedTactic 1;

 setNextTactic 1 (Specify_Problem ["rational","univariate","equation"]);

 autoCalculate 1 (Step 1); fetchProposedTactic 1;

 setNextTactic 1 (Specify_Method ["RatEq","solve_rat_equation"]);

 autoCalculate 1 (Step 1); fetchProposedTactic 1;

 setNextTactic 1 (Apply_Method ["RatEq","solve_rat_equation"]);

 autoCalculate 1 (Step 1); fetchProposedTactic 1;

 setNextTactic 1 (Rewrite_Set "RatEq_simplify");

 autoCalculate 1 (Step 1); fetchProposedTactic 1;

 setNextTactic 1 (Rewrite_Set "norm_Rational");

 autoCalculate 1 (Step 1); fetchProposedTactic 1;

 setNextTactic 1 (Rewrite_Set "RatEq_eliminate");

 autoCalculate 1 (Step 1); fetchProposedTactic 1;

 (*               __________ for "12 * x + 4 * x ^^^ 2 = 4 * (-4 + x ^^^ 2)"*)

 setNextTactic 1 (Subproblem ("PolyEq", ["normalize","polynomial",

					    "univariate","equation"]));

 autoCalculate 1 (Step 1); fetchProposedTactic 1;

 setNextTactic 1 (Model_Problem );

 autoCalculate 1 (Step 1); fetchProposedTactic 1;

(*-----since Model_Problem + complete_mod_ in case cas of SOME-----*

 setNextTactic 1 (Add_Given 

		      "equality (12 * x + 4 * x ^^^ 2 = 4 * (-4 + x ^^^ 2))");

 autoCalculate 1 (Step 1); fetchProposedTactic 1;

 setNextTactic 1 (Add_Given "solveFor x");

 autoCalculate 1 (Step 1); fetchProposedTactic 1;

 setNextTactic 1 (Add_Find "solutions x_i");

 autoCalculate 1 (Step 1); fetchProposedTactic 1;

*-----since Model_Problem + complete_mod_ in case cas of SOME-----*)

 setNextTactic 1 (Specify_Theory "PolyEq");

 autoCalculate 1 (Step 1); fetchProposedTactic 1;

 setNextTactic 1 (Specify_Problem ["normalize","polynomial",

				   "univariate","equation"]);

 autoCalculate 1 (Step 1); fetchProposedTactic 1;

 setNextTactic 1 (Specify_Method ["PolyEq","normalize_poly"]);

 autoCalculate 1 (Step 1); fetchProposedTactic 1;

 setNextTactic 1 (Apply_Method ["PolyEq","normalize_poly"]);

 autoCalculate 1 (Step 1); fetchProposedTactic 1;

 setNextTactic 1 (Rewrite ("all_left",""));

 autoCalculate 1 (Step 1); fetchProposedTactic 1;

 setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "make_ratpoly_in"));

 autoCalculate 1 (Step 1); fetchProposedTactic 1;

 (*               __________ for "16 + 12 * x = 0"*)

 setNextTactic 1 (Subproblem ("PolyEq",

			 ["degree_1","polynomial","univariate","equation"]));

 autoCalculate 1 (Step 1); fetchProposedTactic 1;

 setNextTactic 1 (Model_Problem );

 autoCalculate 1 (Step 1); fetchProposedTactic 1;

(*-----since Model_Problem + complete_mod_ in case cas of SOME-----*

 setNextTactic 1 (Add_Given 

		      "equality (16 + 12 * x = 0)");

 autoCalculate 1 (Step 1); fetchProposedTactic 1;

 setNextTactic 1 (Add_Given "solveFor x");

 autoCalculate 1 (Step 1); fetchProposedTactic 1;

 setNextTactic 1 (Add_Find "solutions x_i");

 autoCalculate 1 (Step 1); fetchProposedTactic 1;

*-----since Model_Problem + complete_mod_ in case cas of SOME-----*)

 setNextTactic 1 (Specify_Theory "PolyEq");

 (*------------- some trials in the problem-hierarchy ---------------*)

 setNextTactic 1 (Specify_Problem ["linear","univariate","equation"]);

 autoCalculate 1 (Step 1); fetchProposedTactic 1; (*<ERROR> helpless </ERROR> !!!*)

 setNextTactic 1 (Refine_Problem ["univariate","equation"]);

 (*------------------------------------------------------------------*)

 autoCalculate 1 (Step 1); fetchProposedTactic 1;

 setNextTactic 1 (Specify_Method ["PolyEq","solve_d1_polyeq_equation"]);

 autoCalculate 1 (Step 1); fetchProposedTactic 1;

 setNextTactic 1 (Apply_Method ["PolyEq","solve_d1_polyeq_equation"]);

 autoCalculate 1 (Step 1); fetchProposedTactic 1;

 setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "d1_polyeq_simplify"));

 autoCalculate 1 (Step 1); fetchProposedTactic 1;

 setNextTactic 1 (Rewrite_Set "polyeq_simplify");

 autoCalculate 1 (Step 1); fetchProposedTactic 1;

 (*==================================================================*)

 setNextTactic 1 Or_to_List;

 autoCalculate 1 (Step 1); fetchProposedTactic 1;

 setNextTactic 1 (Check_elementwise "Assumptions");

 autoCalculate 1 (Step 1); fetchProposedTactic 1;

 setNextTactic 1 (Check_Postcond ["degree_1","polynomial",

				  "univariate","equation"]);

 autoCalculate 1 (Step 1); fetchProposedTactic 1;

 setNextTactic 1 (Check_Postcond ["normalize","polynomial",

				  "univariate","equation"]);

 autoCalculate 1 (Step 1); fetchProposedTactic 1;

(*========== inhibit exn =======================================================

*** exception TYPE raised (line 460 of "old_goals.ML"):

*** Type error in application: Incompatible operand type

*** 

*** Operator:  equality :: bool => una

*** Operand:   [((x * 3) = -4)] :: bool list

*** 

*** bool => una

*** bool list

*** equality

*** [x * 3 = -4]

 setNextTactic 1 (Check_elementwise "Assumptions");

 autoCalculate 1 (Step 1); fetchProposedTactic 1;

 setNextTactic 1 (Check_Postcond ["rational","univariate","equation"]);

 val (ptp,_) = get_calc 1;

 val (Form t,_,_) = pt_extract ptp;

 if get_pos 1 1 = ([], Res) andalso term2str t = "[x = -4 / 3]" then ()

 else writeln "FE-inteface.sml: diff.behav. in rat-eq + subpbl: no_met, NO ..";

============ inhibit exn =====================================================*)

"--------- tryMatchProblem, tryRefineProblem ------------";

"--------- tryMatchProblem, tryRefineProblem ------------";

"--------- tryMatchProblem, tryRefineProblem ------------";

(*{\bf\UC{Having \isac{} Refine the Problem

 * Automatically}\label{SPECIFY:refine-auto}\\} test match and refine with

 * x^^^2 + 4*x + 5 = 2

see isac.bridge.TestSpecify#testMatchRefine*)

 DEconstrCalcTree 1;

 CalcTree

 [(["equality (x^2 + 4*x + 5 = 2)", "solveFor x","solutions L"],

   ("Isac", 

    ["univariate","equation"],

    ["no_met"]))];

 Iterator 1;

 moveActiveRoot 1; 

 fetchProposedTactic 1;

 setNextTactic 1 (Model_Problem );

 (*..this tactic should be done 'tacitly', too !*)

(*

autoCalculate 1 CompleteCalcHead; 

checkContext 1 ([],Pbl) "pbl_equ_univ";

checkContext 1 ([],Pbl) (kestoreID2guh Pbl_ ["univariate","equation"]);

*)

 autoCalculate 1 (Step 1); 

 fetchProposedTactic 1;

 setNextTactic 1 (Add_Given "equality (x ^^^ 2 + 4 * x + 5 = 2)");

 autoCalculate 1 (Step 1); 

 "--------- we go into the ProblemBrowser (_NO_ pblID selected) -";

initContext 1 Pbl_ ([],Pbl);

initContext 1 Met_ ([],Pbl);

 "--------- this match will show some incomplete items: ---------";

checkContext 1 ([],Pbl) (kestoreID2guh Pbl_ ["univariate","equation"]);

checkContext 1 ([],Pbl) (kestoreID2guh Met_ ["LinEq", "solve_lineq_equation"]);

 fetchProposedTactic 1;

 setNextTactic 1 (Add_Given "solveFor x"); autoCalculate 1 (Step 1);

 fetchProposedTactic 1;

 setNextTactic 1 (Add_Find "solutions L"); autoCalculate 1 (Step 1);

 "--------- this is a matching model (all items correct): -------";

checkContext 1  ([],Pbl) (kestoreID2guh Pbl_ ["univariate","equation"]);

 "--------- this is a NOT matching model (some 'false': ---------";

checkContext 1  ([],Pbl)(kestoreID2guh Pbl_["linear","univariate","equation"]);

 "--------- find out a matching problem: ------------------------";

 "--------- find out a matching problem (FAILING: no new pbl) ---";

 refineProblem 1([],Pbl)(pblID2guh ["linear","univariate","equation"]);

 "--------- find out a matching problem (SUCCESSFUL) ------------";

 refineProblem 1 ([],Pbl) (pblID2guh ["univariate","equation"]);

 "--------- tryMatch, tryRefine did not change the calculation -";

 "--------- this is done by <TRANSFER> on the pbl-browser: ------";

 setNextTactic 1 (Specify_Problem ["normalize","polynomial",

				 "univariate","equation"]);

 autoCalculate 1 (Step 1);

(*WN050904 fetchProposedTactic again --> Specify_Problem ["normalize",...

  and Specify_Theory skipped in comparison to below ---^^^-inserted      *)

(*------------vvv-inserted-----------------------------------------------*)

 fetchProposedTactic 1;

 setNextTactic 1 (Specify_Problem ["normalize","polynomial",

				 "univariate","equation"]);

 autoCalculate 1 (Step 1);

(*and Specify_Theory skipped by fetchProposedTactic ?!?*)

 fetchProposedTactic 1;

 setNextTactic 1 (Specify_Method ["PolyEq","normalize_poly"]);

 autoCalculate 1 (Step 1);

 fetchProposedTactic 1;

 setNextTactic 1 (Apply_Method ["PolyEq","normalize_poly"]);

 autoCalculate 1 CompleteCalc;

 val ((pt,_),_) = get_calc 1;

 show_pt pt;

 val p = get_pos 1 1;

 val (Form f, tac, asms) = pt_extract (pt, p);

 if term2str f = "[x = -1, x = -3]" andalso p = ([], Res) then () else 

 error "FE-interface.sml: diff.behav. in tryMatchProblem, tryRefine";

(*------------^^^-inserted-----------------------------------------------*)

(*WN050904 the fetchProposedTactic's below may not have worked like that

  before, too, because there was no check*)

 fetchProposedTactic 1;

 setNextTactic 1 (Specify_Theory "PolyEq");

 autoCalculate 1 (Step 1);

 fetchProposedTactic 1;

 setNextTactic 1 (Specify_Method ["PolyEq","normalize_poly"]);

 autoCalculate 1 (Step 1);

 fetchProposedTactic 1;

 "--------- now the calc-header is ready for enter 'solving' ----";

 autoCalculate 1 CompleteCalc;

 val ((pt,_),_) = get_calc 1;

rootthy pt;

 show_pt pt;

 val p = get_pos 1 1;

 val (Form f, tac, asms) = pt_extract (pt, p);

 if term2str f = "[x = -1, x = -3]" andalso p = ([], Res) then () else 

 error "FE-interface.sml: diff.behav. in tryMatchProblem, tryRefine";

"--------- modifyCalcHead, resetCalcHead, modelProblem --";

"--------- modifyCalcHead, resetCalcHead, modelProblem --";

"--------- modifyCalcHead, resetCalcHead, modelProblem --";

 states:=[]; 

 DEconstrCalcTree 1;

 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], 

   ("Test", ["sqroot-test","univariate","equation","test"],

    ["Test","squ-equ-test-subpbl1"]))];

 Iterator 1;

 moveActiveRoot 1; 

 modifyCalcHead 1 (([],Pbl),(*the position from refFormula*)

		  "solve (x+1=2, x)",(*the headline*)

		  [Given ["equality (x+1=2)", "solveFor x"],

		   Find ["solutions L"](*,Relate []*)],

		  Pbl, 

		  ("Test", 

		   ["sqroot-test","univariate","equation","test"],

		   ["Test","squ-equ-test-subpbl1"]));

resetCalcHead 1;

modelProblem 1;

"--------- maximum-example, UC: Modeling an example -----";

"--------- maximum-example, UC: Modeling an example -----";

"--------- maximum-example, UC: Modeling an example -----";

(* {\bf\UC{Editing the Model}\label{SPECIFY:enter}\label{SPECIFY:check}\\}

see isac.bridge.TestModel#testEditItems

*)

 val elems = ["fixedValues [r=Arbfix]","maximum A","valuesFor [a,b]",

	      "relations [A=a*b, (a/2)^2 + (b/2)^2 = r^2]",

	      "relations [A=a*b, (a/2)^2 + (b/2)^2 = r^2]",

	      "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]",

	      (*^^^ these are the elements for the root-problem (in variants)*)

              (*vvv these are elements required for subproblems*)

	      "boundVariable a","boundVariable b","boundVariable alpha",

	      "interval {x::real. 0 <= x & x <= 2*r}",

	      "interval {x::real. 0 <= x & x <= 2*r}",

	      "interval {x::real. 0 <= x & x <= pi}",

	      "errorBound (eps=(0::real))"]

 (*specifying is not interesting for this example*)

 val spec = ("DiffApp", ["maximum_of","function"], 

	     ["DiffApp","max_by_calculus"]);

 (*the empty model with descriptions for user-guidance by Model_Problem*)

 val empty_model = [Given ["fixedValues []"],

		    Find ["maximum", "valuesFor"],

		    Relate ["relations []"]];

 states:=[];

 DEconstrCalcTree 1;

 CalcTree [(elems, spec)];

 Iterator 1;

 moveActiveRoot 1; 

 refFormula 1 (get_pos 1 1);

 (*this gives a completely empty model*) 

 fetchProposedTactic 1;

(*fill the CalcHead with Descriptions...*)

 setNextTactic 1 (Model_Problem );

 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);

 (*user input is !!!!!EITHER!!!!! _some_ (at least one) items of the model 

 !!!!!OR!!!!! _one_ part of the specification !!!!!!!!!!!!!*)

 (*input of two items, 'fixedValues [r=Arbfix]' and 'maximum b'...*)

 modifyCalcHead 1 (([],Pbl) (*position, from previous refFormula*),

		  "Problem (DiffApp.thy, [maximum_of, function])",

		  (*the head-form ^^^ is not used for input here*)

		  [Given ["fixedValues [r=Arbfix]"(*new input*)],

		   Find ["maximum b"(*new input*), "valuesFor"], 

		   Relate ["relations"]],

		  (*input (Arbfix will dissappear soon)*)

		  Pbl (*belongsto*),

		  e_spec (*no input to the specification*));

 (*the user does not know, what 'superfluous' for 'maximum b' may mean

  and asks what to do next*)

 fetchProposedTactic 1;

 (*the student follows the advice*)

 setNextTactic 1 (Add_Find "maximum A"); (*FIXME.17.11.03: does not yet work*)

  autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);

 (*this input completes the model*)

 modifyCalcHead 1 (([],Pbl), "not used here",

		  [Given ["fixedValues [r=Arbfix]"],

		   Find ["maximum A", "valuesFor [a,b]"(*new input*)], 

		   Relate ["relations [A=a*b, \

			   \(a/2)^2 + (b/2)^2 = r^2]"]], Pbl, e_spec);

 (*specification is not interesting an should be skipped by the dialogguide;

   !!!!!!!!!!!!!!!!!!!! input of ONE part at a time !!!!!!!!!!!!!!!!!!!!!!*)

 modifyCalcHead 1 (([],Pbl), "not used here",

		  [Given ["fixedValues [r=Arbfix]"],

		   Find ["maximum A", "valuesFor [a,b]"(*new input*)], 

		   Relate ["relations [A=a*b, \

			   \(a/2)^2 + (b/2)^2 = r^2]"]], Pbl, 

		  ("DiffApp", ["e_pblID"], ["e_metID"]));

 modifyCalcHead 1 (([],Pbl), "not used here",

		  [Given ["fixedValues [r=Arbfix]"],

		   Find ["maximum A", "valuesFor [a,b]"(*new input*)], 

		   Relate ["relations [A=a*b, \

			   \(a/2)^2 + (b/2)^2 = r^2]"]], Pbl, 

		  ("DiffApp", ["maximum_of","function"], 

		   ["e_metID"]));

 modifyCalcHead 1 (([],Pbl), "not used here",

		  [Given ["fixedValues [r=Arbfix]"],

		   Find ["maximum A", "valuesFor [a,b]"(*new input*)], 

		   Relate ["relations [A=a*b, \

			   \(a/2)^2 + (b/2)^2 = r^2]"]], Pbl, 

		  ("DiffApp", ["maximum_of","function"], 

		   ["DiffApp","max_by_calculus"]));

 (*this final calcHead now has STATUS 'complete' !*)

 DEconstrCalcTree 1;

"--------- solve_linear from pbl-hierarchy --------------";

"--------- solve_linear from pbl-hierarchy --------------";

"--------- solve_linear from pbl-hierarchy --------------";

 states:=[];

 val (fmz, sp) = ([], ("", ["linear","univariate","equation","test"], []));

 CalcTree [(fmz, sp)];

 Iterator 1; moveActiveRoot 1;

 refFormula 1 (get_pos 1 1);

 modifyCalcHead 1 (([],Pbl),"solve (1+-1*2+x=0)",

		  [Given ["equality (1+-1*2+x=0)", "solveFor x"],

		   Find ["solutions L"]],

		  Pbl, 

		  ("Test", ["linear","univariate","equation","test"],

		   ["Test","solve_linear"]));

 autoCalculate 1 CompleteCalc;

 refFormula 1 (get_pos 1 1);

 val ((pt,_),_) = get_calc 1;

 val p = get_pos 1 1;

 val (Form f, tac, asms) = pt_extract (pt, p);

 if term2str f = "[x = 1]" andalso p = ([], Res) then () else 

 error "FE-interface.sml: diff.behav. in from pbl-hierarchy";

"--------- solve_linear as in an algebra system (CAS)----";

"--------- solve_linear as in an algebra system (CAS)----";

"--------- solve_linear as in an algebra system (CAS)----";

 states:=[];

 val (fmz, sp) = ([], ("", [], []));

 CalcTree [(fmz, sp)];

 Iterator 1; moveActiveRoot 1;

 modifyCalcHead 1 (([],Pbl),"solveTest (1+-1*2+x=0,x)", [], Pbl, ("", [], []));

 autoCalculate 1 CompleteCalc;

 refFormula 1 (get_pos 1 1);

 val ((pt,_),_) = get_calc 1;

 val p = get_pos 1 1;

 val (Form f, tac, asms) = pt_extract (pt, p);

 if term2str f = "[x = 1]" andalso p = ([], Res) then () else 

 error "FE-interface.sml: diff.behav. in algebra system";

"--------- interSteps: on 'miniscript with mini-subpbl' -";

"--------- interSteps: on 'miniscript with mini-subpbl' -";

"--------- interSteps: on 'miniscript with mini-subpbl' -";

 states:=[];

 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], 

   ("Test", ["sqroot-test","univariate","equation","test"],

    ["Test","squ-equ-test-subpbl1"]))];

 Iterator 1;

 moveActiveRoot 1;

 autoCalculate 1 CompleteCalc; 

 val ((pt,_),_) = get_calc 1;

 show_pt pt;

 (*UC\label{SOLVE:INFO:intermediate-steps}*)

 interSteps 1 ([2],Res);

 val ((pt,_),_) = get_calc 1; show_pt pt (*new ([2,1],Frm)..([2,6],Res)*);

 val (unc, del, gen) = (([1],Res),([1],Res),([2,6],Res));

 getFormulaeFromTo 1 unc gen 1 false; 

 (*UC\label{SOLVE:INFO:intermediate-steps}*)

 interSteps 1 ([3,2],Res);

 val ((pt,_),_) = get_calc 1; show_pt pt (*new ([3,2,1],Frm)..([3,2,2],Res)*);

 val (unc, del, gen) = (([3,1],Res),([3,1],Res),([3,2,2],Res));

 getFormulaeFromTo 1 unc gen 1 false; 

 (*UC\label{SOLVE:INFO:intermediate-steps}*)

 interSteps 1 ([3],Res)  (*no new steps in subproblems*);

 val (unc, del, gen) = (([3],Pbl),([3],Pbl),([3,2],Res));

 getFormulaeFromTo 1 unc gen 1 false; 

 (*UC\label{SOLVE:INFO:intermediate-steps}*)

 interSteps 1 ([],Res)  (*no new steps in subproblems*);

 val (unc, del, gen) = (([],Pbl),([],Pbl),([4],Res));

 getFormulaeFromTo 1 unc gen 1 false; 

"--------- getTactic, fetchApplicableTactics ------------";