(* Title:  450-nxt-Check_Postcond

   Author: Walther Neuper 1105

   (c) copyright due to lincense terms.

*)

"----------- Minisubplb/490-nxt-Check_Postcond -------------------";

"----------- Minisubplb/490-nxt-Check_Postcond -------------------";

"----------- Minisubplb/490-nxt-Check_Postcond -------------------";

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

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

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

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

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

"~~~~~ 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; (*= []*)

val SOME pI = pIopt;

member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); (*= false*)

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

e_metID = get_obj g_metID pt (par_pblobj pt p); (*false*)

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

val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; (*is: which ctxt?*)

val (tac_,is,(t,_)) = determine_next_tactic (thy',srls) (pt,pos) sc is;

;tac_; (* = Check_Postcond' *)

"~~~~~ fun begin_end_prog, args:"; val ((Check_Postcond' (pI,_)), _, (pt, pos as (p,p_))) =

                                 (tac_, is, ptp);

        val pp = par_pblobj pt p

        val asm =

          (case get_obj g_tac pt p of

		         Check_elementwise _ => (*collects and instantiates asms*)

		           (snd o (get_obj g_result pt)) p

		       | _ => get_assumptions_ pt (p,p_))

	        handle _ => [] (*FIXME.WN030527 asms in subpbls not completely clear*)

        val metID = get_obj g_metID pt pp;

        val {srls=srls,scr=sc,...} = get_met metID;

        val loc as (ScrState (E,l,a,_,_,b), ctxt) = get_loc pt (p,p_); 

        val thy' = get_obj g_domID pt pp;

        val thy = assoc_thy thy';

        val (_,_,(scval,scsaf)) = determine_next_tactic (thy',srls) (pt,(p,p_)) sc loc;

;pp = []; (*false*)

            val ppp = par_pblobj pt (lev_up p);

	          val thy' = get_obj g_domID pt ppp;

            val thy = assoc_thy thy';

	          val metID = get_obj g_metID pt ppp;

	          val {scr,...} = get_met metID;

            val (ScrState (E,l,a,_,_,b), ctxt') = get_loc pt (pp(*!/p/*),Frm)

          val ctxt'' = from_subpbl_to_caller ctxt scval ctxt'

            val tac_ = Check_Postcond' (pI, (scval, asm))

	          val is = ScrState (E,l,a,scval,scsaf,b);

"~~~~~ fun generate1, args:"; val (thy, (Check_Postcond' (pI, (scval, asm))), l, (p,p_), pt) =

                                  (thy, tac_, (is, ctxt''), (pp, Res), pt);

val (pt,c) = append_result pt p l (scval, (*map str2term*) asm) Complete;

(*----------------------------------------############### changed*)

val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*nxt = Check_Postcond ["LINEAR","uval (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; (*is: which ctxt?*)nivariate", ...]) *);

case nxt of ("Check_Postcond", Check_Postcond ["LINEAR", "univariate", "equation", "test"]) => ()

| _ => error "450-nxt-Check_Postcond broken"