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, but applicable ----------------------------------";
12 "----------- re-build: fun determine_next_tactic -----------------------------------------------";
13 "----------- re-build: fun locate_input_formula ------------------------------------------------";
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 val p = e_pos'; val c = [];
22 val (p,_,f,nxt,_,pt) =
24 [(["functionTerm (x^^^2 + 1)", "integrateBy x", "antiDerivative FF"],
25 ("Integrate", ["integrate","function"], ["diff","integration"]))];
26 val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = ("Tac ", ...) --> Add_Given...*)
27 val (p,_,f,nxt,_,pt) = me nxt p c pt;
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;
32 val (p,_,f,nxt,_,pt) = me nxt p c pt;
33 case nxt of (_, Apply_Method ["diff", "integration"]) => ()
34 | _ => error "integrate.sml -- me method [diff,integration] -- spec";
35 "----- step 8: returns nxt = Rewrite_Set_Inst ([\"(''bdv'', x)\"],\"integration\")";
37 "~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), _, (pt:ctree)) = (nxt, p, c, pt);
38 "~~~~~ fun locatetac, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
39 val (mI,m) = mk_tac'_ tac;
40 val Appl m = applicable_in p pt m;
41 member op = specsteps mI (*false*);
42 "~~~~~ fun loc_solve_ , args:"; val (m, (pt,pos)) = ((mI,m), ptp);
44 "~~~~~ fun solve , args:"; val ((_, m as Apply_Method' (mI, _, _, ctxt)), (pt, (pos as (p,_)))) =
46 val {srls, ...} = get_met mI;
47 val itms = case get_obj I pt p of
48 PblObj {meth=itms, ...} => itms
49 | _ => error "solve Apply_Method: uncovered case get_obj"
50 val thy' = get_obj g_domID pt p;
51 val thy = Celem.assoc_thy thy';
52 val srls = Lucin.get_simplifier (pt, pos)
53 val (is, env, ctxt, sc) = case Lucin.init_pstate srls ctxt itms mI of
54 (is as Istate.Pstate {env, ...}, ctxt, sc) => (is, env, ctxt, sc)
55 | _ => error "solve Apply_Method: uncovered case init_pstate";
56 (*+*)scrstate2str (the_pstate is) = "([\"\n(f_f, x ^^^ 2 + 1)\",\"\n(v_v, x)\"], [], e_rls, NONE, \n??.empty, ORundef, AppUndef_, true)";
57 val ini = Lucin.init_form thy sc env;
60 val NONE = (*case*) ini (*of*);
61 val Next_Step (is', ctxt', m') =
62 LucinNEW.determine_next_tactic sc (pt, (p, Res)) is ctxt;
63 (*+*)scrstate2str (the_pstate is') = "([\"\n(f_f, x ^^^ 2 + 1)\",\"\n(v_v, x)\"], [R,L,R], e_rls, NONE, \nIntegral x ^^^ 2 + 1 D x, ORundef, AppUndef_, false)";
64 val Safe_Step (_, _, Take' _) = (*case*)
65 locate_input_tactic sc (pt, (p, Res)) is' ctxt' m' (*of*);
66 "~~~~~ fun locate_input_tactic , args:"; val ((Prog prog), cstate, istate, ctxt, tac)
67 = (sc, (pt, (p, Res)), is', ctxt', m');
69 (*case*) scan_to_tactic1 (prog, (cstate, ctxt, tac)) istate (*of*);
70 "~~~~~ fun scan_to_tactic1 , args:"; val ((prog, (cctt as ((_, p), _, _))), (Istate.Pstate (ist as {path, ...})))
71 = ((prog, (cstate, ctxt, tac)), istate);
72 (*if*) path = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*then*);
74 val Accept_Tac1 (_, _, Take' _) =
75 scan_dn1 cctt (ist |> set_path [R] |> set_or ORundef) (Program.body_of prog);
76 "~~~~~ fun scan_dn1 , args:"; val (xxx, ist, (Const ("HOL.Let", _) $ e $ (Abs (id, T, b))))
77 = (cctt, (ist |> set_path [R] |> set_or ORundef), (Program.body_of prog));
79 (*+*) if term2str e = "Take (Integral f_f D v_v)" then () else error "scan_dn1 Integral changed";
82 scan_dn1 xxx (ist |> path_down [L, R]) e (*of*);
83 (*======= end of scanning tacticals, a leaf =======*)
84 "~~~~~ fun scan_dn1 , args:"; val (((pt, p), ctxt, tac), (ist as {eval, or, ...}), t)
85 = (xxx, (ist |> path_down [L, R]), e);
86 val (Program.Tac stac, a') = interpret_leaf "locate" ctxt eval (get_subst ist) t;
89 "----------- re-build: fun locate_input_tactic -------------------------------------------------";
90 "----------- re-build: fun locate_input_tactic -------------------------------------------------";
91 "----------- re-build: fun locate_input_tactic -------------------------------------------------";
92 val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
93 val (dI',pI',mI') = ("Test", ["sqroot-test","univariate","equation","test"],
94 ["Test","squ-equ-test-subpbl1"]);
95 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
96 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
97 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
98 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
99 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
100 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
101 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
102 (*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = (_, Apply_Method ["Test", "squ-equ-test-subpbl1"])*);
103 (*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Rewrite_Set", Rewrite_Set "norm_equation")*)
105 (*// relevant call --------------------------------------------------------------------------\\*)
106 (*[1], Res*)val (p'''''_''',_,f,nxt'''''_''',_,pt'''''_''') = me nxt p [] pt; (*nxt = Rewrite_Set "Test_simplify"*)
108 "~~~~~ fun me , args:"; val ((_, tac), p, _(*NEW remove*), pt) = (nxt, p, [], pt);
110 (** )val (***)xxxx(***) ( *("ok", (_, _, (pt, p))) =( **) (*case*) locatetac tac (pt,p) (*of*);
111 "~~~~~ fun locatetac , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
112 val (mI, m) = Solve.mk_tac'_ tac;
113 val Applicable.Appl m = (*case*) Applicable.applicable_in p pt m (*of*);
114 (*if*) member op = Solve.specsteps mI; (*else*)
116 (** )val (***)xxxxx(***) ( *Updated (cs' as (_, _, (_, p'))) =( **) loc_solve_ (mI,m) ptp;
117 "~~~~~ fun loc_solve_ , args:"; val (m, (pt, pos)) = ((mI,m), ptp);
119 (** )val (***)xxxxx_x(***) ( *(msg, cs') =( **) Solve.solve m (pt, pos);
120 "~~~~~ fun solve , args:"; val ((_, m), (pt, po as (p, p_))) = (m, (pt, pos));
121 (*+*)val (pt'''''_', (p'''''_', p_'''''_')) = (pt, (p, p_));
122 (*if*) Celem.e_metID = get_obj g_metID pt (par_pblobj pt p); (*else*)
123 val thy' = get_obj g_domID pt (par_pblobj pt p);
124 val (_, is, sc) = Lucin.from_pblobj' thy' (p,p_) pt;
126 locate_input_tactic sc (pt, po) (fst is) (snd is) m;
127 "~~~~~ fun locate_input_tactic , args:"; val (Prog prog, cstate, istate, ctxt, tac)
128 = (sc, (pt, po), (fst is), (snd is), m);
129 val srls = get_simplifier cstate;
131 (** )val Accept_Tac1 ((is as (_,_,_,_,_,strong_ass), ctxt, ss as((tac', _, ctree, pos', _) :: _))) =( **)
132 (*case*) scan_to_tactic1 (prog, (cstate, ctxt, tac)) istate (*of*);
133 "~~~~~ fun scan_to_tactic1 , args:"; val ((prog, (cctt as ((_, p), _, _))), (Istate.Pstate (ist as {path, ...})))
134 = ((prog, (cstate, ctxt, tac)), istate);
135 (*if*) path = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*then*);
137 (** )val xxxxx_xx = ( **)
138 scan_dn1 cctt (ist |> set_path [R] |> set_or ORundef) (Program.body_of prog);
139 "~~~~~ fun scan_dn1 , args:"; val (xxx, ist, (Const ("HOL.Let", _) $ e $ (Abs (id, T, b))))
140 = (cctt, (ist |> set_path [R] |> set_or ORundef), (Program.body_of prog));
142 (*case*) scan_dn1 xxx (ist |> path_down [L, R]) e (*of*);
143 "~~~~~ fun scan_dn1 , args:"; val ((xxx as (cstate, _, _)), ist, (Const ("Tactical.Chain"(*1*), _) $ e1 $ e2 $ a))
144 = (xxx, (ist |> path_down [L, R]), e);
146 (*case*) scan_dn1 xxx (ist |> path_down_form ([L, L, R], a)) e1 (*of*);
147 "~~~~~ fun scan_dn1 , args:"; val (xxx, ist, (Const ("Tactical.Try"(*2*), _) $ e))
148 = (xxx, (ist |> path_down_form ([L, L, R], a)), e1);
150 (*case*) scan_dn1 xxx (ist |> path_down [R]) e (*of*);
151 (*======= end of scanning tacticals, a leaf =======*)
152 "~~~~~ fun scan_dn1 , args:"; val (((pt, p), ctxt, tac), (ist as {env, eval, or, ...}), t)
153 = (xxx, (ist |> path_down [R]), e);
154 val (Program.Tac stac, a') =
155 (*case*) interpret_leaf "locate" ctxt eval (get_subst ist) t (*of*);
156 val Lucin.Ass (m, v', ctxt) =
157 (*case*) associate pt ctxt (m, stac) (*of*);
159 Accept_Tac1 (ist |> set_subst_true (a', v'), ctxt, m) (*return value*);
160 "~~~~~ from scan_dn1 to scan_to_tactic1 return val:"; val (xxxxx_xx)
161 = (Accept_Tac1 (ist |> set_subst_true (a', v'), ctxt, m));
163 "~~~~~ from scan_to_tactic1 to fun locate_input_tactic return val:"; val Accept_Tac1 ((ist as {assoc, ...}), ctxt, tac')
164 = (Accept_Tac1 (ist |> set_subst_true (a', v'), ctxt, m));
165 (*if*) LibraryC.assoc (*then*);
167 Safe_Step (Istate.Pstate ist, ctxt, tac') (*return value*);
168 "~~~~~ from locate_input_tactic to fun solve return:"; val Safe_Step (istate, ctxt, tac)
169 = (*xxxxx_xx*)(**)Safe_Step (Istate.Pstate ist, ctxt, tac')(**);
171 (*+*)val (pt, po as (p, p_)) = (pt'''''_', (p'''''_', p_'''''_')); (* from begin of solve *)
172 val (p'', _, _,pt') =
173 Generate.generate1 (Celem.assoc_thy "Isac_Knowledge") tac
174 (* DEL.^^^^^ ContextC.insert_assumptions asms' ctxt 2nd, fst in Lucin.associate *)
175 (istate, ctxt) (lev_on p, Pbl) pt;
178 ("ok", ([(Tactic.input_from_T tac, tac, (p'', (istate, ctxt)))],
179 [(*ctree NOT cut*)], (pt', p''))) (*return value*);
180 "~~~~~ from solve to loc_solve_ return:"; val ((msg, cs' : calcstate'))
181 = ("ok", ([(Tactic.input_from_T tac, tac, (p'', (istate, ctxt)) )], [(*ctree NOT cut*)], (pt', p'')));
183 "~~~~~ from loc_solve_ to locatetac return:"; val (Updated (cs' as (_, _, (_, p'))))
184 = (*** )xxxxx( ***) (Updated (cs'));
185 (*if*) p' = ([], Pos.Res); (*else*)
187 "~~~~~ from locatetac to me return:"; val (("ok", (_, _, (pt, p)))) = (*** )xxxx( ***) ("ok", cs');
189 (case step p ((pt, Pos.e_pos'), []) of
190 ("ok", (ts as (_, _, _) :: _, _, _)) => ("", ts)
191 | ("helpless", _) => ("helpless: cannot propose tac", [])
192 | ("no-fmz-spec", _) => error "no-fmz-spec"
193 | ("end-of-calculation", (ts, _, _)) => ("", ts)
194 | _ => error "me: uncovered case")
195 handle ERROR msg => raise ERROR msg
198 tacis as (_::_) => let val (tac, _, _) = last_elem tacis in tac end
199 | _ => if p = ([], Pos.Res) then Tactic.End_Proof' else Tactic.Empty_Tac;
201 (p, [] : NEW, TESTg_form (pt, p), (Tactic.tac2IDstr tac, tac), Telem.Sundef, pt);
202 "~~~~~ from me to TOOPLEVEL return:"; val (p,_,f,nxt,_,pt)
203 = (*** )xxx( ***) (p, [] : NEW, TESTg_form (pt, p), (Tactic.tac2IDstr tac, tac), Telem.Sundef, pt);
205 (*//--------------------- check results from modified me ----------------------------------\\*)
206 if p = ([2], Res) andalso
207 pr_ctree pr_short pt = ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 = 2\n"
209 (case nxt of ("Rewrite_Set", Rewrite_Set "Test_simplify") => ()
211 else error "check results from modified me CHANGED";
212 (*\\--------------------- check results from modified me ----------------------------------//*)
214 "~~~~~ from me to TOPLEVEL return:"; val (p,_,f,nxt,_,pt) = (*** )xxx( ***) (**)(p, 000, f, nxt, 000, pt)(**);
215 (*\\------------------ end of modified "fun me" ---------------------------------------------//*)
217 (*[3], Res*)val (p,_,f,nxt,_,pt) = me nxt'''''_''' p'''''_''' [] pt'''''_'''; (*nxt = Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"])*)
218 (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Model_Problem*)
219 (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "equality (-1 + x = 0)"*)
220 (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "solveFor x"*)
221 (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Find "solutions x_i"*)
222 (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Theory "Test"*)
223 (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Problem ["LINEAR", "univariate", "equation", "test"]*)
224 (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Method ["Test", "solve_linear"]*)
225 (*[3], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["Test", "solve_linear"]*)
226 (*[3, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv")*)
227 (*[3, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "Test_simplify"*)
228 (*[3, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["LINEAR", "univariate", "equation", "test"]*)
229 (*[3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_elementwise "Assumptions"*)
230 (*[4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["sqroot-test", "univariate", "equation", "test"]*)
231 (*[], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = End_Proof'*)
233 (*/--------------------- final test ----------------------------------\\*)
234 if p = ([], Res) andalso f2str f = "[x = 1]" andalso fst nxt = "End_Proof'"
235 andalso pr_ctree pr_short pt =
236 ". ----- pblobj -----\n" ^
238 "2. x + 1 + -1 * 2 = 0\n" ^
239 "3. ----- pblobj -----\n" ^
240 "3.1. -1 + x = 0\n" ^
241 "3.2. x = 0 + -1 * -1\n" ^
243 then () else error "re-build: fun locate_input_tactic changed";
246 "----------- fun locate_input_tactic Helpless, but applicable ----------------------------------";
247 "----------- fun locate_input_tactic Helpless, but applicable ----------------------------------";
248 "----------- fun locate_input_tactic Helpless, but applicable ----------------------------------";
249 (*cp from -- try fun applyTactics ------- *)
250 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(["Term (5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12)",
252 ("PolyMinus",["plus_minus","polynom","vereinfachen"],
253 ["simplification","for_polynomials","with_minus"]))];
254 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
255 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
256 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
257 (*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "ordne_alphabetisch"*)
258 (*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "fasse_zusammen"*)
260 (*+*)if map tac2str (sel_appl_atomic_tacs pt p) =
261 ["Rewrite (\"subtrahiere_x_plus_minus\", \"\<lbrakk>?l is_const; ?m is_const\<rbrakk>\n\<Longrightarrow> ?x + ?m * ?v - ?l * ?v = ?x + (?m - ?l) * ?v\")",
262 "Rewrite (\"subtrahiere_x_minus_plus\", \"\<lbrakk>?l is_const; ?m is_const\<rbrakk>\n\<Longrightarrow> ?x - ?m * ?v + ?l * ?v = ?x + (- ?m + ?l) * ?v\")"]
263 then () else error "sel_appl_atomic_tacs ([1], Res) CHANGED";
264 (*[2], Res*)val ("ok", (_, _, ptp as (pt, p))) = locatetac (hd (sel_appl_atomic_tacs pt p)) (pt, p);
266 (*+*)if map tac2str (sel_appl_atomic_tacs pt p) =
267 ["Rewrite (\"tausche_minus\", \"\<lbrakk>?b ist_monom; ?a kleiner ?b\<rbrakk>\n\<Longrightarrow> ?b - ?a = - ?a + ?b\")", "Rewrite (\"tausche_plus_minus\", \"?b kleiner ?c \<Longrightarrow> ?a + ?c - ?b = ?a - ?b + ?c\")",
268 "Rewrite (\"subtrahiere_x_plus_minus\", \"\<lbrakk>?l is_const; ?m is_const\<rbrakk>\n\<Longrightarrow> ?x + ?m * ?v - ?l * ?v = ?x + (?m - ?l) * ?v\")",
269 "Rewrite (\"subtrahiere_x_minus_plus\", \"\<lbrakk>?l is_const; ?m is_const\<rbrakk>\n\<Longrightarrow> ?x - ?m * ?v + ?l * ?v = ?x + (- ?m + ?l) * ?v\")", "Calculate MINUS"]
270 then () else error "sel_appl_atomic_tacs ([1], Res) CHANGED";
271 (* = ([3], Res)*)val ("ok", (_, _, ptp as (pt, p))) = locatetac (hd (sel_appl_atomic_tacs pt p)) (pt, p);
273 (*//----------------- exception PTREE "get_obj f EmptyPtree" raised --------------------------\\*)
274 (** )val ("ok", (_, _, ptp as (pt, p))) =( **) locatetac (hd (sel_appl_atomic_tacs pt p)) (pt, p);
275 "~~~~~ fun locatetac , args:"; val (tac, (ptp as (pt, p))) = (hd (sel_appl_atomic_tacs pt p), (pt, p));
276 val (mI, m) = Solve.mk_tac'_ tac;
277 val Applicable.Appl m = (*case*) Applicable.applicable_in p pt m (*of*);
278 (*if*) member op = Solve.specsteps mI (*else*);
280 loc_solve_ (mI, m) ptp;
281 "~~~~~ fun loc_solve_ , args:"; val (m, (pt, pos)) = ((mI, m), ptp);
283 (* ======== general case ======== *)
284 "~~~~~ fun solve , args:"; val ((_, m), (pt, po as (p, p_))) = (m, (pt, pos));
285 (*if*) Celem.e_metID = get_obj g_metID pt (par_pblobj pt p) (*else*);
286 val thy' = get_obj g_domID pt (par_pblobj pt p);
287 val (_, is, sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;
289 (*case*) locate_input_tactic sc (pt, po) (fst is) (snd is) m (*of*);
290 "~~~~~ fun locate_input_tactic , args:"; val ((Rule.Prog prog), (cstate as (pt, (*?*)pos(*?*))), istate, ctxt, tac)
291 = (sc, (pt, po), (fst is), (snd is), m);
292 val srls = Lucin.get_simplifier cstate (*TODO: shift into Istate.T*);
294 (*case*) scan_to_tactic1 (prog, (cstate, ctxt, tac)) istate (*of*);
295 "~~~~~ fun scan_to_tactic1 , args:"; val ((prog, (cctt as ((_, p), _, _))), (Istate.Pstate (ist as {path, ...})))
296 = ((prog, (cstate, ctxt, tac)), istate);
297 (*if*) path = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*else*);
299 go_scan_up1 (prog, cctt) ist;
300 "~~~~~ and go_scan_up1 , args:"; val ((yyy as (prog, _)), (ist as {path, ...}))
301 = ((prog, cctt), ist);
302 (*if*) 1 < length path (*then*);
304 scan_up1 yyy (ist |> path_up) (go (path_up' path) prog);
305 "~~~~~ fun scan_up1 , args:"; val (yyy, ist, (Const ("Tactical.Try"(*2*), _) $ _))
306 = (yyy, (ist |> path_up), (go (path_up' path) prog));
309 "~~~~~ and go_scan_up1 , args:"; val ((yyy as (prog, _)), (ist as {path, ...}))
311 (*if*) 1 < length path (*then*);
313 scan_up1 yyy (ist |> path_up) (go (path_up' path) prog);
314 "~~~~~ fun scan_up1 , args:"; val ((yyy as (prog, xxx as (cstate, _, _))), ist,
315 (Const ("Tactical.Chain"(*3*), _) $ _ ))
316 = (yyy, (ist |> path_up), (go (path_up' path) prog));
317 val e2 = check_Seq_up ist prog
319 (*case*) scan_dn1 xxx (ist |> path_up_down [R] |> set_or ORundef) e (*of*);
320 "~~~~~ fun scan_dn1 , args:"; val (yyy, ist, (Const ("Tactical.Chain"(*2*), _) $ _ $ _))
321 = (xxx, (ist |> path_up_down [R] |> set_or ORundef), e2);
323 (*case*) scan_dn1 xxx (ist |> path_down [L, R]) e1 (*of*);
324 "~~~~~ fun scan_dn1 , args:"; val (xxx, ist, (Const ("Tactical.Try"(*2*), _) $ e))
325 = (xxx, (ist |> path_down [L, R]), e1);
327 (*case*) scan_dn1 xxx (ist |> path_down [R]) e (*of*);
328 (*======= end of scanning tacticals, a leaf =======*)
329 "~~~~~ fun scan_dn1 , args:"; val (((pt, p), ctxt, tac), (ist as {eval, act_arg, or, ...}), t)
330 = (xxx, (ist |> path_down [R]), e);
331 val (Program.Tac stac, a') = (*case*) interpret_leaf "locate" ctxt eval (get_subst ist) t (*of*);
332 val NotAss = (*case*) associate pt ctxt (tac, stac) (*of*);
333 val ORundef = (*case*) or (*of*);
334 val Notappl "norm_equation not applicable" =
335 (*case*) Applicable.applicable_in p pt (Lucin.stac2tac pt (Celem.assoc_thy "Isac_Knowledge") stac) (*of*);
337 (Term_Val1 act_arg) (* return value *);
339 val Rewrite' ("PolyMinus", "tless_true", _, _, ("tausche_minus",_ (*"?b ist_monom \<Longrightarrow> ?a kleiner ?b \<Longrightarrow> ?b - ?a = - ?a + ?b"*)),
342 if scrstate2str ist =
343 "([\"\n(t_t, 5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * g + 12)\"], [R,L,R,R,L,R,R], e_rls, SOMEt_t, \n" ^
344 "- (8 * g) + (- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f) + 10 * g, ORundef, AppUndef_, false)"
346 term2str t = "- (8 * g) + (- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f) + 10 * g"
348 term2str res = "- (8 * g) + (- 9 + 12 + 5 * e - 7 * e + (- 4 + 6) * f) + 10 * g"
350 terms2str asm = "[\"4 kleiner 6\",\"6 ist_monom\"]"
351 then () else error "locate_input_tactic Helpless, but applicable CHANGED";
354 "----------- re-build: fun determine_next_tactic -----------------------------------------------";
355 "----------- re-build: fun determine_next_tactic -----------------------------------------------";
356 "----------- re-build: fun determine_next_tactic -----------------------------------------------";
357 (*//--------- exception Size raised (line 171 of "./basis/LibrarySupport.sml") ---------------\\
358 THIS CODE WORKS IN Test.Some.thy
359 ------------------------------------
360 val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
362 ("Test", ["sqroot-test","univariate","equation","test"],
363 ["Test","squ-equ-test-subpbl1"]);
364 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
365 (*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, Pos.e_pos'), []);(*Model_Problem*)
366 (*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, Pos.e_pos'), []);(*Specify_Theory*)
367 (*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, Pos.e_pos'), []);(*Specify_Problem ["sqroot-test", "univariate", "equation", "test"*)
368 (*[], Met*)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(*Specify_Method ["Test", "squ-equ-test-subpbl1"]*)
369 (*1], Frm*)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(*Apply_Method ["Test", "squ-equ-test-subpbl1"]*)
370 (*[1], Res*)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(*Rewrite_Set "norm_equation"*)
372 (*// relevant call --------------------------------------------------------------------------\\*)
373 (*[2], Res*)val (aaa, ([(tac'''', bbb, ccc)], ddd, (pt'''', p''''))) =(**) step p ((pt, e_pos'), []);(*Rewrite_Set "Test_simplify"*)
374 (*-- relevant call ----------------------------------------------------------------------------*)
376 "~~~~~ fun step , args:"; val ((ip as (_, p_)), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'), []));
377 val pIopt = get_pblID (pt,ip);
378 (*if*) ip = ([], Pos.Res) (*else*);
379 val _ = (*case*) tacis (*of*);
380 val SOME _ = (*case*) pIopt (*of*);
381 (*if*) member op = [Pos.Pbl, Pos.Met] p_
382 andalso is_none (Ctree.get_obj Ctree.g_env pt (fst p)) (*else*);
384 (** )val cs''''' = ( *..interpret "if member op ="..*)
385 (*case*) do_solve_step (pt, ip) (*of*);
386 "~~~~~ and do_solve_step , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
387 (*if*) Celem.e_metID = get_obj g_metID pt (par_pblobj pt p) (*else*);
388 val thy' = get_obj g_domID pt (par_pblobj pt p);
389 val (_, (ist, ctxt), sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;
391 (*NEW*) val Next_Step (_, _, Rewrite_Set' (_, _, Rls {id = "Test_simplify", ...}, _, _)) = (*case*)
392 (*NEW*) determine_next_tactic sc (pt, pos) ist ctxt (*of*);
393 "~~~~~ fun determine_next_tactic , args:"; val (Rule.Prog prog, ptp as (pt, (p, _)), Istate.Pstate ist, ctxt)
394 = (sc, (pt, pos), ist, ctxt);
395 (*OLD* ) val Accept_Tac2 (m', ist as {act_arg, ...}, ctxt) =
396 (*OLD*) (*case*) scan_to_tactic2 (prog, (ptp, ctxt)) (Istate.Pstate ist) (*of*);
398 (*NEW*) val Accept_Tac2 (tac, ist, ctxt) =
399 (*NEW*)(*case*) scan_to_tactic2 (prog, (ptp, ctxt)) (Istate.Pstate ist) (*of*);
400 (*NEW* )| Term_Val2 prog_result => End_Program (ist, Check_Postcond' ...prog_result...)
401 (*NEW*) (* ist indicates ^^\<Or>?, ctxt already updated, ^^^*)
402 (*NEW*)| Reject_Tac2 => Helpless
405 (*OLD* )(m', (Pstate ist, ctxt), (act_arg, Telem.Safe)) (*return value*);
407 (*NEW*) Next_Step (Istate.Pstate ist, Tactic.insert_assumptions tac ctxt, tac) (*return value*);
409 "~~~~~ from fun determine_next_tactic\<longrightarrow>and do_solve_step , return:"; val (Next_Step (ist, ctxt, tac))
410 = (Next_Step (Istate.Pstate ist, Tactic.insert_assumptions tac ctxt, tac));
411 (*NEW* ) case determine_next_tactic sc (pt, pos) ist ctxt of
412 (*NEW*) Next_Step (ist, ctxt, tac) =>
414 begin_end_prog tac (ist, Tactic.insert_assumptions tac ctxt) ptp;
415 (*NEW* ) | End_Program (ist, tac) => begin_end_prog tac (ist, ctxt) ptp
416 (*NEW*) | Helpless => Chead.e_calcstate'
419 (*+*)val Rewrite_Set' ("Test", false, Rls {id = "Test_simplify", ...}, _, _) = tac;
421 (*OLD skip* ) val _ = (*case*) tac_'''''_' (*of*);
422 (*OLD skip*)begin_end_prog tac_'''''_' is'''''_' ptp'''''_' (*return value*);
424 "~~~~~ fun begin_end_prog , args:"; val (tac_, is, (pt, pos))
425 (*skip* )= (tac_'''''_', is, ptp);( *skip*)
426 (*use*) = (tac, (ist, Tactic.insert_assumptions tac ctxt), ptp) (*use*)
427 val pos = case pos of
428 (p, Met) => ((lev_on o lev_dn) p, Frm) (* begin script *)
429 | (p, Res) => (lev_on p, Res) (* somewhere in script *)
431 val (pos', c, _, pt) = Generate.generate1 (Celem.assoc_thy "Isac_Knowledge") tac_ is pos pt;
433 ([(Tactic.input_from_T tac_, tac_, (pos, is))], c, (pt, pos')) (*return from do_solve_step*);
434 "~~~~~ from and do_solve_step\<longrightarrow>fun step , return:";
435 (*OLD skip* )val (tac_'''''_')
436 (*OLD skip*) = (begin_end_prog tac_'''''_' is ptp);( **)
438 (*use*)([(Tactic.input_from_T tac_, tac_, (pos, is))], c, (pt, pos'));
440 "~~~~~ from fun step\<longrightarrow>TOPLEVEL return:";
441 (*OLD skip* )val (_, ([(tac'''', _, _)], _, (pt'''', p''''))) = ("ok", cs''''')( **);
443 (*use*)val ([(tac, _, (_, _))], _, (pt'''', p'''')) = cs
445 (*\\------------------ end of modified "fun step" -------------------------------------------//*)
447 (*[3], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = step p'''' ((pt'''', e_pos'), []);(*Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"])*)
448 (*[3], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(*Model_Problem*)
449 (*[3], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(*Specify_Theory "Test"*)
450 (*[3], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(*Specify_Problem ["LINEAR", "univariate", "equation", "test"]*)
451 (*[3], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(*Specify_Method ["Test", "solve_linear"]*)
452 (*[3, 1], Frm*)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(*Apply_Method ["Test", "solve_linear"]*)
453 (*[3, 1], Res*)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(*Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv")*)
454 (*[3, 2], Res*)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(*Rewrite_Set "Test_simplify"*)
455 (*[3], Res*)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(*Check_Postcond ["LINEAR", "univariate", "equation", "test"]*)
456 (*[4], Res*)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(*Check_elementwise "Assumptions"*)
457 (*[], Res*)val ("ok", ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(*Check_Postcond ["sqroot-test", "univariate", "equation", "test"]*)
458 (*[], Res*)val ("end-of-calculation", ([], _, (pt, p))) = step p ((pt, e_pos'), []);(**)
460 (*/--------------------- final test ----------------------------------\\*)
461 val (res, asm) = (get_obj g_result pt (fst p));
463 if term2str res = "[x = 1]" andalso terms2str asm = "[\"precond_rootmet 1\"]"
464 then () else error "re-build: fun determine_next_tactic CHANGED 1";
466 if p = ([], Und) (*.. should be ([], Res) *)
468 case get_obj g_tac pt (fst p) of
469 Apply_Method ["Test", "squ-equ-test-subpbl1"] => ((*ok, further tactics are level down*))
470 | _ => error "re-build: fun determine_next_tactic CHANGED 3"
471 else error "re-build: fun determine_next_tactic CHANGED 2";
472 \\--------- exception Size raised (line 171 of "./basis/LibrarySupport.sml") ---------------//*)
475 "----------- re-build: fun locate_input_formula ------------------------------------------------";
476 "----------- re-build: fun locate_input_formula ------------------------------------------------";
477 "----------- re-build: fun locate_input_formula ------------------------------------------------";