1.1 --- a/test/Tools/isac/Knowledge/polyminus.sml Tue Sep 28 08:58:06 2010 +0200
1.2 +++ b/test/Tools/isac/Knowledge/polyminus.sml Tue Sep 28 09:06:56 2010 +0200
1.3 @@ -36,31 +36,31 @@
1.4 ist_monom (str2term "12");
1.5 case eval_ist_monom 0 0 (str2term "12 ist_monom") 0 of
1.6 SOME ("12 ist_monom = True", _) => ()
1.7 - | _ => raise error "polyminus.sml: 12 ist_monom = True";
1.8 + | _ => error "polyminus.sml: 12 ist_monom = True";
1.9
1.10 case eval_ist_monom 0 0 (str2term "a ist_monom") 0 of
1.11 SOME ("a ist_monom = True", _) => ()
1.12 - | _ => raise error "polyminus.sml: a ist_monom = True";
1.13 + | _ => error "polyminus.sml: a ist_monom = True";
1.14
1.15 case eval_ist_monom 0 0 (str2term "(3*a) ist_monom") 0 of
1.16 SOME ("3 * a ist_monom = True", _) => ()
1.17 - | _ => raise error "polyminus.sml: 3 * a ist_monom = True";
1.18 + | _ => error "polyminus.sml: 3 * a ist_monom = True";
1.19
1.20 case eval_ist_monom 0 0 (str2term "(a^^^2) ist_monom") 0 of
1.21 SOME ("a ^^^ 2 ist_monom = True", _) => ()
1.22 - | _ => raise error "polyminus.sml: a^^^2 ist_monom = True";
1.23 + | _ => error "polyminus.sml: a^^^2 ist_monom = True";
1.24
1.25 case eval_ist_monom 0 0 (str2term "(3*a^^^2) ist_monom") 0 of
1.26 SOME ("3 * a ^^^ 2 ist_monom = True", _) => ()
1.27 - | _ => raise error "polyminus.sml: 3*a^^^2 ist_monom = True";
1.28 + | _ => error "polyminus.sml: 3*a^^^2 ist_monom = True";
1.29
1.30 case eval_ist_monom 0 0 (str2term "(a*b) ist_monom") 0 of
1.31 SOME ("a * b ist_monom = True", _) => ()
1.32 - | _ => raise error "polyminus.sml: a*b ist_monom = True";
1.33 + | _ => error "polyminus.sml: a*b ist_monom = True";
1.34
1.35 case eval_ist_monom 0 0 (str2term "(3*a*b) ist_monom") 0 of
1.36 SOME ("3 * a * b ist_monom = True", _) => ()
1.37 - | _ => raise error "polyminus.sml: 3*a*b ist_monom = True";
1.38 + | _ => error "polyminus.sml: 3*a*b ist_monom = True";
1.39
1.40
1.41 "----------- watch order_add_mult -------------------------------";
1.42 @@ -72,7 +72,7 @@
1.43 val t = str2term "((a + d) + c) + b";
1.44 val SOME (t,_) = rewrite_set_ thy false order_add_mult t; term2str t;
1.45 if term2str t = "a + (b + (c + d))" then ()
1.46 -else raise error "polyminus.sml 1 watch order_add_mult";
1.47 +else error "polyminus.sml 1 watch order_add_mult";
1.48 trace_rewrite:=false;
1.49
1.50 "----- the same stepwise...";
1.51 @@ -88,7 +88,7 @@
1.52 val SOME (t,_) = rewrite_ thy od e_rls true add_left_commute t;term2str t;
1.53 "a + (b + (c + d))";
1.54 if term2str t = "a + (b + (c + d))" then ()
1.55 -else raise error "polyminus.sml 2 watch order_add_mult";
1.56 +else error "polyminus.sml 2 watch order_add_mult";
1.57
1.58 "----- if parentheses are right, left_commute is (almost) sufficient...";
1.59 val t = str2term "a + (d + (c + b))";
1.60 @@ -105,7 +105,7 @@
1.61 val t = str2term "((5*a + 4*d) + 3*c) + 2*b";
1.62 val SOME (t,_) = rewrite_set_ thy false order_add_mult t; term2str t;
1.63 if term2str t = "2 * b + (3 * c + (4 * d + 5 * a))" then ()
1.64 -else raise error "polyminus.sml: order_add_mult changed";
1.65 +else error "polyminus.sml: order_add_mult changed";
1.66
1.67 "----- here we see rew_sub going into subterm with ord.rew....";
1.68 val od = ord_make_polynomial false Poly.thy;
1.69 @@ -130,31 +130,31 @@
1.70 (*
1.71 case eval_kleiner 0 0 (str2term "123 kleiner 32") 0 of
1.72 SOME ("12 kleiner 9 = False", _) => ()
1.73 - | _ => raise error "polyminus.sml: 12 kleiner 9 = False";
1.74 + | _ => error "polyminus.sml: 12 kleiner 9 = False";
1.75 *)
1.76 case eval_kleiner 0 0 (str2term "a kleiner b") 0 of
1.77 SOME ("a kleiner b = True", _) => ()
1.78 - | _ => raise error "polyminus.sml: a kleiner b = True";
1.79 + | _ => error "polyminus.sml: a kleiner b = True";
1.80
1.81 case eval_kleiner 0 0 (str2term "(10*g) kleiner f") 0 of
1.82 SOME ("10 * g kleiner f = False", _) => ()
1.83 - | _ => raise error "polyminus.sml: 10 * g kleiner f = False";
1.84 + | _ => error "polyminus.sml: 10 * g kleiner f = False";
1.85
1.86 case eval_kleiner 0 0 (str2term "(a^^^2) kleiner b") 0 of
1.87 SOME ("a ^^^ 2 kleiner b = True", _) => ()
1.88 - | _ => raise error "polyminus.sml: a ^^^ 2 kleiner b = True";
1.89 + | _ => error "polyminus.sml: a ^^^ 2 kleiner b = True";
1.90
1.91 case eval_kleiner 0 0 (str2term "(3*a^^^2) kleiner b") 0 of
1.92 SOME ("3 * a ^^^ 2 kleiner b = True", _) => ()
1.93 - | _ => raise error "polyminus.sml: 3 * a ^^^ 2 kleiner b = True";
1.94 + | _ => error "polyminus.sml: 3 * a ^^^ 2 kleiner b = True";
1.95
1.96 case eval_kleiner 0 0 (str2term "(a*b) kleiner c") 0 of
1.97 SOME ("a * b kleiner c = True", _) => ()
1.98 - | _ => raise error "polyminus.sml: a * b kleiner b = True";
1.99 + | _ => error "polyminus.sml: a * b kleiner b = True";
1.100
1.101 case eval_kleiner 0 0 (str2term "(3*a*b) kleiner c") 0 of
1.102 SOME ("3 * a * b kleiner c = True", _) => ()
1.103 - | _ => raise error "polyminus.sml: 3 * a * b kleiner b = True";
1.104 + | _ => error "polyminus.sml: 3 * a * b kleiner b = True";
1.105
1.106
1.107
1.108 @@ -165,7 +165,7 @@
1.109 val t = str2term "b + a";
1.110 val SOME (t,_) = rewrite_ thy od erls false tausche_plus t; term2str t;
1.111 if term2str t = "a + b" then ()
1.112 -else raise error "polyminus.sml: ordne_alphabetisch1 b + a";
1.113 +else error "polyminus.sml: ordne_alphabetisch1 b + a";
1.114
1.115 val erls = Atools_erls;
1.116 val t = str2term "2*a + 3*a";
1.117 @@ -177,41 +177,41 @@
1.118 val t = str2term "b + a";
1.119 val SOME (t,_) = rewrite_set_ thy false ordne_alphabetisch t; term2str t;
1.120 if term2str t = "a + b" then ()
1.121 -else raise error "polyminus.sml: ordne_alphabetisch a + b";
1.122 +else error "polyminus.sml: ordne_alphabetisch a + b";
1.123
1.124 val t = str2term "2*b + a";
1.125 val SOME (t,_) = rewrite_set_ thy false ordne_alphabetisch t; term2str t;
1.126 if term2str t = "a + 2 * b" then ()
1.127 -else raise error "polyminus.sml: ordne_alphabetisch a + 2 * b";
1.128 +else error "polyminus.sml: ordne_alphabetisch a + 2 * b";
1.129
1.130 val t = str2term "a + c + b";
1.131 val SOME (t,_) = rewrite_set_ thy false ordne_alphabetisch t; term2str t;
1.132 if term2str t = "a + b + c" then ()
1.133 -else raise error "polyminus.sml: ordne_alphabetisch a + b + c";
1.134 +else error "polyminus.sml: ordne_alphabetisch a + b + c";
1.135
1.136 "----- rewrite goes into subterms";
1.137 val t = str2term "a + c + b + d";
1.138 val SOME (t,_) = rewrite_ thy od erls false tausche_plus_plus t; term2str t;
1.139 if term2str t = "a + b + c + d" then ()
1.140 -else raise error "polyminus.sml: ordne_alphabetisch1 a + b + c + d";
1.141 +else error "polyminus.sml: ordne_alphabetisch1 a + b + c + d";
1.142
1.143 val t = str2term "a + c + d + b";
1.144 val SOME (t,_) = rewrite_set_ thy false ordne_alphabetisch t; term2str t;
1.145 if term2str t = "a + b + c + d" then ()
1.146 -else raise error "polyminus.sml: ordne_alphabetisch2 a + b + c + d";
1.147 +else error "polyminus.sml: ordne_alphabetisch2 a + b + c + d";
1.148
1.149 "----- here we see rew_sub going into subterm with cond.rew....";
1.150 val t = str2term "b + a + c + d";
1.151 val SOME (t,_) = rewrite_ thy od erls false tausche_plus t; term2str t;
1.152 if term2str t = "a + b + c + d" then ()
1.153 -else raise error "polyminus.sml: ordne_alphabetisch3 a + b + c + d";
1.154 +else error "polyminus.sml: ordne_alphabetisch3 a + b + c + d";
1.155
1.156 "----- compile rls for the most complicated terms";
1.157 val t = str2term "5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12";
1.158 "5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * g + 12";
1.159 val SOME (t,_) = rewrite_set_ thy false ordne_alphabetisch t;
1.160 if term2str t = "- 9 + 12 + 5 * e - 7 * e + 6 * f - 4 * f - 8 * g + 10 * g"
1.161 -then () else raise error "polyminus.sml: ordne_alphabetisch finished";
1.162 +then () else error "polyminus.sml: ordne_alphabetisch finished";
1.163
1.164
1.165 "----------- build fasse_zusammen --------------------------------";
1.166 @@ -220,7 +220,7 @@
1.167 val t = str2term "- 9 + 12 + 5 * e - 7 * e + 6 * f - 4 * f - 8 * g + 10 * g";
1.168 val SOME (t,_) = rewrite_set_ thy false fasse_zusammen t;
1.169 if term2str t = "3 + -2 * e + 2 * f + 2 * g" then ()
1.170 -else raise error "polyminus.sml: fasse_zusammen finished";
1.171 +else error "polyminus.sml: fasse_zusammen finished";
1.172
1.173 "----------- build verschoenere ----------------------------------";
1.174 "----------- build verschoenere ----------------------------------";
1.175 @@ -228,7 +228,7 @@
1.176 val t = str2term "3 + -2 * e + 2 * f + 2 * g";
1.177 val SOME (t,_) = rewrite_set_ thy false verschoenere t;
1.178 if term2str t = "3 - 2 * e + 2 * f + 2 * g" then ()
1.179 -else raise error "polyminus.sml: verschoenere 3 + -2 * e ...";
1.180 +else error "polyminus.sml: verschoenere 3 + -2 * e ...";
1.181
1.182 trace_rewrite:=true;
1.183 trace_rewrite:=false;
1.184 @@ -259,7 +259,7 @@
1.185 val ((pt,p),_) = get_calc 1; show_pt pt;
1.186 if p = ([], Res) andalso
1.187 term2str (get_obj g_res pt (fst p)) = "3 - 2 * e + 2 * f + 2 * g"
1.188 -then () else raise error "polyminus.sml: Vereinfache (3 - 2 * e + 2 * f...";
1.189 +then () else error "polyminus.sml: Vereinfache (3 - 2 * e + 2 * f...";
1.190
1.191 "----------- 140 d ---";
1.192 states:=[];
1.193 @@ -272,7 +272,7 @@
1.194 val ((pt,p),_) = get_calc 1; show_pt pt;
1.195 if p = ([], Res) andalso
1.196 term2str (get_obj g_res pt (fst p)) = "3 + 3 * r + 6 * s - 8 * t"
1.197 -then () else raise error "polyminus.sml: Vereinfache 140 d)";
1.198 +then () else error "polyminus.sml: Vereinfache 140 d)";
1.199
1.200
1.201 "----------- 139 c ---";
1.202 @@ -286,7 +286,7 @@
1.203 val ((pt,p),_) = get_calc 1; show_pt pt;
1.204 if p = ([], Res) andalso
1.205 term2str (get_obj g_res pt (fst p)) = "- (3 * f)"
1.206 -then () else raise error "polyminus.sml: Vereinfache 139 c)";
1.207 +then () else error "polyminus.sml: Vereinfache 139 c)";
1.208
1.209 "----------- 139 b ---";
1.210 states:=[];
1.211 @@ -299,7 +299,7 @@
1.212 val ((pt,p),_) = get_calc 1; show_pt pt;
1.213 if p = ([], Res) andalso
1.214 term2str (get_obj g_res pt (fst p)) = "-3 * u - v"
1.215 -then () else raise error "polyminus.sml: Vereinfache 139 b)";
1.216 +then () else error "polyminus.sml: Vereinfache 139 b)";
1.217
1.218 "----------- 138 a ---";
1.219 states:=[];
1.220 @@ -312,7 +312,7 @@
1.221 val ((pt,p),_) = get_calc 1; show_pt pt;
1.222 if p = ([], Res) andalso
1.223 term2str (get_obj g_res pt (fst p)) = "-4 * u + 2 * v"
1.224 -then () else raise error "polyminus.sml: Vereinfache 138 a)";
1.225 +then () else error "polyminus.sml: Vereinfache 138 a)";
1.226
1.227
1.228 "----------- met probe fuer_polynom ------------------------------";
1.229 @@ -349,7 +349,7 @@
1.230 although analogies work in interface.sml: FIXME.WN081114 in "Pruefe"*)
1.231 val ((pt,p),_) = get_calc 1;
1.232 if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) = "11 = 11"
1.233 -then () else raise error "polyminus.sml: Probe 11 = 11";
1.234 +then () else error "polyminus.sml: Probe 11 = 11";
1.235 show_pt pt;
1.236
1.237
1.238 @@ -366,7 +366,7 @@
1.239 val ((pt,p),_) = get_calc 1;
1.240 if p = ([], Res) andalso
1.241 term2str (get_obj g_res pt (fst p)) = "1 + 14 * u"
1.242 -then () else raise error "polyminus.sml: Vereinfache (2*u - 5 - (3 - ...";
1.243 +then () else error "polyminus.sml: Vereinfache (2*u - 5 - (3 - ...";
1.244 show_pt pt;
1.245
1.246 "----- probe p.34 -----";
1.247 @@ -380,7 +380,7 @@
1.248 autoCalculate 1 CompleteCalc;
1.249 val ((pt,p),_) = get_calc 1;
1.250 if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) = "29 = 29"
1.251 -then () else raise error "polyminus.sml: Probe 29 = 29";
1.252 +then () else error "polyminus.sml: Probe 29 = 29";
1.253 show_pt pt;
1.254
1.255
1.256 @@ -456,7 +456,7 @@
1.257 autoCalculate 1 CompleteCalc;
1.258 val ((pt,p),_) = get_calc 1; show_pt pt;
1.259 if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) = "2 * g + h"
1.260 -then () else raise error "polyminus.sml: addiere_vor_minus";
1.261 +then () else error "polyminus.sml: addiere_vor_minus";
1.262
1.263
1.264 states:=[];
1.265 @@ -468,7 +468,7 @@
1.266 autoCalculate 1 CompleteCalc;
1.267 val ((pt,p),_) = get_calc 1; show_pt pt;
1.268 if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) = "f + 2 * g"
1.269 -then () else raise error "polyminus.sml: tausche_vor_plus";
1.270 +then () else error "polyminus.sml: tausche_vor_plus";
1.271
1.272
1.273 "----------- pbl binom polynom vereinfachen p.39 -----------------";
1.274 @@ -520,7 +520,7 @@
1.275 (*
1.276 if p = ([], Res) andalso
1.277 term2str (get_obj g_res pt (fst p)) = "1 + 14 * u"
1.278 -then () else raise error "polyminus.sml: Vereinfache (2*u - 5 - (3 - ...";
1.279 +then () else error "polyminus.sml: Vereinfache (2*u - 5 - (3 - ...";
1.280 *)
1.281
1.282
1.283 @@ -555,7 +555,7 @@
1.284 case ma of
1.285 SOME ("matchsub (?a * (?b - ?c)) (8 * (a - q) + \
1.286 \a - 2 * q + 3 * (a - 2 * q)) = True", _) => ()
1.287 - | _ => raise error "polyminus.sml matchsub (?a * (?b - ?c)...A";
1.288 + | _ => error "polyminus.sml matchsub (?a * (?b - ?c)...A";
1.289
1.290 "--- does the respective prls rewrite ?";
1.291 val prls = append_rls "prls_pbl_vereinf_poly" e_rls
1.292 @@ -583,7 +583,7 @@
1.293 val SOME (t', _) = rewrite_set_ thy false prls t;
1.294 trace_rewrite := false;
1.295 if term2str t' = "False" then ()
1.296 -else raise error "polyminus.sml Not (matchsub (?a * (?b + ?c)) (8 ...";
1.297 +else error "polyminus.sml Not (matchsub (?a * (?b + ?c)) (8 ...";
1.298
1.299
1.300