1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/test/Tools/isac/Interpret/inform.sml Mon Aug 30 14:35:51 2010 +0200
1.3 @@ -0,0 +1,772 @@
1.4 +(* tests on inform.sml
1.5 + author: Walther Neuper
1.6 + 060225,
1.7 + (c) due to copyright terms
1.8 +
1.9 +use"../smltest/ME/inform.sml";
1.10 +use"inform.sml";
1.11 +*)
1.12 +
1.13 +"-----------------------------------------------------------------";
1.14 +"table of contents -----------------------------------------------";
1.15 +"-----------------------------------------------------------------";
1.16 +"appendForm with miniscript with mini-subpbl:";
1.17 +"--------- appendFormula: on Res + equ_nrls ----------------------";
1.18 +"--------- appendFormula: on Frm + equ_nrls ----------------------";
1.19 +"--------- appendFormula: on Res + NO deriv ----------------------";
1.20 +"--------- appendFormula: on Res + late deriv --------------------";
1.21 +"--------- appendFormula: on Res + late deriv [x = 3 + -2]---///--";
1.22 +"replaceForm with miniscript with mini-subpbl:";
1.23 +"--------- replaceFormula: on Res + = ----------------------------";
1.24 +"--------- replaceFormula: on Res + = 1st Nd ---------------------";
1.25 +"--------- replaceFormula: on Frm + = 1st Nd ---------------------";
1.26 +"--------- replaceFormula: cut calculation -----------------------";
1.27 +"--------- replaceFormula: cut calculation -----------------------";
1.28 +(* 040307 copied from informtest.sml ... old versions
1.29 +"--------- maximum-example, UC: Modeling / modifyCalcHead --------";*)
1.30 +"--------- syntax error ------------------------------------------";
1.31 +"CAS-command:";
1.32 +"--------- CAS-command on ([],Pbl) -------------------------------";
1.33 +"--------- CAS-command on ([],Pbl) FE-interface ------------------";
1.34 +"--------- inform [rational,simplification] ----------------------";
1.35 +"--------- Take as 1st tac, start with <NEW> (CAS input) ---------";
1.36 +"--------- Take as 1st tac, start from exp -----------------------";
1.37 +"--------- init_form, start with <NEW> (CAS input) ---------------";
1.38 +"-----------------------------------------------------------------";
1.39 +"-----------------------------------------------------------------";
1.40 +"-----------------------------------------------------------------";
1.41 +
1.42 +
1.43 +
1.44 +
1.45 +
1.46 +
1.47 +"--------- appendFormula: on Res + equ_nrls ----------------------";
1.48 +"--------- appendFormula: on Res + equ_nrls ----------------------";
1.49 +"--------- appendFormula: on Res + equ_nrls ----------------------";
1.50 + val Script sc = (#scr o get_met) ["Test","squ-equ-test-subpbl1"];
1.51 + (writeln o term2str) sc;
1.52 + val Script sc = (#scr o get_met) ["Test","solve_linear"];
1.53 + (writeln o term2str) sc;
1.54 +
1.55 + states:=[];
1.56 + CalcTree [(["equality (x+1=2)", "solveFor x","solutions L"],
1.57 + ("Test.thy",
1.58 + ["sqroot-test","univariate","equation","test"],
1.59 + ["Test","squ-equ-test-subpbl1"]))];
1.60 + Iterator 1; moveActiveRoot 1;
1.61 + autoCalculate 1 CompleteCalcHead;
1.62 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
1.63 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);
1.64 +
1.65 + appendFormula 1 "-2 * 1 + (1 + x) = 0"; refFormula 1 (get_pos 1 1);
1.66 + val ((pt,_),_) = get_calc 1;
1.67 + val str = pr_ptree pr_short pt;
1.68 + writeln str;
1.69 + if str = ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + -1 * 2 = 0\n2.1. x + 1 + -1 * 2 = 0\n2.2. -1 * 2 + (x + 1) = 0\n2.3. -1 * 2 + (1 + x) = 0\n2.4. 1 + (-1 * 2 + x) = 0\n2.5. 1 + (-2 + x) = 0\n2.6. 1 + (-2 * 1 + x) = 0\n" then ()
1.70 + else raise error "inform.sml: diff.behav.appendFormula: on Res + equ 1";
1.71 +
1.72 + moveDown 1 ([ ],Pbl); refFormula 1 ([1],Frm); (*x + 1 = 2*)
1.73 + moveDown 1 ([1],Frm); refFormula 1 ([1],Res); (*x + 1 + -1 * 2 = 0*)
1.74 +
1.75 + (*the seven steps of detailed derivation*)
1.76 + moveDown 1 ([1 ],Res); refFormula 1 ([2,1],Frm);
1.77 + moveDown 1 ([2,1],Frm); refFormula 1 ([2,1],Res);
1.78 + moveDown 1 ([2,1],Res); refFormula 1 ([2,2],Res);
1.79 + moveDown 1 ([2,2],Res); refFormula 1 ([2,3],Res);
1.80 + moveDown 1 ([2,3],Res); refFormula 1 ([2,4],Res);
1.81 + moveDown 1 ([2,4],Res); refFormula 1 ([2,5],Res);
1.82 + moveDown 1 ([2,5],Res); refFormula 1 ([2,6],Res);
1.83 + val ((pt,_),_) = get_calc 1;
1.84 + if "-2 * 1 + (1 + x) = 0" = term2str (fst (get_obj g_result pt [2,6])) then()
1.85 + else raise error "inform.sml: diff.behav.appendFormula: on Res + equ 2";
1.86 +
1.87 + fetchProposedTactic 1; (*takes Iterator 1 _1_*)
1.88 + val (_,(tac,_,_)::_) = get_calc 1;
1.89 + if tac = Rewrite_Set "Test_simplify" then ()
1.90 + else raise error "inform.sml: diff.behav.appendFormula: on Res + equ 3";
1.91 + autoCalculate 1 CompleteCalc;
1.92 + val ((pt,_),_) = get_calc 1;
1.93 + if "[x = 1]" = term2str (fst (get_obj g_result pt [])) then ()
1.94 + else raise error "inform.sml: diff.behav.appendFormula: on Res + equ 4";
1.95 + (* autoCalculate 1 CompleteCalc;
1.96 + val ((pt,p),_) = get_calc 1;
1.97 + (writeln o istates2str) (get_obj g_loc pt [ ]);
1.98 + (writeln o istates2str) (get_obj g_loc pt [1]);
1.99 + (writeln o istates2str) (get_obj g_loc pt [2]);
1.100 + (writeln o istates2str) (get_obj g_loc pt [3]);
1.101 + (writeln o istates2str) (get_obj g_loc pt [3,1]);
1.102 + (writeln o istates2str) (get_obj g_loc pt [3,2]);
1.103 + (writeln o istates2str) (get_obj g_loc pt [4]);
1.104 +
1.105 + *)
1.106 +"----------------------------------------------------------";
1.107 + val fod = make_deriv Isac.thy Atools_erls
1.108 + ((#rules o rep_rls) Test_simplify)
1.109 + (sqrt_right false (theory "Pure")) NONE
1.110 + (str2term "x + 1 + -1 * 2 = 0");
1.111 + (writeln o trtas2str) fod;
1.112 +
1.113 + val ifod = make_deriv Isac.thy Atools_erls
1.114 + ((#rules o rep_rls) Test_simplify)
1.115 + (sqrt_right false (theory "Pure")) NONE
1.116 + (str2term "-2 * 1 + (1 + x) = 0");
1.117 + (writeln o trtas2str) ifod;
1.118 + fun equal (_,_,(t1, _)) (_,_,(t2, _)) = t1=t2;
1.119 + val (fod', rifod') = dropwhile' equal (rev fod) (rev ifod);
1.120 + val der = fod' @ (map rev_deriv' rifod');
1.121 + (writeln o trtas2str) der;
1.122 + "----------------------------------------------------------";
1.123 +
1.124 +
1.125 +"--------- appendFormula: on Frm + equ_nrls ----------------------";
1.126 +"--------- appendFormula: on Frm + equ_nrls ----------------------";
1.127 +"--------- appendFormula: on Frm + equ_nrls ----------------------";
1.128 + states:=[];
1.129 + CalcTree [(["equality (x+1=2)", "solveFor x","solutions L"],
1.130 + ("Test.thy",
1.131 + ["sqroot-test","univariate","equation","test"],
1.132 + ["Test","squ-equ-test-subpbl1"]))];
1.133 + Iterator 1; moveActiveRoot 1;
1.134 + autoCalculate 1 CompleteCalcHead;
1.135 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1) (*x + 1 = 2*);
1.136 +
1.137 + appendFormula 1 "2+ -1 + x = 2"; refFormula 1 (get_pos 1 1);
1.138 +
1.139 + moveDown 1 ([],Pbl); refFormula 1 ([1],Frm) (*x + 1 = 2*);
1.140 +
1.141 + moveDown 1 ([1 ],Frm); refFormula 1 ([1,1],Frm);
1.142 + moveDown 1 ([1,1],Frm); refFormula 1 ([1,1],Res);
1.143 + moveDown 1 ([1,1],Res); refFormula 1 ([1,2],Res);
1.144 + moveDown 1 ([1,2],Res); refFormula 1 ([1,3],Res);
1.145 + moveDown 1 ([1,3],Res); refFormula 1 ([1,4],Res);
1.146 + moveDown 1 ([1,4],Res); refFormula 1 ([1,5],Res);
1.147 + moveDown 1 ([1,5],Res); refFormula 1 ([1,6],Res);
1.148 + val ((pt,_),_) = get_calc 1;
1.149 + if "2 + -1 + x = 2" = term2str (fst (get_obj g_result pt [1,6])) then()
1.150 + else raise error "inform.sml: diff.behav.appendFormula: on Frm + equ 1";
1.151 +
1.152 + fetchProposedTactic 1; (*takes Iterator 1 _1_*)
1.153 + val (_,(tac,_,_)::_) = get_calc 1;
1.154 + if tac = Rewrite_Set "norm_equation" then ()
1.155 + else raise error "inform.sml: diff.behav.appendFormula: on Frm + equ 2";
1.156 + autoCalculate 1 CompleteCalc;
1.157 + val ((pt,_),_) = get_calc 1;
1.158 + if "[x = 1]" = term2str (fst (get_obj g_result pt [])) then ()
1.159 + else raise error "inform.sml: diff.behav.appendFormula: on Frm + equ 3";
1.160 +
1.161 +
1.162 +"--------- appendFormula: on Res + NO deriv ----------------------";
1.163 +"--------- appendFormula: on Res + NO deriv ----------------------";
1.164 +"--------- appendFormula: on Res + NO deriv ----------------------";
1.165 + states:=[];
1.166 + CalcTree [(["equality (x+1=2)", "solveFor x","solutions L"],
1.167 + ("Test.thy",
1.168 + ["sqroot-test","univariate","equation","test"],
1.169 + ["Test","squ-equ-test-subpbl1"]))];
1.170 + Iterator 1; moveActiveRoot 1;
1.171 + autoCalculate 1 CompleteCalcHead;
1.172 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
1.173 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);
1.174 +
1.175 + appendFormula 1 "x = 2";
1.176 + val ((pt,p),_) = get_calc 1;
1.177 + val str = pr_ptree pr_short pt;
1.178 + writeln str;
1.179 + if str = ". ----- pblobj -----\n1. x + 1 = 2\n" andalso p = ([1], Res)
1.180 + then ()
1.181 + else raise error "inform.sml: diff.behav.appendFormula: Res + NOder 1";
1.182 +
1.183 + fetchProposedTactic 1;
1.184 + val (_,(tac,_,_)::_) = get_calc 1;
1.185 + if tac = Rewrite_Set "Test_simplify" then ()
1.186 + else raise error "inform.sml: diff.behav.appendFormula: Res + NOder 2";
1.187 + autoCalculate 1 CompleteCalc;
1.188 + val ((pt,_),_) = get_calc 1;
1.189 + if "[x = 1]" = term2str (fst (get_obj g_result pt [])) then ()
1.190 + else raise error "inform.sml: diff.behav.appendFormula: on Frm + equ 3";
1.191 +
1.192 +
1.193 +"--------- appendFormula: on Res + late deriv --------------------";
1.194 +"--------- appendFormula: on Res + late deriv --------------------";
1.195 +"--------- appendFormula: on Res + late deriv --------------------";
1.196 + states:=[];
1.197 + CalcTree [(["equality (x+1=2)", "solveFor x","solutions L"],
1.198 + ("Test.thy",
1.199 + ["sqroot-test","univariate","equation","test"],
1.200 + ["Test","squ-equ-test-subpbl1"]))];
1.201 + Iterator 1; moveActiveRoot 1;
1.202 + autoCalculate 1 CompleteCalcHead;
1.203 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
1.204 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);
1.205 +
1.206 + appendFormula 1 "x = 1";
1.207 + val ((pt,p),_) = get_calc 1;
1.208 + val str = pr_ptree pr_short pt;
1.209 + writeln str;
1.210 + if str = ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + -1 * 2 = 0\n3. ----- pblobj -----\n3.1. -1 + x = 0\n3.2. x = 0 + -1 * -1\n3.2.1. x = 0 + -1 * -1\n3.2.2. x = 0 + 1\n" andalso p = ([3,2], Res)
1.211 + then () (*finds 1 step too early: ([3,2], Res) "x = 1" also by script !!!*)
1.212 + else raise error "inform.sml: diff.behav.appendFormula: Res + late d 1";
1.213 +
1.214 + fetchProposedTactic 1;
1.215 + val (_,(tac,_,_)::_) = get_calc 1;
1.216 + if tac = Check_Postcond ["linear", "univariate", "equation", "test"] then ()
1.217 + else raise error "inform.sml: diff.behav.appendFormula: Res + late d 2";
1.218 + autoCalculate 1 CompleteCalc;
1.219 + val ((pt,_),_) = get_calc 1;
1.220 + if "[x = 1]" = term2str (fst (get_obj g_result pt [])) then ()
1.221 + else raise error "inform.sml: diff.behav.appendFormula: Res + late d 3";
1.222 +
1.223 +
1.224 +"--------- appendFormula: on Res + late deriv [x = 3 + -2]---///--";
1.225 +"--------- appendFormula: on Res + late deriv [x = 3 + -2]---///--";
1.226 +"--------- appendFormula: on Res + late deriv [x = 3 + -2]---///--";
1.227 + states:=[];
1.228 + CalcTree [(["equality (x+1=2)", "solveFor x","solutions L"],
1.229 + ("Test.thy",
1.230 + ["sqroot-test","univariate","equation","test"],
1.231 + ["Test","squ-equ-test-subpbl1"]))];
1.232 + Iterator 1; moveActiveRoot 1;
1.233 + autoCalculate 1 CompleteCalcHead;
1.234 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
1.235 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);
1.236 + appendFormula 1 "[x = 3 + -2*1]";
1.237 + val ((pt,p),_) = get_calc 1;
1.238 + val str = pr_ptree pr_short pt;
1.239 + writeln str;
1.240 + if str=". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + -1 * 2 = 0\n3. ----- pblobj -----\n3.1. -1 + x = 0\n3.2. x = 0 + -1 * -1\n4. [x = 1]\n4.1. [x = 1]\n4.2. [x = -2 + 3]\n4.3. [x = 3 + -2]\n" then ()
1.241 + else raise error "inform.sml: diff.behav.appendFormula: Res + latEE 1";
1.242 + autoCalculate 1 CompleteCalc;
1.243 + val ((pt,p),_) = get_calc 1;
1.244 + if "[x = 3 + -2 * 1]" = term2str (fst (get_obj g_result pt [])) then ()
1.245 + (* ~~~~~~~~~~ simplify as last step in any script ?!*)
1.246 + else raise error "inform.sml: diff.behav.appendFormula: Res + latEE 2";
1.247 +
1.248 +
1.249 +
1.250 +"--------- replaceFormula: on Res + = ----------------------------";
1.251 +"--------- replaceFormula: on Res + = ----------------------------";
1.252 +"--------- replaceFormula: on Res + = ----------------------------";
1.253 + states:=[];
1.254 + CalcTree [(["equality (x+1=2)", "solveFor x","solutions L"],
1.255 + ("Test.thy",
1.256 + ["sqroot-test","univariate","equation","test"],
1.257 + ["Test","squ-equ-test-subpbl1"]))];
1.258 + Iterator 1; moveActiveRoot 1;
1.259 + autoCalculate 1 CompleteCalcHead;
1.260 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
1.261 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);
1.262 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*-1 + x*);
1.263 +
1.264 + replaceFormula 1 "-2 * 1 + (1 + x) = 0"; refFormula 1 (get_pos 1 1);
1.265 + val ((pt,_),_) = get_calc 1;
1.266 + val str = pr_ptree pr_short pt;
1.267 + writeln str;
1.268 + if str=". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + -1 * 2 = 0\n2.1. x + 1 + -1 * 2 = 0\n2.2. -1 * 2 + (x + 1) = 0\n2.3. -1 * 2 + (1 + x) = 0\n2.4. 1 + (-1 * 2 + x) = 0\n2.5. 1 + (-2 + x) = 0\n2.6. 1 + (-2 * 1 + x) = 0\n" then()
1.269 + else raise error "inform.sml: diff.behav.replaceFormula: on Res += 1";
1.270 + autoCalculate 1 CompleteCalc;
1.271 + val ((pt,pos as(p,_)),_) = get_calc 1;
1.272 + if pos=([],Res)andalso"[x = 1]"=(term2str o fst)(get_obj g_result pt p)then()
1.273 + else raise error "inform.sml: diff.behav.replaceFormula: on Res + = 2";
1.274 +
1.275 +
1.276 +"--------- replaceFormula: on Res + = 1st Nd ---------------------";
1.277 +"--------- replaceFormula: on Res + = 1st Nd ---------------------";
1.278 +"--------- replaceFormula: on Res + = 1st Nd ---------------------";
1.279 + states:=[];
1.280 + CalcTree [(["equality (x+1=2)", "solveFor x","solutions L"],
1.281 + ("Test.thy",
1.282 + ["sqroot-test","univariate","equation","test"],
1.283 + ["Test","squ-equ-test-subpbl1"]))];
1.284 + Iterator 1; moveActiveRoot 1;
1.285 + autoCalculate 1 CompleteCalcHead;
1.286 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
1.287 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);
1.288 +
1.289 + replaceFormula 1 "x + 1 = 4 + -2"; refFormula 1 (get_pos 1 1);
1.290 + val ((pt,_),_) = get_calc 1;
1.291 + val str = pr_ptree pr_short pt;
1.292 + writeln str;
1.293 + if str=". ----- pblobj -----\n1. x + 1 = 2\n1.1. x + 1 = 2\n1.2. 1 + x = 2\n1.3. 1 + x = -2 + 4\n1.4. x + 1 = -2 + 4\n" then ()
1.294 + else raise error "inform.sml: diff.behav.replaceFormula: on Res 1 + = 1";
1.295 + autoCalculate 1 CompleteCalc;
1.296 + val ((pt,pos as(p,_)),_) = get_calc 1;
1.297 + if pos=([],Res)andalso"[x = 1]"=(term2str o fst)(get_obj g_result pt p)then()
1.298 + else raise error "inform.sml: diff.behav.replaceFormula: on Res + = 2";
1.299 +
1.300 +
1.301 +"--------- replaceFormula: on Frm + = 1st Nd ---------------------";
1.302 +"--------- replaceFormula: on Frm + = 1st Nd ---------------------";
1.303 +"--------- replaceFormula: on Frm + = 1st Nd ---------------------";
1.304 + states:=[];
1.305 + CalcTree [(["equality (x+1=2)", "solveFor x","solutions L"],
1.306 + ("Test.thy",
1.307 + ["sqroot-test","univariate","equation","test"],
1.308 + ["Test","squ-equ-test-subpbl1"]))];
1.309 + Iterator 1; moveActiveRoot 1;
1.310 + autoCalculate 1 CompleteCalcHead;
1.311 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
1.312 +
1.313 + replaceFormula 1 "x + 1 = 4 + -2"; refFormula 1 (get_pos 1 1);
1.314 + val ((pt,_),_) = get_calc 1;
1.315 + val str = pr_ptree pr_short pt;
1.316 + writeln str;
1.317 + if str=". ----- pblobj -----\n1. x + 1 = 2\n1.1. x + 1 = 2\n1.2. 1 + x = 2\n1.3. 1 + x = -2 + 4\n1.4. x + 1 = -2 + 4\n" then ()
1.318 + else raise error "inform.sml: diff.behav.replaceFormula: on Frm 1 + = 1";
1.319 + autoCalculate 1 CompleteCalc;
1.320 + val ((pt,pos as(p,_)),_) = get_calc 1;
1.321 + if pos=([],Res)andalso"[x = 1]"=(term2str o fst)(get_obj g_result pt p)then()
1.322 + else raise error "inform.sml: diff.behav.replaceFormula: on Frm 1 + = 2";
1.323 +
1.324 +
1.325 +"--------- replaceFormula: cut calculation -----------------------";
1.326 +"--------- replaceFormula: cut calculation -----------------------";
1.327 +"--------- replaceFormula: cut calculation -----------------------";
1.328 + states:=[];
1.329 + CalcTree [(["equality (x+1=2)", "solveFor x","solutions L"],
1.330 + ("Test.thy",
1.331 + ["sqroot-test","univariate","equation","test"],
1.332 + ["Test","squ-equ-test-subpbl1"]))];
1.333 + Iterator 1; moveActiveRoot 1;
1.334 + autoCalculate 1 CompleteCalc;
1.335 + moveActiveRoot 1; moveActiveDown 1;
1.336 + if get_pos 1 1 = ([1], Frm) then ()
1.337 + else raise error "inform.sml: diff.behav. cut calculation 1";
1.338 +
1.339 + replaceFormula 1 "x + 1 = 4 + -2"; refFormula 1 (get_pos 1 1);
1.340 + val ((pt,p),_) = get_calc 1;
1.341 + val str = pr_ptree pr_short pt;
1.342 + writeln str;
1.343 + if p = ([1], Res) then ()
1.344 + else raise error "inform.sml: diff.behav. cut calculation 2";
1.345 +
1.346 +
1.347 +
1.348 +(* 040307 copied from informtest.sml; ... old version
1.349 + "---------------- maximum-example, UC: Modeling / modifyCalcHead -";
1.350 + "---------------- maximum-example, UC: Modeling / modifyCalcHead -";
1.351 + "---------------- maximum-example, UC: Modeling / modifyCalcHead -";
1.352 +
1.353 + val p = ([],Pbl);
1.354 + val elems = ["fixedValues [r=Arbfix]","maximum A","valuesFor [a,b]",
1.355 + "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
1.356 + "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
1.357 + "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]",
1.358 + (*^^^ these are the elements for the root-problem (in variants)*)
1.359 + (*vvv these are elements required for subproblems*)
1.360 + "boundVariable a","boundVariable b","boundVariable alpha",
1.361 + "interval {x::real. 0 <= x & x <= 2*r}",
1.362 + "interval {x::real. 0 <= x & x <= 2*r}",
1.363 + "interval {x::real. 0 <= x & x <= pi}",
1.364 + "errorBound (eps=(0::real))"]
1.365 + (*specifying is not interesting for this example*)
1.366 + val spec = ("DiffApp.thy", ["maximum_of","function"],
1.367 + ["DiffApp","max_by_calculus"]);
1.368 + (*the empty model with descriptions for user-guidance by Model_Problem*)
1.369 + val empty_model = [Given ["fixedValues []"],
1.370 + Find ["maximum", "valuesFor"],
1.371 + Relate ["relations []"]];
1.372 +
1.373 +
1.374 + (*!!!!!!!!!!!!!!!!! DON'T USE me FOR FINDING nxt !!!!!!!!!!!!!!!!!!*)
1.375 + val (p,_,f,nxt,_,pt) = CalcTreeTEST [(elems, spec)];
1.376 + (*val nxt = ("Model_Problem", ...*)
1.377 + val pbl = get_obj g_pbl pt (fst p); (writeln o (itms2str_ ctxt)) pbl;
1.378 +
1.379 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.380 + (*nxt = Add_Given "fixedValues [r = Arbfix]"*)
1.381 + val pbl = get_obj g_pbl pt (fst p); (writeln o (itms2str_ ctxt)) pbl;
1.382 +(*[
1.383 +(0 ,[] ,false ,#Given ,Inc fixedValues [] ,(??.empty, [])),
1.384 +(0 ,[] ,false ,#Find ,Inc maximum ,(??.empty, [])),
1.385 +(0 ,[] ,false ,#Find ,Inc valuesFor ,(??.empty, [])),
1.386 +(0 ,[] ,false ,#Relate ,Inc relations [] ,(??.empty, []))]*)
1.387 +
1.388 + (*the empty CalcHead is checked w.r.t the model and re-established as such*)
1.389 + val (b,pt,ocalhd) = input_icalhd pt (p,"", empty_model, Pbl, e_spec);
1.390 + val pbl = get_obj g_pbl pt (fst p); (writeln o (itms2str_ ctxt)) pbl;
1.391 + if ocalhd2str ocalhd = "(Pbl, ??.empty, [\n(0 ,[] ,false ,#Given ,Inc fixedValues [] ,(??.empty, [])),\n(0 ,[] ,false ,#Find ,Inc maximum ,(??.empty, [])),\n(0 ,[] ,false ,#Find ,Inc valuesFor ,(??.empty, [])),\n(0 ,[] ,false ,#Relate ,Inc relations [] ,(??.empty, []))], [], \n(\"e_domID\", [\"e_pblID\"], [\"e_metID\"]) )" then () else raise error "informtest.sml: diff.behav. max 1";
1.392 +
1.393 + (*there is one input to the model (could be more)*)
1.394 + val (b,pt,ocalhd) =
1.395 + input_icalhd pt (p,"", [Given ["fixedValues [r=Arbfix]"],
1.396 + Find ["maximum", "valuesFor"],
1.397 + Relate ["relations"]], Pbl, e_spec);
1.398 + val pbl = get_obj g_pbl pt (fst p); (writeln o (itms2str_ ctxt)) pbl;
1.399 + if ocalhd2str ocalhd = "(Pbl, ??.empty, [\n(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),\n(0 ,[] ,false ,#Find ,Inc maximum ,(??.empty, [])),\n(0 ,[] ,false ,#Find ,Inc valuesFor ,(??.empty, [])),\n(0 ,[] ,false ,#Relate ,Inc relations [] ,(??.empty, []))], [], \n(\"e_domID\", [\"e_pblID\"], [\"e_metID\"]) )" then ()
1.400 + else raise error "informtest.sml: diff.behav. max 2";
1.401 +
1.402 + (*this input is complete in variant 3, but the ME doesn't recognize FIXXXXME
1.403 + val (b,pt''''',ocalhd) =
1.404 + input_icalhd pt (p,"", [Given ["fixedValues [r=Arbfix]"],
1.405 + Find ["maximum A", "valuesFor [a,b]"],
1.406 + Relate ["relations [A=a*b, a/2=r*sin alpha, \
1.407 + \b/2=r*cos alpha]"]], Pbl, e_spec);
1.408 + val pbl = get_obj g_pbl pt''''' (fst p); (writeln o (itms2str_ ctxt)) pbl;
1.409 + if ocalhd2str ocalhd = ------------^^^^^^^^^^ missing !!!*)
1.410 +
1.411 + (*this input is complete in variant 1 (variant 3 does not work yet)*)
1.412 + val (b,pt''''',ocalhd) =
1.413 + input_icalhd pt (p,"", [Given ["fixedValues [r=Arbfix]"],
1.414 + Find ["maximum A", "valuesFor [a,b]"],
1.415 + Relate ["relations [A=a*b, \
1.416 + \(a/2)^^^2 + (b/2)^^^2 = r^^^2]"]],
1.417 + Pbl, e_spec);
1.418 + val pbl = get_obj g_pbl pt''''' (fst p); (writeln o (itms2str_ ctxt)) pbl;
1.419 +
1.420 + modifycalcheadOK2xml 111 (bool2str b) ocalhd;
1.421 +*)
1.422 +
1.423 +"--------- syntax error ------------------------------------------";
1.424 +"--------- syntax error ------------------------------------------";
1.425 +"--------- syntax error ------------------------------------------";
1.426 + states:=[];
1.427 + CalcTree [(["equality (x+1=2)", "solveFor x","solutions L"],
1.428 + ("Test.thy",
1.429 + ["sqroot-test","univariate","equation","test"],
1.430 + ["Test","squ-equ-test-subpbl1"]))];
1.431 + Iterator 1; moveActiveRoot 1;
1.432 + autoCalculate 1 CompleteCalcHead;
1.433 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
1.434 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);
1.435 +
1.436 + appendFormula 1 " x - "; (*<ERROR> syntax error in ' x - ' </ERROR>*)
1.437 + val ((pt,_),_) = get_calc 1;
1.438 + val str = pr_ptree pr_short pt;
1.439 + writeln str;
1.440 + if str = ". ----- pblobj -----\n1. x + 1 = 2\n" then ()
1.441 + else raise error "inform.sml: diff.behav.appendFormula: syntax error";
1.442 +
1.443 +
1.444 +"--------- CAS-command on ([],Pbl) -------------------------------";
1.445 +"--------- CAS-command on ([],Pbl) -------------------------------";
1.446 +"--------- CAS-command on ([],Pbl) -------------------------------";
1.447 +val (p,_,f,nxt,_,pt) =
1.448 + CalcTreeTEST [([], ("e_domID", ["e_pblID"], ["e_metID"]))];
1.449 +val ifo = "solve(x+1=2,x)";
1.450 +val (_,(_,c,(pt,p))) = inform ([],[],(pt,p)) "solve(x+1=2,x)";
1.451 +show_pt pt;
1.452 +val nxt = ("Apply_Method",Apply_Method ["Test","squ-equ-test-subpbl1"]);
1.453 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.454 +if p = ([1], Frm) andalso f2str f = "x + 1 = 2" then ()
1.455 +else raise error "inform.sml: diff.behav. CAScmd ([],Pbl)";
1.456 +
1.457 +
1.458 +"--------- CAS-command on ([],Pbl) FE-interface ------------------";
1.459 +"--------- CAS-command on ([],Pbl) FE-interface ------------------";
1.460 +"--------- CAS-command on ([],Pbl) FE-interface ------------------";
1.461 +states:=[];
1.462 +CalcTree [([], ("e_domID", ["e_pblID"], ["e_metID"]))];
1.463 +Iterator 1;
1.464 +moveActiveRoot 1;
1.465 +replaceFormula 1 "solve(x+1=2,x)";
1.466 +autoCalculate 1 CompleteCalc;
1.467 +val ((pt,p),_) = get_calc 1;
1.468 +show_pt pt;
1.469 +if p = ([], Res) then ()
1.470 +else raise error "inform.sml: diff.behav. CAScmd ([],Pbl) FE-interface";
1.471 +
1.472 +
1.473 +"--------- inform [rational,simplification] ----------------------";
1.474 +"--------- inform [rational,simplification] ----------------------";
1.475 +"--------- inform [rational,simplification] ----------------------";
1.476 +states:=[];
1.477 +CalcTree [(["term (4/x - 3/y - 1)", "normalform N"],
1.478 + ("Rational.thy",["rational","simplification"],
1.479 + ["simplification","of_rationals"]))];
1.480 +Iterator 1; moveActiveRoot 1;
1.481 +autoCalculate 1 CompleteCalcHead;
1.482 +autoCalculate 1 (Step 1);
1.483 +autoCalculate 1 (Step 1);
1.484 +autoCalculate 1 (Step 1);
1.485 +autoCalculate 1 (Step 1);
1.486 +"--- input the next formula that _should_ be presented by mat-engine";
1.487 +appendFormula 1 "(4 * y + -3 * x) / (x * y) + -1";
1.488 +val ((pt,p),_) = get_calc 1;
1.489 +if p = ([4], Res) andalso (length o children o (get_nd pt)) (fst p) = 2 then ()
1.490 +else raise error ("inform.sml: [rational,simplification] 1");
1.491 +
1.492 +"--- input the next formula that would be presented by mat-engine";
1.493 +(*autoCalculate 1 (Step 1);*)
1.494 +appendFormula 1 "(4 * y + -3 * x + -1 * (x * y)) / (x * y)";
1.495 +val ((pt,p),_) = get_calc 1;
1.496 +if p = ([5], Res) andalso (length o children o (get_nd pt)) (fst p) = 0 then ()
1.497 +else raise error ("inform.sml: [rational,simplification] 2");
1.498 +
1.499 +"--- input the exact final result";(*TODO: Exception- LIST "last_elem" raised*)
1.500 +appendFormula 1 "(-3 * x + 4 * y + -1 * x * y) / (x * y)";
1.501 +val ((pt,p),_) = get_calc 1;
1.502 +if p = ([6], Res) andalso (length o children o (get_nd pt)) (fst p) = 2 then ()
1.503 +else raise error ("inform.sml: [rational,simplification] 3");
1.504 +show_pt pt;
1.505 +
1.506 +"--------- Take as 1st tac, start with <NEW> (CAS input) ---------";
1.507 +"--------- Take as 1st tac, start with <NEW> (CAS input) ---------";
1.508 +"--------- Take as 1st tac, start with <NEW> (CAS input) ---------";
1.509 +val t = str2term "Diff (x^^^2 + x + 1, x)";
1.510 +case t of Const ("Diff.Diff", _) $ _ => ()
1.511 + | _ => raise
1.512 + error "diff.sml behav.changed for CAS Diff (..., x)";
1.513 +atomty t;
1.514 +"-----------------------------------------------------------------";
1.515 +(*1>*)states:=[];
1.516 +(*2>*)CalcTree [([], ("e_domID", ["e_pblID"], ["e_metID"]))];
1.517 +(*3>*)Iterator 1;moveActiveRoot 1;
1.518 +"----- here the Headline has been finished";
1.519 +(*4>*)moveActiveFormula 1 ([],Pbl);
1.520 +(*5>*)replaceFormula 1 "Diff (x^2 + x + 1, x)";
1.521 +val ((pt,_),_) = get_calc 1;
1.522 +val PblObj {probl, meth, spec, fmz, env, loc, ...} = get_obj I pt [];
1.523 +val NONE = env;
1.524 +val (SOME istate, NONE) = loc;
1.525 +print_depth 5;
1.526 +writeln"-----------------------------------------------------------";
1.527 +spec;
1.528 +writeln (itms2str_ ctxt probl);
1.529 +writeln (itms2str_ ctxt meth);
1.530 +writeln (istate2str istate);
1.531 +
1.532 +print_depth 3;
1.533 +
1.534 +refFormula 1 ([],Pbl) (*--> correct CalcHead*);
1.535 + (*081016 NOT necessary (but leave it in Java):*)
1.536 +(*6>*)(*completeCalcHead*)autoCalculate 1 CompleteCalcHead;
1.537 +"----- here the CalcHead has been completed --- ONCE MORE ?????";
1.538 +
1.539 +(***difference II***)
1.540 +val ((pt,p),_) = get_calc 1;
1.541 +(*val p = ([], Pbl)*)
1.542 +val PblObj {probl, meth, spec, fmz, env, loc, ...} = get_obj I pt [];
1.543 +val NONE = env;
1.544 +val (SOME istate, NONE) = loc;
1.545 +print_depth 5; writeln (istate2str istate); print_depth 3;
1.546 +(*ScrState ([],
1.547 + [], NONE,
1.548 + ??.empty, Sundef, false)*)
1.549 +print_depth 5; spec; print_depth 3;
1.550 +(*("Isac.thy",
1.551 + ["derivative_of", "function"],
1.552 + ["diff", "differentiate_on_R"]) : spec*)
1.553 +writeln (itms2str_ ctxt probl);
1.554 +(*[
1.555 +(1 ,[1] ,true ,#Given ,Cor functionTerm (x ^^^ 2 + x + 1) ,(f_, [x ^^^ 2 + x + 1])),
1.556 +(2 ,[1] ,true ,#Given ,Cor differentiateFor x ,(v_, [x])),
1.557 +(3 ,[1] ,true ,#Find ,Cor derivative f_'_ ,(f_'_, [f_'_]))]*)
1.558 +writeln (itms2str_ ctxt meth);
1.559 +(*[
1.560 +(1 ,[1] ,true ,#Given ,Cor functionTerm (x ^^^ 2 + x + 1) ,(f_, [x ^^^ 2 + x + 1])),
1.561 +(2 ,[1] ,true ,#Given ,Cor differentiateFor x ,(v_, [x])),
1.562 +(3 ,[1] ,true ,#Find ,Cor derivative f_'_ ,(f_'_, [f_'_]))]*)
1.563 +writeln"-----------------------------------------------------------";
1.564 +(*7>*)fetchProposedTactic 1 (*--> Apply_Method*);
1.565 +(*WN081028 fixed <ERROR> helpless </ERROR> by inform returning ...(.,Met)*)
1.566 +autoCalculate 1 CompleteCalc;
1.567 +val ((pt,p),_) = get_calc 1;
1.568 +val Form res = (#1 o pt_extract) (pt, ([],Res));
1.569 +show_pt pt;
1.570 +if p = ([], Res) andalso term2str res = "1 + 2 * x" then ()
1.571 +else raise error "diff.sml behav.changed for Diff (x^2 + x + 1, x)";
1.572 +
1.573 +
1.574 +"--------- Take as 1st tac, start from exp -----------------------";
1.575 +"--------- Take as 1st tac, start from exp -----------------------";
1.576 +"--------- Take as 1st tac, start from exp -----------------------";
1.577 +(*the following input is copied from BridgeLog Java <==> SML,
1.578 + omitting unnecessary inputs*)
1.579 +(*1>*)states:=[];
1.580 +(*2>*)CalcTree [(["functionTerm (x^2 + x + 1)", "differentiateFor x", "derivative f_'_"],("Isac.thy",["derivative_of","function"],["diff","differentiate_on_R"]))];
1.581 +(*3>*)Iterator 1; moveActiveRoot 1;
1.582 +
1.583 +(*6>*)(*completeCalcHead*)autoCalculate 1 CompleteCalcHead;
1.584 +
1.585 +(***difference II***)
1.586 +val ((pt,_),_) = get_calc 1;
1.587 +val PblObj {probl, meth, spec, fmz, env, loc, ...} = get_obj I pt [];
1.588 +val NONE = env;
1.589 +val (SOME istate, NONE) = loc;
1.590 +print_depth 5; writeln (istate2str istate); print_depth 3;
1.591 +(*ScrState ([],
1.592 + [], NONE,
1.593 + ??.empty, Sundef, false)*)
1.594 +print_depth 5; spec; print_depth 3;
1.595 +(*("Isac.thy",
1.596 + ["derivative_of", "function"],
1.597 + ["diff", "differentiate_on_R"]) : spec*)
1.598 +writeln (itms2str_ ctxt probl);
1.599 +(*[
1.600 +(1 ,[1] ,true ,#Given ,Cor functionTerm (x ^^^ 2 + x + 1) ,(f_, [x ^^^ 2 + x + 1])),
1.601 +(2 ,[1] ,true ,#Given ,Cor differentiateFor x ,(v_, [x])),
1.602 +(3 ,[1] ,true ,#Find ,Cor derivative f_'_ ,(f_'_, [f_'_]))]*)
1.603 +writeln (itms2str_ ctxt meth);
1.604 +(*[
1.605 +(1 ,[1] ,true ,#Given ,Cor functionTerm (x ^^^ 2 + x + 1) ,(f_, [x ^^^ 2 + x + 1])),
1.606 +(2 ,[1] ,true ,#Given ,Cor differentiateFor x ,(v_, [x])),
1.607 +(3 ,[1] ,true ,#Find ,Cor derivative f_'_ ,(f_'_, [f_'_]))]*)
1.608 +writeln"-----------------------------------------------------------";
1.609 +(*7>*)fetchProposedTactic 1 (*--> Apply_Method*);
1.610 +
1.611 +autoCalculate 1 (Step 1);
1.612 +val ((pt,p),_) = get_calc 1;
1.613 +val Form res = (#1 o pt_extract) (pt, p);
1.614 +if term2str res = "d_d x (x ^^^ 2 + x + 1)" then ()
1.615 +else raise error "diff.sml Diff (x^2 + x + 1, x) from exp";
1.616 +
1.617 +
1.618 +"--------- init_form, start with <NEW> (CAS input) ---------------";
1.619 +"--------- init_form, start with <NEW> (CAS input) ---------------";
1.620 +"--------- init_form, start with <NEW> (CAS input) ---------------";
1.621 +states:=[];
1.622 +CalcTree [([], ("e_domID", ["e_pblID"], ["e_metID"]))];
1.623 +(*[[from sml: > @@@@@begin@@@@@
1.624 +[[from sml: 1
1.625 +[[from sml: <CALCTREE>
1.626 +[[from sml: <CALCID> 1 </CALCID>
1.627 +[[from sml: </CALCTREE>
1.628 +[[from sml: @@@@@end@@@@@*)
1.629 +Iterator 1;
1.630 +(*[[from sml: > @@@@@begin@@@@@
1.631 +[[from sml: 1
1.632 +[[from sml: <ADDUSER>
1.633 +[[from sml: <CALCID> 1 </CALCID>
1.634 +[[from sml: <USERID> 1 </USERID>
1.635 +[[from sml: </ADDUSER>
1.636 +[[from sml: @@@@@end@@@@@*)
1.637 +moveActiveRoot 1;
1.638 +(*[[from sml: > @@@@@begin@@@@@
1.639 +[[from sml: 1
1.640 +[[from sml: <CALCITERATOR>
1.641 +[[from sml: <CALCID> 1 </CALCID>
1.642 +[[from sml: <POSITION>
1.643 +[[from sml: <INTLIST>
1.644 +[[from sml: </INTLIST>
1.645 +[[from sml: <POS> Pbl </POS>
1.646 +[[from sml: </POSITION>
1.647 +[[from sml: </CALCITERATOR>
1.648 +[[from sml: @@@@@end@@@@@*)
1.649 +getFormulaeFromTo 1 ([],Pbl) ([],Pbl) 0 false;
1.650 +(*[[from sml: > @@@@@begin@@@@@ STILL CORRECT
1.651 +[[from sml: 1
1.652 +[[from sml: <GETELEMENTSFROMTO>
1.653 +[[from sml: <CALCID> 1 </CALCID>
1.654 +[[from sml: <FORMHEADS>
1.655 +[[from sml: <CALCFORMULA>
1.656 +[[from sml: <POSITION>
1.657 +[[from sml: <INTLIST>
1.658 +[[from sml: </INTLIST>
1.659 +[[from sml: <POS> Pbl </POS>
1.660 +[[from sml: </POSITION>
1.661 +[[from sml: <FORMULA>
1.662 +[[from sml: <MATHML>
1.663 +[[from sml: <ISA> ________________________________________________ </ISA>
1.664 +[[from sml: </MATHML>
1.665 +[[from sml:
1.666 +[[from sml: </FORMULA>
1.667 +[[from sml: </CALCFORMULA>
1.668 +[[from sml: </FORMHEADS>
1.669 +[[from sml: </GETELEMENTSFROMTO>
1.670 +[[from sml: @@@@@end@@@@@*)
1.671 +refFormula 1 ([],Pbl);
1.672 +(*[[from sml: > @@@@@begin@@@@@ STILL CORRECT
1.673 +[[from sml: 1
1.674 +[[from sml: <REFFORMULA>
1.675 +[[from sml: <CALCID> 1 </CALCID>
1.676 +[[from sml: <CALCHEAD status = "incorrect">
1.677 +[[from sml: <POSITION>
1.678 +[[from sml: <INTLIST>
1.679 +[[from sml: </INTLIST>
1.680 +[[from sml: <POS> Pbl </POS>
1.681 +[[from sml: </POSITION>
1.682 +[[from sml: <HEAD>
1.683 +[[from sml: <MATHML>
1.684 +[[from sml: <ISA> Problem (e_domID, [e_pblID]) </ISA>
1.685 +[[from sml: </MATHML>
1.686 +[[from sml: </HEAD>
1.687 +[[from sml: <MODEL>
1.688 +[[from sml: <GIVEN> </GIVEN>
1.689 +[[from sml: <WHERE> </WHERE>
1.690 +[[from sml: <FIND> </FIND>
1.691 +[[from sml: <RELATE> </RELATE>
1.692 +[[from sml: </MODEL>
1.693 +[[from sml: <BELONGSTO> Pbl </BELONGSTO>
1.694 +[[from sml: <SPECIFICATION>
1.695 +[[from sml: <THEORYID> e_domID </THEORYID>
1.696 +[[from sml: <PROBLEMID>
1.697 +[[from sml: <STRINGLIST>
1.698 +[[from sml: <STRING> e_pblID </STRING>
1.699 +[[from sml: </STRINGLIST>
1.700 +[[from sml: </PROBLEMID>
1.701 +[[from sml: <METHODID>
1.702 +[[from sml: <STRINGLIST>
1.703 +[[from sml: <STRING> e_metID </STRING>
1.704 +[[from sml: </STRINGLIST>
1.705 +[[from sml: </METHODID>
1.706 +[[from sml: </SPECIFICATION>
1.707 +[[from sml: </CALCHEAD>
1.708 +[[from sml: </REFFORMULA>
1.709 +[[from sml: @@@@@end@@@@@*)
1.710 +moveActiveFormula 1 ([],Pbl);
1.711 +(*[[from sml: > @@@@@begin@@@@@
1.712 +[[from sml: 1
1.713 +[[from sml: <CALCITERATOR>
1.714 +[[from sml: <CALCID> 1 </CALCID>
1.715 +[[from sml: <POSITION>
1.716 +[[from sml: <INTLIST>
1.717 +[[from sml: </INTLIST>
1.718 +[[from sml: <POS> Pbl </POS>
1.719 +[[from sml: </POSITION>
1.720 +[[from sml: </CALCITERATOR>
1.721 +[[from sml: @@@@@end@@@@@*)
1.722 +replaceFormula 1 "Simplify (1+2)";
1.723 +(*[[from sml: > @@@@@begin@@@@@
1.724 +[[from sml: 1
1.725 +[[from sml: <REPLACEFORMULA>
1.726 +[[from sml: <CALCID> 1 </CALCID>
1.727 +[[from sml: <CALCCHANGED>
1.728 +[[from sml: <UNCHANGED>
1.729 +[[from sml: <INTLIST>
1.730 +[[from sml: </INTLIST>
1.731 +[[from sml: <POS> Pbl </POS>
1.732 +[[from sml: </UNCHANGED>
1.733 +[[from sml: <DELETED>
1.734 +[[from sml: <INTLIST>
1.735 +[[from sml: </INTLIST>
1.736 +[[from sml: <POS> Pbl </POS>
1.737 +[[from sml: </DELETED>
1.738 +[[from sml: <GENERATED>
1.739 +[[from sml: <INTLIST>
1.740 +[[from sml: </INTLIST>
1.741 +[[from sml: <POS> Met </POS> DIFFERENCE: Pbl
1.742 +[[from sml: </GENERATED>
1.743 +[[from sml: </CALCCHANGED>
1.744 +[[from sml: </REPLACEFORMULA>
1.745 +[[from sml: @@@@@end@@@@@*)
1.746 +getFormulaeFromTo 1 ([],Pbl) ([],Pbl) 0 false(* DIFFERENCE: Pbl*);
1.747 +(*@@@@@begin@@@@@
1.748 + 1
1.749 +<GETELEMENTSFROMTO>
1.750 + <CALCID> 1 </CALCID>
1.751 + <FORMHEADS>
1.752 + <CALCFORMULA>
1.753 + <POSITION>
1.754 + <INTLIST>
1.755 + </INTLIST>
1.756 + <POS> Pbl </POS>
1.757 + </POSITION>
1.758 + <FORMULA>
1.759 + <MATHML>
1.760 + <ISA> Simplify (1 + 2) </ISA> WORKS !!!!!
1.761 + </MATHML>
1.762 + </FORMULA>
1.763 + </CALCFORMULA>
1.764 + </FORMHEADS>
1.765 +</GETELEMENTSFROMTO>
1.766 +@@@@@end@@@@@*)
1.767 +getFormulaeFromTo 1 ([],Pbl) ([],Met) 0 false;
1.768 +(*[[from sml: > @@@@@begin@@@@@
1.769 +[[from sml: 1
1.770 +[[from sml: <SYSERROR>
1.771 +[[from sml: <CALCID> 1 </CALCID>
1.772 +[[from sml: <ERROR> error in getFormulaeFromTo </ERROR>
1.773 +[[from sml: </SYSERROR>
1.774 +[[from sml: @@@@@end@@@@@*)
1.775 +(*step into getFormulaeFromTo --- bug corrected...*)