wneuper/isac: src/smltest/ME/solve.sml@aaa641d8546d

     1 (* tests on solve.sml

     2    author: Walther Neuper

     3    060508,

     4    (c) due to copyright terms

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

     7 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

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

     9 which in turn

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

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

    13 use"solve.sml";

    14 *)

    16 "-----------------------------------------------------------------";

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

    18 "-----------------------------------------------------------------";

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

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

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

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

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

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

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

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

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

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

    43 	   ("Rational.thy",

    44 	    ["rational","simplification"],

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

    46 moveActiveRoot 1;

    47 autoCalculate 1 CompleteCalc;

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

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

    51        \  ((Rewrite_Set norm_Rational False) t_)"

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

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

    54 interSteps 1 ([1], Res);

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

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

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

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

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

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

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

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

    66 --------------------------------------------------------------------*)

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

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

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

    71 interSteps 1 ([1], Res);

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

    73 *)

    74 interSteps 1 ([6], Res);

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

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

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

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

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

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

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

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

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

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

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

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

    92 store_pbt

    93  (prep_pbt Test.thy "pbl_ttestt" [] e_pblID

    94  (["test"],

    95   [],

    96   e_rls, None, []));

    97 store_pbt

    98  (prep_pbt Test.thy "pbl_ttestt_detail" [] e_pblID

    99  (["detail","test"],

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

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

   102    ],

   103   e_rls, None, [["Test","test_detail"]]));

   105 store_met

   106  (prep_met Test.thy "met_detbin" [] e_metID

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

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

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

   110    ],

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

   112    crls=tval_rls, nrls=e_rls(*,

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

   114  "Script Testterm (g_::real) =   \

   115  \(((Rewrite_Set expand_binoms False) @@\

   116  \  (Rewrite_Set cancel False)) g_)"

   117  ));

   118 store_met

   119  (prep_met Test.thy "met_detpoly" [] e_metID

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

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

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

   123    ],

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

   125    crls=tval_rls, nrls=e_rls(*,

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

   127  "Script Testterm (g_::real) =   \

   128  \(((Rewrite_Set make_polynomial False) @@\

   129  \  (Rewrite_Set cancel_p False)) g_)"

   130  ));

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

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

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

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

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

   138 	   "realTestFind s"];

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   158  val str = pr_ptree pr_short pt;

   159  writeln str;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   188 #########################################################################

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

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

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

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

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

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

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

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

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

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

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

   200 (*15.10.02*)

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

   202 (*

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

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

   205 *)

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

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

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

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

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

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

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

   213 else raise error "new behaviour in details.sml, \

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

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

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

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

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

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

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

   223 	   "realTestFind s"];

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

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

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

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

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

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

   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 val (p,_,f,nxt,_,pt) = me nxt p [] pt;

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

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

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

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

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

   241  (*14.3.03*)

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

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

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

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

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

   247  cancel_p_ thy t;

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

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

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

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

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

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

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

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

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

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

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

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

   261  (*14.3.03*)

   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 (*"(3 + -1 * x) / (3 + x)"*)

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

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

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

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

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

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

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

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

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

   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  (*nxt = ("Apply_Method",Apply_Method ("Test.thy","test_detail_poly"))*)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   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;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   324 ----------------------------------------------------------------------*)

   326 (*---------------

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   343 ----------------*)

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

   350 	   "realTestFind s"];

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   374 -------------------------------------------------------------------------*)

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

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

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

   380  states:=[];

   381  CalcTree

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

   383    ("Test.thy",

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

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

   386  Iterator 1;

   387  moveActiveRoot 1;

   388  autoCalculate 1 CompleteCalc;

   389  moveActiveRoot 1;

   391  interSteps 1 ([],Res);

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

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

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

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

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

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

   399  moveActiveDown 1;

   400  moveActiveDown 1;

   401  moveActiveDown 1;

   402  moveActiveDown 1;

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

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

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

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

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

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

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

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

   414    writeln (pr_ptree pr_short pt);

   415    get_obj g_tac pt [4];

   416    *)

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

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

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

   422  states:=[];

   423  CalcTree

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

   425    ("Test.thy",

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

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

   428  Iterator 1;

   429  moveActiveRoot 1;

   430  autoCalculate 1 CompleteCalc;

   431  interSteps 1 ([],Res);

   432  moveActiveRoot 1;

   433  moveActiveDown 1;

   434  moveActiveDown 1;

   435  moveActiveDown 1;

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

   438  interSteps 1 ([2],Res);

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

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

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

   443  moveActiveDown 1;

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

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

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

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

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

   451  moveActiveDown 1;

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

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

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

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

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

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

   460  moveActiveDown 1;

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

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

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

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

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

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

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

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

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

   474 states:=[];

   475 CalcTree

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

   477   ("Test.thy",

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

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

   480 Iterator 1;

   481 moveActiveRoot 1;

   482 autoCalculate 1 CompleteCalcHead;

   483 autoCalculate 1 (Step 1);

   484 autoCalculate 1 (Step 1);

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

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

   487   level as the previous formula*)

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

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

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

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

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

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

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

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

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

   499  states:=[];

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

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

   502    ("Test.thy",

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

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

   505  Iterator 1; moveActiveRoot 1;

   506  autoCalculate 1 CompleteCalcHead;

   507  autoCalculate 1 (Step 1);

   508  autoCalculate 1 (Step 1);

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

   511  (*TODO ...*)

   512  setNextTactic 1 (Detail_Set "Test_simplify");

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

   516  val str = pr_ptree pr_short pt;

   517  writeln str;

   519  print_depth 3;

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

author	wneuper
	Sat, 30 Sep 2006 11:39:40 +0200
branch	start_Take
changeset 669	aaa641d8546d
parent 663	231221da44bc
permissions	-rw-r--r--