(* tests on solve.sml

   author: Walther Neuper

   060508,

   (c) due to copyright terms 

is NOT ONLY dependent on Test, but on other thys:

~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

uses from Rational.ML: Rrls cancel_p, Rrls cancel

which in turn

uses from Poly.ML: Rls make_polynomial, Rls expand_binom 

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

use"solve.sml";

*)

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

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

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

"--------- interSteps on norm_Rational ---------------------------";

(*---vvv NOT working after meNEW.04mmdd*)

"###### val intermediate_ptyps = !ptyps;val intermediate_mets = !mets";

"--------- prepare pbl, met --------------------------------------";

"-------- cancel, without detail ------------------------------";

"-------- cancel, detail rev-rew (cancel) afterwards ----------";

"-------------- cancel_p, without detail ------------------------------";

"-------------- cancel_p, detail rev-rew (cancel) afterwards ----------";

(*---^^^ NOT working*)

"on 'miniscript with mini-subpbl':";

"------ interSteps'donesteps': on 'miniscript with mini-subpbl'---";

"------ interSteps'detailrls' after CompleteCalc -----------------";

"------ interSteps after appendFormula ---------------------------";

(*---vvv not brought to work 0403*)

"------ Detail_Set -----------------------------------------------";

"###### ptyps:= intermediate_ptyps;met:= intermediate_mets;#######";

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

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

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

"--------- interSteps on norm_Rational ---------------------------";

"--------- interSteps on norm_Rational ---------------------------";

"--------- interSteps on norm_Rational ---------------------------";

states:=[];(*exp_IsacCore_Simp_Rat_Double_No-7.xml*)

