1.1 --- a/test/Tools/isac/Frontend/interface.sml Tue Sep 17 18:00:59 2013 +0200
1.2 +++ b/test/Tools/isac/Frontend/interface.sml Tue Sep 17 18:59:56 2013 +0200
1.3 @@ -1,1508 +1,18 @@
1.4 -(* Title: tests the interface of isac's SML-kernel in accordance to
1.5 - java-tests/isac.bridge.
1.6 - Author: Walther Neuper
1.7 - (c) copyright due to lincense terms.
1.8 -
1.9 -WN050707 ... if true, the test ist marked with a \label referring
1.10 -to the same UC in isac-docu.tex as the JUnit testcase.
1.11 -WN120210?not ME: added some labels, which are not among the above,
1.12 -repaired lost \label (s).
1.13 +(* Title: tests for the interface
1.14 + Author: Mathias Lehnfeld 2013
1.15 + Use is subject to license terms.
1.16 *)
1.17
1.18 -"--------------------------------------------------------";
1.19 -"table of contents --------------------------------------";
1.20 -"--------------------------------------------------------";
1.21 -"within struct ------------------------------------------";
1.22 -"--------------------------------------------------------";
1.23 -"--------- encode ^ -> ^^^ ------------------------------";
1.24 -"--------------------------------------------------------";
1.25 -"exported from struct -----------------------------------";
1.26 -"--------------------------------------------------------";
1.27 -"--------- empty rootpbl --------------------------------";
1.28 -"--------- solve_linear as rootpbl FE -------------------";
1.29 -"--------- inspect the CalcTree No.1 with Iterator No.2 -";
1.30 -"--------- miniscript with mini-subpbl ------------------";
1.31 -"--------- mini-subpbl AUTOCALCULATE Step 1 -------------";
1.32 -"--------- solve_linear as rootpbl AUTO CompleteCalc ----";
1.33 -"--------- solve_linear as rootpbl AUTO CompleteHead/Calc ";
1.34 -"--------- mini-subpbl AUTOCALCULATE CompleteCalc -------";
1.35 -"--------- mini-subpbl AUTO CompleteCalcHead ------------";
1.36 -"--------- solve_linear as rootpbl AUTO CompleteModel ---";
1.37 -"--------- setContext..Thy ------------------------------";
1.38 -"--------- mini-subpbl AUTOCALC CompleteToSubpbl --------";
1.39 -"--------- rat-eq + subpbl: no_met, NO solution dropped -";
1.40 -"--------- tryMatchProblem, tryRefineProblem ------------";
1.41 -"--------- modifyCalcHead, resetCalcHead, modelProblem --";
1.42 -"--------- maximum-example, UC: Modeling an example -----";
1.43 -"--------- solve_linear from pbl-hierarchy --------------";
1.44 -"--------- solve_linear as in an algebra system (CAS)----";
1.45 -"--------- interSteps: on 'miniscript with mini-subpbl' -";
1.46 -"--------- getTactic, fetchApplicableTactics ------------";
1.47 -"--------- getAssumptions, getAccumulatedAsms -----------";
1.48 -"--------- arbitrary combinations of steps --------------";
1.49 -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}right";
1.50 -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}other";
1.51 -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}oth 2";
1.52 -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}NOTok";
1.53 -"--------- replaceFormula {SOL:MAN:FOR:replace} right----";
1.54 -"--------- replaceFormula {SOL:MAN:FOR:replace} other----";
1.55 -"--------- replaceFormula {SOL:MAN:FOR:replace} other 2--";
1.56 -"--------- replaceFormula {SOL:MAN:FOR:replace} NOTok----";
1.57 -"--------- UC errpat chain-rule-diff-both, fillpat by input ------";
1.58 -"--------- UC errpat add-fraction, fillpat by input --------------";
1.59 -"--------- UC errpat, fillpat step to Rewrite --------------------";
1.60 -"--------- UC errpat, fillpat step to Rewrite_Set ----------------";
1.61 -"--------------------------------------------------------";
1.62 +"-----------------------------------------------------------------------------";
1.63 +"-----------------------------------------------------------------------------";
1.64 +"table of contents -----------------------------------------------------------";
1.65 +"-----------------------------------------------------------------------------";
1.66 +"-------- TODO ---------------------------------------------------------------";
1.67 +"-----------------------------------------------------------------------------";
1.68 +"-----------------------------------------------------------------------------";
1.69
1.70 -"within struct ---------------------------------------------------";
1.71 -"within struct ---------------------------------------------------";
1.72 -"within struct ---------------------------------------------------";
1.73 -(*==================================================================
1.74
1.75 +"-------- TODO ---------------------------------------------------------------";
1.76 +"-------- TODO ---------------------------------------------------------------";
1.77 +"-------- TODO ---------------------------------------------------------------";
1.78
1.79 -"--------- encode ^ -> ^^^ ------------------------------";
1.80 -"--------- encode ^ -> ^^^ ------------------------------";
1.81 -"--------- encode ^ -> ^^^ ------------------------------";
1.82 -if encode "a^2+b^2=c^2" = "a^^^2+b^^^2=c^^^2" then ()
1.83 -else error "interface.sml: diff.behav. in encode ^ -> ^^^ ";
1.84 -
1.85 -if (decode o encode) "a^2+b^2=c^2" = "a^2+b^2=c^2" then ()
1.86 -else error "interface.sml: diff.behav. in de/encode ^ <-> ^^^ ";
1.87 -
1.88 -==================================================================*)
1.89 -"exported from struct --------------------------------------------";
1.90 -"exported from struct --------------------------------------------";
1.91 -"exported from struct --------------------------------------------";
1.92 -
1.93 -
1.94 -(*------------ set at startup of the Kernel ----------------------*)
1.95 - states:= []; (*resets all state information in Kernel *)
1.96 -(*----------------------------------------------------------------*)
1.97 -
1.98 -"--------- empty rootpbl --------------------------------";
1.99 -"--------- empty rootpbl --------------------------------";
1.100 -"--------- empty rootpbl --------------------------------";
1.101 - CalcTree [([], ("", [], []))];
1.102 - Iterator 1;
1.103 - moveActiveRoot 1;
1.104 - refFormula 1 (get_pos 1 1);
1.105 -(*WN.040222: stoert das sehr, dass e_domID etc. statt leer kommt ???*)
1.106 -DEconstrCalcTree 1;
1.107 -
1.108 -"--------- solve_linear as rootpbl FE -------------------";
1.109 -"--------- solve_linear as rootpbl FE -------------------";
1.110 -"--------- solve_linear as rootpbl FE -------------------";
1.111 - CalcTree (*start of calculation, return No.1*)
1.112 - [(["equality (1+-1*2+x=(0::real))", "solveFor x","solutions L"],
1.113 - ("Test",
1.114 - ["linear","univariate","equation","test"],
1.115 - ["Test","solve_linear"]))];
1.116 - Iterator 1; (*create an active Iterator on CalcTree No.1*)
1.117 -
1.118 - moveActiveRoot 1;(*sets the CalcIterator No.1 at the root of CalcTree No.1*);
1.119 - refFormula 1 (get_pos 1 1) (*gets CalcHead; model is still empty*);
1.120 -
1.121 -
1.122 - fetchProposedTactic 1 (*by using Iterator No.1*);
1.123 - setNextTactic 1 (Model_Problem); (*by using Iterator No.1*)
1.124 - autoCalculate 1 (Step 1);
1.125 - refFormula 1 (get_pos 1 1) (*model contains descriptions for all items*);
1.126 - autoCalculate 1 (Step 1);
1.127 -(*-----since Model_Problem + complete_mod_ in case cas of SOME-----*
1.128 - fetchProposedTactic 1;
1.129 - setNextTactic 1 (Add_Given "equality (1 + -1 * 2 + x = 0)");
1.130 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); (*equality added*);
1.131 -
1.132 - fetchProposedTactic 1;
1.133 - setNextTactic 1 (Add_Given "solveFor x");
1.134 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.135 -
1.136 - fetchProposedTactic 1;
1.137 - setNextTactic 1 (Add_Find "solutions L");
1.138 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.139 -
1.140 - fetchProposedTactic 1;
1.141 - setNextTactic 1 (Specify_Theory "Test");
1.142 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.143 -*-----since Model_Problem + complete_mod_ in case cas of SOME-----*)
1.144 -
1.145 - fetchProposedTactic 1;
1.146 - setNextTactic 1 (Specify_Problem ["linear","univariate","equation","test"]);
1.147 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.148 -(*-------------------------------------------------------------------------*)
1.149 - fetchProposedTactic 1;
1.150 - val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;
1.151 -
1.152 - setNextTactic 1 (Specify_Method ["Test","solve_linear"]);
1.153 - val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;
1.154 -
1.155 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.156 - val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;
1.157 -
1.158 -(*-------------------------------------------------------------------------*)
1.159 - fetchProposedTactic 1;
1.160 - val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;
1.161 -
1.162 - setNextTactic 1 (Apply_Method ["Test","solve_linear"]);
1.163 - (*ERROR.110620 <SETNEXTTACTIC>..<MESSAGE> end-of-calculation*)
1.164 - val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;
1.165 - is_complete_mod ptp;
1.166 - is_complete_spec ptp;
1.167 -
1.168 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.169 - val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;
1.170 - (*term2str (get_obj g_form pt [1]);*)
1.171 -(*-------------------------------------------------------------------------*)
1.172 -
1.173 - fetchProposedTactic 1;
1.174 - setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "isolate_bdv"));
1.175 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.176 -
1.177 - fetchProposedTactic 1;
1.178 - setNextTactic 1 (Rewrite_Set "Test_simplify");
1.179 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.180 -
1.181 - fetchProposedTactic 1;
1.182 - setNextTactic 1 (Check_Postcond ["linear","univariate","equation","test"]);
1.183 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.184 -
1.185 - val ((pt,_),_) = get_calc 1;
1.186 - val ip = get_pos 1 1;
1.187 - val (Form f, tac, asms) = pt_extract (pt, ip);
1.188 - (*exception just above means: 'ModSpec' has been returned: error anyway*)
1.189 - if term2str f = "[x = 1]" then () else
1.190 - error "FE-Kernel-interface.sml: diff.behav. in solve_linear as rootpbl";
1.191 -
1.192 -"--------- inspect the CalcTree No.1 with Iterator No.2 -";
1.193 -"--------- inspect the CalcTree No.1 with Iterator No.2 -";
1.194 -"--------- inspect the CalcTree No.1 with Iterator No.2 -";
1.195 -(*WN041118: inspection shifted to Iterator No.1, because others need pos'*)
1.196 - moveActiveRoot 1;
1.197 - refFormula 1 ([],Pbl); getTactic 1 ([],Pbl);(*Error*)
1.198 - moveActiveDown 1;
1.199 - refFormula 1 ([1],Frm); getTactic 1 ([1],Frm);(*Error*)
1.200 - moveActiveDown 1 ;
1.201 - refFormula 1 ([1],Res); getTactic 1 ([1],Res);(*OK*)
1.202 - (*getAssumption 1 ([1],Res); TODO.WN041217*)
1.203 - moveActiveDown 1 ; refFormula 1 ([2],Res);
1.204 - moveActiveCalcHead 1; refFormula 1 ([],Pbl);
1.205 - moveActiveDown 1;
1.206 - moveActiveDown 1;
1.207 - moveActiveDown 1;
1.208 - if get_pos 1 1 = ([2], Res) then () else
1.209 - error "FE-interface.sml: diff.behav. in a inspect 1 with Iterator 2";
1.210 - moveActiveDown 1; refFormula 1 ([], Res);
1.211 - if get_pos 1 1 = ([], Res) then () else
1.212 - error "FE-interface.sml: diff.behav. in b inspect 1 with Iterator 2";
1.213 - moveActiveCalcHead 1; refFormula 1 ([],Pbl);
1.214 -DEconstrCalcTree 1;
1.215 -
1.216 -"--------- miniscript with mini-subpbl ------------------";
1.217 -"--------- miniscript with mini-subpbl ------------------";
1.218 -"--------- miniscript with mini-subpbl ------------------";
1.219 -(*WN120210?not ME:\label{SOLVE:MANUAL:TACTIC:enter} UC 30.3.2.1 p.175 !!!!!NOT IMPL IN FE*)
1.220 -"=== this sequence of fun-calls resembles fun me ===";
1.221 - states:=[]; (*start of calculation, return No.1*)
1.222 - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
1.223 - ("Test", ["sqroot-test","univariate","equation","test"],
1.224 - ["Test","squ-equ-test-subpbl1"]))];
1.225 - Iterator 1;
1.226 -
1.227 - moveActiveRoot 1;
1.228 - refFormula 1 (get_pos 1 1);
1.229 - fetchProposedTactic 1;
1.230 - setNextTactic 1 (Model_Problem);
1.231 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*gets ModSpec;model is still empty*)
1.232 -
1.233 - fetchProposedTactic 1;
1.234 - setNextTactic 1 (Add_Given "equality (x + 1 = 2)");
1.235 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.236 -
1.237 - fetchProposedTactic 1;
1.238 - setNextTactic 1 (Add_Given "solveFor x");
1.239 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.240 -
1.241 - fetchProposedTactic 1;
1.242 - setNextTactic 1 (Add_Find "solutions L");
1.243 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.244 -
1.245 - fetchProposedTactic 1;
1.246 - setNextTactic 1 (Specify_Theory "Test");
1.247 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.248 -
1.249 - fetchProposedTactic 1;
1.250 - setNextTactic 1 (Specify_Problem
1.251 - ["sqroot-test","univariate","equation","test"]);
1.252 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.253 -"1-----------------------------------------------------------------";
1.254 -
1.255 - fetchProposedTactic 1;
1.256 - setNextTactic 1 (Specify_Method ["Test","squ-equ-test-subpbl1"]);
1.257 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.258 -
1.259 - fetchProposedTactic 1;
1.260 - setNextTactic 1 (Apply_Method ["Test","squ-equ-test-subpbl1"]);
1.261 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.262 -
1.263 - fetchProposedTactic 1;
1.264 - setNextTactic 1 (Rewrite_Set "norm_equation");
1.265 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.266 -
1.267 - fetchProposedTactic 1;
1.268 - setNextTactic 1 (Rewrite_Set "Test_simplify");
1.269 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.270 -
1.271 - fetchProposedTactic 1;(*----------------Subproblem--------------------*);
1.272 - setNextTactic 1 (Subproblem ("Test",
1.273 - ["linear","univariate","equation","test"]));
1.274 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.275 -
1.276 - fetchProposedTactic 1;
1.277 - setNextTactic 1 (Model_Problem );
1.278 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.279 -
1.280 - fetchProposedTactic 1;
1.281 - setNextTactic 1 (Add_Given "equality (-1 + x = 0)");
1.282 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.283 -
1.284 - fetchProposedTactic 1;
1.285 - setNextTactic 1 (Add_Given "solveFor x");
1.286 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.287 -
1.288 - fetchProposedTactic 1;
1.289 - setNextTactic 1 (Add_Find "solutions x_i");
1.290 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.291 -
1.292 - fetchProposedTactic 1;
1.293 - setNextTactic 1 (Specify_Theory "Test");
1.294 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.295 -
1.296 - fetchProposedTactic 1;
1.297 - setNextTactic 1 (Specify_Problem ["linear","univariate","equation","test"]);
1.298 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.299 -"2-----------------------------------------------------------------";
1.300 -
1.301 - fetchProposedTactic 1;
1.302 - setNextTactic 1 (Specify_Method ["Test","solve_linear"]);
1.303 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.304 -
1.305 - fetchProposedTactic 1;
1.306 - setNextTactic 1 (Apply_Method ["Test","solve_linear"]);
1.307 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.308 -
1.309 - fetchProposedTactic 1;
1.310 - setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "isolate_bdv"));
1.311 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.312 -
1.313 - fetchProposedTactic 1;
1.314 - setNextTactic 1 (Rewrite_Set "Test_simplify");
1.315 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.316 -
1.317 - fetchProposedTactic 1;
1.318 - setNextTactic 1 (Check_Postcond ["linear","univariate","equation","test"]);
1.319 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.320 -
1.321 - fetchProposedTactic 1;
1.322 - setNextTactic 1 (Check_elementwise "Assumptions");
1.323 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.324 -
1.325 - val xml = fetchProposedTactic 1;
1.326 - setNextTactic 1 (Check_Postcond
1.327 - ["sqroot-test","univariate","equation","test"]);
1.328 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.329 -
1.330 - val ((pt,_),_) = get_calc 1;
1.331 - val str = pr_ptree pr_short pt;
1.332 - writeln str;
1.333 - val ip = get_pos 1 1;
1.334 - val (Form f, tac, asms) = pt_extract (pt, ip);
1.335 - (*exception just above means: 'ModSpec' has been returned: error anyway*)
1.336 - if term2str f = "[x = 1]" then () else
1.337 - error "FE-interface.sml: diff.behav. in miniscript with mini-subpb";
1.338 - DEconstrCalcTree 1;
1.339 -
1.340 -"--------- mini-subpbl AUTOCALCULATE Step 1 -------------";
1.341 -"--------- mini-subpbl AUTOCALCULATE Step 1 -------------";
1.342 -"--------- mini-subpbl AUTOCALCULATE Step 1 -------------";
1.343 -(*WN120210?not ME:\label{SOLVE:AUTO:one} UC 30.3.3.2 p.176*)
1.344 - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
1.345 - ("Test", ["sqroot-test","univariate","equation","test"],
1.346 - ["Test","squ-equ-test-subpbl1"]))];
1.347 - Iterator 1;
1.348 - moveActiveRoot 1;
1.349 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.350 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.351 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.352 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.353 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.354 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.355 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.356 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.357 - (*here the solve-phase starts*)
1.358 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.359 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.360 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.361 - (*------------------------------------*)
1.362 -(* print_depth 13; get_calc 1;
1.363 - *)
1.364 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.365 - (*calc-head of subproblem*)
1.366 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.367 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.368 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.369 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.370 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.371 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.372 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.373 - (*solve-phase of the subproblem*)
1.374 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.375 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.376 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.377 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.378 - (*finish subproblem*)
1.379 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.380 - (*finish problem*)
1.381 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.382 -
1.383 - (*this checks the test for correctness..*)
1.384 - val ((pt,_),_) = get_calc 1;
1.385 - val p = get_pos 1 1;
1.386 - val (Form f, tac, asms) = pt_extract (pt, p);
1.387 - if term2str f = "[x = 1]" andalso p = ([], Res) then () else
1.388 - error "FE-interface.sml: diff.behav. in miniscript with mini-subpb";
1.389 - DEconstrCalcTree 1;
1.390 -
1.391 -
1.392 -"--------- solve_linear as rootpbl AUTO CompleteCalc ----";
1.393 -"--------- solve_linear as rootpbl AUTO CompleteCalc ----";
1.394 -"--------- solve_linear as rootpbl AUTO CompleteCalc ----";
1.395 -(*WN120210?not ME:\label{SPECIFY:START:auto} UC 30.2.4.2 p.174*)
1.396 - CalcTree
1.397 - [(["equality (1+-1*2+x=(0::real))", "solveFor x","solutions L"],
1.398 - ("Test",
1.399 - ["linear","univariate","equation","test"],
1.400 - ["Test","solve_linear"]))];
1.401 - Iterator 1;
1.402 - moveActiveRoot 1;
1.403 -getFormulaeFromTo 1 ([],Pbl) ([],Pbl) 999 false;
1.404 -
1.405 - autoCalculate 1 CompleteCalc;
1.406 - val (unc, del, gen) = (([],Pbl), ([],Pbl), ([],Res));
1.407 - getFormulaeFromTo 1 unc gen 1 (*only level 1*) false;
1.408 -
1.409 - val ((pt,_),_) = get_calc 1;
1.410 - val p = get_pos 1 1;
1.411 - val (Form f, tac, asms) = pt_extract (pt, p);
1.412 - if term2str f = "[x = 1]" andalso p = ([], Res) then () else
1.413 - error "FE-interface.sml: diff.behav. in solve_linear/rt AUTOCALCULATE ";
1.414 -DEconstrCalcTree 1;
1.415 -
1.416 -"--------- solve_linear as rootpbl AUTO CompleteHead/Calc ";
1.417 -"--------- solve_linear as rootpbl AUTO CompleteHead/Calc ";
1.418 -"--------- solve_linear as rootpbl AUTO CompleteHead/Calc ";
1.419 -(* ERROR: error in kernel ?? *)
1.420 - CalcTree
1.421 - [(["equality (1+-1*2+x=(0::real))", "solveFor x","solutions L"],
1.422 - ("Test",
1.423 - ["linear","univariate","equation","test"],
1.424 - ["Test","solve_linear"]))];
1.425 - Iterator 1;
1.426 - moveActiveRoot 1;
1.427 -
1.428 - autoCalculate 1 CompleteCalcHead;
1.429 - refFormula 1 (get_pos 1 1);
1.430 - val ((pt,p),_) = get_calc 1;
1.431 -
1.432 - autoCalculate 1 CompleteCalc;
1.433 - val ((pt,p),_) = get_calc 1;
1.434 - if p=([], Res) then () else
1.435 - error "FE-interface.sml: diff.behav. in solve_linear AUTOC Head/Calc ";
1.436 -DEconstrCalcTree 1;
1.437 -
1.438 -"--------- mini-subpbl AUTOCALCULATE CompleteCalc -------";
1.439 -"--------- mini-subpbl AUTOCALCULATE CompleteCalc -------";
1.440 -"--------- mini-subpbl AUTOCALCULATE CompleteCalc -------";
1.441 -(*WN120210?not ME:\label{SPECIFY:START:auto} UC 30.2.4.2 p.174*)
1.442 - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
1.443 - ("Test", ["sqroot-test","univariate","equation","test"],
1.444 - ["Test","squ-equ-test-subpbl1"]))];
1.445 - Iterator 1;
1.446 - moveActiveRoot 1;
1.447 - autoCalculate 1 CompleteCalc;
1.448 - val ((pt,p),_) = get_calc 1; show_pt pt;
1.449 -(*
1.450 -getTactic 1 ([1],Frm);
1.451 -getTactic 1 ([1],Res);
1.452 -initContext 1 Thy_ ([1],Res);
1.453 -*)
1.454 - (*... returns calcChangedEvent with*)
1.455 - val (unc, del, gen) = (([],Pbl), ([],Pbl), ([],Res));
1.456 - getFormulaeFromTo 1 unc gen 0 (*only result*) false;
1.457 - getFormulaeFromTo 1 unc gen 1 (*only level 1*) false;
1.458 - getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
1.459 -
1.460 - val ((pt,_),_) = get_calc 1;
1.461 - val p = get_pos 1 1;
1.462 - val (Form f, tac, asms) = pt_extract (pt, p);
1.463 - if term2str f = "[x = 1]" andalso p = ([], Res) then () else
1.464 - error "FE-interface.sml: diff.behav. in mini-subpbl AUTOCALCULATE 6";
1.465 -DEconstrCalcTree 1;
1.466 -
1.467 -"--------- mini-subpbl AUTO CompleteCalcHead ------------";
1.468 -"--------- mini-subpbl AUTO CompleteCalcHead ------------";
1.469 -"--------- mini-subpbl AUTO CompleteCalcHead ------------";
1.470 - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
1.471 - ("Test", ["sqroot-test","univariate","equation","test"],
1.472 - ["Test","squ-equ-test-subpbl1"]))];
1.473 - Iterator 1;
1.474 - moveActiveRoot 1;
1.475 - autoCalculate 1 CompleteCalcHead;
1.476 -
1.477 -val ((Nd (PblObj {env = NONE, fmz = (fm, ("Test", pblID, metID)), loc = (SOME (env, ctxt1), NONE),
1.478 - cell = NONE, ctxt = ctxt2, meth,
1.479 - spec = ("Test", ["sqroot-test", "univariate", "equation", "test"],
1.480 - ["Test", "squ-equ-test-subpbl1"]),
1.481 - probl, branch = TransitiveB, origin, ostate = Incomplete, result}, []),
1.482 - ([], Met)), []) = get_calc 1;
1.483 -if length meth = 3 andalso length probl = 3 (*just some items tested*) then ()
1.484 -else error "--- mini-subpbl AUTO CompleteCalcHead ---";
1.485 -DEconstrCalcTree 1;
1.486 -
1.487 -"--------- solve_linear as rootpbl AUTO CompleteModel ---";
1.488 -"--------- solve_linear as rootpbl AUTO CompleteModel ---";
1.489 -"--------- solve_linear as rootpbl AUTO CompleteModel ---";
1.490 - CalcTree
1.491 - [(["equality (1+-1*2+x=(0::real))", "solveFor x","solutions L"],
1.492 - ("Test",
1.493 - ["linear","univariate","equation","test"],
1.494 - ["Test","solve_linear"]))];
1.495 - Iterator 1;
1.496 - moveActiveRoot 1;
1.497 - autoCalculate 1 CompleteModel;
1.498 - refFormula 1 (get_pos 1 1);
1.499 -
1.500 -setProblem 1 ["linear","univariate","equation","test"];
1.501 -val pos = get_pos 1 1;
1.502 -setContext 1 pos (kestoreID2guh Pbl_["linear","univariate","equation","test"]);
1.503 - refFormula 1 (get_pos 1 1);
1.504 -
1.505 -setMethod 1 ["Test","solve_linear"];
1.506 -setContext 1 pos (kestoreID2guh Met_ ["Test","solve_linear"]);
1.507 - refFormula 1 (get_pos 1 1);
1.508 - val ((pt,_),_) = get_calc 1;
1.509 - if get_obj g_spec pt [] = ("e_domID",
1.510 - ["linear", "univariate","equation","test"],
1.511 - ["Test","solve_linear"]) then ()
1.512 - else error "FE-interface.sml: diff.behav. in setProblem, setMethod";
1.513 -
1.514 - autoCalculate 1 CompleteCalcHead;
1.515 - refFormula 1 (get_pos 1 1);
1.516 - autoCalculate 1 CompleteCalc;
1.517 - moveActiveDown 1;
1.518 - moveActiveDown 1;
1.519 - moveActiveDown 1;
1.520 - refFormula 1 (get_pos 1 1);
1.521 - val ((pt,_),_) = get_calc 1;
1.522 - val p = get_pos 1 1;
1.523 - val (Form f, tac, asms) = pt_extract (pt, p);
1.524 - if term2str f = "[x = 1]" andalso p = ([], Res) then () else
1.525 - error "FE-interface.sml: diff.behav. in mini-subpbl AUTOCALCULATE 6";
1.526 -DEconstrCalcTree 1;
1.527 -
1.528 -"--------- setContext..Thy ------------------------------";
1.529 -"--------- setContext..Thy ------------------------------";
1.530 -"--------- setContext..Thy ------------------------------";
1.531 - states:=[];
1.532 - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
1.533 - ("Test", ["sqroot-test","univariate","equation","test"],
1.534 - ["Test","squ-equ-test-subpbl1"]))];
1.535 - Iterator 1; moveActiveRoot 1;
1.536 - autoCalculate 1 CompleteCalcHead;
1.537 - autoCalculate 1 (Step 1);
1.538 - val ((pt,p),_) = get_calc 1; show_pt pt; (*2 lines, OK*)
1.539 - (*
1.540 - setNextTactic 1 (Rewrite_Set "Test_simplify"); (*--> "thy_isac_Test-rls-Test_simplify"*)
1.541 - autoCalculate 1 (Step 1);
1.542 - val ((pt,p),_) = get_calc 1; show_pt pt;
1.543 - *)
1.544 -"-----^^^^^ and vvvvv do the same -----";
1.545 - setContext 1 p "thy_isac_Test-rls-Test_simplify";
1.546 - val ((pt,p),_) = get_calc 1; show_pt pt; (*2 lines, OK*)
1.547 -
1.548 - autoCalculate 1 (Step 1);
1.549 - setContext 1 p "thy_isac_Test-rls-Test_simplify";
1.550 - val (((pt,_),_), p) = (get_calc 1, get_pos 1 1);
1.551 - val (Form f, tac, asms) = pt_extract (pt, p);
1.552 - if p = ([1], Res) andalso term2str (get_obj g_res pt (fst p)) = "x + 1 + -1 * 2 = 0"
1.553 - then () else error "--- setContext..Thy --- autoCalculate 1 (Step 1) #1";
1.554 -
1.555 - autoCalculate 1 CompleteCalc;
1.556 - val (((pt,_),_), p) = (get_calc 1, get_pos 1 1);
1.557 - val (Form f, tac, asms) = pt_extract (pt, p);
1.558 -
1.559 - if term2str f = "[x = 1]" andalso p = ([], Res) then ()
1.560 - else error "--- setContext..Thy --- autoCalculate CompleteCalc";
1.561 - DEconstrCalcTree 1;
1.562 -
1.563 -"--------- mini-subpbl AUTOCALC CompleteToSubpbl --------";
1.564 -"--------- mini-subpbl AUTOCALC CompleteToSubpbl --------";
1.565 -"--------- mini-subpbl AUTOCALC CompleteToSubpbl --------";
1.566 - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
1.567 - ("Test", ["sqroot-test","univariate","equation","test"],
1.568 - ["Test","squ-equ-test-subpbl1"]))];
1.569 - Iterator 1; moveActiveRoot 1;
1.570 - autoCalculate 1 CompleteToSubpbl;
1.571 - refFormula 1 (get_pos 1 1); (*<ISA> -1 + x = 0 </ISA>*);
1.572 - val ((pt,_),_) = get_calc 1;
1.573 - val str = pr_ptree pr_short pt;
1.574 - writeln str;
1.575 - if str = ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + -1 * 2 = 0\n"
1.576 - then () else
1.577 - error "FE-interface.sml: diff.behav. in mini-subpbl CompleteToSubpbl-1";
1.578 -
1.579 - autoCalculate 1 (Step 1); (*proceeds only, of NOT 1 step before subplb*)
1.580 - autoCalculate 1 CompleteToSubpbl;
1.581 - val ((pt,_),_) = get_calc 1;
1.582 - val str = pr_ptree pr_short pt;
1.583 - writeln str;
1.584 - autoCalculate 1 CompleteCalc; (*das geht ohnehin !*);
1.585 - val ((pt,_),_) = get_calc 1;
1.586 - val p = get_pos 1 1;
1.587 -
1.588 - val (Form f, tac, asms) = pt_extract (pt, p);
1.589 - if term2str f = "[x = 1]" andalso p = ([], Res) then () else
1.590 - error "FE-interface.sml: diff.behav. in mini-subpbl CompleteToSubpbl 1";
1.591 -DEconstrCalcTree 1;
1.592 -
1.593 -"--------- rat-eq + subpbl: no_met, NO solution dropped -";
1.594 -"--------- rat-eq + subpbl: no_met, NO solution dropped -";
1.595 -"--------- rat-eq + subpbl: no_met, NO solution dropped -";
1.596 - CalcTree
1.597 - [(["equality ((5*x)/(x - 2) - x/(x+2)=(4::real))", "solveFor x","solutions L"],
1.598 - ("RatEq", ["univariate","equation"], ["no_met"]))];
1.599 - Iterator 1;
1.600 - moveActiveRoot 1;
1.601 - fetchProposedTactic 1;
1.602 -
1.603 - setNextTactic 1 (Model_Problem);
1.604 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.605 -
1.606 - setNextTactic 1 (Specify_Theory "RatEq");
1.607 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.608 - setNextTactic 1 (Specify_Problem ["rational","univariate","equation"]);
1.609 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.610 - setNextTactic 1 (Specify_Method ["RatEq","solve_rat_equation"]);
1.611 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.612 - setNextTactic 1 (Apply_Method ["RatEq","solve_rat_equation"]);
1.613 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.614 - setNextTactic 1 (Rewrite_Set "RatEq_simplify");
1.615 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.616 - setNextTactic 1 (Rewrite_Set "norm_Rational");
1.617 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.618 - setNextTactic 1 (Rewrite_Set "RatEq_eliminate");
1.619 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.620 - (* __________ for "12 * x + 4 * x ^^^ 2 = 4 * (-4 + x ^^^ 2)"*)
1.621 - setNextTactic 1 (Subproblem ("PolyEq", ["normalize","polynomial",
1.622 - "univariate","equation"]));
1.623 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.624 - setNextTactic 1 (Model_Problem );
1.625 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.626 - setNextTactic 1 (Specify_Theory "PolyEq");
1.627 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.628 - setNextTactic 1 (Specify_Problem ["normalize","polynomial",
1.629 - "univariate","equation"]);
1.630 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.631 - setNextTactic 1 (Specify_Method ["PolyEq","normalize_poly"]);
1.632 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.633 - setNextTactic 1 (Apply_Method ["PolyEq","normalize_poly"]);
1.634 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.635 - setNextTactic 1 (Rewrite ("all_left",""));
1.636 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.637 - setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "make_ratpoly_in"));
1.638 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.639 - (* __________ for "16 + 12 * x = 0"*)
1.640 - setNextTactic 1 (Subproblem ("PolyEq",
1.641 - ["degree_1","polynomial","univariate","equation"]));
1.642 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.643 - setNextTactic 1 (Model_Problem );
1.644 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.645 - setNextTactic 1 (Specify_Theory "PolyEq");
1.646 - (*------------- some trials in the problem-hierarchy ---------------*)
1.647 - setNextTactic 1 (Specify_Problem ["linear","univariate","equation"]);
1.648 - autoCalculate 1 (Step 1); fetchProposedTactic 1; (*<ERROR> helpless </ERROR> !!!*)
1.649 - setNextTactic 1 (Refine_Problem ["univariate","equation"]);
1.650 - (*------------------------------------------------------------------*)
1.651 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.652 - setNextTactic 1 (Specify_Method ["PolyEq","solve_d1_polyeq_equation"]);
1.653 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.654 - setNextTactic 1 (Apply_Method ["PolyEq","solve_d1_polyeq_equation"]);
1.655 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.656 - setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "d1_polyeq_simplify"));
1.657 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.658 - setNextTactic 1 (Rewrite_Set "polyeq_simplify");
1.659 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.660 - setNextTactic 1 Or_to_List;
1.661 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.662 - setNextTactic 1 (Check_elementwise "Assumptions");
1.663 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.664 - setNextTactic 1 (Check_Postcond ["degree_1","polynomial",
1.665 - "univariate","equation"]);
1.666 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.667 - setNextTactic 1 (Check_Postcond ["normalize","polynomial",
1.668 - "univariate","equation"]);
1.669 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.670 - setNextTactic 1 (Check_Postcond ["rational","univariate","equation"]);
1.671 - val (ptp,_) = get_calc 1;
1.672 - val (Form t,_,_) = pt_extract ptp;
1.673 - if get_pos 1 1 = ([], Res) andalso term2str t = "[x = -4 / 3]" then ()
1.674 - else writeln "FE-inteface.sml: diff.behav. in rat-eq + subpbl: no_met, NO ..";
1.675 -DEconstrCalcTree 1;
1.676 -
1.677 -"--------- tryMatchProblem, tryRefineProblem ------------";
1.678 -"--------- tryMatchProblem, tryRefineProblem ------------";
1.679 -"--------- tryMatchProblem, tryRefineProblem ------------";
1.680 -(*{\bf\UC{Having \isac{} Refine the Problem
1.681 - * Automatically}\label{SPECIFY:refine-auto}\\} test match and refine with
1.682 - * x^^^2 + 4*x + 5 = 2
1.683 -see isac.bridge.TestSpecify#testMatchRefine*)
1.684 - CalcTree
1.685 - [(["equality (x^2 + 4*x + 5 = (2::real))", "solveFor x","solutions L"],
1.686 - ("Isac",
1.687 - ["univariate","equation"],
1.688 - ["no_met"]))];
1.689 - Iterator 1;
1.690 - moveActiveRoot 1;
1.691 -
1.692 - fetchProposedTactic 1;
1.693 - setNextTactic 1 (Model_Problem );
1.694 - (*..this tactic should be done 'tacitly', too !*)
1.695 -
1.696 -(*
1.697 -autoCalculate 1 CompleteCalcHead;
1.698 -checkContext 1 ([],Pbl) "pbl_equ_univ";
1.699 -checkContext 1 ([],Pbl) (kestoreID2guh Pbl_ ["univariate","equation"]);
1.700 -*)
1.701 -
1.702 - autoCalculate 1 (Step 1);
1.703 -
1.704 - fetchProposedTactic 1;
1.705 - setNextTactic 1 (Add_Given "equality (x ^^^ 2 + 4 * x + 5 = (2::real))");
1.706 - autoCalculate 1 (Step 1);
1.707 -
1.708 - "--------- we go into the ProblemBrowser (_NO_ pblID selected) -";
1.709 -initContext 1 Pbl_ ([],Pbl);
1.710 -initContext 1 Met_ ([],Pbl);
1.711 -
1.712 - "--------- this match will show some incomplete items: ---------";
1.713 -
1.714 -checkContext 1 ([],Pbl) (kestoreID2guh Pbl_ ["univariate","equation"]);
1.715 -checkContext 1 ([],Pbl) (kestoreID2guh Met_ ["LinEq", "solve_lineq_equation"]);
1.716 -
1.717 -
1.718 - fetchProposedTactic 1;
1.719 - setNextTactic 1 (Add_Given "solveFor x"); autoCalculate 1 (Step 1);
1.720 -
1.721 - fetchProposedTactic 1;
1.722 - setNextTactic 1 (Add_Find "solutions L"); autoCalculate 1 (Step 1);
1.723 -
1.724 - "--------- this is a matching model (all items correct): -------";
1.725 -checkContext 1 ([],Pbl) (kestoreID2guh Pbl_ ["univariate","equation"]);
1.726 - "--------- this is a NOT matching model (some 'false': ---------";
1.727 -checkContext 1 ([],Pbl)(kestoreID2guh Pbl_ ["linear","univariate","equation"]);
1.728 -
1.729 - "--------- find out a matching problem: ------------------------";
1.730 - "--------- find out a matching problem (FAILING: no new pbl) ---";
1.731 - refineProblem 1([],Pbl)(pblID2guh ["linear","univariate","equation"]);
1.732 -
1.733 - "--------- find out a matching problem (SUCCESSFUL) ------------";
1.734 - refineProblem 1 ([],Pbl) (pblID2guh ["univariate","equation"]);
1.735 -
1.736 - "--------- tryMatch, tryRefine did not change the calculation -";
1.737 - "--------- this is done by <TRANSFER> on the pbl-browser: ------";
1.738 - setNextTactic 1 (Specify_Problem ["normalize","polynomial",
1.739 - "univariate","equation"]);
1.740 - autoCalculate 1 (Step 1);
1.741 -(*WN050904 fetchProposedTactic again --> Specify_Problem ["normalize",...
1.742 - and Specify_Theory skipped in comparison to below ---^^^-inserted *)
1.743 -(*------------vvv-inserted-----------------------------------------------*)
1.744 - fetchProposedTactic 1;
1.745 - setNextTactic 1 (Specify_Problem ["normalize","polynomial",
1.746 - "univariate","equation"]);
1.747 - autoCalculate 1 (Step 1);
1.748 -
1.749 -(*and Specify_Theory skipped by fetchProposedTactic ?!?*)
1.750 -
1.751 - fetchProposedTactic 1;
1.752 - setNextTactic 1 (Specify_Method ["PolyEq","normalize_poly"]);
1.753 - autoCalculate 1 (Step 1);
1.754 -
1.755 - fetchProposedTactic 1;
1.756 - setNextTactic 1 (Apply_Method ["PolyEq","normalize_poly"]);
1.757 -
1.758 - autoCalculate 1 CompleteCalc;
1.759 -
1.760 - val ((pt,_),_) = get_calc 1;
1.761 - show_pt pt;
1.762 - val p = get_pos 1 1;
1.763 - val (Form f, tac, asms) = pt_extract (pt, p);
1.764 - if term2str f = "[x = -1, x = -3]" andalso p = ([], Res) then () else
1.765 - error "FE-interface.sml: diff.behav. in tryMatchProblem, tryRefine";
1.766 -
1.767 -(*------------^^^-inserted-----------------------------------------------*)
1.768 -(*WN050904 the fetchProposedTactic's below may not have worked like that
1.769 - before, too, because there was no check*)
1.770 - fetchProposedTactic 1;
1.771 - setNextTactic 1 (Specify_Theory "PolyEq");
1.772 - autoCalculate 1 (Step 1);
1.773 -
1.774 - fetchProposedTactic 1;
1.775 - setNextTactic 1 (Specify_Method ["PolyEq","normalize_poly"]);
1.776 - autoCalculate 1 (Step 1);
1.777 -
1.778 - fetchProposedTactic 1;
1.779 - "--------- now the calc-header is ready for enter 'solving' ----";
1.780 - autoCalculate 1 CompleteCalc;
1.781 -
1.782 - val ((pt,_),_) = get_calc 1;
1.783 - rootthy pt;
1.784 - show_pt pt;
1.785 - val p = get_pos 1 1;
1.786 - val (Form f, tac, asms) = pt_extract (pt, p);
1.787 - if term2str f = "[x = -1, x = -3]" andalso p = ([], Res) then () else
1.788 - error "FE-interface.sml: diff.behav. in tryMatchProblem, tryRefine";
1.789 -
1.790 -DEconstrCalcTree 1;
1.791 -
1.792 -"--------- modifyCalcHead, resetCalcHead, modelProblem --";
1.793 -"--------- modifyCalcHead, resetCalcHead, modelProblem --";
1.794 -"--------- modifyCalcHead, resetCalcHead, modelProblem --";
1.795 - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
1.796 - ("Test", ["sqroot-test","univariate","equation","test"],
1.797 - ["Test","squ-equ-test-subpbl1"]))];
1.798 - Iterator 1;
1.799 - moveActiveRoot 1;
1.800 -
1.801 - modifyCalcHead 1 (([],Pbl),(*the position from refFormula*)
1.802 - "solve (x+1=2, x)",(*the headline*)
1.803 - [Given ["equality (x+1=(2::real))", "solveFor x"],
1.804 - Find ["solutions L"](*,Relate []*)],
1.805 - Pbl,
1.806 - ("Test",
1.807 - ["sqroot-test","univariate","equation","test"],
1.808 - ["Test","squ-equ-test-subpbl1"]));
1.809 -
1.810 -val ((Nd (PblObj {env = NONE,
1.811 - fmz = (fm, tpm),
1.812 - loc = (SOME scrst_ctxt, NONE),
1.813 - ctxt,
1.814 - cell = NONE,
1.815 - meth,
1.816 - spec = (thy,
1.817 - ["sqroot-test", "univariate", "equation", "test"],
1.818 - ["Test", "squ-equ-test-subpbl1"]),
1.819 - probl,
1.820 - branch = TransitiveB,
1.821 - origin,
1.822 - ostate = Incomplete,
1.823 - result},
1.824 - []),
1.825 - ([], Pbl)),
1.826 - []) = get_calc 1;
1.827 -(*WN110622: is the same as in 2002, but shouldn't be probl = [3 items?]*)
1.828 -if length meth = 0 andalso length probl = 0 (*just some items tested*) then ()
1.829 -else error "--- modifyCalcHead, resetCalcHead, modelProblem 1 --";
1.830 -
1.831 -resetCalcHead 1;
1.832 -modelProblem 1;
1.833 -
1.834 -get_calc 1;
1.835 -val ((Nd (PblObj {env = NONE,
1.836 - fmz = (fm, tpm),
1.837 - loc = (SOME scrst_ctxt, NONE),
1.838 - ctxt,
1.839 - cell = NONE,
1.840 - meth,
1.841 - spec = ("e_domID", ["e_pblID"], ["e_metID"]),
1.842 - probl,
1.843 - branch = TransitiveB,
1.844 - origin,
1.845 - ostate = Incomplete,
1.846 - result},
1.847 - []),
1.848 - ([], Pbl)),
1.849 - []) = get_calc 1;
1.850 -if length meth = 3 andalso length probl = 3 (*just some items tested*) then ()
1.851 -else error "--- modifyCalcHead, resetCalcHead, modelProblem 2 --";
1.852 -
1.853 -"--------- maximum-example, UC: Modeling an example -----";
1.854 -"--------- maximum-example, UC: Modeling an example -----";
1.855 -"--------- maximum-example, UC: Modeling an example -----";
1.856 -(* {\bf\UC{Editing the Model}\label{SPECIFY:enter}\label{SPECIFY:check}\\}
1.857 -see isac.bridge.TestModel#testEditItems
1.858 -*)
1.859 - val elems = ["fixedValues [r=Arbfix]","maximum A","valuesFor [a,b]",
1.860 - "relations [A=a*b, (a/2)^2 + (b/2)^2 = r^2]",
1.861 - "relations [A=a*b, (a/2)^2 + (b/2)^2 = r^2]",
1.862 - "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]",
1.863 - (*^^^ these are the elements for the root-problem (in variants)*)
1.864 - (*vvv these are elements required for subproblems*)
1.865 - "boundVariable a","boundVariable b","boundVariable alpha",
1.866 - "interval {x::real. 0 <= x & x <= 2*r}",
1.867 - "interval {x::real. 0 <= x & x <= 2*r}",
1.868 - "interval {x::real. 0 <= x & x <= pi}",
1.869 - "errorBound (eps=(0::real))"]
1.870 - (*specifying is not interesting for this example*)
1.871 - val spec = ("DiffApp", ["maximum_of","function"],
1.872 - ["DiffApp","max_by_calculus"]);
1.873 - (*the empty model with descriptions for user-guidance by Model_Problem*)
1.874 - val empty_model = [Given ["fixedValues []"],
1.875 - Find ["maximum", "valuesFor"],
1.876 - Relate ["relations []"]];
1.877 - DEconstrCalcTree 1;
1.878 -
1.879 -"#################################################################";
1.880 -
1.881 - CalcTree [(elems, spec)];
1.882 - Iterator 1;
1.883 - moveActiveRoot 1;
1.884 - refFormula 1 (get_pos 1 1);
1.885 - (*this gives a completely empty model*)
1.886 -
1.887 - fetchProposedTactic 1;
1.888 -(*fill the CalcHead with Descriptions...*)
1.889 - setNextTactic 1 (Model_Problem );
1.890 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.891 -
1.892 - (*user input is !!!!!EITHER!!!!! _some_ (at least one) items of the model
1.893 - !!!!!OR!!!!! _one_ part of the specification !!!!!!!!!!!!!*)
1.894 - (*input of two items, 'fixedValues [r=Arbfix]' and 'maximum b'...*)
1.895 - modifyCalcHead 1 (([],Pbl) (*position, from previous refFormula*),
1.896 - "Problem (DiffApp.thy, [maximum_of, function])",
1.897 - (*the head-form ^^^ is not used for input here*)
1.898 - [Given ["fixedValues [r=Arbfix]"(*new input*)],
1.899 - Find ["maximum b"(*new input*), "valuesFor"],
1.900 - Relate ["relations"]],
1.901 - (*input (Arbfix will dissappear soon)*)
1.902 - Pbl (*belongsto*),
1.903 - e_spec (*no input to the specification*));
1.904 -
1.905 - (*the user does not know, what 'superfluous' for 'maximum b' may mean
1.906 - and asks what to do next*)
1.907 - fetchProposedTactic 1;
1.908 - (*the student follows the advice*)
1.909 - setNextTactic 1 (Add_Find "maximum A"); (*FIXME.17.11.03: does not yet work*)
1.910 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.911 -
1.912 - (*this input completes the model*)
1.913 - modifyCalcHead 1 (([],Pbl), "not used here",
1.914 - [Given ["fixedValues [r=Arbfix]"],
1.915 - Find ["maximum A", "valuesFor [a,b]"(*new input*)],
1.916 - Relate ["relations [A=a*b, \
1.917 - \(a/2)^2 + (b/2)^2 = r^2]"]], Pbl, e_spec);
1.918 -
1.919 - (*specification is not interesting and should be skipped by the dialogguide;
1.920 - !!!!!!!!!!!!!!!!!!!! input of ONE part at a time !!!!!!!!!!!!!!!!!!!!!!*)
1.921 - modifyCalcHead 1 (([],Pbl), "not used here",
1.922 - [Given ["fixedValues [r=Arbfix]"],
1.923 - Find ["maximum A", "valuesFor [a,b]"(*new input*)],
1.924 - Relate ["relations [A=a*b, \
1.925 - \(a/2)^2 + (b/2)^2 = r^2]"]], Pbl,
1.926 - ("DiffApp", ["e_pblID"], ["e_metID"]));
1.927 - modifyCalcHead 1 (([],Pbl), "not used here",
1.928 - [Given ["fixedValues [r=Arbfix]"],
1.929 - Find ["maximum A", "valuesFor [a,b]"(*new input*)],
1.930 - Relate ["relations [A=a*b, \
1.931 - \(a/2)^2 + (b/2)^2 = r^2]"]], Pbl,
1.932 - ("DiffApp", ["maximum_of","function"],
1.933 - ["e_metID"]));
1.934 - modifyCalcHead 1 (([],Pbl), "not used here",
1.935 - [Given ["fixedValues [r=Arbfix]"],
1.936 - Find ["maximum A", "valuesFor [a,b]"(*new input*)],
1.937 - Relate ["relations [A=a*b, \
1.938 - \(a/2)^2 + (b/2)^2 = r^2]"]], Pbl,
1.939 - ("DiffApp", ["maximum_of","function"],
1.940 - ["DiffApp","max_by_calculus"]));
1.941 - (*this final calcHead now has STATUS 'complete' !*)
1.942 - DEconstrCalcTree 1;
1.943 -
1.944 -"--------- solve_linear from pbl-hierarchy --------------";
1.945 -"--------- solve_linear from pbl-hierarchy --------------";
1.946 -"--------- solve_linear from pbl-hierarchy --------------";
1.947 - val (fmz, sp) = ([], ("", ["linear","univariate","equation","test"], []));
1.948 - CalcTree [(fmz, sp)];
1.949 - Iterator 1; moveActiveRoot 1;
1.950 - refFormula 1 (get_pos 1 1);
1.951 - modifyCalcHead 1 (([],Pbl),"solve (1+-1*2+x=(0::real))",
1.952 - [Given ["equality (1+-1*2+x=(0::real))", "solveFor x"],
1.953 - Find ["solutions L"]],
1.954 - Pbl,
1.955 - ("Test", ["linear","univariate","equation","test"],
1.956 - ["Test","solve_linear"]));
1.957 - autoCalculate 1 CompleteCalc;
1.958 - refFormula 1 (get_pos 1 1);
1.959 - val ((pt,_),_) = get_calc 1;
1.960 - val p = get_pos 1 1;
1.961 - val (Form f, tac, asms) = pt_extract (pt, p);
1.962 - if term2str f = "[x = 1]" andalso p = ([], Res)
1.963 - andalso terms2str asms = "[\"matches (?a = ?b) (1 + -1 * 2 + x = 0)\"]" then ()
1.964 - else error "FE-interface.sml: diff.behav. in from pbl -hierarchy";
1.965 - DEconstrCalcTree 1;
1.966 -
1.967 -"--------- solve_linear as in an algebra system (CAS)----";
1.968 -"--------- solve_linear as in an algebra system (CAS)----";
1.969 -"--------- solve_linear as in an algebra system (CAS)----";
1.970 -(*WN120210?not ME:\label{UC:cas-input} UC 30.1.2.5 p.168*)
1.971 - val (fmz, sp) = ([], ("", [], []));
1.972 - CalcTree [(fmz, sp)];
1.973 - Iterator 1; moveActiveRoot 1;
1.974 - modifyCalcHead 1 (([],Pbl),"solveTest (1+-1*2+x=0,x)", [], Pbl, ("", [], []));
1.975 - autoCalculate 1 CompleteCalc;
1.976 - refFormula 1 (get_pos 1 1);
1.977 - val ((pt,_),_) = get_calc 1;
1.978 - val p = get_pos 1 1;
1.979 - val (Form f, tac, asms) = pt_extract (pt, p);
1.980 - if term2str f = "[x = 1]" andalso p = ([], Res)
1.981 - andalso terms2str asms = "[\"matches (?a = ?b) (1 + -1 * 2 + x = 0)\"]" then ()
1.982 - else error "FE-interface.sml: diff.behav. in from pbl -hierarchy";
1.983 -DEconstrCalcTree 1;
1.984 -
1.985 -"--------- interSteps: on 'miniscript with mini-subpbl' -";
1.986 -"--------- interSteps: on 'miniscript with mini-subpbl' -";
1.987 -"--------- interSteps: on 'miniscript with mini-subpbl' -";
1.988 - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
1.989 - ("Test", ["sqroot-test","univariate","equation","test"],
1.990 - ["Test","squ-equ-test-subpbl1"]))];
1.991 - Iterator 1;
1.992 - moveActiveRoot 1;
1.993 - autoCalculate 1 CompleteCalc;
1.994 - val ((pt,_),_) = get_calc 1;
1.995 - show_pt pt;
1.996 -
1.997 - (*UC\label{UC:inter-steps} UC 30.3.5.5 p.178*)
1.998 - interSteps 1 ([2],Res);
1.999 - val ((pt,_),_) = get_calc 1; show_pt pt (*new ([2,1],Frm)..([2,6],Res)*);
1.1000 - val (unc, del, gen) = (([1],Res),([1],Res),([2,6],Res));
1.1001 - getFormulaeFromTo 1 unc gen 1 false;
1.1002 -
1.1003 - (*UC\label{UC:inter-steps} UC 30.3.5.5 p.178*)
1.1004 - interSteps 1 ([3,2],Res);
1.1005 - val ((pt,_),_) = get_calc 1; show_pt pt (*new ([3,2,1],Frm)..([3,2,2],Res)*);
1.1006 - val (unc, del, gen) = (([3,1],Res),([3,1],Res),([3,2,2],Res));
1.1007 - getFormulaeFromTo 1 unc gen 1 false;
1.1008 -
1.1009 - (*UC\label{UC:inter-steps} UC 30.3.5.5 p.178*)
1.1010 - interSteps 1 ([3],Res) (*no new steps in subproblems*);
1.1011 - val (unc, del, gen) = (([3],Pbl),([3],Pbl),([3,2],Res));
1.1012 - getFormulaeFromTo 1 unc gen 1 false;
1.1013 -
1.1014 - (*UC\label{UC:inter-steps} UC 30.3.5.5 p.178*)
1.1015 - interSteps 1 ([],Res) (*no new steps in subproblems*);
1.1016 - val (unc, del, gen) = (([],Pbl),([],Pbl),([4],Res));
1.1017 - getFormulaeFromTo 1 unc gen 1 false;
1.1018 -DEconstrCalcTree 1;
1.1019 -
1.1020 -"--------- getTactic, fetchApplicableTactics ------------";
1.1021 -"--------- getTactic, fetchApplicableTactics ------------";
1.1022 -"--------- getTactic, fetchApplicableTactics ------------";
1.1023 -(* compare test/../script.sml
1.1024 -"----------- fun sel_rules ---------------------------------------";
1.1025 -*)
1.1026 - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
1.1027 - ("Test", ["sqroot-test","univariate","equation","test"],
1.1028 - ["Test","squ-equ-test-subpbl1"]))];
1.1029 - Iterator 1; moveActiveRoot 1;
1.1030 - autoCalculate 1 CompleteCalc;
1.1031 - val ((pt,_),_) = get_calc 1;
1.1032 - show_pt pt;
1.1033 -
1.1034 - (*UC\label{SOLVE:HIDE:getTactic} \label{SOLVE:AUTO:tactic} UC 30.3.3.1 p.176
1.1035 -WN120210 not impl. in FE*)
1.1036 - getTactic 1 ([],Pbl);
1.1037 - getTactic 1 ([1],Res);
1.1038 - getTactic 1 ([3],Pbl);
1.1039 - getTactic 1 ([3,1],Frm);
1.1040 - getTactic 1 ([3],Res);
1.1041 - getTactic 1 ([],Res);
1.1042 -
1.1043 -(*UC\label{SOLVE:MANUAL:TACTIC:listall} UC 30.3.2.2 p.175*)
1.1044 - fetchApplicableTactics 1 99999 ([],Pbl);
1.1045 - fetchApplicableTactics 1 99999 ([1],Res);
1.1046 - fetchApplicableTactics 1 99999 ([3],Pbl);
1.1047 - fetchApplicableTactics 1 99999 ([3,1],Res);
1.1048 - fetchApplicableTactics 1 99999 ([3],Res);
1.1049 - fetchApplicableTactics 1 99999 ([],Res);
1.1050 -DEconstrCalcTree 1;
1.1051 -
1.1052 -"--------- getAssumptions, getAccumulatedAsms -----------";
1.1053 -"--------- getAssumptions, getAccumulatedAsms -----------";
1.1054 -"--------- getAssumptions, getAccumulatedAsms -----------";
1.1055 -CalcTree
1.1056 -[(["equality (x/(x^2 - 6*x+9) - 1/(x^2 - 3*x) =1/x)",
1.1057 - "solveFor x","solutions L"],
1.1058 - ("RatEq",["univariate","equation"],["no_met"]))];
1.1059 -Iterator 1; moveActiveRoot 1;
1.1060 -autoCalculate 1 CompleteCalc;
1.1061 -val ((pt,_),_) = get_calc 1;
1.1062 -val p = get_pos 1 1;
1.1063 -val (Form f, tac, asms) = pt_extract (pt, p);
1.1064 -(*============ inhibit exn WN120316 compare 2002--2011 ===========================
1.1065 -if map term2str asms =
1.1066 - ["True |\n~ lhs ((3 + -1 * x + x ^^^ 2) * x =\n" ^
1.1067 - " 1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)) is_poly_in x", "-6 * x + 5 * x ^^^ 2 = 0",
1.1068 - "lhs (-6 * x + 5 * x ^^^ 2 = 0) is_poly_in x",
1.1069 - "lhs (-6 * x + 5 * x ^^^ 2 = 0) has_degree_in x = 2",
1.1070 - "9 * x + -6 * x ^^^ 2 + x ^^^ 3 ~= 0"]
1.1071 -andalso term2str f = "[-6 * x + 5 * x ^^^ 2 = 0]" andalso p = ([], Res) then ()
1.1072 -else error "TODO compare 2002--2011"; (*...data during test --- x / (x ^ 2 - 6 * x + 9) - 1...*)
1.1073 -============ inhibit exn WN120316 compare 2002--2011 ===========================*)
1.1074 -if p = ([], Res) andalso term2str f = "[]" (*see WN120317.TODO dropped rateq*)
1.1075 -andalso asms = [] (*STRANGE!, compare test --- x / (x ^ 2 - 6 * x + 9) - 1 / (x ^ 2 ...*)
1.1076 -then () else error "rlang.sml: diff.behav. in Schalk I s.87 Bsp 55b [x = 6 / 5]";
1.1077 -
1.1078 -(*UC\label{SOLVE:HELP:assumptions} UC 30.3.5.1 p.178*)
1.1079 -getAssumptions 1 ([3], Res);
1.1080 -getAssumptions 1 ([5], Res);
1.1081 -(*UC\label{SOLVE:HELP:assumptions-origin} UC 30.3.5.2 p.178
1.1082 - WN0502 still without positions*)
1.1083 -getAccumulatedAsms 1 ([3], Res);
1.1084 -getAccumulatedAsms 1 ([5], Res);
1.1085 -DEconstrCalcTree 1;
1.1086 -
1.1087 -"--------- arbitrary combinations of steps --------------";
1.1088 -"--------- arbitrary combinations of steps --------------";
1.1089 -"--------- arbitrary combinations of steps --------------";
1.1090 - CalcTree (*start of calculation, return No.1*)
1.1091 - [(["equality (1+-1*2+x=(0::real))", "solveFor x","solutions L"],
1.1092 - ("Test",
1.1093 - ["linear","univariate","equation","test"],
1.1094 - ["Test","solve_linear"]))];
1.1095 - Iterator 1; moveActiveRoot 1;
1.1096 -
1.1097 - fetchProposedTactic 1;
1.1098 - (*ERROR get_calc 1 not existent*)
1.1099 - setNextTactic 1 (Model_Problem );
1.1100 - autoCalculate 1 (Step 1);
1.1101 - fetchProposedTactic 1;
1.1102 - fetchProposedTactic 1;
1.1103 -
1.1104 - setNextTactic 1 (Add_Find "solutions L");
1.1105 - setNextTactic 1 (Add_Find "solutions L");
1.1106 -
1.1107 - autoCalculate 1 (Step 1);
1.1108 - autoCalculate 1 (Step 1);
1.1109 -
1.1110 - setNextTactic 1 (Specify_Theory "Test");
1.1111 - fetchProposedTactic 1;
1.1112 - autoCalculate 1 (Step 1);
1.1113 -
1.1114 - autoCalculate 1 (Step 1);
1.1115 - autoCalculate 1 (Step 1);
1.1116 - autoCalculate 1 (Step 1);
1.1117 - autoCalculate 1 (Step 1);
1.1118 -(*------------------------- end calc-head*)
1.1119 -
1.1120 - fetchProposedTactic 1;
1.1121 - setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "isolate_bdv"));
1.1122 - autoCalculate 1 (Step 1);
1.1123 -
1.1124 - setNextTactic 1 (Rewrite_Set "Test_simplify");
1.1125 - fetchProposedTactic 1;
1.1126 - autoCalculate 1 (Step 1);
1.1127 -
1.1128 - autoCalculate 1 CompleteCalc;
1.1129 - val ((pt,_),_) = get_calc 1;
1.1130 - val p = get_pos 1 1;
1.1131 - val (Form f, tac, asms) = pt_extract (pt, p);
1.1132 - if term2str f = "[x = 1]" andalso p = ([], Res) then () else
1.1133 - error "FE-interface.sml: diff.behav. in combinations of steps";
1.1134 -DEconstrCalcTree 1;
1.1135 -
1.1136 -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}right"; (*UC 30.3.2.4 p.175*)
1.1137 -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}right";
1.1138 -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}right";
1.1139 - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
1.1140 - ("Test", ["sqroot-test","univariate","equation","test"],
1.1141 - ["Test","squ-equ-test-subpbl1"]))];
1.1142 - Iterator 1;
1.1143 - moveActiveRoot 1;
1.1144 - autoCalculate 1 CompleteCalcHead;
1.1145 - autoCalculate 1 (Step 1);
1.1146 - autoCalculate 1 (Step 1);
1.1147 - appendFormula 1 "-1 + x = 0";
1.1148 - (*... returns calcChangedEvent with*)
1.1149 - val (unc, del, gen) = (([1],Res), ([1],Res), ([2],Res));
1.1150 - getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
1.1151 -
1.1152 - val ((pt,_),_) = get_calc 1;
1.1153 - val p = get_pos 1 1;
1.1154 - val (Form f, tac, asms) = pt_extract (pt, p);
1.1155 - if term2str f = "-1 + x = 0" andalso p = ([2], Res) then () else
1.1156 - error "FE-interface.sml: diff.behav. in FORMULA:enter} right";
1.1157 -DEconstrCalcTree 1;
1.1158 -
1.1159 -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}other"; (*UC 30.3.2.4 p.175*)
1.1160 -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}other";
1.1161 -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}other";
1.1162 - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
1.1163 - ("Test", ["sqroot-test","univariate","equation","test"],
1.1164 - ["Test","squ-equ-test-subpbl1"]))];
1.1165 - Iterator 1;
1.1166 - moveActiveRoot 1;
1.1167 - autoCalculate 1 CompleteCalcHead;
1.1168 - autoCalculate 1 (Step 1);
1.1169 - autoCalculate 1 (Step 1);
1.1170 - appendFormula 1 "x - 1 = 0";
1.1171 - val (unc, del, gen) = (([1],Res), ([1],Res), ([2],Res));
1.1172 - getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
1.1173 - (*11 elements !!!*)
1.1174 -
1.1175 - val ((pt,_),_) = get_calc 1;
1.1176 - val p = get_pos 1 1;
1.1177 - val (Form f, tac, asms) = pt_extract (pt, p);
1.1178 - if term2str f = "x - 1 = 0" andalso p = ([2], Res) then () else
1.1179 - error "FE-interface.sml: diff.behav. in FORMULA:enter} other";
1.1180 -DEconstrCalcTree 1;
1.1181 -
1.1182 -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}oth 2"; (*UC 30.3.2.4 p.175*)
1.1183 -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}oth 2";
1.1184 -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}oth 2";
1.1185 - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
1.1186 - ("Test", ["sqroot-test","univariate","equation","test"],
1.1187 - ["Test","squ-equ-test-subpbl1"]))];
1.1188 - Iterator 1;
1.1189 - moveActiveRoot 1;
1.1190 - autoCalculate 1 CompleteCalcHead;
1.1191 - autoCalculate 1 (Step 1);
1.1192 - autoCalculate 1 (Step 1);
1.1193 - appendFormula 1 "x = 1";
1.1194 - (*... returns calcChangedEvent with*)
1.1195 - val (unc, del, gen) = (([1],Res), ([1],Res), ([3,2],Res));
1.1196 - getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
1.1197 - (*6 elements !!!*)
1.1198 -
1.1199 - val ((pt,_),_) = get_calc 1;
1.1200 - val p = get_pos 1 1;
1.1201 - val (Form f, tac, asms) = pt_extract (pt, p);
1.1202 - if term2str f = "x = 1" andalso p = ([3,2], Res) then () else
1.1203 - error "FE-interface.sml: diff.behav. in FORMULA:enter} oth 2";
1.1204 -DEconstrCalcTree 1;
1.1205 -
1.1206 -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}NOTok"; (*UC 30.3.2.4 p.175*)
1.1207 -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}NOTok";
1.1208 -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}NOTok";
1.1209 - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
1.1210 - ("Test", ["sqroot-test","univariate","equation","test"],
1.1211 - ["Test","squ-equ-test-subpbl1"]))];
1.1212 - Iterator 1;
1.1213 - moveActiveRoot 1;
1.1214 - autoCalculate 1 CompleteCalcHead;
1.1215 - autoCalculate 1 (Step 1);
1.1216 - autoCalculate 1 (Step 1);
1.1217 - appendFormula 1 "x - 4711 = 0";
1.1218 - (*... returns <ERROR> no derivation found </ERROR>*)
1.1219 -
1.1220 - val ((pt,_),_) = get_calc 1;
1.1221 - val p = get_pos 1 1;
1.1222 - val (Form f, tac, asms) = pt_extract (pt, p);
1.1223 - if term2str f = "x + 1 + -1 * 2 = 0" andalso p = ([1], Res) then () else
1.1224 - error "FE-interface.sml: diff.behav. in FORMULA:enter} NOTok";
1.1225 -DEconstrCalcTree 1;
1.1226 -
1.1227 -"--------- replaceFormula {SOL:MAN:FOR:replace} right----"; (*UC 30.3.2.5 p.176*)
1.1228 -"--------- replaceFormula {SOL:MAN:FOR:replace} right----";
1.1229 -"--------- replaceFormula {SOL:MAN:FOR:replace} right----";
1.1230 -(*\label{SOLVE:MANUAL:FORMULA:replace}*)
1.1231 - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
1.1232 - ("Test", ["sqroot-test","univariate","equation","test"],
1.1233 - ["Test","squ-equ-test-subpbl1"]))];
1.1234 - Iterator 1;
1.1235 - moveActiveRoot 1;
1.1236 - autoCalculate 1 CompleteCalc;
1.1237 - moveActiveFormula 1 ([2],Res);
1.1238 - replaceFormula 1 "-1 + x = 0" (*i.e. repeats input*);
1.1239 - (*... returns <ERROR> formula not changed </ERROR>*)
1.1240 -
1.1241 - val ((pt,_),_) = get_calc 1;
1.1242 - val p = get_pos 1 1;
1.1243 - val (Form f, tac, asms) = pt_extract (pt, p);
1.1244 - if term2str f = "-1 + x = 0" andalso p = ([2], Res) then () else
1.1245 - error "FE-interface.sml: diff.behav. in FORMULA:replace} right 1";
1.1246 - if map fst (get_interval ([2],Res) ([],Res) 9999 pt) =
1.1247 - [([2], Res), ([3], Pbl), ([3, 1], Frm), ([3, 1], Res), ([3, 2], Res),
1.1248 - ([3], Res), ([4], Res), ([], Res)] then () (*nothing deleted!*) else
1.1249 - error "FE-interface.sml: diff.behav. in FORMULA:replace} right 2";
1.1250 -
1.1251 -(*WN050211 replaceFormula didn't work on second ctree: thus now tested...*)
1.1252 - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
1.1253 - ("Test", ["sqroot-test","univariate","equation","test"],
1.1254 - ["Test","squ-equ-test-subpbl1"]))];
1.1255 - Iterator 2;
1.1256 - moveActiveRoot 2;
1.1257 - autoCalculate 2 CompleteCalc;
1.1258 - moveActiveFormula 2 ([2],Res);
1.1259 - replaceFormula 2 "-1 + x = 0" (*i.e. repeats input*);
1.1260 - (*... returns <ERROR> formula not changed </ERROR>*)
1.1261 -
1.1262 - val ((pt,_),_) = get_calc 2;
1.1263 - val p = get_pos 2 1;
1.1264 - val (Form f, tac, asms) = pt_extract (pt, p);
1.1265 - if term2str f = "-1 + x = 0" andalso p = ([2], Res) then () else
1.1266 - error "FE-interface.sml: diff.behav. in FORMULA:replace} right 1";
1.1267 - if map fst (get_interval ([2],Res) ([],Res) 9999 pt) =
1.1268 - [([2], Res), ([3], Pbl), ([3, 1], Frm), ([3, 1], Res), ([3, 2], Res),
1.1269 - ([3], Res), ([4], Res), ([], Res)] then () (*nothing deleted!*) else
1.1270 - error "FE-interface.sml: diff.behav. in FORMULA:replace} right 2b";
1.1271 -DEconstrCalcTree 1;
1.1272 -
1.1273 -"--------- replaceFormula {SOL:MAN:FOR:replace} other----"; (*UC 30.3.2.5 p.176*)
1.1274 -"--------- replaceFormula {SOL:MAN:FOR:replace} other----";
1.1275 -"--------- replaceFormula {SOL:MAN:FOR:replace} other----";
1.1276 -(*\label{SOLVE:MANUAL:FORMULA:replace}*)
1.1277 - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
1.1278 - ("Test", ["sqroot-test","univariate","equation","test"],
1.1279 - ["Test","squ-equ-test-subpbl1"]))];
1.1280 - Iterator 1;
1.1281 - moveActiveRoot 1;
1.1282 - autoCalculate 1 CompleteCalc;
1.1283 - moveActiveFormula 1 ([2],Res); (*there is "-1 + x = 0"*)
1.1284 - replaceFormula 1 "x - 1 = 0"; (*<-------------------------------------*)
1.1285 - (*... returns calcChangedEvent with*)
1.1286 - val (unc, del, gen) = (([1],Res), ([4],Res), ([2],Res));
1.1287 - getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
1.1288 -
1.1289 - val ((pt,_),_) = get_calc 1;
1.1290 - show_pt pt;
1.1291 - val p = get_pos 1 1;
1.1292 - val (Form f, tac, asms) = pt_extract (pt, p);
1.1293 - if term2str f = "x - 1 = 0" andalso p = ([2], Res) then () else
1.1294 - error "FE-interface.sml: diff.behav. in FORMULA:replace} other 1";
1.1295 -(* for getting the list in whole length ...
1.1296 -print_depth 99;map fst (get_interval ([1],Res) ([],Res) 9999 pt);print_depth 3;
1.1297 - *)
1.1298 - if map fst (get_interval ([1],Res) ([],Res) 9999 pt) =
1.1299 - [([1], Res), ([2, 1], Frm), ([2, 1], Res), ([2, 2], Res), ([2, 3], Res),
1.1300 - ([2, 4], Res), ([2, 5], Res), ([2, 6], Res), ([2, 7], Res),
1.1301 - ([2, 8], Res), ([2, 9], Res), ([2], Res)
1.1302 -(*WN060727 {cutlevup->test_trans} removed: ,
1.1303 - ([], Res)(*dropped, if test_trans doesnt stop at PblNd*)*)] then () else
1.1304 - error "FE-interface.sml: diff.behav. in FORMULA:replace} other 2";
1.1305 -DEconstrCalcTree 1;
1.1306 -
1.1307 -"--------- replaceFormula {SOL:MAN:FOR:replace} other 2--"; (*UC 30.3.2.5 p.176*)
1.1308 -"--------- replaceFormula {SOL:MAN:FOR:replace} other 2--";
1.1309 -"--------- replaceFormula {SOL:MAN:FOR:replace} other 2--";
1.1310 -(*\label{SOLVE:MANUAL:FORMULA:replace}*)
1.1311 - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
1.1312 - ("Test", ["sqroot-test","univariate","equation","test"],
1.1313 - ["Test","squ-equ-test-subpbl1"]))];
1.1314 - Iterator 1;
1.1315 - moveActiveRoot 1;
1.1316 - autoCalculate 1 CompleteCalc;
1.1317 - moveActiveFormula 1 ([2],Res); (*there is "-1 + x = 0"*)
1.1318 - replaceFormula 1 "x = 1"; (*<-------------------------------------*)
1.1319 - (*... returns calcChangedEvent with ...*)
1.1320 - val (unc, del, gen) = (([1],Res), ([4],Res), ([3,2],Res));
1.1321 - getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
1.1322 - (*9 elements !!!*)
1.1323 -
1.1324 - val ((pt,_),_) = get_calc 1;
1.1325 - show_pt pt; (*error: ...get_interval drops ([3,2],Res) ...*)
1.1326 - val (t,_) = get_obj g_result pt [3,2]; term2str t;
1.1327 - if map fst (get_interval ([1],Res) ([],Res) 9999 pt) =
1.1328 - [([1], Res), ([2], Res), ([3], Pbl), ([3, 1], Frm), ([3, 1], Res),
1.1329 - ([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res),
1.1330 - ([3,2],Res)] then () else
1.1331 - error "FE-interface.sml: diff.behav. in FORMULA:replace} oth2 1";
1.1332 -
1.1333 - val p = get_pos 1 1;
1.1334 - val (Form f, tac, asms) = pt_extract (pt, p);
1.1335 - if term2str f = "x = 1" andalso p = ([3,2], Res) then () else
1.1336 - error "FE-interface.sml: diff.behav. in FORMULA:replace} oth2 2";
1.1337 -DEconstrCalcTree 1;
1.1338 -
1.1339 -"--------- replaceFormula {SOL:MAN:FOR:replace} NOTok----"; (*UC 30.3.2.5 p.176*)
1.1340 -"--------- replaceFormula {SOL:MAN:FOR:replace} NOTok----";
1.1341 -"--------- replaceFormula {SOL:MAN:FOR:replace} NOTok----";
1.1342 -(*\label{SOLVE:MANUAL:FORMULA:replace}*)
1.1343 - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
1.1344 - ("Test", ["sqroot-test","univariate","equation","test"],
1.1345 - ["Test","squ-equ-test-subpbl1"]))];
1.1346 - Iterator 1;
1.1347 - moveActiveRoot 1;
1.1348 - autoCalculate 1 CompleteCalc;
1.1349 - moveActiveFormula 1 ([2],Res); (*there is "-1 + x = 0"*)
1.1350 - replaceFormula 1 "x - 4711 = 0";
1.1351 - (*... returns <ERROR> no derivation found </ERROR>*)
1.1352 -
1.1353 - val ((pt,_),_) = get_calc 1;
1.1354 - show_pt pt;
1.1355 - val p = get_pos 1 1;
1.1356 - val (Form f, tac, asms) = pt_extract (pt, p);
1.1357 - if term2str f = "-1 + x = 0" andalso p = ([2], Res) then () else
1.1358 - error "FE-interface.sml: diff.behav. in FORMULA:replace} NOTok";
1.1359 -DEconstrCalcTree 1;
1.1360 -
1.1361 -"--------- UC errpat chain-rule-diff-both, fillpat by input ------";
1.1362 -"--------- UC errpat chain-rule-diff-both, fillpat by input ------";
1.1363 -"--------- UC errpat chain-rule-diff-both, fillpat by input ------";
1.1364 -states := [];
1.1365 -CalcTree
1.1366 -[(["functionTerm (x ^ 2 + sin (x ^ 4))", "differentiateFor x", "derivative f_f'"],
1.1367 - ("Isac", ["derivative_of","function"], ["diff","differentiate_on_R"]))];
1.1368 -Iterator 1;
1.1369 -moveActiveRoot 1;
1.1370 -autoCalculate 1 CompleteCalcHead;
1.1371 -autoCalculate 1 (Step 1);
1.1372 -autoCalculate 1 (Step 1);(*([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))*)
1.1373 -appendFormula 1 "d_d x (x ^ 2) + cos (4 * x ^ 3)"; (*<<<<<<<=========================*)
1.1374 -(* the check for errpat is maximally liberal (whole term modulo "nrls" from "type met"),
1.1375 - would recognize "cos (4 * x ^ (4 - 1)) + 2 * x" as well.
1.1376 - results in <CALCMESSAGE> error pattern #chain-rule-diff-both# </CALCMESSAGE>
1.1377 - instead of <CALCMESSAGE> no derivation found </CALCMESSAGE> *)
1.1378 - val ((pt,pos), _) = get_calc 1;
1.1379 - val p = get_pos 1 1;
1.1380 - val (Form f, _, asms) = pt_extract (pt, p);
1.1381 -
1.1382 - if p = ([1], Res) andalso term2str f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" andalso
1.1383 - get_obj g_tac pt (fst p) = Rewrite_Inst (["(bdv, x)"], ("diff_sum", "Diff.diff_sum"(*?!?*)))
1.1384 - then () else error "embed fun get_fillform changed 1";
1.1385 -
1.1386 -(*========== inhibit exn WN1130621 Isabelle2012-->13 !thehier! ====================
1.1387 -findFillpatterns 1 "chain-rule-diff-both"; (*<<<<<<<=================================*)
1.1388 -(*<CALCMESSAGE> fill patterns #fill-d_d-arg#d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) =
1.1389 - d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x ?_dummy_1#fill-both-args#...#...#... *)
1.1390 - val ((pt,pos),_) = get_calc 1;
1.1391 - val p = get_pos 1 1;
1.1392 -
1.1393 - val (Form f, _, asms) = pt_extract (pt, p);
1.1394 - if p = ([1], Res) andalso term2str f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" andalso
1.1395 - get_obj g_tac pt (fst p) = Rewrite_Inst (["(bdv, x)"], ("diff_sum", "Diff.diff_sum"(*?!?*)))
1.1396 - then ()
1.1397 - else error "embed fun get_fillform changed 2";
1.1398 -
1.1399 -(* if we assume, that the fill-patterns are ordered such that the 1st has large gaps
1.1400 - and the last has no gaps, then the number of fill-patterns would suffice
1.1401 - for the DialogGuide to select appropriately. *)
1.1402 -requestFillformula 1 ("chain-rule-diff-both", "fill-both-args");(*<<<<<<<============*)
1.1403 - (*<AUTOCALC> ([1], Res) ([2], Res) ([2], Res) </AUTOCALC>*)
1.1404 - val ((pt,pos),_) = get_calc 1;
1.1405 - val p = get_pos 1 1;
1.1406 - val (Form f, _, asms) = pt_extract (pt, p);
1.1407 - if p = ([1], Res) andalso existpt [2] pt andalso
1.1408 - term2str f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" andalso
1.1409 - get_obj g_tac pt (fst p) = Rewrite_Inst (["(bdv, x)"], ("diff_sum", "Diff.diff_sum"))
1.1410 - then () else error "embed fun get_fillform changed 3";
1.1411 -
1.1412 -inputFillFormula 1 "d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4)";(*<<<<<<<=====*)
1.1413 - val ((pt, _),_) = get_calc 1;
1.1414 - val p = get_pos 1 1;
1.1415 - val (Form f, _, asms) = pt_extract (pt, p);
1.1416 - if p = ([2], Res) andalso
1.1417 - term2str f = "d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4)" andalso
1.1418 - get_obj g_tac pt (fst p) = Rewrite_Inst (["(bdv, x)"], ("diff_sin_chain", ""))
1.1419 - then () else error "inputFillFormula changed 11";
1.1420 -
1.1421 -autoCalculate 1 CompleteCalc;
1.1422 -
1.1423 -"~~~~~ final check: the input formula is inserted as it would have been correct from beginning";
1.1424 -val ((pt, _),_) = get_calc 1;
1.1425 -val p = get_pos 1 1;
1.1426 -val (Form f, _, asms) = pt_extract (pt, p);
1.1427 -if p = ([], Res) andalso term2str f = "2 * x + cos (x ^^^ 4) * 4 * x ^^^ 3"
1.1428 -then () else error "inputFillFormula changed 12";
1.1429 -show_pt pt;
1.1430 -(*[
1.1431 -(([], Frm), Diff (x ^^^ 2 + sin (x ^^^ 4), x)),
1.1432 -(([1], Frm), d_d x (x ^^^ 2 + sin (x ^^^ 4))),
1.1433 -(([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))),
1.1434 -(([2], Res), d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4)), (*<<<<<<<=====*)
1.1435 -(([3], Res), d_d x (x ^^^ 2) + cos (x ^^^ 4) * (4 * x ^^^ (4 - 1))),
1.1436 -(([4], Res), 2 * x ^^^ (2 - 1) + cos (x ^^^ 4) * (4 * x ^^^ (4 - 1))),
1.1437 -(([5], Res), 2 * x + cos (x ^^^ 4) * 4 * x ^^^ 3),
1.1438 -(([], Res), 2 * x + cos (x ^^^ 4) * 4 * x ^^^ 3)] *)
1.1439 -============ inhibit exn WN1130621 Isabelle2012-->13 !thehier! ==================*)
1.1440 -
1.1441 -"--------- UC errpat add-fraction, fillpat by input --------------";
1.1442 -"--------- UC errpat add-fraction, fillpat by input --------------";
1.1443 -"--------- UC errpat add-fraction, fillpat by input --------------";
1.1444 -(*cp from BridgeLog Java <=> SML*)
1.1445 -states := [];
1.1446 -CalcTree [([], ("e_domID", ["e_pblID"], ["e_metID"]))];
1.1447 -Iterator 1;
1.1448 -moveActiveRoot 1;
1.1449 -moveActiveFormula 1 ([],Pbl);
1.1450 -replaceFormula 1 "Simplify (5 * x / (4 * y) + 3 * x / (4 * y))";
1.1451 -autoCalculate 1 CompleteCalcHead;
1.1452 -autoCalculate 1 (Step 1);
1.1453 -appendFormula 1 "8 * x / (8 * y)";
1.1454 -(*<CALCMESSAGE> no derivation found </CALCMESSAGE>
1.1455 ---- but in BridgeLog Java <=> SML:
1.1456 -<CALCMESSAGE> error pattern #addition-of-fractions# </CALCMESSAGE>*)
1.1457 -
1.1458 -"--------- UC errpat, fillpat step to Rewrite --------------------";
1.1459 -"--------- UC errpat, fillpat step to Rewrite --------------------";
1.1460 -"--------- UC errpat, fillpat step to Rewrite --------------------";
1.1461 -(*TODO*)
1.1462 -states:=[];
1.1463 -CalcTree
1.1464 -[(["functionTerm ((x ^ 2) ^ 3 + sin (x ^ 4))",
1.1465 - "differentiateFor x", "derivative f_f'"],
1.1466 - ("Isac", ["derivative_of","function"],
1.1467 - ["diff","differentiate_on_R"]))]; (*<<<======= EP is directly in script*)
1.1468 -Iterator 1;
1.1469 -moveActiveRoot 1;
1.1470 -autoCalculate 1 CompleteCalc;
1.1471 -val ((pt,p),_) = get_calc 1; show_pt pt;
1.1472 -
1.1473 -"--------- UC errpat, fillpat step to Rewrite_Set ----------------";
1.1474 -"--------- UC errpat, fillpat step to Rewrite_Set ----------------";
1.1475 -"--------- UC errpat, fillpat step to Rewrite_Set ----------------";
1.1476 -states:=[];
1.1477 -CalcTree
1.1478 -[(["functionTerm ((x ^ 2) ^ 3 + sin (x ^ 4))",
1.1479 - "differentiateFor x", "derivative f_f'"],
1.1480 - ("Isac", ["derivative_of","function"],
1.1481 - ["diff","after_simplification"]))]; (*<<<======= EP is in a ruleset*)
1.1482 -Iterator 1;
1.1483 -moveActiveRoot 1;
1.1484 -autoCalculate 1 CompleteCalcHead;
1.1485 -autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.1486 -autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.1487 -(*
1.1488 -<NEXTTAC>
1.1489 - <CALCID> 1 </CALCID>
1.1490 - <TACTICERRORPATTERNS>
1.1491 - <STRINGLIST>
1.1492 - <STRING> chain-rule-diff-both </STRING>
1.1493 - <STRING> cancel </STRING>
1.1494 - </STRINGLIST>
1.1495 - <REWRITESETINSTTACTIC name="Rewrite_Set_Inst">
1.1496 - <RULESET> norm_diff </RULESET>
1.1497 - <SUBSTITUTION>
1.1498 - <PAIR>
1.1499 - <VARIABLE>
1.1500 - <MATHML>
1.1501 - <ISA> bdv </ISA>
1.1502 - </MATHML>
1.1503 - </VARIABLE>
1.1504 - <VALUE>
1.1505 - <MATHML>
1.1506 - <ISA> x </ISA>
1.1507 - </MATHML>
1.1508 - </VALUE>
1.1509 - </PAIR>
1.1510 - </SUBSTITUTION>
1.1511 - </REWRITESETINSTTACTIC>
1.1512 - </TACTICERRORPATTERNS>
1.1513 -</NEXTTAC>
1.1514 -
1.1515 -
1.1516 -(*WN1208 postponed due to efforts required for stepToErrorPatterns (NEW rewrite_set_)*)
1.1517 -stepToErrorPatterns 1; (*--> calcChanged, rule immediately calls... *)
1.1518 -stepOnErrorPatterns 1; (*--> calcChanged, rule calls getTactic and displays it *)
1.1519 -(* then --- UC errpat, fillpat by input ---*)
1.1520 -*)
1.1521 -autoCalculate 1 CompleteCalc;
1.1522 -val ((pt,p),_) = get_calc 1; show_pt pt;
1.1523 -(*WN1208 postponed due to efforts required for stepToErrorPatterns (NEW rewrite_set_)*)
1.1524 -
2.1 --- a/test/Tools/isac/Test_Isac.thy Tue Sep 17 18:00:59 2013 +0200
2.2 +++ b/test/Tools/isac/Test_Isac.thy Tue Sep 17 18:59:56 2013 +0200
2.3 @@ -97,6 +97,7 @@
2.4 ML_file "Frontend/messages.sml"
2.5 ML_file "Frontend/states.sml"
2.6 ML_file "Frontend/interface.sml"
2.7 + ML_file "Frontend/use-cases.sml"
2.8 (*WITHOUT inhibit exn WN1130621 Isabelle2012-->13 !thehier! THIS ERROR OCCURS:
2.9 ... SAME ERROR HERE ON ISABELLE2012 AS IN ISAC ON ISABELLE2011*)
2.10 ML_file "print_exn_G.sml"