1.1 --- a/test/Tools/isac/Interpret/script.sml Tue May 03 11:16:55 2011 +0200
1.2 +++ b/test/Tools/isac/Interpret/script.sml Tue May 03 15:58:04 2011 +0200
1.3 @@ -12,10 +12,12 @@
1.4 "----------- WN0509 why does next_tac doesnt find Substitute -----";
1.5 "----------- WN0509 Substitute 2nd part --------------------------";
1.6 "----------- fun sel_appl_atomic_tacs ----------------------------";
1.7 +"----------- fun init_form, fun get_stac -------------------------";
1.8 "-----------------------------------------------------------------";
1.9 "-----------------------------------------------------------------";
1.10 "-----------------------------------------------------------------";
1.11
1.12 +(*========== inhibit exn 110503 ================================================
1.13
1.14 "----------- WN0509 why does next_tac doesnt find Substitute -----";
1.15 "----------- WN0509 why does next_tac doesnt find Substitute -----";
1.16 @@ -247,4 +249,37 @@
1.17 \1 stac too low";
1.18 applyTactic 1 p (hd appltacs);
1.19 autoCalculate 1 CompleteCalc;
1.20 +============ inhibit exn 110503 ==============================================*)
1.21
1.22 +"----------- fun init_form, fun get_stac -------------------------";
1.23 +"----------- fun init_form, fun get_stac -------------------------";
1.24 +"----------- fun init_form, fun get_stac -------------------------";
1.25 +val fmz = ["equality (x+1=(2::real))", "solveFor x", "solutions L"];
1.26 +val (dI',pI',mI') = ("Test",["sqroot-test","univariate","equation","test"],
1.27 + ["Test","squ-equ-test-subpbl1"]);
1.28 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.29 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.30 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.31 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.32 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.33 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.34 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.35 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.36 +"~~~~~ fun me, args:"; val (_,tac) = nxt;
1.37 +"~~~~~ fun locatetac, args:"; val ptp as (pt, p) = (pt, p);
1.38 +val (mI,m) = mk_tac'_ tac;
1.39 +val Appl m = applicable_in p pt m;
1.40 +member op = specsteps mI; (*false*)
1.41 +"~~~~~ fun loc_solve_, args:"; val (m, (pt, pos) ) = ((mI, m), ptp);
1.42 +"~~~~~ fun solve, args:"; val (("Apply_Method", Apply_Method' (mI,_,_,_)), pos as (p,_)) = (m, pos);
1.43 +val {srls, ...} = get_met mI;
1.44 +val PblObj {meth=itms, ...} = get_obj I pt p;
1.45 +val thy' = get_obj g_domID pt p;
1.46 +val thy = assoc_thy thy';
1.47 +val (is as ScrState (env,_,_,_,_,_), ctxt, sc) = init_scrstate thy itms mI;
1.48 +val ini = init_form thy sc env;
1.49 +"----- fun init_form, args:"; val (Script sc) = sc;
1.50 +"----- fun get_stac, args:"; val (y, h $ body) = (thy, sc);
1.51 +case get_stac thy sc of SOME (Free ("e_e", _)) => ()
1.52 +| _ => error "script: Const (?, ?) in script (as term) changed";;
1.53 +