(* Title:  "Minisubpbl/300-init-subpbl-NEXT_STEP.sml"

   Author: Walther Neuper 1105

   (c) copyright due to lincense terms.

*)

"----------- Minisubpbl/300-init-subpbl-NEXT_STEP.sml -----------------------------------------";

"----------- Minisubpbl/300-init-subpbl-NEXT_STEP.sml -----------------------------------------";

"----------- Minisubpbl/300-init-subpbl-NEXT_STEP.sml -----------------------------------------";

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'))];

(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, Pos.e_pos'), []);(*Model_Problem*)

(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, Pos.e_pos'), []);(*Specify_Theory*)

(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, Pos.e_pos'), []);(*Specify_Problem ["sqroot-test", "univariate", "equation", "test"*)

(*[], Met*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Specify_Method ["Test", "squ-equ-test-subpbl1"]*)

(*[1], Frm*)val (_, ([(tac''''', _, _)], _, (pt''''', p'''))) =(**) Step.do_next p ((pt, e_pos'), []);(*Apply_Method ["Test", "squ-equ-test-subpbl1"]*)

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

    val pIopt = get_pblID (pt,ip);

    (*if*) ip = ([], Pos.Res) (*else*);

      val _ = (*case*) tacis (*of*);

      val SOME _ = (*case*) pIopt (*of*);

    (*if*) member op = [Pos.Pbl, Pos.Met] p_ 

  	                    andalso is_none (Ctree.get_obj Ctree.g_env pt (fst p)) (*then*);

(*+*)val (_, ([_], _, (pt''''', p'''''))) =

           Step.specify_do_next (pt, ip);

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

    val (pblobj, meth, origin, oris, dI', pI', mI', probl, dI, pI, mI) = 

  	  case Ctree.get_obj I pt p of

  	    pblobj as (Ctree.PblObj {meth, origin = origin as (oris, (dI', pI', mI'), _),

  		  probl, spec = (dI, pI, mI), ...}) => (pblobj, meth, origin, oris, dI', pI', mI', probl, dI, pI, mI)

      | Ctree.PrfObj _ => error "nxt_specify_: not on PrfObj";

   (*if*) Ctree.just_created_ pblobj (*by Subproblem*) andalso origin <> Ctree.e_origin (*else*);

        val cpI = if pI = Celem.e_pblID then pI' else pI;

  	    val cmI = if mI = Celem.e_metID then mI' else mI;

  	    val {ppc, prls, where_, ...} = Specify.get_pbt cpI;

  	    val pre = Stool.check_preconds "thy 100820" prls where_ probl;

  	    val pb = foldl and_ (true, map fst pre);

  	    val (_, tac) =

  	      Chead.nxt_spec p_ pb oris (dI', pI', mI') (probl, meth) (ppc, (#ppc o Specify.get_met) cmI) (dI, pI, mI)

        val ist_ctxt =  get_loc pt (p, p_)

        val Apply_Method mI = (*case*) tac (*of*);

(*+*)val (_, (_, _, (pt'''', p''''))) =

           Lucin.by_tactic (Tactic.Apply_Method' (mI, NONE, Istate.e_istate, ContextC.e_ctxt)) ist_ctxt ptp;

"~~~~~ fun begin_end_prog , args:"; val ((Tactic.Apply_Method' (mI, _, _, _)), (ist, ctxt), (pt, pos as (p, _)))

  = ((Tactic.Apply_Method' (mI, NONE, Istate.e_istate, ContextC.e_ctxt)), ist_ctxt, ptp);

      val {ppc, ...} = Specify.get_met mI;

      val (itms, oris, probl) = case get_obj I pt p of

        PblObj {meth = itms, origin = (oris, _, _), probl, ...} => (itms, oris, probl)

      | _ => error "begin_end_prog Apply_Method': uncovered case get_obj"

      val itms = if itms <> [] then itms else Chead.complete_metitms oris probl [] ppc

      val thy' = get_obj g_domID pt p;

      val thy = Celem.assoc_thy thy';

      val srls = LItool.get_simplifier (pt, pos);

  (*if*) mI = ["Biegelinien", "ausBelastung"] (*else*);

     val (is, env, ctxt, scr) = case LItool.init_pstate srls ctxt itms mI of

         (is as Istate.Pstate {env, ...}, ctxt, scr) => (is, env, ctxt, scr)

       | _ => error "begin_end_prog Apply_Method': uncovered case init_pstate"

(*[1], Res*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p''''' ((pt''''', e_pos'), []);(*Rewrite_Set "norm_equation"*)

case tac of Rewrite_Set "norm_equation" => (

  if p = ([1], Res) then (

    if pr_ctree pr_short pt = ".    ----- pblobj -----\n1.   x + 1 = 2\n" then ()

    else error "Apply_Method [Test, squ-equ-test-subpbl1] changed pt"

    ) else error "Apply_Method [Test, squ-equ-test-subpbl1] changed p") 

| _ => error "Apply_Method [Test, squ-equ-test-subpbl1] changed tac"