1 (* Title: "Interpret/lucas-interpreter.sml"
3 (c) due to copyright terms
6 "-----------------------------------------------------------------------------------------------";
7 "table of contents -----------------------------------------------------------------------------";
8 "-----------------------------------------------------------------------------------------------";
9 "----------- Take as 1st stac in program -------------------------------------------------------";
10 "----------- re-build: fun locate_input_tactic -------------------------------------------------";
11 "----------- fun locate_input_tactic Helpless, NOT applicable ----------------------------------";
12 "----------- re-build: fun find_next_step, mini ------------------------------------------------";
13 "----------- re-build: fun locate_input_term ---------------------------------------------------";
14 "-----------------------------------------------------------------------------------------------";
15 "-----------------------------------------------------------------------------------------------";
16 "-----------------------------------------------------------------------------------------------";
18 "----------- Take as 1st stac in program -------------------------------------------------------";
19 "----------- Take as 1st stac in program -------------------------------------------------------";
20 "----------- Take as 1st stac in program -------------------------------------------------------";
21 "compare --- Apply_Method with initial Take by Step.do_next --- in test/../step-solve ----------";
22 val p = e_pos'; val c = [];
23 val (p,_,f,nxt,_,pt) =
24 Test_Code.init_calc @{context}
25 [(["functionTerm (x \<up> 2 + 1)", "integrateBy x", "antiDerivative FF"],
26 ("Integrate", ["integrate", "function"], ["diff", "integration"]))];
27 val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow> Add_Given "functionTerm (x \<up> 2 + 1)"*)
28 val (p,_,f,nxt,_,pt) = me nxt p c pt;
29 val (p,_,f,nxt,_,pt) = me nxt p c pt;
30 val (p,_,f,nxt,_,pt) = me nxt p c pt;
31 val (p,_,f,nxt,_,pt) = me nxt p c pt;
33 val (p''',_,f,nxt''',_,pt''') = me nxt p c pt; (*nxt'''= Specify_Method ["diff", "integration"]*)
34 (*//------------------- step into me Specify_Method ["diff", "integration"] ---------------\\*)
35 "~~~~~ fun me , args:"; val (tac, p, _, pt) = (nxt''', p''', c, pt''');
37 (*Step.by_tactic is here for testing by me; do_next would suffice in me*)
38 case Step.by_tactic tac (pt, p) of
39 ("ok", (_, _, ptp)) => ptp
41 val ("ok", ([(Apply_Method ["diff", "integration"], _, _)], _, _)) = (*case*)
42 Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
43 "~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis))
44 = (p, ((pt, Pos.e_pos'), []));
45 (*if*) Pos.on_calc_end ip (*else*);
46 val (_, probl_id, _) = Calc.references (pt, p);
48 (*case*) tacis (*of*);
49 (*if*) probl_id = Problem.id_empty (*else*);
51 val ("ok", ([(Apply_Method ["diff", "integration"], _, _)], _, _)) =
52 Step.switch_specify_solve p_ (pt, ip);
53 "~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
54 (*if*) Pos.on_specification ([], state_pos) (*then*);
56 Step.specify_do_next (pt, input_pos);
57 "~~~~~ fun specify_do_next , args:"; val (ptp as (pt, (p, p_))) = (pt, input_pos);
58 val (_, (p_', tac)) = Specify.find_next_step ptp
59 val ist_ctxt = Ctree.get_loc pt (p, p_)
60 val Tactic.Apply_Method mI =
63 val ("ok", ([(Apply_Method ["diff", "integration"], _, _)], _, _)) =
64 LI.by_tactic (Tactic.Apply_Method' (mI, NONE, Istate.empty, ContextC.empty))
65 ist_ctxt (pt, (p, p_'));
66 "~~~~~ fun by_tactic , args:"; val ((Tactic.Apply_Method' (mI, _, _, _)), (_, ctxt), (pt, pos as (p, _)))
67 = ((Tactic.Apply_Method' (mI, NONE, Istate.empty, ContextC.empty)),
68 ist_ctxt, (pt, (p, p_')));
69 val (itms, oris, probl, o_spec, spec) = case get_obj I pt p of
70 PblObj {meth = itms, origin = (oris, o_spec, _), probl, spec, ...}
71 => (itms, oris, probl, o_spec, spec)
73 val (_, pI', _) = References.select_input o_spec spec
74 val (_, itms) = I_Model.s_make_complete ctxt oris
75 (I_Model.OLD_to_TEST probl, I_Model.OLD_to_TEST itms) (pI', mI)
77 val (is, env, ctxt, prog) = case
78 LItool.init_pstate ctxt itms mI of
79 (is as Pstate {env, ...}, ctxt, program) => (is, env, ctxt, program)
80 val ini = LItool.implicit_take ctxt prog env;
81 val pos = start_new_level pos
85 val Next_Step (iii, ccc, ttt) = (*case*)
86 LI.find_next_step prog (pt, (lev_dn p, Res)) is ctxt (*of*);
87 "~~~~~ fun find_next_step , args:"; val ((Rule.Prog prog), (ptp as (pt, pos as (p, _))), (Pstate ist), ctxt)
88 = (prog, (pt, (lev_dn p, Res)), is, ctxt);
91 scan_to_tactic (prog, (ptp, ctxt)) (Pstate ist) (*of*);
92 "~~~~~ fun scan_to_tactic , args:"; val ((prog, cc), (Pstate (ist as {path, ...})))
93 = ((prog, (ptp, ctxt)), (Pstate ist));
94 (*if*) path = [] (*then*);
96 val Accept_Tac (ttt, sss, ccc) =
97 scan_dn cc (trans_scan_dn ist) (Program.body_of prog);
98 "~~~~~ fun scan_dn , args:"; val (cc, ist, (Const (\<^const_name>\<open>Let\<close>(*1*), _) $ e $ (Abs (i, T, b))))
99 = (cc, (trans_scan_dn ist), (Program.body_of prog));
101 val Accept_Tac (ttt, sss, ccc) = (*case*)
102 scan_dn cc (ist |> path_down [L, R]) e (*of*);
103 "~~~~~ fun scan_dn , args:"; val ((cc as (_, ctxt)), (ist as {eval, ...}), t)
104 = (cc, (ist |> path_down [L, R]), e);
105 (*if*) Tactical.contained_in t (*else*);
106 val (Program.Tac prog_tac, form_arg) =
107 (*case*) LItool.check_leaf "next " ctxt eval (get_subst ist) t (*of*);
109 val Accept_Tac (ttt, sss, ccc) =
110 check_tac cc ist (prog_tac, form_arg);
111 "~~~~~ fun check_tac , args:"; val (((pt, p), ctxt), ist, (prog_tac, form_arg))
112 = (cc, ist, (prog_tac, form_arg));
113 val m = LItool.tac_from_prog (pt, p) prog_tac
115 (*//------------------ step into tac_from_prog ---------------------------------------------\\*)
116 (*keep for continuing check_tac ----------------------------*)
117 val return_tac_from_prog = m
118 (* args of tac_from_prog: ---------------------------------\*)
119 (*+*)val ([0], Res) = p (*isa == isa2*);
120 (*+*)pt (*Output isa == isa2*);
121 (*+*)val "([\"\n(f_f, x \<up> 2 + 1)\", \"\n(v_v, x)\"], [R, L, R], empty, NONE, \n??.empty, ORundef, false, false)"
122 = Istate.pstate2str ist (*isa == isa2*)
123 (*+*)val "Take (Integral x \<up> 2 + 1 D x)" = UnparseC.term @{context} prog_tac (*isa == isa2*)
124 (*+*)val NONE = form_arg (*isa == isa2*)
125 (* args of tac_from_prog: ---------------------------------/*)
126 (* return value ------------------------------------------\*)
127 (*+* )val Take "Integral x \<up> 2 + 1 D x" = m ( *isa <> isa2*)
128 (* return value ------------------------------------------/*)
130 "~~~~~ fun tac_from_prog , args:"; val ((pt, pos), intac) =
133 (*+*)val ([0], Res) = pos
135 val pos = Pos.back_from_new pos
136 val ctxt = Ctree.get_ctxt pt pos
137 val thy = Proof_Context.theory_of ctxt
138 (*-------------------- stop step into tac_from_prog ------------------------------------------*)
139 (*\\------------------ step into tac_from_prog ---------------------------------------------//*)
141 val m = return_tac_from_prog (*kept for continuing check_tac*)
147 Solve_Step.check m (pt, p) (*of*);
148 "~~~~~ fun check , args:"; val ((Tactic.Take str), (pt, pos as (p_, p))) = (m, (pt, p));
150 (*+*)val ([0], Res) = pos; (*<<<-------------------------*)
151 (*-------------------- stop step into me Specify_Method ["diff", "integration"] -------------*)
152 (*\\------------------- step into me Specify_Method ["diff", "integration"] ---------------//*)
154 val (p,_,f,nxt,_,pt) = me nxt''' p''' c pt''';
155 case nxt of (Apply_Method ["diff", "integration"]) => ()
156 | _ => error "integrate.sml -- me method [diff,integration] -- spec";
157 "----- step 8: returns nxt = Rewrite_Set_Inst ([\"(''bdv'', x)\"],\"integration\")";
159 "~~~~~ fun me, args:"; val (tac, (p:pos'), _, (pt:ctree)) = (nxt, p, c, pt);
160 "~~~~~ fun Step.by_tactic, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
161 val Applicable.Yes m = Step.check tac (pt, p);
162 (*if*) Tactic.for_specify' m; (*false*)
163 "~~~~~ fun loc_solve_ , args:"; val (m, (pt,pos)) = (m, ptp);
165 "~~~~~ fun Step_Solve.by_tactic , args:"; val (m as Apply_Method' (mI, _, _, ctxt), (pt, (pos as (p,_))))
167 val (itms, oris, probl, o_spec, spec) = case get_obj I pt p of
168 PblObj {meth = itms, origin = (oris, o_spec, _), probl, spec, ...}
169 => (itms, oris, probl, o_spec, spec)
170 | _ => raise ERROR ""
171 val (_, pI', _) = References.select_input o_spec spec
172 val (_, itms) = I_Model.s_make_complete ctxt oris
173 (I_Model.OLD_to_TEST probl, I_Model.OLD_to_TEST itms) (pI', mI)
175 val (is, env, ctxt, sc) = case
176 LItool.init_pstate ctxt itms mI of
177 (is as Pstate {env, ...}, ctxt, program) => (is, env, ctxt, program)
178 | _ => error "solve Apply_Method: uncovered case init_pstate";
179 (*+*)pstate2str (the_pstate is) = "([\"\n(f_f, x \<up> 2 + 1)\",\"\n(v_v, x)\"], [], empty, NONE, \n??.empty, ORundef, false, true)";
180 val ini = LItool.implicit_take ctxt sc env;
183 val NONE = (*case*) ini (*of*);
184 val Next_Step (is', ctxt', m') =
185 LI.find_next_step sc (pt, (p, Res)) is ctxt;
186 (*+*)pstate2str (the_pstate is') = "([\"\n(f_f, x \<up> 2 + 1)\",\"\n(v_v, x)\"], [R,L,R], empty, NONE, \nIntegral x \<up> 2 + 1 D x, ORundef, false, false)";
187 val Safe_Step (_, _, Take' _) = (*case*)
188 locate_input_tactic sc (pt, (p, Res)) is' ctxt' m' (*of*);
189 "~~~~~ fun locate_input_tactic , args:"; val ((Prog prog), cstate, istate, ctxt, tac)
190 = (sc, (pt, (p, Res)), is', ctxt', m');
192 (*case*) scan_to_tactic1 (prog, (cstate, ctxt, tac)) istate (*of*);
193 "~~~~~ fun scan_to_tactic1 , args:"; val ((prog, (cctt as ((_, p), _, _))), (Istate.Pstate (ist as {path, ...})))
194 = ((prog, (cstate, ctxt, tac)), istate);
195 (*if*) path = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*then*);
197 val Accept_Tac1 (_, _, Take' _) =
198 scan_dn1 cctt (ist |> set_path [R] |> set_or ORundef) (Program.body_of prog);
199 "~~~~~ fun scan_dn1 , args:"; val (xxx, ist, (Const (\<^const_name>\<open>Let\<close>, _) $ e $ (Abs (id, T, b))))
200 = (cctt, (ist |> set_path [R] |> set_or ORundef), (Program.body_of prog));
202 (*+*) if UnparseC.term @{context} e = "Take (Integral f_f D v_v)" then () else error "scan_dn1 Integral changed";
205 scan_dn1 xxx (ist |> path_down [L, R]) e (*of*);
206 (*======= end of scanning tacticals, a leaf =======*)
207 "~~~~~ fun scan_dn1 , args:"; val (((pt, p), ctxt, tac), (ist as {eval, or, ...}), t)
208 = (xxx, (ist |> path_down [L, R]), e);
209 val (Program.Tac stac, a') = check_leaf "locate" ctxt eval (get_subst ist) t;
213 "----------- re-build: fun locate_input_tactic -------------------------------------------------";
214 "----------- re-build: fun locate_input_tactic -------------------------------------------------";
215 "----------- re-build: fun locate_input_tactic -------------------------------------------------";
216 val fmz = ["equality (x+1=(2::real))", "solveFor x", "solutions L"];
217 val (dI',pI',mI') = ("Test", ["sqroot-test", "univariate", "equation", "test"],
218 ["Test", "squ-equ-test-subpbl1"]);
219 val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))];
220 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
221 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
222 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
223 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
224 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
225 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
226 (*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = (_, Apply_Method ["Test", "squ-equ-test-subpbl1"])*);
227 (*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Rewrite_Set", Rewrite_Set "norm_equation")*)
229 (*//------------------ begin step into ------------------------------------------------------\\*)
230 (*[1], Res*)val (p'''''_''',_,f,nxt'''''_''',_,pt'''''_''') = me nxt p [] pt; (*nxt = Rewrite_Set "Test_simplify"*)
232 "~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, [], pt);
234 (** )val (***)xxxx(***) ( *("ok", (_, _, (pt, p))) =( **) (*case*)
235 Step.by_tactic tac (pt,p) (*of*);
236 "~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
237 val Applicable.Yes m = (*case*) Solve_Step.check tac (pt, p) (*of*);
238 (*if*) Tactic.for_specify' m; (*false*)
240 (** )val (***)xxxxx_x(***) ( *(msg, cs') =( **)
241 Step_Solve.by_tactic m ptp;
242 "~~~~~ fun by_tactic , args:"; val (m, (pt, po as (p, p_))) = (m, ptp);
243 (*+*)val (pt'''''_', (p'''''_', p_'''''_')) = (pt, (p, p_));
244 (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p); (*else*)
245 val thy' = get_obj g_domID pt (par_pblobj pt p);
246 val (is, sc) = LItool.resume_prog (p,p_) pt;
248 locate_input_tactic sc (pt, po) (fst is) (snd is) m;
249 "~~~~~ fun locate_input_tactic , args:"; val (Prog prog, cstate, istate, ctxt, tac)
250 = (sc, (pt, po), (fst is), (snd is), m);
251 val prog_rls = get_simplifier cstate;
253 (** )val Accept_Tac1 ((is as (_,_,_,_,_,strong_ass), ctxt, ss as((tac', _, ctree, pos', _) :: _))) =( **)
254 (*case*) scan_to_tactic1 (prog, (cstate, ctxt, tac)) istate (*of*);
255 "~~~~~ fun scan_to_tactic1 , args:"; val ((prog, (cctt as ((_, p), _, _))), (Istate.Pstate (ist as {path, ...})))
256 = ((prog, (cstate, ctxt, tac)), istate);
257 (*if*) path = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*then*);
259 (** )val xxxxx_xx = ( **)
260 scan_dn1 cctt (ist |> set_path [R] |> set_or ORundef) (Program.body_of prog);
261 "~~~~~ fun scan_dn1 , args:"; val (xxx, ist, (Const (\<^const_name>\<open>Let\<close>, _) $ e $ (Abs (id, T, b))))
262 = (cctt, (ist |> set_path [R] |> set_or ORundef), (Program.body_of prog));
264 (*case*) scan_dn1 xxx (ist |> path_down [L, R]) e (*of*);
265 "~~~~~ fun scan_dn1 , args:"; val ((xxx as (cstate, _, _)), ist, (Const (\<^const_name>\<open>Chain\<close>(*1*), _) $ e1 $ e2 $ a))
266 = (xxx, (ist |> path_down [L, R]), e);
268 (*case*) scan_dn1 xxx (ist |> path_down_form ([L, L, R], a)) e1 (*of*);
269 "~~~~~ fun scan_dn1 , args:"; val (xxx, ist, (Const (\<^const_name>\<open>Try\<close>(*2*), _) $ e))
270 = (xxx, (ist |> path_down_form ([L, L, R], a)), e1);
272 (*case*) scan_dn1 xxx (ist |> path_down [R]) e (*of*);
273 (*======= end of scanning tacticals, a leaf =======*)
274 "~~~~~ fun scan_dn1 , args:"; val (((pt, p), ctxt, tac), (ist as {env, eval, or, ...}), t)
275 = (xxx, (ist |> path_down [R]), e);
276 val (Program.Tac stac, a') =
277 (*case*) check_leaf "locate" ctxt eval (get_subst ist) t (*of*);
278 val LItool.Associated (m, v', ctxt) =
279 (*case*) associate (pt, p) ctxt (m, stac) (*of*);
281 Accept_Tac1 (ist |> set_subst_true (a', v'), ctxt, m) (*return value*);
282 "~~~~~ from scan_dn1 to scan_to_tactic1 return val:"; val (xxxxx_xx)
283 = (Accept_Tac1 (ist |> set_subst_true (a', v'), ctxt, m));
285 "~~~~~ from scan_to_tactic1 to fun locate_input_tactic return val:"; val Accept_Tac1 ((ist as {assoc, ...}), ctxt, tac')
286 = (Accept_Tac1 (ist |> set_subst_true (a', v'), ctxt, m));
287 (*if*) LibraryC.assoc (*then*);
289 Safe_Step (Istate.Pstate ist, ctxt, tac') (*return value*);
290 "~~~~~ from locate_input_tactic to fun Step_Solve.by_tactic return:"; val Safe_Step (istate, ctxt, tac)
291 = (*xxxxx_xx*)(**)Safe_Step (Istate.Pstate ist, ctxt, tac')(**);
293 (*+*)val (pt, po as (p, p_)) = (pt'''''_', (p'''''_', p_'''''_')); (* from begin of by_tactic *)
294 val (p'', _, _,pt') =
295 Step.add tac (istate, ctxt) (pt, (lev_on p, Pbl));
298 ("ok", ([(Tactic.input_from_T ctxt tac, tac, (p'', (istate, ctxt)))],
299 [(*ctree NOT cut*)], (pt', p''))) (*return value*);
300 "~~~~~ from Step_Solve.by_tactic \<longrightarrow> Step.by_tactic return:"; val ((msg, cs' : Calc.state_post))
301 = ("ok", ([(Tactic.input_from_T ctxt tac, tac, (p'', (istate, ctxt)) )],
302 [(*ctree NOT cut*)], (pt', p'')));
304 "~~~~~ from Step.by_tactic to me return:"; val (("ok", (_, _, (pt, p)))) = (*** )xxxx( ***) ("ok", cs');
306 (case Step.do_next p ((pt, Pos.e_pos'), []) of
307 ("ok", (ts as (_, _, _) :: _, _, _)) => ("", ts)
308 | ("helpless", _) => ("helpless: cannot propose tac", [])
309 | ("no-fmz-spec", _) => error "no-fmz-spec"
310 | ("end-of-calculation", (ts, _, _)) => ("", ts)
311 | _ => error "me: uncovered case")
312 handle ERROR msg => raise ERROR msg
315 tacis as (_::_) => let val (tac, _, _) = last_elem tacis in tac end
316 | _ => if p = ([], Pos.Res) then Tactic.End_Proof' else Tactic.Empty_Tac;
318 (p, [] : NEW, TESTg_form ctxt (pt, p), (Tactic.tac2IDstr tac, tac), Celem.Sundef, pt);
319 "~~~~~ from me to TOOPLEVEL return:"; val (p,_,f,nxt,_,pt)
320 = (*** )xxx( ***) (p, [] : NEW, TESTg_form ctxt (pt, p), (Tactic.tac2IDstr tac, tac), Celem.Sundef, pt);
322 (*//--------------------- check results from modified me ----------------------------------\\*)
323 if p = ([2], Res) andalso
324 pr_ctree ctxt pr_short pt = ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 = 2\n"
326 (case nxt of ("Rewrite_Set", Rewrite_Set "Test_simplify") => ()
328 else error "check results from modified me CHANGED";
329 (*\\--------------------- check results from modified me ----------------------------------//*)
331 "~~~~~ from me to TOPLEVEL return:"; val (p,_,f,nxt,_,pt) = (*** )xxx( ***) (**)(p, 000, f, nxt, 000, pt)(**);
332 (*\\------------------ end step into --------------------------------------------------------//*)
334 (*[3], Res*)val (p,_,f,nxt,_,pt) = me nxt'''''_''' p'''''_''' [] pt'''''_'''; (*nxt = Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"])*)
335 (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Model_Problem*)
336 (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "equality (- 1 + x = 0)"*)
337 (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "solveFor x"*)
338 (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Find "solutions x_i"*)
339 (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Theory "Test"*)
340 (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Problem ["LINEAR", "univariate", "equation", "test"]*)
341 (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Method ["Test", "solve_linear"]*)
342 (*[3], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["Test", "solve_linear"]*)
343 (*[3, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv")*)
344 (*[3, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "Test_simplify"*)
345 (*[3, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["LINEAR", "univariate", "equation", "test"]*)
346 (*[3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_elementwise "Assumptions"*)
347 (*[4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["sqroot-test", "univariate", "equation", "test"]*)
348 (*[], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = End_Proof'*)
350 (*/--------------------- final test ----------------------------------\\*)
351 if p = ([], Res) andalso f2str f = "[x = 1]" andalso pr_ctree ctxt pr_short pt =
352 ". ----- pblobj -----\n" ^
354 "2. x + 1 + - 1 * 2 = 0\n" ^
355 "3. ----- pblobj -----\n" ^
356 "3.1. - 1 + x = 0\n" ^
357 "3.2. x = 0 + - 1 * - 1\n" ^
359 then case nxt of End_Proof' => () | _ => error "re-build: fun locate_input_tactic changed 1"
360 else error "re-build: fun locate_input_tactic changed 2";
363 "----------- fun locate_input_tactic Helpless, NOT applicable ----------------------------------";
364 "----------- fun locate_input_tactic Helpless, NOT applicable ----------------------------------";
365 "----------- fun locate_input_tactic Helpless, NOT applicable ----------------------------------";
366 (*cp from -- try fun applyTactics ------- *)
367 val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(["Term (5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12)",
369 ("PolyMinus",["plus_minus", "polynom", "vereinfachen"],
370 ["simplification", "for_polynomials", "with_minus"]))];
371 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
372 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
373 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
374 (*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "ordne_alphabetisch"*)
376 (*+*)val Test_Out.FormKF "5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * g + 12" = f
378 (*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "fasse_zusammen"*)
380 (*+*)if map (Tactic.input_to_string ctxt) (specific_from_prog pt p) =
381 ["Rewrite (\"subtrahiere_x_plus_minus\", \"\<lbrakk>?l is_num; ?m is_num\<rbrakk>\n\<Longrightarrow> ?x + ?m * ?v - ?l * ?v = ?x + (?m - ?l) * ?v\")",
382 "Rewrite (\"subtrahiere_x_minus_plus\", \"\<lbrakk>?l is_num; ?m is_num\<rbrakk>\n\<Longrightarrow> ?x - ?m * ?v + ?l * ?v = ?x + (- ?m + ?l) * ?v\")",
383 (*this is new since ThmC.numerals_to_Free.-----\\*)
385 then () else error "specific_from_prog ([1], Res) 1 CHANGED";
386 (*[2], Res*)val ("ok", (_, _, ptp as (pt, p))) = Step.by_tactic (hd (specific_from_prog pt p)) (pt, p);
388 (*+*)if map (Tactic.input_to_string @{context}) (specific_from_prog pt p) = [
389 "Rewrite (\"tausche_minus\", \"\<lbrakk>?b ist_monom; ?a kleiner ?b\<rbrakk>\n\<Longrightarrow> ?b - ?a = - ?a + ?b\")",
390 "Rewrite (\"subtrahiere_x_plus_minus\", \"\<lbrakk>?l is_num; ?m is_num\<rbrakk>\n\<Longrightarrow> ?x + ?m * ?v - ?l * ?v = ?x + (?m - ?l) * ?v\")",
391 "Rewrite (\"subtrahiere_x_minus_plus\", \"\<lbrakk>?l is_num; ?m is_num\<rbrakk>\n\<Longrightarrow> ?x - ?m * ?v + ?l * ?v = ?x + (- ?m + ?l) * ?v\")",
392 (*this is new since ThmC.numerals_to_Free.-----\\*)
394 (*this is new since ThmC.numerals_to_Free.-----//*)
396 then () else error "specific_from_prog ([1], Res) 2 CHANGED";
397 (* = ([3], Res)*)val ("ok", (_, _, ptp as (pt, p))) = Step.by_tactic (hd (specific_from_prog pt p)) (pt, p);
399 (*//----------------- exception PTREE "get_obj f EmptyPtree" raised --------------------------\\*)
400 (**)val ("ok", ([(Rewrite ("tausche_minus", _), _, _)], _, _)) = (*isa*)
401 Step.by_tactic (hd (specific_from_prog pt p)) (pt, p);
402 "~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (hd (specific_from_prog pt p), (pt, p));
403 val Applicable.Yes m = (*case*) Solve_Step.check tac (pt, p) (*of*);
404 (*if*) Tactic.for_specify' m; (*false*)
406 (**) val ("ok", ([(Rewrite ("tausche_minus", _), _, _)], _, _)) = (*isa*)
407 Step_Solve.by_tactic m (pt, p);
408 "~~~~~ fun by_tactic , args:"; val (m, (pt, po as (p, p_))) = (m, (pt, p));
409 (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
410 val thy' = get_obj g_domID pt (par_pblobj pt p);
411 val (is, sc) = LItool.resume_prog (p,p_) pt;
413 (*case*) locate_input_tactic sc (pt, po) (fst is) (snd is) m (*of*);
414 "~~~~~ fun locate_input_tactic , args:"; val ((Rule.Prog prog), (cstate as (pt, (*?*)pos(*?*))), istate, ctxt, tac)
415 = (sc, (pt, po), (fst is), (snd is), m);
416 val prog_rls = LItool.get_simplifier cstate (*TODO: shift into Istate.T*);
418 (*case*) scan_to_tactic1 (prog, (cstate, ctxt, tac)) istate (*of*);
419 "~~~~~ fun scan_to_tactic1 , args:"; val ((prog, (cctt as ((_, p), _, _))), (Istate.Pstate (ist as {path, ...})))
420 = ((prog, (cstate, ctxt, tac)), istate);
421 (*if*) path = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*else*);
423 go_scan_up1 (prog, cctt) ist;
424 "~~~~~ fun go_scan_up1 , args:"; val ((pcct as (prog, _)), (ist as {path, ...}))
425 = ((prog, cctt), ist);
426 (*if*) 1 < length path (*then*);
428 scan_up1 pcct (ist |> path_up) (TermC.sub_at (path_up' path) prog);
429 "~~~~~ and scan_up1 , args:"; val (pcct, ist, (Const (\<^const_name>\<open>Try\<close>(*2*), _) $ _))
430 = (pcct, (ist |> path_up), (TermC.sub_at (path_up' path) prog));
432 go_scan_up1 pcct ist;
433 "~~~~~ and go_scan_up1 , args:"; val ((pcct as (prog, _)), (ist as {path, ...}))
435 (*if*) 1 < length path (*then*);
437 scan_up1 pcct (ist |> path_up) (TermC.sub_at (path_up' path) prog);
438 "~~~~~ and scan_up1 , args:"; val ((pcct as (prog, cct as (cstate, _, _))), ist,
439 (Const (\<^const_name>\<open>Chain\<close>(*3*), _) $ _ ))
440 = (pcct, (ist |> path_up), (TermC.sub_at (path_up' path) prog));
441 val e2 = check_Seq_up ctxt ist prog
443 (*case*) scan_dn1 cct (ist |> path_up_down [R] |> set_or ORundef) e2 (*of*);
444 "~~~~~ fun scan_dn1 , args:"; val (yyy, ist, (Const (\<^const_name>\<open>Chain\<close>(*2*), _) $ e1 $ e2))
445 = (cct, (ist |> path_up_down [R] |> set_or ORundef), e2);
447 (*case*) scan_dn1 cct (ist |> path_down [L, R]) e1 (*of*);
448 "~~~~~ fun scan_dn1 , args:"; val (xxx, ist, (Const (\<^const_name>\<open>Try\<close>(*2*), _) $ e))
449 = (cct, (ist |> path_down [L, R]), e1);
451 (*case*) scan_dn1 cct (ist |> path_down [R]) e (*of*);
452 (*======= end of scanning tacticals, a leaf =======*)
453 "~~~~~ fun scan_dn1 , args:"; val ((cct as (_, ctxt, _)), (ist as {eval, ...}), t)
454 = (cct, (ist |> path_down [R]), e);
455 (*if*) Tactical.contained_in t (*else*);
456 val (Program.Tac prog_tac, form_arg) = (*case*)
457 LItool.check_leaf "locate" ctxt eval (get_subst ist) t (*of*);
459 check_tac1 cct ist (prog_tac, form_arg);
460 "~~~~~ fun check_tac1 , args:"; val (((pt, p), ctxt, tac), (ist as {act_arg, or, ...}), (prog_tac, form_arg)) =
461 (cct, ist, (prog_tac, form_arg));
462 val LItool.Not_Associated = (*case*)
463 LItool.associate (pt, p) ctxt (tac, prog_tac) (*of*);
464 val _(*ORundef*) = (*case*) or (*of*);
466 (*+*)Solve_Step.check (LItool.tac_from_prog (pt, p) prog_tac) (pt, p);
468 val Applicable.Yes m' =
469 (*case*) Solve_Step.check (LItool.tac_from_prog (pt, p) prog_tac) (pt, p) (*of*);
471 Reject_Tac1 (ist |> set_subst_false (form_arg, Tactic.result @{context} m'), ctxt, tac)
472 (*return from check_tac1*);
473 "~~~~~ from fun check_tac1 \<longrightarrow>fun scan_dn1 \<longrightarrow>fun scan_dn1 \<longrightarrow>fun locate_input_tactic , return:"; val (Reject_Tac1 _) =
474 (Reject_Tac1 (ist |> set_subst_false (form_arg, Tactic.result @{context} m'), ctxt, tac));
476 val Test_Out.FormKF "- 9 + 12 + 5 * e - 7 * e + 6 * f - 4 * f - 8 * g + 10 * g" = f;
480 "----------- re-build: fun find_next_step, mini ------------------------------------------------";
481 "----------- re-build: fun find_next_step, mini ------------------------------------------------";
482 "----------- re-build: fun find_next_step, mini ------------------------------------------------";
483 val fmz = ["Term (a + a ::real)", "normalform n_n"];
484 val (dI',pI',mI') = ("Poly",["polynomial", "simplification"],["simplification", "for_polynomials"]);
485 val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))];
486 (*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, Pos.e_pos'), []);(*Model_Problem*)
487 (*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, Pos.e_pos'), []);(*Specify_Theory "Poly"*)
488 (*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, Pos.e_pos'), []);(*Specify_Problem ["polynomial", "simplification"]*)
489 (*[], Met*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Specify_Method ["simplification", "for_polynomials"]*)
490 (*1], Frm*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Apply_Method ["simplification", "for_polynomials"]*)
491 (*[1], Res*)val (_, ([(tac'''''_', _, _)], _, (pt'''''_', p'''''_'))) =
493 Step.do_next p ((pt, e_pos'), []);(*Rewrite_Set "norm_Poly"*)
494 (*//------------------ go into 1 ------------------------------------------------------------\\*)
495 "~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis))
496 = (p, ((pt, e_pos'), []));
497 val pIopt = Ctree.get_pblID (pt, ip);
498 (*if*) ip = ([], Res) (*else*);
499 val _ = (*case*) tacis (*of*);
500 val SOME _ = (*case*) pIopt (*of*);
501 (*if*) member op = [Pos.Pbl, Pos.Met] p_ (*else*);
503 val ("ok", ([(Rewrite_Set "norm_Poly", _, _)], _, (_, ([1], Res)))) =
504 Step_Solve.do_next (pt, ip);
505 "~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
506 (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
507 val thy' = get_obj g_domID pt (par_pblobj pt p);
508 val ((ist, ctxt), sc) = LItool.resume_prog (p,p_) pt;
510 val Next_Step (_, _, Rewrite_Set' ("Poly", _, Rule_Set.Sequence {id = "norm_Poly", ...}, _, _)) =
511 LI.find_next_step sc (pt, pos) ist ctxt (*of*);
512 "~~~~~ fun find_next_step , args:"; val ((Rule.Prog prog), (ptp as(pt, (p, _))), (Pstate ist), ctxt)
513 = (sc, (pt, pos), ist, ctxt);
515 val Accept_Tac (Rewrite_Set' ("Poly", _, Rule_Set.Sequence {id = "norm_Poly", ...}, _, _), _, _) =
516 (*case*) scan_to_tactic (prog, (ptp, ctxt)) (Pstate ist) (*of*);
517 "~~~~~ fun scan_to_tactic , args:"; val ((prog, cc), (Pstate (ist as {path, ...})))
518 = ((prog, (ptp, ctxt)), (Pstate ist));
519 (*if*) path = [] (*then*);
521 val Accept_Tac (Rewrite_Set' ("Poly", _, Rule_Set.Sequence {id = "norm_Poly", ...}, _, _), _, _) =
522 scan_dn cc (trans_scan_dn ist) (Program.body_of prog);
523 "~~~~~ fun scan_dn , args:"; val ((cc as (_, ctxt)), (ist as {eval, ...}), t)
524 = (cc, (trans_scan_dn ist), (Program.body_of prog));
525 (*if*) Tactical.contained_in t (*else*);
526 val (Program.Tac prog_tac, form_arg) = (*case*) LItool.check_leaf "next " ctxt eval (get_subst ist) t (*of*);
528 val Accept_Tac (Rewrite_Set' ("Poly", _, Rule_Set.Sequence {id = "norm_Poly", ...}, _, _), _, _) =
529 check_tac cc ist (prog_tac, form_arg) (*return from xxx*);
530 "~~~~~ from fun scan_dn\<longrightarrow>fun scan_to_tactic\<longrightarrow>fun find_next_step, return:"; val (Accept_Tac (tac, ist, ctxt))
531 = (check_tac cc ist (prog_tac, form_arg));
533 Next_Step (Pstate ist, Tactic.insert_assumptions tac ctxt, tac) (*return from find_next_step*);
534 "~~~~~ from fun find_next_step\<longrightarrow>and do_next\<longrightarrow>fun zzz, return:"; val (Next_Step (ist, ctxt, tac))
535 = (Next_Step (Pstate ist, Tactic.insert_assumptions tac ctxt, tac));
537 LI.by_tactic tac (ist, Tactic.insert_assumptions tac ctxt) ptp (*return from and do_next*);
538 "~~~~~ from and do_next\<longrightarrow>fun do_next\<longrightarrow>toplevel, return:"; val (_, ([(tac''''', _, _)], _, (pt''''', p''''')))
539 = (LI.by_tactic tac (ist, Tactic.insert_assumptions tac ctxt) ptp);
540 (*\\------------------ end of go into 1 -----------------------------------------------------//*)
542 (*[], Res*)val (_, ([(tac''''', _, _)], _, (pt''''', p'''''))) =
544 Step.do_next p'''''_' ((pt'''''_', Pos.e_pos'), []);(* Check_Postcond ["polynomial", "simplification"]*)
545 (*//------------------ go into 2 ------------------------------------------------------------\\*)
546 "~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis))
547 = (p''''', ((pt''''', e_pos'), []));
548 val pIopt = Ctree.get_pblID (pt, ip);
549 (*if*) ip = ([], Res) (*else*);
550 val _ = (*case*) tacis (*of*);
551 val SOME _ = (*case*) pIopt (*of*);
552 (*if*) member op = [Pos.Pbl, Pos.Met] p_ (*else*);
554 val ("ok", ([(Check_Postcond ["polynomial", "simplification"], _, _)], _, (_, ([], Res)))) =
555 Step_Solve.do_next (pt, ip);
556 "~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
557 (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
558 val thy' = get_obj g_domID pt (par_pblobj pt p);
559 val ((ist, ctxt), sc) = LItool.resume_prog (p,p_) pt;
561 (** )val End_Program (ist, tac) =
562 ( *case*) LI.find_next_step sc (pt, pos) ist ctxt (*of*);
563 "~~~~~ fun find_next_step , args:"; val ((Rule.Prog prog), (ptp as(pt, (p, _))), (Pstate ist), ctxt)
564 = (sc, (pt, pos), ist, ctxt);
566 (* val Term_Val (Const (\<^const_name>\<open>times\<close>, _) $ Free ("2", _) $ Free ("a", _))*)
567 (**)val Term_Val prog_result =
568 (*case*) scan_to_tactic (prog, (ptp, ctxt)) (Pstate ist) (*of*);
569 "~~~~~ fun scan_to_tactic , args:"; val ((prog, cc), (Pstate (ist as {path, ...})))
570 = ((prog, (ptp, ctxt)), (Pstate ist));
571 (*if*) path = [] (*else*);
573 go_scan_up (prog, cc) (trans_scan_up ist |> set_found);
574 "~~~~~ fun go_scan_up , args:"; val ((pcc as (sc, _)), (ist as {path, act_arg, found_accept, ...}))
575 = ((prog, cc), (trans_scan_up ist(*|> set_found !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! *)));
576 (*if*) path = [R] (*then*);
577 (*if*) found_accept = true (*then*);
579 Term_Val act_arg (*return from go_scan_up*);
580 "~~~~~ from fun go_scan_up\<longrightarrow>fun scan_to_tactic, return:"; val (Term_Val prog_result) = (Term_Val act_arg);
582 Term_Val prog_result (*return from scan_to_tactic*);
583 "~~~~~ from fun scan_to_tactic\<longrightarrow>fun find_next_step, return:"; val (Term_Val prog_result) = (Term_Val prog_result);
584 val (true, p' as [], Rule_Set.Empty, _) = (*case*) parent_node pt pos (*of*);
585 val (_, pblID, _) = get_obj g_spec pt p';
587 End_Program (Pstate ist, Tactic.Check_Postcond' (pblID, prog_result))
588 (*return from find_next_step*);
589 "~~~~~ from fun find_next_step\<longrightarrow>and do_next\<longrightarrow>fun zzz, return:"; val (End_Program (ist, tac))
590 = (End_Program (Pstate ist, Tactic.Check_Postcond' (pblID,prog_result)));
591 val _ = (*case*) tac (*of*);
593 val ("ok", ([(Check_Postcond ["polynomial", "simplification"], _, _)], _, (_, ([], Res))))
594 = LI.by_tactic tac (ist, ctxt) ptp (*return from and do_next*);
595 "~~~~~ from and do_next\<longrightarrow>top level, return:"; val (_, ([(tac''''', _, _)], _, (pt''''', p''''')))
596 = (LI.by_tactic tac (ist, ctxt) ptp);
597 (*\\------------------ end of go into 2 -----------------------------------------------------//*)
599 (*[], Und*)val (msg, ([], _, (pt, p))) = Step.do_next p''''' ((pt''''', Pos.e_pos'), []);(**)
601 Test_Tool.show_pt_tac pt; (*[
602 ([], Frm), Simplify (a + a)
603 . . . . . . . . . . Apply_Method ["simplification", "for_polynomials"],
605 . . . . . . . . . . Rewrite_Set "norm_Poly",
607 . . . . . . . . . . Check_Postcond ["polynomial", "simplification"],
610 (*/--- final test ---------------------------------------------------------------------------\\*)
611 val (res, asm) = (get_obj g_result pt (fst p));
612 if UnparseC.term @{context} res = "2 * a" andalso map (UnparseC.term @{context}) asm = []
613 andalso p = ([], Und) andalso msg = "end-of-calculation"
614 andalso pr_ctree ctxt pr_short pt = ". ----- pblobj -----\n1. a + a\n"
616 case tac''''' of Check_Postcond ["polynomial", "simplification"] => ()
617 | _ => error "re-build: fun find_next_step, mini 1"
618 else error "re-build: fun find_next_step, mini 2"
621 "----------- re-build: fun locate_input_term ---------------------------------------------------";
622 "----------- re-build: fun locate_input_term ---------------------------------------------------";
623 "----------- re-build: fun locate_input_term ---------------------------------------------------";
625 ----------- appendFormula: on Res + late deriv ------------------------------------------------*)
626 val fmz = ["equality (x+1=(2::real))", "solveFor x", "solutions L"];
627 val (dI',pI',mI') = ("Test", ["sqroot-test", "univariate", "equation", "test"],
628 ["Test", "squ-equ-test-subpbl1"]);
629 val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))];
630 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
631 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
632 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
633 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
634 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
635 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
636 (*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*Apply_Method ["Test", "squ-equ-test-subpbl1"]*);
638 (*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Rewrite_Set "norm_equation"*)
639 (*+*)if f2str f = "x + 1 = 2" then () else error "locate_input_term at ([1], Frm) CHANGED";
641 (*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Rewrite_Set "Test_simplify"*)
642 (*+*)if f2str f = "x + 1 + - 1 * 2 = 0" then () else error "locate_input_term at ([1], Frm) CHANGED";
644 Test_Tool.show_pt_tac pt; (*[
645 ([], Frm), solve (x + 1 = 2, x)
646 . . . . . . . . . . Apply_Method ["Test", "squ-equ-test-subpbl1"],
647 ([1], Frm), x + 1 = 2
648 . . . . . . . . . . Rewrite_Set "norm_equation",
649 ([1], Res), x + 1 + - 1 * 2 = 0 ///Check_Postcond..ERROR*)
651 (*//---------- appendFormula 1 "x = 1" \<longrightarrow> Step_Solve.inform \<longrightarrow> LI.locate_input_term ----------\\*)
652 "~~~~~ fun appendFormula , args:"; val ((*cI, *) ifo: TermC.as_string) = ((**) "x = 1");
653 val cs = (*States.get_calc cI*) ((pt, p), [(*nxt, nxt_, (pos, (ist, ctxt))*)])
654 val pos = (*States.get_pos cI 1*) p
656 (*+*)val ptp''''' = (pt, p);
657 (*+*)if snd ptp''''' = ([1], Res) then () else error "old_cs changed";
658 (*+*)Test_Tool.show_pt_tac pt; (*[
659 (*+*)([], Frm), solve (x + 1 = 2, x)
660 (*+*). . . . . . . . . . Apply_Method ["Test", "squ-equ-test-subpbl1"],
661 (*+*)([1], Frm), x + 1 = 2
662 (*+*). . . . . . . . . . Rewrite_Set "norm_equation",
663 (*+*)([1], Res), x + 1 + - 1 * 2 = 0 ///Check_Postcond*)
665 val ("ok", cs' as (_, _, ptp')) =
666 (*case*) Step.do_next pos cs (*of*);
668 val ("ok", (_(*use in DG !!!*), [], ptp''''' as (pt''''', p'''''))) = (*case*)
669 Step_Solve.by_term ptp' (encode ifo) (*of*);
670 "~~~~~ fun Step_Solve.by_term , args:"; val ((pt, pos as (p, _)), istr)
671 = (ptp', (encode ifo));
673 (*case*) ParseC.term_opt (get_ctxt pt pos) istr (*of*);
674 val pos_pred = lev_back(*'*) pos
675 val f_pred = Ctree.get_curr_formula (pt, pos_pred);
676 val f_succ = Ctree.get_curr_formula (pt, pos);
677 (*if*) f_succ = f_in (*else*);
679 (*case*) CAS_Cmd.input f_in (*of*);
681 (*NEW*) LI.locate_input_term (pt, pos) f_in (*of*);
682 "~~~~~ fun locate_input_term , args:"; val ((pt, pos), tm) = ((pt, pos), f_in);
683 val pos_pred = Pos.lev_back' pos (*f_pred ---"step pos cs"---> f_succ in appendFormula*)
685 val ("ok", (_, _, cstate as (pt', pos'))) =
686 (*case*) compare_step ([], [], (pt, pos_pred)) tm (*of*);
689 Found_Step (cstate, get_istate_LI pt' pos', get_ctxt pt' pos') (*return from locate_input_term*);
691 (*NEW*) Found_Step cstate (*return from locate_input_term*);
692 (*LI.Found_Step ( *)cstate(*, _(*istate*), _)( *return from locate_input_term*);
693 "~~~~~ from fun locate_input_term\<longrightarrow>fun Step_Solve.by_term, return:"; val ("ok", (_(*use in DG !!!*), c, ptp as (_, p)))
694 = (("ok" , ([], [], cstate (* already contains istate, ctxt *))));
696 ("ok", ((*_ use in DG !!!,*) c, ptp(* as (_*), p))(*)*)(*return from Step_Solve.by_term*);
697 "~~~~~ from fun Step_Solve.by_term\<longrightarrow>(fun appendFormula)!toplevel, return:"; val ("ok", (_(*use in DG !!!*), [], ptp''''' as (pt''''', p''''')))
698 = ("ok", ([], [], ptp));
700 (*fun me requires nxt...*)
701 Step.do_next p''''' (ptp''''', []);
702 val ("ok", ([(nxt'''''_' as Check_Postcond ["LINEAR", "univariate", "equation", "test"], _, _)], _,
703 (pt'''''_', p'''''_'))) = Step.do_next p''''' (ptp''''', [])
704 (*\\---------- appendFormula 1 "x = 1" \<longrightarrow> Step_Solve.inform \<longrightarrow> LI.locate_input_term ----------//*)
706 (*//----- REPLACED BY appendFormula 1 "x = 1" \<longrightarrow> Step_Solve.inform \<longrightarrow> LI.locate_input_term -----\\* )
707 (*[2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"])*)
708 (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Model_Problem*)
709 (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "equality (- 1 + x = 0)"*)
710 (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "solveFor x"*)
711 (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Find "solutions x_i"*)
712 (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Theory "Test"*)
713 (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Problem ["LINEAR", "univariate", "equation", "test"]*)
714 (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Method ["Test", "solve_linear"]*)
715 (*[3], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["Test", "solve_linear"]*)
716 (*[3, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv")*)
717 (*[3, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "Test_simplify"*)
718 (*[3, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["LINEAR", "univariate", "equation", "test"]*)
719 ( *\\----- REPLACED BY appendFormula 1 "x = 1" \<longrightarrow> Step_Solve.inform \<longrightarrow> LI.locate_input_term -----//*)
721 (*[3], Res*)val (p,_,f,nxt,_,pt) = me nxt'''''_' p'''''_' [] pt'''''_'; (*nxt = Check_elementwise "Assumptions"*)
722 (*[4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["sqroot-test", "univariate", "equation", "test"]*)
723 (*[], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = End_Proof'*)
725 (*/--- final test ---------------------------------------------------------------------------\\*)
726 if p = ([], Res) andalso f2str f = "[x = 1]" andalso pr_ctree ctxt pr_short pt =
727 ". ----- pblobj -----\n" ^
729 "2. x + 1 + - 1 * 2 = 0\n" ^
730 "3. ----- pblobj -----\n" ^
731 "3.1. - 1 + x = 0\n" ^
732 "3.2. x = 0 + - 1 * - 1\n" ^
733 "3.2.1. x = 0 + - 1 * - 1\n" ^
734 "3.2.2. x = 0 + 1\n" (*ATTENTION: see complete Calc below*)
735 then case nxt of End_Proof' => () | _ => error "re-build: fun locate_input_term CHANGED 1"
736 else error "re-build: fun locate_input_term CHANGED 2";
738 Test_Tool.show_pt_tac pt; (*[
739 ([], Frm), solve (x + 1 = 2, x)
740 . . . . . . . . . . Apply_Method ["Test", "squ-equ-test-subpbl1"],
741 ([1], Frm), x + 1 = 2
742 . . . . . . . . . . Rewrite_Set "norm_equation",
743 ([1], Res), x + 1 + - 1 * 2 = 0
744 . . . . . . . . . . Rewrite_Set "Test_simplify",
745 ([2], Res), - 1 + x = 0
746 . . . . . . . . . . Subproblem (Test, ["LINEAR", "univariate", "equation", "test"]),
747 ([3], Pbl), solve (- 1 + x = 0, x)
748 . . . . . . . . . . Apply_Method ["Test", "solve_linear"],
749 ([3,1], Frm), - 1 + x = 0
750 . . . . . . . . . . Rewrite_Set_Inst ([(''bdv'', x)], "isolate_bdv"),
751 ([3,1], Res), x = 0 + - 1 * - 1
752 . . . . . . . . . . Derive Test_simplify,
753 ([3,2,1], Frm), x = 0 + - 1 * - 1
754 . . . . . . . . . . Rewrite ("#: - 1 * - 1 = 1", "- 1 * - 1 = 1"),
755 ([3,2,1], Res), x = 0 + 1
756 . . . . . . . . . . Rewrite ("radd_0", "0 + ?k = ?k"),
757 ([3,2,2], Res), x = 1
758 . . . . . . . . . . Tactic.input_to_string not impl. for ?!,
760 . . . . . . . . . . Check_Postcond ["LINEAR", "univariate", "equation", "test"],
762 . . . . . . . . . . Check_Postcond ["sqroot-test", "univariate", "equation", "test"],
763 ([], Res), [x = 1]]*)