1.1 --- a/test/Tools/isac/Frontend/interface.sml Mon Jun 20 17:33:06 2011 +0200
1.2 +++ b/test/Tools/isac/Frontend/interface.sml Thu Jun 23 10:17:04 2011 +0200
1.3 @@ -198,6 +198,7 @@
1.4 "--------- miniscript with mini-subpbl ------------------";
1.5 "--------- miniscript with mini-subpbl ------------------";
1.6 "--------- miniscript with mini-subpbl ------------------";
1.7 +"=== this sequence of fun-calls resembles fun me ===";
1.8 states:=[]; (*start of calculation, return No.1*)
1.9 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
1.10 ("Test", ["sqroot-test","univariate","equation","test"],
1.11 @@ -425,7 +426,9 @@
1.12 Iterator 1;
1.13 moveActiveRoot 1;
1.14 autoCalculate 1 CompleteCalc;
1.15 -
1.16 +(*========== inhibit exn 110620 ================================================
1.17 + val ((pt,p),_) = get_calc 1; show_pt pt;
1.18 + ERROR 110620 there is only 1 PblObj
1.19 (*
1.20 getTactic 1 ([1],Frm);
1.21 getTactic 1 ([1],Res);
1.22 @@ -440,15 +443,12 @@
1.23
1.24 val ((pt,_),_) = get_calc 1;
1.25 val p = get_pos 1 1;
1.26 -(*========== inhibit exn 110620 ================================================
1.27 val (Form f, tac, asms) = pt_extract (pt, p);
1.28 -(* ModSpec........... = ...................DIFFERENT !*)
1.29 if term2str f = "[x = 1]" andalso p = ([], Res) then () else
1.30 error "FE-interface.sml: diff.behav. in mini-subpbl AUTOCALCULATE 6";
1.31 ============ inhibit exn 110620 ==============================================*)
1.32
1.33
1.34 -(*=== inhibit exn ?=============================================================
1.35 "--------- mini-subpbl AUTO CompleteCalcHead ------------";
1.36 "--------- mini-subpbl AUTO CompleteCalcHead ------------";
1.37 "--------- mini-subpbl AUTO CompleteCalcHead ------------";
1.38 @@ -458,9 +458,16 @@
1.39 ["Test","squ-equ-test-subpbl1"]))];
1.40 Iterator 1;
1.41 moveActiveRoot 1;
1.42 -(* doesn't terminate !!!
1.43 - autoCalculate 1 CompleteCalcHead;
1.44 -*)
1.45 + autoCalculate 1 CompleteCalcHead;
1.46 +
1.47 +val ((Nd (PblObj {env = NONE, fmz = (fm, ("Test", pblID, metID)), loc = (SOME (env, ctxt1), NONE),
1.48 + cell = NONE, ctxt = ctxt2, meth,
1.49 + spec = ("Test", ["sqroot-test", "univariate", "equation", "test"],
1.50 + ["Test", "squ-equ-test-subpbl1"]),
1.51 + probl, branch = TransitiveB, origin, ostate = Incomplete, result}, []),
1.52 + ([], Met)), []) = get_calc 1;
1.53 +if length meth = 3 andalso length probl = 3 (*just some items tested*) then ()
1.54 +else error "--- mini-subpbl AUTO CompleteCalcHead ---";
1.55
1.56 "--------- solve_linear as rootpbl AUTO CompleteModel ---";
1.57 "--------- solve_linear as rootpbl AUTO CompleteModel ---";
1.58 @@ -473,8 +480,11 @@
1.59 ["Test","solve_linear"]))];
1.60 Iterator 1;
1.61 moveActiveRoot 1;
1.62 - autoCalculate 1 CompleteModel;
1.63 + autoCalculate 1 CompleteModel;
1.64 +(*========== inhibit exn 110622 ================================================
1.65 refFormula 1 (get_pos 1 1);
1.66 + <ERROR> error in kernel </ERROR>
1.67 + get_pos: calc 1 not existent
1.68
1.69 setProblem 1 ["linear","univariate","equation","test"];
1.70 val pos = get_pos 1 1;
1.71 @@ -502,6 +512,7 @@
1.72 val (Form f, tac, asms) = pt_extract (pt, p);
1.73 if term2str f = "[x = 1]" andalso p = ([], Res) then () else
1.74 error "FE-interface.sml: diff.behav. in mini-subpbl AUTOCALCULATE 6";
1.75 +============ inhibit exn 110622 ==============================================*)
1.76
1.77
1.78 "--------- setContext..Thy ------------------------------";
1.79 @@ -514,23 +525,31 @@
1.80 Iterator 1; moveActiveRoot 1;
1.81 autoCalculate 1 CompleteCalcHead;
1.82 autoCalculate 1 (Step 1);
1.83 -val ((pt,p),_) = get_calc 1; show_pt pt;
1.84 +val ((pt,p),_) = get_calc 1; show_pt pt; (*2 lines, OK*)
1.85 (*
1.86 -setNextTactic 1 (Rewrite_Set "Test_simplify");
1.87 +setNextTactic 1 (Rewrite_Set "Test_simplify"); (*--> "thy_isac_Test-rls-Test_simplify"*)
1.88 autoCalculate 1 (Step 1);
1.89 val ((pt,p),_) = get_calc 1; show_pt pt;
1.90 *)
1.91 "-----^^^^^ and vvvvv do the same -----";
1.92 setContext 1 p "thy_isac_Test-rls-Test_simplify";
1.93 -val ((pt,p),_) = get_calc 1; show_pt pt;
1.94 +val ((pt,p),_) = get_calc 1; show_pt pt; (*2 lines, OK*)
1.95
1.96 autoCalculate 1 (Step 1);
1.97 setContext 1 p "thy_isac_Test-rls-Test_simplify";
1.98 -val ((pt,p),_) = get_calc 1; show_pt pt;
1.99 +val ((pt,p),_) = get_calc 1; show_pt pt; (*3 lines, OK*)
1.100 +if p = ([1], Res) andalso term2str (get_obj g_res pt (fst p)) = "x + 1 + -1 * 2 = 0"
1.101 +then () else error "--- setContext..Thy --- autoCalculate 1 (Step 1) #1"
1.102
1.103 autoCalculate 1 CompleteCalc;
1.104 -
1.105 -
1.106 +val ((pt,p),_) = get_calc 1; show_pt pt;
1.107 +val (((pt,_),_), p) = (get_calc 1, get_pos 1 1);
1.108 +(*========== inhibit exn 110622 ================================================
1.109 + ERROR still 3 lines
1.110 +val (Form f, tac, asms) = pt_extract (pt, p);
1.111 +if term2str f = "[x = 1]" andalso p = ([], Res) then () else
1.112 +error "--- setContext..Thy --- autoCalculate CompleteCalc";
1.113 +============ inhibit exn 110622 ==============================================*)
1.114
1.115 "--------- mini-subpbl AUTOCALC CompleteToSubpbl --------";
1.116 "--------- mini-subpbl AUTOCALC CompleteToSubpbl --------";
1.117 @@ -557,14 +576,17 @@
1.118 autoCalculate 1 CompleteCalc; (*das geht ohnehin !*);
1.119 val ((pt,_),_) = get_calc 1;
1.120 val p = get_pos 1 1;
1.121 +(*========== inhibit exn 110622 ================================================
1.122 val (Form f, tac, asms) = pt_extract (pt, p);
1.123 if term2str f = "[x = 1]" andalso p = ([], Res) then () else
1.124 error "FE-interface.sml: diff.behav. in mini-subpbl CompleteToSubpbl 1";
1.125 +============ inhibit exn 110622 ==============================================*)
1.126
1.127
1.128 "--------- rat-eq + subpbl: no_met, NO solution dropped -";
1.129 "--------- rat-eq + subpbl: no_met, NO solution dropped -";
1.130 "--------- rat-eq + subpbl: no_met, NO solution dropped -";
1.131 +(*========== inhibit exn 110622 ================================================
1.132 states:=[];
1.133 CalcTree
1.134 [(["equality ((5*x)/(x - 2) - x/(x+2)=4)", "solveFor x","solutions L"],
1.135 @@ -645,7 +667,6 @@
1.136 autoCalculate 1 (Step 1); fetchProposedTactic 1; (*<ERROR> helpless </ERROR> !!!*)
1.137 setNextTactic 1 (Refine_Problem ["univariate","equation"]);
1.138
1.139 -
1.140 (*------------------------------------------------------------------*)
1.141 autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.142 setNextTactic 1 (Specify_Method ["PolyEq","solve_d1_polyeq_equation"]);
1.143 @@ -667,7 +688,7 @@
1.144 setNextTactic 1 (Check_Postcond ["normalize","polynomial",
1.145 "univariate","equation"]);
1.146 autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.147 -(*========== inhibit exn =======================================================
1.148 +(*========== inhibit exn 2009 ==================================================
1.149 *** exception TYPE raised (line 460 of "old_goals.ML"):
1.150 *** Type error in application: Incompatible operand type
1.151 ***
1.152 @@ -686,7 +707,8 @@
1.153 val (Form t,_,_) = pt_extract ptp;
1.154 if get_pos 1 1 = ([], Res) andalso term2str t = "[x = -4 / 3]" then ()
1.155 else writeln "FE-inteface.sml: diff.behav. in rat-eq + subpbl: no_met, NO ..";
1.156 -============ inhibit exn =====================================================*)
1.157 +============ inhibit exn 2009 ================================================*)
1.158 +============ inhibit exn 110622 ==============================================*)
1.159
1.160
1.161 "--------- tryMatchProblem, tryRefineProblem ------------";
1.162 @@ -769,6 +791,8 @@
1.163
1.164 fetchProposedTactic 1;
1.165 setNextTactic 1 (Apply_Method ["PolyEq","normalize_poly"]);
1.166 +(*========== inhibit exn 110622 ================================================
1.167 + vvvvvvvvvvvv
1.168 autoCalculate 1 CompleteCalc;
1.169 val ((pt,_),_) = get_calc 1;
1.170 show_pt pt;
1.171 @@ -799,6 +823,7 @@
1.172 val (Form f, tac, asms) = pt_extract (pt, p);
1.173 if term2str f = "[x = -1, x = -3]" andalso p = ([], Res) then () else
1.174 error "FE-interface.sml: diff.behav. in tryMatchProblem, tryRefine";
1.175 +============ inhibit exn 110622 ==============================================*)
1.176
1.177
1.178 "--------- modifyCalcHead, resetCalcHead, modelProblem --";
1.179 @@ -820,9 +845,49 @@
1.180 ("Test",
1.181 ["sqroot-test","univariate","equation","test"],
1.182 ["Test","squ-equ-test-subpbl1"]));
1.183 +
1.184 +val ((Nd (PblObj {env = NONE,
1.185 + fmz = (fm, tpm),
1.186 + loc = (SOME scrst_ctxt, NONE),
1.187 + ctxt,
1.188 + cell = NONE,
1.189 + meth,
1.190 + spec = (thy,
1.191 + ["sqroot-test", "univariate", "equation", "test"],
1.192 + ["Test", "squ-equ-test-subpbl1"]),
1.193 + probl,
1.194 + branch = TransitiveB,
1.195 + origin,
1.196 + ostate = Incomplete,
1.197 + result},
1.198 + []),
1.199 + ([], Pbl)),
1.200 + []) = get_calc 1;
1.201 +(*WN110622: is the same as in 2002, but shouldn't be probl = [3 items?]*)
1.202 +if length meth = 0 andalso length probl = 0 (*just some items tested*) then ()
1.203 +else error "--- mini-subpbl AUTO CompleteCalcHead ---";
1.204 +
1.205 resetCalcHead 1;
1.206 modelProblem 1;
1.207
1.208 +get_calc 1;
1.209 +val ((Nd (PblObj {env = NONE,
1.210 + fmz = (fm, tpm),
1.211 + loc = (SOME scrst_ctxt, NONE),
1.212 + ctxt,
1.213 + cell = NONE,
1.214 + meth,
1.215 + spec = ("e_domID", ["e_pblID"], ["e_metID"]),
1.216 + probl,
1.217 + branch = TransitiveB,
1.218 + origin,
1.219 + ostate = Incomplete,
1.220 + result},
1.221 + []),
1.222 + ([], Pbl)),
1.223 + []) = get_calc 1;
1.224 +if length meth = 0 andalso length probl = 0 (*just some items tested*) then ()
1.225 +else error "--- mini-subpbl AUTO CompleteCalcHead ---";
1.226
1.227 "--------- maximum-example, UC: Modeling an example -----";
1.228 "--------- maximum-example, UC: Modeling an example -----";
1.229 @@ -914,6 +979,7 @@
1.230 DEconstrCalcTree 1;
1.231
1.232
1.233 +(*=== inhibit exn ?=============================================================
1.234 "--------- solve_linear from pbl-hierarchy --------------";
1.235 "--------- solve_linear from pbl-hierarchy --------------";
1.236 "--------- solve_linear from pbl-hierarchy --------------";
1.237 @@ -999,7 +1065,7 @@
1.238 ["Test","squ-equ-test-subpbl1"]))];
1.239 Iterator 1; moveActiveRoot 1;
1.240 autoCalculate 1 CompleteCalc;
1.241 - val ((pt,_),_) = get_calc 1;
1.242 + val ((pt,_),_) PblObj;
1.243 show_pt pt;
1.244
1.245 (*UC\label{SOLVE:HIDE:getTactic}*)
2.1 --- a/test/Tools/isac/Test_Isac.thy Mon Jun 20 17:33:06 2011 +0200
2.2 +++ b/test/Tools/isac/Test_Isac.thy Thu Jun 23 10:17:04 2011 +0200
2.3 @@ -141,19 +141,104 @@
2.4 use "Frontend/states.sml" (*new 2011*)
2.5 use "Frontend/interface.sml" (*part.*)
2.6 ML {*
2.7 +*}
2.8 +ML {*
2.9 +"--------- maximum-example, UC: Modeling an example -----";
2.10 +(* {\bf\UC{Editing the Model}\label{SPECIFY:enter}\label{SPECIFY:check}\\}
2.11 +see isac.bridge.TestModel#testEditItems
2.12 +*)
2.13 + val elems = ["fixedValues [r=Arbfix]","maximum A","valuesFor [a,b]",
2.14 + "relations [A=a*b, (a/2)^2 + (b/2)^2 = r^2]",
2.15 + "relations [A=a*b, (a/2)^2 + (b/2)^2 = r^2]",
2.16 + "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]",
2.17 + (*^^^ these are the elements for the root-problem (in variants)*)
2.18 + (*vvv these are elements required for subproblems*)
2.19 + "boundVariable a","boundVariable b","boundVariable alpha",
2.20 + "interval {x::real. 0 <= x & x <= 2*r}",
2.21 + "interval {x::real. 0 <= x & x <= 2*r}",
2.22 + "interval {x::real. 0 <= x & x <= pi}",
2.23 + "errorBound (eps=(0::real))"]
2.24 + (*specifying is not interesting for this example*)
2.25 + val spec = ("DiffApp", ["maximum_of","function"],
2.26 + ["DiffApp","max_by_calculus"]);
2.27 + (*the empty model with descriptions for user-guidance by Model_Problem*)
2.28 + val empty_model = [Given ["fixedValues []"],
2.29 + Find ["maximum", "valuesFor"],
2.30 + Relate ["relations []"]];
2.31 + states:=[];
2.32 + DEconstrCalcTree 1;
2.33 + CalcTree [(elems, spec)];
2.34 + Iterator 1;
2.35 + moveActiveRoot 1;
2.36 + refFormula 1 (get_pos 1 1);
2.37 + (*this gives a completely empty model*)
2.38 +
2.39 + fetchProposedTactic 1;
2.40 +(*fill the CalcHead with Descriptions...*)
2.41 + setNextTactic 1 (Model_Problem );
2.42 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.43 +
2.44 + (*user input is !!!!!EITHER!!!!! _some_ (at least one) items of the model
2.45 + !!!!!OR!!!!! _one_ part of the specification !!!!!!!!!!!!!*)
2.46 + (*input of two items, 'fixedValues [r=Arbfix]' and 'maximum b'...*)
2.47 + modifyCalcHead 1 (([],Pbl) (*position, from previous refFormula*),
2.48 + "Problem (DiffApp.thy, [maximum_of, function])",
2.49 + (*the head-form ^^^ is not used for input here*)
2.50 + [Given ["fixedValues [r=Arbfix]"(*new input*)],
2.51 + Find ["maximum b"(*new input*), "valuesFor"],
2.52 + Relate ["relations"]],
2.53 + (*input (Arbfix will dissappear soon)*)
2.54 + Pbl (*belongsto*),
2.55 + e_spec (*no input to the specification*));
2.56 +
2.57 + (*the user does not know, what 'superfluous' for 'maximum b' may mean
2.58 + and asks what to do next*)
2.59 + fetchProposedTactic 1;
2.60 + (*the student follows the advice*)
2.61 + setNextTactic 1 (Add_Find "maximum A"); (*FIXME.17.11.03: does not yet work*)
2.62 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.63 +
2.64 + (*this input completes the model*)
2.65 + modifyCalcHead 1 (([],Pbl), "not used here",
2.66 + [Given ["fixedValues [r=Arbfix]"],
2.67 + Find ["maximum A", "valuesFor [a,b]"(*new input*)],
2.68 + Relate ["relations [A=a*b, \
2.69 + \(a/2)^2 + (b/2)^2 = r^2]"]], Pbl, e_spec);
2.70 +
2.71 + (*specification is not interesting an should be skipped by the dialogguide;
2.72 + !!!!!!!!!!!!!!!!!!!! input of ONE part at a time !!!!!!!!!!!!!!!!!!!!!!*)
2.73 + modifyCalcHead 1 (([],Pbl), "not used here",
2.74 + [Given ["fixedValues [r=Arbfix]"],
2.75 + Find ["maximum A", "valuesFor [a,b]"(*new input*)],
2.76 + Relate ["relations [A=a*b, \
2.77 + \(a/2)^2 + (b/2)^2 = r^2]"]], Pbl,
2.78 + ("DiffApp", ["e_pblID"], ["e_metID"]));
2.79 + modifyCalcHead 1 (([],Pbl), "not used here",
2.80 + [Given ["fixedValues [r=Arbfix]"],
2.81 + Find ["maximum A", "valuesFor [a,b]"(*new input*)],
2.82 + Relate ["relations [A=a*b, \
2.83 + \(a/2)^2 + (b/2)^2 = r^2]"]], Pbl,
2.84 + ("DiffApp", ["maximum_of","function"],
2.85 + ["e_metID"]));
2.86 + modifyCalcHead 1 (([],Pbl), "not used here",
2.87 + [Given ["fixedValues [r=Arbfix]"],
2.88 + Find ["maximum A", "valuesFor [a,b]"(*new input*)],
2.89 + Relate ["relations [A=a*b, \
2.90 + \(a/2)^2 + (b/2)^2 = r^2]"]], Pbl,
2.91 + ("DiffApp", ["maximum_of","function"],
2.92 + ["DiffApp","max_by_calculus"]));
2.93 + (*this final calcHead now has STATUS 'complete' !*)
2.94 + DEconstrCalcTree 1;
2.95
2.96 *}
2.97 ML {*
2.98 -
2.99 *}
2.100 ML {*
2.101 -
2.102 *}
2.103 ML {*
2.104 -
2.105 *}
2.106 ML {*
2.107 -
2.108 +print_depth 99;
2.109 *}
2.110
2.111 use "print_exn_G.sml" (*new 2011*)
2.112 @@ -219,12 +304,8 @@
2.113 (*=== inhibit exn ?=============================================================
2.114 ===== inhibit exn ?===========================================================*)
2.115
2.116 -(*========== inhibit exn 110620 ================================================
2.117 -
2.118 -"########### testcode inserted vvv ###########################################";
2.119 -"########### testcode inserted ^^^ ###########################################";
2.120 -
2.121 -============ inhibit exn 110620 ==============================================*)
2.122 +(*========== inhibit exn 110622 ================================================
2.123 +============ inhibit exn 110622 ==============================================*)
2.124
2.125 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
2.126 -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)