|
walther@59722
|
1 |
(* Title: "Minisubpbl/790-complete-NEXT_STEP.sml"
|
|
walther@59686
|
2 |
Author: Walther Neuper 1105
|
|
walther@59686
|
3 |
(c) copyright due to lincense terms.
|
|
walther@59686
|
4 |
*)
|
|
walther@59686
|
5 |
|
|
walther@59722
|
6 |
"----------- Minisubpbl/790-complete-NEXT_STEP.sml --------------------------------------------";
|
|
walther@59722
|
7 |
"----------- Minisubpbl/790-complete-NEXT_STEP.sml --------------------------------------------";
|
|
walther@59722
|
8 |
"----------- Minisubpbl/790-complete-NEXT_STEP.sml --------------------------------------------";
|
|
walther@59686
|
9 |
|
|
walther@59997
|
10 |
val fmz = ["equality (x+1=(2::real))", "solveFor x", "solutions L"];
|
|
walther@59686
|
11 |
val (dI',pI',mI') =
|
|
walther@59997
|
12 |
("Test", ["sqroot-test", "univariate", "equation", "test"],
|
|
walther@59997
|
13 |
["Test", "squ-equ-test-subpbl1"]);
|
|
walther@59686
|
14 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
|
walther@59921
|
15 |
(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*\<rightarrow>Model_Problem*)
|
|
walther@59921
|
16 |
(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*\<rightarrow>Specify_Theory*)
|
|
walther@59921
|
17 |
(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*\<rightarrow>Specify_Problem ["sqroot-test", "univariate", "equation", "test"*)
|
|
walther@59921
|
18 |
(*[], Met*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*\<rightarrow>Specify_Method ["Test", "squ-equ-test-subpbl1"]*)
|
|
walther@59921
|
19 |
(*1], Frm*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*\<rightarrow>Apply_Method ["Test", "squ-equ-test-subpbl1"]*)
|
|
walther@59921
|
20 |
(*[1], Res*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*\<rightarrow>Rewrite_Set "norm_equation"*)
|
|
walther@59921
|
21 |
(*[2], Res*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*\<rightarrow>Rewrite_Set "Test_simplify"*)
|
|
walther@59921
|
22 |
(*[3], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*\<rightarrow>Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"])*)
|
|
walther@59921
|
23 |
(*[3], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*\<rightarrow>Model_Problem*)
|
|
walther@59921
|
24 |
(*[3], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*\<rightarrow>Specify_Theory "Test"*)
|
|
walther@59921
|
25 |
(*[3], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*\<rightarrow>Specify_Problem ["LINEAR", "univariate", "equation", "test"]*)
|
|
walther@59921
|
26 |
(*[3], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*\<rightarrow>Specify_Method ["Test", "solve_linear"]*)
|
|
walther@59921
|
27 |
(*[3, 1], Frm*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*\<rightarrow>Apply_Method ["Test", "solve_linear"]*)
|
|
walther@59921
|
28 |
(*[3, 1], Res*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*\<rightarrow>Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv")*)
|
|
walther@59921
|
29 |
(*[3, 2], Res*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*\<rightarrow>Rewrite_Set "Test_simplify"*)
|
|
walther@59921
|
30 |
(*[3], Res*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*\<rightarrow>Check_Postcond ["LINEAR", "univariate", "equation", "test"]*)
|
|
walther@59686
|
31 |
|
|
walther@59868
|
32 |
((get_obj g_result pt (fst p)) |> snd |> UnparseC.terms) = "[]";(*isa*)
|
|
wenzelm@60237
|
33 |
((get_obj g_result pt (fst p)) |> snd |> UnparseC.terms) = "[\"matches (?a = ?b) (-1 + x = 0)\"]";(*REP*)
|
|
walther@60242
|
34 |
(* there are questionable assumptions either --------- \<up> \<up> \<up> \<up> \<up> \<up> \<up> \<up> \<up> \<up> \<up> \<up> ^^*)
|
|
walther@59686
|
35 |
|
|
walther@59765
|
36 |
(*[4], Res*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Check_elementwise "Assumptions"*)
|
|
walther@59686
|
37 |
|
|
walther@59868
|
38 |
((get_obj g_result pt (fst p)) |> snd |> UnparseC.terms) = "[]";(*isa*)
|
|
walther@59868
|
39 |
((get_obj g_result pt (fst p)) |> snd |> UnparseC.terms) = "[\"precond_rootmet 1\"]";(*REP*)
|
|
walther@59686
|
40 |
|
|
walther@59765
|
41 |
(*[], Res*)val ("ok", ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Check_Postcond ["sqroot-test", "univariate", "equation", "test"]*)
|
|
walther@59686
|
42 |
|
|
walther@59868
|
43 |
((get_obj g_result pt (fst p)) |> snd |> UnparseC.terms) = "[]";(*isa*)
|
|
walther@59868
|
44 |
((get_obj g_result pt (fst p)) |> snd |> UnparseC.terms) = "[\"precond_rootmet 1\"]";(*REP*)
|
|
walther@59686
|
45 |
|
|
walther@59765
|
46 |
(*[], Res*)val ("end-of-calculation", ([], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(**)
|
|
walther@59686
|
47 |
|
|
walther@59686
|
48 |
(*/--------------------- final test ----------------------------------\\*)
|
|
walther@59686
|
49 |
val (res, asm) = (get_obj g_result pt (fst p));
|
|
walther@59686
|
50 |
|
|
walther@59868
|
51 |
if UnparseC.term res = "[x = 1]" andalso
|
|
walther@59868
|
52 |
map UnparseC.term asm = [] (* assumptions have gone to the ctxt *)
|
|
walther@59772
|
53 |
then () else error "Minisubpbl/790-complete-NEXT_STEP.sml, find_next_step CHANGED";
|
|
walther@59686
|
54 |
|
|
walther@59686
|
55 |
if p = ([], Und)
|
|
walther@59686
|
56 |
then
|
|
walther@59686
|
57 |
case get_obj g_tac pt (fst p) of
|
|
walther@59686
|
58 |
Apply_Method ["Test", "squ-equ-test-subpbl1"] => ()
|
|
walther@59722
|
59 |
| _ => error "Minisubpbl/790-complete-NEXT_STEP.sml, WRONG RESULT CHANGED 2"
|
|
walther@59722
|
60 |
else error "Minisubpbl/790-complete-NEXT_STEP.sml, WRONG RESULT CHANGED 1"
|