1 (* Title: 450-nxt-Check_Postcond
2 Author: Walther Neuper 1105
3 (c) copyright due to lincense terms.
6 "----------- Minisubplb/490-nxt-Check_Postcond -------------------";
7 "----------- Minisubplb/490-nxt-Check_Postcond -------------------";
8 "----------- Minisubplb/490-nxt-Check_Postcond -------------------";
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) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))];
14 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
15 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
16 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
17 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
18 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
19 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
20 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val Apply_Method ["Test", "squ-equ-test-subpbl1"] = nxt;
21 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
23 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"]) = nxt;
24 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
25 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
26 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
27 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
28 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
29 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
30 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
31 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val Apply_Method ["Test", "solve_linear"] = nxt;
32 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv") = nxt;
33 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val Rewrite_Set "Test_simplify" = nxt;
35 val return_me_Rewrite_Set_Test_simplify = me nxt p [] pt;
36 (*//----------- step into me_Rewrite_Set_Test_simplify ------------------------------\\*)
37 (*//------------------ step into me_Rewrite_Set_Test_simplify ------------------------------\\*)
38 "~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, [], pt);
39 val (pt, p) = case Step.by_tactic tac (pt,p) of
40 ("ok", (_, _, ptp)) => ptp | _ => error "script.sml Step.by_tactic";
41 "~~~~~ fun do_next , args:"; val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'), []))
42 val pIopt = get_pblID (pt,ip); (*= SOME ["sqroot-test", "univariate", ...]*)
43 (*if*) tacis; (*= []*)
45 (*if*) member op = [Pbl,Met] p_; (*= false*)
47 "~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
48 (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p); (*false*)
49 val thy' = get_obj g_domID pt (par_pblobj pt p);
50 val ((ist, ctxt), sc) = resume_prog (p,p_) pt;
52 val End_Program (ist, tac) =
53 (*case*) LI.find_next_step sc (pt,pos) ist ctxt (*of*);
55 val ("ok", ([(Check_Postcond ["LINEAR", "univariate", "equation", "test"], _, _)], _, _)) =
56 LI.by_tactic tac (ist, ctxt) ptp;
57 "~~~~~ fun by_tactic , args:"; val ((Check_Postcond' (pI, _)), (sub_ist, sub_ctxt), (pt, pos as (p,_))) =
58 (tac, (ist, ctxt), ptp);
59 val parent_pos = par_pblobj pt p
60 val {program, ...} = MethodC.from_store ctxt (get_obj g_metID pt parent_pos);
62 case LI.find_next_step program (pt, pos) sub_ist sub_ctxt of
63 Next_Step (_, _, Tactic.Check_elementwise' (_, _, (prog_res, _))) => prog_res
64 | End_Program (_, Tactic.Check_Postcond' (_, prog_res)) => prog_res
65 | _ => raise ERROR ("Step_Solve.by_tactic Check_Postcond " ^ strs2str' pI)
66 val asm = (*?!? Rfun,Rrls rm case*)(case get_obj g_tac pt p of
67 Tactic.Check_elementwise _ => (snd o (get_obj g_result pt)) p
68 | _ => Ctree.get_assumptions pt pos);
70 (*if*) parent_pos = []; (*else*)
72 val (ist_parent, ctxt_parent) = case get_loc pt (parent_pos, Frm) of
73 (Pstate i, c) => (i, c)
74 | _ => error "LI.by_tactic Check_Postcond': uncovered case get_loc"
75 val (prog_res', ctxt') = ContextC.subpbl_to_caller sub_ctxt prog_res ctxt_parent
76 val tac = Tactic.Check_Postcond' (pI, prog_res')
77 val ist' = Pstate (ist_parent |> set_act prog_res |> set_found)
79 "~~~~~ fun add , args:"; val ((Check_Postcond' (_, scval)), l, (pt, (p, _))) =
80 (tac, (ist', ctxt'), (pt, (parent_pos, Res)));
81 val (pt,c) = append_result pt p l (scval, asm) Complete;
82 (*\\------------------ step into me_Rewrite_Set_Test_simplify ------------------------------//*)
83 val (p,_,f,nxt,_,pt) = return_me_Rewrite_Set_Test_simplify;
84 val Check_Postcond ["LINEAR", "univariate", "equation", "test"] = nxt;
85 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val Check_elementwise "Assumptions" = nxt;