1.1 --- a/test/Tools/isac/Knowledge/polyminus.sml Mon Jul 18 09:50:15 2011 +0200
1.2 +++ b/test/Tools/isac/Knowledge/polyminus.sml Mon Jul 18 15:20:04 2011 +0200
1.3 @@ -37,7 +37,6 @@
1.4 "----------- fun eval_ist_monom ----------------------------------";
1.5 "----------- fun eval_ist_monom ----------------------------------";
1.6 ist_monom (str2term "12");
1.7 -(*========== inhibit exn =======================================================
1.8 case eval_ist_monom 0 0 (str2term "12 ist_monom") 0 of
1.9 SOME ("12 ist_monom = True", _) => ()
1.10 | _ => error "polyminus.sml: 12 ist_monom = True";
1.11 @@ -66,7 +65,6 @@
1.12 SOME ("3 * a * b ist_monom = True", _) => ()
1.13 | _ => error "polyminus.sml: 3*a*b ist_monom = True";
1.14
1.15 -============ inhibit exn =====================================================*)
1.16
1.17 "----------- watch order_add_mult -------------------------------";
1.18 "----------- watch order_add_mult -------------------------------";
1.19 @@ -303,13 +301,14 @@
1.20 moveActiveRoot 1;
1.21 autoCalculate 1 CompleteCalc;
1.22 val ((pt,p),_) = get_calc 1; show_pt pt;
1.23 -(*========== inhibit exn 110520 ================================================
1.24 -"??.empty" came with getting preconditions into ctxt:
1.25
1.26 +show_pt pt;
1.27 +p;
1.28 +(get_obj g_res pt (fst p));
1.29 +term2str (get_obj g_res pt (fst p));
1.30 if p = ([], Res) andalso
1.31 term2str (get_obj g_res pt (fst p)) = "3 + 3 * r + 6 * s - 8 * t"
1.32 then () else error "polyminus.sml: Vereinfache 140 d)";
1.33 -============ inhibit exn 110520 ==============================================*)
1.34
1.35
1.36 "----------- 139 c ---";
1.37 @@ -385,7 +384,6 @@
1.38 @@@@@WN081114 gives "??.empty", all "Pruefe" are the same,
1.39 although analogies work in interface.sml: FIXME.WN081114 in "Pruefe"*)
1.40 val ((pt,p),_) = get_calc 1;
1.41 -(*========== inhibit exn 110310 ================================================
1.42 if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) = "11 = 11"
1.43 then () else error "polyminus.sml: Probe 11 = 11";
1.44 show_pt pt;
1.45 @@ -665,4 +663,3 @@
1.46 (2, [1], "#Find", Const (...), [...])]
1.47 : ori list
1.48 *)
1.49 -============ inhibit exn 110310 ==============================================*)
2.1 --- a/test/Tools/isac/Test_Isac.thy Mon Jul 18 09:50:15 2011 +0200
2.2 +++ b/test/Tools/isac/Test_Isac.thy Mon Jul 18 15:20:04 2011 +0200
2.3 @@ -240,8 +240,8 @@
2.4 use "Knowledge/integrate.sml" (*part. was complete 2009-2
2.5 diff.emacs--jedit*)
2.6 (*use "Knowledge/eqsystem.sml" 2002*)
2.7 - use "Knowledge/test.sml" (*new 2011*)
2.8 - use "Knowledge/polyminus.sml" (*part.*)
2.9 + use "Knowledge/test.sml" (*complete*)
2.10 + use "Knowledge/polyminus.sml" (*complete*)
2.11 (*use "Knowledge/vect.sml" 2002*)
2.12 (*use "Knowledge/diffapp.sml" 2002*)
2.13 (*use "Knowledge/biegelinie.sml" 2002*)
3.1 --- a/test/Tools/isac/Test_Some.thy Mon Jul 18 09:50:15 2011 +0200
3.2 +++ b/test/Tools/isac/Test_Some.thy Mon Jul 18 15:20:04 2011 +0200
3.3 @@ -5,12 +5,638 @@
3.4
3.5 theory Test_Some imports Isac begin
3.6
3.7 -ML {*
3.8 -*}
3.9 -
3.10 ML{* writeln "**** run the test ***************************************" *}
3.11
3.12 -use"../../../test/Tools/isac/Interpret/script.sml"
3.13 +use"../../../test/Tools/isac/Knowledge/integrate.sml"
3.14 +
3.15 +ML{*
3.16 +(* tests on integration over the reals
3.17 + author: Walther Neuper 2005
3.18 + (c) due to copyright terms
3.19 +*)
3.20 +"--------------------------------------------------------";
3.21 +"table of contents --------------------------------------";
3.22 +"--------------------------------------------------------";
3.23 +"----------- parsing ------------------------------------";
3.24 +"----------- integrate by rewriting ---------------------";
3.25 +"----------- test add_new_c, is_f_x ---------------------";
3.26 +"----------- simplify by ruleset reducing make_ratpoly_in";
3.27 +"----------- integrate by ruleset -----------------------";
3.28 +"----------- rewrite 3rd integration in 7.27 ------------";
3.29 +"----------- check probem type --------------------------";
3.30 +"----------- check Scripts ------------------------------";
3.31 +"----------- me method [diff,integration] ---------------";
3.32 +"----------- autoCalculate [diff,integration] -----------";
3.33 +"----------- me method [diff,integration,named] ---------";
3.34 +"----------- me met [diff,integration,named] Biegelinie.Q";
3.35 +"----------- interSteps [diff,integration] --------------";
3.36 +"----------- method analog to rls 'integration' ---------";
3.37 +"----------- Ambiguous input: Integral ?u + ?v D ?bdv = .";
3.38 +"----------- CAS input ----------------------------------";
3.39 +"--------------------------------------------------------";
3.40 +"--------------------------------------------------------";
3.41 +"--------------------------------------------------------";
3.42 +
3.43 +(*these val/fun provide for exact parsing in Integrate.thy, not Isac.thy;
3.44 +they are used several times below; TODO remove duplicates*)
3.45 +val thy = @{theory "Integrate"};
3.46 +val ctxt = thy2ctxt thy;
3.47 +
3.48 +fun str2t str = parseNEW ctxt str |> the;
3.49 +fun term2s t = Print_Mode.setmp [] (Syntax.string_of_term ctxt) t;
3.50 +
3.51 +val conditions_in_integration_rules =
3.52 + Rls {id="conditions_in_integration_rules",
3.53 + preconds = [],
3.54 + rew_ord = ("termlessI",termlessI),
3.55 + erls = Erls,
3.56 + srls = Erls, calc = [],
3.57 + rules = [(*for rewriting conditions in Thm's*)
3.58 + Calc ("Atools.occurs'_in",
3.59 + eval_occurs_in "#occurs_in_"),
3.60 + Thm ("not_true",num_str @{thm not_true}),
3.61 + Thm ("not_false",num_str @{thm not_false})],
3.62 + scr = EmptyScr};
3.63 +val subs = [(str2t "bdv", str2t "x")];
3.64 +fun rewrit thm str =
3.65 + fst (the (rewrite_inst_ thy tless_true
3.66 + conditions_in_integration_rules
3.67 + true subs thm str));
3.68 +
3.69 +
3.70 +"----------- parsing ------------------------------------";
3.71 +"----------- parsing ------------------------------------";
3.72 +"----------- parsing ------------------------------------";
3.73 +val t = str2t "Integral x D x";
3.74 +val t = str2t "Integral x^^^2 D x";
3.75 +case t of
3.76 + Const ("Integrate.Integral", _) $
3.77 + (Const ("Atools.pow", _) $ Free _ $ Free _) $ Free ("x", _) => ()
3.78 + | _ => error "integrate.sml: parsing: Integral x^^^2 D x";
3.79 +
3.80 +val t = str2t "ff x is_f_x";
3.81 +case t of Const ("Integrate.is'_f'_x", _) $ _ => ()
3.82 + | _ => error "integrate.sml: parsing: ff x is_f_x";
3.83 +
3.84 +
3.85 +"----------- integrate by rewriting ---------------------";
3.86 +"----------- integrate by rewriting ---------------------";
3.87 +"----------- integrate by rewriting ---------------------";
3.88 +(*========== inhibit exn 110628 ================================================
3.89 +val str = rewrit @{thm "integral_const"} (str2t "Integral 1 D x");
3.90 +if term2s str = "1 * x" then () else error "integrate.sml Integral 1 D x";
3.91 +
3.92 +val str = rewrit @{thm "integral_const"} (str2t "Integral M'/EJ D x");
3.93 +term2s str;
3.94 +val str = (rewrit @{thm "integral_const"} (str2t "Integral x D x"))
3.95 + handle OPTION => str2t "no_rewrite";
3.96 +
3.97 +val str = rewrit @{thm "integral_var"} (str2t "Integral x D x");
3.98 +term2s str;
3.99 +val str = (rewrit @{thm "integral_var"} (str2t "Integral a D x"))
3.100 + handle OPTION => str2t "no_rewrite";
3.101 +
3.102 +val str = rewrit @{thm "integral_add"} (str2t "Integral x + 1 D x");
3.103 +term2s str;
3.104 +
3.105 +val str = rewrit @{thm "integral_mult"} (str2t "Integral M'/EJ * x^^^3 D x");
3.106 +term2s str;
3.107 +val str = (rewrit @{thm "integral_mult"} (str2t "Integral x * x D x"))
3.108 + handle OPTION => str2t "no_rewrite";
3.109 +
3.110 +val str = rewrit @{thm "integral_pow"} (str2t "Integral x^^^3 D x");
3.111 +if term2s str = "x ^^^ (3 + 1) / (3 + 1)" then ()
3.112 +else error "integrate.sml Integral x^^^3 D x";
3.113 +============ inhibit exn 110628 ==============================================*)
3.114 +
3.115 +
3.116 +(*=== inhibit exn ?=============================================================
3.117 +"----------- test add_new_c, is_f_x ---------------------";
3.118 +"----------- test add_new_c, is_f_x ---------------------";
3.119 +"----------- test add_new_c, is_f_x ---------------------";
3.120 +val term = str2t "x^^^2 * c + c_2";
3.121 +val cc = new_c term;
3.122 +if term2str cc = "c_3" then () else error "integrate.sml: new_c ???";
3.123 +
3.124 +val SOME (id,t') = eval_add_new_c "" "Integrate.add'_new'_c" term thy;
3.125 +if term2str t' = "x ^^^ 2 * c + c_2 = x ^^^ 2 * c + c_2 + c_3" then ()
3.126 +else error "intergrate.sml: diff. eval_add_new_c";
3.127 +
3.128 +val cc = ("Integrate.add'_new'_c", eval_add_new_c "add_new_c_");
3.129 +val SOME (thmstr, thm) = get_calculation1_ thy cc term;
3.130 +
3.131 +val SOME (t',_) = rewrite_set_ thy true add_new_c term;
3.132 +if term2str t' = "x ^^^ 2 * c + c_2 + c_3" then ()
3.133 +else error "intergrate.sml: diff. rewrite_set add_new_c 1";
3.134 +
3.135 +val term = str2t "ff x = x^^^2*c + c_2";
3.136 +val SOME (t',_) = rewrite_set_ thy true add_new_c term;
3.137 +if term2str t' = "ff x = x ^^^ 2 * c + c_2 + c_3" then ()
3.138 +else error "intergrate.sml: diff. rewrite_set add_new_c 2";
3.139 +
3.140 +
3.141 +(*WN080222 replace call_new_c with add_new_c----------------------
3.142 +val term = str2t "new_c (c * x^^^2 + c_2)";
3.143 +val SOME (_,t') = eval_new_c 0 0 term 0;
3.144 +if term2s t' = "new_c c * x ^^^ 2 + c_2 = c_3" then ()
3.145 +else error "integrate.sml: eval_new_c ???";
3.146 +
3.147 +val t = str2t "matches (?u + new_c ?v) (x ^^^ 2 / 2)";
3.148 +val SOME (_,t') = eval_matches "" "Tools.matches" t thy; term2s t';
3.149 +if term2s t' = "matches (?u + new_c ?v) (x ^^^ 2 / 2) = False" then ()
3.150 +else error "integrate.sml: matches new_c = False";
3.151 +
3.152 +val t = str2t "matches (?u + new_c ?v) (x ^^^ 2 / 2 + new_c x ^^^ 2 / 2)";
3.153 +val SOME (_,t') = eval_matches "" "Tools.matches" t thy; term2s t';
3.154 +if term2s t'="matches (?u + new_c ?v) (x ^^^ 2 / 2 + new_c x ^^^ 2 / 2) = True"
3.155 +then () else error "integrate.sml: matches new_c = True";
3.156 +
3.157 +val t = str2t "ff x is_f_x";
3.158 +val SOME (_,t') = eval_is_f_x "" "" t thy; term2s t';
3.159 +if term2s t' = "(ff x is_f_x) = True" then ()
3.160 +else error "integrate.sml: eval_is_f_x --> true";
3.161 +
3.162 +val t = str2t "q_0/2 * L * x is_f_x";
3.163 +val SOME (_,t') = eval_is_f_x "" "" t thy; term2s t';
3.164 +if term2s t' = "(q_0 / 2 * L * x is_f_x) = False" then ()
3.165 +else error "integrate.sml: eval_is_f_x --> false";
3.166 +
3.167 +val conditions_in_integration =
3.168 +Rls {id="conditions_in_integration",
3.169 + preconds = [],
3.170 + rew_ord = ("termlessI",termlessI),
3.171 + erls = Erls,
3.172 + srls = Erls, calc = [],
3.173 + rules = [Calc ("Tools.matches",eval_matches ""),
3.174 + Calc ("Integrate.is'_f'_x",
3.175 + eval_is_f_x "is_f_x_"),
3.176 + Thm ("not_true",num_str @{thm not_true}),
3.177 + Thm ("not_false",num_str @{thm not_false})
3.178 + ],
3.179 + scr = EmptyScr};
3.180 +fun rewrit thm t =
3.181 + fst (the (rewrite_inst_ thy tless_true
3.182 + conditions_in_integration true subs thm t));
3.183 +val t = rewrit call_for_new_c (str2t "x ^^^ 2 / 2"); term2s t;
3.184 +val t = (rewrit call_for_new_c t)
3.185 + handle OPTION => str2t "no_rewrite";
3.186 +
3.187 +val t = rewrit call_for_new_c
3.188 + (str2t "ff x = q_0/2 *L*x"); term2s t;
3.189 +val t = (rewrit call_for_new_c
3.190 + (str2t "ff x = q_0 / 2 * L * x + new_c q_0 / 2 * L * x"))
3.191 + handle OPTION => (*NOT: + new_c ..=..!!*)str2t "no_rewrite";
3.192 +--------------------------------------------------------------------*)
3.193 +
3.194 +
3.195 +"----------- simplify by ruleset reducing make_ratpoly_in";
3.196 +"----------- simplify by ruleset reducing make_ratpoly_in";
3.197 +"----------- simplify by ruleset reducing make_ratpoly_in";
3.198 +val thy = @{theory "Isac"};
3.199 +"===== test 1";
3.200 +val subs = [(str2t "bdv", str2t "x")];
3.201 +val t = str2t "1/EI * (L * q_0 * x / 2 + -1 * q_0 * x^^^2 / 2)";
3.202 +
3.203 +"----- stepwise from the rulesets in simplify_Integral and below-----";
3.204 +val rls = norm_Rational_noadd_fractions;
3.205 +case rewrite_set_inst_ thy true subs rls t of
3.206 + SOME _ => error "integrate.sml simplify by ruleset norm_Rational_.#2"
3.207 + | NONE => ();
3.208 +
3.209 +"===== test 2";
3.210 +val rls = order_add_mult_in;
3.211 +val SOME (t,[]) = rewrite_set_ thy true rls t;
3.212 +if term2str t = "1 / EI * (L * (q_0 * x) / 2 + -1 * (q_0 * x ^^^ 2) / 2)" then()
3.213 +else error "integrate.sml simplify by ruleset order_add_mult_in #2";
3.214 +
3.215 +"===== test 3";
3.216 +val rls = discard_parentheses;
3.217 +val SOME (t,[]) = rewrite_set_ thy true rls t;
3.218 +if term2str t = "1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)" then ()
3.219 +else error "integrate.sml simplify by ruleset discard_parenth.. #3";
3.220 +
3.221 +"===== test 4";
3.222 +val rls =
3.223 + (append_rls "separate_bdv"
3.224 + collect_bdv
3.225 + [Thm ("separate_bdv", num_str @{thm separate_bdv}),
3.226 + (*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*)
3.227 + (*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*)
3.228 + Thm ("separate_bdv_n", num_str @{thm separate_bdv_n}),
3.229 + (*"?a * ?bdv ^^^ ?n / ?b = ?a / ?b * ?bdv ^^^ ?n"*)
3.230 + Thm ("separate_1_bdv", num_str @{thm separate_1_bdv}),
3.231 + (*"?bdv / ?b = (1 / ?b) * ?bdv"*)
3.232 + (*"?bdv / ?b = (1::?'a) / ?b * ?bdv"*)
3.233 + Thm ("separate_1_bdv_n", num_str @{thm separate_1_bdv_n})
3.234 + (*"?bdv ^^^ ?n / ?b = 1 / ?b * ?bdv ^^^ ?n"*)
3.235 + ]);
3.236 +(*show_types := true; --- do we need type-constraint in thms? *)
3.237 +@{thm separate_bdv}; (*::?'a does NOT rewrite here WITHOUT type constraint*)
3.238 +@{thm separate_bdv_n}; (*::real ..because of ^^^, rewrites*)
3.239 +@{thm separate_1_bdv}; (*::?'a*)
3.240 +val xxx = num_str @{thm separate_1_bdv}; (*::?'a*)
3.241 +@{thm separate_1_bdv_n}; (*::real ..because of ^^^*)
3.242 +(*show_types := false; --- do we need type-constraint in thms? YES ?!?!?!*)
3.243 +
3.244 +val SOME (t, []) = rewrite_set_inst_ thy true subs rls t;
3.245 +if term2str t = "1 / EI * (L * q_0 / 2 * x + -1 * q_0 / 2 * x ^^^ 2)" then ()
3.246 +else error "integrate.sml simplify by ruleset separate_bdv.. #4";
3.247 +
3.248 +"===== test 5";
3.249 +val t = str2t "1/EI * (L * q_0 * x / 2 + -1 * q_0 * x^^^2 / 2)";
3.250 +val rls = simplify_Integral;
3.251 +val SOME (t,[]) = rewrite_set_inst_ thy true subs rls t;
3.252 +(* given was: "1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x^^^2 / 2)" *)
3.253 +if term2str t = "1 / EI * (L * q_0 / 2 * x + -1 * q_0 / 2 * x ^^^ 2)" then ()
3.254 +else error "integrate.sml, simplify_Integral #99";
3.255 +
3.256 +
3.257 +"........... 2nd integral ........................................";
3.258 +"........... 2nd integral ........................................";
3.259 +"........... 2nd integral ........................................";
3.260 +val t = str2t
3.261 +"Integral 1 / EI * (L * q_0 / 2 * (x ^^^ 2 / 2) + -1 * q_0 / 2 * (x ^^^ 3 / 3)) D x";
3.262 +val rls = simplify_Integral;
3.263 +val SOME (t,[]) = rewrite_set_inst_ thy true subs rls t;
3.264 +if term2str t =
3.265 + "Integral 1 / EI * (L * q_0 / 4 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3) D x"
3.266 +then () else raise error "integrate.sml, simplify_Integral #198";
3.267 +
3.268 +val rls = integration_rules;
3.269 +val SOME (t,[]) = rewrite_set_ thy true rls t;
3.270 +term2str t;
3.271 +if term2str t =
3.272 + "1 / EI * (L * q_0 / 4 * (x ^^^ 3 / 3) + -1 * q_0 / 6 * (x ^^^ 4 / 4))"
3.273 +then () else error "integrate.sml, simplify_Integral #199";
3.274 +
3.275 +
3.276 +"----------- integrate by ruleset -----------------------";
3.277 +"----------- integrate by ruleset -----------------------";
3.278 +"----------- integrate by ruleset -----------------------";
3.279 +val rls = "integration_rules";
3.280 +val subs = [("bdv","x::real")];
3.281 +fun rewrit_sinst subs rls str =
3.282 + fst (the (rewrite_set_inst "Integrate" true subs rls str));
3.283 +(*~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
3.284 +val str = rewrit_sinst subs rls "Integral x D x";
3.285 +val str = rewrit_sinst subs rls "Integral c * x ^^^ 2 + c_2 D x";
3.286 +if str = "c * (x ^^^ 3 / 3) + c_2 * x"
3.287 +then () else error "integrate.sml: diff.behav. in integration_rules";
3.288 +
3.289 +val rls = "add_new_c";
3.290 +val str = rewrit_sinst subs rls "c * (x ^^^ 3 / 3) + c_2 * x";
3.291 +if str = "c * (x ^^^ 3 / 3) + c_2 * x + c_3" then ()
3.292 +else error "integrate.sml: diff.behav. in add_new_c simpl.";
3.293 +
3.294 +val str = rewrit_sinst subs rls "F x = x ^^^ 3 / 3 + x";
3.295 +if str = "F x = x ^^^ 3 / 3 + x + c"(*not "F x + c =..."*) then ()
3.296 +else error "integrate.sml: diff.behav. in add_new_c equation";
3.297 +
3.298 +val rls = "simplify_Integral";
3.299 +(*~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
3.300 +val str = "ff x = c * x + -1 * q_0 * (x ^^^ 2 / 2) + c_2";
3.301 +val str = rewrit_sinst subs rls str;
3.302 +if str = "ff x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2"
3.303 +then () else error "integrate.sml: diff.behav. in simplify_I #1";
3.304 +
3.305 +val rls = "integration";
3.306 +(*~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
3.307 +val str = rewrit_sinst subs rls "Integral c * x ^^^ 2 + c_2 D x";
3.308 +if str = "c_3 + c_2 * x + c / 3 * x ^^^ 3"
3.309 +then () else error "integrate.sml: diff.behav. in integration #1";
3.310 +
3.311 +val str = rewrit_sinst subs rls "Integral 3*x^^^2 + 2*x + 1 D x";
3.312 +if str = "c + x + x ^^^ 2 + x ^^^ 3" then ()
3.313 +else error "integrate.sml: diff.behav. in integration #2";
3.314 +
3.315 +val str = rewrit_sinst subs rls
3.316 +"Integral 1 / EI * (L * q_0 / 2 * x + -1 * q_0 / 2 * x ^^^ 2) D x";
3.317 +if str =
3.318 + "c + 1 / EI * (L * q_0 / 4 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)"
3.319 +then () else error "integrate.sml: diff.behav. in integration #3";
3.320 +
3.321 +val str = "Integral "^str^" D x";
3.322 +val str = rewrit_sinst subs rls str;
3.323 +if str =
3.324 + "c_2 + c * x + 1 / EI * (L * q_0 / 12 * x ^^^ 3 + -1 * q_0 / 24 * x ^^^ 4)"
3.325 +then () else error "integrate.sml: diff.behav. in integration #4";
3.326 +
3.327 +
3.328 +"----------- rewrite 3rd integration in 7.27 ------------";
3.329 +"----------- rewrite 3rd integration in 7.27 ------------";
3.330 +"----------- rewrite 3rd integration in 7.27 ------------";
3.331 +val thy = @{theory "Isac"} (*because of Undeclared constant "Biegelinie.EI*);
3.332 +val bdv = [(str2t"bdv", str2t"x")];
3.333 +val t = str2t
3.334 + "Integral 1 / EI * ((L * q_0 * x + -1 * q_0 * x ^^^ 2) / 2) D x";
3.335 +val SOME(t,_)= rewrite_set_inst_ thy true bdv simplify_Integral t;
3.336 +if term2str t =
3.337 + "Integral 1 / EI * (L * q_0 / 2 * x + -1 * q_0 / 2 * x ^^^ 2) D x"
3.338 +then () else error "integrate.sml 3rd integration in 7.27, simplify_Integral";
3.339 +
3.340 +val SOME(t,_)= rewrite_set_inst_ thy true bdv integration t;
3.341 +term2str t;
3.342 +if term2str t =
3.343 + "c + 1 / EI * (L * q_0 / 4 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)"
3.344 +then () else error "integrate.sml 3rd integration in 7.27, integration";
3.345 +
3.346 +
3.347 +"----------- check probem type --------------------------";
3.348 +"----------- check probem type --------------------------";
3.349 +"----------- check probem type --------------------------";
3.350 +val model = {Given =["functionTerm f_f", "integrateBy v_v"],
3.351 + Where =[],
3.352 + Find =["antiDerivative F_F"],
3.353 + With =[],
3.354 + Relate=[]}:string ppc;
3.355 +val chkmodel = ((map (the o (parse thy))) o ppc2list) model;
3.356 +val t1 = (term_of o hd) chkmodel;
3.357 +val t2 = (term_of o hd o tl) chkmodel;
3.358 +val t3 = (term_of o hd o tl o tl) chkmodel;
3.359 +case t3 of Const ("Integrate.antiDerivative", _) $ _ => ()
3.360 + | _ => error "integrate.sml: Integrate.antiDerivative ???";
3.361 +
3.362 +val model = {Given =["functionTerm f_f", "integrateBy v_v"],
3.363 + Where =[],
3.364 + Find =["antiDerivativeName F_F"],
3.365 + With =[],
3.366 + Relate=[]}:string ppc;
3.367 +val chkmodel = ((map (the o (parse thy))) o ppc2list) model;
3.368 +val t1 = (term_of o hd) chkmodel;
3.369 +val t2 = (term_of o hd o tl) chkmodel;
3.370 +val t3 = (term_of o hd o tl o tl) chkmodel;
3.371 +case t3 of Const ("Integrate.antiDerivativeName", _) $ _ => ()
3.372 + | _ => error "integrate.sml: Integrate.antiDerivativeName";
3.373 +
3.374 +"----- compare 'Find's from problem, script, formalization -------";
3.375 +val {ppc,...} = get_pbt ["named","integrate","function"];
3.376 +val ("#Find", (Const ("Integrate.antiDerivativeName", _),
3.377 + F1_ as Free ("F_F", F1_type))) = last_elem ppc;
3.378 +val {scr = Script sc,... } = get_met ["diff","integration","named"];
3.379 +val [_,_, F2_] = formal_args sc;
3.380 +if F1_ = F2_ then () else error "integrate.sml: unequal find's";
3.381 +
3.382 +val ((dsc as Const ("Integrate.antiDerivativeName", _))
3.383 + $ Free ("ff", F3_type)) = str2t "antiDerivativeName ff";
3.384 +if is_dsc dsc then () else error "integrate.sml: no description";
3.385 +if F1_type = F3_type then ()
3.386 +else error "integrate.sml: unequal types in find's";
3.387 +
3.388 +show_ptyps();
3.389 +val pbl = get_pbt ["integrate","function"];
3.390 +case #cas pbl of SOME (Const ("Integrate.Integrate",_) $ _) => ()
3.391 + | _ => error "integrate.sml: Integrate.Integrate ???";
3.392 +
3.393 +
3.394 +"----------- check Scripts ------------------------------";
3.395 +"----------- check Scripts ------------------------------";
3.396 +"----------- check Scripts ------------------------------";
3.397 +val str =
3.398 +"Script IntegrationScript (f_f::real) (v_v::real) = \
3.399 +\ (let t_t = Take (Integral f_f D v_v) \
3.400 +\ in (Rewrite_Set_Inst [(bdv,v_v)] integration False) (t_t::real))";
3.401 +val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
3.402 +atomty sc;
3.403 +
3.404 +val str =
3.405 +"Script NamedIntegrationScript (f_f::real) (v_v::real) (F_F::real=>real) = \
3.406 +\ (let t_t = Take (F_F v_v = Integral f_f D v_v) \
3.407 +\ in (Rewrite_Set_Inst [(bdv,v_v)] integration False) t_t)";
3.408 +val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
3.409 +atomty sc;
3.410 +show_mets();
3.411 +
3.412 +
3.413 +"----------- me method [diff,integration] ---------------";
3.414 +"----------- me method [diff,integration] ---------------";
3.415 +"----------- me method [diff,integration] ---------------";
3.416 +(*exp_CalcInt_No-1.xml*)
3.417 +val p = e_pos'; val c = [];
3.418 +"----- step 0: returns nxt = Model_Problem ---";
3.419 +val (p,_,f,nxt,_,pt) =
3.420 + CalcTreeTEST
3.421 + [(["functionTerm (x^^^2 + 1)", "integrateBy x", "antiDerivative FF"],
3.422 + ("Integrate", ["integrate","function"], ["diff","integration"]))];
3.423 +"----- step 1: returns nxt = Add_Given \"functionTerm (x ^^^ 2 + 1)\" ---";
3.424 +val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = ("Tac ", ...) --> Add_Given...*)
3.425 +"----- step 2: returns nxt = Add_Given \"integrateBy x\" ---";
3.426 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.427 +"----- step 3: returns nxt = Add_Find \"Integrate.antiDerivative FF\" ---";
3.428 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.429 +"----- step 4: returns nxt = Specify_Theory \"Integrate\" ---";
3.430 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.431 +"----- step 5: returns nxt = Specify_Problem [\"integrate\", \"function\"] ---";
3.432 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.433 +"----- step 6: returns nxt = Specify_Method [\"diff\", \"integration\"] ---";
3.434 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.435 +"----- step 7: returns nxt = Apply_Method [\"diff\", \"integration\"] ---";
3.436 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.437 +case nxt of (_, Apply_Method ["diff", "integration"]) => ()
3.438 + | _ => error "integrate.sml -- me method [diff,integration] -- spec";
3.439 +"----- step 8: returns nxt = Rewrite_Set_Inst ([\"(bdv, x)\"],\"integration\")";
3.440 +(*========== inhibit exn 110310 ================================================
3.441 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3.442 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3.443 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3.444 +if f2str f = "c + x + 1 / 3 * x ^^^ 3" then ()
3.445 +else error "integrate.sml -- me method [diff,integration] -- end";
3.446 +
3.447 +
3.448 +"----------- autoCalculate [diff,integration] -----------";
3.449 +"----------- autoCalculate [diff,integration] -----------";
3.450 +"----------- autoCalculate [diff,integration] -----------";
3.451 +states:=[];
3.452 +CalcTree
3.453 + [(["functionTerm (x^2 + 1)", "integrateBy x", "antiDerivative FF"],
3.454 + ("Integrate", ["integrate","function"], ["diff","integration"]))];
3.455 +Iterator 1;
3.456 +moveActiveRoot 1;
3.457 +autoCalculate 1 CompleteCalc;
3.458 +val ((pt,p),_) = get_calc 1; PolyML.makestring p; show_pt pt;
3.459 +val (Form t,_,_) = pt_extract (pt, p);
3.460 +if term2str t = "c + x + 1 / 3 * x ^^^ 3" then ()
3.461 +else error "integrate.sml -- interSteps [diff,integration] -- result";
3.462 +
3.463 +
3.464 +"----------- me method [diff,integration,named] ---------";
3.465 +"----------- me method [diff,integration,named] ---------";
3.466 +"----------- me method [diff,integration,named] ---------";
3.467 +(*exp_CalcInt_No-2.xml*)
3.468 +val fmz = ["functionTerm (x^^^2 + 1)",
3.469 + "integrateBy x","antiDerivativeName F"];
3.470 +val (dI',pI',mI') =
3.471 + ("Integrate",["named","integrate","function"],
3.472 + ["diff","integration","named"]);
3.473 +val p = e_pos'; val c = [];
3.474 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
3.475 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.476 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.477 +val (p,_,f,nxt,_,pt) = me nxt p c pt(*nxt <- Add_Find *);
3.478 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.479 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.480 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.481 +val (p,_,f,nxt,_,pt) = me nxt p c pt(*nxt <- Apply_Method*);
3.482 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.483 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.484 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3.485 +if f2str f = "F x = c + x + 1 / 3 * x ^^^ 3" then()
3.486 +else error "integrate.sml: method [diff,integration,named]";
3.487 +
3.488 +
3.489 +"----------- me met [diff,integration,named] Biegelinie.Q";
3.490 +"----------- me met [diff,integration,named] Biegelinie.Q";
3.491 +"----------- me met [diff,integration,named] Biegelinie.Q";
3.492 +(*exp_CalcInt_No-3.xml*)
3.493 +val fmz = ["functionTerm (- q_0)",
3.494 + "integrateBy x","antiDerivativeName Q"];
3.495 +val (dI',pI',mI') =
3.496 + ("Biegelinie",["named","integrate","function"],
3.497 + ["diff","integration","named"]);
3.498 +val p = e_pos'; val c = [];
3.499 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
3.500 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.501 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.502 +(*Error Tac Q not in ...*)
3.503 +val (p,_,f,nxt,_,pt) = me nxt p c pt(*nxt <- Add_Find *);
3.504 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.505 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.506 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.507 +val (p,_,f,nxt,_,pt) = me nxt p c pt(*nxt <- Apply_Method*);
3.508 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.509 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.510 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3.511 +
3.512 +if f2str f = "Q x = c + -1 * q_0 * x" then()
3.513 +else error "integrate.sml: method [diff,integration,named] .Q";
3.514 +
3.515 +
3.516 +"----------- interSteps [diff,integration] --------------";
3.517 +"----------- interSteps [diff,integration] --------------";
3.518 +"----------- interSteps [diff,integration] --------------";
3.519 +states:=[];
3.520 +CalcTree
3.521 + [(["functionTerm (x^2 + 1)", "integrateBy x", "antiDerivative FF"],
3.522 + ("Integrate", ["integrate","function"], ["diff","integration"]))];
3.523 +Iterator 1;
3.524 +moveActiveRoot 1;
3.525 +autoCalculate 1 CompleteCalc;
3.526 +interSteps 1 ([1],Res);
3.527 +val ((pt,p),_) = get_calc 1; show_pt pt;
3.528 +if existpt' ([1,3], Res) pt then ()
3.529 +else error "integrate.sml: interSteps on Rewrite_Set_Inst";
3.530 +
3.531 +
3.532 +"----------- method analog to rls 'integration' ---------";
3.533 +"----------- method analog to rls 'integration' ---------";
3.534 +"----------- method analog to rls 'integration' ---------";
3.535 +store_met
3.536 + (prep_met thy "met_testint" [] e_metID
3.537 + (["diff","integration","test"],
3.538 + [("#Given" ,["functionTerm f_f", "integrateBy v_v"]),
3.539 + ("#Find" ,["antiDerivative F_F"])
3.540 + ],
3.541 + {rew_ord'="tless_true", rls'=Atools_erls, calc = [],
3.542 + srls = e_rls,
3.543 + prls=e_rls,
3.544 + crls = Atools_erls, nrls = e_rls},
3.545 +"Script IntegrationScript (f_f::real) (v_v::real) = \
3.546 +\ (((Rewrite_Set_Inst [(bdv,v_v)] integration_rules False) @@ \
3.547 +\ (Rewrite_Set_Inst [(bdv,v_v)] add_new_c False) @@ \
3.548 +\ (Rewrite_Set_Inst [(bdv,v_v)] simplify_Integral False)) (f_f::real))"
3.549 +));
3.550 +
3.551 +states:=[];
3.552 +CalcTree
3.553 +[(["functionTerm (Integral x^2 + 1 D x)", "integrateBy x", "antiDerivative FF"],
3.554 + ("Integrate", ["integrate","function"], ["diff","integration","test"]))];
3.555 +Iterator 1;
3.556 +moveActiveRoot 1;
3.557 +autoCalculate 1 CompleteCalcHead;
3.558 +
3.559 +fetchProposedTactic 1 (*..Apply_Method*);
3.560 +autoCalculate 1 (Step 1);
3.561 +getTactic 1 ([1], Frm) (*still empty*);
3.562 +
3.563 +fetchProposedTactic 1 (*Rewrite_Set_Inst integration_rules*);
3.564 +autoCalculate 1 (Step 1);
3.565 +
3.566 +fetchProposedTactic 1 (*Rewrite_Set_Inst add_new_c*);
3.567 +autoCalculate 1 (Step 1);
3.568 +
3.569 +fetchProposedTactic 1 (*Rewrite_Set_Inst simplify_Integral*);
3.570 +autoCalculate 1 (Step 1);
3.571 +
3.572 +autoCalculate 1 CompleteCalc;
3.573 +val ((pt,p),_) = get_calc 1; show_pt pt;
3.574 +val (Form t,_,_) = pt_extract (pt, p); term2str t;
3.575 +if existpt' ([3], Res) pt andalso term2str t = "c + x + 1 / 3 * x ^^^ 3" then ()
3.576 +else error "integrate.sml: test-script doesnt work";
3.577 +
3.578 +
3.579 +"----------- Ambiguous input: Integral ?u + ?v D ?bdv = .";
3.580 +"----------- Ambiguous input: Integral ?u + ?v D ?bdv = .";
3.581 +"----------- Ambiguous input: Integral ?u + ?v D ?bdv = .";
3.582 +states:=[];
3.583 +CalcTree
3.584 +[(["functionTerm (x^2 + 1)","integrateBy x","antiDerivative FF"],
3.585 + ("Integrate",["integrate","function"],
3.586 + ["diff","integration"]))];
3.587 +Iterator 1;
3.588 +moveActiveRoot 1;
3.589 +autoCalculate 1 CompleteCalc;
3.590 +val ((pt,p),_) = get_calc 1; show_pt pt;
3.591 +
3.592 +interSteps 1 ([1],Res);
3.593 +val ((pt,p),_) = get_calc 1; show_pt pt;
3.594 +interSteps 1 ([1,1],Res);
3.595 +val ((pt,p),_) = get_calc 1; show_pt pt;
3.596 +getTactic 1 ([1,1,1],Frm);
3.597 +
3.598 +val str = (unenclose o string_of_thm) @{thm integral_add};
3.599 +writeln str;
3.600 +(*
3.601 +read_cterm (sign_of thy) (str,(TVar(("DUMMY",0),[])));
3.602 +
3.603 +*** More than one term is type correct:
3.604 +*** ((Integral (?u + ?v) D ?bdv) =
3.605 +*** (Integral ?u D (?bdv + (Integral ?v D ?bdv))))
3.606 + ###^^^###
3.607 +*** ((Integral (?u + ?v) D ?bdv) =
3.608 +*** ((Integral ?u D ?bdv) + (Integral ?v D ?bdv)))
3.609 +*)
3.610 +if existpt' ([1,1,5], Res) pt then ()
3.611 +else error "integrate.sml: interSteps on Rewrite_Set_Inst 2";
3.612 +
3.613 +
3.614 +"----------- CAS input ----------------------------------";
3.615 +"----------- CAS input ----------------------------------";
3.616 +"----------- CAS input ----------------------------------";
3.617 +val t = str2t "Integrate (x^^^2 + x + 1, x)";
3.618 +case t of Const ("Integrate.Integrate", _) $ _ => ()
3.619 + | _ => error "diff.sml behav.changed for Integrate (..., x)";
3.620 +atomty t;
3.621 +
3.622 +states:=[];
3.623 +CalcTree [([], ("e_domID", ["e_pblID"], ["e_metID"]))];
3.624 +Iterator 1;
3.625 +moveActiveRoot 1;
3.626 +replaceFormula 1 "Integrate (x^2 + x + 1, x)";
3.627 +autoCalculate 1 CompleteCalc;
3.628 +val ((pt,p),_) = get_calc 1;
3.629 +val Form res = (#1 o pt_extract) (pt, ([],Res));
3.630 +show_pt pt;
3.631 +(* WN070703 does not work like Diff due to error in next-pos
3.632 +if p = ([], Res) andalso term2str res = "5 * a" then ()
3.633 +else raise error "diff.sml behav.changed for Integrate (x^2 + x + 1, x)";
3.634 +
3.635 +WN101010 this test produced <SYSERROR>.."error in kernel" already in CVS-version
3.636 +from 2007; not touched since then.
3.637 +*)
3.638 +
3.639 +============ inhibit exn 110310 ==============================================*)
3.640 +===== inhibit exn ?===========================================================*)
3.641 +
3.642 +*}
3.643
3.644 end
3.645