(* tests on inform.sml

   author: Walther Neuper

   060225,

   (c) due to copyright terms 

use"../smltest/ME/inform.sml";

use"inform.sml";

*)

"-----------------------------------------------------------------";

"table of contents -----------------------------------------------";

"-----------------------------------------------------------------";

"appendForm with miniscript with mini-subpbl:";

"--------- appendFormula: on Res + equ_nrls ----------------------";

"--------- appendFormula: on Frm + equ_nrls ----------------------";

"--------- appendFormula: on Res + NO deriv ----------------------";

"--------- appendFormula: on Res + late deriv --------------------";

"--------- appendFormula: on Res + late deriv [x = 3 + -2]---///--";

"replaceForm with miniscript with mini-subpbl:";

"--------- replaceFormula: on Res + = ----------------------------";

"--------- replaceFormula: on Res + = 1st Nd ---------------------";

"--------- replaceFormula: on Frm + = 1st Nd ---------------------";

"--------- replaceFormula: cut calculation -----------------------";

"--------- replaceFormula: cut calculation -----------------------";

(* 040307 copied from informtest.sml ... old versions

"--------- maximum-example, UC: Modeling / modifyCalcHead --------";*)

"--------- syntax error ------------------------------------------";

"CAS-command:";

"--------- CAS-command on ([],Pbl) -------------------------------";

"--------- CAS-command on ([],Pbl) FE-interface ------------------";

"--------- inform [rational,simplification] ----------------------";

"-----------------------------------------------------------------";

"-----------------------------------------------------------------";

"-----------------------------------------------------------------";

"--------- appendFormula: on Res + equ_nrls ----------------------";

"--------- appendFormula: on Res + equ_nrls ----------------------";

"--------- appendFormula: on Res + equ_nrls ----------------------";

 val Script sc = (#scr o get_met) ["Test","squ-equ-test-subpbl1"];

 (writeln o term2str) sc;

 val Script sc = (#scr o get_met) ["Test","solve_linear"];

 (writeln o term2str) sc;

 states:=[];

 CalcTree [(["equality (x+1=2)", "solveFor x","solutions L"], 

	    ("Test.thy", 

	     ["sqroot-test","univariate","equation","test"],

	     ["Test","squ-equ-test-subpbl1"]))];

 Iterator 1; moveActiveRoot 1;

 autoCalculate 1 CompleteCalcHead;

 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)

 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);

 appendFormula 1 "-2 * 1 + (1 + x) = 0"; refFormula 1 (get_pos 1 1);

 val ((pt,_),_) = get_calc 1;

 val str = pr_ptree pr_short pt;

 writeln str;

 if str = ".    ----- pblobj -----\n1.   x + 1 = 2\n2.   x + 1 + -1 * 2 = 0\n2.1.   x + 1 + -1 * 2 = 0\n2.2.   -1 * 2 + (x + 1) = 0\n2.3.   -1 * 2 + (1 + x) = 0\n2.4.   1 + (-1 * 2 + x) = 0\n2.5.   1 + (-2 + x) = 0\n2.6.   1 + (-2 * 1 + x) = 0\n" then ()

 else raise error "inform.sml: diff.behav.appendFormula: on Res + equ 1";

 moveDown 1 ([ ],Pbl); refFormula 1 ([1],Frm); (*x + 1 = 2*)

 moveDown 1 ([1],Frm); refFormula 1 ([1],Res); (*x + 1 + -1 * 2 = 0*)

 (*the seven steps of detailed derivation*)

 moveDown 1 ([1  ],Res); refFormula 1 ([2,1],Frm); 

 moveDown 1 ([2,1],Frm); refFormula 1 ([2,1],Res);

 moveDown 1 ([2,1],Res); refFormula 1 ([2,2],Res);

 moveDown 1 ([2,2],Res); refFormula 1 ([2,3],Res); 

 moveDown 1 ([2,3],Res); refFormula 1 ([2,4],Res);

 moveDown 1 ([2,4],Res); refFormula 1 ([2,5],Res);

 moveDown 1 ([2,5],Res); refFormula 1 ([2,6],Res);

 val ((pt,_),_) = get_calc 1;

 if "-2 * 1 + (1 + x) = 0" = term2str (fst (get_obj g_result pt [2,6])) then()

 else raise error "inform.sml: diff.behav.appendFormula: on Res + equ 2";

 fetchProposedTactic 1; (*takes Iterator 1 _1_*)

 val (_,(tac,_,_)::_) = get_calc 1;

 if tac = Rewrite_Set "Test_simplify" then ()

 else raise error "inform.sml: diff.behav.appendFormula: on Res + equ 3";

 autoCalculate 1 CompleteCalc;

 val ((pt,_),_) = get_calc 1;

 if "[x = 1]" = term2str (fst (get_obj g_result pt [])) then ()

 else raise error "inform.sml: diff.behav.appendFormula: on Res + equ 4";

 (* autoCalculate 1 CompleteCalc;

   val ((pt,p),_) = get_calc 1;

   (writeln o istates2str) (get_obj g_loc pt [ ]);  

   (writeln o istates2str) (get_obj g_loc pt [1]);  

   (writeln o istates2str) (get_obj g_loc pt [2]);  

   (writeln o istates2str) (get_obj g_loc pt [3]);  

   (writeln o istates2str) (get_obj g_loc pt [3,1]);  

   (writeln o istates2str) (get_obj g_loc pt [3,2]);  

   (writeln o istates2str) (get_obj g_loc pt [4]);  

   *)

