1.1 --- a/test/Tools/isac/Knowledge/polyminus.sml Fri Sep 09 10:53:51 2022 +0200
1.2 +++ b/test/Tools/isac/Knowledge/polyminus.sml Sun Sep 11 14:31:15 2022 +0200
1.3 @@ -371,66 +371,66 @@
1.4 "----------- pbl polynom vereinfachen p.33 -----------------------";
1.5 "----------- pbl polynom vereinfachen p.33 -----------------------";
1.6 "----------- 140 c ---";
1.7 -reset_states ();
1.8 +States.reset ();
1.9 CalcTree [(["Term (5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12)",
1.10 "normalform N"],
1.11 ("PolyMinus",["plus_minus", "polynom", "vereinfachen"],
1.12 ["simplification", "for_polynomials", "with_minus"]))];
1.13 moveActiveRoot 1;
1.14 autoCalculate 1 CompleteCalc;
1.15 -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
1.16 +val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
1.17 if p = ([], Res) andalso
1.18 UnparseC.term (get_obj g_res pt (fst p)) = "3 - 2 * e + 2 * f + 2 * g"
1.19 then () else error "polyminus.sml: Vereinfache (3 - 2 * e + 2 * f...";
1.20
1.21 "======= 140 d ---";
1.22 -reset_states ();
1.23 +States.reset ();
1.24 CalcTree [(["Term (-r - 2*s - 3*t + 5 + 4*r + 8*s - 5*t - 2)",
1.25 "normalform N"],
1.26 ("PolyMinus",["plus_minus", "polynom", "vereinfachen"],
1.27 ["simplification", "for_polynomials", "with_minus"]))];
1.28 moveActiveRoot 1;
1.29 autoCalculate 1 CompleteCalc;
1.30 -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
1.31 +val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
1.32 if p = ([], Res) andalso
1.33 UnparseC.term (get_obj g_res pt (fst p)) = "3 + 3 * r + 6 * s - 8 * t"
1.34 then () else error "polyminus.sml: Vereinfache 140 d)";
1.35
1.36 "======= 139 c ---";
1.37 -reset_states ();
1.38 +States.reset ();
1.39 CalcTree [(["Term (3*e - 6*f - 8*e - 4*f + 5*e + 7*f)",
1.40 "normalform N"],
1.41 ("PolyMinus",["plus_minus", "polynom", "vereinfachen"],
1.42 ["simplification", "for_polynomials", "with_minus"]))];
1.43 moveActiveRoot 1;
1.44 autoCalculate 1 CompleteCalc;
1.45 -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
1.46 +val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
1.47 if p = ([], Res) andalso
1.48 UnparseC.term (get_obj g_res pt (fst p)) = "- (3 * f)"
1.49 then () else error "polyminus.sml: Vereinfache 139 c)";
1.50
1.51 "======= 139 b ---";
1.52 -reset_states ();
1.53 +States.reset ();
1.54 CalcTree [(["Term (8*u - 5*v - 5*u + 7*v - 6*u - 3*v)",
1.55 "normalform N"],
1.56 ("PolyMinus",["plus_minus", "polynom", "vereinfachen"],
1.57 ["simplification", "for_polynomials", "with_minus"]))];
1.58 moveActiveRoot 1;
1.59 autoCalculate 1 CompleteCalc;
1.60 -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
1.61 +val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
1.62 if p = ([], Res) andalso
1.63 UnparseC.term (get_obj g_res pt (fst p)) = "- 3 * u - v"
1.64 then () else error "polyminus.sml: Vereinfache 139 b)";
1.65
1.66 "======= 138 a ---";
1.67 -reset_states ();
1.68 +States.reset ();
1.69 CalcTree [(["Term (2*u - 3*v - 6*u + 5*v)",
1.70 "normalform N"],
1.71 ("PolyMinus",["plus_minus", "polynom", "vereinfachen"],
1.72 ["simplification", "for_polynomials", "with_minus"]))];
1.73 moveActiveRoot 1;
1.74 autoCalculate 1 CompleteCalc;
1.75 -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
1.76 +val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
1.77 if p = ([], Res) andalso
1.78 UnparseC.term (get_obj g_res pt (fst p)) = "- 4 * u + 2 * v"
1.79 then () else error "polyminus.sml: Vereinfache 138 a)";
1.80 @@ -451,7 +451,7 @@
1.81 "----------- pbl polynom probe -----------------------------------";
1.82 "----------- pbl polynom probe -----------------------------------";
1.83 "----------- pbl polynom probe -----------------------------------";
1.84 -reset_states ();
1.85 +States.reset ();
1.86 CalcTree [(["Pruefe ((5::int)*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12 =\
1.87 \3 - 2 * e + 2 * f + 2 * (g::int))",
1.88 "mitWert [e = (1::int), f = (2::int), g = (3::int)]",
1.89 @@ -463,10 +463,10 @@
1.90 (* autoCalculate 1 CompleteCalcHead;
1.91 autoCalculate 1 (Steps 1);
1.92 autoCalculate 1 (Steps 1);
1.93 - val ((pt,p),_) = get_calc 1; UnparseC.term (get_obj g_res pt (fst p));
1.94 + val ((pt,p),_) = States.get_calc 1; UnparseC.term (get_obj g_res pt (fst p));
1.95 @@@@@WN081114 gives "??.empty", all "Pruefe" are the same,
1.96 although analogies work in interface.sml: FIXME.WN081114 in "Pruefe"*)
1.97 -val ((pt,p),_) = get_calc 1;
1.98 +val ((pt,p),_) = States.get_calc 1;
1.99 if p = ([], Res) andalso UnparseC.term (get_obj g_res pt (fst p)) = "11 = 11"
1.100 then () else error "polyminus.sml: Probe 11 = 11";
1.101 Test_Tool.show_pt pt;
1.102 @@ -475,21 +475,21 @@
1.103 "----------- pbl klammer polynom vereinfachen p.34 ---------------";
1.104 "----------- pbl klammer polynom vereinfachen p.34 ---------------";
1.105 "----------- pbl klammer polynom vereinfachen p.34 ---------------";
1.106 -reset_states ();
1.107 +States.reset ();
1.108 CalcTree [(["Term (2*u - 5 - (3 - 4*u) + (8*u + 9))",
1.109 "normalform N"],
1.110 ("PolyMinus",["klammer", "polynom", "vereinfachen"],
1.111 ["simplification", "for_polynomials", "with_parentheses"]))];
1.112 moveActiveRoot 1;
1.113 autoCalculate 1 CompleteCalc;
1.114 -val ((pt,p),_) = get_calc 1;
1.115 +val ((pt,p),_) = States.get_calc 1;
1.116 if p = ([], Res) andalso
1.117 UnparseC.term (get_obj g_res pt (fst p)) = "1 + 14 * u"
1.118 then () else error "polyminus.sml: Vereinfache (2*u - 5 - (3 - ...";
1.119 Test_Tool.show_pt pt;
1.120
1.121 "======= probe p.34 -----";
1.122 -reset_states ();
1.123 +States.reset ();
1.124 CalcTree [(["Pruefe (2*u - 5 - (3 - 4*u) + (8*u + 9) = 1 + 14 * (u::int))",
1.125 "mitWert [u = (2::int)]",
1.126 "Geprueft b"],
1.127 @@ -497,7 +497,7 @@
1.128 ["probe", "fuer_polynom"]))];
1.129 moveActiveRoot 1;
1.130 autoCalculate 1 CompleteCalc;
1.131 -val ((pt,p),_) = get_calc 1;
1.132 +val ((pt,p),_) = States.get_calc 1;
1.133 if p = ([], Res) andalso UnparseC.term (get_obj g_res pt (fst p)) = "29 = 29"
1.134 then () else error "polyminus.sml: Probe 29 = 29";
1.135 Test_Tool.show_pt pt;
1.136 @@ -506,7 +506,7 @@
1.137 "----------- try fun applyTactics --------------------------------";
1.138 "----------- try fun applyTactics --------------------------------";
1.139 "----------- try fun applyTactics --------------------------------";
1.140 -reset_states ();
1.141 +States.reset ();
1.142 CalcTree [(["Term (5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12)",
1.143 "normalform N"],
1.144 ("PolyMinus",["plus_minus", "polynom", "vereinfachen"],
1.145 @@ -515,12 +515,12 @@
1.146 autoCalculate 1 CompleteCalcHead;
1.147 autoCalculate 1 (Steps 1);
1.148 autoCalculate 1 (Steps 1);
1.149 -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
1.150 +val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
1.151 "----- 1 \<up> ";
1.152 fetchApplicableTactics 1 0 p;
1.153 val appltacs = specific_from_prog pt p;
1.154 applyTactic 1 p (hd appltacs) (*addiere_x_plus_minus*);
1.155 -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
1.156 +val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
1.157 "----- 2 \<up> ";
1.158 (*Rewrite.trace_on := true; ..stopped Test_Isac.thy*)
1.159 val erls = erls_ordne_alphabetisch;
1.160 @@ -540,25 +540,25 @@
1.161
1.162
1.163 applyTactic 1 p (hd (specific_from_prog pt p)) (*tausche_minus*);
1.164 -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
1.165 +val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
1.166 "----- 3 \<up> ";
1.167 applyTactic 1 p (hd (specific_from_prog pt p)) (**);
1.168 -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
1.169 +val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
1.170 "----- 4 \<up> ";
1.171 applyTactic 1 p (hd (specific_from_prog pt p)) (**);
1.172 -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
1.173 +val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
1.174 "----- 5 \<up> ";
1.175 applyTactic 1 p (hd (specific_from_prog pt p)) (**);
1.176 -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
1.177 +val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
1.178 "----- 6 \<up> ";
1.179
1.180 (*<CALCMESSAGE> failure </CALCMESSAGE>
1.181 applyTactic 1 p (hd (specific_from_prog pt p)) (**);
1.182 -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
1.183 +val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
1.184 "----- 7 \<up> ";
1.185 *)
1.186 autoCalculate 1 CompleteCalc;
1.187 -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
1.188 +val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
1.189 (*independent from failure above: met_simp_poly_minus not confluent:
1.190 (([9], Res), - (8 * g) + 10 * g + (3 - 2 * e + 2 * f)),
1.191 (([], Res), - (8 * g) + 10 * g + (3 - 2 * e + 2 * f))]
1.192 @@ -569,27 +569,27 @@
1.193
1.194
1.195 "#############################################################################";
1.196 -reset_states ();
1.197 +States.reset ();
1.198 CalcTree [(["Term (- (8 * g) + 10 * g + h)",
1.199 "normalform N"],
1.200 ("PolyMinus",["plus_minus", "polynom", "vereinfachen"],
1.201 ["simplification", "for_polynomials", "with_minus"]))];
1.202 moveActiveRoot 1;
1.203 autoCalculate 1 CompleteCalc;
1.204 -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
1.205 +val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
1.206 if p = ([], Res) andalso UnparseC.term (get_obj g_res pt (fst p)) = "2 * g + h"
1.207 then () else error "polyminus.sml: addiere_vor_minus";
1.208
1.209
1.210 "#############################################################################";
1.211 -reset_states ();
1.212 +States.reset ();
1.213 CalcTree [(["Term (- (8 * g) + 10 * g + f)",
1.214 "normalform N"],
1.215 ("PolyMinus",["plus_minus", "polynom", "vereinfachen"],
1.216 ["simplification", "for_polynomials", "with_minus"]))];
1.217 moveActiveRoot 1;
1.218 autoCalculate 1 CompleteCalc;
1.219 -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
1.220 +val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
1.221 if p = ([], Res) andalso UnparseC.term (get_obj g_res pt (fst p)) = "f + 2 * g"
1.222 then () else error "polyminus.sml: tausche_vor_plus";
1.223
1.224 @@ -627,14 +627,14 @@
1.225 *)
1.226
1.227 (*@@@@@@@*)
1.228 -reset_states ();
1.229 +States.reset ();
1.230 CalcTree [(["Term ((3*a + 2) * (4*a - 1))",
1.231 "normalform N"],
1.232 ("PolyMinus",["binom_klammer", "polynom", "vereinfachen"],
1.233 ["simplification", "for_polynomials", "with_parentheses_mult"]))];
1.234 moveActiveRoot 1;
1.235 autoCalculate 1 CompleteCalc;
1.236 -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
1.237 +val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
1.238
1.239 if p = ([], Res) andalso
1.240 UnparseC.term (get_obj g_res pt (fst p)) =(*"- 2 + 12 * a \<up> 2 + 5 * a" with OLD numerals*)
1.241 @@ -644,13 +644,13 @@
1.242 "----------- pbl binom polynom vereinfachen: cube ----------------";
1.243 "----------- pbl binom polynom vereinfachen: cube ----------------";
1.244 "----------- pbl binom polynom vereinfachen: cube ----------------";
1.245 -reset_states ();
1.246 +States.reset ();
1.247 CalcTree [(["Term (8*(a - q) + a - 2*q + 3*(a - 2*q))", "normalform N"],
1.248 ("PolyMinus",["binom_klammer", "polynom", "vereinfachen"],
1.249 ["simplification", "for_polynomials", "with_parentheses_mult"]))];
1.250 moveActiveRoot 1;
1.251 autoCalculate 1 CompleteCalc;
1.252 -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
1.253 +val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
1.254 if p = ([], Res) andalso UnparseC.term (get_obj g_res pt (fst p)) = "12 * a - 16 * q"
1.255 then () else error "pbl binom polynom vereinfachen: cube";
1.256