4 (c) due to copyright terms
6 use"../smltest/ME/me.sml";
10 "-----------------------------------------------------------------";
11 "table of contents -----------------------------------------------";
12 "-----------------------------------------------------------------";
13 "=====new ptree 1: crippled by cut_level_'_ ======================";
14 "-------------- get_interval from ctree with move_dn:modspec.sml -";
15 "=====new ptree 2 without changes ================================";
16 "-------------- getFormulaeFromTo --------------------------------";
18 "--------- solve_linear as rootpbl AUTOCALCULATE CompleteModel ---";
19 "--------- solve_linear as rootpbl AUTOCALCULATE CompleteCalcHead-";
20 "--------- maximum-example: complete_metitms ---------------------";
21 "--------- maximum-example: complete_mod -------------------------";
22 "-----------------------------------------------------------------";
23 "-----------------------------------------------------------------";
24 "-----------------------------------------------------------------";
28 "=====new ptree 1: crippled by cut_level_'_ ======================";
29 "=====new ptree 1: crippled by cut_level_'_ ======================";
30 "=====new ptree 1: crippled by cut_level_'_ ======================";
33 [(["equality (x/(x^2 - 6*x+9) - 1/(x^2 - 3*x) =1/x)",
34 "solveFor x","solutions L"],
35 ("RatEq",["univariate","equation"],["no_met"]))];
36 Iterator 1; moveActiveRoot 1;
37 autoCalculate' 1 CompleteCalc;
39 getTactic 1 ([1],Res);(*Rewrite_Set RatEq_simplify*)
40 getTactic 1 ([2],Res);(*Rewrite_Set norm_Rational*)
41 getTactic 1 ([3],Res);(*Rewrite_Set RatEq_eliminate*)
42 getTactic 1 ([4,1],Res);(*Rewrite all_left*)
43 getTactic 1 ([4,2],Res);(*Rewrite_Set expand_binoms*)
44 getTactic 1 ([4,3],Res);(*Rewrite_Set_Inst make_ratpoly_in*)
46 moveActiveFormula 1 ([1],Res)(*1.1...1.4*);
47 moveActiveFormula 1 ([2],Res)(**ME_Isa: 'expand' not known*);
48 moveActiveFormula 1 ([3],Res)(*3.1.*);
49 moveActiveFormula 1 ([4,2],Res)(*4.2.1.*);
50 moveActiveFormula 1 ([4,3],Res)(**one_scr_arg: called by Script Stepwise t_=*);
52 moveActiveFormula 1 ([1],Res)(*1.1...1.4*);
53 interSteps 1 ([1],Res)(*..is activeFormula !?!*);
55 getTactic 1 ([1,1],Res);(*Rewrite real_diff_minus*)
56 getTactic 1 ([1,2],Res);(*Rewrite real_diff_minus*)
57 getTactic 1 ([1,3],Res);(*Rewrite real_diff_minus*)
58 getTactic 1 ([1,4],Res);(*Rewrite real_rat_mult_1*)
60 moveActiveFormula 1 ([4,2],Res)(*4.2.1.*);
61 interSteps 1 ([4,2],Res)(*..is activeFormula !?!*);
62 val ((pt,_),_) = get_calc 1;
63 writeln(pr_ptree pr_short pt);
64 (*delete [4,1] in order to make pos [4],[4,4] for pblobjs differen [4],[4,3]:
65 ###########################################################################*)
66 val (pt, _) = cut_level_'_ [] [] pt ([4,1],Frm); (*#*)
67 (*##########################################################################*)
68 writeln(pr_ptree pr_short pt);
69 (*##########################################################################
70 attention: the ctree in states is still the old (perfect) !!!
71 ############################################################################*)
75 "-------------- get_interval from ctree with move_dn:modspec.sml -";
76 "-------------- get_interval from ctree with move_dn:modspec.sml -";
77 "-------------- get_interval from ctree with move_dn:modspec.sml -";
78 writeln(pr_ptree pr_short pt);
79 writeln(posterms2str (get_interval ([],Frm) ([],Res) 99999 pt));
81 case map fst (get_interval ([],Frm) ([],Res) 99999 pt) of
109 | _ => error "diff.behav.in ctree.sml: get_interval lev 1f";
110 case map fst (get_interval ([],Frm) ([],Res) 1 pt) of
120 | _ => error "diff.behav.in ctree.sml: get_interval lev 1f";
121 case map fst (get_interval ([],Frm) ([],Res) 0 pt) of
124 | _ => error "diff.behav.in ctree.sml: get_interval lev 1f";
126 case map fst (get_interval ([1,3],Res) ([4,1,1],Frm) 99999 pt) of
134 ([4, 1, 1], Frm)] => ()
135 | _ => error "diff.behav.in ctree.sml: get_interval lev 1a";
137 (*this pos' is not generated bu move_dn:......vvv: goes to end of calc*)
138 case map fst (get_interval ([2],Res) ([4,3,2],Frm) 99999 pt) of
151 ([4, 3, 3], Res),(*this is beyond 'to'*)
152 ([4, 3, 4], Res),(*this is beyond 'to'*)
153 ([4, 3, 5], Res),(*this is beyond 'to'*)
154 ([4, 3], Res), (*this is beyond 'to'*)
155 ([4], Res), (*this is beyond 'to'*)
156 ([5], Res), (*this is beyond 'to'*)
157 ([], Res)] => () (*this is beyond 'to'*)
158 | _ => error "diff.behav.in ctree.sml: get_interval lev 1b";
159 case map fst (get_interval ([1,4],Res) ([4,3,1],Frm) 99999 pt) of
171 ([4, 3, 1], Frm)] => ()
172 | _ => error "diff.behav.in ctree.sml: get_interval lev 1c";
173 case map fst (get_interval ([4,2],Res) ([5],Res) 99999 pt) of
185 | _ => error "diff.behav.in ctree.sml: get_interval lev 1d";
186 case map fst (get_interval ([],Frm) ([4,3,2],Res) 99999 pt) of
206 ([4, 3, 2], Res)] => ()
207 | _ => error "diff.behav.in ctree.sml: get_interval lev 1e";
208 case map fst (get_interval ([4,3],Frm) ([4,3],Res) 99999 pt) of
217 | _ => error "diff.behav.in ctree.sml: get_interval lev 1g";
222 "=====new ptree 2 without changes ================================";
223 "=====new ptree 2 without changes ================================";
224 "=====new ptree 2 without changes ================================";
227 [(["equality (x/(x^2 - 6*x+9) - 1/(x^2 - 3*x) =1/x)",
228 "solveFor x","solutions L"],
229 ("RatEq",["univariate","equation"],["no_met"]))];
230 Iterator 1; moveActiveRoot 1;
231 autoCalculate' 1 CompleteCalc;
232 val ((pt,_),_) = get_calc 1;
234 val (Form f, tac, asms) = pt_extract (pt, p);
235 if term2str f = "[x = 6 / 5]" andalso p = ([], Res) then ()
236 else error "after ===new ptree 2 without changes ===";
237 writeln(pr_ptree pr_short pt);
240 "-------------- getFormulaeFromTo --------------------------------";
241 "-------------- getFormulaeFromTo --------------------------------";
242 "-------------- getFormulaeFromTo --------------------------------";
243 getFormulaeFromTo 1 ([4, 2], Res) ([4, 4], Pbl) 000;
245 "@@@@@begin@@@@@" //...................................................
246 + " 1" //..............................................................
247 + "<GETELEMENTSFROMTO>" //...................................................
248 + " <CALCID> 1 </CALCID>" //..........................................
249 + " <POSFORMHEADS>" //................................................
250 + " <POSFORM>" //...................................................
251 + " <GENERATED>" //...............................................
252 + " <INTLIST>" //...............................................
253 + " <INT> 4 </INT>" //........................................
254 + " <INT> 3 </INT>" //........................................
255 + " </INTLIST>" //..............................................
256 + " <POS> Res </POS>" //........................................
257 + " </GENERATED>" //..............................................
258 + " <FORMULA>" //.................................................
259 + " <MATHML>" //................................................
260 + " <ISA> -6 * x + 5 * x ^^^ 2 = 0 </ISA>" //.................
261 + " </MATHML>" //...............................................
262 + " </FORMULA>" //................................................
263 + " </POSFORM>" //..................................................
264 + " <POSHEAD>" //...................................................
265 + " <GENERATED>" //...............................................
266 + " <INTLIST>" //...............................................
267 + " <INT> 4 </INT>" //........................................
268 + " <INT> 4 </INT>" //........................................
269 + " </INTLIST>" //..............................................
270 + " <POS> Pbl </POS>" //........................................
271 + " </GENERATED>" //..............................................
272 + " <CALCHEAD status = "correct">" //.............................
273 + " <HEAD>" //...................................................
274 + " <MATHML>" //...............................................
275 + " <ISA> solve (-6 * x + 5 * x ^^^ 2 = 0, x) </ISA>" //.....
276 + " </MATHML>" //..............................................
277 + " </HEAD>" //..................................................
278 + " <MODEL>" //.................................................
279 + " <GIVEN>" //...............................................
280 + " <ITEM status="correct">" //.............................
281 + " <MATHML>" //..........................................
282 + " <ISA> equality (-6 * x + 5 * x ^^^ 2 = 0) </ISA>" //
283 + " </MATHML>" //.........................................
284 + " </ITEM>" //.............................................
285 + " <ITEM status="correct">" //.............................
286 + " <MATHML>" //..........................................
287 + " <ISA> solveFor x </ISA>" //.........................
288 + " </MATHML>" //.........................................
289 + " </ITEM>" //.............................................
290 + " </GIVEN>" //..............................................
291 + " <WHERE>" //...............................................
292 + " <ITEM status="correct">" //.............................
293 + " <MATHML>" //..........................................
294 + " <ISA> matches (?a * ?v_ + ?v_ ^^^ 2 = 0) (-6 * x + 5 * x ^^^ 2 = 0) |"
295 + "matches (?v_ + ?v_ ^^^ 2 = 0) (-6 * x + 5 * x ^^^ 2 = 0) |" //......
296 + "matches (?v_ + ?b * ?v_ ^^^ 2 = 0) (-6 * x + 5 * x ^^^ 2 = 0) |"
297 + "matches (?a * ?v_ + ?b * ?v_ ^^^ 2 = 0) (-6 * x + 5 * x ^^^ 2 = 0) |"
298 + "matches (?v_ ^^^ 2 = 0) (-6 * x + 5 * x ^^^ 2 = 0) |" //............
299 + "matches (?b * ?v_ ^^^ 2 = 0) (-6 * x + 5 * x ^^^ 2 = 0) </ISA>" //..
300 + " </MATHML>" //.........................................
301 + " </ITEM>" //.............................................
302 + " </WHERE>" //..............................................
303 + " <FIND>" //................................................
304 + " <ITEM status="correct">" //.............................
305 + " <MATHML>" //..........................................
306 + " <ISA> solutions x_i </ISA>" //......................
307 + " </MATHML>" //.........................................
308 + " </ITEM>" //.............................................
309 + " </FIND>" //...............................................
310 + " <RELATE> </RELATE>" //...................................
311 + " </MODEL>" //................................................
312 + " <BELONGSTO> Pbl </BELONGSTO>" //............................
313 + " <SPECIFICATION>" //.........................................
314 + " <THEORYID> PolyEq.thy </THEORYID>" //.....................
315 + " <PROBLEMID>" //...........................................
316 + " <STRINGLIST>" //........................................
317 + " <STRING> bdv_only </STRING>" //.......................
318 + " <STRING> degree_2 </STRING>" //.......................
319 + " <STRING> polynomial </STRING>" //.....................
320 + " <STRING> univariate </STRING>" //.....................
321 + " <STRING> equation </STRING>" //.......................
322 + " </STRINGLIST>" //.......................................
323 + " </PROBLEMID>" //..........................................
324 + " <METHODID>" //............................................
325 + " <STRINGLIST>" //........................................
326 + " <STRING> PolyEq </STRING>" //.........................
327 + " <STRING> solve_d2_polyeq_bdvonly_equation </STRING>"
328 + " </STRINGLIST>" //.......................................
329 + " </METHODID>" //...........................................
330 + " </SPECIFICATION>" //........................................
331 + " </CALCHEAD>" //...............................................
332 + " </POSHEAD>" //..................................................
333 + " <POSFORMHEADS>" //................................................
334 + "</GETELEMENTSFROMTO>" //..................................................
339 "--------- solve_linear as rootpbl AUTOCALCULATE CompleteModel ---";
340 "--------- solve_linear as rootpbl AUTOCALCULATE CompleteModel ---";
341 "--------- solve_linear as rootpbl AUTOCALCULATE CompleteModel ---";
343 val (p,_,f,nxt,_,pt) = CalcTreeTEST
344 [(["equality (1+-1*2+x=(0::real))", "solveFor x","solutions L"],
346 ["LINEAR","univariate","equation","test"],
347 ["Test","solve_linear"]))];
348 val (p,_,f,nxt,_,pt) = me nxt p c pt;
349 val (p,_,f,nxt,_,pt) = me nxt p c pt;
350 (*xt = Add_Given "solveFor x"*)
351 writeln (itms2str_ ctxt (get_obj g_pbl pt (fst p)));
353 (0 ,[] ,false ,#Given ,Inc solveFor ,(??.empty, [])),
354 (0 ,[] ,false ,#Find ,Inc solutions [] ,(??.empty, [])),
355 (1 ,[1] ,true ,#Given ,Cor equality (1 + -1 * 2 + x = 0) ,(e_, [1 + -1 * 2 + x = 0]))]*)
356 val (pt,p) = complete_mod (pt, p);
357 if itms2str_ ctxt (get_obj g_pbl pt (fst p)) = "[\n(1 ,[1] ,true ,#Given ,Cor equality (1 + -1 * 2 + x = 0) ,(e_, [1 + -1 * 2 + x = 0])),\n(2 ,[1] ,true ,#Given ,Cor solveFor x ,(v_, [x])),\n(3 ,[1] ,true ,#Find ,Cor solutions L ,(v_i_, [L]))]" then ()
358 else error "completetest.sml: new behav. in complete_mod 1";
359 writeln (itms2str_ ctxt (get_obj g_pbl pt (fst p)));
361 (1 ,[1] ,true ,#Given ,Cor equality (1 + -1 * 2 + x = 0) ,(e_, [1 + -1 * 2 + x = 0])),
362 (2 ,[1] ,true ,#Given ,Cor solveFor x ,(solveFor, [x])),
363 (3 ,[1] ,true ,#Find ,Cor solutions L ,(solutions, [L]))]*)
364 val mits = get_obj g_met pt (fst p);
365 if itms2str_ ctxt mits = "[\n(1 ,[1] ,true ,#Given ,Cor equality (1 + -1 * 2 + x = 0) ,(e_, [1 + -1 * 2 + x = 0])),\n(2 ,[1] ,true ,#Given ,Cor solveFor x ,(v_, [x])),\n(3 ,[1] ,true ,#Find ,Cor solutions L ,(v_i_, [L]))]"
366 then () else error "completetest.sml: new behav. in complete_mod 2";
367 writeln (itms2str_ ctxt mits);
369 (1 ,[1] ,true ,#Given ,Cor equality (1 + -1 * 2 + x = 0) ,(e_, [1 + -1 * 2 + x = 0])),
370 (2 ,[1] ,true ,#Given ,Cor solveFor x ,(solveFor, [x])),
371 (3 ,[1] ,true ,#Find ,Cor solutions L ,(solutions, [L]))]*)
375 "--------- solve_linear as rootpbl AUTOCALCULATE CompleteCalcHead-";
376 "--------- solve_linear as rootpbl AUTOCALCULATE CompleteCalcHead-";
377 "--------- solve_linear as rootpbl AUTOCALCULATE CompleteCalcHead-";
379 CalcTree (*start of calculation, return No.1*)
380 [(["equality (1+-1*2+x=(0::real))", "solveFor x","solutions L"],
382 ["LINEAR","univariate","equation","test"],
383 ["Test","solve_linear"]))];
384 Iterator 1; moveActiveRoot 1;
387 autoCalculate' 1 CompleteCalcHead;
388 autoCalculate' 1 (Step 1);
389 refFormula 1 (get_pos 1 1);
393 autoCalculate' 1 CompleteCalcHead;
394 fetchProposedTactic 1; (*-> Apply_Method*);
395 setNextTactic 1 (Apply_Method ["Test","solve_linear"]);
396 autoCalculate' 1 (Step 1);
397 refFormula 1 (get_pos 1 1);
401 autoCalculate' 1 (Step 1);
402 refFormula 1 (get_pos 1 1);
404 autoCalculate' 1 CompleteModel;
405 refFormula 1 (get_pos 1 1);
407 autoCalculate' 1 CompleteCalcHead;
408 (* *** complete_mod: only impl.for Pbl, called with ([], Met) FIXXXXXXXXXXME*)
412 "--------- maximum-example: complete_metitms ---------------------";
413 "--------- maximum-example: complete_metitms ---------------------";
414 "--------- maximum-example: complete_metitms ---------------------";
415 val (p,_,f,nxt,_,pt) =
417 [(["fixedValues [r=Arbfix]","maximum A",
419 "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
420 "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
421 "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]",
423 "boundVariable a","boundVariable b","boundVariable alpha",
424 "interval {x::real. 0 <= x & x <= 2*r}",
425 "interval {x::real. 0 <= x & x <= 2*r}",
426 "interval {x::real. 0 <= x & x <= pi}",
427 "errorBound (eps=(0::real))"],
428 ("DiffApp",["maximum_of","function"],["DiffApp","max_by_calculus"])
430 val (p,_,f,nxt,_,pt) = me nxt p c pt;
431 val (p,_,f,nxt,_,pt) = me nxt p c pt;
432 val (p,_,f,nxt,_,pt) = me nxt p c pt;
433 val (p,_,f,nxt,_,pt) = me nxt p c pt;
434 val (p,_,f,nxt,_,pt) = (me nxt p c pt) handle e => OldGoals.print_exn e;
435 val (p,_,f,nxt,_,pt) = me nxt p c pt;
436 val (p,_,f,nxt,_,pt) = me nxt p c pt;
437 (*nxt = Specify_Theory "DiffApp"*)
438 val (oris, _, _) = get_obj g_origin pt (fst p);
439 writeln (oris2str oris);
441 (1, ["1","2","3"], #Given,fixedValues, ["[r = Arbfix]"]),
442 (2, ["1","2","3"], #Find,maximum, ["A"]),
443 (3, ["1","2","3"], #Find,valuesFor, ["[a]","[b]"]),
444 (4, ["1","2"], #Relate,relations, ["[A = a * b]","[(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]"]),
445 (5, ["3"], #Relate,relations, ["[A = a * b]","[a / 2 = r * sin alpha]","[b / 2 = r * cos alpha]"]),
446 (6, ["1"], #undef,boundVariable, ["a"]),
447 (7, ["2"], #undef,boundVariable, ["b"]),
448 (8, ["3"], #undef,boundVariable, ["alpha"]),
449 (9, ["1","2"], #undef,interval, ["{x. 0 <= x & x <= 2 * r}"]),
450 (10, ["3"], #undef,interval, ["{x. 0 <= x & x <= pi}"]),
451 (11, ["1","2","3"], #undef,errorBound, ["eps = 0"])]*)
452 val pits = get_obj g_pbl pt (fst p);
453 writeln (itms2str_ ctxt pits);
455 (1 ,[1,2,3] ,true,#Given ,Cor fixedValues [r = Arbfix],(fix_, [[r = Arbfix]])),
456 (2 ,[1,2,3] ,true,#Find ,Cor maximum A ,(m_, [A])),
457 (3 ,[1,2,3] ,true,#Find ,Cor valuesFor [a, b] ,(vs_, [[a, b]])),
458 (4 ,[1,2] ,true,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^
459 2 = r ^^^ 2] ,(rs_, [[A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]]))]*)
460 val mits = get_obj g_met pt (fst p);
461 val mits = complete_metitms oris pits []
462 ((#ppc o get_met) ["DiffApp","max_by_calculus"]);
463 writeln (itms2str_ ctxt mits);
465 (1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),
466 (2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),
467 (3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(vs_, [[a, b]])),
468 (4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^
469 2 = r ^^^ 2] ,(rs_, [[A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]])),
470 (6 ,[1] ,true ,#undef ,Cor boundVariable a ,(boundVariable, [a])),
471 (9 ,[1,2] ,true ,#undef ,Cor interval {x. 0 <= x & x <= 2 * r} ,(interval, [{x.
472 0 <= x & x <= 2 * r}])),
473 (11 ,[1,2,3] ,true ,#undef ,Cor errorBound (eps = 0) ,(errorBound, [eps = 0]))]*)
474 if itms2str_ ctxt mits = "[\n(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),\n(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),\n(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(vs_, [[a, b]])),\n(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2] ,(rs_, [[A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]])),\n(6 ,[1] ,true ,#undef ,Cor boundVariable a ,(v_, [a])),\n(9 ,[1,2] ,true ,#undef ,Cor interval {x. 0 <= x & x <= 2 * r} ,(itv_, [{x. 0 <= x & x <= 2 * r}])),\n(11 ,[1,2,3] ,true ,#undef ,Cor errorBound (eps = 0) ,(err_, [eps = 0]))]" then ()
475 else error "completetest.sml: new behav. in complete_metitms 1";
478 "--------- maximum-example: complete_mod -------------------------";
479 "--------- maximum-example: complete_mod -------------------------";
480 "--------- maximum-example: complete_mod -------------------------";
481 val (p,_,f,nxt,_,pt) =
483 [(["fixedValues [r=Arbfix]","maximum A",
485 "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
486 "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
487 "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]",
489 "boundVariable a","boundVariable b","boundVariable alpha",
490 "interval {x::real. 0 <= x & x <= 2*r}",
491 "interval {x::real. 0 <= x & x <= 2*r}",
492 "interval {x::real. 0 <= x & x <= pi}",
493 "errorBound (eps=(0::real))"],
494 ("DiffApp",["maximum_of","function"],["DiffApp","max_by_calculus"])
496 val (p,_,f,nxt,_,pt) = me nxt p c pt;
497 val (p,_,f,nxt,_,pt) = me nxt p c pt;
498 val (p,_,f,nxt,_,pt) = me nxt p c pt;
499 (*nxt = nxt = Add_Find "valuesFor [a]" FIXME.12.03 +handle Inc !*)
500 val pits = get_obj g_pbl pt (fst p);
501 writeln (itms2str_ ctxt pits);
503 (0 ,[] ,false ,#Find ,Inc valuesFor ,(??.empty, [])),
504 (0 ,[] ,false ,#Relate ,Inc relations [] ,(??.empty, [])),
505 (1 ,[1,2,3] ,true,#Given,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),
506 (2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A]))]*)
507 val (pt,p) = complete_mod (pt,p);
508 val pits = get_obj g_pbl pt (fst p);
509 if itms2str_ ctxt pits = "[\n(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),\n(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),\n(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(vs_, [[a],[b]])),\n(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2] ,(rs_, [[A = a * b],[(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]]))]"
510 then () else error "completetest.sml: new behav. in complete_mod 3";
511 writeln (itms2str_ ctxt pits);
513 (1 ,[1,2,3] ,true,#Given,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),
514 (2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),
515 (3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(valuesFor, [[a],[b]])),
516 (4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^
517 2 = r ^^^ 2] ,(relations, [[A = a * b],[(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]]))]*)
518 val mits = get_obj g_met pt (fst p);
519 if itms2str_ ctxt mits = "[\n(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),\n(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),\n(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(vs_, [[a],[b]])),\n(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2] ,(rs_, [[A = a * b],[(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]])),\n(6 ,[1] ,true ,#undef ,Cor boundVariable a ,(v_, [a])),\n(9 ,[1,2] ,true ,#undef ,Cor interval {x. 0 <= x & x <= 2 * r} ,(itv_, [{x. 0 <= x & x <= 2 * r}])),\n(11 ,[1,2,3] ,true ,#undef ,Cor errorBound (eps = 0) ,(err_, [eps = 0]))]"
520 then () else error "completetest.sml: new behav. in complete_mod 3";
521 writeln (itms2str_ ctxt mits);
523 (1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),
524 (2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),
525 (3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(valuesFor, [[a],[b]])),
526 (4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^
527 2 = r ^^^ 2] ,(relations, [[A = a * b],[(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]])),
528 (6 ,[1] ,true ,#undef ,Cor boundVariable a ,(boundVariable, [a])),
529 (9 ,[1,2] ,true ,#undef ,Cor interval {x. 0 <= x & x <= 2 * r} ,(interval, [{x.
530 0 <= x & x <= 2 * r}])),
531 (11 ,[1,2,3] ,true ,#undef ,Cor errorBound (eps = 0) ,(errorBound, [eps = 0]))]*)