test/Tools/isac/Minisubpbl/300-init-subpbl.sml
author Walther Neuper <neuper@ist.tugraz.at>
Fri, 13 May 2011 09:28:38 +0200
branchdecompose-isar
changeset 41986 64efbbbed4b4
parent 41985 cb8ea2269e6f
child 42011 6a9ba30ab6bc
permissions -rw-r--r--
tuned
neuper@41985
     1
(* Title:  300-init-subpbl.sml
neuper@41985
     2
   Author: Walther Neuper 1105
neuper@41985
     3
   (c) copyright due to lincense terms.
neuper@41985
     4
*)
neuper@41985
     5
neuper@41985
     6
val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
neuper@41985
     7
val (dI',pI',mI') =
neuper@41985
     8
  ("Test", ["sqroot-test","univariate","equation","test"],
neuper@41985
     9
   ["Test","squ-equ-test-subpbl1"]);
neuper@41985
    10
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@41985
    11
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@41986
    12
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@41986
    13
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@41986
    14
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@41986
    15
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@41986
    16
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@41986
    17
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@41986
    18
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@41986
    19
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@41986
    20
val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Subproblem"*)
neuper@41986
    21
"~~~~~ fun me, args:"; val (_,tac) = nxt;
neuper@41986
    22
"~~~~~ fun locatetac, args:"; val (tac, ptp as (pt, p)) = (tac, (pt,p));
neuper@41986
    23
val (mI,m) = mk_tac'_ tac;
neuper@41986
    24
val Appl m = applicable_in p pt m;
neuper@41986
    25
neuper@41985
    26
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@41986
    27
case nxt of ("Model_Problem", _) => ()
neuper@41986
    28
| _ => error "minisubpbl: CalcTreeTEST has no nxt = Model_Problem";
neuper@41986
    29