349 (0 ,[] ,false ,#Given ,Inc solveFor ,(??.empty, [])), |
349 (0 ,[] ,false ,#Given ,Inc solveFor ,(??.empty, [])), |
350 (0 ,[] ,false ,#Find ,Inc solutions [] ,(??.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]))]*) |
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); |
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 () |
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"; |
354 else error "completetest.sml: new behav. in complete_mod 1"; |
355 writeln (itms2str_ ctxt (get_obj g_pbl pt (fst p))); |
355 writeln (itms2str_ ctxt (get_obj g_pbl pt (fst p))); |
356 (*[ |
356 (*[ |
357 (1 ,[1] ,true ,#Given ,Cor equality (1 + -1 * 2 + x = 0) ,(e_, [1 + -1 * 2 + x = 0])), |
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])), |
358 (2 ,[1] ,true ,#Given ,Cor solveFor x ,(solveFor, [x])), |
359 (3 ,[1] ,true ,#Find ,Cor solutions L ,(solutions, [L]))]*) |
359 (3 ,[1] ,true ,#Find ,Cor solutions L ,(solutions, [L]))]*) |
360 val mits = get_obj g_met pt (fst p); |
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]))]" |
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"; |
362 then () else error "completetest.sml: new behav. in complete_mod 2"; |
363 writeln (itms2str_ ctxt mits); |
363 writeln (itms2str_ ctxt mits); |
364 (*[ |
364 (*[ |
365 (1 ,[1] ,true ,#Given ,Cor equality (1 + -1 * 2 + x = 0) ,(e_, [1 + -1 * 2 + x = 0])), |
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])), |
366 (2 ,[1] ,true ,#Given ,Cor solveFor x ,(solveFor, [x])), |
367 (3 ,[1] ,true ,#Find ,Cor solutions L ,(solutions, [L]))]*) |
367 (3 ,[1] ,true ,#Find ,Cor solutions L ,(solutions, [L]))]*) |
466 (6 ,[1] ,true ,#undef ,Cor boundVariable a ,(boundVariable, [a])), |
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. |
467 (9 ,[1,2] ,true ,#undef ,Cor interval {x. 0 <= x & x <= 2 * r} ,(interval, [{x. |
468 0 <= x & x <= 2 * r}])), |
468 0 <= x & x <= 2 * r}])), |
469 (11 ,[1,2,3] ,true ,#undef ,Cor errorBound (eps = 0) ,(errorBound, [eps = 0]))]*) |
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 () |
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"; |
471 else error "completetest.sml: new behav. in complete_metitms 1"; |
472 |
472 |
473 |
473 |
474 "--------- maximum-example: complete_mod -------------------------"; |
474 "--------- maximum-example: complete_mod -------------------------"; |
475 "--------- maximum-example: complete_mod -------------------------"; |
475 "--------- maximum-example: complete_mod -------------------------"; |
476 "--------- maximum-example: complete_mod -------------------------"; |
476 "--------- maximum-example: complete_mod -------------------------"; |
501 (1 ,[1,2,3] ,true,#Given,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])), |
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]))]*) |
502 (2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A]))]*) |
503 val (pt,p) = complete_mod (pt,p); |
503 val (pt,p) = complete_mod (pt,p); |
504 val pits = get_obj g_pbl pt (fst 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]]))]" |
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"; |
506 then () else error "completetest.sml: new behav. in complete_mod 3"; |
507 writeln (itms2str_ ctxt pits); |
507 writeln (itms2str_ ctxt pits); |
508 (*[ |
508 (*[ |
509 (1 ,[1,2,3] ,true,#Given,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])), |
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])), |
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]])), |
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) ^^^ |
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]]))]*) |
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); |
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]))]" |
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"; |
516 then () else error "completetest.sml: new behav. in complete_mod 3"; |
517 writeln (itms2str_ ctxt mits); |
517 writeln (itms2str_ ctxt mits); |
518 (*[ |
518 (*[ |
519 (1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])), |
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])), |
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]])), |
521 (3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(valuesFor, [[a],[b]])), |