1.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Thu Oct 13 13:46:30 2011 +0200
1.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Thu Oct 13 15:03:28 2011 +0200
1.3 @@ -596,7 +596,7 @@
1.4 " (equ::bool) = (denom = (0::real));" ^
1.5
1.6 " (L_L::bool list) = (SubProblem (PolyEq'," ^
1.7 -" [abcFormula,degree_2,polynomial,univariate,equation],[no_meth])" ^
1.8 +" [abcFormula,degree_2,polynomial,univariate,equation],[no_met])" ^
1.9 " [BOOL equ, REAL zzz]) " ^
1.10 " in X)"
1.11 ));
1.12 @@ -641,9 +641,7 @@
1.13 val (p,_,f,nxt,_,pt) = me nxt p [] pt; "nxt = Apply_Method";
1.14 val (p,_,f,nxt,_,pt) = me nxt p [] pt; "nxt = Rewrite (ruleZY, Inverse_Z_Transform.ruleZY) --> X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))"; (*TODO naming!*)
1.15 val (p,_,f,nxt,_,pt) = me nxt p [] pt; "nxt = Rewrite_Set norm_Rational --> X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))";
1.16 -*}
1.17 -ML {*
1.18 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; "nxt = Empty_Tac instead of SubProblem";
1.19 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; "nxt = SubProblem";
1.20 *}
1.21 text {* Instead of nxt = Subproblem above we had Empty_Tac; the search for the reason
1.22 considered the following points:
1.23 @@ -666,39 +664,24 @@
1.24 ... shows the right script.difference in the arguments
1.25 # test --- why helpless here ? --- shows: replace no_meth by [no_meth] in Script
1.26 *}
1.27 +
1.28 ML {*
1.29 -print_depth 9999;
1.30 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; "nxt = Empty_Tac instead Model_Problem";
1.31 -print_depth 9999;
1.32 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; "nxt = Model_Problem";
1.33 *}
1.34 text {* Instead of nxt = Model_Problem above we had Empty_Tac; the search for the reason
1.35 considered the following points:difference in the arguments
1.36 # comparison with subsection { *solve equation* }: there solving this equation works,
1.37 - so there must be some difference in the arguments of the Subproblem.
1.38 -
1.39 + so there must be some difference in the arguments of the Subproblem:
1.40 + RIGHT: we had [no_meth] instead of [no_met] ;-))
1.41 *}
1.42 ML {*
1.43 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; "equality (-1 + -2 * z + 8 * z ^^^ 2 = 0)";
1.44 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; "nxt = Add_Given equality (-1 + -2 * z + 8 * z ^^^ 2 = 0)";
1.45 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; "nxt = Add_Given solveFor z";
1.46 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; "nxt = Add_Find solutions z_i";
1.47 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; "nxt = Specify_Theory Isac";
1.48 *}
1.49 -ML {*
1.50 -
1.51 -*}
1.52 -ML {*
1.53 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; "solveFor z";
1.54 -*}
1.55 -ML {*
1.56 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; "nxt = Add_Find";
1.57 -*}
1.58 -ML {*
1.59 -show_pt pt;
1.60 -*}
1.61 -ML {*
1.62 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; "nxt = (Empty_Tac";
1.63 -*}
1.64 -ML {*
1.65 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; "nxt = (Empty_Tac instead Specify_Theory";
1.66 -*}
1.67 -text {* We had "nxt = (Empty_Tac"; the search for the reason considered the following points:
1.68 +text {* We had "nxt = Empty_Tac instead Specify_Theory;
1.69 + the search for the reason considered the following points:
1.70 # was there an error message ? NO --ok
1.71 # has "nxt = Add_Find" been inserted in pt: get_obj g_pbl pt (fst p); YES --ok
1.72 # what is the returned "formula": print_depth 999; f; print_depth 999; --
1.73 @@ -721,50 +704,20 @@
1.74 Or you leave the selection of the appropriate type to isac as done in the final Script ;-))
1.75 *}
1.76 ML {*
1.77 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.78 -*}
1.79 -ML {*
1.80 -
1.81 -*}
1.82 -ML {*
1.83 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; "nxt = Specify_Problem [abcFormula,...";
1.84 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; "nxt = Specify_Method [PolyEq,solve_d2_polyeq_abc_equation";
1.85 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; "nxt = Apply_Method [PolyEq,solve_d2_polyeq_abc_equation";
1.86 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; "nxt = Rewrite_Set_Inst ([(bdv, z)], d2_polyeq_abcFormula_simplify";
1.87 show_pt pt;
1.88 *}
1.89 ML {*
1.90 *}
1.91 ML {*
1.92 -
1.93 -*}
1.94 -ML {*
1.95 -
1.96 -*}
1.97 -ML {*
1.98 -
1.99 -*}
1.100 -ML {*
1.101 -
1.102 -*}
1.103 -
1.104 -ML {*
1.105 -
1.106 -*}
1.107 -ML {*
1.108 -@{theory Isac}
1.109 -*}
1.110 -
1.111 -ML {*
1.112 -*}
1.113 -ML {*
1.114 *}
1.115 ML {*
1.116 *}
1.117
1.118
1.119 -
1.120 -
1.121 -
1.122 -
1.123 -
1.124 -
1.125 section {*Write Tests for Crucial Details*}
1.126 text{*===================================*}
1.127 ML {*
2.1 --- a/test/Tools/isac/Knowledge/partial_fractions.sml Thu Oct 13 13:46:30 2011 +0200
2.2 +++ b/test/Tools/isac/Knowledge/partial_fractions.sml Thu Oct 13 15:03:28 2011 +0200
2.3 @@ -27,10 +27,8 @@
2.4 val (p,_,f,nxt,_,pt) = me nxt p [] pt; "Specify_Problem";
2.5 val (p,_,f,nxt,_,pt) = me nxt p [] pt; "Specify_Method";
2.6 val (p,_,f,nxt,_,pt) = me nxt p [] pt; "nxt = Apply_Method";
2.7 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.8 - "nxt = Rewrite (ruleZY, Inverse_Z_Transform.ruleZY) --> X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))";
2.9 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
2.10 - "nxt = Rewrite_Set norm_Rational --> X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))";
2.11 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; "nxt = Rewrite (ruleZY, Inverse_Z_Transform.ruleZY) --> X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))";
2.12 +val (p''',_,f,nxt''',_,pt''') = me nxt p [] pt; "nxt = Rewrite_Set norm_Rational --> X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))";
2.13 "~~~~~ fun me, args:"; val ((_,tac), (p:pos'), _, (pt:ptree)) = (nxt, p, [], pt);
2.14 val ("ok", (_, _, ptp)) = locatetac tac (pt,p)
2.15 val (pt, p) = ptp;
3.1 --- a/test/Tools/isac/Test_Some.thy Thu Oct 13 13:46:30 2011 +0200
3.2 +++ b/test/Tools/isac/Test_Some.thy Thu Oct 13 15:03:28 2011 +0200
3.3 @@ -1,7 +1,7 @@
3.4
3.5 theory Test_Some imports Isac begin
3.6
3.7 -use"../../../test/Tools/isac/Knowledge/partial_fractions.sml"
3.8 +use"../../../test/Tools/isac/Interpret/rewtools.sml"
3.9
3.10 ML {* (*=================*)
3.11 *}