(* 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";

 *)

 print_depth 3;

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

"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 --------------------";

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

"--------- solve_linear as rootpbl AUTOCALCULATE CompleteCalc ----";

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

"--------- miniscript with mini-subpbl AUTOCALCULATE CompleteCalc-";

"--------- miniscript with mini-subpbl AUTO CompleteCalcHead------";

"--------- solve_linear as rootpbl AUTOCALCULATE CompleteModel ---";

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

"--------- miniscript with mini-subpbl AUTOCALC CompleteToSubpbl -";

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

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

"--------- 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 -----------------------";

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

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

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

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

"--------- replaceFormula {SOLVE:MANUAL:FORMULA:replace} right----";

"--------- replaceFormula {SOLVE:MANUAL:FORMULA:replace} other----";

"--------- replaceFormula {SOLVE:MANUAL:FORMULA:replace} other 2--";

"--------- replaceFormula {SOLVE:MANUAL:FORMULA: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)", "solveFor x","solutions L"],

       ("Test.thy", 

	["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 (*["linear","univariate","equation","test"]*));

                        (*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.thy");

 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;

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

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

 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";

"--------- 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);

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

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

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

 states:=[];

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

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

   ("Test.thy", 

    ["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.thy");

 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.thy",

			      ["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.thy");

 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;

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

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

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

 states:=[];

 CalcTree

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

   ("Test.thy", 

    ["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;

"--------- solve_linear as rootpbl AUTOCALCULATE CompleteCalc ----";

"--------- solve_linear as rootpbl AUTOCALCULATE CompleteCalc ----";

"--------- solve_linear as rootpbl AUTOCALCULATE CompleteCalc ----";

 states:=[];

 CalcTree

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

       ("Test.thy", 

	["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 AUTOCALC CompleteHead/Calc ----";

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

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

 states:=[];

 CalcTree

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

       ("Test.thy", 

	["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 ";

"--------- miniscript with mini-subpbl AUTOCALCULATE CompleteCalc-";

"--------- miniscript with mini-subpbl AUTOCALCULATE CompleteCalc-";

"--------- miniscript with mini-subpbl AUTOCALCULATE CompleteCalc-";

 states:=[];

 CalcTree

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

   ("Test.thy", 

    ["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;

 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";

"--------- miniscript with mini-subpbl AUTO CompleteCalcHead------";

"--------- miniscript with mini-subpbl AUTO CompleteCalcHead------";

"--------- miniscript with mini-subpbl AUTO CompleteCalcHead------";

 states:=[];

 CalcTree

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

   ("Test.thy", 

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

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

 Iterator 1;

(* doesn't terminate !!!

 autoCalculate 1 CompleteCalcHead; 

*)

"--------- solve_linear as rootpbl AUTOCALCULATE CompleteModel ---";

"--------- solve_linear as rootpbl AUTOCALCULATE CompleteModel ---";

"--------- solve_linear as rootpbl AUTOCALCULATE CompleteModel ---";

 states:=[];

 CalcTree

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

       ("Test.thy", 

	["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)", "solveFor x","solutions L"], 

  ("Test.thy", 

   ["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;

"--------- miniscript with mini-subpbl AUTOCALC CompleteToSubpbl -";

"--------- miniscript with mini-subpbl AUTOCALC CompleteToSubpbl -";

"--------- miniscript with mini-subpbl AUTOCALC CompleteToSubpbl -";

 states:=[];

 CalcTree

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

   ("Test.thy", 

    ["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.thy", ["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.thy");

 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.thy", ["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.thy");

 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.thy",

			 ["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.thy");

 (*------------- 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;

 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 ..";

"---------------- 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.thy", 

    ["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.thy");

 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)", "solveFor x","solutions L"], 

   ("Test.thy", 

    ["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.thy", 

		   ["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.thy", ["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.thy", ["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.thy", ["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.thy", ["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.thy", ["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)", "solveFor x","solutions L"], 

   ("Test.thy", 

    ["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*);