1.1 --- a/src/Tools/isac/Interpret/calchead.sml Fri May 20 07:24:18 2011 +0200
1.2 +++ b/src/Tools/isac/Interpret/calchead.sml Fri May 20 08:12:51 2011 +0200
1.3 @@ -1534,7 +1534,7 @@
1.4 (hd o #met o get_pbt) pI') end
1.5 else (pI, get_pbt pI |> #ppc |> prep_ori fmz thy, mI)
1.6 val {cas, ppc, thy=thy',...} = get_pbt pI (*take dI from _refined_ pbl*)
1.7 - val dI = theory2theory' (maxthy thy thy');
1.8 + val dI = theory2theory' (maxthy thy thy')
1.9 val hdl =
1.10 case cas of
1.11 NONE => pblterm dI pI
2.1 --- a/src/Tools/isac/Interpret/mathengine.sml Fri May 20 07:24:18 2011 +0200
2.2 +++ b/src/Tools/isac/Interpret/mathengine.sml Fri May 20 08:12:51 2011 +0200
2.3 @@ -377,13 +377,11 @@
2.4 (*.create a calc-tree; for use within sml: thus ^^^ NOT decoded to ^;
2.5 compare "fun CalcTree" which DOES decode.*)
2.6 fun CalcTreeTEST [(fmz, sp):fmz] =
2.7 -(* val [(fmz, sp):fmz] = [(fmz, (dI',pI',mI'))];
2.8 - val [(fmz, sp):fmz] = [([], ("e_domID", ["e_pblID"], ["e_metID"]))];
2.9 - *)
2.10 - let val cs as ((pt,p), tacis) = nxt_specify_init_calc (fmz, sp)
2.11 - val tac = case tacis of [] => Empty_Tac | _ => (#1 o hd) tacis
2.12 - val f = TESTg_form (pt,p)
2.13 - in (p, []:NEW, f, (tac2IDstr tac, tac), Sundef, pt) end;
2.14 + let
2.15 + val cs as ((pt,p), tacis) = nxt_specify_init_calc (fmz, sp)
2.16 + val tac = case tacis of [] => Empty_Tac | _ => (#1 o hd) tacis
2.17 + val f = TESTg_form (pt,p)
2.18 + in (p, []:NEW, f, (tac2IDstr tac, tac), Sundef, pt) end;
2.19
2.20 (*for tests > 15.8.03 after separation setnexttactic / nextTac:
2.21 external view: me should be used by math-authors as done so far
3.1 --- a/src/Tools/isac/Interpret/script.sml Fri May 20 07:24:18 2011 +0200
3.2 +++ b/src/Tools/isac/Interpret/script.sml Fri May 20 08:12:51 2011 +0200
3.3 @@ -1555,11 +1555,11 @@
3.4
3.5
3.6 (*.create the initial interpreter state from the items of the guard.*)
3.7 -fun init_scrstate thy itms metID =(*FIXME.WN170511: delete ctxt from value*)
3.8 +fun init_scrstate thy itms metID =
3.9 let
3.10 - val actuals = itms2args thy metID itms;
3.11 - val scr as Script sc = (#scr o get_met) metID;
3.12 - val formals = formal_args sc
3.13 + val actuals = itms2args thy metID itms
3.14 + val scr as Script sc = (#scr o get_met) metID
3.15 + val formals = formal_args sc
3.16 (*expects same sequence of (actual) args in itms and (formal) args in met*)
3.17 fun relate_args env [] [] = env
3.18 | relate_args env _ [] =
3.19 @@ -1587,7 +1587,8 @@
3.20 "formals: " ^ terms2str formals ^ "\n" ^
3.21 "actuals: " ^ terms2str actuals)
3.22 val env = relate_args [] formals actuals;
3.23 - in (ScrState (env,[],NONE,e_term,Safe,true), (*FIXME.WN170511 remove*)e_ctxt, scr):istate * Proof.context * scr end;
3.24 + val ctxt = ProofContext.init_global thy |> declare_constraints' actuals
3.25 + in (ScrState (env,[],NONE,e_term,Safe,true), ctxt, scr):istate * Proof.context * scr end;
3.26
3.27 (* decide, where to get script/istate from:
3.28 (*1*) from PblObj.env: at begin of script if no init_form
4.1 --- a/test/Tools/isac/Minisubpbl/100-init-rootpbl.sml Fri May 20 07:24:18 2011 +0200
4.2 +++ b/test/Tools/isac/Minisubpbl/100-init-rootpbl.sml Fri May 20 08:12:51 2011 +0200
4.3 @@ -3,10 +3,29 @@
4.4 (c) copyright due to lincense terms.
4.5 *)
4.6
4.7 +"----------- Minisubplb/100-init-rootpbl.sml ---------------------";
4.8 +"----------- Minisubplb/100-init-rootpbl.sml ---------------------";
4.9 +"----------- Minisubplb/100-init-rootpbl.sml ---------------------";
4.10 val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
4.11 val (dI',pI',mI') =
4.12 ("Test", ["sqroot-test","univariate","equation","test"],
4.13 ["Test","squ-equ-test-subpbl1"]);
4.14 +*}
4.15 +ML {*
4.16 +"~~~~~ fun CalcTreeTEST, args:"; val [(fmz, sp):fmz] = [(fmz, (dI',pI',mI'))];
4.17 +"~~~~~ fun nxt_specify_init_calc, args:"; val (fmz : fmz_, (dI, pI, mI) : spec) = (fmz, sp);
4.18 +val thy = assoc_thy dI
4.19 +;mI = ["no_met"]; (*false*)
4.20 +val (pI, (pors, pctxt), mI) = (pI, get_pbt pI |> #ppc |> prep_ori fmz thy, mI)
4.21 +val {cas, ppc, thy=thy',...} = get_pbt pI
4.22 +val dI = theory2theory' (maxthy thy thy');
4.23 +val hdl =
4.24 + case cas of SOME t => subst_atomic ((vars_of_pbl_' ppc) ~~~ vals_of_oris pors) t;
4.25 +val (pt, _) = cappend_problem e_ptree [] (e_istate, pctxt) (fmz, (dI, pI, mI))
4.26 + (pors, (dI, pI, mI), hdl)
4.27 +val pt = update_ctxt pt [] pctxt
4.28 +;((pt, ([], Pbl)), fst3 (nxt_specif Model_Problem (pt, ([], Pbl)))) : calcstate;
4.29 +
4.30 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
4.31 case nxt of ("Model_Problem", _) => ()
4.32 | _ => error "minisubpbl: CalcTreeTEST has no nxt = Model_Problem";
5.1 --- a/test/Tools/isac/Minisubpbl/200-start-method.sml Fri May 20 07:24:18 2011 +0200
5.2 +++ b/test/Tools/isac/Minisubpbl/200-start-method.sml Fri May 20 08:12:51 2011 +0200
5.3 @@ -3,6 +3,9 @@
5.4 (c) copyright due to lincense terms.
5.5 *)
5.6
5.7 +"----------- Minisubplb/200-start-method.sml ---------------------";
5.8 +"----------- Minisubplb/200-start-method.sml ---------------------";
5.9 +"----------- Minisubplb/200-start-method.sml ---------------------";
5.10 val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
5.11 val (dI',pI',mI') =
5.12 ("Test", ["sqroot-test","univariate","equation","test"],
6.1 --- a/test/Tools/isac/Minisubpbl/300-init-subpbl.sml Fri May 20 07:24:18 2011 +0200
6.2 +++ b/test/Tools/isac/Minisubpbl/300-init-subpbl.sml Fri May 20 08:12:51 2011 +0200
6.3 @@ -3,6 +3,9 @@
6.4 (c) copyright due to lincense terms.
6.5 *)
6.6
6.7 +"----------- Minisubplb/300-init-subpbl.sml ----------------------";
6.8 +"----------- Minisubplb/300-init-subpbl.sml ----------------------";
6.9 +"----------- Minisubplb/300-init-subpbl.sml ----------------------";
6.10 val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
6.11 val (dI',pI',mI') =
6.12 ("Test", ["sqroot-test","univariate","equation","test"],
7.1 --- a/test/Tools/isac/Test_Isac.thy Fri May 20 07:24:18 2011 +0200
7.2 +++ b/test/Tools/isac/Test_Isac.thy Fri May 20 08:12:51 2011 +0200
7.3 @@ -166,6 +166,102 @@
7.4
7.5 ML {*
7.6 *}
7.7 +ML {*
7.8 +"----------- Minisubplb/100-init-rootpbl.sml ---------------------";
7.9 +val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
7.10 +val (dI',pI',mI') =
7.11 + ("Test", ["sqroot-test","univariate","equation","test"],
7.12 + ["Test","squ-equ-test-subpbl1"]);
7.13 +*}
7.14 +ML {*
7.15 +*}
7.16 +ML {*
7.17 +"----------- Minisubplb/200-start-method.sml ---------------------";
7.18 +val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
7.19 +val (dI',pI',mI') =
7.20 + ("Test", ["sqroot-test","univariate","equation","test"],
7.21 + ["Test","squ-equ-test-subpbl1"]);
7.22 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
7.23 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.24 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.25 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.26 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.27 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.28 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.29 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Apply_Method"*)
7.30 +val (pt'''', p'''') = (pt, p);
7.31 +"~~~~~ fun me, args:"; val (_,tac) = nxt;
7.32 +"~~~~~ fun locatetac, args:"; val ptp as (pt, p) = (pt, p);
7.33 +val (mI,m) = mk_tac'_ tac;
7.34 +val Appl m = applicable_in p pt m;
7.35 +member op = specsteps mI; (*false*)
7.36 +"~~~~~ fun loc_solve_, args:"; val (m, (pt, pos) ) = ((mI, m), ptp);
7.37 +"~~~~~ fun solve, args:"; val (("Apply_Method", Apply_Method' (mI,_,_,_)), pos as (p,_)) = (m, pos);
7.38 +val PblObj {meth, ctxt, ...} = get_obj I pt p;
7.39 +val thy' = get_obj g_domID pt p;
7.40 +val thy = assoc_thy thy';
7.41 +val {srls, pre, prls, ...} = get_met mI;
7.42 +val pres = check_preconds thy prls pre meth |> map snd;
7.43 +val ctxt = ctxt |> insert_assumptions pres;
7.44 +val (is'''' as ScrState (env'''',_,_,_,_,_), _, sc'''') = init_scrstate thy meth mI;
7.45 +*}
7.46 +ML {*
7.47 +"~~~~~ fun init_scrstate, args:"; val (thy, itms, metID) = (thy, meth, mI)
7.48 + val actuals = itms2args thy metID itms
7.49 + val scr as Script sc = (#scr o get_met) metID
7.50 + val formals = formal_args sc
7.51 + (*expects same sequence of (actual) args in itms and (formal) args in met*)
7.52 + fun relate_args env [] [] = env
7.53 + | relate_args env _ [] =
7.54 + error ("ERROR in creating the environment for '" ^
7.55 + id_of_scr sc ^ "' from \nthe items of the guard of " ^
7.56 + metID2str metID ^ ",\n" ^
7.57 + "formal arg(s), from the script, miss actual arg(s), from the guards env:\n" ^
7.58 + (string_of_int o length) formals ^
7.59 + " formals: " ^ terms2str formals ^ "\n" ^
7.60 + (string_of_int o length) actuals ^
7.61 + " actuals: " ^ terms2str actuals)
7.62 + | relate_args env [] actual_finds = env (*may drop Find!*)
7.63 + | relate_args env (a::aa) (f::ff) =
7.64 + if type_of a = type_of f
7.65 + then relate_args (env @ [(a, f)]) aa ff
7.66 + else
7.67 + error ("ERROR in creating the environment for '" ^
7.68 + id_of_scr sc ^ "' from \nthe items of the guard of " ^
7.69 + metID2str metID ^ ",\n" ^
7.70 + "different types of formal arg, from the script, " ^
7.71 + "and actual arg, from the guards env:'\n" ^
7.72 + "formal: '" ^ term2str a ^ "::" ^ (type2str o type_of) a ^ "'\n" ^
7.73 + "actual: '" ^ term2str f ^ "::" ^ (type2str o type_of) f ^ "'\n" ^
7.74 + "in\n" ^
7.75 + "formals: " ^ terms2str formals ^ "\n" ^
7.76 + "actuals: " ^ terms2str actuals)
7.77 + val env = relate_args [] formals actuals;
7.78 +*}
7.79 +ML {*
7.80 +val ctxt = ProofContext.init_global thy;
7.81 +declare_constraints' actuals
7.82 +*}
7.83 +ML {*
7.84 +val ctxt = ProofContext.init_global thy |> declare_constraints' actuals
7.85 +*}
7.86 +ML {*
7.87 +"~~~~~ continue solve";
7.88 +val ini = init_form thy sc'''' env'''';
7.89 +val p = lev_dn p;
7.90 +val SOME t = ini;
7.91 +val (pos,c,_,pt) =
7.92 + generate1 thy (Apply_Method' (mI, SOME t, is, ctxt))
7.93 + (is, ctxt) (lev_on p, Frm)(*implicit Take*) pt;
7.94 +("ok",([(Apply_Method mI, Apply_Method' (mI, SOME t, is, ctxt),
7.95 + ((lev_on p, Frm), (is, ctxt)))], c, (pt,pos)):calcstate');
7.96 +
7.97 +val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*nxt = ("Rewrite_Set"*)
7.98 +case nxt of ("Rewrite_Set", _) => ()
7.99 +| _ => error "minisubpbl: Method not started in root-problem";
7.100 +*}
7.101 +ML {*
7.102 +*}
7.103
7.104 ML {*
7.105 (*############################################################################*)