1.1 --- a/test/Tools/isac/Interpret/error-pattern.sml Fri Sep 09 10:53:51 2022 +0200
1.2 +++ b/test/Tools/isac/Interpret/error-pattern.sml Sun Sep 11 14:31:15 2022 +0200
1.3 @@ -52,17 +52,17 @@
1.4 val Prog sc = (#scr o MethodC.from_store) ["Test", "solve_linear"];
1.5 (writeln o UnparseC.term) sc;
1.6
1.7 - reset_states ();
1.8 + States.reset ();
1.9 CalcTree [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
1.10 ("Test", ["sqroot-test", "univariate", "equation", "test"],
1.11 ["Test", "squ-equ-test-subpbl1"]))];
1.12 Iterator 1; moveActiveRoot 1;
1.13 autoCalculate 1 CompleteCalcHead;
1.14 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
1.15 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 + - 1 * 2 = 0*);
1.16 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);(*x + 1 = 2*)
1.17 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);(*x + 1 + - 1 * 2 = 0*);
1.18
1.19 - appendFormula 1 "- 2 * 1 + (1 + x) = 0" (*|> Future.join*); refFormula 1 (get_pos 1 1);
1.20 - val ((pt,_),_) = get_calc 1;
1.21 + appendFormula 1 "- 2 * 1 + (1 + x) = 0" (*|> Future.join*); refFormula 1 (States.get_pos 1 1);
1.22 + val ((pt,_),_) = States.get_calc 1;
1.23 val str = pr_ctree pr_short pt;
1.24 if str =
1.25 (". ----- pblobj -----\n" ^
1.26 @@ -87,24 +87,24 @@
1.27 moveDown 1 ([2,3],Res); refFormula 1 ([2,4],Res);
1.28 moveDown 1 ([2,4],Res); refFormula 1 ([2,5],Res);
1.29 moveDown 1 ([2,5],Res); refFormula 1 ([2,6],Res);
1.30 - val ((pt,_),_) = get_calc 1;
1.31 + val ((pt,_),_) = States.get_calc 1;
1.32 if "- 2 * 1 + (1 + x) = 0" = UnparseC.term (fst (get_obj g_result pt [2,6])) then()
1.33 else error "inform.sml: diff.behav.appendFormula: on Res + equ 2";
1.34
1.35 fetchProposedTactic 1; (*takes Iterator 1 _1_*)
1.36 (* <ERROR> error in kernel </ERROR> ALREADY IN 2009-2*)
1.37 (*========== inhibit exn WN1130701 broken at Isabelle2002 --> 2009-2 =============
1.38 - val (_,(tac,_,_)::_) = get_calc 1;
1.39 + val (_,(tac,_,_)::_) = States.get_calc 1;
1.40 if tac = Rewrite_Set "Test_simplify" then ()
1.41 else error "inform.sml: diff.behav.appendFormula: on Res + equ 3";
1.42 ============ inhibit exn WN1130701 broken at Isabelle2002 --> 2009-2 ============*)
1.43
1.44 autoCalculate 1 CompleteCalc;
1.45 - val ((pt,_),_) = get_calc 1;
1.46 + val ((pt,_),_) = States.get_calc 1;
1.47 if "[x = 1]" = UnparseC.term (fst (get_obj g_result pt [])) then ()
1.48 else error "inform.sml: diff.behav.appendFormula: on Res + equ 4";
1.49 (* autoCalculate 1 CompleteCalc;
1.50 - val ((pt,p),_) = get_calc 1;
1.51 + val ((pt,p),_) = States.get_calc 1;
1.52 (writeln o istates2str) (get_obj g_loc pt [ ]);
1.53 (writeln o istates2str) (get_obj g_loc pt [1]);
1.54 (writeln o istates2str) (get_obj g_loc pt [2]);
1.55 @@ -137,14 +137,14 @@
1.56 "--------- appendFormula: on Frm + equ_nrls ----------------------";
1.57 "--------- appendFormula: on Frm + equ_nrls ----------------------";
1.58 "--------- appendFormula: on Frm + equ_nrls ----------------------";
1.59 - reset_states ();
1.60 + States.reset ();
1.61 CalcTree [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
1.62 ("Test", ["sqroot-test", "univariate", "equation", "test"],
1.63 ["Test", "squ-equ-test-subpbl1"]))];
1.64 Iterator 1; moveActiveRoot 1;
1.65 autoCalculate 1 CompleteCalcHead;
1.66 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1) (*x + 1 = 2*);
1.67 - appendFormula 1 "2+ - 1 + x = 2" (*|> Future.join*); refFormula 1 (get_pos 1 1);
1.68 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1) (*x + 1 = 2*);
1.69 + appendFormula 1 "2+ - 1 + x = 2" (*|> Future.join*); refFormula 1 (States.get_pos 1 1);
1.70
1.71 moveDown 1 ([],Pbl); refFormula 1 ([1],Frm) (*x + 1 = 2*);
1.72
1.73 @@ -155,16 +155,16 @@
1.74 moveDown 1 ([1,3],Res); refFormula 1 ([1,4],Res);
1.75 moveDown 1 ([1,4],Res); refFormula 1 ([1,5],Res);
1.76 moveDown 1 ([1,5],Res); refFormula 1 ([1,6],Res);
1.77 - val ((pt,_),_) = get_calc 1;
1.78 + val ((pt,_),_) = States.get_calc 1;
1.79 if "2 + - 1 + x = 2" = UnparseC.term (fst (get_obj g_result pt [1,6])) then()
1.80 else error "inform.sml: diff.behav.appendFormula: on Frm + equ 1";
1.81
1.82 fetchProposedTactic 1; (*takes Iterator 1 _1_*)
1.83 - val (_,(tac,_,_)::_) = get_calc 1;
1.84 + val (_,(tac,_,_)::_) = States.get_calc 1;
1.85 case tac of Rewrite_Set "norm_equation" => ()
1.86 | _ => error "inform.sml: diff.behav.appendFormula: on Frm + equ 2";
1.87 autoCalculate 1 CompleteCalc;
1.88 - val ((pt,_),_) = get_calc 1;
1.89 + val ((pt,_),_) = States.get_calc 1;
1.90 if "[x = 1]" = UnparseC.term (fst (get_obj g_result pt [])) then ()
1.91 else error "inform.sml: diff.behav.appendFormula: on Frm + equ 3";
1.92 DEconstrCalcTree 1;
1.93 @@ -172,17 +172,17 @@
1.94 "--------- appendFormula: on Res + NO deriv ----------------------";
1.95 "--------- appendFormula: on Res + NO deriv ----------------------";
1.96 "--------- appendFormula: on Res + NO deriv ----------------------";
1.97 - reset_states ();
1.98 + States.reset ();
1.99 CalcTree [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
1.100 ("Test", ["sqroot-test", "univariate", "equation", "test"],
1.101 ["Test", "squ-equ-test-subpbl1"]))];
1.102 Iterator 1; moveActiveRoot 1;
1.103 autoCalculate 1 CompleteCalcHead;
1.104 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
1.105 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 + - 1 * 2 = 0*);
1.106 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);(*x + 1 = 2*)
1.107 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);(*x + 1 + - 1 * 2 = 0*);
1.108
1.109 appendFormula 1 "x = 2" (*|> Future.join*);
1.110 - val ((pt,p),_) = get_calc 1;
1.111 + val ((pt,p),_) = States.get_calc 1;
1.112 val str = pr_ctree pr_short pt;
1.113 writeln str;
1.114 if str = ". ----- pblobj -----\n1. x + 1 = 2\n" andalso p = ([1], Res)
1.115 @@ -190,11 +190,11 @@
1.116 else error "inform.sml: diff.behav.appendFormula: Res + NOder 1";
1.117
1.118 fetchProposedTactic 1;
1.119 - val (_,(tac,_,_)::_) = get_calc 1;
1.120 + val (_,(tac,_,_)::_) = States.get_calc 1;
1.121 case tac of Rewrite_Set "Test_simplify" => ()
1.122 | _ => error "inform.sml: diff.behav.appendFormula: Res + NOder 2";
1.123 autoCalculate 1 CompleteCalc;
1.124 - val ((pt,_),_) = get_calc 1;
1.125 + val ((pt,_),_) = States.get_calc 1;
1.126 if "[x = 1]" = UnparseC.term (fst (get_obj g_result pt [])) then ()
1.127 else error "inform.sml: diff.behav.appendFormula: on Frm + equ 3";
1.128 DEconstrCalcTree 1;
1.129 @@ -205,17 +205,17 @@
1.130 (*cp with "fun me" to test/../lucas-interpreter.sml:
1.131 re-build: fun locate_input_term ---------------------------------------------------";
1.132 *)
1.133 - reset_states ();
1.134 + States.reset ();
1.135 CalcTree [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
1.136 ("Test", ["sqroot-test", "univariate", "equation", "test"],
1.137 ["Test", "squ-equ-test-subpbl1"]))];
1.138 Iterator 1; moveActiveRoot 1;
1.139 autoCalculate 1 CompleteCalcHead;
1.140 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
1.141 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 + - 1 * 2 = 0*);
1.142 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);(*x + 1 = 2*)
1.143 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);(*x + 1 + - 1 * 2 = 0*);
1.144
1.145 appendFormula 1 "x = 1" (*|> Future.join*);
1.146 - val ((pt,p),_) = get_calc 1;
1.147 + val ((pt,p),_) = States.get_calc 1;
1.148 val str = pr_ctree pr_short pt;
1.149 writeln str;
1.150 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.151 @@ -223,11 +223,11 @@
1.152 else error "inform.sml: diff.behav.appendFormula: Res + late d 1";
1.153
1.154 fetchProposedTactic 1;
1.155 - val (_,(tac,_,_)::_) = get_calc 1;
1.156 + val (_,(tac,_,_)::_) = States.get_calc 1;
1.157 case tac of Check_Postcond ["LINEAR", "univariate", "equation", "test"] => ()
1.158 | _ => error "inform.sml: diff.behav.appendFormula: Res + late d 2";
1.159 autoCalculate 1 CompleteCalc;
1.160 - val ((pt,_),_) = get_calc 1;
1.161 + val ((pt,_),_) = States.get_calc 1;
1.162 if "[x = 1]" = UnparseC.term (fst (get_obj g_result pt [])) then ()
1.163 else error "inform.sml: diff.behav.appendFormula: Res + late d 3";
1.164 DEconstrCalcTree 1;
1.165 @@ -235,22 +235,22 @@
1.166 "--------- appendFormula: on Res + late deriv [x = 3 + - 2]---///--";
1.167 "--------- appendFormula: on Res + late deriv [x = 3 + - 2]---///--";
1.168 "--------- appendFormula: on Res + late deriv [x = 3 + - 2]---///--";
1.169 - reset_states ();
1.170 + States.reset ();
1.171 CalcTree [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
1.172 ("Test", ["sqroot-test", "univariate", "equation", "test"],
1.173 ["Test", "squ-equ-test-subpbl1"]))];
1.174 Iterator 1; moveActiveRoot 1;
1.175 autoCalculate 1 CompleteCalcHead;
1.176 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
1.177 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 + - 1 * 2 = 0*);
1.178 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);(*x + 1 = 2*)
1.179 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);(*x + 1 + - 1 * 2 = 0*);
1.180 appendFormula 1 "[x = 3 + -2*1]" (*|> Future.join*);
1.181 - val ((pt,p),_) = get_calc 1;
1.182 + val ((pt,p),_) = States.get_calc 1;
1.183 val str = pr_ctree pr_short pt;
1.184 writeln str;
1.185 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.186 else error "inform.sml: diff.behav.appendFormula: Res + latEE 1";
1.187 autoCalculate 1 CompleteCalc;
1.188 - val ((pt,p),_) = get_calc 1;
1.189 + val ((pt,p),_) = States.get_calc 1;
1.190 if "[x = 3 + - 2 * 1]" = UnparseC.term (fst (get_obj g_result pt [])) then ()
1.191 (* ~~~~~~~~~~ simplify as last step in any script ?!*)
1.192 else error "inform.sml: diff.behav.appendFormula: Res + latEE 2";
1.193 @@ -259,18 +259,18 @@
1.194 "--------- replaceFormula: on Res + = ----------------------------";
1.195 "--------- replaceFormula: on Res + = ----------------------------";
1.196 "--------- replaceFormula: on Res + = ----------------------------";
1.197 - reset_states ();
1.198 + States.reset ();
1.199 CalcTree [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
1.200 ("Test", ["sqroot-test", "univariate", "equation", "test"],
1.201 ["Test", "squ-equ-test-subpbl1"]))];
1.202 Iterator 1; moveActiveRoot 1;
1.203 autoCalculate 1 CompleteCalcHead;
1.204 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
1.205 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 + - 1 * 2 = 0*);
1.206 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*- 1 + x*);
1.207 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);(*x + 1 = 2*)
1.208 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);(*x + 1 + - 1 * 2 = 0*);
1.209 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);(*- 1 + x*);
1.210
1.211 - replaceFormula 1 "-2 * 1 + (1 + x) = 0"; refFormula 1 (get_pos 1 1);
1.212 - val ((pt,_),_) = get_calc 1;
1.213 + replaceFormula 1 "-2 * 1 + (1 + x) = 0"; refFormula 1 (States.get_pos 1 1);
1.214 + val ((pt,_),_) = States.get_calc 1;
1.215 val str = pr_ctree pr_short pt;
1.216
1.217 (* before AK110725 this was
1.218 @@ -297,7 +297,7 @@
1.219 else error "inform.sml: diff.behav.replaceFormula: on Res += 1";
1.220
1.221 autoCalculate 1 CompleteCalc;
1.222 - val ((pt,pos as (p,_)),_) = get_calc 1;
1.223 + val ((pt,pos as (p,_)),_) = States.get_calc 1;
1.224 if pos = ([],Res) andalso "[x = 1]" = (UnparseC.term o fst) (get_obj g_result pt p) then()
1.225 else error "inform.sml: diff.behav.replaceFormula: on Res + = 2";
1.226 DEconstrCalcTree 1;
1.227 @@ -305,23 +305,23 @@
1.228 "--------- replaceFormula: on Res + = 1st Nd ---------------------";
1.229 "--------- replaceFormula: on Res + = 1st Nd ---------------------";
1.230 "--------- replaceFormula: on Res + = 1st Nd ---------------------";
1.231 - reset_states ();
1.232 + States.reset ();
1.233 CalcTree [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
1.234 ("Test", ["sqroot-test", "univariate", "equation", "test"],
1.235 ["Test", "squ-equ-test-subpbl1"]))];
1.236 Iterator 1; moveActiveRoot 1;
1.237 autoCalculate 1 CompleteCalcHead;
1.238 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
1.239 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 + - 1 * 2 = 0*);
1.240 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);(*x + 1 = 2*)
1.241 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);(*x + 1 + - 1 * 2 = 0*);
1.242
1.243 - replaceFormula 1 "x + 1 = 4 + -2"; refFormula 1 (get_pos 1 1);
1.244 - val ((pt,_),_) = get_calc 1;
1.245 + replaceFormula 1 "x + 1 = 4 + -2"; refFormula 1 (States.get_pos 1 1);
1.246 + val ((pt,_),_) = States.get_calc 1;
1.247 val str = pr_ctree pr_short pt;
1.248 writeln str;
1.249 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.250 else error "inform.sml: diff.behav.replaceFormula: on Res 1 + = 1";
1.251 autoCalculate 1 CompleteCalc;
1.252 - val ((pt,pos as (p,_)),_) = get_calc 1;
1.253 + val ((pt,pos as (p,_)),_) = States.get_calc 1;
1.254 if pos = ([],Res) andalso "[x = 1]" = (UnparseC.term o fst)(get_obj g_result pt p) then()
1.255 else error "inform.sml: diff.behav.replaceFormula: on Res + = 2";
1.256 DEconstrCalcTree 1;
1.257 @@ -329,22 +329,22 @@
1.258 "--------- replaceFormula: on Frm + = 1st Nd ---------------------";
1.259 "--------- replaceFormula: on Frm + = 1st Nd ---------------------";
1.260 "--------- replaceFormula: on Frm + = 1st Nd ---------------------";
1.261 - reset_states ();
1.262 + States.reset ();
1.263 CalcTree [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
1.264 ("Test", ["sqroot-test", "univariate", "equation", "test"],
1.265 ["Test", "squ-equ-test-subpbl1"]))];
1.266 Iterator 1; moveActiveRoot 1;
1.267 autoCalculate 1 CompleteCalcHead;
1.268 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
1.269 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);(*x + 1 = 2*)
1.270
1.271 - replaceFormula 1 "x + 1 = 4 + -2"; refFormula 1 (get_pos 1 1);
1.272 - val ((pt,_),_) = get_calc 1;
1.273 + replaceFormula 1 "x + 1 = 4 + -2"; refFormula 1 (States.get_pos 1 1);
1.274 + val ((pt,_),_) = States.get_calc 1;
1.275 val str = pr_ctree pr_short pt;
1.276 writeln str;
1.277 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.278 else error "inform.sml: diff.behav.replaceFormula: on Frm 1 + = 1";
1.279 autoCalculate 1 CompleteCalc;
1.280 - val ((pt,pos as (p,_)),_) = get_calc 1;
1.281 + val ((pt,pos as (p,_)),_) = States.get_calc 1;
1.282 if pos = ([],Res) andalso "[x = 1]" = (UnparseC.term o fst)(get_obj g_result pt p) then()
1.283 else error "inform.sml: diff.behav.replaceFormula: on Frm 1 + = 2";
1.284 DEconstrCalcTree 1;
1.285 @@ -352,18 +352,18 @@
1.286 "--------- replaceFormula: cut calculation -----------------------";
1.287 "--------- replaceFormula: cut calculation -----------------------";
1.288 "--------- replaceFormula: cut calculation -----------------------";
1.289 - reset_states ();
1.290 + States.reset ();
1.291 CalcTree [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
1.292 ("Test", ["sqroot-test", "univariate", "equation", "test"],
1.293 ["Test", "squ-equ-test-subpbl1"]))];
1.294 Iterator 1; moveActiveRoot 1;
1.295 autoCalculate 1 CompleteCalc;
1.296 moveActiveRoot 1; moveActiveDown 1;
1.297 - if get_pos 1 1 = ([1], Frm) then ()
1.298 + if States.get_pos 1 1 = ([1], Frm) then ()
1.299 else error "inform.sml: diff.behav. cut calculation 1";
1.300
1.301 - replaceFormula 1 "x + 1 = 4 + -2"; refFormula 1 (get_pos 1 1);
1.302 - val ((pt,p),_) = get_calc 1;
1.303 + replaceFormula 1 "x + 1 = 4 + -2"; refFormula 1 (States.get_pos 1 1);
1.304 + val ((pt,p),_) = States.get_calc 1;
1.305 val str = pr_ctree pr_short pt;
1.306 writeln str;
1.307 if p = ([1], Res) then ()
1.308 @@ -449,17 +449,17 @@
1.309 "--------- syntax error ------------------------------------------";
1.310 "--------- syntax error ------------------------------------------";
1.311 "--------- syntax error ------------------------------------------";
1.312 - reset_states ();
1.313 + States.reset ();
1.314 CalcTree [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
1.315 ("Test", ["sqroot-test", "univariate", "equation", "test"],
1.316 ["Test", "squ-equ-test-subpbl1"]))];
1.317 Iterator 1; moveActiveRoot 1;
1.318 autoCalculate 1 CompleteCalcHead;
1.319 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
1.320 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 + - 1 * 2 = 0*);
1.321 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);(*x + 1 = 2*)
1.322 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);(*x + 1 + - 1 * 2 = 0*);
1.323
1.324 appendFormula 1 " x - "; (*<ERROR> syntax error in ' x - ' </ERROR>*)
1.325 - val ((pt,_),_) = get_calc 1;
1.326 + val ((pt,_),_) = States.get_calc 1;
1.327 val str = pr_ctree pr_short pt;
1.328 writeln str;
1.329 if str = ". ----- pblobj -----\n1. x + 1 = 2\n" then ()
1.330 @@ -491,13 +491,13 @@
1.331 "--------- CAS-command on ([],Pbl) FE-interface ------------------";
1.332 "--------- CAS-command on ([],Pbl) FE-interface ------------------";
1.333 "--------- CAS-command on ([],Pbl) FE-interface ------------------";
1.334 -reset_states ();
1.335 +States.reset ();
1.336 CalcTree [([], References.empty)];
1.337 Iterator 1;
1.338 moveActiveRoot 1;
1.339 replaceFormula 1 "solve(x+1=2,x)";
1.340 autoCalculate 1 CompleteCalc;
1.341 -val ((pt,p),_) = get_calc 1;
1.342 +val ((pt,p),_) = States.get_calc 1;
1.343 Test_Tool.show_pt pt;
1.344 if p = ([], Res) then ()
1.345 else error "inform.sml: diff.behav. CAScmd ([],Pbl) FE-interface";
1.346 @@ -506,7 +506,7 @@
1.347 "--------- inform [rational,simplification] ----------------------";
1.348 "--------- inform [rational,simplification] ----------------------";
1.349 "--------- inform [rational,simplification] ----------------------";
1.350 -reset_states ();
1.351 +States.reset ();
1.352 CalcTree [(["Term (a * x / (b * x) + c * x / (d * x) + e / f)", "normalform N"],
1.353 ("Rational", ["rational", "simplification"], ["simplification", "of_rationals"]))];
1.354 Iterator 1; moveActiveRoot 1;
1.355 @@ -515,7 +515,7 @@
1.356 "--- (- 1) give a preview on the calculation without any input";
1.357 (*
1.358 autoCalculate 1 CompleteCalc;
1.359 -val ((pt, p), _) = get_calc 1;
1.360 +val ((pt, p), _) = States.get_calc 1;
1.361 Test_Tool.show_pt pt;
1.362 [
1.363 (([], Frm), Simplify (a * x / (b * x) + c * x / (d * x) + e / f)),
1.364 @@ -530,7 +530,7 @@
1.365 "--- (0) user input as the *first* step does not work, thus impdo at least 1 step";
1.366 autoCalculate 1 (Steps 1);
1.367 autoCalculate 1 (Steps 1);
1.368 -val ((pt, p), _) = get_calc 1;
1.369 +val ((pt, p), _) = States.get_calc 1;
1.370 (*Test_Tool.show_pt pt;
1.371 [
1.372 (([], Frm), Simplify (a * x / (b * x) + c * x / (d * x) + e / f)),
1.373 @@ -539,7 +539,7 @@
1.374 *)
1.375 "--- (1) input an arbitrary next formula";
1.376 appendFormula 1 "((a * d) + (c * b)) / (b * d) + e / f" (*|> Future.join*);
1.377 -val ((pt, p), _) = get_calc 1;
1.378 +val ((pt, p), _) = States.get_calc 1;
1.379 (*Test_Tool.show_pt pt;
1.380 [
1.381 (([], Frm), Simplify (a * x / (b * x) + c * x / (d * x) + e / f)),
1.382 @@ -550,14 +550,14 @@
1.383 (([2,2], Res), (a * d + c * b) / (b * d) + e / f),
1.384 (([2], Res), (a * d + c * b) / (b * d) + e / f)]
1.385 *)
1.386 -val ((pt,p),_) = get_calc 1;
1.387 +val ((pt,p),_) = States.get_calc 1;
1.388 if p = ([2], Res) andalso (length o children o (get_nd pt)) (fst p) = 2 then ()
1.389 else error ("inform.sml: [rational,simplification] 1");
1.390
1.391 "--- (2) input the next formula that would be presented by mat-engine";
1.392 (* generate a preview:
1.393 autoCalculate 1 (Steps 1);
1.394 -val ((pt, p), _) = get_calc 1;
1.395 +val ((pt, p), _) = States.get_calc 1;
1.396 Test_Tool.show_pt pt;
1.397 [
1.398 (([], Frm), Simplify (a * x / (b * x) + c * x / (d * x) + e / f)),
1.399 @@ -570,7 +570,7 @@
1.400 (([3], Res), (b * d * e + b * c * f + a * d * f) / (b * d * f))] <--- input this
1.401 *)
1.402 appendFormula 1 "(b * d * e + b * c * f + a * d * f) / (b * d * f)" (*|> Future.join*);
1.403 -val ((pt, p), _) = get_calc 1;
1.404 +val ((pt, p), _) = States.get_calc 1;
1.405 (*Test_Tool.show_pt pt;
1.406 [
1.407 (([], Frm), Simplify (a * x / (b * x) + c * x / (d * x) + e / f)),
1.408 @@ -587,7 +587,7 @@
1.409
1.410 "--- (3) input the exact final result";
1.411 appendFormula 1 "(b * d * e + b * c * f + a * d * f) / (b * d * f)" (*|> Future.join*);
1.412 -val ((pt, p), _) = get_calc 1;
1.413 +val ((pt, p), _) = States.get_calc 1;
1.414 (*Test_Tool.show_pt pt;
1.415 [
1.416 (([], Frm), Simplify (a * x / (b * x) + c * x / (d * x) + e / f)),
1.417 @@ -608,7 +608,7 @@
1.418
1.419 "--- (4) finish the calculation + check the postcondition (in the future)";
1.420 autoCalculate 1 CompleteCalc;
1.421 -val ((pt, p), _) = get_calc 1;
1.422 +val ((pt, p), _) = States.get_calc 1;
1.423 val (t, asm) = get_obj g_result pt [];
1.424 if UnparseC.term t = "(a * d * f + b * c * f + b * d * e) / (b * d * f)" andalso
1.425 UnparseC.terms asm =(*"[\"b * d * f \<noteq> 0\",\"d \<noteq> 0\",\"b \<noteq> 0\",\"a * x / (b * x) + c * x / (d * x) + e / f is_ratpolyexp\"]"*)
1.426 @@ -643,13 +643,13 @@
1.427 error "diff.sml behav.changed for CAS Diff (..., x)";
1.428 TermC.atomty t;
1.429 "-----------------------------------------------------------------";
1.430 -(*1>*)reset_states ();
1.431 +(*1>*)States.reset ();
1.432 (*2>*)CalcTree [([], References.empty)];
1.433 (*3>*)Iterator 1;moveActiveRoot 1;
1.434 "----- here the Headline has been finished";
1.435 (*4>*)moveActiveFormula 1 ([],Pbl);
1.436 (*5>*)replaceFormula 1 "Diff (x \<up> 2 + x + 1, x)";
1.437 -val ((pt,_),_) = get_calc 1;
1.438 +val ((pt,_),_) = States.get_calc 1;
1.439 val PblObj {probl, meth, spec, fmz, loc, ...} = get_obj I pt [];
1.440 val (SOME istate, NONE) = loc;
1.441 (*default_print_depth 5;*)
1.442 @@ -665,7 +665,7 @@
1.443 "----- here the CalcHead has been completed --- ONCE MORE ?????";
1.444
1.445 (***difference II***)
1.446 -val ((pt,p),_) = get_calc 1;
1.447 +val ((pt,p),_) = States.get_calc 1;
1.448 (*val p = ([], Pbl)*)
1.449 val PblObj {probl, meth, spec, fmz, loc, ...} = get_obj I pt [];
1.450 val (SOME istate, NONE) = loc;
1.451 @@ -691,7 +691,7 @@
1.452 (*7>*)fetchProposedTactic 1 (*--> Apply_Method*);
1.453 (*WN081028 fixed <ERROR> helpless </ERROR> by inform returning ...(.,Met)*)
1.454 autoCalculate 1 CompleteCalc;
1.455 -val ((pt,p),_) = get_calc 1;
1.456 +val ((pt,p),_) = States.get_calc 1;
1.457 val Form res = (#1 o ME_Misc.pt_extract) (pt, ([],Res));
1.458 Test_Tool.show_pt pt;
1.459
1.460 @@ -704,13 +704,13 @@
1.461 "--------- Take as 1st tac, start from exp -----------------------";
1.462 (*the following input is copied from BridgeLog Java <==> SML,
1.463 omitting unnecessary inputs*)
1.464 -(*1>*)reset_states ();
1.465 +(*1>*)States.reset ();
1.466 (*2>*)CalcTree [(["functionTerm (x \<up> 2 + x + 1)", "differentiateFor x", "derivative f_'_f"],("Isac_Knowledge",["derivative_of", "function"],["diff", "differentiate_on_R"]))];
1.467 (*3>*)Iterator 1; moveActiveRoot 1;
1.468
1.469 (*6>*)(*completeCalcHead*)autoCalculate 1 CompleteCalcHead;
1.470 (***difference II***)
1.471 -val ((pt,_),_) = get_calc 1;
1.472 +val ((pt,_),_) = States.get_calc 1;
1.473 val PblObj {probl, meth, spec, fmz, loc, ...} = get_obj I pt [];
1.474 val (SOME istate, NONE) = loc;
1.475 (*default_print_depth 5;*) writeln (Istate.string_of (fst istate)); (*default_print_depth 3;*)
1.476 @@ -734,7 +734,7 @@
1.477 writeln"-----------------------------------------------------------";
1.478 (*7>*)fetchProposedTactic 1 (*--> Apply_Method*);
1.479 autoCalculate 1 (Steps 1);
1.480 -val ((pt,p),_) = get_calc 1;
1.481 +val ((pt,p),_) = States.get_calc 1;
1.482 val Form res = (#1 o ME_Misc.pt_extract) (pt, p);
1.483 if UnparseC.term res = "d_d x (x \<up> 2 + x + 1)" then ()
1.484 else error "diff.sml Diff (x \<up> 2 + x + 1, x) from exp";
1.485 @@ -743,7 +743,7 @@
1.486 "--------- implicit_take, start with <NEW> (CAS input) ---------------";
1.487 "--------- implicit_take, start with <NEW> (CAS input) ---------------";
1.488 "--------- implicit_take, start with <NEW> (CAS input) ---------------";
1.489 -reset_states ();
1.490 +States.reset ();
1.491 CalcTree [([], References.empty)];
1.492 (*[[from sml: > @@@@@begin@@@@@
1.493 [[from sml: 1
1.494 @@ -1006,7 +1006,7 @@
1.495 "--------- embed fun check_for ------------------------";
1.496 "--------- embed fun check_for ------------------------";
1.497 "--------- embed fun check_for ------------------------";
1.498 -reset_states ();
1.499 +States.reset ();
1.500 CalcTree
1.501 [(["functionTerm (x \<up> 2 + sin (x \<up> 4))", "differentiateFor x", "derivative f_f'"],
1.502 ("Isac_Knowledge", ["derivative_of", "function"], ["diff", "differentiate_on_R"]))];
1.503 @@ -1019,8 +1019,8 @@
1.504
1.505 "~~~~~ fun appendFormula , args:"; val (cI, (ifo:TermC.as_string)) = (1, "d_d x (x \<up> 2) + cos (4 * x \<up> 3)");
1.506 "~~~~~ fun appendFormula' , args:"; val (cI, (ifo: TermC.as_string)) = (cI, ifo);
1.507 - val cs = get_calc cI
1.508 - val pos = get_pos cI 1;
1.509 + val cs = States.get_calc cI
1.510 + val pos = States.get_pos cI 1;
1.511 (*+*)if pos = ([1], Res) then () else error "inform with (positive) Error_Pattern.check_for broken 1";
1.512 val ("ok", cs' as (_, _, ptp)) = (*case*) Step.do_next pos cs (*of*);
1.513 (*case*) Step_Solve.by_term ptp (encode ifo) (*of*); (*ERROR WAS: "no derivation found"*)
1.514 @@ -1065,7 +1065,7 @@
1.515 "--------- embed fun find_fill_patterns ---------------------------";
1.516 "--------- embed fun find_fill_patterns ---------------------------";
1.517 "--------- embed fun find_fill_patterns ---------------------------";
1.518 -reset_states ();
1.519 +States.reset ();
1.520 CalcTree
1.521 [(["functionTerm (x \<up> 2 + sin (x \<up> 4))", "differentiateFor x", "derivative f_f'"],
1.522 ("Isac_Knowledge", ["derivative_of", "function"], ["diff", "differentiate_on_R"]))];
1.523 @@ -1080,8 +1080,8 @@
1.524 <CALCMESSAGE> no derivation found </CALCMESSAGE>*)
1.525
1.526 "~~~~~ fun findFillpatterns, args:"; val (cI, errpatID) = (1, "chain-rule-diff-both");
1.527 - val ((pt, _), _) = get_calc cI
1.528 - val pos = get_pos cI 1;
1.529 + val ((pt, _), _) = States.get_calc cI
1.530 + val pos = States.get_pos cI 1;
1.531 "~~~~~ fun find_fill_patterns , args:"; val ((pt, pos as (p, _)), errpatID) = ((pt, pos), errpatID);
1.532 val f_curr = Ctree.get_curr_formula (pt, pos);
1.533 val pp = Ctree.par_pblobj pt p
1.534 @@ -1150,7 +1150,7 @@
1.535 "--------- build fun is_exactly_equal, inputFillFormula ----------";
1.536 "--------- build fun is_exactly_equal, inputFillFormula ----------";
1.537 "--------- build fun is_exactly_equal, inputFillFormula ----------";
1.538 -reset_states ();
1.539 +States.reset ();
1.540 CalcTree
1.541 [(["functionTerm (x \<up> 2 + sin (x \<up> 4))", "differentiateFor x", "derivative f_f'"],
1.542 ("Isac_Knowledge", ["derivative_of", "function"], ["diff", "differentiate_on_R"]))];
1.543 @@ -1164,8 +1164,8 @@
1.544 would recognize "cos (4 * x \<up> (4 - 1)) + 2 * x" as well.
1.545 results in <CALCMESSAGE> error pattern #chain-rule-diff-both# </CALCMESSAGE>
1.546 instead of <CALCMESSAGE> no derivation found </CALCMESSAGE> *)
1.547 - val ((pt,pos), _) = get_calc 1;
1.548 - val p = get_pos 1 1;
1.549 + val ((pt,pos), _) = States.get_calc 1;
1.550 + val p = States.get_pos 1 1;
1.551 val (Form f, _, asms) = ME_Misc.pt_extract (pt, p);
1.552
1.553 if p = ([1], Res) andalso UnparseC.term f = "d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))" then
1.554 @@ -1179,8 +1179,8 @@
1.555 findFillpatterns 1 "chain-rule-diff-both"; (*<<<<<<<=================================*)
1.556 (*<CALCMESSAGE> fill patterns #fill-d_d-arg#d_d x (x \<up> 2) + d_d x (sin (x \<up> 4)) =
1.557 d_d x (x \<up> 2) + cos (x \<up> 4) * d_d x ?_dummy_1#fill-both-args#...#...#... *)
1.558 - val ((pt,pos),_) = get_calc 1;
1.559 - val p = get_pos 1 1;
1.560 + val ((pt,pos),_) = States.get_calc 1;
1.561 + val p = States.get_pos 1 1;
1.562
1.563 val (Form f, _, asms) = ME_Misc.pt_extract (pt, p);
1.564 if p = ([1], Res) andalso UnparseC.term f = "d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))" then
1.565 @@ -1193,8 +1193,8 @@
1.566
1.567 requestFillformula 1 ("chain-rule-diff-both", "fill-both-args");(*<<<<<<<============*)
1.568 (*<AUTOCALC> ([1], Res) ([2], Res) ([2], Res) </AUTOCALC>*)
1.569 - val ((pt,pos),_) = get_calc 1;
1.570 - val p = get_pos 1 1;
1.571 + val ((pt,pos),_) = States.get_calc 1;
1.572 + val p = States.get_pos 1 1;
1.573 val (Form f, _, asms) = ME_Misc.pt_extract (pt, p);
1.574 if p = ([1], Res) andalso existpt [2] pt
1.575 andalso UnparseC.term f = "d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))"
1.576 @@ -1212,8 +1212,8 @@
1.577 *)
1.578 "~~~~~ fun inputFillFormula, args:"; val (cI, ifo) =
1.579 (1, "d_d x (x \<up> 2) + cos (x \<up> 4) * d_d x (x \<up> 4)");
1.580 - val ((pt, _), _) = get_calc cI
1.581 - val pos = get_pos cI 1;
1.582 + val ((pt, _), _) = States.get_calc cI
1.583 + val pos = States.get_pos cI 1;
1.584
1.585 "~~~~~ fun is_exactly_equal, args:"; val ((pt, pos as (p, p_)), istr) = ((pt, pos), ifo);
1.586 val SOME ifo = parseNEW (ThyC.get_theory "Isac_Knowledge" |> Proof_Context.init_global) istr
1.587 @@ -1227,13 +1227,13 @@
1.588
1.589 "~~~~~ to inputFillFormula return val:"; val ("ok", tac) = ("ok", tac);
1.590 val ("ok", (_, c, ptp as (_,p'))) = Step.by_tactic tac (pt, pos);
1.591 - upd_calc cI (ptp, []);
1.592 - upd_ipos cI 1 p';
1.593 + States.upd_calc cI (ptp, []);
1.594 + States.upd_ipos cI 1 p';
1.595 autocalculateOK2xml cI pos (if null c then p' else last_elem c) p';
1.596
1.597 "~~~~~ final check:";
1.598 -val ((pt, _),_) = get_calc 1;
1.599 -val p = get_pos 1 1;
1.600 +val ((pt, _),_) = States.get_calc 1;
1.601 +val p = States.get_pos 1 1;
1.602 val (Form f, _, asms) = ME_Misc.pt_extract (pt, p);
1.603 if p = ([2], Res) andalso UnparseC.term f = "d_d x (x \<up> 2) + cos (x \<up> 4) * d_d x (x \<up> 4)"
1.604 then case get_obj g_tac pt (fst p) of Rewrite_Inst (["(''bdv'', x)"],