1 (* Title: tests on inform.sml
2 Author: Walther Neuper 060225,
3 (c) due to copyright terms
5 use"../smltest/ME/inform.sml";
9 "-----------------------------------------------------------------";
10 "table of contents -----------------------------------------------";
11 "-----------------------------------------------------------------";
12 "appendForm with miniscript with mini-subpbl:";
13 "--------- appendFormula: on Res + equ_nrls ----------------------";
14 "--------- appendFormula: on Frm + equ_nrls ----------------------";
15 "--------- appendFormula: on Res + NO deriv ----------------------";
16 "--------- appendFormula: on Res + late deriv --------------------";
17 "--------- appendFormula: on Res + late deriv [x = 3 + -2]---///--";
18 "replaceForm with miniscript with mini-subpbl:";
19 "--------- replaceFormula: on Res + = ----------------------------";
20 "--------- replaceFormula: on Res + = 1st Nd ---------------------";
21 "--------- replaceFormula: on Frm + = 1st Nd ---------------------";
22 "--------- replaceFormula: cut calculation -----------------------";
23 "--------- replaceFormula: cut calculation -----------------------";
24 (* 040307 copied from informtest.sml ... old versions
25 "--------- maximum-example, UC: Modeling / modifyCalcHead --------";*)
26 "--------- syntax error ------------------------------------------";
28 "--------- CAS-command on ([],Pbl) -------------------------------";
29 "--------- CAS-command on ([],Pbl) FE-interface ------------------";
30 "--------- inform [rational,simplification] ----------------------";
31 "--------- Take as 1st tac, start with <NEW> (CAS input) ---------";
32 "--------- Take as 1st tac, start from exp -----------------------";
33 "--------- init_form, start with <NEW> (CAS input) ---------------";
34 "--------- build fun check_err_patt ------------------------------";
35 "--------- build fun check_err_patt ?bdv -------------------------";
36 "--------- build fun check_error_patterns ------------------------";
37 "--------- embed fun check_error_patterns ------------------------";
38 "-----------------------------------------------------------------";
39 "-----------------------------------------------------------------";
40 "-----------------------------------------------------------------";
47 "--------- appendFormula: on Res + equ_nrls ----------------------";
48 "--------- appendFormula: on Res + equ_nrls ----------------------";
49 "--------- appendFormula: on Res + equ_nrls ----------------------";
51 val Script sc = (#scr o get_met) ["Test","squ-equ-test-subpbl1"];
52 (writeln o term2str) sc;
53 val Script sc = (#scr o get_met) ["Test","solve_linear"];
54 (writeln o term2str) sc;
57 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
58 ("Test", ["sqroot-test","univariate","equation","test"],
59 ["Test","squ-equ-test-subpbl1"]))];
60 Iterator 1; moveActiveRoot 1;
61 autoCalculate 1 CompleteCalcHead;
62 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
63 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);
65 appendFormula 1 "-2 * 1 + (1 + x) = 0"; refFormula 1 (get_pos 1 1);
66 val ((pt,_),_) = get_calc 1;
67 val str = pr_ptree pr_short pt;
70 (*============ inhibit exn AK110726 ==============================================
71 (* 2nd string should be the same as 1st one *)
72 ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + -1 * 2 = 0\n2.1. x + 1 + -1 * 2 = 0\n2.2. 1 + x + -1 * 2 = 0\n2.3. 1 + (x + -1 * 2) = 0\n2.4. 1 + (x + -2) = 0\n2.5. 1 + (x + -2 * 1) = 0\n2.6. 1 + x + -2 * 1 = 0\n";
73 ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + -1 * 2 = 0\n2.1. x + 1 + -1 * 2 = 0\n2.2. -1 * 2 + (x + 1) = 0\n2.3. -1 * 2 + (1 + x) = 0\n2.4. 1 + (-1 * 2 + x) = 0\n2.5. 1 + (-2 + x) = 0\n2.6. 1 + (-2 * 1 + x) = 0\n";
74 if str = ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + -1 * 2 = 0\n2.1. x + 1 + -1 * 2 = 0\n2.2. -1 * 2 + (x + 1) = 0\n2.3. -1 * 2 + (1 + x) = 0\n2.4. 1 + (-1 * 2 + x) = 0\n2.5. 1 + (-2 + x) = 0\n2.6. 1 + (-2 * 1 + x) = 0\n" then ()
75 else error "inform.sml: diff.behav.appendFormula: on Res + equ 1";
76 ============ inhibit exn AK110726 ==============================================*)
78 moveDown 1 ([ ],Pbl); refFormula 1 ([1],Frm); (*x + 1 = 2*)
79 moveDown 1 ([1],Frm); refFormula 1 ([1],Res); (*x + 1 + -1 * 2 = 0*)
81 (*the seven steps of detailed derivation*)
82 moveDown 1 ([1 ],Res); refFormula 1 ([2,1],Frm);
83 moveDown 1 ([2,1],Frm); refFormula 1 ([2,1],Res);
84 moveDown 1 ([2,1],Res); refFormula 1 ([2,2],Res);
85 moveDown 1 ([2,2],Res); refFormula 1 ([2,3],Res);
86 moveDown 1 ([2,3],Res); refFormula 1 ([2,4],Res);
87 moveDown 1 ([2,4],Res); refFormula 1 ([2,5],Res);
88 moveDown 1 ([2,5],Res); refFormula 1 ([2,6],Res);
89 val ((pt,_),_) = get_calc 1;
90 if "-2 * 1 + (1 + x) = 0" = term2str (fst (get_obj g_result pt [2,6])) then()
91 else error "inform.sml: diff.behav.appendFormula: on Res + equ 2";
93 fetchProposedTactic 1; (*takes Iterator 1 _1_*)
95 (*============ inhibit exn AK110725 ==============================================
96 (* ERROR: exception Bind raised *)
97 val (_,(tac,_,_)::_) = get_calc 1;
98 if tac = Rewrite_Set "Test_simplify" then ()
99 else error "inform.sml: diff.behav.appendFormula: on Res + equ 3";
100 ============ inhibit exn AK110725 ==============================================*)
102 autoCalculate 1 CompleteCalc;
103 val ((pt,_),_) = get_calc 1;
104 if "[x = 1]" = term2str (fst (get_obj g_result pt [])) then ()
105 else error "inform.sml: diff.behav.appendFormula: on Res + equ 4";
106 (* autoCalculate 1 CompleteCalc;
107 val ((pt,p),_) = get_calc 1;
108 (writeln o istates2str) (get_obj g_loc pt [ ]);
109 (writeln o istates2str) (get_obj g_loc pt [1]);
110 (writeln o istates2str) (get_obj g_loc pt [2]);
111 (writeln o istates2str) (get_obj g_loc pt [3]);
112 (writeln o istates2str) (get_obj g_loc pt [3,1]);
113 (writeln o istates2str) (get_obj g_loc pt [3,2]);
114 (writeln o istates2str) (get_obj g_loc pt [4]);
117 "----------------------------------------------------------";
119 val fod = make_deriv (@{theory "Isac"}) Atools_erls
120 ((#rules o rep_rls) Test_simplify)
121 (sqrt_right false (@{theory "Pure"})) NONE
122 (str2term "x + 1 + -1 * 2 = 0");
123 (writeln o trtas2str) fod;
125 val ifod = make_deriv (@{theory "Isac"}) Atools_erls
126 ((#rules o rep_rls) Test_simplify)
127 (sqrt_right false (@{theory "Pure"})) NONE
128 (str2term "-2 * 1 + (1 + x) = 0");
129 (writeln o trtas2str) ifod;
130 fun equal (_,_,(t1, _)) (_,_,(t2, _)) = t1 = t2;
131 val (fod', rifod') = dropwhile' equal (rev fod) (rev ifod);
132 val der = fod' @ (map rev_deriv' rifod');
133 (writeln o trtas2str) der;
134 "----------------------------------------------------------";
137 "--------- appendFormula: on Frm + equ_nrls ----------------------";
138 "--------- appendFormula: on Frm + equ_nrls ----------------------";
139 "--------- appendFormula: on Frm + equ_nrls ----------------------";
141 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
142 ("Test", ["sqroot-test","univariate","equation","test"],
143 ["Test","squ-equ-test-subpbl1"]))];
144 Iterator 1; moveActiveRoot 1;
145 autoCalculate 1 CompleteCalcHead;
146 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1) (*x + 1 = 2*);
147 appendFormula 1 "2+ -1 + x = 2"; refFormula 1 (get_pos 1 1);
149 moveDown 1 ([],Pbl); refFormula 1 ([1],Frm) (*x + 1 = 2*);
151 moveDown 1 ([1 ],Frm); refFormula 1 ([1,1],Frm);
152 moveDown 1 ([1,1],Frm); refFormula 1 ([1,1],Res);
153 moveDown 1 ([1,1],Res); refFormula 1 ([1,2],Res);
154 moveDown 1 ([1,2],Res); refFormula 1 ([1,3],Res);
155 moveDown 1 ([1,3],Res); refFormula 1 ([1,4],Res);
156 moveDown 1 ([1,4],Res); refFormula 1 ([1,5],Res);
157 moveDown 1 ([1,5],Res); refFormula 1 ([1,6],Res);
158 val ((pt,_),_) = get_calc 1;
159 if "2 + -1 + x = 2" = term2str (fst (get_obj g_result pt [1,6])) then()
160 else error "inform.sml: diff.behav.appendFormula: on Frm + equ 1";
162 fetchProposedTactic 1; (*takes Iterator 1 _1_*)
163 val (_,(tac,_,_)::_) = get_calc 1;
164 if tac = Rewrite_Set "norm_equation" then ()
165 else error "inform.sml: diff.behav.appendFormula: on Frm + equ 2";
166 autoCalculate 1 CompleteCalc;
167 val ((pt,_),_) = get_calc 1;
168 if "[x = 1]" = term2str (fst (get_obj g_result pt [])) then ()
169 else error "inform.sml: diff.behav.appendFormula: on Frm + equ 3";
172 "--------- appendFormula: on Res + NO deriv ----------------------";
173 "--------- appendFormula: on Res + NO deriv ----------------------";
174 "--------- appendFormula: on Res + NO deriv ----------------------";
176 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
177 ("Test", ["sqroot-test","univariate","equation","test"],
178 ["Test","squ-equ-test-subpbl1"]))];
179 Iterator 1; moveActiveRoot 1;
180 autoCalculate 1 CompleteCalcHead;
181 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
182 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);
184 appendFormula 1 "x = 2";
185 val ((pt,p),_) = get_calc 1;
186 val str = pr_ptree pr_short pt;
188 if str = ". ----- pblobj -----\n1. x + 1 = 2\n" andalso p = ([1], Res)
190 else error "inform.sml: diff.behav.appendFormula: Res + NOder 1";
192 fetchProposedTactic 1;
193 val (_,(tac,_,_)::_) = get_calc 1;
194 if tac = Rewrite_Set "Test_simplify" then ()
195 else error "inform.sml: diff.behav.appendFormula: Res + NOder 2";
196 autoCalculate 1 CompleteCalc;
197 val ((pt,_),_) = get_calc 1;
198 if "[x = 1]" = term2str (fst (get_obj g_result pt [])) then ()
199 else error "inform.sml: diff.behav.appendFormula: on Frm + equ 3";
202 "--------- appendFormula: on Res + late deriv --------------------";
203 "--------- appendFormula: on Res + late deriv --------------------";
204 "--------- appendFormula: on Res + late deriv --------------------";
206 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
207 ("Test", ["sqroot-test","univariate","equation","test"],
208 ["Test","squ-equ-test-subpbl1"]))];
209 Iterator 1; moveActiveRoot 1;
210 autoCalculate 1 CompleteCalcHead;
211 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
212 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);
214 appendFormula 1 "x = 1";
215 val ((pt,p),_) = get_calc 1;
216 val str = pr_ptree pr_short pt;
218 if str = ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + -1 * 2 = 0\n3. ----- pblobj -----\n3.1. -1 + x = 0\n3.2. x = 0 + -1 * -1\n3.2.1. x = 0 + -1 * -1\n3.2.2. x = 0 + 1\n" andalso p = ([3,2], Res)
219 then () (*finds 1 step too early: ([3,2], Res) "x = 1" also by script !!!*)
220 else error "inform.sml: diff.behav.appendFormula: Res + late d 1";
222 fetchProposedTactic 1;
223 val (_,(tac,_,_)::_) = get_calc 1;
224 if tac = Check_Postcond ["linear", "univariate", "equation", "test"] then ()
225 else error "inform.sml: diff.behav.appendFormula: Res + late d 2";
226 autoCalculate 1 CompleteCalc;
227 val ((pt,_),_) = get_calc 1;
228 if "[x = 1]" = term2str (fst (get_obj g_result pt [])) then ()
229 else error "inform.sml: diff.behav.appendFormula: Res + late d 3";
232 "--------- appendFormula: on Res + late deriv [x = 3 + -2]---///--";
233 "--------- appendFormula: on Res + late deriv [x = 3 + -2]---///--";
234 "--------- appendFormula: on Res + late deriv [x = 3 + -2]---///--";
236 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
237 ("Test", ["sqroot-test","univariate","equation","test"],
238 ["Test","squ-equ-test-subpbl1"]))];
239 Iterator 1; moveActiveRoot 1;
240 autoCalculate 1 CompleteCalcHead;
241 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
242 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);
243 appendFormula 1 "[x = 3 + -2*1]";
244 val ((pt,p),_) = get_calc 1;
245 val str = pr_ptree pr_short pt;
247 if str=". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + -1 * 2 = 0\n3. ----- pblobj -----\n3.1. -1 + x = 0\n3.2. x = 0 + -1 * -1\n4. [x = 1]\n4.1. [x = 1]\n4.2. [x = -2 + 3]\n4.3. [x = 3 + -2]\n" then ()
248 else error "inform.sml: diff.behav.appendFormula: Res + latEE 1";
249 autoCalculate 1 CompleteCalc;
250 val ((pt,p),_) = get_calc 1;
251 if "[x = 3 + -2 * 1]" = term2str (fst (get_obj g_result pt [])) then ()
252 (* ~~~~~~~~~~ simplify as last step in any script ?!*)
253 else error "inform.sml: diff.behav.appendFormula: Res + latEE 2";
257 "--------- replaceFormula: on Res + = ----------------------------";
258 "--------- replaceFormula: on Res + = ----------------------------";
259 "--------- replaceFormula: on Res + = ----------------------------";
261 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
262 ("Test", ["sqroot-test","univariate","equation","test"],
263 ["Test","squ-equ-test-subpbl1"]))];
264 Iterator 1; moveActiveRoot 1;
265 autoCalculate 1 CompleteCalcHead;
266 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
267 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);
268 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*-1 + x*);
270 replaceFormula 1 "-2 * 1 + (1 + x) = 0"; refFormula 1 (get_pos 1 1);
271 val ((pt,_),_) = get_calc 1;
272 val str = pr_ptree pr_short pt;
275 (*============ inhibit exn AK110725 ==============================================
276 (* 2nd string should be the same as 1st one *)
277 ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + -1 * 2 = 0\n2.1. x + 1 + -1 * 2 = 0\n2.2. 1 + x + -1 * 2 = 0\n2.3. 1 + (x + -1 * 2) = 0\n2.4. 1 + (x + -2) = 0\n2.5. 1 + (x + -2 * 1) = 0\n2.6. 1 + x + -2 * 1 = 0\n";
278 ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + -1 * 2 = 0\n2.1. x + 1 + -1 * 2 = 0\n2.2. -1 * 2 + (x + 1) = 0\n2.3. -1 * 2 + (1 + x) = 0\n2.4. 1 + (-1 * 2 + x) = 0\n2.5. 1 + (-2 + x) = 0\n2.6. 1 + (-2 * 1 + x) = 0\n";
279 if str = ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + -1 * 2 = 0\n2.1. x + 1 + -1 * 2 = 0\n2.2. -1 * 2 + (x + 1) = 0\n2.3. -1 * 2 + (1 + x) = 0\n2.4. 1 + (-1 * 2 + x) = 0\n2.5. 1 + (-2 + x) = 0\n2.6. 1 + (-2 * 1 + x) = 0\n" then()
280 else error "inform.sml: diff.behav.replaceFormula: on Res += 1";
281 ============ inhibit exn AK110725 ==============================================*)
283 autoCalculate 1 CompleteCalc;
284 val ((pt,pos as (p,_)),_) = get_calc 1;
285 if pos = ([],Res) andalso "[x = 1]" = (term2str o fst) (get_obj g_result pt p) then()
286 else error "inform.sml: diff.behav.replaceFormula: on Res + = 2";
289 "--------- replaceFormula: on Res + = 1st Nd ---------------------";
290 "--------- replaceFormula: on Res + = 1st Nd ---------------------";
291 "--------- replaceFormula: on Res + = 1st Nd ---------------------";
293 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
294 ("Test", ["sqroot-test","univariate","equation","test"],
295 ["Test","squ-equ-test-subpbl1"]))];
296 Iterator 1; moveActiveRoot 1;
297 autoCalculate 1 CompleteCalcHead;
298 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
299 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);
301 replaceFormula 1 "x + 1 = 4 + -2"; refFormula 1 (get_pos 1 1);
302 val ((pt,_),_) = get_calc 1;
303 val str = pr_ptree pr_short pt;
305 if str= ". ----- pblobj -----\n1. x + 1 = 2\n1.1. x + 1 = 2\n1.2. 1 + x = 2\n1.3. 1 + x = -2 + 4\n1.4. x + 1 = -2 + 4\n" then ()
306 else error "inform.sml: diff.behav.replaceFormula: on Res 1 + = 1";
307 autoCalculate 1 CompleteCalc;
308 val ((pt,pos as (p,_)),_) = get_calc 1;
309 if pos = ([],Res) andalso "[x = 1]" = (term2str o fst)(get_obj g_result pt p) then()
310 else error "inform.sml: diff.behav.replaceFormula: on Res + = 2";
313 "--------- replaceFormula: on Frm + = 1st Nd ---------------------";
314 "--------- replaceFormula: on Frm + = 1st Nd ---------------------";
315 "--------- replaceFormula: on Frm + = 1st Nd ---------------------";
317 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
318 ("Test", ["sqroot-test","univariate","equation","test"],
319 ["Test","squ-equ-test-subpbl1"]))];
320 Iterator 1; moveActiveRoot 1;
321 autoCalculate 1 CompleteCalcHead;
322 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
324 replaceFormula 1 "x + 1 = 4 + -2"; refFormula 1 (get_pos 1 1);
325 val ((pt,_),_) = get_calc 1;
326 val str = pr_ptree pr_short pt;
328 if str= ". ----- pblobj -----\n1. x + 1 = 2\n1.1. x + 1 = 2\n1.2. 1 + x = 2\n1.3. 1 + x = -2 + 4\n1.4. x + 1 = -2 + 4\n" then ()
329 else error "inform.sml: diff.behav.replaceFormula: on Frm 1 + = 1";
330 autoCalculate 1 CompleteCalc;
331 val ((pt,pos as (p,_)),_) = get_calc 1;
332 if pos = ([],Res) andalso "[x = 1]" = (term2str o fst)(get_obj g_result pt p) then()
333 else error "inform.sml: diff.behav.replaceFormula: on Frm 1 + = 2";
336 "--------- replaceFormula: cut calculation -----------------------";
337 "--------- replaceFormula: cut calculation -----------------------";
338 "--------- replaceFormula: cut calculation -----------------------";
340 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
341 ("Test", ["sqroot-test","univariate","equation","test"],
342 ["Test","squ-equ-test-subpbl1"]))];
343 Iterator 1; moveActiveRoot 1;
344 autoCalculate 1 CompleteCalc;
345 moveActiveRoot 1; moveActiveDown 1;
346 if get_pos 1 1 = ([1], Frm) then ()
347 else error "inform.sml: diff.behav. cut calculation 1";
349 replaceFormula 1 "x + 1 = 4 + -2"; refFormula 1 (get_pos 1 1);
350 val ((pt,p),_) = get_calc 1;
351 val str = pr_ptree pr_short pt;
353 if p = ([1], Res) then ()
354 else error "inform.sml: diff.behav. cut calculation 2";
357 (* 040307 copied from informtest.sml; ... old version
358 "---------------- maximum-example, UC: Modeling / modifyCalcHead -";
359 "---------------- maximum-example, UC: Modeling / modifyCalcHead -";
360 "---------------- maximum-example, UC: Modeling / modifyCalcHead -";
363 val elems = ["fixedValues [r=Arbfix]","maximum A","valuesFor [a,b]",
364 "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
365 "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
366 "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]",
367 (*^^^ these are the elements for the root-problem (in variants)*)
368 (*vvv these are elements required for subproblems*)
369 "boundVariable a","boundVariable b","boundVariable alpha",
370 "interval {x::real. 0 <= x & x <= 2*r}",
371 "interval {x::real. 0 <= x & x <= 2*r}",
372 "interval {x::real. 0 <= x & x <= pi}",
373 "errorBound (eps=(0::real))"]
374 (*specifying is not interesting for this example*)
375 val spec = ("DiffApp", ["maximum_of","function"],
376 ["DiffApp","max_by_calculus"]);
377 (*the empty model with descriptions for user-guidance by Model_Problem*)
378 val empty_model = [Given ["fixedValues []"],
379 Find ["maximum", "valuesFor"],
380 Relate ["relations []"]];
383 (*!!!!!!!!!!!!!!!!! DON'T USE me FOR FINDING nxt !!!!!!!!!!!!!!!!!!*)
384 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(elems, spec)];
385 (*val nxt = ("Model_Problem", ...*)
386 val pbl = get_obj g_pbl pt (fst p); (writeln o (itms2str_ ctxt)) pbl;
388 val (p,_,f,nxt,_,pt) = me nxt p c pt;
389 (*nxt = Add_Given "fixedValues [r = Arbfix]"*)
390 val pbl = get_obj g_pbl pt (fst p); (writeln o (itms2str_ ctxt)) pbl;
392 (0 ,[] ,false ,#Given ,Inc fixedValues [] ,(??.empty, [])),
393 (0 ,[] ,false ,#Find ,Inc maximum ,(??.empty, [])),
394 (0 ,[] ,false ,#Find ,Inc valuesFor ,(??.empty, [])),
395 (0 ,[] ,false ,#Relate ,Inc relations [] ,(??.empty, []))]*)
397 (*the empty CalcHead is checked w.r.t the model and re-established as such*)
398 val (b,pt,ocalhd) = input_icalhd pt (p,"", empty_model, Pbl, e_spec);
399 val pbl = get_obj g_pbl pt (fst p); (writeln o (itms2str_ ctxt)) pbl;
400 if ocalhd2str ocalhd = "(Pbl, ??.empty, [\n(0 ,[] ,false ,#Given ,Inc fixedValues [] ,(??.empty, [])),\n(0 ,[] ,false ,#Find ,Inc maximum ,(??.empty, [])),\n(0 ,[] ,false ,#Find ,Inc valuesFor ,(??.empty, [])),\n(0 ,[] ,false ,#Relate ,Inc relations [] ,(??.empty, []))], [], \n(\"e_domID\", [\"e_pblID\"], [\"e_metID\"]) )" then () else error "informtest.sml: diff.behav. max 1";
402 (*there is one input to the model (could be more)*)
404 input_icalhd pt (p,"", [Given ["fixedValues [r=Arbfix]"],
405 Find ["maximum", "valuesFor"],
406 Relate ["relations"]], Pbl, e_spec);
407 val pbl = get_obj g_pbl pt (fst p); (writeln o (itms2str_ ctxt)) pbl;
408 if ocalhd2str ocalhd = "(Pbl, ??.empty, [\n(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),\n(0 ,[] ,false ,#Find ,Inc maximum ,(??.empty, [])),\n(0 ,[] ,false ,#Find ,Inc valuesFor ,(??.empty, [])),\n(0 ,[] ,false ,#Relate ,Inc relations [] ,(??.empty, []))], [], \n(\"e_domID\", [\"e_pblID\"], [\"e_metID\"]) )" then ()
409 else error "informtest.sml: diff.behav. max 2";
411 (*this input is complete in variant 3, but the ME doesn't recognize FIXXXXME
412 val (b,pt''''',ocalhd) =
413 input_icalhd pt (p,"", [Given ["fixedValues [r=Arbfix]"],
414 Find ["maximum A", "valuesFor [a,b]"],
415 Relate ["relations [A=a*b, a/2=r*sin alpha, \
416 \b/2=r*cos alpha]"]], Pbl, e_spec);
417 val pbl = get_obj g_pbl pt''''' (fst p); (writeln o (itms2str_ ctxt)) pbl;
418 if ocalhd2str ocalhd = ------------^^^^^^^^^^ missing !!!*)
420 (*this input is complete in variant 1 (variant 3 does not work yet)*)
421 val (b,pt''''',ocalhd) =
422 input_icalhd pt (p,"", [Given ["fixedValues [r=Arbfix]"],
423 Find ["maximum A", "valuesFor [a,b]"],
424 Relate ["relations [A=a*b, \
425 \(a/2)^^^2 + (b/2)^^^2 = r^^^2]"]],
427 val pbl = get_obj g_pbl pt''''' (fst p); (writeln o (itms2str_ ctxt)) pbl;
429 modifycalcheadOK2xml 111 (bool2str b) ocalhd;
432 "--------- syntax error ------------------------------------------";
433 "--------- syntax error ------------------------------------------";
434 "--------- syntax error ------------------------------------------";
436 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
437 ("Test", ["sqroot-test","univariate","equation","test"],
438 ["Test","squ-equ-test-subpbl1"]))];
439 Iterator 1; moveActiveRoot 1;
440 autoCalculate 1 CompleteCalcHead;
441 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
442 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);
444 appendFormula 1 " x - "; (*<ERROR> syntax error in ' x - ' </ERROR>*)
445 val ((pt,_),_) = get_calc 1;
446 val str = pr_ptree pr_short pt;
448 if str = ". ----- pblobj -----\n1. x + 1 = 2\n" then ()
449 else error "inform.sml: diff.behav.appendFormula: syntax error";
452 "--------- CAS-command on ([],Pbl) -------------------------------";
453 "--------- CAS-command on ([],Pbl) -------------------------------";
454 "--------- CAS-command on ([],Pbl) -------------------------------";
455 val (p,_,f,nxt,_,pt) =
456 CalcTreeTEST [([], ("e_domID", ["e_pblID"], ["e_metID"]))];
457 val ifo = "solve(x+1=2,x)";
458 val (_,(_,c,(pt,p))) = inform ([],[],(pt,p)) "solve(x+1=2,x)";
460 val nxt = ("Apply_Method",Apply_Method ["Test","squ-equ-test-subpbl1"]);
461 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
462 if p = ([1], Frm) andalso f2str f = "x + 1 = 2" then ()
463 else error "inform.sml: diff.behav. CAScmd ([],Pbl)";
466 "--------- CAS-command on ([],Pbl) FE-interface ------------------";
467 "--------- CAS-command on ([],Pbl) FE-interface ------------------";
468 "--------- CAS-command on ([],Pbl) FE-interface ------------------";
470 CalcTree [([], ("e_domID", ["e_pblID"], ["e_metID"]))];
473 replaceFormula 1 "solve(x+1=2,x)";
474 autoCalculate 1 CompleteCalc;
475 val ((pt,p),_) = get_calc 1;
477 if p = ([], Res) then ()
478 else error "inform.sml: diff.behav. CAScmd ([],Pbl) FE-interface";
481 "--------- inform [rational,simplification] ----------------------";
482 "--------- inform [rational,simplification] ----------------------";
483 "--------- inform [rational,simplification] ----------------------";
485 CalcTree [(["Term (4/x - 3/y - 1)", "normalform N"],
486 ("Rational",["rational","simplification"],
487 ["simplification","of_rationals"]))];
488 Iterator 1; moveActiveRoot 1;
489 autoCalculate 1 CompleteCalcHead;
490 autoCalculate 1 (Step 1);
491 autoCalculate 1 (Step 1);
492 autoCalculate 1 (Step 1);
493 autoCalculate 1 (Step 1);
494 "--- input the next formula that _should_ be presented by mat-engine";
495 appendFormula 1 "(4 * y + -3 * x) / (x * y) + -1";
496 val ((pt,p),_) = get_calc 1;
497 if p = ([4], Res) andalso (length o children o (get_nd pt)) (fst p) = 2 then ()
498 else error ("inform.sml: [rational,simplification] 1");
500 "--- input the next formula that would be presented by mat-engine";
501 (*autoCalculate 1 (Step 1);*)
502 appendFormula 1 "(4 * y + -3 * x + -1 * (x * y)) / (x * y)";
503 val ((pt,p),_) = get_calc 1;
504 if p = ([5], Res) andalso (length o children o (get_nd pt)) (fst p) = 0 then ()
505 else error ("inform.sml: [rational,simplification] 2");
507 "--- input the exact final result";(*TODO: Exception- LIST "last_elem" raised*)
508 appendFormula 1 "(-3 * x + 4 * y + -1 * x * y) / (x * y)";
509 val ((pt,p),_) = get_calc 1;
510 if p = ([6], Res) andalso (length o children o (get_nd pt)) (fst p) = 2 then ()
511 else error ("inform.sml: [rational,simplification] 3");
514 "--------- Take as 1st tac, start with <NEW> (CAS input) ---------";
515 "--------- Take as 1st tac, start with <NEW> (CAS input) ---------";
516 "--------- Take as 1st tac, start with <NEW> (CAS input) ---------";
517 val t = str2term "Diff (x^^^2 + x + 1, x)";
518 case t of Const ("Diff.Diff", _) $ _ => ()
520 error "diff.sml behav.changed for CAS Diff (..., x)";
522 "-----------------------------------------------------------------";
524 (*2>*)CalcTree [([], ("e_domID", ["e_pblID"], ["e_metID"]))];
525 (*3>*)Iterator 1;moveActiveRoot 1;
526 "----- here the Headline has been finished";
527 (*4>*)moveActiveFormula 1 ([],Pbl);
528 (*5>*)replaceFormula 1 "Diff (x^2 + x + 1, x)";
529 val ((pt,_),_) = get_calc 1;
530 val PblObj {probl, meth, spec, fmz, env, loc, ...} = get_obj I pt [];
532 val (SOME istate, NONE) = loc;
534 writeln"-----------------------------------------------------------";
536 writeln (itms2str_ ctxt probl);
537 writeln (itms2str_ ctxt meth);
539 (*============ inhibit exn AK110725 ==============================================
540 (* ERROR: Argument: istate : istate * Proof.context Reason:
541 Can't unify istate to istate * Proof.context *)
542 writeln (istate2str istate);
543 ============ inhibit exn AK110725 ==============================================*)
547 refFormula 1 ([],Pbl) (*--> correct CalcHead*);
548 (*081016 NOT necessary (but leave it in Java):*)
549 (*6>*)(*completeCalcHead*)autoCalculate 1 CompleteCalcHead;
550 "----- here the CalcHead has been completed --- ONCE MORE ?????";
552 (***difference II***)
553 val ((pt,p),_) = get_calc 1;
554 (*val p = ([], Pbl)*)
555 val PblObj {probl, meth, spec, fmz, env, loc, ...} = get_obj I pt [];
557 val (SOME istate, NONE) = loc;
558 (*============ inhibit exn AK110725 ==============================================
559 (* ERROR: Argument: istate : istate * Proof.context Reason: Can't unify istate to istate * Proof.context *)
560 print_depth 5; writeln (istate2str istate); print_depth 3;
561 ============ inhibit exn AK110725 ==============================================*)
564 ??.empty, Sundef, false)*)
565 print_depth 5; spec; print_depth 3;
567 ["derivative_of", "function"],
568 ["diff", "differentiate_on_R"]) : spec*)
569 writeln (itms2str_ ctxt probl);
571 (1 ,[1] ,true ,#Given ,Cor functionTerm (x ^^^ 2 + x + 1) ,(f_, [x ^^^ 2 + x + 1])),
572 (2 ,[1] ,true ,#Given ,Cor differentiateFor x ,(v_, [x])),
573 (3 ,[1] ,true ,#Find ,Cor derivative f_'_f ,(f_'_f, [f_'_f]))]*)
574 writeln (itms2str_ ctxt meth);
576 (1 ,[1] ,true ,#Given ,Cor functionTerm (x ^^^ 2 + x + 1) ,(f_, [x ^^^ 2 + x + 1])),
577 (2 ,[1] ,true ,#Given ,Cor differentiateFor x ,(v_, [x])),
578 (3 ,[1] ,true ,#Find ,Cor derivative f_'_f ,(f_'_f, [f_'_f]))]*)
579 writeln"-----------------------------------------------------------";
580 (*7>*)fetchProposedTactic 1 (*--> Apply_Method*);
581 (*WN081028 fixed <ERROR> helpless </ERROR> by inform returning ...(.,Met)*)
582 autoCalculate 1 CompleteCalc;
583 val ((pt,p),_) = get_calc 1;
584 val Form res = (#1 o pt_extract) (pt, ([],Res));
586 if p = ([], Res) andalso term2str res = "1 + 2 * x" then ()
587 else error "diff.sml behav.changed for Diff (x^2 + x + 1, x)";
590 "--------- Take as 1st tac, start from exp -----------------------";
591 "--------- Take as 1st tac, start from exp -----------------------";
592 "--------- Take as 1st tac, start from exp -----------------------";
593 (*the following input is copied from BridgeLog Java <==> SML,
594 omitting unnecessary inputs*)
596 (*2>*)CalcTree [(["functionTerm (x^2 + x + 1)", "differentiateFor x", "derivative f_'_f"],("Isac",["derivative_of","function"],["diff","differentiate_on_R"]))];
597 (*3>*)Iterator 1; moveActiveRoot 1;
599 (*6>*)(*completeCalcHead*)autoCalculate 1 CompleteCalcHead;
600 (***difference II***)
601 val ((pt,_),_) = get_calc 1;
602 val PblObj {probl, meth, spec, fmz, env, loc, ...} = get_obj I pt [];
604 val (SOME istate, NONE) = loc;
605 (*============ inhibit exn AK110725 ==============================================
606 (* ERROR: Argument: istate : istate * Proof.context Reason: Can't unify istate to istate * Proof.context *)
607 print_depth 5; writeln (istate2str istate); print_depth 3;
608 ============ inhibit exn AK110725 ==============================================*)
611 ??.empty, Sundef, false)*)
612 print_depth 5; spec; print_depth 3;
614 ["derivative_of", "function"],
615 ["diff", "differentiate_on_R"]) : spec*)
616 writeln (itms2str_ ctxt probl);
618 (1 ,[1] ,true ,#Given ,Cor functionTerm (x ^^^ 2 + x + 1) ,(f_, [x ^^^ 2 + x + 1])),
619 (2 ,[1] ,true ,#Given ,Cor differentiateFor x ,(v_, [x])),
620 (3 ,[1] ,true ,#Find ,Cor derivative f_'_f ,(f_'_f, [f_'_f]))]*)
621 writeln (itms2str_ ctxt meth);
623 (1 ,[1] ,true ,#Given ,Cor functionTerm (x ^^^ 2 + x + 1) ,(f_, [x ^^^ 2 + x + 1])),
624 (2 ,[1] ,true ,#Given ,Cor differentiateFor x ,(v_, [x])),
625 (3 ,[1] ,true ,#Find ,Cor derivative f_'_f ,(f_'_f, [f_'_f]))]*)
626 writeln"-----------------------------------------------------------";
627 (*7>*)fetchProposedTactic 1 (*--> Apply_Method*);
628 autoCalculate 1 (Step 1);
629 val ((pt,p),_) = get_calc 1;
630 val Form res = (#1 o pt_extract) (pt, p);
631 if term2str res = "d_d x (x ^^^ 2 + x + 1)" then ()
632 else error "diff.sml Diff (x^2 + x + 1, x) from exp";
635 "--------- init_form, start with <NEW> (CAS input) ---------------";
636 "--------- init_form, start with <NEW> (CAS input) ---------------";
637 "--------- init_form, start with <NEW> (CAS input) ---------------";
639 CalcTree [([], ("e_domID", ["e_pblID"], ["e_metID"]))];
640 (*[[from sml: > @@@@@begin@@@@@
642 [[from sml: <CALCTREE>
643 [[from sml: <CALCID> 1 </CALCID>
644 [[from sml: </CALCTREE>
645 [[from sml: @@@@@end@@@@@*)
647 (*[[from sml: > @@@@@begin@@@@@
649 [[from sml: <ADDUSER>
650 [[from sml: <CALCID> 1 </CALCID>
651 [[from sml: <USERID> 1 </USERID>
652 [[from sml: </ADDUSER>
653 [[from sml: @@@@@end@@@@@*)
655 (*[[from sml: > @@@@@begin@@@@@
657 [[from sml: <CALCITERATOR>
658 [[from sml: <CALCID> 1 </CALCID>
659 [[from sml: <POSITION>
660 [[from sml: <INTLIST>
661 [[from sml: </INTLIST>
662 [[from sml: <POS> Pbl </POS>
663 [[from sml: </POSITION>
664 [[from sml: </CALCITERATOR>
665 [[from sml: @@@@@end@@@@@*)
666 getFormulaeFromTo 1 ([],Pbl) ([],Pbl) 0 false;
667 (*[[from sml: > @@@@@begin@@@@@ STILL CORRECT
669 [[from sml: <GETELEMENTSFROMTO>
670 [[from sml: <CALCID> 1 </CALCID>
671 [[from sml: <FORMHEADS>
672 [[from sml: <CALCFORMULA>
673 [[from sml: <POSITION>
674 [[from sml: <INTLIST>
675 [[from sml: </INTLIST>
676 [[from sml: <POS> Pbl </POS>
677 [[from sml: </POSITION>
678 [[from sml: <FORMULA>
680 [[from sml: <ISA> ________________________________________________ </ISA>
681 [[from sml: </MATHML>
683 [[from sml: </FORMULA>
684 [[from sml: </CALCFORMULA>
685 [[from sml: </FORMHEADS>
686 [[from sml: </GETELEMENTSFROMTO>
687 [[from sml: @@@@@end@@@@@*)
688 refFormula 1 ([],Pbl);
689 (*[[from sml: > @@@@@begin@@@@@ STILL CORRECT
691 [[from sml: <REFFORMULA>
692 [[from sml: <CALCID> 1 </CALCID>
693 [[from sml: <CALCHEAD status = "incorrect">
694 [[from sml: <POSITION>
695 [[from sml: <INTLIST>
696 [[from sml: </INTLIST>
697 [[from sml: <POS> Pbl </POS>
698 [[from sml: </POSITION>
701 [[from sml: <ISA> Problem (e_domID, [e_pblID]) </ISA>
702 [[from sml: </MATHML>
705 [[from sml: <GIVEN> </GIVEN>
706 [[from sml: <WHERE> </WHERE>
707 [[from sml: <FIND> </FIND>
708 [[from sml: <RELATE> </RELATE>
710 [[from sml: <BELONGSTO> Pbl </BELONGSTO>
711 [[from sml: <SPECIFICATION>
712 [[from sml: <THEORYID> e_domID </THEORYID>
713 [[from sml: <PROBLEMID>
714 [[from sml: <STRINGLIST>
715 [[from sml: <STRING> e_pblID </STRING>
716 [[from sml: </STRINGLIST>
717 [[from sml: </PROBLEMID>
718 [[from sml: <METHODID>
719 [[from sml: <STRINGLIST>
720 [[from sml: <STRING> e_metID </STRING>
721 [[from sml: </STRINGLIST>
722 [[from sml: </METHODID>
723 [[from sml: </SPECIFICATION>
724 [[from sml: </CALCHEAD>
725 [[from sml: </REFFORMULA>
726 [[from sml: @@@@@end@@@@@*)
727 moveActiveFormula 1 ([],Pbl);
728 (*[[from sml: > @@@@@begin@@@@@
730 [[from sml: <CALCITERATOR>
731 [[from sml: <CALCID> 1 </CALCID>
732 [[from sml: <POSITION>
733 [[from sml: <INTLIST>
734 [[from sml: </INTLIST>
735 [[from sml: <POS> Pbl </POS>
736 [[from sml: </POSITION>
737 [[from sml: </CALCITERATOR>
738 [[from sml: @@@@@end@@@@@*)
739 replaceFormula 1 "Simplify (1+2)";
740 (*[[from sml: > @@@@@begin@@@@@
742 [[from sml: <REPLACEFORMULA>
743 [[from sml: <CALCID> 1 </CALCID>
744 [[from sml: <CALCCHANGED>
745 [[from sml: <UNCHANGED>
746 [[from sml: <INTLIST>
747 [[from sml: </INTLIST>
748 [[from sml: <POS> Pbl </POS>
749 [[from sml: </UNCHANGED>
750 [[from sml: <DELETED>
751 [[from sml: <INTLIST>
752 [[from sml: </INTLIST>
753 [[from sml: <POS> Pbl </POS>
754 [[from sml: </DELETED>
755 [[from sml: <GENERATED>
756 [[from sml: <INTLIST>
757 [[from sml: </INTLIST>
758 [[from sml: <POS> Met </POS> DIFFERENCE: Pbl
759 [[from sml: </GENERATED>
760 [[from sml: </CALCCHANGED>
761 [[from sml: </REPLACEFORMULA>
762 [[from sml: @@@@@end@@@@@*)
763 getFormulaeFromTo 1 ([],Pbl) ([],Pbl) 0 false(* DIFFERENCE: Pbl*);
777 <ISA> Simplify (1 + 2) </ISA> WORKS !!!!!
784 getFormulaeFromTo 1 ([],Pbl) ([],Met) 0 false;
785 (*[[from sml: > @@@@@begin@@@@@
787 [[from sml: <SYSERROR>
788 [[from sml: <CALCID> 1 </CALCID>
789 [[from sml: <ERROR> error in getFormulaeFromTo </ERROR>
790 [[from sml: </SYSERROR>
791 [[from sml: @@@@@end@@@@@*)
792 (*step into getFormulaeFromTo --- bug corrected...*)
794 "--------- build fun check_err_patt ------------------------------";
795 "--------- build fun check_err_patt ------------------------------";
796 "--------- build fun check_err_patt ------------------------------";
797 val subst = [(str2term "bdv", str2term "x")]: subst;
798 val rls = norm_Rational
799 val pat = parse_patt @{theory} "(?a + ?b)/(?b + ?c) = ?a / ?c";
800 val (res, inf) = (str2term "(2 + 3)/(3 + 4)", str2term "2 / 4");
801 val (res, inf) = (str2term "(2 + 3)/(3 + 4)", str2term "1 / 2");
803 val (res', _, _, rewritten) = (*rewritten: the lhs of the pattern matches in res*)
804 rew_sub thy 1 [] e_rew_ord e_rls false [] (Trueprop $ pat) res;
805 if rewritten then NONE else SOME "e_errpatID";
807 val norm_res = case rewrite_set_ (Isac()) false rls res' of
809 | SOME (norm_res, _) => norm_res
811 val norm_inf = case rewrite_set_ (Isac()) false rls inf of
813 | SOME (norm_inf, _) => norm_inf;
818 val pat = parse_patt @{theory} "(?a + ?b)/?a = ?b";
819 val (res, inf) = (str2term "(2 + 3)/2", str2term "3");
820 if check_err_patt (res, inf) subst ("errpatID", pat) rls = SOME "errpatID"
821 then () else error "error patt example1 changed";
823 val pat = parse_patt @{theory} "(?a + ?b)/(?a + ?c) = ?b / ?c";
824 val (res, inf) = (str2term "(2 + 3)/(2 + 4)", str2term "3 / 4");
825 if check_err_patt (res, inf) subst ("errpatID", pat) rls = SOME "errpatID"
826 then () else error "error patt example2 changed";
828 val pat = parse_patt @{theory} "(?a + ?b)/(?b + ?c) = ?a / ?c";
829 val (res, inf) = (str2term "(2 + 3)/(3 + 4)", str2term "2 / 4");
830 if check_err_patt (res, inf) subst ("errpatID", pat) rls = SOME "errpatID"
831 then () else error "error patt example3 changed";
833 val inf = str2term "1 / 2";
834 if check_err_patt (res, inf) subst ("errpatID", pat) rls = SOME "errpatID"
835 then () else error "error patt example3 changed";
837 "--------- build fun check_err_patt ?bdv -------------------------";
838 "--------- build fun check_err_patt ?bdv -------------------------";
839 "--------- build fun check_err_patt ?bdv -------------------------";
840 val subst = [(str2term "bdv", str2term "x")]: subst;
841 val t = str2term "d_d x (x ^^^ 2 + sin (x ^^^ 4))";
842 val SOME (t, _) = rewrite_set_inst_ thy false subst norm_diff t;
843 if term2str t = "2 * x + cos (x ^^^ 4) * 4 * x ^^^ 3" then ()
844 else error "build fun check_err_patt ?bdv changed 1";
847 val pat = parse_patt @{theory} "d_d ?bdv (sin ?u) = cos (d_d ?bdv ?u)";
848 val (res, inf) = (str2term "2 * x + d_d x (sin (x ^^^ 4))", str2term "2 * x + cos (4 * x ^^^ 3)");
850 val (res', _, _, rewritten) = (*rewritten: the lhs of the pattern matches in res*)
851 rew_sub thy 1 subst e_rew_ord e_rls false [] (Trueprop $ pat) res;
852 if term2str res' = "2 * x + cos (d_d x (x ^^^ 4))" andalso rewritten then ()
853 else error "build fun check_err_patt ?bdv changed 2";
855 val norm_res = case rewrite_set_inst_ (Isac()) false subst rls res' of
857 | SOME (norm_res, _) => norm_res;
858 if term2str norm_res = "2 * x + cos (4 * x ^^^ 3)" then ()
859 else error "build fun check_err_patt ?bdv changed 3";
861 val norm_inf = case rewrite_set_inst_ (Isac()) false subst rls inf of
863 | SOME (norm_inf, _) => norm_inf;
864 if term2str norm_inf = "2 * x + cos (4 * x ^^^ 3)" then ()
865 else error "build fun check_err_patt ?bdv changed 4";
868 if norm_res = norm_inf then ()
869 else error "build fun check_err_patt ?bdv changed 5";
871 if check_err_patt (res, inf) (subst: subst) ("errpatID": errpatID, pat) rls = SOME "errpatID"
872 then () else error "error patt example1 changed";
874 "--------- build fun check_error_patterns ------------------------";
875 "--------- build fun check_error_patterns ------------------------";
876 "--------- build fun check_error_patterns ------------------------";
878 (str2term "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))",
879 str2term "d_d x (x ^^^ 2) + cos (4 * x ^^^ 3)");
880 val {errpats, nrls = rls, scr = Script prog, ...} = get_met ["diff", "differentiate_on_R"]
882 val env = [(str2term "v_v", str2term "x")];
884 [e_errpat, (*generalised for testing*)
885 ("chain-rule-diff-both",
886 [parse_patt @{theory} "d_d ?bdv (sin ?u) = cos (d_d ?bdv ?u)",
887 parse_patt @{theory} "d_d ?bdv (cos ?u) = - sin (d_d ?bdv ?u)",
888 parse_patt @{theory} "d_d ?bdv (?u ^^^ ?n) = ?n * ?u ^^^ (?n - 1)",
889 parse_patt @{theory} "d_d ?bdv (LogExp.ln ?u) = 1 / ?u",
890 parse_patt @{theory} "d_d ?bdv (LogExp.ln ?u) = 1 / d_d ?bdv ?u"],
891 [@{thm diff_sin_chain}, @{thm diff_cos_chain}, @{thm diff_pow_chain},
892 @{thm diff_ln_chain}, @{thm diff_exp_chain}])]: errpat list;
894 case check_error_patterns (res, inf) (prog, env) (errpats, rls) of SOME _ => ()
895 | NONE => error "check_error_patterns broken";
898 "--------- embed fun check_error_patterns ------------------------";
899 "--------- embed fun check_error_patterns ------------------------";
900 "--------- embed fun check_error_patterns ------------------------";
903 [(["functionTerm (x ^ 2 + sin (x ^ 4))", "differentiateFor x", "derivative f_f'"],
904 ("Isac", ["derivative_of","function"], ["diff","differentiate_on_R"]))];
907 autoCalculate 1 CompleteCalcHead;
908 autoCalculate 1 (Step 1);
909 autoCalculate 1 (Step 1);(*([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))*)
910 (*autoCalculate 1 (Step 1);([2], Res), d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4)*)
912 "~~~~~ fun appendFormula, args:"; val (cI, (ifo:cterm')) = (1, "d_d x (x ^ 2) + cos (4 * x ^ 3)");
914 val pos as (_,p_) = get_pos cI 1; (*pos = ([1], Res)*)
919 val (_, _, (pt, ([2], Res))) = cs';
921 [(([], Frm), Diff (x ^^^ 2 + sin (x ^^^ 4), x)),
922 (([1], Frm), d_d x (x ^^^ 2 + sin (x ^^^ 4))),
923 (([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))), <<=== input follos: "...+ cos(4.x^3)"
924 (([2], Res), d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4))] *)
926 "~~~~~ fun inform, args:"; val ((cs as (_, _, ptp as (pt, pos as (p, p_))): calcstate'), istr) =
928 val SOME f_in = parse (assoc_thy "Isac") istr
929 val f_in = term_of f_in
930 val pos_pred = lev_back' pos
931 (* f_pred ---"step pos cs"---> f_succ in appendFormula
932 TODO.WN120517: one starting point for redesign of pos' *)
933 val (f_pred, f_succ) = (get_pred_formula (pt, pos_pred), get_pred_formula (pt, pos));
935 term2str f_pred = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))";
936 term2str f_succ = "d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4)";
938 f_succ = f_in; (* = false*)
939 cas_input f_in; (* = NONE*)
940 val msg_calcstate' = compare_step ([], [], (pt, pos_pred)) f_in
941 val ("no derivation found", calcstate') = msg_calcstate';
942 val pp = par_pblobj pt p
943 val {errpats, nrls, scr = Script prog, ...} = get_met (get_obj g_metID pt pp)
944 val ScrState (env, _, _, _, _, _) = get_istate pt pos;
945 case check_error_patterns (f_pred, f_in) (prog, env) (errpats, nrls) of
946 SOME errpatID => ("error pattern #" ^ errpatID ^ "#", calcstate')
947 | NONE => msg_calcstate';
949 "~~~~~ from inform return val:"; val () = ();
950 case check_error_patterns (f_pred, f_in) (prog, env) (errpats, nrls) of
952 | NONE => error "check_error_patterns broken";
955 case inform cs' (encode ifo) of
956 ("error pattern #chain-rule-diff-both#", calcstate') => ()
957 | _ => error "inform with (positive) check_error_patterns broken"