"----------------------------------------------------------";

 val fod = make_deriv Isac.thy Atools_erls 

		       ((#rules o rep_rls) Test_simplify)

		       (sqrt_right false ProtoPure.thy) None 

		       (str2term "x + 1 + -1 * 2 = 0");

 (writeln o trtas2str) fod;

 val ifod = make_deriv Isac.thy Atools_erls 

		       ((#rules o rep_rls) Test_simplify)

		       (sqrt_right false ProtoPure.thy) None 

		       (str2term "-2 * 1 + (1 + x) = 0");

 (writeln o trtas2str) ifod;

 fun equal (_,_,(t1, _)) (_,_,(t2, _)) = t1=t2;

 val (fod', rifod') = dropwhile' equal (rev fod) (rev ifod);

 val der = fod' @ (map rev_deriv' rifod');

 (writeln o trtas2str) der;

 "----------------------------------------------------------";

"--------- appendFormula: on Frm + equ_nrls ----------------------";

"--------- appendFormula: on Frm + equ_nrls ----------------------";

"--------- appendFormula: on Frm + equ_nrls ----------------------";

 states:=[];

 CalcTree [(["equality (x+1=2)", "solveFor x","solutions L"], 

	    ("Test.thy", 

	     ["sqroot-test","univariate","equation","test"],

	     ["Test","squ-equ-test-subpbl1"]))];

 Iterator 1; moveActiveRoot 1;

 autoCalculate 1 CompleteCalcHead;

 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1) (*x + 1 = 2*);

 appendFormula 1 "2+ -1 + x = 2"; refFormula 1 (get_pos 1 1);

 moveDown 1 ([],Pbl); refFormula 1 ([1],Frm) (*x + 1 = 2*);

 moveDown 1 ([1  ],Frm); refFormula 1 ([1,1],Frm); 

 moveDown 1 ([1,1],Frm); refFormula 1 ([1,1],Res); 

 moveDown 1 ([1,1],Res); refFormula 1 ([1,2],Res); 

 moveDown 1 ([1,2],Res); refFormula 1 ([1,3],Res); 

 moveDown 1 ([1,3],Res); refFormula 1 ([1,4],Res); 

 moveDown 1 ([1,4],Res); refFormula 1 ([1,5],Res); 

 moveDown 1 ([1,5],Res); refFormula 1 ([1,6],Res); 

 val ((pt,_),_) = get_calc 1;

 if "2 + -1 + x = 2" = term2str (fst (get_obj g_result pt [1,6])) then()

 else raise error "inform.sml: diff.behav.appendFormula: on Frm + equ 1";

 fetchProposedTactic 1; (*takes Iterator 1 _1_*)

 val (_,(tac,_,_)::_) = get_calc 1;

 if tac = Rewrite_Set "norm_equation" then ()

 else raise error "inform.sml: diff.behav.appendFormula: on Frm + equ 2";

 autoCalculate 1 CompleteCalc;

 val ((pt,_),_) = get_calc 1;

 if "[x = 1]" = term2str (fst (get_obj g_result pt [])) then ()

 else raise error "inform.sml: diff.behav.appendFormula: on Frm + equ 3";

"--------- appendFormula: on Res + NO deriv ----------------------";

"--------- appendFormula: on Res + NO deriv ----------------------";

"--------- appendFormula: on Res + NO deriv ----------------------";

 states:=[];

 CalcTree [(["equality (x+1=2)", "solveFor x","solutions L"], 

	    ("Test.thy", 

	     ["sqroot-test","univariate","equation","test"],

	     ["Test","squ-equ-test-subpbl1"]))];

 Iterator 1; moveActiveRoot 1;

 autoCalculate 1 CompleteCalcHead;

 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)

 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);

 appendFormula 1 "x = 2";

 val ((pt,p),_) = get_calc 1;

 val str = pr_ptree pr_short pt;

 writeln str;

 if str = ".    ----- pblobj -----\n1.   x + 1 = 2\n" andalso p = ([1], Res)

 then ()

 else raise error "inform.sml: diff.behav.appendFormula: Res + NOder 1";

 fetchProposedTactic 1;

 val (_,(tac,_,_)::_) = get_calc 1;

 if tac = Rewrite_Set "Test_simplify" then ()

 else raise error "inform.sml: diff.behav.appendFormula: Res + NOder 2";

 autoCalculate 1 CompleteCalc;

 val ((pt,_),_) = get_calc 1;

 if "[x = 1]" = term2str (fst (get_obj g_result pt [])) then ()

 else raise error "inform.sml: diff.behav.appendFormula: on Frm + equ 3";

"--------- appendFormula: on Res + late deriv --------------------";

"--------- appendFormula: on Res + late deriv --------------------";

"--------- appendFormula: on Res + late deriv --------------------";

 states:=[];

 CalcTree [(["equality (x+1=2)", "solveFor x","solutions L"], 

	    ("Test.thy", 

	     ["sqroot-test","univariate","equation","test"],

	     ["Test","squ-equ-test-subpbl1"]))];

 Iterator 1; moveActiveRoot 1;

 autoCalculate 1 CompleteCalcHead;

 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)

 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);

 appendFormula 1 "x = 1";

 val ((pt,p),_) = get_calc 1;

 val str = pr_ptree pr_short pt;

 writeln str;

 if str = ".    ----- pblobj -----\n1.   x + 1 = 2\n2.   x + 1 + -1 * 2 = 0\n3.    ----- pblobj -----\n3.1.   -1 + x = 0\n3.2.   x = 0 + -1 * -1\n3.2.1.   x = 0 + -1 * -1\n3.2.2.   x = 0 + 1\n" andalso p = ([3,2], Res)

 then () (*finds 1 step too early: ([3,2], Res) "x = 1" also by script !!!*)

 else raise error "inform.sml: diff.behav.appendFormula: Res + late d 1";

 fetchProposedTactic 1;

 val (_,(tac,_,_)::_) = get_calc 1;

 if tac = Check_Postcond ["linear", "univariate", "equation", "test"] then ()

 else raise error "inform.sml: diff.behav.appendFormula: Res + late d 2";

 autoCalculate 1 CompleteCalc;

 val ((pt,_),_) = get_calc 1;

 if "[x = 1]" = term2str (fst (get_obj g_result pt [])) then ()

 else raise error "inform.sml: diff.behav.appendFormula: Res + late d 3";

