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

"----------- re-build: fun find_next_tactic ----------------------------------------------------";

"----------- re-build: fun locate_input_formula ------------------------------------------------";

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

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

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

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

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

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

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

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):tac'_), (p:pos'), _, (pt:ctree)) = (nxt, p, c, pt);

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

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

val Appl m = applicable_in p pt m;

member op = specsteps mI (*false*);

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

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

                            (m, (pt, pos));

      val {srls, ...} = get_met 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 = Celem.assoc_thy thy';

      val srls = Lucin.get_simplifier (pt, pos)

      val (is, env, ctxt, sc) = case Lucin.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";

(*+*)scrstate2str (the_pstate is) = "([\"\n(f_f, x ^^^ 2 + 1)\",\"\n(v_v, x)\"], [], e_rls, NONE, \n??.empty, ORundef, AppUndef_, true)";

      val ini = Lucin.init_form thy sc env;

      val p = lev_dn p;

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

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

              LucinNEW.find_next_tactic sc (pt, (p, Res)) is ctxt;

(*+*)scrstate2str (the_pstate is') = "([\"\n(f_f, x ^^^ 2 + 1)\",\"\n(v_v, x)\"], [R,L,R], e_rls, NONE, \nIntegral x ^^^ 2 + 1 D x, ORundef, AppUndef_, 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 ("HOL.Let", _) $ e $ (Abs (id, T, b))))

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

(*+*) if term2str 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') = interpret_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")*)

(*// relevant call --------------------------------------------------------------------------\\*)

(*[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*) locatetac tac (pt,p) (*of*);

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

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

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

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

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

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

    (** )val (***)xxxxx_x(***) ( *(msg, cs') =( **) Solve.solve m (pt, pos);

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

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

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

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

	      val (_, is, sc) = Lucin.from_pblobj' 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 ("HOL.Let", _) $ 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 ("Tactical.Chain"(*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 ("Tactical.Try"(*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*) interpret_leaf "locate" ctxt eval (get_subst ist) t (*of*);

    val Lucin.Ass (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 solve 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 solve *)

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

                    Generate.generate1 (Celem.assoc_thy "Isac_Knowledge") tac

                    (* DEL.^^^^^ ContextC.insert_assumptions asms' ctxt 2nd, fst in Lucin.associate *)

                      (istate, ctxt) (lev_on p, Pbl) pt;

            (*in*)

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

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

"~~~~~ from solve to loc_solve_ return:"; val ((msg, cs' : calcstate'))

  =                    ("ok", ([(Tactic.input_from_T tac, tac, (p'', (istate, ctxt)) )], [(*ctree NOT cut*)], (pt', p'')));

"~~~~~ from loc_solve_ to locatetac return:"; val (Updated (cs' as (_, _, (_, p'))))

   = (*** )xxxxx( ***) (Updated (cs'));

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

          ("ok", cs');

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

	  val (_, ts) =

	    (case step 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), Telem.Sundef, pt);

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

   = (*** )xxx( ***) (p, [] : NEW, TESTg_form (pt, p), (Tactic.tac2IDstr tac, tac), Telem.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 of modified "fun me" ---------------------------------------------//*)

(*[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 fst nxt = "End_Proof'"

  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 () else error "re-build: fun locate_input_tactic changed";

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

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

"----------- fun locate_input_tactic Helpless, but 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"*)

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

(*+*)if map tac2str (sel_appl_atomic_tacs pt p) =

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

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

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

(*[2], Res*)val ("ok", (_, _, ptp as (pt, p))) = locatetac (hd (sel_appl_atomic_tacs pt p)) (pt, p);

(*+*)if map tac2str (sel_appl_atomic_tacs pt p) =

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

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

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

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

(* = ([3], Res)*)val ("ok", (_, _, ptp as (pt, p))) = locatetac (hd (sel_appl_atomic_tacs pt p)) (pt, p);

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

(** )val ("ok", (_, _, ptp as (pt, p))) =( **) locatetac (hd (sel_appl_atomic_tacs pt p)) (pt, p);

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

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

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

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

      loc_solve_ (mI, m) ptp;

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

      solve m (pt, pos);

  (* ======== general case ======== *)

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

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

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

	      val (_, is, sc) = Lucin.from_pblobj_or_detail' 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 = Lucin.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;

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

  = ((prog, cctt), ist);

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

           scan_up1 yyy (ist |> path_up) (go (path_up' path) prog);

"~~~~~ fun scan_up1 , args:"; val (yyy, ist, (Const ("Tactical.Try"(*2*), _) $ _))

  = (yyy, (ist |> path_up), (go (path_up' path) prog));

           go_scan_up1 yyy ist;

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

  = (yyy, ist);

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

           scan_up1 yyy (ist |> path_up) (go (path_up' path) prog);

"~~~~~ fun scan_up1 , args:"; val ((yyy as (prog, xxx as (cstate, _, _))), ist,

    (Const ("Tactical.Chain"(*3*), _) $ _ ))

  = (yyy, (ist |> path_up), (go (path_up' path) prog));

       val e2 = check_Seq_up ist prog

;

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

"~~~~~ fun scan_dn1 , args:"; val (yyy, ist, (Const ("Tactical.Chain"(*2*), _) $ _ $ _))

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

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

"~~~~~ fun scan_dn1 , args:"; val (xxx, ist, (Const ("Tactical.Try"(*2*), _) $ e))

  = (xxx, (ist |> path_down [L, R]), 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 {eval, act_arg, or, ...}), t)

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

    val (Program.Tac stac, a') = (*case*) interpret_leaf "locate" ctxt eval (get_subst ist) t (*of*);

      val NotAss = (*case*) associate pt ctxt (tac, stac) (*of*);

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

  val Notappl "norm_equation not applicable" =    

      (*case*) Applicable.applicable_in p pt (Lucin.stac2tac pt (Celem.assoc_thy "Isac_Knowledge") stac) (*of*);

   (Term_Val1 act_arg) (* return value *);

val Rewrite' ("PolyMinus", "tless_true", _, _, ("tausche_minus",_ (*"?b ist_monom \<Longrightarrow> ?a kleiner ?b \<Longrightarrow> ?b - ?a = - ?a + ?b"*)),

   t, (res, asm)) = m;

if scrstate2str ist =

  "([\"\n(t_t, 5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * g + 12)\"], [R,L,R,R,L,R,R], e_rls, SOMEt_t, \n" ^

  "- (8 * g) + (- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f) + 10 * g, ORundef, AppUndef_, false)"

andalso

  term2str t = "- (8 * g) + (- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f) + 10 * g"

andalso

  term2str res = "- (8 * g) + (- 9 + 12 + 5 * e - 7 * e + (- 4 + 6) * f) + 10 * g"

andalso

  terms2str asm = "[\"4 kleiner 6\",\"6 ist_monom\"]"

then () else error "locate_input_tactic Helpless, but applicable CHANGED";

"----------- re-build: fun find_next_tactic -----------------------------------------------";

"----------- re-build: fun find_next_tactic -----------------------------------------------";

"----------- re-build: fun find_next_tactic -----------------------------------------------";

(*//--------- exception Size raised (line 171 of "./basis/LibrarySupport.sml") ---------------\\

    THIS CODE WORKS IN Test.Some.thy

------------------------------------

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

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

(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, Pos.e_pos'), []);(*Specify_Theory*)

(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, Pos.e_pos'), []);(*Specify_Problem ["sqroot-test", "univariate", "equation", "test"*)

(*[], Met*)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(*Specify_Method ["Test", "squ-equ-test-subpbl1"]*)

(*1], Frm*)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(*Apply_Method ["Test", "squ-equ-test-subpbl1"]*)

(*[1], Res*)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(*Rewrite_Set "norm_equation"*)

(*// relevant call --------------------------------------------------------------------------\\*)

(*[2], Res*)val (aaa, ([(tac'''', bbb, ccc)], ddd, (pt'''', p''''))) =(**) step p ((pt, e_pos'), []);(*Rewrite_Set "Test_simplify"*)

(*-- relevant call ----------------------------------------------------------------------------*)

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

    val pIopt = get_pblID (pt,ip);

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

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

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

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

  	                    andalso is_none (Ctree.get_obj Ctree.g_env pt (fst p)) (*else*);

(** )val cs''''' = ( *..interpret "if member op ="..*)

  (*case*) do_solve_step (pt, ip) (*of*);

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

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

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

	      val (_, (ist, ctxt), sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;

(*NEW*) val Next_Step (_, _, Rewrite_Set' (_, _, Rls {id = "Test_simplify", ...}, _, _)) = (*case*)

(*NEW*)    find_next_tactic sc (pt, pos) ist ctxt (*of*);

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

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

(*OLD* ) val Accept_Tac2 (m', ist as {act_arg, ...}, ctxt) =

(*OLD*)   (*case*) scan_to_tactic2 (prog, (ptp, ctxt)) (Istate.Pstate ist) (*of*);

( *OLD*)  

(*NEW*) val Accept_Tac2 (tac, ist, ctxt) =

(*NEW*)(*case*) scan_to_tactic2 (prog, (ptp, ctxt)) (Istate.Pstate ist) (*of*);

(*NEW* )| Term_Val2 prog_result => End_Program (ist, Check_Postcond' ...prog_result...)

(*NEW*)    (* ist indicates ^^\<Or>?, ctxt already updated, ^^^*)

(*NEW*)| Reject_Tac2 => Helpless

( *NEW*)

(*OLD* )(m',        (Pstate ist, ctxt),           (act_arg, Telem.Safe))  (*return value*);

( *OLD*)

(*NEW*) Next_Step (Istate.Pstate ist, Tactic.insert_assumptions tac ctxt, tac)  (*return value*);

(*NEW*)

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

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

(*NEW* ) case  find_next_tactic sc (pt, pos) ist ctxt of

(*NEW*)    Next_Step (ist, ctxt, tac) =>

( *NEW*)

             begin_end_prog tac (ist, Tactic.insert_assumptions tac ctxt) ptp;

(*NEW* ) | End_Program (ist, tac) => begin_end_prog tac (ist, ctxt) ptp

(*NEW*)  | Helpless => Chead.e_calcstate'

( *NEW*)

(*+*)val Rewrite_Set' ("Test", false, Rls {id = "Test_simplify", ...}, _, _) = tac;

(*OLD skip* )  val _ = (*case*) tac_'''''_' (*of*);

(*OLD skip*)begin_end_prog tac_'''''_' is'''''_' ptp'''''_'  (*return value*);

( *OLD*)

"~~~~~ fun begin_end_prog , args:"; val (tac_, is, (pt, pos))

(*skip* )= (tac_'''''_', is, ptp);( *skip*)

(*use*) = (tac, (ist, Tactic.insert_assumptions tac ctxt), ptp) (*use*)

      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

 	    val (pos', c, _, pt) = Generate.generate1 (Celem.assoc_thy "Isac_Knowledge") tac_ is pos pt;

      ([(Tactic.input_from_T tac_, tac_, (pos, is))], c, (pt, pos')) (*return from do_solve_step*);

"~~~~~ from and do_solve_step\<longrightarrow>fun step , return:"; 

(*OLD skip* )val (tac_'''''_')

(*OLD skip*)  = (begin_end_prog tac_'''''_' is ptp);( **)

(*use*)val cs =

(*use*)([(Tactic.input_from_T tac_, tac_, (pos, is))], c, (pt, pos'));

(*use*)

"~~~~~ from fun step\<longrightarrow>TOPLEVEL return:";

(*OLD skip* )val (_, ([(tac'''', _, _)], _, (pt'''', p'''')))  = ("ok", cs''''')( **);

(*OLD skip*)

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

(*use*)

(*\\------------------ end of modified "fun step" -------------------------------------------//*)

(*[3], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = step p'''' ((pt'''', e_pos'), []);(*Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"])*)

(*[3], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(*Model_Problem*)

(*[3], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(*Specify_Theory "Test"*)

(*[3], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(*Specify_Problem ["LINEAR", "univariate", "equation", "test"]*)

(*[3], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(*Specify_Method ["Test", "solve_linear"]*)

(*[3, 1], Frm*)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(*Apply_Method ["Test", "solve_linear"]*)

(*[3, 1], Res*)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(*Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv")*)

(*[3, 2], Res*)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(*Rewrite_Set "Test_simplify"*)

(*[3], Res*)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(*Check_Postcond ["LINEAR", "univariate", "equation", "test"]*)

(*[4], Res*)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(*Check_elementwise "Assumptions"*)

(*[], Res*)val ("ok", ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(*Check_Postcond ["sqroot-test", "univariate", "equation", "test"]*)

(*[], Res*)val ("end-of-calculation", ([], _, (pt, p))) = step p ((pt, e_pos'), []);(**)

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

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

if term2str res = "[x = 1]" andalso terms2str asm = "[\"precond_rootmet 1\"]"

then () else error "re-build: fun find_next_tactic CHANGED 1";

if p = ([], Und)  (*.. should be ([], Res) *)

then

  case get_obj g_tac pt (fst p) of

    Apply_Method ["Test", "squ-equ-test-subpbl1"] => ((*ok, further tactics are level down*))

  | _ => error "re-build: fun find_next_tactic CHANGED 3"

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

  \\--------- exception Size raised (line 171 of "./basis/LibrarySupport.sml") ---------------//*)

"----------- re-build: fun locate_input_formula ------------------------------------------------";

"----------- re-build: fun locate_input_formula ------------------------------------------------";

"----------- re-build: fun locate_input_formula ------------------------------------------------";