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