(* 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 (mI,m) = mk_tac'_ tac;

val Appl m = applicable_in p pt m;

member op = specsteps mI; (*false*)

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

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

(*val (msg, cs') = solve m (pt, pos);*)

"~~~~~ fun solve , args:"; val ((mI,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 (progr, cstate, istate, ctxt, tac)

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

       val srls = get_simplifier cstate;

         (*case*) execute_progr_2 srls m cstate (progr, e_rls(*!!!*)) (istate, ctxt)(*of*);

"~~~~~ fun execute_progr_2 , args:"; val (((*thy',*) srls), m, (pt, p), (scr as Rule.Prog sc, d), (Istate.Pstate (E,l,a,v,S,b), ctxt))

  = (srls, m, cstate, (progr, e_rls(*!!!*)), (istate, ctxt));

   (*if*)l = [] orelse ((*init.in solve..Apply_Method...*)

			         (last_elem o fst) p = 0 andalso snd p = Res) (*else*);

(*val Assoc (iss as (is as (_,_,_,_,_,bb), ss as ((m',f',pt',p',c')::_))) =

    (astep_up (thy',srls,scr,d) ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]) );*)

"~~~~~ fun astep_up, args:"; val ((ys as (_,_,Prog sc,_)), ((E,l,a,v,S,b),ss))

  = ((ctxt,srls,scr, (pt, p)), ((E,l,a,v,S,b), m));

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

val up = drop_last l;

           ass_up ys ((E,up,a,v,S,b),ss) (go up sc);

"~~~~~ fun ass_up, args:"; val (ysa, iss, (Const ("Tactical.Try",_) $ e)) =

                                             (ys, ((E,up,a,v,S,b),ss), (go up sc));

           astep_up ysa iss;

"~~~~~ and astep_up , args:"; val ((ys as (_,_,Rule.Prog sc,_)), ((E,l,a,v,S,b),ss)) = (ysa, iss);

  (*if*) 1 < length l; (*then*)

  val up = drop_last l;

           ass_up ys ((E,up,a,v,S,b),ss) (go up sc);

"~~~~~ fun ass_up , args:"; val (ysa, iss, (Const ("Tactical.Seq",_) $ _ $ _ )) = (ys, ((E,up,a,v,S,b),ss), (go up sc));

           astep_up ysa iss (*2*: comes from e2*);

"~~~~~ and astep_up , args:"; val ((ys as (_,_,Rule.Prog sc,_)), ((E,l,a,v,S,b),ss)) = (ysa, iss);

  (*if*) 1 < length l; (*then*)

  val up = drop_last l;

           ass_up ys ((E,up,a,v,S,b),ss) (go up sc);

"~~~~~ fun ass_up , args:"; val (ysa, iss, (Const ("Tactical.Seq",_) $ _ $ _ $ _)) = (ys, ((E,up,a,v,S,b),ss), (go up sc));

       astep_up ysa iss (*all has been done in (*2*) below*);

"~~~~~ and astep_up , args:"; val ((ys as (_,_,Rule.Prog sc,_)), ((E,l,a,v,S,b),ss)) = (ysa, iss);

  (*if*) 1 < length l; (*then*)

  val up = drop_last l;

           ass_up ys ((E,up,a,v,S,b),ss) (go up sc);

"~~~~~ fun ass_up , args:"; val ((ys as (ctxt,s,Rule.Prog sc,d)), ((E,l,a,v,S,b),ss), (Const ("HOL.Let",_) $ _))

  = (ys, ((E,up,a,v,S,b),ss), (go up sc));

	    val l = drop_last l; (*comes from e, goes to Abs*)

      val (i, T, body) =

        (case go l sc of

           Const ("HOL.Let",_) $ _ $ (Abs (i, T, body)) => (i, T, body)

         | t => error ("ass_up..HOL.Let $ _ with " ^ Rule.term2str t))

      val i = TermC.mk_Free (i, T);

      val E = Env.upd_env E (i, v);

  (*case*) assy (ctxt,s,d,Aundef) ((E, l @ [Celem.R, Celem.D], a,v,S,b),ss) body (*of*);

"~~~~~ fun assy , args:"; val (ya, ((E,l,a,v,S,b),ss), (Const ("HOL.Let",_) $ e $ (Abs (id,T,body))))

  = ((ctxt,s,d,Aundef), ((E, l @ [Celem.R, Celem.D], a,v,S,b),ss), body);

  (*case*) assy ya ((E , l @ [Celem.L, Celem.R], a,v,S,b), ss) e (*of*);

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

"~~~~~ fun assy , args:"; val ((ctxt,sr,(pt,p),ap), ((E,l,a,v,S,_), m), t)

  = (ya, ((E , l @ [Celem.L, Celem.R], a,v,S,b), ss), e);

(*val (a', STac stac) = ( *case*) Lucin.handle_leaf "locate" "Isac_Knowledge" sr (E, (a, v)) t (*of*);

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

  = ("locate", "Isac_Knowledge", sr, (E, (a, v)), t);

    val (a', STac stac) = (*case*) Prog_Tac.subst_stacexpr E a v t (*of*);

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

  = (E, a, v, t);

     (NONE, STac (subst_atomic E t)); (*return value*)

"~~~~~ from subst_stacexpr to handle_leaf return val:"; val ((a', STac stac))

  = ((NONE : term option, STac (subst_atomic E t)));

        val stac' =

            Rewrite.eval_listexpr_ (Celem.assoc_thy thy) srls (subst_atomic (upd_env_opt E (a,v)) stac);

                                 (*return value*) (a', STac stac');

"~~~~~ from handle_leaf to assy return val:"; val (a', STac stac)

  = ((a' : term option, STac stac'));

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

(*+*)if is_e_ctxt ctxt then error "ERROR: assy 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";