1.1 --- a/test/Tools/isac/Frontend/interface.sml Tue May 03 15:58:04 2011 +0200
1.2 +++ b/test/Tools/isac/Frontend/interface.sml Tue May 03 16:20:55 2011 +0200
1.3 @@ -196,11 +196,9 @@
1.4 "--------- miniscript with mini-subpbl ------------------";
1.5 "--------- miniscript with mini-subpbl ------------------";
1.6 "--------- miniscript with mini-subpbl ------------------";
1.7 - states:=[];
1.8 - CalcTree (*start of calculation, return No.1*)
1.9 - [(["equality (x+1=2)", "solveFor x","solutions L"],
1.10 - ("Test",
1.11 - ["sqroot-test","univariate","equation","test"],
1.12 + states:=[]; (*start of calculation, return No.1*)
1.13 + CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
1.14 + ("Test", ["sqroot-test","univariate","equation","test"],
1.15 ["Test","squ-equ-test-subpbl1"]))];
1.16 Iterator 1;
1.17
1.18 @@ -323,10 +321,8 @@
1.19 "--------- mini-subpbl AUTOCALCULATE Step 1 -------------";
1.20 "--------- mini-subpbl AUTOCALCULATE Step 1 -------------";
1.21 states:=[];
1.22 - CalcTree
1.23 - [(["equality (x+1=2)", "solveFor x","solutions L"],
1.24 - ("Test",
1.25 - ["sqroot-test","univariate","equation","test"],
1.26 + CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
1.27 + ("Test", ["sqroot-test","univariate","equation","test"],
1.28 ["Test","squ-equ-test-subpbl1"]))];
1.29 Iterator 1;
1.30 moveActiveRoot 1;
1.31 @@ -424,10 +420,8 @@
1.32 "--------- mini-subpbl AUTOCALCULATE CompleteCalc -------";
1.33 "--------- mini-subpbl AUTOCALCULATE CompleteCalc -------";
1.34 states:=[];
1.35 - CalcTree
1.36 - [(["equality (x+1=2)", "solveFor x","solutions L"],
1.37 - ("Test",
1.38 - ["sqroot-test","univariate","equation","test"],
1.39 + CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
1.40 + ("Test", ["sqroot-test","univariate","equation","test"],
1.41 ["Test","squ-equ-test-subpbl1"]))];
1.42 Iterator 1;
1.43 moveActiveRoot 1;
1.44 @@ -456,10 +450,8 @@
1.45 "--------- mini-subpbl AUTO CompleteCalcHead ------------";
1.46 "--------- mini-subpbl AUTO CompleteCalcHead ------------";
1.47 states:=[];
1.48 - CalcTree
1.49 - [(["equality (x+1=2)", "solveFor x","solutions L"],
1.50 - ("Test",
1.51 - ["sqroot-test","univariate","equation","test"],
1.52 + CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
1.53 + ("Test", ["sqroot-test","univariate","equation","test"],
1.54 ["Test","squ-equ-test-subpbl1"]))];
1.55 Iterator 1;
1.56 (* doesn't terminate !!!
1.57 @@ -512,10 +504,8 @@
1.58 "--------- setContext..Thy ------------------------------";
1.59 "--------- setContext..Thy ------------------------------";
1.60 states:=[];
1.61 -CalcTree
1.62 -[(["equality (x+1=2)", "solveFor x","solutions L"],
1.63 - ("Test",
1.64 - ["sqroot-test","univariate","equation","test"],
1.65 +CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
1.66 + ("Test", ["sqroot-test","univariate","equation","test"],
1.67 ["Test","squ-equ-test-subpbl1"]))];
1.68 Iterator 1; moveActiveRoot 1;
1.69 autoCalculate 1 CompleteCalcHead;
1.70 @@ -542,10 +532,8 @@
1.71 "--------- mini-subpbl AUTOCALC CompleteToSubpbl --------";
1.72 "--------- mini-subpbl AUTOCALC CompleteToSubpbl --------";
1.73 states:=[];
1.74 - CalcTree
1.75 - [(["equality (x+1=2)", "solveFor x","solutions L"],
1.76 - ("Test",
1.77 - ["sqroot-test","univariate","equation","test"],
1.78 + CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
1.79 + ("Test", ["sqroot-test","univariate","equation","test"],
1.80 ["Test","squ-equ-test-subpbl1"]))];
1.81 Iterator 1; moveActiveRoot 1;
1.82 autoCalculate 1 CompleteToSubpbl;
1.83 @@ -814,17 +802,15 @@
1.84 "--------- modifyCalcHead, resetCalcHead, modelProblem --";
1.85 states:=[];
1.86 DEconstrCalcTree 1;
1.87 - CalcTree
1.88 - [(["equality (x+1=2)", "solveFor x","solutions L"],
1.89 - ("Test",
1.90 - ["sqroot-test","univariate","equation","test"],
1.91 + CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
1.92 + ("Test", ["sqroot-test","univariate","equation","test"],
1.93 ["Test","squ-equ-test-subpbl1"]))];
1.94 Iterator 1;
1.95 moveActiveRoot 1;
1.96
1.97 modifyCalcHead 1 (([],Pbl),(*the position from refFormula*)
1.98 "solve (x+1=2, x)",(*the headline*)
1.99 - [Given ["equality (x+1=2)", "solveFor x"],
1.100 + [Given ["equality (x+1=(2::real))", "solveFor x"],
1.101 Find ["solutions L"](*,Relate []*)],
1.102 Pbl,
1.103 ("Test",
1.104 @@ -968,10 +954,8 @@
1.105 "--------- interSteps: on 'miniscript with mini-subpbl' -";
1.106 "--------- interSteps: on 'miniscript with mini-subpbl' -";
1.107 states:=[];
1.108 - CalcTree
1.109 - [(["equality (x+1=2)", "solveFor x","solutions L"],
1.110 - ("Test",
1.111 - ["sqroot-test","univariate","equation","test"],
1.112 + CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
1.113 + ("Test", ["sqroot-test","univariate","equation","test"],
1.114 ["Test","squ-equ-test-subpbl1"]))];
1.115 Iterator 1;
1.116 moveActiveRoot 1;
1.117 @@ -1006,10 +990,8 @@
1.118 "--------- getTactic, fetchApplicableTactics ------------";
1.119 "--------- getTactic, fetchApplicableTactics ------------";
1.120 states:=[];
1.121 - CalcTree
1.122 - [(["equality (x+1=2)", "solveFor x","solutions L"],
1.123 - ("Test",
1.124 - ["sqroot-test","univariate","equation","test"],
1.125 + CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
1.126 + ("Test", ["sqroot-test","univariate","equation","test"],
1.127 ["Test","squ-equ-test-subpbl1"]))];
1.128 Iterator 1; moveActiveRoot 1;
1.129 autoCalculate 1 CompleteCalc;
1.130 @@ -1108,10 +1090,8 @@
1.131 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}right";
1.132 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}right";
1.133 states:=[];
1.134 - CalcTree
1.135 - [(["equality (x+1=2)", "solveFor x","solutions L"],
1.136 - ("Test",
1.137 - ["sqroot-test","univariate","equation","test"],
1.138 + CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
1.139 + ("Test", ["sqroot-test","univariate","equation","test"],
1.140 ["Test","squ-equ-test-subpbl1"]))];
1.141 Iterator 1;
1.142 moveActiveRoot 1;
1.143 @@ -1134,10 +1114,8 @@
1.144 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}other";
1.145 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}other";
1.146 states:=[];
1.147 - CalcTree
1.148 - [(["equality (x+1=2)", "solveFor x","solutions L"],
1.149 - ("Test",
1.150 - ["sqroot-test","univariate","equation","test"],
1.151 + CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
1.152 + ("Test", ["sqroot-test","univariate","equation","test"],
1.153 ["Test","squ-equ-test-subpbl1"]))];
1.154 Iterator 1;
1.155 moveActiveRoot 1;
1.156 @@ -1160,10 +1138,8 @@
1.157 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}oth 2";
1.158 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}oth 2";
1.159 states:=[];
1.160 - CalcTree
1.161 - [(["equality (x+1=2)", "solveFor x","solutions L"],
1.162 - ("Test",
1.163 - ["sqroot-test","univariate","equation","test"],
1.164 + CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
1.165 + ("Test", ["sqroot-test","univariate","equation","test"],
1.166 ["Test","squ-equ-test-subpbl1"]))];
1.167 Iterator 1;
1.168 moveActiveRoot 1;
1.169 @@ -1187,10 +1163,8 @@
1.170 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}NOTok";
1.171 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}NOTok";
1.172 states:=[];
1.173 - CalcTree
1.174 - [(["equality (x+1=2)", "solveFor x","solutions L"],
1.175 - ("Test",
1.176 - ["sqroot-test","univariate","equation","test"],
1.177 + CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
1.178 + ("Test", ["sqroot-test","univariate","equation","test"],
1.179 ["Test","squ-equ-test-subpbl1"]))];
1.180 Iterator 1;
1.181 moveActiveRoot 1;
1.182 @@ -1211,10 +1185,8 @@
1.183 "--------- replaceFormula {SOL:MAN:FOR:replace} right----";
1.184 "--------- replaceFormula {SOL:MAN:FOR:replace} right----";
1.185 states:=[];
1.186 - CalcTree
1.187 - [(["equality (x+1=2)", "solveFor x","solutions L"],
1.188 - ("Test",
1.189 - ["sqroot-test","univariate","equation","test"],
1.190 + CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
1.191 + ("Test", ["sqroot-test","univariate","equation","test"],
1.192 ["Test","squ-equ-test-subpbl1"]))];
1.193 Iterator 1;
1.194 moveActiveRoot 1;
1.195 @@ -1234,10 +1206,8 @@
1.196 error "FE-interface.sml: diff.behav. in FORMULA:replace} right 2";
1.197
1.198 (*WN050211 replaceFormula didn't work on second ctree: thus now tested...*)
1.199 - CalcTree
1.200 - [(["equality (x+1=2)", "solveFor x","solutions L"],
1.201 - ("Test",
1.202 - ["sqroot-test","univariate","equation","test"],
1.203 + CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
1.204 + ("Test", ["sqroot-test","univariate","equation","test"],
1.205 ["Test","squ-equ-test-subpbl1"]))];
1.206 Iterator 2;
1.207 moveActiveRoot 2;
1.208 @@ -1261,10 +1231,8 @@
1.209 "--------- replaceFormula {SOL:MAN:FOR:replace} other----";
1.210 "--------- replaceFormula {SOL:MAN:FOR:replace} other----";
1.211 states:=[];
1.212 - CalcTree
1.213 - [(["equality (x+1=2)", "solveFor x","solutions L"],
1.214 - ("Test",
1.215 - ["sqroot-test","univariate","equation","test"],
1.216 + CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
1.217 + ("Test", ["sqroot-test","univariate","equation","test"],
1.218 ["Test","squ-equ-test-subpbl1"]))];
1.219 Iterator 1;
1.220 moveActiveRoot 1;
1.221 @@ -1297,10 +1265,8 @@
1.222 "--------- replaceFormula {SOL:MAN:FOR:replace} other 2--";
1.223 "--------- replaceFormula {SOL:MAN:FOR:replace} other 2--";
1.224 states:=[];
1.225 - CalcTree
1.226 - [(["equality (x+1=2)", "solveFor x","solutions L"],
1.227 - ("Test",
1.228 - ["sqroot-test","univariate","equation","test"],
1.229 + CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
1.230 + ("Test", ["sqroot-test","univariate","equation","test"],
1.231 ["Test","squ-equ-test-subpbl1"]))];
1.232 Iterator 1;
1.233 moveActiveRoot 1;
1.234 @@ -1331,10 +1297,8 @@
1.235 "--------- replaceFormula {SOL:MAN:FOR:replace} NOTok----";
1.236 "--------- replaceFormula {SOL:MAN:FOR:replace} NOTok----";
1.237 states:=[];
1.238 - CalcTree
1.239 - [(["equality (x+1=2)", "solveFor x","solutions L"],
1.240 - ("Test",
1.241 - ["sqroot-test","univariate","equation","test"],
1.242 + CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
1.243 + ("Test", ["sqroot-test","univariate","equation","test"],
1.244 ["Test","squ-equ-test-subpbl1"]))];
1.245 Iterator 1;
1.246 moveActiveRoot 1;
2.1 --- a/test/Tools/isac/Interpret/calchead.sml Tue May 03 15:58:04 2011 +0200
2.2 +++ b/test/Tools/isac/Interpret/calchead.sml Tue May 03 16:20:55 2011 +0200
2.3 @@ -26,10 +26,8 @@
2.4 "--------- get_interval after replace} other 2 ----------";
2.5 "--------- get_interval after replace} other 2 ----------";
2.6 states := [];
2.7 - CalcTree
2.8 - [(["equality (x+1=2)", "solveFor x","solutions L"],
2.9 - ("Test",
2.10 - ["sqroot-test","univariate","equation","test"],
2.11 + CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
2.12 + ("Test", ["sqroot-test","univariate","equation","test"],
2.13 ["Test","squ-equ-test-subpbl1"]))];
2.14 Iterator 1;
2.15 moveActiveRoot 1;
3.1 --- a/test/Tools/isac/Interpret/ctree.sml Tue May 03 15:58:04 2011 +0200
3.2 +++ b/test/Tools/isac/Interpret/ctree.sml Tue May 03 16:20:55 2011 +0200
3.3 @@ -323,8 +323,7 @@
3.4 "=====new ptree 1a miniscript with mini-subpbl ===================";
3.5 "=====new ptree 1a miniscript with mini-subpbl ===================";
3.6 "=====new ptree 1a miniscript with mini-subpbl ===================";
3.7 -val fmz = ["equality (x+1=2)",
3.8 - "solveFor x","solutions L"];
3.9 +val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
3.10 val (dI',pI',mI') =
3.11 ("Test",["sqroot-test","univariate","equation","test"],
3.12 ["Test","squ-equ-test-subpbl1"]);
3.13 @@ -366,10 +365,8 @@
3.14 "=====new ptree 2 miniscript with mini-subpbl ====================";
3.15 "=====new ptree 2 miniscript with mini-subpbl ====================";
3.16 states:=[];
3.17 - CalcTree
3.18 - [(["equality (x+1=2)", "solveFor x","solutions L"],
3.19 - ("Test",
3.20 - ["sqroot-test","univariate","equation","test"],
3.21 + CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
3.22 + ("Test", ["sqroot-test","univariate","equation","test"],
3.23 ["Test","squ-equ-test-subpbl1"]))];
3.24 Iterator 1; moveActiveRoot 1;
3.25 autoCalculate 1 CompleteCalc;
3.26 @@ -431,8 +428,7 @@
3.27 "-------------- cappend minisubpbl -------------------------------";
3.28 "-------------- cappend minisubpbl -------------------------------";
3.29 "=====new ptree 1 miniscript with mini-subpbl ====================";
3.30 -val fmz = ["equality (x+1=2)",
3.31 - "solveFor x","solutions L"];
3.32 +val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
3.33 val (dI',pI',mI') =
3.34 ("Test",["sqroot-test","univariate","equation","test"],
3.35 ["Test","squ-equ-test-subpbl1"]);
3.36 @@ -533,10 +529,8 @@
3.37 "=====new ptree 3 ================================================";
3.38 "=====new ptree 3 ================================================";
3.39 states:=[];
3.40 - CalcTree
3.41 - [(["equality (x+1=2)", "solveFor x","solutions L"],
3.42 - ("Test",
3.43 - ["sqroot-test","univariate","equation","test"],
3.44 + CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
3.45 + ("Test", ["sqroot-test","univariate","equation","test"],
3.46 ["Test","squ-equ-test-subpbl1"]))];
3.47 Iterator 1; moveActiveRoot 1;
3.48 autoCalculate 1 CompleteCalc;
3.49 @@ -617,10 +611,8 @@
3.50 "------ move into detail -----------------------------------------";
3.51 "------ move into detail -----------------------------------------";
3.52 states:=[];
3.53 - CalcTree
3.54 - [(["equality (x+1=2)", "solveFor x","solutions L"],
3.55 - ("Test",
3.56 - ["sqroot-test","univariate","equation","test"],
3.57 + CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
3.58 + ("Test", ["sqroot-test","univariate","equation","test"],
3.59 ["Test","squ-equ-test-subpbl1"]))];
3.60 Iterator 1; moveActiveRoot 1;
3.61 autoCalculate 1 CompleteCalc;
3.62 @@ -651,10 +643,8 @@
3.63 "=====new ptree 3a ===============================================";
3.64 "=====new ptree 3a ===============================================";
3.65 states:=[];
3.66 - CalcTree
3.67 - [(["equality (x+1=2)", "solveFor x","solutions L"],
3.68 - ("Test",
3.69 - ["sqroot-test","univariate","equation","test"],
3.70 + CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
3.71 + ("Test", ["sqroot-test","univariate","equation","test"],
3.72 ["Test","squ-equ-test-subpbl1"]))];
3.73 Iterator 1; moveActiveRoot 1;
3.74 autoCalculate 1 CompleteCalcHead;
3.75 @@ -908,10 +898,8 @@
3.76 "=====new ptree 5 minisubpbl =====================================";
3.77 "=====new ptree 5 minisubpbl =====================================";
3.78 states:=[];
3.79 -CalcTree
3.80 - [(["equality (x+1=2)", "solveFor x","solutions L"],
3.81 - ("Test",
3.82 - ["sqroot-test","univariate","equation","test"],
3.83 +CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
3.84 + ("Test", ["sqroot-test","univariate","equation","test"],
3.85 ["Test","squ-equ-test-subpbl1"]))];
3.86 Iterator 1; moveActiveRoot 1;
3.87 autoCalculate 1 CompleteCalc;
3.88 @@ -987,10 +975,8 @@
3.89 "=====new ptree 6 minisubpbl intersteps ==========================";
3.90 "=====new ptree 6 minisubpbl intersteps ==========================";
3.91 states:=[];
3.92 -CalcTree
3.93 - [(["equality (x+1=2)", "solveFor x","solutions L"],
3.94 - ("Test",
3.95 - ["sqroot-test","univariate","equation","test"],
3.96 +CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
3.97 + ("Test", ["sqroot-test","univariate","equation","test"],
3.98 ["Test","squ-equ-test-subpbl1"]))];
3.99 Iterator 1; moveActiveRoot 1;
3.100 autoCalculate 1 CompleteCalc;
4.1 --- a/test/Tools/isac/Interpret/inform.sml Tue May 03 15:58:04 2011 +0200
4.2 +++ b/test/Tools/isac/Interpret/inform.sml Tue May 03 16:20:55 2011 +0200
4.3 @@ -50,9 +50,8 @@
4.4 (writeln o term2str) sc;
4.5
4.6 states:=[];
4.7 - CalcTree [(["equality (x+1=2)", "solveFor x","solutions L"],
4.8 - ("Test",
4.9 - ["sqroot-test","univariate","equation","test"],
4.10 + CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
4.11 + ("Test", ["sqroot-test","univariate","equation","test"],
4.12 ["Test","squ-equ-test-subpbl1"]))];
4.13 Iterator 1; moveActiveRoot 1;
4.14 autoCalculate 1 CompleteCalcHead;
4.15 @@ -123,9 +122,8 @@
4.16 "--------- appendFormula: on Frm + equ_nrls ----------------------";
4.17 "--------- appendFormula: on Frm + equ_nrls ----------------------";
4.18 states:=[];
4.19 - CalcTree [(["equality (x+1=2)", "solveFor x","solutions L"],
4.20 - ("Test",
4.21 - ["sqroot-test","univariate","equation","test"],
4.22 + CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
4.23 + ("Test", ["sqroot-test","univariate","equation","test"],
4.24 ["Test","squ-equ-test-subpbl1"]))];
4.25 Iterator 1; moveActiveRoot 1;
4.26 autoCalculate 1 CompleteCalcHead;
4.27 @@ -160,9 +158,8 @@
4.28 "--------- appendFormula: on Res + NO deriv ----------------------";
4.29 "--------- appendFormula: on Res + NO deriv ----------------------";
4.30 states:=[];
4.31 - CalcTree [(["equality (x+1=2)", "solveFor x","solutions L"],
4.32 - ("Test",
4.33 - ["sqroot-test","univariate","equation","test"],
4.34 + CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
4.35 + ("Test", ["sqroot-test","univariate","equation","test"],
4.36 ["Test","squ-equ-test-subpbl1"]))];
4.37 Iterator 1; moveActiveRoot 1;
4.38 autoCalculate 1 CompleteCalcHead;
4.39 @@ -191,9 +188,8 @@
4.40 "--------- appendFormula: on Res + late deriv --------------------";
4.41 "--------- appendFormula: on Res + late deriv --------------------";
4.42 states:=[];
4.43 - CalcTree [(["equality (x+1=2)", "solveFor x","solutions L"],
4.44 - ("Test",
4.45 - ["sqroot-test","univariate","equation","test"],
4.46 + CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
4.47 + ("Test", ["sqroot-test","univariate","equation","test"],
4.48 ["Test","squ-equ-test-subpbl1"]))];
4.49 Iterator 1; moveActiveRoot 1;
4.50 autoCalculate 1 CompleteCalcHead;
4.51 @@ -222,9 +218,8 @@
4.52 "--------- appendFormula: on Res + late deriv [x = 3 + -2]---///--";
4.53 "--------- appendFormula: on Res + late deriv [x = 3 + -2]---///--";
4.54 states:=[];
4.55 - CalcTree [(["equality (x+1=2)", "solveFor x","solutions L"],
4.56 - ("Test",
4.57 - ["sqroot-test","univariate","equation","test"],
4.58 + CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
4.59 + ("Test", ["sqroot-test","univariate","equation","test"],
4.60 ["Test","squ-equ-test-subpbl1"]))];
4.61 Iterator 1; moveActiveRoot 1;
4.62 autoCalculate 1 CompleteCalcHead;
4.63 @@ -248,9 +243,8 @@
4.64 "--------- replaceFormula: on Res + = ----------------------------";
4.65 "--------- replaceFormula: on Res + = ----------------------------";
4.66 states:=[];
4.67 - CalcTree [(["equality (x+1=2)", "solveFor x","solutions L"],
4.68 - ("Test",
4.69 - ["sqroot-test","univariate","equation","test"],
4.70 + CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
4.71 + ("Test", ["sqroot-test","univariate","equation","test"],
4.72 ["Test","squ-equ-test-subpbl1"]))];
4.73 Iterator 1; moveActiveRoot 1;
4.74 autoCalculate 1 CompleteCalcHead;
4.75 @@ -274,9 +268,8 @@
4.76 "--------- replaceFormula: on Res + = 1st Nd ---------------------";
4.77 "--------- replaceFormula: on Res + = 1st Nd ---------------------";
4.78 states:=[];
4.79 - CalcTree [(["equality (x+1=2)", "solveFor x","solutions L"],
4.80 - ("Test",
4.81 - ["sqroot-test","univariate","equation","test"],
4.82 + CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
4.83 + ("Test", ["sqroot-test","univariate","equation","test"],
4.84 ["Test","squ-equ-test-subpbl1"]))];
4.85 Iterator 1; moveActiveRoot 1;
4.86 autoCalculate 1 CompleteCalcHead;
4.87 @@ -299,9 +292,8 @@
4.88 "--------- replaceFormula: on Frm + = 1st Nd ---------------------";
4.89 "--------- replaceFormula: on Frm + = 1st Nd ---------------------";
4.90 states:=[];
4.91 - CalcTree [(["equality (x+1=2)", "solveFor x","solutions L"],
4.92 - ("Test",
4.93 - ["sqroot-test","univariate","equation","test"],
4.94 + CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
4.95 + ("Test", ["sqroot-test","univariate","equation","test"],
4.96 ["Test","squ-equ-test-subpbl1"]))];
4.97 Iterator 1; moveActiveRoot 1;
4.98 autoCalculate 1 CompleteCalcHead;
4.99 @@ -323,9 +315,8 @@
4.100 "--------- replaceFormula: cut calculation -----------------------";
4.101 "--------- replaceFormula: cut calculation -----------------------";
4.102 states:=[];
4.103 - CalcTree [(["equality (x+1=2)", "solveFor x","solutions L"],
4.104 - ("Test",
4.105 - ["sqroot-test","univariate","equation","test"],
4.106 + CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
4.107 + ("Test", ["sqroot-test","univariate","equation","test"],
4.108 ["Test","squ-equ-test-subpbl1"]))];
4.109 Iterator 1; moveActiveRoot 1;
4.110 autoCalculate 1 CompleteCalc;
4.111 @@ -421,9 +412,8 @@
4.112 "--------- syntax error ------------------------------------------";
4.113 "--------- syntax error ------------------------------------------";
4.114 states:=[];
4.115 - CalcTree [(["equality (x+1=2)", "solveFor x","solutions L"],
4.116 - ("Test",
4.117 - ["sqroot-test","univariate","equation","test"],
4.118 + CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
4.119 + ("Test", ["sqroot-test","univariate","equation","test"],
4.120 ["Test","squ-equ-test-subpbl1"]))];
4.121 Iterator 1; moveActiveRoot 1;
4.122 autoCalculate 1 CompleteCalcHead;
5.1 --- a/test/Tools/isac/Interpret/mathengine.sml Tue May 03 15:58:04 2011 +0200
5.2 +++ b/test/Tools/isac/Interpret/mathengine.sml Tue May 03 16:20:55 2011 +0200
5.3 @@ -162,10 +162,8 @@
5.4 "----------- debugging setContext..pbl_ -----------------";
5.5 "----------- debugging setContext..pbl_ -----------------";
5.6 states:=[];
5.7 -CalcTree
5.8 -[(["equality (x+1=2)", "solveFor x","solutions L"],
5.9 - ("Test",
5.10 - ["sqroot-test","univariate","equation","test"],
5.11 +CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
5.12 + ("Test", ["sqroot-test","univariate","equation","test"],
5.13 ["Test","squ-equ-test-subpbl1"]))];
5.14 Iterator 1;
5.15 moveActiveRoot 1; modelProblem 1;
6.1 --- a/test/Tools/isac/Interpret/rewtools.sml Tue May 03 15:58:04 2011 +0200
6.2 +++ b/test/Tools/isac/Interpret/rewtools.sml Tue May 03 16:20:55 2011 +0200
6.3 @@ -243,11 +243,9 @@
6.4 "----------- initContext..Thy_, fun context_thm ---------";
6.5 "----------- initContext..Thy_, fun context_thm ---------";
6.6 "----------- initContext..Thy_, fun context_thm ---------";
6.7 -states:=[];
6.8 -CalcTree (*start of calculation, return No.1*)
6.9 -[(["equality (x+1=2)", "solveFor x","solutions L"],
6.10 - ("Test",
6.11 - ["sqroot-test","univariate","equation","test"],
6.12 +states:=[]; (*start of calculation, return No.1*)
6.13 +CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
6.14 + ("Test", ["sqroot-test","univariate","equation","test"],
6.15 ["Test","squ-equ-test-subpbl1"]))];
6.16 Iterator 1; moveActiveRoot 1;
6.17 autoCalculate 1 CompleteCalc;
6.18 @@ -373,11 +371,9 @@
6.19 "----------- checkContext..Thy_ on last formula ---------";
6.20 "----------- checkContext..Thy_ on last formula ---------";
6.21 "----------- checkContext..Thy_ on last formula ---------";
6.22 -states:=[];
6.23 -CalcTree (*start of calculation, return No.1*)
6.24 -[(["equality (x+1=2)", "solveFor x","solutions L"],
6.25 - ("Test",
6.26 - ["sqroot-test","univariate","equation","test"],
6.27 +states:=[]; (*start of calculation, return No.1*)
6.28 +CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
6.29 + ("Test", ["sqroot-test","univariate","equation","test"],
6.30 ["Test","squ-equ-test-subpbl1"]))];
6.31 Iterator 1; moveActiveRoot 1;
6.32
7.1 --- a/test/Tools/isac/Interpret/script.sml Tue May 03 15:58:04 2011 +0200
7.2 +++ b/test/Tools/isac/Interpret/script.sml Tue May 03 16:20:55 2011 +0200
7.3 @@ -221,10 +221,8 @@
7.4 "----------- fun sel_appl_atomic_tacs ----------------------------";
7.5 "----------- fun sel_appl_atomic_tacs ----------------------------";
7.6 states:=[];
7.7 -CalcTree
7.8 -[(["equality (x+1=2)", "solveFor x","solutions L"],
7.9 - ("Test",
7.10 - ["sqroot-test","univariate","equation","test"],
7.11 +CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
7.12 + ("Test", ["sqroot-test","univariate","equation","test"],
7.13 ["Test","squ-equ-test-subpbl1"]))];
7.14 Iterator 1;
7.15 moveActiveRoot 1;
8.1 --- a/test/Tools/isac/Interpret/solve.sml Tue May 03 15:58:04 2011 +0200
8.2 +++ b/test/Tools/isac/Interpret/solve.sml Tue May 03 16:20:55 2011 +0200
8.3 @@ -386,10 +386,8 @@
8.4 "------ interSteps'donesteps': on 'miniscript with mini-subpbl'---";
8.5 "------ interSteps'donesteps': on 'miniscript with mini-subpbl'---";
8.6 states:=[];
8.7 - CalcTree
8.8 - [(["equality (x+1=2)", "solveFor x","solutions L"],
8.9 - ("Test",
8.10 - ["sqroot-test","univariate","equation","test"],
8.11 + CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
8.12 + ("Test", ["sqroot-test","univariate","equation","test"],
8.13 ["Test","squ-equ-test-subpbl1"]))];
8.14 Iterator 1;
8.15 moveActiveRoot 1;
8.16 @@ -428,10 +426,8 @@
8.17 "------ interSteps'detailrls' after CompleteCalc -----------------";
8.18 "------ interSteps'detailrls' after CompleteCalc -----------------";
8.19 states:=[];
8.20 - CalcTree
8.21 - [(["equality (x+1=2)", "solveFor x","solutions L"],
8.22 - ("Test",
8.23 - ["sqroot-test","univariate","equation","test"],
8.24 + CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
8.25 + ("Test", ["sqroot-test","univariate","equation","test"],
8.26 ["Test","squ-equ-test-subpbl1"]))];
8.27 Iterator 1;
8.28 moveActiveRoot 1;
8.29 @@ -480,10 +476,8 @@
8.30 "------ interSteps after appendFormula ---------------------------";
8.31 "------ interSteps after appendFormula ---------------------------";
8.32 states:=[];
8.33 -CalcTree
8.34 -[(["equality (x+1=2)", "solveFor x","solutions L"],
8.35 - ("Test",
8.36 - ["sqroot-test","univariate","equation","test"],
8.37 +CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
8.38 + ("Test", ["sqroot-test","univariate","equation","test"],
8.39 ["Test","squ-equ-test-subpbl1"]))];
8.40 Iterator 1;
8.41 moveActiveRoot 1;
8.42 @@ -504,11 +498,9 @@
8.43 "------ Detail_Set -----------------------------------------------";
8.44 "------ Detail_Set -----------------------------------------------";
8.45 "------ Detail_Set -----------------------------------------------";
8.46 - states:=[];
8.47 - CalcTree (*start of calculation, return No.1*)
8.48 - [(["equality (x+1=2)", "solveFor x","solutions L"],
8.49 - ("Test",
8.50 - ["sqroot-test","univariate","equation","test"],
8.51 + states:=[]; (*start of calculation, return No.1*)
8.52 + CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
8.53 + ("Test", ["sqroot-test","univariate","equation","test"],
8.54 ["Test","squ-equ-test-subpbl1"]))];
8.55 Iterator 1; moveActiveRoot 1;
8.56 autoCalculate 1 CompleteCalcHead;
9.1 --- a/test/Tools/isac/OLDTESTS/modspec.sml Tue May 03 15:58:04 2011 +0200
9.2 +++ b/test/Tools/isac/OLDTESTS/modspec.sml Tue May 03 16:20:55 2011 +0200
9.3 @@ -12,10 +12,8 @@
9.4 "--------- get_interval after replace} other 2 -------------------";
9.5 "--------- get_interval after replace} other 2 -------------------";
9.6 states:=[];
9.7 - CalcTree
9.8 - [(["equality (x+1=2)", "solveFor x","solutions L"],
9.9 - ("Test",
9.10 - ["sqroot-test","univariate","equation","test"],
9.11 + CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
9.12 + ("Test", ["sqroot-test","univariate","equation","test"],
9.13 ["Test","squ-equ-test-subpbl1"]))];
9.14 Iterator 1;
9.15 moveActiveRoot 1;
10.1 --- a/test/Tools/isac/OLDTESTS/script.sml Tue May 03 15:58:04 2011 +0200
10.2 +++ b/test/Tools/isac/OLDTESTS/script.sml Tue May 03 16:20:55 2011 +0200
10.3 @@ -304,10 +304,8 @@
10.4 "--------- sel_rules ---------------------------------------------";
10.5 "--------- sel_rules ---------------------------------------------";
10.6 states:=[];
10.7 - CalcTree
10.8 - [(["equality (x+1=2)", "solveFor x","solutions L"],
10.9 - ("Test",
10.10 - ["sqroot-test","univariate","equation","test"],
10.11 + CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
10.12 + ("Test", ["sqroot-test","univariate","equation","test"],
10.13 ["Test","squ-equ-test-subpbl1"]))];
10.14 Iterator 1;
10.15 moveActiveRoot 1;
11.1 --- a/test/Tools/isac/OLDTESTS/subp-rooteq.sml Tue May 03 15:58:04 2011 +0200
11.2 +++ b/test/Tools/isac/OLDTESTS/subp-rooteq.sml Tue May 03 16:20:55 2011 +0200
11.3 @@ -22,14 +22,13 @@
11.4 (*###########################################################
11.5 ## 12.03 next_tac repariert (gab keine Value zurueck ###
11.6 ###########################################################*)
11.7 -val fmz = ["equality (x+1=2)",
11.8 - "solveFor x","solutions L"];
11.9 +val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
11.10 val (dI',pI',mI') =
11.11 ("Test",["sqroot-test","univariate","equation","test"],
11.12 ["Test","squ-equ-test-subpbl1"]);
11.13
11.14 - val Script sc = (#scr o get_met) ["Test","squ-equ-test-subpbl1"];
11.15 - (writeln o term2str) sc;
11.16 +val Script sc = (#scr o get_met) ["Test","squ-equ-test-subpbl1"];
11.17 +(writeln o term2str) sc;
11.18
11.19 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
11.20 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
12.1 --- a/test/Tools/isac/OLDTESTS/tacis.sml Tue May 03 15:58:04 2011 +0200
12.2 +++ b/test/Tools/isac/OLDTESTS/tacis.sml Tue May 03 16:20:55 2011 +0200
12.3 @@ -13,9 +13,8 @@
12.4 "------ fetchProposedTactic -> autoCalculate (Step1 ) ------------";
12.5 "------ fetchProposedTactic -> autoCalculate (Step1 ) ------------";
12.6 states:=[];
12.7 - CalcTree [(["equality (x+1=2)", "solveFor x","solutions L"],
12.8 - ("Test",
12.9 - ["sqroot-test","univariate","equation","test"],
12.10 + CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
12.11 + ("Test", ["sqroot-test","univariate","equation","test"],
12.12 ["Test","squ-equ-test-subpbl1"]))];
12.13 Iterator 1; moveActiveRoot 1;
12.14 autoCalculate 1 CompleteCalcHead;
12.15 @@ -84,9 +83,8 @@
12.16 "------ setNextTactic -> autoCalculate (Step1 ) ------------------";
12.17 "------ setNextTactic -> autoCalculate (Step1 ) ------------------";
12.18 states:=[];
12.19 - CalcTree [(["equality (x+1=2)", "solveFor x","solutions L"],
12.20 - ("Test",
12.21 - ["sqroot-test","univariate","equation","test"],
12.22 + CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
12.23 + ("Test", ["sqroot-test","univariate","equation","test"],
12.24 ["Test","squ-equ-test-subpbl1"]))];
12.25 Iterator 1; moveActiveRoot 1;
12.26 autoCalculate 1 CompleteCalcHead;