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

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

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

(*+*)if p'''' = ([1],  Frm) andalso f'''' = Test_Out.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";

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

val ("ok", (_, _, ptp''''')) = (*case*)

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

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

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

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

Step_Solve.by_tactic m ptp;

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

  (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (* = else*);

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

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

  val Safe_Step (_, _, Rewrite_Set' (_, _, Rule_Set.Repeat {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 (\<^const_name>\<open>Let\<close>, _) $ e $ (Abs (id, T, b))))

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

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

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

"~~~~~ fun scan_dn1, args:"; val ((xxx as (cstate, _, _)), ist, (Const (\<^const_name>\<open>Chain\<close>(*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 (\<^const_name>\<open>Try\<close>(*1*),_) $ e)) =

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

(*+*)UnparseC.term 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*) check_leaf "locate" ctxt eval (get_subst ist) t (*of*);

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

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

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

      (Const (\<^const_name>\<open>Rewrite_Set\<close>, _) $ rls_ $ f_)) = (pt, ctxt, m, stac);

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

"~~~~~ continue me[1] after Step.by_tactic";

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

(* isabisac17: val ("helpless", _) = (*case*) Step.do_next 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_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);

   MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) = false;

    (*if*) MethodC.id_empty = 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) = LItool.resume_prog thy' (p,p_) pt;

	      val Next_Step (_, _, _) =

           (*case*)  LI.find_next_step sc (pt, pos) ist ctxt (*of*);

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

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

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

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

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

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

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

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

           go_scan_up (prog, cct) (trans_scan_up ist |> set_found);

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

  ((prog, cct), (trans_scan_up ist |> set_found));

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

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

"~~~~~ fun scan_up , args:"; val (yyy, ist, (Const (\<^const_name>\<open>Try\<close>(*2*), _) $ _)) =

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

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

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

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

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

(*+*)val p'''''_'' = p; (* keep for final test*)

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

    val (pt, p) = 

	    (*Step.by_tactic is here for testing by me; step would suffice in me*)

	    case Step.by_tactic 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.do_next 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_ (**else*);

           Step_Solve.do_next (pt, ip);

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

    (*if*) MethodC.id_empty = 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) = LItool.resume_prog thy' (p,p_) pt;

	      val Next_Step (_, _, _) =

           (*case*)  LI.find_next_step sc (pt, pos) ist ctxt (*of*);

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

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

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

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

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

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

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

       go_scan_up (prog, cc) (trans_scan_up ist |> set_found);

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

  = ((prog, cct), (trans_scan_up ist |> set_found));

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

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

"~~~~~ and scan_up , args:"; val (yyy, ist, (Const (\<^const_name>\<open>Try\<close>(*1*),_) $ _ ))

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

           go_scan_up yyy (ist |> set_found);

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

  = (yyy, (ist |> set_found));

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

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

"~~~~~ and scan_up , args:"; val (yyy, ist, (Const (\<^const_name>\<open>Chain\<close>(*2*), _) $ _ $ _))

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

           go_scan_up yyy ist;

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

  = (yyy, ist);

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

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

"~~~~~ fun scan_up , args:"; val (yyy, ist, (Const (\<^const_name>\<open>Chain\<close>(*1*), _) $ _ $ _ $ _))

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

           go_scan_up yyy ist;

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

  = (yyy, ist);

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

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

"~~~~~ fun scan_up , args:"; val ((yyy as (prog, xxx)), (ist as {found_accept, ...}), (Const (\<^const_name>\<open>Let\<close>(*1*), _) $ _))

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

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

        val (i, body) = check_Let_up ist prog;

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

"~~~~~ fun scan_dn , args:"; val (xxx, ist, (Const (\<^const_name>\<open>Let\<close>(*1*),_) $ e $ (Abs (i,T,b))))

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

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

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

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

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

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

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

   (*val m =*)

Sub_Problem.tac_from_prog pt stac;

"~~~~~ fun tac_from_prog , args:"; val (pt, _, (stac as Const (\<^const_name>\<open>SubProblem\<close>, _) $ spec' $ ags'))

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

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

      val thy = ThyC.sub_common (ThyC.get_theory dI, rootthy pt);

	    val ags = TermC.isalist2list ags';

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

	    val (pI, pors, mI) = 

        (pI, (M_Match.arguments thy ((#ppc o Problem.from_store) pI) ags)

		       handle ERROR "actual args do not match formal args"

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

      val (fmz_, vals) = O_Model.values' pors;

	    val {cas,ppc,thy,...} = Problem.from_store pI

	    val dI = Context.theory_name thy (*.take dI from _refined_ pbl.*)

	    val dI = Context.theory_name (ThyC.sub_common (ThyC.get_theory dI, rootthy pt));

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

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

val p = p'''''_''; (*kept from before stepping into detail*)

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";