wneuper/isa: src/Pure/isac/smltest/ME/solve.sml@875b6efa7ced

     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 "###### val intermediate_ptyps = !ptyps;val intermediate_mets = !mets";

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    37 "-----------------------------------------------------------------";

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

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

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

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

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

    45 	   ("Rational.thy",

    46 	    ["rational","simplification"],

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

    48 moveActiveRoot 1;

    49 autoCalculate 1 CompleteCalc;

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

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

    53        \  ((Rewrite_Set norm_Rational False) t_)"

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

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

    56 interSteps 1 ([1], Res);

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

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

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

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

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

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

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

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

    68 --------------------------------------------------------------------*)

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

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

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

    73 interSteps 1 ([1], Res);

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

    75 *)

    76 interSteps 1 ([6], Res);

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

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

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

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

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

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

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

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

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

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

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

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

    94 val intermediate_ptyps = !ptyps;

    95 val intermediate_mets = !mets;

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

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

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

   100 store_pbt

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

   102  (["test"],

   103   [],

   104   e_rls, None, []));

   105 store_pbt

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

   107  (["detail","test"],

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

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

   110    ],

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

   113 store_met

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

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

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

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

   118    ],

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

   120    crls=tval_rls, nrls=e_rls(*,

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

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

   123  \(((Rewrite_Set expand_binoms False) @@\

   124  \  (Rewrite_Set cancel False)) g_)"

   125  ));

   126 store_met

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

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

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

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

   131    ],

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

   133    crls=tval_rls, nrls=e_rls(*,

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

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

   136  \(((Rewrite_Set make_polynomial False) @@\

   137  \  (Rewrite_Set cancel_p False)) g_)"

   138  ));

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

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

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

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

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

   146 	   "realTestFind s"];

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   166  val str = pr_ptree pr_short pt;

   167  writeln str;

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

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

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

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

   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;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   196 #########################################################################

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

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

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

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

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

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

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

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

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

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

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

   208 (*15.10.02*)

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

   210 (*

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

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

   213 *)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   231 	   "realTestFind s"];

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   249  (*14.3.03*)

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

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

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

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

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

   255  cancel_p_ thy t;

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

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

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

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

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

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

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

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

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

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

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

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

   269  (*14.3.03*)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   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  if nxt = ("End_Detail",End_Detail) then ()

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

   332 ----------------------------------------------------------------------*)

   334 (*---------------

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   351 ----------------*)

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

   358 	   "realTestFind s"];

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   382 -------------------------------------------------------------------------*)

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

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

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

   388  states:=[];

   389  CalcTree

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

   391    ("Test.thy",

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

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

   394  Iterator 1;

   395  moveActiveRoot 1;

   396  autoCalculate 1 CompleteCalc;

   397  moveActiveRoot 1;

   399  interSteps 1 ([],Res);

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

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

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

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

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

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

   407  moveActiveDown 1;

   408  moveActiveDown 1;

   409  moveActiveDown 1;

   410  moveActiveDown 1;

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

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

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

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

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

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

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

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

   422    writeln (pr_ptree pr_short pt);

   423    get_obj g_tac pt [4];

   424    *)

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

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

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

   430  states:=[];

   431  CalcTree

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

   433    ("Test.thy",

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

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

   436  Iterator 1;

   437  moveActiveRoot 1;

   438  autoCalculate 1 CompleteCalc;

   439  interSteps 1 ([],Res);

   440  moveActiveRoot 1;

   441  moveActiveDown 1;

   442  moveActiveDown 1;

   443  moveActiveDown 1;

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

   446  interSteps 1 ([2],Res);

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

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

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

   451  moveActiveDown 1;

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

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

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

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

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

   459  moveActiveDown 1;

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

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

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

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

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

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

   468  moveActiveDown 1;

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

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

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

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

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

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

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

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

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

   482 states:=[];

   483 CalcTree

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

   485   ("Test.thy",

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

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

   488 Iterator 1;

   489 moveActiveRoot 1;

   490 autoCalculate 1 CompleteCalcHead;

   491 autoCalculate 1 (Step 1);

   492 autoCalculate 1 (Step 1);

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

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

   495   level as the previous formula*)

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

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

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

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

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

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

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

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

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

   507  states:=[];

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

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

   510    ("Test.thy",

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

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

   513  Iterator 1; moveActiveRoot 1;

   514  autoCalculate 1 CompleteCalcHead;

   515  autoCalculate 1 (Step 1);

   516  autoCalculate 1 (Step 1);

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

   519  (*TODO ...*)

   520  setNextTactic 1 (Detail_Set "Test_simplify");

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

   524  val str = pr_ptree pr_short pt;

   525  writeln str;

   527  print_depth 3;

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

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

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

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

   536 ptyps:= intermediate_ptyps;

   537 mets:= intermediate_mets;

author	Walther Neuper <neuper@ist.tugraz.at>
	Wed, 21 Jul 2010 13:53:39 +0200
branch	isac-from-Isabelle2009-2
changeset 37871	875b6efa7ced
permissions	-rw-r--r--