(* Title:  All tests on isac (some outcommented since Isabelle2002-->2009-2)

   Author: Walther Neuper 101001

   (c) copyright due to license terms.

   Isac's tests are organised parallel to sources: 

     $ISABELLE_ISAC_TEST has same directory structure as $ISABELLE_ISAC

   plus

     $ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS

     $ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl: the Lucas-Interpreter's core functionality

Note, that only the first error in a file is shown here.

*)

section \<open>Notes on running tests\<close>

subsection \<open>Switch between running tests and updating code\<close>

text \<open>

  Isac encapsulates code as much as possible in structures without open.

  This policy conflicts with those tests, which go into functions to details

  not declared in the signatures.

\<close>

subsection \<open>Decide between running Test_Isac_Short.thy and Test_Isac.thy\<close>

text \<open>

  Some tests raise exception Size raised (line 171 of "./basis/LibrarySupport.sml")

  if run in x86_64_32 mode of Poly/ML 5.8 (which is set as default).

  This exception can be avoided by ML_system_64 = "true" in ~/.isabelle/isabisac/etc/preferences.

  A model is in the repository at ~~/etc/preferences.

  These preferences have drawbacks, however:

  * they claim more memory such that Isabelle instances canNOT run in parallel.

  * they do NOT reach Build_Isac.thy hanging in Build_Thydata.thy, see there.

  So default for Build_Isac.thy and for general testing is Test_Isac_Short.thy is x86_64_32 mode.

  From time to time full testing in Test_Isac.thy is recommended. For that purpose

  * set ML_system_64 = "true" in ~/.isabelle/isabisac/etc/preferences.

\\******************* don't forget to re-set defaults BEFORE updating code *******************//

    Note that Isabelle/jEdit re-generates the preferences file on shutdown, thus always use

    ***************** $ gedit ~/.isabelle/isabisac/etc/preferences &

\<close>

section \<open>Run the tests\<close>

text \<open>

* say "OK" to the popup asking for theories to be loaded

* watch the <Theories> window for errors in the "imports" below

\<close>

