(* test for sml/ME/mathengine.sml

   authors: Walther Neuper 2000, 2006

   (c) due to copyright terms

*)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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 = ProofContext.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 ptree";

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

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

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

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

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

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

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

(*=== inhibit exn 110718 ? =============================================================

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

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

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

"----------- 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 110718 =======================================================

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

"----------- 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 110628 ================================================

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

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

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

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

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

 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;