(* Title:  "Minisubpbl/600-postcond-NEXT_STEP.sml"

   Author: Walther Neuper 200121

   (c) copyright due to lincense terms.

*)

"----------- Minisubplb/600-postcond-NEXT_STEP.sml -------------------------------------------";

"----------- Minisubplb/600-postcond-NEXT_STEP.sml -------------------------------------------";

"----------- Minisubplb/600-postcond-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) = CalcTreeTEST [(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*)

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

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

(*+*)if (get_istate_LI pt p |> the_pstate |> pstate2str)

 = "([], [], e_rls, NONE, \n??.empty, ORundef, false, false)"

then () else error "pstate changed after ([], Met)";

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

(*+*)if (get_istate_LI pt''''' p''''' |> the_pstate |> pstate2str)

 = "([\"\n(e_e, x + 1 = 2)\",\"\n(v_v, x)\"], [], e_rls, NONE, \n??.empty, ORundef, false, true)"

then () else error "pstate changed after ([1], Frm)"; (*this shall be corrected ...^^^^^^^^^: a tac has been found !!!*)

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

(*+*)if (get_istate_LI pt p |> the_pstate |> pstate2str)

(*= "([\"\n(e_e, x + 1 = 2)\",\"\n(v_v, x)\"], [R,L,R,L,L,R,R], e_rls, SOMEe_e, \nx + 1 + -1 * 2 = 0, ORundef, false, false)"*)

  = "([\"\n(e_e, x + 1 = 2)\",\"\n(v_v, x)\"], [R,L,R,L,L,R,R], e_rls, SOME e_e, \nx + 1 + -1 * 2 = 0, ORundef, true, false)"

then () else error "pstate changed after ([1], Res)"; (*this shall be corrected .............................^^^^^^^^^*)

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

(*+*)if (get_istate_LI pt p |> the_pstate |> pstate2str)

(*= "([\"\n(e_e, x + 1 = 2)\",\"\n(v_v, x)\"], [R,L,R,L,R,R], e_rls, SOMEe_e, \n-1 + x = 0, ORundef, false, false)"*)

  = "([\"\n(e_e, x + 1 = 2)\",\"\n(v_v, x)\"], [R,L,R,L,R,R], e_rls, SOME e_e, \n-1 + x = 0, ORundef, true, false)"

then () else error "pstate changed after ([2], Res)"; (*this shall be corrected ...................^^^^^^^^^*)

