test/Tools/isac/Knowledge/partial_fractions.sml
author Walther Neuper <neuper@ist.tugraz.at>
Thu, 13 Oct 2011 15:03:28 +0200
branchdecompose-isar
changeset 42315 c2e6ac4a5d04
parent 42313 f6a46e84067a
child 42352 52ffa99930b2
permissions -rw-r--r--
Build_Inverse_Z_Transform 1 step further

the expected error in isac:
prep. repair Apply_Method without init_form
was a simple error in the CTP-based program
     1 (* Title:  partial fraction decomposition
     2    Author: Jan Rocnik
     3    (c) due to copyright terms
     4 *)
     5 
     6 "--------------------------------------------------------";
     7 "table of contents --------------------------------------";
     8 "--------------------------------------------------------";
     9 "----------- why helpless here ? ------------------------";
    10 "----------- why not nxt = Model_Problem here ? ---------";
    11 "--------------------------------------------------------";
    12 "--------------------------------------------------------";
    13 "--------------------------------------------------------";
    14 
    15 
    16 "----------- why helpless here ? ------------------------";
    17 "----------- why helpless here ? ------------------------";
    18 "----------- why helpless here ? ------------------------";
    19 val fmz = ["filterExpression (X z = 3 / (z - 1/4 + -1/8 * (1/(z::real))))", 
    20   "stepResponse (x[n::real]::bool)"];
    21 val (dI,pI,mI) = ("Isac", ["inverse", "Z_Transform", "SignalProcessing"], 
    22   ["SignalProcessing","Z_Transform","inverse"]);
    23 val (p,_,f,nxt,_,pt)  = CalcTreeTEST [(fmz, (dI,pI,mI))]; 
    24 val (p,_,f,nxt,_,pt) = me nxt p [] pt; "Add_Given";
    25 val (p,_,f,nxt,_,pt) = me nxt p [] pt; "Add_Find";
    26 val (p,_,f,nxt,_,pt) = me nxt p [] pt; "Specify_Theory";
    27 val (p,_,f,nxt,_,pt) = me nxt p [] pt; "Specify_Problem";
    28 val (p,_,f,nxt,_,pt) = me nxt p [] pt; "Specify_Method";
    29 val (p,_,f,nxt,_,pt) = me nxt p [] pt; "nxt = Apply_Method";
    30 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))";
    31 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)))";
    32 "~~~~~ fun me, args:"; val ((_,tac), (p:pos'), _, (pt:ptree)) = (nxt, p, [], pt);
    33 val ("ok", (_, _, ptp)) = locatetac tac (pt,p)
    34 val (pt, p) = ptp;
    35 "~~~~~ fun step, args:"; val (((ip as (_,p_)):pos'), ((ptp as (pt,p), tacis):calcstate)) = 
    36                            (p, ((pt, e_pos'),[]));
    37 val pIopt = get_pblID (pt,ip);
    38 ip = ([],Res); "false";
    39 tacis; " = []";
    40 pIopt; (* = SOME ["inverse", "Z_Transform", "SignalProcessing"]*)
    41 member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); "false";
    42 (*nxt_solve_ (pt,ip); "WAS isalist2list applied to NON-list 'no_meth'"
    43    THIS MEANS: replace no_meth by [no_meth] in Script.*)
    44 (*WAS val ("helpless",_) = step p ((pt, e_pos'),[]) *)
    45 (*WAS val (p,_,f,nxt,_,pt) = me nxt p [] pt; "Empty_Tac instead SubProblem";*)
    46 
    47 "----------- why not nxt = Model_Problem here ? ---------";
    48 "----------- why not nxt = Model_Problem here ? ---------";
    49 "----------- why not nxt = Model_Problem here ? ---------";
    50 val (p,_,f,nxt,_,pt) = me nxt''' p''' [] pt'''; 
    51 "~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), _, (pt:ptree)) = (nxt, p, c, pt);
    52 val ("ok", (_, _, ptp)) = locatetac tac (pt,p);
    53 val (pt, p) = ptp;
    54 "~~~~~ fun step, args:"; val (((ip as (_,p_)):pos'), ((ptp as (pt,p), tacis):calcstate)) =
    55                            (p, ((pt, e_pos'),[]));
    56 val pIopt = get_pblID (pt,ip);
    57 ip = ([],Res); " = false";
    58 tacis; " = []";                                         
    59 pIopt (* = SOME ["inverse", "Z_Transform", "SignalProcessing"]*);
    60 member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); " = false";
    61 (*                               ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ leads into
    62 nxt_solve_, which is definitely WRONG (should be nxt_specify_ for FIND_ADD).
    63 This ERROR seems to be introduced together with ctxt, concerns Apply_Method without init_form.
    64 See TODO.txt
    65 *)
    66