1 (* Title: "Minisubpbl/600-postcond-NEXT_STEP.sml"
2 Author: Walther Neuper 200121
3 (c) copyright due to lincense terms.
6 "----------- Minisubplb/600-postcond-NEXT_STEP.sml -------------------------------------------";
7 "----------- Minisubplb/600-postcond-NEXT_STEP.sml -------------------------------------------";
8 "----------- Minisubplb/600-postcond-NEXT_STEP.sml -------------------------------------------";
9 val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
11 ("Test", ["sqroot-test","univariate","equation","test"],
12 ["Test","squ-equ-test-subpbl1"]);
13 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
14 (*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Model_Problem*)
15 (*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Specify_Theory*)
16 (*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Specify_Problem ["sqroot-test", "univariate", "equation", "test"*)
17 (*[], Met*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Specify_Method ["Test", "squ-equ-test-subpbl1"]*)
19 (*+*)if (get_istate_LI pt p |> the_pstate |> pstate2str)
20 = "([], [], e_rls, NONE, \n??.empty, ORundef, false, false)"
21 then () else error "pstate changed after ([], Met)";
23 (*[1], Frm*)val (_, ([(tac''''', _, _)], _, (pt''''', p'''''))) =(**) Step.do_next p ((pt, e_pos'), []);(*Apply_Method ["Test", "squ-equ-test-subpbl1"]*)
25 (*+*)if (get_istate_LI pt''''' p''''' |> the_pstate |> pstate2str)
26 = "([\"\n(e_e, x + 1 = 2)\",\"\n(v_v, x)\"], [], e_rls, NONE, \n??.empty, ORundef, false, true)"
27 then () else error "pstate changed after ([1], Frm)"; (*this shall be corrected ...^^^^^^^^^: a tac has been found !!!*)
29 (*[1], Res*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p''''' ((pt''''', e_pos'), []);(*Rewrite_Set "norm_equation"*)
31 (*+*)if (get_istate_LI pt p |> the_pstate |> pstate2str)
32 (*= "([\"\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)"*)
33 = "([\"\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)"
34 then () else error "pstate changed after ([1], Res)"; (*this shall be corrected .............................^^^^^^^^^*)
36 (*[2], Res*)val (_, ([(tac, _, _)], _, (pt, p))) =(**) Step.do_next p ((pt, e_pos'), []);(*Rewrite_Set "Test_simplify"*)
38 (*+*)if (get_istate_LI pt p |> the_pstate |> pstate2str)
39 (*= "([\"\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)"*)
40 = "([\"\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)"
41 then () else error "pstate changed after ([2], Res)"; (*this shall be corrected ...................^^^^^^^^^*)
43 (*[3], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"])*)
45 (*+*)if (get_istate_LI pt p |> the_pstate |> pstate2str)
46 (*= "([\"\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)"*)
47 = "([\"\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)"
48 then () else error "pstate changed after ([3], Pbl)";
50 (*[3], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Model_Problem*)
51 (*[3], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Specify_Theory "Test"*)
52 (*[3], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Specify_Problem ["LINEAR", "univariate", "equation", "test"]*)
53 (*[3], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Specify_Method ["Test", "solve_linear"]*)
55 (*+*)if (get_istate_LI pt p |> the_pstate |> pstate2str)
56 (*= "([\"\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)"*)
57 = "([\"\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)"
58 then () else error "pstate changed after ([3], Pbl)";
60 (*[3, 1], Frm*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Apply_Method ["Test", "solve_linear"]*)
62 (*+*)if (get_istate_LI pt p |> the_pstate |> pstate2str)
63 = "([\"\n(e_e, -1 + x = 0)\",\"\n(v_v, x)\"], [], e_rls, NONE, \n??.empty, ORundef, false, true)"
64 then () else error "pstate changed after ([3, 1], Frm)";
66 (*[3, 1], Res*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv")*)
68 (*+*)if (get_istate_LI pt p |> the_pstate |> pstate2str)
69 (*= "([\"\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)"*)
70 = "([\"\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)"
71 then () else error "pstate changed after ([3, 1], Res)";
73 (*[3, 2], Res*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Rewrite_Set "Test_simplify"*)
75 (*+*)if (get_istate_LI pt p |> the_pstate |> pstate2str)
76 (*= "([\"\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)"*)
77 = "([\"\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)"
78 then () else error "pstate changed after ([3, 2], Res)"; (*this shall be corrected ............^^^^^^^^^*)
80 (*[3], Res*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Check_Postcond ["LINEAR", "univariate", "equation", "test"]*)
82 (*+*)if (get_istate_LI pt p |> the_pstate |> pstate2str)
83 = "([\"\n(e_e, -1 + x = 0)\",\"\n(v_v, x)\"], [R,R,D,L,R], e_rls, NONE, \n[x = 1], ORundef, true, false)"
84 then () else error "pstate changed after ([3], Res)";
86 (*[4], Res*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Check_elementwise "Assumptions"*)
88 (*+*)if (get_istate_LI pt p |> the_pstate |> pstate2str)
89 (*= "([\"\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)"*)
90 = "([\"\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)"
91 then () else error "pstate changed after ([4], Res)"; (*this shall be corrected ..................................^^^^^^^^^*)
93 (*[], Res* )val ("ok", ([(tac, _, _)], _, (pt, p))) =( **) Step.do_next p ((pt, e_pos'), []);(*Check_Postcond ["sqroot-test", "univariate", "equation", "test"]*)
95 (*+*)if (get_istate_LI pt p |> the_pstate |> pstate2str)
96 (*= "([\"\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)"*)
97 = "([\"\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)"
98 then () else error "pstate changed after ([], Res)"; (*this shall be corrected ...................................^^^^^^^^^*)
100 "~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) = (p, ((pt, e_pos'), []));
101 val pIopt = Ctree.get_pblID (pt, ip);
102 (*if*) ip = ([], Pos.Res) (*else*);
103 val _ = (*case*) tacis (*of*);
104 val SOME _ = (*case*) pIopt (*of*);
105 (*if*) member op = [Pos.Pbl, Pos.Met] p_ (*else*);
107 Step_Solve.do_next (pt, ip);
108 "~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
109 (*if*) Celem.e_metID = get_obj g_metID pt (par_pblobj pt p) (*else*);
110 val thy' = get_obj g_domID pt (par_pblobj pt p);
111 val ((ist, ctxt), sc) = LItool.resume_prog thy' (p,p_) pt;
113 (*+*)Istate.string_of ist
114 = "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],"
115 ^ " ORundef, true, false)"; (*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~true ok*)
117 (*case*) LI.find_next_step sc (pt, pos) ist ctxt (*of*);
118 "~~~~~ fun find_next_step , args:"; val ((Rule.Prog prog), (ptp as(pt, (p, _))), (Pstate ist), ctxt)
119 = (sc, (pt, pos), ist, ctxt);
121 (*case*) scan_to_tactic (prog, (ptp, ctxt)) (Pstate ist) (*of*);
122 "~~~~~ fun scan_to_tactic , args:"; val ((prog, cc), (Pstate (ist as {path, ...}))) = ((prog, (ptp, ctxt)), (Pstate ist));
123 (*if*) path = [] (*else*);
126 go_scan_up (prog, cc) (trans_scan_up ist);
127 "~~~~~ fun go_scan_up , args:"; val ((pcc as (sc, _)), (ist as {path, act_arg, found_accept, ...}))
128 = ((prog, cc), (trans_scan_up ist));
129 (*if*) 1 < length path (*then*);
132 scan_up pcc (ist |> path_up) (go_up path sc);
133 "~~~~~ and scan_up , args:"; val (pcc, ist, (Abs _(*2*))) = (pcc, (ist |> path_up), (go_up path sc));
137 "~~~~~ fun go_scan_up , args:"; val ((pcc as (sc, _)), (ist as {path, act_arg, found_accept, ...}))
139 (*if*) 1 < length path (*then*);
143 "~~~~~ and scan_up , args:"; val (pcc, ist, (Const ("HOL.Let"(*3*),_) $ _ $ (Abs _)))
144 = (pcc, (ist |> path_up), (go_up path sc));
146 (*/--------------------- final test ---------------------------------------------------------\\*)
148 = "([\"\n(e_e, -1 + x = 0)\",\"\n(v_v, x)\",\"\n(L_L, [x = 1])\"], [R,R,D], e_rls, NONE, \n[x = 1],"^
149 " ORundef, true, false)"
150 then () else error "";