1.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy	Tue Oct 11 15:41:44 2011 +0200
     1.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy	Tue Oct 11 16:43:02 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_meth])" ^
     1.9  "        [BOOL equ, REAL zzz])              " ^
    1.10  "  in X)"
    1.11   ));
    1.12 @@ -630,7 +630,9 @@
    1.13    "stepResponse (x[n::real]::bool)"];
    1.14  val (dI,pI,mI) = ("Isac", ["inverse", "Z_Transform", "SignalProcessing"], 
    1.15    ["SignalProcessing","Z_Transform","inverse"]);
    1.16 -val (p,_,f,nxt,_,pt)  = CalcTreeTEST [(fmz, (dI,pI,mI))]; 
    1.17 +val (p,_,f,nxt,_,pt)  = CalcTreeTEST [(fmz, (dI,pI,mI))];
    1.18 +*}
    1.19 +ML {*
    1.20  val (p,_,f,nxt,_,pt) = me nxt p [] pt; "Add_Given";
    1.21  val (p,_,f,nxt,_,pt) = me nxt p [] pt; "Add_Find";
    1.22  val (p,_,f,nxt,_,pt) = me nxt p [] pt; "Specify_Theory";
    1.23 @@ -658,10 +660,10 @@
    1.24       [BOOL (-1 + -2 * z + 8 * z ^^^ 2 = 0), REAL z]'
    1.25      ... and see the SubProblem with correct arguments from searching next step
    1.26      (program text !!!--->!!! STac (script tactic) with arguments evaluated.)
    1.27 -  # do we have the right Script ...
    1.28 +  # do we have the right Script ...difference in the argumentsdifference in the arguments
    1.29      val Script s = (#scr o get_met) ["SignalProcessing","Z_Transform","inverse"];
    1.30      writeln (term2str s);
    1.31 -    ... shows the right script.
    1.32 +    ... shows the right script.difference in the arguments
    1.33    # test --- why helpless here ? --- shows: replace no_meth by [no_meth] in Script
    1.34  *}
    1.35  ML {*
    1.36 @@ -670,7 +672,7 @@
    1.37  print_depth 9999;
    1.38  *}
    1.39  text {* Instead of nxt = Model_Problem above we had Empty_Tac; the search for the reason 
    1.40 -  considered the following points:
    1.41 +  considered the following points:difference in the arguments
    1.42    # comparison with subsection { *solve equation* }: there solving this equation works,
    1.43      so there must be some difference in the arguments of the Subproblem.
    1.44  

     2.1 --- a/test/Tools/isac/Knowledge/partial_fractions.sml	Tue Oct 11 15:41:44 2011 +0200
     2.2 +++ b/test/Tools/isac/Knowledge/partial_fractions.sml	Tue Oct 11 16:43:02 2011 +0200
     2.3 @@ -7,6 +7,7 @@
     2.4  "table of contents --------------------------------------";
     2.5  "--------------------------------------------------------";
     2.6  "----------- why helpless here ? ------------------------";
     2.7 +"----------- why not nxt = Model_Problem here ? ---------";
     2.8  "--------------------------------------------------------";
     2.9  "--------------------------------------------------------";
    2.10  "--------------------------------------------------------";
    2.11 @@ -45,3 +46,7 @@
    2.12  (*WAS val ("helpless",_) = step p ((pt, e_pos'),[]) *)
    2.13  (*WAS val (p,_,f,nxt,_,pt) = me nxt p [] pt; "Empty_Tac instead SubProblem";*)
    2.14  
    2.15 +"----------- why not nxt = Model_Problem here ? ---------";
    2.16 +"----------- why not nxt = Model_Problem here ? ---------";
    2.17 +"----------- why not nxt = Model_Problem here ? ---------";
    2.18 +

     3.1 --- a/test/Tools/isac/Test_Some.thy	Tue Oct 11 15:41:44 2011 +0200
     3.2 +++ b/test/Tools/isac/Test_Some.thy	Tue Oct 11 16:43:02 2011 +0200
     3.3 @@ -10,6 +10,73 @@
     3.4  use"../../../test/Tools/isac/Knowledge/partial_fractions.sml" 
     3.5  
     3.6  ML {* (*=================*)
     3.7 +"----------- why helpless here ? ------------------------";
     3.8 +val fmz = ["filterExpression (X z = 3 / (z - 1/4 + -1/8 * (1/(z::real))))", 
     3.9 +  "stepResponse (x[n::real]::bool)"];
    3.10 +val (dI,pI,mI) = ("Isac", ["inverse", "Z_Transform", "SignalProcessing"], 
    3.11 +  ["SignalProcessing","Z_Transform","inverse"]);
    3.12 +val (p,_,f,nxt,_,pt)  = CalcTreeTEST [(fmz, (dI,pI,mI))]; 
    3.13 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; "Add_Given";
    3.14 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; "Add_Find";
    3.15 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; "Specify_Theory";
    3.16 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; "Specify_Problem";
    3.17 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; "Specify_Method";
    3.18 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; "nxt = Apply_Method";
    3.19 +*}
    3.20 +ML{*
    3.21 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; 
    3.22 +  "nxt = Rewrite (ruleZY, Inverse_Z_Transform.ruleZY) --> X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))";
    3.23 +*}
    3.24 +ML{*
    3.25 +val (p''',_,f,nxt''',_,pt''') = me nxt p [] pt; 
    3.26 +  "nxt = Rewrite_Set norm_Rational --> X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))";
    3.27 +*}
    3.28 +ML{*
    3.29 +"~~~~~ fun me, args:"; val ((_,tac), (p:pos'), _, (pt:ptree)) = (nxt, p, [], pt);
    3.30 +val ("ok", (_, _, ptp)) = locatetac tac (pt,p)
    3.31 +val (pt, p) = ptp;
    3.32 +"~~~~~ fun step, args:"; val (((ip as (_,p_)):pos'), ((ptp as (pt,p), tacis):calcstate)) = 
    3.33 +                           (p, ((pt, e_pos'),[]));
    3.34 +val pIopt = get_pblID (pt,ip);
    3.35 +ip = ([],Res); "false";
    3.36 +tacis; " = []";
    3.37 +pIopt; (* = SOME ["inverse", "Z_Transform", "SignalProcessing"]*)
    3.38 +member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); "false";
    3.39 +(*nxt_solve_ (pt,ip); "WAS isalist2list applied to NON-list 'no_meth'"
    3.40 +   THIS MEANS: replace no_meth by [no_meth] in Script.*)
    3.41 +(*WAS val ("helpless",_) = step p ((pt, e_pos'),[]) *)
    3.42 +(*WAS val (p,_,f,nxt,_,pt) = me nxt p [] pt; "Empty_Tac instead SubProblem";*)
    3.43 +*}
    3.44 +ML{*
    3.45 +"----------- why not nxt = Model_Problem here ? ---------";
    3.46 +val (p,_,f,nxt,_,pt) = me nxt''' p''' [] pt'''; 
    3.47 +"~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), _, (pt:ptree)) = (nxt, p, c, pt);
    3.48 +val ("ok", (_, _, ptp)) = locatetac tac (pt,p);
    3.49 +val (pt, p) = ptp;
    3.50 +"~~~~~ fun step, args:"; val (((ip as (_,p_)):pos'), ((ptp as (pt,p), tacis):calcstate)) =
    3.51 +                           (p, ((pt, e_pos'),[]));
    3.52 +val pIopt = get_pblID (pt,ip);
    3.53 +ip = ([],Res); " = false";
    3.54 +tacis; " = []";
    3.55 +pIopt (* = SOME ["inverse", "Z_Transform", "SignalProcessing"]*);
    3.56 +member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); " = true";
    3.57 +"~~~~~ fun nxt_specify_, args:"; val ((ptp as (pt, pos as (p,p_)))) = ((pt, ip));
    3.58 +val pblobj as (PblObj{meth,origin=origin as (oris,(dI',pI',mI'),_),
    3.59 +			  probl,spec=(dI,pI,mI), ...}) = get_obj I pt p;
    3.60 +just_created_ pblobj (*by Subproblem*) andalso origin <> e_origin; "true";
    3.61 +*}
    3.62 +ML{*
    3.63 + mI' = ["no_meth"];
    3.64 +*}
    3.65 +ML{*
    3.66 +nxt_specif (Refine_Tacitly pI') (pt, (p, Pbl))
    3.67 +*}
    3.68 +ML{*
    3.69 +*}
    3.70 +ML{*
    3.71 +(*WAS nxt_specify_ (pt, ip) get_pbt not found: ["no_meth"]*)
    3.72 +(*WAS val ("helpless",_) = step p ((pt, e_pos'),[])*)
    3.73 +(*WAS val (p,_,f,nxt,_,pt) = me nxt p [] pt; "nxt = Empty_Tac instead Model_Problem";*)
    3.74  *}
    3.75  ML{*
    3.76  show_pt pt;