walther@59722
|
1 |
(* Title: "Minisubpbl/470-Check_elementwise-NEXT_STEP.sml"
|
walther@59722
|
2 |
Author: Walther Neuper 1911
|
walther@59722
|
3 |
(c) copyright due to lincense terms.
|
walther@59722
|
4 |
*)
|
walther@59722
|
5 |
|
walther@59722
|
6 |
"----------- Minisubpbl/470-Check_elementwise-NEXT_STEP.sml -----------------------------------";
|
walther@59722
|
7 |
"----------- Minisubpbl/470-Check_elementwise-NEXT_STEP.sml -----------------------------------";
|
walther@59722
|
8 |
"----------- Minisubpbl/470-Check_elementwise-NEXT_STEP.sml -----------------------------------";
|
walther@59722
|
9 |
|
walther@59722
|
10 |
val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
|
walther@59722
|
11 |
val (dI',pI',mI') =
|
walther@59722
|
12 |
("Test", ["sqroot-test","univariate","equation","test"],
|
walther@59722
|
13 |
["Test","squ-equ-test-subpbl1"]);
|
walther@59722
|
14 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
walther@59765
|
15 |
(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, Pos.e_pos'), []);(*Model_Problem*)
|
walther@59765
|
16 |
(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, Pos.e_pos'), []);(*Specify_Theory*)
|
walther@59765
|
17 |
(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, Pos.e_pos'), []);(*Specify_Problem ["sqroot-test", "univariate", "equation", "test"*)
|
walther@59765
|
18 |
(*[], Met*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Specify_Method ["Test", "squ-equ-test-subpbl1"]*)
|
walther@59765
|
19 |
(*[1], Frm*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Apply_Method ["Test", "squ-equ-test-subpbl1"]*)
|
walther@59765
|
20 |
(*[2], Res*)val (_, ([(tac, _, _)], _, (pt, p))) =(**) Step.do_next p ((pt, e_pos'), []);(*Rewrite_Set "Test_simplify"*)
|
walther@59765
|
21 |
(*[3], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"])*)
|
walther@59765
|
22 |
(*[3], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Model_Problem*)
|
walther@59765
|
23 |
(*[3], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Specify_Theory "Test"*)
|
walther@59765
|
24 |
(*[3], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Specify_Problem ["LINEAR", "univariate", "equation", "test"]*)
|
walther@59765
|
25 |
(*[3], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Specify_Method ["Test", "solve_linear"]*)
|
walther@59765
|
26 |
(*[3, 1], Frm*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Apply_Method ["Test", "solve_linear"]*)
|
walther@59765
|
27 |
(*[3, 1], Res*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv")*)
|
walther@59765
|
28 |
(*[3, 2], Res*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Rewrite_Set "Test_simplify"*)
|
walther@59765
|
29 |
(*[3], Res*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Check_Postcond ["LINEAR", "univariate", "equation", "test"]*)
|
walther@59722
|
30 |
|
walther@59722
|
31 |
(*+*)if ((get_obj g_result pt (fst p)) |> snd |> terms2str) = "[]"
|
walther@59722
|
32 |
(*+*)then () else error "470-Check_elementwise-NEXT_STEP: Rewrite_Set changed asms";
|
walther@59722
|
33 |
|
walther@59722
|
34 |
(*+*)case tac of Rewrite_Set "Test_simplify" => (
|
walther@59722
|
35 |
(*+*) if p = ([3, 2], Res) then (
|
walther@59722
|
36 |
(*+*) if pr_ctree pr_short pt = ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + -1 * 2 = 0\n3. ----- pblobj -----\n3.1. -1 + x = 0\n3.2. x = 0 + -1 * -1\n"
|
walther@59722
|
37 |
(*+*) then () else error "470-Check_elementwise-NEXT_STEP: Rewrite_Set changed pt"
|
walther@59722
|
38 |
(*+*) ) else error "470-Check_elementwise-NEXT_STEP: Rewrite_Set changed p")
|
walther@59722
|
39 |
(*+*)| _ => error "470-Check_elementwise-NEXT_STEP: Rewrite_Set changed tac";
|
walther@59722
|
40 |
|
walther@59722
|
41 |
(*+*)if (get_ctxt pt p |> Proof_Context.theory_of |> theory2str) = "Test" then ()
|
walther@59722
|
42 |
(*+*)else error "470-Check_elementwise-NEXT_STEP: Rewrite_Set changed ctxt";
|
walther@59722
|
43 |
|
walther@59765
|
44 |
(*[4], Res*)val (_, ([(tac''''', _, _)], _, (pt''''', p'''''))) =(**) Step.do_next p ((pt, e_pos'), []);(*Check_elementwise "Assumptions"*)
|
walther@59722
|
45 |
|
walther@59761
|
46 |
"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'), []));
|
walther@59722
|
47 |
val pIopt = get_pblID (pt,ip);
|
walther@59722
|
48 |
(*if*) ip = ([], Pos.Res) (*else*);
|
walther@59722
|
49 |
val _ = (*case*) tacis (*of*);
|
walther@59722
|
50 |
(*if*) ip = p (*else*);
|
walther@59722
|
51 |
(*if*) member op = [Pos.Pbl, Pos.Met] p_ (*else*);
|
walther@59722
|
52 |
|
walther@59791
|
53 |
LI.do_next (pt, ip);
|
walther@59760
|
54 |
"~~~~~ and do_next , args:"; val ((ptp as (pt, pos as (p, p_)))) = ((pt, ip));
|
walther@59722
|
55 |
(*if*) Celem.e_metID = get_obj g_metID pt (par_pblobj pt p) (*else*);
|
walther@59722
|
56 |
val thy' = get_obj g_domID pt (par_pblobj pt p);
|
walther@59831
|
57 |
val ((ist, ctxt), sc) = LItool.resume_prog thy' (p,p_) pt;
|
walther@59722
|
58 |
|
walther@59791
|
59 |
LI.find_next_step sc (pt, pos) ist ctxt;
|
walther@59772
|
60 |
"~~~~~ fun find_next_step , args:"; val (Rule.Prog prog, (ptp as(pt, (p, _))), Istate.Pstate ist, ctxt)
|
walther@59723
|
61 |
= (sc, (pt, pos), ist, ctxt);
|
walther@59722
|
62 |
|
walther@59769
|
63 |
(*case*) scan_to_tactic (prog, (ptp, ctxt)) (Istate.Pstate ist) (*of*);
|
walther@59769
|
64 |
"~~~~~ fun scan_to_tactic , args:"; val ((prog, cc), (Istate.Pstate (ist as {path, ...})))
|
walther@59722
|
65 |
= ((prog, (ptp, ctxt)), (Istate.Pstate ist));
|
walther@59722
|
66 |
(*if*) path = [] (*else*);
|
walther@59722
|
67 |
|
walther@59785
|
68 |
go_scan_up (prog, cc) (trans_scan_up ist |> set_found);
|
walther@59784
|
69 |
"~~~~~ fun go_scan_up , args:"; val ((pcc as (sc, _)), (ist as {path, act_arg, found_accept, ...}))
|
walther@59785
|
70 |
= ((prog, cc), (trans_scan_up ist |> set_found));
|
walther@59722
|
71 |
(*if*) 1 < length path (*then*);
|
walther@59722
|
72 |
|
walther@59769
|
73 |
scan_up pcc (ist |> path_up) (go_up path sc);
|
walther@59769
|
74 |
"~~~~~ and scan_up , args:"; val (pcc, ist, (Const ("Tactical.Chain"(*2*), _) $ _ $ _))
|
walther@59722
|
75 |
= (pcc, (ist |> path_up), (go_up path sc));
|
walther@59722
|
76 |
|
walther@59769
|
77 |
go_scan_up pcc ist;
|
walther@59784
|
78 |
"~~~~~ fun go_scan_up , args:"; val ((pcc as (sc, _)), (ist as {path, act_arg, found_accept, ...}))
|
walther@59722
|
79 |
= (pcc, ist);
|
walther@59722
|
80 |
(*if*) 1 < length path (*then*);
|
walther@59722
|
81 |
|
walther@59769
|
82 |
scan_up pcc (ist |> path_up) (go_up path sc);
|
walther@59769
|
83 |
"~~~~~ and scan_up , args:"; val ((pcc as (_, cc)), ist, (Const ("Tactical.Repeat"(*2*), _) $ e))
|
walther@59722
|
84 |
= (pcc, (ist |> path_up), (go_up path sc));
|
walther@59722
|
85 |
|
walther@59769
|
86 |
(*case*) scan_dn cc (ist |> path_down [R]) e (*of*);
|
walther@59769
|
87 |
"~~~~~ fun scan_dn , args:"; val (pcc, ist, (Const ("Tactical.Chain"(*2*), _) $ _ $ _))
|
walther@59722
|
88 |
= (cc, (ist |> path_down [R]), e);
|
walther@59722
|
89 |
(*============== stopped, when all worked ===================*)
|
walther@59722
|
90 |
|
walther@59722
|
91 |
|
walther@59765
|
92 |
(*[], Res*)val (_, ([(Check_elementwise "Assumptions", _, _)], _, (pt, p))) = Step.do_next p''''' ((pt''''', e_pos'), []);(**)
|
walther@59765
|
93 |
(*[], Res*)val (_, ([(Check_Postcond ["sqroot-test", "univariate", "equation", "test"], _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(**)
|
walther@59722
|
94 |
|
walther@59722
|
95 |
(*+*)val (res, asm) = (get_obj g_result pt (fst p));
|
walther@59722
|
96 |
(*+*)if p = ([], Res) andalso
|
walther@59722
|
97 |
(*+*) term2str res = "[x = 1]" andalso terms2str asm = "[\"precond_rootmet 1\"]"
|
walther@59723
|
98 |
(*+*)then () else error "Minisubpbl/470-Check_elementwise-NEXT_STEP.sml CHANGED"; |