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 "-----------------------------------------------------------------";
37 "-----------------------------------------------------------------";
38 "-----------------------------------------------------------------";
45 "--------- appendFormula: on Res + equ_nrls ----------------------";
46 "--------- appendFormula: on Res + equ_nrls ----------------------";
47 "--------- appendFormula: on Res + equ_nrls ----------------------";
49 val Script sc = (#scr o get_met) ["Test","squ-equ-test-subpbl1"];
50 (writeln o term2str) sc;
51 val Script sc = (#scr o get_met) ["Test","solve_linear"];
52 (writeln o term2str) sc;
55 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
56 ("Test", ["sqroot-test","univariate","equation","test"],
57 ["Test","squ-equ-test-subpbl1"]))];
58 Iterator 1; moveActiveRoot 1;
59 autoCalculate 1 CompleteCalcHead;
60 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
61 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);
63 appendFormula 1 "-2 * 1 + (1 + x) = 0"; refFormula 1 (get_pos 1 1);
64 val ((pt,_),_) = get_calc 1;
65 val str = pr_ptree pr_short pt;
68 (*============ inhibit exn AK110726 ==============================================
69 (* 2nd string should be the same as 1st one *)
70 ". ----- 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";
71 ". ----- 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";
72 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 ()
73 else error "inform.sml: diff.behav.appendFormula: on Res + equ 1";
74 ============ inhibit exn AK110726 ==============================================*)
76 moveDown 1 ([ ],Pbl); refFormula 1 ([1],Frm); (*x + 1 = 2*)
77 moveDown 1 ([1],Frm); refFormula 1 ([1],Res); (*x + 1 + -1 * 2 = 0*)
79 (*the seven steps of detailed derivation*)
80 moveDown 1 ([1 ],Res); refFormula 1 ([2,1],Frm);
81 moveDown 1 ([2,1],Frm); refFormula 1 ([2,1],Res);
82 moveDown 1 ([2,1],Res); refFormula 1 ([2,2],Res);
83 moveDown 1 ([2,2],Res); refFormula 1 ([2,3],Res);
84 moveDown 1 ([2,3],Res); refFormula 1 ([2,4],Res);
85 moveDown 1 ([2,4],Res); refFormula 1 ([2,5],Res);
86 moveDown 1 ([2,5],Res); refFormula 1 ([2,6],Res);
87 val ((pt,_),_) = get_calc 1;
88 if "-2 * 1 + (1 + x) = 0" = term2str (fst (get_obj g_result pt [2,6])) then()
89 else error "inform.sml: diff.behav.appendFormula: on Res + equ 2";
91 fetchProposedTactic 1; (*takes Iterator 1 _1_*)
93 (*============ inhibit exn AK110725 ==============================================
94 (* ERROR: exception Bind raised *)
95 val (_,(tac,_,_)::_) = get_calc 1;
96 if tac = Rewrite_Set "Test_simplify" then ()
97 else error "inform.sml: diff.behav.appendFormula: on Res + equ 3";
98 ============ inhibit exn AK110725 ==============================================*)
100 autoCalculate 1 CompleteCalc;
101 val ((pt,_),_) = get_calc 1;
102 if "[x = 1]" = term2str (fst (get_obj g_result pt [])) then ()
103 else error "inform.sml: diff.behav.appendFormula: on Res + equ 4";
104 (* autoCalculate 1 CompleteCalc;
105 val ((pt,p),_) = get_calc 1;
106 (writeln o istates2str) (get_obj g_loc pt [ ]);
107 (writeln o istates2str) (get_obj g_loc pt [1]);
108 (writeln o istates2str) (get_obj g_loc pt [2]);
109 (writeln o istates2str) (get_obj g_loc pt [3]);
110 (writeln o istates2str) (get_obj g_loc pt [3,1]);
111 (writeln o istates2str) (get_obj g_loc pt [3,2]);
112 (writeln o istates2str) (get_obj g_loc pt [4]);
115 "----------------------------------------------------------";
117 val fod = make_deriv (@{theory "Isac"}) Atools_erls
118 ((#rules o rep_rls) Test_simplify)
119 (sqrt_right false (@{theory "Pure"})) NONE
120 (str2term "x + 1 + -1 * 2 = 0");
121 (writeln o trtas2str) fod;
123 val ifod = make_deriv (@{theory "Isac"}) Atools_erls
124 ((#rules o rep_rls) Test_simplify)
125 (sqrt_right false (@{theory "Pure"})) NONE
126 (str2term "-2 * 1 + (1 + x) = 0");
127 (writeln o trtas2str) ifod;
128 fun equal (_,_,(t1, _)) (_,_,(t2, _)) = t1 = t2;
129 val (fod', rifod') = dropwhile' equal (rev fod) (rev ifod);
130 val der = fod' @ (map rev_deriv' rifod');
131 (writeln o trtas2str) der;
132 "----------------------------------------------------------";
135 "--------- appendFormula: on Frm + equ_nrls ----------------------";
136 "--------- appendFormula: on Frm + equ_nrls ----------------------";
137 "--------- appendFormula: on Frm + equ_nrls ----------------------";
139 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
140 ("Test", ["sqroot-test","univariate","equation","test"],
141 ["Test","squ-equ-test-subpbl1"]))];
142 Iterator 1; moveActiveRoot 1;
143 autoCalculate 1 CompleteCalcHead;
144 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1) (*x + 1 = 2*);
145 appendFormula 1 "2+ -1 + x = 2"; refFormula 1 (get_pos 1 1);
147 moveDown 1 ([],Pbl); refFormula 1 ([1],Frm) (*x + 1 = 2*);
149 moveDown 1 ([1 ],Frm); refFormula 1 ([1,1],Frm);
150 moveDown 1 ([1,1],Frm); refFormula 1 ([1,1],Res);
151 moveDown 1 ([1,1],Res); refFormula 1 ([1,2],Res);
152 moveDown 1 ([1,2],Res); refFormula 1 ([1,3],Res);
153 moveDown 1 ([1,3],Res); refFormula 1 ([1,4],Res);
154 moveDown 1 ([1,4],Res); refFormula 1 ([1,5],Res);
155 moveDown 1 ([1,5],Res); refFormula 1 ([1,6],Res);
156 val ((pt,_),_) = get_calc 1;
157 if "2 + -1 + x = 2" = term2str (fst (get_obj g_result pt [1,6])) then()
158 else error "inform.sml: diff.behav.appendFormula: on Frm + equ 1";
160 fetchProposedTactic 1; (*takes Iterator 1 _1_*)
161 val (_,(tac,_,_)::_) = get_calc 1;
162 if tac = Rewrite_Set "norm_equation" then ()
163 else error "inform.sml: diff.behav.appendFormula: on Frm + equ 2";
164 autoCalculate 1 CompleteCalc;
165 val ((pt,_),_) = get_calc 1;
166 if "[x = 1]" = term2str (fst (get_obj g_result pt [])) then ()
167 else error "inform.sml: diff.behav.appendFormula: on Frm + equ 3";
170 "--------- appendFormula: on Res + NO deriv ----------------------";
171 "--------- appendFormula: on Res + NO deriv ----------------------";
172 "--------- appendFormula: on Res + NO deriv ----------------------";
174 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
175 ("Test", ["sqroot-test","univariate","equation","test"],
176 ["Test","squ-equ-test-subpbl1"]))];
177 Iterator 1; moveActiveRoot 1;
178 autoCalculate 1 CompleteCalcHead;
179 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
180 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);
182 appendFormula 1 "x = 2";
183 val ((pt,p),_) = get_calc 1;
184 val str = pr_ptree pr_short pt;
186 if str = ". ----- pblobj -----\n1. x + 1 = 2\n" andalso p = ([1], Res)
188 else error "inform.sml: diff.behav.appendFormula: Res + NOder 1";
190 fetchProposedTactic 1;
191 val (_,(tac,_,_)::_) = get_calc 1;
192 if tac = Rewrite_Set "Test_simplify" then ()
193 else error "inform.sml: diff.behav.appendFormula: Res + NOder 2";
194 autoCalculate 1 CompleteCalc;
195 val ((pt,_),_) = get_calc 1;
196 if "[x = 1]" = term2str (fst (get_obj g_result pt [])) then ()
197 else error "inform.sml: diff.behav.appendFormula: on Frm + equ 3";
200 "--------- appendFormula: on Res + late deriv --------------------";
201 "--------- appendFormula: on Res + late deriv --------------------";
202 "--------- appendFormula: on Res + late deriv --------------------";
204 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
205 ("Test", ["sqroot-test","univariate","equation","test"],
206 ["Test","squ-equ-test-subpbl1"]))];
207 Iterator 1; moveActiveRoot 1;
208 autoCalculate 1 CompleteCalcHead;
209 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
210 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);
212 appendFormula 1 "x = 1";
213 val ((pt,p),_) = get_calc 1;
214 val str = pr_ptree pr_short pt;
216 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)
217 then () (*finds 1 step too early: ([3,2], Res) "x = 1" also by script !!!*)
218 else error "inform.sml: diff.behav.appendFormula: Res + late d 1";
220 fetchProposedTactic 1;
221 val (_,(tac,_,_)::_) = get_calc 1;
222 if tac = Check_Postcond ["linear", "univariate", "equation", "test"] then ()
223 else error "inform.sml: diff.behav.appendFormula: Res + late d 2";
224 autoCalculate 1 CompleteCalc;
225 val ((pt,_),_) = get_calc 1;
226 if "[x = 1]" = term2str (fst (get_obj g_result pt [])) then ()
227 else error "inform.sml: diff.behav.appendFormula: Res + late d 3";
230 "--------- appendFormula: on Res + late deriv [x = 3 + -2]---///--";
231 "--------- appendFormula: on Res + late deriv [x = 3 + -2]---///--";
232 "--------- appendFormula: on Res + late deriv [x = 3 + -2]---///--";
234 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
235 ("Test", ["sqroot-test","univariate","equation","test"],
236 ["Test","squ-equ-test-subpbl1"]))];
237 Iterator 1; moveActiveRoot 1;
238 autoCalculate 1 CompleteCalcHead;
239 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
240 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);
241 appendFormula 1 "[x = 3 + -2*1]";
242 val ((pt,p),_) = get_calc 1;
243 val str = pr_ptree pr_short pt;
245 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 ()
246 else error "inform.sml: diff.behav.appendFormula: Res + latEE 1";
247 autoCalculate 1 CompleteCalc;
248 val ((pt,p),_) = get_calc 1;
249 if "[x = 3 + -2 * 1]" = term2str (fst (get_obj g_result pt [])) then ()
250 (* ~~~~~~~~~~ simplify as last step in any script ?!*)
251 else error "inform.sml: diff.behav.appendFormula: Res + latEE 2";
255 "--------- replaceFormula: on Res + = ----------------------------";
256 "--------- replaceFormula: on Res + = ----------------------------";
257 "--------- replaceFormula: on Res + = ----------------------------";
259 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
260 ("Test", ["sqroot-test","univariate","equation","test"],
261 ["Test","squ-equ-test-subpbl1"]))];
262 Iterator 1; moveActiveRoot 1;
263 autoCalculate 1 CompleteCalcHead;
264 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
265 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);
266 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*-1 + x*);
268 replaceFormula 1 "-2 * 1 + (1 + x) = 0"; refFormula 1 (get_pos 1 1);
269 val ((pt,_),_) = get_calc 1;
270 val str = pr_ptree pr_short pt;
273 (*============ inhibit exn AK110725 ==============================================
274 (* 2nd string should be the same as 1st one *)
275 ". ----- 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";
276 ". ----- 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";
277 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()
278 else error "inform.sml: diff.behav.replaceFormula: on Res += 1";
279 ============ inhibit exn AK110725 ==============================================*)
281 autoCalculate 1 CompleteCalc;
282 val ((pt,pos as (p,_)),_) = get_calc 1;
283 if pos = ([],Res) andalso "[x = 1]" = (term2str o fst) (get_obj g_result pt p) then()
284 else error "inform.sml: diff.behav.replaceFormula: on Res + = 2";
287 "--------- replaceFormula: on Res + = 1st Nd ---------------------";
288 "--------- replaceFormula: on Res + = 1st Nd ---------------------";
289 "--------- replaceFormula: on Res + = 1st Nd ---------------------";
291 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
292 ("Test", ["sqroot-test","univariate","equation","test"],
293 ["Test","squ-equ-test-subpbl1"]))];
294 Iterator 1; moveActiveRoot 1;
295 autoCalculate 1 CompleteCalcHead;
296 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
297 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);
299 replaceFormula 1 "x + 1 = 4 + -2"; refFormula 1 (get_pos 1 1);
300 val ((pt,_),_) = get_calc 1;
301 val str = pr_ptree pr_short pt;
303 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 ()
304 else error "inform.sml: diff.behav.replaceFormula: on Res 1 + = 1";
305 autoCalculate 1 CompleteCalc;
306 val ((pt,pos as (p,_)),_) = get_calc 1;
307 if pos = ([],Res) andalso "[x = 1]" = (term2str o fst)(get_obj g_result pt p) then()
308 else error "inform.sml: diff.behav.replaceFormula: on Res + = 2";
311 "--------- replaceFormula: on Frm + = 1st Nd ---------------------";
312 "--------- replaceFormula: on Frm + = 1st Nd ---------------------";
313 "--------- replaceFormula: on Frm + = 1st Nd ---------------------";
315 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
316 ("Test", ["sqroot-test","univariate","equation","test"],
317 ["Test","squ-equ-test-subpbl1"]))];
318 Iterator 1; moveActiveRoot 1;
319 autoCalculate 1 CompleteCalcHead;
320 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
322 replaceFormula 1 "x + 1 = 4 + -2"; refFormula 1 (get_pos 1 1);
323 val ((pt,_),_) = get_calc 1;
324 val str = pr_ptree pr_short pt;
326 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 ()
327 else error "inform.sml: diff.behav.replaceFormula: on Frm 1 + = 1";
328 autoCalculate 1 CompleteCalc;
329 val ((pt,pos as (p,_)),_) = get_calc 1;
330 if pos = ([],Res) andalso "[x = 1]" = (term2str o fst)(get_obj g_result pt p) then()
331 else error "inform.sml: diff.behav.replaceFormula: on Frm 1 + = 2";
334 "--------- replaceFormula: cut calculation -----------------------";
335 "--------- replaceFormula: cut calculation -----------------------";
336 "--------- replaceFormula: cut calculation -----------------------";
338 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
339 ("Test", ["sqroot-test","univariate","equation","test"],
340 ["Test","squ-equ-test-subpbl1"]))];
341 Iterator 1; moveActiveRoot 1;
342 autoCalculate 1 CompleteCalc;
343 moveActiveRoot 1; moveActiveDown 1;
344 if get_pos 1 1 = ([1], Frm) then ()
345 else error "inform.sml: diff.behav. cut calculation 1";
347 replaceFormula 1 "x + 1 = 4 + -2"; refFormula 1 (get_pos 1 1);
348 val ((pt,p),_) = get_calc 1;
349 val str = pr_ptree pr_short pt;
351 if p = ([1], Res) then ()
352 else error "inform.sml: diff.behav. cut calculation 2";
355 (* 040307 copied from informtest.sml; ... old version
356 "---------------- maximum-example, UC: Modeling / modifyCalcHead -";
357 "---------------- maximum-example, UC: Modeling / modifyCalcHead -";
358 "---------------- maximum-example, UC: Modeling / modifyCalcHead -";
361 val elems = ["fixedValues [r=Arbfix]","maximum A","valuesFor [a,b]",
362 "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
363 "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
364 "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]",
365 (*^^^ these are the elements for the root-problem (in variants)*)
366 (*vvv these are elements required for subproblems*)
367 "boundVariable a","boundVariable b","boundVariable alpha",
368 "interval {x::real. 0 <= x & x <= 2*r}",
369 "interval {x::real. 0 <= x & x <= 2*r}",
370 "interval {x::real. 0 <= x & x <= pi}",
371 "errorBound (eps=(0::real))"]
372 (*specifying is not interesting for this example*)
373 val spec = ("DiffApp", ["maximum_of","function"],
374 ["DiffApp","max_by_calculus"]);
375 (*the empty model with descriptions for user-guidance by Model_Problem*)
376 val empty_model = [Given ["fixedValues []"],
377 Find ["maximum", "valuesFor"],
378 Relate ["relations []"]];
381 (*!!!!!!!!!!!!!!!!! DON'T USE me FOR FINDING nxt !!!!!!!!!!!!!!!!!!*)
382 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(elems, spec)];
383 (*val nxt = ("Model_Problem", ...*)
384 val pbl = get_obj g_pbl pt (fst p); (writeln o (itms2str_ ctxt)) pbl;
386 val (p,_,f,nxt,_,pt) = me nxt p c pt;
387 (*nxt = Add_Given "fixedValues [r = Arbfix]"*)
388 val pbl = get_obj g_pbl pt (fst p); (writeln o (itms2str_ ctxt)) pbl;
390 (0 ,[] ,false ,#Given ,Inc fixedValues [] ,(??.empty, [])),
391 (0 ,[] ,false ,#Find ,Inc maximum ,(??.empty, [])),
392 (0 ,[] ,false ,#Find ,Inc valuesFor ,(??.empty, [])),
393 (0 ,[] ,false ,#Relate ,Inc relations [] ,(??.empty, []))]*)
395 (*the empty CalcHead is checked w.r.t the model and re-established as such*)
396 val (b,pt,ocalhd) = input_icalhd pt (p,"", empty_model, Pbl, e_spec);
397 val pbl = get_obj g_pbl pt (fst p); (writeln o (itms2str_ ctxt)) pbl;
398 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";
400 (*there is one input to the model (could be more)*)
402 input_icalhd pt (p,"", [Given ["fixedValues [r=Arbfix]"],
403 Find ["maximum", "valuesFor"],
404 Relate ["relations"]], Pbl, e_spec);
405 val pbl = get_obj g_pbl pt (fst p); (writeln o (itms2str_ ctxt)) pbl;
406 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 ()
407 else error "informtest.sml: diff.behav. max 2";
409 (*this input is complete in variant 3, but the ME doesn't recognize FIXXXXME
410 val (b,pt''''',ocalhd) =
411 input_icalhd pt (p,"", [Given ["fixedValues [r=Arbfix]"],
412 Find ["maximum A", "valuesFor [a,b]"],
413 Relate ["relations [A=a*b, a/2=r*sin alpha, \
414 \b/2=r*cos alpha]"]], Pbl, e_spec);
415 val pbl = get_obj g_pbl pt''''' (fst p); (writeln o (itms2str_ ctxt)) pbl;
416 if ocalhd2str ocalhd = ------------^^^^^^^^^^ missing !!!*)
418 (*this input is complete in variant 1 (variant 3 does not work yet)*)
419 val (b,pt''''',ocalhd) =
420 input_icalhd pt (p,"", [Given ["fixedValues [r=Arbfix]"],
421 Find ["maximum A", "valuesFor [a,b]"],
422 Relate ["relations [A=a*b, \
423 \(a/2)^^^2 + (b/2)^^^2 = r^^^2]"]],
425 val pbl = get_obj g_pbl pt''''' (fst p); (writeln o (itms2str_ ctxt)) pbl;
427 modifycalcheadOK2xml 111 (bool2str b) ocalhd;
430 "--------- syntax error ------------------------------------------";
431 "--------- syntax error ------------------------------------------";
432 "--------- syntax error ------------------------------------------";
434 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
435 ("Test", ["sqroot-test","univariate","equation","test"],
436 ["Test","squ-equ-test-subpbl1"]))];
437 Iterator 1; moveActiveRoot 1;
438 autoCalculate 1 CompleteCalcHead;
439 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
440 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);
442 appendFormula 1 " x - "; (*<ERROR> syntax error in ' x - ' </ERROR>*)
443 val ((pt,_),_) = get_calc 1;
444 val str = pr_ptree pr_short pt;
446 if str = ". ----- pblobj -----\n1. x + 1 = 2\n" then ()
447 else error "inform.sml: diff.behav.appendFormula: syntax error";
450 "--------- CAS-command on ([],Pbl) -------------------------------";
451 "--------- CAS-command on ([],Pbl) -------------------------------";
452 "--------- CAS-command on ([],Pbl) -------------------------------";
453 val (p,_,f,nxt,_,pt) =
454 CalcTreeTEST [([], ("e_domID", ["e_pblID"], ["e_metID"]))];
455 val ifo = "solve(x+1=2,x)";
456 val (_,(_,c,(pt,p))) = inform ([],[],(pt,p)) "solve(x+1=2,x)";
458 val nxt = ("Apply_Method",Apply_Method ["Test","squ-equ-test-subpbl1"]);
459 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
460 if p = ([1], Frm) andalso f2str f = "x + 1 = 2" then ()
461 else error "inform.sml: diff.behav. CAScmd ([],Pbl)";
464 "--------- CAS-command on ([],Pbl) FE-interface ------------------";
465 "--------- CAS-command on ([],Pbl) FE-interface ------------------";
466 "--------- CAS-command on ([],Pbl) FE-interface ------------------";
468 CalcTree [([], ("e_domID", ["e_pblID"], ["e_metID"]))];
471 replaceFormula 1 "solve(x+1=2,x)";
472 autoCalculate 1 CompleteCalc;
473 val ((pt,p),_) = get_calc 1;
475 if p = ([], Res) then ()
476 else error "inform.sml: diff.behav. CAScmd ([],Pbl) FE-interface";
479 "--------- inform [rational,simplification] ----------------------";
480 "--------- inform [rational,simplification] ----------------------";
481 "--------- inform [rational,simplification] ----------------------";
483 CalcTree [(["Term (4/x - 3/y - 1)", "normalform N"],
484 ("Rational",["rational","simplification"],
485 ["simplification","of_rationals"]))];
486 Iterator 1; moveActiveRoot 1;
487 autoCalculate 1 CompleteCalcHead;
488 autoCalculate 1 (Step 1);
489 autoCalculate 1 (Step 1);
490 autoCalculate 1 (Step 1);
491 autoCalculate 1 (Step 1);
492 "--- input the next formula that _should_ be presented by mat-engine";
493 appendFormula 1 "(4 * y + -3 * x) / (x * y) + -1";
494 val ((pt,p),_) = get_calc 1;
495 if p = ([4], Res) andalso (length o children o (get_nd pt)) (fst p) = 2 then ()
496 else error ("inform.sml: [rational,simplification] 1");
498 "--- input the next formula that would be presented by mat-engine";
499 (*autoCalculate 1 (Step 1);*)
500 appendFormula 1 "(4 * y + -3 * x + -1 * (x * y)) / (x * y)";
501 val ((pt,p),_) = get_calc 1;
502 if p = ([5], Res) andalso (length o children o (get_nd pt)) (fst p) = 0 then ()
503 else error ("inform.sml: [rational,simplification] 2");
505 "--- input the exact final result";(*TODO: Exception- LIST "last_elem" raised*)
506 appendFormula 1 "(-3 * x + 4 * y + -1 * x * y) / (x * y)";
507 val ((pt,p),_) = get_calc 1;
508 if p = ([6], Res) andalso (length o children o (get_nd pt)) (fst p) = 2 then ()
509 else error ("inform.sml: [rational,simplification] 3");
512 "--------- Take as 1st tac, start with <NEW> (CAS input) ---------";
513 "--------- Take as 1st tac, start with <NEW> (CAS input) ---------";
514 "--------- Take as 1st tac, start with <NEW> (CAS input) ---------";
515 val t = str2term "Diff (x^^^2 + x + 1, x)";
516 case t of Const ("Diff.Diff", _) $ _ => ()
518 error "diff.sml behav.changed for CAS Diff (..., x)";
520 "-----------------------------------------------------------------";
522 (*2>*)CalcTree [([], ("e_domID", ["e_pblID"], ["e_metID"]))];
523 (*3>*)Iterator 1;moveActiveRoot 1;
524 "----- here the Headline has been finished";
525 (*4>*)moveActiveFormula 1 ([],Pbl);
526 (*5>*)replaceFormula 1 "Diff (x^2 + x + 1, x)";
527 val ((pt,_),_) = get_calc 1;
528 val PblObj {probl, meth, spec, fmz, env, loc, ...} = get_obj I pt [];
530 val (SOME istate, NONE) = loc;
532 writeln"-----------------------------------------------------------";
534 writeln (itms2str_ ctxt probl);
535 writeln (itms2str_ ctxt meth);
537 (*============ inhibit exn AK110725 ==============================================
538 (* ERROR: Argument: istate : istate * Proof.context Reason:
539 Can't unify istate to istate * Proof.context *)
540 writeln (istate2str istate);
541 ============ inhibit exn AK110725 ==============================================*)
545 refFormula 1 ([],Pbl) (*--> correct CalcHead*);
546 (*081016 NOT necessary (but leave it in Java):*)
547 (*6>*)(*completeCalcHead*)autoCalculate 1 CompleteCalcHead;
548 "----- here the CalcHead has been completed --- ONCE MORE ?????";
550 (***difference II***)
551 val ((pt,p),_) = get_calc 1;
552 (*val p = ([], Pbl)*)
553 val PblObj {probl, meth, spec, fmz, env, loc, ...} = get_obj I pt [];
555 val (SOME istate, NONE) = loc;
556 (*============ inhibit exn AK110725 ==============================================
557 (* ERROR: Argument: istate : istate * Proof.context Reason: Can't unify istate to istate * Proof.context *)
558 print_depth 5; writeln (istate2str istate); print_depth 3;
559 ============ inhibit exn AK110725 ==============================================*)
562 ??.empty, Sundef, false)*)
563 print_depth 5; spec; print_depth 3;
565 ["derivative_of", "function"],
566 ["diff", "differentiate_on_R"]) : spec*)
567 writeln (itms2str_ ctxt probl);
569 (1 ,[1] ,true ,#Given ,Cor functionTerm (x ^^^ 2 + x + 1) ,(f_, [x ^^^ 2 + x + 1])),
570 (2 ,[1] ,true ,#Given ,Cor differentiateFor x ,(v_, [x])),
571 (3 ,[1] ,true ,#Find ,Cor derivative f_'_f ,(f_'_f, [f_'_f]))]*)
572 writeln (itms2str_ ctxt meth);
574 (1 ,[1] ,true ,#Given ,Cor functionTerm (x ^^^ 2 + x + 1) ,(f_, [x ^^^ 2 + x + 1])),
575 (2 ,[1] ,true ,#Given ,Cor differentiateFor x ,(v_, [x])),
576 (3 ,[1] ,true ,#Find ,Cor derivative f_'_f ,(f_'_f, [f_'_f]))]*)
577 writeln"-----------------------------------------------------------";
578 (*7>*)fetchProposedTactic 1 (*--> Apply_Method*);
579 (*WN081028 fixed <ERROR> helpless </ERROR> by inform returning ...(.,Met)*)
580 autoCalculate 1 CompleteCalc;
581 val ((pt,p),_) = get_calc 1;
582 val Form res = (#1 o pt_extract) (pt, ([],Res));
584 if p = ([], Res) andalso term2str res = "1 + 2 * x" then ()
585 else error "diff.sml behav.changed for Diff (x^2 + x + 1, x)";
588 "--------- Take as 1st tac, start from exp -----------------------";
589 "--------- Take as 1st tac, start from exp -----------------------";
590 "--------- Take as 1st tac, start from exp -----------------------";
591 (*the following input is copied from BridgeLog Java <==> SML,
592 omitting unnecessary inputs*)
594 (*2>*)CalcTree [(["functionTerm (x^2 + x + 1)", "differentiateFor x", "derivative f_'_f"],("Isac",["derivative_of","function"],["diff","differentiate_on_R"]))];
595 (*3>*)Iterator 1; moveActiveRoot 1;
597 (*6>*)(*completeCalcHead*)autoCalculate 1 CompleteCalcHead;
598 (***difference II***)
599 val ((pt,_),_) = get_calc 1;
600 val PblObj {probl, meth, spec, fmz, env, loc, ...} = get_obj I pt [];
602 val (SOME istate, NONE) = loc;
603 (*============ inhibit exn AK110725 ==============================================
604 (* ERROR: Argument: istate : istate * Proof.context Reason: Can't unify istate to istate * Proof.context *)
605 print_depth 5; writeln (istate2str istate); print_depth 3;
606 ============ inhibit exn AK110725 ==============================================*)
609 ??.empty, Sundef, false)*)
610 print_depth 5; spec; print_depth 3;
612 ["derivative_of", "function"],
613 ["diff", "differentiate_on_R"]) : spec*)
614 writeln (itms2str_ ctxt probl);
616 (1 ,[1] ,true ,#Given ,Cor functionTerm (x ^^^ 2 + x + 1) ,(f_, [x ^^^ 2 + x + 1])),
617 (2 ,[1] ,true ,#Given ,Cor differentiateFor x ,(v_, [x])),
618 (3 ,[1] ,true ,#Find ,Cor derivative f_'_f ,(f_'_f, [f_'_f]))]*)
619 writeln (itms2str_ ctxt meth);
621 (1 ,[1] ,true ,#Given ,Cor functionTerm (x ^^^ 2 + x + 1) ,(f_, [x ^^^ 2 + x + 1])),
622 (2 ,[1] ,true ,#Given ,Cor differentiateFor x ,(v_, [x])),
623 (3 ,[1] ,true ,#Find ,Cor derivative f_'_f ,(f_'_f, [f_'_f]))]*)
624 writeln"-----------------------------------------------------------";
625 (*7>*)fetchProposedTactic 1 (*--> Apply_Method*);
626 autoCalculate 1 (Step 1);
627 val ((pt,p),_) = get_calc 1;
628 val Form res = (#1 o pt_extract) (pt, p);
629 if term2str res = "d_d x (x ^^^ 2 + x + 1)" then ()
630 else error "diff.sml Diff (x^2 + x + 1, x) from exp";
633 "--------- init_form, start with <NEW> (CAS input) ---------------";
634 "--------- init_form, start with <NEW> (CAS input) ---------------";
635 "--------- init_form, start with <NEW> (CAS input) ---------------";
637 CalcTree [([], ("e_domID", ["e_pblID"], ["e_metID"]))];
638 (*[[from sml: > @@@@@begin@@@@@
640 [[from sml: <CALCTREE>
641 [[from sml: <CALCID> 1 </CALCID>
642 [[from sml: </CALCTREE>
643 [[from sml: @@@@@end@@@@@*)
645 (*[[from sml: > @@@@@begin@@@@@
647 [[from sml: <ADDUSER>
648 [[from sml: <CALCID> 1 </CALCID>
649 [[from sml: <USERID> 1 </USERID>
650 [[from sml: </ADDUSER>
651 [[from sml: @@@@@end@@@@@*)
653 (*[[from sml: > @@@@@begin@@@@@
655 [[from sml: <CALCITERATOR>
656 [[from sml: <CALCID> 1 </CALCID>
657 [[from sml: <POSITION>
658 [[from sml: <INTLIST>
659 [[from sml: </INTLIST>
660 [[from sml: <POS> Pbl </POS>
661 [[from sml: </POSITION>
662 [[from sml: </CALCITERATOR>
663 [[from sml: @@@@@end@@@@@*)
664 getFormulaeFromTo 1 ([],Pbl) ([],Pbl) 0 false;
665 (*[[from sml: > @@@@@begin@@@@@ STILL CORRECT
667 [[from sml: <GETELEMENTSFROMTO>
668 [[from sml: <CALCID> 1 </CALCID>
669 [[from sml: <FORMHEADS>
670 [[from sml: <CALCFORMULA>
671 [[from sml: <POSITION>
672 [[from sml: <INTLIST>
673 [[from sml: </INTLIST>
674 [[from sml: <POS> Pbl </POS>
675 [[from sml: </POSITION>
676 [[from sml: <FORMULA>
678 [[from sml: <ISA> ________________________________________________ </ISA>
679 [[from sml: </MATHML>
681 [[from sml: </FORMULA>
682 [[from sml: </CALCFORMULA>
683 [[from sml: </FORMHEADS>
684 [[from sml: </GETELEMENTSFROMTO>
685 [[from sml: @@@@@end@@@@@*)
686 refFormula 1 ([],Pbl);
687 (*[[from sml: > @@@@@begin@@@@@ STILL CORRECT
689 [[from sml: <REFFORMULA>
690 [[from sml: <CALCID> 1 </CALCID>
691 [[from sml: <CALCHEAD status = "incorrect">
692 [[from sml: <POSITION>
693 [[from sml: <INTLIST>
694 [[from sml: </INTLIST>
695 [[from sml: <POS> Pbl </POS>
696 [[from sml: </POSITION>
699 [[from sml: <ISA> Problem (e_domID, [e_pblID]) </ISA>
700 [[from sml: </MATHML>
703 [[from sml: <GIVEN> </GIVEN>
704 [[from sml: <WHERE> </WHERE>
705 [[from sml: <FIND> </FIND>
706 [[from sml: <RELATE> </RELATE>
708 [[from sml: <BELONGSTO> Pbl </BELONGSTO>
709 [[from sml: <SPECIFICATION>
710 [[from sml: <THEORYID> e_domID </THEORYID>
711 [[from sml: <PROBLEMID>
712 [[from sml: <STRINGLIST>
713 [[from sml: <STRING> e_pblID </STRING>
714 [[from sml: </STRINGLIST>
715 [[from sml: </PROBLEMID>
716 [[from sml: <METHODID>
717 [[from sml: <STRINGLIST>
718 [[from sml: <STRING> e_metID </STRING>
719 [[from sml: </STRINGLIST>
720 [[from sml: </METHODID>
721 [[from sml: </SPECIFICATION>
722 [[from sml: </CALCHEAD>
723 [[from sml: </REFFORMULA>
724 [[from sml: @@@@@end@@@@@*)
725 moveActiveFormula 1 ([],Pbl);
726 (*[[from sml: > @@@@@begin@@@@@
728 [[from sml: <CALCITERATOR>
729 [[from sml: <CALCID> 1 </CALCID>
730 [[from sml: <POSITION>
731 [[from sml: <INTLIST>
732 [[from sml: </INTLIST>
733 [[from sml: <POS> Pbl </POS>
734 [[from sml: </POSITION>
735 [[from sml: </CALCITERATOR>
736 [[from sml: @@@@@end@@@@@*)
737 replaceFormula 1 "Simplify (1+2)";
738 (*[[from sml: > @@@@@begin@@@@@
740 [[from sml: <REPLACEFORMULA>
741 [[from sml: <CALCID> 1 </CALCID>
742 [[from sml: <CALCCHANGED>
743 [[from sml: <UNCHANGED>
744 [[from sml: <INTLIST>
745 [[from sml: </INTLIST>
746 [[from sml: <POS> Pbl </POS>
747 [[from sml: </UNCHANGED>
748 [[from sml: <DELETED>
749 [[from sml: <INTLIST>
750 [[from sml: </INTLIST>
751 [[from sml: <POS> Pbl </POS>
752 [[from sml: </DELETED>
753 [[from sml: <GENERATED>
754 [[from sml: <INTLIST>
755 [[from sml: </INTLIST>
756 [[from sml: <POS> Met </POS> DIFFERENCE: Pbl
757 [[from sml: </GENERATED>
758 [[from sml: </CALCCHANGED>
759 [[from sml: </REPLACEFORMULA>
760 [[from sml: @@@@@end@@@@@*)
761 getFormulaeFromTo 1 ([],Pbl) ([],Pbl) 0 false(* DIFFERENCE: Pbl*);
775 <ISA> Simplify (1 + 2) </ISA> WORKS !!!!!
782 getFormulaeFromTo 1 ([],Pbl) ([],Met) 0 false;
783 (*[[from sml: > @@@@@begin@@@@@
785 [[from sml: <SYSERROR>
786 [[from sml: <CALCID> 1 </CALCID>
787 [[from sml: <ERROR> error in getFormulaeFromTo </ERROR>
788 [[from sml: </SYSERROR>
789 [[from sml: @@@@@end@@@@@*)
790 (*step into getFormulaeFromTo --- bug corrected...*)
792 "--------- build fun check_err_patt ------------------------------";
793 "--------- build fun check_err_patt ------------------------------";
794 "--------- build fun check_err_patt ------------------------------";
795 val subst = [(str2term "bdv", str2term "x")]: subst;
796 val rls = norm_Rational
797 val pat = parse_patt @{theory} "(?a + ?b)/(?b + ?c) = ?a / ?c";
798 val (res, inf) = (str2term "(2 + 3)/(3 + 4)", str2term "2 / 4");
799 val (res, inf) = (str2term "(2 + 3)/(3 + 4)", str2term "1 / 2");
801 val (res', _, _, rewritten) = (*rewritten: the lhs of the pattern matches in res*)
802 rew_sub thy 1 [] e_rew_ord e_rls false [] (Trueprop $ pat) res;
803 if rewritten then NONE else SOME "e_errpatID";
805 val norm_res = case rewrite_set_ (Isac()) false rls res' of
807 | SOME (norm_res, _) => norm_res
809 val norm_inf = case rewrite_set_ (Isac()) false rls inf of
811 | SOME (norm_inf, _) => norm_inf;
816 val pat = parse_patt @{theory} "(?a + ?b)/?a = ?b";
817 val (res, inf) = (str2term "(2 + 3)/2", str2term "3");
818 if check_err_patt (res, inf) subst ("errpatID", pat) rls = SOME "errpatID"
819 then () else error "error patt example1 changed";
821 val pat = parse_patt @{theory} "(?a + ?b)/(?a + ?c) = ?b / ?c";
822 val (res, inf) = (str2term "(2 + 3)/(2 + 4)", str2term "3 / 4");
823 if check_err_patt (res, inf) subst ("errpatID", pat) rls = SOME "errpatID"
824 then () else error "error patt example2 changed";
826 val pat = parse_patt @{theory} "(?a + ?b)/(?b + ?c) = ?a / ?c";
827 val (res, inf) = (str2term "(2 + 3)/(3 + 4)", str2term "2 / 4");
828 if check_err_patt (res, inf) subst ("errpatID", pat) rls = SOME "errpatID"
829 then () else error "error patt example3 changed";
831 val inf = str2term "1 / 2";
832 if check_err_patt (res, inf) subst ("errpatID", pat) rls = SOME "errpatID"
833 then () else error "error patt example3 changed";
835 "--------- build fun check_err_patt ?bdv -------------------------";
836 "--------- build fun check_err_patt ?bdv -------------------------";
837 "--------- build fun check_err_patt ?bdv -------------------------";
838 val subst = [(str2term "bdv", str2term "x")]: subst;
839 val t = str2term "d_d x (x ^^^ 2 + sin (x ^^^ 4))";
840 val SOME (t, _) = rewrite_set_inst_ thy false subst norm_diff t;
841 if term2str t = "2 * x + cos (x ^^^ 4) * 4 * x ^^^ 3" then ()
842 else error "build fun check_err_patt ?bdv changed 1";
845 val pat = parse_patt @{theory} "d_d ?bdv (sin ?u) = cos (d_d ?bdv ?u)";
846 val (res, inf) = (str2term "2 * x + d_d x (sin (x ^^^ 4))", str2term "2 * x + cos (4 * x ^^^ 3)");
848 val (res', _, _, rewritten) = (*rewritten: the lhs of the pattern matches in res*)
849 rew_sub thy 1 subst e_rew_ord e_rls false [] (Trueprop $ pat) res;
850 if term2str res' = "2 * x + cos (d_d x (x ^^^ 4))" andalso rewritten then ()
851 else error "build fun check_err_patt ?bdv changed 2";
853 val norm_res = case rewrite_set_inst_ (Isac()) false subst rls res' of
855 | SOME (norm_res, _) => norm_res;
856 if term2str norm_res = "2 * x + cos (4 * x ^^^ 3)" then ()
857 else error "build fun check_err_patt ?bdv changed 3";
859 val norm_inf = case rewrite_set_inst_ (Isac()) false subst rls inf of
861 | SOME (norm_inf, _) => norm_inf;
862 if term2str norm_inf = "2 * x + cos (4 * x ^^^ 3)" then ()
863 else error "build fun check_err_patt ?bdv changed 4";
866 if norm_res = norm_inf then ()
867 else error "build fun check_err_patt ?bdv changed 5";
869 if check_err_patt (res, inf) (subst: subst) ("errpatID": errpatID, pat) rls = SOME "errpatID"
870 then () else error "error patt example1 changed";