(* Title:  "Minisubpbl/200-start-method-NEXT_STEP.sml"

    Author: Walther Neuper 1105

    (c) copyright due to lincense terms.

 *)

 open Rewrite;

 open Pos;

 open TermC;

 "----------- Minisubplb/200-start-method-NEXT_STEP.sml ---------------------------------------";

 "----------- Minisubplb/200-start-method-NEXT_STEP.sml ---------------------------------------";

 "----------- Minisubplb/200-start-method-NEXT_STEP.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'))];

 (*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Model_Problem*)

 (*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Specify_Theory "Test"*)

 (*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Specify_Problem ["sqroot-test", "univariate", "equation", "test"*)

 (*[], Met*)val return_Step_do_next_Specify_Problem = Step.do_next p ((pt, e_pos'), []);(*Specify_Method ["Test", "squ-equ-test-subpbl1"]*)

 (*/------------------- step into Step.do_next_Specify_Problem ------------------------------\\*)

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

   (p, ((pt, e_pos'), []));

   (*if*) Pos.on_calc_end ip (*else*);

       val (_, probl_id, _) = Calc.references (pt, p);

 val _ =

       (*case*) tacis (*of*);

         (*if*) probl_id = Problem.id_empty (*else*);

       Step.switch_specify_solve p_ (pt, ip);

 "~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));

       (*if*) Pos.on_specification ([], state_pos) (*then*);

       Step.specify_do_next (pt, input_pos);

 "~~~~~ fun specify_do_next , args:"; val ((ptp as (pt, (p, p_)))) = ((pt, input_pos));

     val (_, (p_', tac)) = Specify.find_next_step ptp

     val ist_ctxt =  Ctree.get_loc pt (p, p_)

 val _ =

     (*case*) tac (*of*);

 Step_Specify.by_tactic_input tac (pt, (p, p_'));

 "~~~~~ fun by_tactic_input , args:"; val ((Tactic.Specify_Method id), (pt, pos)) =

   (tac, (pt, (p, p_')));

       val (o_model, ctxt, i_model) =

 Specify_Step.complete_for id (pt, pos);

 "~~~~~ fun complete_for , args:"; val (mID, (ctree, pos)) = (id, (pt, pos));

     val {origin = (o_model, _, _), probl = i_prob, ctxt,

        ...} = Calc.specify_data (ctree, pos);

     val {model = m_patt, where_, where_rls, ...} = MethodC.from_store ctxt mID

     val {origin = (root_model, _, _), ...} = Calc.specify_data (ctree, ([], Pos.Und))

     val (o_model', ctxt') = O_Model.complete_for m_patt root_model (o_model, ctxt)

     val (_, (i_model, _)) =

    M_Match.match_itms_oris ctxt i_prob (m_patt, where_, where_rls) o_model';

 "~~~~~ fun match_itms_oris , args:"; val (ctxt, pbl, (pbt, where_, where_rls), oris) =

   (ctxt, i_prob, (m_patt, where_, where_rls), o_model');

  (*0*)val mv = Pre_Conds.max_variant pbl;

       fun eqdsc_pbt_itm ((_,(d,_))) (_, _, _, _, itm_) = d = I_Model.descriptor itm_;

       fun notmem pbl pbt1 = case find_first (eqdsc_pbt_itm pbt1) pbl of

 				SOME _ => false | NONE => true;

  (*1*)val mis = (filter (notmem pbl)) pbt;

       fun eqdsc_ori (_,(d,_)) (_, _, _, d', _) = d = d';

       fun ori2itmMis (f, (d, pid)) (i, v, _, _, _) = (i, v, false, f, I_Model.Mis (d, pid));

  (*2*)fun oris2itms oris mis1 = ((map (ori2itmMis mis1)) o (filter (eqdsc_ori mis1))) oris;

       val news = (flat o (map (oris2itms oris))) mis;

  (*3*)fun mem_vat (_, vats, _, _, _) = member op = vats mv;

       val newitms = filter mem_vat news;

  (*4*)val itms' = pbl @ newitms;

       val (pb, where_') =

  Pre_Conds.check ctxt where_rls where_ itms' mv;

 "~~~~~ fun check , args:"; val (ctxt, where_rls, pres, pbl, (_)) =

   (ctxt, where_rls, where_, itms', mv);

       val env = Pre_Conds.environment pbl;

       val pres' = map (TermC.subst_atomic_all env) pres;

 (*+*)val "Test" = ctxt |> Proof_Context.theory_of  |> ThyC.id_of

 (*+*)val Rule_Set.Repeat {id = "prls_met_test_squ_sub", ...} = where_rls

 (*+*)val [(true, tTEST as Const ("Test.precond_rootmet", _) $ Free ("x", xxx))] = pres'

 (*+*)val ctxt = Config.put rewrite_trace true ctxt;

       val evals = map (

  Pre_Conds.eval ctxt where_rls) pres';

 (* (*declare [[rewrite_trace = true]]*)

 @## rls: prls_met_test_squ_sub on: precond_rootmet x 

 @### try calc: "Test.precond_rootmet" 

 @#### eval asms: "(precond_rootmet x) = True" 

 @### calc. to: True 

 @### try calc: "Test.precond_rootmet" 

 @### try calc: "Test.precond_rootmet" 

 *)

 (*+*)val ctxt = Config.put rewrite_trace false ctxt;

 "~~~~~ fun eval_precond_rootmet , args:"; val ((thmid:string), _, (t as (Const (\<^const_name>\<open>Test.precond_rootmet\<close>, _) $ arg)), ctxt) =

   ("aaa", "bbb", tTEST, ctxt);

     SOME (TermC.mk_thmid thmid (UnparseC.term ctxt arg) "",

       HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))

 ;

     (TermC.mk_thmid thmid (UnparseC.term ctxt arg)) "";

 "~~~~~ fun mk_thmid , args:"; val (thmid, n1, n2) = (thmid, (UnparseC.term ctxt arg), "");

   thmid ^ (cut_longid n1) ^ "_" ^ (cut_longid n2);

       (cut_longid n2);

 "~~~~~ fun cut_longid , args:"; val (dn) = (n2);

 (*\------------------- step into Step.do_next_Specify_Problem ------------------------------//*)

 val (_, ([(tac, _, _)], _, (pt, p))) = return_Step_do_next_Specify_Problem

 (*[1], Frm*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Apply_Method ["Test", "squ-equ-test-subpbl1"]*)

 (*[1], Res*)val return_Step_do_next_Apply_Method = Step.do_next p ((pt, e_pos'), []);(*Rewrite_Set "norm_equation"*)

 (*/------------------- step into Apply_Method ----------------------------------------------\\*)

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

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

   (*if*) Pos.on_calc_end ip (*else*);

       val (_, probl_id, _) = Calc.references (pt, p);

 val _ =

       (*case*) tacis (*of*);

         (*if*) probl_id = Problem.id_empty (*else*);

       Step.switch_specify_solve p_ (pt, ip);

 "~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos))

   = (p_, (pt, ip));

       (*if*) Pos.on_specification ([], state_pos) (*else*);

         LI.do_next (pt, input_pos);

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

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

 	      val ((ist, ctxt), sc) = LItool.resume_prog (p,p_) pt;

 val return_LI_find_next_step = (*case*)

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

 (*//------------------ step into LI.find_next_step -----------------------------------------\\*)

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

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

 (*.. this showed that we have ContextC.empty*)

 (*\\------------------ step into XXXXX -----------------------------------------------------//*)

 val LI.Next_Step (ist, ctxt, tac) = return_LI_find_next_step;

         LI.by_tactic tac (ist, Tactic.insert_assumptions tac ctxt) ptp;

 "~~~~~ fun by_tactic , args:"; val (tac_, ic, (pt, pos))

   = (tac, (ist, Tactic.insert_assumptions tac ctxt), ptp);

       val pos = next_in_prog' pos

  	    val (pos', c, _, pt) =

 Solve_Step.add_general tac_ ic (pt, pos);

 "~~~~~ fun add_general , args:"; val (tac, ic, cs)

   = (tac_, ic, (pt, pos));

  (*if*) Tactic.for_specify' tac (*else*);

 Solve_Step.add tac ic cs;

 "~~~~~ fun add , args:"; val ((Tactic.Rewrite_Set' (_, _, rls', f, (f', asm))), (is, ctxt), (pt, (p, _)))

   = (tac, ic, cs);

       val (pt, c) = Ctree.cappend_atomic pt p (is, ctxt) f 

         (Tactic.Rewrite_Set (Rule_Set.id rls')) (f', asm) Ctree.Complete

       val pt = Ctree.update_branch pt p Ctree.TransitiveB

 val return =

       ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term ctxt f'), pt)

 (*\------------------- step into Apply_Method ----------------------------------------------//*)

 val (_, ([(tac, _, _)], _, (pt, p))) = return_Step_do_next_Apply_Method

 (*[2], Res*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Rewrite_Set "Test_simplify"*)

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

 (*+*)val ([2], Res) = p;

 Test_Tool.show_pt_tac pt; (*[

 ([], Frm), solve (x + 1 = 2, x)

 . . . . . . . . . . Apply_Method ["Test", "squ-equ-test-subpbl1"], 

 ([1], Frm), x + 1 = 2

 . . . . . . . . . . Rewrite_Set "norm_equation", 

 ([1], Res), x + 1 + - 1 * 2 = 0

 . . . . . . . . . . Rewrite_Set "Test_simplify", 

 ([2], Res), - 1 + x = 0

 . . . . . . . . . . Check_Postcond ["sqroot-test", "univariate", "equation", "test"]]   ..INCORRECT

 *)