(* Title:  tests for MathEngine/mathengine-stateless.sml

   Author: Walther Neuper 2000, 2006, 2020

   (c) due to copyright terms

theory Test_Some imports Build_Thydata begin 

ML {* Know_Store.set_ref_thy @{theory};

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

ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Interpret/mathengine.sml"

*)

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

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

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

"----------- change to TermC.parse ctxt -----------------------";

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

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

"----------- check thy in Test_Code.init_calc @{context} ------------------";

"----------- identified error in fun getTactic, ThmC.string_of_thm ---------------";

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

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

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

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

"----------- change to TermC.parse ctxt -----------------------";

"----------- change to TermC.parse ctxt -----------------------";

"----------- change to TermC.parse ctxt -----------------------";

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

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

val (thyID, pblID, metID) =

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

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

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

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

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

States.reset ();

CalcTree @{context} [(["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) (Ptool.pblID2guh @{context} ["LINEAR", "univariate", "equation"])

(*gives "pbl_equ_univ_lin" incorrect*);

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

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

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

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

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

val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(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;

"~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ continue AFTER previous step 'me' ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~";

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

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

val ("ok", (_, _, ptp))  = Step.by_tactic tac (pt,p)

val (pt, p) = ptp;

"~~~~~ fun Step.do_next, args:"; val (((ip as (_,p_)):pos'), ((ptp as (pt,p), tacis):Calc.state_pre)) =

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

val pIopt = get_pblID (pt,ip);

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

ip = p; (*false*)

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

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

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

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

val ((ist, ctxt), sc) = resume_prog (p,p_) pt;

val Next_Step (istate, ctxt, tac) = LI.find_next_step sc (pt,pos) ist ctxt; (*WAS Empty_Tac_: tac_*)

case tac of Or_to_List' _ => ()

| _ => error "Or_to_List broken ?"

"----------- check thy in Test_Code.init_calc @{context} ------------------";

"----------- check thy in Test_Code.init_calc @{context} ------------------";

"----------- check thy in Test_Code.init_calc @{context} ------------------";

"WN1109 with Inverse_Z_Transform.thy when starting tests with Test_Code.init_calc @{context} \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_Knowledge};

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))))", "boundVariable z",

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

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

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

val (p,_,fb,nxt,_,pt)  = Test_Code.init_calc @{context} [(fmz, (dI,pI,mI))]; 

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

"~~~~~ fun Test_Code.init_calc @{context} , args:"; val [(fmz, sp):Formalise.T] = [(fmz, (dI,pI,mI))];

    (*val ((pt, p), tacis) =*) 

Step_Specify.nxt_specify_init_calc ctxt (fmz, sp);

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

	    (*val (_, hdl, (dI, pI, mI), pors, pctxt) =*) 

Step_Specify.initialise ctxt (fmz, (dI, pI, mI));

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

	    val thy = ThyC.get_theory dI

	    val ctxt = Proof_Context.init_global thy;

        (*if*) mI = ["no_met"](*else*);

	         val (pors, pctxt) = Problem.from_store ctxt pI |> #model |> O_Model.init_PIDE thy fmz;

	      val {cas, model, thy=thy',...} = Problem.from_store ctxt pI; (*take dI from _refined_ pbl*)

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

      val dI = Context.theory_name (ThyC.parent_of 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 [] (Istate.empty, pctxt) (fmz, (dI, pI, mI))

				  (pors, (dI, pI, mI), hdl, ContextC.empty)

;

"~~~~~ fun Step_Specify.by_tactic_input, 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 References.select_input, args:"; val ((odI, opI, omI), (dI, pI, mI)) = (ospec, spec);

dI = ThyC.id_empty; (*true*)

odI = "Build_Inverse_Z_Transform"; (*true*)

dI = ThyC.id_empty; (*true*)

"~~~~~ after fun References.select_input:";

      val (dI, pI, mI) = References.select_input ospec spec;

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

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

"----------- identified error in fun getTactic, ThmC.string_of_thm ---------------";

"----------- identified error in fun getTactic, ThmC.string_of_thm ---------------";

"----------- identified error in fun getTactic, ThmC.string_of_thm ---------------";

States.reset ();

CalcTree @{context} [(["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 (Steps 1);

autoCalculate 1 (Steps 1);

autoCalculate 1 (Steps 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) = States.get_calc cI;

(not o is_interpos) ip = false;

val ip' = lev_pred' pt ip;

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

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

(*         \<up> \<up> \<up> only once in test/../solve.sml*)

    val t = get_obj g_form pt p

	  val tac = get_obj g_tac pt p

    val ctxt = get_ctxt pt pos

	  val rls = ((get_rls ctxt) o rls_of) tac

    val ctxt = get_ctxt pt pos

(*rls = Rule_Set.Repeat {calc = [], asm_rls = ...*)

          val is = Istate.init_detail ctxt tac t

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

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

	        val tac_ = Apply_Method' (MethodC.id_empty(*WN0402: see Step.add !?!*), SOME t, is, ctxt)

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

	        val thy = ThyC.get_theory "Isac_Knowledge"

	        val (_,_,_,pt') = (*implicit Take*)Step.add tac_ (is, ctxt) (pt, pos');

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

	        (*                   \<up> \<up> \<up> \<up> ^^ in test/../mathengine.sml*)

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

                                                           \<up> \<up> \<up> \<up> \<up> \<up> \<up> \<up>  \<up> *)

"~~~~~ 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')) = Step_Solve.do_next ptp;

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

                                                \<up> \<up> \<up> \<up> \<up> \<up> \<up> \<up>  \<up> *)

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

MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) = false;

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

	        val ((ist, ctxt), sc) = resume_prog (p,p_) pt;

	        val Next_Step (is, ctxt, tac_) = LI.find_next_step sc (pt,pos) ist ctxt;

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

(*----- outcommented during cleanup of args in lucas-interpreter.sml ------------------------\\* )

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

  (sc as Prog (h $ body)), (Pstate (ist as (E,l,rls,a,v,s,b)), ctxt)) = ((thy',prog_rls), (pt,pos), sc, is);

l = [] = false;

go_scan_up thy ptp sc ist true (*--> Accept_Tac (Rewrite' (.., (.., "Test.rnorm_equation_add"), ...)

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

;

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

if ThmC.string_of_thm @{thm rnorm_equation_add} =  "\<not> ?b =!= 0 \<Longrightarrow> (?a = ?b) = (?a + - 1 * ?b = 0)"

then () else error "ThmC.string_of_thm changed";

if ThmC.string_of_thm @{thm rnorm_equation_add} =  "\<not> ?b =!= 0 \<Longrightarrow> (?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 begin_end_prog, 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;

Step.add tac_ is pos pt;

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

                                        \<up> \<up> \<up> \<up> \<up> \<up> \<up> \<up>  \<up> *)

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

  (is, ctxt), (p,p_), pt) = ((ThyC.get_theory "Isac_Knowledge"), tac_, is, pos, pt);

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

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

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

                                               \<up> \<up> \<up> \<up> \<up> \<up> \<up> \<up>  \<up> *)

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

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

existpt p pt andalso Tactic.is_empty (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,_),_) = States.get_calc cI

val (form, tac, asms) = ME_Misc.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};

(UnparseC.term 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" \<up> \<up> \<up> \<up> \<up> \<up> \<up> \<up> \<up> \<up> \<up> \<up> \<up> \<up> ^*)

;

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

( *----- outcommented during cleanup of args in lucas-interpreter.sml ------------------------//*)

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

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

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

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

States.reset (); val cI = 1;

CalcTree @{context} [(["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 (Steps 1);

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

    val pos as (_,p_) = States.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''') = States.get_calc cI;

Test_Tool.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 = States.get_calc cI             (* we improve from the calcstate here [*] *);

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

val ("ok", cs' as (_, _, ptp')) = Step.do_next pos cs;

(*val ("ok", (_, c, ptp as (_,p))) = *)Step_Solve.by_term ptp' (encode ifo);

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

  (cs', (encode ifo));

val SOME f_in = TermC.parseNEW (get_ctxt pt pos) istr

	      val f_succ = get_curr_formula (pt, pos);

f_succ = f_in  = false;

val NONE = CAS_Cmd.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

			| _ => TermC.empty (*on PblObj is fo <> ifo*);

	  val {rew_rls, ...} = MethodC.from_store ctxt (get_obj g_metID pt (par_pblobj pt p))

	  val {rew_ord, asm_rls, rules, ...} = Rule_Set.rep rew_rls;

	  (*val (found, der) = *)Derive.steps ctxt rew_ord asm_rls rules fo ifo; (*<---------------*)

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

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

    fun derivat ([]:(term * rule * (term * term list)) list) = TermC.empty

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

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

    (*val  fod = *)Derive.do_one ctxt asm_rls rules (snd rew_ord) NONE  fo;

    (*val ifod = *)Derive.do_one ctxt asm_rls rules (snd rew_ord) NONE ifo;