(* Title:  "Minisubpbl/250-Rewrite_Set-from-method.sml"

   Author: Walther Neuper 1105

   (c) copyright due to lincense terms.

*)

"----------- Minisubpbl/250-Rewrite_Set-from-method.sml ----------";

"----------- Minisubpbl/250-Rewrite_Set-from-method.sml ----------";

"----------- Minisubpbl/250-Rewrite_Set-from-method.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 begin step into relevant call -----------^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^-----\\

      1 relevant for original decomposition                                                     *)

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

if p'''' = ([1],  Frm) andalso f'''' = FormKF "x + 1 = 2"

then case nxt'''' of Rewrite_Set _ => () | _ => error "start of test CHANGED 1"

else error "250-Rewrite_Set-from-method.sml: start of test CHANGED";

(* val (p,_,f,nxt,_,pt) = ERROR WAS: nxt = ("Empty_Tac",..*) me nxt p [] pt;

(*                        ERROR WAS: scan_dn1: call by ([3], Pbl) *)

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

(*ERROR WAS: scan_dn1: call by ([3], Pbl)*)

val ("ok", (_, _, ptp''''')) = (*case*) locatetac tac (pt,p) (*of*);

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

      val (mI, m) = Solve.mk_tac'_ tac;

val Applicable.Appl m = (*case*) Applicable.applicable_in p pt m (*of*);