"--------- appendFormula: on Res + late deriv [x = 3 + -2]---///--";

"--------- appendFormula: on Res + late deriv [x = 3 + -2]---///--";

"--------- appendFormula: on Res + late deriv [x = 3 + -2]---///--";

 states:=[];

 CalcTree [(["equality (x+1=2)", "solveFor x","solutions L"], 

	    ("Test.thy", 

	     ["sqroot-test","univariate","equation","test"],

	     ["Test","squ-equ-test-subpbl1"]))];

 Iterator 1; moveActiveRoot 1;

 autoCalculate 1 CompleteCalcHead;

 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)

 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);

 appendFormula 1 "[x = 3 + -2*1]";

 val ((pt,p),_) = get_calc 1;

 val str = pr_ptree pr_short pt;

 writeln str;

 if str=".    ----- pblobj -----\n1.   x + 1 = 2\n2.   x + 1 + -1 * 2 = 0\n3.    ----- pblobj -----\n3.1.   -1 + x = 0\n3.2.   x = 0 + -1 * -1\n4.   [x = 1]\n4.1.   [x = 1]\n4.2.   [x = -2 + 3]\n4.3.   [x = 3 + -2]\n" then ()

 else raise error "inform.sml: diff.behav.appendFormula: Res + latEE 1";

 autoCalculate 1 CompleteCalc;

 val ((pt,p),_) = get_calc 1;

 if "[x = 3 + -2 * 1]" = term2str (fst (get_obj g_result pt [])) then ()

 (*       ~~~~~~~~~~ simplify as last step in any script ?!*)

 else raise error "inform.sml: diff.behav.appendFormula: Res + latEE 2";

