(* Title: 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) = 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;

val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["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; (*nxt = Subp ["LINEAR", "univariate", "equation", "test"]*)

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; (*OKnxt = Apply_Method ["Test", "solve_linear"]*)

val (p'',_,f,nxt,_,pt'') = me nxt p [] pt; (*nxt = Rewrite_Set_Inst..OK isolate_bdv*);

get_ctxt pt'' p'' |> is_e_ctxt; (*OKfalse*)

val ctxt = get_ctxt pt'' p'';

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

get_loc pt'' p'' |> snd |> is_e_ctxt; (**OKfalse*)

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

get_ctxt pt p |> is_e_ctxt; (*false*)

val ctxt = get_ctxt pt p;

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

get_loc pt p |> snd |> is_e_ctxt; (*false*)

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

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

"~~~~~ fun me, args:"; val (_,tac) = nxt;

val (pt, p) = case locatetac tac (pt,p) of

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

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

"~~~~~ fun step, 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_ andalso is_none (get_obj g_env pt (fst p)); (*= false*)

"~~~~~ 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 (srls, is, sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;

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

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

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

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

      (*case*)

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

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

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

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

       go_scan_up2 (prog, cct) (trans_scan_up2 ist |> set_appy Skip_);

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

  = ((prog, cct), (trans_scan_up2 ist |> set_appy Skip_));

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

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

"~~~~~ fun scan_up2 , args:"; val ((yyy as (prog, xxx)), (ist as {finish, ...}), (Const ("HOL.Let"(*1*), _) $ _))

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

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

        val (i, body) = check_Let_up ist prog;

        (*case*)

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

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

"~~~~~ fun scan_dn2 , 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*)

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

	      val (Check_elementwise "Assumptions", Empty_Tac_) =

           stac2tac_ pt (Celem.assoc_thy ctxt) stac;

"~~~~~ fun stac2tac_ , args:"; val (pt, thy, (Const("Prog_Tac.Check'_elementwise",_) $ _ $

    (set as Const ("Set.Collect",_) $ Abs (_,_,pred))))

  = (pt, (assoc_thy th), stac);

val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*WAS nxt = ("Empty_Tac", Empty_Tac)*)

case nxt of ("Check_elementwise", Check_elementwise "Assumptions") => ()

| _ => error "Check_elementwise changed; after switch sub-->root-method";