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

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

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

   Author: Walther Neuper 1105

   (c) copyright due to lincense terms.

*)

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

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

"----------- Minisubpbl/300-init-subpbl.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"]);

(*[], Pbl*)val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

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

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

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

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

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

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

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

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

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

(*[2], Res*)val (p''',_,f,nxt''',_,pt''') = me nxt p [] pt; (*nxt = ("Subproblem"*)

(*//--1 begin step into relevant call -----------^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^-----\\

      1 relevant for updating ctxt                                                              *)

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

    val ("ok", (_, _, (pt'''', p''''))) = (*case*)

      Step.by_tactic tac (pt, p) (*of*);

                          get_ctxt pt'''' p'''' |> ContextC.is_empty; (*should NOT be true after this step*)

"~~~~~ fun by_tactic , args:"; val (tac, ptp as (pt, p)) = (tac, (pt''',p'''));

  val Applicable.Yes m = Step.check tac (pt, p);

  (*if*) Tactic.for_specify' m; (*false*)

(*val (msg, cs') =*)

Step_Solve.by_tactic m (pt, p);

"~~~~~ fun by_tactic , args:"; val (m, (pt, po as (p,p_))) = (m, (pt, p));

  (*if*) Method.id_empty = get_obj g_metID pt (par_pblobj pt p) (*false*);

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

	      val (is, sc) = resume_prog thy' (p,p_) pt;

val Safe_Step (Pstate ist''''', ctxt''''', tac'_''''') =

           locate_input_tactic sc (pt, po) (fst is) (snd is) m;

"~~~~~ fun locate_input_tactic , args:"; val (Rule.Prog prog, cstate, istate, ctxt, tac)

     = (sc, (pt, po), (fst is), (snd is), m);

  val Accept_Tac1 (_, _, Subproblem' (_, _, _, _, _, _)) = (*case*)

           scan_to_tactic1 (prog, (cstate, ctxt, tac)) istate (*of*);

"~~~~~ fun scan_to_tactic1 , args:"; val ((prog, (cctt as ((_, p), _, _))), (Pstate (ist as {path, ...})))

  = ((prog, (cstate, ctxt, tac)), istate);

   (*if*) path = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*else*);

           go_scan_up1 (prog, cctt) ist;