"--------- replaceFormula: on Res + = ----------------------------";

"--------- replaceFormula: on Res + = ----------------------------";

"--------- replaceFormula: on Res + = ----------------------------";

 states:=[];

 CalcTree [(["equality (x+1=2)", "solveFor x","solutions L"], 

	    ("Test.thy", 

	     ["sqroot-test","univariate","equation","test"],

	     ["Test","squ-equ-test-subpbl1"]))];

 Iterator 1; moveActiveRoot 1;

 autoCalculate 1 CompleteCalcHead;

 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)

 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);

 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*-1 + x*);

 replaceFormula 1 "-2 * 1 + (1 + x) = 0"; refFormula 1 (get_pos 1 1);

 val ((pt,_),_) = get_calc 1;

 val str = pr_ptree pr_short pt;

 writeln str;

 if str=".    ----- pblobj -----\n1.   x + 1 = 2\n2.   x + 1 + -1 * 2 = 0\n2.1.   x + 1 + -1 * 2 = 0\n2.2.   -1 * 2 + (x + 1) = 0\n2.3.   -1 * 2 + (1 + x) = 0\n2.4.   1 + (-1 * 2 + x) = 0\n2.5.   1 + (-2 + x) = 0\n2.6.   1 + (-2 * 1 + x) = 0\n" then()

 else raise error "inform.sml: diff.behav.replaceFormula: on Res += 1";

 autoCalculate 1 CompleteCalc;

 val ((pt,pos as(p,_)),_) = get_calc 1;

 if pos=([],Res)andalso"[x = 1]"=(term2str o fst)(get_obj g_result pt p)then()

 else raise error "inform.sml: diff.behav.replaceFormula: on Res + = 2";

"--------- replaceFormula: on Res + = 1st Nd ---------------------";

"--------- replaceFormula: on Res + = 1st Nd ---------------------";

