1.1 --- a/test/Tools/isac/Interpret/inform.sml Wed Oct 05 10:51:25 2016 +0200
1.2 +++ b/test/Tools/isac/Interpret/inform.sml Wed Oct 05 13:09:54 2016 +0200
1.3 @@ -56,9 +56,9 @@
1.4 ("Test", ["sqroot-test","univariate","equation","test"],
1.5 ["Test","squ-equ-test-subpbl1"]))];
1.6 Iterator 1; moveActiveRoot 1;
1.7 - autoCalculate' 1 CompleteCalcHead;
1.8 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
1.9 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);
1.10 + autoCalculate 1 CompleteCalcHead;
1.11 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
1.12 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);
1.13
1.14 appendFormula 1 "-2 * 1 + (1 + x) = 0" (*|> Future.join*); refFormula 1 (get_pos 1 1);
1.15 val ((pt,_),_) = get_calc 1;
1.16 @@ -98,11 +98,11 @@
1.17 else error "inform.sml: diff.behav.appendFormula: on Res + equ 3";
1.18 ============ inhibit exn WN1130701 broken at Isabelle2002 --> 2009-2 ============*)
1.19
1.20 - autoCalculate' 1 CompleteCalc;
1.21 + autoCalculate 1 CompleteCalc;
1.22 val ((pt,_),_) = get_calc 1;
1.23 if "[x = 1]" = term2str (fst (get_obj g_result pt [])) then ()
1.24 else error "inform.sml: diff.behav.appendFormula: on Res + equ 4";
1.25 - (* autoCalculate' 1 CompleteCalc;
1.26 + (* autoCalculate 1 CompleteCalc;
1.27 val ((pt,p),_) = get_calc 1;
1.28 (writeln o istates2str) (get_obj g_loc pt [ ]);
1.29 (writeln o istates2str) (get_obj g_loc pt [1]);
1.30 @@ -141,8 +141,8 @@
1.31 ("Test", ["sqroot-test","univariate","equation","test"],
1.32 ["Test","squ-equ-test-subpbl1"]))];
1.33 Iterator 1; moveActiveRoot 1;
1.34 - autoCalculate' 1 CompleteCalcHead;
1.35 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1) (*x + 1 = 2*);
1.36 + autoCalculate 1 CompleteCalcHead;
1.37 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1) (*x + 1 = 2*);
1.38 appendFormula 1 "2+ -1 + x = 2" (*|> Future.join*); refFormula 1 (get_pos 1 1);
1.39
1.40 moveDown 1 ([],Pbl); refFormula 1 ([1],Frm) (*x + 1 = 2*);
1.41 @@ -162,7 +162,7 @@
1.42 val (_,(tac,_,_)::_) = get_calc 1;
1.43 if tac = Rewrite_Set "norm_equation" then ()
1.44 else error "inform.sml: diff.behav.appendFormula: on Frm + equ 2";
1.45 - autoCalculate' 1 CompleteCalc;
1.46 + autoCalculate 1 CompleteCalc;
1.47 val ((pt,_),_) = get_calc 1;
1.48 if "[x = 1]" = term2str (fst (get_obj g_result pt [])) then ()
1.49 else error "inform.sml: diff.behav.appendFormula: on Frm + equ 3";
1.50 @@ -176,9 +176,9 @@
1.51 ("Test", ["sqroot-test","univariate","equation","test"],
1.52 ["Test","squ-equ-test-subpbl1"]))];
1.53 Iterator 1; moveActiveRoot 1;
1.54 - autoCalculate' 1 CompleteCalcHead;
1.55 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
1.56 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);
1.57 + autoCalculate 1 CompleteCalcHead;
1.58 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
1.59 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);
1.60
1.61 appendFormula 1 "x = 2" (*|> Future.join*);
1.62 val ((pt,p),_) = get_calc 1;
1.63 @@ -192,7 +192,7 @@
1.64 val (_,(tac,_,_)::_) = get_calc 1;
1.65 if tac = Rewrite_Set "Test_simplify" then ()
1.66 else error "inform.sml: diff.behav.appendFormula: Res + NOder 2";
1.67 - autoCalculate' 1 CompleteCalc;
1.68 + autoCalculate 1 CompleteCalc;
1.69 val ((pt,_),_) = get_calc 1;
1.70 if "[x = 1]" = term2str (fst (get_obj g_result pt [])) then ()
1.71 else error "inform.sml: diff.behav.appendFormula: on Frm + equ 3";
1.72 @@ -206,9 +206,9 @@
1.73 ("Test", ["sqroot-test","univariate","equation","test"],
1.74 ["Test","squ-equ-test-subpbl1"]))];
1.75 Iterator 1; moveActiveRoot 1;
1.76 - autoCalculate' 1 CompleteCalcHead;
1.77 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
1.78 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);
1.79 + autoCalculate 1 CompleteCalcHead;
1.80 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
1.81 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);
1.82
1.83 appendFormula 1 "x = 1" (*|> Future.join*);
1.84 val ((pt,p),_) = get_calc 1;
1.85 @@ -222,7 +222,7 @@
1.86 val (_,(tac,_,_)::_) = get_calc 1;
1.87 if tac = Check_Postcond ["LINEAR", "univariate", "equation", "test"] then ()
1.88 else error "inform.sml: diff.behav.appendFormula: Res + late d 2";
1.89 - autoCalculate' 1 CompleteCalc;
1.90 + autoCalculate 1 CompleteCalc;
1.91 val ((pt,_),_) = get_calc 1;
1.92 if "[x = 1]" = term2str (fst (get_obj g_result pt [])) then ()
1.93 else error "inform.sml: diff.behav.appendFormula: Res + late d 3";
1.94 @@ -236,16 +236,16 @@
1.95 ("Test", ["sqroot-test","univariate","equation","test"],
1.96 ["Test","squ-equ-test-subpbl1"]))];
1.97 Iterator 1; moveActiveRoot 1;
1.98 - autoCalculate' 1 CompleteCalcHead;
1.99 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
1.100 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);
1.101 + autoCalculate 1 CompleteCalcHead;
1.102 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
1.103 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);
1.104 appendFormula 1 "[x = 3 + -2*1]" (*|> Future.join*);
1.105 val ((pt,p),_) = get_calc 1;
1.106 val str = pr_ptree pr_short pt;
1.107 writeln str;
1.108 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.109 else error "inform.sml: diff.behav.appendFormula: Res + latEE 1";
1.110 - autoCalculate' 1 CompleteCalc;
1.111 + autoCalculate 1 CompleteCalc;
1.112 val ((pt,p),_) = get_calc 1;
1.113 if "[x = 3 + -2 * 1]" = term2str (fst (get_obj g_result pt [])) then ()
1.114 (* ~~~~~~~~~~ simplify as last step in any script ?!*)
1.115 @@ -261,10 +261,10 @@
1.116 ("Test", ["sqroot-test","univariate","equation","test"],
1.117 ["Test","squ-equ-test-subpbl1"]))];
1.118 Iterator 1; moveActiveRoot 1;
1.119 - autoCalculate' 1 CompleteCalcHead;
1.120 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
1.121 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);
1.122 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);(*-1 + x*);
1.123 + autoCalculate 1 CompleteCalcHead;
1.124 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
1.125 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);
1.126 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*-1 + x*);
1.127
1.128 replaceFormula 1 "-2 * 1 + (1 + x) = 0"; refFormula 1 (get_pos 1 1);
1.129 val ((pt,_),_) = get_calc 1;
1.130 @@ -293,7 +293,7 @@
1.131 "2.6. 1 + x + -2 * 1 = 0\n" then()
1.132 else error "inform.sml: diff.behav.replaceFormula: on Res += 1";
1.133
1.134 - autoCalculate' 1 CompleteCalc;
1.135 + autoCalculate 1 CompleteCalc;
1.136 val ((pt,pos as (p,_)),_) = get_calc 1;
1.137 if pos = ([],Res) andalso "[x = 1]" = (term2str o fst) (get_obj g_result pt p) then()
1.138 else error "inform.sml: diff.behav.replaceFormula: on Res + = 2";
1.139 @@ -306,9 +306,9 @@
1.140 ("Test", ["sqroot-test","univariate","equation","test"],
1.141 ["Test","squ-equ-test-subpbl1"]))];
1.142 Iterator 1; moveActiveRoot 1;
1.143 - autoCalculate' 1 CompleteCalcHead;
1.144 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
1.145 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);
1.146 + autoCalculate 1 CompleteCalcHead;
1.147 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
1.148 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);
1.149
1.150 replaceFormula 1 "x + 1 = 4 + -2"; refFormula 1 (get_pos 1 1);
1.151 val ((pt,_),_) = get_calc 1;
1.152 @@ -316,7 +316,7 @@
1.153 writeln str;
1.154 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.155 else error "inform.sml: diff.behav.replaceFormula: on Res 1 + = 1";
1.156 - autoCalculate' 1 CompleteCalc;
1.157 + autoCalculate 1 CompleteCalc;
1.158 val ((pt,pos as (p,_)),_) = get_calc 1;
1.159 if pos = ([],Res) andalso "[x = 1]" = (term2str o fst)(get_obj g_result pt p) then()
1.160 else error "inform.sml: diff.behav.replaceFormula: on Res + = 2";
1.161 @@ -330,8 +330,8 @@
1.162 ("Test", ["sqroot-test","univariate","equation","test"],
1.163 ["Test","squ-equ-test-subpbl1"]))];
1.164 Iterator 1; moveActiveRoot 1;
1.165 - autoCalculate' 1 CompleteCalcHead;
1.166 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
1.167 + autoCalculate 1 CompleteCalcHead;
1.168 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
1.169
1.170 replaceFormula 1 "x + 1 = 4 + -2"; refFormula 1 (get_pos 1 1);
1.171 val ((pt,_),_) = get_calc 1;
1.172 @@ -339,7 +339,7 @@
1.173 writeln str;
1.174 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.175 else error "inform.sml: diff.behav.replaceFormula: on Frm 1 + = 1";
1.176 - autoCalculate' 1 CompleteCalc;
1.177 + autoCalculate 1 CompleteCalc;
1.178 val ((pt,pos as (p,_)),_) = get_calc 1;
1.179 if pos = ([],Res) andalso "[x = 1]" = (term2str o fst)(get_obj g_result pt p) then()
1.180 else error "inform.sml: diff.behav.replaceFormula: on Frm 1 + = 2";
1.181 @@ -353,7 +353,7 @@
1.182 ("Test", ["sqroot-test","univariate","equation","test"],
1.183 ["Test","squ-equ-test-subpbl1"]))];
1.184 Iterator 1; moveActiveRoot 1;
1.185 - autoCalculate' 1 CompleteCalc;
1.186 + autoCalculate 1 CompleteCalc;
1.187 moveActiveRoot 1; moveActiveDown 1;
1.188 if get_pos 1 1 = ([1], Frm) then ()
1.189 else error "inform.sml: diff.behav. cut calculation 1";
1.190 @@ -449,9 +449,9 @@
1.191 ("Test", ["sqroot-test","univariate","equation","test"],
1.192 ["Test","squ-equ-test-subpbl1"]))];
1.193 Iterator 1; moveActiveRoot 1;
1.194 - autoCalculate' 1 CompleteCalcHead;
1.195 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
1.196 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);
1.197 + autoCalculate 1 CompleteCalcHead;
1.198 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
1.199 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);
1.200
1.201 appendFormula 1 " x - "; (*<ERROR> syntax error in ' x - ' </ERROR>*)
1.202 val ((pt,_),_) = get_calc 1;
1.203 @@ -483,7 +483,7 @@
1.204 Iterator 1;
1.205 moveActiveRoot 1;
1.206 replaceFormula 1 "solve(x+1=2,x)";
1.207 -autoCalculate' 1 CompleteCalc;
1.208 +autoCalculate 1 CompleteCalc;
1.209 val ((pt,p),_) = get_calc 1;
1.210 show_pt pt;
1.211 if p = ([], Res) then ()
1.212 @@ -497,11 +497,11 @@
1.213 CalcTree [(["Term (a * x / (b * x) + c * x / (d * x) + e / f)", "normalform N"],
1.214 ("Rational", ["rational", "simplification"], ["simplification", "of_rationals"]))];
1.215 Iterator 1; moveActiveRoot 1;
1.216 -autoCalculate' 1 CompleteCalcHead;
1.217 +autoCalculate 1 CompleteCalcHead;
1.218
1.219 "--- (-1) give a preview on the calculation without any input";
1.220 (*
1.221 -autoCalculate' 1 CompleteCalc;
1.222 +autoCalculate 1 CompleteCalc;
1.223 val ((pt, p), _) = get_calc 1;
1.224 show_pt pt;
1.225 [
1.226 @@ -515,8 +515,8 @@
1.227 EXAMPLE NOT OPTIMAL
1.228 *)
1.229 "--- (0) user input as the *first* step does not work, thus impdo at least 1 step";
1.230 -autoCalculate' 1 (Step 1);
1.231 -autoCalculate' 1 (Step 1);
1.232 +autoCalculate 1 (Step 1);
1.233 +autoCalculate 1 (Step 1);
1.234 val ((pt, p), _) = get_calc 1;
1.235 (*show_pt pt;
1.236 [
1.237 @@ -543,7 +543,7 @@
1.238
1.239 "--- (2) input the next formula that would be presented by mat-engine";
1.240 (* generate a preview:
1.241 -autoCalculate' 1 (Step 1);
1.242 +autoCalculate 1 (Step 1);
1.243 val ((pt, p), _) = get_calc 1;
1.244 show_pt pt;
1.245 [
1.246 @@ -594,7 +594,7 @@
1.247 else error ("inform.sml: [rational,simplification] 3");
1.248
1.249 "--- (4) finish the calculation + check the postcondition (in the future)";
1.250 -autoCalculate' 1 CompleteCalc;
1.251 +autoCalculate 1 CompleteCalc;
1.252 val ((pt, p), _) = get_calc 1;
1.253 val (t, asm) = get_obj g_result pt [];
1.254 if term2str t = "(a * d * f + b * c * f + b * d * e) / (b * d * f)" andalso
1.255 @@ -648,7 +648,7 @@
1.256
1.257 refFormula 1 ([],Pbl) (*--> correct CalcHead*);
1.258 (*081016 NOT necessary (but leave it in Java):*)
1.259 -(*6>*)(*completeCalcHead*)autoCalculate' 1 CompleteCalcHead;
1.260 +(*6>*)(*completeCalcHead*)autoCalculate 1 CompleteCalcHead;
1.261 "----- here the CalcHead has been completed --- ONCE MORE ?????";
1.262
1.263 (***difference II***)
1.264 @@ -678,7 +678,7 @@
1.265 writeln"-----------------------------------------------------------";
1.266 (*7>*)fetchProposedTactic 1 (*--> Apply_Method*);
1.267 (*WN081028 fixed <ERROR> helpless </ERROR> by inform returning ...(.,Met)*)
1.268 -autoCalculate' 1 CompleteCalc;
1.269 +autoCalculate 1 CompleteCalc;
1.270 val ((pt,p),_) = get_calc 1;
1.271 val Form res = (#1 o pt_extract) (pt, ([],Res));
1.272 show_pt pt;
1.273 @@ -694,7 +694,7 @@
1.274 (*2>*)CalcTree [(["functionTerm (x^2 + x + 1)", "differentiateFor x", "derivative f_'_f"],("Isac",["derivative_of","function"],["diff","differentiate_on_R"]))];
1.275 (*3>*)Iterator 1; moveActiveRoot 1;
1.276
1.277 -(*6>*)(*completeCalcHead*)autoCalculate' 1 CompleteCalcHead;
1.278 +(*6>*)(*completeCalcHead*)autoCalculate 1 CompleteCalcHead;
1.279 (***difference II***)
1.280 val ((pt,_),_) = get_calc 1;
1.281 val PblObj {probl, meth, spec, fmz, env, loc, ...} = get_obj I pt [];
1.282 @@ -720,7 +720,7 @@
1.283 (3 ,[1] ,true ,#Find ,Cor derivative f_'_f ,(f_'_f, [f_'_f]))]*)
1.284 writeln"-----------------------------------------------------------";
1.285 (*7>*)fetchProposedTactic 1 (*--> Apply_Method*);
1.286 -autoCalculate' 1 (Step 1);
1.287 +autoCalculate 1 (Step 1);
1.288 val ((pt,p),_) = get_calc 1;
1.289 val Form res = (#1 o pt_extract) (pt, p);
1.290 if term2str res = "d_d x (x ^^^ 2 + x + 1)" then ()
1.291 @@ -996,10 +996,10 @@
1.292 ("Isac", ["derivative_of","function"], ["diff","differentiate_on_R"]))];
1.293 Iterator 1;
1.294 moveActiveRoot 1;
1.295 -autoCalculate' 1 CompleteCalcHead;
1.296 -autoCalculate' 1 (Step 1);
1.297 -autoCalculate' 1 (Step 1);(*([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))*)
1.298 -(*autoCalculate' 1 (Step 1);([2], Res), d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4)*)
1.299 +autoCalculate 1 CompleteCalcHead;
1.300 +autoCalculate 1 (Step 1);
1.301 +autoCalculate 1 (Step 1);(*([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))*)
1.302 +(*autoCalculate 1 (Step 1);([2], Res), d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4)*)
1.303
1.304 "~~~~~ fun appendFormula, args:"; val (cI, (ifo:cterm')) = (1, "d_d x (x ^ 2) + cos (4 * x ^ 3)");
1.305 val cs = get_calc cI
1.306 @@ -1116,9 +1116,9 @@
1.307 ("Isac", ["derivative_of","function"], ["diff","differentiate_on_R"]))];
1.308 Iterator 1;
1.309 moveActiveRoot 1;
1.310 -autoCalculate' 1 CompleteCalcHead;
1.311 -autoCalculate' 1 (Step 1);
1.312 -autoCalculate' 1 (Step 1);(*([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))*)
1.313 +autoCalculate 1 CompleteCalcHead;
1.314 +autoCalculate 1 (Step 1);
1.315 +autoCalculate 1 (Step 1);(*([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))*)
1.316 appendFormula 1 "d_d x (x ^ 2) + cos (4 * x ^ 3)" (*|> Future.join*);
1.317 (*<CALCMESSAGE> error pattern #chain-rule-diff-both# </CALCMESSAGE>*)
1.318 (*or
1.319 @@ -1198,9 +1198,9 @@
1.320 ("Isac", ["derivative_of","function"], ["diff","differentiate_on_R"]))];
1.321 Iterator 1;
1.322 moveActiveRoot 1;
1.323 -autoCalculate' 1 CompleteCalcHead;
1.324 -autoCalculate' 1 (Step 1);
1.325 -autoCalculate' 1 (Step 1);(*([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))*)
1.326 +autoCalculate 1 CompleteCalcHead;
1.327 +autoCalculate 1 (Step 1);
1.328 +autoCalculate 1 (Step 1);(*([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))*)
1.329 appendFormula 1 "d_d x (x ^ 2) + cos (4 * x ^ 3)" (*|> Future.join*); (*<<<<<<<=========================*)
1.330 (* the check for errpat is maximally liberal (whole term modulo "nrls" from "type met"),
1.331 would recognize "cos (4 * x ^ (4 - 1)) + 2 * x" as well.