1.1 --- a/test/Tools/isac/ProgLang/rewrite.sml Thu Jul 28 10:58:17 2011 +0200
1.2 +++ b/test/Tools/isac/ProgLang/rewrite.sml Thu Jul 28 11:22:54 2011 +0200
1.3 @@ -117,7 +117,7 @@
1.4 "----------- conditional rewriting without Isac's thys --";
1.5 "----------- conditional rewriting without Isac's thys --";
1.6 "----------- conditional rewriting without Isac's thys --";
1.7 -(*ML {*)
1.8 +
1.9 "===== prepr cond.rew. with Pattern.match";
1.10 val thy = @{theory Complex_Main};
1.11 val ctxt = @{context};
2.1 --- a/test/Tools/isac/Test_Some.thy Thu Jul 28 10:58:17 2011 +0200
2.2 +++ b/test/Tools/isac/Test_Some.thy Thu Jul 28 11:22:54 2011 +0200
2.3 @@ -9,16 +9,1402 @@
2.4
2.5 ML {*
2.6
2.7 -*}
2.8 -ML{*
2.9 -*}
2.10 -ML{*
2.11 -*}
2.12 -ML{*
2.13 -*}
2.14 -ML{*
2.15 -*}
2.16 -ML{*
2.17 +(* tests the interface of isac's SML-kernel in accordance to
2.18 + java-tests/isac.bridge.
2.19 +
2.20 +WN050707 ... if true, the test ist marked with a \label referring
2.21 +to the same UC in isac-docu.tex as the JUnit testcase.
2.22 +use"../smltest/FE-interface/interface.sml";
2.23 +use"interface.sml";
2.24 + *)
2.25 +
2.26 +"--------------------------------------------------------";
2.27 +"table of contents --------------------------------------";
2.28 +"--------------------------------------------------------";
2.29 +"within struct ------------------------------------------";
2.30 +"--------------------------------------------------------";
2.31 +"--------- encode ^ -> ^^^ ------------------------------";
2.32 +"--------------------------------------------------------";
2.33 +"exported from struct -----------------------------------";
2.34 +"--------------------------------------------------------";
2.35 +"--------- empty rootpbl --------------------------------";
2.36 +"--------- solve_linear as rootpbl FE -------------------";
2.37 +"--------- inspect the CalcTree No.1 with Iterator No.2 -";
2.38 +"--------- miniscript with mini-subpbl ------------------";
2.39 +"--------- mini-subpbl AUTOCALCULATE Step 1 -------------";
2.40 +"--------- solve_linear as rootpbl AUTO CompleteCalc ----";
2.41 +"--------- solve_linear as rootpbl AUTO CompleteHead/Calc ";
2.42 +"--------- mini-subpbl AUTOCALCULATE CompleteCalc -------";
2.43 +"--------- mini-subpbl AUTO CompleteCalcHead ------------";
2.44 +"--------- solve_linear as rootpbl AUTO CompleteModel ---";
2.45 +"--------- setContext..Thy ------------------------------";
2.46 +"--------- mini-subpbl AUTOCALC CompleteToSubpbl --------";
2.47 +"--------- rat-eq + subpbl: no_met, NO solution dropped -";
2.48 +"--------- tryMatchProblem, tryRefineProblem ------------";
2.49 +"--------- modifyCalcHead, resetCalcHead, modelProblem --";
2.50 +"--------- maximum-example, UC: Modeling an example -----";
2.51 +"--------- solve_linear from pbl-hierarchy --------------";
2.52 +"--------- solve_linear as in an algebra system (CAS)----";
2.53 +"--------- interSteps: on 'miniscript with mini-subpbl' -";
2.54 +"--------- getTactic, fetchApplicableTactics ------------";
2.55 +"--------- getAssumptions, getAccumulatedAsms -----------";
2.56 +"--------- arbitrary combinations of steps --------------";
2.57 +"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}right";
2.58 +"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}other";
2.59 +"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}oth 2";
2.60 +"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}NOTok";
2.61 +"--------- replaceFormula {SOL:MAN:FOR:replace} right----";
2.62 +"--------- replaceFormula {SOL:MAN:FOR:replace} other----";
2.63 +"--------- replaceFormula {SOL:MAN:FOR:replace} other 2--";
2.64 +"--------- replaceFormula {SOL:MAN:FOR:replace} NOTok----";
2.65 +"--------------------------------------------------------";
2.66 +
2.67 +"within struct ---------------------------------------------------";
2.68 +"within struct ---------------------------------------------------";
2.69 +"within struct ---------------------------------------------------";
2.70 +(*==================================================================
2.71 +
2.72 +
2.73 +"--------- encode ^ -> ^^^ ------------------------------";
2.74 +"--------- encode ^ -> ^^^ ------------------------------";
2.75 +"--------- encode ^ -> ^^^ ------------------------------";
2.76 +if encode "a^2+b^2=c^2" = "a^^^2+b^^^2=c^^^2" then ()
2.77 +else error "interface.sml: diff.behav. in encode ^ -> ^^^ ";
2.78 +
2.79 +if (decode o encode) "a^2+b^2=c^2" = "a^2+b^2=c^2" then ()
2.80 +else error "interface.sml: diff.behav. in de/encode ^ <-> ^^^ ";
2.81 +
2.82 +==================================================================*)
2.83 +"exported from struct --------------------------------------------";
2.84 +"exported from struct --------------------------------------------";
2.85 +"exported from struct --------------------------------------------";
2.86 +
2.87 +
2.88 +(*------------ set at startup of the Kernel ----------------------*)
2.89 + states:= []; (*resets all state information in Kernel *)
2.90 +(*----------------------------------------------------------------*)
2.91 +
2.92 +"--------- empty rootpbl --------------------------------";
2.93 +"--------- empty rootpbl --------------------------------";
2.94 +"--------- empty rootpbl --------------------------------";
2.95 + CalcTree [([], ("", [], []))];
2.96 + Iterator 1;
2.97 + moveActiveRoot 1;
2.98 + refFormula 1 (get_pos 1 1);
2.99 +(*WN.040222: stoert das sehr, dass e_domID etc. statt leer kommt ???*)
2.100 +DEconstrCalcTree 1;
2.101 +
2.102 +"--------- solve_linear as rootpbl FE -------------------";
2.103 +"--------- solve_linear as rootpbl FE -------------------";
2.104 +"--------- solve_linear as rootpbl FE -------------------";
2.105 + CalcTree (*start of calculation, return No.1*)
2.106 + [(["equality (1+-1*2+x=(0::real))", "solveFor x","solutions L"],
2.107 + ("Test",
2.108 + ["linear","univariate","equation","test"],
2.109 + ["Test","solve_linear"]))];
2.110 + Iterator 1; (*create an active Iterator on CalcTree No.1*)
2.111 +
2.112 + moveActiveRoot 1;(*sets the CalcIterator No.1 at the root of CalcTree No.1*);
2.113 + refFormula 1 (get_pos 1 1) (*gets CalcHead; model is still empty*);
2.114 +
2.115 +
2.116 + fetchProposedTactic 1 (*by using Iterator No.1*);
2.117 + setNextTactic 1 (Model_Problem); (*by using Iterator No.1*)
2.118 + autoCalculate 1 (Step 1);
2.119 + refFormula 1 (get_pos 1 1) (*model contains descriptions for all items*);
2.120 + autoCalculate 1 (Step 1);
2.121 +(*-----since Model_Problem + complete_mod_ in case cas of SOME-----*
2.122 + fetchProposedTactic 1;
2.123 + setNextTactic 1 (Add_Given "equality (1 + -1 * 2 + x = (0::real))");
2.124 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); (*equality added*);
2.125 +
2.126 + fetchProposedTactic 1;
2.127 + setNextTactic 1 (Add_Given "solveFor x");
2.128 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.129 +
2.130 + fetchProposedTactic 1;
2.131 + setNextTactic 1 (Add_Find "solutions L");
2.132 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.133 +
2.134 + fetchProposedTactic 1;
2.135 + setNextTactic 1 (Specify_Theory "Test");
2.136 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.137 +*-----since Model_Problem + complete_mod_ in case cas of SOME-----*)
2.138 +
2.139 + fetchProposedTactic 1;
2.140 + setNextTactic 1 (Specify_Problem ["linear","univariate","equation","test"]);
2.141 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.142 +(*-------------------------------------------------------------------------*)
2.143 + fetchProposedTactic 1;
2.144 + val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;
2.145 +
2.146 + setNextTactic 1 (Specify_Method ["Test","solve_linear"]);
2.147 + val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;
2.148 +
2.149 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.150 + val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;
2.151 +
2.152 +(*-------------------------------------------------------------------------*)
2.153 + fetchProposedTactic 1;
2.154 + val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;
2.155 +
2.156 + setNextTactic 1 (Apply_Method ["Test","solve_linear"]);
2.157 + (*ERROR.110620 <SETNEXTTACTIC>..<MESSAGE> end-of-calculation*)
2.158 + val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;
2.159 + is_complete_mod ptp;
2.160 + is_complete_spec ptp;
2.161 +
2.162 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.163 + val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;
2.164 + (*term2str (get_obj g_form pt [1]);*)
2.165 +(*-------------------------------------------------------------------------*)
2.166 +
2.167 + fetchProposedTactic 1;
2.168 + setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "isolate_bdv"));
2.169 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.170 +
2.171 + fetchProposedTactic 1;
2.172 + setNextTactic 1 (Rewrite_Set "Test_simplify");
2.173 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.174 +
2.175 + fetchProposedTactic 1;
2.176 + setNextTactic 1 (Check_Postcond ["linear","univariate","equation","test"]);
2.177 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.178 +
2.179 + val ((pt,_),_) = get_calc 1;
2.180 + val ip = get_pos 1 1;
2.181 + val (Form f, tac, asms) = pt_extract (pt, ip);
2.182 + (*exception just above means: 'ModSpec' has been returned: error anyway*)
2.183 + if term2str f = "[x = 1]" then () else
2.184 + error "FE-Kernel-interface.sml: diff.behav. in solve_linear as rootpbl";
2.185 +
2.186 +"--------- inspect the CalcTree No.1 with Iterator No.2 -";
2.187 +"--------- inspect the CalcTree No.1 with Iterator No.2 -";
2.188 +"--------- inspect the CalcTree No.1 with Iterator No.2 -";
2.189 +(*WN041118: inspection shifted to Iterator No.1, because others need pos'*)
2.190 + moveActiveRoot 1;
2.191 + refFormula 1 ([],Pbl); getTactic 1 ([],Pbl);(*Error*)
2.192 + moveActiveDown 1;
2.193 + refFormula 1 ([1],Frm); getTactic 1 ([1],Frm);(*Error*)
2.194 + moveActiveDown 1 ;
2.195 + refFormula 1 ([1],Res); getTactic 1 ([1],Res);(*OK*)
2.196 + (*getAssumption 1 ([1],Res); TODO.WN041217*)
2.197 + moveActiveDown 1 ; refFormula 1 ([2],Res);
2.198 + moveActiveCalcHead 1; refFormula 1 ([],Pbl);
2.199 + moveActiveDown 1;
2.200 + moveActiveDown 1;
2.201 + moveActiveDown 1;
2.202 + if get_pos 1 1 = ([2], Res) then () else
2.203 + error "FE-interface.sml: diff.behav. in a inspect 1 with Iterator 2";
2.204 + moveActiveDown 1; refFormula 1 ([], Res);
2.205 + if get_pos 1 1 = ([], Res) then () else
2.206 + error "FE-interface.sml: diff.behav. in b inspect 1 with Iterator 2";
2.207 + moveActiveCalcHead 1; refFormula 1 ([],Pbl);
2.208 +DEconstrCalcTree 1;
2.209 +
2.210 +"--------- miniscript with mini-subpbl ------------------";
2.211 +"--------- miniscript with mini-subpbl ------------------";
2.212 +"--------- miniscript with mini-subpbl ------------------";
2.213 +"=== this sequence of fun-calls resembles fun me ===";
2.214 + states:=[]; (*start of calculation, return No.1*)
2.215 + CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
2.216 + ("Test", ["sqroot-test","univariate","equation","test"],
2.217 + ["Test","squ-equ-test-subpbl1"]))];
2.218 + Iterator 1;
2.219 +
2.220 + moveActiveRoot 1;
2.221 + refFormula 1 (get_pos 1 1);
2.222 + fetchProposedTactic 1;
2.223 + setNextTactic 1 (Model_Problem);
2.224 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*gets ModSpec;model is still empty*)
2.225 +
2.226 + fetchProposedTactic 1;
2.227 + setNextTactic 1 (Add_Given "equality (x + 1 = 2)");
2.228 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.229 +
2.230 + fetchProposedTactic 1;
2.231 + setNextTactic 1 (Add_Given "solveFor x");
2.232 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.233 +
2.234 + fetchProposedTactic 1;
2.235 + setNextTactic 1 (Add_Find "solutions L");
2.236 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.237 +
2.238 + fetchProposedTactic 1;
2.239 + setNextTactic 1 (Specify_Theory "Test");
2.240 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.241 +
2.242 + fetchProposedTactic 1;
2.243 + setNextTactic 1 (Specify_Problem
2.244 + ["sqroot-test","univariate","equation","test"]);
2.245 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.246 +"1-----------------------------------------------------------------";
2.247 +
2.248 + fetchProposedTactic 1;
2.249 + setNextTactic 1 (Specify_Method ["Test","squ-equ-test-subpbl1"]);
2.250 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.251 +
2.252 + fetchProposedTactic 1;
2.253 + setNextTactic 1 (Apply_Method ["Test","squ-equ-test-subpbl1"]);
2.254 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.255 +
2.256 + fetchProposedTactic 1;
2.257 + setNextTactic 1 (Rewrite_Set "norm_equation");
2.258 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.259 +
2.260 + fetchProposedTactic 1;
2.261 + setNextTactic 1 (Rewrite_Set "Test_simplify");
2.262 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.263 +
2.264 + fetchProposedTactic 1;(*----------------Subproblem--------------------*);
2.265 + setNextTactic 1 (Subproblem ("Test",
2.266 + ["linear","univariate","equation","test"]));
2.267 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.268 +
2.269 + fetchProposedTactic 1;
2.270 + setNextTactic 1 (Model_Problem );
2.271 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.272 +
2.273 + fetchProposedTactic 1;
2.274 + setNextTactic 1 (Add_Given "equality (-1 + x = 0)");
2.275 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.276 +
2.277 + fetchProposedTactic 1;
2.278 + setNextTactic 1 (Add_Given "solveFor x");
2.279 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.280 +
2.281 + fetchProposedTactic 1;
2.282 + setNextTactic 1 (Add_Find "solutions x_i");
2.283 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.284 +
2.285 + fetchProposedTactic 1;
2.286 + setNextTactic 1 (Specify_Theory "Test");
2.287 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.288 +
2.289 + fetchProposedTactic 1;
2.290 + setNextTactic 1 (Specify_Problem ["linear","univariate","equation","test"]);
2.291 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.292 +"2-----------------------------------------------------------------";
2.293 +
2.294 + fetchProposedTactic 1;
2.295 + setNextTactic 1 (Specify_Method ["Test","solve_linear"]);
2.296 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.297 +
2.298 + fetchProposedTactic 1;
2.299 + setNextTactic 1 (Apply_Method ["Test","solve_linear"]);
2.300 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.301 +
2.302 + fetchProposedTactic 1;
2.303 + setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "isolate_bdv"));
2.304 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.305 +
2.306 + fetchProposedTactic 1;
2.307 + setNextTactic 1 (Rewrite_Set "Test_simplify");
2.308 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.309 +
2.310 + fetchProposedTactic 1;
2.311 + setNextTactic 1 (Check_Postcond ["linear","univariate","equation","test"]);
2.312 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.313 +
2.314 + fetchProposedTactic 1;
2.315 + setNextTactic 1 (Check_elementwise "Assumptions");
2.316 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.317 +
2.318 + val xml = fetchProposedTactic 1;
2.319 + setNextTactic 1 (Check_Postcond
2.320 + ["sqroot-test","univariate","equation","test"]);
2.321 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.322 +
2.323 + val ((pt,_),_) = get_calc 1;
2.324 + val str = pr_ptree pr_short pt;
2.325 + writeln str;
2.326 + val ip = get_pos 1 1;
2.327 + val (Form f, tac, asms) = pt_extract (pt, ip);
2.328 + (*exception just above means: 'ModSpec' has been returned: error anyway*)
2.329 + if term2str f = "[x = 1]" then () else
2.330 + error "FE-interface.sml: diff.behav. in miniscript with mini-subpb";
2.331 + DEconstrCalcTree 1;
2.332 +
2.333 +"--------- mini-subpbl AUTOCALCULATE Step 1 -------------";
2.334 +"--------- mini-subpbl AUTOCALCULATE Step 1 -------------";
2.335 +"--------- mini-subpbl AUTOCALCULATE Step 1 -------------";
2.336 + CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
2.337 + ("Test", ["sqroot-test","univariate","equation","test"],
2.338 + ["Test","squ-equ-test-subpbl1"]))];
2.339 + Iterator 1;
2.340 + moveActiveRoot 1;
2.341 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.342 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.343 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.344 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.345 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.346 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.347 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.348 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.349 + (*here the solve-phase starts*)
2.350 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.351 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.352 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.353 + (*------------------------------------*)
2.354 +(* print_depth 13; get_calc 1;
2.355 + *)
2.356 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.357 + (*calc-head of subproblem*)
2.358 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.359 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.360 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.361 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.362 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.363 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.364 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.365 + (*solve-phase of the subproblem*)
2.366 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.367 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.368 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.369 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.370 + (*finish subproblem*)
2.371 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.372 + (*finish problem*)
2.373 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.374 +
2.375 + (*this checks the test for correctness..*)
2.376 + val ((pt,_),_) = get_calc 1;
2.377 + val p = get_pos 1 1;
2.378 + val (Form f, tac, asms) = pt_extract (pt, p);
2.379 + if term2str f = "[x = 1]" andalso p = ([], Res) then () else
2.380 + error "FE-interface.sml: diff.behav. in miniscript with mini-subpb";
2.381 + DEconstrCalcTree 1;
2.382 +
2.383 +
2.384 +"--------- solve_linear as rootpbl AUTO CompleteCalc ----";
2.385 +"--------- solve_linear as rootpbl AUTO CompleteCalc ----";
2.386 +"--------- solve_linear as rootpbl AUTO CompleteCalc ----";
2.387 + CalcTree
2.388 + [(["equality (1+-1*2+x=(0::real))", "solveFor x","solutions L"],
2.389 + ("Test",
2.390 + ["linear","univariate","equation","test"],
2.391 + ["Test","solve_linear"]))];
2.392 + Iterator 1;
2.393 + moveActiveRoot 1;
2.394 +getFormulaeFromTo 1 ([],Pbl) ([],Pbl) 999 false;
2.395 +
2.396 + autoCalculate 1 CompleteCalc;
2.397 + val (unc, del, gen) = (([],Pbl), ([],Pbl), ([],Res));
2.398 + getFormulaeFromTo 1 unc gen 1 (*only level 1*) false;
2.399 +
2.400 + val ((pt,_),_) = get_calc 1;
2.401 + val p = get_pos 1 1;
2.402 + val (Form f, tac, asms) = pt_extract (pt, p);
2.403 + if term2str f = "[x = 1]" andalso p = ([], Res) then () else
2.404 + error "FE-interface.sml: diff.behav. in solve_linear/rt AUTOCALCULATE ";
2.405 +DEconstrCalcTree 1;
2.406 +
2.407 +"--------- solve_linear as rootpbl AUTO CompleteHead/Calc ";
2.408 +"--------- solve_linear as rootpbl AUTO CompleteHead/Calc ";
2.409 +"--------- solve_linear as rootpbl AUTO CompleteHead/Calc ";
2.410 +(* ERROR: error in kernel ?? *)
2.411 + CalcTree
2.412 + [(["equality (1+-1*2+x=(0::real))", "solveFor x","solutions L"],
2.413 + ("Test",
2.414 + ["linear","univariate","equation","test"],
2.415 + ["Test","solve_linear"]))];
2.416 + Iterator 1;
2.417 + moveActiveRoot 1;
2.418 +
2.419 + autoCalculate 1 CompleteCalcHead;
2.420 + refFormula 1 (get_pos 1 1);
2.421 + val ((pt,p),_) = get_calc 1;
2.422 +
2.423 + autoCalculate 1 CompleteCalc;
2.424 + val ((pt,p),_) = get_calc 1;
2.425 + if p=([], Res) then () else
2.426 + error "FE-interface.sml: diff.behav. in solve_linear AUTOC Head/Calc ";
2.427 +DEconstrCalcTree 1;
2.428 +
2.429 +"--------- mini-subpbl AUTOCALCULATE CompleteCalc -------";
2.430 +"--------- mini-subpbl AUTOCALCULATE CompleteCalc -------";
2.431 +"--------- mini-subpbl AUTOCALCULATE CompleteCalc -------";
2.432 + CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
2.433 + ("Test", ["sqroot-test","univariate","equation","test"],
2.434 + ["Test","squ-equ-test-subpbl1"]))];
2.435 + Iterator 1;
2.436 + moveActiveRoot 1;
2.437 + autoCalculate 1 CompleteCalc;
2.438 + val ((pt,p),_) = get_calc 1; show_pt pt;
2.439 +(*
2.440 +getTactic 1 ([1],Frm);
2.441 +getTactic 1 ([1],Res);
2.442 +initContext 1 Thy_ ([1],Res);
2.443 +*)
2.444 + (*... returns calcChangedEvent with*)
2.445 + val (unc, del, gen) = (([],Pbl), ([],Pbl), ([],Res));
2.446 + getFormulaeFromTo 1 unc gen 0 (*only result*) false;
2.447 + getFormulaeFromTo 1 unc gen 1 (*only level 1*) false;
2.448 + getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
2.449 +
2.450 + val ((pt,_),_) = get_calc 1;
2.451 + val p = get_pos 1 1;
2.452 + val (Form f, tac, asms) = pt_extract (pt, p);
2.453 + if term2str f = "[x = 1]" andalso p = ([], Res) then () else
2.454 + error "FE-interface.sml: diff.behav. in mini-subpbl AUTOCALCULATE 6";
2.455 +DEconstrCalcTree 1;
2.456 +
2.457 +"--------- mini-subpbl AUTO CompleteCalcHead ------------";
2.458 +"--------- mini-subpbl AUTO CompleteCalcHead ------------";
2.459 +"--------- mini-subpbl AUTO CompleteCalcHead ------------";
2.460 + CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
2.461 + ("Test", ["sqroot-test","univariate","equation","test"],
2.462 + ["Test","squ-equ-test-subpbl1"]))];
2.463 + Iterator 1;
2.464 + moveActiveRoot 1;
2.465 + autoCalculate 1 CompleteCalcHead;
2.466 +
2.467 +val ((Nd (PblObj {env = NONE, fmz = (fm, ("Test", pblID, metID)), loc = (SOME (env, ctxt1), NONE),
2.468 + cell = NONE, ctxt = ctxt2, meth,
2.469 + spec = ("Test", ["sqroot-test", "univariate", "equation", "test"],
2.470 + ["Test", "squ-equ-test-subpbl1"]),
2.471 + probl, branch = TransitiveB, origin, ostate = Incomplete, result}, []),
2.472 + ([], Met)), []) = get_calc 1;
2.473 +if length meth = 3 andalso length probl = 3 (*just some items tested*) then ()
2.474 +else error "--- mini-subpbl AUTO CompleteCalcHead ---";
2.475 +DEconstrCalcTree 1;
2.476 +
2.477 +"--------- solve_linear as rootpbl AUTO CompleteModel ---";
2.478 +"--------- solve_linear as rootpbl AUTO CompleteModel ---";
2.479 +"--------- solve_linear as rootpbl AUTO CompleteModel ---";
2.480 + CalcTree
2.481 + [(["equality (1+-1*2+x=(0::real))", "solveFor x","solutions L"],
2.482 + ("Test",
2.483 + ["linear","univariate","equation","test"],
2.484 + ["Test","solve_linear"]))];
2.485 + Iterator 1;
2.486 + moveActiveRoot 1;
2.487 + autoCalculate 1 CompleteModel;
2.488 + refFormula 1 (get_pos 1 1);
2.489 +
2.490 +setProblem 1 ["linear","univariate","equation","test"];
2.491 +val pos = get_pos 1 1;
2.492 +setContext 1 pos (kestoreID2guh Pbl_["linear","univariate","equation","test"]);
2.493 + refFormula 1 (get_pos 1 1);
2.494 +
2.495 +setMethod 1 ["Test","solve_linear"];
2.496 +setContext 1 pos (kestoreID2guh Met_ ["Test","solve_linear"]);
2.497 + refFormula 1 (get_pos 1 1);
2.498 + val ((pt,_),_) = get_calc 1;
2.499 + if get_obj g_spec pt [] = ("e_domID",
2.500 + ["linear", "univariate","equation","test"],
2.501 + ["Test","solve_linear"]) then ()
2.502 + else error "FE-interface.sml: diff.behav. in setProblem, setMethod";
2.503 +
2.504 + autoCalculate 1 CompleteCalcHead;
2.505 + refFormula 1 (get_pos 1 1);
2.506 + autoCalculate 1 CompleteCalc;
2.507 + moveActiveDown 1;
2.508 + moveActiveDown 1;
2.509 + moveActiveDown 1;
2.510 + refFormula 1 (get_pos 1 1);
2.511 + val ((pt,_),_) = get_calc 1;
2.512 + val p = get_pos 1 1;
2.513 + val (Form f, tac, asms) = pt_extract (pt, p);
2.514 + if term2str f = "[x = 1]" andalso p = ([], Res) then () else
2.515 + error "FE-interface.sml: diff.behav. in mini-subpbl AUTOCALCULATE 6";
2.516 +DEconstrCalcTree 1;
2.517 +
2.518 +"--------- setContext..Thy ------------------------------";
2.519 +"--------- setContext..Thy ------------------------------";
2.520 +"--------- setContext..Thy ------------------------------";
2.521 + states:=[];
2.522 + CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
2.523 + ("Test", ["sqroot-test","univariate","equation","test"],
2.524 + ["Test","squ-equ-test-subpbl1"]))];
2.525 + Iterator 1; moveActiveRoot 1;
2.526 + autoCalculate 1 CompleteCalcHead;
2.527 + autoCalculate 1 (Step 1);
2.528 + val ((pt,p),_) = get_calc 1; show_pt pt; (*2 lines, OK*)
2.529 + (*
2.530 + setNextTactic 1 (Rewrite_Set "Test_simplify"); (*--> "thy_isac_Test-rls-Test_simplify"*)
2.531 + autoCalculate 1 (Step 1);
2.532 + val ((pt,p),_) = get_calc 1; show_pt pt;
2.533 + *)
2.534 +"-----^^^^^ and vvvvv do the same -----";
2.535 + setContext 1 p "thy_isac_Test-rls-Test_simplify";
2.536 + val ((pt,p),_) = get_calc 1; show_pt pt; (*2 lines, OK*)
2.537 +
2.538 + autoCalculate 1 (Step 1);
2.539 + setContext 1 p "thy_isac_Test-rls-Test_simplify";
2.540 + val (((pt,_),_), p) = (get_calc 1, get_pos 1 1);
2.541 + val (Form f, tac, asms) = pt_extract (pt, p);
2.542 + if p = ([1], Res) andalso term2str (get_obj g_res pt (fst p)) = "x + 1 + -1 * 2 = 0"
2.543 + then () else error "--- setContext..Thy --- autoCalculate 1 (Step 1) #1";
2.544 +
2.545 + autoCalculate 1 CompleteCalc;
2.546 + val (((pt,_),_), p) = (get_calc 1, get_pos 1 1);
2.547 + val (Form f, tac, asms) = pt_extract (pt, p);
2.548 +
2.549 + if term2str f = "[x = 1]" andalso p = ([], Res) then ()
2.550 + else error "--- setContext..Thy --- autoCalculate CompleteCalc";
2.551 + DEconstrCalcTree 1;
2.552 +
2.553 +"--------- mini-subpbl AUTOCALC CompleteToSubpbl --------";
2.554 +"--------- mini-subpbl AUTOCALC CompleteToSubpbl --------";
2.555 +"--------- mini-subpbl AUTOCALC CompleteToSubpbl --------";
2.556 + CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
2.557 + ("Test", ["sqroot-test","univariate","equation","test"],
2.558 + ["Test","squ-equ-test-subpbl1"]))];
2.559 + Iterator 1; moveActiveRoot 1;
2.560 + autoCalculate 1 CompleteToSubpbl;
2.561 + refFormula 1 (get_pos 1 1); (*<ISA> -1 + x = 0 </ISA>*);
2.562 + val ((pt,_),_) = get_calc 1;
2.563 + val str = pr_ptree pr_short pt;
2.564 + writeln str;
2.565 + if str = ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + -1 * 2 = 0\n"
2.566 + then () else
2.567 + error "FE-interface.sml: diff.behav. in mini-subpbl CompleteToSubpbl-1";
2.568 +
2.569 + autoCalculate 1 (Step 1); (*proceeds only, of NOT 1 step before subplb*)
2.570 + autoCalculate 1 CompleteToSubpbl;
2.571 + val ((pt,_),_) = get_calc 1;
2.572 + val str = pr_ptree pr_short pt;
2.573 + writeln str;
2.574 + autoCalculate 1 CompleteCalc; (*das geht ohnehin !*);
2.575 + val ((pt,_),_) = get_calc 1;
2.576 + val p = get_pos 1 1;
2.577 +
2.578 + val (Form f, tac, asms) = pt_extract (pt, p);
2.579 + if term2str f = "[x = 1]" andalso p = ([], Res) then () else
2.580 + error "FE-interface.sml: diff.behav. in mini-subpbl CompleteToSubpbl 1";
2.581 +DEconstrCalcTree 1;
2.582 +
2.583 +"--------- rat-eq + subpbl: no_met, NO solution dropped -";
2.584 +"--------- rat-eq + subpbl: no_met, NO solution dropped -";
2.585 +"--------- rat-eq + subpbl: no_met, NO solution dropped -";
2.586 + CalcTree
2.587 + [(["equality ((5*x)/(x - 2) - x/(x+2)=(4::real))", "solveFor x","solutions L"],
2.588 + ("RatEq", ["univariate","equation"], ["no_met"]))];
2.589 + Iterator 1;
2.590 + moveActiveRoot 1;
2.591 + fetchProposedTactic 1;
2.592 +
2.593 + setNextTactic 1 (Model_Problem);
2.594 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
2.595 +
2.596 + setNextTactic 1 (Specify_Theory "RatEq");
2.597 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
2.598 + setNextTactic 1 (Specify_Problem ["rational","univariate","equation"]);
2.599 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
2.600 + setNextTactic 1 (Specify_Method ["RatEq","solve_rat_equation"]);
2.601 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
2.602 + setNextTactic 1 (Apply_Method ["RatEq","solve_rat_equation"]);
2.603 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
2.604 + setNextTactic 1 (Rewrite_Set "RatEq_simplify");
2.605 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
2.606 + setNextTactic 1 (Rewrite_Set "norm_Rational");
2.607 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
2.608 + setNextTactic 1 (Rewrite_Set "RatEq_eliminate");
2.609 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
2.610 + (* __________ for "12 * x + 4 * x ^^^ 2 = 4 * (-4 + x ^^^ 2)"*)
2.611 + setNextTactic 1 (Subproblem ("PolyEq", ["normalize","polynomial",
2.612 + "univariate","equation"]));
2.613 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
2.614 + setNextTactic 1 (Model_Problem );
2.615 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
2.616 + setNextTactic 1 (Specify_Theory "PolyEq");
2.617 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
2.618 + setNextTactic 1 (Specify_Problem ["normalize","polynomial",
2.619 + "univariate","equation"]);
2.620 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
2.621 + setNextTactic 1 (Specify_Method ["PolyEq","normalize_poly"]);
2.622 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
2.623 + setNextTactic 1 (Apply_Method ["PolyEq","normalize_poly"]);
2.624 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
2.625 + setNextTactic 1 (Rewrite ("all_left",""));
2.626 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
2.627 + setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "make_ratpoly_in"));
2.628 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
2.629 + (* __________ for "16 + 12 * x = 0"*)
2.630 + setNextTactic 1 (Subproblem ("PolyEq",
2.631 + ["degree_1","polynomial","univariate","equation"]));
2.632 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
2.633 + setNextTactic 1 (Model_Problem );
2.634 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
2.635 + setNextTactic 1 (Specify_Theory "PolyEq");
2.636 + (*------------- some trials in the problem-hierarchy ---------------*)
2.637 + setNextTactic 1 (Specify_Problem ["linear","univariate","equation"]);
2.638 + autoCalculate 1 (Step 1); fetchProposedTactic 1; (*<ERROR> helpless </ERROR> !!!*)
2.639 + setNextTactic 1 (Refine_Problem ["univariate","equation"]);
2.640 + (*------------------------------------------------------------------*)
2.641 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
2.642 + setNextTactic 1 (Specify_Method ["PolyEq","solve_d1_polyeq_equation"]);
2.643 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
2.644 + setNextTactic 1 (Apply_Method ["PolyEq","solve_d1_polyeq_equation"]);
2.645 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
2.646 + setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "d1_polyeq_simplify"));
2.647 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
2.648 + setNextTactic 1 (Rewrite_Set "polyeq_simplify");
2.649 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
2.650 + (*==================================================================*)
2.651 + setNextTactic 1 Or_to_List;
2.652 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
2.653 + setNextTactic 1 (Check_elementwise "Assumptions");
2.654 + (*WAS: exception Match raised (line 1218 of ".../script.sml")*)
2.655 +"~~~~~ fun setNextTactic, args:"; val ((cI:calcID), tac) = (1, (Check_elementwise "Assumptions"));
2.656 +val ((pt, _), _) = get_calc cI;
2.657 +val ip = get_pos cI 1;
2.658 +(*locatetac tac (pt, ip) WAS: exception Match raised (line 1218 of ".../script.sml")*)
2.659 +"~~~~~ fun locatetac, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, ip));
2.660 +val (mI,m) = mk_tac'_ tac;
2.661 +val Appl m = applicable_in p pt m;
2.662 +member op = specsteps mI (*false*);
2.663 +(* loc_solve_ (mI,m) ptp WAS: exception Match raised (line 1218 of ".../script.sml")*)
2.664 +"~~~~~ fun loc_solve_, args:"; val (m, (pt,pos)) = ((mI,m), ptp);
2.665 +(*solve m (pt, pos); WAS: exception Match raised (line 1218 of ".../script.sml")*)
2.666 +"~~~~~ fun solve, args:"; val ((mI,m), (pt, po as (p,p_))) = (m, (pt, pos));
2.667 +e_metID = get_obj g_metID pt (par_pblobj pt p) (*false*);
2.668 + val thy' = get_obj g_domID pt (par_pblobj pt p);
2.669 + val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
2.670 + val d = e_rls;
2.671 +(*locate_gen (thy',srls) m (pt,(p,p_)) (sc,d) is;
2.672 + WAS: exception Match raised (line 1218 of "isabisac/src/Tools/isac/Interpret/script.sml"*)
2.673 +"~~~~~ fun locate_gen, args:"; val ((ts as (thy',srls)), (m:tac_), ((pt,p):ptree * pos'),
2.674 + (scr as Script (h $ body),d), (ScrState (E,l,a,v,S,b), ctxt)) =
2.675 + ((thy',srls), m ,(pt,(p,p_)) ,(sc,d) ,is); (* locate_gen 2nd pattern *)
2.676 +val thy = assoc_thy thy';
2.677 +l = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*false*);
2.678 +(*WAS val NasApp _ =(astep_up (thy',srls,scr,d) ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]) )
2.679 + ... Assoc ... is correct*)
2.680 +"~~~~~ and astep_up, args:"; val ((ys as (_,_,Script sc,_)), ((E,l,a,v,S,b),ss)) =
2.681 + ((thy',srls,scr,d), ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]));
2.682 +1 < length l (*true*);
2.683 +val up = drop_last l;
2.684 + term2str (go up sc);
2.685 + (go up sc);
2.686 +(*WAS val NasNap _ = ass_up ys ((E,up,a,v,S,b),ss) (go up sc)
2.687 + ... ???? ... is correct*)
2.688 +"~~~~~ fun ass_up, args:"; val ((ys as (y,s,Script sc,d)), (is as (E,l,a,v,S,b),ss),
2.689 + (Const ("HOL.Let",_) $ _)) = (ys, ((E,up,a,v,S,b),ss), (go up sc));
2.690 + val l = drop_last l; (*comes from e, goes to Abs*)
2.691 + val (Const ("HOL.Let",_) $ e $ (Abs (i,T,body))) = go l sc;
2.692 + val i = mk_Free (i, T);
2.693 + val E = upd_env E (i, v);
2.694 +(*Type error ...: Can't unify _a to pos * pos_ (Incompatible types)*)
2.695 +val [(tac_, mout, ptree, pos', xxx)] = ss;
2.696 +val ss = [(tac_, mout, ptree, pos', []:(pos * pos_) list)];
2.697 +(*WAS val NasApp iss = assy (((y,s),d),Aundef) ((E, l@[R,D], a,v,S,b),ss) body
2.698 + ... Assoc ... is correct*)
2.699 +"~~~~~ fun assy, args:"; val ((((thy',sr),d),ap), (is as (E,l,a,v,S,b), (m,_,pt,(p,p_),c)::ss), t) =
2.700 + ((((y,s),d),Aundef), ((E, l@[R,D], a,v,S,b),ss), body);
2.701 +val (a', STac stac) = handle_leaf "locate" thy' sr E a v t
2.702 + val ctxt = get_ctxt pt (p,p_)
2.703 + val p' = lev_on p : pos;
2.704 +(* WAS val NotAss = assod pt d m stac
2.705 + ... Ass ... is correct*)
2.706 +"~~~~~ fun assod, args:"; val (pt, _, (m as Check_elementwise' (consts,_,(consts_chkd,_))),
2.707 + (Const ("Script.Check'_elementwise",_) $ consts' $ _)) = (pt, d, m, stac);
2.708 +consts = consts' (*WAS false*);
2.709 +(*==================================================================*)
2.710 +
2.711 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
2.712 + setNextTactic 1 (Check_Postcond ["degree_1","polynomial",
2.713 + "univariate","equation"]);
2.714 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
2.715 + setNextTactic 1 (Check_Postcond ["normalize","polynomial",
2.716 + "univariate","equation"]);
2.717 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
2.718 + setNextTactic 1 (Check_Postcond ["rational","univariate","equation"]);
2.719 + val (ptp,_) = get_calc 1;
2.720 + val (Form t,_,_) = pt_extract ptp;
2.721 + if get_pos 1 1 = ([], Res) andalso term2str t = "[x = -4 / 3]" then ()
2.722 + else writeln "FE-inteface.sml: diff.behav. in rat-eq + subpbl: no_met, NO ..";
2.723 +DEconstrCalcTree 1;
2.724 +
2.725 +"--------- tryMatchProblem, tryRefineProblem ------------";
2.726 +"--------- tryMatchProblem, tryRefineProblem ------------";
2.727 +"--------- tryMatchProblem, tryRefineProblem ------------";
2.728 +(*{\bf\UC{Having \isac{} Refine the Problem
2.729 + * Automatically}\label{SPECIFY:refine-auto}\\} test match and refine with
2.730 + * x^^^2 + 4*x + 5 = 2
2.731 +see isac.bridge.TestSpecify#testMatchRefine*)
2.732 + CalcTree
2.733 + [(["equality (x^2 + 4*x + 5 = (2::real))", "solveFor x","solutions L"],
2.734 + ("Isac",
2.735 + ["univariate","equation"],
2.736 + ["no_met"]))];
2.737 + Iterator 1;
2.738 + moveActiveRoot 1;
2.739 +
2.740 + fetchProposedTactic 1;
2.741 + setNextTactic 1 (Model_Problem );
2.742 + (*..this tactic should be done 'tacitly', too !*)
2.743 +
2.744 +(*
2.745 +autoCalculate 1 CompleteCalcHead;
2.746 +checkContext 1 ([],Pbl) "pbl_equ_univ";
2.747 +checkContext 1 ([],Pbl) (kestoreID2guh Pbl_ ["univariate","equation"]);
2.748 +*)
2.749 +
2.750 + autoCalculate 1 (Step 1);
2.751 +
2.752 + fetchProposedTactic 1;
2.753 + setNextTactic 1 (Add_Given "equality (x ^^^ 2 + 4 * x + 5 = (2::real))");
2.754 + autoCalculate 1 (Step 1);
2.755 +
2.756 + "--------- we go into the ProblemBrowser (_NO_ pblID selected) -";
2.757 +initContext 1 Pbl_ ([],Pbl);
2.758 +initContext 1 Met_ ([],Pbl);
2.759 +
2.760 + "--------- this match will show some incomplete items: ---------";
2.761 +checkContext 1 ([],Pbl) (kestoreID2guh Pbl_ ["univariate","equation"]);
2.762 +checkContext 1 ([],Pbl) (kestoreID2guh Met_ ["LinEq", "solve_lineq_equation"]);
2.763 +
2.764 +
2.765 + fetchProposedTactic 1;
2.766 + setNextTactic 1 (Add_Given "solveFor x"); autoCalculate 1 (Step 1);
2.767 +
2.768 + fetchProposedTactic 1;
2.769 + setNextTactic 1 (Add_Find "solutions L"); autoCalculate 1 (Step 1);
2.770 +
2.771 + "--------- this is a matching model (all items correct): -------";
2.772 +checkContext 1 ([],Pbl) (kestoreID2guh Pbl_ ["univariate","equation"]);
2.773 + "--------- this is a NOT matching model (some 'false': ---------";
2.774 +checkContext 1 ([],Pbl)(kestoreID2guh Pbl_["linear","univariate","equation"]);
2.775 +
2.776 + "--------- find out a matching problem: ------------------------";
2.777 + "--------- find out a matching problem (FAILING: no new pbl) ---";
2.778 + refineProblem 1([],Pbl)(pblID2guh ["linear","univariate","equation"]);
2.779 +
2.780 + "--------- find out a matching problem (SUCCESSFUL) ------------";
2.781 + refineProblem 1 ([],Pbl) (pblID2guh ["univariate","equation"]);
2.782 +
2.783 + "--------- tryMatch, tryRefine did not change the calculation -";
2.784 + "--------- this is done by <TRANSFER> on the pbl-browser: ------";
2.785 + setNextTactic 1 (Specify_Problem ["normalize","polynomial",
2.786 + "univariate","equation"]);
2.787 + autoCalculate 1 (Step 1);
2.788 +(*WN050904 fetchProposedTactic again --> Specify_Problem ["normalize",...
2.789 + and Specify_Theory skipped in comparison to below ---^^^-inserted *)
2.790 +(*------------vvv-inserted-----------------------------------------------*)
2.791 + fetchProposedTactic 1;
2.792 + setNextTactic 1 (Specify_Problem ["normalize","polynomial",
2.793 + "univariate","equation"]);
2.794 + autoCalculate 1 (Step 1);
2.795 +
2.796 +(*and Specify_Theory skipped by fetchProposedTactic ?!?*)
2.797 +
2.798 + fetchProposedTactic 1;
2.799 + setNextTactic 1 (Specify_Method ["PolyEq","normalize_poly"]);
2.800 + autoCalculate 1 (Step 1);
2.801 +
2.802 + fetchProposedTactic 1;
2.803 + setNextTactic 1 (Apply_Method ["PolyEq","normalize_poly"]);
2.804 +
2.805 + autoCalculate 1 CompleteCalc;
2.806 +
2.807 + val ((pt,_),_) = get_calc 1;
2.808 + show_pt pt;
2.809 + val p = get_pos 1 1;
2.810 + val (Form f, tac, asms) = pt_extract (pt, p);
2.811 +(*========== inhibit exn 110719 ================================================
2.812 + if term2str f = "[x = -1, x = -3]" andalso p = ([], Res) then () else
2.813 + error "FE-interface.sml: diff.behav. in tryMatchProblem, tryRefine";
2.814 +========== inhibit exn 110719 ================================================*)
2.815 +
2.816 +(*------------^^^-inserted-----------------------------------------------*)
2.817 +(*WN050904 the fetchProposedTactic's below may not have worked like that
2.818 + before, too, because there was no check*)
2.819 + fetchProposedTactic 1;
2.820 + setNextTactic 1 (Specify_Theory "PolyEq");
2.821 + autoCalculate 1 (Step 1);
2.822 +
2.823 + fetchProposedTactic 1;
2.824 + setNextTactic 1 (Specify_Method ["PolyEq","normalize_poly"]);
2.825 + autoCalculate 1 (Step 1);
2.826 +
2.827 + fetchProposedTactic 1;
2.828 + "--------- now the calc-header is ready for enter 'solving' ----";
2.829 + autoCalculate 1 CompleteCalc;
2.830 +
2.831 + val ((pt,_),_) = get_calc 1;
2.832 + rootthy pt;
2.833 + show_pt pt;
2.834 + val p = get_pos 1 1;
2.835 +
2.836 +(*============ inhibit exn AK110719 ==============================================
2.837 +(* ERROR: execption Bind raised *)
2.838 + val (Form f, tac, asms) = pt_extract (pt, p);
2.839 + if term2str f = "[x = -1, x = -3]" andalso p = ([], Res) then () else
2.840 + error "FE-interface.sml: diff.behav. in tryMatchProblem, tryRefine";
2.841 +============ inhibit exn AK110719 ==============================================*)
2.842 +
2.843 +(* (* AK110727 Debugging (to be continued) *)
2.844 + asms; (*term list (!)*)
2.845 + print_depth 99;
2.846 + pt_extract (pt, p); (* ptform * tac option * term list*)
2.847 + (Form f, tac, asms);
2.848 + val (myval,myval2,myval3s) = pt_extract (pt,p);
2.849 +
2.850 +"~~~~~ fun pt_extract, args:"; val ((pt, pos as (p,p_(*Frm,Pbl*)))) = ((pt, p));
2.851 + val ppobj = get_obj I pt p;
2.852 + is_pblobj ppobj; (*true*)
2.853 + pt_model ppobj p_;
2.854 + val tac = g_tac ppobj;
2.855 + (f, SOME tac, []) (* term * tac option * 'a list (!) *)
2.856 +*)
2.857 +
2.858 +DEconstrCalcTree 1;
2.859 +
2.860 +"--------- modifyCalcHead, resetCalcHead, modelProblem --";
2.861 +"--------- modifyCalcHead, resetCalcHead, modelProblem --";
2.862 +"--------- modifyCalcHead, resetCalcHead, modelProblem --";
2.863 + CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
2.864 + ("Test", ["sqroot-test","univariate","equation","test"],
2.865 + ["Test","squ-equ-test-subpbl1"]))];
2.866 + Iterator 1;
2.867 + moveActiveRoot 1;
2.868 +
2.869 + modifyCalcHead 1 (([],Pbl),(*the position from refFormula*)
2.870 + "solve (x+1=2, x)",(*the headline*)
2.871 + [Given ["equality (x+1=(2::real))", "solveFor x"],
2.872 + Find ["solutions L"](*,Relate []*)],
2.873 + Pbl,
2.874 + ("Test",
2.875 + ["sqroot-test","univariate","equation","test"],
2.876 + ["Test","squ-equ-test-subpbl1"]));
2.877 +
2.878 +val ((Nd (PblObj {env = NONE,
2.879 + fmz = (fm, tpm),
2.880 + loc = (SOME scrst_ctxt, NONE),
2.881 + ctxt,
2.882 + cell = NONE,
2.883 + meth,
2.884 + spec = (thy,
2.885 + ["sqroot-test", "univariate", "equation", "test"],
2.886 + ["Test", "squ-equ-test-subpbl1"]),
2.887 + probl,
2.888 + branch = TransitiveB,
2.889 + origin,
2.890 + ostate = Incomplete,
2.891 + result},
2.892 + []),
2.893 + ([], Pbl)),
2.894 + []) = get_calc 1;
2.895 +(*WN110622: is the same as in 2002, but shouldn't be probl = [3 items?]*)
2.896 +if length meth = 0 andalso length probl = 0 (*just some items tested*) then ()
2.897 +else error "--- modifyCalcHead, resetCalcHead, modelProblem 1 --";
2.898 +
2.899 +resetCalcHead 1;
2.900 +modelProblem 1;
2.901 +
2.902 +get_calc 1;
2.903 +val ((Nd (PblObj {env = NONE,
2.904 + fmz = (fm, tpm),
2.905 + loc = (SOME scrst_ctxt, NONE),
2.906 + ctxt,
2.907 + cell = NONE,
2.908 + meth,
2.909 + spec = ("e_domID", ["e_pblID"], ["e_metID"]),
2.910 + probl,
2.911 + branch = TransitiveB,
2.912 + origin,
2.913 + ostate = Incomplete,
2.914 + result},
2.915 + []),
2.916 + ([], Pbl)),
2.917 + []) = get_calc 1;
2.918 +if length meth = 3 andalso length probl = 3 (*just some items tested*) then ()
2.919 +else error "--- modifyCalcHead, resetCalcHead, modelProblem 2 --";
2.920 +
2.921 +"--------- maximum-example, UC: Modeling an example -----";
2.922 +"--------- maximum-example, UC: Modeling an example -----";
2.923 +"--------- maximum-example, UC: Modeling an example -----";
2.924 +(* {\bf\UC{Editing the Model}\label{SPECIFY:enter}\label{SPECIFY:check}\\}
2.925 +see isac.bridge.TestModel#testEditItems
2.926 +*)
2.927 + val elems = ["fixedValues [r=Arbfix]","maximum A","valuesFor [a,b]",
2.928 + "relations [A=a*b, (a/2)^2 + (b/2)^2 = r^2]",
2.929 + "relations [A=a*b, (a/2)^2 + (b/2)^2 = r^2]",
2.930 + "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]",
2.931 + (*^^^ these are the elements for the root-problem (in variants)*)
2.932 + (*vvv these are elements required for subproblems*)
2.933 + "boundVariable a","boundVariable b","boundVariable alpha",
2.934 + "interval {x::real. 0 <= x & x <= 2*r}",
2.935 + "interval {x::real. 0 <= x & x <= 2*r}",
2.936 + "interval {x::real. 0 <= x & x <= pi}",
2.937 + "errorBound (eps=(0::real))"]
2.938 + (*specifying is not interesting for this example*)
2.939 + val spec = ("DiffApp", ["maximum_of","function"],
2.940 + ["DiffApp","max_by_calculus"]);
2.941 + (*the empty model with descriptions for user-guidance by Model_Problem*)
2.942 + val empty_model = [Given ["fixedValues []"],
2.943 + Find ["maximum", "valuesFor"],
2.944 + Relate ["relations []"]];
2.945 + DEconstrCalcTree 1;
2.946 +
2.947 +"#################################################################";
2.948 +
2.949 + CalcTree [(elems, spec)];
2.950 + Iterator 1;
2.951 + moveActiveRoot 1;
2.952 + refFormula 1 (get_pos 1 1);
2.953 + (*this gives a completely empty model*)
2.954 +
2.955 + fetchProposedTactic 1;
2.956 +(*fill the CalcHead with Descriptions...*)
2.957 + setNextTactic 1 (Model_Problem );
2.958 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.959 +
2.960 + (*user input is !!!!!EITHER!!!!! _some_ (at least one) items of the model
2.961 + !!!!!OR!!!!! _one_ part of the specification !!!!!!!!!!!!!*)
2.962 + (*input of two items, 'fixedValues [r=Arbfix]' and 'maximum b'...*)
2.963 + modifyCalcHead 1 (([],Pbl) (*position, from previous refFormula*),
2.964 + "Problem (DiffApp.thy, [maximum_of, function])",
2.965 + (*the head-form ^^^ is not used for input here*)
2.966 + [Given ["fixedValues [r=Arbfix]"(*new input*)],
2.967 + Find ["maximum b"(*new input*), "valuesFor"],
2.968 + Relate ["relations"]],
2.969 + (*input (Arbfix will dissappear soon)*)
2.970 + Pbl (*belongsto*),
2.971 + e_spec (*no input to the specification*));
2.972 +
2.973 + (*the user does not know, what 'superfluous' for 'maximum b' may mean
2.974 + and asks what to do next*)
2.975 + fetchProposedTactic 1;
2.976 + (*the student follows the advice*)
2.977 + setNextTactic 1 (Add_Find "maximum A"); (*FIXME.17.11.03: does not yet work*)
2.978 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.979 +
2.980 + (*this input completes the model*)
2.981 + modifyCalcHead 1 (([],Pbl), "not used here",
2.982 + [Given ["fixedValues [r=Arbfix]"],
2.983 + Find ["maximum A", "valuesFor [a,b]"(*new input*)],
2.984 + Relate ["relations [A=a*b, \
2.985 + \(a/2)^2 + (b/2)^2 = r^2]"]], Pbl, e_spec);
2.986 +
2.987 + (*specification is not interesting and should be skipped by the dialogguide;
2.988 + !!!!!!!!!!!!!!!!!!!! input of ONE part at a time !!!!!!!!!!!!!!!!!!!!!!*)
2.989 + modifyCalcHead 1 (([],Pbl), "not used here",
2.990 + [Given ["fixedValues [r=Arbfix]"],
2.991 + Find ["maximum A", "valuesFor [a,b]"(*new input*)],
2.992 + Relate ["relations [A=a*b, \
2.993 + \(a/2)^2 + (b/2)^2 = r^2]"]], Pbl,
2.994 + ("DiffApp", ["e_pblID"], ["e_metID"]));
2.995 + modifyCalcHead 1 (([],Pbl), "not used here",
2.996 + [Given ["fixedValues [r=Arbfix]"],
2.997 + Find ["maximum A", "valuesFor [a,b]"(*new input*)],
2.998 + Relate ["relations [A=a*b, \
2.999 + \(a/2)^2 + (b/2)^2 = r^2]"]], Pbl,
2.1000 + ("DiffApp", ["maximum_of","function"],
2.1001 + ["e_metID"]));
2.1002 + modifyCalcHead 1 (([],Pbl), "not used here",
2.1003 + [Given ["fixedValues [r=Arbfix]"],
2.1004 + Find ["maximum A", "valuesFor [a,b]"(*new input*)],
2.1005 + Relate ["relations [A=a*b, \
2.1006 + \(a/2)^2 + (b/2)^2 = r^2]"]], Pbl,
2.1007 + ("DiffApp", ["maximum_of","function"],
2.1008 + ["DiffApp","max_by_calculus"]));
2.1009 + (*this final calcHead now has STATUS 'complete' !*)
2.1010 + DEconstrCalcTree 1;
2.1011 +
2.1012 +"--------- solve_linear from pbl-hierarchy --------------";
2.1013 +"--------- solve_linear from pbl-hierarchy --------------";
2.1014 +"--------- solve_linear from pbl-hierarchy --------------";
2.1015 + val (fmz, sp) = ([], ("", ["linear","univariate","equation","test"], []));
2.1016 + CalcTree [(fmz, sp)];
2.1017 + Iterator 1; moveActiveRoot 1;
2.1018 + refFormula 1 (get_pos 1 1);
2.1019 + modifyCalcHead 1 (([],Pbl),"solve (1+-1*2+x=(0::real))",
2.1020 + [Given ["equality (1+-1*2+x=(0::real))", "solveFor x"],
2.1021 + Find ["solutions L"]],
2.1022 + Pbl,
2.1023 + ("Test", ["linear","univariate","equation","test"],
2.1024 + ["Test","solve_linear"]));
2.1025 + autoCalculate 1 CompleteCalc;
2.1026 + refFormula 1 (get_pos 1 1);
2.1027 + val ((pt,_),_) = get_calc 1;
2.1028 + val p = get_pos 1 1;
2.1029 + val (Form f, tac, asms) = pt_extract (pt, p);
2.1030 + if term2str f = "[x = 1]" andalso p = ([], Res)
2.1031 + andalso terms2str asms = "[\"matches (?a = ?b) (1 + -1 * 2 + x = 0)\"]" then ()
2.1032 + else error "FE-interface.sml: diff.behav. in from pbl -hierarchy";
2.1033 + DEconstrCalcTree 1;
2.1034 +
2.1035 +"--------- solve_linear as in an algebra system (CAS)----";
2.1036 +"--------- solve_linear as in an algebra system (CAS)----";
2.1037 +"--------- solve_linear as in an algebra system (CAS)----";
2.1038 + val (fmz, sp) = ([], ("", [], []));
2.1039 + CalcTree [(fmz, sp)];
2.1040 + Iterator 1; moveActiveRoot 1;
2.1041 + modifyCalcHead 1 (([],Pbl),"solveTest (1+-1*2+x=0,x)", [], Pbl, ("", [], []));
2.1042 + autoCalculate 1 CompleteCalc;
2.1043 + refFormula 1 (get_pos 1 1);
2.1044 + val ((pt,_),_) = get_calc 1;
2.1045 + val p = get_pos 1 1;
2.1046 + val (Form f, tac, asms) = pt_extract (pt, p);
2.1047 + if term2str f = "[x = 1]" andalso p = ([], Res)
2.1048 + andalso terms2str asms = "[\"matches (?a = ?b) (1 + -1 * 2 + x = 0)\"]" then ()
2.1049 + else error "FE-interface.sml: diff.behav. in from pbl -hierarchy";
2.1050 +DEconstrCalcTree 1;
2.1051 +
2.1052 +"--------- interSteps: on 'miniscript with mini-subpbl' -";
2.1053 +"--------- interSteps: on 'miniscript with mini-subpbl' -";
2.1054 +"--------- interSteps: on 'miniscript with mini-subpbl' -";
2.1055 + CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
2.1056 + ("Test", ["sqroot-test","univariate","equation","test"],
2.1057 + ["Test","squ-equ-test-subpbl1"]))];
2.1058 + Iterator 1;
2.1059 + moveActiveRoot 1;
2.1060 + autoCalculate 1 CompleteCalc;
2.1061 + val ((pt,_),_) = get_calc 1;
2.1062 + show_pt pt;
2.1063 +
2.1064 + (*UC\label{SOLVE:INFO:intermediate-steps}*)
2.1065 + interSteps 1 ([2],Res);
2.1066 + val ((pt,_),_) = get_calc 1; show_pt pt (*new ([2,1],Frm)..([2,6],Res)*);
2.1067 + val (unc, del, gen) = (([1],Res),([1],Res),([2,6],Res));
2.1068 + getFormulaeFromTo 1 unc gen 1 false;
2.1069 +
2.1070 + (*UC\label{SOLVE:INFO:intermediate-steps}*)
2.1071 + interSteps 1 ([3,2],Res);
2.1072 + val ((pt,_),_) = get_calc 1; show_pt pt (*new ([3,2,1],Frm)..([3,2,2],Res)*);
2.1073 + val (unc, del, gen) = (([3,1],Res),([3,1],Res),([3,2,2],Res));
2.1074 + getFormulaeFromTo 1 unc gen 1 false;
2.1075 +
2.1076 + (*UC\label{SOLVE:INFO:intermediate-steps}*)
2.1077 + interSteps 1 ([3],Res) (*no new steps in subproblems*);
2.1078 + val (unc, del, gen) = (([3],Pbl),([3],Pbl),([3,2],Res));
2.1079 + getFormulaeFromTo 1 unc gen 1 false;
2.1080 +
2.1081 + (*UC\label{SOLVE:INFO:intermediate-steps}*)
2.1082 + interSteps 1 ([],Res) (*no new steps in subproblems*);
2.1083 + val (unc, del, gen) = (([],Pbl),([],Pbl),([4],Res));
2.1084 + getFormulaeFromTo 1 unc gen 1 false;
2.1085 +DEconstrCalcTree 1;
2.1086 +
2.1087 +"--------- getTactic, fetchApplicableTactics ------------";
2.1088 +"--------- getTactic, fetchApplicableTactics ------------";
2.1089 +"--------- getTactic, fetchApplicableTactics ------------";
2.1090 + CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
2.1091 + ("Test", ["sqroot-test","univariate","equation","test"],
2.1092 + ["Test","squ-equ-test-subpbl1"]))];
2.1093 + Iterator 1; moveActiveRoot 1;
2.1094 + autoCalculate 1 CompleteCalc;
2.1095 + val ((pt,_),_) = get_calc 1;
2.1096 + show_pt pt;
2.1097 +
2.1098 + (*UC\label{SOLVE:HIDE:getTactic}*)
2.1099 + getTactic 1 ([],Pbl);
2.1100 + getTactic 1 ([1],Res);
2.1101 + getTactic 1 ([3],Pbl);
2.1102 + getTactic 1 ([3,1],Frm);
2.1103 + getTactic 1 ([3],Res);
2.1104 + getTactic 1 ([],Res);
2.1105 +
2.1106 +(*UC\label{SOLVE:MANUAL:TACTIC:listall}*)
2.1107 + fetchApplicableTactics 1 99999 ([],Pbl);
2.1108 + fetchApplicableTactics 1 99999 ([1],Res);
2.1109 + fetchApplicableTactics 1 99999 ([3],Pbl);
2.1110 + fetchApplicableTactics 1 99999 ([3,1],Res);
2.1111 + fetchApplicableTactics 1 99999 ([3],Res);
2.1112 + fetchApplicableTactics 1 99999 ([],Res);
2.1113 +DEconstrCalcTree 1;
2.1114 +
2.1115 +"--------- getAssumptions, getAccumulatedAsms -----------";
2.1116 +"--------- getAssumptions, getAccumulatedAsms -----------";
2.1117 +"--------- getAssumptions, getAccumulatedAsms -----------";
2.1118 +CalcTree
2.1119 +[(["equality (x/(x^2 - 6*x+9) - 1/(x^2 - 3*x) =1/x)",
2.1120 + "solveFor x","solutions L"],
2.1121 + ("RatEq",["univariate","equation"],["no_met"]))];
2.1122 +Iterator 1; moveActiveRoot 1;
2.1123 +autoCalculate 1 CompleteCalc;
2.1124 +val ((pt,_),_) = get_calc 1;
2.1125 +val p = get_pos 1 1;
2.1126 +val (Form f, tac, asms) = pt_extract (pt, p);
2.1127 +if map term2str asms =
2.1128 + ["True |\n~ lhs ((3 + -1 * x + x ^^^ 2) * x =\n 1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)) is_poly_in x", "-6 * x + 5 * x ^^^ 2 = 0",
2.1129 + "lhs (-6 * x + 5 * x ^^^ 2 = 0) is_poly_in x",
2.1130 + "lhs (-6 * x + 5 * x ^^^ 2 = 0) has_degree_in x = 2",
2.1131 + "9 * x + -6 * x ^^^ 2 + x ^^^ 3 ~= 0"]
2.1132 +andalso term2str f = "[-6 * x + 5 * x ^^^ 2 = 0]" andalso p = ([], Res) then ()
2.1133 +else error "TODO compare 2002--2011";
2.1134 +
2.1135 +(*UC\label{SOLVE:HELP:assumptions}*)
2.1136 +getAssumptions 1 ([3], Res);
2.1137 +getAssumptions 1 ([5], Res);
2.1138 +(*UC\label{SOLVE:HELP:assumptions-origin} WN0502 still without positions*)
2.1139 +getAccumulatedAsms 1 ([3], Res);
2.1140 +getAccumulatedAsms 1 ([5], Res);
2.1141 +DEconstrCalcTree 1;
2.1142 +
2.1143 +"--------- arbitrary combinations of steps --------------";
2.1144 +"--------- arbitrary combinations of steps --------------";
2.1145 +"--------- arbitrary combinations of steps --------------";
2.1146 + CalcTree (*start of calculation, return No.1*)
2.1147 + [(["equality (1+-1*2+x=(0::real))", "solveFor x","solutions L"],
2.1148 + ("Test",
2.1149 + ["linear","univariate","equation","test"],
2.1150 + ["Test","solve_linear"]))];
2.1151 + Iterator 1; moveActiveRoot 1;
2.1152 +
2.1153 + fetchProposedTactic 1;
2.1154 + (*ERROR get_calc 1 not existent*)
2.1155 + setNextTactic 1 (Model_Problem );
2.1156 + autoCalculate 1 (Step 1);
2.1157 + fetchProposedTactic 1;
2.1158 + fetchProposedTactic 1;
2.1159 +
2.1160 + setNextTactic 1 (Add_Find "solutions L");
2.1161 + setNextTactic 1 (Add_Find "solutions L");
2.1162 +
2.1163 + autoCalculate 1 (Step 1);
2.1164 + autoCalculate 1 (Step 1);
2.1165 +
2.1166 + setNextTactic 1 (Specify_Theory "Test");
2.1167 + fetchProposedTactic 1;
2.1168 + autoCalculate 1 (Step 1);
2.1169 +
2.1170 + autoCalculate 1 (Step 1);
2.1171 + autoCalculate 1 (Step 1);
2.1172 + autoCalculate 1 (Step 1);
2.1173 + autoCalculate 1 (Step 1);
2.1174 +(*------------------------- end calc-head*)
2.1175 +
2.1176 + fetchProposedTactic 1;
2.1177 + setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "isolate_bdv"));
2.1178 + autoCalculate 1 (Step 1);
2.1179 +
2.1180 + setNextTactic 1 (Rewrite_Set "Test_simplify");
2.1181 + fetchProposedTactic 1;
2.1182 + autoCalculate 1 (Step 1);
2.1183 +
2.1184 + autoCalculate 1 CompleteCalc;
2.1185 + val ((pt,_),_) = get_calc 1;
2.1186 + val p = get_pos 1 1;
2.1187 + val (Form f, tac, asms) = pt_extract (pt, p);
2.1188 + if term2str f = "[x = 1]" andalso p = ([], Res) then () else
2.1189 + error "FE-interface.sml: diff.behav. in combinations of steps";
2.1190 +DEconstrCalcTree 1;
2.1191 +
2.1192 +"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}right";
2.1193 +"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}right";
2.1194 +"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}right";
2.1195 + CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
2.1196 + ("Test", ["sqroot-test","univariate","equation","test"],
2.1197 + ["Test","squ-equ-test-subpbl1"]))];
2.1198 + Iterator 1;
2.1199 + moveActiveRoot 1;
2.1200 + autoCalculate 1 CompleteCalcHead;
2.1201 + autoCalculate 1 (Step 1);
2.1202 + autoCalculate 1 (Step 1);
2.1203 + appendFormula 1 "-1 + x = 0";
2.1204 + (*... returns calcChangedEvent with*)
2.1205 + val (unc, del, gen) = (([1],Res), ([1],Res), ([2],Res));
2.1206 + getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
2.1207 +
2.1208 + val ((pt,_),_) = get_calc 1;
2.1209 + val p = get_pos 1 1;
2.1210 + val (Form f, tac, asms) = pt_extract (pt, p);
2.1211 + if term2str f = "-1 + x = 0" andalso p = ([2], Res) then () else
2.1212 + error "FE-interface.sml: diff.behav. in FORMULA:enter} right";
2.1213 +DEconstrCalcTree 1;
2.1214 +
2.1215 +"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}other";
2.1216 +"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}other";
2.1217 +"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}other";
2.1218 + CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
2.1219 + ("Test", ["sqroot-test","univariate","equation","test"],
2.1220 + ["Test","squ-equ-test-subpbl1"]))];
2.1221 + Iterator 1;
2.1222 + moveActiveRoot 1;
2.1223 + autoCalculate 1 CompleteCalcHead;
2.1224 + autoCalculate 1 (Step 1);
2.1225 + autoCalculate 1 (Step 1);
2.1226 + appendFormula 1 "x - 1 = 0";
2.1227 + val (unc, del, gen) = (([1],Res), ([1],Res), ([2],Res));
2.1228 + getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
2.1229 + (*11 elements !!!*)
2.1230 +
2.1231 + val ((pt,_),_) = get_calc 1;
2.1232 + val p = get_pos 1 1;
2.1233 + val (Form f, tac, asms) = pt_extract (pt, p);
2.1234 + if term2str f = "x - 1 = 0" andalso p = ([2], Res) then () else
2.1235 + error "FE-interface.sml: diff.behav. in FORMULA:enter} other";
2.1236 +DEconstrCalcTree 1;
2.1237 +
2.1238 +"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}oth 2";
2.1239 +"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}oth 2";
2.1240 +"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}oth 2";
2.1241 + CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
2.1242 + ("Test", ["sqroot-test","univariate","equation","test"],
2.1243 + ["Test","squ-equ-test-subpbl1"]))];
2.1244 + Iterator 1;
2.1245 + moveActiveRoot 1;
2.1246 + autoCalculate 1 CompleteCalcHead;
2.1247 + autoCalculate 1 (Step 1);
2.1248 + autoCalculate 1 (Step 1);
2.1249 + appendFormula 1 "x = 1";
2.1250 + (*... returns calcChangedEvent with*)
2.1251 + val (unc, del, gen) = (([1],Res), ([1],Res), ([3,2],Res));
2.1252 + getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
2.1253 + (*6 elements !!!*)
2.1254 +
2.1255 + val ((pt,_),_) = get_calc 1;
2.1256 + val p = get_pos 1 1;
2.1257 + val (Form f, tac, asms) = pt_extract (pt, p);
2.1258 + if term2str f = "x = 1" andalso p = ([3,2], Res) then () else
2.1259 + error "FE-interface.sml: diff.behav. in FORMULA:enter} oth 2";
2.1260 +DEconstrCalcTree 1;
2.1261 +
2.1262 +"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}NOTok";
2.1263 +"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}NOTok";
2.1264 +"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}NOTok";
2.1265 + CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
2.1266 + ("Test", ["sqroot-test","univariate","equation","test"],
2.1267 + ["Test","squ-equ-test-subpbl1"]))];
2.1268 + Iterator 1;
2.1269 + moveActiveRoot 1;
2.1270 + autoCalculate 1 CompleteCalcHead;
2.1271 + autoCalculate 1 (Step 1);
2.1272 + autoCalculate 1 (Step 1);
2.1273 + appendFormula 1 "x - 4711 = 0";
2.1274 + (*... returns <ERROR> no derivation found </ERROR>*)
2.1275 +
2.1276 + val ((pt,_),_) = get_calc 1;
2.1277 + val p = get_pos 1 1;
2.1278 + val (Form f, tac, asms) = pt_extract (pt, p);
2.1279 + if term2str f = "x + 1 + -1 * 2 = 0" andalso p = ([1], Res) then () else
2.1280 + error "FE-interface.sml: diff.behav. in FORMULA:enter} NOTok";
2.1281 +DEconstrCalcTree 1;
2.1282 +
2.1283 +"--------- replaceFormula {SOL:MAN:FOR:replace} right----";
2.1284 +"--------- replaceFormula {SOL:MAN:FOR:replace} right----";
2.1285 +"--------- replaceFormula {SOL:MAN:FOR:replace} right----";
2.1286 + CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
2.1287 + ("Test", ["sqroot-test","univariate","equation","test"],
2.1288 + ["Test","squ-equ-test-subpbl1"]))];
2.1289 + Iterator 1;
2.1290 + moveActiveRoot 1;
2.1291 + autoCalculate 1 CompleteCalc;
2.1292 + moveActiveFormula 1 ([2],Res);
2.1293 + replaceFormula 1 "-1 + x = 0" (*i.e. repeats input*);
2.1294 + (*... returns <ERROR> formula not changed </ERROR>*)
2.1295 +
2.1296 + val ((pt,_),_) = get_calc 1;
2.1297 + val p = get_pos 1 1;
2.1298 + val (Form f, tac, asms) = pt_extract (pt, p);
2.1299 + if term2str f = "-1 + x = 0" andalso p = ([2], Res) then () else
2.1300 + error "FE-interface.sml: diff.behav. in FORMULA:replace} right 1";
2.1301 + if map fst (get_interval ([2],Res) ([],Res) 9999 pt) =
2.1302 + [([2], Res), ([3], Pbl), ([3, 1], Frm), ([3, 1], Res), ([3, 2], Res),
2.1303 + ([3], Res), ([4], Res), ([], Res)] then () (*nothing deleted!*) else
2.1304 + error "FE-interface.sml: diff.behav. in FORMULA:replace} right 2";
2.1305 +
2.1306 +(*WN050211 replaceFormula didn't work on second ctree: thus now tested...*)
2.1307 + CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
2.1308 + ("Test", ["sqroot-test","univariate","equation","test"],
2.1309 + ["Test","squ-equ-test-subpbl1"]))];
2.1310 + Iterator 2;
2.1311 + moveActiveRoot 2;
2.1312 + autoCalculate 2 CompleteCalc;
2.1313 + moveActiveFormula 2 ([2],Res);
2.1314 + replaceFormula 2 "-1 + x = 0" (*i.e. repeats input*);
2.1315 + (*... returns <ERROR> formula not changed </ERROR>*)
2.1316 +
2.1317 + val ((pt,_),_) = get_calc 2;
2.1318 + val p = get_pos 2 1;
2.1319 + val (Form f, tac, asms) = pt_extract (pt, p);
2.1320 + if term2str f = "-1 + x = 0" andalso p = ([2], Res) then () else
2.1321 + error "FE-interface.sml: diff.behav. in FORMULA:replace} right 1";
2.1322 + if map fst (get_interval ([2],Res) ([],Res) 9999 pt) =
2.1323 + [([2], Res), ([3], Pbl), ([3, 1], Frm), ([3, 1], Res), ([3, 2], Res),
2.1324 + ([3], Res), ([4], Res), ([], Res)] then () (*nothing deleted!*) else
2.1325 + error "FE-interface.sml: diff.behav. in FORMULA:replace} right 2b";
2.1326 +DEconstrCalcTree 1;
2.1327 +
2.1328 +"--------- replaceFormula {SOL:MAN:FOR:replace} other----";
2.1329 +"--------- replaceFormula {SOL:MAN:FOR:replace} other----";
2.1330 +"--------- replaceFormula {SOL:MAN:FOR:replace} other----";
2.1331 + CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
2.1332 + ("Test", ["sqroot-test","univariate","equation","test"],
2.1333 + ["Test","squ-equ-test-subpbl1"]))];
2.1334 + Iterator 1;
2.1335 + moveActiveRoot 1;
2.1336 + autoCalculate 1 CompleteCalc;
2.1337 + moveActiveFormula 1 ([2],Res); (*there is "-1 + x = 0"*)
2.1338 + replaceFormula 1 "x - 1 = 0"; (*<-------------------------------------*)
2.1339 + (*... returns calcChangedEvent with*)
2.1340 + val (unc, del, gen) = (([1],Res), ([4],Res), ([2],Res));
2.1341 + getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
2.1342 +
2.1343 + val ((pt,_),_) = get_calc 1;
2.1344 + show_pt pt;
2.1345 + val p = get_pos 1 1;
2.1346 + val (Form f, tac, asms) = pt_extract (pt, p);
2.1347 + if term2str f = "x - 1 = 0" andalso p = ([2], Res) then () else
2.1348 + error "FE-interface.sml: diff.behav. in FORMULA:replace} other 1";
2.1349 +(* for getting the list in whole length ...
2.1350 +print_depth 99;map fst (get_interval ([1],Res) ([],Res) 9999 pt);print_depth 3;
2.1351 + *)
2.1352 + if map fst (get_interval ([1],Res) ([],Res) 9999 pt) =
2.1353 + [([1], Res), ([2, 1], Frm), ([2, 1], Res), ([2, 2], Res), ([2, 3], Res),
2.1354 + ([2, 4], Res), ([2, 5], Res), ([2, 6], Res), ([2, 7], Res),
2.1355 + ([2, 8], Res), ([2, 9], Res), ([2], Res)
2.1356 +(*WN060727 {cutlevup->test_trans} removed: ,
2.1357 + ([], Res)(*dropped, if test_trans doesnt stop at PblNd*)*)] then () else
2.1358 + error "FE-interface.sml: diff.behav. in FORMULA:replace} other 2";
2.1359 +DEconstrCalcTree 1;
2.1360 +
2.1361 +"--------- replaceFormula {SOL:MAN:FOR:replace} other 2--";
2.1362 +"--------- replaceFormula {SOL:MAN:FOR:replace} other 2--";
2.1363 +"--------- replaceFormula {SOL:MAN:FOR:replace} other 2--";
2.1364 + CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
2.1365 + ("Test", ["sqroot-test","univariate","equation","test"],
2.1366 + ["Test","squ-equ-test-subpbl1"]))];
2.1367 + Iterator 1;
2.1368 + moveActiveRoot 1;
2.1369 + autoCalculate 1 CompleteCalc;
2.1370 + moveActiveFormula 1 ([2],Res); (*there is "-1 + x = 0"*)
2.1371 + replaceFormula 1 "x = 1"; (*<-------------------------------------*)
2.1372 + (*... returns calcChangedEvent with ...*)
2.1373 + val (unc, del, gen) = (([1],Res), ([4],Res), ([3,2],Res));
2.1374 + getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
2.1375 + (*9 elements !!!*)
2.1376 +
2.1377 + val ((pt,_),_) = get_calc 1;
2.1378 + show_pt pt; (*error: ...get_interval drops ([3,2],Res) ...*)
2.1379 + val (t,_) = get_obj g_result pt [3,2]; term2str t;
2.1380 + if map fst (get_interval ([1],Res) ([],Res) 9999 pt) =
2.1381 + [([1], Res), ([2], Res), ([3], Pbl), ([3, 1], Frm), ([3, 1], Res),
2.1382 + ([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res),
2.1383 + ([3,2],Res)] then () else
2.1384 + error "FE-interface.sml: diff.behav. in FORMULA:replace} oth2 1";
2.1385 +
2.1386 + val p = get_pos 1 1;
2.1387 + val (Form f, tac, asms) = pt_extract (pt, p);
2.1388 + if term2str f = "x = 1" andalso p = ([3,2], Res) then () else
2.1389 + error "FE-interface.sml: diff.behav. in FORMULA:replace} oth2 2";
2.1390 +DEconstrCalcTree 1;
2.1391 +
2.1392 +"--------- replaceFormula {SOL:MAN:FOR:replace} NOTok----";
2.1393 +"--------- replaceFormula {SOL:MAN:FOR:replace} NOTok----";
2.1394 +"--------- replaceFormula {SOL:MAN:FOR:replace} NOTok----";
2.1395 + CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
2.1396 + ("Test", ["sqroot-test","univariate","equation","test"],
2.1397 + ["Test","squ-equ-test-subpbl1"]))];
2.1398 + Iterator 1;
2.1399 + moveActiveRoot 1;
2.1400 + autoCalculate 1 CompleteCalc;
2.1401 + moveActiveFormula 1 ([2],Res); (*there is "-1 + x = 0"*)
2.1402 + replaceFormula 1 "x - 4711 = 0";
2.1403 + (*... returns <ERROR> no derivation found </ERROR>*)
2.1404 +
2.1405 + val ((pt,_),_) = get_calc 1;
2.1406 + show_pt pt;
2.1407 + val p = get_pos 1 1;
2.1408 + val (Form f, tac, asms) = pt_extract (pt, p);
2.1409 + if term2str f = "-1 + x = 0" andalso p = ([2], Res) then () else
2.1410 + error "FE-interface.sml: diff.behav. in FORMULA:replace} NOTok";
2.1411 +DEconstrCalcTree 1;
2.1412 +
2.1413
2.1414
2.1415 *}