1.1 --- a/test/Tools/isac/Interpret/script.sml	Tue May 03 16:23:07 2011 +0200
     1.2 +++ b/test/Tools/isac/Interpret/script.sml	Wed May 04 09:01:10 2011 +0200
     1.3 @@ -13,6 +13,7 @@
     1.4  "----------- WN0509 Substitute 2nd part --------------------------";
     1.5  "----------- fun sel_appl_atomic_tacs ----------------------------";
     1.6  "----------- fun init_form, fun get_stac -------------------------";
     1.7 +"----------- x+1=2 start SubProblem 'stac2tac_ TODO: no match for ";
     1.8  "-----------------------------------------------------------------";
     1.9  "-----------------------------------------------------------------";
    1.10  "-----------------------------------------------------------------";
    1.11 @@ -281,3 +282,51 @@
    1.12  case get_stac thy sc of SOME (Free ("e_e", _)) => ()
    1.13  | _ => error "script: Const (?, ?) in script (as term) changed";;
    1.14  
    1.15 +
    1.16 +"----------- x+1=2 start SubProblem 'stac2tac_ TODO: no match for ";
    1.17 +"----------- x+1=2 start SubProblem 'stac2tac_ TODO: no match for ";
    1.18 +"----------- x+1=2 start SubProblem 'stac2tac_ TODO: no match for ";
    1.19 +val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
    1.20 +val (dI',pI',mI') =
    1.21 +  ("Test", ["sqroot-test","univariate","equation","test"],
    1.22 +   ["Test","squ-equ-test-subpbl1"]);
    1.23 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
    1.24 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.25 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.26 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.27 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.28 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.29 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.30 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.31 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.32 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.33 +(*val (p,_,f,nxt,_,pt) = me nxt p [1] pt; WAS: Empty_Tac, helpless*)
    1.34 +show_pt pt;
    1.35 +"~~~~~ fun me, args:"; val (_,tac) = nxt;
    1.36 +    val (pt, p) = 
    1.37 +	    (*locatetac is here for testing by me; step would suffice in me*)
    1.38 +	    case locatetac tac (pt,p) of
    1.39 +		      ("ok", (_, _, ptp))  => ptp | _ => error "test";
    1.40 +"~~~~~ fun step, args:"; val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'), []))
    1.41 +val pIopt = get_pblID (pt,ip);
    1.42 +tacis; (*= []*)
    1.43 +pIopt; (*= SOME ["sqroot-test", "univariate", ...]*)
    1.44 +member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); (*= false*)
    1.45 +"~~~~~ fun nxt_solve_, args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
    1.46 +                                 (*WAS stac2tac_ TODO: no match for SubProblem*)
    1.47 +val thy' = get_obj g_domID pt (par_pblobj pt p);
    1.48 +val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
    1.49 +"~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt,(p,_)):ptree * pos'), (sc as Script (h $ body)), 
    1.50 +	                               (ScrState (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is);
    1.51 +l; (*= [R, L, R, L, R, R]*)
    1.52 +val Appy (m', scrst as (_,_,_,v,_,_)) = nstep_up thy ptp sc E l Skip_ a v;
    1.53 +"~~~~~ dont like to go into nstep_up...";
    1.54 +val t = str2term ("SubProblem" ^ 
    1.55 +  "(Test', [linear, univariate, equation, test], [Test, solve_linear])" ^
    1.56 +  "[BOOL (-1 + x = 0), REAL x]");
    1.57 +val (tac, tac_) = stac2tac_ pt @{theory "Isac"} t; (*WAS stac2tac_ TODO: no match for SubProblem*)
    1.58 +case tac_ of 
    1.59 +  Subproblem' _ => ()
    1.60 +| _ => error "script.sml x+1=2 start SubProblem from script";
    1.61 +
    1.62 +