1 (* Title: "Minisubpbl/200-start-method.sml"
2 Author: Walther Neuper 1105
3 (c) copyright due to lincense terms.
6 "----------- Minisubplb/200-start-method.sml -------------------------------------------------";
7 "----------- Minisubplb/200-start-method.sml -------------------------------------------------";
8 "----------- Minisubplb/200-start-method.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 (*[], Pbl*)val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
14 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*\<rightarrow>Add_Given "equality (x + 1 = 2)"*)
15 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*\<rightarrow>Add_Given "solveFor x"*)
16 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*\<rightarrow>Add_Find "solutions L"*)
17 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*\<rightarrow>Specify_Theory "Test"*)
18 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*\<rightarrow>Specify_Problem ["sqroot-test", "univariate", "equation", "test"]*)
19 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*\<rightarrow>Specify_Method ["Test", "squ-equ-test-subpbl1"]*)
21 (*//------------------ begin step into ------------------------------------------------------\\*)
22 (*[], Met*)val (p''''',_,f,nxt''''',_,pt''''') = me nxt p [] pt; (*\<rightarrow>Apply_Method ["Test", "squ-equ-test-subpbl1"])*);
24 "~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, [], pt);
26 val ("ok", ([] ,[] , (_, _))) = (*case*)
27 Step.by_tactic tac (pt, p) (*of*);
28 "~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));
29 (*val Applicable.Yes (Specify_Method' (["Test", "squ-equ-test-subpbl1"], [], [])) =*)
30 val Applicable.Yes tac' =
31 (*case*) check tac (pt, p) (*of*);
32 (*if*) Tactic.for_specify' tac' (*then*);
34 val ("ok", (_, _, ptp)) = (*return from by_tactic *)
35 Step_Specify.by_tactic tac' ptp;
36 "~~~~~ from fun by_tactic \<longrightarrow>fun me , return:"; val (pt, p) = (ptp);
38 val (pt'''''_', p'''''_') = (ptp); (* keep for end of me*)
40 val ("ok", ([(Apply_Method ["Test", "squ-equ-test-subpbl1"], _, _)] ,[] , (_, _))) = (*case*)
41 Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
42 "~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) =
43 (p, ((pt, Pos.e_pos'), []));
44 val pIopt = Ctree.get_pblID (pt, ip);
45 (*if*) ip = ([], Pos.Res) (*else*);
46 val _ = (*case*) tacis (*of*);
47 val SOME _ = (*case*) pIopt (*of*);
49 val ("ok", ([(Apply_Method ["Test", "squ-equ-test-subpbl1"], _, _)], _, (_, _))) =
50 switch_specify_solve p_ (pt, ip);
51 "~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
52 (*if*) Library.member op = [Pos.Pbl, Pos.Met] state_pos (*then*);
54 val ("ok", ([(Apply_Method ["Test", "squ-equ-test-subpbl1"], _, _)], _, (_, _))) =
55 specify_do_next (pt, input_pos);
56 "~~~~~ fun specify_do_next , args:"; val (ptp as (pt, (p, p_))) = (pt, input_pos);
57 val (_, (p_', tac)) = Specify.find_next_step ptp
58 val ist_ctxt = Ctree.get_loc pt (p, p_)
59 val Tactic.Apply_Method mI = (*case*) tac (*of*);
61 (*val ("ok", ([(Apply_Method ["Test", "squ-equ-test-subpbl1"], _, _)], _, (_, _))) =*)
63 LI.by_tactic (Tactic.Apply_Method' (mI, NONE, Istate.empty, ContextC.empty)) ist_ctxt (pt, (p, p_'));
64 "~~~~~ fun by_tactic , args:"; val ((Tactic.Apply_Method' (mI, _, _, _)), (_, ctxt), (pt, pos as (p, _))) =
65 ((Tactic.Apply_Method' (mI, NONE, Istate.empty, ContextC.empty)), ist_ctxt, (pt, (p, p_')));
66 val (itms, (*l..*)oris, probl(*..l*)) = case get_obj I pt p of
67 PblObj {meth = itms, origin = (oris, _, _), probl, ...} => (itms, oris, probl)
68 | _ => error "LI.by_tactic Apply_Method': uncovered case get_obj"
69 val {ppc, ...} = Method.from_store mI;
70 val itms = if itms <> [] then itms else I_Model.complete oris probl [] ppc
71 val itms = Step_Specify.hack_until_review_Specify_1 mI itms
72 val srls = LItool.get_simplifier (pt, pos)
73 val (is, env, ctxt, prog) = case LItool.init_pstate srls ctxt itms mI of
74 (is as Pstate {env, ...}, ctxt, scr) => (is, env, ctxt, scr)
75 | _ => error "LI.by_tactic Apply_Method': uncovered case init_pstate"
76 val ini = LItool.implicit_take prog env;
77 val pos = start_new_level pos
78 val SOME t = (*case*) ini (*of*);
79 val show_add = Tactic.Apply_Method' (mI, SOME t, is, ctxt);
80 val (pos, c, _, pt) = Solve_Step.add show_add (is, ctxt) (pt, pos);
81 (*-------------------- stop step into -------------------------------------------------------*)
83 "~~~~~ from fun specify_do_next \<longrightarrow>fun switch_specify_solve \<longrightarrow>fun do_next \<longrightarrow>fun me , return:";
84 val (_, (ts as (_, _, _) :: _, _, _)) = (xxxxx);
85 val tacis as (_::_) = (*case*) ts (*of*);
86 val (tac, _, _) = last_elem tacis;
88 (p, [] : NEW, TESTg_form (pt'''''_', p'''''_'), tac, Celem.Sundef, pt) (*return from me*);
89 (*\------------------- end step into 1 -----------------------------------------------------/*)
91 (*/------------------- begin step into 2 ---------------------------------------------------\*)
92 val (p'''''_',_,f'''''_',nxt'''''_',_,pt) = me nxt''''' p''''' [] pt'''''; (*nxt = ("Rewrite_Set"*)
93 "~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt''''', p''''', [], pt''''');
95 Step.by_tactic tac (pt, p) (*of*);
96 "~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));
97 val Applicable.Yes tac' = (*case*) Step.check tac (pt, p) (*of*);
98 (*-------------------- stop step into -------------------------------------------------------*)
100 (*\------------------- end step into 2 -----------------------------------------------------/*)
103 if p'''''_' = ([1], Frm) andalso f2str f'''''_' = "x + 1 = 2"
104 then case nxt'''''_' of (Rewrite_Set "norm_equation") => ()
105 | _ => error "minisubpbl: Method not started in root-problem 1"
106 else error "minisubpbl: Method not started in root-problem 2";