(* 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) = 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; (*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 Step.by_tactic tac (pt,p) of

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

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

"~~~~~ 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", ...]*)

    (*if*) tacis; (*= []*)

    val SOME pI = pIopt;

    (*if*) 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); (*false*)

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

val ((ist, ctxt), sc) = resume_prog (p,p_) pt;

val End_Program (ist, tac) =

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

  val ("ok", ([(Check_Postcond ["LINEAR", "univariate", "equation", "test"], _, _)], _, _)) =

        LI.by_tactic tac (ist, ctxt) ptp;

"~~~~~ fun by_tactic , args:"; val ((Check_Postcond' (pI, _)), (sub_ist, sub_ctxt), (pt, pos as (p,_))) =

                                 (tac, (ist, ctxt), ptp);

      val parent_pos = par_pblobj pt p

      val {scr, ...} = MethodC.from_store ctxt (get_obj g_metID pt parent_pos);

      val prog_res =

         case LI.find_next_step scr (pt, pos) sub_ist sub_ctxt of

(*OLD*)    Next_Step (_, _, Tactic.Check_elementwise' (_, _, (prog_res, _))) => prog_res

  |(*OLD*) End_Program (_, Tactic.Check_Postcond' (_, prog_res)) => prog_res

(*OLD*)  | _ => raise ERROR ("Step_Solve.by_tactic Check_Postcond " ^ strs2str' pI)

(*OLD* )   vvv--- handled by ctxt \<rightarrow> drop ( *OLD*)

(*OLD*)val asm = (*?!? Rfun,Rrls rm case*)(case get_obj g_tac pt p of

(*OLD*)    Tactic.Check_elementwise _ => (snd o (get_obj g_result pt)) p

(*OLD*)  | _ => Ctree.get_assumptions pt pos);

(*OLD* )val tac = Tactic.Check_Postcond' (pI, (prog_res, asm))

( *OLD*)

    (*if*) parent_pos = []; (*else*)

(*NEW*)   val (ist_parent, ctxt_parent) = case get_loc pt (parent_pos, Frm) of

(*NEW*)     (Pstate i, c) => (i, c)

(*NEW*)   | _ => error "LI.by_tactic Check_Postcond': uncovered case get_loc"

(*NEW*)   val (prog_res', ctxt') = ContextC.subpbl_to_caller sub_ctxt prog_res ctxt_parent

(*NEW*)   val tac = Tactic.Check_Postcond' (pI, prog_res')

(*NEW*)   val ist' = Pstate (ist_parent |> set_act prog_res |> set_found)

;

"~~~~~ fun add , args:"; val ((Check_Postcond' (_, scval)), l, (pt, (p, _))) =

                                  (tac, (ist', ctxt'), (pt, (parent_pos, Res)));

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

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

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

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

Proof_Context.theory_of (Ctree.get_ctxt pt p); (*"Test"*)