1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/test/Tools/isac/Frontend/interface.sml Mon Aug 30 14:35:51 2010 +0200
1.3 @@ -0,0 +1,1349 @@
1.4 +(* tests the interface of isac's SML-kernel in accordance to
1.5 + java-tests/isac.bridge.
1.6 +
1.7 +WN050707 ... if true, the test ist marked with a \label referring
1.8 +to the same UC in isac-docu.tex as the JUnit testcase.
1.9 +use"../smltest/FE-interface/interface.sml";
1.10 +use"interface.sml";
1.11 + *)
1.12 +
1.13 + print_depth 3;
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 +"--------- miniscript with mini-subpbl AUTOCALCULATE Step 1-------";
1.29 +"--------- solve_linear as rootpbl AUTOCALCULATE CompleteCalc ----";
1.30 +"--------- solve_linear as rootpbl AUTOCALC CompleteHead/Calc ----";
1.31 +"--------- miniscript with mini-subpbl AUTOCALCULATE CompleteCalc-";
1.32 +"--------- miniscript with mini-subpbl AUTO CompleteCalcHead------";
1.33 +"--------- solve_linear as rootpbl AUTOCALCULATE CompleteModel ---";
1.34 +"--------- setContext..Thy ---------------------------------------";
1.35 +"--------- miniscript with mini-subpbl AUTOCALC CompleteToSubpbl -";
1.36 +"---------------- rat-eq + subpbl: no_met, NO solution dropped ---";
1.37 +"--------- tryMatchProblem, tryRefineProblem -------------------UC";
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 +"--------- appendFormula label{SOLVE:MANUAL:FORMULA:enter} right--";
1.47 +"--------- appendFormula label{SOLVE:MANUAL:FORMULA:enter} other--";
1.48 +"--------- appendFormula label{SOLVE:MANUAL:FORMULA:enter} oth 2--";
1.49 +"--------- appendFormula label{SOLVE:MANUAL:FORMULA:enter} NOTok--";
1.50 +"--------- replaceFormula {SOLVE:MANUAL:FORMULA:replace} right----";
1.51 +"--------- replaceFormula {SOLVE:MANUAL:FORMULA:replace} other----";
1.52 +"--------- replaceFormula {SOLVE:MANUAL:FORMULA:replace} other 2--";
1.53 +"--------- replaceFormula {SOLVE:MANUAL:FORMULA:replace} NOTok----";
1.54 +"-----------------------------------------------------------------";
1.55 +
1.56 +"within struct ---------------------------------------------------";
1.57 +"within struct ---------------------------------------------------";
1.58 +"within struct ---------------------------------------------------";
1.59 +(*==================================================================
1.60 +
1.61 +
1.62 +"--------- encode ^ -> ^^^ ---------------------------------------";
1.63 +"--------- encode ^ -> ^^^ ---------------------------------------";
1.64 +"--------- encode ^ -> ^^^ ---------------------------------------";
1.65 +if encode "a^2+b^2=c^2" = "a^^^2+b^^^2=c^^^2" then ()
1.66 +else raise error "interface.sml: diff.behav. in encode ^ -> ^^^ ";
1.67 +
1.68 +if (decode o encode) "a^2+b^2=c^2" = "a^2+b^2=c^2" then ()
1.69 +else raise error "interface.sml: diff.behav. in de/encode ^ <-> ^^^ ";
1.70 +
1.71 +==================================================================*)
1.72 +"exported from struct --------------------------------------------";
1.73 +"exported from struct --------------------------------------------";
1.74 +"exported from struct --------------------------------------------";
1.75 +
1.76 +
1.77 +(*------------ set at startup of the Kernel --------------------------*)
1.78 + states:= []; (*resets all state information in Kernel *)
1.79 +(*----------------------------------------------------------------*)
1.80 +
1.81 +"---------------- empty rootpbl ----------------------------------";
1.82 +"---------------- empty rootpbl ----------------------------------";
1.83 +"---------------- empty rootpbl ----------------------------------";
1.84 + CalcTree [([], ("", [], []))];
1.85 + Iterator 1;
1.86 + moveActiveRoot 1;
1.87 + refFormula 1 (get_pos 1 1);
1.88 +(*WN.040222: stoert das sehr, dass e_domID etc. statt leer kommt ???*)
1.89 +
1.90 +
1.91 +"---------------- solve_linear as rootpbl FE ---------------------";
1.92 +"---------------- solve_linear as rootpbl FE ---------------------";
1.93 +"---------------- solve_linear as rootpbl FE ---------------------";
1.94 + states := [];
1.95 + CalcTree (*start of calculation, return No.1*)
1.96 + [(["equality (1+-1*2+x=0)", "solveFor x","solutions L"],
1.97 + ("Test.thy",
1.98 + ["linear","univariate","equation","test"],
1.99 + ["Test","solve_linear"]))];
1.100 + Iterator 1; (*create an active Iterator on CalcTree No.1*)
1.101 +
1.102 + moveActiveRoot 1;(*sets the CalcIterator No.1 at the root of CalcTree No.1*);
1.103 + refFormula 1 (get_pos 1 1) (*gets CalcHead; model is still empty*);
1.104 +
1.105 + fetchProposedTactic 1 (*by using Iterator No.1*);
1.106 + setNextTactic 1 (Model_Problem (*["linear","univariate","equation","test"]*));
1.107 + (*by using Iterator No.1*)
1.108 + autoCalculate 1 (Step 1);
1.109 + refFormula 1 (get_pos 1 1) (*model contains descriptions for all items*);
1.110 + autoCalculate 1 (Step 1);
1.111 +(*-----since Model_Problem + complete_mod_ in case cas of SOME-----*
1.112 + fetchProposedTactic 1;
1.113 + setNextTactic 1 (Add_Given "equality (1 + -1 * 2 + x = 0)");
1.114 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); (*equality added*);
1.115 +
1.116 + fetchProposedTactic 1;
1.117 + setNextTactic 1 (Add_Given "solveFor x");
1.118 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.119 +
1.120 + fetchProposedTactic 1;
1.121 + setNextTactic 1 (Add_Find "solutions L");
1.122 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.123 +
1.124 + fetchProposedTactic 1;
1.125 + setNextTactic 1 (Specify_Theory "Test.thy");
1.126 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.127 +*-----since Model_Problem + complete_mod_ in case cas of SOME-----*)
1.128 +
1.129 + fetchProposedTactic 1;
1.130 + setNextTactic 1 (Specify_Problem ["linear","univariate","equation","test"]);
1.131 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.132 +(*-------------------------------------------------------------------------*)
1.133 + fetchProposedTactic 1;
1.134 + val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;
1.135 +
1.136 + setNextTactic 1 (Specify_Method ["Test","solve_linear"]);
1.137 + val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;
1.138 +
1.139 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.140 + val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;
1.141 +
1.142 +(*-------------------------------------------------------------------------*)
1.143 + fetchProposedTactic 1;
1.144 + val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;
1.145 +
1.146 + setNextTactic 1 (Apply_Method ["Test","solve_linear"]);
1.147 + val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;
1.148 + is_complete_mod ptp;
1.149 + is_complete_spec ptp;
1.150 +
1.151 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.152 + val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;
1.153 + (*term2str (get_obj g_form pt [1]);*)
1.154 +(*-------------------------------------------------------------------------*)
1.155 +
1.156 + fetchProposedTactic 1;
1.157 + setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "isolate_bdv"));
1.158 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.159 +
1.160 + fetchProposedTactic 1;
1.161 + setNextTactic 1 (Rewrite_Set "Test_simplify");
1.162 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.163 +
1.164 + fetchProposedTactic 1;
1.165 + setNextTactic 1 (Check_Postcond ["linear","univariate","equation","test"]);
1.166 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.167 +
1.168 + val ((pt,_),_) = get_calc 1;
1.169 + val ip = get_pos 1 1;
1.170 + val (Form f, tac, asms) = pt_extract (pt, ip);
1.171 + (*exception just above means: 'ModSpec' has been returned: error anyway*)
1.172 + if term2str f = "[x = 1]" then () else
1.173 + raise error "FE-Kernel-interface.sml: diff.behav. in solve_linear as rootpbl";
1.174 +
1.175 +
1.176 +
1.177 +"--------- inspect the CalcTree No.1 with Iterator No.2 ---------";
1.178 +"--------- inspect the CalcTree No.1 with Iterator No.2 ---------";
1.179 +"--------- inspect the CalcTree No.1 with Iterator No.2 ---------";
1.180 +(*WN041118: inspection shifted to Iterator No.1, because others need pos'*)
1.181 + moveActiveRoot 1;
1.182 + refFormula 1 ([],Pbl); getTactic 1 ([],Pbl);(*Error*)
1.183 + moveActiveDown 1;
1.184 + refFormula 1 ([1],Frm); getTactic 1 ([1],Frm);(*Error*)
1.185 + moveActiveDown 1 ;
1.186 + refFormula 1 ([1],Res); getTactic 1 ([1],Res);(*OK*)
1.187 + (*getAssumption 1 ([1],Res); TODO.WN041217*)
1.188 + moveActiveDown 1 ; refFormula 1 ([2],Res);
1.189 + moveActiveCalcHead 1; refFormula 1 ([],Pbl);
1.190 + moveActiveDown 1;
1.191 + moveActiveDown 1;
1.192 + moveActiveDown 1;
1.193 + if get_pos 1 1 = ([2], Res) then () else
1.194 + raise error "FE-interface.sml: diff.behav. in a inspect 1 with Iterator 2";
1.195 + moveActiveDown 1; refFormula 1 ([], Res);
1.196 + if get_pos 1 1 = ([], Res) then () else
1.197 + raise error "FE-interface.sml: diff.behav. in b inspect 1 with Iterator 2";
1.198 + moveActiveCalcHead 1; refFormula 1 ([],Pbl);
1.199 +
1.200 +
1.201 +
1.202 +"---------------- miniscript with mini-subpbl --------------------";
1.203 +"---------------- miniscript with mini-subpbl --------------------";
1.204 +"---------------- miniscript with mini-subpbl --------------------";
1.205 + states:=[];
1.206 + CalcTree (*start of calculation, return No.1*)
1.207 + [(["equality (x+1=2)", "solveFor x","solutions L"],
1.208 + ("Test.thy",
1.209 + ["sqroot-test","univariate","equation","test"],
1.210 + ["Test","squ-equ-test-subpbl1"]))];
1.211 + Iterator 1;
1.212 +
1.213 + moveActiveRoot 1;
1.214 + refFormula 1 (get_pos 1 1);
1.215 + fetchProposedTactic 1;
1.216 + setNextTactic 1 (Model_Problem);
1.217 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*gets ModSpec;model is still empty*)
1.218 +
1.219 + fetchProposedTactic 1;
1.220 + setNextTactic 1 (Add_Given "equality (x + 1 = 2)");
1.221 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.222 +
1.223 + fetchProposedTactic 1;
1.224 + setNextTactic 1 (Add_Given "solveFor x");
1.225 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.226 +
1.227 + fetchProposedTactic 1;
1.228 + setNextTactic 1 (Add_Find "solutions L");
1.229 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.230 +
1.231 + fetchProposedTactic 1;
1.232 + setNextTactic 1 (Specify_Theory "Test.thy");
1.233 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.234 +
1.235 + fetchProposedTactic 1;
1.236 + setNextTactic 1 (Specify_Problem
1.237 + ["sqroot-test","univariate","equation","test"]);
1.238 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.239 +"1-----------------------------------------------------------------";
1.240 +
1.241 + fetchProposedTactic 1;
1.242 + setNextTactic 1 (Specify_Method ["Test","squ-equ-test-subpbl1"]);
1.243 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.244 +
1.245 + fetchProposedTactic 1;
1.246 + setNextTactic 1 (Apply_Method ["Test","squ-equ-test-subpbl1"]);
1.247 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.248 +
1.249 + fetchProposedTactic 1;
1.250 + setNextTactic 1 (Rewrite_Set "norm_equation");
1.251 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.252 +
1.253 + fetchProposedTactic 1;
1.254 + setNextTactic 1 (Rewrite_Set "Test_simplify");
1.255 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.256 +
1.257 + fetchProposedTactic 1;(*----------------Subproblem--------------------*);
1.258 + setNextTactic 1 (Subproblem ("Test.thy",
1.259 + ["linear","univariate","equation","test"]));
1.260 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.261 +
1.262 + fetchProposedTactic 1;
1.263 + setNextTactic 1 (Model_Problem );
1.264 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.265 +
1.266 + fetchProposedTactic 1;
1.267 + setNextTactic 1 (Add_Given "equality (-1 + x = 0)");
1.268 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.269 +
1.270 + fetchProposedTactic 1;
1.271 + setNextTactic 1 (Add_Given "solveFor x");
1.272 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.273 +
1.274 + fetchProposedTactic 1;
1.275 + setNextTactic 1 (Add_Find "solutions x_i");
1.276 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.277 +
1.278 + fetchProposedTactic 1;
1.279 + setNextTactic 1 (Specify_Theory "Test.thy");
1.280 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.281 +
1.282 + fetchProposedTactic 1;
1.283 + setNextTactic 1 (Specify_Problem ["linear","univariate","equation","test"]);
1.284 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.285 +"2-----------------------------------------------------------------";
1.286 +
1.287 + fetchProposedTactic 1;
1.288 + setNextTactic 1 (Specify_Method ["Test","solve_linear"]);
1.289 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.290 +
1.291 + fetchProposedTactic 1;
1.292 + setNextTactic 1 (Apply_Method ["Test","solve_linear"]);
1.293 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.294 +
1.295 + fetchProposedTactic 1;
1.296 + setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "isolate_bdv"));
1.297 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.298 +
1.299 + fetchProposedTactic 1;
1.300 + setNextTactic 1 (Rewrite_Set "Test_simplify");
1.301 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.302 +
1.303 + fetchProposedTactic 1;
1.304 + setNextTactic 1 (Check_Postcond ["linear","univariate","equation","test"]);
1.305 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.306 +
1.307 + fetchProposedTactic 1;
1.308 + setNextTactic 1 (Check_elementwise "Assumptions");
1.309 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.310 +
1.311 + val xml = fetchProposedTactic 1;
1.312 + setNextTactic 1 (Check_Postcond
1.313 + ["sqroot-test","univariate","equation","test"]);
1.314 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.315 +
1.316 + val ((pt,_),_) = get_calc 1;
1.317 + val str = pr_ptree pr_short pt;
1.318 + writeln str;
1.319 + val ip = get_pos 1 1;
1.320 + val (Form f, tac, asms) = pt_extract (pt, ip);
1.321 + (*exception just above means: 'ModSpec' has been returned: error anyway*)
1.322 + if term2str f = "[x = 1]" then () else
1.323 + raise error "FE-interface.sml: diff.behav. in miniscript with mini-subpb";
1.324 +
1.325 + DEconstrCalcTree 1;
1.326 +
1.327 +
1.328 +"--------- miniscript with mini-subpbl AUTOCALCULATE Step 1-------";
1.329 +"--------- miniscript with mini-subpbl AUTOCALCULATE Step 1-------";
1.330 +"--------- miniscript with mini-subpbl AUTOCALCULATE Step 1-------";
1.331 + states:=[];
1.332 + CalcTree
1.333 + [(["equality (x+1=2)", "solveFor x","solutions L"],
1.334 + ("Test.thy",
1.335 + ["sqroot-test","univariate","equation","test"],
1.336 + ["Test","squ-equ-test-subpbl1"]))];
1.337 + Iterator 1;
1.338 + moveActiveRoot 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 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
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 + (*here the solve-phase starts*)
1.348 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 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 + (*------------------------------------*)
1.352 +(* print_depth 13; get_calc 1;
1.353 + *)
1.354 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.355 + (*calc-head of subproblem*)
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 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
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 + (*solve-phase of the subproblem*)
1.364 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.365 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
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 + (*finish subproblem*)
1.369 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.370 + (*finish problem*)
1.371 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.372 +
1.373 + (*this checks the test for correctness..*)
1.374 + val ((pt,_),_) = get_calc 1;
1.375 + val p = get_pos 1 1;
1.376 + val (Form f, tac, asms) = pt_extract (pt, p);
1.377 + if term2str f = "[x = 1]" andalso p = ([], Res) then () else
1.378 + raise error "FE-interface.sml: diff.behav. in miniscript with mini-subpb";
1.379 +
1.380 + DEconstrCalcTree 1;
1.381 +
1.382 +"--------- solve_linear as rootpbl AUTOCALCULATE CompleteCalc ----";
1.383 +"--------- solve_linear as rootpbl AUTOCALCULATE CompleteCalc ----";
1.384 +"--------- solve_linear as rootpbl AUTOCALCULATE CompleteCalc ----";
1.385 + states:=[];
1.386 + CalcTree
1.387 + [(["equality (1+-1*2+x=0)", "solveFor x","solutions L"],
1.388 + ("Test.thy",
1.389 + ["linear","univariate","equation","test"],
1.390 + ["Test","solve_linear"]))];
1.391 + Iterator 1;
1.392 + moveActiveRoot 1;
1.393 +getFormulaeFromTo 1 ([],Pbl) ([],Pbl) 999 false;
1.394 +
1.395 + autoCalculate 1 CompleteCalc;
1.396 + val (unc, del, gen) = (([],Pbl), ([],Pbl), ([],Res));
1.397 + getFormulaeFromTo 1 unc gen 1 (*only level 1*) false;
1.398 +
1.399 + val ((pt,_),_) = get_calc 1;
1.400 + val p = get_pos 1 1;
1.401 + val (Form f, tac, asms) = pt_extract (pt, p);
1.402 + if term2str f = "[x = 1]" andalso p = ([], Res) then () else
1.403 + raise error "FE-interface.sml: diff.behav. in solve_linear/rt AUTOCALCULATE ";
1.404 +
1.405 +
1.406 +"--------- solve_linear as rootpbl AUTOCALC CompleteHead/Calc ----";
1.407 +"--------- solve_linear as rootpbl AUTOCALC CompleteHead/Calc ----";
1.408 +"--------- solve_linear as rootpbl AUTOCALC CompleteHead/Calc ----";
1.409 + states:=[];
1.410 + CalcTree
1.411 + [(["equality (1+-1*2+x=0)", "solveFor x","solutions L"],
1.412 + ("Test.thy",
1.413 + ["linear","univariate","equation","test"],
1.414 + ["Test","solve_linear"]))];
1.415 + Iterator 1;
1.416 + moveActiveRoot 1;
1.417 + autoCalculate 1 CompleteCalcHead;
1.418 + refFormula 1 (get_pos 1 1);
1.419 + val ((pt,p),_) = get_calc 1;
1.420 +
1.421 +
1.422 +
1.423 + autoCalculate 1 CompleteCalc;
1.424 + val ((pt,p),_) = get_calc 1;
1.425 + if p=([], Res) then () else
1.426 + raise error "FE-interface.sml: diff.behav. in solve_linear AUTOC Head/Calc ";
1.427 +
1.428 +
1.429 +"--------- miniscript with mini-subpbl AUTOCALCULATE CompleteCalc-";
1.430 +"--------- miniscript with mini-subpbl AUTOCALCULATE CompleteCalc-";
1.431 +"--------- miniscript with mini-subpbl AUTOCALCULATE CompleteCalc-";
1.432 + states:=[];
1.433 + CalcTree
1.434 + [(["equality (x+1=2)", "solveFor x","solutions L"],
1.435 + ("Test.thy",
1.436 + ["sqroot-test","univariate","equation","test"],
1.437 + ["Test","squ-equ-test-subpbl1"]))];
1.438 + Iterator 1;
1.439 + moveActiveRoot 1;
1.440 + autoCalculate 1 CompleteCalc;
1.441 +
1.442 +(*
1.443 +getTactic 1 ([1],Frm);
1.444 +getTactic 1 ([1],Res);
1.445 +initContext 1 Thy_ ([1],Res);
1.446 +*)
1.447 +
1.448 + (*... returns calcChangedEvent with*)
1.449 + val (unc, del, gen) = (([],Pbl), ([],Pbl), ([],Res));
1.450 + getFormulaeFromTo 1 unc gen 0 (*only result*) false;
1.451 + getFormulaeFromTo 1 unc gen 1 (*only level 1*) false;
1.452 + getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
1.453 +
1.454 + val ((pt,_),_) = get_calc 1;
1.455 + val p = get_pos 1 1;
1.456 + val (Form f, tac, asms) = pt_extract (pt, p);
1.457 + if term2str f = "[x = 1]" andalso p = ([], Res) then () else
1.458 + raise error "FE-interface.sml: diff.behav. in mini-subpbl AUTOCALCULATE 6";
1.459 +
1.460 +
1.461 +"--------- miniscript with mini-subpbl AUTO CompleteCalcHead------";
1.462 +"--------- miniscript with mini-subpbl AUTO CompleteCalcHead------";
1.463 +"--------- miniscript with mini-subpbl AUTO CompleteCalcHead------";
1.464 + states:=[];
1.465 + CalcTree
1.466 + [(["equality (x+1=2)", "solveFor x","solutions L"],
1.467 + ("Test.thy",
1.468 + ["sqroot-test","univariate","equation","test"],
1.469 + ["Test","squ-equ-test-subpbl1"]))];
1.470 + Iterator 1;
1.471 +(* doesn't terminate !!!
1.472 + autoCalculate 1 CompleteCalcHead;
1.473 +*)
1.474 +
1.475 +"--------- solve_linear as rootpbl AUTOCALCULATE CompleteModel ---";
1.476 +"--------- solve_linear as rootpbl AUTOCALCULATE CompleteModel ---";
1.477 +"--------- solve_linear as rootpbl AUTOCALCULATE CompleteModel ---";
1.478 + states:=[];
1.479 + CalcTree
1.480 + [(["equality (1+-1*2+x=0)", "solveFor x","solutions L"],
1.481 + ("Test.thy",
1.482 + ["linear","univariate","equation","test"],
1.483 + ["Test","solve_linear"]))];
1.484 + Iterator 1;
1.485 + moveActiveRoot 1;
1.486 + autoCalculate 1 CompleteModel;
1.487 + refFormula 1 (get_pos 1 1);
1.488 +
1.489 +setProblem 1 ["linear","univariate","equation","test"];
1.490 +val pos = get_pos 1 1;
1.491 +setContext 1 pos (kestoreID2guh Pbl_["linear","univariate","equation","test"]);
1.492 + refFormula 1 (get_pos 1 1);
1.493 +
1.494 +setMethod 1 ["Test","solve_linear"];
1.495 +setContext 1 pos (kestoreID2guh Met_ ["Test","solve_linear"]);
1.496 + refFormula 1 (get_pos 1 1);
1.497 + val ((pt,_),_) = get_calc 1;
1.498 + if get_obj g_spec pt [] = ("e_domID",
1.499 + ["linear", "univariate","equation","test"],
1.500 + ["Test","solve_linear"]) then ()
1.501 + else raise error "FE-interface.sml: diff.behav. in setProblem, setMethod";
1.502 +
1.503 + autoCalculate 1 CompleteCalcHead;
1.504 + refFormula 1 (get_pos 1 1);
1.505 + autoCalculate 1 CompleteCalc;
1.506 + moveActiveDown 1;
1.507 + moveActiveDown 1;
1.508 + moveActiveDown 1;
1.509 + refFormula 1 (get_pos 1 1);
1.510 + val ((pt,_),_) = get_calc 1;
1.511 + val p = get_pos 1 1;
1.512 + val (Form f, tac, asms) = pt_extract (pt, p);
1.513 + if term2str f = "[x = 1]" andalso p = ([], Res) then () else
1.514 + raise error "FE-interface.sml: diff.behav. in mini-subpbl AUTOCALCULATE 6";
1.515 +
1.516 +
1.517 +"--------- setContext..Thy ---------------------------------------";
1.518 +"--------- setContext..Thy ---------------------------------------";
1.519 +"--------- setContext..Thy ---------------------------------------";
1.520 +states:=[];
1.521 +CalcTree
1.522 +[(["equality (x+1=2)", "solveFor x","solutions L"],
1.523 + ("Test.thy",
1.524 + ["sqroot-test","univariate","equation","test"],
1.525 + ["Test","squ-equ-test-subpbl1"]))];
1.526 +Iterator 1; moveActiveRoot 1;
1.527 +autoCalculate 1 CompleteCalcHead;
1.528 +autoCalculate 1 (Step 1);
1.529 +val ((pt,p),_) = get_calc 1; show_pt pt;
1.530 +(*
1.531 +setNextTactic 1 (Rewrite_Set "Test_simplify");
1.532 +autoCalculate 1 (Step 1);
1.533 +val ((pt,p),_) = get_calc 1; show_pt pt;
1.534 +*)
1.535 +"-----^^^^^ and vvvvv do the same -----";
1.536 +setContext 1 p "thy_isac_Test-rls-Test_simplify";
1.537 +val ((pt,p),_) = get_calc 1; show_pt pt;
1.538 +
1.539 +autoCalculate 1 (Step 1);
1.540 +setContext 1 p "thy_isac_Test-rls-Test_simplify";
1.541 +val ((pt,p),_) = get_calc 1; show_pt pt;
1.542 +
1.543 +autoCalculate 1 CompleteCalc;
1.544 +
1.545 +
1.546 +
1.547 +"--------- miniscript with mini-subpbl AUTOCALC CompleteToSubpbl -";
1.548 +"--------- miniscript with mini-subpbl AUTOCALC CompleteToSubpbl -";
1.549 +"--------- miniscript with mini-subpbl AUTOCALC CompleteToSubpbl -";
1.550 + states:=[];
1.551 + CalcTree
1.552 + [(["equality (x+1=2)", "solveFor x","solutions L"],
1.553 + ("Test.thy",
1.554 + ["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 + raise 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 + val (Form f, tac, asms) = pt_extract (pt, p);
1.575 + if term2str f = "[x = 1]" andalso p = ([], Res) then () else
1.576 + raise error "FE-interface.sml: diff.behav. in mini-subpbl CompleteToSubpbl 1";
1.577 +
1.578 +
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 + states:=[];
1.584 + CalcTree
1.585 + [(["equality ((5*x)/(x - 2) - x/(x+2)=4)", "solveFor x","solutions L"],
1.586 + ("RatEq.thy", ["univariate","equation"], ["no_met"]))];
1.587 + Iterator 1;
1.588 + moveActiveRoot 1;
1.589 + fetchProposedTactic 1;
1.590 + setNextTactic 1 (Model_Problem );
1.591 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.592 +(*-----since Model_Problem + complete_mod_ in case cas of SOME-----*
1.593 + setNextTactic 1 (Add_Given "equality (5 * x / (x - 2) - x / (x + 2) = 4)");
1.594 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.595 + setNextTactic 1 (Add_Given "solveFor x");
1.596 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.597 + setNextTactic 1 (Add_Find "solutions L");
1.598 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.599 +*-----since Model_Problem + complete_mod_ in case cas of SOME-----*)
1.600 + setNextTactic 1 (Specify_Theory "RatEq.thy");
1.601 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.602 + setNextTactic 1 (Specify_Problem ["rational","univariate","equation"]);
1.603 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.604 + setNextTactic 1 (Specify_Method ["RatEq","solve_rat_equation"]);
1.605 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.606 + setNextTactic 1 (Apply_Method ["RatEq","solve_rat_equation"]);
1.607 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.608 + setNextTactic 1 (Rewrite_Set "RatEq_simplify");
1.609 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.610 + setNextTactic 1 (Rewrite_Set "norm_Rational");
1.611 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.612 + setNextTactic 1 (Rewrite_Set "RatEq_eliminate");
1.613 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.614 + (* __________ for "12 * x + 4 * x ^^^ 2 = 4 * (-4 + x ^^^ 2)"*)
1.615 + setNextTactic 1 (Subproblem ("PolyEq.thy", ["normalize","polynomial",
1.616 + "univariate","equation"]));
1.617 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.618 + setNextTactic 1 (Model_Problem );
1.619 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.620 +(*-----since Model_Problem + complete_mod_ in case cas of SOME-----*
1.621 + setNextTactic 1 (Add_Given
1.622 + "equality (12 * x + 4 * x ^^^ 2 = 4 * (-4 + x ^^^ 2))");
1.623 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.624 + setNextTactic 1 (Add_Given "solveFor x");
1.625 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.626 + setNextTactic 1 (Add_Find "solutions x_i");
1.627 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.628 +*-----since Model_Problem + complete_mod_ in case cas of SOME-----*)
1.629 + setNextTactic 1 (Specify_Theory "PolyEq.thy");
1.630 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.631 + setNextTactic 1 (Specify_Problem ["normalize","polynomial",
1.632 + "univariate","equation"]);
1.633 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.634 + setNextTactic 1 (Specify_Method ["PolyEq","normalize_poly"]);
1.635 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.636 + setNextTactic 1 (Apply_Method ["PolyEq","normalize_poly"]);
1.637 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.638 + setNextTactic 1 (Rewrite ("all_left",""));
1.639 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.640 + setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "make_ratpoly_in"));
1.641 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.642 + (* __________ for "16 + 12 * x = 0"*)
1.643 + setNextTactic 1 (Subproblem ("PolyEq.thy",
1.644 + ["degree_1","polynomial","univariate","equation"]));
1.645 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.646 + setNextTactic 1 (Model_Problem );
1.647 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.648 +(*-----since Model_Problem + complete_mod_ in case cas of SOME-----*
1.649 + setNextTactic 1 (Add_Given
1.650 + "equality (16 + 12 * x = 0)");
1.651 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.652 + setNextTactic 1 (Add_Given "solveFor x");
1.653 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.654 + setNextTactic 1 (Add_Find "solutions x_i");
1.655 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.656 +*-----since Model_Problem + complete_mod_ in case cas of SOME-----*)
1.657 + setNextTactic 1 (Specify_Theory "PolyEq.thy");
1.658 + (*------------- some trials in the problem-hierarchy ---------------*)
1.659 + setNextTactic 1 (Specify_Problem ["linear","univariate","equation"]);
1.660 + autoCalculate 1 (Step 1); fetchProposedTactic 1; (*<ERROR> helpless </ERROR> !!!*)
1.661 + setNextTactic 1 (Refine_Problem ["univariate","equation"]);
1.662 +
1.663 +
1.664 +
1.665 +
1.666 +
1.667 + (*------------------------------------------------------------------*)
1.668 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.669 + setNextTactic 1 (Specify_Method ["PolyEq","solve_d1_polyeq_equation"]);
1.670 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.671 + setNextTactic 1 (Apply_Method ["PolyEq","solve_d1_polyeq_equation"]);
1.672 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.673 + setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "d1_polyeq_simplify"));
1.674 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.675 + setNextTactic 1 (Rewrite_Set "polyeq_simplify");
1.676 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.677 + (*==================================================================*)
1.678 + setNextTactic 1 Or_to_List;
1.679 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.680 + setNextTactic 1 (Check_elementwise "Assumptions");
1.681 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.682 + setNextTactic 1 (Check_Postcond ["degree_1","polynomial",
1.683 + "univariate","equation"]);
1.684 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.685 + setNextTactic 1 (Check_Postcond ["normalize","polynomial",
1.686 + "univariate","equation"]);
1.687 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.688 + setNextTactic 1 (Check_elementwise "Assumptions");
1.689 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.690 + setNextTactic 1 (Check_Postcond ["rational","univariate","equation"]);
1.691 + val (ptp,_) = get_calc 1;
1.692 + val (Form t,_,_) = pt_extract ptp;
1.693 + if get_pos 1 1 = ([], Res) andalso term2str t = "[x = -4 / 3]" then ()
1.694 + else writeln "FE-inteface.sml: diff.behav. in rat-eq + subpbl: no_met, NO ..";
1.695 +
1.696 +
1.697 +"---------------- tryMatchProblem, tryRefineProblem --------------";
1.698 +"---------------- tryMatchProblem, tryRefineProblem --------------";
1.699 +"---------------- tryMatchProblem, tryRefineProblem --------------";
1.700 +(*{\bf\UC{Having \isac{} Refine the Problem
1.701 + * Automatically}\label{SPECIFY:refine-auto}\\} test match and refine with
1.702 + * x^^^2 + 4*x + 5 = 2
1.703 +see isac.bridge.TestSpecify#testMatchRefine*)
1.704 + DEconstrCalcTree 1;
1.705 + CalcTree
1.706 + [(["equality (x^2 + 4*x + 5 = 2)", "solveFor x","solutions L"],
1.707 + ("Isac.thy",
1.708 + ["univariate","equation"],
1.709 + ["no_met"]))];
1.710 + Iterator 1;
1.711 + moveActiveRoot 1;
1.712 +
1.713 + fetchProposedTactic 1;
1.714 + setNextTactic 1 (Model_Problem );
1.715 + (*..this tactic should be done 'tacitly', too !*)
1.716 +
1.717 +(*
1.718 +autoCalculate 1 CompleteCalcHead;
1.719 +checkContext 1 ([],Pbl) "pbl_equ_univ";
1.720 +checkContext 1 ([],Pbl) (kestoreID2guh Pbl_ ["univariate","equation"]);
1.721 +*)
1.722 +
1.723 + autoCalculate 1 (Step 1);
1.724 +
1.725 + fetchProposedTactic 1;
1.726 + setNextTactic 1 (Add_Given "equality (x ^^^ 2 + 4 * x + 5 = 2)");
1.727 + autoCalculate 1 (Step 1);
1.728 +
1.729 + "--------- we go into the ProblemBrowser (_NO_ pblID selected) -";
1.730 +initContext 1 Pbl_ ([],Pbl);
1.731 +initContext 1 Met_ ([],Pbl);
1.732 +
1.733 + "--------- this match will show some incomplete items: ---------";
1.734 +checkContext 1 ([],Pbl) (kestoreID2guh Pbl_ ["univariate","equation"]);
1.735 +checkContext 1 ([],Pbl) (kestoreID2guh Met_ ["LinEq", "solve_lineq_equation"]);
1.736 +
1.737 +
1.738 + fetchProposedTactic 1;
1.739 + setNextTactic 1 (Add_Given "solveFor x"); autoCalculate 1 (Step 1);
1.740 +
1.741 + fetchProposedTactic 1;
1.742 + setNextTactic 1 (Add_Find "solutions L"); autoCalculate 1 (Step 1);
1.743 +
1.744 + "--------- this is a matching model (all items correct): -------";
1.745 +checkContext 1 ([],Pbl) (kestoreID2guh Pbl_ ["univariate","equation"]);
1.746 + "--------- this is a NOT matching model (some 'false': ---------";
1.747 +checkContext 1 ([],Pbl)(kestoreID2guh Pbl_["linear","univariate","equation"]);
1.748 +
1.749 + "--------- find out a matching problem: ------------------------";
1.750 + "--------- find out a matching problem (FAILING: no new pbl) ---";
1.751 + refineProblem 1([],Pbl)(pblID2guh ["linear","univariate","equation"]);
1.752 +
1.753 + "--------- find out a matching problem (SUCCESSFUL) ------------";
1.754 + refineProblem 1 ([],Pbl) (pblID2guh ["univariate","equation"]);
1.755 +
1.756 + "--------- tryMatch, tryRefine did not change the calculation -";
1.757 + "--------- this is done by <TRANSFER> on the pbl-browser: ------";
1.758 + setNextTactic 1 (Specify_Problem ["normalize","polynomial",
1.759 + "univariate","equation"]);
1.760 + autoCalculate 1 (Step 1);
1.761 +(*WN050904 fetchProposedTactic again --> Specify_Problem ["normalize",...
1.762 + and Specify_Theory skipped in comparison to below ---^^^-inserted *)
1.763 +(*------------vvv-inserted-----------------------------------------------*)
1.764 + fetchProposedTactic 1;
1.765 + setNextTactic 1 (Specify_Problem ["normalize","polynomial",
1.766 + "univariate","equation"]);
1.767 + autoCalculate 1 (Step 1);
1.768 +
1.769 +(*and Specify_Theory skipped by fetchProposedTactic ?!?*)
1.770 +
1.771 + fetchProposedTactic 1;
1.772 + setNextTactic 1 (Specify_Method ["PolyEq","normalize_poly"]);
1.773 + autoCalculate 1 (Step 1);
1.774 +
1.775 + fetchProposedTactic 1;
1.776 + setNextTactic 1 (Apply_Method ["PolyEq","normalize_poly"]);
1.777 + autoCalculate 1 CompleteCalc;
1.778 + val ((pt,_),_) = get_calc 1;
1.779 + show_pt pt;
1.780 + val p = get_pos 1 1;
1.781 + val (Form f, tac, asms) = pt_extract (pt, p);
1.782 + if term2str f = "[x = -1, x = -3]" andalso p = ([], Res) then () else
1.783 + raise error "FE-interface.sml: diff.behav. in tryMatchProblem, tryRefine";
1.784 +
1.785 +(*------------^^^-inserted-----------------------------------------------*)
1.786 +(*WN050904 the fetchProposedTactic's below may not have worked like that
1.787 + before, too, because there was no check*)
1.788 + fetchProposedTactic 1;
1.789 + setNextTactic 1 (Specify_Theory "PolyEq.thy");
1.790 + autoCalculate 1 (Step 1);
1.791 +
1.792 + fetchProposedTactic 1;
1.793 + setNextTactic 1 (Specify_Method ["PolyEq","normalize_poly"]);
1.794 + autoCalculate 1 (Step 1);
1.795 +
1.796 + fetchProposedTactic 1;
1.797 + "--------- now the calc-header is ready for enter 'solving' ----";
1.798 + autoCalculate 1 CompleteCalc;
1.799 +
1.800 + val ((pt,_),_) = get_calc 1;
1.801 +rootthy pt;
1.802 + show_pt pt;
1.803 + val p = get_pos 1 1;
1.804 + val (Form f, tac, asms) = pt_extract (pt, p);
1.805 + if term2str f = "[x = -1, x = -3]" andalso p = ([], Res) then () else
1.806 + raise error "FE-interface.sml: diff.behav. in tryMatchProblem, tryRefine";
1.807 +
1.808 +
1.809 +"--------- modifyCalcHead, resetCalcHead, modelProblem ------------";
1.810 +"--------- modifyCalcHead, resetCalcHead, modelProblem ------------";
1.811 +"--------- modifyCalcHead, resetCalcHead, modelProblem ------------";
1.812 +
1.813 + states:=[];
1.814 + DEconstrCalcTree 1;
1.815 + CalcTree
1.816 + [(["equality (x+1=2)", "solveFor x","solutions L"],
1.817 + ("Test.thy",
1.818 + ["sqroot-test","univariate","equation","test"],
1.819 + ["Test","squ-equ-test-subpbl1"]))];
1.820 + Iterator 1;
1.821 + moveActiveRoot 1;
1.822 +
1.823 + modifyCalcHead 1 (([],Pbl),(*the position from refFormula*)
1.824 + "solve (x+1=2, x)",(*the headline*)
1.825 + [Given ["equality (x+1=2)", "solveFor x"],
1.826 + Find ["solutions L"](*,Relate []*)],
1.827 + Pbl,
1.828 + ("Test.thy",
1.829 + ["sqroot-test","univariate","equation","test"],
1.830 + ["Test","squ-equ-test-subpbl1"]));
1.831 +resetCalcHead 1;
1.832 +modelProblem 1;
1.833 +
1.834 +
1.835 +"---------------- maximum-example, UC: Modeling an example -------";
1.836 +"---------------- maximum-example, UC: Modeling an example -------";
1.837 +"---------------- maximum-example, UC: Modeling an example -------";
1.838 +(* {\bf\UC{Editing the Model}\label{SPECIFY:enter}\label{SPECIFY:check}\\}
1.839 +see isac.bridge.TestModel#testEditItems
1.840 +*)
1.841 + val elems = ["fixedValues [r=Arbfix]","maximum A","valuesFor [a,b]",
1.842 + "relations [A=a*b, (a/2)^2 + (b/2)^2 = r^2]",
1.843 + "relations [A=a*b, (a/2)^2 + (b/2)^2 = r^2]",
1.844 + "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]",
1.845 + (*^^^ these are the elements for the root-problem (in variants)*)
1.846 + (*vvv these are elements required for subproblems*)
1.847 + "boundVariable a","boundVariable b","boundVariable alpha",
1.848 + "interval {x::real. 0 <= x & x <= 2*r}",
1.849 + "interval {x::real. 0 <= x & x <= 2*r}",
1.850 + "interval {x::real. 0 <= x & x <= pi}",
1.851 + "errorBound (eps=(0::real))"]
1.852 + (*specifying is not interesting for this example*)
1.853 + val spec = ("DiffApp.thy", ["maximum_of","function"],
1.854 + ["DiffApp","max_by_calculus"]);
1.855 + (*the empty model with descriptions for user-guidance by Model_Problem*)
1.856 + val empty_model = [Given ["fixedValues []"],
1.857 + Find ["maximum", "valuesFor"],
1.858 + Relate ["relations []"]];
1.859 + states:=[];
1.860 + DEconstrCalcTree 1;
1.861 + CalcTree [(elems, spec)];
1.862 + Iterator 1;
1.863 + moveActiveRoot 1;
1.864 + refFormula 1 (get_pos 1 1);
1.865 + (*this gives a completely empty model*)
1.866 +
1.867 + fetchProposedTactic 1;
1.868 +(*fill the CalcHead with Descriptions...*)
1.869 + setNextTactic 1 (Model_Problem );
1.870 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.871 +
1.872 + (*user input is !!!!!EITHER!!!!! _some_ (at least one) items of the model
1.873 + !!!!!OR!!!!! _one_ part of the specification !!!!!!!!!!!!!*)
1.874 + (*input of two items, 'fixedValues [r=Arbfix]' and 'maximum b'...*)
1.875 + modifyCalcHead 1 (([],Pbl) (*position, from previous refFormula*),
1.876 + "Problem (DiffApp.thy, [maximum_of, function])",
1.877 + (*the head-form ^^^ is not used for input here*)
1.878 + [Given ["fixedValues [r=Arbfix]"(*new input*)],
1.879 + Find ["maximum b"(*new input*), "valuesFor"],
1.880 + Relate ["relations"]],
1.881 + (*input (Arbfix will dissappear soon)*)
1.882 + Pbl (*belongsto*),
1.883 + e_spec (*no input to the specification*));
1.884 +
1.885 + (*the user does not know, what 'superfluous' for 'maximum b' may mean
1.886 + and asks what to do next*)
1.887 + fetchProposedTactic 1;
1.888 + (*the student follows the advice*)
1.889 + setNextTactic 1 (Add_Find "maximum A"); (*FIXME.17.11.03: does not yet work*)
1.890 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.891 +
1.892 + (*this input completes the model*)
1.893 + modifyCalcHead 1 (([],Pbl), "not used here",
1.894 + [Given ["fixedValues [r=Arbfix]"],
1.895 + Find ["maximum A", "valuesFor [a,b]"(*new input*)],
1.896 + Relate ["relations [A=a*b, \
1.897 + \(a/2)^2 + (b/2)^2 = r^2]"]], Pbl, e_spec);
1.898 +
1.899 + (*specification is not interesting an should be skipped by the dialogguide;
1.900 + !!!!!!!!!!!!!!!!!!!! input of ONE part at a time !!!!!!!!!!!!!!!!!!!!!!*)
1.901 + modifyCalcHead 1 (([],Pbl), "not used here",
1.902 + [Given ["fixedValues [r=Arbfix]"],
1.903 + Find ["maximum A", "valuesFor [a,b]"(*new input*)],
1.904 + Relate ["relations [A=a*b, \
1.905 + \(a/2)^2 + (b/2)^2 = r^2]"]], Pbl,
1.906 + ("DiffApp.thy", ["e_pblID"], ["e_metID"]));
1.907 + modifyCalcHead 1 (([],Pbl), "not used here",
1.908 + [Given ["fixedValues [r=Arbfix]"],
1.909 + Find ["maximum A", "valuesFor [a,b]"(*new input*)],
1.910 + Relate ["relations [A=a*b, \
1.911 + \(a/2)^2 + (b/2)^2 = r^2]"]], Pbl,
1.912 + ("DiffApp.thy", ["maximum_of","function"],
1.913 + ["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.thy", ["maximum_of","function"],
1.920 + ["DiffApp","max_by_calculus"]));
1.921 + (*this final calcHead now has STATUS 'complete' !*)
1.922 + DEconstrCalcTree 1;
1.923 +
1.924 +
1.925 +"--------- solve_linear from pbl-hierarchy -----------------------";
1.926 +"--------- solve_linear from pbl-hierarchy -----------------------";
1.927 +"--------- solve_linear from pbl-hierarchy -----------------------";
1.928 + states:=[];
1.929 + val (fmz, sp) = ([], ("", ["linear","univariate","equation","test"], []));
1.930 + CalcTree [(fmz, sp)];
1.931 + Iterator 1; moveActiveRoot 1;
1.932 + refFormula 1 (get_pos 1 1);
1.933 + modifyCalcHead 1 (([],Pbl),"solve (1+-1*2+x=0)",
1.934 + [Given ["equality (1+-1*2+x=0)", "solveFor x"],
1.935 + Find ["solutions L"]],
1.936 + Pbl,
1.937 + ("Test.thy", ["linear","univariate","equation","test"],
1.938 + ["Test","solve_linear"]));
1.939 + autoCalculate 1 CompleteCalc;
1.940 + refFormula 1 (get_pos 1 1);
1.941 + val ((pt,_),_) = get_calc 1;
1.942 + val p = get_pos 1 1;
1.943 + val (Form f, tac, asms) = pt_extract (pt, p);
1.944 + if term2str f = "[x = 1]" andalso p = ([], Res) then () else
1.945 + raise error "FE-interface.sml: diff.behav. in from pbl-hierarchy";
1.946 +
1.947 +
1.948 +
1.949 +"--------- solve_linear as in an algebra system (CAS)-------------";
1.950 +"--------- solve_linear as in an algebra system (CAS)-------------";
1.951 +"--------- solve_linear as in an algebra system (CAS)-------------";
1.952 + states:=[];
1.953 + val (fmz, sp) = ([], ("", [], []));
1.954 + CalcTree [(fmz, sp)];
1.955 + Iterator 1; moveActiveRoot 1;
1.956 + modifyCalcHead 1 (([],Pbl),"solveTest (1+-1*2+x=0,x)", [], Pbl, ("", [], []));
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) then () else
1.963 + raise error "FE-interface.sml: diff.behav. in algebra system";
1.964 +
1.965 +
1.966 +
1.967 +"--------- interSteps: on 'miniscript with mini-subpbl' ----------";
1.968 +"--------- interSteps: on 'miniscript with mini-subpbl' ----------";
1.969 +"--------- interSteps: on 'miniscript with mini-subpbl' ----------";
1.970 + states:=[];
1.971 + CalcTree
1.972 + [(["equality (x+1=2)", "solveFor x","solutions L"],
1.973 + ("Test.thy",
1.974 + ["sqroot-test","univariate","equation","test"],
1.975 + ["Test","squ-equ-test-subpbl1"]))];
1.976 + Iterator 1;
1.977 + moveActiveRoot 1;
1.978 + autoCalculate 1 CompleteCalc;
1.979 + val ((pt,_),_) = get_calc 1;
1.980 + show_pt pt;
1.981 +
1.982 + (*UC\label{SOLVE:INFO:intermediate-steps}*)
1.983 + interSteps 1 ([2],Res);
1.984 + val ((pt,_),_) = get_calc 1; show_pt pt (*new ([2,1],Frm)..([2,6],Res)*);
1.985 + val (unc, del, gen) = (([1],Res),([1],Res),([2,6],Res));
1.986 + getFormulaeFromTo 1 unc gen 1 false;
1.987 +
1.988 + (*UC\label{SOLVE:INFO:intermediate-steps}*)
1.989 + interSteps 1 ([3,2],Res);
1.990 + val ((pt,_),_) = get_calc 1; show_pt pt (*new ([3,2,1],Frm)..([3,2,2],Res)*);
1.991 + val (unc, del, gen) = (([3,1],Res),([3,1],Res),([3,2,2],Res));
1.992 + getFormulaeFromTo 1 unc gen 1 false;
1.993 +
1.994 + (*UC\label{SOLVE:INFO:intermediate-steps}*)
1.995 + interSteps 1 ([3],Res) (*no new steps in subproblems*);
1.996 + val (unc, del, gen) = (([3],Pbl),([3],Pbl),([3,2],Res));
1.997 + getFormulaeFromTo 1 unc gen 1 false;
1.998 +
1.999 + (*UC\label{SOLVE:INFO:intermediate-steps}*)
1.1000 + interSteps 1 ([],Res) (*no new steps in subproblems*);
1.1001 + val (unc, del, gen) = (([],Pbl),([],Pbl),([4],Res));
1.1002 + getFormulaeFromTo 1 unc gen 1 false;
1.1003 +
1.1004 +
1.1005 +"--------- getTactic, fetchApplicableTactics ---------------------";
1.1006 +"--------- getTactic, fetchApplicableTactics ---------------------";
1.1007 +"--------- getTactic, fetchApplicableTactics ---------------------";
1.1008 + states:=[];
1.1009 + CalcTree
1.1010 + [(["equality (x+1=2)", "solveFor x","solutions L"],
1.1011 + ("Test.thy",
1.1012 + ["sqroot-test","univariate","equation","test"],
1.1013 + ["Test","squ-equ-test-subpbl1"]))];
1.1014 + Iterator 1; moveActiveRoot 1;
1.1015 + autoCalculate 1 CompleteCalc;
1.1016 + val ((pt,_),_) = get_calc 1;
1.1017 + show_pt pt;
1.1018 +
1.1019 + (*UC\label{SOLVE:HIDE:getTactic}*)
1.1020 + getTactic 1 ([],Pbl);
1.1021 + getTactic 1 ([1],Res);
1.1022 + getTactic 1 ([3],Pbl);
1.1023 + getTactic 1 ([3,1],Frm);
1.1024 + getTactic 1 ([3],Res);
1.1025 + getTactic 1 ([],Res);
1.1026 +
1.1027 +(*UC\label{SOLVE:MANUAL:TACTIC:listall}*)
1.1028 + fetchApplicableTactics 1 99999 ([],Pbl);
1.1029 + fetchApplicableTactics 1 99999 ([1],Res);
1.1030 + fetchApplicableTactics 1 99999 ([3],Pbl);
1.1031 + fetchApplicableTactics 1 99999 ([3,1],Res);
1.1032 + fetchApplicableTactics 1 99999 ([3],Res);
1.1033 + fetchApplicableTactics 1 99999 ([],Res);
1.1034 +
1.1035 +
1.1036 +"--------- getAssumptions, getAccumulatedAsms --------------------";
1.1037 +"--------- getAssumptions, getAccumulatedAsms --------------------";
1.1038 +"--------- getAssumptions, getAccumulatedAsms --------------------";
1.1039 +states:=[];
1.1040 +CalcTree
1.1041 +[(["equality (x/(x^2 - 6*x+9) - 1/(x^2 - 3*x) =1/x)",
1.1042 + "solveFor x","solutions L"],
1.1043 + ("RatEq.thy",["univariate","equation"],["no_met"]))];
1.1044 +Iterator 1; moveActiveRoot 1;
1.1045 +autoCalculate 1 CompleteCalc;
1.1046 +val ((pt,_),_) = get_calc 1;
1.1047 +show_pt pt;
1.1048 +
1.1049 +(*UC\label{SOLVE:HELP:assumptions}*)
1.1050 +getAssumptions 1 ([3], Res);
1.1051 +getAssumptions 1 ([5], Res);
1.1052 +(*UC\label{SOLVE:HELP:assumptions-origin} WN0502 still without positions*)
1.1053 +getAccumulatedAsms 1 ([3], Res);
1.1054 +getAccumulatedAsms 1 ([5], Res);
1.1055 +
1.1056 +
1.1057 +"--------- arbitrary combinations of steps -----------------------";
1.1058 +"--------- arbitrary combinations of steps -----------------------";
1.1059 +"--------- arbitrary combinations of steps -----------------------";
1.1060 + states:=[];
1.1061 + CalcTree (*start of calculation, return No.1*)
1.1062 + [(["equality (1+-1*2+x=0)", "solveFor x","solutions L"],
1.1063 + ("Test.thy",
1.1064 + ["linear","univariate","equation","test"],
1.1065 + ["Test","solve_linear"]))];
1.1066 + Iterator 1; moveActiveRoot 1;
1.1067 +
1.1068 + fetchProposedTactic 1;
1.1069 + setNextTactic 1 (Model_Problem );
1.1070 + autoCalculate 1 (Step 1);
1.1071 +
1.1072 + fetchProposedTactic 1;
1.1073 + fetchProposedTactic 1;
1.1074 +
1.1075 + setNextTactic 1 (Add_Find "solutions L");
1.1076 + setNextTactic 1 (Add_Find "solutions L");
1.1077 +
1.1078 + autoCalculate 1 (Step 1);
1.1079 + autoCalculate 1 (Step 1);
1.1080 +
1.1081 + setNextTactic 1 (Specify_Theory "Test.thy");
1.1082 + fetchProposedTactic 1;
1.1083 + autoCalculate 1 (Step 1);
1.1084 +
1.1085 + autoCalculate 1 (Step 1);
1.1086 + autoCalculate 1 (Step 1);
1.1087 + autoCalculate 1 (Step 1);
1.1088 + autoCalculate 1 (Step 1);
1.1089 +(*------------------------- end calc-head*)
1.1090 +
1.1091 + fetchProposedTactic 1;
1.1092 + setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "isolate_bdv"));
1.1093 + autoCalculate 1 (Step 1);
1.1094 +
1.1095 + setNextTactic 1 (Rewrite_Set "Test_simplify");
1.1096 + fetchProposedTactic 1;
1.1097 + autoCalculate 1 (Step 1);
1.1098 +
1.1099 + autoCalculate 1 CompleteCalc;
1.1100 + val ((pt,_),_) = get_calc 1;
1.1101 + val p = get_pos 1 1;
1.1102 + val (Form f, tac, asms) = pt_extract (pt, p);
1.1103 + if term2str f = "[x = 1]" andalso p = ([], Res) then () else
1.1104 + raise error "FE-interface.sml: diff.behav. in combinations of steps";
1.1105 +
1.1106 +
1.1107 +"--------- appendFormula label{SOLVE:MANUAL:FORMULA:enter} right--";
1.1108 +"--------- appendFormula label{SOLVE:MANUAL:FORMULA:enter} right--";
1.1109 +"--------- appendFormula label{SOLVE:MANUAL:FORMULA:enter} right--";
1.1110 + states:=[];
1.1111 + CalcTree
1.1112 + [(["equality (x+1=2)", "solveFor x","solutions L"],
1.1113 + ("Test.thy",
1.1114 + ["sqroot-test","univariate","equation","test"],
1.1115 + ["Test","squ-equ-test-subpbl1"]))];
1.1116 + Iterator 1;
1.1117 + moveActiveRoot 1;
1.1118 + autoCalculate 1 CompleteCalcHead;
1.1119 + autoCalculate 1 (Step 1);
1.1120 + autoCalculate 1 (Step 1);
1.1121 + appendFormula 1 "-1 + x = 0";
1.1122 + (*... returns calcChangedEvent with*)
1.1123 + val (unc, del, gen) = (([1],Res), ([1],Res), ([2],Res));
1.1124 + getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
1.1125 +
1.1126 + val ((pt,_),_) = get_calc 1;
1.1127 + val p = get_pos 1 1;
1.1128 + val (Form f, tac, asms) = pt_extract (pt, p);
1.1129 + if term2str f = "-1 + x = 0" andalso p = ([2], Res) then () else
1.1130 + raise error "FE-interface.sml: diff.behav. in FORMULA:enter} right";
1.1131 +
1.1132 +"--------- appendFormula label{SOLVE:MANUAL:FORMULA:enter} other--";
1.1133 +"--------- appendFormula label{SOLVE:MANUAL:FORMULA:enter} other--";
1.1134 +"--------- appendFormula label{SOLVE:MANUAL:FORMULA:enter} other--";
1.1135 + states:=[];
1.1136 + CalcTree
1.1137 + [(["equality (x+1=2)", "solveFor x","solutions L"],
1.1138 + ("Test.thy",
1.1139 + ["sqroot-test","univariate","equation","test"],
1.1140 + ["Test","squ-equ-test-subpbl1"]))];
1.1141 + Iterator 1;
1.1142 + moveActiveRoot 1;
1.1143 + autoCalculate 1 CompleteCalcHead;
1.1144 + autoCalculate 1 (Step 1);
1.1145 + autoCalculate 1 (Step 1);
1.1146 + appendFormula 1 "x - 1 = 0";
1.1147 + val (unc, del, gen) = (([1],Res), ([1],Res), ([2],Res));
1.1148 + getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
1.1149 + (*11 elements !!!*)
1.1150 +
1.1151 + val ((pt,_),_) = get_calc 1;
1.1152 + val p = get_pos 1 1;
1.1153 + val (Form f, tac, asms) = pt_extract (pt, p);
1.1154 + if term2str f = "x - 1 = 0" andalso p = ([2], Res) then () else
1.1155 + raise error "FE-interface.sml: diff.behav. in FORMULA:enter} other";
1.1156 +
1.1157 +"--------- appendFormula label{SOLVE:MANUAL:FORMULA:enter} oth 2--";
1.1158 +"--------- appendFormula label{SOLVE:MANUAL:FORMULA:enter} oth 2--";
1.1159 +"--------- appendFormula label{SOLVE:MANUAL:FORMULA:enter} oth 2--";
1.1160 + states:=[];
1.1161 + CalcTree
1.1162 + [(["equality (x+1=2)", "solveFor x","solutions L"],
1.1163 + ("Test.thy",
1.1164 + ["sqroot-test","univariate","equation","test"],
1.1165 + ["Test","squ-equ-test-subpbl1"]))];
1.1166 + Iterator 1;
1.1167 + moveActiveRoot 1;
1.1168 + autoCalculate 1 CompleteCalcHead;
1.1169 + autoCalculate 1 (Step 1);
1.1170 + autoCalculate 1 (Step 1);
1.1171 + appendFormula 1 "x = 1";
1.1172 + (*... returns calcChangedEvent with*)
1.1173 + val (unc, del, gen) = (([1],Res), ([1],Res), ([3,2],Res));
1.1174 + getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
1.1175 + (*6 elements !!!*)
1.1176 +
1.1177 + val ((pt,_),_) = get_calc 1;
1.1178 + val p = get_pos 1 1;
1.1179 + val (Form f, tac, asms) = pt_extract (pt, p);
1.1180 + if term2str f = "x = 1" andalso p = ([3,2], Res) then () else
1.1181 + raise error "FE-interface.sml: diff.behav. in FORMULA:enter} oth 2";
1.1182 +
1.1183 +
1.1184 +"--------- appendFormula label{SOLVE:MANUAL:FORMULA:enter} NOTok--";
1.1185 +"--------- appendFormula label{SOLVE:MANUAL:FORMULA:enter} NOTok--";
1.1186 +"--------- appendFormula label{SOLVE:MANUAL:FORMULA:enter} NOTok--";
1.1187 + states:=[];
1.1188 + CalcTree
1.1189 + [(["equality (x+1=2)", "solveFor x","solutions L"],
1.1190 + ("Test.thy",
1.1191 + ["sqroot-test","univariate","equation","test"],
1.1192 + ["Test","squ-equ-test-subpbl1"]))];
1.1193 + Iterator 1;
1.1194 + moveActiveRoot 1;
1.1195 + autoCalculate 1 CompleteCalcHead;
1.1196 + autoCalculate 1 (Step 1);
1.1197 + autoCalculate 1 (Step 1);
1.1198 + appendFormula 1 "x - 4711 = 0";
1.1199 + (*... returns <ERROR> no derivation found </ERROR>*)
1.1200 +
1.1201 + val ((pt,_),_) = get_calc 1;
1.1202 + val p = get_pos 1 1;
1.1203 + val (Form f, tac, asms) = pt_extract (pt, p);
1.1204 + if term2str f = "x + 1 + -1 * 2 = 0" andalso p = ([1], Res) then () else
1.1205 + raise error "FE-interface.sml: diff.behav. in FORMULA:enter} NOTok";
1.1206 +
1.1207 +
1.1208 +"--------- replaceFormula {SOLVE:MANUAL:FORMULA:replace} right----";
1.1209 +"--------- replaceFormula {SOLVE:MANUAL:FORMULA:replace} right----";
1.1210 +"--------- replaceFormula {SOLVE:MANUAL:FORMULA:replace} right----";
1.1211 + states:=[];
1.1212 + CalcTree
1.1213 + [(["equality (x+1=2)", "solveFor x","solutions L"],
1.1214 + ("Test.thy",
1.1215 + ["sqroot-test","univariate","equation","test"],
1.1216 + ["Test","squ-equ-test-subpbl1"]))];
1.1217 + Iterator 1;
1.1218 + moveActiveRoot 1;
1.1219 + autoCalculate 1 CompleteCalc;
1.1220 + moveActiveFormula 1 ([2],Res);
1.1221 + replaceFormula 1 "-1 + x = 0" (*i.e. repeats input*);
1.1222 + (*... returns <ERROR> formula not changed </ERROR>*)
1.1223 +
1.1224 + val ((pt,_),_) = get_calc 1;
1.1225 + val p = get_pos 1 1;
1.1226 + val (Form f, tac, asms) = pt_extract (pt, p);
1.1227 + if term2str f = "-1 + x = 0" andalso p = ([2], Res) then () else
1.1228 + raise error "FE-interface.sml: diff.behav. in FORMULA:replace} right 1";
1.1229 + if map fst (get_interval ([2],Res) ([],Res) 9999 pt) =
1.1230 + [([2], Res), ([3], Pbl), ([3, 1], Frm), ([3, 1], Res), ([3, 2], Res),
1.1231 + ([3], Res), ([4], Res), ([], Res)] then () (*nothing deleted!*) else
1.1232 + raise error "FE-interface.sml: diff.behav. in FORMULA:replace} right 2";
1.1233 +
1.1234 +(*WN050211 replaceFormula didn't work on second ctree: thus now tested...*)
1.1235 + CalcTree
1.1236 + [(["equality (x+1=2)", "solveFor x","solutions L"],
1.1237 + ("Test.thy",
1.1238 + ["sqroot-test","univariate","equation","test"],
1.1239 + ["Test","squ-equ-test-subpbl1"]))];
1.1240 + Iterator 2;
1.1241 + moveActiveRoot 2;
1.1242 + autoCalculate 2 CompleteCalc;
1.1243 + moveActiveFormula 2 ([2],Res);
1.1244 + replaceFormula 2 "-1 + x = 0" (*i.e. repeats input*);
1.1245 + (*... returns <ERROR> formula not changed </ERROR>*)
1.1246 +
1.1247 + val ((pt,_),_) = get_calc 2;
1.1248 + val p = get_pos 2 1;
1.1249 + val (Form f, tac, asms) = pt_extract (pt, p);
1.1250 + if term2str f = "-1 + x = 0" andalso p = ([2], Res) then () else
1.1251 + raise error "FE-interface.sml: diff.behav. in FORMULA:replace} right 1";
1.1252 + if map fst (get_interval ([2],Res) ([],Res) 9999 pt) =
1.1253 + [([2], Res), ([3], Pbl), ([3, 1], Frm), ([3, 1], Res), ([3, 2], Res),
1.1254 + ([3], Res), ([4], Res), ([], Res)] then () (*nothing deleted!*) else
1.1255 + raise error "FE-interface.sml: diff.behav. in FORMULA:replace} right 2b";
1.1256 +
1.1257 +"--------- replaceFormula {SOLVE:MANUAL:FORMULA:replace} other----";
1.1258 +"--------- replaceFormula {SOLVE:MANUAL:FORMULA:replace} other----";
1.1259 +"--------- replaceFormula {SOLVE:MANUAL:FORMULA:replace} other----";
1.1260 + states:=[];
1.1261 + CalcTree
1.1262 + [(["equality (x+1=2)", "solveFor x","solutions L"],
1.1263 + ("Test.thy",
1.1264 + ["sqroot-test","univariate","equation","test"],
1.1265 + ["Test","squ-equ-test-subpbl1"]))];
1.1266 + Iterator 1;
1.1267 + moveActiveRoot 1;
1.1268 + autoCalculate 1 CompleteCalc;
1.1269 + moveActiveFormula 1 ([2],Res); (*there is "-1 + x = 0"*)
1.1270 + replaceFormula 1 "x - 1 = 0"; (*<-------------------------------------*)
1.1271 + (*... returns calcChangedEvent with*)
1.1272 + val (unc, del, gen) = (([1],Res), ([4],Res), ([2],Res));
1.1273 + getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
1.1274 +
1.1275 + val ((pt,_),_) = get_calc 1;
1.1276 + show_pt pt;
1.1277 + val p = get_pos 1 1;
1.1278 + val (Form f, tac, asms) = pt_extract (pt, p);
1.1279 + if term2str f = "x - 1 = 0" andalso p = ([2], Res) then () else
1.1280 + raise error "FE-interface.sml: diff.behav. in FORMULA:replace} other 1";
1.1281 +(* for getting the list in whole length ...
1.1282 +print_depth 99;map fst (get_interval ([1],Res) ([],Res) 9999 pt);print_depth 3;
1.1283 + *)
1.1284 + if map fst (get_interval ([1],Res) ([],Res) 9999 pt) =
1.1285 + [([1], Res), ([2, 1], Frm), ([2, 1], Res), ([2, 2], Res), ([2, 3], Res),
1.1286 + ([2, 4], Res), ([2, 5], Res), ([2, 6], Res), ([2, 7], Res),
1.1287 + ([2, 8], Res), ([2, 9], Res), ([2], Res)
1.1288 +(*WN060727 {cutlevup->test_trans} removed: ,
1.1289 + ([], Res)(*dropped, if test_trans doesnt stop at PblNd*)*)] then () else
1.1290 + raise error "FE-interface.sml: diff.behav. in FORMULA:replace} other 2";
1.1291 +
1.1292 +
1.1293 +
1.1294 +"--------- replaceFormula {SOLVE:MANUAL:FORMULA:replace} other 2--";
1.1295 +"--------- replaceFormula {SOLVE:MANUAL:FORMULA:replace} other 2--";
1.1296 +"--------- replaceFormula {SOLVE:MANUAL:FORMULA:replace} other 2--";
1.1297 + states:=[];
1.1298 + CalcTree
1.1299 + [(["equality (x+1=2)", "solveFor x","solutions L"],
1.1300 + ("Test.thy",
1.1301 + ["sqroot-test","univariate","equation","test"],
1.1302 + ["Test","squ-equ-test-subpbl1"]))];
1.1303 + Iterator 1;
1.1304 + moveActiveRoot 1;
1.1305 + autoCalculate 1 CompleteCalc;
1.1306 + moveActiveFormula 1 ([2],Res); (*there is "-1 + x = 0"*)
1.1307 + replaceFormula 1 "x = 1"; (*<-------------------------------------*)
1.1308 + (*... returns calcChangedEvent with ...*)
1.1309 + val (unc, del, gen) = (([1],Res), ([4],Res), ([3,2],Res));
1.1310 + getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
1.1311 + (*9 elements !!!*)
1.1312 +
1.1313 + val ((pt,_),_) = get_calc 1;
1.1314 + show_pt pt; (*error: ...get_interval drops ([3,2],Res) ...*)
1.1315 + val (t,_) = get_obj g_result pt [3,2]; term2str t;
1.1316 + if map fst (get_interval ([1],Res) ([],Res) 9999 pt) =
1.1317 + [([1], Res), ([2], Res), ([3], Pbl), ([3, 1], Frm), ([3, 1], Res),
1.1318 + ([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res),
1.1319 + ([3,2],Res)] then () else
1.1320 + raise error "FE-interface.sml: diff.behav. in FORMULA:replace} oth2 1";
1.1321 +
1.1322 + val p = get_pos 1 1;
1.1323 + val (Form f, tac, asms) = pt_extract (pt, p);
1.1324 + if term2str f = "x = 1" andalso p = ([3,2], Res) then () else
1.1325 + raise error "FE-interface.sml: diff.behav. in FORMULA:replace} oth2 2";
1.1326 +
1.1327 +
1.1328 +
1.1329 +"--------- replaceFormula {SOLVE:MANUAL:FORMULA:replace} NOTok----";
1.1330 +"--------- replaceFormula {SOLVE:MANUAL:FORMULA:replace} NOTok----";
1.1331 +"--------- replaceFormula {SOLVE:MANUAL:FORMULA:replace} NOTok----";
1.1332 + states:=[];
1.1333 + CalcTree
1.1334 + [(["equality (x+1=2)", "solveFor x","solutions L"],
1.1335 + ("Test.thy",
1.1336 + ["sqroot-test","univariate","equation","test"],
1.1337 + ["Test","squ-equ-test-subpbl1"]))];
1.1338 + Iterator 1;
1.1339 + moveActiveRoot 1;
1.1340 + autoCalculate 1 CompleteCalc;
1.1341 + moveActiveFormula 1 ([2],Res); (*there is "-1 + x = 0"*)
1.1342 + replaceFormula 1 "x - 4711 = 0";
1.1343 + (*... returns <ERROR> no derivation found </ERROR>*)
1.1344 +
1.1345 + val ((pt,_),_) = get_calc 1;
1.1346 + show_pt pt;
1.1347 + val p = get_pos 1 1;
1.1348 + val (Form f, tac, asms) = pt_extract (pt, p);
1.1349 + if term2str f = "-1 + x = 0" andalso p = ([2], Res) then () else
1.1350 + raise error "FE-interface.sml: diff.behav. in FORMULA:replace} NOTok";
1.1351 +
1.1352 +