(* Title: 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] ----------------------";

"--------- Take as 1st tac, start with <NEW> (CAS input) ---------";

"--------- Take as 1st tac, start from exp -----------------------";

"--------- init_form, start with <NEW> (CAS input) ---------------";

"--------- build fun check_err_patt ------------------------------";

"--------- build fun check_err_patt ?bdv -------------------------";

"--------- build fun check_error_patterns ------------------------";

"--------- embed fun check_error_patterns ------------------------";

"--------- embed fun find_fillpatterns ---------------------------";

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

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

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

"--------- 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::real))", "solveFor x","solutions L"], 

	    ("Test", ["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;

(*============ inhibit exn AK110726 ==============================================

(* 2nd string should be the same as 1st one *)

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

".    ----- 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";

 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 error "inform.sml: diff.behav.appendFormula: on Res + equ 1";

============ inhibit exn AK110726 ==============================================*)

 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 error "inform.sml: diff.behav.appendFormula: on Res + equ 2";

 fetchProposedTactic 1; (*takes Iterator 1 _1_*)

(*============ inhibit exn AK110725 ==============================================

(* ERROR: exception Bind raised *)

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

 if tac = Rewrite_Set "Test_simplify" then ()

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

============ inhibit exn AK110725 ==============================================*)

 autoCalculate 1 CompleteCalc;

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

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

 else 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 (@{theory "Isac"}) Atools_erls 

		       ((#rules o rep_rls) Test_simplify)

		       (sqrt_right false (@{theory "Pure"})) NONE 

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

 (writeln o trtas2str) fod;

 val ifod = make_deriv (@{theory "Isac"}) Atools_erls 

		       ((#rules o rep_rls) Test_simplify)

		       (sqrt_right false (@{theory "Pure"})) 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::real))", "solveFor x","solutions L"], 

	    ("Test", ["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 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 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 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::real))", "solveFor x","solutions L"], 

	    ("Test", ["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 error "inform.sml: diff.behav.appendFormula: Res + NOder 1";

 fetchProposedTactic 1;

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

 if tac = Rewrite_Set "Test_simplify" then ()

 else 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 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::real))", "solveFor x","solutions L"], 

	    ("Test", ["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 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 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 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::real))", "solveFor x","solutions L"], 

	    ("Test", ["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 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 error "inform.sml: diff.behav.appendFormula: Res + latEE 2";

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

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

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

 states:=[];

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

	    ("Test", ["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;

(*============ inhibit exn AK110725 ==============================================

(* 2nd string should be the same as 1st one *)

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

".    ----- 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";

 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 error "inform.sml: diff.behav.replaceFormula: on Res += 1";

============ inhibit exn AK110725 ==============================================*)

 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 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::real))", "solveFor x","solutions L"], 

	    ("Test", ["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 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 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::real))", "solveFor x","solutions L"], 

	    ("Test", ["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 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 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::real))", "solveFor x","solutions L"], 

	    ("Test", ["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 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 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", ["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_ ctxt)) 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_ ctxt)) 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_ ctxt)) 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 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_ ctxt)) 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 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_ ctxt)) 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_ ctxt)) pbl; 

 modifycalcheadOK2xml 111 (bool2str b) ocalhd;

*)

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

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

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

 states:=[];

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

	    ("Test", ["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 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 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 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",["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 _should_ be presented by mat-engine";

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

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

if p = ([4], Res) andalso (length o children o (get_nd pt)) (fst p) = 2 then ()

else error ("inform.sml: [rational,simplification] 1");

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

(*autoCalculate 1 (Step 1);*)

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

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

if p = ([5], Res) andalso (length o children o (get_nd pt)) (fst p) = 0 then ()

else error ("inform.sml: [rational,simplification] 2");

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

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

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

if p = ([6], Res) andalso (length o children o (get_nd pt)) (fst p) = 2 then ()

else error ("inform.sml: [rational,simplification] 3");

show_pt pt;

"--------- Take as 1st tac, start with <NEW> (CAS input) ---------";

"--------- Take as 1st tac, start with <NEW> (CAS input) ---------";

"--------- Take as 1st tac, start with <NEW> (CAS input) ---------";

val t = str2term "Diff (x^^^2 + x + 1, x)";

case t of Const ("Diff.Diff", _) $ _ => ()

	| _ => raise 

	      error "diff.sml behav.changed for CAS Diff (..., x)";

atomty t;

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

(*1>*)states:=[];

(*2>*)CalcTree [([], ("e_domID", ["e_pblID"], ["e_metID"]))];

(*3>*)Iterator 1;moveActiveRoot 1;

"----- here the Headline has been finished";

(*4>*)moveActiveFormula 1 ([],Pbl);

(*5>*)replaceFormula 1 "Diff (x^2 + x + 1, x)";

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

val PblObj {probl, meth, spec, fmz, env, loc, ...} = get_obj I pt [];

val NONE = env;

val (SOME istate, NONE) = loc;

print_depth 5;

writeln"-----------------------------------------------------------";

spec;

writeln (itms2str_ ctxt probl);

writeln (itms2str_ ctxt meth);

(*============ inhibit exn AK110725 ==============================================

(* ERROR: Argument: istate : istate * Proof.context Reason: 

        Can't unify istate to istate * Proof.context *)

writeln (istate2str istate);

============ inhibit exn AK110725 ==============================================*)

print_depth 3;

refFormula 1 ([],Pbl) (*--> correct CalcHead*);

 (*081016 NOT necessary (but leave it in Java):*)

(*6>*)(*completeCalcHead*)autoCalculate 1 CompleteCalcHead;

"----- here the CalcHead has been completed --- ONCE MORE ?????";

(***difference II***)

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

(*val p = ([], Pbl)*)

val PblObj {probl, meth, spec, fmz, env, loc, ...} = get_obj I pt [];

val NONE = env;

val (SOME istate, NONE) = loc;

(*============ inhibit exn AK110725 ==============================================

(* ERROR: Argument: istate : istate * Proof.context Reason: Can't unify istate to istate * Proof.context *)

print_depth 5; writeln (istate2str istate);  print_depth 3;

============ inhibit exn AK110725 ==============================================*)

(*ScrState ([],

 [], NONE,

 ??.empty, Sundef, false)*)

print_depth 5; spec; print_depth 3;

(*("Isac",

      ["derivative_of", "function"],

      ["diff", "differentiate_on_R"]) : spec*)

writeln (itms2str_ ctxt probl);

(*[

(1 ,[1] ,true ,#Given ,Cor functionTerm (x ^^^ 2 + x + 1) ,(f_, [x ^^^ 2 + x + 1])),

(2 ,[1] ,true ,#Given ,Cor differentiateFor x ,(v_, [x])),

(3 ,[1] ,true ,#Find ,Cor derivative f_'_f ,(f_'_f, [f_'_f]))]*)

writeln (itms2str_ ctxt meth);

(*[

(1 ,[1] ,true ,#Given ,Cor functionTerm (x ^^^ 2 + x + 1) ,(f_, [x ^^^ 2 + x + 1])),

(2 ,[1] ,true ,#Given ,Cor differentiateFor x ,(v_, [x])),

(3 ,[1] ,true ,#Find ,Cor derivative f_'_f ,(f_'_f, [f_'_f]))]*)

writeln"-----------------------------------------------------------";

(*7>*)fetchProposedTactic 1 (*--> Apply_Method*);

(*WN081028 fixed <ERROR> helpless </ERROR> by inform returning ...(.,Met)*)

autoCalculate 1 CompleteCalc;

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

val Form res = (#1 o pt_extract) (pt, ([],Res));

show_pt pt;

if p = ([], Res) andalso term2str res = "1 + 2 * x" then ()

else error "diff.sml behav.changed for Diff (x^2 + x + 1, x)";

"--------- Take as 1st tac, start from exp -----------------------";

"--------- Take as 1st tac, start from exp -----------------------";

"--------- Take as 1st tac, start from exp -----------------------";

(*the following input is copied from BridgeLog Java <==> SML,

  omitting unnecessary inputs*)

(*1>*)states:=[];

(*2>*)CalcTree [(["functionTerm (x^2 + x + 1)", "differentiateFor x", "derivative f_'_f"],("Isac",["derivative_of","function"],["diff","differentiate_on_R"]))];

(*3>*)Iterator 1; moveActiveRoot 1;

(*6>*)(*completeCalcHead*)autoCalculate 1 CompleteCalcHead;

(***difference II***)

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

val PblObj {probl, meth, spec, fmz, env, loc, ...} = get_obj I pt [];

val NONE = env;

val (SOME istate, NONE) = loc;

(*============ inhibit exn AK110725 ==============================================

(* ERROR: Argument: istate : istate * Proof.context Reason: Can't unify istate to istate * Proof.context *)

print_depth 5; writeln (istate2str istate);  print_depth 3;

============ inhibit exn AK110725 ==============================================*)

(*ScrState ([],

 [], NONE,

 ??.empty, Sundef, false)*)

print_depth 5; spec; print_depth 3;

(*("Isac",

      ["derivative_of", "function"],

      ["diff", "differentiate_on_R"]) : spec*)

writeln (itms2str_ ctxt probl);

(*[

(1 ,[1] ,true ,#Given ,Cor functionTerm (x ^^^ 2 + x + 1) ,(f_, [x ^^^ 2 + x + 1])),

(2 ,[1] ,true ,#Given ,Cor differentiateFor x ,(v_, [x])),

(3 ,[1] ,true ,#Find ,Cor derivative f_'_f ,(f_'_f, [f_'_f]))]*)

writeln (itms2str_ ctxt meth);

(*[

(1 ,[1] ,true ,#Given ,Cor functionTerm (x ^^^ 2 + x + 1) ,(f_, [x ^^^ 2 + x + 1])),

(2 ,[1] ,true ,#Given ,Cor differentiateFor x ,(v_, [x])),

(3 ,[1] ,true ,#Find ,Cor derivative f_'_f ,(f_'_f, [f_'_f]))]*)

writeln"-----------------------------------------------------------";

(*7>*)fetchProposedTactic 1 (*--> Apply_Method*);

autoCalculate 1 (Step 1);

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

val Form res = (#1 o pt_extract) (pt, p);

if term2str res = "d_d x (x ^^^ 2 + x + 1)" then ()

else error "diff.sml Diff (x^2 + x + 1, x) from exp";

"--------- init_form, start with <NEW> (CAS input) ---------------";

"--------- init_form, start with <NEW> (CAS input) ---------------";

"--------- init_form, start with <NEW> (CAS input) ---------------";

states:=[];

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

(*[[from sml: > @@@@@begin@@@@@

[[from sml:  1 

[[from sml: <CALCTREE>

[[from sml:    <CALCID> 1 </CALCID>

[[from sml: </CALCTREE>

[[from sml: @@@@@end@@@@@*)

Iterator 1;

(*[[from sml: > @@@@@begin@@@@@

[[from sml:  1 

[[from sml: <ADDUSER>

[[from sml:   <CALCID> 1 </CALCID>

[[from sml:   <USERID> 1 </USERID>

[[from sml: </ADDUSER>

[[from sml: @@@@@end@@@@@*)

moveActiveRoot 1;

(*[[from sml: > @@@@@begin@@@@@

[[from sml:  1 

[[from sml: <CALCITERATOR>

[[from sml:   <CALCID> 1 </CALCID>

[[from sml:   <POSITION>

[[from sml:     <INTLIST>

[[from sml:     </INTLIST>

[[from sml:     <POS> Pbl </POS>

[[from sml:   </POSITION>

[[from sml: </CALCITERATOR>

[[from sml: @@@@@end@@@@@*)

getFormulaeFromTo 1 ([],Pbl) ([],Pbl) 0 false;

(*[[from sml: > @@@@@begin@@@@@                STILL CORRECT

[[from sml:  1 

[[from sml: <GETELEMENTSFROMTO>

[[from sml:   <CALCID> 1 </CALCID>

[[from sml:   <FORMHEADS>

[[from sml:     <CALCFORMULA>

[[from sml:       <POSITION>

[[from sml:         <INTLIST>

[[from sml:         </INTLIST>

[[from sml:         <POS> Pbl </POS>

[[from sml:       </POSITION>

[[from sml:       <FORMULA>

[[from sml:         <MATHML>

[[from sml:           <ISA> ________________________________________________ </ISA>

[[from sml:         </MATHML>

[[from sml: 

[[from sml:       </FORMULA>

[[from sml:     </CALCFORMULA>

[[from sml:   </FORMHEADS>

[[from sml: </GETELEMENTSFROMTO>

[[from sml: @@@@@end@@@@@*)

refFormula 1 ([],Pbl);

(*[[from sml: > @@@@@begin@@@@@                STILL CORRECT

[[from sml:  1 

[[from sml: <REFFORMULA>

[[from sml:   <CALCID> 1 </CALCID>

[[from sml:   <CALCHEAD status = "incorrect">

[[from sml:     <POSITION>

[[from sml:       <INTLIST>

[[from sml:       </INTLIST>

[[from sml:       <POS> Pbl </POS>

[[from sml:     </POSITION>

[[from sml:     <HEAD>

[[from sml:       <MATHML>

[[from sml:         <ISA> Problem (e_domID, [e_pblID]) </ISA>

[[from sml:       </MATHML>

[[from sml:     </HEAD>

[[from sml:     <MODEL>

[[from sml:       <GIVEN>  </GIVEN>

[[from sml:       <WHERE>  </WHERE>

[[from sml:       <FIND>  </FIND>

[[from sml:       <RELATE>  </RELATE>

[[from sml:     </MODEL>

[[from sml:     <BELONGSTO> Pbl </BELONGSTO>

[[from sml:     <SPECIFICATION>

[[from sml:       <THEORYID> e_domID </THEORYID>

[[from sml:       <PROBLEMID>

[[from sml:         <STRINGLIST>

[[from sml:           <STRING> e_pblID </STRING>

[[from sml:         </STRINGLIST>

[[from sml:       </PROBLEMID>

[[from sml:       <METHODID>

[[from sml:         <STRINGLIST>

[[from sml:           <STRING> e_metID </STRING>

[[from sml:         </STRINGLIST>

[[from sml:       </METHODID>

[[from sml:     </SPECIFICATION>

[[from sml:   </CALCHEAD>

[[from sml: </REFFORMULA>

[[from sml: @@@@@end@@@@@*)

moveActiveFormula 1 ([],Pbl);

(*[[from sml: > @@@@@begin@@@@@

[[from sml:  1 

[[from sml: <CALCITERATOR>

[[from sml:   <CALCID> 1 </CALCID>

[[from sml:   <POSITION>

[[from sml:     <INTLIST>

[[from sml:     </INTLIST>

[[from sml:     <POS> Pbl </POS>

[[from sml:   </POSITION>

[[from sml: </CALCITERATOR>

[[from sml: @@@@@end@@@@@*)

replaceFormula 1 "Simplify (1+2)";

(*[[from sml: > @@@@@begin@@@@@

[[from sml:  1 

[[from sml: <REPLACEFORMULA>

[[from sml:   <CALCID> 1 </CALCID>

[[from sml:   <CALCCHANGED>

[[from sml:     <UNCHANGED>

[[from sml:       <INTLIST>

[[from sml:       </INTLIST>

[[from sml:       <POS> Pbl </POS>

[[from sml:     </UNCHANGED>

[[from sml:     <DELETED>

[[from sml:       <INTLIST>

[[from sml:       </INTLIST>

[[from sml:       <POS> Pbl </POS>

[[from sml:     </DELETED>

[[from sml:     <GENERATED>

[[from sml:       <INTLIST>

[[from sml:       </INTLIST>

[[from sml:       <POS> Met </POS>                           DIFFERENCE: Pbl

[[from sml:     </GENERATED>

[[from sml:   </CALCCHANGED>

[[from sml: </REPLACEFORMULA>

[[from sml: @@@@@end@@@@@*)

getFormulaeFromTo 1 ([],Pbl) ([],Pbl) 0 false(*              DIFFERENCE: Pbl*);

(*@@@@@begin@@@@@

 1

<GETELEMENTSFROMTO>

  <CALCID> 1 </CALCID>

  <FORMHEADS>

    <CALCFORMULA>

      <POSITION>

        <INTLIST>

        </INTLIST>

        <POS> Pbl </POS>

      </POSITION>

      <FORMULA>

        <MATHML>

          <ISA> Simplify (1 + 2) </ISA>                      WORKS !!!!!

        </MATHML>

      </FORMULA>

    </CALCFORMULA>

  </FORMHEADS>

</GETELEMENTSFROMTO>

@@@@@end@@@@@*)

getFormulaeFromTo 1 ([],Pbl) ([],Met) 0 false;

(*[[from sml: > @@@@@begin@@@@@

[[from sml:  1 

[[from sml: <SYSERROR>

[[from sml:   <CALCID> 1 </CALCID>

[[from sml:   <ERROR> error in getFormulaeFromTo </ERROR>

[[from sml: </SYSERROR>

[[from sml: @@@@@end@@@@@*)

(*step into getFormulaeFromTo --- bug corrected...*)

"--------- build fun check_err_patt ------------------------------";

"--------- build fun check_err_patt ------------------------------";

"--------- build fun check_err_patt ------------------------------";

val subst = [(str2term "bdv", str2term "x")]: subst;

val rls = norm_Rational

val pat = parse_patt @{theory} "(?a + ?b)/(?b + ?c) = ?a / ?c";

val (res, inf) = (str2term "(2 + 3)/(3 + 4)", str2term "2 / 4");

val (res, inf) = (str2term "(2 + 3)/(3 + 4)", str2term "1 / 2");

val (res', _, _, rewritten) = (*rewritten: the lhs of the pattern matches in res*)

  rew_sub thy 1 [] e_rew_ord e_rls false [] (Trueprop $ pat) res;

if rewritten then NONE else SOME "e_errpatID";

val norm_res = case rewrite_set_ (Isac()) false rls res' of

  NONE => res'

| SOME (norm_res, _) => norm_res

val norm_inf = case rewrite_set_ (Isac()) false rls inf of

  NONE => inf

| SOME (norm_inf, _) => norm_inf;

res' = inf;

norm_res = norm_inf;

val pat = parse_patt @{theory} "(?a + ?b)/?a = ?b";

val (res, inf) = (str2term "(2 + 3)/2", str2term "3");

if check_err_patt (res, inf) subst ("errpatID", pat) rls = SOME "errpatID"

then () else error "error patt example1 changed";

val pat = parse_patt @{theory} "(?a + ?b)/(?a + ?c) = ?b / ?c";

val (res, inf) = (str2term "(2 + 3)/(2 + 4)", str2term "3 / 4");

if check_err_patt (res, inf) subst ("errpatID", pat) rls = SOME "errpatID"

then () else error "error patt example2 changed";

val pat = parse_patt @{theory} "(?a + ?b)/(?b + ?c) = ?a / ?c";

val (res, inf) = (str2term "(2 + 3)/(3 + 4)", str2term "2 / 4");

if check_err_patt (res, inf) subst ("errpatID", pat) rls = SOME "errpatID"

then () else error "error patt example3 changed";

val inf =  str2term "1 / 2";

if check_err_patt (res, inf) subst ("errpatID", pat) rls = SOME "errpatID"

then () else error "error patt example3 changed";

"--------- build fun check_err_patt ?bdv -------------------------";

"--------- build fun check_err_patt ?bdv -------------------------";

"--------- build fun check_err_patt ?bdv -------------------------";

val subst = [(str2term "bdv", str2term "x")]: subst;

val t = str2term "d_d x (x ^^^ 2 + sin (x ^^^ 4))";

val SOME (t, _) = rewrite_set_inst_ thy false subst norm_diff t;

if term2str t = "2 * x + cos (x ^^^ 4) * 4 * x ^^^ 3" then ()

else error "build fun check_err_patt ?bdv changed 1"; 

val rls = norm_diff

val pat = parse_patt @{theory} "d_d ?bdv (sin ?u) = cos (d_d ?bdv ?u)"; 

val (res, inf) = (str2term "2 * x + d_d x (sin (x ^^^ 4))", str2term "2 * x + cos (4 * x ^^^ 3)");

val (res', _, _, rewritten) = (*rewritten: the lhs of the pattern matches in res*)

  rew_sub thy 1 subst e_rew_ord e_rls false [] (Trueprop $ pat) res;

if term2str res' = "2 * x + cos (d_d x (x ^^^ 4))" andalso rewritten then ()

else error "build fun check_err_patt ?bdv changed 2";

val norm_res = case rewrite_set_inst_ (Isac()) false subst rls  res' of

  NONE => res'

| SOME (norm_res, _) => norm_res;

if term2str norm_res = "2 * x + cos (4 * x ^^^ 3)" then ()

else error "build fun check_err_patt ?bdv changed 3";

val norm_inf = case rewrite_set_inst_ (Isac()) false subst rls inf of

  NONE => inf

| SOME (norm_inf, _) => norm_inf;

if term2str norm_inf = "2 * x + cos (4 * x ^^^ 3)" then ()

else error "build fun check_err_patt ?bdv changed 4";

res' = inf;

if norm_res = norm_inf then ()

else error "build fun check_err_patt ?bdv changed 5";

if check_err_patt (res, inf) (subst: subst) ("errpatID": errpatID, pat) rls = SOME "errpatID"

then () else error "error patt example1 changed";

"--------- build fun check_error_patterns ------------------------";

"--------- build fun check_error_patterns ------------------------";

"--------- build fun check_error_patterns ------------------------";

val (res, inf) =

  (str2term "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))",

   str2term "d_d x (x ^^^ 2) + cos (4 * x ^^^ 3)");

val {errpats, nrls = rls, scr = Script prog, ...} = get_met ["diff", "differentiate_on_R"]

val env = [(str2term "v_v", str2term "x")];

val errpats =

  [e_errpat, (*generalised for testing*)

   ("chain-rule-diff-both",

     [parse_patt @{theory} "d_d ?bdv (sin ?u) = cos (d_d ?bdv ?u)",

      parse_patt @{theory} "d_d ?bdv (cos ?u) = - sin (d_d ?bdv ?u)",

      parse_patt @{theory} "d_d ?bdv (?u ^^^ ?n) = ?n * ?u ^^^ (?n - 1)",

      parse_patt @{theory} "d_d ?bdv (LogExp.ln ?u) = 1 / ?u",

      parse_patt @{theory} "d_d ?bdv (LogExp.ln ?u) = 1 / d_d ?bdv ?u"],

     [@{thm diff_sin_chain}, @{thm diff_cos_chain}, @{thm diff_pow_chain}, 

      @{thm diff_ln_chain}, @{thm  diff_exp_chain}])]: errpat list;

case check_error_patterns (res, inf) (prog, env) (errpats, rls) of SOME _ => () 

| NONE => error "check_error_patterns broken";

"--------- embed fun check_error_patterns ------------------------";

"--------- embed fun check_error_patterns ------------------------";

"--------- embed fun check_error_patterns ------------------------";

states:=[];

CalcTree

[(["functionTerm (x ^ 2 + sin (x ^ 4))", "differentiateFor x", "derivative f_f'"], 

  ("Isac", ["derivative_of","function"], ["diff","differentiate_on_R"]))];

Iterator 1;

moveActiveRoot 1;

autoCalculate 1 CompleteCalcHead;

autoCalculate 1 (Step 1);

autoCalculate 1 (Step 1);(*([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))*)

(*autoCalculate 1 (Step 1);([2], Res), d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4)*)

"~~~~~ fun appendFormula, args:"; val (cI, (ifo:cterm')) = (1, "d_d x (x ^ 2) + cos (4 * x ^ 3)");

val cs = get_calc cI

val pos as (_,p_) = get_pos cI 1; (*pos = ([1], Res)*)

val cs' = 

    case step pos cs of

	    ("ok", cs') => cs';

val (_, _, (pt, ([2], Res))) = cs';

(*show_pt pt;

  [(([], Frm), Diff (x ^^^ 2 + sin (x ^^^ 4), x)),

   (([1], Frm), d_d x (x ^^^ 2 + sin (x ^^^ 4))),

   (([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))), <<=== input follos: "...+ cos(4.x^3)"

   (([2], Res), d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4))] *)

"~~~~~ fun inform, args:"; val ((cs as (_, _, ptp as (pt, pos as (p, p_))): calcstate'), istr) =

  (cs', (encode ifo));

val 	SOME f_in = parse (assoc_thy "Isac") istr

val f_in = term_of f_in

val pos_pred = lev_back' pos

			(* f_pred ---"step pos cs"---> f_succ in appendFormula

   TODO.WN120517: one starting point for redesign of pos' *)

val (f_pred, f_succ) = (get_pred_formula (pt, pos_pred), get_pred_formula (pt, pos));

term2str f_pred = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))";

term2str f_succ = "d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4)";

			f_succ = f_in; (* = false*)

cas_input f_in; (* = NONE*)

val msg_calcstate' = compare_step ([], [], (pt, pos_pred)) f_in

val ("no derivation found", calcstate') = msg_calcstate';

			                 val pp = par_pblobj pt p

			                 val {errpats, nrls, scr = Script prog, ...} = get_met (get_obj g_metID pt pp)

			                 val ScrState (env, _, _, _, _, _) = get_istate pt pos;

                 case check_error_patterns (f_pred, f_in) (prog, env) (errpats, nrls) of

			                   SOME errpatID => ("error pattern #" ^ errpatID ^ "#", calcstate')

			                 | NONE => msg_calcstate';

"~~~~~ from inform return val:"; val () = ();

case check_error_patterns (f_pred, f_in) (prog, env) (errpats, nrls) of

			  SOME errpatID => ()

			| NONE => error "check_error_patterns broken";

"--- final check:";

case inform cs' (encode ifo) of

  ("error pattern #chain-rule-diff-both#", calcstate') => ()

| _ => error "inform with (positive) check_error_patterns broken"

"--------- embed fun find_fillpatterns ---------------------------";

"--------- embed fun find_fillpatterns ---------------------------";

"--------- embed fun find_fillpatterns ---------------------------";

states:=[];

CalcTree

[(["functionTerm (x ^ 2 + sin (x ^ 4))", "differentiateFor x", "derivative f_f'"], 

  ("Isac", ["derivative_of","function"], ["diff","differentiate_on_R"]))];

Iterator 1;

moveActiveRoot 1;

autoCalculate 1 CompleteCalcHead;

autoCalculate 1 (Step 1);

autoCalculate 1 (Step 1);(*([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))*)

appendFormula 1 "d_d x (x ^ 2) + cos (4 * x ^ 3)";

  (*<CALCMESSAGE> error pattern #chain-rule-diff-both# </CALCMESSAGE>*)

  (*TODO BACK TO <CALCMESSAGE> no derivation found </CALCMESSAGE>*)

"~~~~~ fun FindFillpatterns, args:"; val (cI, errpatID) = (1, "chain-rule-diff-both");

  val ((pt, _), _) = get_calc cI

				val pos = get_pos cI 1;

			"~~~~~ fun find_fillpatterns, args:"; val ((pt, pos as (p, _)), errpatID) = ((pt, pos), errpatID);

	    val f_curr = get_pred_formula (pt, pos); (* = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))"*)

    val pp = par_pblobj pt p

			    val {errpats, scr = Script prog, ...} = get_met (get_obj g_metID pt pp)

    val ScrState (env, _, _, _, _, _) = get_istate pt pos

    val subst = get_bdv_subst prog env

    val errpatthms = errpats

      |> filter ((curry op = errpatID) o (#1: errpat -> errpatID))

      |> map (#3: errpat -> thm list)

      |> flat;

case map (get_fillpats subst f_curr errpatID) errpatthms |> flat of

 ("fill-d_d-arg",

  "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) =\nd_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x ?_dummy_1")

    :: _ => ()