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

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;

(*[], 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''');

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

  val Appl m = applicable_in p pt tac;

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

(*val Updated (cs' as (_,_,(_,p'))) =  loc_solve_ (mI,m) ptp;*)

"~~~~~ fun loc_solve_, args:"; val (m, (pt,pos)) = (m, ptp);

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

           Step_Solve.by_tactic m (pt, pos);

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

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;

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

"~~~~~ fun locate_input_tactic , args:"; val (Rule.Prog progr, 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), _, _))),

     (Istate.Pstate (ist as {path, ...})))

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

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

           go_scan_up1 (progr, cctt) ist;

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

  = ((prog, cctt), ist);

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

           scan_up1 yyy (ist |> path_up) (at_location (path_up' path) prog);

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

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

           go_scan_up1 yyy ist;

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

  = (yyy, ist);

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

           scan_up1 yyy (ist |> path_up) (at_location (path_up' path) prog);

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

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

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

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

  = (yyy, ist);

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

           scan_up1 yyy (ist |> path_up) (at_location (path_up' path) prog);

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

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

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

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

  = (yyy, ist);

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

           scan_up1 yyy (ist |> path_up) (at_location (path_up' path) prog);

"~~~~~ fun scan_up1 , args:"; val ((yyy as (prog, xxx as (cstate, _, _))), ist, (Const ("HOL.Let"(*1*), _) $ _))

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

      val (i, body) = check_Let_up ist prog

;

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

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

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

  (*case*) scan_dn1 xxx (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)

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

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

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

"~~~~~ fun interpret_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 eval_leaf to interpret_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);

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

"~~~~~ from interpret_leaf to scan_dn1 return val:"; val (a', Program.Tac stac)

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

           val Lucin.Ass (m, v', ctxt) = (*case*) Lucin.associate pt ctxt (m, stac) (*of*);

(*+*)if is_e_ctxt ctxt then error "ERROR: scan_dn1 returns e_ctxt" else ();

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

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

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

then

  case nxt of (Model_Problem) => ()

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

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