(* 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" //..............................................................

+ "<GETELEMENTSFROMTO>" //...................................................

+ "  <CALCID> 1 </CALCID>" //..........................................

+ "  <POSFORMHEADS>" //................................................

+ "    <POSFORM>" //...................................................

+ "      <GENERATED>" //...............................................

+ "        <INTLIST>" //...............................................

+ "          <INT> 4 </INT>" //........................................

+ "          <INT> 3 </INT>" //........................................

+ "        </INTLIST>" //..............................................

+ "        <POS> Res </POS>" //........................................

+ "      </GENERATED>" //..............................................

+ "      <FORMULA>" //.................................................

+ "        <MATHML>" //................................................

+ "          <ISA> -6 * x + 5 * x ^^^ 2 = 0 </ISA>" //.................

+ "        </MATHML>" //...............................................

+ "      </FORMULA>" //................................................

+ "    </POSFORM>" //..................................................

+ "    <POSHEAD>" //...................................................

+ "      <GENERATED>" //...............................................

+ "        <INTLIST>" //...............................................

+ "          <INT> 4 </INT>" //........................................

+ "          <INT> 4 </INT>" //........................................

+ "        </INTLIST>" //..............................................

+ "        <POS> Pbl </POS>" //........................................

+ "      </GENERATED>" //..............................................

+ "      <CALCHEAD status = "correct">" //.............................

+ "       <HEAD>" //...................................................

+ "         <MATHML>" //...............................................

+ "           <ISA> solve (-6 * x + 5 * x ^^^ 2 = 0, x) </ISA>" //.....

+ "         </MATHML>" //..............................................

+ "       </HEAD>" //..................................................

+ "        <MODEL>" //.................................................

+ "          <GIVEN>" //...............................................

+ "            <ITEM status="correct">" //.............................

+ "              <MATHML>" //..........................................

+ "                <ISA> equality (-6 * x + 5 * x ^^^ 2 = 0) </ISA>" //

+ "              </MATHML>" //.........................................

+ "            </ITEM>" //.............................................

+ "            <ITEM status="correct">" //.............................

+ "              <MATHML>" //..........................................

+ "                <ISA> solveFor x </ISA>" //.........................

+ "              </MATHML>" //.........................................

+ "            </ITEM>" //.............................................

+ "          </GIVEN>" //..............................................

+ "          <WHERE>" //...............................................

+ "            <ITEM status="correct">" //.............................

+ "              <MATHML>" //..........................................

+ "                <ISA> 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) </ISA>" //..

+ "              </MATHML>" //.........................................

+ "            </ITEM>" //.............................................

+ "          </WHERE>" //..............................................

+ "          <FIND>" //................................................

+ "            <ITEM status="correct">" //.............................

+ "              <MATHML>" //..........................................

+ "                <ISA> solutions x_i </ISA>" //......................

+ "              </MATHML>" //.........................................

+ "            </ITEM>" //.............................................

+ "          </FIND>" //...............................................

+ "          <RELATE>  </RELATE>" //...................................

+ "        </MODEL>" //................................................

+ "        <BELONGSTO> Pbl </BELONGSTO>" //............................

+ "        <SPECIFICATION>" //.........................................

+ "          <THEORYID> PolyEq.thy </THEORYID>" //.....................

+ "          <PROBLEMID>" //...........................................

+ "            <STRINGLIST>" //........................................

+ "              <STRING> bdv_only </STRING>" //.......................

+ "              <STRING> degree_2 </STRING>" //.......................

+ "              <STRING> polynomial </STRING>" //.....................

+ "              <STRING> univariate </STRING>" //.....................

+ "              <STRING> equation </STRING>" //.......................

+ "            </STRINGLIST>" //.......................................

+ "          </PROBLEMID>" //..........................................

+ "          <METHODID>" //............................................

+ "            <STRINGLIST>" //........................................

+ "              <STRING> PolyEq </STRING>" //.........................

+ "              <STRING> solve_d2_polyeq_bdvonly_equation </STRING>" 

+ "            </STRINGLIST>" //.......................................

+ "          </METHODID>" //...........................................

+ "        </SPECIFICATION>" //........................................

+ "      </CALCHEAD>" //...............................................

+ "    </POSHEAD>" //..................................................

+ "  <POSFORMHEADS>" //................................................

+ "</GETELEMENTSFROMTO>" //..................................................

+ "@@@@@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_ ctxt (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_ 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 ()

 else raise error "completetest.sml: new behav. in complete_mod 1";

 writeln (itms2str_ ctxt (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_ 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]))]" 

 then () else raise error "completetest.sml: new behav. in complete_mod 2";

 writeln (itms2str_ ctxt 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_ ctxt 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_ ctxt 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_ 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 ()

 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_ ctxt 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_ 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]]))]" 

 then () else raise error "completetest.sml: new behav. in complete_mod 3";

 writeln (itms2str_ ctxt 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_ 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 () else raise error "completetest.sml: new behav. in complete_mod 3";

 writeln (itms2str_ ctxt 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]))]*)