"--------- replaceFormula: on Res + = 1st Nd ---------------------";

 states:=[];

 CalcTree [(["equality (x+1=2)", "solveFor x","solutions L"], 

	    ("Test.thy", 

	     ["sqroot-test","univariate","equation","test"],

	     ["Test","squ-equ-test-subpbl1"]))];

 Iterator 1; moveActiveRoot 1;

 autoCalculate 1 CompleteCalcHead;

 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)

 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);

 replaceFormula 1 "x + 1 = 4 + -2"; refFormula 1 (get_pos 1 1);

 val ((pt,_),_) = get_calc 1;

 val str = pr_ptree pr_short pt;

 writeln str;

 if str=".    ----- pblobj -----\n1.   x + 1 = 2\n1.1.   x + 1 = 2\n1.2.   1 + x = 2\n1.3.   1 + x = -2 + 4\n1.4.   x + 1 = -2 + 4\n" then ()

 else raise error "inform.sml: diff.behav.replaceFormula: on Res 1 + = 1";

 autoCalculate 1 CompleteCalc;

 val ((pt,pos as(p,_)),_) = get_calc 1;

 if pos=([],Res)andalso"[x = 1]"=(term2str o fst)(get_obj g_result pt p)then()

 else raise error "inform.sml: diff.behav.replaceFormula: on Res + = 2";

"--------- replaceFormula: on Frm + = 1st Nd ---------------------";

"--------- replaceFormula: on Frm + = 1st Nd ---------------------";

"--------- replaceFormula: on Frm + = 1st Nd ---------------------";

 states:=[];

 CalcTree [(["equality (x+1=2)", "solveFor x","solutions L"], 

	    ("Test.thy", 

	     ["sqroot-test","univariate","equation","test"],

	     ["Test","squ-equ-test-subpbl1"]))];

 Iterator 1; moveActiveRoot 1;

 autoCalculate 1 CompleteCalcHead;

 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)

 replaceFormula 1 "x + 1 = 4 + -2"; refFormula 1 (get_pos 1 1);

 val ((pt,_),_) = get_calc 1;

 val str = pr_ptree pr_short pt;

 writeln str;

 if str=".    ----- pblobj -----\n1.   x + 1 = 2\n1.1.   x + 1 = 2\n1.2.   1 + x = 2\n1.3.   1 + x = -2 + 4\n1.4.   x + 1 = -2 + 4\n" then ()

 else raise error "inform.sml: diff.behav.replaceFormula: on Frm 1 + = 1";

 autoCalculate 1 CompleteCalc;

 val ((pt,pos as(p,_)),_) = get_calc 1;

 if pos=([],Res)andalso"[x = 1]"=(term2str o fst)(get_obj g_result pt p)then()

 else raise error "inform.sml: diff.behav.replaceFormula: on Frm 1 + = 2";

"--------- replaceFormula: cut calculation -----------------------";

"--------- replaceFormula: cut calculation -----------------------";

"--------- replaceFormula: cut calculation -----------------------";

 states:=[];

 CalcTree [(["equality (x+1=2)", "solveFor x","solutions L"], 

	    ("Test.thy", 

	     ["sqroot-test","univariate","equation","test"],

	     ["Test","squ-equ-test-subpbl1"]))];

 Iterator 1; moveActiveRoot 1;

 autoCalculate 1 CompleteCalc;

 moveActiveRoot 1; moveActiveDown 1;

 if get_pos 1 1 = ([1], Frm) then ()

 else raise error "inform.sml: diff.behav. cut calculation 1";

 replaceFormula 1 "x + 1 = 4 + -2"; refFormula 1 (get_pos 1 1);

 val ((pt,p),_) = get_calc 1;

 val str = pr_ptree pr_short pt;

 writeln str;

 if p = ([1], Res) then ()

 else raise error "inform.sml: diff.behav. cut calculation 2";