(*[3], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"])*)

(*+*)if (get_istate_LI pt p |> the_pstate |> pstate2str)

(*= "([\"\n(e_e, -1 + x = 0)\",\"\n(v_v, x)\"], [R,R,D,L,R], e_rls, NONE, \nSubproblem\n (''Test'',\n  ??.\<^const>String.char.Char ''LINEAR'' ''univariate'' ''equation''\n   ''test''), ORundef, false, false)"*)

  = "([\"\n(e_e, -1 + x = 0)\",\"\n(v_v, x)\"], [R,R,D,L,R], e_rls, NONE, \nSubproblem\n (''Test'',\n  ??.\<^const>String.char.Char ''LINEAR'' ''univariate'' ''equation''\n   ''test''), ORundef, true, false)"

then () else error "pstate changed after ([3], Pbl)";

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

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

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

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

(*+*)if (get_istate_LI pt p |> the_pstate |> pstate2str)

(*= "([\"\n(e_e, -1 + x = 0)\",\"\n(v_v, x)\"], [R,R,D,L,R], e_rls, NONE, \nSubproblem\n (''Test'',\n  ??.\<^const>String.char.Char ''LINEAR'' ''univariate'' ''equation''\n   ''test''), ORundef, false, false)"*)

  = "([\"\n(e_e, -1 + x = 0)\",\"\n(v_v, x)\"], [R,R,D,L,R], e_rls, NONE, \nSubproblem\n (''Test'',\n  ??.\<^const>String.char.Char ''LINEAR'' ''univariate'' ''equation''\n   ''test''), ORundef, true, false)"

then () else error "pstate changed after ([3], Pbl)";

(*[3, 1], Frm*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Apply_Method ["Test", "solve_linear"]*)

(*+*)if (get_istate_LI pt p |> the_pstate |> pstate2str)

 = "([\"\n(e_e, -1 + x = 0)\",\"\n(v_v, x)\"], [], e_rls, NONE, \n??.empty, ORundef, false, true)"

then () else error "pstate changed after ([3, 1], Frm)";

(*[3, 1], Res*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv")*)

(*+*)if (get_istate_LI pt p |> the_pstate |> pstate2str)

(*= "([\"\n(e_e, -1 + x = 0)\",\"\n(v_v, x)\"], [R,L,R,L,R,L,R], e_rls, SOMEe_e, \nx = 0 + -1 * -1, ORundef, false, false)"*)

  = "([\"\n(e_e, -1 + x = 0)\",\"\n(v_v, x)\"], [R,L,R,L,R,L,R], e_rls, SOME e_e, \nx = 0 + -1 * -1, ORundef, true, false)"

then () else error "pstate changed after ([3, 1], Res)";

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

(*+*)if (get_istate_LI pt p |> the_pstate |> pstate2str)

(*= "([\"\n(e_e, -1 + x = 0)\",\"\n(v_v, x)\"], [R,L,R,L,R,R], e_rls, SOMEe_e, \nx = 1, ORundef, false, false)"*)

  = "([\"\n(e_e, -1 + x = 0)\",\"\n(v_v, x)\"], [R,L,R,L,R,R], e_rls, SOME e_e, \nx = 1, ORundef, true, false)"

then () else error "pstate changed after ([3, 2], Res)"; (*this shall be corrected ............^^^^^^^^^*)

(*[3], Res*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Check_Postcond ["LINEAR", "univariate", "equation", "test"]*)

(*+*)if (get_istate_LI pt p |> the_pstate |> pstate2str)

 = "([\"\n(e_e, -1 + x = 0)\",\"\n(v_v, x)\"], [R,R,D,L,R], e_rls, NONE, \n[x = 1], ORundef, true, false)"

then () else error "pstate changed after ([3], Res)";

(*[4], Res*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Check_elementwise "Assumptions"*)

(*+*)if (get_istate_LI pt p |> the_pstate |> pstate2str)

(*= "([\"\n(e_e, -1 + x = 0)\",\"\n(v_v, x)\",\"\n(L_L, [x = 1])\"], [R,R,D,R,D], e_rls, NONE, \n[x = 1], ORundef, false, false)"*)

  = "([\"\n(e_e, -1 + x = 0)\",\"\n(v_v, x)\",\"\n(L_L, [x = 1])\"], [R,R,D,R,D], e_rls, NONE, \n[x = 1], ORundef, true, false)"

then () else error "pstate changed after ([4], Res)"; (*this shall be corrected ..................................^^^^^^^^^*)

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

(*+*)if (get_istate_LI pt p |> the_pstate |> pstate2str)

(*= "([\"\n(e_e, -1 + x = 0)\",\"\n(v_v, x)\",\"\n(L_L, [x = 1])\"], [R,R,D,R,D], e_rls, NONE, \n[x = 1], ORundef, false, false)"*)

  = "([\"\n(e_e, -1 + x = 0)\",\"\n(v_v, x)\",\"\n(L_L, [x = 1])\"], [R,R,D,R,D], e_rls, NONE, \n[x = 1], ORundef, true, false)"

then () else error "pstate changed after ([], Res)"; (*this shall be corrected ...................................^^^^^^^^^*)

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

  val pIopt = Ctree.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*);

Step_Solve.do_next (pt, ip);

"~~~~~ and do_next , 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 ((ist, ctxt), sc) = LItool.resume_prog thy' (p,p_) pt;

(*+*)istate2str ist

 = "Pstate ([\"\n(e_e, -1 + x = 0)\",\"\n(v_v, x)\",\"\n(L_L, [x = 1])\"], [R,R,D,R,D], e_rls, NONE, \n[x = 1],"

  ^ " ORundef, true, false)"; (*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~true ok*)

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

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

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

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

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

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

  val Term_Val _ =

           go_scan_up (prog, cc) (trans_scan_up ist);

"~~~~~ fun go_scan_up , args:"; val ((pcc as (sc, _)), (ist as {path, act_arg, found_accept, ...}))

  = ((prog, cc), (trans_scan_up ist));

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

  val Term_Val _ =

           scan_up pcc (ist |> path_up) (go_up path sc);

"~~~~~ and scan_up , args:"; val (pcc, ist, (Abs _(*2*))) = (pcc, (ist |> path_up), (go_up path sc));

  val Term_Val _ =

           go_scan_up pcc ist;

"~~~~~ fun go_scan_up , args:"; val ((pcc as (sc, _)), (ist as {path, act_arg, found_accept, ...}))

  = (pcc, ist);

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

  val Term_Val _ =

             go_scan_up pcc ist;

"~~~~~ and scan_up , args:"; val (pcc, ist, (Const ("HOL.Let"(*3*),_) $ _ $ (Abs _)))

  = (pcc, (ist |> path_up), (go_up path sc));

(*/--------------------- final test ---------------------------------------------------------\\*)

if pstate2str ist

 = "([\"\n(e_e, -1 + x = 0)\",\"\n(v_v, x)\",\"\n(L_L, [x = 1])\"], [R,R,D], e_rls, NONE, \n[x = 1],"^

  " ORundef, true, false)"

then () else error "";