1 (* test for sml/ME/mathengine.sml
2 authors: Walther Neuper 2000, 2006
3 (c) due to copyright terms
5 "--------------------------------------------------------";
6 "table of contents --------------------------------------";
7 "--------------------------------------------------------";
8 "----------- change to parse ctxt -----------------------";
9 "----------- debugging setContext..pbl_ -----------------";
10 "----------- tryrefine ----------------------------------";
11 "----------- fun step: Apply_Method without init_form ---";
12 "----------- fun step -----------------------------------";
13 "----------- fun autocalc -------------------------------";
14 "----------- fun autoCalculate --------------------------";
15 "----------- fun autoCalculate..CompleteCalc ------------";
16 "--------------------------------------------------------";
17 "--------------------------------------------------------";
18 "--------------------------------------------------------";
20 "----------- change to parse ctxt -----------------------";
21 "----------- change to parse ctxt -----------------------";
22 "----------- change to parse ctxt -----------------------";
23 "===== start calculation: from problem description (fmz) to origin";
24 val fmz = ["realTestGiven (((1+2)*4/3)^^^2)","realTestFind s"];
25 val (thyID, pblID, metID) =
26 ("Test", ["calculate", "test"], ["Test", "test_calculate"]);
27 val (p,_,_,nxt,_,pt) = CalcTreeTEST [(fmz, (thyID, pblID, metID))];
29 (* call sequence: CalcTreeTEST
30 > nxt_specify_init_calc
33 val (thy, pbt) = (Thy_Info.get_theory thyID, (#ppc o get_pbt) pblID);
35 val ctxt = ProofContext.init_global thy;
37 val ctopts = map (parseNEW ctxt) fmz;
38 val dts = map (split_dts o the) ctopts;
40 (term * term list) list
41 formulas: e.g. ((1+2)*4/3)^^^2
42 description: e.g. realTestGiven
47 string list -> theory -> (string * (term * 'a)) list -> ori list
50 string list -> theory -> (string * (term * 'a)) list -> (ori list * ctxt)
52 FROM val oris = prep_ori...
53 TO val (oris, _) = prep_ori...
55 "----- insert ctxt in ptree";
57 FROM loc : istate option * istate option,
58 TO loc : (istate * ctxt) option * (istate * ctxt) option,
60 FROM val pt = Nd (PblObj
61 {.., loc = (SOME (ScrState ([], [], NONE, Const ("empty", "'a"), Sundef, false)),
63 TO val pt = Nd (PblObj
65 ((SOME (ScrState ([], [], NONE, Const ("empty", "'a"), Sundef, false)), ctxt),
69 "===== interactive specification: from origin to specification (probl)";
70 val (p,_,_,nxt,_,pt) = me nxt p [1] pt;
71 (*nxt =("Add_Given", Model_Problem)*)
72 val (p,_,_,nxt,_,pt) = me nxt p [1] pt;
73 (*nxt = ("Add_Find",Add_Find "realTestFind s") : string * tac*)
75 (* call sequence: me Model_Problem
76 > me ("Add_Given", Add_Given "realTestGiven (((1 + 2) * 4 / 3) ^^^ 2)")
79 > specify GET ctxt (stored in ctree)
90 val (p,_,_,nxt,_,pt) = me nxt p [1] pt;
91 (*nxt = ("Specify_Theory",Specify_Theory "Test") : string * tac*)
92 val (p,_,_,nxt,_,pt) = me nxt p [1] pt;
93 (*nxt = ("Specify_Problem",Specify_Problem ["calculate","test"])*)
95 "===== end specify: from specification (probl) to guard (method)";
96 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
97 (*nxt = ("Specify_Method",Specify_Method ("Test","test_calculate"))*)
99 "===== start interpretation: from guard to environment";
100 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
101 (*nxt = ("Apply_Method",Apply_Method ("Test","test_calculate"))*)
103 (* call sequence: me ("Apply_Method",...
106 > solve ("Apply_Method",...
108 val ((_,tac), ptp) = (nxt, (pt, p));
109 locatetac tac (pt,p);
110 val (mI, m) = mk_tac'_ tac;
111 val Appl m = applicable_in p pt m;
112 member op = specsteps mI;
113 loc_solve_ (mI,m) ptp;
114 val (m, (pt, pos)) = ((mI,m), ptp);
116 val ((_, m as Apply_Method' (mI, _, _, _)), (pt, (pos as (p,_)))) =
118 val {srls,...} = get_met mI;
119 val PblObj{meth=itms,...} = get_obj I pt p;
120 val thy' = get_obj g_domID pt p;
121 val thy = assoc_thy thy';
122 val (is as ScrState (env,_,_,_,_,_), ctxt, sc) = init_scrstate thy itms mI;
124 "----- go on in the calculation";
125 val (p,_,f,nxt,_,pt) = me nxt pos [1] pt;
126 (*nxt = ("Calculate",Calculate "PLUS")*)
127 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
128 (*nxt = ("Calculate",Calculate "TIMES")*)
130 "===== input a formula to be derived from previous istate";
131 "----- appendFormula TODO: first repair error";
132 val cs = ((pt,p),[]);
133 val ("ok", cs' as (_,_,(pt,p))) = step p cs;
134 val ifo = (* encode "4^^^2" \<longrightarrow>*) "4^2";
136 val ("no derivation found", (_,_,(pt, p))) = inform cs' ((*encode*) ifo);
137 here ^^^^^^^^^^^^^^^^^^^^^ should be "ok"
140 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
141 (*nxt = ("Calculate",Calculate "DIVIDE")*)
142 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
143 (*nxt = ("Calculate",Calculate "POWER")*)
144 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
145 (*nxt = ("Check_Postcond",Check_Postcond ["calculate","test"])*)
146 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
147 (*nxt = ("End_Proof'",End_Proof')*)
148 if f = Form' (FormKF (~1,EdUndef,0,Nundef,"16")) then ()
149 else error "calculate.sml: script test_calculate changed behaviour";
151 "===== tactic Subproblem: from environment to origin";
154 (*=== inhibit exn ?=============================================================
156 "----------- debugging setContext..pbl_ -----------------";
157 "----------- debugging setContext..pbl_ -----------------";
158 "----------- debugging setContext..pbl_ -----------------";
160 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
161 ("Test", ["sqroot-test","univariate","equation","test"],
162 ["Test","squ-equ-test-subpbl1"]))];
164 moveActiveRoot 1; modelProblem 1;
166 val pos as (p,_) = ([],Pbl);
167 val guh = "pbl_equ_univ";
168 checkContext 1 pos guh;
169 val ((pt,_),_) = get_calc 1;
170 val pp = par_pblobj pt p;
171 val keID = guh2kestoreID guh;
172 case context_pbl keID pt pp of (true,["univariate", "equation"],_,_,_)=>()
173 | _ => error "mathengine.sml: context_pbl .. pbl_equ_univ checked";
175 case get_obj g_spec pt p of (_, ["e_pblID"], _) => ()
176 | _ => error "mathengine.sml: context_pbl .. pbl still empty";
177 setContext 1 pos guh;
178 val ((pt,_),_) = get_calc 1;
179 case get_obj g_spec pt p of (_, ["univariate", "equation"], _) => ()
180 | _ => error "mathengine.sml: context_pbl .. pbl set";
183 setContext 1 pos "met_eq_lin";
184 val ((pt,_),_) = get_calc 1;
185 case get_obj g_spec pt p of (_, _, ["LinEq", "solve_lineq_equation"]) => ()
186 | _ => error "mathengine.sml: context_pbl .. pbl set";
189 "----------- tryrefine ----------------------------------";
190 "----------- tryrefine ----------------------------------";
191 "----------- tryrefine ----------------------------------";
193 CalcTree [(["equality (x/(x^2 - 6*x+9) - 1/(x^2 - 3*x) =1/x)",
194 "solveFor x", "solutions L"],
195 ("RatEq",["univariate","equation"],["no_met"]))];
197 moveActiveRoot 1; autoCalculate 1 CompleteCalc;
199 refineProblem 1 ([1],Res) "pbl_equ_univ"
200 (*gives "pbl_equ_univ_rat" correct*);
202 refineProblem 1 ([1],Res) (pblID2guh ["linear","univariate","equation"])
203 (*gives "pbl_equ_univ_lin" incorrect*);
206 "----------- fun step: Apply_Method without init_form ---";
207 "----------- fun step: Apply_Method without init_form ---";
208 "----------- fun step: Apply_Method without init_form ---";
209 val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
211 ("Test", ["sqroot-test","univariate","equation","test"],
212 ["Test","squ-equ-test-subpbl1"]);
213 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
214 "~~~~~ fun me, args:"; val (_,tac) = nxt;
215 val ("ok", (_, _, (pt, p))) = locatetac tac (pt,p);
216 "~~~~~ fun step, args:"; val (ip as (_,p_), ptp as (pt,p), tacis) = (p, (pt, e_pos'), []);
217 val pIopt = get_pblID (pt,ip);
218 ip = ([],Res) (*false*);
220 member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p))
221 (*^^^^^^^^: Apply_Method without init_form*)
222 ===== inhibit exn ?===========================================================*)
224 "----------- fun step -----------------------------------";
225 "----------- fun step -----------------------------------";
226 "----------- fun step -----------------------------------";
227 val p = e_pos'; val c = [];
228 val (p,_,f,nxt,_,pt) =
230 [(["functionTerm (x^^^2 + 1)", "integrateBy x", "antiDerivative FF"],
231 ("Integrate", ["integrate","function"], ["diff","integration"]))];
232 "----- step 1: returns tac = Model_Problem ---";
233 val (str, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);
234 "----- step 2: returns tac = ---";
235 val (str, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);
236 "----- step 3: returns tac = ---";
237 val (str, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);
238 "----- step 4: returns tac = ---";
239 val (str, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);
240 "----- step 5: returns tac = ---";
242 (*========== inhibit exn =======================================================
243 2002 stops here as well: TODO review actual arguments:
244 val (str, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);
245 "----- step 6: returns tac = ---";
246 val (str, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);
247 "----- step 7: returns tac = ---";
248 val (str, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);
249 "----- step 8: returns tac = ---";
250 val (str, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);
251 ============ inhibit exn =====================================================*)
254 "----------- fun autocalc -------------------------------";
255 "----------- fun autocalc -------------------------------";
256 "----------- fun autocalc -------------------------------";
257 val p = e_pos'; val c = [];
258 val (p,_,f,nxt,_,pt) =
260 [(["functionTerm (x^^^2 + 1)", "integrateBy x", "antiDerivative FF"],
261 ("Integrate",["integrate","function"], ["diff","integration"]))];
262 (*-----since Model_Problem + complete_mod_ in case cas of SOME-----*
263 modeling is skipped FIXME
264 *-----since Model_Problem + complete_mod_ in case cas of SOME-----*)
265 tracing "----- step 1 ---";
266 val (str, cut, (pt, p)) = autocalc [] p ((pt, e_pos'),[]) (Step 1); show_pt pt;
267 tracing "----- step 2 ---";
268 val (str, cut, (pt, p)) = autocalc [] p ((pt, e_pos'),[]) (Step 1); show_pt pt;
269 tracing "----- step 3 ---";
270 val (str, cut, (pt, p)) = autocalc [] p ((pt, e_pos'),[]) (Step 1); show_pt pt;
271 tracing "----- step 4 ---";
272 val (str, cut, (pt, p)) = autocalc [] p ((pt, e_pos'),[]) (Step 1); show_pt pt;
273 tracing "----- step 5 ---";
274 val (str, cut, (pt, p)) = autocalc [] p ((pt, e_pos'),[]) (Step 1); show_pt pt;
275 tracing "----- step 6 ---";
276 val (str, cut, (pt, p)) = autocalc [] p ((pt, e_pos'),[]) (Step 1); show_pt pt;
277 tracing "----- step 7 ---";
278 val (str, cut, (pt, p)) = autocalc [] p ((pt, e_pos'),[]) (Step 1); show_pt pt;
279 tracing "----- step 8 ---";
280 val (str, cut, (pt, p)) = autocalc [] p ((pt, e_pos'),[]) (Step 1); show_pt pt;
281 (*========== inhibit exn 110628 ================================================
282 WN110628: Integration does not work, see Knowledge/integrate.sml
284 if str = "end-of-calculation" andalso
285 term2str (get_obj g_res pt (fst p)) = "c + x + 1 / 3 * x ^^^ 3" then ()
286 else error "mathengine.sml -- fun autocalc -- end";
287 ============ inhibit exn 110628 ==============================================*)
290 "----------- fun autoCalculate -----------------------------------";
291 "----------- fun autoCalculate -----------------------------------";
292 "----------- fun autoCalculate -----------------------------------";
294 CalcTree (*ATTENTION: encode_fmz ... unlike CalcTreeTEST*)
295 [(["functionTerm (x^2 + 1)", "integrateBy x", "antiDerivative FF"],
296 ("Integrate", ["integrate", "function"], ["diff", "integration"]))];
299 (*-----since Model_Problem + complete_mod_ in case cas of SOME-----*
300 modeling is skipped FIXME
301 see test/../interface -- solve_linear as rootpbl FE -- for OTHER expl:
302 setNextTactic 1 (Add_Given "equality (1 + -1 * 2 + x = 0)");
303 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); (*equality added*);
305 fetchProposedTactic 1;
306 setNextTactic 1 (Add_Given "solveFor x");
307 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
309 fetchProposedTactic 1;
310 setNextTactic 1 (Add_Find "solutions L");
311 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
313 fetchProposedTactic 1;
314 setNextTactic 1 (Specify_Theory "Test");
315 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
316 *-----since Model_Problem + complete_mod_ in case cas of SOME-----*)
317 autoCalculate 1 (Step 1);
319 autoCalculate 1 (Step 1);
321 autoCalculate 1 (Step 1);
323 autoCalculate 1 (Step 1);
325 autoCalculate 1 (Step 1);
327 autoCalculate 1 (Step 1);
329 autoCalculate 1 (Step 1);
331 autoCalculate 1 (Step 1);
333 autoCalculate 1 (Step 1);
334 val (ptp as (_, p), _) = get_calc 1;
335 val (Form t,_,_) = pt_extract ptp;
336 (*========== inhibit exn 110310 ================================================
337 if term2str t = "c + x + 1 / 3 * x ^^^ 3" andalso p = ([], Res) then ()
338 else error "mathengine.sml -- fun autoCalculate -- end";
339 ============ inhibit exn 110310 ==============================================*)
341 "----------- fun autoCalculate..CompleteCalc ------------";
342 "----------- fun autoCalculate..CompleteCalc ------------";
343 "----------- fun autoCalculate..CompleteCalc ------------";
345 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
346 ("Test", ["sqroot-test","univariate","equation","test"],
347 ["Test","squ-equ-test-subpbl1"]))];
350 (*autoCalculate 1 CompleteCalc; (*WAS <SYSERROR>..<ERROR> error in kernel </ERROR>*)*)
351 "~~~~~ fun autoCalculate, args:"; val (cI, auto) = (1, CompleteCalc);
352 val pold = get_pos cI 1;
353 (*autocalc [] pold (get_calc cI) auto; (*WAS Type unification failed
354 Type error in application: incompatible operand type
355 Operator: solveFor :: real \<Rightarrow> una
356 Operand: x :: 'a *)*)
357 "~~~~~ fun autocalc, args:"; val (c, (pos as (_,p_)), ((pt,_), _), auto)
358 = ([] : pos' list, pold, (get_calc cI), auto);
359 autoord auto > 3 andalso just_created (pt, pos); (*true*)
360 val ptp = all_modspec (pt, pos);
361 "TODO all_modspec: preconds for rootpbl";
362 (*all_solve auto c ptp; (*WAS Type unification failed...*)*)
363 "~~~~~ and all_solve, args:"; val (auto, c, (ptp as (pt, pos as (p,_)))) =
365 val (_,_,mI) = get_obj g_spec pt p
366 val ctxt = get_ctxt pt pos
367 val (ttt, c', ptp) = nxt_solv (Apply_Method' (mI, NONE, e_istate, ctxt)) (e_istate, ctxt) ptp;
368 (* complete_solve auto (c @ c') ptp; (*WAS Type unification failed...*) pos = ([], Met)*)
369 "~~~~~ fun complete_solve, args:"; val (auto, c, (ptp as (_, p as (_,p_)))) =
370 (auto, (c @ c'), ptp);
371 p = ([], Res) (*false p = ([1], Frm)*);
372 member op = [Pbl,Met] p_ (*false*);
373 val (ttt, c', ptp') = nxt_solve_ ptp; (*ttt = Rewrite_Set "norm_equation"*)
374 (* complete_solve auto (c @ c') ptp'; (*WAS Type unification failed...*) pos = ([], Met)*)
375 "~~~~~ fun complete_solve, args:"; val (auto, c, (ptp as (_, p as (_,p_)))) =
376 (auto, (c @ c'), ptp');
377 p = ([], Res) (*false p = ([1], Res)*);
378 member op = [Pbl,Met] p_ (*false*);
379 val (ttt, c', ptp') = nxt_solve_ ptp; (*ttt = Rewrite_Set "Test_simplify"*)
380 (* complete_solve auto (c @ c') ptp'; (*WAS Type unification failed...*) pos = ([], Met)*)
381 "~~~~~ fun complete_solve, args:"; val (auto, c, (ptp as (_, p as (_,p_)))) =
382 (auto, (c @ c'), ptp');
383 p = ([], Res) (*false p = ([2], Res)*);
384 member op = [Pbl,Met] p_ (*false*);
385 val ((Subproblem _, tac_, (_, is))::_, c', ptp') = nxt_solve_ ptp;
386 autoord auto < 5 (*false*);
387 (* val ptp = all_modspec ptp' (*WAS Type unification failed...*)*)
388 "~~~~~ fun all_modspec, args:"; val (pt, pos as (p,_)) = (ptp');
389 val (PblObj {fmz = (fmz_, _), origin = (pors, spec as (dI,pI,mI), hdl), ...}) = get_obj I pt p;
390 val thy = assoc_thy dI;
391 val {ppc, ...} = get_met mI;
392 (* val (mors, ctxt) = prep_ori fmz_ thy ppc; WAS Type unification failed because
393 val ctxt' = dI |> Thy_Info.get_theory |> ProofContext.init_global;
394 (parseNEW ctxt' "x" |> the |> type_of) = TFree ("'a",[]);
396 (*vvv from: | assod pt _ (Subproblem'...*)
397 val (fmz_, vals) = oris2fmz_vals pors;
399 val ctxt = dI |> Thy_Info.get_theory |> ProofContext.init_global
400 |> declare_constraints' vals
402 (*^^^ from: | assod pt _ (Subproblem'...*)
403 val [(1, [1], "#Given", dsc_eq, [equality]),
404 (2, [1], "#Given", dsc_solvefor, [xxx]),
405 (3, [1], "#Find", dsc_solutions, [x_i])] = pors;
406 if term2str xxx = "x" andalso type_of xxx = HOLogic.realT then ()
407 else error "autoCalculate..CompleteCalc: SubProblem broken 1";
408 val pt = update_pblppc pt p (map (ori2Coritm ppc) pors);
409 val pt = update_metppc pt p (map (ori2Coritm ppc) pors);
410 val pt = update_spec pt p (dI,pI,mI);
411 val pt = update_ctxt pt p ctxt;
412 "~~~~~ return to complete_solve, args:"; val (ptp) = (pt, (p,Met));
413 val (msg, c, (pt, p)) = complete_solve auto (c @ c') ptp;
414 if msg = "end-of-calculation" andalso c = [] andalso p = ([], Res) then ()
415 else error "autoCalculate..CompleteCalc: final result";
416 if terms2strs (get_assumptions_ pt p) =
417 ["matches (?a = ?b) (-1 + x = 0)", "x = 1", "precond_rootmet x"]
418 then () else error "autoCalculate..CompleteCalc: ctxt at final result";