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) = Test_Code.init_calc @{context} [(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"]*)
20 (*[], Met*)val (p''''',_,f,nxt''''',_,pt''''') = me nxt p [] pt; (*\<rightarrow>Apply_Method ["Test", "squ-equ-test-subpbl1"])*);
22 (*//------------------ step into Specify_Method --------------------------------------------\\*)
23 "~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, [], pt);
24 val ("ok", ([] ,[] , (_, _))) = (*case*)
25 Step.by_tactic tac (pt, p) (*of*);
26 "~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));
27 (*val Applicable.Yes (Specify_Method' (["Test", "squ-equ-test-subpbl1"], [], [])) =*)
28 val Applicable.Yes tac' =
29 (*case*) Step.check tac (pt, p) (*of*);
30 (*if*) Tactic.for_specify' tac' (*then*);
32 val ("ok", (_, _, ptp)) = (*return from by_tactic *)
33 Step_Specify.by_tactic tac' ptp;
34 "~~~~~ from fun by_tactic \<longrightarrow>fun me , return:"; val (pt, p) = (ptp);
36 val (pt'''''_', p'''''_') = (ptp); (* keep for end of me*)
38 val ("ok", ([(Apply_Method ["Test", "squ-equ-test-subpbl1"], _, _)] ,[] , (_, _))) = (*case*)
39 Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
40 "~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) =
41 (p, ((pt, Pos.e_pos'), []));
42 val pIopt = Ctree.get_pblID (pt, ip);
43 (*if*) ip = ([], Pos.Res) (*else*);
44 val _ = (*case*) tacis (*of*);
45 val SOME _ = (*case*) pIopt (*of*);
47 val ("ok", ([(Apply_Method ["Test", "squ-equ-test-subpbl1"], _, _)], _, (_, _))) =
48 Step.switch_specify_solve p_ (pt, ip);
49 "~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
50 (*if*) member op = [Pos.Pbl, Pos.Met] state_pos (*then*);
52 val ("ok", ([(Apply_Method ["Test", "squ-equ-test-subpbl1"], _, _)], _, (_, _))) =
53 Step.specify_do_next (pt, input_pos);
54 "~~~~~ fun specify_do_next , args:"; val (ptp as (pt, (p, p_))) = (pt, input_pos);
55 val (_, (p_', tac)) = Specify.find_next_step ptp
56 val ist_ctxt = Ctree.get_loc pt (p, p_)
57 val Tactic.Apply_Method mI = (*case*) tac (*of*);
59 (*val ("ok", ([(Apply_Method ["Test", "squ-equ-test-subpbl1"], _, _)], _, (_, _))) =*)
60 (*keep for continuing Specify_Method*)
62 LI.by_tactic (Tactic.Apply_Method' (mI, NONE, Istate.empty, ContextC.empty)) ist_ctxt (pt, (p, p_'));
63 "~~~~~ fun by_tactic , args:"; val ((Tactic.Apply_Method' (mI, _, _, _)), (_, ctxt), (pt, pos as (p, _))) =
64 ((Tactic.Apply_Method' (mI, NONE, Istate.empty, ContextC.empty)), ist_ctxt, (pt, (p, p_')));
65 val (itms, (*l..*)oris, probl(*..l*)) = case get_obj I pt p of
66 PblObj {meth = itms, origin = (oris, _, _), probl, ...} => (itms, oris, probl)
67 | _ => error "LI.by_tactic Apply_Method': uncovered case get_obj"
68 val {model, ...} = MethodC.from_store ctxt mI;
69 val itms = if itms <> [] then itms else I_Model.complete oris probl [] model
70 val prog_rls = LItool.get_simplifier (pt, pos)
71 val (is, env, ctxt, prog) = case LItool.init_pstate prog_rls ctxt itms mI of
72 (is as Istate.Pstate {env, ...}, ctxt, program) => (is, env, ctxt, program)
73 | _ => error "LI.by_tactic Apply_Method': uncovered case init_pstate"
74 val ini = LItool.implicit_take ctxt prog env;
75 val pos = start_new_level pos
76 val SOME t = (*case*) ini (*of*);
77 val show_add = Tactic.Apply_Method' (mI, SOME t, is, ctxt);
78 val (pos, c, _, pt) = Solve_Step.add show_add (is, ctxt) (pt, pos);
80 (*-------------------- continuing Specify_Method ---------------------------------------------*)
81 "~~~~~ from fun specify_do_next \<longrightarrow>fun switch_specify_solve \<longrightarrow>fun do_next \<longrightarrow>fun me , return:";
82 val (_, (ts as (_, _, _) :: _, _, _)) = (xxxxx);
83 val tacis as (_::_) = (*case*) ts (*of*);
84 val (tac, _, _) = last_elem tacis;
86 (p, [] : NEW, TESTg_form ctxt (pt'''''_', p'''''_'), tac, Celem.Sundef, pt) (*return from me*);
87 (*-------------------- continuing Specify_Method ---------------------------------------------*)
88 (*\\------------------ step into Specify_Method --------------------------------------------//*)
90 val (p'''',_,f'''',nxt'''',_,pt'''') = me nxt''''' p''''' [] pt'''''; (*nxt'''' = Rewrite_Set "norm_equation"*)
92 (*//------------------ step into Rewrite_Set -----------------------------------------------\\*)
93 "~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt''''', p''''', [], pt''''');
94 val ctxt = Ctree.get_ctxt pt p;
95 val ("ok", (_, _, ptp)) =
96 (*case*) Step.by_tactic tac (pt, p) (*of*);
98 val ("ok", (ts as (_, _, _) :: _, _, _)) =
99 (*case*) Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
100 val (_, ts) = ("", ts)
101 val tacis as (_::_) =
103 val (tac, _, _) = last_elem tacis
106 (p, [] : NEW, TESTg_form ctxt (pt, p) (* form output comes from Step.by_tactic *),
107 tac, Celem.Sundef, pt);
109 TESTg_form ctxt (pt, p);
110 "~~~~~ fun TESTg_form , args:"; val (ctxt, ptp) = (ctxt, (pt, p));
111 val (form, _, _) = ME_Misc.pt_extract ctxt ptp
113 (*case*) form (*of*);
114 Test_Out.FormKF (UnparseC.term ctxt t);
115 (*-------------------- stop step into Rewrite_Set --------------------------------------------*)
116 (*\\------------------ step into Rewrite_Set -----------------------------------------------//*)
118 (* final test ... ----------------------------------------------------------------------------*)
119 if p'''' = ([1], Frm) andalso f2str f'''' = "x + 1 = 2"
120 then case nxt'''' of (Rewrite_Set "norm_equation") => ()
121 | _ => error "minisubpbl: MethodC not started in root-problem 1"
122 else error "minisubpbl: MethodC not started in root-problem 2";
124 Test_Tool.show_pt_tac pt''''; (*[
125 ([], Frm), solve (x + 1 = 2, x)
126 . . . . . . . . . . Apply_Method ["Test", "squ-equ-test-subpbl1"],
127 ([1], Frm), x + 1 = 2
128 . . . . . . . . . . Empty_Tac]