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 val Model_Problem = nxt;
15 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; val Add_Given "equality (x + 1 = 2)" = nxt;
16 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; val Add_Given "solveFor x" = nxt;
17 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; val Add_Find "solutions L" = nxt;
18 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; val Specify_Theory "Test" = nxt;
19 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; val Specify_Problem ["sqroot-test", "univariate", "equation", "test"] = nxt;
20 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; val Specify_Method ["Test", "squ-equ-test-subpbl1"] = nxt;
22 (*[], Met*)val return_me_Specify_Method = me nxt p [] pt;
23 (*//------------------ step into Specify_Method --------------------------------------------\\*)
24 "~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, [], pt);
25 val ("ok", ([] ,[] , (_, _))) = (*case*)
26 Step.by_tactic tac (pt, p) (*of*);
27 "~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));
28 (*val Applicable.Yes (Specify_Method' (["Test", "squ-equ-test-subpbl1"], [], [])) =*)
29 val Applicable.Yes tac' =
30 (*case*) Step.check tac (pt, p) (*of*);
31 (*if*) Tactic.for_specify' tac' (*then*);
33 val ("ok", (_, _, ptp)) = (*return from by_tactic *)
34 Step_Specify.by_tactic tac' ptp;
35 "~~~~~ from fun by_tactic \<longrightarrow>fun me , return:"; val (pt, p) = (ptp);
37 val (pt'''''_', p'''''_') = (ptp); (* keep for end of me*)
39 val ("ok", ([(Apply_Method ["Test", "squ-equ-test-subpbl1"], _, _)] ,[] , (_, _))) = (*case*)
40 Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
41 "~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) =
42 (p, ((pt, Pos.e_pos'), []));
43 val pIopt = Ctree.get_pblID (pt, ip);
44 (*if*) ip = ([], Pos.Res) (*else*);
45 val _ = (*case*) tacis (*of*);
46 val SOME _ = (*case*) pIopt (*of*);
48 val ("ok", ([(Apply_Method ["Test", "squ-equ-test-subpbl1"], _, _)], _, (_, _))) =
49 Step.switch_specify_solve p_ (pt, ip);
50 "~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
51 (*if*) member op = [Pos.Pbl, Pos.Met] state_pos (*then*);
53 val ("ok", ([(Apply_Method ["Test", "squ-equ-test-subpbl1"], _, _)], _, (_, _))) =
54 Step.specify_do_next (pt, input_pos);
55 "~~~~~ fun specify_do_next , args:"; val (ptp as (pt, (p, p_))) = (pt, input_pos);
56 val (_, (p_', tac)) = Specify.find_next_step ptp
57 val ist_ctxt = Ctree.get_loc pt (p, p_)
58 val Tactic.Apply_Method mI = (*case*) tac (*of*);
60 (*val ("ok", ([(Apply_Method ["Test", "squ-equ-test-subpbl1"], _, _)], _, (_, _))) =*)
61 (*keep for continuing Specify_Method*)
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, oris, probl, o_spec, spec) = case get_obj I pt p of
67 PblObj {meth = itms, origin = (oris, o_spec, _), probl, spec, ...}
68 => (itms, oris, probl, o_spec, spec)
70 val (_, pI', _) = References.select_input o_spec spec
71 val (_, itms) = I_Model.s_make_complete ctxt oris
72 (I_Model.OLD_to_TEST probl, I_Model.OLD_to_TEST itms) (pI', mI)
74 val (is, env, ctxt, prog) = case
75 LItool.init_pstate ctxt itms mI of
76 (is as Pstate {env, ...}, ctxt, program) => (is, env, ctxt, program)
77 | _ => error "LI.by_tactic Apply_Method': uncovered case init_pstate"
78 val ini = LItool.implicit_take ctxt prog env;
79 val pos = start_new_level pos
80 val SOME t = (*case*) ini (*of*);
81 val show_add = Tactic.Apply_Method' (mI, SOME t, is, ctxt);
82 val (pos, c, _, pt) = Solve_Step.add show_add (is, ctxt) (pt, pos);
84 (*-------------------- continuing Specify_Method ---------------------------------------------*)
85 "~~~~~ from fun specify_do_next \<longrightarrow>fun switch_specify_solve \<longrightarrow>fun do_next \<longrightarrow>fun me , return:";
86 val (_, (ts as (_, _, _) :: _, _, _)) = (xxxxx);
87 val tacis as (_::_) = (*case*) ts (*of*);
88 val (tac, _, _) = last_elem tacis;
90 (p, [] : NEW, TESTg_form ctxt (pt'''''_', p'''''_'), tac, Celem.Sundef, pt) (*return from me*);
91 (*-------------------- continuing Specify_Method ---------------------------------------------*)
92 (*\\------------------ step into Specify_Method --------------------------------------------//*)
93 val (p,_,f,nxt,_,pt) = return_me_Specify_Method; val Apply_Method ["Test", "squ-equ-test-subpbl1"] = nxt;
95 val return_me_Rewrite_Set = me nxt p [] pt;
96 (*//------------------ step into Rewrite_Set -----------------------------------------------\\*)
97 "~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, [], pt);
98 val ctxt = Ctree.get_ctxt pt p;
99 val ("ok", (_, _, ptp)) =
100 (*case*) Step.by_tactic tac (pt, p) (*of*);
102 val ("ok", (ts as (_, _, _) :: _, _, _)) =
103 (*case*) Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
104 val (_, ts) = ("", ts)
105 val tacis as (_::_) =
107 val (tac, _, _) = last_elem tacis
110 (p, [] : NEW, TESTg_form ctxt (pt, p) (* form output comes from Step.by_tactic *),
111 tac, Celem.Sundef, pt);
113 TESTg_form ctxt (pt, p);
114 "~~~~~ fun TESTg_form , args:"; val (ctxt, ptp) = (ctxt, (pt, p));
115 val (form, _, _) = ME_Misc.pt_extract ctxt ptp
117 (*case*) form (*of*);
118 Test_Out.FormKF (UnparseC.term ctxt t);
119 (*-------------------- stop step into Rewrite_Set --------------------------------------------*)
120 (*\\------------------ step into Rewrite_Set -----------------------------------------------//*)
121 val (p,_,f,nxt,_,pt) = return_me_Rewrite_Set; val Rewrite_Set "norm_equation" = nxt;
123 (* final test ... ----------------------------------------------------------------------------*)
124 if p = ([1], Frm) andalso f2str f = "x + 1 = 2"
125 then case nxt of (Rewrite_Set "norm_equation") => ()
126 | _ => error "minisubpbl: MethodC not started in root-problem 1"
127 else error "minisubpbl: MethodC not started in root-problem 2";
129 Test_Tool.show_pt_tac pt; (*[
130 ([], Frm), solve (x + 1 = 2, x)
131 . . . . . . . . . . Apply_Method ["Test", "squ-equ-test-subpbl1"],
132 ([1], Frm), x + 1 = 2
133 . . . . . . . . . . Empty_Tac]