test/Tools/isac/Interpret/script.sml
branchdecompose-isar
changeset 41969 a350b4ed575b
parent 41924 7407ceef2aed
child 41970 25957ffe68e8
     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 +