1.1 --- a/test/Tools/isac/Test_Isac.thy Fri May 20 07:24:18 2011 +0200
1.2 +++ b/test/Tools/isac/Test_Isac.thy Fri May 20 08:12:51 2011 +0200
1.3 @@ -166,6 +166,102 @@
1.4
1.5 ML {*
1.6 *}
1.7 +ML {*
1.8 +"----------- Minisubplb/100-init-rootpbl.sml ---------------------";
1.9 +val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
1.10 +val (dI',pI',mI') =
1.11 + ("Test", ["sqroot-test","univariate","equation","test"],
1.12 + ["Test","squ-equ-test-subpbl1"]);
1.13 +*}
1.14 +ML {*
1.15 +*}
1.16 +ML {*
1.17 +"----------- Minisubplb/200-start-method.sml ---------------------";
1.18 +val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
1.19 +val (dI',pI',mI') =
1.20 + ("Test", ["sqroot-test","univariate","equation","test"],
1.21 + ["Test","squ-equ-test-subpbl1"]);
1.22 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.23 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.24 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.25 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.26 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.27 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.28 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.29 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Apply_Method"*)
1.30 +val (pt'''', p'''') = (pt, p);
1.31 +"~~~~~ fun me, args:"; val (_,tac) = nxt;
1.32 +"~~~~~ fun locatetac, args:"; val ptp as (pt, p) = (pt, p);
1.33 +val (mI,m) = mk_tac'_ tac;
1.34 +val Appl m = applicable_in p pt m;
1.35 +member op = specsteps mI; (*false*)
1.36 +"~~~~~ fun loc_solve_, args:"; val (m, (pt, pos) ) = ((mI, m), ptp);
1.37 +"~~~~~ fun solve, args:"; val (("Apply_Method", Apply_Method' (mI,_,_,_)), pos as (p,_)) = (m, pos);
1.38 +val PblObj {meth, ctxt, ...} = get_obj I pt p;
1.39 +val thy' = get_obj g_domID pt p;
1.40 +val thy = assoc_thy thy';
1.41 +val {srls, pre, prls, ...} = get_met mI;
1.42 +val pres = check_preconds thy prls pre meth |> map snd;
1.43 +val ctxt = ctxt |> insert_assumptions pres;
1.44 +val (is'''' as ScrState (env'''',_,_,_,_,_), _, sc'''') = init_scrstate thy meth mI;
1.45 +*}
1.46 +ML {*
1.47 +"~~~~~ fun init_scrstate, args:"; val (thy, itms, metID) = (thy, meth, mI)
1.48 + val actuals = itms2args thy metID itms
1.49 + val scr as Script sc = (#scr o get_met) metID
1.50 + val formals = formal_args sc
1.51 + (*expects same sequence of (actual) args in itms and (formal) args in met*)
1.52 + fun relate_args env [] [] = env
1.53 + | relate_args env _ [] =
1.54 + error ("ERROR in creating the environment for '" ^
1.55 + id_of_scr sc ^ "' from \nthe items of the guard of " ^
1.56 + metID2str metID ^ ",\n" ^
1.57 + "formal arg(s), from the script, miss actual arg(s), from the guards env:\n" ^
1.58 + (string_of_int o length) formals ^
1.59 + " formals: " ^ terms2str formals ^ "\n" ^
1.60 + (string_of_int o length) actuals ^
1.61 + " actuals: " ^ terms2str actuals)
1.62 + | relate_args env [] actual_finds = env (*may drop Find!*)
1.63 + | relate_args env (a::aa) (f::ff) =
1.64 + if type_of a = type_of f
1.65 + then relate_args (env @ [(a, f)]) aa ff
1.66 + else
1.67 + error ("ERROR in creating the environment for '" ^
1.68 + id_of_scr sc ^ "' from \nthe items of the guard of " ^
1.69 + metID2str metID ^ ",\n" ^
1.70 + "different types of formal arg, from the script, " ^
1.71 + "and actual arg, from the guards env:'\n" ^
1.72 + "formal: '" ^ term2str a ^ "::" ^ (type2str o type_of) a ^ "'\n" ^
1.73 + "actual: '" ^ term2str f ^ "::" ^ (type2str o type_of) f ^ "'\n" ^
1.74 + "in\n" ^
1.75 + "formals: " ^ terms2str formals ^ "\n" ^
1.76 + "actuals: " ^ terms2str actuals)
1.77 + val env = relate_args [] formals actuals;
1.78 +*}
1.79 +ML {*
1.80 +val ctxt = ProofContext.init_global thy;
1.81 +declare_constraints' actuals
1.82 +*}
1.83 +ML {*
1.84 +val ctxt = ProofContext.init_global thy |> declare_constraints' actuals
1.85 +*}
1.86 +ML {*
1.87 +"~~~~~ continue solve";
1.88 +val ini = init_form thy sc'''' env'''';
1.89 +val p = lev_dn p;
1.90 +val SOME t = ini;
1.91 +val (pos,c,_,pt) =
1.92 + generate1 thy (Apply_Method' (mI, SOME t, is, ctxt))
1.93 + (is, ctxt) (lev_on p, Frm)(*implicit Take*) pt;
1.94 +("ok",([(Apply_Method mI, Apply_Method' (mI, SOME t, is, ctxt),
1.95 + ((lev_on p, Frm), (is, ctxt)))], c, (pt,pos)):calcstate');
1.96 +
1.97 +val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*nxt = ("Rewrite_Set"*)
1.98 +case nxt of ("Rewrite_Set", _) => ()
1.99 +| _ => error "minisubpbl: Method not started in root-problem";
1.100 +*}
1.101 +ML {*
1.102 +*}
1.103
1.104 ML {*
1.105 (*############################################################################*)