(* Title:  tests for Interpret/mathengine.sml

   Author: Walther Neuper 2000, 2006

   (c) due to copyright terms

theory Test_Some imports Build_Thydata begin 

ML {* KEStore_Elems.set_ref_thy @{theory};

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

ML_file "~~/test/Tools/isac/Interpret/mathengine.sml"

*)

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

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

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

"----------- change to parse ctxt -----------------------";

"----------- debugging setContext..pbl_ -----------------";

"----------- tryrefine ----------------------------------";

"---------- mini-subpbl isac-java 3992e3bd1948: initial <NEXT> ---------------";

"----------- fun step: Apply_Method without init_form ---";

"----------- fun step -----------------------------------";

"----------- fun autocalc -------------------------------";

"----------- fun autoCalculate --------------------------";

"----------- fun autoCalculate..CompleteCalc ------------";

"----------- search for Or_to_List ----------------------";

"----------- check thy in CalcTreeTEST ------------------";

"----------- identified error in fun getTactic, string_of_thmI ---------------";

"----------- improved fun getTactic for interSteps and numeral calculations --";

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

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

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

"----------- change to parse ctxt -----------------------";

"----------- change to parse ctxt -----------------------";

"----------- change to parse ctxt -----------------------";

"===== start calculation: from problem description (fmz) to origin";

val fmz = ["realTestGiven (((1+2)*4/3)^^^2)","realTestFind s"];

val (thyID, pblID, metID) =

  ("Test", ["calculate", "test"], ["Test", "test_calculate"]);

(*======= Isabelle2013-2 --> Isabelle2014: unclear, why this test ever run ========================

val (p,_,_,nxt,_,pt) = CalcTreeTEST [(fmz, (thyID, pblID, metID))];

"----- ";

(* call sequence: CalcTreeTEST 

                > nxt_specify_init_calc 

                > prep_ori

*)

val (thy, pbt) = (Thy_Info.get_theory thyID, (#ppc o get_pbt) pblID);

"----- in  prep_ori";

val ctxt = Proof_Context.init_global thy;

val ctopts = map (parseNEW ctxt) fmz;

val dts = map (split_dts o the) ctopts;

(*split_dts:

(term * term list) list

        formulas: e.g. ((1+2)*4/3)^^^2

 description: e.g. realTestGiven

*)

 prep_ori;

(* FROM

val it = fn:

   string list -> theory -> (string * (term * 'a)) list -> ori list

TO

val it = fn:

   string list -> theory -> (string * (term * 'a)) list -> (ori list * ctxt)

AND

FROM val oris = prep_ori...

TO   val (oris, _) = prep_ori...

*)

"----- insert ctxt in ctree";

(* datatype ppobj

FROM loc   : istate option * istate option,

TO   loc   : (istate * ctxt) option * (istate * ctxt) option,

e.g.

FROM val pt = Nd (PblObj

       {.., loc = (SOME (ScrState ([], [], NONE, Const ("empty", "'a"), Sundef, false)),

          NONE),

TO   val pt = Nd (PblObj

       {.., loc = 

        ((SOME (ScrState ([], [], NONE, Const ("empty", "'a"), Sundef, false)), ctxt),

          NONE),

*)

"===== interactive specification: from origin to specification (probl)";

val (p,_,_,nxt,_,pt) = me nxt p [1] pt; 

  (*nxt =("Add_Given", Model_Problem)*)

val (p,_,_,nxt,_,pt) = me nxt p [1] pt;

  (*nxt = ("Add_Find",Add_Find "realTestFind s") : string * tac*)

"----- ";

(* call sequence: me Model_Problem 

                > me ("Add_Given", Add_Given "realTestGiven (((1 + 2) * 4 / 3) ^^^ 2)")

                > locatetac tac

                > loc_specify_

                > specify          GET ctxt (stored in ctree)

                > specify_additem

                > appl_add

*)

"----- in appl_add";

(* FROM appl_add thy

   TO   appl_add ctxt

   FROM parse thy str

   TO   parseNEW ctxt str

*)

val (p,_,_,nxt,_,pt) = me nxt p [1] pt; 

  (*nxt = ("Specify_Theory",Specify_Theory "Test") : string * tac*)

val (p,_,_,nxt,_,pt) = me nxt p [1] pt; 

  (*nxt = ("Specify_Problem",Specify_Problem ["calculate","test"])*)

"===== end specify: from specification (probl) to guard (method)";

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

  (*nxt = ("Specify_Method",Specify_Method ("Test","test_calculate"))*)

"===== start interpretation: from guard to environment";

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

  (*nxt = ("Apply_Method",Apply_Method ("Test","test_calculate"))*)

"----- ";

(* call sequence: me ("Apply_Method",...

                > locatetac

                > loc_solve_

                > solve ("Apply_Method",...

*)

val ((_,tac), ptp) = (nxt, (pt, p));

locatetac tac (pt,p);

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

  val Appl m = applicable_in p pt m;

  member op = specsteps mI;

  loc_solve_ (mI,m) ptp;

    val (m, (pt, pos)) = ((mI,m), ptp);

    solve m (pt, pos);

      val ((_, m as Apply_Method' (mI, _, _, _)), (pt, (pos as (p,_)))) = 

        (m, (pt, pos));

      val {srls,...} = get_met mI;

      val PblObj{meth=itms,...} = get_obj I pt p;

      val thy' = get_obj g_domID pt p;

      val thy = assoc_thy thy';

      val (is as ScrState (env,_,_,_,_,_), ctxt, sc) = init_scrstate thy itms mI;

"----- go on in the calculation";

val (p,_,f,nxt,_,pt) = me nxt pos [1] pt;

  (*nxt = ("Calculate",Calculate "PLUS")*)

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

  (*nxt = ("Calculate",Calculate "TIMES")*)

"===== input a formula to be derived from previous istate";

"----- appendFormula TODO: first repair error";

  val cs = ((pt,p),[]);

  val ("ok", cs' as (_,_,(pt,p))) = step p cs;

  val ifo = (* encode "4^^^2" \<longrightarrow>*) "4^2";

(*

  val ("no derivation found", (_,_,(pt, p))) = inform cs' ((*encode*) ifo);

  here ^^^^^^^^^^^^^^^^^^^^^ should be "ok"

*)

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

(*nxt = ("Calculate",Calculate "DIVIDE")*)

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

(*nxt = ("Calculate",Calculate "POWER")*)

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

(*nxt = ("Check_Postcond",Check_Postcond ["calculate","test"])*)

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

(*nxt = ("End_Proof'",End_Proof')*)

if f = Form' (FormKF (~1,EdUndef,0,Nundef,"16")) then ()

else error "calculate.sml: script test_calculate changed behaviour";

"===== tactic Subproblem: from environment to origin";

"----- TODO";

======= Isabelle2013-2 --> Isabelle2014: unclear, why this test ever run ========================*)

"----------- debugging setContext..pbl_ -----------------";

"----------- debugging setContext..pbl_ -----------------";

"----------- debugging setContext..pbl_ -----------------";

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

val pos as (p,_) = ([],Pbl);

val guh = "pbl_equ_univ";

checkContext 1 pos guh;

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

val pp = par_pblobj pt p;

val keID = guh2kestoreID guh;

case context_pbl keID pt pp of (true,["univariate", "equation"],_,_,_)=>()

| _ => error "mathengine.sml: context_pbl .. pbl_equ_univ checked";

case get_obj g_spec pt p of (_, ["e_pblID"], _) => ()

| _ => error "mathengine.sml: context_pbl .. pbl still empty";

setContext 1 pos guh;

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

case get_obj g_spec pt p of (_, ["univariate", "equation"], _) => ()

| _ => error "mathengine.sml: context_pbl .. pbl set";

setContext 1 pos "met_eq_lin";

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

case get_obj g_spec pt p of (_,  _, ["LinEq", "solve_lineq_equation"]) => ()

| _ => error "mathengine.sml: context_pbl .. pbl set";

"----------- tryrefine ----------------------------------";

"----------- tryrefine ----------------------------------";

"----------- tryrefine ----------------------------------";

reset_states ();

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

	    "solveFor x", "solutions L"],

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

Iterator 1;

moveActiveRoot 1; autoCalculate 1 CompleteCalc;

refineProblem 1 ([1],Res) "pbl_equ_univ" 

(*gives "pbl_equ_univ_rat" correct*);

refineProblem 1 ([1],Res) (pblID2guh ["LINEAR","univariate","equation"])

(*gives "pbl_equ_univ_lin" incorrect*);

"---------- mini-subpbl isac-java 3992e3bd1948: initial <NEXT> ---------------";

"---------- mini-subpbl isac-java 3992e3bd1948: initial <NEXT> ---------------";

"---------- mini-subpbl isac-java 3992e3bd1948: initial <NEXT> ---------------";

reset_states ();

(*this is the exact sequence of input provided by isac-java 3992e3bd1948;

  Surrounding ML { * ... * } are omitted.

  The multiple calls suggest to replicate the CalcTree in the Dialogue.

*)

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; 

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

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

(*completeCalcHead*)autoCalculate 1 CompleteCalcHead; 

(*completeCalcHead*)getActiveFormula 1 ; 

(*completeCalcHead*)refFormula 1 ([],Met); 

refFormula 1 ([],Pbl); 

(*<REFFORMULA>  <CALCID> 1 </CALCID>  <CALCHEAD status = "correct"> *)

fetchProposedTactic 1; 

(*-> <STRINGLISTTACTIC name="Apply_Method">

       <STRINGLIST>

         <STRING> Test </STRING>

         <STRING> squ-equ-test-subpbl1 </STRING>

WAS PREVIOUSLY: <SYSERROR>  <CALCID> 1 </CALCID>  <ERROR> error in kernel </ERROR></SYSERROR>*)

"~~~~~ fun fetchProposedTactic, args:"; val (cI) = (1);

val ("ok", (tacis, _, _)) = step (get_pos cI 1) (get_calc cI)

val _= upd_tacis cI tacis

	       val (tac,_,_) = last_elem tacis;

(*fetchproposedtacticOK2xml cI tac (fetchErrorpatterns tac);

                                    fetchErrorpatterns tac

WAS PREVIOUSLY ERROR: app_py: not found: ["IsacKnowledge","KEStore","Rulesets","e_rls"]*)

"~~~~~ fun fetchErrorpatterns, args:"; val (tac) = (tac);

    val rlsID = "e_rls"

    val (part, thyID) = thy_containing_rls "Build_Thydata" rlsID;

if part = "IsacScripts" andalso thyID = "KEStore" then ()

else error "fetchErrorpatterns .. e_rls changed";

val Hrls {thy_rls = (_, rls), ...} = get_the [part, thyID, "Rulesets", rlsID];

(* WAS PREVIOUSLY ERROR app_py: not found: ["IsacKnowledge","KEStore","Rulesets","e_rls"]*)

case rls of

  Rls {id = "e_rls", ...} => ()

| _ => error "thy_containing_rls changed for e_rls"

"----------- fun step: Apply_Method without init_form ---";

"----------- fun step: Apply_Method without init_form ---";

"----------- fun step: Apply_Method without init_form ---";

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

val (dI',pI',mI') =

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

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

val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

"~~~~~ fun me, args:"; val (_,tac) = nxt;

val ("ok", (_, _, (pt, p))) = locatetac tac (pt,p);

"~~~~~ fun step, args:"; val (ip as (_,p_), ptp as (pt,p), tacis) = (p, (pt, e_pos'), []);

val pIopt = get_pblID (pt,ip);

ip = ([],Res) (*false*);

val SOME pI = pIopt;

member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p));

			                          (*^^^^^^^^: Apply_Method without init_form*)

"----------- fun step -----------------------------------";

"----------- fun step -----------------------------------";

"----------- fun step -----------------------------------";

val p = e_pos'; val c = []; 

val (p,_,f,nxt,_,pt) = 

    CalcTreeTEST 

        [(["functionTerm (x^^^2 + 1)", "integrateBy x", "antiDerivative FF"], 

          ("Integrate", ["integrate","function"], ["diff","integration"]))];

"----- step 1: returns tac = Model_Problem ---";

val (str, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);

"----- step 2: returns tac =  ---";

val (str, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);

"----- step 3: returns tac =  ---";

val (str, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);

"----- step 4: returns tac =  ---";

val (str, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);

"----- step 5: returns tac =  ---";

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

2002 stops here as well: TODO review actual arguments:

val (str, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);

"----- step 6: returns tac =  ---";

val (str, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);

"----- step 7: returns tac =  ---";

val (str, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);

"----- step 8: returns tac =  ---";

val (str, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);

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

"----------- fun autocalc -------------------------------";

"----------- fun autocalc -------------------------------";

"----------- fun autocalc -------------------------------";

val p = e_pos'; val c = []; 

val (p,_,f,nxt,_,pt) = 

    CalcTreeTEST 

        [(["functionTerm (x^^^2 + 1)", "integrateBy x", "antiDerivative FF"], 

          ("Integrate",["integrate","function"], ["diff","integration"]))];

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

modeling is skipped FIXME 

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

tracing "----- step 1 ---";

val (str, cut, (pt, p)) = autocalc [] p ((pt, e_pos'),[]) (Step 1); show_pt pt;

tracing "----- step 2 ---";

val (str, cut, (pt, p)) = autocalc [] p ((pt, e_pos'),[]) (Step 1); show_pt pt;

tracing "----- step 3 ---";

val (str, cut, (pt, p)) = autocalc [] p ((pt, e_pos'),[]) (Step 1); show_pt pt;

tracing "----- step 4 ---";

val (str, cut, (pt, p)) = autocalc [] p ((pt, e_pos'),[]) (Step 1); show_pt pt;

tracing "----- step 5 ---";

val (str, cut, (pt, p)) = autocalc [] p ((pt, e_pos'),[]) (Step 1); show_pt pt;

tracing "----- step 6 ---";

val (str, cut, (pt, p)) = autocalc [] p ((pt, e_pos'),[]) (Step 1); show_pt pt;

tracing "----- step 7 ---";

val (str, cut, (pt, p)) = autocalc [] p ((pt, e_pos'),[]) (Step 1); show_pt pt;

tracing "----- step 8 ---";

val (str, cut, (pt, p)) = autocalc [] p ((pt, e_pos'),[]) (Step 1); show_pt pt;

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

WN110628: Integration does not work, see Knowledge/integrate.sml

if str = "end-of-calculation" andalso 

   term2str (get_obj g_res pt (fst p)) = "c + x + 1 / 3 * x ^^^ 3" then ()

else error "mathengine.sml -- fun autocalc -- end";

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

"----------- fun autoCalculate -----------------------------------";

"----------- fun autoCalculate -----------------------------------";

"----------- fun autoCalculate -----------------------------------";

reset_states ();

CalcTree (*ATTENTION: encode_fmz ... unlike CalcTreeTEST*)

    [(["functionTerm (x^2 + 1)", "integrateBy x", "antiDerivative FF"],

      ("Integrate", ["integrate", "function"], ["diff", "integration"]))];

Iterator 1;

moveActiveRoot 1;

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

modeling is skipped FIXME 

see test/../interface -- solve_linear as rootpbl FE -- for OTHER expl:

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

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

 fetchProposedTactic 1;

 setNextTactic 1 (Add_Given "solveFor x");

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

 fetchProposedTactic 1;

 setNextTactic 1 (Add_Find "solutions L");

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

 fetchProposedTactic 1;

 setNextTactic 1 (Specify_Theory "Test");

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

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

autoCalculate 1 (Step 1); 

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

autoCalculate 1 (Step 1);

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

autoCalculate 1 (Step 1);

"----- step 3 ---";

autoCalculate 1 (Step 1);

"----- step 4 ---";

autoCalculate 1 (Step 1);

"----- step 5 ---";

autoCalculate 1 (Step 1);

"----- step 6 ---";

autoCalculate 1 (Step 1);

"----- step 7 ---";

autoCalculate 1 (Step 1);

"----- step 8 ---";

autoCalculate 1 (Step 1);

val (ptp as (_, p), _) = get_calc 1;

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

if term2str t = "c + x + 1 / 3 * x ^^^ 3" andalso p = ([], Res) then ()

else error "mathengine.sml -- fun autoCalculate -- end";

"----------- fun autoCalculate..CompleteCalc ------------";

"----------- fun autoCalculate..CompleteCalc ------------";

"----------- fun autoCalculate..CompleteCalc ------------";

 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 CompleteCalc; (*WAS <SYSERROR>..<ERROR> error in kernel </ERROR>*)*)

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

val pold = get_pos cI 1;

(*autocalc [] pold (get_calc cI) auto;  (*WAS Type unification failed

  Type error in application: incompatible operand type

  Operator:  solveFor :: real \<Rightarrow> una

  Operand:   x :: 'a *)*)

"~~~~~ fun autocalc, args:"; val (c, (pos as (_,p_)), ((pt,_), _), auto) 

                               = ([] : pos' list, pold, (get_calc cI), auto);

autoord auto > 3 andalso just_created (pt, pos); (*true*)

val ptp = all_modspec (pt, pos);

"TODO all_modspec: preconds for rootpbl";

(*all_solve auto c ptp; (*WAS Type unification failed...*)*)

"~~~~~ and all_solve, args:"; val (auto, c, (ptp as (pt, pos as (p,_)))) =

                                                                  (auto, c, ptp);

    val (_,_,mI) = get_obj g_spec pt p

    val ctxt = get_ctxt pt pos

    val (ttt, c', ptp) = nxt_solv (Apply_Method' (mI, NONE, e_istate, ctxt)) (e_istate, ctxt) ptp;

(* complete_solve auto (c @ c') ptp; (*WAS Type unification failed...*) pos = ([], Met)*)

"~~~~~ fun complete_solve, args:"; val (auto, c, (ptp as (_, p as (_,p_)))) =

                                                           (auto, (c @ c'), ptp);

p = ([], Res) (*false p = ([1], Frm)*);

member op = [Pbl,Met] p_ (*false*);

val (ttt, c', ptp') = nxt_solve_ ptp; (*ttt = Rewrite_Set "norm_equation"*)

(* complete_solve auto (c @ c') ptp'; (*WAS Type unification failed...*) pos = ([], Met)*)

"~~~~~ fun complete_solve, args:"; val (auto, c, (ptp as (_, p as (_,p_)))) =

                                                           (auto, (c @ c'), ptp');

p = ([], Res) (*false p = ([1], Res)*);

member op = [Pbl,Met] p_ (*false*);

val (ttt, c', ptp') = nxt_solve_ ptp; (*ttt = Rewrite_Set "Test_simplify"*)

(* complete_solve auto (c @ c') ptp'; (*WAS Type unification failed...*) pos = ([], Met)*)

"~~~~~ fun complete_solve, args:"; val (auto, c, (ptp as (_, p as (_,p_)))) =

                                                           (auto, (c @ c'), ptp');

p = ([], Res) (*false p = ([2], Res)*);

member op = [Pbl,Met] p_ (*false*);

val ((Subproblem _, tac_, (_, is))::_, c', ptp') = nxt_solve_ ptp;

autoord auto < 5 (*false*);

(* val ptp = all_modspec ptp' (*WAS Type unification failed...*)*)

"~~~~~ fun all_modspec, args:"; val (pt, pos as (p,_)) = (ptp');

    val (PblObj {fmz = (fmz_, _), origin = (pors, spec as (dI,pI,mI), hdl), ...}) = get_obj I pt p;

    val thy = assoc_thy dI;

	    val {ppc, ...} = get_met mI;

(*  val (mors, ctxt) = prep_ori fmz_ thy ppc; WAS Type unification failed because

val ctxt' = dI |> Thy_Info.get_theory |> Proof_Context.init_global;

(parseNEW ctxt' "x" |> the |> type_of) = TFree ("'a",[]); 

                                               ^^^^^ *)

(*vvv from:  | assod pt _ (Subproblem'...*)

    val (fmz_, vals) = oris2fmz_vals pors;

(**)

    val ctxt = dI |> Thy_Info.get_theory |> Proof_Context.init_global 

      |> declare_constraints' vals

(**)

(*^^^ from:  | assod pt _ (Subproblem'...*)

val [(1, [1], "#Given", dsc_eq, [equality]),

     (2, [1], "#Given", dsc_solvefor, [xxx]),

     (3, [1], "#Find", dsc_solutions, [x_i])] = pors;

if term2str xxx = "x" andalso type_of xxx = HOLogic.realT then () 

else error "autoCalculate..CompleteCalc: SubProblem broken 1";

    val pt = update_pblppc pt p (map (ori2Coritm ppc) pors);

	    val pt = update_metppc pt p (map (ori2Coritm ppc) pors);

	    val pt = update_spec pt p (dI,pI,mI);

    val pt = update_ctxt pt p ctxt;

"~~~~~ return to complete_solve, args:"; val (ptp) = (pt, (p,Met));

val (msg, c, (pt, p)) = complete_solve auto (c @ c') ptp;

if msg = "end-of-calculation" andalso c = [] andalso p = ([], Res) then ()

else error "autoCalculate..CompleteCalc: final result";

if terms2strs (get_assumptions_ pt p) = 

  ["matches (?a = ?b) (-1 + x = 0)", (*precond of submet*) 

   "x = 1",                          (*result of subpbl and rootpbl*)

   "precond_rootmet x"]              (*precond of rootmet*)

then () else error "autoCalculate..CompleteCalc: ctxt at final result";

"--------- search for Or_to_List ------------------------";

"--------- search for Or_to_List ------------------------";

"--------- search for Or_to_List ------------------------";

val fmz = ["equality (x^^^2 + 4*x + 5 = (2::real))", "solveFor x","solutions L"];

val (dI',pI',mI') = ("Isac", ["univariate","equation"], ["no_met"])

val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

val (p,_,f,nxt,_,pt) = me nxt p [] pt;

val (p,_,f,nxt,_,pt) = me nxt p [] pt;

val (p,_,f,nxt,_,pt) = me nxt p [] pt;

val (p,_,f,nxt,_,pt) = me nxt p [] pt;

val (p,_,f,nxt,_,pt) = me nxt p [] pt;

val (p,_,f,nxt,_,pt) = me nxt p [] pt;

val (p,_,f,nxt,_,pt) = me nxt p [] pt;

val (p,_,f,nxt,_,pt) = me nxt p [] pt;

val (p,_,f,nxt,_,pt) = me nxt p [] pt;

val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Subproblem"*)

val (p,_,f,nxt,_,pt) = me nxt p [] pt;

val (p,_,f,nxt,_,pt) = me nxt p [] pt;

val (p,_,f,nxt,_,pt) = me nxt p [] pt;

val (p,_,f,nxt,_,pt) = me nxt p [] pt;

val (p,_,f,nxt,_,pt) = me nxt p [] pt;

val (p,_,f,nxt,_,pt) = me nxt p [] pt;

val (p,_,f,nxt,_,pt) = me nxt p [] pt;

val (p,_,f,nxt,_,pt) = me nxt p [] pt;

val (p,_,f,nxt,_,pt) = me nxt p [] pt;

val (p,_,f,nxt,_,pt) = me nxt p [] pt;

"~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), (_:NEW(*remove*)), (pt:ctree)) = 

                            (nxt, p, [], pt);

val ("ok", (_, _, ptp))  = locatetac tac (pt,p)

val (pt, p) = ptp;

"~~~~~ fun step, args:"; val (((ip as (_,p_)):pos'), ((ptp as (pt,p), tacis):calcstate)) =

                          (p, ((pt, e_pos'),[]));

val pIopt = get_pblID (pt,ip);

ip = ([],Res); (*false*)

ip = p; (*false*)

member op = [Pbl,Met] p_; (*false*)

"~~~~~ fun nxt_solve_, args:"; val (ptp as (pt, pos as (p,p_))) = (pt,ip);

e_metID = get_obj g_metID pt (par_pblobj pt p); (*false*)

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

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

val (tac_,is,(t,_)) = next_tac (thy',srls) (pt,pos) sc is; (*WAS Empty_Tac_: tac_*)

case tac_ of Or_to_List' _ => ()

| _ => error "Or_to_List broken ?"

"----------- check thy in CalcTreeTEST ------------------";

"----------- check thy in CalcTreeTEST ------------------";

"----------- check thy in CalcTreeTEST ------------------";

"WN1109 with Inverse_Z_Transform.thy when starting tests with CalcTreeTEST \n" ^

"we got the message: ME_Isa: thy 'Build_Inverse_Z_Transform' not in system \n" ^

"Below there are the steps which found out the reason: \n" ^

"store_pbt mistakenly stored that theory.";

val ctxt = Proof_Context.init_global @{theory Isac};

val SOME t = parseNEW ctxt "filterExpression (X  = 3 / (z - 1/4 + -1/8 * (1/(z::real))))";

val SOME t = parseNEW ctxt "stepResponse (x[n::real]::bool)";

val fmz = ["filterExpression (X  = 3 / (z - 1/4 + -1/8 * (1/(z::real))))", 

  "stepResponse (x[n::real]::bool)"];

val (dI,pI,mI) = ("Isac", ["Inverse", "Z_Transform", "SignalProcessing"], 

  ["SignalProcessing","Z_Transform","Inverse"]);

val (p,_,fb,nxt,_,pt)  = CalcTreeTEST [(fmz, (dI,pI,mI))]; 

(*WAS ME_Isa: thy 'Build_Inverse_Z_Transform' not in system*)

"~~~~~ T fun CalcTreeTEST, args:"; val [(fmz, sp):fmz] = [(fmz, (dI,pI,mI))];

"~~~~~ fun nxt_specify_init_calc, args:"; val (fmz, (dI, pI, mI)) = (fmz, sp);

	      val thy = assoc_thy dI;

    mI = ["no_met"]; (*false*)

		      val (pI, (pors, pctxt), mI) = (pI, get_pbt pI |> #ppc |> prep_ori fmz thy, mI)

	      val {cas, ppc, thy=thy',...} = get_pbt pI; (*take dI from _refined_ pbl*)

	"tracing bottom up"; Context.theory_name thy' = "Build_Inverse_Z_Transform"; (*WAS true*)

      val dI = theory2theory' (maxthy thy thy');

"tracing bottom up"; dI = "Build_Inverse_Z_Transform"; (*WAS true*)

    cas = NONE; (*true*)

	      val hdl = pblterm dI pI;

        val (pt, _) = cappend_problem e_ctree [] (e_istate, pctxt) (fmz, (dI, pI, mI))

				  (pors, (dI, pI, mI), hdl)

        val pt = update_ctxt pt [] pctxt;

"~~~~~ fun nxt_specif, args:"; val ((tac as Model_Problem), (pt, pos as (p,p_))) = (Model_Problem, (pt, ([], Pbl)));

      val PblObj {origin = (oris, ospec, _), probl, spec, ctxt, ...} = get_obj I pt p;

"tracing bottom up"; #1(ospec) = "Build_Inverse_Z_Transform"; (*WAS true*)

"~~~~~ fun some_spec, args:"; val ((odI, opI, omI), (dI, pI, mI)) = (ospec, spec);

dI = e_domID; (*true*)

odI = "Build_Inverse_Z_Transform"; (*true*)

dI = "e_domID"; (*true*)

"~~~~~ after fun some_spec:";

      val (dI, pI, mI) = some_spec ospec spec;

"tracing bottom up"; dI = "Build_Inverse_Z_Transform"; (*WAS true*)

      val thy = assoc_thy dI; (*caused ME_Isa: thy 'Build_Inverse_Z_Transform' not in system*)

"----------- identified error in fun getTactic, string_of_thmI ---------------";

"----------- identified error in fun getTactic, string_of_thmI ---------------";

"----------- identified error in fun getTactic, string_of_thmI ---------------";

reset_states ();

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

  ("Test",["sqroot-test","univariate","equation","test"],["Test","squ-equ-test-subpbl1"]))];

moveActiveRoot 1;

autoCalculate 1 CompleteCalcHead;

autoCalculate 1 (Step 1);

autoCalculate 1 (Step 1);

autoCalculate 1 (Step 1);

getTactic 1 ([1],Frm); (*<RULESET> norm_equation </RULESET>*)

interSteps 1 ([1],Res);

"~~~~~ fun interSteps, args:"; val (cI, ip) = (1, ([1],Res));

val ((pt,p), tacis) = get_calc cI;

(not o is_interpos) ip = false;

val ip' = lev_pred' pt ip;

"~~~~~ fun detailstep, args:"; val (pt, (pos as (p,p_):pos')) = (pt, ip);

(*         ^^^^^^^^^ not in test/../ *)

    val nd = get_nd pt p

    val cn = children nd;

null cn = false;

(is_rewset o (get_obj g_tac nd)) [(*root of nd*)] = true;

"~~~~~ fun detailrls, args:"; val (pt, (pos as (p,p_):pos')) = (pt, pos);

(*         ^^^^^^^^^ only once in test/../solve.sml*)

    val t = get_obj g_form pt p

	  val tac = get_obj g_tac pt p

	  val rls = (assoc_rls o rls_of) tac

    val ctxt = get_ctxt pt pos

(*rls = Rls {calc = [], erls = ...*)

          val is = init_istate tac t

	        (*TODO.WN060602 ScrState (["(t_, Problem (Isac,[equation,univar]))"]

				    is wrong for simpl, but working ?!? *)

	        val tac_ = Apply_Method' (e_metID(*WN0402: see generate1 !?!*), SOME t, is, ctxt)

	        val pos' = ((lev_on o lev_dn) p, Frm)

	        val thy = assoc_thy "Isac"

	        val (_,_,_,pt') = (*implicit Take*)generate1 thy tac_ (is, ctxt) pos' pt;

	        (*val (_,_,(pt'',_)) = *)complete_solve CompleteSubpbl [] (pt',pos');

	        (*                   ^^^^^^^^^^^^^^ in test/../mathengine.sml*)

	        (* in pt'': tac = Rewrite ("rnorm_equation_add", "Test.rnorm_equation_add")},

                                                           ^^^^^^^^^^^^^^^^^^^^^^^^^^^*)

"~~~~~ fun complete_solve, args:"; val (auto, c, (ptp as (_, p as (_,p_)): ctree * pos')) =

  (CompleteSubpbl, [], (pt',pos'));

p = ([], Res) = false;

member op = [Pbl,Met] p_ = false;

val (_, c', ptp') = nxt_solve_ ptp;

(* in pt': tac = Rewrite ("rnorm_equation_add", "Test.rnorm_equation_add")},

                                                ^^^^^^^^^^^^^^^^^^^^^^^^^^^*)

"~~~~~ fun nxt_solve_, args:"; val ((ptp as (pt, pos as (p,p_)))) = (ptp);

e_metID = get_obj g_metID pt (par_pblobj pt p) = false;

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

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

	        val (tac_,is,(t,_)) = next_tac (thy',srls) (pt,pos) sc is;

(*tac_ = Rewrite' (..., ("rnorm_equation_add", "Test.rnorm_equation_add"), ...) !!!!!!!!!!!!!!!!*)

"~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt, pos as (p, _)):ctree * pos'), 

  (sc as Prog (h $ body)), (ScrState (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is);

l = [] = false;

nstep_up thy ptp sc E l Skip_ a v (*--> Appy (Rewrite' (.., (.., "Test.rnorm_equation_add"), ...)

  BUT WE FIND IN THE CODE ABOVE IN next_tac:*)

;

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

if string_of_thmI @{thm rnorm_equation_add} = "~ ?b =!= 0 ==> (?a = ?b) = (?a + - 1 * ?b = 0)"

then () else error "string_of_thmI changed";

if string_of_thm @{thm rnorm_equation_add} = "~ ?b =!= 0 ==> (?a = ?b) = (?a + - 1 * ?b = 0)"

then () else error "string_of_thm changed";

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

;

(*SEARCH FOR THE ERROR WENT DOWN TO THE END OF THIS TEST, AND THEN UP TO HERE AGAIN*)

"~~~~~ fun nxt_solv, args:"; val (tac_, is, (pt, pos as (p,p_))) = (tac_, is, ptp);

        val pos =

          case pos of

		        (p, Met) => ((lev_on o lev_dn) p, Frm)(*begin script*)

		      | (p, Res) => (lev_on p,Res) (*somewhere in script*)

		      | _ => pos;

generate1 (assoc_thy "Isac") tac_ is pos pt;

(* tac = Rewrite ("rnorm_equation_add", "Test.rnorm_equation_add")},

                                        ^^^^^^^^^^^^^^^^^^^^^^^^^^^*)

"~~~~~ fun generate1, args:"; val (thy, (Rewrite' (thy',ord',rls',pa,thm',f,(f',asm))), 

  (is, ctxt), (p,p_), pt) = ((assoc_thy "Isac"), tac_, is, pos, pt);

        val (pt,c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f

          (Rewrite thm') (f',asm) Complete;

(* in pt: tac = Rewrite ("rnorm_equation_add", "Test.rnorm_equation_add")},

                                               ^^^^^^^^^^^^^^^^^^^^^^^^^^^*)

"~~~~~ fun cappend_atomic, args:"; val (pt, p, ist_res, f, r, f', s) = 

  (pt, p, (is, insert_assumptions asm ctxt), f, (Rewrite thm'), (f',asm), Complete);

existpt p pt andalso is_empty_tac (get_obj g_tac pt p) = false;

apfst (append_atomic p ist_res f r f' s) (cut_tree pt (p,Frm));

apfst : ('a -> 'b) -> 'a * 'c -> 'b * 'c;

(append_atomic p ist_res f r f' s) : ctree -> ctree;

;

(* HERE THE ERROR OCCURED IN THE FIRST APPROACH

  getTactic 1 ([1,1],Frm); <ERROR> syserror in getTactic </ERROR>  <<<<<=========================*)

"~~~~~ fun getTactic, args:"; val (cI, (p:pos')) = (1, ([1,1],Frm));

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

val (form, tac, asms) = pt_extract (pt, p)

val SOME ta = tac;

"~~~~~ fun gettacticOK2xml, args:"; val ((cI:calcID), tac) = (cI, ta);

val i = 2;

"~~~~~ fun tac2xml, args:"; val (j, (Rewrite thm')) = (i, tac);

"~~~~~ fun thm'2xml, args:"; val (j, ((ID, form) : thm'')) = ((j+i), thm');

ID = "rnorm_equation_add";

@{thm rnorm_equation_add};

(term2str o Thm.prop_of) form = "~ ?b =!= 0 ==> (?a = ?b) = (?a + -1 * ?b = 0)"

  (*?!? should be "\<not> ?b =!= 0 \<Longrightarrow> (?a = ?b) = (?a + -1 * ?b = 0)"*)

(*thmstr2xml (j+i) form;

ERROR Undeclared constant: "Test.rnorm_equation_add" ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)

;

show_pt pt;

(*[

(([], Frm), solve (x + 1 = 2, x)),

(([1], Frm), x + 1 = 2),

(([1,1], Frm), x + 1 = 2),

(([1,1], Res), x + 1 + -1 * 2 = 0),

(([1], Res), x + 1 + -1 * 2 = 0),

(([2], Res), -1 + x = 0)]

pt;   --> tac = Rewrite ("rnorm_equation_add", "Test.rnorm_equation_add")*)

"----------- improved fun getTactic for interSteps and numeral calculations --";

"----------- improved fun getTactic for interSteps and numeral calculations --";

"----------- improved fun getTactic for interSteps and numeral calculations --";

reset_states (); val cI = 1;

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

  ("Test",["sqroot-test","univariate","equation","test"],["Test","squ-equ-test-subpbl1"]))];

moveActiveRoot 1;

autoCalculate 1 CompleteCalcHead;

autoCalculate 1 (Step 1);

    val cs = get_calc cI             (* we improve from the calcstate here [*] *);

    val pos as (_,p_) = get_pos cI 1 (* we improve from the calcstate here [*] *);

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

interSteps 1 ([1],Res); (* already done by appendFormula, now showed to frontend *)

getTactic 1 ([1,1], Res); 

  (*<ID> sym_#add_Float ((~3,0), (0,0)) __ ((4,0), (0,0)) </ID>  <<<<<================== to improve

  <ISA> 1 + x = -3 + (4 + x) </ISA>*)

val ((pt''',p'''), tacis''') = get_calc cI;

show_pt pt'''

(*[

(([], Frm), solve (x + 1 = 2, x)),

(([1], Frm), x + 1 = 2),

(([1,1], Frm), x + 1 = 2),

(([1,1], Res), 1 + x = 2),

(([1,2], Res), -3 + (4 + x) = 2),

(([1,3], Res), -3 + (x + 4) = 2),

(([1,4], Res), x + 4 + -3 = 2),

(([1], Res), x + 4 + -3 = 2)]*)

;

"~~~~~ fun appendFormula', args:"; val (cI, ifo) = (1, "x + 4 + -3 = 2");

(*  val cs = get_calc cI             (* we improve from the calcstate here [*] *);

    val pos as (_,p_) = get_pos cI 1 (* we improve from the calcstate here [*] *);*)

val ("ok", cs') = step pos cs;

(*val ("ok", (_, c, ptp as (_,p))) = *)inform cs' (encode ifo);

"~~~~~ fun inform, args:"; val (cs as (_, _, ptp as (pt, pos as (p, p_))), istr) =

  (cs', (encode ifo));

val SOME f_in = parse (assoc_thy "Isac") istr

	      val f_in = Thm.term_of f_in

	      val f_succ = get_curr_formula (pt, pos);

f_succ = f_in  = false;

val NONE = cas_input f_in 

			          val pos_pred = lev_back' pos

			          (* f_pred ---"step pos cs"---> f_succ in appendFormula *)

			          val f_pred = get_curr_formula (pt, pos_pred);

			          (*val msg_calcstate' = *)compare_step ([], [], (pt, pos_pred)) f_in (*<<=====*);

"~~~~~ fun compare_step, args:"; val (((tacis, c, ptp as (pt, pos as (p,p_)))), ifo) = 

  (([], [], (pt, pos_pred)), f_in);

    val fo =

      case p_ of

        Frm => get_obj g_form pt p

			| Res => (fst o (get_obj g_result pt)) p

			| _ => e_term (*on PblObj is fo <> ifo*);

	  val {nrls, ...} = get_met (get_obj g_metID pt (par_pblobj pt p))

	  val {rew_ord, erls, rules, ...} = rep_rls nrls;

	  (*val (found, der) = *)concat_deriv rew_ord erls rules fo ifo; (*<---------------*)

"~~~~~ fun concat_deriv, args:"; val (rew_ord, erls, rules, fo, ifo) =

  (rew_ord, erls, rules, fo, ifo);

    fun derivat ([]:(term * rule * (term * term list)) list) = e_term

      | derivat dt = (#1 o #3 o last_elem) dt

    fun equal (_,_,(t1, _)) (_,_,(t2, _)) = t1=t2

    (*val  fod = *)make_deriv (Isac"") erls rules (snd rew_ord) NONE  fo;

    (*val ifod = *)make_deriv (Isac"") erls rules (snd rew_ord) NONE ifo;