1.1 --- a/test/Tools/isac/Frontend/interface.sml Mon Jul 18 16:42:26 2011 +0200
1.2 +++ b/test/Tools/isac/Frontend/interface.sml Mon Jul 18 17:21:21 2011 +0200
1.3 @@ -371,13 +371,13 @@
1.4
1.5 DEconstrCalcTree 1;
1.6
1.7 -(*========== inhibit exn 110620 ================================================
1.8 +
1.9 "--------- solve_linear as rootpbl AUTO CompleteCalc ----";
1.10 "--------- solve_linear as rootpbl AUTO CompleteCalc ----";
1.11 "--------- solve_linear as rootpbl AUTO CompleteCalc ----";
1.12 states:=[];
1.13 CalcTree
1.14 - [(["equality (1+-1*2+x=0)", "solveFor x","solutions L"],
1.15 + [(["equality (1+-1*2+x=(0::real))", "solveFor x","solutions L"],
1.16 ("Test",
1.17 ["linear","univariate","equation","test"],
1.18 ["Test","solve_linear"]))];
1.19 @@ -395,17 +395,19 @@
1.20 if term2str f = "[x = 1]" andalso p = ([], Res) then () else
1.21 error "FE-interface.sml: diff.behav. in solve_linear/rt AUTOCALCULATE ";
1.22
1.23 +
1.24 "--------- solve_linear as rootpbl AUTO CompleteHead/Calc ";
1.25 "--------- solve_linear as rootpbl AUTO CompleteHead/Calc ";
1.26 "--------- solve_linear as rootpbl AUTO CompleteHead/Calc ";
1.27 states:=[];
1.28 CalcTree
1.29 - [(["equality (1+-1*2+x=0)", "solveFor x","solutions L"],
1.30 + [(["equality (1+-1*2+x=(0::real)", "solveFor x","solutions L"],
1.31 ("Test",
1.32 ["linear","univariate","equation","test"],
1.33 ["Test","solve_linear"]))];
1.34 Iterator 1;
1.35 moveActiveRoot 1;
1.36 +(*========== inhibit exn 110718 ================================================
1.37 autoCalculate 1 CompleteCalcHead;
1.38 refFormula 1 (get_pos 1 1);
1.39 val ((pt,p),_) = get_calc 1;
1.40 @@ -414,7 +416,7 @@
1.41 val ((pt,p),_) = get_calc 1;
1.42 if p=([], Res) then () else
1.43 error "FE-interface.sml: diff.behav. in solve_linear AUTOC Head/Calc ";
1.44 -============ inhibit exn 110620 ==============================================*)
1.45 +============ inhibit exn 110718 ==============================================*)
1.46
1.47 "--------- mini-subpbl AUTOCALCULATE CompleteCalc -------";
1.48 "--------- mini-subpbl AUTOCALCULATE CompleteCalc -------";
1.49 @@ -426,15 +428,12 @@
1.50 Iterator 1;
1.51 moveActiveRoot 1;
1.52 autoCalculate 1 CompleteCalc;
1.53 -(*========== inhibit exn 110620 ================================================
1.54 val ((pt,p),_) = get_calc 1; show_pt pt;
1.55 - ERROR 110620 there is only 1 PblObj
1.56 (*
1.57 getTactic 1 ([1],Frm);
1.58 getTactic 1 ([1],Res);
1.59 initContext 1 Thy_ ([1],Res);
1.60 *)
1.61 -
1.62 (*... returns calcChangedEvent with*)
1.63 val (unc, del, gen) = (([],Pbl), ([],Pbl), ([],Res));
1.64 getFormulaeFromTo 1 unc gen 0 (*only result*) false;
1.65 @@ -446,7 +445,6 @@
1.66 val (Form f, tac, asms) = pt_extract (pt, p);
1.67 if term2str f = "[x = 1]" andalso p = ([], Res) then () else
1.68 error "FE-interface.sml: diff.behav. in mini-subpbl AUTOCALCULATE 6";
1.69 -============ inhibit exn 110620 ==============================================*)
1.70
1.71
1.72 "--------- mini-subpbl AUTO CompleteCalcHead ------------";
1.73 @@ -469,6 +467,7 @@
1.74 if length meth = 3 andalso length probl = 3 (*just some items tested*) then ()
1.75 else error "--- mini-subpbl AUTO CompleteCalcHead ---";
1.76
1.77 +
1.78 "--------- solve_linear as rootpbl AUTO CompleteModel ---";
1.79 "--------- solve_linear as rootpbl AUTO CompleteModel ---";
1.80 "--------- solve_linear as rootpbl AUTO CompleteModel ---";
1.81 @@ -480,11 +479,9 @@
1.82 ["Test","solve_linear"]))];
1.83 Iterator 1;
1.84 moveActiveRoot 1;
1.85 +(*========== inhibit exn 110718 ================================================
1.86 autoCalculate 1 CompleteModel;
1.87 -(*========== inhibit exn 110622 ================================================
1.88 refFormula 1 (get_pos 1 1);
1.89 - <ERROR> error in kernel </ERROR>
1.90 - get_pos: calc 1 not existent
1.91
1.92 setProblem 1 ["linear","univariate","equation","test"];
1.93 val pos = get_pos 1 1;
1.94 @@ -512,8 +509,7 @@
1.95 val (Form f, tac, asms) = pt_extract (pt, p);
1.96 if term2str f = "[x = 1]" andalso p = ([], Res) then () else
1.97 error "FE-interface.sml: diff.behav. in mini-subpbl AUTOCALCULATE 6";
1.98 -============ inhibit exn 110622 ==============================================*)
1.99 -
1.100 +============ inhibit exn 110718 ==============================================*)
1.101
1.102 "--------- setContext..Thy ------------------------------";
1.103 "--------- setContext..Thy ------------------------------";
1.104 @@ -1401,4 +1397,3 @@
1.105 error "FE-interface.sml: diff.behav. in FORMULA:replace} NOTok";
1.106 ============ inhibit exn 110628 ==============================================*)
1.107
1.108 -
2.1 --- a/test/Tools/isac/Test_Some.thy Mon Jul 18 16:42:26 2011 +0200
2.2 +++ b/test/Tools/isac/Test_Some.thy Mon Jul 18 17:21:21 2011 +0200
2.3 @@ -7,635 +7,20 @@
2.4
2.5 ML{* writeln "**** run the test ***************************************" *}
2.6
2.7 -use"../../../test/Tools/isac/Knowledge/integrate.sml"
2.8 +use"../../../test/Tools/isac/Frontend/interface.sml"
2.9
2.10 ML{*
2.11 -(* tests on integration over the reals
2.12 - author: Walther Neuper 2005
2.13 - (c) due to copyright terms
2.14 -*)
2.15 -"--------------------------------------------------------";
2.16 -"table of contents --------------------------------------";
2.17 -"--------------------------------------------------------";
2.18 -"----------- parsing ------------------------------------";
2.19 -"----------- integrate by rewriting ---------------------";
2.20 -"----------- test add_new_c, is_f_x ---------------------";
2.21 -"----------- simplify by ruleset reducing make_ratpoly_in";
2.22 -"----------- integrate by ruleset -----------------------";
2.23 -"----------- rewrite 3rd integration in 7.27 ------------";
2.24 -"----------- check probem type --------------------------";
2.25 -"----------- check Scripts ------------------------------";
2.26 -"----------- me method [diff,integration] ---------------";
2.27 -"----------- autoCalculate [diff,integration] -----------";
2.28 -"----------- me method [diff,integration,named] ---------";
2.29 -"----------- me met [diff,integration,named] Biegelinie.Q";
2.30 -"----------- interSteps [diff,integration] --------------";
2.31 -"----------- method analog to rls 'integration' ---------";
2.32 -"----------- Ambiguous input: Integral ?u + ?v D ?bdv = .";
2.33 -"----------- CAS input ----------------------------------";
2.34 -"--------------------------------------------------------";
2.35 -"--------------------------------------------------------";
2.36 -"--------------------------------------------------------";
2.37 +*}
2.38 +ML{*
2.39 +*}
2.40 +ML{*
2.41
2.42 -(*these val/fun provide for exact parsing in Integrate.thy, not Isac.thy;
2.43 -they are used several times below; TODO remove duplicates*)
2.44 -val thy = @{theory "Integrate"};
2.45 -val ctxt = thy2ctxt thy;
2.46 -
2.47 -fun str2t str = parseNEW ctxt str |> the;
2.48 -fun term2s t = Print_Mode.setmp [] (Syntax.string_of_term ctxt) t;
2.49 -
2.50 -val conditions_in_integration_rules =
2.51 - Rls {id="conditions_in_integration_rules",
2.52 - preconds = [],
2.53 - rew_ord = ("termlessI",termlessI),
2.54 - erls = Erls,
2.55 - srls = Erls, calc = [],
2.56 - rules = [(*for rewriting conditions in Thm's*)
2.57 - Calc ("Atools.occurs'_in",
2.58 - eval_occurs_in "#occurs_in_"),
2.59 - Thm ("not_true",num_str @{thm not_true}),
2.60 - Thm ("not_false",num_str @{thm not_false})],
2.61 - scr = EmptyScr};
2.62 -val subs = [(str2t "bdv", str2t "x")];
2.63 -fun rewrit thm str =
2.64 - fst (the (rewrite_inst_ thy tless_true
2.65 - conditions_in_integration_rules
2.66 - true subs thm str));
2.67 -
2.68 -
2.69 -"----------- parsing ------------------------------------";
2.70 -"----------- parsing ------------------------------------";
2.71 -"----------- parsing ------------------------------------";
2.72 -val t = str2t "Integral x D x";
2.73 -val t = str2t "Integral x^^^2 D x";
2.74 -case t of
2.75 - Const ("Integrate.Integral", _) $
2.76 - (Const ("Atools.pow", _) $ Free _ $ Free _) $ Free ("x", _) => ()
2.77 - | _ => error "integrate.sml: parsing: Integral x^^^2 D x";
2.78 -
2.79 -val t = str2t "ff x is_f_x";
2.80 -case t of Const ("Integrate.is'_f'_x", _) $ _ => ()
2.81 - | _ => error "integrate.sml: parsing: ff x is_f_x";
2.82 -
2.83 -
2.84 -"----------- integrate by rewriting ---------------------";
2.85 -"----------- integrate by rewriting ---------------------";
2.86 -"----------- integrate by rewriting ---------------------";
2.87 -(*========== inhibit exn 110628 ================================================
2.88 -val str = rewrit @{thm "integral_const"} (str2t "Integral 1 D x");
2.89 -if term2s str = "1 * x" then () else error "integrate.sml Integral 1 D x";
2.90 -
2.91 -val str = rewrit @{thm "integral_const"} (str2t "Integral M'/EJ D x");
2.92 -term2s str;
2.93 -val str = (rewrit @{thm "integral_const"} (str2t "Integral x D x"))
2.94 - handle OPTION => str2t "no_rewrite";
2.95 -
2.96 -val str = rewrit @{thm "integral_var"} (str2t "Integral x D x");
2.97 -term2s str;
2.98 -val str = (rewrit @{thm "integral_var"} (str2t "Integral a D x"))
2.99 - handle OPTION => str2t "no_rewrite";
2.100 -
2.101 -val str = rewrit @{thm "integral_add"} (str2t "Integral x + 1 D x");
2.102 -term2s str;
2.103 -
2.104 -val str = rewrit @{thm "integral_mult"} (str2t "Integral M'/EJ * x^^^3 D x");
2.105 -term2s str;
2.106 -val str = (rewrit @{thm "integral_mult"} (str2t "Integral x * x D x"))
2.107 - handle OPTION => str2t "no_rewrite";
2.108 -
2.109 -val str = rewrit @{thm "integral_pow"} (str2t "Integral x^^^3 D x");
2.110 -if term2s str = "x ^^^ (3 + 1) / (3 + 1)" then ()
2.111 -else error "integrate.sml Integral x^^^3 D x";
2.112 -============ inhibit exn 110628 ==============================================*)
2.113 -
2.114 -
2.115 -(*=== inhibit exn ?=============================================================
2.116 -"----------- test add_new_c, is_f_x ---------------------";
2.117 -"----------- test add_new_c, is_f_x ---------------------";
2.118 -"----------- test add_new_c, is_f_x ---------------------";
2.119 -val term = str2t "x^^^2 * c + c_2";
2.120 -val cc = new_c term;
2.121 -if term2str cc = "c_3" then () else error "integrate.sml: new_c ???";
2.122 -
2.123 -val SOME (id,t') = eval_add_new_c "" "Integrate.add'_new'_c" term thy;
2.124 -if term2str t' = "x ^^^ 2 * c + c_2 = x ^^^ 2 * c + c_2 + c_3" then ()
2.125 -else error "intergrate.sml: diff. eval_add_new_c";
2.126 -
2.127 -val cc = ("Integrate.add'_new'_c", eval_add_new_c "add_new_c_");
2.128 -val SOME (thmstr, thm) = get_calculation1_ thy cc term;
2.129 -
2.130 -val SOME (t',_) = rewrite_set_ thy true add_new_c term;
2.131 -if term2str t' = "x ^^^ 2 * c + c_2 + c_3" then ()
2.132 -else error "intergrate.sml: diff. rewrite_set add_new_c 1";
2.133 -
2.134 -val term = str2t "ff x = x^^^2*c + c_2";
2.135 -val SOME (t',_) = rewrite_set_ thy true add_new_c term;
2.136 -if term2str t' = "ff x = x ^^^ 2 * c + c_2 + c_3" then ()
2.137 -else error "intergrate.sml: diff. rewrite_set add_new_c 2";
2.138 -
2.139 -
2.140 -(*WN080222 replace call_new_c with add_new_c----------------------
2.141 -val term = str2t "new_c (c * x^^^2 + c_2)";
2.142 -val SOME (_,t') = eval_new_c 0 0 term 0;
2.143 -if term2s t' = "new_c c * x ^^^ 2 + c_2 = c_3" then ()
2.144 -else error "integrate.sml: eval_new_c ???";
2.145 -
2.146 -val t = str2t "matches (?u + new_c ?v) (x ^^^ 2 / 2)";
2.147 -val SOME (_,t') = eval_matches "" "Tools.matches" t thy; term2s t';
2.148 -if term2s t' = "matches (?u + new_c ?v) (x ^^^ 2 / 2) = False" then ()
2.149 -else error "integrate.sml: matches new_c = False";
2.150 -
2.151 -val t = str2t "matches (?u + new_c ?v) (x ^^^ 2 / 2 + new_c x ^^^ 2 / 2)";
2.152 -val SOME (_,t') = eval_matches "" "Tools.matches" t thy; term2s t';
2.153 -if term2s t'="matches (?u + new_c ?v) (x ^^^ 2 / 2 + new_c x ^^^ 2 / 2) = True"
2.154 -then () else error "integrate.sml: matches new_c = True";
2.155 -
2.156 -val t = str2t "ff x is_f_x";
2.157 -val SOME (_,t') = eval_is_f_x "" "" t thy; term2s t';
2.158 -if term2s t' = "(ff x is_f_x) = True" then ()
2.159 -else error "integrate.sml: eval_is_f_x --> true";
2.160 -
2.161 -val t = str2t "q_0/2 * L * x is_f_x";
2.162 -val SOME (_,t') = eval_is_f_x "" "" t thy; term2s t';
2.163 -if term2s t' = "(q_0 / 2 * L * x is_f_x) = False" then ()
2.164 -else error "integrate.sml: eval_is_f_x --> false";
2.165 -
2.166 -val conditions_in_integration =
2.167 -Rls {id="conditions_in_integration",
2.168 - preconds = [],
2.169 - rew_ord = ("termlessI",termlessI),
2.170 - erls = Erls,
2.171 - srls = Erls, calc = [],
2.172 - rules = [Calc ("Tools.matches",eval_matches ""),
2.173 - Calc ("Integrate.is'_f'_x",
2.174 - eval_is_f_x "is_f_x_"),
2.175 - Thm ("not_true",num_str @{thm not_true}),
2.176 - Thm ("not_false",num_str @{thm not_false})
2.177 - ],
2.178 - scr = EmptyScr};
2.179 -fun rewrit thm t =
2.180 - fst (the (rewrite_inst_ thy tless_true
2.181 - conditions_in_integration true subs thm t));
2.182 -val t = rewrit call_for_new_c (str2t "x ^^^ 2 / 2"); term2s t;
2.183 -val t = (rewrit call_for_new_c t)
2.184 - handle OPTION => str2t "no_rewrite";
2.185 -
2.186 -val t = rewrit call_for_new_c
2.187 - (str2t "ff x = q_0/2 *L*x"); term2s t;
2.188 -val t = (rewrit call_for_new_c
2.189 - (str2t "ff x = q_0 / 2 * L * x + new_c q_0 / 2 * L * x"))
2.190 - handle OPTION => (*NOT: + new_c ..=..!!*)str2t "no_rewrite";
2.191 ---------------------------------------------------------------------*)
2.192 -
2.193 -
2.194 -"----------- simplify by ruleset reducing make_ratpoly_in";
2.195 -"----------- simplify by ruleset reducing make_ratpoly_in";
2.196 -"----------- simplify by ruleset reducing make_ratpoly_in";
2.197 -val thy = @{theory "Isac"};
2.198 -"===== test 1";
2.199 -val subs = [(str2t "bdv", str2t "x")];
2.200 -val t = str2t "1/EI * (L * q_0 * x / 2 + -1 * q_0 * x^^^2 / 2)";
2.201 -
2.202 -"----- stepwise from the rulesets in simplify_Integral and below-----";
2.203 -val rls = norm_Rational_noadd_fractions;
2.204 -case rewrite_set_inst_ thy true subs rls t of
2.205 - SOME _ => error "integrate.sml simplify by ruleset norm_Rational_.#2"
2.206 - | NONE => ();
2.207 -
2.208 -"===== test 2";
2.209 -val rls = order_add_mult_in;
2.210 -val SOME (t,[]) = rewrite_set_ thy true rls t;
2.211 -if term2str t = "1 / EI * (L * (q_0 * x) / 2 + -1 * (q_0 * x ^^^ 2) / 2)" then()
2.212 -else error "integrate.sml simplify by ruleset order_add_mult_in #2";
2.213 -
2.214 -"===== test 3";
2.215 -val rls = discard_parentheses;
2.216 -val SOME (t,[]) = rewrite_set_ thy true rls t;
2.217 -if term2str t = "1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)" then ()
2.218 -else error "integrate.sml simplify by ruleset discard_parenth.. #3";
2.219 -
2.220 -"===== test 4";
2.221 -val rls =
2.222 - (append_rls "separate_bdv"
2.223 - collect_bdv
2.224 - [Thm ("separate_bdv", num_str @{thm separate_bdv}),
2.225 - (*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*)
2.226 - (*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*)
2.227 - Thm ("separate_bdv_n", num_str @{thm separate_bdv_n}),
2.228 - (*"?a * ?bdv ^^^ ?n / ?b = ?a / ?b * ?bdv ^^^ ?n"*)
2.229 - Thm ("separate_1_bdv", num_str @{thm separate_1_bdv}),
2.230 - (*"?bdv / ?b = (1 / ?b) * ?bdv"*)
2.231 - (*"?bdv / ?b = (1::?'a) / ?b * ?bdv"*)
2.232 - Thm ("separate_1_bdv_n", num_str @{thm separate_1_bdv_n})
2.233 - (*"?bdv ^^^ ?n / ?b = 1 / ?b * ?bdv ^^^ ?n"*)
2.234 - ]);
2.235 -(*show_types := true; --- do we need type-constraint in thms? *)
2.236 -@{thm separate_bdv}; (*::?'a does NOT rewrite here WITHOUT type constraint*)
2.237 -@{thm separate_bdv_n}; (*::real ..because of ^^^, rewrites*)
2.238 -@{thm separate_1_bdv}; (*::?'a*)
2.239 -val xxx = num_str @{thm separate_1_bdv}; (*::?'a*)
2.240 -@{thm separate_1_bdv_n}; (*::real ..because of ^^^*)
2.241 -(*show_types := false; --- do we need type-constraint in thms? YES ?!?!?!*)
2.242 -
2.243 -val SOME (t, []) = rewrite_set_inst_ thy true subs rls t;
2.244 -if term2str t = "1 / EI * (L * q_0 / 2 * x + -1 * q_0 / 2 * x ^^^ 2)" then ()
2.245 -else error "integrate.sml simplify by ruleset separate_bdv.. #4";
2.246 -
2.247 -"===== test 5";
2.248 -val t = str2t "1/EI * (L * q_0 * x / 2 + -1 * q_0 * x^^^2 / 2)";
2.249 -val rls = simplify_Integral;
2.250 -val SOME (t,[]) = rewrite_set_inst_ thy true subs rls t;
2.251 -(* given was: "1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x^^^2 / 2)" *)
2.252 -if term2str t = "1 / EI * (L * q_0 / 2 * x + -1 * q_0 / 2 * x ^^^ 2)" then ()
2.253 -else error "integrate.sml, simplify_Integral #99";
2.254 -
2.255 -
2.256 -"........... 2nd integral ........................................";
2.257 -"........... 2nd integral ........................................";
2.258 -"........... 2nd integral ........................................";
2.259 -val t = str2t
2.260 -"Integral 1 / EI * (L * q_0 / 2 * (x ^^^ 2 / 2) + -1 * q_0 / 2 * (x ^^^ 3 / 3)) D x";
2.261 -val rls = simplify_Integral;
2.262 -val SOME (t,[]) = rewrite_set_inst_ thy true subs rls t;
2.263 -if term2str t =
2.264 - "Integral 1 / EI * (L * q_0 / 4 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3) D x"
2.265 -then () else raise error "integrate.sml, simplify_Integral #198";
2.266 -
2.267 -val rls = integration_rules;
2.268 -val SOME (t,[]) = rewrite_set_ thy true rls t;
2.269 -term2str t;
2.270 -if term2str t =
2.271 - "1 / EI * (L * q_0 / 4 * (x ^^^ 3 / 3) + -1 * q_0 / 6 * (x ^^^ 4 / 4))"
2.272 -then () else error "integrate.sml, simplify_Integral #199";
2.273 -
2.274 -
2.275 -"----------- integrate by ruleset -----------------------";
2.276 -"----------- integrate by ruleset -----------------------";
2.277 -"----------- integrate by ruleset -----------------------";
2.278 -val rls = "integration_rules";
2.279 -val subs = [("bdv","x::real")];
2.280 -fun rewrit_sinst subs rls str =
2.281 - fst (the (rewrite_set_inst "Integrate" true subs rls str));
2.282 -(*~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
2.283 -val str = rewrit_sinst subs rls "Integral x D x";
2.284 -val str = rewrit_sinst subs rls "Integral c * x ^^^ 2 + c_2 D x";
2.285 -if str = "c * (x ^^^ 3 / 3) + c_2 * x"
2.286 -then () else error "integrate.sml: diff.behav. in integration_rules";
2.287 -
2.288 -val rls = "add_new_c";
2.289 -val str = rewrit_sinst subs rls "c * (x ^^^ 3 / 3) + c_2 * x";
2.290 -if str = "c * (x ^^^ 3 / 3) + c_2 * x + c_3" then ()
2.291 -else error "integrate.sml: diff.behav. in add_new_c simpl.";
2.292 -
2.293 -val str = rewrit_sinst subs rls "F x = x ^^^ 3 / 3 + x";
2.294 -if str = "F x = x ^^^ 3 / 3 + x + c"(*not "F x + c =..."*) then ()
2.295 -else error "integrate.sml: diff.behav. in add_new_c equation";
2.296 -
2.297 -val rls = "simplify_Integral";
2.298 -(*~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
2.299 -val str = "ff x = c * x + -1 * q_0 * (x ^^^ 2 / 2) + c_2";
2.300 -val str = rewrit_sinst subs rls str;
2.301 -if str = "ff x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2"
2.302 -then () else error "integrate.sml: diff.behav. in simplify_I #1";
2.303 -
2.304 -val rls = "integration";
2.305 -(*~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
2.306 -val str = rewrit_sinst subs rls "Integral c * x ^^^ 2 + c_2 D x";
2.307 -if str = "c_3 + c_2 * x + c / 3 * x ^^^ 3"
2.308 -then () else error "integrate.sml: diff.behav. in integration #1";
2.309 -
2.310 -val str = rewrit_sinst subs rls "Integral 3*x^^^2 + 2*x + 1 D x";
2.311 -if str = "c + x + x ^^^ 2 + x ^^^ 3" then ()
2.312 -else error "integrate.sml: diff.behav. in integration #2";
2.313 -
2.314 -val str = rewrit_sinst subs rls
2.315 -"Integral 1 / EI * (L * q_0 / 2 * x + -1 * q_0 / 2 * x ^^^ 2) D x";
2.316 -if str =
2.317 - "c + 1 / EI * (L * q_0 / 4 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)"
2.318 -then () else error "integrate.sml: diff.behav. in integration #3";
2.319 -
2.320 -val str = "Integral "^str^" D x";
2.321 -val str = rewrit_sinst subs rls str;
2.322 -if str =
2.323 - "c_2 + c * x + 1 / EI * (L * q_0 / 12 * x ^^^ 3 + -1 * q_0 / 24 * x ^^^ 4)"
2.324 -then () else error "integrate.sml: diff.behav. in integration #4";
2.325 -
2.326 -
2.327 -"----------- rewrite 3rd integration in 7.27 ------------";
2.328 -"----------- rewrite 3rd integration in 7.27 ------------";
2.329 -"----------- rewrite 3rd integration in 7.27 ------------";
2.330 -val thy = @{theory "Isac"} (*because of Undeclared constant "Biegelinie.EI*);
2.331 -val bdv = [(str2t"bdv", str2t"x")];
2.332 -val t = str2t
2.333 - "Integral 1 / EI * ((L * q_0 * x + -1 * q_0 * x ^^^ 2) / 2) D x";
2.334 -val SOME(t,_)= rewrite_set_inst_ thy true bdv simplify_Integral t;
2.335 -if term2str t =
2.336 - "Integral 1 / EI * (L * q_0 / 2 * x + -1 * q_0 / 2 * x ^^^ 2) D x"
2.337 -then () else error "integrate.sml 3rd integration in 7.27, simplify_Integral";
2.338 -
2.339 -val SOME(t,_)= rewrite_set_inst_ thy true bdv integration t;
2.340 -term2str t;
2.341 -if term2str t =
2.342 - "c + 1 / EI * (L * q_0 / 4 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)"
2.343 -then () else error "integrate.sml 3rd integration in 7.27, integration";
2.344 -
2.345 -
2.346 -"----------- check probem type --------------------------";
2.347 -"----------- check probem type --------------------------";
2.348 -"----------- check probem type --------------------------";
2.349 -val model = {Given =["functionTerm f_f", "integrateBy v_v"],
2.350 - Where =[],
2.351 - Find =["antiDerivative F_F"],
2.352 - With =[],
2.353 - Relate=[]}:string ppc;
2.354 -val chkmodel = ((map (the o (parse thy))) o ppc2list) model;
2.355 -val t1 = (term_of o hd) chkmodel;
2.356 -val t2 = (term_of o hd o tl) chkmodel;
2.357 -val t3 = (term_of o hd o tl o tl) chkmodel;
2.358 -case t3 of Const ("Integrate.antiDerivative", _) $ _ => ()
2.359 - | _ => error "integrate.sml: Integrate.antiDerivative ???";
2.360 -
2.361 -val model = {Given =["functionTerm f_f", "integrateBy v_v"],
2.362 - Where =[],
2.363 - Find =["antiDerivativeName F_F"],
2.364 - With =[],
2.365 - Relate=[]}:string ppc;
2.366 -val chkmodel = ((map (the o (parse thy))) o ppc2list) model;
2.367 -val t1 = (term_of o hd) chkmodel;
2.368 -val t2 = (term_of o hd o tl) chkmodel;
2.369 -val t3 = (term_of o hd o tl o tl) chkmodel;
2.370 -case t3 of Const ("Integrate.antiDerivativeName", _) $ _ => ()
2.371 - | _ => error "integrate.sml: Integrate.antiDerivativeName";
2.372 -
2.373 -"----- compare 'Find's from problem, script, formalization -------";
2.374 -val {ppc,...} = get_pbt ["named","integrate","function"];
2.375 -val ("#Find", (Const ("Integrate.antiDerivativeName", _),
2.376 - F1_ as Free ("F_F", F1_type))) = last_elem ppc;
2.377 -val {scr = Script sc,... } = get_met ["diff","integration","named"];
2.378 -val [_,_, F2_] = formal_args sc;
2.379 -if F1_ = F2_ then () else error "integrate.sml: unequal find's";
2.380 -
2.381 -val ((dsc as Const ("Integrate.antiDerivativeName", _))
2.382 - $ Free ("ff", F3_type)) = str2t "antiDerivativeName ff";
2.383 -if is_dsc dsc then () else error "integrate.sml: no description";
2.384 -if F1_type = F3_type then ()
2.385 -else error "integrate.sml: unequal types in find's";
2.386 -
2.387 -show_ptyps();
2.388 -val pbl = get_pbt ["integrate","function"];
2.389 -case #cas pbl of SOME (Const ("Integrate.Integrate",_) $ _) => ()
2.390 - | _ => error "integrate.sml: Integrate.Integrate ???";
2.391 -
2.392 -
2.393 -"----------- check Scripts ------------------------------";
2.394 -"----------- check Scripts ------------------------------";
2.395 -"----------- check Scripts ------------------------------";
2.396 -val str =
2.397 -"Script IntegrationScript (f_f::real) (v_v::real) = \
2.398 -\ (let t_t = Take (Integral f_f D v_v) \
2.399 -\ in (Rewrite_Set_Inst [(bdv,v_v)] integration False) (t_t::real))";
2.400 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
2.401 -atomty sc;
2.402 -
2.403 -val str =
2.404 -"Script NamedIntegrationScript (f_f::real) (v_v::real) (F_F::real=>real) = \
2.405 -\ (let t_t = Take (F_F v_v = Integral f_f D v_v) \
2.406 -\ in (Rewrite_Set_Inst [(bdv,v_v)] integration False) t_t)";
2.407 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
2.408 -atomty sc;
2.409 -show_mets();
2.410 -
2.411 -
2.412 -"----------- me method [diff,integration] ---------------";
2.413 -"----------- me method [diff,integration] ---------------";
2.414 -"----------- me method [diff,integration] ---------------";
2.415 -(*exp_CalcInt_No-1.xml*)
2.416 -val p = e_pos'; val c = [];
2.417 -"----- step 0: returns nxt = Model_Problem ---";
2.418 -val (p,_,f,nxt,_,pt) =
2.419 - CalcTreeTEST
2.420 - [(["functionTerm (x^^^2 + 1)", "integrateBy x", "antiDerivative FF"],
2.421 - ("Integrate", ["integrate","function"], ["diff","integration"]))];
2.422 -"----- step 1: returns nxt = Add_Given \"functionTerm (x ^^^ 2 + 1)\" ---";
2.423 -val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = ("Tac ", ...) --> Add_Given...*)
2.424 -"----- step 2: returns nxt = Add_Given \"integrateBy x\" ---";
2.425 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.426 -"----- step 3: returns nxt = Add_Find \"Integrate.antiDerivative FF\" ---";
2.427 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.428 -"----- step 4: returns nxt = Specify_Theory \"Integrate\" ---";
2.429 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.430 -"----- step 5: returns nxt = Specify_Problem [\"integrate\", \"function\"] ---";
2.431 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.432 -"----- step 6: returns nxt = Specify_Method [\"diff\", \"integration\"] ---";
2.433 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.434 -"----- step 7: returns nxt = Apply_Method [\"diff\", \"integration\"] ---";
2.435 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.436 -case nxt of (_, Apply_Method ["diff", "integration"]) => ()
2.437 - | _ => error "integrate.sml -- me method [diff,integration] -- spec";
2.438 -"----- step 8: returns nxt = Rewrite_Set_Inst ([\"(bdv, x)\"],\"integration\")";
2.439 -(*========== inhibit exn 110310 ================================================
2.440 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2.441 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2.442 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2.443 -if f2str f = "c + x + 1 / 3 * x ^^^ 3" then ()
2.444 -else error "integrate.sml -- me method [diff,integration] -- end";
2.445 -
2.446 -
2.447 -"----------- autoCalculate [diff,integration] -----------";
2.448 -"----------- autoCalculate [diff,integration] -----------";
2.449 -"----------- autoCalculate [diff,integration] -----------";
2.450 -states:=[];
2.451 -CalcTree
2.452 - [(["functionTerm (x^2 + 1)", "integrateBy x", "antiDerivative FF"],
2.453 - ("Integrate", ["integrate","function"], ["diff","integration"]))];
2.454 -Iterator 1;
2.455 -moveActiveRoot 1;
2.456 -autoCalculate 1 CompleteCalc;
2.457 -val ((pt,p),_) = get_calc 1; PolyML.makestring p; show_pt pt;
2.458 -val (Form t,_,_) = pt_extract (pt, p);
2.459 -if term2str t = "c + x + 1 / 3 * x ^^^ 3" then ()
2.460 -else error "integrate.sml -- interSteps [diff,integration] -- result";
2.461 -
2.462 -
2.463 -"----------- me method [diff,integration,named] ---------";
2.464 -"----------- me method [diff,integration,named] ---------";
2.465 -"----------- me method [diff,integration,named] ---------";
2.466 -(*exp_CalcInt_No-2.xml*)
2.467 -val fmz = ["functionTerm (x^^^2 + 1)",
2.468 - "integrateBy x","antiDerivativeName F"];
2.469 -val (dI',pI',mI') =
2.470 - ("Integrate",["named","integrate","function"],
2.471 - ["diff","integration","named"]);
2.472 -val p = e_pos'; val c = [];
2.473 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
2.474 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.475 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.476 -val (p,_,f,nxt,_,pt) = me nxt p c pt(*nxt <- Add_Find *);
2.477 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.478 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.479 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.480 -val (p,_,f,nxt,_,pt) = me nxt p c pt(*nxt <- Apply_Method*);
2.481 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.482 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.483 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2.484 -if f2str f = "F x = c + x + 1 / 3 * x ^^^ 3" then()
2.485 -else error "integrate.sml: method [diff,integration,named]";
2.486 -
2.487 -
2.488 -"----------- me met [diff,integration,named] Biegelinie.Q";
2.489 -"----------- me met [diff,integration,named] Biegelinie.Q";
2.490 -"----------- me met [diff,integration,named] Biegelinie.Q";
2.491 -(*exp_CalcInt_No-3.xml*)
2.492 -val fmz = ["functionTerm (- q_0)",
2.493 - "integrateBy x","antiDerivativeName Q"];
2.494 -val (dI',pI',mI') =
2.495 - ("Biegelinie",["named","integrate","function"],
2.496 - ["diff","integration","named"]);
2.497 -val p = e_pos'; val c = [];
2.498 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
2.499 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.500 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.501 -(*Error Tac Q not in ...*)
2.502 -val (p,_,f,nxt,_,pt) = me nxt p c pt(*nxt <- Add_Find *);
2.503 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.504 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.505 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.506 -val (p,_,f,nxt,_,pt) = me nxt p c pt(*nxt <- Apply_Method*);
2.507 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.508 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.509 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2.510 -
2.511 -if f2str f = "Q x = c + -1 * q_0 * x" then()
2.512 -else error "integrate.sml: method [diff,integration,named] .Q";
2.513 -
2.514 -
2.515 -"----------- interSteps [diff,integration] --------------";
2.516 -"----------- interSteps [diff,integration] --------------";
2.517 -"----------- interSteps [diff,integration] --------------";
2.518 -states:=[];
2.519 -CalcTree
2.520 - [(["functionTerm (x^2 + 1)", "integrateBy x", "antiDerivative FF"],
2.521 - ("Integrate", ["integrate","function"], ["diff","integration"]))];
2.522 -Iterator 1;
2.523 -moveActiveRoot 1;
2.524 -autoCalculate 1 CompleteCalc;
2.525 -interSteps 1 ([1],Res);
2.526 -val ((pt,p),_) = get_calc 1; show_pt pt;
2.527 -if existpt' ([1,3], Res) pt then ()
2.528 -else error "integrate.sml: interSteps on Rewrite_Set_Inst";
2.529 -
2.530 -
2.531 -"----------- method analog to rls 'integration' ---------";
2.532 -"----------- method analog to rls 'integration' ---------";
2.533 -"----------- method analog to rls 'integration' ---------";
2.534 -store_met
2.535 - (prep_met thy "met_testint" [] e_metID
2.536 - (["diff","integration","test"],
2.537 - [("#Given" ,["functionTerm f_f", "integrateBy v_v"]),
2.538 - ("#Find" ,["antiDerivative F_F"])
2.539 - ],
2.540 - {rew_ord'="tless_true", rls'=Atools_erls, calc = [],
2.541 - srls = e_rls,
2.542 - prls=e_rls,
2.543 - crls = Atools_erls, nrls = e_rls},
2.544 -"Script IntegrationScript (f_f::real) (v_v::real) = \
2.545 -\ (((Rewrite_Set_Inst [(bdv,v_v)] integration_rules False) @@ \
2.546 -\ (Rewrite_Set_Inst [(bdv,v_v)] add_new_c False) @@ \
2.547 -\ (Rewrite_Set_Inst [(bdv,v_v)] simplify_Integral False)) (f_f::real))"
2.548 -));
2.549 -
2.550 -states:=[];
2.551 -CalcTree
2.552 -[(["functionTerm (Integral x^2 + 1 D x)", "integrateBy x", "antiDerivative FF"],
2.553 - ("Integrate", ["integrate","function"], ["diff","integration","test"]))];
2.554 -Iterator 1;
2.555 -moveActiveRoot 1;
2.556 -autoCalculate 1 CompleteCalcHead;
2.557 -
2.558 -fetchProposedTactic 1 (*..Apply_Method*);
2.559 -autoCalculate 1 (Step 1);
2.560 -getTactic 1 ([1], Frm) (*still empty*);
2.561 -
2.562 -fetchProposedTactic 1 (*Rewrite_Set_Inst integration_rules*);
2.563 -autoCalculate 1 (Step 1);
2.564 -
2.565 -fetchProposedTactic 1 (*Rewrite_Set_Inst add_new_c*);
2.566 -autoCalculate 1 (Step 1);
2.567 -
2.568 -fetchProposedTactic 1 (*Rewrite_Set_Inst simplify_Integral*);
2.569 -autoCalculate 1 (Step 1);
2.570 -
2.571 -autoCalculate 1 CompleteCalc;
2.572 -val ((pt,p),_) = get_calc 1; show_pt pt;
2.573 -val (Form t,_,_) = pt_extract (pt, p); term2str t;
2.574 -if existpt' ([3], Res) pt andalso term2str t = "c + x + 1 / 3 * x ^^^ 3" then ()
2.575 -else error "integrate.sml: test-script doesnt work";
2.576 -
2.577 -
2.578 -"----------- Ambiguous input: Integral ?u + ?v D ?bdv = .";
2.579 -"----------- Ambiguous input: Integral ?u + ?v D ?bdv = .";
2.580 -"----------- Ambiguous input: Integral ?u + ?v D ?bdv = .";
2.581 -states:=[];
2.582 -CalcTree
2.583 -[(["functionTerm (x^2 + 1)","integrateBy x","antiDerivative FF"],
2.584 - ("Integrate",["integrate","function"],
2.585 - ["diff","integration"]))];
2.586 -Iterator 1;
2.587 -moveActiveRoot 1;
2.588 -autoCalculate 1 CompleteCalc;
2.589 -val ((pt,p),_) = get_calc 1; show_pt pt;
2.590 -
2.591 -interSteps 1 ([1],Res);
2.592 -val ((pt,p),_) = get_calc 1; show_pt pt;
2.593 -interSteps 1 ([1,1],Res);
2.594 -val ((pt,p),_) = get_calc 1; show_pt pt;
2.595 -getTactic 1 ([1,1,1],Frm);
2.596 -
2.597 -val str = (unenclose o string_of_thm) @{thm integral_add};
2.598 -writeln str;
2.599 -(*
2.600 -read_cterm (sign_of thy) (str,(TVar(("DUMMY",0),[])));
2.601 -
2.602 -*** More than one term is type correct:
2.603 -*** ((Integral (?u + ?v) D ?bdv) =
2.604 -*** (Integral ?u D (?bdv + (Integral ?v D ?bdv))))
2.605 - ###^^^###
2.606 -*** ((Integral (?u + ?v) D ?bdv) =
2.607 -*** ((Integral ?u D ?bdv) + (Integral ?v D ?bdv)))
2.608 -*)
2.609 -if existpt' ([1,1,5], Res) pt then ()
2.610 -else error "integrate.sml: interSteps on Rewrite_Set_Inst 2";
2.611 -
2.612 -
2.613 -"----------- CAS input ----------------------------------";
2.614 -"----------- CAS input ----------------------------------";
2.615 -"----------- CAS input ----------------------------------";
2.616 -val t = str2t "Integrate (x^^^2 + x + 1, x)";
2.617 -case t of Const ("Integrate.Integrate", _) $ _ => ()
2.618 - | _ => error "diff.sml behav.changed for Integrate (..., x)";
2.619 -atomty t;
2.620 -
2.621 -states:=[];
2.622 -CalcTree [([], ("e_domID", ["e_pblID"], ["e_metID"]))];
2.623 -Iterator 1;
2.624 -moveActiveRoot 1;
2.625 -replaceFormula 1 "Integrate (x^2 + x + 1, x)";
2.626 -autoCalculate 1 CompleteCalc;
2.627 -val ((pt,p),_) = get_calc 1;
2.628 -val Form res = (#1 o pt_extract) (pt, ([],Res));
2.629 -show_pt pt;
2.630 -(* WN070703 does not work like Diff due to error in next-pos
2.631 -if p = ([], Res) andalso term2str res = "5 * a" then ()
2.632 -else raise error "diff.sml behav.changed for Integrate (x^2 + x + 1, x)";
2.633 -
2.634 -WN101010 this test produced <SYSERROR>.."error in kernel" already in CVS-version
2.635 -from 2007; not touched since then.
2.636 -*)
2.637 -
2.638 -============ inhibit exn 110310 ==============================================*)
2.639 -===== inhibit exn ?===========================================================*)
2.640 -
2.641 +*}
2.642 +ML{*
2.643 +*}
2.644 +ML{*
2.645 +*}
2.646 +ML{*
2.647 *}
2.648
2.649 end
2.650 @@ -645,12 +30,8 @@
2.651 ===== inhibit exn ?===========================================================*)
2.652
2.653
2.654 -(*========== inhibit exn 110415 ================================================
2.655 -
2.656 -"########### testcode inserted vvv ###########################################";
2.657 -"########### testcode inserted ^^^ ###########################################";
2.658 -
2.659 -============ inhibit exn 110415 ==============================================*)
2.660 +(*========== inhibit exn 110718 ================================================
2.661 +============ inhibit exn 110718 ==============================================*)
2.662
2.663
2.664 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.