1.1 --- a/test/Tools/isac/FE-interface/interface.sml Mon Aug 30 14:29:49 2010 +0200
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,1349 +0,0 @@
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 -