(* 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" andalso fst nxt'''' = "Rewrite_Set"

then () 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: assy: call by ([3], Pbl) *)

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

(*ERROR WAS: assy: 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 Chead.Appl m = (*case*) Applicable.applicable_in p pt m (*of*);

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

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

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

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

    (* step somewhere within a calculation *)

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

Celem.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) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;

   locate_input_tactic sc (pt, po) (fst is) (snd is) m;  (* assy: call by ([3], Pbl)*)

"~~~~~ 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 ((last_elem o fst) p = 0 andalso snd p = Res) (*then*);

(*val Assoc (scrstate, steps) =     in isabisacREP*)

(*ERROR  assy: call by ([3], Pbl)   in isabisac*)

assy (ctxt,srls,d,Aundef) ((E,[Celem.R],a,v,S,b), [(m,Generate.EmptyMout,pt,p,[])]) (Program.body_of sc);  

(* checked all arguments of assy for equality: isabisac -- isabisacREP *)

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

  (((*thy',*)ctxt,srls,d,Aundef), ((E,[Celem.R],a,v,S,b), [(m,Generate.EmptyMout,pt,p,[])]), (Program.body_of sc));

(*val Assoc (scrstate, steps) =    in isabisacREP*)

(*val NasApp ((E',l,a,v,S,_),ss) = in isabisac*) assy ya ((E , l @ [Celem.L, Celem.R], a,v,S,b), ss) e;

"~~~~~ fun assy, args:"; val (ya, ((E,l,_,v,S,b),ss:step list), (Const ("Tactical.Seq"(*2[1]*),_) $e1 $ e2 $ a)) =

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

(*val Assoc (scrstate, steps) =    in isabisacREP*)

(*val NasApp ((E,_,_,v,_,_),ss) =  in isabisac*)

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

"~~~~~ fun assy, args:"; val (ya, ((E,l,a,v,S,b),ss), (Const ("Tactical.Try"(*1*),_) $ e)) =

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

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

term2str e1 = "Try (Rewrite_Set norm_equation)"      (*in isabisacREP*);

termopt2str a = "(SOME e_e)"  (*in isabisac + isabisacREP*);

(*val Assoc (scrstate, steps) =    in isabisacREP*)

(*val NasApp ((E,_,_,v,_,_),ss) =  in isabisac*)

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

    (*here is not a tactical like TRY etc, but a tactic creating a step in calculation*)

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

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

val (a', STac stac) = (*case*) handle_leaf "locate" thy' sr E a v t (*of*)

           val p' = 

             case p_ of Frm => p 

             | Res => lev_on p

		         | _ => error ("assy: call by " ^ pos'2str (p,p_));

(*val Ass (m,v') = in isabisacREP*)

(*val NotAss =     in isabisac*)

(*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, Ctree.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 = ([], Ctree.Res) = false;

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

(*if*) ip = p = false;

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

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

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

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

(* isabisac17: val (tac_, is, (t, _)) = determine_next_tactic (thy', srls) (pt, pos) sc is;

go: no [L,L,R] *)

"~~~~~ fun determine_next_tactic, args:"; val (thy, (ptp as (pt, (p, _))), (sc as Prog (_ $ body)), 

	    (Pstate (E,l,a,v,s,_), ctxt) ) = ((thy', srls), (pt, pos), sc, is);

(*if*) l = [] = false;

(* isabisac17:                             nstep_up thy ptp sc E l Skip_ a v   ERROR go: no [L,L,R] *)

(* isabisac15: val Appy (tac_, scrstate) = nstep_up thy ptp sc E l Skip_ a v *)

"~~~~~ fun nstep_up, args:"; val (thy, ptp, (Prog sc), E, l, ay, a, v) =

  (thy, ptp, sc, E, l, Skip_, a, v);

1 < length l = true;

val up = drop_last l; 

if up = [R, L, R, L, L, R] then () else error "250-Rewrite_Set: nstep_up CHANGED";

(*isabisac17: nxt_up thy ptp (Celem.Prog sc) E up ay (go up sc) a v    ERROR go: no [L,L,R]*)

(*isabisac17:                                        (go up sc)        ERROR go: no [L,L,R]*)

(*isabisac15:*)

val ttt as Const ("Tactical.Try", _) $ (Const ("Prog_Tac.Rewrite'_Set", _) $ rls) = (go up sc)

val (Const ("Tactical.Try"(*2*), _) $ _) = ttt;

if term2str ttt = "Try (Rewrite_Set ''norm_equation'')"

then () else error "250-Rewrite_Set: (go up sc) CHANGED";

"~~~~~ fun nxt_up, args:"; val (thy, ptp, scr, E, l, _, (Const ("Tactical.Try"(*2*), _) $ _), a, v) =

  (thy, ptp, (Prog sc), E, up, ay, (go up sc), a, v );

(*\\--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, Ctree.e_pos'), []) (*of*);

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

  = (p, ((pt, Ctree.e_pos'), []));

     val pIopt = get_pblID (pt,ip);

    (*if*) ip = ([], Ctree.Res) (*else*);

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

      val SOME _ = (*case*) pIopt (*of*);

      (*if*) member op = [Ctree.Pbl, Ctree.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, is, sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;

	      (*val (tac_, is, (t, _)) =*) determine_next_tactic (thy', srls) (pt, pos) sc is;

"~~~~~ fun determine_next_tactic , args:"; val (thy, (ptp as (pt, (p, _))), sc, (Istate.Pstate (E,l,a,v,s,_), ctxt))

  = ((thy', srls), (pt, pos), sc, is);

     (*case*) execute_progr_1 thy ptp sc (Istate.Pstate (E,l,a,v,s,false)) (*of*);

"~~~~~ fun execute_progr_1 , args:"; val (thy, ptp, (sc as Rule.Prog prog), (Istate.Pstate (E, l, a, v, _, _)))

  = (thy, ptp, sc, (Istate.Pstate (E,l,a,v,s,false)));

    (*if*) l = [] (*else*);

      nstep_up thy ptp sc E l Skip_ a v;

"~~~~~ and nstep_up , args:"; val (thy, ptp, (Rule.Prog sc), E, l, ay, a, v)

  = (thy, ptp, sc, E, l, Skip_, a, v);

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

    val up = drop_last l; 

           nxt_up thy ptp (Rule.Prog sc) E up ay (go up sc) a v;

"~~~~~ fun nxt_up , args:"; val (thy, ptp, scr, E, l, _, (Const ("Tactical.Try"(*1*),_) $ _ ), a, v)

  = (thy, ptp, (Rule.Prog sc), E, up, ay, (go up sc), a, v);

           nstep_up thy ptp scr E l Skip_ a v;

"~~~~~ and nstep_up , args:"; val (thy, ptp, (Rule.Prog sc), E, l, ay, a, v)

  = (thy, ptp, scr, E, l, Skip_, a, v);

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

    val up = drop_last l; 

           nxt_up thy ptp (Rule.Prog sc) E up ay (go up sc) a v;

"~~~~~ fun nxt_up , args:"; val (thy, ptp, scr, E, l, ay, (Const ("Tactical.Seq"(*2*), _) $ _ $ _), a, v)

  = (thy, ptp, (Rule.Prog sc), E, up, ay, (go up sc), a, v);

    nstep_up thy ptp scr E l ay a v;

"~~~~~ and nstep_up , args:"; val (thy, ptp, (Rule.Prog sc), E, l, ay, a, v)

  = (thy, ptp, scr, E, l, ay, a, v);

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

    val up = drop_last l; 

           nxt_up thy ptp (Rule.Prog sc) E up ay (go up sc) a v;

"~~~~~ fun nxt_up , args:"; val (thy, ptp, scr, E, l, ay, (Const ("Tactical.Seq"(*1*), _) $ _ $ _ $ _), a, v)

  = (thy, ptp, (Rule.Prog sc), E, up, ay, (go up sc), a, v);

           nstep_up thy ptp scr E l ay a v;

"~~~~~ and nstep_up , args:"; val (thy, ptp, (Rule.Prog sc), E, l, ay, a, v)

  = (thy, ptp, scr, E, l, ay, a, v);

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

    val up = drop_last l; 

           nxt_up thy ptp (Rule.Prog sc) E up ay (go up sc) a v;

"~~~~~ fun nxt_up , args:"; val (thy, ptp, scr, E, l, ay, (Const ("HOL.Let", _) $ _), a, v)

  = (thy, ptp, (Rule.Prog sc), E, up, ay, (go up sc), a, v);

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

        val up = drop_last l

        val (i, T, body) =

          (case go up sc of

             Const ("HOL.Let",_) $ _ $ (Abs aa) => aa

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

        val i = TermC.mk_Free (i, T)

        val E = upd_env E (i, v);

  (*case*) appy thy ptp E (up @ [Celem.R, Celem.D]) body a v (*of*);

"~~~~~ fun appy , args:"; val (thy, ptp, E, l, (Const ("HOL.Let",_) $ e $ (Abs (i,T,b))), a, v)

  = (thy, ptp, E, (up @ [Celem.R, Celem.D]), body, a, v);

  (*case*) appy thy ptp E (l @ [Celem.L, Celem.R]) e a v (*of*);

"~~~~~ fun appy , args:"; val (((th,sr)), (pt, p), E, l, t, a, v)

  = (thy, ptp, E, (l @ [Celem.L, Celem.R]), e, a, v);

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

   (*val (m,m') = Lucin.*) stac2tac_ pt (Celem.assoc_thy th) stac;

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

  = (pt, (Celem.assoc_thy th), 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", 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*)