member op = Solve.specsteps mI (* = false*);

           loc_solve_ m ptp ;  (* scan_dn1: call by ([3], Pbl)*)

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

           solve m (pt, pos);  (* scan_dn1: call by ([3], Pbl)*)

    (* ======== general tactic as fall through ======== *)

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

  (*if*) Celem.e_metID = get_obj g_metID pt (par_pblobj pt p) (* = else*);

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

	      val (_, is, sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;

  val Safe_Step (_, _, Rewrite_Set' (_, _, Rls {id = "norm_equation", ...}, _, _)) = (*case*)

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

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

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

       val srls = get_simplifier cstate;

         (*case*) scan_to_tactic1 (progr, (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) (*then*);

           scan_dn1 cctt (ist |> set_path [R] |> set_or ORundef) (Program.body_of prog);

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

  = (cctt, (ist |> set_path [R] |> set_or ORundef), (Program.body_of prog));

val Accept_Tac1 (_, _, Rewrite_Set' (_, _, Rls {id = "norm_equation", ...}, _, _)) = (*case*)

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

"~~~~~ fun scan_dn1, args:"; val ((xxx as (cstate, _, _)), ist, (Const ("Tactical.Chain"(*1*),_) $e1 $ e2 $ a)) =

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

val Accept_Tac1 _ =  (*case*)

           scan_dn1 xxx (ist |> path_down_form ([L, L, R], a)) e1 (*of*);

"~~~~~ fun scan_dn1, args:"; val (xxx, ist, (Const ("Tactical.Try"(*1*),_) $ e)) =

  (xxx, (ist |> path_down_form ([L, L, R], a)), e1);

(*+*)term2str e1 = "Try (Rewrite_Set ''norm_equation'')"  (*in isabisac*);

val Accept_Tac1 _ =  (*case*)

           scan_dn1 xxx (ist |> path_down_form ([L, R], a)) e (*of*);

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

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

  (xxx, (ist |> path_down_form ([L, R], a)), e);

val (Program.Tac stac, a') = (*case*) interpret_leaf "locate" ctxt eval (get_subst ist) t (*of*);

val Ass (Rewrite_Set' _, _, _) = (*case*)

           associate pt ctxt (m, stac) (*of*);

"~~~~~ fun associate, args:"; val (_, ctxt, (m as Tactic.Rewrite_Set' (_, _, rls, f, (f', _))), 

      (Const ("Prog_Tac.Rewrite'_Set", _) $ rls_ $ f_)) = (pt, d, m, stac);

(*+*)if Rule.id_rls rls = HOLogic.dest_string rls_ then () else error "Prog_Tac.associate changed";

"~~~~~ continue me[1] after locatetac";

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

(* isabisac17: val ("helpless", _) = (*case*) step p ((pt, Pos.e_pos'),[]) (*of*)*)

"~~~~~ 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) = false;

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

(*if*) ip = p = false;

(*if*) member op = [Pbl, Met] p_ = false;

"~~~~~ and do_solve_step , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);

   e_metID = get_obj g_metID pt (par_pblobj pt p) = false;

    (*if*) Celem.e_metID = get_obj g_metID pt (par_pblobj pt p)(*else*);

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

	      val (_, (ist, ctxt), sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;

	      val Next_Step (_, _, _) =

           (*case*)  find_next_tactic sc (pt, pos) ist ctxt (*of*);

"~~~~~ fun find_next_tactic , args:"; val ((Rule.Prog prog), (ptp as(pt, (p, _))), Istate.Pstate ist, ctxt)

  = (sc, (pt, pos), ist, ctxt);

val Accept_Tac2 (Rewrite_Set' _, _, _) = (*case*)

           scan_to_tactic2 (prog, (ptp, ctxt)) (Istate.Pstate ist) (*of*);

"~~~~~ fun scan_to_tactic2 , args:"; val ((prog, cct), (Istate.Pstate (ist as {path, ...})))

  = ((prog, (ptp, ctxt)), (Istate.Pstate ist));

  (*if*) 0 = length path (*else*);

val Accept_Tac2 (Rewrite_Set' _, _, _) =

           go_scan_up2 (prog, cct) (trans_scan_up2 ist |> set_appy Skip_);

"~~~~~ and go_scan_up2 , args:"; val ((yyy as (prog, _)), (ist as {env, path, finish, ...})) =

  ((prog, cct), (trans_scan_up2 ist |> set_appy Skip_));

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

           scan_up2 yyy (ist |> path_up) (go_up path prog);

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

  (yyy, (ist |> path_up), (go_up path prog));

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

(*                                               nxt'''_' = Rewrite_Set "Test_simplify"

  //--2 begin step into relevant call -----------^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^-----\\

      2 relevant for exception TERM raised (line 297 of "term.ML"): dest_Free -1 + x = 0                                                           *)

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

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

    val (pt, p) = 

	    (*locatetac is here for testing by me; step would suffice in me*)

	    case locatetac tac (pt, p) of

		    ("ok", (_, _, ptp)) => ptp

	    | ("unsafe-ok", (_, _, ptp)) => ptp

	    | ("not-applicable",_) => (pt, p)

	    | ("end-of-calculation", (_, _, ptp)) => ptp

	    | ("failure", _) => error "sys-error"

	    | _ => error "me: uncovered case"

  (*case*) step p ((pt, Pos.e_pos'), []) (*of*);

"~~~~~ fun step , args:"; val ((ip as (_, p_)), (ptp as (pt,p), tacis))

  = (p, ((pt, Pos.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)) (*else*);

           do_solve_step (pt, ip);

"~~~~~ and do_solve_step , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);

    (*if*) Celem.e_metID = get_obj g_metID pt (par_pblobj pt p) (*else*);

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

	      val (srls, (ist, ctxt), sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;

	      val Next_Step (_, _, _) =

           (*case*) find_next_tactic sc (pt, pos) ist ctxt (*of*);

"~~~~~ fun find_next_tactic , args:"; val (Rule.Prog prog, (ptp as(pt, (p, _))), Istate.Pstate ist, ctxt)

  = (sc, (pt, pos), ist, ctxt);

val Accept_Tac2 (_, _, _) = (*case*)

           scan_to_tactic2 (prog, (ptp, ctxt)) (Istate.Pstate ist) (*of*);

"~~~~~ fun scan_to_tactic2 , args:"; val ((prog, cct), (Istate.Pstate (ist as {path, ...})))

  = ((prog, (ptp, ctxt)), (Istate.Pstate ist));

    (*if*) 0 = length path (*else*);

       go_scan_up2 (prog, cc) (trans_scan_up2 ist |> set_appy Skip_);

"~~~~~ fun go_scan_up2 , args:"; val ((yyy as (prog, _)), (ist as {env, path, finish, ...}))

  = ((prog, cct), (trans_scan_up2 ist |> set_appy Skip_));

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

           scan_up2 yyy (ist |> path_up) (go_up path prog);

"~~~~~ and scan_up2 , args:"; val (yyy, ist, (Const ("Tactical.Try"(*1*),_) $ _ ))

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

           go_scan_up2 yyy (ist |> set_appy Skip_);

"~~~~~ fun go_scan_up2 , args:"; val ((yyy as (prog, _)), (ist as {env, path, finish, ...}))

  = (yyy, (ist |> set_appy Skip_));

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

           scan_up2 yyy (ist |> path_up) (go_up path prog);

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

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

           go_scan_up2 yyy ist;

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

  = (yyy, ist);

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

           scan_up2 yyy (ist |> path_up) (go_up path prog);

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

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

           go_scan_up2 yyy ist;

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

  = (yyy, ist);

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

           scan_up2 yyy (ist |> path_up) (go_up path prog);

"~~~~~ fun scan_up2 , args:"; val ((yyy as (prog, xxx)), (ist as {finish, ...}), (Const ("HOL.Let"(*1*), _) $ _))

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

    (*if*) finish = Napp_ (*else*);

        val (i, body) = check_Let_up ist prog;

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

"~~~~~ fun scan_dn2 , args:"; val (xxx, ist, (Const ("HOL.Let"(*1*),_) $ e $ (Abs (i,T,b))))

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

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

           scan_dn2 xxx (ist |> path_down [L, R]) e (*of*);

    (*========== a leaf has been found ==========*)   

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

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

        val (Program.Tac stac, a') = (*case*) Lucin.interpret_leaf  "next  " ctxt eval (get_subst ist) t (*of*);

   (*val (m,m') = Lucin.*) stac2tac_ pt (Proof_Context.theory_of ctxt) stac;

"~~~~~ fun stac2tac_ , args:"; val (pt, _, (stac as Const ("Prog_Tac.SubProblem", _) $ spec' $ ags'))

  = (pt, (Proof_Context.theory_of ctxt), stac);

      val (dI, pI, mI) = Prog_Tac.dest_spec spec'

      val thy = Stool.common_subthy (Celem.assoc_thy dI, rootthy pt);

	    val ags = TermC.isalist2list ags';

	      (*if*) mI = ["no_met"] (*else*);

	    val (pI, pors, mI) = 

        (pI, (Chead.match_ags thy ((#ppc o Specify.get_pbt) pI) ags)

		       handle ERROR "actual args do not match formal args"

		       => (Chead.match_ags_msg pI stac ags(*raise exn*); []), mI)

      val (fmz_, vals) = Chead.oris2fmz_vals pors;

	    val {cas,ppc,thy,...} = Specify.get_pbt pI

	    val dI = Rule.theory2theory' thy (*.take dI from _refined_ pbl.*)

	    val dI = Rule.theory2theory' (Stool.common_subthy (Celem.assoc_thy dI, rootthy pt));

      val ctxt = ContextC.initialise dI (map TermC.vars vals |> flat |> distinct);

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

if p = ([2], Res) andalso f2str f = "-1 + x = 0" then

  case nxt of

    (Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"])) => ()

  | _ => error "Minisubpbl/250-Rewrite_Set-from-method changed 1"

else error "Minisubpbl/250-Rewrite_Set-from-method changed 2";

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