(* 040307 copied from informtest.sml; ... old version 

 "---------------- maximum-example, UC: Modeling / modifyCalcHead -";

 "---------------- maximum-example, UC: Modeling / modifyCalcHead -";

 "---------------- maximum-example, UC: Modeling / modifyCalcHead -";

 val p = ([],Pbl);

 val elems = ["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]",

	      (*^^^ these are the elements for the root-problem (in variants)*)

              (*vvv these are elements required for subproblems*)

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

 (*specifying is not interesting for this example*)

 val spec = ("DiffApp.thy", ["maximum_of","function"], 

	     ["DiffApp","max_by_calculus"]);

 (*the empty model with descriptions for user-guidance by Model_Problem*)

 val empty_model = [Given ["fixedValues []"],

		    Find ["maximum", "valuesFor"],

		    Relate ["relations []"]];

 (*!!!!!!!!!!!!!!!!! DON'T USE me FOR FINDING nxt !!!!!!!!!!!!!!!!!!*)

 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(elems, spec)];

 (*val nxt = ("Model_Problem", ...*)

 val pbl = get_obj g_pbl pt (fst p); (writeln o (itms2str thy)) pbl; 

 val (p,_,f,nxt,_,pt) = me nxt p c pt;

 (*nxt = Add_Given "fixedValues [r = Arbfix]"*)

 val pbl = get_obj g_pbl pt (fst p); (writeln o (itms2str thy)) pbl; 

(*[

(0 ,[] ,false ,#Given ,Inc fixedValues [] ,(??.empty, [])),

(0 ,[] ,false ,#Find ,Inc maximum ,(??.empty, [])),

(0 ,[] ,false ,#Find ,Inc valuesFor ,(??.empty, [])),

(0 ,[] ,false ,#Relate ,Inc relations [] ,(??.empty, []))]*)

 (*the empty CalcHead is checked w.r.t the model and re-established as such*)

 val (b,pt,ocalhd) = input_icalhd pt (p,"", empty_model, Pbl, e_spec);

 val pbl = get_obj g_pbl pt (fst p); (writeln o (itms2str thy)) pbl; 

 if ocalhd2str ocalhd = "(Pbl, ??.empty, [\n(0 ,[] ,false ,#Given ,Inc fixedValues [] ,(??.empty, [])),\n(0 ,[] ,false ,#Find ,Inc maximum ,(??.empty, [])),\n(0 ,[] ,false ,#Find ,Inc valuesFor ,(??.empty, [])),\n(0 ,[] ,false ,#Relate ,Inc relations [] ,(??.empty, []))], [], \n(\"e_domID\", [\"e_pblID\"], [\"e_metID\"]) )" then () else raise error "informtest.sml: diff.behav. max 1";

 (*there is one input to the model (could be more)*)

 val (b,pt,ocalhd) = 

     input_icalhd pt (p,"", [Given ["fixedValues [r=Arbfix]"],

			     Find ["maximum", "valuesFor"],

			     Relate ["relations"]], Pbl, e_spec);

 val pbl = get_obj g_pbl pt (fst p); (writeln o (itms2str thy)) pbl; 

 if ocalhd2str ocalhd = "(Pbl, ??.empty, [\n(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),\n(0 ,[] ,false ,#Find ,Inc maximum ,(??.empty, [])),\n(0 ,[] ,false ,#Find ,Inc valuesFor ,(??.empty, [])),\n(0 ,[] ,false ,#Relate ,Inc relations [] ,(??.empty, []))], [], \n(\"e_domID\", [\"e_pblID\"], [\"e_metID\"]) )" then () 

 else raise error "informtest.sml: diff.behav. max 2";

 (*this input is complete in variant 3, but the ME doesn't recognize FIXXXXME

 val (b,pt''''',ocalhd) = 

     input_icalhd pt (p,"", [Given ["fixedValues [r=Arbfix]"],

			     Find ["maximum A", "valuesFor [a,b]"],

			     Relate ["relations [A=a*b, a/2=r*sin alpha, \

				     \b/2=r*cos alpha]"]], Pbl, e_spec);

 val pbl = get_obj g_pbl pt''''' (fst p); (writeln o (itms2str thy)) pbl; 

 if ocalhd2str ocalhd = ------------^^^^^^^^^^ missing !!!*)

 (*this input is complete in variant 1 (variant 3 does not work yet)*)

 val (b,pt''''',ocalhd) = 

     input_icalhd pt (p,"", [Given ["fixedValues [r=Arbfix]"],

			     Find ["maximum A", "valuesFor [a,b]"],

			     Relate ["relations [A=a*b, \

				     \(a/2)^^^2 + (b/2)^^^2 = r^^^2]"]], 

		      Pbl, e_spec);

 val pbl = get_obj g_pbl pt''''' (fst p); (writeln o (itms2str thy)) pbl; 

 modifycalcheadOK2xml 111 (bool2str b) ocalhd;

*)

"--------- syntax error ------------------------------------------";

"--------- syntax error ------------------------------------------";

"--------- syntax error ------------------------------------------";

 states:=[];

 CalcTree [(["equality (x+1=2)", "solveFor x","solutions L"], 

	    ("Test.thy", 

	     ["sqroot-test","univariate","equation","test"],

	     ["Test","squ-equ-test-subpbl1"]))];

 Iterator 1; moveActiveRoot 1;

 autoCalculate 1 CompleteCalcHead;

 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)

 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);

 appendFormula 1 " x - "; (*<ERROR> syntax error in ' x - ' </ERROR>*)

 val ((pt,_),_) = get_calc 1;

 val str = pr_ptree pr_short pt;

 writeln str;

 if str = ".    ----- pblobj -----\n1.   x + 1 = 2\n" then ()

 else raise error "inform.sml: diff.behav.appendFormula: syntax error";

"--------- CAS-command on ([],Pbl) -------------------------------";

"--------- CAS-command on ([],Pbl) -------------------------------";

"--------- CAS-command on ([],Pbl) -------------------------------";

val (p,_,f,nxt,_,pt) = 

    CalcTreeTEST [([], ("e_domID", ["e_pblID"], ["e_metID"]))];

val ifo = "solve(x+1=2,x)";

val (_,(_,c,(pt,p))) = inform ([],[],(pt,p)) "solve(x+1=2,x)";

show_pt pt;

val nxt = ("Apply_Method",Apply_Method ["Test","squ-equ-test-subpbl1"]);

val (p,_,f,nxt,_,pt) = me nxt p [] pt;

if p = ([1], Frm) andalso f2str f = "x + 1 = 2" then ()

else raise error "inform.sml: diff.behav. CAScmd ([],Pbl)";

"--------- CAS-command on ([],Pbl) FE-interface ------------------";

"--------- CAS-command on ([],Pbl) FE-interface ------------------";

"--------- CAS-command on ([],Pbl) FE-interface ------------------";

states:=[];

CalcTree [([], ("e_domID", ["e_pblID"], ["e_metID"]))];

Iterator 1;

moveActiveRoot 1;

replaceFormula 1 "solve(x+1=2,x)";

autoCalculate 1 CompleteCalc;

val ((pt,p),_) = get_calc 1;

show_pt pt;

if p = ([], Res) then ()

else raise error "inform.sml: diff.behav. CAScmd ([],Pbl) FE-interface";

"--------- inform [rational,simplification] ----------------------";

"--------- inform [rational,simplification] ----------------------";

"--------- inform [rational,simplification] ----------------------";

states:=[];

CalcTree [(["term (4/x - 3/y - 1)", "normalform N"],

	   ("Rational.thy",["rational","simplification"],

	    ["simplification","of_rationals"]))];

Iterator 1; moveActiveRoot 1;

autoCalculate 1 CompleteCalcHead;

autoCalculate 1 (Step 1);

autoCalculate 1 (Step 1);

autoCalculate 1 (Step 1);

autoCalculate 1 (Step 1);

"--- input the next formula that would be presented by mat-engine";

appendFormula 1 "(4 * y + -3 * x) / (x * y) + -1";

(*

print_depth 9;

print_depth 5; cs'; print_depth 3;

val (_,_,(pptt,pp)) = cs';

val tt = get_obj g_res pptt [4];

term2str tt;

(mk_tacis rew_ord erls) (nth 1 der);

*)

"--- input the exact final result";(*TODO: Exception- LIST "last_elem" raised*)

appendFormula 1 "(-3 * x + 4 * y + -1 * x * y) / (x * y)";