wneuper/isa: comparison test/Tools/isac/Knowledge/integrate.sml

equal deleted inserted replaced

-:95d956108461
+:460c24a6a6ba
 val t = str2term "Integral x^^^2 D x";
 atomty t;
 val t = str2term "ff x is_f_x";
 case t of Const ("Integrate.is'_f'_x", _) $ _ => ()
-	| _ => raise error "integrate.sml: parsing: ff x is_f_x";
+	| _ => error "integrate.sml: parsing: ff x is_f_x";
 "----------- integrate by rewriting ---------------------";
 "----------- integrate by rewriting ---------------------";
 "----------- integrate by rewriting ---------------------";
 "----------- test add_new_c, is_f_x ---------------------";
 "----------- test add_new_c, is_f_x ---------------------";
 "----------- test add_new_c, is_f_x ---------------------";
 val term = str2term "x^^^2*c + c_2";
 val cc = new_c term;
-if term2str cc = "c_3" then () else raise error "integrate.sml: new_c ???";
+if term2str cc = "c_3" then () else error "integrate.sml: new_c ???";
 val SOME (id,t') = eval_add_new_c "" "Integrate.add'_new'_c" term thy;
 if term2str t' = "x ^^^ 2 * c + c_2 = x ^^^ 2 * c + c_2 + c_3" then ()
-else raise error "intergrate.sml: diff. eval_add_new_c";
+else error "intergrate.sml: diff. eval_add_new_c";
 val cc = ("Integrate.add'_new'_c", eval_add_new_c "add_new_c_");
 val SOME (thmstr, thm) = get_calculation1_ thy cc term;
 val SOME (t',_) = rewrite_set_ thy true add_new_c term;
 if term2str t' = "x ^^^ 2 * c + c_2 + c_3" then ()
-else raise error "intergrate.sml: diff. rewrite_set add_new_c 1";
+else error "intergrate.sml: diff. rewrite_set add_new_c 1";
 val term = str2term "ff x = x^^^2*c + c_2";
 val SOME (t',_) = rewrite_set_ thy true add_new_c term;
 if term2str t' = "ff x = x ^^^ 2 * c + c_2 + c_3" then ()
-else raise error "intergrate.sml: diff. rewrite_set add_new_c 2";
+else error "intergrate.sml: diff. rewrite_set add_new_c 2";
 (*WN080222 replace call_new_c with add_new_c----------------------
 val term = str2term "new_c (c * x^^^2 + c_2)";
 val SOME (_,t') = eval_new_c 0 0 term 0;
 if term2s t' = "new_c c * x ^^^ 2 + c_2 = c_3" then ()
-else raise error "integrate.sml: eval_new_c ???";
+else error "integrate.sml: eval_new_c ???";
 val t = str2term "matches (?u + new_c ?v) (x ^^^ 2 / 2)";
 val SOME (_,t') = eval_matches "" "Tools.matches" t thy; term2s t';
 if term2s t' = "matches (?u + new_c ?v) (x ^^^ 2 / 2) = False" then ()
-else raise error "integrate.sml: matches new_c = False";
+else error "integrate.sml: matches new_c = False";
 val t = str2term "matches (?u + new_c ?v) (x ^^^ 2 / 2 + new_c x ^^^ 2 / 2)";
 val SOME (_,t') = eval_matches "" "Tools.matches" t thy; term2s t';
 if term2s t'="matches (?u + new_c ?v) (x ^^^ 2 / 2 + new_c x ^^^ 2 / 2) = True"
-then () else raise error "integrate.sml: matches new_c = True";
+then () else error "integrate.sml: matches new_c = True";
 val t = str2term "ff x is_f_x";
 val SOME (_,t') = eval_is_f_x "" "" t thy; term2s t';
 if term2s t' = "(ff x is_f_x) = True" then ()
-else raise error "integrate.sml: eval_is_f_x --> true";
+else error "integrate.sml: eval_is_f_x --> true";
 val t = str2term "q_0/2 * L * x is_f_x";
 val SOME (_,t') = eval_is_f_x "" "" t thy; term2s t';
 if term2s t' = "(q_0 / 2 * L * x is_f_x) = False" then ()
-else raise error "integrate.sml: eval_is_f_x --> false";
+else error "integrate.sml: eval_is_f_x --> false";
 val conditions_in_integration =
 Rls {id="conditions_in_integration",
 preconds = [],
 rew_ord = ("termlessI",termlessI),
 val t = str2term "1/EI * (L * q_0 * x / 2 + -1 * q_0 * x^^^2 / 2)";
 "----- stepwise from the rulesets in simplify_Integral and below-----";
 val rls = norm_Rational_noadd_fractions;
 case rewrite_set_inst_ thy true subs rls t of
-SOME _ => raise error "integrate.sml simplify by ruleset norm_Rational_.#2"
+SOME _ => error "integrate.sml simplify by ruleset norm_Rational_.#2"
 | NONE => ();
 "===== test 2";
 val rls = order_add_mult_in;
 val SOME (t,[]) = rewrite_set_ thy true rls t;
 if term2str t = "1 / EI * (L * (q_0 * x) / 2 + -1 * (q_0 * x ^^^ 2) / 2)" then()
-else raise error "integrate.sml simplify by ruleset order_add_mult_in #2";
+else error "integrate.sml simplify by ruleset order_add_mult_in #2";
 "===== test 3";
 val rls = discard_parentheses;
 val SOME (t,[]) = rewrite_set_ thy true rls t;
 if term2str t = "1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)" then ()
-else raise error "integrate.sml simplify by ruleset discard_parenth.. #3";
+else error "integrate.sml simplify by ruleset discard_parenth.. #3";
 "===== test 4";
 val rls =
 (append_rls "separate_bdv"
 	       collect_bdv
 @{thm separate_1_bdv_n}; (*::real ..because of ^^^*)
 (*show_types := false; --- do we need type-constraint in thms? YES ?!?!?!*)
 val SOME (t, []) = rewrite_set_inst_ thy true subs rls t;
 if term2str t = "1 / EI * (L * q_0 / 2 * x + -1 * q_0 / 2 * x ^^^ 2)" then ()
-else raise error "integrate.sml simplify by ruleset separate_bdv.. #4";
+else error "integrate.sml simplify by ruleset separate_bdv.. #4";
 "===== test 5";
 val t = str2term "1/EI * (L * q_0 * x / 2 + -1 * q_0 * x^^^2 / 2)";
 val rls = simplify_Integral;
 val SOME (t,[]) = rewrite_set_inst_ thy true subs rls t;
 if term2str t = "1 / EI * (L * q_0 / 2 * x + -1 * q_0 / 2 * x ^^^ 2)" then ()
-else raise error "integrate.sml, simplify_Integral #99";
+else error "integrate.sml, simplify_Integral #99";
 "........... 2nd integral ........................................";
 "........... 2nd integral ........................................";
 "........... 2nd integral ........................................";
 (*===== inhibit exn ============================================================
 if term2str t =
 "Integral 1 / EI * (L * q_0 / 4 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3) D x"
 GOON: still 2*3 TODO...
 "Integral 1 / EI * (L * q_0 / 4 * x ^^^ 2 + -1 * q_0 / (2 * 3) * x ^^^ 3) D x"
-then () else raise error "integrate.sml, simplify_Integral #198";
+then () else error "integrate.sml, simplify_Integral #198";
 trace_rewrite := true;
 tracing "====== test 4 =============================";
 tracing "====== test 4 =============================";
 val rls = integration_rules;
 val SOME (t,[]) = rewrite_set_ thy true rls t;
 if term2str t =
 "1 / EI * (L * q_0 / 4 * (x ^^^ 3 / 3) + -1 * q_0 / 6 * (x ^^^ 4 / 4))"
-then () else raise error "integrate.sml, simplify_Integral #199";
+then () else error "integrate.sml, simplify_Integral #199";
 "----------- simplify by extending make_polynomial_in ---";
 "----------- simplify by extending make_polynomial_in ---";
 fst (the (rewrite_set_inst "Integrate" true subs rls str));
 (*~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
 val str = rewrit_sinst subs rls "Integral x D x";
 val str = rewrit_sinst subs rls "Integral c * x ^^^ 2 + c_2 D x";
 if str = "c * (x ^^^ 3 / 3) + c_2 * x"
-then () else raise error "integrate.sml: diff.behav. in integration_rules";
+then () else error "integrate.sml: diff.behav. in integration_rules";
 val rls = "add_new_c";
 val str = rewrit_sinst subs rls "c * (x ^^^ 3 / 3) + c_2 * x";
 if str = "c * (x ^^^ 3 / 3) + c_2 * x + c_3" then ()
-else raise error "integrate.sml: diff.behav. in add_new_c simpl.";
+else error "integrate.sml: diff.behav. in add_new_c simpl.";
 val str = rewrit_sinst subs rls "F x = x ^^^ 3 / 3 + x";
 if str = "F x = x ^^^ 3 / 3 + x + c"(*not "F x + c =..."*) then ()
-else raise error "integrate.sml: diff.behav. in add_new_c equation";
+else error "integrate.sml: diff.behav. in add_new_c equation";
 val rls = "simplify_Integral";
 (*~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
 val str = "ff x = c * x + -1 * q_0 * (x ^^^ 2 / 2) + c_2";
 val str = rewrit_sinst subs rls str;
 if str = "ff x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2"
-then () else raise error "integrate.sml: diff.behav. in simplify_I #1";
+then () else error "integrate.sml: diff.behav. in simplify_I #1";
 val rls = "integration";
 (*~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
 val str = rewrit_sinst subs rls "Integral c * x ^^^ 2 + c_2 D x";
 if str = "c_3 + c_2 * x + c / 3 * x ^^^ 3"
-then () else raise error "integrate.sml: diff.behav. in integration #1";
+then () else error "integrate.sml: diff.behav. in integration #1";
 val str = rewrit_sinst subs rls "Integral 3*x^^^2 + 2*x + 1 D x";
 if str = "c + x + x ^^^ 2 + x ^^^ 3" then ()
-else raise error "integrate.sml: diff.behav. in integration #2";
+else error "integrate.sml: diff.behav. in integration #2";
 val str = rewrit_sinst subs rls
 "Integral 1 / EI * (L * q_0 / 2 * x + -1 * q_0 / 2 * x ^^^ 2) D x";
 if str =
 "c + 1 / EI * (L * q_0 / 4 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)"
-then () else raise error "integrate.sml: diff.behav. in integration #3";
+then () else error "integrate.sml: diff.behav. in integration #3";
 val str = "Integral "^str^" D x";
 val str = rewrit_sinst subs rls str;
 if str =
 "c_2 + c * x + 1 / EI * (L * q_0 / 12 * x ^^^ 3 + -1 * q_0 / 24 * x ^^^ 4)"
-then () else raise error "integrate.sml: diff.behav. in integration #4";
+then () else error "integrate.sml: diff.behav. in integration #4";
 "----------- rewrite 3rd integration in 7.27 ------------";
 "----------- rewrite 3rd integration in 7.27 ------------";
 "----------- rewrite 3rd integration in 7.27 ------------";
 val t = str2term
 	    "Integral 1 / EI * ((L * q_0 * x + -1 * q_0 * x ^^^ 2) / 2) D x";
 val SOME(t,_)= rewrite_set_inst_ thy true bdv simplify_Integral t;
 if term2str t =
 "Integral 1 / EI * (L * q_0 / 2 * x + -1 * q_0 / 2 * x ^^^ 2) D x" then ()
-else raise error "integrate.sml 3rd integration in 7.27, simplify_Integral";
+else error "integrate.sml 3rd integration in 7.27, simplify_Integral";
 val SOME(t,_)= rewrite_set_inst_ thy true bdv integration t;
 if term2str t = "c + 1 / EI * (L * q_0 / 4 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)"
-then () else raise error "integrate.sml 3rd integration in 7.27, integration";
+then () else error "integrate.sml 3rd integration in 7.27, integration";
 "----------- check probem type --------------------------";
 "----------- check probem type --------------------------";
 "----------- check probem type --------------------------";
 val chkmodel = ((map (the o (parse thy))) o ppc2list) model;
 val t1 = (term_of o hd) chkmodel;
 val t2 = (term_of o hd o tl) chkmodel;
 val t3 = (term_of o hd o tl o tl) chkmodel;
 case t3 of Const ("Integrate.antiDerivative", _) $ _ => ()
-	 | _ => raise error "integrate.sml: Integrate.antiDerivative ???";
+	 | _ => error "integrate.sml: Integrate.antiDerivative ???";
 val model = {Given =["functionTerm f_f", "integrateBy v_v"],
 	     Where =[],
 	     Find  =["antiDerivativeName F_"],
 	     With  =[],
 val chkmodel = ((map (the o (parse thy))) o ppc2list) model;
 val t1 = (term_of o hd) chkmodel;
 val t2 = (term_of o hd o tl) chkmodel;
 val t3 = (term_of o hd o tl o tl) chkmodel;
 case t3 of Const ("Integrate.antiDerivativeName", _) $ _ => ()
-	 | _ => raise error "integrate.sml: Integrate.antiDerivativeName";
+	 | _ => error "integrate.sml: Integrate.antiDerivativeName";
 "----- compare 'Find's from problem, script, formalization -------";
 val {ppc,...} = get_pbt ["named","integrate","function"];
 val ("#Find", (Const ("Integrate.antiDerivativeName", _),
 	       F1_ as Free ("F_", F1_type))) = last_elem ppc;
 val {scr = Script sc,... } = get_met ["diff","integration","named"];
 val [_,_, F2_] = formal_args sc;
-if F1_ = F2_ then () else raise error "integrate.sml: unequal find's";
+if F1_ = F2_ then () else error "integrate.sml: unequal find's";
 val ((dsc as Const ("Integrate.antiDerivativeName", _))
 	 $ Free ("ff", F3_type)) = str2term "antiDerivativeName ff";
-if is_dsc dsc then () else raise error "integrate.sml: no description";
+if is_dsc dsc then () else error "integrate.sml: no description";
 if F1_type = F3_type then ()
-else raise error "integrate.sml: unequal types in find's";
+else error "integrate.sml: unequal types in find's";
 show_ptyps();
 val pbl = get_pbt ["integrate","function"];
 case #cas pbl of SOME (Const ("Integrate.Integrate",_) $ _) => ()
-	 | _ => raise error "integrate.sml: Integrate.Integrate ???";
+	 | _ => error "integrate.sml: Integrate.Integrate ???";
 "----------- check Scripts ------------------------------";
 "----------- check Scripts ------------------------------";
 "----------- check Scripts ------------------------------";
 val (p,_,f,nxt,_,pt) = me nxt p c pt(*nxt <- Apply_Method*);
 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
 if f2str f = "c + x + 1 / 3 * x ^^^ 3" then ()
-else raise error "integrate.sml: method [diff,integration]";
+else error "integrate.sml: method [diff,integration]";
 "----------- me method [diff,integration,named] ---------";
 "----------- me method [diff,integration,named] ---------";
 "----------- me method [diff,integration,named] ---------";
 val (p,_,f,nxt,_,pt) = me nxt p c pt(*nxt <- Apply_Method*);
 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
 if f2str f = "F x = c + x + 1 / 3 * x ^^^ 3" then()
-else raise error "integrate.sml: method [diff,integration,named]";
+else error "integrate.sml: method [diff,integration,named]";
 "----------- me met [diff,integration,named] Biegelinie.Q";
 "----------- me met [diff,integration,named] Biegelinie.Q";
 "----------- me met [diff,integration,named] Biegelinie.Q";
 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
 if f2str f = "Q x = c + -1 * q_0 * x" then()
-else raise error "integrate.sml: method [diff,integration,named] .Q";
+else error "integrate.sml: method [diff,integration,named] .Q";
 "----------- interSteps [diff,integration] --------------";
 "----------- interSteps [diff,integration] --------------";
 "----------- interSteps [diff,integration] --------------";
 val ((pt,p),_) = get_calc 1; show_pt pt;
 interSteps 1 ([1],Res);
 val ((pt,p),_) = get_calc 1; show_pt pt;
 if existpt' ([1,3], Res) pt then ()
-else raise error "integrate.sml: interSteps on Rewrite_Set_Inst 1";
+else error "integrate.sml: interSteps on Rewrite_Set_Inst 1";
 "----------- method analog to rls 'integration' ---------";
 "----------- method analog to rls 'integration' ---------";
 "----------- method analog to rls 'integration' ---------";
 autoCalculate 1 (Step 1);
 autoCalculate 1 CompleteCalc;
 val ((pt,p),_) = get_calc 1; show_pt pt;
 if existpt' ([3], Res) pt then ()
-else raise error  "integrate.sml: test-script doesnt work";
+else error  "integrate.sml: test-script doesnt work";
 "----------- Ambiguous input: Integral ?u + ?v D ?bdv = .";
 "----------- Ambiguous input: Integral ?u + ?v D ?bdv = .";
 "----------- Ambiguous input: Integral ?u + ?v D ?bdv = .";
 *** ((Integral (?u + ?v) D ?bdv) =
 ***  ((Integral ?u D ?bdv) + (Integral ?v D ?bdv)))
 *)
 if existpt' ([1,1,5], Res) pt then ()
-else raise error "integrate.sml: interSteps on Rewrite_Set_Inst 2";
+else error "integrate.sml: interSteps on Rewrite_Set_Inst 2";
 "----------- CAS input ----------------------------------";
 "----------- CAS input ----------------------------------";
 "----------- CAS input ----------------------------------";
 val t = str2term "Integrate (x^^^2 + x + 1, x)";
 case t of Const ("Integrate.Integrate", _) $ _ => ()
-	| _ => raise error "diff.sml behav.changed for Integrate (..., x)";
+	| _ => error "diff.sml behav.changed for Integrate (..., x)";
 atomty t;
 states:=[];
 CalcTree [([], ("e_domID", ["e_pblID"], ["e_metID"]))];
 Iterator 1;
 val ((pt,p),_) = get_calc 1;
 val Form res = (#1 o pt_extract) (pt, ([],Res));
 show_pt pt;
 (* WN070703 does not work like Diff due to error in next-pos
 if p = ([], Res) andalso term2str res = "5 * a" then ()
-else raise error "diff.sml behav.changed for Integrate (x^2 + x + 1, x)";
+else error "diff.sml behav.changed for Integrate (x^2 + x + 1, x)";
 *)
 ===== inhibit exn ============================================================*)

branch	isac-update-Isa09-2
changeset 38031	460c24a6a6ba
parent 38030	95d956108461
child 38048	377d9061ec3e