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 {* Know_Store.set_ref_thy @{theory};
7 fun autoCalculate' cI auto = autoCalculate cI auto |> Future.join *}
8 ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Interpret/mathengine.sml"
10 "--------------------------------------------------------";
11 "table of contents --------------------------------------";
12 "--------------------------------------------------------";
13 "----------- change to TermC.parse ctxt -----------------------";
14 "----------- tryrefine ----------------------------------";
15 "----------- search for Or_to_List ----------------------";
16 "----------- check thy in Test_Code.init_calc @{context} ------------------";
17 "----------- identified error in fun getTactic, ThmC.string_of_thm ---------------";
18 "----------- improved fun getTactic for interSteps and numeral calculations --";
19 "--------------------------------------------------------";
20 "--------------------------------------------------------";
21 "--------------------------------------------------------";
23 "----------- change to TermC.parse ctxt -----------------------";
24 "----------- change to TermC.parse ctxt -----------------------";
25 "----------- change to TermC.parse ctxt -----------------------";
26 "===== start calculation: from problem description (fmz) to origin";
27 val fmz = ["realTestGiven (((1+2)*4/3) \<up> 2)", "realTestFind s"];
28 val (thyID, pblID, metID) =
29 ("Test", ["calculate", "test"], ["Test", "test_calculate"]);
30 (*======= Isabelle2013- 2 --> Isabelle2014: unclear, why this test ever run =====================*)
33 "----------- tryrefine ----------------------------------";
34 "----------- tryrefine ----------------------------------";
35 "----------- tryrefine ----------------------------------";
37 CalcTree @{context} [(["equality (x/(x^2 - 6*x+9) - 1/(x^2 - 3*x) =1/x)",
38 "solveFor x", "solutions L"],
39 ("RatEq",["univariate", "equation"],["no_met"]))];
41 moveActiveRoot 1; autoCalculate 1 CompleteCalc;
43 refineProblem 1 ([1],Res) "pbl_equ_univ"
44 (*gives "pbl_equ_univ_rat" correct*);
46 refineProblem 1 ([1],Res) (Ptool.pblID2guh @{context} ["LINEAR", "univariate", "equation"])
47 (*gives "pbl_equ_univ_lin" incorrect*);
49 "--------- search for Or_to_List ------------------------";
50 "--------- search for Or_to_List ------------------------";
51 "--------- search for Or_to_List ------------------------";
52 val fmz = ["equality (x \<up> 2 + 4*x + 5 = (2::real))", "solveFor x", "solutions L"];
53 val (dI',pI',mI') = ("Isac_Knowledge", ["univariate", "equation"], ["no_met"])
54 val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))];
55 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
56 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
57 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
58 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
59 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
60 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
61 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
62 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
63 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
64 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Subproblem"*)
65 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
66 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
67 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
68 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
69 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
70 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
71 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
72 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
73 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
74 val (p''''',_,f,nxt''''',_,pt''''') = me nxt p [] pt;
75 "~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ continue AFTER previous step 'me' ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~";
76 "~~~~~ fun me, args:"; val (tac, (p:pos'), (_:NEW(*remove*)), (pt:ctree)) =
77 (nxt''''', p''''', [], pt''''');
78 val ("ok", (_, _, ptp)) = Step.by_tactic tac (pt,p)
80 "~~~~~ fun Step.do_next, args:"; val (((ip as (_,p_)):pos'), ((ptp as (pt,p), tacis):Calc.state_pre)) =
81 (p, ((pt, e_pos'),[]));
82 val pIopt = get_pblID (pt,ip);
83 ip = ([],Res); (*false*)
85 member op = [Pbl,Met] p_; (*false*)
86 "~~~~~ fun do_next, args:"; val (ptp as (pt, pos as (p,p_))) = (pt,ip);
87 MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p); (*false*)
88 val thy' = get_obj g_domID pt (par_pblobj pt p);
89 val ((ist, ctxt), sc) = resume_prog (p,p_) pt;
91 val Next_Step (istate, ctxt, tac) = LI.find_next_step sc (pt,pos) ist ctxt; (*WAS Empty_Tac_: tac_*)
92 case tac of Or_to_List' _ => ()
93 | _ => error "Or_to_List broken ?"
96 "----------- check thy in Test_Code.init_calc @{context} ------------------";
97 "----------- check thy in Test_Code.init_calc @{context} ------------------";
98 "----------- check thy in Test_Code.init_calc @{context} ------------------";
99 "WN1109 with Inverse_Z_Transform.thy when starting tests with Test_Code.init_calc @{context} \n" ^
100 "we got the message: ME_Isa: thy 'Build_Inverse_Z_Transform' not in system \n" ^
101 "Below there are the steps which found out the reason: \n" ^
102 "store_pbt mistakenly stored that theory.";
103 val ctxt = Proof_Context.init_global @{theory Isac_Knowledge};
104 val SOME t = ParseC.term_opt ctxt "filterExpression (X = 3 / (z - 1/4 + - 1/8 * (1/(z::real))))";
105 val SOME t = ParseC.term_opt ctxt "stepResponse (x[n::real]::bool)";
107 val fmz = ["filterExpression (X = 3 / (z - 1/4 + - 1/8 * (1/(z::real))))", "boundVariable z",
108 "stepResponse (x[n::real]::bool)"];
109 val (dI,pI,mI) = ("Isac_Knowledge", ["Inverse", "Z_Transform", "SignalProcessing"],
110 ["SignalProcessing", "Z_Transform", "Inverse"]);
112 val (p,_,fb,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI,pI,mI))];
113 (*WAS ME_Isa: thy 'Build_Inverse_Z_Transform' not in system*)
114 (*old* )val ctxt = thy_id |> ThyC.get_theory_PIDE ctxt |> Proof_Context.init_global
115 ( *new*)val thy = thy_id |> ThyC.get_theory_PIDE ctxt (*^^^^^^^^^^^^^^^^^^^^^^^^^ misleading*);
117 "~~~~~ fun init_calc @{context} , args:"; val [(fmz, sp):Formalise.T] = [(fmz, (dI,pI,mI))];
118 (*val ((pt, p), tacis) =*)
119 Step_Specify.initialise' thy (fmz, sp);
120 "~~~~~ fun initialise' , args:"; val (fmz, (dI, pI, mI)) = (fmz, sp);
121 (*val (_, hdl, (dI, pI, mI), pors, pctxt) =*)
122 Step_Specify.initialise thy (fmz, (dI, pI, mI));
123 "~~~~~ fun initialise , args:"; val (fmz, (dI, pI, mI)) = (fmz, (dI, pI, mI));
124 val thy = ThyC.get_theory dI
125 val ctxt = Proof_Context.init_global thy;
126 (*if*) mI = ["no_met"](*else*);
127 val (pors, pctxt) = Problem.from_store ctxt pI |> #model |> O_Model.init thy fmz;
128 val {cas, model, thy=thy',...} = Problem.from_store ctxt pI; (*take dI from _refined_ pbl*)
129 "tracing bottom up"; Context.theory_name thy' = "Build_Inverse_Z_Transform"; (*WAS true*)
130 val dI = Context.theory_name (ThyC.parent_of thy thy');
131 "tracing bottom up"; dI = "Build_Inverse_Z_Transform"; (*WAS true*)
133 val hdl = pblterm dI pI;
134 val (pt, _) = cappend_problem e_ctree [] (Istate.empty, pctxt) (fmz, (dI, pI, mI))
135 (pors, (dI, pI, mI), hdl, ContextC.empty)
137 "~~~~~ fun Step_Specify.by_tactic_input, args:"; val ((tac as Model_Problem), (pt, pos as (p,p_))) = (Model_Problem, (pt, ([], Pbl)));
138 val PblObj {origin = (oris, ospec, _), probl, spec, ctxt, ...} = get_obj I pt p;
139 "tracing bottom up"; #1(ospec) = "Build_Inverse_Z_Transform"; (*WAS true*)
141 "~~~~~ fun References.select_input, args:"; val ((odI, opI, omI), (dI, pI, mI)) = (ospec, spec);
142 dI = ThyC.id_empty; (*true*)
143 odI = "Build_Inverse_Z_Transform"; (*true*)
144 dI = ThyC.id_empty; (*true*)
145 "~~~~~ after fun References.select_input:";
146 val (dI, pI, mI) = References.select_input ospec spec;
147 "tracing bottom up"; dI = "Build_Inverse_Z_Transform"; (*WAS true*)
148 val thy = ThyC.get_theory dI; (*caused ME_Isa: thy 'Build_Inverse_Z_Transform' not in system*)
150 "----------- identified error in fun getTactic, ThmC.string_of_thm ---------------";
151 "----------- identified error in fun getTactic, ThmC.string_of_thm ---------------";
152 "----------- identified error in fun getTactic, ThmC.string_of_thm ---------------";
154 CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
155 ("Test",["sqroot-test", "univariate", "equation", "test"],["Test", "squ-equ-test-subpbl1"]))];
157 autoCalculate 1 CompleteCalcHead;
158 autoCalculate 1 (Steps 1);
159 autoCalculate 1 (Steps 1);
160 autoCalculate 1 (Steps 1);
161 getTactic 1 ([1],Frm); (*<RULESET> norm_equation </RULESET>*)
162 interSteps 1 ([1],Res);
163 "~~~~~ fun interSteps, args:"; val (cI, ip) = (1, ([1],Res));
164 val ((pt,p), tacis) = States.get_calc cI;
165 (not o is_interpos) ip = false;
166 val ip' = lev_pred' pt ip;
167 "~~~~~ fun go, args:"; val (pt, (pos as (p,p_):pos')) = (pt, ip);
168 (* \<up> \<up> \<up> not in test/../ *)
170 val cn = children nd;
172 (is_rewset o (get_obj g_tac nd)) [(*root of nd*)] = true;
173 "~~~~~ fun detailrls, args:"; val (pt, (pos as (p,p_):pos')) = (pt, pos);
174 (* \<up> \<up> \<up> only once in test/../solve.sml*)
175 val t = get_obj g_form pt p
176 val tac = get_obj g_tac pt p
177 val ctxt = get_ctxt pt pos
178 val rls = ((get_rls ctxt) o rls_of) tac
179 val ctxt = get_ctxt pt pos
180 (*rls = Rule_Set.Repeat {calc = [], asm_rls = ...*)
181 val is = Istate.init_detail ctxt tac t
182 (*TODO.WN060602 Pstate (["(t_, Problem (Isac,[equation,univar]))"]
183 is wrong for simpl, but working ?!? *)
184 val tac_ = Apply_Method' (MethodC.id_empty(*WN0402: see Step.add !?!*), SOME t, is, ctxt)
185 val pos' = ((lev_on o lev_dn) p, Frm)
186 val thy = ThyC.get_theory "Isac_Knowledge"
187 val (_,_,_,pt') = (*implicit Take*)Step.add tac_ (is, ctxt) (pt, pos');
188 (*val (_,_,(pt'',_)) = *)complete_solve CompleteSubpbl [] (pt',pos');
189 (* \<up> \<up> \<up> \<up> ^^ in test/../mathengine.sml*)
190 (* in pt'': tac = Rewrite ("rnorm_equation_add", "Test.rnorm_equation_add")},
191 \<up> \<up> \<up> \<up> \<up> \<up> \<up> \<up> \<up> *)
192 "~~~~~ fun complete_solve , args:"; val (auto, c, (ptp as (_, p as (_,p_)): ctree * pos')) =
193 (CompleteSubpbl, [], (pt',pos'));
194 p = ([], Res) = false;
195 member op = [Pbl,Met] p_ = false;
196 val (_, (_, c', ptp')) = Step_Solve.do_next ptp;
197 (* in pt': tac = Rewrite ("rnorm_equation_add", "Test.rnorm_equation_add")},
198 \<up> \<up> \<up> \<up> \<up> \<up> \<up> \<up> \<up> *)
199 "~~~~~ fun do_next , args:"; val ((ptp as (pt, pos as (p,p_)))) = (ptp);
200 MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) = false;
201 val thy' = get_obj g_domID pt (par_pblobj pt p);
202 val ((ist, ctxt), sc) = resume_prog (p,p_) pt;
203 val Next_Step (is, ctxt, tac_) = LI.find_next_step sc (pt,pos) ist ctxt;
204 (*tac_ = Rewrite' (..., ("rnorm_equation_add", "Test.rnorm_equation_add"), ...) !!!!!!!!!!!!!!!!*)
206 (*----- outcommented during cleanup of args in lucas-interpreter.sml ------------------------\\* )
207 "~~~~~ fun find_next_step , args:"; val (thy, (ptp as (pt, pos as (p, _)):ctree * pos'),
208 (sc as Prog (h $ body)), (Pstate (ist as (E,l,rls,a,v,s,b)), ctxt)) = ((thy',prog_rls), (pt,pos), sc, is);
210 go_scan_up thy ptp sc ist true (*--> Accept_Tac (Rewrite' (.., (.., "Test.rnorm_equation_add"), ...)
211 BUT WE FIND IN THE CODE ABOVE IN find_next_step:*)
213 (*----------------------------------------------------------------------------------------------*)
214 if ThmC.string_of_thm @{thm rnorm_equation_add} = "\<not> ?b =!= 0 \<Longrightarrow> (?a = ?b) = (?a + - 1 * ?b = 0)"
215 then () else error "ThmC.string_of_thm changed";
216 if ThmC.string_of_thm @{thm rnorm_equation_add} = "\<not> ?b =!= 0 \<Longrightarrow> (?a = ?b) = (?a + - 1 * ?b = 0)"
217 then () else error "string_of_thm changed";
218 (*----------------------------------------------------------------------------------------------*)
220 (*SEARCH FOR THE ERROR WENT DOWN TO THE END OF THIS TEST, AND THEN UP TO HERE AGAIN*)
221 "~~~~~ fun begin_end_prog, args:"; val (tac_, is, (pt, pos as (p,p_))) = (tac_, is, ptp);
224 (p, Met) => ((lev_on o lev_dn) p, Frm)(*begin script*)
225 | (p, Res) => (lev_on p,Res) (*somewhere in script*)
227 Step.add tac_ is pos pt;
228 (* tac = Rewrite ("rnorm_equation_add", "Test.rnorm_equation_add")},
229 \<up> \<up> \<up> \<up> \<up> \<up> \<up> \<up> \<up> *)
230 "~~~~~ fun add, args:"; val (thy, (Rewrite' (thy',ord',rls',pa,thm',f,(f',asm))),
231 (is, ctxt), (p,p_), pt) = ((ThyC.get_theory "Isac_Knowledge"), tac_, is, pos, pt);
232 val (pt,c) = cappend_atomic pt p (is, ContextC.insert_assumptions asm ctxt) f
233 (Rewrite thm') (f',asm) Complete;
234 (* in pt: tac = Rewrite ("rnorm_equation_add", "Test.rnorm_equation_add")},
235 \<up> \<up> \<up> \<up> \<up> \<up> \<up> \<up> \<up> *)
236 "~~~~~ fun cappend_atomic, args:"; val (pt, p, ist_res, f, r, f', s) =
237 (pt, p, (is, ContextC.insert_assumptions asm ctxt), f, (Rewrite thm'), (f',asm), Complete);
238 existpt p pt andalso Tactic.is_empty (get_obj g_tac pt p) = false;
239 apfst (append_atomic p ist_res f r f' s) (cut_tree pt (p,Frm));
240 apfst : ('a -> 'b) -> 'a * 'c -> 'b * 'c;
241 (append_atomic p ist_res f r f' s) : ctree -> ctree;
243 (* HERE THE ERROR OCCURED IN THE FIRST APPROACH
244 getTactic 1 ([1,1],Frm); <ERROR> syserror in getTactic </ERROR> <<<<<=========================*)
245 "~~~~~ fun getTactic, args:"; val (cI, (p:pos')) = (1, ([1,1],Frm));
246 val ((pt,_),_) = States.get_calc cI
247 val (form, tac, asms) = ME_Misc.pt_extract (pt, p)
249 "~~~~~ fun gettacticOK2xml, args:"; val ((cI:calcID), tac) = (cI, ta);
251 "~~~~~ fun tac2xml, args:"; val (j, (Rewrite thm')) = (i, tac);
252 "~~~~~ fun thm'2xml, args:"; val (j, ((ID, form) : thm'')) = ((j+i), thm');
253 ID = "rnorm_equation_add";
254 @{thm rnorm_equation_add};
255 (UnparseC.term o Thm.prop_of) form = "~ ?b =!= 0 ==> (?a = ?b) = (?a + - 1 * ?b = 0)"
256 (*?!? should be "\<not> ?b =!= 0 \<Longrightarrow> (?a = ?b) = (?a + - 1 * ?b = 0)"*)
257 (*thmstr2xml (j+i) form;
258 ERROR Undeclared constant: "Test.rnorm_equation_add" \<up> \<up> \<up> \<up> \<up> \<up> \<up> \<up> \<up> \<up> \<up> \<up> \<up> \<up> ^*)
260 Test_Tool.show_pt pt;
262 (([], Frm), solve (x + 1 = 2, x)),
263 (([1], Frm), x + 1 = 2),
264 (([1,1], Frm), x + 1 = 2),
265 (([1,1], Res), x + 1 + - 1 * 2 = 0),
266 (([1], Res), x + 1 + - 1 * 2 = 0),
267 (([2], Res), - 1 + x = 0)]
269 pt; --> tac = Rewrite ("rnorm_equation_add", "Test.rnorm_equation_add")*)
270 ( *----- outcommented during cleanup of args in lucas-interpreter.sml ------------------------//*)
272 "----------- improved fun getTactic for interSteps and numeral calculations --";
273 "----------- improved fun getTactic for interSteps and numeral calculations --";
274 "----------- improved fun getTactic for interSteps and numeral calculations --";
275 val ctxt = Proof_Context.init_global @{theory Test};
276 States.reset (); val cI = 1;
277 CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
278 ("Test",["sqroot-test", "univariate", "equation", "test"],["Test", "squ-equ-test-subpbl1"]))];
280 autoCalculate 1 CompleteCalcHead;
281 autoCalculate 1 (Steps 1);
283 val cs = States.get_calc cI (* we improve from the calcstate here [*] *);
284 val pos as (_,p_) = States.get_pos cI 1 (* we improve from the calcstate here [*] *);
286 appendFormula 1 "x + 4 + -3 = 2" (*|> Future.join*);
287 interSteps 1 ([1],Res); (* already done by appendFormula, now showed to frontend *)
288 getTactic 1 ([1,1], Res);
289 (*<ID> sym_#add_Float ((~3,0), (0,0)) __ ((4,0), (0,0)) </ID> <<<<<================== to improve
290 <ISA> 1 + x = -3 + (4 + x) </ISA>*)
292 val ((pt''',p'''), tacis''') = States.get_calc cI;
293 Test_Tool.show_pt pt'''
295 (([], Frm), solve (x + 1 = 2, x)),
296 (([1], Frm), x + 1 = 2),
297 (([1,1], Frm), x + 1 = 2),
298 (([1,1], Res), 1 + x = 2),
299 (([1,2], Res), -3 + (4 + x) = 2),
300 (([1,3], Res), -3 + (x + 4) = 2),
301 (([1,4], Res), x + 4 + -3 = 2),
302 (([1], Res), x + 4 + -3 = 2)]*)
304 "~~~~~ fun appendFormula', args:"; val (cI, ifo) = (1, "x + 4 + -3 = 2");
305 (* val cs = States.get_calc cI (* we improve from the calcstate here [*] *);
306 val pos as (_,p_) = States.get_pos cI 1 (* we improve from the calcstate here [*] *);*)
307 val ("ok", cs' as (_, _, ptp')) = Step.do_next pos cs;
308 (*val ("ok", (_, c, ptp as (_,p))) = *)Step_Solve.by_term ptp' (encode ifo);
309 "~~~~~ fun Step_Solve.by_term , args:"; val (cs as (_, _, ptp as (pt, pos as (p, p_))), istr) =
311 val SOME f_in = ParseC.term_opt (get_ctxt pt pos) istr
312 val f_succ = get_curr_formula (pt, pos);
313 f_succ = f_in = false;
314 val NONE = CAS_Cmd.input f_in
315 val pos_pred = lev_back' pos
316 (* f_pred ---"step pos cs"---> f_succ in appendFormula *)
317 val f_pred = get_curr_formula (pt, pos_pred);
318 (*val msg_calcstate' = *)compare_step ([], [], (pt, pos_pred)) f_in (*<<=====*);
319 "~~~~~ fun compare_step, args:"; val (((tacis, c, ptp as (pt, pos as (p,p_)))), ifo) =
320 (([], [], (pt, pos_pred)), f_in);
323 Frm => get_obj g_form pt p
324 | Res => (fst o (get_obj g_result pt)) p
325 | _ => TermC.empty (*on PblObj is fo <> ifo*);
326 val {rew_rls, ...} = MethodC.from_store ctxt (get_obj g_metID pt (par_pblobj pt p))
327 val {rew_ord, asm_rls, rules, ...} = Rule_Set.rep rew_rls;
328 (*val (found, der) = *)Derive.steps ctxt rew_ord asm_rls rules fo ifo; (*<---------------*)
329 "~~~~~ fun concat_deriv, args:"; val (rew_ord, asm_rls, rules, fo, ifo) =
330 (rew_ord, asm_rls, rules, fo, ifo);
331 fun derivat ([]:(term * rule * (term * term list)) list) = TermC.empty
332 | derivat dt = (#1 o #3 o last_elem) dt
333 fun equal (_,_,(t1, _)) (_,_,(t2, _)) = t1=t2
334 (*val fod = *)Derive.do_one ctxt asm_rls rules (snd rew_ord) NONE fo;
335 (*val ifod = *)Derive.do_one ctxt asm_rls rules (snd rew_ord) NONE ifo;