theory Test_Isac_Short

  imports Isac.Build_Isac (* note that imports are WITHOUT open struct ..*)

  (* in case of ERROR Bad theory import "Draft.Thy_All"..., open each theory one by one

     and find out, which ML_file or *.thy causes an error (might be ONLY one).

     Also backup files (#* ) recognised by jEdit cause this trouble                    *)

(*/---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------\*)

(*  "$ISABELLE_ISAC_TEST/ADDTESTS/accumulate-val/Thy_All"(*but ok in editor*)*)

(**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/accumulate-val/Lucas_Interpreter"

(**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/Ctxt"

(**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/test-depend/Build_Test"

(**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/All_Ctxt"

(**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/Test_Units"

(**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/course/phst11/T1_Basics"

(**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/course/phst11/T2_Rewriting"

(**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/course/phst11/T3_MathEngine"

(**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/file-depend/BuildC_Test"

(**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/session-get_theory/Foo"

(*"ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform"

   ADDTESTS/------------------------------------------- see end of tests *)

(*/~~~ these work directly from Pure, but create problems here ..

  "$ISABELLE_ISAC_TEST/Pure/Isar/Keyword_ISAC.thy"           (* Malformed theory import, "keywords" ?!? *)

  "$ISABELLE_ISAC_TEST/Pure/Isar/Test_Parse_Isac.thy"        (* Malformed theory import, "keywords" ?!? *)

  "$ISABELLE_ISAC_TEST/Pure/Isar/Test_Parsers_Cookbook.thy"  (* Malformed theory import             ?!? *)

  "$ISABELLE_ISAC_TEST/Pure/Isar/Theory_Commands"            (* Duplicate outer syntax command "ISAC"   *)

  "$ISABELLE_ISAC_TEST/Pure/Isar/Downto_Synchronized"        (* re-defines / breaks structures      !!! *)

  \~~~ .. these work independently, but create problems here *)

(**)"$ISABELLE_ISAC_TEST/Pure/Isar/Test_Parsers"

(**)"$ISABELLE_ISAC_TEST/HOL/Tools/Sledgehammer/Try_Sledgehammer"

(*/---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------\*)

  "$ISABELLE_ISAC_TEST/Tools/isac/Specify/refine"        (* setup for refine.sml   *)

  "$ISABELLE_ISAC_TEST/Tools/isac/ProgLang/calculate"    (* setup for evaluate.sml *)

  "$ISABELLE_ISAC_TEST/Tools/isac/Knowledge/integrate"   (* setup for integrate.sml*)

(** )

(*\---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------/*)

(*"$ISABELLE_ISAC/Knowledge/GCD_Poly_OLD" (*not imported by Isac.thy*)        Test_Isac_Short*)

(*"$ISABELLE_ISAC/Knowledge/GCD_Poly_FP"  (*not imported by Isac.thy*)        Test_Isac_Short*)

(*\---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------/*)

( **)

  "$ISABELLE_ISAC_TEST/Tools/isac/BridgeJEdit/Test_VSCode_Example"

begin

declare [[ML_print_depth = 20]]

ML \<open>open ML_System\<close>

ML \<open>

  open Kernel;

  open Math_Engine;

  open Test_Code;              CalcTreeTEST;

  open LItool;                 arguments_from_model;

  open Sub_Problem;

  open Fetch_Tacs;

  open Step

  open Env;

  open LI;                     scan_dn;

  open Istate;

  open Error_Pattern;

  open Error_Pattern_Def;

  open Specification;

  open Ctree;                  append_problem;

  open Pos;

  open Program;

  open Prog_Tac;

  open Tactical;

  open Prog_Expr;

  open Auto_Prog;              rule2stac;

  open Input_Descript;

  open Specify;

  open Specify;

  open Step_Specify;

  open Step_Solve;

  open Step;

  open Solve;                  (* NONE *)

  open ContextC;               transfer_asms_from_to;

  open Tactic;                 (* NONE *)

  open I_Model;

  open O_Model;

  open P_Model;                (* NONE *)

  open Rewrite;

  open Eval;                   get_pair;

  open TermC;                  atomt;

  open Rule;

  open Rule_Set;               Sequence;

  open Eval_Def

  open ThyC

  open ThmC_Def

  open ThmC

  open Rewrite_Ord

  open UnparseC

\<close>

ML \<open>

"~~~~~ fun xxx , args:"; val () = ();

"~~~~~ and xxx , args:"; val () = ();

"~~~~~ from fun xxx \<longrightarrow>fun yyy \<longrightarrow>fun zzz , return:"; val () = ();

(*if*) (*then*); (*else*);   (*case*) (*of*);  (*return value*); (*in*) (*end*);

"xx"

^ "xxx"   (*+*) (*+++*) (*!for return!*) (*isa*) (*REP*) (**)

\<close> ML \<open> (*//---------------- adhoc inserted ------------------------------------------------\\*)

\<close> ML \<open>

\<close> ML \<open> (*\\---------------- adhoc inserted ------------------------------------------------//*)

\<close>

ML \<open>

\<close> ML \<open>

\<close> ML \<open>

\<close> ML \<open>

\<close> ML \<open>

\<close>

ML \<open>

  KEStore_Elems.set_ref_thy @{theory};

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

\<close>

section \<open>trials with Isabelle's functions\<close>

  ML \<open>"%%%%%%%%%%%%%%%%% start Isabelle %%%%%%%%%%%%%%%%%%%%%%%";\<close>

  ML_file "$ISABELLE_ISAC_TEST/Pure/General/alist.ML"

  ML_file "$ISABELLE_ISAC_TEST/Pure/General/basics.ML"

  ML_file "$ISABELLE_ISAC_TEST/Pure/General/scan.ML"

  ML_file "$ISABELLE_ISAC_TEST/Pure/PIDE/xml.ML"

  ML \<open>"%%%%%%%%%%%%%%%%% end Isabelle %%%%%%%%%%%%%%%%%%%%%%%%%";\<close>

section \<open>test ML Code of isac\<close>

subsection \<open>basic code first\<close>

  ML \<open>"%%%%%%%%%%%%%%%%% start ProgLang.thy %%%%%%%%%%%%%%%%%%%";\<close>

  ML_file "BaseDefinitions/base-definitions.sml"

  ML_file "BaseDefinitions/libraryC.sml"

  ML_file "BaseDefinitions/rule-def.sml"

  ML_file "BaseDefinitions/eval-def.sml"

  ML_file "BaseDefinitions/rewrite-order.sml"

  ML_file "BaseDefinitions/theoryC.sml"

  ML_file "BaseDefinitions/rule.sml"

  ML_file "BaseDefinitions/thmC-def.sml"

  ML_file "BaseDefinitions/error-fill-def.sml"

  ML_file "BaseDefinitions/rule-set.sml"

  ML_file "BaseDefinitions/check-unique.sml"

(*called by Know_Store..*)

  ML_file "BaseDefinitions/calcelems.sml"

  ML_file "BaseDefinitions/termC.sml"

  ML_file "BaseDefinitions/substitution.sml"

  ML_file "BaseDefinitions/contextC.sml" (*!!!!! sometimes evaluates if separated into ML blocks*)

  ML_file "BaseDefinitions/environment.sml"

(**)ML_file "BaseDefinitions/kestore.sml"(*setup in ADDTEST/accumulate-val/lucas_interpreter.sml*)

(*---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------

  ---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------*)

  ML_file "ProgLang/calculate.sml"

  ML_file "ProgLang/evaluate.sml"       (* requires setup from calculate.thy                    *)

  ML_file "ProgLang/listC.sml"

  ML_file "ProgLang/prog_expr.sml"

  ML_file "ProgLang/program.sml"

  ML_file "ProgLang/prog_tac.sml"

  ML_file "ProgLang/tactical.sml"

  ML_file "ProgLang/auto_prog.sml"

(*---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------

  ---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------*)

subsection \<open>basic functionality on simple example first\<close>

  ML_file "Minisubpbl/000-comments.sml"

  ML_file "Minisubpbl/100-init-rootpbl.sml"

  ML_file "Minisubpbl/150-add-given.sml"

  ML_file "Minisubpbl/200-start-method-NEXT_STEP.sml"

  ML_file "Minisubpbl/200-start-method.sml"

  ML_file "Minisubpbl/250-Rewrite_Set-from-method.sml"

  ML_file "Minisubpbl/300-init-subpbl-NEXT_STEP.sml"

  ML_file "Minisubpbl/300-init-subpbl.sml"

  ML_file "Minisubpbl/400-start-meth-subpbl.sml"

  ML_file "Minisubpbl/450-Rewrite_Set_Inst.sml"

  ML_file "Minisubpbl/470-Check_elementwise-NEXT_STEP.sml"

  ML_file "Minisubpbl/490-nxt-Check_Postcond.sml"

  ML_file "Minisubpbl/500-met-sub-to-root.sml"

  ML_file "Minisubpbl/530-error-Check_Elementwise.sml"

  ML_file "Minisubpbl/600-postcond-NEXT_STEP.sml"

  ML_file "Minisubpbl/600-postcond.sml"

  ML_file "Minisubpbl/700-interSteps.sml"

  ML_file "Minisubpbl/710-interSteps-short.sml"

  ML_file "Minisubpbl/790-complete-NEXT_STEP.sml"

  ML_file "Minisubpbl/790-complete.sml"

  ML_file "Minisubpbl/800-append-on-Frm.sml"

subsection \<open>further functionality alongside batch build sequence\<close>

  ML_file "MathEngBasic/thmC.sml"

  ML_file "MathEngBasic/rewrite.sml"

  ML_file "MathEngBasic/tactic.sml"

  ML_file "MathEngBasic/ctree.sml" (*if red, get the file into a text buffer -- this might clear*)

  ML_file "MathEngBasic/calculation.sml"

  ML_file "Specify/formalise.sml"

  ML_file "Specify/o-model.sml"

  ML_file "Specify/i-model.sml"

  ML_file "Specify/pre-conditions.sml"

  ML_file "Specify/p-model.sml"

  ML_file "Specify/m-match.sml"

  ML_file "Specify/refine.sml"        (* requires setup from refine.thy *)

  ML_file "Specify/test-out.sml"

  ML_file "Specify/specify-step.sml"

  ML_file "Specify/specification.sml"

  ML_file "Specify/cas-command.sml"

  ML_file "Specify/p-spec.sml"

  ML_file "Specify/specify.sml"

  ML_file "Specify/step-specify.sml"

  ML_file "Interpret/istate.sml"

  ML_file "Interpret/sub-problem.sml"

  ML_file "Interpret/error-pattern.sml"

  ML_file "Interpret/li-tool.sml"

  ML_file "Interpret/lucas-interpreter.sml"

ML \<open>

\<close> ML \<open>

\<close> ML \<open>

(* Title:  "Interpret/lucas-interpreter.sml"

   Author: Walther Neuper

   (c) due to copyright terms

*)

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

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

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

"----------- Take as 1st stac in program -------------------------------------------------------";

"----------- re-build: fun locate_input_tactic -------------------------------------------------";

"----------- fun locate_input_tactic Helpless, NOT applicable ----------------------------------";

"----------- re-build: fun find_next_step, mini ------------------------------------------------";

"----------- re-build: fun locate_input_term ---------------------------------------------------";

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

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

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

"----------- Take as 1st stac in program -------------------------------------------------------";

"----------- Take as 1st stac in program -------------------------------------------------------";

"----------- Take as 1st stac in program -------------------------------------------------------";

"compare --- Apply_Method with initial Take by Step.do_next --- in test/../step-solve ----------";

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

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

    CalcTreeTEST 

        [(["functionTerm (x \<up> 2 + 1)", "integrateBy x", "antiDerivative FF"],

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

val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = ("Tac ", ...) --> Add_Given...*)

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

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

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

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

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

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

case nxt of (Apply_Method ["diff", "integration"]) => ()

          | _ => error "integrate.sml -- me method [diff,integration] -- spec";

"----- step 8: returns nxt = Rewrite_Set_Inst ([\"(''bdv'', x)\"],\"integration\")";

"~~~~~ fun me, args:"; val (tac, (p:pos'), _, (pt:ctree)) = (nxt, p, c, pt);

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

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

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

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

"~~~~~ fun Step_Solve.by_tactic , args:"; val (m as Apply_Method' (mI, _, _, ctxt), (pt, (pos as (p,_))))

  = (m, (pt, pos));

      val {srls, ...} = MethodC.from_store mI;

      val itms = case get_obj I pt p of

        PblObj {meth=itms, ...} => itms

      | _ => error "solve Apply_Method: uncovered case get_obj"

      val thy' = get_obj g_domID pt p;

      val thy = ThyC.get_theory thy';

      val srls = LItool.get_simplifier (pt, pos)

      val (is, env, ctxt, sc) = case LItool.init_pstate srls ctxt itms mI of

        (is as Istate.Pstate {env, ...}, ctxt, sc) =>  (is, env, ctxt, sc)

      | _ => error "solve Apply_Method: uncovered case init_pstate";

(*+*)pstate2str (the_pstate is) = "([\"\n(f_f, x \<up> 2 + 1)\",\"\n(v_v, x)\"], [], empty, NONE, \n??.empty, ORundef, false, true)";

      val ini = LItool.implicit_take sc env;

      val p = lev_dn p;

      val NONE = (*case*) ini (*of*);

            val Next_Step (is', ctxt', m') =

              LI.find_next_step sc (pt, (p, Res)) is ctxt;

(*+*)pstate2str (the_pstate is') = "([\"\n(f_f, x \<up> 2 + 1)\",\"\n(v_v, x)\"], [R,L,R], empty, NONE, \nIntegral x \<up> 2 + 1 D x, ORundef, false, false)";

  val Safe_Step (_, _, Take' _) = (*case*)

           locate_input_tactic sc (pt, (p, Res)) is' ctxt' m' (*of*);

"~~~~~ fun locate_input_tactic , args:"; val ((Prog prog), cstate, istate, ctxt, tac)

  = (sc, (pt, (p, Res)), is', ctxt', m');

    (*case*) scan_to_tactic1 (prog, (cstate, ctxt, tac)) istate (*of*);

"~~~~~ fun scan_to_tactic1 , args:"; val ((prog, (cctt as ((_, p), _, _))), (Istate.Pstate (ist as {path, ...})))

  = ((prog, (cstate, ctxt, tac)), istate);

    (*if*) path = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*then*);

  val Accept_Tac1 (_, _, Take' _) =

       scan_dn1 cctt (ist |> set_path [R] |> set_or ORundef) (Program.body_of prog);

"~~~~~ fun scan_dn1 , args:"; val (xxx, ist, (Const (\<^const_name>\<open>Let\<close>, _) $ e $ (Abs (id, T, b))))

  = (cctt, (ist |> set_path [R] |> set_or ORundef), (Program.body_of prog));

(*+*) if UnparseC.term e = "Take (Integral f_f D v_v)" then () else error "scan_dn1 Integral changed";

    (*case*)

           scan_dn1 xxx (ist |> path_down [L, R]) e (*of*);

    (*======= end of scanning tacticals, a leaf =======*)

"~~~~~ fun scan_dn1 , args:"; val (((pt, p), ctxt, tac), (ist as {eval, or, ...}), t)

  = (xxx, (ist |> path_down [L, R]), e);

val (Program.Tac stac, a') = check_leaf "locate" ctxt eval (get_subst ist) t;

"----------- re-build: fun locate_input_tactic -------------------------------------------------";

"----------- re-build: fun locate_input_tactic -------------------------------------------------";

"----------- re-build: fun locate_input_tactic -------------------------------------------------";

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

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;

(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = (_, Apply_Method ["Test", "squ-equ-test-subpbl1"])*);

(*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Rewrite_Set", Rewrite_Set "norm_equation")*)

(*//------------------ begin step into ------------------------------------------------------\\*)

(*[1], Res*)val (p'''''_''',_,f,nxt'''''_''',_,pt'''''_''') = me nxt p [] pt; (*nxt = Rewrite_Set "Test_simplify"*)

"~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, [], pt);

    (** )val (***)xxxx(***) ( *("ok", (_, _, (pt, p))) =( **)  (*case*)

      Step.by_tactic tac (pt,p) (*of*);

"~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));

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

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

    (** )val (***)xxxxx_x(***) ( *(msg, cs') =( **)

Step_Solve.by_tactic m ptp;

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

(*+*)val (pt'''''_', (p'''''_', p_'''''_')) = (pt, (p, p_));

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

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

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

     locate_input_tactic sc (pt, po) (fst is) (snd is) m;

"~~~~~ fun locate_input_tactic , args:"; val (Prog prog, cstate, istate, ctxt, tac)

    = (sc, (pt, po), (fst is), (snd is), m);

      val srls = get_simplifier cstate;

 (** )val Accept_Tac1 ((is as (_,_,_,_,_,strong_ass), ctxt, ss as((tac', _, ctree, pos', _) :: _))) =( **)

  (*case*) scan_to_tactic1 (prog, (cstate, ctxt, tac)) istate (*of*);

"~~~~~ fun scan_to_tactic1 , args:"; val ((prog, (cctt as ((_, p), _, _))), (Istate.Pstate (ist as {path, ...})))

  = ((prog, (cstate, ctxt, tac)), istate);

    (*if*) path = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*then*);

    (** )val xxxxx_xx = ( **)

           scan_dn1 cctt (ist |> set_path [R] |> set_or ORundef) (Program.body_of prog);

"~~~~~ fun scan_dn1 , args:"; val (xxx, ist, (Const (\<^const_name>\<open>Let\<close>, _) $ e $ (Abs (id, T, b))))

  = (cctt, (ist |> set_path [R] |> set_or ORundef), (Program.body_of prog));

  (*case*) scan_dn1 xxx (ist |> path_down [L, R]) e (*of*);

"~~~~~ fun scan_dn1 , args:"; val ((xxx as (cstate, _, _)), ist, (Const (\<^const_name>\<open>Chain\<close>(*1*), _) $ e1 $ e2 $ a))

  = (xxx, (ist |> path_down [L, R]), e);

  (*case*) scan_dn1 xxx (ist |> path_down_form ([L, L, R], a)) e1 (*of*);

"~~~~~ fun scan_dn1 , args:"; val (xxx, ist, (Const (\<^const_name>\<open>Try\<close>(*2*), _) $ e))

  = (xxx, (ist |> path_down_form ([L, L, R], a)), e1);

  (*case*) scan_dn1 xxx (ist |> path_down [R]) e (*of*);

    (*======= end of scanning tacticals, a leaf =======*)

"~~~~~ fun scan_dn1 , args:"; val (((pt, p), ctxt, tac), (ist as {env, eval, or, ...}), t)

  = (xxx, (ist |> path_down [R]), e);

    val (Program.Tac stac, a') =

      (*case*) check_leaf "locate" ctxt eval (get_subst ist) t (*of*);

    val LItool.Associated (m, v', ctxt) =

      (*case*) associate pt ctxt (m, stac) (*of*);

       Accept_Tac1 (ist |> set_subst_true  (a', v'), ctxt, m)  (*return value*);

"~~~~~ from scan_dn1 to scan_to_tactic1 return val:"; val (xxxxx_xx)

  = (Accept_Tac1 (ist |> set_subst_true  (a', v'), ctxt, m));

"~~~~~ from scan_to_tactic1 to fun locate_input_tactic return val:"; val Accept_Tac1 ((ist as {assoc, ...}), ctxt, tac')

  = (Accept_Tac1 (ist |> set_subst_true  (a', v'), ctxt, m));

        (*if*) LibraryC.assoc (*then*);

       Safe_Step (Istate.Pstate ist, ctxt, tac')  (*return value*);

"~~~~~ from locate_input_tactic to fun Step_Solve.by_tactic return:"; val Safe_Step (istate, ctxt, tac)

  = (*xxxxx_xx*)(**)Safe_Step (Istate.Pstate ist, ctxt, tac')(**);

(*+*)val (pt, po as (p, p_)) = (pt'''''_', (p'''''_', p_'''''_')); (* from begin of by_tactic *)

                  val (p'', _, _,pt') =

                    Step.add tac (istate, ctxt) (pt, (lev_on p, Pbl));

            (*in*)

         	  	    ("ok", ([(Tactic.input_from_T tac, tac, (p'', (istate, ctxt)))],

                    [(*ctree NOT cut*)], (pt', p'')))  (*return value*);

"~~~~~ from Step_Solve.by_tactic \<longrightarrow> Step.by_tactic return:"; val ((msg, cs' : Calc.state_post))

  =               ("ok", ([(Tactic.input_from_T tac, tac, (p'', (istate, ctxt)) )],

                    [(*ctree NOT cut*)], (pt', p'')));

"~~~~~ from Step.by_tactic to me return:"; val (("ok", (_, _, (pt, p)))) = (*** )xxxx( ***) ("ok", cs');

	  val (_, ts) =

	    (case Step.do_next p ((pt, Pos.e_pos'), []) of

		    ("ok", (ts as (_, _, _) :: _, _, _)) => ("", ts)

	    | ("helpless", _) => ("helpless: cannot propose tac", [])

	    | ("no-fmz-spec", _) => error "no-fmz-spec"

	    | ("end-of-calculation", (ts, _, _)) => ("", ts)

	    | _ => error "me: uncovered case")

	      handle ERROR msg => raise ERROR msg

	  val tac = 

      case ts of 

        tacis as (_::_) => let val (tac, _, _) = last_elem tacis in tac end 

		  | _ => if p = ([], Pos.Res) then Tactic.End_Proof' else Tactic.Empty_Tac;

   (p, [] : NEW, TESTg_form (pt, p), (Tactic.tac2IDstr tac, tac), Celem.Sundef, pt);

"~~~~~ from me to TOOPLEVEL return:"; val (p,_,f,nxt,_,pt)

   = (*** )xxx( ***) (p, [] : NEW, TESTg_form (pt, p), (Tactic.tac2IDstr tac, tac), Celem.Sundef, pt);

(*//--------------------- check results from modified me ----------------------------------\\*)

if p = ([2], Res) andalso

  pr_ctree pr_short pt = ".    ----- pblobj -----\n1.   x + 1 = 2\n2.   x + 1 = 2\n"

then

  (case nxt of ("Rewrite_Set", Rewrite_Set "Test_simplify") => ()

   | _ => error "")

else error "check results from modified me CHANGED";

(*\\--------------------- check results from modified me ----------------------------------//*)

"~~~~~ from me to TOPLEVEL return:"; val (p,_,f,nxt,_,pt) = (*** )xxx( ***) (**)(p, 000, f, nxt, 000, pt)(**);

(*\\------------------ end step into --------------------------------------------------------//*)

(*[3], Res*)val (p,_,f,nxt,_,pt) = me nxt'''''_''' p'''''_''' [] pt'''''_'''; (*nxt = Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"])*)

(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Model_Problem*)

(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "equality (- 1 + x = 0)"*)

(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "solveFor x"*)

(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Find "solutions x_i"*)

(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Theory "Test"*)

(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Problem ["LINEAR", "univariate", "equation", "test"]*)

(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Method ["Test", "solve_linear"]*)

(*[3], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["Test", "solve_linear"]*)

(*[3, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv")*)

(*[3, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "Test_simplify"*)

(*[3, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["LINEAR", "univariate", "equation", "test"]*)

(*[3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_elementwise "Assumptions"*)

(*[4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["sqroot-test", "univariate", "equation", "test"]*)

(*[], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = End_Proof'*)

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

if p = ([], Res) andalso f2str f = "[x = 1]" andalso pr_ctree pr_short pt =

  ".    ----- pblobj -----\n" ^

  "1.   x + 1 = 2\n" ^

  "2.   x + 1 + - 1 * 2 = 0\n" ^

  "3.    ----- pblobj -----\n" ^

  "3.1.   - 1 + x = 0\n" ^

  "3.2.   x = 0 + - 1 * - 1\n" ^

  "4.   [x = 1]\n"

then case nxt of End_Proof' => () | _ => error "re-build: fun locate_input_tactic changed 1"

else error "re-build: fun locate_input_tactic changed 2";

"----------- fun locate_input_tactic Helpless, NOT applicable ----------------------------------";

"----------- fun locate_input_tactic Helpless, NOT applicable ----------------------------------";

"----------- fun locate_input_tactic Helpless, NOT applicable ----------------------------------";

(*cp from -- try fun applyTactics ------- *)

val (p,_,f,nxt,_,pt) = CalcTreeTEST [(["Term (5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12)",

	    "normalform N"],

	   ("PolyMinus",["plus_minus", "polynom", "vereinfachen"],

	    ["simplification", "for_polynomials", "with_minus"]))];

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;

(*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "ordne_alphabetisch"*)

(*+*)val Test_Out.FormKF "5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * g + 12" = f

(*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "fasse_zusammen"*)

(*+*)if map Tactic.input_to_string (specific_from_prog pt p) =

   ["Rewrite (\"subtrahiere_x_plus_minus\", \"\<lbrakk>?l is_num; ?m is_num\<rbrakk>\n\<Longrightarrow> ?x + ?m * ?v - ?l * ?v = ?x + (?m - ?l) * ?v\")",

    "Rewrite (\"subtrahiere_x_minus_plus\", \"\<lbrakk>?l is_num; ?m is_num\<rbrakk>\n\<Longrightarrow> ?x - ?m * ?v + ?l * ?v = ?x + (- ?m + ?l) * ?v\")",

(*this is new since ThmC.numerals_to_Free.-----\\*)

    "Calculate PLUS"]

  then () else error "specific_from_prog ([1], Res) 1 CHANGED";

(*[2], Res*)val ("ok", (_, _, ptp as (pt, p))) = Step.by_tactic (hd (specific_from_prog pt p)) (pt, p);

(*+*)if map Tactic.input_to_string (specific_from_prog pt p) = [

  "Rewrite (\"tausche_minus\", \"\<lbrakk>?b ist_monom; ?a kleiner ?b\<rbrakk>\n\<Longrightarrow> ?b - ?a = - ?a + ?b\")",

  "Rewrite (\"subtrahiere_x_plus_minus\", \"\<lbrakk>?l is_num; ?m is_num\<rbrakk>\n\<Longrightarrow> ?x + ?m * ?v - ?l * ?v = ?x + (?m - ?l) * ?v\")",

  "Rewrite (\"subtrahiere_x_minus_plus\", \"\<lbrakk>?l is_num; ?m is_num\<rbrakk>\n\<Longrightarrow> ?x - ?m * ?v + ?l * ?v = ?x + (- ?m + ?l) * ?v\")",

  (*this is new since ThmC.numerals_to_Free.-----\\*)

  "Calculate PLUS",

  (*this is new since ThmC.numerals_to_Free.-----//*)

  "Calculate MINUS"]

  then () else error "specific_from_prog ([1], Res) 2 CHANGED";

(* = ([3], Res)*)val ("ok", (_, _, ptp as (pt, p))) = Step.by_tactic (hd (specific_from_prog pt p)) (pt, p);

(*//----------------- exception PTREE "get_obj f EmptyPtree" raised --------------------------\\*)

(**)val ("ok", ([(Rewrite ("tausche_minus", _), _, _)], _, _)) = (*isa*)

      Step.by_tactic (hd (specific_from_prog pt p)) (pt, p);

"~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (hd (specific_from_prog pt p), (pt, p));

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

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

(**) val ("ok", ([(Rewrite ("tausche_minus", _), _, _)], _, _)) = (*isa*)

Step_Solve.by_tactic m (pt, p);

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

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

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

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

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

"~~~~~ fun locate_input_tactic , args:"; val ((Rule.Prog prog), (cstate as (pt, (*?*)pos(*?*))), istate, ctxt, tac)

  = (sc, (pt, po), (fst is), (snd is), m);

      val srls = LItool.get_simplifier cstate (*TODO: shift into Istate.T*);

  (*case*) scan_to_tactic1 (prog, (cstate, ctxt, tac)) istate (*of*);

"~~~~~ fun scan_to_tactic1 , args:"; val ((prog, (cctt as ((_, p), _, _))), (Istate.Pstate (ist as {path, ...})))

  = ((prog, (cstate, ctxt, tac)), istate);

    (*if*) path = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*else*);

           go_scan_up1 (prog, cctt) ist;

"~~~~~ fun go_scan_up1 , args:"; val ((pcct as (prog, _)), (ist as {path, ...}))

  = ((prog, cctt), ist);

  (*if*) 1 < length path (*then*);

           scan_up1 pcct (ist |> path_up) (TermC.sub_at (path_up' path) prog);

"~~~~~ and scan_up1 , args:"; val (pcct, ist, (Const (\<^const_name>\<open>Try\<close>(*2*), _) $ _))

  = (pcct, (ist |> path_up), (TermC.sub_at (path_up' path) prog));

           go_scan_up1 pcct ist;

"~~~~~ and go_scan_up1 , args:"; val ((pcct as (prog, _)), (ist as {path, ...}))

  = (pcct, ist);

  (*if*) 1 < length path (*then*);

           scan_up1 pcct (ist |> path_up) (TermC.sub_at (path_up' path) prog);

"~~~~~ and scan_up1 , args:"; val ((pcct as (prog, cct as (cstate, _, _))), ist,

    (Const (\<^const_name>\<open>Chain\<close>(*3*), _) $ _ ))

  = (pcct, (ist |> path_up), (TermC.sub_at (path_up' path) prog));

       val e2 = check_Seq_up ist prog

;

  (*case*) scan_dn1 cct (ist |> path_up_down [R] |> set_or ORundef) e2 (*of*);

"~~~~~ fun scan_dn1 , args:"; val (yyy, ist, (Const (\<^const_name>\<open>Chain\<close>(*2*), _) $ e1 $ e2))

  = (cct, (ist |> path_up_down [R] |> set_or ORundef), e2);

  (*case*) scan_dn1 cct (ist |> path_down [L, R]) e1 (*of*);

"~~~~~ fun scan_dn1 , args:"; val (xxx, ist, (Const (\<^const_name>\<open>Try\<close>(*2*), _) $ e))

  = (cct, (ist |> path_down [L, R]), e1);

\<close> ML \<open>

  (*case*) scan_dn1 cct (ist |> path_down [R]) e (*of*);

    (*======= end of scanning tacticals, a leaf =======*)

"~~~~~ fun scan_dn1 , args:"; val ((cct as (_, ctxt, _)), (ist as {eval, ...}), t)

  = (cct, (ist |> path_down [R]), e);

    (*if*) Tactical.contained_in t (*else*);

  val (Program.Tac prog_tac, form_arg) = (*case*)

    LItool.check_leaf "locate" ctxt eval (get_subst ist) t (*of*);

           check_tac1 cct ist (prog_tac, form_arg);

"~~~~~ fun check_tac1 , args:"; val (((pt, p), ctxt, tac), (ist as {act_arg, or, ...}), (prog_tac, form_arg)) =

  (cct, ist, (prog_tac, form_arg));

val LItool.Not_Associated = (*case*)

  LItool.associate pt ctxt (tac, prog_tac) (*of*);

     val _(*ORundef*) = (*case*) or (*of*);

(*+*)Solve_Step.check (LItool.tac_from_prog pt (ThyC.get_theory "Isac_Knowledge") prog_tac) (pt, p);

     val Applicable.Yes m' =

          (*case*) Solve_Step.check (LItool.tac_from_prog pt (ThyC.get_theory "Isac_Knowledge") prog_tac) (pt, p) (*of*);

  Reject_Tac1 (ist |> set_subst_false (form_arg, Tactic.result m'), ctxt, tac)

          (*return from check_tac1*);

"~~~~~ from fun check_tac1 \<longrightarrow>fun scan_dn1 \<longrightarrow>fun scan_dn1  \<longrightarrow>fun locate_input_tactic , return:"; val (Reject_Tac1 _) =

  (Reject_Tac1 (ist |> set_subst_false (form_arg, Tactic.result m'), ctxt, tac));

val Test_Out.FormKF "- 9 + 12 + 5 * e - 7 * e + 6 * f - 4 * f - 8 * g + 10 * g" = f;

val ([3], Res) = p;

\<close> ML \<open>

"----------- re-build: fun find_next_step, mini ------------------------------------------------";

"----------- re-build: fun find_next_step, mini ------------------------------------------------";

"----------- re-build: fun find_next_step, mini ------------------------------------------------";

val fmz = ["Term (a + a ::real)", "normalform n_n"];

val (dI',pI',mI') = ("Poly",["polynomial", "simplification"],["simplification", "for_polynomials"]);

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

(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, Pos.e_pos'), []);(*Model_Problem*)

(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, Pos.e_pos'), []);(*Specify_Theory "Poly"*)

(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, Pos.e_pos'), []);(*Specify_Problem ["polynomial", "simplification"]*)

(*[], Met*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Specify_Method  ["simplification", "for_polynomials"]*)

(*1], Frm*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Apply_Method ["simplification", "for_polynomials"]*)

(*[1], Res*)val (_, ([(tac'''''_', _, _)], _, (pt'''''_', p'''''_'))) =

      Step.do_next p ((pt, e_pos'), []);(*Rewrite_Set "norm_Poly"*)

(*//------------------ go into 1 ------------------------------------------------------------\\*)

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

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

  val pIopt = Ctree.get_pblID (pt, ip);

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

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

      val SOME _ = (*case*) pIopt (*of*);

      (*if*) member op = [Pos.Pbl, Pos.Met] p_ (*else*);

val ("ok", ([(Rewrite_Set "norm_Poly", _, _)], _, (_, ([1], Res)))) =

Step_Solve.do_next (pt, ip);

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

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

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

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

val Next_Step (_, _, Rewrite_Set' ("Poly", _, Rule_Set.Sequence {id = "norm_Poly", ...}, _, _)) =

           LI.find_next_step sc (pt, pos) ist ctxt (*of*);

"~~~~~ fun find_next_step , args:"; val ((Rule.Prog prog), (ptp as(pt, (p, _))), (Pstate ist), ctxt)

  = (sc, (pt, pos), ist, ctxt);

val Accept_Tac (Rewrite_Set' ("Poly", _, Rule_Set.Sequence {id = "norm_Poly", ...}, _, _), _, _) =

  (*case*) scan_to_tactic (prog, (ptp, ctxt)) (Pstate ist) (*of*);

"~~~~~ fun scan_to_tactic , args:"; val ((prog, cc), (Pstate (ist as {path, ...})))

  = ((prog, (ptp, ctxt)), (Pstate ist));

  (*if*) path = [] (*then*);

val Accept_Tac (Rewrite_Set' ("Poly", _, Rule_Set.Sequence {id = "norm_Poly", ...}, _, _), _, _) =

            scan_dn cc (trans_scan_dn ist) (Program.body_of prog);

"~~~~~ fun scan_dn , args:"; val ((cc as (_, ctxt)), (ist as {eval, ...}), t)

  = (cc, (trans_scan_dn ist), (Program.body_of prog));

    (*if*) Tactical.contained_in t (*else*);

      val (Program.Tac prog_tac, form_arg) = (*case*) LItool.check_leaf "next  " ctxt eval (get_subst ist) t (*of*);

val Accept_Tac (Rewrite_Set' ("Poly", _, Rule_Set.Sequence {id = "norm_Poly", ...}, _, _), _, _) =

          check_tac cc ist (prog_tac, form_arg)  (*return from xxx*);

"~~~~~ from fun scan_dn\<longrightarrow>fun scan_to_tactic\<longrightarrow>fun find_next_step, return:"; val (Accept_Tac (tac, ist, ctxt))

  = (check_tac cc ist (prog_tac, form_arg));

    Next_Step (Pstate ist, Tactic.insert_assumptions tac ctxt, tac)  (*return from find_next_step*);

"~~~~~ from fun find_next_step\<longrightarrow>and do_next\<longrightarrow>fun zzz, return:"; val (Next_Step (ist, ctxt, tac))

  = (Next_Step (Pstate ist, Tactic.insert_assumptions tac ctxt, tac));

           LI.by_tactic tac (ist, Tactic.insert_assumptions tac ctxt) ptp  (*return from and do_next*);

"~~~~~ from and do_next\<longrightarrow>fun do_next\<longrightarrow>toplevel, return:"; val  (_, ([(tac''''', _, _)], _, (pt''''', p''''')))

  = (LI.by_tactic tac (ist, Tactic.insert_assumptions tac ctxt) ptp);

(*\\------------------ end of go into 1 -----------------------------------------------------//*)

(*[], Res*)val (_, ([(tac''''', _, _)], _, (pt''''', p'''''))) =

      Step.do_next p'''''_' ((pt'''''_', Pos.e_pos'), []);(* Check_Postcond ["polynomial", "simplification"]*)

(*//------------------ go into 2 ------------------------------------------------------------\\*)

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

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

  val pIopt = Ctree.get_pblID (pt, ip);

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

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

      val SOME _ = (*case*) pIopt (*of*);

      (*if*) member op = [Pos.Pbl, Pos.Met] p_ (*else*);

val ("ok", ([(Check_Postcond ["polynomial", "simplification"], _, _)], _, (_, ([], Res)))) =

Step_Solve.do_next (pt, ip);

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

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

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

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

  (** )val End_Program (ist, tac) = 

 ( *case*) LI.find_next_step sc (pt, pos) ist ctxt (*of*);

"~~~~~ fun find_next_step , args:"; val ((Rule.Prog prog), (ptp as(pt, (p, _))), (Pstate ist), ctxt)

  = (sc, (pt, pos), ist, ctxt);

(*  val Term_Val (Const (\<^const_name>\<open>times\<close>, _) $ Free ("2", _) $ Free ("a", _))*)

  (** )val Term_Val prog_result =

 ( *case*) scan_to_tactic (prog, (ptp, ctxt)) (Pstate ist) (*of*);

"~~~~~ fun scan_to_tactic , args:"; val ((prog, cc), (Pstate (ist as {path, ...})))

  = ((prog, (ptp, ctxt)), (Pstate ist));

  (*if*) path = [] (*else*);

           go_scan_up (prog, cc) (trans_scan_up ist |> set_found);

"~~~~~ fun go_scan_up , args:"; val ((pcc as (sc, _)), (ist as {path, act_arg, found_accept, ...}))

  = ((prog, cc), (trans_scan_up ist(*|> set_found !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! *)));

    (*if*) path = [R] (*then*);

      (*if*) found_accept = true (*then*);

      Term_Val act_arg (*return from go_scan_up*);

"~~~~~ from fun go_scan_up\<longrightarrow>fun scan_to_tactic, return:"; val (Term_Val prog_result) = (Term_Val act_arg);

    Term_Val prog_result  (*return from scan_to_tactic*);

"~~~~~ from fun scan_to_tactic\<longrightarrow>fun find_next_step, return:"; val (Term_Val prog_result) = (Term_Val prog_result);

    val (true, p', _) = (*case*) parent_node pt p (*of*);

              val (_, pblID, _) = get_obj g_spec pt p';

     End_Program (Pstate ist, Tactic.Check_Postcond' (pblID, prog_result))

     (*return from find_next_step*);

"~~~~~ from fun find_next_step\<longrightarrow>and do_next\<longrightarrow>fun zzz, return:"; val (End_Program (ist, tac))

  = (End_Program (Pstate ist, Tactic.Check_Postcond' (pblID,prog_result)));

      val _ = (*case*) tac (*of*);

val ("ok", ([(Check_Postcond ["polynomial", "simplification"], _, _)], _, (_, ([], Res))))

   = LI.by_tactic tac (ist, ctxt) ptp (*return from and do_next*);

"~~~~~ from and do_next\<longrightarrow>top level, return:"; val (_, ([(tac''''', _, _)], _, (pt''''', p''''')))

  = (LI.by_tactic tac (ist, ctxt) ptp);

(*\\------------------ end of go into 2 -----------------------------------------------------//*)

(*[], Und*)val (msg, ([], _, (pt, p))) = Step.do_next p''''' ((pt''''', Pos.e_pos'), []);(**)

Test_Tool.show_pt_tac pt; (*[

([], Frm), Simplify (a + a)

. . . . . . . . . . Apply_Method ["simplification", "for_polynomials"],

([1], Frm), a + a

. . . . . . . . . . Rewrite_Set "norm_Poly",

([1], Res), 2 * a

. . . . . . . . . . Check_Postcond ["polynomial", "simplification"],

([], Res), 2 * a]*)

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

val (res, asm) = (get_obj g_result pt (fst p));

if UnparseC.term res = "2 * a" andalso map UnparseC.term asm = []

andalso p = ([], Und) andalso msg = "end-of-calculation"

andalso pr_ctree pr_short pt = ".    ----- pblobj -----\n1.   a + a\n"

then 

  case tac''''' of Check_Postcond ["polynomial", "simplification"] => () 

  | _ => error "re-build: fun find_next_step, mini 1"

else error "re-build: fun find_next_step, mini 2"

"----------- re-build: fun locate_input_term ---------------------------------------------------";

"----------- re-build: fun locate_input_term ---------------------------------------------------";

"----------- re-build: fun locate_input_term ---------------------------------------------------";

(*cp from inform.sml

 ----------- appendFormula: on Res + late deriv ------------------------------------------------*)

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

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;

(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*Apply_Method ["Test", "squ-equ-test-subpbl1"]*);

(*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Rewrite_Set "norm_equation"*)

(*+*)if f2str f = "x + 1 = 2" then () else error "locate_input_term at ([1], Frm) CHANGED";

(*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Rewrite_Set "Test_simplify"*)

(*+*)if f2str f = "x + 1 + - 1 * 2 = 0" then () else error "locate_input_term at ([1], Frm) CHANGED";

Test_Tool.show_pt_tac pt; (*[

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

. . . . . . . . . . Apply_Method ["Test", "squ-equ-test-subpbl1"],

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

. . . . . . . . . . Rewrite_Set "norm_equation",

([1], Res), x + 1 + - 1 * 2 = 0             ///Check_Postcond..ERROR*)

\<close> ML \<open>

(*//---------- appendFormula 1 "x = 1" \<longrightarrow> Step_Solve.inform \<longrightarrow> LI.locate_input_term ----------\\*)

"~~~~~ fun appendFormula , args:"; val ((*cI, *) ifo: TermC.as_string) = ((**) "x = 1");

    val cs = (*get_calc cI*) ((pt, p), [(*nxt, nxt_, (pos, (ist, ctxt))*)])

    val pos = (*get_pos cI 1*) p

(*+*)val ptp''''' = (pt, p);

(*+*)if snd ptp''''' = ([1], Res) then () else error "old_cs changed";

(*+*)Test_Tool.show_pt_tac pt; (*[

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

(*+*). . . . . . . . . . Apply_Method ["Test", "squ-equ-test-subpbl1"],

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

(*+*). . . . . . . . . . Rewrite_Set "norm_equation",

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

  val ("ok", cs' as (_, _, ptp')) =

    (*case*) Step.do_next pos cs (*of*);

\<close> ML \<open>

val ("ok", (_(*use in DG !!!*), [], ptp''''' as (pt''''', p'''''))) = (*case*)

Step_Solve.by_term ptp' (encode ifo) (*of*);

\<close> ML \<open>

"~~~~~ fun by_term , args:"; val ((pt, pos as (p, _)), istr)

  = (ptp', (encode ifo));

\<close> ML \<open>

  val SOME f_in =

    (*case*) TermC.parseNEW (get_ctxt pt pos) istr (*of*);

      val pos_pred = lev_back(*'*) pos

  	  val f_pred = Ctree.get_curr_formula (pt, pos_pred);

  	  val f_succ = Ctree.get_curr_formula (pt, pos);

      (*if*) f_succ = f_in (*else*);

  val NONE =

        (*case*) CAS_Cmd.input f_in (*of*);

\<close> ML \<open>

(*NEW*) LI.locate_input_term (pt, pos) f_in (*of*);

\<close> ML \<open>

"~~~~~ fun locate_input_term , args:"; val ((pt, pos), tm) = ((pt, pos), f_in);

   		val pos_pred = Pos.lev_back' pos (*f_pred ---"step pos cs"---> f_succ in appendFormula*)

 \<close> ML \<open>

 val ("ok", (_, _, cstate as (pt', pos'))) =

  (*case*) compare_step ([], [], (pt, pos_pred)) tm (*of*);

\<close> ML \<open>

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

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

    val fo = Calc.current_formula ptp

	  val {nrls, ...} = MethodC.from_store (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p))

	  val {rew_ord, erls, rules, ...} = Rule_Set.rep nrls

\<close> ML \<open>

(*+*)Proof_Context.theory_of (Ctree.get_ctxt pt pos) (*Isac.Test OK!*)

\<close> ML \<open>

	  val (found, der) = Derive.steps (Ctree.get_ctxt pt pos) rew_ord erls rules fo ifo; (*<---------------*)

\<close> ML \<open>

    (*if*) found (*else*);

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

\<close> ML \<open>

           val msg_cs' as (_, (tacis, c', ptp)) = LI.do_next ptp; (*<---------------------*)

\<close> ML \<open>

           (*case*) tacis (*of \<longrightarrow> [(Rewrite_Set "Test_simplify",...*) :State_Steps.T;

\<close> ML \<open>

(*+*) val ((input, tac, (pos, (ist, ctxt))) :: _) = tacis;

(*+*) input (*= Tactic.Rewrite_Set "Test_simplify"*);

(*+*) tac;

(*+*) pos = ([2], Res);

(*+*) ist;

(*+*) Proof_Context.theory_of ctxt (*.., Isac.Test*);

\<close> ML \<open>

		(*in*) compare_step (tacis, c @ c' (*@ c'' =c'BECAUSE OF | _ => msg_cs'*), ptp) ifo (*end*)

\<close> ML \<open>

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

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

    val fo = Calc.current_formula ptp

	  val {nrls, ...} = MethodC.from_store (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p))

	  val {rew_ord, erls, rules, ...} = Rule_Set.rep nrls

\<close> ML \<open>

	  val (found, der) = Derive.steps (Ctree.get_ctxt pt pos) rew_ord erls rules fo ifo; (*<---------------*)

\<close> ML \<open>

    (*if*) found (*else*);

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

\<close> ML \<open>

           val msg_cs' as (_, (tacis, c', ptp)) = LI.do_next ptp; (*<---------------------*)

\<close> ML \<open>

(*+*) val ((input, tac, (pos, (ist, ctxt))) :: _) = tacis;

(*+*) input (*= Tactic.Rewrite_Set "Test_simplify"*);

\<close> ML \<open>

(*+*) tac;

(*+*) pos = ([2], Res);

(*+*) ist;

(*+*) Proof_Context.theory_of ctxt (*.., Isac.Test*);

\<close> ML \<open>

\<close> ML \<open>                               

\<close> ML \<open>

Tactic.Apply_Method': MethodC.id * term option * Istate.T * Proof.context -> Tactic.T

\<close> ML \<open>

\<close> ML \<open>

\<close> ML \<open>

\<close> ML \<open>

\<close> ML \<open>

\<close> ML \<open>

\<close> ML \<open>

\<close> ML \<open> (*----- original..*)

(*NEW*)     Found_Step cstate (*return from locate_input_term*);

       (*LI.Found_Step ( *)cstate(*, _(*istate*), _(*ctxt*))( *return from locate_input_term*);

"~~~~~ from fun locate_input_term\<longrightarrow>fun Step_Solve.by_term, return:"; val ("ok", (_(*use in DG !!!*), c, ptp as (_, p)))

  = (("ok" , ([], [], cstate (* already contains istate, ctxt *))));

    ("ok", ((*_ use in DG !!!,*) c, ptp(* as (_*), p))(*)*)(*return from Step_Solve.by_term*);

"~~~~~ from fun Step_Solve.by_term\<longrightarrow>(fun appendFormula)!toplevel, return:"; val ("ok", (_(*use in DG !!!*), [], ptp''''' as (pt''''', p''''')))

  = ("ok", ([], [], ptp));

\<close> ML \<open>

(*fun me requires nxt...*)

    Step.do_next p''''' (ptp''''', []);

  val ("ok", ([(nxt'''''_' as Check_Postcond ["LINEAR", "univariate", "equation", "test"], _, _)], _,

    (pt'''''_', p'''''_'))) = Step.do_next p''''' (ptp''''', [])

(*\\---------- appendFormula 1 "x = 1" \<longrightarrow> Step_Solve.inform \<longrightarrow> LI.locate_input_term ----------//*)

(*//----- REPLACED BY appendFormula 1 "x = 1" \<longrightarrow> Step_Solve.inform \<longrightarrow> LI.locate_input_term -----\\* )

 (*[2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"])*)

 (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Model_Problem*)

 (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "equality (- 1 + x = 0)"*)

 (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "solveFor x"*)

 (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Find "solutions x_i"*)

 (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Theory "Test"*)

 (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Problem ["LINEAR", "univariate", "equation", "test"]*)

 (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Method ["Test", "solve_linear"]*)

 (*[3], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["Test", "solve_linear"]*)

 (*[3, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv")*)

 (*[3, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "Test_simplify"*)

 (*[3, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["LINEAR", "univariate", "equation", "test"]*)

( *\\----- REPLACED BY appendFormula 1 "x = 1" \<longrightarrow> Step_Solve.inform \<longrightarrow> LI.locate_input_term -----//*)

 (*[3], Res*)val (p,_,f,nxt,_,pt) = me nxt'''''_' p'''''_' [] pt'''''_'; (*nxt = Check_elementwise "Assumptions"*)

 (*[4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["sqroot-test", "univariate", "equation", "test"]*)

 (*[], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = End_Proof'*)

\<close> ML \<open>

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

if p = ([], Res) andalso f2str f = "[x = 1]" andalso pr_ctree pr_short pt =

   ".    ----- pblobj -----\n" ^

   "1.   x + 1 = 2\n" ^

   "2.   x + 1 + - 1 * 2 = 0\n" ^

   "3.    ----- pblobj -----\n" ^

   "3.1.   - 1 + x = 0\n" ^

   "3.2.   x = 0 + - 1 * - 1\n" ^

   "3.2.1.   x = 0 + - 1 * - 1\n" ^

   "3.2.2.   x = 0 + 1\n" (*ATTENTION: see complete Calc below*)

then case nxt of End_Proof' => () | _ => error "re-build: fun locate_input_term CHANGED 1"

else error "re-build: fun locate_input_term CHANGED 2";

Test_Tool.show_pt_tac pt; (*[

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

. . . . . . . . . . Apply_Method ["Test", "squ-equ-test-subpbl1"],

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

. . . . . . . . . . Rewrite_Set "norm_equation",

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

. . . . . . . . . . Rewrite_Set "Test_simplify",

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

. . . . . . . . . . Subproblem (Test, ["LINEAR", "univariate", "equation", "test"]),

([3], Pbl), solve (- 1 + x = 0, x)

. . . . . . . . . . Apply_Method ["Test", "solve_linear"],

([3,1], Frm), - 1 + x = 0

. . . . . . . . . . Rewrite_Set_Inst ([(''bdv'', x)], "isolate_bdv"),

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

. . . . . . . . . . Derive Test_simplify,

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

. . . . . . . . . . Rewrite ("#: - 1 * - 1 = 1", "- 1 * - 1 = 1"),

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

. . . . . . . . . . Rewrite ("radd_0", "0 + ?k = ?k"),

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

. . . . . . . . . . Tactic.input_to_string not impl. for ?!,

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

. . . . . . . . . . Check_Postcond ["LINEAR", "univariate", "equation", "test"],

([3], Res), [x = 1]

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

([], Res), [x = 1]]*)

\<close> ML \<open>

\<close> ML \<open>

\<close>

  ML_file "Interpret/step-solve.sml"

  ML_file "MathEngine/me-misc.sml"

  ML_file "MathEngine/fetch-tactics.sml"

  ML_file "MathEngine/solve.sml"

  ML_file "MathEngine/step.sml"

  ML_file "MathEngine/mathengine-stateless.sml"    (*!part. WN130804: +check Interpret/me.sml*)

  ML_file "MathEngine/messages.sml"

  ML_file "MathEngine/states.sml"

  ML_file "BridgeLibisabelle/thy-present.sml"

  ML_file "BridgeLibisabelle/mathml.sml"           (*part.*)

  ML_file "BridgeLibisabelle/pbl-met-hierarchy.sml"

  ML_file "BridgeLibisabelle/thy-hierarchy.sml"

  ML_file "BridgeLibisabelle/interface-xml.sml"     (*TODO after 2009-2*)

  ML_file "BridgeLibisabelle/interface.sml"

  ML_file "BridgeJEdit/parseC.sml"

  ML_file "BridgeJEdit/preliminary.sml"

  ML_file "BridgeJEdit/vscode-example.sml"

  ML_file "Knowledge/delete.sml"

  ML_file "Knowledge/descript.sml"

  ML_file "Knowledge/simplify.sml"