1.1 --- a/src/Tools/isac/Interpret/script.sml	Fri May 20 08:32:57 2011 +0200
     1.2 +++ b/src/Tools/isac/Interpret/script.sml	Fri May 20 09:12:40 2011 +0200
     1.3 @@ -1588,6 +1588,9 @@
     1.4  			      "actuals: " ^ terms2str actuals)
     1.5       val env = relate_args [] formals actuals;
     1.6       val ctxt = ProofContext.init_global thy |> declare_constraints' actuals
     1.7 +     val {pre, prls, ...} = get_met metID;
     1.8 +     val pres = check_preconds thy prls pre itms |> map snd;
     1.9 +     (*val ctxt = ctxt |> insert_assumptions pres;*)
    1.10     in (ScrState (env,[],NONE,e_term,Safe,true), ctxt, scr):istate * Proof.context * scr end;
    1.11  
    1.12  (* decide, where to get script/istate from:

     2.1 --- a/test/Tools/isac/Minisubpbl/200-start-method.sml	Fri May 20 08:32:57 2011 +0200
     2.2 +++ b/test/Tools/isac/Minisubpbl/200-start-method.sml	Fri May 20 09:12:40 2011 +0200
     2.3 @@ -32,17 +32,61 @@
     2.4  val {srls, pre, prls, ...} = get_met mI;
     2.5  val pres = check_preconds thy prls pre meth |> map snd;
     2.6  val ctxt = ctxt |> insert_assumptions pres;
     2.7 -val (is as ScrState (env,_,_,_,_,_), _, sc) = init_scrstate thy meth mI;
     2.8 -val ini = init_form thy sc env;
     2.9 +val (is'''' as ScrState (env'''',_,_,_,_,_), _, sc'''') = init_scrstate thy meth mI;
    2.10 +"~~~~~ fun init_scrstate, args:"; val (thy, itms, metID) = (thy, meth, mI)
    2.11 +    val actuals = itms2args thy metID itms
    2.12 +	  val scr as Script sc = (#scr o get_met) metID
    2.13 +    val formals = formal_args sc    
    2.14 +	  (*expects same sequence of (actual) args in itms and (formal) args in met*)
    2.15 +	  fun relate_args env [] [] = env
    2.16 +	    | relate_args env _ [] = 
    2.17 +	        error ("ERROR in creating the environment for '" ^
    2.18 +			    id_of_scr sc ^ "' from \nthe items of the guard of " ^
    2.19 +			    metID2str metID ^ ",\n" ^
    2.20 +			    "formal arg(s), from the script, miss actual arg(s), from the guards env:\n" ^
    2.21 +			    (string_of_int o length) formals ^
    2.22 +			    " formals: " ^ terms2str formals ^ "\n" ^
    2.23 +			    (string_of_int o length) actuals ^
    2.24 +			    " actuals: " ^ terms2str actuals)
    2.25 +	    | relate_args env [] actual_finds = env (*may drop Find!*)
    2.26 +	    | relate_args env (a::aa) (f::ff) = 
    2.27 +	        if type_of a = type_of f 
    2.28 +	        then relate_args (env @ [(a, f)]) aa ff
    2.29 +          else 
    2.30 +	          error ("ERROR in creating the environment for '" ^
    2.31 +			      id_of_scr sc ^ "' from \nthe items of the guard of " ^
    2.32 +			      metID2str metID ^ ",\n" ^
    2.33 +			      "different types of formal arg, from the script, " ^
    2.34 +			      "and actual arg, from the guards env:'\n" ^
    2.35 +			      "formal: '" ^ term2str a ^ "::" ^ (type2str o type_of) a ^ "'\n" ^
    2.36 +			      "actual: '" ^ term2str f ^ "::" ^ (type2str o type_of) f ^ "'\n" ^
    2.37 +			      "in\n" ^
    2.38 +			      "formals: " ^ terms2str formals ^ "\n" ^
    2.39 +			      "actuals: " ^ terms2str actuals)
    2.40 +     val env = relate_args [] formals actuals;
    2.41 +val ctxt = ProofContext.init_global thy |> declare_constraints' actuals
    2.42 +val {pre, prls, ...} = get_met metID;
    2.43 +val pres = check_preconds thy prls pre itms |> map snd;
    2.44 +val ctxt = ctxt |> insert_assumptions pres;
    2.45 +
    2.46 +"~~~~~ continue solve";
    2.47 +val ini = init_form thy sc'''' env'''';
    2.48  val p = lev_dn p;
    2.49  val SOME t = ini;
    2.50  val (pos,c,_,pt) = 
    2.51 -		  generate1 thy (Apply_Method' (mI, SOME t, is, ctxt))
    2.52 -			    (is, ctxt) (lev_on p, Frm)(*implicit Take*) pt;
    2.53 -("ok",([(Apply_Method mI, Apply_Method' (mI, SOME t, is, ctxt), 
    2.54 -		    ((lev_on p, Frm), (is, ctxt)))], c, (pt,pos)):calcstate');
    2.55 +		  generate1 thy (Apply_Method' (mI, SOME t, is'''', ctxt))
    2.56 +			    (is'''', ctxt) (lev_on p, Frm)(*implicit Take*) pt;
    2.57 +("ok",([(Apply_Method mI, Apply_Method' (mI, SOME t, is'''', ctxt), 
    2.58 +		    ((lev_on p, Frm), (is'''', ctxt)))], c, (pt,pos)):calcstate');
    2.59 +
    2.60 +val ctxt = get_ctxt pt pos;
    2.61 +val SOME known_x = parseNEW ctxt "x+z+z"; (*x has declare_constraints to real*)
    2.62 +val SOME unknown = parseNEW ctxt "a+b+c";
    2.63 +if type_of known_x = Type ("RealDef.real",[]) then ()
    2.64 +else error "x+1=2 after start root-pbl wrong type-inference for known_x";
    2.65 +if  type_of unknown = TFree ("'a", ["Groups.plus"]) then ()
    2.66 +else error "x+1=2 after start root-pbl wrong type-inference for unknown";
    2.67  
    2.68  val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*nxt = ("Rewrite_Set"*)
    2.69  case nxt of ("Rewrite_Set", _) => ()
    2.70  | _ => error "minisubpbl: Method not started in root-problem";
    2.71 -

     3.1 --- a/test/Tools/isac/Test_Isac.thy	Fri May 20 08:32:57 2011 +0200
     3.2 +++ b/test/Tools/isac/Test_Isac.thy	Fri May 20 09:12:40 2011 +0200
     3.3 @@ -171,89 +171,6 @@
     3.4  ML {*
     3.5  *}
     3.6  ML {*
     3.7 -"----------- Minisubplb/200-start-method.sml ---------------------";
     3.8 -val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
     3.9 -val (dI',pI',mI') =
    3.10 -  ("Test", ["sqroot-test","univariate","equation","test"],
    3.11 -   ["Test","squ-equ-test-subpbl1"]);
    3.12 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
    3.13 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    3.14 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    3.15 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    3.16 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    3.17 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    3.18 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    3.19 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Apply_Method"*)
    3.20 -val (pt'''', p'''') = (pt, p);
    3.21 -"~~~~~ fun me, args:"; val (_,tac) = nxt;
    3.22 -"~~~~~ fun locatetac, args:"; val ptp as (pt, p) = (pt, p);
    3.23 -val (mI,m) = mk_tac'_ tac;
    3.24 -val Appl m = applicable_in p pt m;
    3.25 -member op = specsteps mI; (*false*)
    3.26 -"~~~~~ fun loc_solve_, args:"; val (m, (pt, pos) ) = ((mI, m), ptp);
    3.27 -"~~~~~ fun solve, args:"; val (("Apply_Method", Apply_Method' (mI,_,_,_)), pos as (p,_)) = (m, pos);
    3.28 -val PblObj {meth, ctxt, ...} = get_obj I pt p;
    3.29 -val thy' = get_obj g_domID pt p;
    3.30 -val thy = assoc_thy thy';
    3.31 -val {srls, pre, prls, ...} = get_met mI;
    3.32 -val pres = check_preconds thy prls pre meth |> map snd;
    3.33 -val ctxt = ctxt |> insert_assumptions pres;
    3.34 -val (is'''' as ScrState (env'''',_,_,_,_,_), _, sc'''') = init_scrstate thy meth mI;
    3.35 -*}
    3.36 -ML {*
    3.37 -"~~~~~ fun init_scrstate, args:"; val (thy, itms, metID) = (thy, meth, mI)
    3.38 -    val actuals = itms2args thy metID itms
    3.39 -	  val scr as Script sc = (#scr o get_met) metID
    3.40 -    val formals = formal_args sc    
    3.41 -	  (*expects same sequence of (actual) args in itms and (formal) args in met*)
    3.42 -	  fun relate_args env [] [] = env
    3.43 -	    | relate_args env _ [] = 
    3.44 -	        error ("ERROR in creating the environment for '" ^
    3.45 -			    id_of_scr sc ^ "' from \nthe items of the guard of " ^
    3.46 -			    metID2str metID ^ ",\n" ^
    3.47 -			    "formal arg(s), from the script, miss actual arg(s), from the guards env:\n" ^
    3.48 -			    (string_of_int o length) formals ^
    3.49 -			    " formals: " ^ terms2str formals ^ "\n" ^
    3.50 -			    (string_of_int o length) actuals ^
    3.51 -			    " actuals: " ^ terms2str actuals)
    3.52 -	    | relate_args env [] actual_finds = env (*may drop Find!*)
    3.53 -	    | relate_args env (a::aa) (f::ff) = 
    3.54 -	        if type_of a = type_of f 
    3.55 -	        then relate_args (env @ [(a, f)]) aa ff
    3.56 -          else 
    3.57 -	          error ("ERROR in creating the environment for '" ^
    3.58 -			      id_of_scr sc ^ "' from \nthe items of the guard of " ^
    3.59 -			      metID2str metID ^ ",\n" ^
    3.60 -			      "different types of formal arg, from the script, " ^
    3.61 -			      "and actual arg, from the guards env:'\n" ^
    3.62 -			      "formal: '" ^ term2str a ^ "::" ^ (type2str o type_of) a ^ "'\n" ^
    3.63 -			      "actual: '" ^ term2str f ^ "::" ^ (type2str o type_of) f ^ "'\n" ^
    3.64 -			      "in\n" ^
    3.65 -			      "formals: " ^ terms2str formals ^ "\n" ^
    3.66 -			      "actuals: " ^ terms2str actuals)
    3.67 -     val env = relate_args [] formals actuals;
    3.68 -*}
    3.69 -ML {*
    3.70 -val ctxt = ProofContext.init_global thy;
    3.71 -declare_constraints' actuals
    3.72 -*}
    3.73 -ML {*
    3.74 -val ctxt = ProofContext.init_global thy |> declare_constraints' actuals
    3.75 -*}
    3.76 -ML {*
    3.77 -"~~~~~ continue solve";
    3.78 -val ini = init_form thy sc'''' env'''';
    3.79 -val p = lev_dn p;
    3.80 -val SOME t = ini;
    3.81 -val (pos,c,_,pt) = 
    3.82 -		  generate1 thy (Apply_Method' (mI, SOME t, is, ctxt))
    3.83 -			    (is, ctxt) (lev_on p, Frm)(*implicit Take*) pt;
    3.84 -("ok",([(Apply_Method mI, Apply_Method' (mI, SOME t, is, ctxt), 
    3.85 -		    ((lev_on p, Frm), (is, ctxt)))], c, (pt,pos)):calcstate');
    3.86 -
    3.87 -val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*nxt = ("Rewrite_Set"*)
    3.88 -case nxt of ("Rewrite_Set", _) => ()
    3.89 -| _ => error "minisubpbl: Method not started in root-problem";
    3.90  *}
    3.91  ML {*
    3.92  *}