(* Title:  700-interSteps.sml

   Author: Walther Neuper 1105

   (c) copyright due to lincense terms.

*)

"----------- Minisubplb/700-interSteps.sml -----------------------";

"----------- Minisubplb/700-interSteps.sml -----------------------";

"----------- Minisubplb/700-interSteps.sml -----------------------";

(** adaption from rewtools.sml --- initContext..Thy_, fun context_thm ---,

  *into a functional representation, i.e. we outcomment statements with side-effects:

 ** reset_states ();

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

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

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

 ** Iterator 1; moveActiveRoot 1;

 ** autoCalculate 1 CompleteCalc;

 **)

val (p,_,f,nxt,_,pt) = CalcTreeTEST [(["equality (x+1=(2::real))", "solveFor x","solutions L"],

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

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

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;

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;

if p = ([], Res)

then case nxt of ("End_Proof'", End_Proof') => ()

  | _ => error "calculation not finished correctly 1"

else error "calculation not finished correctly 2";

show_pt pt; (* 11 lines with subpbl *)

;

"----- no thy-context at result -----";

(** val p = ([], Res);

 ** initContext 1 Thy_ p

 ***  = <MESSAGE><CALCID>1</CALCID><STRING>no thy-context at result</STRING></MESSAGE>: XML.tree;

 ** val ((pt,_),_) = get_calc 1;  (* 11 lines with subpbl *)

 **

 ** interSteps 1 ([2], Res); (* added [2,1]..[2,6] *)

 **)

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

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

val ip' = lev_pred' pt ip;

val ("detailrls", pt, _(*lastpos*)) = (*case*) Math_Engine.detailstep pt ip (*of*) (* LOST ([3,1,1], Frm) .. ([], Res), [x = 1]*);

show_pt pt;                  (* added [2,1]..[2,6] *)

(**

 ** interSteps 1 ([3,1], Res); (* added [3,1,1] Frm + Res *)

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

 ** show_pt pt;                   (*show 6 + 2 steps added*)

 **

 ** if existpt' ([1,1,1], Frm) pt then ()

 ** else error "integrate.sml: interSteps on Rewrite_Set_Inst";

 **)

;

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

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

(*if*) (not o is_interpos) ip (* = false*);

val ip' = lev_pred' pt ip;

(*case*) Math_Engine.detailstep pt ip (*of*) (* LOST ([3,1,1], Frm) .. ([], Res), [x = 1]*);

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

    val nd = Ctree.get_nd pt p

    val cn = Ctree.children nd;

(*if*) null cn  (* = true*);

(*if*) (Tactic.is_rewset o (Ctree.get_obj Ctree.g_tac nd)) [(*root of nd*)]  (* = true*)

;

(* ?!?: in spite of exception PTREE "ins_chn: pos mustNOT be overwritten" insertion OK ?!?*)

(* Solve.detailrls pt pos (* LOST ([3,1,1], Frm) ff.. ([], Res), [x = 1]*)  *)

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

    val t = get_obj g_form pt p

	  val tac = get_obj g_tac pt p

	  val rls = (assoc_rls o Tactic.rls_of) tac

    val ctxt = get_ctxt pt pos;

 (*case*) rls (*of*);

        val is = Generate.init_istate tac t

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

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

	      val thy = Celem.assoc_thy "Isac_Knowledge"

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

show_pt pt'; (* cut ctree after ([3,1,1], Frm) *)

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

"~~~~~ fun complete_solve, args:"; val (auto, c, (ptp as (_, p as (_, p_)))) = (CompleteSubpbl, [], (pt', pos'));

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

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

val ([(Rewrite_Inst (["(''bdv'', x)"], ("risolate_bdv_add", _)), _, _)], _, _) = (*case*)

           do_solve_step ptp (*of*);

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

  (*if*) Celem.e_metID = get_obj g_metID pt (par_pblobj pt p) (* = false  isabisac = ?*);

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

	      val (srls, is, sc) =

           from_pblobj_or_detail' thy' (p,p_) pt;

"~~~~~ fun from_pblobj_or_detail' , args:"; val (_, (p, p_), pt) = (thy', (p,p_), pt);

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

    val (pbl, p', rls') = par_pbl_det pt p;

  (*if*) pbl (*else*);

	          val scr = (*case*) rls' (*of*);

    (Rule.e_rls(*!!!*), get_loc pt (p, p_), scr)  (*return value*);

(*+*)id_rls rls' = "isolate_bdv";

"~~~~~ from from_pblobj_or_detail' to do_solve_step return val:"; val () = ();

  val (Rewrite_Inst' (_, _, _, _, _, ("risolate_bdv_add", _), _, _), is, (t, _)) =

            determine_next_tactic (thy', srls) (pt, pos) sc is;

"~~~~~ fun determine_next_tactic , args:"; val ((thy, _), (ptp as (pt, (p, _))), sc, (Istate.Pstate ist, _(*ctxt*)))

  = ((thy', srls), (pt, pos), sc, is);

    (*case*)

           scan_to_tactic2 (sc, (ptp, thy)) (Istate.Pstate ist) (*of*);

"~~~~~ fun scan_to_tactic2 , args:"; val ((sc as Rule.Prog prog, cct), (Istate.Pstate (ist as {path, ...})))

  = ((sc, (ptp, thy)), (Istate.Pstate ist));

  (*if*) 0 = length path (*else*);

           go_scan_up2 (sc, cct) (trans_scan_up2 ist |> upd_appy Skip_);

"~~~~~ and go_scan_up2 , args:"; val ((yyy as (Rule.Prog sc, _)), (ist as {env, path, finish, ...}) )

  = ((sc, cct), (trans_scan_up2 ist |> upd_appy Skip_));

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

      scan_up2 yyy (ist |> path_up) (go_up path sc);

"~~~~~ fun scan_up2 , args:"; val ((yyy as (_, xxx)), ist, (Const ("Tactical.Repeat"(*2*), _) $ e))

  = (yyy, (ist |> path_up), (go_up path sc));

    (*case*)

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

    (*========== a leaf has been found ==========*)   

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

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

  val (a', STac stac) =

  (*case*) handle_leaf "next  " th sr (get_subst ist) t (*of*);

"~~~~~ fun handle_leaf , args:"; val (call, thy, srls, (E, (a, v)), t)

  = ("next  ", th, sr, (get_subst ist), t);

(*+*)val [(Free ("t_t", Tt_t), Const ("HOL.eq", _) $ (Const ("Groups.plus_class.plus", _) $ Free ("-1", _) $ Free ("x", _)) $ Free ("0", _)),

    (Free ("v", Tv), Free ("x", Tx))] = E (* THE WRONG TYPES IN E ..(TODO.4)*)

(*+*)val TFree ("'z", ["HOL.type"]) = Tt_t;

(*+*)val Type ("Real.real", []) = Tv;

(*+*)val Type ("Real.real", []) = Tx;

(*+*)val SOME (Const ("empty", Ta)) = a;

(*+*)val Type ("'a", []) = Ta;

(*+*)if term2str v = "x = 0 + -1 * -1" then () else error "handle_leaf changed";

(*+*)val Type ("Real.real", []) = Tv;

    (*case*) Prog_Tac.subst_stacexpr E a v t (*of*);

"~~~~~ fun subst_stacexpr , args:"; val (E, a, v, (t as (*2*)(Const ("Prog_Tac.Rewrite'_Inst", _) $ _ $ _)))

  = (E, a, v, t);

(*+*)val [(Free ("t_t", Tt_t), Const ("HOL.eq", _) $ (Const ("Groups.plus_class.plus", _) $ Free ("-1", _) $ Free ("x", _)) $ Free ("0", _)),

    (Free ("v", Tv), Free ("x", Tx)) ] = E ;      (* THIS IS CORRECT*)

(*+*)term2str t = "Rewrite_Inst [(''bdv'', v)] ''risolate_bdv_add''";

(*+*)val Const ("Prog_Tac.Rewrite'_Inst", _)

  $ (Const ("List.list.Cons", _) 

    $ ((Const ("Product_Type.Pair", _) $ _(*''bdv''*) $ Free ("v", Tv))) 

      $ Const ("List.list.Nil", _))

  $ _ = t;

(*+*)val Type ("Real.real",[]) = Tv;   (* Free ("v", Tv) WRONG TYPE*)

(* THUS (*TODO.*): the "v" (argument of Prog + Prog_Tac ) must get the appropriate type "real" *)

    val SOME a' = (*case*) a (*of*);

"~~~~~ from subst_stacexpr to handle_leaf return val:"; val (a', Celem.STac stac) =

  ((a, Celem.STac (subst_atomic E (t $ a'))));

  val stac' = Rewrite.eval_listexpr_ (Celem.assoc_thy thy) srls (subst_atomic (update_opt E (a,v)) stac)

  (*------------------------------------------- HERE IS A SECOND subst_atomic ?!?*)

;

"~~~~~ from handle_leaf to scan_dn2 return val:"; val (a', Celem.STac stac) = (a', Celem.STac stac);

  val (m,m') = (stac2tac_ : ctree -> theory -> term -> input * T) pt (Celem.assoc_thy th) stac;

  case m of

(**)Rewrite_Inst ([_(*"(''bdv'', x)"*)], ("risolate_bdv_add", _)) => ();

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

"~~~~~ fun applicable_in, args:"; val ((p, p_), pt, (m as Tactic.Rewrite_Inst (subs, thm''))) =

  (p, pt, m);

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

        val pp = par_pblobj pt p;

        val thy' = get_obj g_domID pt pp;

        val thy = Celem.assoc_thy thy';

        val {rew_ord' = ro', erls = erls, ...} = Specify.get_met (get_obj g_metID pt pp);

        val (f, _) = case p_ of (*p 12.4.00 unnecessary*)

                      Frm => (get_obj g_form pt p, p)

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

                    | _ => error ("applicable_in: call by " ^ pos'2str (p, p_));

          val subst = Selem.subs2subst thy subs;

val SOME (f', asm) = (*case*) Rewrite.rewrite_inst_ thy (Rule.assoc_rew_ord ro') erls false subst (snd thm'') f (*of*)

;

Chead.Appl (Tactic.Rewrite_Inst' (thy', ro', erls, false, subst, thm'', f, (f', asm)))

;

"~~~~~ fun rewrite_inst_ , args:"; val (thy, rew_ord, rls, put_asm, subst, thm, ct) =

  (thy, (Rule.assoc_rew_ord ro'), erls, false, subst, (snd thm''), f);

"~~~~~ fun rewrite__ , args:"; val (thy, i, bdv, tless, rls, put_asm, thm, ct) =

  (thy, 1, subst, rew_ord, rls, put_asm, thm, ct);

    val (t', asms, _ (*lrd*), rew) = rew_sub thy i bdv tless rls put_asm ([(*root of the term*)]: Celem.lrd list)

		  (((TermC.inst_bdv bdv) o Calc.norm o #prop o Thm.rep_thm) thm) ct

;

"~~~~~ fun rew_sub , args:"; val (thy, i, bdv, tless, rls, put_asm, lrd, r, t) =

  (thy, i, bdv, tless, rls, put_asm, ([(*root of the term*)]: Celem.lrd list),

		  (((TermC.inst_bdv bdv) o Calc.norm o #prop o Thm.rep_thm) thm), ct);

(*+*)val [(Free ("bdv", Tbdv), Free ("x", Tv))] = bdv

(*+*)val Type ("Real.real",[]) = Tbdv

(*+*)val Type ("Real.real",[]) = Tv;

    val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r

    val r' = (Envir.subst_term (Pattern.match thy (lhs, t) (Vartab.empty, Vartab.empty)) r)

(*+*) handle Pattern.MATCH => @{term aaaaaaaaaaaaaaa} (* <<<<<<<<<-----------------(*TODO.90*)*)

    val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems) (Logic.count_prems r', [], r'))

    val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r'