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

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

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

  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:HIDE:getTactic}*)

  getTactic 1 ([],Pbl);

  getTactic 1 ([1],Res);

  getTactic 1 ([3],Pbl);

  getTactic 1 ([3,1],Frm);

  getTactic 1 ([3],Res);

  getTactic 1 ([],Res);

 (*UC\label{SOLVE:MANUAL:TACTIC:listall}*)

  fetchApplicableTactics 1 99999 ([],Pbl);

  fetchApplicableTactics 1 99999 ([1],Res);

  fetchApplicableTactics 1 99999 ([3],Pbl);

  fetchApplicableTactics 1 99999 ([3,1],Res);

  fetchApplicableTactics 1 99999 ([3],Res);

  fetchApplicableTactics 1 99999 ([],Res);

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

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

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

 states:=[];

 CalcTree

 [(["equality (x/(x^2 - 6*x+9) - 1/(x^2 - 3*x) =1/x)",

 	   "solveFor x","solutions L"], 

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

 Iterator 1; moveActiveRoot 1;

 autoCalculate 1 CompleteCalc; 

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

 show_pt pt;

 (*UC\label{SOLVE:HELP:assumptions}*)

 getAssumptions 1 ([3], Res);

 getAssumptions 1 ([5], Res);

 (*UC\label{SOLVE:HELP:assumptions-origin} WN0502 still without positions*)

 getAccumulatedAsms 1 ([3], Res);

 getAccumulatedAsms 1 ([5], Res);

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

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

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

  states:=[];

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

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

        ("Test", 

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

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

  Iterator 1; moveActiveRoot 1;

  fetchProposedTactic 1;

  setNextTactic 1 (Model_Problem );

  autoCalculate 1 (Step 1); 

  fetchProposedTactic 1;

  fetchProposedTactic 1;

  setNextTactic 1 (Add_Find "solutions L");

  setNextTactic 1 (Add_Find "solutions L");

  autoCalculate 1 (Step 1); 

  autoCalculate 1 (Step 1); 

  setNextTactic 1 (Specify_Theory "Test");

  fetchProposedTactic 1;

  autoCalculate 1 (Step 1); 

  autoCalculate 1 (Step 1); 

  autoCalculate 1 (Step 1); 

  autoCalculate 1 (Step 1); 

  autoCalculate 1 (Step 1); 

 (*------------------------- end calc-head*)

  fetchProposedTactic 1;

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

  autoCalculate 1 (Step 1); 

  setNextTactic 1 (Rewrite_Set "Test_simplify");

  fetchProposedTactic 1;

  autoCalculate 1 (Step 1); 

  autoCalculate 1 CompleteCalc; 

  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 combinations of steps";

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

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

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

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

  autoCalculate 1 (Step 1);

  appendFormula 1 "-1 + x = 0";  

  (*... returns calcChangedEvent with*)

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

  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 = "-1 + x = 0" andalso p = ([2], Res) then () else 

  error "FE-interface.sml: diff.behav. in FORMULA:enter} right";

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

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

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

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

  autoCalculate 1 (Step 1);

  appendFormula 1 "x - 1 = 0"; 

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

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

  (*11 elements !!!*)

  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 = 0" andalso p = ([2], Res) then () else 

  error "FE-interface.sml: diff.behav. in FORMULA:enter} other";

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

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

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

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

  autoCalculate 1 (Step 1);

  appendFormula 1 "x = 1"; 

  (*... returns calcChangedEvent with*)

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

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

  (*6 elements !!!*)

  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 = ([3,2], Res) then () else 

  error "FE-interface.sml: diff.behav. in FORMULA:enter} oth 2";

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

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

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

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

  autoCalculate 1 (Step 1);

  appendFormula 1 "x - 4711 = 0"; 

  (*... returns <ERROR> no derivation found </ERROR>*)

  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 + -1 * 2 = 0" andalso p = ([1], Res) then () else 

  error "FE-interface.sml: diff.behav. in FORMULA:enter} NOTok";

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

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

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

  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;

  moveActiveFormula 1 ([2],Res);

  replaceFormula 1 "-1 + x = 0" (*i.e. repeats input*);

  (*... returns <ERROR> formula not changed </ERROR>*)

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

  val p = get_pos 1 1;

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

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

  error "FE-interface.sml: diff.behav. in FORMULA:replace} right 1";

  if map fst (get_interval ([2],Res) ([],Res) 9999 pt) = 

     [([2], Res), ([3], Pbl), ([3, 1], Frm), ([3, 1], Res), ([3, 2], Res),

      ([3], Res), ([4], Res), ([], Res)] then () (*nothing deleted!*) else

  error "FE-interface.sml: diff.behav. in FORMULA:replace} right 2";

 (*WN050211 replaceFormula didn't work on second ctree: thus now tested...*)

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

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

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

  Iterator 2;

  moveActiveRoot 2;

  autoCalculate 2 CompleteCalc;

  moveActiveFormula 2 ([2],Res);

  replaceFormula 2 "-1 + x = 0" (*i.e. repeats input*);

  (*... returns <ERROR> formula not changed </ERROR>*)

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

  val p = get_pos 2 1;

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

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

  error "FE-interface.sml: diff.behav. in FORMULA:replace} right 1";

  if map fst (get_interval ([2],Res) ([],Res) 9999 pt) = 

     [([2], Res), ([3], Pbl), ([3, 1], Frm), ([3, 1], Res), ([3, 2], Res),

      ([3], Res), ([4], Res), ([], Res)] then () (*nothing deleted!*) else

  error "FE-interface.sml: diff.behav. in FORMULA:replace} right 2b";

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

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

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

  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;

  moveActiveFormula 1 ([2],Res); (*there is "-1 + x = 0"*)

  replaceFormula 1 "x - 1 = 0"; (*<-------------------------------------*)

  (*... returns calcChangedEvent with*)

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

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

  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 = 0" andalso p = ([2], Res) then () else 

  error "FE-interface.sml: diff.behav. in FORMULA:replace} other 1";

 (* for getting the list in whole length ...

 print_depth 99;map fst (get_interval ([1],Res) ([],Res) 9999 pt);print_depth 3;

    *)

  if map fst (get_interval ([1],Res) ([],Res) 9999 pt) = 

     [([1], Res), ([2, 1], Frm), ([2, 1], Res), ([2, 2], Res), ([2, 3], Res),

       ([2, 4], Res), ([2, 5], Res), ([2, 6], Res), ([2, 7], Res),

       ([2, 8], Res), ([2, 9], Res), ([2], Res)

 (*WN060727 {cutlevup->test_trans} removed: , 

       ([], Res)(*dropped, if test_trans doesnt stop at PblNd*)*)] then () else

  error "FE-interface.sml: diff.behav. in FORMULA:replace} other 2";

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

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

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

  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;

  moveActiveFormula 1 ([2],Res); (*there is "-1 + x = 0"*)

  replaceFormula 1 "x = 1"; (*<-------------------------------------*)

  (*... returns calcChangedEvent with ...*)

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

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

  (*9 elements !!!*)

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

  show_pt pt; (*error: ...get_interval drops ([3,2],Res) ...*)

  val (t,_) = get_obj g_result pt [3,2]; term2str t;

   if map fst (get_interval ([1],Res) ([],Res) 9999 pt) = 

     [([1], Res), ([2], Res), ([3], Pbl), ([3, 1], Frm), ([3, 1], Res),

       ([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res), 

       ([3,2],Res)] then () else

  error "FE-interface.sml: diff.behav. in FORMULA:replace} oth2 1";

  val p = get_pos 1 1;

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

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

  error "FE-interface.sml: diff.behav. in FORMULA:replace} oth2 2";

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

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

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

  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;

  moveActiveFormula 1 ([2],Res); (*there is "-1 + x = 0"*)

  replaceFormula 1 "x - 4711 = 0"; 

  (*... returns <ERROR> no derivation found </ERROR>*)

  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 = "-1 + x = 0" andalso p = ([2], Res) then () else 

  error "FE-interface.sml: diff.behav. in FORMULA:replace} NOTok";

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