"~~~~~ fun go_scan_up1 , args:"; val ((pcct as (prog, _)), (ist as {path, act_arg, ...}))

  = ((prog, cctt), ist);

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

           scan_up1 pcct (ist |> path_up) (TermC.sub_at (path_up' path) prog);

"~~~~~ and scan_up1 , args:"; val (pcct, ist, (Const ("Tactical.Try"(*2*), _) $ _))

  = (pcct, (ist |> path_up), (TermC.sub_at (path_up' path) prog));

           go_scan_up1 pcct ist;

"~~~~~ fun go_scan_up1 , args:"; val ((pcct as (prog, _)), (ist as {path, ...}))

  = (pcct, ist);

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

           scan_up1 pcct (ist |> path_up) (TermC.sub_at (path_up' path) prog);

"~~~~~ and scan_up1 , args:"; val (pcct, ist, (Const ("Tactical.Chain"(*2*), _) $ _ $ _))

  = (pcct, (ist |> path_up), (TermC.sub_at (path_up' path) prog));

           go_scan_up1 pcct ist (*2*: comes from e2*);

"~~~~~ fun go_scan_up1, args:"; val ((pcct as (prog, _)), (ist as {path, ...}))

  = (pcct, ist);

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

           scan_up1 pcct (ist |> path_up) (TermC.sub_at (path_up' path) prog);

"~~~~~ and scan_up1 , args:"; val (pcct, ist, (Const ("Tactical.Chain"(*1*), _) $ _ $ _ $ _))

  = (pcct, (ist |> path_up), (TermC.sub_at (path_up' path) prog));

       go_scan_up1 pcct ist (*all has been done in (*2*) below*);

"~~~~~ fun go_scan_up1, args:"; val ((pcct as (prog, _)), (ist as {path, ...}))

  = (pcct, ist);

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

           scan_up1 pcct (ist |> path_up) (TermC.sub_at (path_up' path) prog);

"~~~~~ and scan_up1 , args:"; val ((pcct as (prog, cct as (cstate, _, _))), ist, (Const ("HOL.Let"(*1*), _) $ _))

  = (pcct, (ist |> path_up), (TermC.sub_at (path_up' path) prog));

      val (i, body) = check_Let_up ist prog;

  (*case*) scan_dn1 cct (ist |> path_up_down [R, D] |> upd_env i |> set_or ORundef) body (*of*);

"~~~~~ fun scan_dn1 , args:"; val (cct, ist, (Const ("HOL.Let", _) $ e $ (Abs (id, T, b))))

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

  (*case*) scan_dn1 cct (ist |> path_down [L, R]) e (*of*);

    (*======= end of scanning tacticals, a leaf =======*)

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

  = (cct, (ist |> path_down [L, R]), e);

val (Program.Tac _, NONE) = (*case*)

           check_leaf "locate" ctxt eval (get_subst ist) t (*of*);

"~~~~~ fun check_leaf , args:"; val (call, thy, srls, (E, (a, v)), t)

  = ("locate", ctxt, eval, (get_subst ist), t);

    val (Program.Tac stac, a) = (*case*) Prog_Tac.eval_leaf E a v t (*of*);

"~~~~~ fun eval_leaf , args:"; val (E, _, _, (t as (Const ("Prog_Tac.SubProblem", _) $ _ $ _)))

  = (E, a, v, t);

     (Program.Tac (subst_atomic E t), NONE); (*return value*)

"~~~~~ from fun eval_leaf \<longrightarrow> fun check_leaf return val:"; val ((Program.Tac stac, a'))

  = ((Program.Tac (subst_atomic E t), NONE : term option));

        val stac' =

            Rewrite.eval_prog_expr (Proof_Context.theory_of ctxt) srls 

              (subst_atomic (Env.update_opt E (a,v)) stac);

    (Program.Tac stac', a'); (*return from check_leaf*) 

"~~~~~ from fun check_leaf \<longrightarrow> fun scan_dn1 return val:"; val  (Program.Tac prog_tac, form_arg)

  = (Program.Tac stac', a' : term option);

        (Program.Tac prog_tac, form_arg)  (*return from check_leaf*);

     check_tac1 cct ist (prog_tac, form_arg)  (*return from scan_dn1*);

"~~~~~ from fun scan_dn1\<longrightarrow>fun scan_up1 HOL.Let(*1*), return:"; val (Accept_Tac1 iss)

  = (check_tac1 cct ist (prog_tac, form_arg));

(*+*)val (pstate, ctxt, tac) = iss;

(*+*)if ContextC.is_empty ctxt then error "ERROR: scan_dn1 should NOT return ContextC.empty" else ();

"~~~~~ from fun scan_up1 HOL.Let(*1*), --------------------------------- NO return:"; val () = ();

(*+*)if ContextC.is_empty ctxt''''' then error "locate_input_tactic should NOT return ContextC.empty" else ();

"~~~~~ from fun locate_input_tactic \<longrightarrow>Step_Solve.by_tactic , return:"; val (LI.Safe_Step (istate, ctxt, tac))

  = (Safe_Step (Pstate ist''''', ctxt''''', tac'_'''''));

               val p' = next_in_prog po

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

  Step.add tac (istate, ctxt) (pt, (p', p_));

"~~~~~ fun add , args:"; val (thy, (Tactic.Subproblem' ((domID, pblID, metID), oris, hdl, fmz_, ctxt_specify, f)),

      (l as (_, ctxt)), (pos as (p, p_)), pt)

  = ((ThyC.get_theory "Isac_Knowledge"), tac, (istate, ctxt), (p', p_), pt);

	    val (pt, c) = cappend_problem pt p l (fmz_, (domID, pblID, metID))

	      (oris, (domID, pblID, metID), hdl, ctxt_specify);

(*+*)if ContextC.is_empty ctxt_specify then error "ERROR: Step.add should NOT get input ContextC.empty" else ();

(*+*)if (get_ctxt pt pos |> ContextC.is_empty) then error "Step.add MUST store ctxt"

(*+*)else ();

(*\\--1 end step into relevant call ----------------------------------------------------------//*)

(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt''' p''' [1] pt''';(*nxt = Model_Problem*)

if p = ([3], Pbl) andalso not (get_ctxt pt p |> ContextC.is_empty)

then

  case nxt of (Model_Problem) => ()

  | _ => error "minisubpbl: CalcTreeTEST has no nxt = Model_Problem"

else error "Minisubpbl/300-init-subpbl.sml changed";