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.thy",["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 | _ => raise error "diff.behav.in ctree.sml: get_interval lev 1f";
110 case map fst (get_interval ([],Frm) ([],Res) 1 pt) of
120 | _ => raise error "diff.behav.in ctree.sml: get_interval lev 1f";
121 case map fst (get_interval ([],Frm) ([],Res) 0 pt) of
124 | _ => raise 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 | _ => raise 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 | _ => raise 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 | _ => raise 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 | _ => raise 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 | _ => raise 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 | _ => raise 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.thy",["univariate","equation"],["no_met"]))];
230 Iterator 1; moveActiveRoot 1;
231 autoCalculate 1 CompleteCalc;
232 val ((pt,_),_) = get_calc 1;
233 writeln(pr_ptree pr_short pt);
236 "-------------- getFormulaeFromTo --------------------------------";
237 "-------------- getFormulaeFromTo --------------------------------";
238 "-------------- getFormulaeFromTo --------------------------------";
239 getFormulaeFromTo 1 ([4, 2], Res) ([4, 4], Pbl) 000;
241 "@@@@@begin@@@@@" //...................................................
242 + " 1" //..............................................................
243 + "<GETELEMENTSFROMTO>" //...................................................
244 + " <CALCID> 1 </CALCID>" //..........................................
245 + " <POSFORMHEADS>" //................................................
246 + " <POSFORM>" //...................................................
247 + " <GENERATED>" //...............................................
248 + " <INTLIST>" //...............................................
249 + " <INT> 4 </INT>" //........................................
250 + " <INT> 3 </INT>" //........................................
251 + " </INTLIST>" //..............................................
252 + " <POS> Res </POS>" //........................................
253 + " </GENERATED>" //..............................................
254 + " <FORMULA>" //.................................................
255 + " <MATHML>" //................................................
256 + " <ISA> -6 * x + 5 * x ^^^ 2 = 0 </ISA>" //.................
257 + " </MATHML>" //...............................................
258 + " </FORMULA>" //................................................
259 + " </POSFORM>" //..................................................
260 + " <POSHEAD>" //...................................................
261 + " <GENERATED>" //...............................................
262 + " <INTLIST>" //...............................................
263 + " <INT> 4 </INT>" //........................................
264 + " <INT> 4 </INT>" //........................................
265 + " </INTLIST>" //..............................................
266 + " <POS> Pbl </POS>" //........................................
267 + " </GENERATED>" //..............................................
268 + " <CALCHEAD status = "correct">" //.............................
269 + " <HEAD>" //...................................................
270 + " <MATHML>" //...............................................
271 + " <ISA> solve (-6 * x + 5 * x ^^^ 2 = 0, x) </ISA>" //.....
272 + " </MATHML>" //..............................................
273 + " </HEAD>" //..................................................
274 + " <MODEL>" //.................................................
275 + " <GIVEN>" //...............................................
276 + " <ITEM status="correct">" //.............................
277 + " <MATHML>" //..........................................
278 + " <ISA> equality (-6 * x + 5 * x ^^^ 2 = 0) </ISA>" //
279 + " </MATHML>" //.........................................
280 + " </ITEM>" //.............................................
281 + " <ITEM status="correct">" //.............................
282 + " <MATHML>" //..........................................
283 + " <ISA> solveFor x </ISA>" //.........................
284 + " </MATHML>" //.........................................
285 + " </ITEM>" //.............................................
286 + " </GIVEN>" //..............................................
287 + " <WHERE>" //...............................................
288 + " <ITEM status="correct">" //.............................
289 + " <MATHML>" //..........................................
290 + " <ISA> matches (?a * ?v_ + ?v_ ^^^ 2 = 0) (-6 * x + 5 * x ^^^ 2 = 0) |"
291 + "matches (?v_ + ?v_ ^^^ 2 = 0) (-6 * x + 5 * x ^^^ 2 = 0) |" //......
292 + "matches (?v_ + ?b * ?v_ ^^^ 2 = 0) (-6 * x + 5 * x ^^^ 2 = 0) |"
293 + "matches (?a * ?v_ + ?b * ?v_ ^^^ 2 = 0) (-6 * x + 5 * x ^^^ 2 = 0) |"
294 + "matches (?v_ ^^^ 2 = 0) (-6 * x + 5 * x ^^^ 2 = 0) |" //............
295 + "matches (?b * ?v_ ^^^ 2 = 0) (-6 * x + 5 * x ^^^ 2 = 0) </ISA>" //..
296 + " </MATHML>" //.........................................
297 + " </ITEM>" //.............................................
298 + " </WHERE>" //..............................................
299 + " <FIND>" //................................................
300 + " <ITEM status="correct">" //.............................
301 + " <MATHML>" //..........................................
302 + " <ISA> solutions x_i </ISA>" //......................
303 + " </MATHML>" //.........................................
304 + " </ITEM>" //.............................................
305 + " </FIND>" //...............................................
306 + " <RELATE> </RELATE>" //...................................
307 + " </MODEL>" //................................................
308 + " <BELONGSTO> Pbl </BELONGSTO>" //............................
309 + " <SPECIFICATION>" //.........................................
310 + " <THEORYID> PolyEq.thy </THEORYID>" //.....................
311 + " <PROBLEMID>" //...........................................
312 + " <STRINGLIST>" //........................................
313 + " <STRING> bdv_only </STRING>" //.......................
314 + " <STRING> degree_2 </STRING>" //.......................
315 + " <STRING> polynomial </STRING>" //.....................
316 + " <STRING> univariate </STRING>" //.....................
317 + " <STRING> equation </STRING>" //.......................
318 + " </STRINGLIST>" //.......................................
319 + " </PROBLEMID>" //..........................................
320 + " <METHODID>" //............................................
321 + " <STRINGLIST>" //........................................
322 + " <STRING> PolyEq </STRING>" //.........................
323 + " <STRING> solve_d2_polyeq_bdvonly_equation </STRING>"
324 + " </STRINGLIST>" //.......................................
325 + " </METHODID>" //...........................................
326 + " </SPECIFICATION>" //........................................
327 + " </CALCHEAD>" //...............................................
328 + " </POSHEAD>" //..................................................
329 + " <POSFORMHEADS>" //................................................
330 + "</GETELEMENTSFROMTO>" //..................................................
335 "--------- solve_linear as rootpbl AUTOCALCULATE CompleteModel ---";
336 "--------- solve_linear as rootpbl AUTOCALCULATE CompleteModel ---";
337 "--------- solve_linear as rootpbl AUTOCALCULATE CompleteModel ---";
339 val (p,_,f,nxt,_,pt) = CalcTreeTEST
340 [(["equality (1+-1*2+x=0)", "solveFor x","solutions L"],
342 ["linear","univariate","equation","test"],
343 ["Test","solve_linear"]))];
344 val (p,_,f,nxt,_,pt) = me nxt p c pt;
345 val (p,_,f,nxt,_,pt) = me nxt p c pt;
346 (*xt = Add_Given "solveFor x"*)
347 writeln (itms2str_ ctxt (get_obj g_pbl pt (fst p)));
349 (0 ,[] ,false ,#Given ,Inc solveFor ,(??.empty, [])),
350 (0 ,[] ,false ,#Find ,Inc solutions [] ,(??.empty, [])),
351 (1 ,[1] ,true ,#Given ,Cor equality (1 + -1 * 2 + x = 0) ,(e_, [1 + -1 * 2 + x = 0]))]*)
352 val (pt,p) = complete_mod (pt, p);
353 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 ()
354 else raise error "completetest.sml: new behav. in complete_mod 1";
355 writeln (itms2str_ ctxt (get_obj g_pbl pt (fst p)));
357 (1 ,[1] ,true ,#Given ,Cor equality (1 + -1 * 2 + x = 0) ,(e_, [1 + -1 * 2 + x = 0])),
358 (2 ,[1] ,true ,#Given ,Cor solveFor x ,(solveFor, [x])),
359 (3 ,[1] ,true ,#Find ,Cor solutions L ,(solutions, [L]))]*)
360 val mits = get_obj g_met pt (fst p);
361 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]))]"
362 then () else raise error "completetest.sml: new behav. in complete_mod 2";
363 writeln (itms2str_ ctxt mits);
365 (1 ,[1] ,true ,#Given ,Cor equality (1 + -1 * 2 + x = 0) ,(e_, [1 + -1 * 2 + x = 0])),
366 (2 ,[1] ,true ,#Given ,Cor solveFor x ,(solveFor, [x])),
367 (3 ,[1] ,true ,#Find ,Cor solutions L ,(solutions, [L]))]*)
371 "--------- solve_linear as rootpbl AUTOCALCULATE CompleteCalcHead-";
372 "--------- solve_linear as rootpbl AUTOCALCULATE CompleteCalcHead-";
373 "--------- solve_linear as rootpbl AUTOCALCULATE CompleteCalcHead-";
375 CalcTree (*start of calculation, return No.1*)
376 [(["equality (1+-1*2+x=0)", "solveFor x","solutions L"],
378 ["linear","univariate","equation","test"],
379 ["Test","solve_linear"]))];
380 Iterator 1; moveActiveRoot 1;
383 autoCalculate 1 CompleteCalcHead;
384 autoCalculate 1 (Step 1);
385 refFormula 1 (get_pos 1 1);
389 autoCalculate 1 CompleteCalcHead;
390 fetchProposedTactic 1; (*-> Apply_Method*);
391 setNextTactic 1 (Apply_Method ["Test","solve_linear"]);
392 autoCalculate 1 (Step 1);
393 refFormula 1 (get_pos 1 1);
397 autoCalculate 1 (Step 1);
398 refFormula 1 (get_pos 1 1);
400 autoCalculate 1 CompleteModel;
401 refFormula 1 (get_pos 1 1);
403 autoCalculate 1 CompleteCalcHead;
404 (* *** complete_mod: only impl.for Pbl, called with ([], Met) FIXXXXXXXXXXME*)
408 "--------- maximum-example: complete_metitms ---------------------";
409 "--------- maximum-example: complete_metitms ---------------------";
410 "--------- maximum-example: complete_metitms ---------------------";
411 val (p,_,f,nxt,_,pt) =
413 [(["fixedValues [r=Arbfix]","maximum A",
415 "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
416 "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
417 "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]",
419 "boundVariable a","boundVariable b","boundVariable alpha",
420 "interval {x::real. 0 <= x & x <= 2*r}",
421 "interval {x::real. 0 <= x & x <= 2*r}",
422 "interval {x::real. 0 <= x & x <= pi}",
423 "errorBound (eps=(0::real))"],
424 ("DiffApp.thy",["maximum_of","function"],["DiffApp","max_by_calculus"])
426 val (p,_,f,nxt,_,pt) = me nxt p c pt;
427 val (p,_,f,nxt,_,pt) = me nxt p c pt;
428 val (p,_,f,nxt,_,pt) = me nxt p c pt;
429 val (p,_,f,nxt,_,pt) = me nxt p c pt;
430 val (p,_,f,nxt,_,pt) = (me nxt p c pt) handle e => print_exn e;
431 val (p,_,f,nxt,_,pt) = me nxt p c pt;
432 val (p,_,f,nxt,_,pt) = me nxt p c pt;
433 (*nxt = Specify_Theory "DiffApp.thy"*)
434 val (oris, _, _) = get_obj g_origin pt (fst p);
435 writeln (oris2str oris);
437 (1, ["1","2","3"], #Given,fixedValues, ["[r = Arbfix]"]),
438 (2, ["1","2","3"], #Find,maximum, ["A"]),
439 (3, ["1","2","3"], #Find,valuesFor, ["[a]","[b]"]),
440 (4, ["1","2"], #Relate,relations, ["[A = a * b]","[(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]"]),
441 (5, ["3"], #Relate,relations, ["[A = a * b]","[a / 2 = r * sin alpha]","[b / 2 = r * cos alpha]"]),
442 (6, ["1"], #undef,boundVariable, ["a"]),
443 (7, ["2"], #undef,boundVariable, ["b"]),
444 (8, ["3"], #undef,boundVariable, ["alpha"]),
445 (9, ["1","2"], #undef,interval, ["{x. 0 <= x & x <= 2 * r}"]),
446 (10, ["3"], #undef,interval, ["{x. 0 <= x & x <= pi}"]),
447 (11, ["1","2","3"], #undef,errorBound, ["eps = 0"])]*)
448 val pits = get_obj g_pbl pt (fst p);
449 writeln (itms2str_ ctxt pits);
451 (1 ,[1,2,3] ,true,#Given ,Cor fixedValues [r = Arbfix],(fix_, [[r = Arbfix]])),
452 (2 ,[1,2,3] ,true,#Find ,Cor maximum A ,(m_, [A])),
453 (3 ,[1,2,3] ,true,#Find ,Cor valuesFor [a, b] ,(vs_, [[a, b]])),
454 (4 ,[1,2] ,true,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^
455 2 = r ^^^ 2] ,(rs_, [[A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]]))]*)
456 val mits = get_obj g_met pt (fst p);
457 val mits = complete_metitms oris pits []
458 ((#ppc o get_met) ["DiffApp","max_by_calculus"]);
459 writeln (itms2str_ ctxt mits);
461 (1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),
462 (2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),
463 (3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(vs_, [[a, b]])),
464 (4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^
465 2 = r ^^^ 2] ,(rs_, [[A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]])),
466 (6 ,[1] ,true ,#undef ,Cor boundVariable a ,(boundVariable, [a])),
467 (9 ,[1,2] ,true ,#undef ,Cor interval {x. 0 <= x & x <= 2 * r} ,(interval, [{x.
468 0 <= x & x <= 2 * r}])),
469 (11 ,[1,2,3] ,true ,#undef ,Cor errorBound (eps = 0) ,(errorBound, [eps = 0]))]*)
470 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 ()
471 else raise error "completetest.sml: new behav. in complete_metitms 1";
474 "--------- maximum-example: complete_mod -------------------------";
475 "--------- maximum-example: complete_mod -------------------------";
476 "--------- maximum-example: complete_mod -------------------------";
477 val (p,_,f,nxt,_,pt) =
479 [(["fixedValues [r=Arbfix]","maximum A",
481 "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
482 "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
483 "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]",
485 "boundVariable a","boundVariable b","boundVariable alpha",
486 "interval {x::real. 0 <= x & x <= 2*r}",
487 "interval {x::real. 0 <= x & x <= 2*r}",
488 "interval {x::real. 0 <= x & x <= pi}",
489 "errorBound (eps=(0::real))"],
490 ("DiffApp.thy",["maximum_of","function"],["DiffApp","max_by_calculus"])
492 val (p,_,f,nxt,_,pt) = me nxt p c pt;
493 val (p,_,f,nxt,_,pt) = me nxt p c pt;
494 val (p,_,f,nxt,_,pt) = me nxt p c pt;
495 (*nxt = nxt = Add_Find "valuesFor [a]" FIXME.12.03 +handle Inc !*)
496 val pits = get_obj g_pbl pt (fst p);
497 writeln (itms2str_ ctxt pits);
499 (0 ,[] ,false ,#Find ,Inc valuesFor ,(??.empty, [])),
500 (0 ,[] ,false ,#Relate ,Inc relations [] ,(??.empty, [])),
501 (1 ,[1,2,3] ,true,#Given,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),
502 (2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A]))]*)
503 val (pt,p) = complete_mod (pt,p);
504 val pits = get_obj g_pbl pt (fst p);
505 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]]))]"
506 then () else raise error "completetest.sml: new behav. in complete_mod 3";
507 writeln (itms2str_ ctxt pits);
509 (1 ,[1,2,3] ,true,#Given,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),
510 (2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),
511 (3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(valuesFor, [[a],[b]])),
512 (4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^
513 2 = r ^^^ 2] ,(relations, [[A = a * b],[(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]]))]*)
514 val mits = get_obj g_met pt (fst p);
515 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]))]"
516 then () else raise error "completetest.sml: new behav. in complete_mod 3";
517 writeln (itms2str_ ctxt mits);
519 (1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),
520 (2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),
521 (3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(valuesFor, [[a],[b]])),
522 (4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^
523 2 = r ^^^ 2] ,(relations, [[A = a * b],[(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]])),
524 (6 ,[1] ,true ,#undef ,Cor boundVariable a ,(boundVariable, [a])),
525 (9 ,[1,2] ,true ,#undef ,Cor interval {x. 0 <= x & x <= 2 * r} ,(interval, [{x.
526 0 <= x & x <= 2 * r}])),
527 (11 ,[1,2,3] ,true ,#undef ,Cor errorBound (eps = 0) ,(errorBound, [eps = 0]))]*)