1 (* Title: "Minisubpbl/300-init-subpbl-NEXT_STEP.sml"
2 Author: Walther Neuper 1105
3 (c) copyright due to lincense terms.
6 "----------- Minisubpbl/300-init-subpbl-NEXT_STEP.sml -----------------------------------------";
7 "----------- Minisubpbl/300-init-subpbl-NEXT_STEP.sml -----------------------------------------";
8 "----------- Minisubpbl/300-init-subpbl-NEXT_STEP.sml -----------------------------------------";
10 val fmz = ["equality (x+1=(2::real))", "solveFor x", "solutions L"];
12 ("Test", ["sqroot-test", "univariate", "equation", "test"],
13 ["Test", "squ-equ-test-subpbl1"]);
14 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
15 (*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, Pos.e_pos'), []);(*Model_Problem*)
16 (*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, Pos.e_pos'), []);(*Specify_Theory*)
17 (*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, Pos.e_pos'), []);(*Specify_Problem ["sqroot-test", "univariate", "equation", "test"*)
18 (*[], Met*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Specify_Method ["Test", "squ-equ-test-subpbl1"]*)
19 (*[1], Frm*)val (_, ([(tac''''', _, _)], _, (pt''''', p'''))) =(**) Step.do_next p ((pt, e_pos'), []);(*Apply_Method ["Test", "squ-equ-test-subpbl1"]*)
21 "~~~~~ fun step , args:"; val ((ip as (_, p_)), (ptp as (pt,p), tacis)) = (p ,((pt, e_pos'), []));
22 val pIopt = get_pblID (pt,ip);
23 (*if*) ip = ([], Pos.Res) (*else*);
24 val _ = (*case*) tacis (*of*);
25 val SOME _ = (*case*) pIopt (*of*);
26 (*if*) member op = [Pos.Pbl, Pos.Met] p_ (*then*);
28 (*+*)val (_, ([_], _, (pt''''', p'''''))) =
29 Step.specify_do_next (pt, ip);
30 "~~~~~ fun specify_do_next , args:"; val ((ptp as (pt, (p, p_)))) = (pt, ip);
31 val (_, (p_', tac)) = Specify.find_next_step ptp
32 val ist_ctxt = Ctree.get_loc pt (p, p_)
33 (*val Apply_Method ["Test", "squ-equ-test-subpbl1"]*)
34 val Tactic.Apply_Method mI = (*case*) tac (*of*);
36 LI.by_tactic (Tactic.Apply_Method' (mI, NONE, Istate.empty, ContextC.empty)) ist_ctxt ptp;
37 "~~~~~ fun begin_end_prog , args:"; val ((Tactic.Apply_Method' (mI, _, _, _)), (ist, ctxt), (pt, pos as (p, _)))
38 = ((Tactic.Apply_Method' (mI, NONE, Istate.empty, ContextC.empty)), ist_ctxt, ptp);
39 val {ppc, ...} = MethodC.from_store mI;
40 val (itms, oris, probl) = case get_obj I pt p of
41 PblObj {meth = itms, origin = (oris, _, _), probl, ...} => (itms, oris, probl)
42 | _ => error "begin_end_prog Apply_Method': uncovered case get_obj"
43 val itms = if itms <> [] then itms else I_Model.complete oris probl [] ppc
44 val thy' = get_obj g_domID pt p;
45 val thy = ThyC.get_theory thy';
46 val srls = LItool.get_simplifier (pt, pos);
48 (*if*) mI = ["Biegelinien", "ausBelastung"] (*else*);
49 val (is, env, ctxt, scr) = case LItool.init_pstate srls ctxt itms mI of
50 (is as Istate.Pstate {env, ...}, ctxt, scr) => (is, env, ctxt, scr)
51 | _ => error "begin_end_prog Apply_Method': uncovered case init_pstate"
54 (*[1], Res*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p''''' ((pt''''', e_pos'), []);(*Rewrite_Set "norm_equation"*)
55 case tac of Rewrite_Set "norm_equation" => (
56 if p = ([1], Res) then (
57 if pr_ctree pr_short pt = ". ----- pblobj -----\n1. x + 1 = 2\n" then ()
58 else error "Apply_Method [Test, squ-equ-test-subpbl1] changed pt"
59 ) else error "Apply_Method [Test, squ-equ-test-subpbl1] changed p")
60 | _ => error "Apply_Method [Test, squ-equ-test-subpbl1] changed tac";
62 (*ctxt*)Proof_Context.theory_of (Ctree.get_ctxt pt p); (*"Test"*)