1 (* Title: 700-interSteps.sml
2 Author: Walther Neuper 1105
3 (c) copyright due to lincense terms.
14 ATTENTION: nested "step into", use ML "--- step into XXXXX ---" from Test_*.thy
15 for Sidekick in order to get levels of "step into" right.
18 "----------- Minisubplb/700-interSteps.sml -----------------------";
19 "----------- Minisubplb/700-interSteps.sml -----------------------";
20 "----------- Minisubplb/700-interSteps.sml -----------------------";
21 (** adaption from rewtools.sml --- initContext..Ptool.Thy_, fun context_thm ---,
22 ** into a functional representation, i.e. we outcomment statements with side-effects:
24 ** CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
25 ** ("Test", ["sqroot-test", "univariate", "equation", "test"],
26 ** ["Test", "squ-equ-test-subpbl1"]))];
27 ** Iterator 1; moveActiveRoot 1;
28 ** autoCalculate 1 CompleteCalc;
30 val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
31 ("Test", ["sqroot-test", "univariate", "equation", "test"],
32 ["Test", "squ-equ-test-subpbl1"]))];
33 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
34 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
35 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
36 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
37 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
38 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
39 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
40 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
41 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
42 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"]) = nxt;
43 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
44 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
45 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
46 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
47 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
48 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
49 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
50 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
51 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
52 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
53 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
54 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
55 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
56 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val End_Proof' = nxt;
59 (*+*)Test_Tool.show_pt pt; (* 11 lines with subpbl *)
61 (** val p = ([], Res);
62 ** initContext 1 Ptool.Thy_ p
63 ** = <MESSAGE><CALCID>1</CALCID><STRING>no thy-context at result</STRING></MESSAGE>: XML.tree;
64 ** val ((pt,_),_) = States.get_calc 1; (* 11 lines with subpbl *)
66 ** interSteps 1 ([2], Res); (* added [2,1]..[2,6] *)
68 "~~~~~ fun interSteps, args:"; val (cI, ip) = (1, ([2], Res));
69 (** val ((pt, p), tacis) = States.get_calc cI;*)
70 val ip' = lev_pred' pt ip;
73 (*+*)ip' = ([1], Res);
74 (*+*)Test_Tool.show_pt pt; (* 11 lines, as produced by autoCalculate CompleteCalc *)
76 val ("detailrls", pt''''', _) = (*case*)
77 Detail_Step.go pt ip (*of*);
79 (*+*)Test_Tool.show_pt pt'''''; (* added [2,1]..[2,6] after ([1], Res)*)
81 (*//------------------ step into Detail_Step.go --------------------------------------------\\*)
82 "~~~~~ fun go , args:"; val (pt, (pos as (p, _))) = (pt, ip);
84 (*+*)pos = ([2], Res);
86 val nd = Ctree.get_nd pt p
87 val cn = Ctree.children nd
89 (*if*) null cn (*then*);
90 (*if*) (Tactic.is_rewset o (Ctree.get_obj Ctree.g_tac nd)) [(*root of nd*)] (*then*);
92 Detail_Step.detailrls pt pos;
93 "~~~~~ fun detailrls , args:"; val (pt, (pos as (p, _))) = (pt, pos);
94 val t = get_obj g_form pt p
95 val tac = get_obj g_tac pt p
96 val ctxt = get_ctxt pt pos
97 val rls = tac |> Tactic.rls_of |> get_rls ctxt
98 val xxx = (*case*) rls (*of*);
99 val is = Istate.init_detail ctxt tac t
101 (*+*)val Rule_Set.Repeat {program = EmptyProg, ...} = rls; (*this prog is replaced by Auto_Prog.gen on the fly*)
103 val is = Istate.init_detail ctxt tac t
104 val tac_ = Tactic.Apply_Method' (MethodC.id_empty(*WN0402: see generate1 !?!*), SOME t, is, ctxt)
105 val pos' = ((lev_on o lev_dn) p, Frm)
106 val (_, _, _, pt') = Step.add tac_ (is, ctxt) (pt, pos') (* implicit Take *);
108 (** )val (_,_, (pt'', _)) =( **)
109 complete_solve CompleteSubpbl [] (pt', pos');
110 "~~~~~ fun complete_solve , args:"; val (auto, c, (ptp as (_, p as (_, p_))))
111 = (CompleteSubpbl, [], (pt', pos'));
112 (*if*) p = ([], Res) (*else*);
113 (*if*) member op = [Pbl,Met] p_ (*else*);
115 val (aaa, ([(Rewrite ("radd_commute", bbb), ccc, ddd)], c', ptp')) =
116 (*case*) Step_Solve.do_next ptp (*of*);
118 val return_do_next_Rewrite_radd_commute = (aaa, ([(Rewrite ("radd_commute", bbb), ccc, ddd)], c', ptp'));
119 (*///----------------- step into do_next --------------------------------------------------\\\*)
120 "~~~~~ fun do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (ptp);
121 (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
122 val ((ist, ctxt), sc) = LItool.resume_prog pos pt;
124 (*case*) find_next_step sc ptp ist ctxt (*of*);
125 "~~~~~ fun find_next_step , args:"; val ((Rule.Prog prog), (ptp as (pt, pos as (p, _))), (Pstate ist), ctxt) =
126 (sc, ptp, ist, ctxt);
128 (*case*) scan_to_tactic (prog, (ptp, ctxt)) (Pstate ist) (*of*);
129 "~~~~~ fun scan_to_tactic , args:"; val ((prog, cc), (Pstate (ist as {path, ...}))) =
130 ((prog, (ptp, ctxt)), (Pstate ist));
131 (*if*) path = [] (*then*);
133 scan_dn cc (trans_scan_dn ist) (Program.body_of prog);
134 "~~~~~ fun scan_dn , args:"; val (cc, ist, (Const (\<^const_name>\<open>Tactical.Repeat\<close>(*2*), _) $ e)) =
135 (cc, (trans_scan_dn ist), (Program.body_of prog));
137 scan_dn cc (ist |> path_down [R]) e;
138 "~~~~~ fun scan_dn , args:"; val (cc, ist, (Const (\<^const_name>\<open>Tactical.Chain\<close>(*1*), _) $ e1 $ e2 $ a)) =
139 (cc, (ist |> path_down [R]), e);
141 (*case*) scan_dn cc (ist |> path_down_form ([L, L, R], a)) e1 (*of*);
142 "~~~~~ fun scan_dn , args:"; val (cc, (ist as {act_arg, ...}), (Const (\<^const_name>\<open>Tactical.Try\<close>(*2*), _) $ e)) =
143 (cc, (ist |> path_down_form ([L, L, R], a)), e1);
145 (*case*) scan_dn cc (ist |> path_down [R]) e (*of*);
146 "~~~~~ fun scan_dn , args:"; val (cc, ist, (Const (\<^const_name>\<open>Tactical.Repeat\<close>(*1*), _) $ e)) =
147 (cc, (ist |> path_down [R]), e);
149 scan_dn cc (ist |> path_down_form ([L, R], a)) e;
150 "~~~~~ fun scan_dn , args:"; val ((cc as (_, ctxt)), (ist as {eval, ...}), t (*fall-through*)) =
151 (cc, (ist |> path_down_form ([L, R], a)), e);
152 (*if*) Tactical.contained_in t (*else*);
153 val (Program.Tac prog_tac, form_arg) =
154 (*case*) LItool.check_leaf "next " ctxt eval (get_subst ist) t (*of*);
156 check_tac cc ist (prog_tac, form_arg);
157 "~~~~~ fun check_tac , args:"; val (((pt, p), ctxt), ist, (prog_tac, form_arg)) =
158 (cc, ist, (prog_tac, form_arg));
159 val m = LItool.tac_from_prog (pt, p) prog_tac
164 Solve_Step.check m (pt, p) (*of*);
165 "~~~~~ fun check , args:"; val ((Tactic.Rewrite thm), (cs as (pt, pos as (p, _)))) =
167 (*\\\----------------- step into do_next --------------------------------------------------///*)
168 val (_, ([(Rewrite ("radd_commute", _), _, _)], c', ptp')) = return_do_next_Rewrite_radd_commute;
170 (*+*)val [([2], Res), ([3], Pbl), ([3, 1], Frm), ([3, 1], Res), ([3, 2], Res), ([3], Res),
171 (*+*) ([4], Res), ([], Res)] = c';
172 (*+*)Test_Tool.show_pt (fst ptp');(*[
173 (([], Frm), solve (x + 1 = 2, x)),
174 (([1], Frm), x + 1 = 2),
175 (([1], Res), x + 1 + - 1 * 2 = 0),
176 (([2,1], Frm), x + 1 + - 1 * 2 = 0),
177 (([2,1], Res), 1 + x + - 1 * 2 = 0)]*)
179 (** )val (_, c', ptp') =( **)
180 complete_solve auto (c @ c') ptp';
181 "~~~~~ fun complete_solve , args:"; val (auto, c, (ptp as (_, p as (_, p_))))
182 = (auto, (c @ c'), ptp');
183 (*if*) p = ([], Res) (*else*);
184 (*if*) member op = [Pbl,Met] p_ (*else*);
186 val (_, ([(Rewrite ("add.assoc", _), _, _)], c', ptp')) = (*case*) Step_Solve.do_next ptp (*of*);
188 "~~~~~ fun complete_solve , args:"; val (auto, c, (ptp as (_, p as (_, p_))))
189 = (auto, (c @ c'), ptp');
190 (*if*) p = ([], Res) (*else*);
191 (*if*) member op = [Pbl,Met] p_ (*else*);
192 val (_, ([(Calculate "TIMES", _, _)], c', ptp')) = (*case*)Step_Solve.do_next ptp (*of*);
194 Test_Tool.show_pt (fst ptp'); (* added [2,1]..[2,3], more to come *)
195 (*-------------------- stop step into Detail_Step.go -----------------------------------------*)
196 (*\\------------------ step into Detail_Step.go --------------------------------------------//*)
199 ** interSteps 1 ([3,1], Res);
201 "~~~~~ fun interSteps, args:"; val (cI, ip) = (1, ([3,1], Res));
202 (**val ((pt, p), tacis) = States.get_calc cI;*)
203 val ip' = lev_pred' pt ip;
205 (*+*)ip = ([3, 1], Res);
206 (*+*)ip' = ([3, 1], Frm);
208 val ("detailrls", pt, _) = (*case*) Detail_Step.go pt''''' ip (*of*);
210 Test_Tool.show_pt pt; (* added ([3,1,1], Frm), ([3,1,1], Res) after ([3,1], Frm)*)
212 (* final test ... ----------------------------------------------------------------------------*)
213 if pr_ctree ctxt pr_short pt =
214 ". ----- pblobj -----\n1" ^
216 "2. x + 1 + - 1 * 2 = 0\n" ^
217 "2.1. x + 1 + - 1 * 2 = 0\n" ^
218 "2.2. 1 + x + - 1 * 2 = 0\n" ^
219 "2.3. 1 + (x + - 1 * 2) = 0\n" ^
220 "2.4. 1 + (x + - 2) = 0\n" ^
221 "2.5. 1 + (- 2 + x) = 0\n" ^
222 "2.6. - 2 + (1 + x) = 0\n" ^
223 "3. ----- pblobj -----\n" ^
224 "3.1. - 1 + x = 0\n" ^
225 "3.1.1. - 1 + x = 0\n" ^
226 (*([3,1,1], Res), x = 0 + - 1 * - 1) only shown by Test_Tool.show_pt*)
227 "3.2. x = 0 + - 1 * - 1\n" ^(* another difference to Test_Tool.show_pt*)
229 (*". [x = 1]" only shown by Test_Tool.show_pt*)
230 then () else error "intermediate steps CHANGED";