(* Title: "Minisubpbl/530-error-Check_Elementwise.sml"

   Author: Walther Neuper 1105

   (c) copyright due to lincense terms.

*)

"----------- Minisubplb/530-error-Check_Elementwise.sml ----------";

"----------- Minisubplb/530-error-Check_Elementwise.sml ----------";

"----------- Minisubplb/530-error-Check_Elementwise.sml ----------";

(*see also --- x / (x ^ 2 - 6 * x + 9) - 1 / (x ^ 2 - 3 * x) = 1 /x" by me ---*)

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) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))];

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

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

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

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

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

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

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

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 Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"]) = nxt;

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 Apply_Method ["Test", "solve_linear"] = nxt;

val return_me_Rewrite_Set_Inst = me nxt p [] pt;

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

get_ctxt pt p |> ContextC.is_empty; (*OKfalse*)

val ctxt = get_ctxt pt p;

val SOME t = ParseC.term_opt ctxt "Check_elementwise [x = 1] {(v_v::real). Assumptions}";

get_loc pt p |> snd |> ContextC.is_empty; (**OKfalse*)

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

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

                                       val Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv") = nxt;

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

(*+*)get_ctxt pt p |> ContextC.is_empty; (*false*)

(*+*)val ctxt = get_ctxt pt p;

(*+*)val SOME t = ParseC.term_opt ctxt "Check_elementwise [x = 1] {(v_v::real). Assumptions}";

(*+*)get_loc pt p |> snd |> ContextC.is_empty; (*false*)

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

val return_me_Rewrite_Set = me nxt p [] pt;

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

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

val (pt, p) = case Step.by_tactic tac (pt,p) of

("ok", (_, _, ptp)) => ptp | _ => error "script.sml Step.by_tactic";

Test_Tool.show_pt pt; (*...(([3], Res), [x = 1])]... back in root, OK *)

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

val pIopt = get_pblID (pt,ip); (*= SOME ["sqroot-test", "univariate", ...]*)

tacis; (*= []*)

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

"~~~~~ 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 (p,p_) pt;

    val Next_Step (_, _, Check_elementwise' _) =

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

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

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

      (*case*)

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

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

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

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

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

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

  = ((prog, cct), (trans_scan_up ist |> set_found));

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

           scan_up yyy (ist |> path_up) (go_up ctxt path prog);

"~~~~~ fun scan_up , args:"; val ((yyy as (prog, xxx)), (ist as {found_accept, ...}), (Const (\<^const_name>\<open>Let\<close>(*1*), _) $ _))

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

    (*if* ) found_accept = Napp_ ( *else*);

        val (i, body) = check_Let_up ctxt ist prog;

        (*case*)

           scan_dn xxx (ist |> path_up_down [R, D] |> upd_env i) body (*of*);

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

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

  = (xxx, (ist |> path_up_down [R, D] |> upd_env i), body);

  val (Program.Tac stac, a') = (*case*)

      check_leaf "next " ctxt eval (get_subst ist) t;

	      val Check_elementwise "Assumptions" =

    LItool.tac_from_prog (pt, p) stac;

"~~~~~ fun tac_from_prog , args:"; val (pt, thy, (Const (\<^const_name>\<open>Check_elementwise\<close>, _) $ _ $

    (set as Const (\<^const_name>\<open>Collect\<close>,_) $ Abs (_,_,pred))))

  = (pt, (Proof_Context.theory_of ctxt), stac);

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

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

                                       val Check_elementwise "Assumptions" = nxt;

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