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

            java-tests/isac.bridge.

    Author: Walther Neuper

    (c) copyright due to lincense terms.

 Tests the interface of isac's SML-kernel in accordance to java-tests/isac.bridge.

 Some tests are outcommented since "eliminate ThmC.numerals_to_Free";

 these are considered irrelevant for Isabelle/Isac.

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

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

 WN120210?not ME: added some labels, which are not among the above,

 repaired lost \label (s).

 theory Test_Some imports Isac.Build_Thydata begin 

 ML {* KEStore_Elems.set_ref_thy @{theory};

   fun autoCalculate' cI auto = autoCalculate cI auto (*|> Future.join*) *}

 ML_file "Frontend/use-cases.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 Steps 1 ------------";

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

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

 "--------- 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 - WITH fun me IN test/../solve.sml";

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

 "--------- UC errpat chain-rule-diff-both, fillpat by input ------";

 "--------- UC errpat add-fraction, fillpat by input --------------";

 "--------- UC errpat, fillpat step to Rewrite --------------------";

 "--------- UC errpat, fillpat step to Rewrite_Set ----------------";

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

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

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

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

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

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

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

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

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

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

 reset_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 ThyC.id_empty etc. statt leer kommt ???*)

 DEconstrCalcTree 1;

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

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

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

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

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

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

  autoCalculate 1 (Steps 1);

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

  autoCalculate 1 (Steps 1);

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

 (*2*)  fetchProposedTactic 1;

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

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

 (*3*)  fetchProposedTactic 1;

  setNextTactic 1 (Add_Given "solveFor x");

  autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);

 (*4*)  fetchProposedTactic 1;

  setNextTactic 1 (Add_Find "solutions L");

  autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);

 (*5*)  fetchProposedTactic 1;

  setNextTactic 1 (Specify_Theory "Test");

  autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);

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

 (*6*)  fetchProposedTactic 1;

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

  autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);

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

 (*7*)  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 (Steps 1); refFormula 1 (get_pos 1 1);

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

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

 (*8*)  fetchProposedTactic 1;

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

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

  SpecificationC.is_complete ptp;

  References.are_complete ptp;

 (*8*)  autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1); (*<---------------------- orig. test code*)

  val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1; (*<---------------------- orig. test code*)

 (*+isa=REP*) if p = ([1], Frm) andalso UnparseC.term (get_obj g_form pt [1]) = "1 + - 1 * 2 + x = 0"

 andalso Istate.string_of (get_istate_LI pt p)

   = "Pstate ([\"\n(e_e, 1 + - 1 * 2 + x = 0)\", \"\n(v_v, x)\"], [], empty, NONE, \n??.empty, ORundef, false, true)"

 then () else error "refFormula =   1 + - 1 * 2 + x = 0   changed";

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

 (*9*) fetchProposedTactic 1; (*<----------------------------------------------------- orig. test code*)

 (*+\\------------------------------------------ isa == REP -----------------------------------//* )

 (*+//========================================== isa <> REP (1) ===============================\\*)

 (*9*) setNextTactic 1 (Rewrite_Set_Inst (["(''bdv'',x)"], "isolate_bdv")); ( *<------- orig. test code*)

 "~~~~~ fun setNextTactic , args:"; val (cI, tac) = (1, (Rewrite_Set_Inst (["(''bdv'',x)"], "isolate_bdv")));

     val ((pt'''''_', _), _) = get_calc cI

     val ip'''''_' = get_pos cI 1;

     val xxxxx_x(*"ok", (tacis, _, _)*) = (*case*) Step.by_tactic tac (pt'''''_', ip'''''_') (*of*);

 (*+isa+REP*)val ("ok", ( [ (Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv"),

      Rewrite_Set_Inst' _, (pos', (istate, ctxt))) ] , _, cstate)) = xxxxx_x;

 (*//******************* Step.by_tactic returns tac_ + istate + cstate *****************************\\*)

 Step.by_tactic : Tactic.input -> state -> string * (State_Steps.T * pos' list * state);

 if Istate.string_of istate

  = "Pstate ([\"\n(e_e, 1 + - 1 * 2 + x = 0)\", \"\n(v_v, x)\"], [R, L, R, L, R, L, R], empty, SOME e_e, \nx = 0 + - 1 * (1 + - 1 * 2), ORundef, true, true)"

 then () else error "from Step.by_tactic return --- changed 1";

 if Istate.string_of (get_istate_LI (fst cstate) (snd cstate))

  = "Pstate ([\"\n(e_e, 1 + - 1 * 2 + x = 0)\", \"\n(v_v, x)\"], [R, L, R, L, R, L, R], empty, SOME e_e, \nx = 0 + - 1 * (1 + - 1 * 2), ORundef, true, true)"

 then () else error "from Step.by_tactic return --- changed 2";

 (*\\******************* Step.by_tactic returns tac_ + istate + cstate *****************************//*)

 "~~~~~ fun Step.by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt'''''_', ip'''''_'));

       val Applicable.Yes m = (*case*) Step.check tac (pt, p) (*of*);

       (*if*) Tactic.for_specify' m; (*false*)

 Step_Solve.by_tactic m (pt, p);

 "~~~~~ fun by_tactic , args:"; val (m, (pt, po as (p, p_))) = (m, (pt, p));

     (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p); (*else*)

 	      val thy' = get_obj g_domID pt (par_pblobj pt p);

 	      val (is, sc) = LItool.resume_prog thy' (p,p_) pt;

         val Safe_Step (istate, _, tac) =

           (*case*) LI.locate_input_tactic sc (pt, po) (fst is) (snd is) m (*of*);

 (*+*)Safe_Step: Istate.T * Proof.context * Tactic.T -> input_tactic_result;

 (********************* locate_input_tactic returns cstate * istate * Proof.context  *************)

 (*+*)if Istate.string_of istate

 (*+isa*) = "Pstate ([\"\n(e_e, 1 + - 1 * 2 + x = 0)\", \"\n(v_v, x)\"], [R, L, R, L, R, L, R], empty, SOME e_e, \nx = 0 + - 1 * (1 + - 1 * 2), ORundef, true, true)"

 then case m of Rewrite_Set_Inst' _ => ()

 else error "from locate_input_tactic return --- changed";

 val ("ok", (tacis'''''_', _, _)) = xxxxx_x;

 "~~~~~ from TOPLEVEL to states return:"; upd_calc cI ((pt'''''_', ip'''''_'), tacis'''''_');

 (*\\=========================================== isa <> REP (1) ===============================//*)

 (*//=========================================== isa <> REP (2) ===============================\\*)

 (*9* ) autoCalculate 1 (Steps 1); (*<-------------------------------------------------- orig. test code*)

 ( *isa: <AUTOCALC><CALCID>1</CALCID><CALCCHANGED><UNCHANGED><INTLIST><INT>1</INT></INTLIST><POS>Frm</POS></UNCHANGED><DELETED><INTLIST><INT>1</INT></INTLIST><POS>Frm</POS></DELETED><GENERATED><INTLIST><INT>1</INT></INTLIST><POS>Res</POS></GENERATED></CALCCHANGED></AUTOCALC>*)

 "~~~~~ fun autoCalculate , args:"; val (cI, auto) = (1, (Steps 1));

      val pold = get_pos cI 1;

      val xxx = (get_calc cI);

 (*isa*) val (**)xxxx(**) (**) = (**) 

        (*case*) Math_Engine.autocalc [] pold (xxx) auto (*of*);

 "~~~~~ fun autocalc , args:"; val (c, ip, cs, (Solve.Steps s)) = ([], pold, (xxx), auto);

     (*if*) s <= 1; (*then*)

     (*val (str, (_, c', ptp)) =*)

 Step.do_next ip cs;

 "~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt,p), tacis)) = (ip, cs);

 (*+isa==REP*)val [(Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv"),

      Rewrite_Set_Inst' _, (pos', (istate, ctxt)))] = tacis;

 (*+*)if pos' = ([1], Res) andalso Istate.string_of istate

  = "Pstate ([\"\n(e_e, 1 + - 1 * 2 + x = 0)\", \"\n(v_v, x)\"], [R, L, R, L, R, L, R], empty, SOME e_e, \nx = 0 + - 1 * (1 + - 1 * 2), ORundef, true, true)"

 then () else error "init. step 1 + - 1 * 2 + x = 0 changed";

        val pIopt = get_pblID (pt,ip);

        (*if*) ip = ([], Pos.Res);(*else*)

          val (_::_) = (*case*) tacis (*of*);

 (*isa==REP*)    (*if*) ip = p;(*then*)

            (*val (pt',c',p') =*) Solve_Step.s_add_general tacis (pt,[],p);

 (*//------------------------------------- final test -----------------------------------------\\*)

 val ("ok", [], ptp as (pt, p)) = xxxx;

 if Istate.string_of (get_istate_LI pt p) (*                <>                 <>                 <>                 <>                     \<up> \<up> \<up> \<up> ^*)

 (*REP*) = "Pstate ([\"\n(e_e, 1 + - 1 * 2 + x = 0)\", \"\n(v_v, x)\"], [R, L, R, L, R, L, R], empty, SOME e_e, \nx = 0 + - 1 * (1 + - 1 * 2), ORundef, true, true)"

 then () else error "REP autoCalculate on (e_e, 1 + - 1 * 2 + x = 0) changed"

 "~~~~~ from TOPLEVEL to states return:";  upd_calc cI (ptp, []); upd_ipos cI 1 p;

 (*\\=========================================== isa <> REP (2) ===============================//*)

 (*10*)  fetchProposedTactic 1;

  setNextTactic 1 (Rewrite_Set "Test_simplify");

  autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);

 (*11*)  fetchProposedTactic 1;

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

  autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);

 (*======= final test ==================================================*)

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

  val ip = get_pos 1 1;

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

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

  if ip = ([], Res) andalso UnparseC.term 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'*)

 (*-------- WN190723: doesnt work since changeset 59474	21d4d2868b83

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

 DEconstrCalcTree 1;

 ------------------------------------------------------------------------------------------------*)

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

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

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

 (*WN120210?not ME:\label{SOLVE:MANUAL:TACTIC:enter} UC 30.3.2.1 p.175 !!!!!NOT IMPL IN FE*)

 "=== this sequence of fun-calls resembles fun me ===";

  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 (Steps 1); refFormula 1 (get_pos 1 1);(*gets ModSpec;model is still empty*)

  fetchProposedTactic 1; (*<SYSERROR><CALCID>1</CALCID><ERROR>error in kernel 3</ERROR></SYSERROR>* )

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

  autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);

  fetchProposedTactic 1;

  setNextTactic 1 (Add_Given "solveFor x");

  autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);

  fetchProposedTactic 1;

  setNextTactic 1 (Add_Find "solutions L");

  autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);

  fetchProposedTactic 1;

  setNextTactic 1 (Specify_Theory "Test");

  autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);

  fetchProposedTactic 1;

  setNextTactic 1 (Specify_Problem 

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

  autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);

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

  fetchProposedTactic 1;

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

  autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);

  fetchProposedTactic 1;

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

  autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);

  fetchProposedTactic 1;

  setNextTactic 1 (Rewrite_Set "norm_equation");

  autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);

  fetchProposedTactic 1;

  setNextTactic 1 (Rewrite_Set "Test_simplify");

  autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);

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

  setNextTactic 1 (Subproblem ("Test",

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

  autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);

  fetchProposedTactic 1;

  setNextTactic 1 (Model_Problem );

  autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);

  fetchProposedTactic 1;

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

  autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);

  fetchProposedTactic 1;

  setNextTactic 1 (Add_Given "solveFor x");

  autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);

  fetchProposedTactic 1;

  setNextTactic 1 (Add_Find "solutions x_i");

  autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);

  fetchProposedTactic 1;

  setNextTactic 1 (Specify_Theory "Test");

  autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);

  fetchProposedTactic 1;

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

  autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);

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

  fetchProposedTactic 1;

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

  autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);

  fetchProposedTactic 1;

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

  autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);

  fetchProposedTactic 1;

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

  autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);

  fetchProposedTactic 1;

  setNextTactic 1 (Rewrite_Set "Test_simplify");

  autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);

  fetchProposedTactic 1;

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

  autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);

  fetchProposedTactic 1;

  setNextTactic 1 (Check_elementwise "Assumptions");

  autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);

  val xml = fetchProposedTactic 1;

  setNextTactic 1 (Check_Postcond 

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

  autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);

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

  val str = pr_ctree pr_short pt;

  writeln str;

  val ip = get_pos 1 1;

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

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

  if UnparseC.term f = "[x = 1]" then () else 

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

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

  DEconstrCalcTree 1;

 "--------- mini-subpbl AUTOCALCULATE Steps 1 -------------";

 "--------- mini-subpbl AUTOCALCULATE Steps 1 -------------";

 "--------- mini-subpbl AUTOCALCULATE Steps 1 -------------";

 (*WN120210?not ME:\label{SOLVE:AUTO:one} UC 30.3.3.2 p.176*)

  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 (Steps 1); refFormula 1 (get_pos 1 1);

  autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);

  autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);

  autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);

  autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);

  autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);

  autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);

  autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);

  (*here the solve-phase starts*)

  autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);

  autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);

  autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);

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

 (* (*default_print_depth 13*) get_calc 1;

    *)

  autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);

  (*calc-head of subproblem*)

  autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);

  autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);

  autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);

  autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);

  autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);

  autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);

  autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);

  (*solve-phase of the subproblem*)

  autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);

  autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);

  autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);

  autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);

  (*finish subproblem*)

  autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);

  (*finish problem*)

  autoCalculate 1 (Steps 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) = ME_Misc.pt_extract (pt, p);

  if UnparseC.term 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 AUTO CompleteCalc ----";

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

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

 (*WN120210?not ME:\label{SPECIFY:START:auto} UC 30.2.4.2 p.174*)

  CalcTree

      [(["equality (1+- 1*2+x=(0::real))", "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) = ME_Misc.pt_extract (pt, p);

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

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

 DEconstrCalcTree 1;

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

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

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

 (* ERROR: error in kernel ?? *)

  CalcTree

      [(["equality (1+- 1*2+x=(0::real))", "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/Eval ";

 DEconstrCalcTree 1;

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

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

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

 (*WN120210?not ME:\label{SPECIFY:START:auto} UC 30.2.4.2 p.174*)

  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,p),_) = get_calc 1; Test_Tool.show_pt pt;

 (*

 getTactic 1 ([1],Frm);

 getTactic 1 ([1],Res);

 initContext 1 Ptool.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) = ME_Misc.pt_extract (pt, p);

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

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

  DEconstrCalcTree 1;

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

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

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

  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;

 val ((Nd (PblObj {fmz = (fm, ("Test", pblID, metID)), loc = (SOME (env, ctxt1), NONE),

       meth, probl,

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

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

       branch = TransitiveB, ostate = Incomplete (*!?\<forall>*), ...}, []), 

    ([], Met)), []) = get_calc 1;

 if length meth = 3 andalso length probl = 3 (*just some items tested*) then () 

 else error "--- mini-subpbl AUTO CompleteCalcHead ---";

 DEconstrCalcTree 1;

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

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

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

 reset_states ();

  CalcTree

      [(["equality (1+- 1*2+x=(0::real))", "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 (Ptool.kestoreID2guh Ptool.Pbl_["LINEAR", "univariate", "equation", "test"]);*)

  refFormula 1 (get_pos 1 1);

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

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

  refFormula 1 (get_pos 1 1);

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

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

 			    ["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) = ME_Misc.pt_extract (pt, p);

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

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

  DEconstrCalcTree 1;

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

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

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

 reset_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 (Steps 1);

  val ((pt,p),_) = get_calc 1;  Test_Tool.show_pt pt; (*2 lines, OK*)

  (*

  setNextTactic 1 (Rewrite_Set "Test_simplify"); (*--> "thy_isac_Test-rls-Test_simplify"*)

  autoCalculate 1 (Steps 1);

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

  *)

 "----- \<up> ^^ and vvvvv do the same -----";

 (*setContext 1 p "thy_isac_Test-rls-Test_simplify";*)

  val ((pt,p),_) = get_calc 1;  Test_Tool.show_pt pt; (*2 lines, OK*)

  autoCalculate 1 (Steps 1);

 (*setContext 1 p "thy_isac_Test-rls-Test_simplify";*)

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

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

  if p = ([1], Res) andalso UnparseC.term (get_obj g_res pt (fst p)) = "x + 1 + - 1 * 2 = 0"

  then () else error "--- setContext..Thy --- autoCalculate 1 (Steps 1) #1";

  autoCalculate 1 CompleteCalc;

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

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

  if UnparseC.term f = "[x = 1]" andalso p = ([], Res) then () 

   else error "--- setContext..Thy --- autoCalculate CompleteCalc";

  DEconstrCalcTree 1;

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

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

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

 reset_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_ctree 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 (Steps 1); (*proceeds only, if NOT 1 step before subplb*)

  autoCalculate 1 CompleteToSubpbl;

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

  val str = pr_ctree 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) = ME_Misc.pt_extract (pt, p);

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

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

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

 "--------- rat-eq + subpbl: no_met, NO solution dropped - see LI: '--- simpl.rat.term, '..";

 (*--- THIS IS RE-USED WITH fun me IN  test/../MathEngine/solve.sml -------------------

       ---- rat-eq + subpbl: set_found in check_tac1 ----*)

  CalcTree

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

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

  Iterator 1;

  moveActiveRoot 1; 

  fetchProposedTactic 1;

  setNextTactic 1 (Model_Problem);

  autoCalculate 1 (Steps 1); fetchProposedTactic 1;

  setNextTactic 1 (Specify_Theory "RatEq");

  autoCalculate 1 (Steps 1); fetchProposedTactic 1;

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

  autoCalculate 1 (Steps 1); fetchProposedTactic 1;

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

  autoCalculate 1 (Steps 1); fetchProposedTactic 1;

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

  autoCalculate 1 (Steps 1); fetchProposedTactic 1;

  setNextTactic 1 (Rewrite_Set "RatEq_simplify");

  autoCalculate 1 (Steps 1); fetchProposedTactic 1;

  setNextTactic 1 (Rewrite_Set "norm_Rational");

  autoCalculate 1 (Steps 1); fetchProposedTactic 1;

  setNextTactic 1 (Rewrite_Set "RatEq_eliminate");

  autoCalculate 1 (Steps 1); fetchProposedTactic 1;

  (*               __________ for "12 * x + 4 * x \<up> 2 = 4 * (-4 + x \<up> 2)"*)

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

 					    "univariate", "equation"]));

  autoCalculate 1 (Steps 1); fetchProposedTactic 1;

  setNextTactic 1 (Model_Problem );

  autoCalculate 1 (Steps 1); fetchProposedTactic 1;

  setNextTactic 1 (Specify_Theory "PolyEq");

  autoCalculate 1 (Steps 1); fetchProposedTactic 1;

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

 				   "univariate", "equation"]);

  autoCalculate 1 (Steps 1); fetchProposedTactic 1;

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

  autoCalculate 1 (Steps 1); fetchProposedTactic 1;

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

  autoCalculate 1 (Steps 1); fetchProposedTactic 1;

  setNextTactic 1 (Rewrite ("all_left", @{thm all_left}));

  autoCalculate 1 (Steps 1); fetchProposedTactic 1;

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

  autoCalculate 1 (Steps 1); fetchProposedTactic 1;

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

  setNextTactic 1 (Subproblem ("PolyEq",

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

  autoCalculate 1 (Steps 1); fetchProposedTactic 1;

  setNextTactic 1 (Model_Problem );

  autoCalculate 1 (Steps 1); fetchProposedTactic 1;

  setNextTactic 1 (Specify_Theory "PolyEq");

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

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

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

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

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

  autoCalculate 1 (Steps 1); fetchProposedTactic 1;

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

  autoCalculate 1 (Steps 1); fetchProposedTactic 1;

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

  autoCalculate 1 (Steps 1); fetchProposedTactic 1;

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

 (*SINCE eliminate ThmC.numerals_to_Free: 

     rewrite_set_, rewrite_ "- 4 / 3 = - 4 / 3" x = - 4 / 3 = NONE---------------------------\\* )

  autoCalculate 1 (Steps 1); fetchProposedTactic 1;

  setNextTactic 1 (Rewrite_Set "polyeq_simplify");

  autoCalculate 1 (Steps 1); fetchProposedTactic 1;

  setNextTactic 1 Or_to_List;

  autoCalculate 1 (Steps 1); fetchProposedTactic 1;

  setNextTactic 1 (Check_elementwise "Assumptions"); 

  autoCalculate 1 (Steps 1); fetchProposedTactic 1;

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

 				  "univariate", "equation"]);

  autoCalculate 1 (Steps 1); fetchProposedTactic 1;

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

 				  "univariate", "equation"]);

  autoCalculate 1 (Steps 1); fetchProposedTactic 1;

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

  val (ptp,_) = get_calc 1;

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

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

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

  DEconstrCalcTree 1;

 ( *SINCE eliminate ThmC.numerals_to_Free: 

     rewrite_set_, rewrite_ "- 4 / 3 = - 4 / 3" x = - 4 / 3 = NONE---------------------------//*)

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

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

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

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

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

  * x \<up>2 + 4*x + 5 = 2

 see isac.bridge.TestSpecify#testMatchRefine*)

 reset_states ();

  CalcTree

  [(["equality (x \<up> 2 + 4*x + 5 = (2::real))", "solveFor x", "solutions L"],

    ("Isac_Knowledge", 

     ["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) (Ptool.kestoreID2guh Ptool.Pbl_ ["univariate", "equation"]);

 *)

  autoCalculate 1 (Steps 1); 

  fetchProposedTactic 1;

  setNextTactic 1 (Add_Given "equality (x \<up> 2 + 4 * x + 5 = (2::real))");

  autoCalculate 1 (Steps 1); 

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

 (*initContext 1 Ptool.Pbl_ ([],Pbl);*)

 (* this would break if a calculation would be inserted before: CALCID...

    and pattern matching is not available in *.java.

 if cut_xml xml = "(CONTEXTPBL)\n. (CALCID)\n. . 1\n. (/CALCID)\n. (CONTEXTDATA)\n. . (GUH)\n. . . pbl_equ_univ\n. . (/GUH)\n. . (STATUS)\n. . . correct\n. . (/STATUS)\n. . (HEAD)\n. . . (MATHML)\n. . . . (ISA)\n. . . . . solve (x ^ 2 + 4 * x + 5 = 2, x)\n. . . . (/ISA)\n. . . (/MATHML)\n. . (/HEAD)\n. . (MODEL)\n. . . (GIVEN)\n. . . . (ITEM status=correct)\n. . . . . (MATHML)\n. . . . . . (ISA)\n. . . . . . . equality (x ^ 2 + 4 * x + 5 = 2)\n. . . . . . (/ISA)\n. . . . . (/MATHML)\n. . . . (/ITEM)\n. . . . (ITEM status=correct)\n. . . . . (MATHML)\n. . . . . . (ISA)\n. . . . . . . solveFor x\n. . . . . . (/ISA)\n. . . . . (/MATHML)\n. . . . (/ITEM)\n. . . (/GIVEN)\n. . . (WHERE)\n. . . . (ITEM status=correct)\n. . . . . (MATHML)\n. . . . . . (ISA)\n. . . . . . . TermC.matches (?a = ?b) (x  \<up> ^ 2 + 4 * x + 5 = 2)\n. . . . . . (/ISA)\n. . . . . (/MATHML)\n. . . . (/ITEM)\n. . . (/WHERE)\n. . . (FIND)\n. . . . (ITEM status=correct)\n. . . . . (MATHML)\n. . . . . . (ISA)\n. . . . . . . solutions L\n. . . . . . (/ISA)\n. . . . . (/MATHML)\n. . . . (/ITEM)\n. . . (/FI"

 then () else error "--- tryMatchProblem, tryRefineProblem: initContext 1 Ptool.Pbl_ ([],Pbl); CHANGED";

 *)

 (*initContext 1 Ptool.Met_ ([],Pbl);*)

 (*<SYSERROR><CALCID>1</CALCID><ERROR>error in kernel 33</ERROR></SYSERROR>*)

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

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

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

  fetchProposedTactic 1;

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

  fetchProposedTactic 1;

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

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

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

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

 (*checkContext 1  ([],Pbl)(Ptool.kestoreID2guh Ptool.Pbl_ ["LINEAR", "univariate", "equation"]);*)

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

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

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

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

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

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

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

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

 				 "univariate", "equation"]);

  autoCalculate 1 (Steps 1);

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

   and Specify_Theory skipped in comparison to below --- \<up> -inserted      *)

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

  fetchProposedTactic 1;

 (*/-----ERROR INTRODUCED BY CHILD OF 33913fe24685 --------------------------------------------\* )

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

 				 "univariate", "equation"]);

  autoCalculate 1 (Steps 1);

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

  fetchProposedTactic 1;

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

  autoCalculate 1 (Steps 1);

  fetchProposedTactic 1;

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

  autoCalculate 1 CompleteCalc;

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

  Test_Tool.show_pt pt;

  val p = get_pos 1 1;

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

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

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

 (*------------ \<up> -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 (Steps 1);

  fetchProposedTactic 1;

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

  autoCalculate 1 (Steps 1);

  fetchProposedTactic 1;

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

  autoCalculate 1 CompleteCalc;

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

  rootthy pt;

  Test_Tool.show_pt pt;

  val p = get_pos 1 1;

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

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

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

  DEconstrCalcTree 1;

 ( *\-----ERROR INTRODUCED BY CHILD OF 33913fe24685 --------------------------------------------/*)

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

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

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

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

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

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

 		  [P_Spec.Given ["equality (x+1=(2::real))", "solveFor x"],

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

 		  Pbl, 

 		  ("Test", 

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

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

 val ((Nd (PblObj {fmz = (fm, tpm),

                   loc = (SOME scrst_ctxt, NONE),

                   ctxt,

                   meth,

                   spec = (thy,

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

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

                   probl,

                   branch = TransitiveB,

                   origin,

                   ostate = Incomplete,

                   result},

                []),

          ([], Pbl)),

       []) = get_calc 1;

 (*WN110622: is the same as in 2002, but shouldn't be probl = [3 items?]*)

 if length meth = 0 andalso length probl = 0 (*just some items tested*) then () 

 else error "--- modifyCalcHead, resetCalcHead, modelProblem 1 --";

 resetCalcHead 1;

 modelProblem 1;

 get_calc 1;

 val ((Nd (PblObj {fmz = (fm, tpm),

                   loc = (SOME scrst_ctxt, NONE),

                   ctxt,

                   meth,

                   spec = ("empty_thy_id", ["empty_probl_id"], ["empty_meth_id"]),

                   probl,

                   branch = TransitiveB,

                   origin,

                   ostate = Incomplete,

                   result},

                []),

          ([], Pbl)),

       []) = get_calc 1;

 if length meth = 3 andalso length probl = 3 (*just some items tested*) then () 

 else error "--- modifyCalcHead, resetCalcHead, modelProblem 2 --";

 "--------- 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) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]",

 	      "relations [A=a*b, (a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]",

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

 	      (* \<up>  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 = [P_Spec.Given ["fixedValues []"],

 		    P_Spec.Find ["maximum", "valuesFor"],

 		    P_Spec.Relate ["relations []"]]; 

  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 (Steps 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 \<up> is not used for input here*)

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

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

 		   P_Spec.Relate ["relations"]],

 		  (*input (Arbfix will dissappear soon)*)

 		  Pbl (*belongsto*),

 		  References.empty (*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 (Steps 1); refFormula 1 (get_pos 1 1);

  (*this input completes the model*)

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

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

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

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

 			   \(a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]"]], Pbl, References.empty);

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

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

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

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

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

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

 			   \(a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]"]], Pbl, 

 		  ("DiffApp", ["empty_probl_id"], ["empty_meth_id"]));

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

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

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

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

 			   \(a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]"]], Pbl, 

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

 		   ["empty_meth_id"]));

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

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

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

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

 			   \(a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 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 --------------";

 reset_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::real))",

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

 		   P_Spec.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) = ME_Misc.pt_extract (pt, p);

  if UnparseC.term f = "[x = 1]" andalso p = ([], Res) andalso map UnparseC.term asms = [] then () 

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

  DEconstrCalcTree 1;

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

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

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

 (*WN120210?not ME:\label{UC:cas-input} UC 30.1.2.5 p.168*)

 reset_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) = ME_Misc.pt_extract (pt, p);

  if UnparseC.term f = "[x = 1]" andalso p = ([], Res) andalso map UnparseC.term asms = [] then () 

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

 DEconstrCalcTree 1;

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

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

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

  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;

  Test_Tool.show_pt pt;

  (*UC\label{UC:inter-steps} UC 30.3.5.5 p.178*)

  interSteps 1 ([2],Res);

  val ((pt,_),_) = get_calc 1; Test_Tool.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{UC:inter-steps} UC 30.3.5.5 p.178*)

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

  val ((pt,_),_) = get_calc 1; Test_Tool.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{UC:inter-steps} UC 30.3.5.5 p.178*)

  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{UC:inter-steps} UC 30.3.5.5 p.178*)

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

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

  getFormulaeFromTo 1 unc gen 1 false; 

 DEconstrCalcTree 1;

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

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

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

 (* compare test/../script.sml

 "----------- fun from_prog ---------------------------------------";

 *)

  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;

  Test_Tool.show_pt pt;

  (*UC\label{SOLVE:HIDE:getTactic} \label{SOLVE:AUTO:tactic} UC 30.3.3.1 p.176

 WN120210 not impl. in FE*)

  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} UC 30.3.2.2 p.175*)

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

 DEconstrCalcTree 1;

 (*SINCE eliminate ThmC.numerals_to_Free: loops ---------------------------------------------\\* )

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

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

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

 reset_states ();

 CalcTree

 [(["equality (x/(x \<up> 2 - 6*x+9) - 1/(x \<up> 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;

 val p = get_pos 1 1;

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

 (*============ inhibit exn WN120316 compare 2002-- 2011 ===========================

 if map UnparseC.term asms = 

  ["True |\n~ lhs ((3 + - 1 * x + x \<up> 2) * x =\n" ^

   "       1 * (9 * x + -6 * x \<up> 2 + x \<up> 3)) is_poly_in x", "-6 * x + 5 * x \<up>\<up> 2 = 0", 

   "lhs (-6 * x + 5 * x \<up> 2 = 0) is_poly_in x",

   "lhs (-6 * x + 5 * x \<up>\<up> 2 = 0) has_degree_in x = 2", 

   "9 * x + -6 * x \<up> 2 + x \<up> 3 ~= 0"] 

 andalso UnparseC.term f = "[-6 * x + 5 * x \<up> 2 = 0]" andalso p = ([], Res) then ()

 else error "TODO compare 2002-- 2011"; (*...data during test --- x / (x  \<up>  2 - 6 * x + 9) - 1...*)

 ============ inhibit exn WN120316 compare 2002-- 2011 ===========================*)

 if p = ([], Res) andalso UnparseC.term f = "[x = 6 / 5]"

 andalso map UnparseC.term asms = []

 then () else error "rlang.sml: diff.behav. in  Schalk I s.87 Bsp 55b [x = 6 / 5]";

 (*UC\label{SOLVE:HELP:assumptions} UC 30.3.5.1 p.178*)

 getAssumptions 1 ([3], Res);

 getAssumptions 1 ([5], Res);

 (*UC\label{SOLVE:HELP:assumptions-origin} UC 30.3.5.2 p.178

   WN0502 still without positions*)

 getAccumulatedAsms 1 ([3], Res);

 getAccumulatedAsms 1 ([5], Res);

 DEconstrCalcTree 1;

 ( *SINCE eliminate ThmC.numerals_to_Free: loops ---------------------------------------------//*)

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

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

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

  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; moveActiveRoot 1;

  fetchProposedTactic 1;

              (*ERROR get_calc 1 not existent*)

  setNextTactic 1 (Model_Problem );

  autoCalculate 1 (Steps 1); 

  fetchProposedTactic 1;

  fetchProposedTactic 1;

  setNextTactic 1 (Add_Find "solutions L");

  setNextTactic 1 (Add_Find "solutions L");

  autoCalculate 1 (Steps 1); 

  autoCalculate 1 (Steps 1); 

  setNextTactic 1 (Specify_Theory "Test");

  fetchProposedTactic 1;

  autoCalculate 1 (Steps 1); 

  autoCalculate 1 (Steps 1); 

  autoCalculate 1 (Steps 1); 

  autoCalculate 1 (Steps 1); 

  autoCalculate 1 (Steps 1); 

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

  fetchProposedTactic 1;

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

  autoCalculate 1 (Steps 1); 

  setNextTactic 1 (Rewrite_Set "Test_simplify");

  fetchProposedTactic 1;

  autoCalculate 1 (Steps 1); 

  autoCalculate 1 CompleteCalc; 

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

  val p = get_pos 1 1;

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

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

  error "FE-interface.sml: diff.behav. in combinations of steps";

 DEconstrCalcTree 1;

 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}right"; (*UC 30.3.2.4 p.175*)

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

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

  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 (Steps 1);

  autoCalculate 1 (Steps 1);

  appendFormula 1 "- 1 + x = 0" (*|> Future.join*);

  (*... 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) = ME_Misc.pt_extract (pt, p);

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

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

 DEconstrCalcTree 1;

 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}other"; (*UC 30.3.2.4 p.175*)

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

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

  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 (Steps 1);

  autoCalculate 1 (Steps 1);

  appendFormula 1 "x - 1 = 0" (*|> Future.join*);

  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) = ME_Misc.pt_extract (pt, p);

  if UnparseC.term f = "x - 1 = 0" andalso p = ([2], Res) then () else 

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

 DEconstrCalcTree 1;

 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}oth 2"; (*UC 30.3.2.4 p.175*)

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

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

  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 (Steps 1);

  autoCalculate 1 (Steps 1);

  appendFormula 1 "x = 1" (*|> Future.join*);

  (*... 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) = ME_Misc.pt_extract (pt, p);

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

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

 DEconstrCalcTree 1;

 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}NOTok"; (*UC 30.3.2.4 p.175*)

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

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

  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 (Steps 1);

  autoCalculate 1 (Steps 1);

  appendFormula 1 "x - 4711 = 0" (*|> Future.join*);

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

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

  val p = get_pos 1 1;

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

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

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

 DEconstrCalcTree 1;

 "--------- replaceFormula {SOL:MAN:FOR:replace} right----"; (*UC 30.3.2.5 p.176*)

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

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

 (*\label{SOLVE:MANUAL:FORMULA:replace}*)

  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) = ME_Misc.pt_extract (pt, p);

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

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

  if map fst3 (ME_Misc.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; (*! ! ! 1 CalcTree inbetween reset_states (); *)

  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) = ME_Misc.pt_extract (pt, p);

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

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

  if map fst3 (ME_Misc.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";

 DEconstrCalcTree 1;

 "--------- replaceFormula {SOL:MAN:FOR:replace} other----"; (*UC 30.3.2.5 p.176*)

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

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

 (*\label{SOLVE:MANUAL:FORMULA:replace}*)

  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;

  Test_Tool.show_pt pt;

  val p = get_pos 1 1;

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

  if UnparseC.term 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 ...

 (*default_print_depth 99*) map fst3 (ME_Misc.get_interval ([1],Res) ([],Res) 9999 pt); (*default_print_depth 3*)

    *)

  if map fst3 (ME_Misc.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)] then () else

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

 DEconstrCalcTree 1;

 "--------- replaceFormula {SOL:MAN:FOR:replace} other 2--"; (*UC 30.3.2.5 p.176*)

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

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

 (*\label{SOLVE:MANUAL:FORMULA:replace}*)

  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;

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

  val (t,_) = get_obj g_result pt [3,2]; UnparseC.term t;

   if map fst3 (ME_Misc.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) = ME_Misc.pt_extract (pt, p);

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

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

 DEconstrCalcTree 1;

 "--------- replaceFormula {SOL:MAN:FOR:replace} NOTok----"; (*UC 30.3.2.5 p.176*)

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

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

 (*\label{SOLVE:MANUAL:FORMULA:replace}*)

  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;

  Test_Tool.show_pt pt;

  val p = get_pos 1 1;

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

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

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

  DEconstrCalcTree 1;

 "--------- UC errpat chain-rule-diff-both, fillpat by input ------";

 "--------- UC errpat chain-rule-diff-both, fillpat by input ------";

 "--------- UC errpat chain-rule-diff-both, fillpat by input ------";

 CalcTree

 [(["functionTerm (x  \<up>  2 + sin (x  \<up>  4))", "differentiateFor x", "derivative f_f'"], 

   ("Isac_Knowledge", ["derivative_of", "function"], ["diff", "differentiate_on_R"]))];

 Iterator 1;

 moveActiveRoot 1;

 autoCalculate 1 CompleteCalcHead;

 autoCalculate 1 (Steps 1);

 autoCalculate 1 (Steps 1);(*([1], Res), d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))*)

 appendFormula 1 "d_d x (x  \<up>  2) + cos (4 * x  \<up>  3)" (*|> Future.join*); (*<<<<<<<=========================*)

 (* the check for errpat is maximally liberal (whole term modulo "nrls" from "type met"),

   would recognize "cos (4 * x  \<up>  (4 - 1)) + 2 * x" as well.

   results in <CALCMESSAGE> error pattern #chain-rule-diff-both# </CALCMESSAGE>

   instead of <CALCMESSAGE> no derivation found </CALCMESSAGE> *)

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

   val p = get_pos 1 1;

   val (Form f, _, asms) = ME_Misc.pt_extract (pt, p);

   if p = ([1], Res) andalso UnparseC.term f = "d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))"

   then case get_obj g_tac pt (fst p) of Rewrite_Inst (["(''bdv'', x)"],

       ("diff_sum", thm)) => () | _ => error "embed fun fill_form changed 0"

   | _ => error "embed fun fill_form changed 1"

 else error "embed fun fill_form changed 2";

 (*========== inhibit exn WN1130621 Isabelle2012-->13 !thehier! ====================

 findFillpatterns 1 "chain-rule-diff-both"; (*<<<<<<<=================================*)

 (*<CALCMESSAGE> fill patterns #fill-d_d-arg#d_d x (x \<up> 2) + d_d x (sin (x \<up> 4)) =

   d_d x (x \<up> 2) + cos (x \<up> 4) * d_d x ?_dummy_1#fill-both-args#...#...#... *)

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

   val p = get_pos 1 1;

   val (Form f, _, asms) = ME_Misc.pt_extract (pt, p);

   if p = ([1], Res) andalso UnparseC.term f = "d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))" andalso

     get_obj g_tac pt (fst p) = Rewrite_Inst (["(''bdv'', x)"], ("diff_sum", "Diff.diff_sum"(*?!?*)))

   then ()

   else error "embed fun fill_form changed 2";

 (* if we assume, that the fill-patterns are ordered such that the 1st has large gaps

    and the last has no gaps, then the number of fill-patterns would suffice

    for the DialogGuide to select appropriately. *)

 requestFillformula 1 ("chain-rule-diff-both", "fill-both-args");(*<<<<<<<============*)

   (*<AUTOCALC> ([1], Res) ([2], Res) ([2], Res) </AUTOCALC>*)

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

   val p = get_pos 1 1;

   val (Form f, _, asms) = ME_Misc.pt_extract (pt, p);

   if p = ([1], Res) andalso existpt [2] pt andalso

     UnparseC.term f = "d_d x (x \<up> 2) + d_d x (sin (x \<up>\<up> 4))" andalso

     get_obj g_tac pt (fst p) = Rewrite_Inst (["(''bdv'', x)"], ("diff_sum", "Diff.diff_sum"))

   then () else error "embed fun fill_form changed 3";

 inputFillFormula 1 "d_d x (x \<up> 2) + cos (x \<up> 4) * d_d x (x \<up> 4)";(*<<<<<<<=====*)

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

   val p = get_pos 1 1;

   val (Form f, _, asms) = ME_Misc.pt_extract (pt, p);

   if p = ([2], Res) andalso

     UnparseC.term f = "d_d x (x \<up> 2) + cos (x \<up> 4) * d_d x (x \<up> 4)" andalso

     get_obj g_tac pt (fst p) = Rewrite_Inst (["(''bdv'', x)"], ("diff_sin_chain", ""))

   then () else error "inputFillFormula changed 11";

 autoCalculate 1 CompleteCalc;

 "~~~~~ final check: the input formula is inserted as it would have been correct from beginning";

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

 val p = get_pos 1 1;

 val (Form f, _, asms) = ME_Misc.pt_extract (pt, p);

 if p = ([], Res) andalso UnparseC.term f = "2 * x + cos (x \<up> 4) * 4 * x \<up> 3"

 then () else error "inputFillFormula changed 12";

 Test_Tool.show_pt pt;

 (*[

 (([], Frm), Diff (x \<up> 2 + sin (x \<up> 4), x)),

 (([1], Frm), d_d x (x \<up> 2 + sin (x \<up> 4))),

 (([1], Res), d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))),

 (([2], Res), d_d x (x \<up> 2) + cos (x \<up> 4) * d_d x (x \<up> 4)),       (*<<<<<<<=====*)

 (([3], Res), d_d x (x \<up> 2) + cos (x \<up> 4) * (4 * x \<up> (4 - 1))),

 (([4], Res), 2 * x \<up> (2 - 1) + cos (x \<up> 4) * (4 * x \<up> (4 - 1))),

 (([5], Res), 2 * x + cos (x \<up> 4) * 4 * x \<up> 3),

 (([], Res), 2 * x + cos (x \<up> 4) * 4 * x \<up> 3)] *)

 ============ inhibit exn WN1130621 Isabelle2012-->13 !thehier! ==================*)

 DEconstrCalcTree 1;

 "--------- UC errpat add-fraction, fillpat by input --------------";

 "--------- UC errpat add-fraction, fillpat by input --------------";

 "--------- UC errpat add-fraction, fillpat by input --------------";

 (*cp from BridgeLog Java <=> SML*)

 CalcTree [([], ("empty_thy_id", ["empty_probl_id"], ["empty_meth_id"]))];

 Iterator 1;

 moveActiveRoot 1;

 moveActiveFormula 1 ([],Pbl);

 replaceFormula 1 "Simplify (5 * x / (4 * y) + 3 * x / (4 * y))";

 autoCalculate 1 CompleteCalcHead;

 autoCalculate 1 (Steps 1);

 appendFormula 1 "8 * x / (8 * y)" (*|> Future.join*);

 (*<CALCMESSAGE> no derivation found </CALCMESSAGE> 

 --- but in BridgeLog Java <=> SML:

 <CALCMESSAGE> error pattern #addition-of-fractions# </CALCMESSAGE>*)

 DEconstrCalcTree 1;

 "--------- UC errpat, fillpat step to Rewrite --------------------";

 "--------- UC errpat, fillpat step to Rewrite --------------------";

 "--------- UC errpat, fillpat step to Rewrite --------------------";

 (*TODO*)

 CalcTree

 [(["functionTerm ((x  \<up>  2)  \<up>  3 + sin (x  \<up>  4))",

    "differentiateFor x", "derivative f_f'"], 

   ("Isac_Knowledge", ["derivative_of", "function"],

   ["diff", "differentiate_on_R"]))]; (*<<<======= EP is directly in script*)

 Iterator 1;

 moveActiveRoot 1;

 autoCalculate 1 CompleteCalc;

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

 DEconstrCalcTree 1;

 "--------- UC errpat, fillpat step to Rewrite_Set ----------------";

 "--------- UC errpat, fillpat step to Rewrite_Set ----------------";

 "--------- UC errpat, fillpat step to Rewrite_Set ----------------";

 CalcTree

 [(["functionTerm ((x  \<up>  2)  \<up>  3 + sin (x  \<up>  4))",

    "differentiateFor x", "derivative f_f'"], 

   ("Isac_Knowledge", ["derivative_of", "function"],

   ["diff", "after_simplification"]))]; (*<<<======= EP is in a ruleset*)

 Iterator 1;

 moveActiveRoot 1;

 autoCalculate 1 CompleteCalcHead;

 autoCalculate 1 (Steps 1); fetchProposedTactic 1;

 autoCalculate 1 (Steps 1); fetchProposedTactic 1;

 (*

 <NEXTTAC>

   <CALCID> 1 </CALCID>

   <TACTICERRORPATTERNS>

     <STRINGLIST>

       <STRING> chain-rule-diff-both </STRING>

       <STRING> cancel </STRING>

     </STRINGLIST>

     <REWRITESETINSTTACTIC name="Rewrite_Set_Inst">

       <RULESET> norm_diff </RULESET>

       <SUBSTITUTION>

         <PAIR>

           <VARIABLE>

             <MATHML>

               <ISA> bdv </ISA>

             </MATHML>

           </VARIABLE>

           <VALUE>

             <MATHML>

               <ISA> x </ISA>

             </MATHML>

           </VALUE>

         </PAIR>

       </SUBSTITUTION>

     </REWRITESETINSTTACTIC>

   </TACTICERRORPATTERNS>

 </NEXTTAC>

 (*WN1208 postponed due to efforts required for stepToErrorPatterns (NEW rewrite_set_)*)

 stepToErrorPatterns 1; (*--> calcChanged, rule immediately calls... *)

 stepOnErrorPatterns 1; (*--> calcChanged, rule calls getTactic and displays it *)

 (* then --- UC errpat, fillpat by input ---*)

 *)

 autoCalculate 1 CompleteCalc;

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

 (*WN1208 postponed due to efforts required for stepToErrorPatterns (NEW rewrite_set_)*)

 DEconstrCalcTree 1;