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

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

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

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

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

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

(*2*)  fetchProposedTactic 1;

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

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

(*3*)  fetchProposedTactic 1;

 setNextTactic 1 (Add_Given "solveFor x");

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

(*4*)  fetchProposedTactic 1;

 setNextTactic 1 (Add_Find "solutions L");

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

(*5*)  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-----*)

(*6*)  fetchProposedTactic 1;

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

 autoCalculate 1 (Step 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 (Step 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;

 is_complete_mod ptp;

 is_complete_spec ptp;

(*8*)  autoCalculate 1 (Step 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 term2str (get_obj g_form pt [1]) = "1 + -1 * 2 + x = 0"

andalso istate2str (get_istate pt p)

  = "Pstate ([\"\n(e_e, 1 + -1 * 2 + x = 0)\",\"\n(v_v, x)\"], [], e_rls, NONE, \n??.empty, ORundef, AppUndef_, 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*) Math_Engine.locatetac tac (pt'''''_', ip'''''_') (*of*);

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

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

(*//******************* locatetac returns tac_ + istate + cstate *****************************\\*)

locatetac : Tactic.input -> state -> string * (taci list * pos' list * state);

if istate2str istate

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

then () else error "from locatetac return --- changed 1";

if istate2str (get_istate (fst cstate) (snd cstate))

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

then () else error "from locatetac return --- changed 2";

(*\\******************* locatetac returns tac_ + istate + cstate *****************************//*)

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

      val (mI, m) = Solve.mk_tac'_ tac;

      val Chead.Appl m = (*case*) Applicable.applicable_in p pt m (*of*);

      (*if*) member op = Solve.specsteps mI; (*else*)

        (*val Updated (cs' as (_, _, (_, p'))) =*) loc_solve_ (mI,m) ptp;

"~~~~~ fun loc_solve_ , args:"; val (m, (pt, pos)) = ((mI,m), ptp); 

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

    (*if*) Celem.e_metID = get_obj g_metID pt (par_pblobj pt p); (*else*)

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

	      val (srls, is, sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;

        val Safe_Step (istate, _, tac) =

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

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

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

(*+*)if istate2str istate

(*+isa*) = "Pstate ([\"\n(e_e, 1 + -1 * 2 + x = 0)\",\"\n(v_v, x)\"], [R,L,R,L,R,L,R], e_rls, SOMEe_e, \nx = 0 + -1 * (1 + -1 * 2), ORundef, AppUndef_, 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 (Step 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, (Step 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.Step s)) = ([], pold, (xxx), auto);

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

    (*val (str, (_, c', ptp)) =*) step ip cs;

"~~~~~ fun step , 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 istate2str istate

 = "Pstate ([\"\n(e_e, 1 + -1 * 2 + x = 0)\",\"\n(v_v, x)\"], [R,L,R,L,R,L,R], e_rls, SOMEe_e, \nx = 0 + -1 * (1 + -1 * 2), ORundef, AppUndef_, 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') =*) Generate.generate tacis (pt,[],p);

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

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

if istate2str (get_istate pt p) (*                <>                 <>                 <>                 <>                     ^^^^^^^^^^^^^*)

(*REP*) = "Pstate ([\"\n(e_e, 1 + -1 * 2 + x = 0)\",\"\n(v_v, x)\"], [R,L,R,L,R,L,R], e_rls, SOMEe_e, \nx = 0 + -1 * (1 + -1 * 2), ORundef, AppUndef_, 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 (Step 1); refFormula 1 (get_pos 1 1);

(*11*)  fetchProposedTactic 1;

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

 autoCalculate 1 (Step 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) = pt_extract (pt, ip);

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

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

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

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

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

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

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

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

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

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

(* (*default_print_depth 13*) get_calc 1;

   *)

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

 (*calc-head of subproblem*)

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

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

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

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

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

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

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

 (*solve-phase of the subproblem*)

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

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

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

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

 (*finish subproblem*)

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

 (*finish problem*)

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

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

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

 val p = get_pos 1 1;

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

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

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

 DEconstrCalcTree 1;

"--------- solve_linear as rootpbl 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) = 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 ";

DEconstrCalcTree 1;

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

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

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

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

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; show_pt pt;

(*

getTactic 1 ([1],Frm);

getTactic 1 ([1],Res);

initContext 1 Thy_ ([1],Res);

*)

 (*... returns calcChangedEvent with*)

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

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

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

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

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

 val p = get_pos 1 1;

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

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

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

 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 {env = NONE, fmz = (fm, ("Test", pblID, metID)), loc = (SOME (env, ctxt1), NONE), 

      cell = NONE, ctxt = ctxt2, meth,

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

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

      probl, branch = TransitiveB, origin, ostate = Incomplete, result}, []),

   ([], 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 ---";

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

 DEconstrCalcTree 1;

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

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

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

 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; (*2 lines, OK*)

 (*

 setNextTactic 1 (Rewrite_Set "Test_simplify"); (*--> "thy_isac_Test-rls-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; (*2 lines, OK*)

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

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

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

 autoCalculate 1 CompleteCalc;

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

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

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

 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 (Step 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) = 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";

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

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

 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", ["normalise","polynomial",

					    "univariate","equation"]));

 autoCalculate 1 (Step 1); fetchProposedTactic 1;

 setNextTactic 1 (Model_Problem );

 autoCalculate 1 (Step 1); fetchProposedTactic 1;

 setNextTactic 1 (Specify_Theory "PolyEq");

 autoCalculate 1 (Step 1); fetchProposedTactic 1;

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

				   "univariate","equation"]);

 autoCalculate 1 (Step 1); fetchProposedTactic 1;

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

 autoCalculate 1 (Step 1); fetchProposedTactic 1;

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

 autoCalculate 1 (Step 1); fetchProposedTactic 1;

 setNextTactic 1 (Rewrite ("all_left", num_str @{thm 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;

 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 ["normalise","polynomial",

				  "univariate","equation"]);

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

 DEconstrCalcTree 1;

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

 CalcTree

 [(["equality (x^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) (kestoreID2guh Pbl_ ["univariate","equation"]);

*)

 autoCalculate 1 (Step 1); 

 fetchProposedTactic 1;

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

 autoCalculate 1 (Step 1); 

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

initContext 1 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. . . . . . . matches (?a = ?b) (x ^ 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 Pbl_ ([],Pbl); CHANGED";

*)

initContext 1 Met_ ([],Pbl);

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

 "--------- 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 ["normalise","polynomial",

				 "univariate","equation"]);

 autoCalculate 1 (Step 1);

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

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

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

 fetchProposedTactic 1;

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

				 "univariate","equation"]);

 autoCalculate 1 (Step 1);

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

 fetchProposedTactic 1;

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

 autoCalculate 1 (Step 1);

 fetchProposedTactic 1;

 setNextTactic 1 (Apply_Method ["PolyEq","normalise_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","normalise_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";

 DEconstrCalcTree 1;

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

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

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

 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::real))", "solveFor x"],

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

		  Pbl, 

		  ("Test", 

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

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

val ((Nd (PblObj {env = NONE,

                  fmz = (fm, tpm),

                  loc = (SOME scrst_ctxt, NONE),

                  ctxt,

                  cell = NONE,

                  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 {env = NONE,

                  fmz = (fm, tpm),

                  loc = (SOME scrst_ctxt, NONE),

                  ctxt,

                  cell = NONE,

                  meth,

                  spec = ("e_domID", ["e_pblID"], ["e_metID"]),

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

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

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