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