CalcTree [(["TERM ((2/(x+3) + 2/(x - 3)) / (8*x/(x^2 - 9)))","normalform N"],

	   ("Rational.thy", 

	    ["rational","simplification"],

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

moveActiveRoot 1;

autoCalculate 1 CompleteCalc; 

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

(*with "Script SimplifyScript (t_::real) =       -----------------

       \  ((Rewrite_Set norm_Rational False) t_)"

case pt of Nd (PblObj _, [Nd _]) => ((*met only applies norm_Rational*))

	 | _ => error  "solve.sml: interSteps on norm_Rational 1";

interSteps 1 ([1], Res);

getFormulaeFromTo 1 ([1], Frm) ([1,12], Res) 99999 false;

interSteps 1 ([1,3], Res);

getTactic 1 ([1,4], Res)  (*here get the tactic, and ...*);

interSteps 1 ([1,5], Res) (*... here get the intermediate steps above*);

getTactic 1 ([1,5,1], Frm);

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

getTactic 1 ([1,8], Res) (*Rewrite_Set "common_nominator_p" *);

interSteps 1 ([1,9], Res)(*TODO.WN060606 reverse rew*);

--------------------------------------------------------------------*)

case pt of Nd (PblObj _, [Nd _, Nd _, Nd _, Nd _, Nd _, Nd _]) => ()

	 | _ => error  "solve.sml: interSteps on norm_Rational 1";

(*these have been done now by the script ^^^ immediately...

interSteps 1 ([1], Res);

getFormulaeFromTo 1 ([1], Frm) ([1,12], Res) 99999 false;

*)

interSteps 1 ([6], Res);

getTactic 1 ([6,1], Frm)  (*here get the tactic, and ...*);

interSteps 1 ([6,1], Res) (*... here get the intermediate steps above*);

getTactic 1 ([3,4,1], Frm);

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

val (Form form, SOME tac, asm) = pt_extract (pt, ([6], Res));

case (term2str form, tac, terms2strs asm) of

    ("1 / 2", Check_Postcond ["rational", "simplification"], 

     ["-36 * x + 4 * x ^^^ 3 ~= 0"]) => ()

  | _ => error "solve.sml: interSteps on norm_Rational 2";

"###### val intermediate_ptyps = !ptyps;val intermediate_mets = !mets";

"###### val intermediate_ptyps = !ptyps;val intermediate_mets = !mets";

"###### val intermediate_ptyps = !ptyps;val intermediate_mets = !mets";

val intermediate_ptyps = !ptyps;

val intermediate_mets = !mets;

"--------- prepare pbl, met --------------------------------------";

"--------- prepare pbl, met --------------------------------------";

"--------- prepare pbl, met --------------------------------------";

store_pbt

 (prep_pbt Test.thy "pbl_ttestt" [] e_pblID

 (["test"],

  [],

  e_rls, NONE, []));

store_pbt

 (prep_pbt Test.thy "pbl_ttestt_detail" [] e_pblID

 (["detail","test"],

  [("#Given" ,["realTestGiven t_"]),

   ("#Find"  ,["realTestFind s_"])

   ],

  e_rls, NONE, [["Test","test_detail"]]));

store_met

 (prep_met Test.thy "met_detbin" [] e_metID

 (["Test","test_detail_binom"]:metID,

  [("#Given" ,["realTestGiven t_"]),

   ("#Find"  ,["realTestFind s_"])

   ],

  {rew_ord'="sqrt_right",rls'=tval_rls,calc = [],srls=e_rls,prls=e_rls,

   crls=tval_rls, nrls=e_rls(*,

   asm_rls=[],asm_thm=[("real_mult_div_cancel2","")]*)},

 "Script Testterm (g_::real) =   \

 \(((Rewrite_Set expand_binoms False) @@\

 \  (Rewrite_Set cancel False)) g_)"

 ));

store_met

 (prep_met Test.thy "met_detpoly" [] e_metID

 (["Test","test_detail_poly"]:metID,

  [("#Given" ,["realTestGiven t_"]),

   ("#Find"  ,["realTestFind s_"])

   ],

  {rew_ord'="sqrt_right",rls'=tval_rls,calc=[],srls=e_rls,prls=e_rls,

   crls=tval_rls, nrls=e_rls(*,

   asm_rls=[],asm_thm=[("real_mult_div_cancel2","")]*)},

 "Script Testterm (g_::real) =   \

 \(((Rewrite_Set make_polynomial False) @@\

 \  (Rewrite_Set cancel_p False)) g_)"

 ));

(*---- funktionieren mit Rationals.ML: dummy-Funktionen(1)--------*)

"-------- cancel, without detail ------------------------------";

"-------- cancel, without detail ------------------------------";

"-------- cancel, without detail ------------------------------";

val fmz = ["realTestGiven (((3 + x) * (3 - x)) / ((3 + x) * (3 + x)))",

	   "realTestFind s"];

val (dI',pI',mI') =

  ("Test.thy",["detail","test"],["Test","test_detail_binom"]);

val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

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

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

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

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

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

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

(*nxt = ("Apply_Method",Apply_Method ("Test.thy","test_detail"))*)

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

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

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

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

(*"(3 + -1 * x) / (3 + x)"*)

if nxt = ("End_Proof'",End_Proof') then ()

else error "details.sml, changed behaviour in: without detail";

 val str = pr_ptree pr_short pt;

 writeln str;

"-------- cancel, detail rev-rew (cancel) afterwards ----------";

"-------- cancel, detail rev-rew (cancel) afterwards ----------";

"-------- cancel, detail rev-rew (cancel) afterwards ----------";

 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

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

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

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

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

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

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

 (*nxt = ("Apply_Method",Apply_Method ("Test.thy","test_detail"))*)

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

 (*val nxt = ("Rewrite_Set",Rewrite_Set "expand_binoms")*)

 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* rewrite must exist for Detail*)

(* val nxt = ("Detail",Detail);"----------------------";*)

(*WN.11.9.03: after meNEW not yet implemented -------------------------*)

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

(*FIXXXXXME.040216 #####################################################

# val nxt = ("Detail", Detail) : string * tac

val it = "----------------------" : string

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

val f = Form' (FormKF (~1, EdUndef, ...)) : mout

val nxt = ("Empty_Tac", Empty_Tac) : string * tac

val p = ([2, 1], Res) : pos'

#########################################################################

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

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

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

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

 (*val nxt = ("End_Detail",End_Detail)*)

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

 (*val nxt = ("Rewrite_Set",Rewrite_Set "cancel")*)

 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* rewrite must exist for Detail*)

 val nxt = ("Detail",Detail);"----------------------";

 val (p,_,f,nxt,_,pt) = (me nxt p [] pt) handle e => print_exn e;

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

(*15.10.02*)

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

(*

rewrite "Rationals.thy" "tless_true""e_rls"true("sym_real_plus_minus_binom","")

	"3 ^^^ 2 - x ^^^ 2";

*)

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

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

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

 val (p,_,f,nxt,_,pt) = (me nxt p [] pt) handle e => print_exn e;

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

if f = Form' (FormKF (~1,EdUndef,0,Nundef,"(3 - x) / (3 + x)"))

   andalso nxt = ("End_Proof'",End_Proof') then ()

else error "new behaviour in details.sml, \

		 \cancel, rev-rew (cancel) afterwards";

FIXXXXXME.040216 #####################################################*)

(*---- funktionieren mit Rationals.ML: dummy-Funktionen(1)--------*)

"-------------- cancel_p, without detail ------------------------------";

"-------------- cancel_p, without detail ------------------------------";

"-------------- cancel_p, without detail ------------------------------";

val fmz = ["realTestGiven (((3 + x)*(3+(-1)*x)) / ((3+x) * (3+x)))",

	   "realTestFind s"];

val (dI',pI',mI') =

  ("Test.thy",["detail","test"],["Test","test_detail_poly"]);

(*val p = e_pos'; val c = [];

val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));

val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)

val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

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

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

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

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

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

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

(*nxt = ("Apply_Method",Apply_Method ("Test.thy","test_detail"))*)

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

"(3 + x) * (3 + -1 * x) / ((3 + x) * (3 + x))";

 (*14.3.03*)

(*---------------WN060614?!?---

 val t = str2term "(3 + x) * (3 + -1 * x) / ((3 + x) * (3 + x))";

 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;

 "(9 + - (x ^^^ 2)) / (9 + 6 * x + x ^^^ 2)";

 val SOME (t,_) = rewrite_set_ thy false cancel_p t; term2str t;

 cancel_p_ thy t;

(---------------WN060614?!?---*)

 val t = str2term "(3 + x) * (3 + -1 * x)";

 val SOME (t,_) = rewrite_set_ thy false expand_poly t; term2str t;

 "3 * 3 + 3 * (-1 * x) + (x * 3 + x * (-1 * x))";

 val SOME (t,_) = rewrite_set_ thy false order_add_mult t; term2str t;

 "3 * 3 + (3 * x + (-1 * (3 * x) + -1 * (x * x)))";

 val SOME (t,_) = rewrite_set_ thy false simplify_power t; term2str t;

 "3 ^^^ 2 + (3 * x + (-1 * (3 * x) + -1 * x ^^^ 2))";

 val SOME (t,_) = rewrite_set_ thy false collect_numerals t; term2str t;

 "9 + (0 * x + -1 * x ^^^ 2)";

 val SOME (t,_) = rewrite_set_ thy false reduce_012 t; term2str t;

 "9 + - (x ^^^ 2)"; 

 (*14.3.03*)

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

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

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

(*"(3 + -1 * x) / (3 + x)"*)

if nxt = ("End_Proof'",End_Proof') then ()

else error "details.sml, changed behaviour in: cancel_p, without detail";

"-------------- cancel_p, detail rev-rew (cancel) afterwards ----------";

"-------------- cancel_p, detail rev-rew (cancel) afterwards ----------";

"-------------- cancel_p, detail rev-rew (cancel) afterwards ----------";

(* val p = e_pos'; val c = [];

 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));

 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)

val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

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

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

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

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

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

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

 (*nxt = ("Apply_Method",Apply_Method ("Test.thy","test_detail_poly"))*)

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

 (*val nxt = ("Rewrite_Set",Rewrite_Set "make_polynomial")*)

 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* rewrite must exist for Detail*)

(*14.3.03.FIXXXXXME since Isa02/reverse-rew.sml:

  fun make_deriv ...  Rls_ not yet impl. (| Thm | Calc) 

  Rls_ needed for make_polynomial ----------------------

 val nxt = ("Detail",Detail);"----------------------";

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

 if nxt = ("End_Detail",End_Detail) then ()

 else error "details.sml: new behav. in Detail make_polynomial";

----------------------------------------------------------------------*)

(*---------------

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

 (*val nxt = ("Rewrite_Set",Rewrite_Set "cancel_p")*)

 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* rewrite must exist for Detail*)

 val nxt = ("Detail",Detail);"----------------------";

 val (p,_,f,nxt,_,pt) = (me nxt p [] pt) handle e => print_exn e;

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

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

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

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

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

 val (p,_,f,nxt,_,pt) = (me nxt p [] pt) handle e => print_exn e;

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

if f = Form' (FormKF (~1,EdUndef,0,Nundef,"(3 + x) / (3 - x)"))

   andalso nxt = ("End_Proof'",End_Proof') then ()

else error "new behaviour in details.sml, cancel_p afterwards";

----------------*)

val fmz = ["realTestGiven ((x+3)+(-1)*(2+6*x))",

	   "realTestFind s"];

val (dI',pI',mI') =

  ("Test.thy",["detail","test"],["Test","test_detail_poly"]);

(* val p = e_pos'; val c = [];

 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));

 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)

val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

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

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

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

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

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

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

 (*nxt = ("Apply_Method",Apply_Method ("Test.thy","test_detail_poly"))*)

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

(*16.10.02 --- kommt auf POLY_EXCEPTION ?!??? ----------------------------

 (*val nxt = ("Rewrite_Set",Rewrite_Set "make_polynomial")*)

 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* rewrite must exist for Detail*)

 val nxt = ("Detail",Detail);"----------------------";

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

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

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

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

-------------------------------------------------------------------------*)

"------ interSteps'donesteps': on 'miniscript with mini-subpbl'---";

"------ interSteps'donesteps': on 'miniscript with mini-subpbl'---";

"------ interSteps'donesteps': on 'miniscript with mini-subpbl'---";

 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; 

 interSteps 1 ([],Res);

 val [(_,(((pt,_),_),[(_,ip)]))] = !states;

 val ("donesteps",_(*,ss*), lastpos) = detailstep pt ip;

 (*case ss of [(_,_,t1),(_,_,t2),(_,_,t3),(_,_,t4),(_,_,t5),(_,_,t6)] => 

	    (writeln o terms2str) [t1,t2,t3,t4,t5,t6]

	  | _ => error "details.sml: diff.behav. in detail miniscript";*) if lastpos = ([4], Res) then ()

 else error "details.sml: diff.behav. in interSteps'donesteps' 1";

 moveActiveDown 1;

 moveActiveDown 1;

 moveActiveDown 1;

 moveActiveDown 1; 

 interSteps 1 ([3],Pbl) (*subproblem*);

 val [(_,(((pt,_),_),[(_,ip)]))] = !states;

 val ("donesteps",_(*,ss*), lastpos) = detailstep pt ip;

 (*case ss of [(_,_,t1),(_,_,t2),(_,_,t3)] => 

	    (writeln o terms2str) [t1,t2,t3]

	  | _ => error "details.sml: diff.behav. in detail miniscript";*) if lastpos = ([3, 2], Res) then ()

 else error "details.sml: diff.behav. in interSteps'donesteps' 1";

(* val [(_,(((pt,_),_),[(_,ip)]))] = !states;

   writeln (pr_ptree pr_short pt);

   get_obj g_tac pt [4];

   *)

"------ interSteps'detailrls' after CompleteCalc -----------------";

"------ interSteps'detailrls' after CompleteCalc -----------------";

"------ interSteps'detailrls' after CompleteCalc -----------------";

 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;

 interSteps 1 ([],Res);

 moveActiveRoot 1; 

 moveActiveDown 1;

 moveActiveDown 1;

 moveActiveDown 1;  

 refFormula 1 (get_pos 1 1); (* 2 Res, <ISA> -1 + x = 0 </ISA> *)

 interSteps 1 ([2],Res);

 val [(_,(((pt,_),_),[(_,(p,_))]))] = !states;

 if length (children (get_nd pt p)) = 6 then ()

 else error "details.sml: diff.behav. in interSteps'detailrls' 1";

 moveActiveDown 1;

 moveActiveDown 1; refFormula 1 (get_pos 1 1); (* 3,1 Frm, <ISA> -1 + x = 0 </ISA>  *);

 interSteps 1 ([3,1],Frm) (*<ERROR> first formula on level has NO detail </E*);

 val [(_,(((pt,_),_),[(_,(p,_))]))] = !states;

 if length (children (get_nd pt p)) = 0 then () (*NO detail at ([xxx,1],Frm)*)

 else error "details.sml: diff.behav. in interSteps'detailrls' 2";

 moveActiveDown 1; 

 refFormula 1 (get_pos 1 1); (* 3,1 Res, <ISA> x = 0 + -1 * -1 </ISA> *)

 interSteps 1 ([3,1],Res);

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

 term2str (get_obj g_res pt [3,1,1]);(*"x = 0 + -1 * -1"  ok*)

 term2str (get_obj g_form pt [3,2]); (*"x = 0 + -1 * -1"  ok*)

 get_obj g_tac pt [3,1,1];           (*Rewrite_Inst.."risolate_bdv_add ok*)

 moveActiveDown 1; 

 refFormula 1 (get_pos 1 1); (* 3,2 Res, <ISA> x = 1 </ISA> *)

 interSteps 1 ([3,2],Res);

 val [(_,(((pt,_),_),[(_,(p,_))]))] = !states;

 if length (children (get_nd pt p)) = 2 then ()

 else error "details.sml: diff.behav. in interSteps'detailrls' 3";

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

"------ interSteps after appendFormula ---------------------------";

"------ interSteps after appendFormula ---------------------------";

"------ interSteps after appendFormula ---------------------------";

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);

autoCalculate 1 (Step 1);

appendFormula 1 "x - 1 = 0"(*generates intermediate steps*);

(*these are not shown, because the resulting formula is on the same

  level as the previous formula*)

interSteps 1 ([2],Res) (*error: last unchanged was ([2, 9], Res)*); 

(*...and these are the internals*)

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

val (_,_,lastpos) =detailstep pt p;

if p = ([2], Res) andalso lastpos = ([2, 9], Res) then ()

else error "solve.sml: diff.beh. after appendFormula x - 1 = 0";

"------ Detail_Set -----------------------------------------------";

"------ Detail_Set -----------------------------------------------";

"------ Detail_Set -----------------------------------------------";

 states:=[];

 CalcTree      (*start of calculation, return No.1*)

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

 autoCalculate 1 (Step 1);

 fetchProposedTactic 1 (*DG decides to do this tactic in detail*);

 (*TODO ...*)

 setNextTactic 1 (Detail_Set "Test_simplify");

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

 val str = pr_ptree pr_short pt;

 writeln str;

 print_depth 3;

 term2str (fst (get_obj g_result pt [1]));

"###### ptyps:= intermediate_ptyps;met:= intermediate_mets;#######";

"###### ptyps:= intermediate_ptyps;met:= intermediate_mets;#######";

"###### ptyps:= intermediate_ptyps;met:= intermediate_mets;#######";

ptyps:= intermediate_ptyps;

mets:= intermediate_mets;