1.1 --- a/test/Tools/isac/Knowledge/integrate.sml Tue Jul 19 10:25:37 2011 +0200
1.2 +++ b/test/Tools/isac/Knowledge/integrate.sml Tue Jul 19 13:04:59 2011 +0200
1.3 @@ -422,12 +422,15 @@
1.4 case nxt of (_, Apply_Method ["diff", "integration"]) => ()
1.5 | _ => error "integrate.sml -- me method [diff,integration] -- spec";
1.6 "----- step 8: returns nxt = Rewrite_Set_Inst ([\"(bdv, x)\"],\"integration\")";
1.7 -(*========== inhibit exn 110310 ================================================
1.8 +===== inhibit exn ?===========================================================*)
1.9 +
1.10 +(*========== inhibit exn 110719 ================================================
1.11 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.12 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.13 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.14 if f2str f = "c + x + 1 / 3 * x ^^^ 3" then ()
1.15 else error "integrate.sml -- me method [diff,integration] -- end";
1.16 +============ inhibit exn 110719 ==============================================*)
1.17
1.18
1.19 "----------- autoCalculate [diff,integration] -----------";
1.20 @@ -445,11 +448,13 @@
1.21 if term2str t = "c + x + 1 / 3 * x ^^^ 3" then ()
1.22 else error "integrate.sml -- interSteps [diff,integration] -- result";
1.23
1.24 +(*========== inhibit exn 110719 ================================================
1.25
1.26 "----------- me method [diff,integration,named] ---------";
1.27 "----------- me method [diff,integration,named] ---------";
1.28 "----------- me method [diff,integration,named] ---------";
1.29 (*exp_CalcInt_No-2.xml*)
1.30 +
1.31 val fmz = ["functionTerm (x^^^2 + 1)",
1.32 "integrateBy x","antiDerivativeName F"];
1.33 val (dI',pI',mI') =
1.34 @@ -501,6 +506,8 @@
1.35 "----------- interSteps [diff,integration] --------------";
1.36 "----------- interSteps [diff,integration] --------------";
1.37 "----------- interSteps [diff,integration] --------------";
1.38 +============ inhibit exn 110719 ==============================================*)
1.39 +
1.40 states:=[];
1.41 CalcTree
1.42 [(["functionTerm (x^2 + 1)", "integrateBy x", "antiDerivative FF"],
1.43 @@ -573,6 +580,11 @@
1.44 moveActiveRoot 1;
1.45 autoCalculate 1 CompleteCalc;
1.46 val ((pt,p),_) = get_calc 1; show_pt pt;
1.47 +if p= ([], Res) andalso term2str (get_obj g_res pt (fst p))=
1.48 + "c + x + 1 / 3 * x ^^^ 3"
1.49 +then ()
1.50 +else error "Ambiguous input: Integral ?u + ?v D ?bdv ="
1.51 +(*========== inhibit exn 110719 ================================================
1.52
1.53 interSteps 1 ([1],Res);
1.54 val ((pt,p),_) = get_calc 1; show_pt pt;
1.55 @@ -595,6 +607,7 @@
1.56 if existpt' ([1,1,5], Res) pt then ()
1.57 else error "integrate.sml: interSteps on Rewrite_Set_Inst 2";
1.58
1.59 +============ inhibit exn 110719 ==============================================*)
1.60
1.61 "----------- CAS input ----------------------------------";
1.62 "----------- CAS input ----------------------------------";
1.63 @@ -620,7 +633,4 @@
1.64 WN101010 this test produced <SYSERROR>.."error in kernel" already in CVS-version
1.65 from 2007; not touched since then.
1.66 *)
1.67 -
1.68 -============ inhibit exn 110310 ==============================================*)
1.69 -===== inhibit exn ?===========================================================*)
1.70 -
1.71 +
2.1 --- a/test/Tools/isac/Knowledge/polyminus.sml Tue Jul 19 10:25:37 2011 +0200
2.2 +++ b/test/Tools/isac/Knowledge/polyminus.sml Tue Jul 19 13:04:59 2011 +0200
2.3 @@ -379,12 +379,10 @@
2.4 @@@@@WN081114 gives "??.empty", all "Pruefe" are the same,
2.5 although analogies work in interface.sml: FIXME.WN081114 in "Pruefe"*)
2.6 val ((pt,p),_) = get_calc 1;
2.7 -(*========== inhibit exn 110719 ================================================
2.8 if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) = "11 = 11"
2.9 then () else error "polyminus.sml: Probe 11 = 11";
2.10 show_pt pt;
2.11 -============ inhibit exn 110719 ==============================================*)
2.12 -(*========== inhibit exn 110719 ================================================
2.13 +
2.14
2.15
2.16 "----------- pbl klammer polynom vereinfachen p.34 ---------------";
2.17 @@ -416,7 +414,6 @@
2.18 if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) = "29 = 29"
2.19 then () else error "polyminus.sml: Probe 29 = 29";
2.20 show_pt pt;
2.21 -============ inhibit exn 110719 ==============================================*)
2.22 (*========== inhibit exn 110719 ================================================
2.23
2.24
2.25 @@ -475,15 +472,14 @@
2.26 val ((pt,p),_) = get_calc 1; show_pt pt;
2.27 "----- 7 ^^^";
2.28 *)
2.29 -
2.30 +============ inhibit exn 110719 ==============================================*)
2.31 autoCalculate 1 CompleteCalc;
2.32 val ((pt,p),_) = get_calc 1; show_pt pt;
2.33 (*independent from failure above: met_simp_poly_minus not confluent:
2.34 (([9], Res), - (8 * g) + 10 * g + (3 - 2 * e + 2 * f)),
2.35 (([], Res), - (8 * g) + 10 * g + (3 - 2 * e + 2 * f))]
2.36 ~~~~~~~~~~~###~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
2.37 -============ inhibit exn 110719 ==============================================*)
2.38 -(*========== inhibit exn 110719 ================================================
2.39 +
2.40
2.41 "#############################################################################";
2.42 states:=[];
2.43 @@ -510,7 +506,6 @@
2.44 if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) = "f + 2 * g"
2.45 then () else error "polyminus.sml: tausche_vor_plus";
2.46
2.47 -============ inhibit exn 110719 ==============================================*)
2.48 (*========== inhibit exn 110719 ================================================
2.49
2.50 "----------- pbl binom polynom vereinfachen p.39 -----------------";
2.51 @@ -559,15 +554,10 @@
2.52 moveActiveRoot 1;
2.53 autoCalculate 1 CompleteCalc;
2.54 val ((pt,p),_) = get_calc 1; show_pt pt;
2.55 -
2.56 -
2.57 if p = ([], Res) andalso
2.58 term2str (get_obj g_res pt (fst p)) = "-2 + 12 * a ^^^ 2 + 5 * a"
2.59 then () else error "polyminus.sml: Vereinfache (2*u - 5 - (3 - ...";
2.60
2.61 -(*=== inhibit exn ?=============================================================
2.62 -
2.63 -============ inhibit exn 110719 ==============================================*)
2.64
2.65
2.66 "----------- pbl binom polynom vereinfachen: cube ----------------";
3.1 --- a/test/Tools/isac/Test_Isac.thy Tue Jul 19 10:25:37 2011 +0200
3.2 +++ b/test/Tools/isac/Test_Isac.thy Tue Jul 19 13:04:59 2011 +0200
3.3 @@ -166,7 +166,7 @@
3.4 diff.emacs--jedit*)
3.5 (*use "Knowledge/eqsystem.sml" 2002*)
3.6 use "Knowledge/test.sml" (*complete*)
3.7 - use "Knowledge/polyminus.sml" (*//complete*)
3.8 + use "Knowledge/polyminus.sml" (*complete*)
3.9 (*use "Knowledge/vect.sml" 2002*)
3.10 (*use "Knowledge/diffapp.sml" 2002*)
3.11 (*use "Knowledge/biegelinie.sml" 2002*)
4.1 --- a/test/Tools/isac/Test_Some.thy Tue Jul 19 10:25:37 2011 +0200
4.2 +++ b/test/Tools/isac/Test_Some.thy Tue Jul 19 13:04:59 2011 +0200
4.3 @@ -7,1414 +7,22 @@
4.4
4.5 ML{* writeln "**** run the test ***************************************" *}
4.6
4.7 -use"../../../test/Tools/isac/Frontend/interface.sml"
4.8 +use"../../../test/Tools/isac/Knowledge/integrate.sml"
4.9
4.10 ML{*
4.11
4.12 -hdejdhjmd
4.13 -cdscds
4.14 -sdca
4.15 -
4.16 -
4.17 -
4.18 -
4.19 -(* tests the interface of isac's SML-kernel in accordance to
4.20 - java-tests/isac.bridge.
4.21 -
4.22 -WN050707 ... if true, the test ist marked with a \label referring
4.23 -to the same UC in isac-docu.tex as the JUnit testcase.
4.24 -use"../smltest/FE-interface/interface.sml";
4.25 -use"interface.sml";
4.26 - *)
4.27 -
4.28 -"--------------------------------------------------------";
4.29 -"table of contents --------------------------------------";
4.30 -"--------------------------------------------------------";
4.31 -"within struct ------------------------------------------";
4.32 -"--------------------------------------------------------";
4.33 -"--------- encode ^ -> ^^^ ------------------------------";
4.34 -"--------------------------------------------------------";
4.35 -"exported from struct -----------------------------------";
4.36 -"--------------------------------------------------------";
4.37 -"--------- empty rootpbl --------------------------------";
4.38 -"--------- solve_linear as rootpbl FE -------------------";
4.39 -"--------- inspect the CalcTree No.1 with Iterator No.2 -";
4.40 -"--------- miniscript with mini-subpbl ------------------";
4.41 -"--------- mini-subpbl AUTOCALCULATE Step 1 -------------";
4.42 -"--------- solve_linear as rootpbl AUTO CompleteCalc ----";
4.43 -"--------- solve_linear as rootpbl AUTO CompleteHead/Calc ";
4.44 -"--------- mini-subpbl AUTOCALCULATE CompleteCalc -------";
4.45 -"--------- mini-subpbl AUTO CompleteCalcHead ------------";
4.46 -"--------- solve_linear as rootpbl AUTO CompleteModel ---";
4.47 -"--------- setContext..Thy ------------------------------";
4.48 -"--------- mini-subpbl AUTOCALC CompleteToSubpbl --------";
4.49 -"--------- rat-eq + subpbl: no_met, NO solution dropped -";
4.50 -"--------- tryMatchProblem, tryRefineProblem ------------";
4.51 -"--------- modifyCalcHead, resetCalcHead, modelProblem --";
4.52 -"--------- maximum-example, UC: Modeling an example -----";
4.53 -"--------- solve_linear from pbl-hierarchy --------------";
4.54 -"--------- solve_linear as in an algebra system (CAS)----";
4.55 -"--------- interSteps: on 'miniscript with mini-subpbl' -";
4.56 -"--------- getTactic, fetchApplicableTactics ------------";
4.57 -"--------- getAssumptions, getAccumulatedAsms -----------";
4.58 -"--------- arbitrary combinations of steps --------------";
4.59 -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}right";
4.60 -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}other";
4.61 -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}oth 2";
4.62 -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}NOTok";
4.63 -"--------- replaceFormula {SOL:MAN:FOR:replace} right----";
4.64 -"--------- replaceFormula {SOL:MAN:FOR:replace} other----";
4.65 -"--------- replaceFormula {SOL:MAN:FOR:replace} other 2--";
4.66 -"--------- replaceFormula {SOL:MAN:FOR:replace} NOTok----";
4.67 -"--------------------------------------------------------";
4.68 -
4.69 -"within struct ---------------------------------------------------";
4.70 -"within struct ---------------------------------------------------";
4.71 -"within struct ---------------------------------------------------";
4.72 -(*==================================================================
4.73 -
4.74 -
4.75 -"--------- encode ^ -> ^^^ ------------------------------";
4.76 -"--------- encode ^ -> ^^^ ------------------------------";
4.77 -"--------- encode ^ -> ^^^ ------------------------------";
4.78 -if encode "a^2+b^2=c^2" = "a^^^2+b^^^2=c^^^2" then ()
4.79 -else error "interface.sml: diff.behav. in encode ^ -> ^^^ ";
4.80 -
4.81 -if (decode o encode) "a^2+b^2=c^2" = "a^2+b^2=c^2" then ()
4.82 -else error "interface.sml: diff.behav. in de/encode ^ <-> ^^^ ";
4.83 -
4.84 -==================================================================*)
4.85 -"exported from struct --------------------------------------------";
4.86 -"exported from struct --------------------------------------------";
4.87 -"exported from struct --------------------------------------------";
4.88 -
4.89 -
4.90 -(*------------ set at startup of the Kernel --------------------------*)
4.91 - states:= []; (*resets all state information in Kernel *)
4.92 -(*----------------------------------------------------------------*)
4.93 -
4.94 -"--------- empty rootpbl --------------------------------";
4.95 -"--------- empty rootpbl --------------------------------";
4.96 -"--------- empty rootpbl --------------------------------";
4.97 - CalcTree [([], ("", [], []))];
4.98 - Iterator 1;
4.99 - moveActiveRoot 1;
4.100 - refFormula 1 (get_pos 1 1);
4.101 -(*WN.040222: stoert das sehr, dass e_domID etc. statt leer kommt ???*)
4.102 -
4.103 -
4.104 -"--------- solve_linear as rootpbl FE -------------------";
4.105 -"--------- solve_linear as rootpbl FE -------------------";
4.106 -"--------- solve_linear as rootpbl FE -------------------";
4.107 - states := [];
4.108 - CalcTree (*start of calculation, return No.1*)
4.109 - [(["equality (1+-1*2+x=(0::real))", "solveFor x","solutions L"],
4.110 - ("Test",
4.111 - ["linear","univariate","equation","test"],
4.112 - ["Test","solve_linear"]))];
4.113 - Iterator 1; (*create an active Iterator on CalcTree No.1*)
4.114 -
4.115 - moveActiveRoot 1;(*sets the CalcIterator No.1 at the root of CalcTree No.1*);
4.116 - refFormula 1 (get_pos 1 1) (*gets CalcHead; model is still empty*);
4.117 -
4.118 -
4.119 - fetchProposedTactic 1 (*by using Iterator No.1*);
4.120 - setNextTactic 1 (Model_Problem); (*by using Iterator No.1*)
4.121 - autoCalculate 1 (Step 1);
4.122 - refFormula 1 (get_pos 1 1) (*model contains descriptions for all items*);
4.123 - autoCalculate 1 (Step 1);
4.124 -(*-----since Model_Problem + complete_mod_ in case cas of SOME-----*
4.125 - fetchProposedTactic 1;
4.126 - setNextTactic 1 (Add_Given "equality (1 + -1 * 2 + x = 0)");
4.127 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); (*equality added*);
4.128 -
4.129 - fetchProposedTactic 1;
4.130 - setNextTactic 1 (Add_Given "solveFor x");
4.131 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
4.132 -
4.133 - fetchProposedTactic 1;
4.134 - setNextTactic 1 (Add_Find "solutions L");
4.135 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
4.136 -
4.137 - fetchProposedTactic 1;
4.138 - setNextTactic 1 (Specify_Theory "Test");
4.139 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
4.140 -*-----since Model_Problem + complete_mod_ in case cas of SOME-----*)
4.141 -
4.142 - fetchProposedTactic 1;
4.143 - setNextTactic 1 (Specify_Problem ["linear","univariate","equation","test"]);
4.144 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
4.145 -(*-------------------------------------------------------------------------*)
4.146 - fetchProposedTactic 1;
4.147 - val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;
4.148 -
4.149 - setNextTactic 1 (Specify_Method ["Test","solve_linear"]);
4.150 - val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;
4.151 -
4.152 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
4.153 - val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;
4.154 -
4.155 -(*-------------------------------------------------------------------------*)
4.156 - fetchProposedTactic 1;
4.157 -(*========== inhibit exn 110310 ================================================
4.158 - val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;
4.159 -
4.160 - setNextTactic 1 (Apply_Method ["Test","solve_linear"]);
4.161 - (*ERROR.110620 <SETNEXTTACTIC>..<MESSAGE> end-of-calculation*)
4.162 - val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;
4.163 - is_complete_mod ptp;
4.164 - is_complete_spec ptp;
4.165 -
4.166 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
4.167 - val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;
4.168 - (*term2str (get_obj g_form pt [1]);*)
4.169 -(*-------------------------------------------------------------------------*)
4.170 -
4.171 - fetchProposedTactic 1;
4.172 - setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "isolate_bdv"));
4.173 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
4.174 -
4.175 - fetchProposedTactic 1;
4.176 - setNextTactic 1 (Rewrite_Set "Test_simplify");
4.177 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
4.178 -
4.179 - fetchProposedTactic 1;
4.180 - setNextTactic 1 (Check_Postcond ["linear","univariate","equation","test"]);
4.181 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
4.182 -
4.183 - val ((pt,_),_) = get_calc 1;
4.184 - val ip = get_pos 1 1;
4.185 - val (Form f, tac, asms) = pt_extract (pt, ip);
4.186 - (*exception just above means: 'ModSpec' has been returned: error anyway*)
4.187 - if term2str f = "[x = 1]" then () else
4.188 - error "FE-Kernel-interface.sml: diff.behav. in solve_linear as rootpbl";
4.189 -============ inhibit exn 110310 ==============================================*)
4.190 -
4.191 -(*========== inhibit exn 110620 ================================================
4.192 -"--------- inspect the CalcTree No.1 with Iterator No.2 -";
4.193 -"--------- inspect the CalcTree No.1 with Iterator No.2 -";
4.194 -"--------- inspect the CalcTree No.1 with Iterator No.2 -";
4.195 -(*WN041118: inspection shifted to Iterator No.1, because others need pos'*)
4.196 - moveActiveRoot 1;
4.197 - refFormula 1 ([],Pbl); getTactic 1 ([],Pbl);(*Error*)
4.198 - moveActiveDown 1;
4.199 - refFormula 1 ([1],Frm); getTactic 1 ([1],Frm);(*Error*)
4.200 - moveActiveDown 1 ;
4.201 - refFormula 1 ([1],Res); getTactic 1 ([1],Res);(*OK*)
4.202 - (*getAssumption 1 ([1],Res); TODO.WN041217*)
4.203 - moveActiveDown 1 ; refFormula 1 ([2],Res);
4.204 - moveActiveCalcHead 1; refFormula 1 ([],Pbl);
4.205 - moveActiveDown 1;
4.206 - moveActiveDown 1;
4.207 - moveActiveDown 1;
4.208 - if get_pos 1 1 = ([2], Res) then () else
4.209 - error "FE-interface.sml: diff.behav. in a inspect 1 with Iterator 2";
4.210 - moveActiveDown 1; refFormula 1 ([], Res);
4.211 - if get_pos 1 1 = ([], Res) then () else
4.212 - error "FE-interface.sml: diff.behav. in b inspect 1 with Iterator 2";
4.213 - moveActiveCalcHead 1; refFormula 1 ([],Pbl);
4.214 -============ inhibit exn 110620 ==============================================*)
4.215 -
4.216 -"--------- miniscript with mini-subpbl ------------------";
4.217 -"--------- miniscript with mini-subpbl ------------------";
4.218 -"--------- miniscript with mini-subpbl ------------------";
4.219 -"=== this sequence of fun-calls resembles fun me ===";
4.220 - states:=[]; (*start of calculation, return No.1*)
4.221 - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
4.222 - ("Test", ["sqroot-test","univariate","equation","test"],
4.223 - ["Test","squ-equ-test-subpbl1"]))];
4.224 - Iterator 1;
4.225 -
4.226 - moveActiveRoot 1;
4.227 - refFormula 1 (get_pos 1 1);
4.228 - fetchProposedTactic 1;
4.229 - setNextTactic 1 (Model_Problem);
4.230 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*gets ModSpec;model is still empty*)
4.231 -
4.232 - fetchProposedTactic 1;
4.233 - setNextTactic 1 (Add_Given "equality (x + 1 = 2)");
4.234 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
4.235 -
4.236 - fetchProposedTactic 1;
4.237 - setNextTactic 1 (Add_Given "solveFor x");
4.238 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
4.239 -
4.240 - fetchProposedTactic 1;
4.241 - setNextTactic 1 (Add_Find "solutions L");
4.242 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
4.243 -
4.244 - fetchProposedTactic 1;
4.245 - setNextTactic 1 (Specify_Theory "Test");
4.246 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
4.247 -
4.248 - fetchProposedTactic 1;
4.249 - setNextTactic 1 (Specify_Problem
4.250 - ["sqroot-test","univariate","equation","test"]);
4.251 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
4.252 -"1-----------------------------------------------------------------";
4.253 -
4.254 - fetchProposedTactic 1;
4.255 - setNextTactic 1 (Specify_Method ["Test","squ-equ-test-subpbl1"]);
4.256 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
4.257 -
4.258 - fetchProposedTactic 1;
4.259 - setNextTactic 1 (Apply_Method ["Test","squ-equ-test-subpbl1"]);
4.260 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
4.261 -
4.262 - fetchProposedTactic 1;
4.263 - setNextTactic 1 (Rewrite_Set "norm_equation");
4.264 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
4.265 -
4.266 - fetchProposedTactic 1;
4.267 - setNextTactic 1 (Rewrite_Set "Test_simplify");
4.268 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
4.269 -
4.270 - fetchProposedTactic 1;(*----------------Subproblem--------------------*);
4.271 - setNextTactic 1 (Subproblem ("Test",
4.272 - ["linear","univariate","equation","test"]));
4.273 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
4.274 -
4.275 - fetchProposedTactic 1;
4.276 - setNextTactic 1 (Model_Problem );
4.277 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
4.278 -
4.279 - fetchProposedTactic 1;
4.280 - setNextTactic 1 (Add_Given "equality (-1 + x = 0)");
4.281 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
4.282 -
4.283 - fetchProposedTactic 1;
4.284 - setNextTactic 1 (Add_Given "solveFor x");
4.285 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
4.286 -
4.287 - fetchProposedTactic 1;
4.288 - setNextTactic 1 (Add_Find "solutions x_i");
4.289 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
4.290 -
4.291 - fetchProposedTactic 1;
4.292 - setNextTactic 1 (Specify_Theory "Test");
4.293 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
4.294 -
4.295 - fetchProposedTactic 1;
4.296 - setNextTactic 1 (Specify_Problem ["linear","univariate","equation","test"]);
4.297 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
4.298 -"2-----------------------------------------------------------------";
4.299 -
4.300 - fetchProposedTactic 1;
4.301 - setNextTactic 1 (Specify_Method ["Test","solve_linear"]);
4.302 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
4.303 -
4.304 - fetchProposedTactic 1;
4.305 - setNextTactic 1 (Apply_Method ["Test","solve_linear"]);
4.306 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
4.307 -
4.308 - fetchProposedTactic 1;
4.309 - setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "isolate_bdv"));
4.310 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
4.311 -
4.312 - fetchProposedTactic 1;
4.313 - setNextTactic 1 (Rewrite_Set "Test_simplify");
4.314 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
4.315 -
4.316 - fetchProposedTactic 1;
4.317 - setNextTactic 1 (Check_Postcond ["linear","univariate","equation","test"]);
4.318 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
4.319 -
4.320 - fetchProposedTactic 1;
4.321 - setNextTactic 1 (Check_elementwise "Assumptions");
4.322 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
4.323 -
4.324 - val xml = fetchProposedTactic 1;
4.325 - setNextTactic 1 (Check_Postcond
4.326 - ["sqroot-test","univariate","equation","test"]);
4.327 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
4.328 -
4.329 - val ((pt,_),_) = get_calc 1;
4.330 - val str = pr_ptree pr_short pt;
4.331 - writeln str;
4.332 - val ip = get_pos 1 1;
4.333 - val (Form f, tac, asms) = pt_extract (pt, ip);
4.334 - (*exception just above means: 'ModSpec' has been returned: error anyway*)
4.335 - if term2str f = "[x = 1]" then () else
4.336 - error "FE-interface.sml: diff.behav. in miniscript with mini-subpb";
4.337 -
4.338 - DEconstrCalcTree 1;
4.339 -
4.340 -"--------- mini-subpbl AUTOCALCULATE Step 1 -------------";
4.341 -"--------- mini-subpbl AUTOCALCULATE Step 1 -------------";
4.342 -"--------- mini-subpbl AUTOCALCULATE Step 1 -------------";
4.343 - states:=[];
4.344 - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
4.345 - ("Test", ["sqroot-test","univariate","equation","test"],
4.346 - ["Test","squ-equ-test-subpbl1"]))];
4.347 - Iterator 1;
4.348 - moveActiveRoot 1;
4.349 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
4.350 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
4.351 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
4.352 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
4.353 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
4.354 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
4.355 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
4.356 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
4.357 - (*here the solve-phase starts*)
4.358 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
4.359 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
4.360 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
4.361 - (*------------------------------------*)
4.362 -(* print_depth 13; get_calc 1;
4.363 - *)
4.364 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
4.365 - (*calc-head of subproblem*)
4.366 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
4.367 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
4.368 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
4.369 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
4.370 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
4.371 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
4.372 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
4.373 - (*solve-phase of the subproblem*)
4.374 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
4.375 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
4.376 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
4.377 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
4.378 - (*finish subproblem*)
4.379 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
4.380 - (*finish problem*)
4.381 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
4.382 -
4.383 - (*this checks the test for correctness..*)
4.384 - val ((pt,_),_) = get_calc 1;
4.385 - val p = get_pos 1 1;
4.386 - val (Form f, tac, asms) = pt_extract (pt, p);
4.387 - if term2str f = "[x = 1]" andalso p = ([], Res) then () else
4.388 - error "FE-interface.sml: diff.behav. in miniscript with mini-subpb";
4.389 -
4.390 - DEconstrCalcTree 1;
4.391 -
4.392 -
4.393 -"--------- solve_linear as rootpbl AUTO CompleteCalc ----";
4.394 -"--------- solve_linear as rootpbl AUTO CompleteCalc ----";
4.395 -"--------- solve_linear as rootpbl AUTO CompleteCalc ----";
4.396 - states:=[];
4.397 - CalcTree
4.398 - [(["equality (1+-1*2+x=(0::real))", "solveFor x","solutions L"],
4.399 - ("Test",
4.400 - ["linear","univariate","equation","test"],
4.401 - ["Test","solve_linear"]))];
4.402 - Iterator 1;
4.403 - moveActiveRoot 1;
4.404 -getFormulaeFromTo 1 ([],Pbl) ([],Pbl) 999 false;
4.405 -
4.406 - autoCalculate 1 CompleteCalc;
4.407 - val (unc, del, gen) = (([],Pbl), ([],Pbl), ([],Res));
4.408 - getFormulaeFromTo 1 unc gen 1 (*only level 1*) false;
4.409 -
4.410 - val ((pt,_),_) = get_calc 1;
4.411 - val p = get_pos 1 1;
4.412 - val (Form f, tac, asms) = pt_extract (pt, p);
4.413 - if term2str f = "[x = 1]" andalso p = ([], Res) then () else
4.414 - error "FE-interface.sml: diff.behav. in solve_linear/rt AUTOCALCULATE ";
4.415 -
4.416 -
4.417 -"--------- solve_linear as rootpbl AUTO CompleteHead/Calc ";
4.418 -"--------- solve_linear as rootpbl AUTO CompleteHead/Calc ";
4.419 -"--------- solve_linear as rootpbl AUTO CompleteHead/Calc ";
4.420 - states:=[];
4.421 - CalcTree
4.422 - [(["equality (1+-1*2+x=(0::real)", "solveFor x","solutions L"],
4.423 - ("Test",
4.424 - ["linear","univariate","equation","test"],
4.425 - ["Test","solve_linear"]))];
4.426 - Iterator 1;
4.427 - moveActiveRoot 1;
4.428 -(*========== inhibit exn 110718 ================================================
4.429 - autoCalculate 1 CompleteCalcHead;
4.430 - refFormula 1 (get_pos 1 1);
4.431 - val ((pt,p),_) = get_calc 1;
4.432 -
4.433 - autoCalculate 1 CompleteCalc;
4.434 - val ((pt,p),_) = get_calc 1;
4.435 - if p=([], Res) then () else
4.436 - error "FE-interface.sml: diff.behav. in solve_linear AUTOC Head/Calc ";
4.437 -============ inhibit exn 110718 ==============================================*)
4.438 -
4.439 -"--------- mini-subpbl AUTOCALCULATE CompleteCalc -------";
4.440 -"--------- mini-subpbl AUTOCALCULATE CompleteCalc -------";
4.441 -"--------- mini-subpbl AUTOCALCULATE CompleteCalc -------";
4.442 - states:=[];
4.443 - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
4.444 - ("Test", ["sqroot-test","univariate","equation","test"],
4.445 - ["Test","squ-equ-test-subpbl1"]))];
4.446 - Iterator 1;
4.447 - moveActiveRoot 1;
4.448 - autoCalculate 1 CompleteCalc;
4.449 - val ((pt,p),_) = get_calc 1; show_pt pt;
4.450 -(*
4.451 -getTactic 1 ([1],Frm);
4.452 -getTactic 1 ([1],Res);
4.453 -initContext 1 Thy_ ([1],Res);
4.454 -*)
4.455 - (*... returns calcChangedEvent with*)
4.456 - val (unc, del, gen) = (([],Pbl), ([],Pbl), ([],Res));
4.457 - getFormulaeFromTo 1 unc gen 0 (*only result*) false;
4.458 - getFormulaeFromTo 1 unc gen 1 (*only level 1*) false;
4.459 - getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
4.460 -
4.461 - val ((pt,_),_) = get_calc 1;
4.462 - val p = get_pos 1 1;
4.463 - val (Form f, tac, asms) = pt_extract (pt, p);
4.464 - if term2str f = "[x = 1]" andalso p = ([], Res) then () else
4.465 - error "FE-interface.sml: diff.behav. in mini-subpbl AUTOCALCULATE 6";
4.466 -
4.467 -
4.468 -"--------- mini-subpbl AUTO CompleteCalcHead ------------";
4.469 -"--------- mini-subpbl AUTO CompleteCalcHead ------------";
4.470 -"--------- mini-subpbl AUTO CompleteCalcHead ------------";
4.471 - states:=[];
4.472 - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
4.473 - ("Test", ["sqroot-test","univariate","equation","test"],
4.474 - ["Test","squ-equ-test-subpbl1"]))];
4.475 - Iterator 1;
4.476 - moveActiveRoot 1;
4.477 - autoCalculate 1 CompleteCalcHead;
4.478 -
4.479 -val ((Nd (PblObj {env = NONE, fmz = (fm, ("Test", pblID, metID)), loc = (SOME (env, ctxt1), NONE),
4.480 - cell = NONE, ctxt = ctxt2, meth,
4.481 - spec = ("Test", ["sqroot-test", "univariate", "equation", "test"],
4.482 - ["Test", "squ-equ-test-subpbl1"]),
4.483 - probl, branch = TransitiveB, origin, ostate = Incomplete, result}, []),
4.484 - ([], Met)), []) = get_calc 1;
4.485 -if length meth = 3 andalso length probl = 3 (*just some items tested*) then ()
4.486 -else error "--- mini-subpbl AUTO CompleteCalcHead ---";
4.487 -
4.488 -
4.489 -"--------- solve_linear as rootpbl AUTO CompleteModel ---";
4.490 -"--------- solve_linear as rootpbl AUTO CompleteModel ---";
4.491 -"--------- solve_linear as rootpbl AUTO CompleteModel ---";
4.492 - states:=[];
4.493 - CalcTree
4.494 - [(["equality (1+-1*2+x=0)", "solveFor x","solutions L"],
4.495 - ("Test",
4.496 - ["linear","univariate","equation","test"],
4.497 - ["Test","solve_linear"]))];
4.498 - Iterator 1;
4.499 - moveActiveRoot 1;
4.500 -(*========== inhibit exn 110718 ================================================
4.501 - autoCalculate 1 CompleteModel;
4.502 - refFormula 1 (get_pos 1 1);
4.503 -
4.504 -setProblem 1 ["linear","univariate","equation","test"];
4.505 -val pos = get_pos 1 1;
4.506 -setContext 1 pos (kestoreID2guh Pbl_["linear","univariate","equation","test"]);
4.507 - refFormula 1 (get_pos 1 1);
4.508 -
4.509 -setMethod 1 ["Test","solve_linear"];
4.510 -setContext 1 pos (kestoreID2guh Met_ ["Test","solve_linear"]);
4.511 - refFormula 1 (get_pos 1 1);
4.512 - val ((pt,_),_) = get_calc 1;
4.513 - if get_obj g_spec pt [] = ("e_domID",
4.514 - ["linear", "univariate","equation","test"],
4.515 - ["Test","solve_linear"]) then ()
4.516 - else error "FE-interface.sml: diff.behav. in setProblem, setMethod";
4.517 -
4.518 - autoCalculate 1 CompleteCalcHead;
4.519 - refFormula 1 (get_pos 1 1);
4.520 - autoCalculate 1 CompleteCalc;
4.521 - moveActiveDown 1;
4.522 - moveActiveDown 1;
4.523 - moveActiveDown 1;
4.524 - refFormula 1 (get_pos 1 1);
4.525 - val ((pt,_),_) = get_calc 1;
4.526 - val p = get_pos 1 1;
4.527 - val (Form f, tac, asms) = pt_extract (pt, p);
4.528 - if term2str f = "[x = 1]" andalso p = ([], Res) then () else
4.529 - error "FE-interface.sml: diff.behav. in mini-subpbl AUTOCALCULATE 6";
4.530 -============ inhibit exn 110718 ==============================================*)
4.531 -
4.532 -"--------- setContext..Thy ------------------------------";
4.533 -"--------- setContext..Thy ------------------------------";
4.534 -"--------- setContext..Thy ------------------------------";
4.535 -states:=[];
4.536 -CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
4.537 - ("Test", ["sqroot-test","univariate","equation","test"],
4.538 - ["Test","squ-equ-test-subpbl1"]))];
4.539 -Iterator 1; moveActiveRoot 1;
4.540 -autoCalculate 1 CompleteCalcHead;
4.541 -autoCalculate 1 (Step 1);
4.542 -val ((pt,p),_) = get_calc 1; show_pt pt; (*2 lines, OK*)
4.543 -(*
4.544 -setNextTactic 1 (Rewrite_Set "Test_simplify"); (*--> "thy_isac_Test-rls-Test_simplify"*)
4.545 -autoCalculate 1 (Step 1);
4.546 -val ((pt,p),_) = get_calc 1; show_pt pt;
4.547 -*)
4.548 -"-----^^^^^ and vvvvv do the same -----";
4.549 -setContext 1 p "thy_isac_Test-rls-Test_simplify";
4.550 -val ((pt,p),_) = get_calc 1; show_pt pt; (*2 lines, OK*)
4.551 -
4.552 -autoCalculate 1 (Step 1);
4.553 -setContext 1 p "thy_isac_Test-rls-Test_simplify";
4.554 -val ((pt,p),_) = get_calc 1; show_pt pt; (*3 lines, OK*)
4.555 -if p = ([1], Res) andalso term2str (get_obj g_res pt (fst p)) = "x + 1 + -1 * 2 = 0"
4.556 -then () else error "--- setContext..Thy --- autoCalculate 1 (Step 1) #1"
4.557 -
4.558 -autoCalculate 1 CompleteCalc;
4.559 -val ((pt,p),_) = get_calc 1; show_pt pt;
4.560 -val (((pt,_),_), p) = (get_calc 1, get_pos 1 1);
4.561 -(*========== inhibit exn 110622 ================================================
4.562 - ERROR still 3 lines
4.563 -val (Form f, tac, asms) = pt_extract (pt, p);
4.564 -if term2str f = "[x = 1]" andalso p = ([], Res) then () else
4.565 -error "--- setContext..Thy --- autoCalculate CompleteCalc";
4.566 -============ inhibit exn 110622 ==============================================*)
4.567 -
4.568 -"--------- mini-subpbl AUTOCALC CompleteToSubpbl --------";
4.569 -"--------- mini-subpbl AUTOCALC CompleteToSubpbl --------";
4.570 -"--------- mini-subpbl AUTOCALC CompleteToSubpbl --------";
4.571 - states:=[];
4.572 - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
4.573 - ("Test", ["sqroot-test","univariate","equation","test"],
4.574 - ["Test","squ-equ-test-subpbl1"]))];
4.575 - Iterator 1; moveActiveRoot 1;
4.576 - autoCalculate 1 CompleteToSubpbl;
4.577 - refFormula 1 (get_pos 1 1); (*<ISA> -1 + x = 0 </ISA>*);
4.578 - val ((pt,_),_) = get_calc 1;
4.579 - val str = pr_ptree pr_short pt;
4.580 - writeln str;
4.581 - if str = ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + -1 * 2 = 0\n"
4.582 - then () else
4.583 - error "FE-interface.sml: diff.behav. in mini-subpbl CompleteToSubpbl-1";
4.584 -
4.585 - autoCalculate 1 (Step 1); (*proceeds only, of NOT 1 step before subplb*)
4.586 - autoCalculate 1 CompleteToSubpbl;
4.587 - val ((pt,_),_) = get_calc 1;
4.588 - val str = pr_ptree pr_short pt;
4.589 - writeln str;
4.590 - autoCalculate 1 CompleteCalc; (*das geht ohnehin !*);
4.591 - val ((pt,_),_) = get_calc 1;
4.592 - val p = get_pos 1 1;
4.593 -(*========== inhibit exn 110622 ================================================
4.594 - val (Form f, tac, asms) = pt_extract (pt, p);
4.595 - if term2str f = "[x = 1]" andalso p = ([], Res) then () else
4.596 - error "FE-interface.sml: diff.behav. in mini-subpbl CompleteToSubpbl 1";
4.597 -============ inhibit exn 110622 ==============================================*)
4.598 -
4.599 -
4.600 -"--------- rat-eq + subpbl: no_met, NO solution dropped -";
4.601 -"--------- rat-eq + subpbl: no_met, NO solution dropped -";
4.602 -"--------- rat-eq + subpbl: no_met, NO solution dropped -";
4.603 -(*========== inhibit exn 110622 ================================================
4.604 - states:=[];
4.605 - CalcTree
4.606 - [(["equality ((5*x)/(x - 2) - x/(x+2)=4)", "solveFor x","solutions L"],
4.607 - ("RatEq", ["univariate","equation"], ["no_met"]))];
4.608 - Iterator 1;
4.609 - moveActiveRoot 1;
4.610 - fetchProposedTactic 1;
4.611 - setNextTactic 1 (Model_Problem );
4.612 -autoCalculate 1 (Step 1); fetchProposedTactic 1;
4.613 -(*-----since Model_Problem + complete_mod_ in case cas of SOME-----*
4.614 - setNextTactic 1 (Add_Given "equality (5 * x / (x - 2) - x / (x + 2) = 4)");
4.615 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
4.616 - setNextTactic 1 (Add_Given "solveFor x");
4.617 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
4.618 - setNextTactic 1 (Add_Find "solutions L");
4.619 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
4.620 -*-----since Model_Problem + complete_mod_ in case cas of SOME-----*)
4.621 - setNextTactic 1 (Specify_Theory "RatEq");
4.622 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
4.623 - setNextTactic 1 (Specify_Problem ["rational","univariate","equation"]);
4.624 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
4.625 - setNextTactic 1 (Specify_Method ["RatEq","solve_rat_equation"]);
4.626 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
4.627 - setNextTactic 1 (Apply_Method ["RatEq","solve_rat_equation"]);
4.628 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
4.629 - setNextTactic 1 (Rewrite_Set "RatEq_simplify");
4.630 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
4.631 - setNextTactic 1 (Rewrite_Set "norm_Rational");
4.632 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
4.633 - setNextTactic 1 (Rewrite_Set "RatEq_eliminate");
4.634 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
4.635 - (* __________ for "12 * x + 4 * x ^^^ 2 = 4 * (-4 + x ^^^ 2)"*)
4.636 - setNextTactic 1 (Subproblem ("PolyEq", ["normalize","polynomial",
4.637 - "univariate","equation"]));
4.638 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
4.639 - setNextTactic 1 (Model_Problem );
4.640 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
4.641 -(*-----since Model_Problem + complete_mod_ in case cas of SOME-----*
4.642 - setNextTactic 1 (Add_Given
4.643 - "equality (12 * x + 4 * x ^^^ 2 = 4 * (-4 + x ^^^ 2))");
4.644 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
4.645 - setNextTactic 1 (Add_Given "solveFor x");
4.646 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
4.647 - setNextTactic 1 (Add_Find "solutions x_i");
4.648 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
4.649 -*-----since Model_Problem + complete_mod_ in case cas of SOME-----*)
4.650 - setNextTactic 1 (Specify_Theory "PolyEq");
4.651 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
4.652 - setNextTactic 1 (Specify_Problem ["normalize","polynomial",
4.653 - "univariate","equation"]);
4.654 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
4.655 - setNextTactic 1 (Specify_Method ["PolyEq","normalize_poly"]);
4.656 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
4.657 - setNextTactic 1 (Apply_Method ["PolyEq","normalize_poly"]);
4.658 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
4.659 - setNextTactic 1 (Rewrite ("all_left",""));
4.660 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
4.661 - setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "make_ratpoly_in"));
4.662 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
4.663 - (* __________ for "16 + 12 * x = 0"*)
4.664 - setNextTactic 1 (Subproblem ("PolyEq",
4.665 - ["degree_1","polynomial","univariate","equation"]));
4.666 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
4.667 - setNextTactic 1 (Model_Problem );
4.668 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
4.669 -(*-----since Model_Problem + complete_mod_ in case cas of SOME-----*
4.670 - setNextTactic 1 (Add_Given
4.671 - "equality (16 + 12 * x = 0)");
4.672 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
4.673 - setNextTactic 1 (Add_Given "solveFor x");
4.674 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
4.675 - setNextTactic 1 (Add_Find "solutions x_i");
4.676 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
4.677 -*-----since Model_Problem + complete_mod_ in case cas of SOME-----*)
4.678 - setNextTactic 1 (Specify_Theory "PolyEq");
4.679 - (*------------- some trials in the problem-hierarchy ---------------*)
4.680 - setNextTactic 1 (Specify_Problem ["linear","univariate","equation"]);
4.681 - autoCalculate 1 (Step 1); fetchProposedTactic 1; (*<ERROR> helpless </ERROR> !!!*)
4.682 - setNextTactic 1 (Refine_Problem ["univariate","equation"]);
4.683 -
4.684 - (*------------------------------------------------------------------*)
4.685 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
4.686 - setNextTactic 1 (Specify_Method ["PolyEq","solve_d1_polyeq_equation"]);
4.687 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
4.688 - setNextTactic 1 (Apply_Method ["PolyEq","solve_d1_polyeq_equation"]);
4.689 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
4.690 - setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "d1_polyeq_simplify"));
4.691 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
4.692 - setNextTactic 1 (Rewrite_Set "polyeq_simplify");
4.693 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
4.694 - (*==================================================================*)
4.695 - setNextTactic 1 Or_to_List;
4.696 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
4.697 - setNextTactic 1 (Check_elementwise "Assumptions");
4.698 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
4.699 - setNextTactic 1 (Check_Postcond ["degree_1","polynomial",
4.700 - "univariate","equation"]);
4.701 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
4.702 - setNextTactic 1 (Check_Postcond ["normalize","polynomial",
4.703 - "univariate","equation"]);
4.704 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
4.705 -(*========== inhibit exn 2009 ==================================================
4.706 -*** exception TYPE raised (line 460 of "old_goals.ML"):
4.707 -*** Type error in application: Incompatible operand type
4.708 -***
4.709 -*** Operator: equality :: bool => una
4.710 -*** Operand: [((x * 3) = -4)] :: bool list
4.711 -***
4.712 -*** bool => una
4.713 -*** bool list
4.714 -*** equality
4.715 -*** [x * 3 = -4]
4.716 -
4.717 - setNextTactic 1 (Check_elementwise "Assumptions");
4.718 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
4.719 - setNextTactic 1 (Check_Postcond ["rational","univariate","equation"]);
4.720 - val (ptp,_) = get_calc 1;
4.721 - val (Form t,_,_) = pt_extract ptp;
4.722 - if get_pos 1 1 = ([], Res) andalso term2str t = "[x = -4 / 3]" then ()
4.723 - else writeln "FE-inteface.sml: diff.behav. in rat-eq + subpbl: no_met, NO ..";
4.724 -============ inhibit exn 2009 ================================================*)
4.725 -============ inhibit exn 110622 ==============================================*)
4.726 -
4.727 -
4.728 -"--------- tryMatchProblem, tryRefineProblem ------------";
4.729 -"--------- tryMatchProblem, tryRefineProblem ------------";
4.730 -"--------- tryMatchProblem, tryRefineProblem ------------";
4.731 -(*{\bf\UC{Having \isac{} Refine the Problem
4.732 - * Automatically}\label{SPECIFY:refine-auto}\\} test match and refine with
4.733 - * x^^^2 + 4*x + 5 = 2
4.734 -see isac.bridge.TestSpecify#testMatchRefine*)
4.735 - DEconstrCalcTree 1;
4.736 - CalcTree
4.737 - [(["equality (x^2 + 4*x + 5 = 2)", "solveFor x","solutions L"],
4.738 - ("Isac",
4.739 - ["univariate","equation"],
4.740 - ["no_met"]))];
4.741 - Iterator 1;
4.742 - moveActiveRoot 1;
4.743 -
4.744 - fetchProposedTactic 1;
4.745 - setNextTactic 1 (Model_Problem );
4.746 - (*..this tactic should be done 'tacitly', too !*)
4.747 -
4.748 -(*
4.749 -autoCalculate 1 CompleteCalcHead;
4.750 -checkContext 1 ([],Pbl) "pbl_equ_univ";
4.751 -checkContext 1 ([],Pbl) (kestoreID2guh Pbl_ ["univariate","equation"]);
4.752 -*)
4.753 -
4.754 - autoCalculate 1 (Step 1);
4.755 -
4.756 - fetchProposedTactic 1;
4.757 - setNextTactic 1 (Add_Given "equality (x ^^^ 2 + 4 * x + 5 = 2)");
4.758 - autoCalculate 1 (Step 1);
4.759 -
4.760 - "--------- we go into the ProblemBrowser (_NO_ pblID selected) -";
4.761 -initContext 1 Pbl_ ([],Pbl);
4.762 -initContext 1 Met_ ([],Pbl);
4.763 -
4.764 - "--------- this match will show some incomplete items: ---------";
4.765 -checkContext 1 ([],Pbl) (kestoreID2guh Pbl_ ["univariate","equation"]);
4.766 -checkContext 1 ([],Pbl) (kestoreID2guh Met_ ["LinEq", "solve_lineq_equation"]);
4.767 -
4.768 -
4.769 - fetchProposedTactic 1;
4.770 - setNextTactic 1 (Add_Given "solveFor x"); autoCalculate 1 (Step 1);
4.771 -
4.772 - fetchProposedTactic 1;
4.773 - setNextTactic 1 (Add_Find "solutions L"); autoCalculate 1 (Step 1);
4.774 -
4.775 - "--------- this is a matching model (all items correct): -------";
4.776 -checkContext 1 ([],Pbl) (kestoreID2guh Pbl_ ["univariate","equation"]);
4.777 - "--------- this is a NOT matching model (some 'false': ---------";
4.778 -checkContext 1 ([],Pbl)(kestoreID2guh Pbl_["linear","univariate","equation"]);
4.779 -
4.780 - "--------- find out a matching problem: ------------------------";
4.781 - "--------- find out a matching problem (FAILING: no new pbl) ---";
4.782 - refineProblem 1([],Pbl)(pblID2guh ["linear","univariate","equation"]);
4.783 -
4.784 - "--------- find out a matching problem (SUCCESSFUL) ------------";
4.785 - refineProblem 1 ([],Pbl) (pblID2guh ["univariate","equation"]);
4.786 -
4.787 - "--------- tryMatch, tryRefine did not change the calculation -";
4.788 - "--------- this is done by <TRANSFER> on the pbl-browser: ------";
4.789 - setNextTactic 1 (Specify_Problem ["normalize","polynomial",
4.790 - "univariate","equation"]);
4.791 - autoCalculate 1 (Step 1);
4.792 -(*WN050904 fetchProposedTactic again --> Specify_Problem ["normalize",...
4.793 - and Specify_Theory skipped in comparison to below ---^^^-inserted *)
4.794 -(*------------vvv-inserted-----------------------------------------------*)
4.795 - fetchProposedTactic 1;
4.796 - setNextTactic 1 (Specify_Problem ["normalize","polynomial",
4.797 - "univariate","equation"]);
4.798 - autoCalculate 1 (Step 1);
4.799 -
4.800 -(*and Specify_Theory skipped by fetchProposedTactic ?!?*)
4.801 -
4.802 - fetchProposedTactic 1;
4.803 - setNextTactic 1 (Specify_Method ["PolyEq","normalize_poly"]);
4.804 - autoCalculate 1 (Step 1);
4.805 -
4.806 - fetchProposedTactic 1;
4.807 - setNextTactic 1 (Apply_Method ["PolyEq","normalize_poly"]);
4.808 -(*========== inhibit exn 110622 ================================================
4.809 - vvvvvvvvvvvv
4.810 - autoCalculate 1 CompleteCalc;
4.811 - val ((pt,_),_) = get_calc 1;
4.812 - show_pt pt;
4.813 - val p = get_pos 1 1;
4.814 - val (Form f, tac, asms) = pt_extract (pt, p);
4.815 - if term2str f = "[x = -1, x = -3]" andalso p = ([], Res) then () else
4.816 - error "FE-interface.sml: diff.behav. in tryMatchProblem, tryRefine";
4.817 -
4.818 -(*------------^^^-inserted-----------------------------------------------*)
4.819 -(*WN050904 the fetchProposedTactic's below may not have worked like that
4.820 - before, too, because there was no check*)
4.821 - fetchProposedTactic 1;
4.822 - setNextTactic 1 (Specify_Theory "PolyEq");
4.823 - autoCalculate 1 (Step 1);
4.824 -
4.825 - fetchProposedTactic 1;
4.826 - setNextTactic 1 (Specify_Method ["PolyEq","normalize_poly"]);
4.827 - autoCalculate 1 (Step 1);
4.828 -
4.829 - fetchProposedTactic 1;
4.830 - "--------- now the calc-header is ready for enter 'solving' ----";
4.831 - autoCalculate 1 CompleteCalc;
4.832 -
4.833 - val ((pt,_),_) = get_calc 1;
4.834 -rootthy pt;
4.835 - show_pt pt;
4.836 - val p = get_pos 1 1;
4.837 - val (Form f, tac, asms) = pt_extract (pt, p);
4.838 - if term2str f = "[x = -1, x = -3]" andalso p = ([], Res) then () else
4.839 - error "FE-interface.sml: diff.behav. in tryMatchProblem, tryRefine";
4.840 -============ inhibit exn 110622 ==============================================*)
4.841 -
4.842 -
4.843 -"--------- modifyCalcHead, resetCalcHead, modelProblem --";
4.844 -"--------- modifyCalcHead, resetCalcHead, modelProblem --";
4.845 -"--------- modifyCalcHead, resetCalcHead, modelProblem --";
4.846 - states:=[];
4.847 - DEconstrCalcTree 1;
4.848 - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
4.849 - ("Test", ["sqroot-test","univariate","equation","test"],
4.850 - ["Test","squ-equ-test-subpbl1"]))];
4.851 - Iterator 1;
4.852 - moveActiveRoot 1;
4.853 -
4.854 - modifyCalcHead 1 (([],Pbl),(*the position from refFormula*)
4.855 - "solve (x+1=2, x)",(*the headline*)
4.856 - [Given ["equality (x+1=2)", "solveFor x"],
4.857 - Find ["solutions L"](*,Relate []*)],
4.858 - Pbl,
4.859 - ("Test",
4.860 - ["sqroot-test","univariate","equation","test"],
4.861 - ["Test","squ-equ-test-subpbl1"]));
4.862 -
4.863 -val ((Nd (PblObj {env = NONE,
4.864 - fmz = (fm, tpm),
4.865 - loc = (SOME scrst_ctxt, NONE),
4.866 - ctxt,
4.867 - cell = NONE,
4.868 - meth,
4.869 - spec = (thy,
4.870 - ["sqroot-test", "univariate", "equation", "test"],
4.871 - ["Test", "squ-equ-test-subpbl1"]),
4.872 - probl,
4.873 - branch = TransitiveB,
4.874 - origin,
4.875 - ostate = Incomplete,
4.876 - result},
4.877 - []),
4.878 - ([], Pbl)),
4.879 - []) = get_calc 1;
4.880 -(*WN110622: is the same as in 2002, but shouldn't be probl = [3 items?]*)
4.881 -if length meth = 0 andalso length probl = 0 (*just some items tested*) then ()
4.882 -else error "--- modifyCalcHead, resetCalcHead, modelProblem 1 --";
4.883 -
4.884 -resetCalcHead 1;
4.885 -modelProblem 1;
4.886 -
4.887 -get_calc 1;
4.888 -val ((Nd (PblObj {env = NONE,
4.889 - fmz = (fm, tpm),
4.890 - loc = (SOME scrst_ctxt, NONE),
4.891 - ctxt,
4.892 - cell = NONE,
4.893 - meth,
4.894 - spec = ("e_domID", ["e_pblID"], ["e_metID"]),
4.895 - probl,
4.896 - branch = TransitiveB,
4.897 - origin,
4.898 - ostate = Incomplete,
4.899 - result},
4.900 - []),
4.901 - ([], Pbl)),
4.902 - []) = get_calc 1;
4.903 -if length meth = 3 andalso length probl = 3 (*just some items tested*) then ()
4.904 -else error "--- modifyCalcHead, resetCalcHead, modelProblem 2 --";
4.905 -
4.906 -"--------- maximum-example, UC: Modeling an example -----";
4.907 -"--------- maximum-example, UC: Modeling an example -----";
4.908 -"--------- maximum-example, UC: Modeling an example -----";
4.909 -(* {\bf\UC{Editing the Model}\label{SPECIFY:enter}\label{SPECIFY:check}\\}
4.910 -see isac.bridge.TestModel#testEditItems
4.911 -*)
4.912 - val elems = ["fixedValues [r=Arbfix]","maximum A","valuesFor [a,b]",
4.913 - "relations [A=a*b, (a/2)^2 + (b/2)^2 = r^2]",
4.914 - "relations [A=a*b, (a/2)^2 + (b/2)^2 = r^2]",
4.915 - "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]",
4.916 - (*^^^ these are the elements for the root-problem (in variants)*)
4.917 - (*vvv these are elements required for subproblems*)
4.918 - "boundVariable a","boundVariable b","boundVariable alpha",
4.919 - "interval {x::real. 0 <= x & x <= 2*r}",
4.920 - "interval {x::real. 0 <= x & x <= 2*r}",
4.921 - "interval {x::real. 0 <= x & x <= pi}",
4.922 - "errorBound (eps=(0::real))"]
4.923 - (*specifying is not interesting for this example*)
4.924 - val spec = ("DiffApp", ["maximum_of","function"],
4.925 - ["DiffApp","max_by_calculus"]);
4.926 - (*the empty model with descriptions for user-guidance by Model_Problem*)
4.927 - val empty_model = [Given ["fixedValues []"],
4.928 - Find ["maximum", "valuesFor"],
4.929 - Relate ["relations []"]];
4.930 - states:=[];
4.931 - DEconstrCalcTree 1;
4.932 - CalcTree [(elems, spec)];
4.933 - Iterator 1;
4.934 - moveActiveRoot 1;
4.935 - refFormula 1 (get_pos 1 1);
4.936 - (*this gives a completely empty model*)
4.937 -
4.938 - fetchProposedTactic 1;
4.939 -(*fill the CalcHead with Descriptions...*)
4.940 - setNextTactic 1 (Model_Problem );
4.941 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
4.942 -
4.943 - (*user input is !!!!!EITHER!!!!! _some_ (at least one) items of the model
4.944 - !!!!!OR!!!!! _one_ part of the specification !!!!!!!!!!!!!*)
4.945 - (*input of two items, 'fixedValues [r=Arbfix]' and 'maximum b'...*)
4.946 - modifyCalcHead 1 (([],Pbl) (*position, from previous refFormula*),
4.947 - "Problem (DiffApp.thy, [maximum_of, function])",
4.948 - (*the head-form ^^^ is not used for input here*)
4.949 - [Given ["fixedValues [r=Arbfix]"(*new input*)],
4.950 - Find ["maximum b"(*new input*), "valuesFor"],
4.951 - Relate ["relations"]],
4.952 - (*input (Arbfix will dissappear soon)*)
4.953 - Pbl (*belongsto*),
4.954 - e_spec (*no input to the specification*));
4.955 -
4.956 - (*the user does not know, what 'superfluous' for 'maximum b' may mean
4.957 - and asks what to do next*)
4.958 - fetchProposedTactic 1;
4.959 - (*the student follows the advice*)
4.960 - setNextTactic 1 (Add_Find "maximum A"); (*FIXME.17.11.03: does not yet work*)
4.961 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
4.962 -
4.963 - (*this input completes the model*)
4.964 - modifyCalcHead 1 (([],Pbl), "not used here",
4.965 - [Given ["fixedValues [r=Arbfix]"],
4.966 - Find ["maximum A", "valuesFor [a,b]"(*new input*)],
4.967 - Relate ["relations [A=a*b, \
4.968 - \(a/2)^2 + (b/2)^2 = r^2]"]], Pbl, e_spec);
4.969 -
4.970 - (*specification is not interesting an should be skipped by the dialogguide;
4.971 - !!!!!!!!!!!!!!!!!!!! input of ONE part at a time !!!!!!!!!!!!!!!!!!!!!!*)
4.972 - modifyCalcHead 1 (([],Pbl), "not used here",
4.973 - [Given ["fixedValues [r=Arbfix]"],
4.974 - Find ["maximum A", "valuesFor [a,b]"(*new input*)],
4.975 - Relate ["relations [A=a*b, \
4.976 - \(a/2)^2 + (b/2)^2 = r^2]"]], Pbl,
4.977 - ("DiffApp", ["e_pblID"], ["e_metID"]));
4.978 - modifyCalcHead 1 (([],Pbl), "not used here",
4.979 - [Given ["fixedValues [r=Arbfix]"],
4.980 - Find ["maximum A", "valuesFor [a,b]"(*new input*)],
4.981 - Relate ["relations [A=a*b, \
4.982 - \(a/2)^2 + (b/2)^2 = r^2]"]], Pbl,
4.983 - ("DiffApp", ["maximum_of","function"],
4.984 - ["e_metID"]));
4.985 - modifyCalcHead 1 (([],Pbl), "not used here",
4.986 - [Given ["fixedValues [r=Arbfix]"],
4.987 - Find ["maximum A", "valuesFor [a,b]"(*new input*)],
4.988 - Relate ["relations [A=a*b, \
4.989 - \(a/2)^2 + (b/2)^2 = r^2]"]], Pbl,
4.990 - ("DiffApp", ["maximum_of","function"],
4.991 - ["DiffApp","max_by_calculus"]));
4.992 - (*this final calcHead now has STATUS 'complete' !*)
4.993 - DEconstrCalcTree 1;
4.994 -
4.995 -"--------- solve_linear from pbl-hierarchy --------------";
4.996 -"--------- solve_linear from pbl-hierarchy --------------";
4.997 -"--------- solve_linear from pbl-hierarchy --------------";
4.998 - states:=[];
4.999 - val (fmz, sp) = ([], ("", ["linear","univariate","equation","test"], []));
4.1000 - CalcTree [(fmz, sp)];
4.1001 - Iterator 1; moveActiveRoot 1;
4.1002 - refFormula 1 (get_pos 1 1);
4.1003 - modifyCalcHead 1 (([],Pbl),"solve (1+-1*2+x=0)",
4.1004 - [Given ["equality (1+-1*2+x=0)", "solveFor x"],
4.1005 - Find ["solutions L"]],
4.1006 - Pbl,
4.1007 - ("Test", ["linear","univariate","equation","test"],
4.1008 - ["Test","solve_linear"]));
4.1009 - autoCalculate 1 CompleteCalc;
4.1010 - refFormula 1 (get_pos 1 1);
4.1011 - val ((pt,_),_) = get_calc 1;
4.1012 - val p = get_pos 1 1;
4.1013 - val (Form f, tac, asms) = pt_extract (pt, p);
4.1014 - if term2str f = "[x = 1]" andalso p = ([], Res)
4.1015 - andalso terms2str asms = "[\"matches (?a = ?b) (1 + -1 * 2 + x = 0)\"]" then ()
4.1016 - else error "FE-interface.sml: diff.behav. in from pbl -hierarchy";
4.1017 -
4.1018 -"--------- solve_linear as in an algebra system (CAS)----";
4.1019 -"--------- solve_linear as in an algebra system (CAS)----";
4.1020 -"--------- solve_linear as in an algebra system (CAS)----";
4.1021 - states:=[];
4.1022 - val (fmz, sp) = ([], ("", [], []));
4.1023 - CalcTree [(fmz, sp)];
4.1024 - Iterator 1; moveActiveRoot 1;
4.1025 - modifyCalcHead 1 (([],Pbl),"solveTest (1+-1*2+x=0,x)", [], Pbl, ("", [], []));
4.1026 - autoCalculate 1 CompleteCalc;
4.1027 - refFormula 1 (get_pos 1 1);
4.1028 - val ((pt,_),_) = get_calc 1;
4.1029 - val p = get_pos 1 1;
4.1030 - val (Form f, tac, asms) = pt_extract (pt, p);
4.1031 - if term2str f = "[x = 1]" andalso p = ([], Res)
4.1032 - andalso terms2str asms = "[\"matches (?a = ?b) (1 + -1 * 2 + x = 0)\"]" then ()
4.1033 - else error "FE-interface.sml: diff.behav. in from pbl -hierarchy";
4.1034 -
4.1035 -"--------- interSteps: on 'miniscript with mini-subpbl' -";
4.1036 -"--------- interSteps: on 'miniscript with mini-subpbl' -";
4.1037 -"--------- interSteps: on 'miniscript with mini-subpbl' -";
4.1038 - states:=[];
4.1039 - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
4.1040 - ("Test", ["sqroot-test","univariate","equation","test"],
4.1041 - ["Test","squ-equ-test-subpbl1"]))];
4.1042 - Iterator 1;
4.1043 - moveActiveRoot 1;
4.1044 - autoCalculate 1 CompleteCalc;
4.1045 - val ((pt,_),_) = get_calc 1;
4.1046 - show_pt pt;
4.1047 -
4.1048 - (*UC\label{SOLVE:INFO:intermediate-steps}*)
4.1049 - interSteps 1 ([2],Res);
4.1050 - val ((pt,_),_) = get_calc 1; show_pt pt (*new ([2,1],Frm)..([2,6],Res)*);
4.1051 - val (unc, del, gen) = (([1],Res),([1],Res),([2,6],Res));
4.1052 - getFormulaeFromTo 1 unc gen 1 false;
4.1053 -
4.1054 - (*UC\label{SOLVE:INFO:intermediate-steps}*)
4.1055 - interSteps 1 ([3,2],Res);
4.1056 - val ((pt,_),_) = get_calc 1; show_pt pt (*new ([3,2,1],Frm)..([3,2,2],Res)*);
4.1057 - val (unc, del, gen) = (([3,1],Res),([3,1],Res),([3,2,2],Res));
4.1058 - getFormulaeFromTo 1 unc gen 1 false;
4.1059 -
4.1060 - (*UC\label{SOLVE:INFO:intermediate-steps}*)
4.1061 - interSteps 1 ([3],Res) (*no new steps in subproblems*);
4.1062 - val (unc, del, gen) = (([3],Pbl),([3],Pbl),([3,2],Res));
4.1063 - getFormulaeFromTo 1 unc gen 1 false;
4.1064 -
4.1065 - (*UC\label{SOLVE:INFO:intermediate-steps}*)
4.1066 - interSteps 1 ([],Res) (*no new steps in subproblems*);
4.1067 - val (unc, del, gen) = (([],Pbl),([],Pbl),([4],Res));
4.1068 - getFormulaeFromTo 1 unc gen 1 false;
4.1069 -
4.1070 -
4.1071 -"--------- getTactic, fetchApplicableTactics ------------";
4.1072 -"--------- getTactic, fetchApplicableTactics ------------";
4.1073 -"--------- getTactic, fetchApplicableTactics ------------";
4.1074 - states:=[];
4.1075 - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
4.1076 - ("Test", ["sqroot-test","univariate","equation","test"],
4.1077 - ["Test","squ-equ-test-subpbl1"]))];
4.1078 - Iterator 1; moveActiveRoot 1;
4.1079 - autoCalculate 1 CompleteCalc;
4.1080 - val ((pt,_),_) = get_calc 1;
4.1081 - show_pt pt;
4.1082 -
4.1083 - (*UC\label{SOLVE:HIDE:getTactic}*)
4.1084 - getTactic 1 ([],Pbl);
4.1085 - getTactic 1 ([1],Res);
4.1086 - getTactic 1 ([3],Pbl);
4.1087 - getTactic 1 ([3,1],Frm);
4.1088 - getTactic 1 ([3],Res);
4.1089 - getTactic 1 ([],Res);
4.1090 -
4.1091 -(*UC\label{SOLVE:MANUAL:TACTIC:listall}*)
4.1092 - fetchApplicableTactics 1 99999 ([],Pbl);
4.1093 - fetchApplicableTactics 1 99999 ([1],Res);
4.1094 - fetchApplicableTactics 1 99999 ([3],Pbl);
4.1095 - fetchApplicableTactics 1 99999 ([3,1],Res);
4.1096 - fetchApplicableTactics 1 99999 ([3],Res);
4.1097 - fetchApplicableTactics 1 99999 ([],Res);
4.1098 -
4.1099 -
4.1100 -"--------- getAssumptions, getAccumulatedAsms -----------";
4.1101 -"--------- getAssumptions, getAccumulatedAsms -----------";
4.1102 -"--------- getAssumptions, getAccumulatedAsms -----------";
4.1103 -states:=[];
4.1104 -CalcTree
4.1105 -[(["equality (x/(x^2 - 6*x+9) - 1/(x^2 - 3*x) =1/x)",
4.1106 - "solveFor x","solutions L"],
4.1107 - ("RatEq",["univariate","equation"],["no_met"]))];
4.1108 -Iterator 1; moveActiveRoot 1;
4.1109 -autoCalculate 1 CompleteCalc;
4.1110 -val ((pt,_),_) = get_calc 1;
4.1111 -val p = get_pos 1 1;
4.1112 -val (Form f, tac, asms) = pt_extract (pt, p);
4.1113 -if map term2str asms =
4.1114 - ["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",
4.1115 - "lhs (-6 * x + 5 * x ^^^ 2 = 0) is_poly_in x",
4.1116 - "lhs (-6 * x + 5 * x ^^^ 2 = 0) has_degree_in x = 2",
4.1117 - "9 * x + -6 * x ^^^ 2 + x ^^^ 3 ~= 0"]
4.1118 -andalso term2str f = "[-6 * x + 5 * x ^^^ 2 = 0]" andalso p = ([], Res) then ()
4.1119 -else error "TODO compare 2002--2011";
4.1120 -
4.1121 -(*UC\label{SOLVE:HELP:assumptions}*)
4.1122 -getAssumptions 1 ([3], Res);
4.1123 -getAssumptions 1 ([5], Res);
4.1124 -(*UC\label{SOLVE:HELP:assumptions-origin} WN0502 still without positions*)
4.1125 -getAccumulatedAsms 1 ([3], Res);
4.1126 -getAccumulatedAsms 1 ([5], Res);
4.1127 -
4.1128 -
4.1129 -"--------- arbitrary combinations of steps --------------";
4.1130 -"--------- arbitrary combinations of steps --------------";
4.1131 -"--------- arbitrary combinations of steps --------------";
4.1132 - states:=[];
4.1133 - CalcTree (*start of calculation, return No.1*)
4.1134 - [(["equality (1+-1*2+x=0)", "solveFor x","solutions L"],
4.1135 - ("Test",
4.1136 - ["linear","univariate","equation","test"],
4.1137 - ["Test","solve_linear"]))];
4.1138 - Iterator 1; moveActiveRoot 1;
4.1139 -
4.1140 - fetchProposedTactic 1;
4.1141 -(*========== inhibit exn 110628 ================================================
4.1142 - ERROR get_calc 1 not existent
4.1143 - setNextTactic 1 (Model_Problem );
4.1144 - autoCalculate 1 (Step 1);
4.1145 -
4.1146 - fetchProposedTactic 1;
4.1147 - fetchProposedTactic 1;
4.1148 -
4.1149 - setNextTactic 1 (Add_Find "solutions L");
4.1150 - setNextTactic 1 (Add_Find "solutions L");
4.1151 -
4.1152 - autoCalculate 1 (Step 1);
4.1153 - autoCalculate 1 (Step 1);
4.1154 -
4.1155 - setNextTactic 1 (Specify_Theory "Test");
4.1156 - fetchProposedTactic 1;
4.1157 - autoCalculate 1 (Step 1);
4.1158 -
4.1159 - autoCalculate 1 (Step 1);
4.1160 - autoCalculate 1 (Step 1);
4.1161 - autoCalculate 1 (Step 1);
4.1162 - autoCalculate 1 (Step 1);
4.1163 -(*------------------------- end calc-head*)
4.1164 -
4.1165 - fetchProposedTactic 1;
4.1166 - setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "isolate_bdv"));
4.1167 - autoCalculate 1 (Step 1);
4.1168 -
4.1169 - setNextTactic 1 (Rewrite_Set "Test_simplify");
4.1170 - fetchProposedTactic 1;
4.1171 - autoCalculate 1 (Step 1);
4.1172 -
4.1173 - autoCalculate 1 CompleteCalc;
4.1174 - val ((pt,_),_) = get_calc 1;
4.1175 - val p = get_pos 1 1;
4.1176 - val (Form f, tac, asms) = pt_extract (pt, p);
4.1177 - if term2str f = "[x = 1]" andalso p = ([], Res) then () else
4.1178 - error "FE-interface.sml: diff.behav. in combinations of steps";
4.1179 -============ inhibit exn 11062 ==============================================*)
4.1180 -
4.1181 -
4.1182 -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}right";
4.1183 -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}right";
4.1184 -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}right";
4.1185 - states:=[];
4.1186 - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
4.1187 - ("Test", ["sqroot-test","univariate","equation","test"],
4.1188 - ["Test","squ-equ-test-subpbl1"]))];
4.1189 - Iterator 1;
4.1190 - moveActiveRoot 1;
4.1191 - autoCalculate 1 CompleteCalcHead;
4.1192 - autoCalculate 1 (Step 1);
4.1193 - autoCalculate 1 (Step 1);
4.1194 - appendFormula 1 "-1 + x = 0";
4.1195 - (*... returns calcChangedEvent with*)
4.1196 - val (unc, del, gen) = (([1],Res), ([1],Res), ([2],Res));
4.1197 - getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
4.1198 -
4.1199 - val ((pt,_),_) = get_calc 1;
4.1200 - val p = get_pos 1 1;
4.1201 - val (Form f, tac, asms) = pt_extract (pt, p);
4.1202 - if term2str f = "-1 + x = 0" andalso p = ([2], Res) then () else
4.1203 - error "FE-interface.sml: diff.behav. in FORMULA:enter} right";
4.1204 -
4.1205 -
4.1206 -
4.1207 -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}other";
4.1208 -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}other";
4.1209 -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}other";
4.1210 - states:=[];
4.1211 - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
4.1212 - ("Test", ["sqroot-test","univariate","equation","test"],
4.1213 - ["Test","squ-equ-test-subpbl1"]))];
4.1214 - Iterator 1;
4.1215 - moveActiveRoot 1;
4.1216 - autoCalculate 1 CompleteCalcHead;
4.1217 - autoCalculate 1 (Step 1);
4.1218 - autoCalculate 1 (Step 1);
4.1219 - appendFormula 1 "x - 1 = 0";
4.1220 - val (unc, del, gen) = (([1],Res), ([1],Res), ([2],Res));
4.1221 - getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
4.1222 - (*11 elements !!!*)
4.1223 -
4.1224 - val ((pt,_),_) = get_calc 1;
4.1225 - val p = get_pos 1 1;
4.1226 - val (Form f, tac, asms) = pt_extract (pt, p);
4.1227 - if term2str f = "x - 1 = 0" andalso p = ([2], Res) then () else
4.1228 - error "FE-interface.sml: diff.behav. in FORMULA:enter} other";
4.1229 -
4.1230 -
4.1231 -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}oth 2";
4.1232 -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}oth 2";
4.1233 -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}oth 2";
4.1234 - states:=[];
4.1235 - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
4.1236 - ("Test", ["sqroot-test","univariate","equation","test"],
4.1237 - ["Test","squ-equ-test-subpbl1"]))];
4.1238 - Iterator 1;
4.1239 - moveActiveRoot 1;
4.1240 - autoCalculate 1 CompleteCalcHead;
4.1241 - autoCalculate 1 (Step 1);
4.1242 - autoCalculate 1 (Step 1);
4.1243 - appendFormula 1 "x = 1";
4.1244 - (*... returns calcChangedEvent with*)
4.1245 - val (unc, del, gen) = (([1],Res), ([1],Res), ([3,2],Res));
4.1246 - getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
4.1247 - (*6 elements !!!*)
4.1248 -
4.1249 - val ((pt,_),_) = get_calc 1;
4.1250 - val p = get_pos 1 1;
4.1251 - val (Form f, tac, asms) = pt_extract (pt, p);
4.1252 -(*========== inhibit exn 110628 ================================================*)
4.1253 - if term2str f = "x = 1" andalso p = ([3,2], Res) then () else
4.1254 - error "FE-interface.sml: diff.behav. in FORMULA:enter} oth 2";
4.1255 -(*============ inhibit exn 110682 ==============================================*)
4.1256 -
4.1257 -
4.1258 -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}NOTok";
4.1259 -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}NOTok";
4.1260 -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}NOTok";
4.1261 - states:=[];
4.1262 - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
4.1263 - ("Test", ["sqroot-test","univariate","equation","test"],
4.1264 - ["Test","squ-equ-test-subpbl1"]))];
4.1265 - Iterator 1;
4.1266 - moveActiveRoot 1;
4.1267 - autoCalculate 1 CompleteCalcHead;
4.1268 - autoCalculate 1 (Step 1);
4.1269 - autoCalculate 1 (Step 1);
4.1270 - appendFormula 1 "x - 4711 = 0";
4.1271 - (*... returns <ERROR> no derivation found </ERROR>*)
4.1272 -
4.1273 - val ((pt,_),_) = get_calc 1;
4.1274 - val p = get_pos 1 1;
4.1275 - val (Form f, tac, asms) = pt_extract (pt, p);
4.1276 - if term2str f = "x + 1 + -1 * 2 = 0" andalso p = ([1], Res) then () else
4.1277 - error "FE-interface.sml: diff.behav. in FORMULA:enter} NOTok";
4.1278 -
4.1279 -
4.1280 -"--------- replaceFormula {SOL:MAN:FOR:replace} right----";
4.1281 -"--------- replaceFormula {SOL:MAN:FOR:replace} right----";
4.1282 -"--------- replaceFormula {SOL:MAN:FOR:replace} right----";
4.1283 - states:=[];
4.1284 - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
4.1285 - ("Test", ["sqroot-test","univariate","equation","test"],
4.1286 - ["Test","squ-equ-test-subpbl1"]))];
4.1287 - Iterator 1;
4.1288 - moveActiveRoot 1;
4.1289 - autoCalculate 1 CompleteCalc;
4.1290 - moveActiveFormula 1 ([2],Res);
4.1291 - replaceFormula 1 "-1 + x = 0" (*i.e. repeats input*);
4.1292 - (*... returns <ERROR> formula not changed </ERROR>*)
4.1293 -
4.1294 - val ((pt,_),_) = get_calc 1;
4.1295 - val p = get_pos 1 1;
4.1296 - val (Form f, tac, asms) = pt_extract (pt, p);
4.1297 - if term2str f = "-1 + x = 0" andalso p = ([2], Res) then () else
4.1298 - error "FE-interface.sml: diff.behav. in FORMULA:replace} right 1";
4.1299 - if map fst (get_interval ([2],Res) ([],Res) 9999 pt) =
4.1300 - [([2], Res), ([3], Pbl), ([3, 1], Frm), ([3, 1], Res), ([3, 2], Res),
4.1301 - ([3], Res), ([4], Res), ([], Res)] then () (*nothing deleted!*) else
4.1302 - error "FE-interface.sml: diff.behav. in FORMULA:replace} right 2";
4.1303 -
4.1304 -(*WN050211 replaceFormula didn't work on second ctree: thus now tested...*)
4.1305 - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
4.1306 - ("Test", ["sqroot-test","univariate","equation","test"],
4.1307 - ["Test","squ-equ-test-subpbl1"]))];
4.1308 - Iterator 2;
4.1309 - moveActiveRoot 2;
4.1310 - autoCalculate 2 CompleteCalc;
4.1311 - moveActiveFormula 2 ([2],Res);
4.1312 - replaceFormula 2 "-1 + x = 0" (*i.e. repeats input*);
4.1313 - (*... returns <ERROR> formula not changed </ERROR>*)
4.1314 -
4.1315 - val ((pt,_),_) = get_calc 2;
4.1316 - val p = get_pos 2 1;
4.1317 - val (Form f, tac, asms) = pt_extract (pt, p);
4.1318 - if term2str f = "-1 + x = 0" andalso p = ([2], Res) then () else
4.1319 - error "FE-interface.sml: diff.behav. in FORMULA:replace} right 1";
4.1320 - if map fst (get_interval ([2],Res) ([],Res) 9999 pt) =
4.1321 - [([2], Res), ([3], Pbl), ([3, 1], Frm), ([3, 1], Res), ([3, 2], Res),
4.1322 - ([3], Res), ([4], Res), ([], Res)] then () (*nothing deleted!*) else
4.1323 - error "FE-interface.sml: diff.behav. in FORMULA:replace} right 2b";
4.1324 -
4.1325 -"--------- replaceFormula {SOL:MAN:FOR:replace} other----";
4.1326 -"--------- replaceFormula {SOL:MAN:FOR:replace} other----";
4.1327 -"--------- replaceFormula {SOL:MAN:FOR:replace} other----";
4.1328 - states:=[];
4.1329 - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
4.1330 - ("Test", ["sqroot-test","univariate","equation","test"],
4.1331 - ["Test","squ-equ-test-subpbl1"]))];
4.1332 - Iterator 1;
4.1333 - moveActiveRoot 1;
4.1334 - autoCalculate 1 CompleteCalc;
4.1335 - moveActiveFormula 1 ([2],Res); (*there is "-1 + x = 0"*)
4.1336 - replaceFormula 1 "x - 1 = 0"; (*<-------------------------------------*)
4.1337 - (*... returns calcChangedEvent with*)
4.1338 - val (unc, del, gen) = (([1],Res), ([4],Res), ([2],Res));
4.1339 - getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
4.1340 -
4.1341 - val ((pt,_),_) = get_calc 1;
4.1342 - show_pt pt;
4.1343 - val p = get_pos 1 1;
4.1344 - val (Form f, tac, asms) = pt_extract (pt, p);
4.1345 - if term2str f = "x - 1 = 0" andalso p = ([2], Res) then () else
4.1346 - error "FE-interface.sml: diff.behav. in FORMULA:replace} other 1";
4.1347 -(* for getting the list in whole length ...
4.1348 -print_depth 99;map fst (get_interval ([1],Res) ([],Res) 9999 pt);print_depth 3;
4.1349 - *)
4.1350 - if map fst (get_interval ([1],Res) ([],Res) 9999 pt) =
4.1351 - [([1], Res), ([2, 1], Frm), ([2, 1], Res), ([2, 2], Res), ([2, 3], Res),
4.1352 - ([2, 4], Res), ([2, 5], Res), ([2, 6], Res), ([2, 7], Res),
4.1353 - ([2, 8], Res), ([2, 9], Res), ([2], Res)
4.1354 -(*WN060727 {cutlevup->test_trans} removed: ,
4.1355 - ([], Res)(*dropped, if test_trans doesnt stop at PblNd*)*)] then () else
4.1356 - error "FE-interface.sml: diff.behav. in FORMULA:replace} other 2";
4.1357 -
4.1358 -
4.1359 -"--------- replaceFormula {SOL:MAN:FOR:replace} other 2--";
4.1360 -"--------- replaceFormula {SOL:MAN:FOR:replace} other 2--";
4.1361 -"--------- replaceFormula {SOL:MAN:FOR:replace} other 2--";
4.1362 - states:=[];
4.1363 - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
4.1364 - ("Test", ["sqroot-test","univariate","equation","test"],
4.1365 - ["Test","squ-equ-test-subpbl1"]))];
4.1366 - Iterator 1;
4.1367 - moveActiveRoot 1;
4.1368 - autoCalculate 1 CompleteCalc;
4.1369 - moveActiveFormula 1 ([2],Res); (*there is "-1 + x = 0"*)
4.1370 - replaceFormula 1 "x = 1"; (*<-------------------------------------*)
4.1371 - (*... returns calcChangedEvent with ...*)
4.1372 - val (unc, del, gen) = (([1],Res), ([4],Res), ([3,2],Res));
4.1373 - getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
4.1374 - (*9 elements !!!*)
4.1375 -
4.1376 - val ((pt,_),_) = get_calc 1;
4.1377 - show_pt pt; (*error: ...get_interval drops ([3,2],Res) ...*)
4.1378 - val (t,_) = get_obj g_result pt [3,2]; term2str t;
4.1379 - if map fst (get_interval ([1],Res) ([],Res) 9999 pt) =
4.1380 - [([1], Res), ([2], Res), ([3], Pbl), ([3, 1], Frm), ([3, 1], Res),
4.1381 - ([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res),
4.1382 - ([3,2],Res)] then () else
4.1383 - error "FE-interface.sml: diff.behav. in FORMULA:replace} oth2 1";
4.1384 -
4.1385 - val p = get_pos 1 1;
4.1386 - val (Form f, tac, asms) = pt_extract (pt, p);
4.1387 - if term2str f = "x = 1" andalso p = ([3,2], Res) then () else
4.1388 - error "FE-interface.sml: diff.behav. in FORMULA:replace} oth2 2";
4.1389 -
4.1390 -
4.1391 -"--------- replaceFormula {SOL:MAN:FOR:replace} NOTok----";
4.1392 -"--------- replaceFormula {SOL:MAN:FOR:replace} NOTok----";
4.1393 -"--------- replaceFormula {SOL:MAN:FOR:replace} NOTok----";
4.1394 - states:=[];
4.1395 - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
4.1396 - ("Test", ["sqroot-test","univariate","equation","test"],
4.1397 - ["Test","squ-equ-test-subpbl1"]))];
4.1398 - Iterator 1;
4.1399 - moveActiveRoot 1;
4.1400 - autoCalculate 1 CompleteCalc;
4.1401 - moveActiveFormula 1 ([2],Res); (*there is "-1 + x = 0"*)
4.1402 - replaceFormula 1 "x - 4711 = 0";
4.1403 - (*... returns <ERROR> no derivation found </ERROR>*)
4.1404 -
4.1405 - val ((pt,_),_) = get_calc 1;
4.1406 - show_pt pt;
4.1407 - val p = get_pos 1 1;
4.1408 - val (Form f, tac, asms) = pt_extract (pt, p);
4.1409 - if term2str f = "-1 + x = 0" andalso p = ([2], Res) then () else
4.1410 - error "FE-interface.sml: diff.behav. in FORMULA:replace} NOTok";
4.1411 -
4.1412 -
4.1413
4.1414 *}
4.1415
4.1416 +ML{*
4.1417 +
4.1418 +*}
4.1419 +ML{*
4.1420 +p
4.1421 +*}
4.1422 +ML{*
4.1423 +
4.1424 +*}
4.1425 end
4.1426
4.1427