diff -r 5100a9c3abf8 -r 875b6efa7ced src/Pure/isac/smltest/ME/me.sml --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/isac/smltest/ME/me.sml Wed Jul 21 13:53:39 2010 +0200 @@ -0,0 +1,528 @@ +(* tests on me.sml + author: Walther Neuper + 060225, + (c) due to copyright terms + +use"../smltest/ME/me.sml"; +use"me.sml"; +*) + +"-----------------------------------------------------------------"; +"table of contents -----------------------------------------------"; +"-----------------------------------------------------------------"; +"=====new ptree 1: crippled by cut_level_'_ ======================"; +"-------------- get_interval from ctree with move_dn:modspec.sml -"; +"=====new ptree 2 without changes ================================"; +"-------------- getFormulaeFromTo --------------------------------"; +"autoCalculate"; +"--------- solve_linear as rootpbl AUTOCALCULATE CompleteModel ---"; +"--------- solve_linear as rootpbl AUTOCALCULATE CompleteCalcHead-"; +"--------- maximum-example: complete_metitms ---------------------"; +"--------- maximum-example: complete_mod -------------------------"; +"-----------------------------------------------------------------"; +"-----------------------------------------------------------------"; +"-----------------------------------------------------------------"; + + + +"=====new ptree 1: crippled by cut_level_'_ ======================"; +"=====new ptree 1: crippled by cut_level_'_ ======================"; +"=====new ptree 1: crippled by cut_level_'_ ======================"; +states:=[]; +CalcTree +[(["equality (x/(x^2 - 6*x+9) - 1/(x^2 - 3*x) =1/x)", + "solveFor x","solutions L"], + ("RatEq.thy",["univariate","equation"],["no_met"]))]; +Iterator 1; moveActiveRoot 1; +autoCalculate 1 CompleteCalc; + +getTactic 1 ([1],Res);(*Rewrite_Set RatEq_simplify*) +getTactic 1 ([2],Res);(*Rewrite_Set norm_Rational*) +getTactic 1 ([3],Res);(*Rewrite_Set RatEq_eliminate*) +getTactic 1 ([4,1],Res);(*Rewrite all_left*) +getTactic 1 ([4,2],Res);(*Rewrite_Set expand_binoms*) +getTactic 1 ([4,3],Res);(*Rewrite_Set_Inst make_ratpoly_in*) + +moveActiveFormula 1 ([1],Res)(*1.1...1.4*); +moveActiveFormula 1 ([2],Res)(**ME_Isa: 'expand' not known*); +moveActiveFormula 1 ([3],Res)(*3.1.*); +moveActiveFormula 1 ([4,2],Res)(*4.2.1.*); +moveActiveFormula 1 ([4,3],Res)(**one_scr_arg: called by Script Stepwise t_=*); + +moveActiveFormula 1 ([1],Res)(*1.1...1.4*); +interSteps 1 ([1],Res)(*..is activeFormula !?!*); + +getTactic 1 ([1,1],Res);(*Rewrite real_diff_minus*) +getTactic 1 ([1,2],Res);(*Rewrite real_diff_minus*) +getTactic 1 ([1,3],Res);(*Rewrite real_diff_minus*) +getTactic 1 ([1,4],Res);(*Rewrite real_rat_mult_1*) + +moveActiveFormula 1 ([4,2],Res)(*4.2.1.*); +interSteps 1 ([4,2],Res)(*..is activeFormula !?!*); +val ((pt,_),_) = get_calc 1; +writeln(pr_ptree pr_short pt); +(*delete [4,1] in order to make pos [4],[4,4] for pblobjs differen [4],[4,3]: + ###########################################################################*) +val (pt, _) = cut_level_'_ [] [] pt ([4,1],Frm); (*#*) +(*##########################################################################*) +writeln(pr_ptree pr_short pt); +(*########################################################################## + attention: the ctree in states is still the old (perfect) !!! +############################################################################*) + + + +"-------------- get_interval from ctree with move_dn:modspec.sml -"; +"-------------- get_interval from ctree with move_dn:modspec.sml -"; +"-------------- get_interval from ctree with move_dn:modspec.sml -"; +writeln(pr_ptree pr_short pt); +writeln(posterms2str (get_interval ([],Frm) ([],Res) 99999 pt)); + +case map fst (get_interval ([],Frm) ([],Res) 99999 pt) of + [([], Frm), + ([1], Frm), + ([1, 1], Frm), + ([1, 1], Res), + ([1, 2], Res), + ([1, 3], Res), + ([1, 4], Res), + ([1], Res), + ([2], Res), + ([3], Res), + ([4], Pbl), + ([4, 1], Frm), + ([4, 1, 1], Frm), + ([4, 1, 1], Res), + ([4, 1], Res), + ([4, 2], Res), + ([4, 3], Pbl), + ([4, 3, 1], Frm), + ([4, 3, 1], Res), + ([4, 3, 2], Res), + ([4, 3, 3], Res), + ([4, 3, 4], Res), + ([4, 3, 5], Res), + ([4, 3], Res), + ([4], Res), + ([5], Res), + ([], Res)] => () + | _ => raise error "diff.behav.in ctree.sml: get_interval lev 1f"; +case map fst (get_interval ([],Frm) ([],Res) 1 pt) of + [([], Frm), + ([1], Frm), + ([1], Res), + ([2], Res), + ([3], Res), + ([4], Pbl), + ([4], Res), + ([5], Res), + ([], Res)] => () + | _ => raise error "diff.behav.in ctree.sml: get_interval lev 1f"; +case map fst (get_interval ([],Frm) ([],Res) 0 pt) of + [([], Frm), + ([], Res)] => () + | _ => raise error "diff.behav.in ctree.sml: get_interval lev 1f"; + +case map fst (get_interval ([1,3],Res) ([4,1,1],Frm) 99999 pt) of + [([1, 3], Res), + ([1, 4], Res), + ([1], Res), + ([2], Res), + ([3], Res), + ([4], Pbl), + ([4, 1], Frm), + ([4, 1, 1], Frm)] => () + | _ => raise error "diff.behav.in ctree.sml: get_interval lev 1a"; + +(*this pos' is not generated bu move_dn:......vvv: goes to end of calc*) +case map fst (get_interval ([2],Res) ([4,3,2],Frm) 99999 pt) of + [([2], Res), + ([3], Res), + ([4], Pbl), + ([4, 1], Frm), + ([4, 1, 1], Frm), + ([4, 1, 1], Res), + ([4, 1], Res), + ([4, 2], Res), + ([4, 3], Pbl), + ([4, 3, 1], Frm), + ([4, 3, 1], Res), + ([4, 3, 2], Res), + ([4, 3, 3], Res),(*this is beyond 'to'*) + ([4, 3, 4], Res),(*this is beyond 'to'*) + ([4, 3, 5], Res),(*this is beyond 'to'*) + ([4, 3], Res), (*this is beyond 'to'*) + ([4], Res), (*this is beyond 'to'*) + ([5], Res), (*this is beyond 'to'*) + ([], Res)] => () (*this is beyond 'to'*) + | _ => raise error "diff.behav.in ctree.sml: get_interval lev 1b"; +case map fst (get_interval ([1,4],Res) ([4,3,1],Frm) 99999 pt) of + [([1, 4], Res), + ([1], Res), + ([2], Res), + ([3], Res), + ([4], Pbl), + ([4, 1], Frm), + ([4, 1, 1], Frm), + ([4, 1, 1], Res), + ([4, 1], Res), + ([4, 2], Res), + ([4, 3], Pbl), + ([4, 3, 1], Frm)] => () + | _ => raise error "diff.behav.in ctree.sml: get_interval lev 1c"; +case map fst (get_interval ([4,2],Res) ([5],Res) 99999 pt) of + [([4, 2], Res), + ([4, 3], Pbl), + ([4, 3, 1], Frm), + ([4, 3, 1], Res), + ([4, 3, 2], Res), + ([4, 3, 3], Res), + ([4, 3, 4], Res), + ([4, 3, 5], Res), + ([4, 3], Res), + ([4], Res), + ([5], Res)]=>() + | _ => raise error "diff.behav.in ctree.sml: get_interval lev 1d"; +case map fst (get_interval ([],Frm) ([4,3,2],Res) 99999 pt) of + [([], Frm), + ([1], Frm), + ([1, 1], Frm), + ([1, 1], Res), + ([1, 2], Res), + ([1, 3], Res), + ([1, 4], Res), + ([1], Res), + ([2], Res), + ([3], Res), + ([4], Pbl), + ([4, 1], Frm), + ([4, 1, 1], Frm), + ([4, 1, 1], Res), + ([4, 1], Res), + ([4, 2], Res), + ([4, 3], Pbl), + ([4, 3, 1], Frm), + ([4, 3, 1], Res), + ([4, 3, 2], Res)] => () + | _ => raise error "diff.behav.in ctree.sml: get_interval lev 1e"; +case map fst (get_interval ([4,3],Frm) ([4,3],Res) 99999 pt) of + [([4, 3], Frm), + ([4, 3, 1], Frm), + ([4, 3, 1], Res), + ([4, 3, 2], Res), + ([4, 3, 3], Res), + ([4, 3, 4], Res), + ([4, 3, 5], Res), + ([4, 3], Res)] => () + | _ => raise error "diff.behav.in ctree.sml: get_interval lev 1g"; + + + + +"=====new ptree 2 without changes ================================"; +"=====new ptree 2 without changes ================================"; +"=====new ptree 2 without changes ================================"; +states:=[]; +CalcTree +[(["equality (x/(x^2 - 6*x+9) - 1/(x^2 - 3*x) =1/x)", + "solveFor x","solutions L"], + ("RatEq.thy",["univariate","equation"],["no_met"]))]; +Iterator 1; moveActiveRoot 1; +autoCalculate 1 CompleteCalc; +val ((pt,_),_) = get_calc 1; +writeln(pr_ptree pr_short pt); + + +"-------------- getFormulaeFromTo --------------------------------"; +"-------------- getFormulaeFromTo --------------------------------"; +"-------------- getFormulaeFromTo --------------------------------"; +getFormulaeFromTo 1 ([4, 2], Res) ([4, 4], Pbl) 000; +(* +"@@@@@begin@@@@@" //................................................... ++ " 1" //.............................................................. ++ "" //................................................... ++ " 1 " //.......................................... ++ " " //................................................ ++ " " //................................................... ++ " " //............................................... ++ " " //............................................... ++ " 4 " //........................................ ++ " 3 " //........................................ ++ " " //.............................................. ++ " Res " //........................................ ++ " " //.............................................. ++ " " //................................................. ++ " " //................................................ ++ " -6 * x + 5 * x ^^^ 2 = 0 " //................. ++ " " //............................................... ++ " " //................................................ ++ " " //.................................................. ++ " " //................................................... ++ " " //............................................... ++ " " //............................................... ++ " 4 " //........................................ ++ " 4 " //........................................ ++ " " //.............................................. ++ " Pbl " //........................................ ++ " " //.............................................. ++ " " //............................. ++ " " //................................................... ++ " " //............................................... ++ " solve (-6 * x + 5 * x ^^^ 2 = 0, x) " //..... ++ " " //.............................................. ++ " " //.................................................. ++ " " //................................................. ++ " " //............................................... ++ " " //............................. ++ " " //.......................................... ++ " equality (-6 * x + 5 * x ^^^ 2 = 0) " // ++ " " //......................................... ++ " " //............................................. ++ " " //............................. ++ " " //.......................................... ++ " solveFor x " //......................... ++ " " //......................................... ++ " " //............................................. ++ " " //.............................................. ++ " " //............................................... ++ " " //............................. ++ " " //.......................................... ++ " matches (?a * ?v_ + ?v_ ^^^ 2 = 0) (-6 * x + 5 * x ^^^ 2 = 0) |" ++ "matches (?v_ + ?v_ ^^^ 2 = 0) (-6 * x + 5 * x ^^^ 2 = 0) |" //...... ++ "matches (?v_ + ?b * ?v_ ^^^ 2 = 0) (-6 * x + 5 * x ^^^ 2 = 0) |" ++ "matches (?a * ?v_ + ?b * ?v_ ^^^ 2 = 0) (-6 * x + 5 * x ^^^ 2 = 0) |" ++ "matches (?v_ ^^^ 2 = 0) (-6 * x + 5 * x ^^^ 2 = 0) |" //............ ++ "matches (?b * ?v_ ^^^ 2 = 0) (-6 * x + 5 * x ^^^ 2 = 0) " //.. ++ " " //......................................... ++ " " //............................................. ++ " " //.............................................. ++ " " //................................................ ++ " " //............................. ++ " " //.......................................... ++ " solutions x_i " //...................... ++ " " //......................................... ++ " " //............................................. ++ " " //............................................... ++ " " //................................... ++ " " //................................................ ++ " Pbl " //............................ ++ " " //......................................... ++ " PolyEq.thy " //..................... ++ " " //........................................... ++ " " //........................................ ++ " bdv_only " //....................... ++ " degree_2 " //....................... ++ " polynomial " //..................... ++ " univariate " //..................... ++ " equation " //....................... ++ " " //....................................... ++ " " //.......................................... ++ " " //............................................ ++ " " //........................................ ++ " PolyEq " //......................... ++ " solve_d2_polyeq_bdvonly_equation " ++ " " //....................................... ++ " " //........................................... ++ " " //........................................ ++ " " //............................................... ++ " " //.................................................. ++ " " //................................................ ++ "" //.................................................. ++ "@@@@@end@@@@@" +*) + + +"--------- solve_linear as rootpbl AUTOCALCULATE CompleteModel ---"; +"--------- solve_linear as rootpbl AUTOCALCULATE CompleteModel ---"; +"--------- solve_linear as rootpbl AUTOCALCULATE CompleteModel ---"; + val c = []; + val (p,_,f,nxt,_,pt) = CalcTreeTEST + [(["equality (1+-1*2+x=0)", "solveFor x","solutions L"], + ("Test.thy", + ["linear","univariate","equation","test"], + ["Test","solve_linear"]))]; + val (p,_,f,nxt,_,pt) = me nxt p c pt; + val (p,_,f,nxt,_,pt) = me nxt p c pt; + (*xt = Add_Given "solveFor x"*) + writeln (itms2str thy (get_obj g_pbl pt (fst p))); +(*[ +(0 ,[] ,false ,#Given ,Inc solveFor ,(??.empty, [])), +(0 ,[] ,false ,#Find ,Inc solutions [] ,(??.empty, [])), +(1 ,[1] ,true ,#Given ,Cor equality (1 + -1 * 2 + x = 0) ,(e_, [1 + -1 * 2 + x = 0]))]*) + val (pt,p) = complete_mod (pt, p); + if itms2str thy (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 () + else raise error "completetest.sml: new behav. in complete_mod 1"; + writeln (itms2str thy (get_obj g_pbl pt (fst p))); +(*[ +(1 ,[1] ,true ,#Given ,Cor equality (1 + -1 * 2 + x = 0) ,(e_, [1 + -1 * 2 + x = 0])), +(2 ,[1] ,true ,#Given ,Cor solveFor x ,(solveFor, [x])), +(3 ,[1] ,true ,#Find ,Cor solutions L ,(solutions, [L]))]*) + val mits = get_obj g_met pt (fst p); + if itms2str thy 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]))]" + then () else raise error "completetest.sml: new behav. in complete_mod 2"; + writeln (itms2str thy mits); +(*[ +(1 ,[1] ,true ,#Given ,Cor equality (1 + -1 * 2 + x = 0) ,(e_, [1 + -1 * 2 + x = 0])), +(2 ,[1] ,true ,#Given ,Cor solveFor x ,(solveFor, [x])), +(3 ,[1] ,true ,#Find ,Cor solutions L ,(solutions, [L]))]*) + + + +"--------- solve_linear as rootpbl AUTOCALCULATE CompleteCalcHead-"; +"--------- solve_linear as rootpbl AUTOCALCULATE CompleteCalcHead-"; +"--------- solve_linear as rootpbl AUTOCALCULATE CompleteCalcHead-"; + states:=[]; + CalcTree (*start of calculation, return No.1*) + [(["equality (1+-1*2+x=0)", "solveFor x","solutions L"], + ("Test.thy", + ["linear","univariate","equation","test"], + ["Test","solve_linear"]))]; + Iterator 1; moveActiveRoot 1; + +(* + autoCalculate 1 CompleteCalcHead; + autoCalculate 1 (Step 1); + refFormula 1 (get_pos 1 1); + +... works + + autoCalculate 1 CompleteCalcHead; + fetchProposedTactic 1; (*-> Apply_Method*); + setNextTactic 1 (Apply_Method ["Test","solve_linear"]); + autoCalculate 1 (Step 1); + refFormula 1 (get_pos 1 1); + +... works *) + + autoCalculate 1 (Step 1); + refFormula 1 (get_pos 1 1); + + autoCalculate 1 CompleteModel; + refFormula 1 (get_pos 1 1); + + autoCalculate 1 CompleteCalcHead; +(* *** complete_mod: only impl.for Pbl, called with ([], Met) FIXXXXXXXXXXME*) + + + +"--------- maximum-example: complete_metitms ---------------------"; +"--------- maximum-example: complete_metitms ---------------------"; +"--------- maximum-example: complete_metitms ---------------------"; + val (p,_,f,nxt,_,pt) = + CalcTreeTEST + [(["fixedValues [r=Arbfix]","maximum A", + "valuesFor [a,b]", + "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]", + "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]", + "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]", + + "boundVariable a","boundVariable b","boundVariable alpha", + "interval {x::real. 0 <= x & x <= 2*r}", + "interval {x::real. 0 <= x & x <= 2*r}", + "interval {x::real. 0 <= x & x <= pi}", + "errorBound (eps=(0::real))"], + ("DiffApp.thy",["maximum_of","function"],["DiffApp","max_by_calculus"]) + )]; + val (p,_,f,nxt,_,pt) = me nxt p c pt; + val (p,_,f,nxt,_,pt) = me nxt p c pt; + val (p,_,f,nxt,_,pt) = me nxt p c pt; + val (p,_,f,nxt,_,pt) = me nxt p c pt; + val (p,_,f,nxt,_,pt) = (me nxt p c pt) handle e => print_exn e; + val (p,_,f,nxt,_,pt) = me nxt p c pt; + val (p,_,f,nxt,_,pt) = me nxt p c pt; + (*nxt = Specify_Theory "DiffApp.thy"*) + val (oris, _, _) = get_obj g_origin pt (fst p); + writeln (oris2str oris); +(*[ +(1, ["1","2","3"], #Given,fixedValues, ["[r = Arbfix]"]), +(2, ["1","2","3"], #Find,maximum, ["A"]), +(3, ["1","2","3"], #Find,valuesFor, ["[a]","[b]"]), +(4, ["1","2"], #Relate,relations, ["[A = a * b]","[(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]"]), +(5, ["3"], #Relate,relations, ["[A = a * b]","[a / 2 = r * sin alpha]","[b / 2 = r * cos alpha]"]), +(6, ["1"], #undef,boundVariable, ["a"]), +(7, ["2"], #undef,boundVariable, ["b"]), +(8, ["3"], #undef,boundVariable, ["alpha"]), +(9, ["1","2"], #undef,interval, ["{x. 0 <= x & x <= 2 * r}"]), +(10, ["3"], #undef,interval, ["{x. 0 <= x & x <= pi}"]), +(11, ["1","2","3"], #undef,errorBound, ["eps = 0"])]*) + val pits = get_obj g_pbl pt (fst p); + writeln (itms2str thy pits); +(*[ +(1 ,[1,2,3] ,true,#Given ,Cor fixedValues [r = Arbfix],(fix_, [[r = Arbfix]])), +(2 ,[1,2,3] ,true,#Find ,Cor maximum A ,(m_, [A])), +(3 ,[1,2,3] ,true,#Find ,Cor valuesFor [a, b] ,(vs_, [[a, b]])), +(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]]))]*) + val mits = get_obj g_met pt (fst p); + val mits = complete_metitms oris pits [] + ((#ppc o get_met) ["DiffApp","max_by_calculus"]); + writeln (itms2str thy mits); +(*[ +(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])), +(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])), +(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(vs_, [[a, b]])), +(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]])), +(6 ,[1] ,true ,#undef ,Cor boundVariable a ,(boundVariable, [a])), +(9 ,[1,2] ,true ,#undef ,Cor interval {x. 0 <= x & x <= 2 * r} ,(interval, [{x. +0 <= x & x <= 2 * r}])), +(11 ,[1,2,3] ,true ,#undef ,Cor errorBound (eps = 0) ,(errorBound, [eps = 0]))]*) + if itms2str thy 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 () + else raise error "completetest.sml: new behav. in complete_metitms 1"; + + +"--------- maximum-example: complete_mod -------------------------"; +"--------- maximum-example: complete_mod -------------------------"; +"--------- maximum-example: complete_mod -------------------------"; + val (p,_,f,nxt,_,pt) = + CalcTreeTEST + [(["fixedValues [r=Arbfix]","maximum A", + "valuesFor [a,b]", + "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]", + "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]", + "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]", + + "boundVariable a","boundVariable b","boundVariable alpha", + "interval {x::real. 0 <= x & x <= 2*r}", + "interval {x::real. 0 <= x & x <= 2*r}", + "interval {x::real. 0 <= x & x <= pi}", + "errorBound (eps=(0::real))"], + ("DiffApp.thy",["maximum_of","function"],["DiffApp","max_by_calculus"]) + )]; + val (p,_,f,nxt,_,pt) = me nxt p c pt; + val (p,_,f,nxt,_,pt) = me nxt p c pt; + val (p,_,f,nxt,_,pt) = me nxt p c pt; + (*nxt = nxt = Add_Find "valuesFor [a]" FIXME.12.03 +handle Inc !*) + val pits = get_obj g_pbl pt (fst p); + writeln (itms2str thy pits); +(*[ +(0 ,[] ,false ,#Find ,Inc valuesFor ,(??.empty, [])), +(0 ,[] ,false ,#Relate ,Inc relations [] ,(??.empty, [])), +(1 ,[1,2,3] ,true,#Given,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])), +(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A]))]*) + val (pt,p) = complete_mod (pt,p); + val pits = get_obj g_pbl pt (fst p); + if itms2str thy 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]]))]" + then () else raise error "completetest.sml: new behav. in complete_mod 3"; + writeln (itms2str thy pits); +(*[ +(1 ,[1,2,3] ,true,#Given,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])), +(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])), +(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(valuesFor, [[a],[b]])), +(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ +2 = r ^^^ 2] ,(relations, [[A = a * b],[(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]]))]*) + val mits = get_obj g_met pt (fst p); + if itms2str thy 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 () else raise error "completetest.sml: new behav. in complete_mod 3"; + writeln (itms2str thy mits); +(*[ +(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])), +(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])), +(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(valuesFor, [[a],[b]])), +(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ +2 = r ^^^ 2] ,(relations, [[A = a * b],[(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]])), +(6 ,[1] ,true ,#undef ,Cor boundVariable a ,(boundVariable, [a])), +(9 ,[1,2] ,true ,#undef ,Cor interval {x. 0 <= x & x <= 2 * r} ,(interval, [{x. +0 <= x & x <= 2 * r}])), +(11 ,[1,2,3] ,true ,#undef ,Cor errorBound (eps = 0) ,(errorBound, [eps = 0]))]*) +