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

   Author: Walther Neuper 1105

   (c) copyright due to lincense terms.

*)

open Istate;

open LI;

"----------- 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) = Test_Code.init_calc @{context} [(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; val Apply_Method ["Test", "squ-equ-test-subpbl1"] = nxt;

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

(*[1], Res*)val return_me_Rewrite_Set_norm_equation = me nxt p [] pt;

(*//------------------ step into Rewrite_Set "norm_equation" -------------------------------\\*)

"~~~~~ 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 (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 prog_rls = LItool.get_simplifier cstate;

  (*case*) scan_to_tactic1 (progr, (cstate, ctxt, tac)) istate (*of*);

"~~~~~ fun scan_to_tactic1 , args:"; val ((prog, (cctt as ((_, p), _, _))), (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 ctxt 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*) LItool.check_leaf "locate" ctxt eval (get_subst ist) t (*of*);

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

    LItool.associate (pt, p) 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 (p,p_) pt;

	      val Next_Step (_, _, _) =

           (*case*)  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 ctxt path prog);

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

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

(*\\------------------ step into Rewrite_Set "norm_equation" -------------------------------//*)

val (p,_,f,nxt,_,pt) = return_me_Rewrite_Set_norm_equation; val Rewrite_Set "Test_simplify" = nxt;

(*[2], Res*)val return_Rewrite_Set_Test_simplify = me nxt p [] pt;

(*//------------------ step into Rewrite_Set "Test_simplify" -------------------------------\\*)

(*+*)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 (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 ctxt path prog);

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

  = (yyy, (ist |> path_up), (go_up ctxt 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 ctxt path prog);

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

  = (yyy, (ist |> path_up), (go_up ctxt 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 ctxt path prog);

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

  = (yyy, (ist |> path_up), (go_up ctxt 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 ctxt 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 ctxt path prog));

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

(*//------------------ revive with CS: push through ctxt to Tactic.Subproblem --------------\\* )

        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, pos) 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 = Sub_Problem.common_sub_thy (Know_Store.get_via_last_thy dI, Ctree.root_thy pt);

      val init_ctxt = Proof_Context.init_global thy

	    val ags = TermC.isalist2list ags';

	    val (pI, pors, mI) = 

	      if mI = ["no_met"]

	      then

          let

            val pors = (M_Match.arguments thy ((#model o (Problem.from_store init_ctxt)) pI) ags): O_Model.T

		          handle ERROR "actual args do not match formal args"

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

		        val pI' = Refine.by_o_model' init_ctxt pors pI;

		      in (pI', pors (* refinement over models with diff.prec only *), 

		          (hd o #solve_mets o Problem.from_store init_ctxt) pI') end

	      else (pI, (M_Match.arguments thy ((#model o Problem.from_store init_ctxt) pI) ags)

		      handle ERROR "actual args do not match formal args"

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

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

	    val {cas, model, thy, ...} = Problem.from_store init_ctxt pI

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

	    val dI = Context.theory_name

        (Sub_Problem.common_sub_thy (Know_Store.get_via_last_thy dI, Ctree.root_thy pt))

	    val ctxt = ContextC.init_for_prog init_ctxt vals

( *\\------------------ revive with CS: push through ctxt to Tactic.Subproblem --------------//*)

(*\\------------------ step into Rewrite_Set "Test_simplify" -------------------------------//*)

val (p,_,f,nxt,_,pt) =  return_Rewrite_Set_Test_simplify; val Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"]) = nxt;

(* final test ... ----------------------------------------------------------------------------*)

if pos = ([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";