test/Tools/isac/Knowledge/partial_fractions.sml
branchdecompose-isar
changeset 42305 3ff2cf70f845
parent 42301 93083d4e05d8
child 42310 55931ca19f4d
     1.1 --- a/test/Tools/isac/Knowledge/partial_fractions.sml	Fri Oct 07 16:54:31 2011 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/partial_fractions.sml	Tue Oct 11 10:59:42 2011 +0200
     1.3 @@ -6,10 +6,42 @@
     1.4  "--------------------------------------------------------";
     1.5  "table of contents --------------------------------------";
     1.6  "--------------------------------------------------------";
     1.7 -"----------- get_denominator ----------------------------";
     1.8 +"----------- why helpless here ? ------------------------";
     1.9  "--------------------------------------------------------";
    1.10  "--------------------------------------------------------";
    1.11  "--------------------------------------------------------";
    1.12  
    1.13  
    1.14 +"----------- why helpless here ? ------------------------";
    1.15 +"----------- why helpless here ? ------------------------";
    1.16 +"----------- why helpless here ? ------------------------";
    1.17 +val fmz = ["filterExpression (X z = 3 / (z - 1/4 + -1/8 * (1/(z::real))))", 
    1.18 +  "stepResponse (x[n::real]::bool)"];
    1.19 +val (dI,pI,mI) = ("Isac", ["inverse", "Z_Transform", "SignalProcessing"], 
    1.20 +  ["SignalProcessing","Z_Transform","inverse"]);
    1.21 +val (p,_,f,nxt,_,pt)  = CalcTreeTEST [(fmz, (dI,pI,mI))]; 
    1.22 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; "Add_Given";
    1.23 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; "Add_Find";
    1.24 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; "Specify_Theory";
    1.25 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; "Specify_Problem";
    1.26 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; "Specify_Method";
    1.27 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; "nxt = Apply_Method";
    1.28 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; 
    1.29 +  "nxt = Rewrite (ruleZY, Inverse_Z_Transform.ruleZY) --> X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))";
    1.30 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; 
    1.31 +  "nxt = Rewrite_Set norm_Rational --> X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))";
    1.32 +"~~~~~ fun me, args:"; val ((_,tac), (p:pos'), _, (pt:ptree)) = (nxt, p, [], pt);
    1.33 +val ("ok", (_, _, ptp)) = locatetac tac (pt,p)
    1.34 +val (pt, p) = ptp;
    1.35 +"~~~~~ fun step, args:"; val (((ip as (_,p_)):pos'), ((ptp as (pt,p), tacis):calcstate)) = 
    1.36 +                           (p, ((pt, e_pos'),[]));
    1.37 +val pIopt = get_pblID (pt,ip);
    1.38 +ip = ([],Res); "false";
    1.39 +tacis; " = []";
    1.40 +pIopt; (* = SOME ["inverse", "Z_Transform", "SignalProcessing"]*)
    1.41 +member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); "false";
    1.42 +(*nxt_solve_ (pt,ip); "WAS isalist2list applied to NON-list 'no_meth'"
    1.43 +   THIS MEANS: replace no_meth by [no_meth] in Script.*)
    1.44 +(*WAS val ("helpless",_) = step p ((pt, e_pos'),[]) *)
    1.45 +(*WAS val (p,_,f,nxt,_,pt) = me nxt p [] pt; "Empty_Tac instead SubProblem";*)
    1.46