wneuper/isa: test/Tools/isac/Test

     1 (* Title:  run tests on a particular test file

     2    Author: Walther Neuper 101001

     3    (c) copyright due to lincense terms.

     4 *)

     6 theory Test_Some imports Isac begin

     8 ML{* writeln "**** run the test ***************************************" *}

    10 use"../../../test/Tools/isac/Interpret/script.sml"

    12 ML{*

    16 (* Title: tests on solve.sml

    17    Author: Walther Neuper 060508,

    18    (c) due to copyright terms

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

    21 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

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

    23 which in turn

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

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

    27 use"solve.sml";

    28 *)

    30 "-----------------------------------------------------------------";

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    49 "-----------------------------------------------------------------";

    50 "-----------------------------------------------------------------";

    51 "-----------------------------------------------------------------";

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

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

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

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

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

    59 	    ("Rational",

    60 	     ["rational","simplification"],

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

    62  moveActiveRoot 1;

    63  autoCalculate 1 CompleteCalc;

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

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

    67        \  ((Rewrite_Set norm_Rational False) t_)"

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

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

    70 interSteps 1 ([1], Res);

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

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

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

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

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

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

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

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

    82 --------------------------------------------------------------------*)

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

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

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

    87 interSteps 1 ([1], Res);

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

    89 *)

    90 interSteps 1 ([6], Res);

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

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

    94 (*========== inhibit exn AK110721 ================================================

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

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

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

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

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

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

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

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

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

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

   109 val intermediate_ptyps = !ptyps;

   110 val intermediate_mets = !mets;

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

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

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

   115 store_pbt

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

   117  (["test"],

   118   [],

   119   e_rls, NONE, []));

   120 store_pbt

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

   122  (["detail","test"],

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

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

   125    ],

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

   128 store_met

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

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

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

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

   133    ],

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

   135    crls=tval_rls, nrls=e_rls(*,

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

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

   138  \(((Rewrite_Set expand_binoms False) @@\

   139  \  (Rewrite_Set cancel False)) g_)"

   140  ));

   141 store_met

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

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

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

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

   146    ],

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

   148    crls=tval_rls, nrls=e_rls(*,

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

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

   151  \(((Rewrite_Set make_polynomial False) @@\

   152  \  (Rewrite_Set cancel_p False)) g_)"

   153  ));

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

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

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

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

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

   161 	   "realTestFind s"];

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

   163   ("Test",["detail","test"],["Test","test_detail_binom"]);

   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","test_detail"))*)

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

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

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

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

   181  val str = pr_ptree pr_short pt;

   182  writeln str;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   211 #########################################################################

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

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

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

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

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

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

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

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

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

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

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

   223 (*15.10.02*)

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

   225 (*

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

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

   228 *)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   246 	   "realTestFind s"];

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   264  (*14.3.03*)

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

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

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

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

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

   270  cancel_p_ thy t;

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

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

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

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

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

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

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

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

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

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

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

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

   284  (*14.3.03*)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   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;

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

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

   347 ----------------------------------------------------------------------*)

   349 (*---------------

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

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

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

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

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

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

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

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

   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) handle e => OldGoals.print_exn e;

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

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

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

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

   366 ----------------*)

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

   373 	   "realTestFind s"];

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   397 -------------------------------------------------------------------------*)

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

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

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

   403  states:=[];

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

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

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

   407  Iterator 1;

   408  moveActiveRoot 1;

   409  autoCalculate 1 CompleteCalc;

   410  moveActiveRoot 1;

   412  interSteps 1 ([],Res);

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

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

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

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

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

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

   420  moveActiveDown 1;

   421  moveActiveDown 1;

   422  moveActiveDown 1;

   423  moveActiveDown 1;

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

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

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

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

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

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

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

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

   435    writeln (pr_ptree pr_short pt);

   436    get_obj g_tac pt [4];

   437    *)

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

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

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

   443  states:=[];

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

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

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

   447  Iterator 1;

   448  moveActiveRoot 1;

   449  autoCalculate 1 CompleteCalc;

   450  interSteps 1 ([],Res);

   451  moveActiveRoot 1;

   452  moveActiveDown 1;

   453  moveActiveDown 1;

   454  moveActiveDown 1;

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

   457  interSteps 1 ([2],Res);

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

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

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

   462  moveActiveDown 1;

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

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

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

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

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

   470  moveActiveDown 1;

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

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

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

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

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

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

   479  moveActiveDown 1;

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

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

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

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

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

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

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

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

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

   493 states:=[];

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

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

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

   497 Iterator 1;

   498 moveActiveRoot 1;

   499 autoCalculate 1 CompleteCalcHead;

   500 autoCalculate 1 (Step 1);

   501 autoCalculate 1 (Step 1);

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

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

   504   level as the previous formula*)

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

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

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

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

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

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

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

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

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

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

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

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

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

   520  Iterator 1; moveActiveRoot 1;

   521  autoCalculate 1 CompleteCalcHead;

   522  autoCalculate 1 (Step 1);

   523  autoCalculate 1 (Step 1);

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

   526  (*TODO ...*)

   527  setNextTactic 1 (Detail_Set "Test_simplify");

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

   531  val str = pr_ptree pr_short pt;

   532  writeln str;

   534  print_depth 3;

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

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

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

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

   543 ptyps:= intermediate_ptyps;

   544 mets:= intermediate_mets;

   545 ========== inhibit exn AK110721 ================================================*)

   550 *}

   551 ML{*

   552 *}

   553 ML{*

   554 *}

   555 ML{*

   556 *}

   557 ML{*

   558 *}

   559 ML{*

   560 "~~~~~ fun , args:"; val () = ();

   561 *}

   562 end

   565 (*========== inhibit exn 110719 ================================================

   566 ============ inhibit exn 110719 ==============================================*)

   569 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.

   570 -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)

author	Alexander Kargl <akargl@brgkepler.net>
	Fri, 22 Jul 2011 17:09:35 +0200
branch	decompose-isar
changeset 42171	4156f9e75464
parent 42170	6a5ed9444736
child 42176	3573fd729e99
child 42177	c96da633a273
child 42196	f5f726ef4f6a
permissions	-rw-r--r--