1 (* Title: tests for MathEngine/mathengine-stateless.sml
2 Author: Walther Neuper 2000, 2006, 2020
3 (c) due to copyright terms
5 theory Test_Some imports Build_Thydata begin
6 ML {* KEStore_Elems.set_ref_thy @{theory};
7 fun autoCalculate' cI auto = autoCalculate cI auto |> Future.join *}
8 ML_file "~~/test/Tools/isac/Interpret/mathengine.sml"
10 "--------------------------------------------------------";
11 "table of contents --------------------------------------";
12 "--------------------------------------------------------";
13 "----------- change to parse ctxt -----------------------";
14 "----------- debugging setContext..pbl_ -----------------";
15 "----------- tryrefine ----------------------------------";
16 "----------- search for Or_to_List ----------------------";
17 "----------- check thy in CalcTreeTEST ------------------";
18 "----------- identified error in fun getTactic, ThmC.string_of_thm ---------------";
19 "----------- improved fun getTactic for interSteps and numeral calculations --";
20 "--------------------------------------------------------";
21 "--------------------------------------------------------";
22 "--------------------------------------------------------";
24 "----------- change to parse ctxt -----------------------";
25 "----------- change to parse ctxt -----------------------";
26 "----------- change to parse ctxt -----------------------";
27 "===== start calculation: from problem description (fmz) to origin";
28 val fmz = ["realTestGiven (((1+2)*4/3)^^^2)","realTestFind s"];
29 val (thyID, pblID, metID) =
30 ("Test", ["calculate", "test"], ["Test", "test_calculate"]);
31 (*======= Isabelle2013-2 --> Isabelle2014: unclear, why this test ever run =====================*)
33 "----------- debugging setContext..pbl_ -----------------";
34 "----------- debugging setContext..pbl_ -----------------";
35 "----------- debugging setContext..pbl_ -----------------";
37 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
38 ("Test", ["sqroot-test","univariate","equation","test"],
39 ["Test","squ-equ-test-subpbl1"]))];
41 moveActiveRoot 1; modelProblem 1;
43 val pos as (p,_) = ([],Pbl);
44 val guh = "pbl_equ_univ";
45 checkContext 1 pos guh;
46 val ((pt,_),_) = get_calc 1;
47 val pp = par_pblobj pt p;
48 val keID = guh2kestoreID guh;
49 case context_pbl keID pt pp of (true,["univariate","equation"],_,_,_)=>()
50 | _ => error "mathengine.sml: context_pbl .. pbl_equ_univ checked";
52 case get_obj g_spec pt p of (_, ["empty_probl_id"], _) => ()
53 | _ => error "mathengine.sml: context_pbl .. pbl still empty";
55 val ((pt,_),_) = get_calc 1;
56 case get_obj g_spec pt p of (_, ["univariate","equation"], _) => ()
57 | _ => error "mathengine.sml: context_pbl .. pbl set";
60 setContext 1 pos "met_eq_lin";
61 val ((pt,_),_) = get_calc 1;
62 case get_obj g_spec pt p of (_, _, ["LinEq", "solve_lineq_equation"]) => ()
63 | _ => error "mathengine.sml: context_pbl .. pbl set";
66 "----------- tryrefine ----------------------------------";
67 "----------- tryrefine ----------------------------------";
68 "----------- tryrefine ----------------------------------";
70 CalcTree [(["equality (x/(x^2 - 6*x+9) - 1/(x^2 - 3*x) =1/x)",
71 "solveFor x", "solutions L"],
72 ("RatEq",["univariate","equation"],["no_met"]))];
74 moveActiveRoot 1; autoCalculate 1 CompleteCalc;
76 refineProblem 1 ([1],Res) "pbl_equ_univ"
77 (*gives "pbl_equ_univ_rat" correct*);
79 refineProblem 1 ([1],Res) (pblID2guh ["LINEAR","univariate","equation"])
80 (*gives "pbl_equ_univ_lin" incorrect*);
82 "--------- search for Or_to_List ------------------------";
83 "--------- search for Or_to_List ------------------------";
84 "--------- search for Or_to_List ------------------------";
85 val fmz = ["equality (x^^^2 + 4*x + 5 = (2::real))", "solveFor x","solutions L"];
86 val (dI',pI',mI') = ("Isac_Knowledge", ["univariate","equation"], ["no_met"])
87 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
88 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
89 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
90 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
91 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
92 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
93 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
94 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
95 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
96 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
97 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Subproblem"*)
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 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
103 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
104 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
105 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
106 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
107 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
108 "~~~~~ fun me, args:"; val (tac, (p:pos'), (_:NEW(*remove*)), (pt:ctree)) =
110 val ("ok", (_, _, ptp)) = Step.by_tactic tac (pt,p)
112 "~~~~~ fun Step.do_next, args:"; val (((ip as (_,p_)):pos'), ((ptp as (pt,p), tacis):calcstate)) =
113 (p, ((pt, e_pos'),[]));
114 val pIopt = get_pblID (pt,ip);
115 ip = ([],Res); (*false*)
117 Library.member op = [Pbl,Met] p_; (*false*)
118 "~~~~~ fun do_next, args:"; val (ptp as (pt, pos as (p,p_))) = (pt,ip);
119 Method.id_empty = get_obj g_metID pt (par_pblobj pt p); (*false*)
120 val thy' = get_obj g_domID pt (par_pblobj pt p);
121 val ((ist, ctxt), sc) = resume_prog thy' (p,p_) pt;
123 val Next_Step (istate, ctxt, tac) = LI.find_next_step sc (pt,pos) ist ctxt; (*WAS Empty_Tac_: tac_*)
124 case tac of Or_to_List' _ => ()
125 | _ => error "Or_to_List broken ?"
128 "----------- check thy in CalcTreeTEST ------------------";
129 "----------- check thy in CalcTreeTEST ------------------";
130 "----------- check thy in CalcTreeTEST ------------------";
131 "WN1109 with Inverse_Z_Transform.thy when starting tests with CalcTreeTEST \n" ^
132 "we got the message: ME_Isa: thy 'Build_Inverse_Z_Transform' not in system \n" ^
133 "Below there are the steps which found out the reason: \n" ^
134 "store_pbt mistakenly stored that theory.";
135 val ctxt = Proof_Context.init_global @{theory Isac_Knowledge};
136 val SOME t = parseNEW ctxt "filterExpression (X = 3 / (z - 1/4 + -1/8 * (1/(z::real))))";
137 val SOME t = parseNEW ctxt "stepResponse (x[n::real]::bool)";
139 val fmz = ["filterExpression (X = 3 / (z - 1/4 + -1/8 * (1/(z::real))))", "boundVariable z",
140 "stepResponse (x[n::real]::bool)"];
141 val (dI,pI,mI) = ("Isac_Knowledge", ["Inverse", "Z_Transform", "SignalProcessing"],
142 ["SignalProcessing","Z_Transform","Inverse"]);
144 val (p,_,fb,nxt,_,pt) = CalcTreeTEST [(fmz, (dI,pI,mI))];
145 (*WAS ME_Isa: thy 'Build_Inverse_Z_Transform' not in system*)
147 "~~~~~ T fun CalcTreeTEST, args:"; val [(fmz, sp):fmz] = [(fmz, (dI,pI,mI))];
148 "~~~~~ fun nxt_specify_init_calc, args:"; val (fmz, (dI, pI, mI)) = (fmz, sp);
149 val thy = ThyC.get_theory dI;
150 mI = ["no_met"]; (*false*)
151 val (pI, (pors, pctxt), mI) = (pI, get_pbt pI |> #ppc |> prep_ori fmz thy, mI)
152 val {cas, ppc, thy=thy',...} = get_pbt pI; (*take dI from _refined_ pbl*)
153 "tracing bottom up"; Context.theory_name thy' = "Build_Inverse_Z_Transform"; (*WAS true*)
154 val dI = Context.theory_name (maxthy thy thy');
155 "tracing bottom up"; dI = "Build_Inverse_Z_Transform"; (*WAS true*)
157 val hdl = pblterm dI pI;
158 val (pt, _) = cappend_problem e_ctree [] (Istate.empty, pctxt) (fmz, (dI, pI, mI))
159 (pors, (dI, pI, mI), hdl, ContextC.empty)
161 "~~~~~ fun Step_Specify.by_tactic_input, args:"; val ((tac as Model_Problem), (pt, pos as (p,p_))) = (Model_Problem, (pt, ([], Pbl)));
162 val PblObj {origin = (oris, ospec, _), probl, spec, ctxt, ...} = get_obj I pt p;
163 "tracing bottom up"; #1(ospec) = "Build_Inverse_Z_Transform"; (*WAS true*)
165 "~~~~~ fun some_spec, args:"; val ((odI, opI, omI), (dI, pI, mI)) = (ospec, spec);
166 dI = ThyC.id_empty; (*true*)
167 odI = "Build_Inverse_Z_Transform"; (*true*)
168 dI = "empty_thy_id"; (*true*)
169 "~~~~~ after fun some_spec:";
170 val (dI, pI, mI) = some_spec ospec spec;
171 "tracing bottom up"; dI = "Build_Inverse_Z_Transform"; (*WAS true*)
172 val thy = ThyC.get_theory dI; (*caused ME_Isa: thy 'Build_Inverse_Z_Transform' not in system*)
174 "----------- identified error in fun getTactic, ThmC.string_of_thm ---------------";
175 "----------- identified error in fun getTactic, ThmC.string_of_thm ---------------";
176 "----------- identified error in fun getTactic, ThmC.string_of_thm ---------------";
178 CalcTree [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
179 ("Test",["sqroot-test","univariate","equation","test"],["Test","squ-equ-test-subpbl1"]))];
181 autoCalculate 1 CompleteCalcHead;
182 autoCalculate 1 (Steps 1);
183 autoCalculate 1 (Steps 1);
184 autoCalculate 1 (Steps 1);
185 getTactic 1 ([1],Frm); (*<RULESET> norm_equation </RULESET>*)
186 interSteps 1 ([1],Res);
187 "~~~~~ fun interSteps, args:"; val (cI, ip) = (1, ([1],Res));
188 val ((pt,p), tacis) = get_calc cI;
189 (not o is_interpos) ip = false;
190 val ip' = lev_pred' pt ip;
191 "~~~~~ fun go, args:"; val (pt, (pos as (p,p_):pos')) = (pt, ip);
192 (* ^^^^^^^^^ not in test/../ *)
194 val cn = children nd;
196 (is_rewset o (get_obj g_tac nd)) [(*root of nd*)] = true;
197 "~~~~~ fun detailrls, args:"; val (pt, (pos as (p,p_):pos')) = (pt, pos);
198 (* ^^^^^^^^^ only once in test/../solve.sml*)
199 val t = get_obj g_form pt p
200 val tac = get_obj g_tac pt p
201 val rls = (assoc_rls o rls_of) tac
202 val ctxt = get_ctxt pt pos
203 (*rls = Rule_Set.Repeat {calc = [], erls = ...*)
204 val is = init_istate tac t
205 (*TODO.WN060602 Pstate (["(t_, Problem (Isac,[equation,univar]))"]
206 is wrong for simpl, but working ?!? *)
207 val tac_ = Apply_Method' (Method.id_empty(*WN0402: see generate1 !?!*), SOME t, is, ctxt)
208 val pos' = ((lev_on o lev_dn) p, Frm)
209 val thy = ThyC.get_theory "Isac_Knowledge"
210 val (_,_,_,pt') = (*implicit Take*)generate1 tac_ (is, ctxt) (pt, pos');
211 (*val (_,_,(pt'',_)) = *)complete_solve CompleteSubpbl [] (pt',pos');
212 (* ^^^^^^^^^^^^^^ in test/../mathengine.sml*)
213 (* in pt'': tac = Rewrite ("rnorm_equation_add", "Test.rnorm_equation_add")},
214 ^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
215 "~~~~~ fun complete_solve , args:"; val (auto, c, (ptp as (_, p as (_,p_)): ctree * pos')) =
216 (CompleteSubpbl, [], (pt',pos'));
217 p = ([], Res) = false;
218 Library.member op = [Pbl,Met] p_ = false;
219 val (_, (_, c', ptp')) = Step_Solve.do_next ptp;
220 (* in pt': tac = Rewrite ("rnorm_equation_add", "Test.rnorm_equation_add")},
221 ^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
222 "~~~~~ fun do_next , args:"; val ((ptp as (pt, pos as (p,p_)))) = (ptp);
223 Method.id_empty = get_obj g_metID pt (par_pblobj pt p) = false;
224 val thy' = get_obj g_domID pt (par_pblobj pt p);
225 val ((ist, ctxt), sc) = resume_prog thy' (p,p_) pt;
226 val Next_Step (is, ctxt, tac_) = LI.find_next_step sc (pt,pos) ist ctxt;
227 (*tac_ = Rewrite' (..., ("rnorm_equation_add", "Test.rnorm_equation_add"), ...) !!!!!!!!!!!!!!!!*)
229 (*----- outcommented during cleanup of args in lucas-interpreter.sml ------------------------\\* )
230 "~~~~~ fun find_next_step , args:"; val (thy, (ptp as (pt, pos as (p, _)):ctree * pos'),
231 (sc as Prog (h $ body)), (Pstate (ist as (E,l,rls,a,v,s,b)), ctxt)) = ((thy',srls), (pt,pos), sc, is);
233 go_scan_up thy ptp sc ist true (*--> Accept_Tac (Rewrite' (.., (.., "Test.rnorm_equation_add"), ...)
234 BUT WE FIND IN THE CODE ABOVE IN find_next_step:*)
236 (*----------------------------------------------------------------------------------------------*)
237 if ThmC.string_of_thm @{thm rnorm_equation_add} = "\<not> ?b =!= 0 \<Longrightarrow> (?a = ?b) = (?a + - 1 * ?b = 0)"
238 then () else error "ThmC.string_of_thm changed";
239 if ThmC.string_of_thm @{thm rnorm_equation_add} = "\<not> ?b =!= 0 \<Longrightarrow> (?a = ?b) = (?a + - 1 * ?b = 0)"
240 then () else error "string_of_thm changed";
241 (*----------------------------------------------------------------------------------------------*)
243 (*SEARCH FOR THE ERROR WENT DOWN TO THE END OF THIS TEST, AND THEN UP TO HERE AGAIN*)
244 "~~~~~ fun begin_end_prog, args:"; val (tac_, is, (pt, pos as (p,p_))) = (tac_, is, ptp);
247 (p, Met) => ((lev_on o lev_dn) p, Frm)(*begin script*)
248 | (p, Res) => (lev_on p,Res) (*somewhere in script*)
250 generate1 tac_ is pos pt;
251 (* tac = Rewrite ("rnorm_equation_add", "Test.rnorm_equation_add")},
252 ^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
253 "~~~~~ fun generate1, args:"; val (thy, (Rewrite' (thy',ord',rls',pa,thm',f,(f',asm))),
254 (is, ctxt), (p,p_), pt) = ((ThyC.get_theory "Isac_Knowledge"), tac_, is, pos, pt);
255 val (pt,c) = cappend_atomic pt p (is, ContextC.insert_assumptions asm ctxt) f
256 (Rewrite thm') (f',asm) Complete;
257 (* in pt: tac = Rewrite ("rnorm_equation_add", "Test.rnorm_equation_add")},
258 ^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
259 "~~~~~ fun cappend_atomic, args:"; val (pt, p, ist_res, f, r, f', s) =
260 (pt, p, (is, ContextC.insert_assumptions asm ctxt), f, (Rewrite thm'), (f',asm), Complete);
261 existpt p pt andalso Tactic.is_empty (get_obj g_tac pt p) = false;
262 apfst (append_atomic p ist_res f r f' s) (cut_tree pt (p,Frm));
263 apfst : ('a -> 'b) -> 'a * 'c -> 'b * 'c;
264 (append_atomic p ist_res f r f' s) : ctree -> ctree;
266 (* HERE THE ERROR OCCURED IN THE FIRST APPROACH
267 getTactic 1 ([1,1],Frm); <ERROR> syserror in getTactic </ERROR> <<<<<=========================*)
268 "~~~~~ fun getTactic, args:"; val (cI, (p:pos')) = (1, ([1,1],Frm));
269 val ((pt,_),_) = get_calc cI
270 val (form, tac, asms) = pt_extract (pt, p)
272 "~~~~~ fun gettacticOK2xml, args:"; val ((cI:calcID), tac) = (cI, ta);
274 "~~~~~ fun tac2xml, args:"; val (j, (Rewrite thm')) = (i, tac);
275 "~~~~~ fun thm'2xml, args:"; val (j, ((ID, form) : thm'')) = ((j+i), thm');
276 ID = "rnorm_equation_add";
277 @{thm rnorm_equation_add};
278 (UnparseC.term o Thm.prop_of) form = "~ ?b =!= 0 ==> (?a = ?b) = (?a + -1 * ?b = 0)"
279 (*?!? should be "\<not> ?b =!= 0 \<Longrightarrow> (?a = ?b) = (?a + -1 * ?b = 0)"*)
280 (*thmstr2xml (j+i) form;
281 ERROR Undeclared constant: "Test.rnorm_equation_add" ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
285 (([], Frm), solve (x + 1 = 2, x)),
286 (([1], Frm), x + 1 = 2),
287 (([1,1], Frm), x + 1 = 2),
288 (([1,1], Res), x + 1 + -1 * 2 = 0),
289 (([1], Res), x + 1 + -1 * 2 = 0),
290 (([2], Res), -1 + x = 0)]
292 pt; --> tac = Rewrite ("rnorm_equation_add", "Test.rnorm_equation_add")*)
293 ( *----- outcommented during cleanup of args in lucas-interpreter.sml ------------------------//*)
295 "----------- improved fun getTactic for interSteps and numeral calculations --";
296 "----------- improved fun getTactic for interSteps and numeral calculations --";
297 "----------- improved fun getTactic for interSteps and numeral calculations --";
298 reset_states (); val cI = 1;
299 CalcTree [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
300 ("Test",["sqroot-test","univariate","equation","test"],["Test","squ-equ-test-subpbl1"]))];
302 autoCalculate 1 CompleteCalcHead;
303 autoCalculate 1 (Steps 1);
305 val cs = get_calc cI (* we improve from the calcstate here [*] *);
306 val pos as (_,p_) = get_pos cI 1 (* we improve from the calcstate here [*] *);
308 appendFormula 1 "x + 4 + -3 = 2" (*|> Future.join*);
309 interSteps 1 ([1],Res); (* already done by appendFormula, now showed to frontend *)
310 getTactic 1 ([1,1], Res);
311 (*<ID> sym_#add_Float ((~3,0), (0,0)) __ ((4,0), (0,0)) </ID> <<<<<================== to improve
312 <ISA> 1 + x = -3 + (4 + x) </ISA>*)
314 val ((pt''',p'''), tacis''') = get_calc cI;
317 (([], Frm), solve (x + 1 = 2, x)),
318 (([1], Frm), x + 1 = 2),
319 (([1,1], Frm), x + 1 = 2),
320 (([1,1], Res), 1 + x = 2),
321 (([1,2], Res), -3 + (4 + x) = 2),
322 (([1,3], Res), -3 + (x + 4) = 2),
323 (([1,4], Res), x + 4 + -3 = 2),
324 (([1], Res), x + 4 + -3 = 2)]*)
326 "~~~~~ fun appendFormula', args:"; val (cI, ifo) = (1, "x + 4 + -3 = 2");
327 (* val cs = get_calc cI (* we improve from the calcstate here [*] *);
328 val pos as (_,p_) = get_pos cI 1 (* we improve from the calcstate here [*] *);*)
329 val ("ok", cs' as (_, _, ptp')) = Step.do_next pos cs;
330 (*val ("ok", (_, c, ptp as (_,p))) = *)Step_Solve.by_term ptp' (encode ifo);
331 "~~~~~ fun Step_Solve.by_term , args:"; val (cs as (_, _, ptp as (pt, pos as (p, p_))), istr) =
333 val SOME f_in = parse (ThyC.get_theory "Isac_Knowledge") istr
334 val f_in = Thm.term_of f_in
335 val f_succ = get_curr_formula (pt, pos);
336 f_succ = f_in = false;
337 val NONE = cas_input f_in
338 val pos_pred = lev_back' pos
339 (* f_pred ---"step pos cs"---> f_succ in appendFormula *)
340 val f_pred = get_curr_formula (pt, pos_pred);
341 (*val msg_calcstate' = *)compare_step ([], [], (pt, pos_pred)) f_in (*<<=====*);
342 "~~~~~ fun compare_step, args:"; val (((tacis, c, ptp as (pt, pos as (p,p_)))), ifo) =
343 (([], [], (pt, pos_pred)), f_in);
346 Frm => get_obj g_form pt p
347 | Res => (fst o (get_obj g_result pt)) p
348 | _ => TermC.empty (*on PblObj is fo <> ifo*);
349 val {nrls, ...} = get_met (get_obj g_metID pt (par_pblobj pt p))
350 val {rew_ord, erls, rules, ...} = Rule_Set.rep nrls;
351 (*val (found, der) = *)Derive.steps rew_ord erls rules fo ifo; (*<---------------*)
352 "~~~~~ fun .concat_deriv, args:"; val (rew_ord, erls, rules, fo, ifo) =
353 (rew_ord, erls, rules, fo, ifo);
354 fun derivat ([]:(term * rule * (term * term list)) list) = TermC.empty
355 | derivat dt = (#1 o #3 o last_elem) dt
356 fun equal (_,_,(t1, _)) (_,_,(t2, _)) = t1=t2
357 (*val fod = *)Derive.do_one (Isac"") erls rules (snd rew_ord) NONE fo;
358 (*val ifod = *)Derive.do_one (Isac"") erls rules (snd rew_ord) NONE ifo;