1.1 --- a/test/Tools/isac/Knowledge/integrate.sml Tue Sep 28 08:58:06 2010 +0200
1.2 +++ b/test/Tools/isac/Knowledge/integrate.sml Tue Sep 28 09:06:56 2010 +0200
1.3 @@ -46,7 +46,7 @@
1.4
1.5 val t = str2term "ff x is_f_x";
1.6 case t of Const ("Integrate.is'_f'_x", _) $ _ => ()
1.7 - | _ => raise error "integrate.sml: parsing: ff x is_f_x";
1.8 + | _ => error "integrate.sml: parsing: ff x is_f_x";
1.9
1.10
1.11 "----------- integrate by rewriting ---------------------";
1.12 @@ -99,50 +99,50 @@
1.13 "----------- test add_new_c, is_f_x ---------------------";
1.14 val term = str2term "x^^^2*c + c_2";
1.15 val cc = new_c term;
1.16 -if term2str cc = "c_3" then () else raise error "integrate.sml: new_c ???";
1.17 +if term2str cc = "c_3" then () else error "integrate.sml: new_c ???";
1.18
1.19 val SOME (id,t') = eval_add_new_c "" "Integrate.add'_new'_c" term thy;
1.20 if term2str t' = "x ^^^ 2 * c + c_2 = x ^^^ 2 * c + c_2 + c_3" then ()
1.21 -else raise error "intergrate.sml: diff. eval_add_new_c";
1.22 +else error "intergrate.sml: diff. eval_add_new_c";
1.23
1.24 val cc = ("Integrate.add'_new'_c", eval_add_new_c "add_new_c_");
1.25 val SOME (thmstr, thm) = get_calculation1_ thy cc term;
1.26
1.27 val SOME (t',_) = rewrite_set_ thy true add_new_c term;
1.28 if term2str t' = "x ^^^ 2 * c + c_2 + c_3" then ()
1.29 -else raise error "intergrate.sml: diff. rewrite_set add_new_c 1";
1.30 +else error "intergrate.sml: diff. rewrite_set add_new_c 1";
1.31
1.32 val term = str2term "ff x = x^^^2*c + c_2";
1.33 val SOME (t',_) = rewrite_set_ thy true add_new_c term;
1.34 if term2str t' = "ff x = x ^^^ 2 * c + c_2 + c_3" then ()
1.35 -else raise error "intergrate.sml: diff. rewrite_set add_new_c 2";
1.36 +else error "intergrate.sml: diff. rewrite_set add_new_c 2";
1.37
1.38
1.39 (*WN080222 replace call_new_c with add_new_c----------------------
1.40 val term = str2term "new_c (c * x^^^2 + c_2)";
1.41 val SOME (_,t') = eval_new_c 0 0 term 0;
1.42 if term2s t' = "new_c c * x ^^^ 2 + c_2 = c_3" then ()
1.43 -else raise error "integrate.sml: eval_new_c ???";
1.44 +else error "integrate.sml: eval_new_c ???";
1.45
1.46 val t = str2term "matches (?u + new_c ?v) (x ^^^ 2 / 2)";
1.47 val SOME (_,t') = eval_matches "" "Tools.matches" t thy; term2s t';
1.48 if term2s t' = "matches (?u + new_c ?v) (x ^^^ 2 / 2) = False" then ()
1.49 -else raise error "integrate.sml: matches new_c = False";
1.50 +else error "integrate.sml: matches new_c = False";
1.51
1.52 val t = str2term "matches (?u + new_c ?v) (x ^^^ 2 / 2 + new_c x ^^^ 2 / 2)";
1.53 val SOME (_,t') = eval_matches "" "Tools.matches" t thy; term2s t';
1.54 if term2s t'="matches (?u + new_c ?v) (x ^^^ 2 / 2 + new_c x ^^^ 2 / 2) = True"
1.55 -then () else raise error "integrate.sml: matches new_c = True";
1.56 +then () else error "integrate.sml: matches new_c = True";
1.57
1.58 val t = str2term "ff x is_f_x";
1.59 val SOME (_,t') = eval_is_f_x "" "" t thy; term2s t';
1.60 if term2s t' = "(ff x is_f_x) = True" then ()
1.61 -else raise error "integrate.sml: eval_is_f_x --> true";
1.62 +else error "integrate.sml: eval_is_f_x --> true";
1.63
1.64 val t = str2term "q_0/2 * L * x is_f_x";
1.65 val SOME (_,t') = eval_is_f_x "" "" t thy; term2s t';
1.66 if term2s t' = "(q_0 / 2 * L * x is_f_x) = False" then ()
1.67 -else raise error "integrate.sml: eval_is_f_x --> false";
1.68 +else error "integrate.sml: eval_is_f_x --> false";
1.69
1.70 val conditions_in_integration =
1.71 Rls {id="conditions_in_integration",
1.72 @@ -183,20 +183,20 @@
1.73 "----- stepwise from the rulesets in simplify_Integral and below-----";
1.74 val rls = norm_Rational_noadd_fractions;
1.75 case rewrite_set_inst_ thy true subs rls t of
1.76 - SOME _ => raise error "integrate.sml simplify by ruleset norm_Rational_.#2"
1.77 + SOME _ => error "integrate.sml simplify by ruleset norm_Rational_.#2"
1.78 | NONE => ();
1.79
1.80 "===== test 2";
1.81 val rls = order_add_mult_in;
1.82 val SOME (t,[]) = rewrite_set_ thy true rls t;
1.83 if term2str t = "1 / EI * (L * (q_0 * x) / 2 + -1 * (q_0 * x ^^^ 2) / 2)" then()
1.84 -else raise error "integrate.sml simplify by ruleset order_add_mult_in #2";
1.85 +else error "integrate.sml simplify by ruleset order_add_mult_in #2";
1.86
1.87 "===== test 3";
1.88 val rls = discard_parentheses;
1.89 val SOME (t,[]) = rewrite_set_ thy true rls t;
1.90 if term2str t = "1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)" then ()
1.91 -else raise error "integrate.sml simplify by ruleset discard_parenth.. #3";
1.92 +else error "integrate.sml simplify by ruleset discard_parenth.. #3";
1.93
1.94 "===== test 4";
1.95 val rls =
1.96 @@ -223,14 +223,14 @@
1.97
1.98 val SOME (t, []) = rewrite_set_inst_ thy true subs rls t;
1.99 if term2str t = "1 / EI * (L * q_0 / 2 * x + -1 * q_0 / 2 * x ^^^ 2)" then ()
1.100 -else raise error "integrate.sml simplify by ruleset separate_bdv.. #4";
1.101 +else error "integrate.sml simplify by ruleset separate_bdv.. #4";
1.102
1.103 "===== test 5";
1.104 val t = str2term "1/EI * (L * q_0 * x / 2 + -1 * q_0 * x^^^2 / 2)";
1.105 val rls = simplify_Integral;
1.106 val SOME (t,[]) = rewrite_set_inst_ thy true subs rls t;
1.107 if term2str t = "1 / EI * (L * q_0 / 2 * x + -1 * q_0 / 2 * x ^^^ 2)" then ()
1.108 -else raise error "integrate.sml, simplify_Integral #99";
1.109 +else error "integrate.sml, simplify_Integral #99";
1.110
1.111
1.112 "........... 2nd integral ........................................";
1.113 @@ -247,7 +247,7 @@
1.114 "Integral 1 / EI * (L * q_0 / 4 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3) D x"
1.115 GOON: still 2*3 TODO...
1.116 "Integral 1 / EI * (L * q_0 / 4 * x ^^^ 2 + -1 * q_0 / (2 * 3) * x ^^^ 3) D x"
1.117 -then () else raise error "integrate.sml, simplify_Integral #198";
1.118 +then () else error "integrate.sml, simplify_Integral #198";
1.119
1.120
1.121 trace_rewrite := true;
1.122 @@ -263,7 +263,7 @@
1.123 val SOME (t,[]) = rewrite_set_ thy true rls t;
1.124 if term2str t =
1.125 "1 / EI * (L * q_0 / 4 * (x ^^^ 3 / 3) + -1 * q_0 / 6 * (x ^^^ 4 / 4))"
1.126 -then () else raise error "integrate.sml, simplify_Integral #199";
1.127 +then () else error "integrate.sml, simplify_Integral #199";
1.128
1.129
1.130
1.131 @@ -286,45 +286,45 @@
1.132 val str = rewrit_sinst subs rls "Integral x D x";
1.133 val str = rewrit_sinst subs rls "Integral c * x ^^^ 2 + c_2 D x";
1.134 if str = "c * (x ^^^ 3 / 3) + c_2 * x"
1.135 -then () else raise error "integrate.sml: diff.behav. in integration_rules";
1.136 +then () else error "integrate.sml: diff.behav. in integration_rules";
1.137
1.138 val rls = "add_new_c";
1.139 val str = rewrit_sinst subs rls "c * (x ^^^ 3 / 3) + c_2 * x";
1.140 if str = "c * (x ^^^ 3 / 3) + c_2 * x + c_3" then ()
1.141 -else raise error "integrate.sml: diff.behav. in add_new_c simpl.";
1.142 +else error "integrate.sml: diff.behav. in add_new_c simpl.";
1.143
1.144 val str = rewrit_sinst subs rls "F x = x ^^^ 3 / 3 + x";
1.145 if str = "F x = x ^^^ 3 / 3 + x + c"(*not "F x + c =..."*) then ()
1.146 -else raise error "integrate.sml: diff.behav. in add_new_c equation";
1.147 +else error "integrate.sml: diff.behav. in add_new_c equation";
1.148
1.149 val rls = "simplify_Integral";
1.150 (*~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
1.151 val str = "ff x = c * x + -1 * q_0 * (x ^^^ 2 / 2) + c_2";
1.152 val str = rewrit_sinst subs rls str;
1.153 if str = "ff x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2"
1.154 -then () else raise error "integrate.sml: diff.behav. in simplify_I #1";
1.155 +then () else error "integrate.sml: diff.behav. in simplify_I #1";
1.156
1.157 val rls = "integration";
1.158 (*~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
1.159 val str = rewrit_sinst subs rls "Integral c * x ^^^ 2 + c_2 D x";
1.160 if str = "c_3 + c_2 * x + c / 3 * x ^^^ 3"
1.161 -then () else raise error "integrate.sml: diff.behav. in integration #1";
1.162 +then () else error "integrate.sml: diff.behav. in integration #1";
1.163
1.164 val str = rewrit_sinst subs rls "Integral 3*x^^^2 + 2*x + 1 D x";
1.165 if str = "c + x + x ^^^ 2 + x ^^^ 3" then ()
1.166 -else raise error "integrate.sml: diff.behav. in integration #2";
1.167 +else error "integrate.sml: diff.behav. in integration #2";
1.168
1.169 val str = rewrit_sinst subs rls
1.170 "Integral 1 / EI * (L * q_0 / 2 * x + -1 * q_0 / 2 * x ^^^ 2) D x";
1.171 if str =
1.172 "c + 1 / EI * (L * q_0 / 4 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)"
1.173 -then () else raise error "integrate.sml: diff.behav. in integration #3";
1.174 +then () else error "integrate.sml: diff.behav. in integration #3";
1.175
1.176 val str = "Integral "^str^" D x";
1.177 val str = rewrit_sinst subs rls str;
1.178 if str =
1.179 "c_2 + c * x + 1 / EI * (L * q_0 / 12 * x ^^^ 3 + -1 * q_0 / 24 * x ^^^ 4)"
1.180 -then () else raise error "integrate.sml: diff.behav. in integration #4";
1.181 +then () else error "integrate.sml: diff.behav. in integration #4";
1.182
1.183
1.184 "----------- rewrite 3rd integration in 7.27 ------------";
1.185 @@ -337,11 +337,11 @@
1.186 val SOME(t,_)= rewrite_set_inst_ thy true bdv simplify_Integral t;
1.187 if term2str t =
1.188 "Integral 1 / EI * (L * q_0 / 2 * x + -1 * q_0 / 2 * x ^^^ 2) D x" then ()
1.189 -else raise error "integrate.sml 3rd integration in 7.27, simplify_Integral";
1.190 +else error "integrate.sml 3rd integration in 7.27, simplify_Integral";
1.191
1.192 val SOME(t,_)= rewrite_set_inst_ thy true bdv integration t;
1.193 if term2str t = "c + 1 / EI * (L * q_0 / 4 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)"
1.194 -then () else raise error "integrate.sml 3rd integration in 7.27, integration";
1.195 +then () else error "integrate.sml 3rd integration in 7.27, integration";
1.196
1.197
1.198 "----------- check probem type --------------------------";
1.199 @@ -357,7 +357,7 @@
1.200 val t2 = (term_of o hd o tl) chkmodel;
1.201 val t3 = (term_of o hd o tl o tl) chkmodel;
1.202 case t3 of Const ("Integrate.antiDerivative", _) $ _ => ()
1.203 - | _ => raise error "integrate.sml: Integrate.antiDerivative ???";
1.204 + | _ => error "integrate.sml: Integrate.antiDerivative ???";
1.205
1.206 val model = {Given =["functionTerm f_f", "integrateBy v_v"],
1.207 Where =[],
1.208 @@ -369,7 +369,7 @@
1.209 val t2 = (term_of o hd o tl) chkmodel;
1.210 val t3 = (term_of o hd o tl o tl) chkmodel;
1.211 case t3 of Const ("Integrate.antiDerivativeName", _) $ _ => ()
1.212 - | _ => raise error "integrate.sml: Integrate.antiDerivativeName";
1.213 + | _ => error "integrate.sml: Integrate.antiDerivativeName";
1.214
1.215 "----- compare 'Find's from problem, script, formalization -------";
1.216 val {ppc,...} = get_pbt ["named","integrate","function"];
1.217 @@ -377,18 +377,18 @@
1.218 F1_ as Free ("F_", F1_type))) = last_elem ppc;
1.219 val {scr = Script sc,... } = get_met ["diff","integration","named"];
1.220 val [_,_, F2_] = formal_args sc;
1.221 -if F1_ = F2_ then () else raise error "integrate.sml: unequal find's";
1.222 +if F1_ = F2_ then () else error "integrate.sml: unequal find's";
1.223
1.224 val ((dsc as Const ("Integrate.antiDerivativeName", _))
1.225 $ Free ("ff", F3_type)) = str2term "antiDerivativeName ff";
1.226 -if is_dsc dsc then () else raise error "integrate.sml: no description";
1.227 +if is_dsc dsc then () else error "integrate.sml: no description";
1.228 if F1_type = F3_type then ()
1.229 -else raise error "integrate.sml: unequal types in find's";
1.230 +else error "integrate.sml: unequal types in find's";
1.231
1.232 show_ptyps();
1.233 val pbl = get_pbt ["integrate","function"];
1.234 case #cas pbl of SOME (Const ("Integrate.Integrate",_) $ _) => ()
1.235 - | _ => raise error "integrate.sml: Integrate.Integrate ???";
1.236 + | _ => error "integrate.sml: Integrate.Integrate ???";
1.237
1.238
1.239 "----------- check Scripts ------------------------------";
1.240 @@ -432,7 +432,7 @@
1.241 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.242 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.243 if f2str f = "c + x + 1 / 3 * x ^^^ 3" then ()
1.244 -else raise error "integrate.sml: method [diff,integration]";
1.245 +else error "integrate.sml: method [diff,integration]";
1.246
1.247
1.248 "----------- me method [diff,integration,named] ---------";
1.249 @@ -457,7 +457,7 @@
1.250 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.251 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.252 if f2str f = "F x = c + x + 1 / 3 * x ^^^ 3" then()
1.253 -else raise error "integrate.sml: method [diff,integration,named]";
1.254 +else error "integrate.sml: method [diff,integration,named]";
1.255
1.256
1.257 "----------- me met [diff,integration,named] Biegelinie.Q";
1.258 @@ -484,7 +484,7 @@
1.259 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.260
1.261 if f2str f = "Q x = c + -1 * q_0 * x" then()
1.262 -else raise error "integrate.sml: method [diff,integration,named] .Q";
1.263 +else error "integrate.sml: method [diff,integration,named] .Q";
1.264
1.265
1.266 "----------- interSteps [diff,integration] --------------";
1.267 @@ -503,7 +503,7 @@
1.268 interSteps 1 ([1],Res);
1.269 val ((pt,p),_) = get_calc 1; show_pt pt;
1.270 if existpt' ([1,3], Res) pt then ()
1.271 -else raise error "integrate.sml: interSteps on Rewrite_Set_Inst 1";
1.272 +else error "integrate.sml: interSteps on Rewrite_Set_Inst 1";
1.273
1.274
1.275 "----------- method analog to rls 'integration' ---------";
1.276 @@ -551,7 +551,7 @@
1.277 autoCalculate 1 CompleteCalc;
1.278 val ((pt,p),_) = get_calc 1; show_pt pt;
1.279 if existpt' ([3], Res) pt then ()
1.280 -else raise error "integrate.sml: test-script doesnt work";
1.281 +else error "integrate.sml: test-script doesnt work";
1.282
1.283
1.284 "----------- Ambiguous input: Integral ?u + ?v D ?bdv = .";
1.285 @@ -587,7 +587,7 @@
1.286 *)
1.287
1.288 if existpt' ([1,1,5], Res) pt then ()
1.289 -else raise error "integrate.sml: interSteps on Rewrite_Set_Inst 2";
1.290 +else error "integrate.sml: interSteps on Rewrite_Set_Inst 2";
1.291
1.292
1.293 "----------- CAS input ----------------------------------";
1.294 @@ -595,7 +595,7 @@
1.295 "----------- CAS input ----------------------------------";
1.296 val t = str2term "Integrate (x^^^2 + x + 1, x)";
1.297 case t of Const ("Integrate.Integrate", _) $ _ => ()
1.298 - | _ => raise error "diff.sml behav.changed for Integrate (..., x)";
1.299 + | _ => error "diff.sml behav.changed for Integrate (..., x)";
1.300 atomty t;
1.301
1.302 states:=[];
1.303 @@ -609,7 +609,7 @@
1.304 show_pt pt;
1.305 (* WN070703 does not work like Diff due to error in next-pos
1.306 if p = ([], Res) andalso term2str res = "5 * a" then ()
1.307 -else raise error "diff.sml behav.changed for Integrate (x^2 + x + 1, x)";
1.308 +else error "diff.sml behav.changed for Integrate (x^2 + x + 1, x)";
1.309 *)
1.310
1.311 ===== inhibit exn ============================================================*)