Mercurial Mercurial > wneuper > isa / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
test/Tools/isac/Interpret/solve.sml
author Walther Neuper <neuper@ist.tugraz.at>
Mon, 16 Sep 2013 12:20:00 +0200
changeset 52105 2786cc9704c8
parent 52073 f709e6ab4e09
child 55352 7987eb501765
permissions -rw-r--r--
Test_Isac works again, perfectly ..

# the same tests works as in 8df4b6196660 (the *child* of "Test_Isac works...")
# ..EXCEPT those marked with "exception Div raised"
# for general state of tests see Test_Isac section {* history of tests *}. 
     1 (* Title: tests on solve.sml

     2    Author: Walther Neuper 060508,

     3    (c) due to copyright terms 

     4 

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

     6 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

     7 uses from Rational.ML: Rrls cancel_p, Rrls cancel

     8 which in turn

     9 uses from Poly.ML: Rls make_polynomial, Rls expand_binom 

    10 *)

    11 

    12 print_depth 5;

    13 trace_rewrite := false;

    14 trace_script := false;

    15 "-----------------------------------------------------------------";

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

    17 "-----------------------------------------------------------------";

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    34 "-----------------------------------------------------------------";

    35 "-----------------------------------------------------------------";

    36 "-----------------------------------------------------------------";

    37 

    38 val thy= @{theory Isac};

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

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

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

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

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

    44 	("Rational", ["rational","simplification"], ["simplification","of_rationals"]))];

    45 moveActiveRoot 1;

    46 autoCalculate 1 CompleteCalc; 

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

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

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

    50 interSteps 1 ([6], Res);

    51 

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

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

    54 

    55 getTactic 1 ([6,1,1], Frm); (*WN130909 <ERROR> syserror in getTactic </ERROR>*)

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

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

    58 case (term2str form, tac, terms2strs asm) of

    59     ("1 / 2", Check_Postcond ["rational", "simplification"], []) => ()

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

    61 get_obj g_res pt [];

    62 val (t, asm) = get_obj g_result pt [];

    63 if terms2str asm = "[\"8 * x ~= 0\",\"-9 + x ^^^ 2 ~= 0\"," ^

    64   "\"(2 / (x + 3) + 2 / (x - 3)) / (8 * x / (x ^^^ 2 - 9)) is_ratpolyexp\"]"

    65 then () else error "solve.sml: interSteps on norm_Rational 2, asms";

    66 

    67 

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

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

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

    71 val intermediate_ptyps = !ptyps;

    72 val intermediate_mets = !mets;

    73 

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

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

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

    77 store_pbt

    78   (prep_pbt @{theory Test} "pbl_ttestt" [] e_pblID

    79     (["test"], [], e_rls, NONE, []));

    80 store_pbt

    81   (prep_pbt @{theory Test} "pbl_ttestt_detail" [] e_pblID

    82     (["detail","test"],

    83     [("#Given", ["realTestGiven t_t"]), ("#Find", ["realTestFind s_s"])],

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

    85 

    86 store_met

    87   (prep_met @{theory Test} "met_detbin" [] e_metID

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

    89     [("#Given", ["realTestGiven t_t"]), ("#Find", ["realTestFind s_s"])],

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

    91       crls = tval_rls, errpats = [], nrls = e_rls},

    92     "Script Testterm (g_g::real) =" ^

    93     "(((Rewrite_Set expand_binoms False) @@" ^

    94     "(Rewrite_Set cancel_p False)) g_g)"));

    95 store_met

    96   (prep_met @{theory Test} "met_detpoly" [] e_metID

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

    98     [("#Given", ["realTestGiven t_t"]), ("#Find", ["realTestFind s_s"])],

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

   100       crls = tval_rls, errpats = [], nrls = e_rls},

   101     "Script Testterm (g_g::real) =" ^

   102     "(((Rewrite_Set make_polynomial False) @@" ^

   103     "(Rewrite_Set cancel_p False)) g_g)"));

   104 

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

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

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

   108 val fmz = ["realTestGiven (((3 + x) * (3 + -1*x)) / ((3 + x) * (3 + x)))", "realTestFind s"];

   109 val (dI',pI',mI') = ("Test", ["detail", "test"], ["Test", "test_detail_binom"]);

   110 

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

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

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

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

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

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

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

   118 (*nxt = ("Apply_Method",Apply_Method ("Test","test_detail"))*)

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

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

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

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

   123 (*WN130909: detail will be discontinued

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

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

   126 *)

   127 val str = pr_ptree pr_short pt;

   128 

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

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

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

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

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

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

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

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

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

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

   139  (*nxt = ("Apply_Method",Apply_Method ("Test","test_detail"))*)

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

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

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

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

   144 

   145 

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

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

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

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

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

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

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

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

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

   155 #########################################################################

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

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

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

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

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

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

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

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

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

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

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

   167 

   168 (*15.10.02*)

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

   170 (*

   171 rewrite "Rationals" "tless_true""e_rls"true("sym_real_plus_minus_binom","")

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

   173 *)

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

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

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

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

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

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

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

   181 else error "new behaviour in details.sml, \

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

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

   184 

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

   186 

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

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

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

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

   191 	   "realTestFind s"];

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

   193   ("Test",["detail","test"],["Test","test_detail_poly"]);

   194 

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

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

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

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

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

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

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

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

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

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

   205 (*nxt = ("Apply_Method",Apply_Method ("Test","test_detail"))*)

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

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

   208 

   209  (*14.3.03*)

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

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

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

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

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

   215  cancel_p_ thy t;

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

   217 

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

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

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

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

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

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

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

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

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

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

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

   229 

   230  (*14.3.03*)

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

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

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

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

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

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

   237 

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

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

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

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

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

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

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

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

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

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

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

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

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

   251  (*nxt = ("Apply_Method",Apply_Method ("Test","test_detail_poly"))*)

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

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

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

   255 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   292 ----------------------------------------------------------------------*)

   293 

   294 (*---------------

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   310 

   311 ----------------*)

   312 

   313 

   314 

   315 

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

   317 	   "realTestFind s"];

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

   319   ("Test",["detail","test"],["Test","test_detail_poly"]);

   320 

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

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

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

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

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

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

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

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

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

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

   331  (*nxt = ("Apply_Method",Apply_Method ("Test","test_detail_poly"))*)

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

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

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

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

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

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

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

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

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

   341 -------------------------------------------------------------------------*)

   342 

   343 

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

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

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

   347  states:=[];

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

   349    ("Test", ["sqroot-test","univariate","equation","test"],

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

   351  Iterator 1;

   352  moveActiveRoot 1;

   353  autoCalculate 1 CompleteCalc; 

   354  moveActiveRoot 1; 

   355 

   356  interSteps 1 ([],Res);

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

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

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

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

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

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

   363 

   364  moveActiveDown 1;

   365  moveActiveDown 1;

   366  moveActiveDown 1;

   367  moveActiveDown 1; 

   368 

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

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

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

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

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

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

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

   376 

   377 

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

   379    writeln (pr_ptree pr_short pt);

   380    get_obj g_tac pt [4];

   381    *)

   382 

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

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

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

   386  states:=[];

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

   388    ("Test", ["sqroot-test","univariate","equation","test"],

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

   390  Iterator 1;

   391  moveActiveRoot 1;

   392  autoCalculate 1 CompleteCalc;

   393  interSteps 1 ([],Res);

   394  moveActiveRoot 1; 

   395  moveActiveDown 1;

   396  moveActiveDown 1;

   397  moveActiveDown 1;  

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

   399 

   400  interSteps 1 ([2],Res);

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

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

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

   404 

   405  moveActiveDown 1;

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

   407 

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

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

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

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

   412 

   413  moveActiveDown 1; 

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

   415 

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

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

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

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

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

   421 

   422  moveActiveDown 1; 

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

   424 

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

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

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

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

   429 

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

   431 

   432 

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

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

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

   436 states:=[];

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

   438   ("Test", ["sqroot-test","univariate","equation","test"],

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

   440 Iterator 1;

   441 moveActiveRoot 1;

   442 autoCalculate 1 CompleteCalcHead;

   443 autoCalculate 1 (Step 1);

   444 autoCalculate 1 (Step 1);

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

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

   447   level as the previous formula*)

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

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

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

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

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

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

   454 

   455 

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

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

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

   459  states:=[]; (*start of calculation, return No.1*)

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

   461    ("Test", ["sqroot-test","univariate","equation","test"],

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

   463  Iterator 1; moveActiveRoot 1; 

   464  autoCalculate 1 CompleteCalcHead;

   465  autoCalculate 1 (Step 1);

   466  autoCalculate 1 (Step 1);

   467 

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

   469  (*TODO ...*)

   470  setNextTactic 1 (Detail_Set "Test_simplify");

   471 

   472 

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

   474  val str = pr_ptree pr_short pt;

   475  writeln str;

   476 

   477  print_depth 3;

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

   479 

   480 

   481 

   482 

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

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

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

   486 ptyps:= intermediate_ptyps;

   487 mets:= intermediate_mets;
wneuper/isa