1.1 --- a/src/Tools/isac/calcelems.sml Thu Sep 23 08:54:26 2010 +0200
1.2 +++ b/src/Tools/isac/calcelems.sml Thu Sep 23 12:56:51 2010 +0200
1.3 @@ -601,7 +601,12 @@
1.4 fun termopt2str (SOME t) =
1.5 "SOME " ^ (Syntax.string_of_term (thy2ctxt' "Isac") t)
1.6 | termopt2str NONE = "NONE";
1.7 -fun term2str t = Syntax.string_of_term (thy2ctxt' "Isac") t;
1.8 +(*fun term2str t = Syntax.string_of_term (thy2ctxt' "Isac") t; Isa2002*)
1.9 +(*Florian1009: 'val' would ensure static lookup, i.e. only at compile time;
1.10 + however, dynamic lookup is required, since "Isac" is not yet built here.*)
1.11 +fun term2str t = Print_Mode.setmp [] (Syntax.string_of_term
1.12 +(ProofContext.init_global (Thy_Info.get_theory "Isac"))) t;
1.13 +
1.14 fun terms2str ts= (strs2str o (map (Syntax.string_of_term
1.15 (thy2ctxt' "Isac")))) ts;
1.16 fun type2str typ = Syntax.string_of_typ (thy2ctxt' "Isac") typ;
2.1 --- a/test/Tools/isac/Knowledge/integrate.sml Thu Sep 23 08:54:26 2010 +0200
2.2 +++ b/test/Tools/isac/Knowledge/integrate.sml Thu Sep 23 12:56:51 2010 +0200
2.3 @@ -8,35 +8,35 @@
2.4 *)
2.5 val thy = theory "Integrate";
2.6
2.7 -"-----------------------------------------------------------------";
2.8 -"table of contents -----------------------------------------------";
2.9 -"-----------------------------------------------------------------";
2.10 -"----------- parsing ---------------------------------------------";
2.11 -"----------- integrate by rewriting ------------------------------";
2.12 -"----------- test add_new_c, is_f_x ------------------------------";
2.13 -"----------- simplify by ruleset reducing make_ratpoly_in --------";
2.14 -"----------- simplify by ruleset extending make_polynomial_in ----";
2.15 -"----------- integrate by ruleset --------------------------------";
2.16 -"----------- rewrite 3rd integration in 7.27 ---------------------";
2.17 -"----------- check probem type -----------------------------------";
2.18 -"----------- check Scripts ---------------------------------------";
2.19 -"----------- me method [diff,integration] ------------------------";
2.20 -"----------- me method [diff,integration,named] ------------------";
2.21 -"----------- me method [diff,integration,named] Biegelinie.Q -----";
2.22 -"----------- interSteps [diff,integration] -----------------------";
2.23 -"----------- method analog to rls 'integration' ------------------";
2.24 -"----------- Ambiguous input: Integral ?u + ?v D ?bdv = ..--------";
2.25 -"----------- CAS input -------------------------------------------";
2.26 -"-----------------------------------------------------------------";
2.27 -"-----------------------------------------------------------------";
2.28 -"-----------------------------------------------------------------";
2.29 +"--------------------------------------------------------";
2.30 +"table of contents --------------------------------------";
2.31 +"--------------------------------------------------------";
2.32 +"----------- parsing ------------------------------------";
2.33 +"----------- integrate by rewriting ---------------------";
2.34 +"----------- test add_new_c, is_f_x ---------------------";
2.35 +"----------- simplify by ruleset reducing make_ratpoly_in";
2.36 +"----------- simplify by extending make_polynomial_in ---";
2.37 +"----------- integrate by ruleset -----------------------";
2.38 +"----------- rewrite 3rd integration in 7.27 ------------";
2.39 +"----------- check probem type --------------------------";
2.40 +"----------- check Scripts ------------------------------";
2.41 +"----------- me method [diff,integration] ---------------";
2.42 +"----------- me method [diff,integration,named] ---------";
2.43 +"----------- me met [diff,integration,named] Biegelinie.Q";
2.44 +"----------- interSteps [diff,integration] --------------";
2.45 +"----------- method analog to rls 'integration' ---------";
2.46 +"----------- Ambiguous input: Integral ?u + ?v D ?bdv = .";
2.47 +"----------- CAS input ----------------------------------";
2.48 +"--------------------------------------------------------";
2.49 +"--------------------------------------------------------";
2.50 +"--------------------------------------------------------";
2.51
2.52
2.53
2.54 -"----------- parsing ---------------------------------------------";
2.55 -"----------- parsing ---------------------------------------------";
2.56 -"----------- parsing ---------------------------------------------";
2.57 -fun str2term str = (term_of o the o (parse Integrate.thy)) str;
2.58 +"----------- parsing ------------------------------------";
2.59 +"----------- parsing ------------------------------------";
2.60 +"----------- parsing ------------------------------------";
2.61 +fun str2term str = (term_of o the o (parse thy)) str;
2.62 fun term2s t = Syntax.string_of_term (thy2ctxt' "Integrate") t;
2.63
2.64 val t = str2term "Integral x D x";
2.65 @@ -48,9 +48,9 @@
2.66 | _ => raise error "integrate.sml: parsing: ff x is_f_x";
2.67
2.68
2.69 -"----------- integrate by rewriting ------------------------------";
2.70 -"----------- integrate by rewriting ------------------------------";
2.71 -"----------- integrate by rewriting ------------------------------";
2.72 +"----------- integrate by rewriting ---------------------";
2.73 +"----------- integrate by rewriting ---------------------";
2.74 +"----------- integrate by rewriting ---------------------";
2.75 val conditions_in_integration_rules =
2.76 Rls {id="conditions_in_integration_rules",
2.77 preconds = [],
2.78 @@ -66,38 +66,50 @@
2.79 scr = EmptyScr};
2.80 val subs = [(str2term "bdv", str2term "x")];
2.81 fun rewrit thm str =
2.82 - fst (the (rewrite_inst_ Integrate.thy tless_true
2.83 + fst (the (rewrite_inst_ thy tless_true
2.84 conditions_in_integration_rules
2.85 true subs thm str));
2.86 -val str = rewrit integral_const (str2term "Integral 1 D x"); term2s str;
2.87 -val str = rewrit integral_const (str2term "Integral M'/EJ D x"); term2s str;
2.88 -val str = (rewrit integral_const (str2term "Integral x D x"))
2.89 +val str = rewrit @{thm "integral_const"} (str2term "Integral 1 D x");
2.90 +term2s str;
2.91 +val str = rewrit @{thm "integral_const"} (str2term "Integral M'/EJ D x");
2.92 +term2s str;
2.93 +val str = (rewrit @{thm "integral_const"} (str2term "Integral x D x"))
2.94 handle OPTION => str2term "no_rewrite";
2.95
2.96 -val str = rewrit integral_var (str2term "Integral x D x"); term2s str;
2.97 -val str = (rewrit integral_var (str2term "Integral a D x"))
2.98 +val str = rewrit @{thm "integral_var"} (str2term "Integral x D x");
2.99 +term2s str;
2.100 +val str = (rewrit @{thm "integral_var"} (str2term "Integral a D x"))
2.101 handle OPTION => str2term "no_rewrite";
2.102
2.103 -val str = rewrit integral_add (str2term "Integral x + 1 D x"); term2s str;
2.104 +val str = rewrit @{thm "integral_add"} (str2term "Integral x + 1 D x");
2.105 +term2s str;
2.106
2.107 -val str = rewrit integral_mult (str2term "Integral M'/EJ * x^^^3 D x");term2s str;
2.108 -val str = (rewrit integral_mult (str2term "Integral x * x D x"))
2.109 +val str = rewrit @{thm "integral_mult"} (str2term "Integral M'/EJ * x^^^3 D x");
2.110 +term2s str;
2.111 +val str = (rewrit @{thm "integral_mult"} (str2term "Integral x * x D x"))
2.112 handle OPTION => str2term "no_rewrite";
2.113
2.114 -val str = rewrit integral_pow (str2term "Integral x^^^3 D x"); term2s str;
2.115 +val str = rewrit @{thm "integral_pow"} (str2term "Integral x^^^3 D x");
2.116 +term2s str;
2.117
2.118
2.119 -"----------- test add_new_c, is_f_x ------------------------------";
2.120 -"----------- test add_new_c, is_f_x ------------------------------";
2.121 -"----------- test add_new_c, is_f_x ------------------------------";
2.122 +"----------- test add_new_c, is_f_x ---------------------";
2.123 +"----------- test add_new_c, is_f_x ---------------------";
2.124 +"----------- test add_new_c, is_f_x ---------------------";
2.125 val term = str2term "x^^^2*c + c_2";
2.126 val cc = new_c term;
2.127 if term2str cc = "c_3" then () else raise error "integrate.sml: new_c ???";
2.128
2.129 val SOME (id,t') = eval_add_new_c "" "Integrate.add'_new'_c" term thy;
2.130 +"####1###################################################";
2.131 +term2str t' = "x ^^^ 2 * c + c_2 = op + (x ^^^ 2 * c + c_2) c_3" --REDO "op +";
2.132 +"####2###################################################";
2.133 +
2.134 if term2str t' = "x ^^^ 2 * c + c_2 = x ^^^ 2 * c + c_2 + c_3" then ()
2.135 else raise error "intergrate.sml: diff. eval_add_new_c";
2.136
2.137 +"####3###################################################";
2.138 +
2.139 val cc = ("Integrate.add'_new'_c", eval_add_new_c "add_new_c_");
2.140 val SOME (thmstr, thm) = get_calculation1_ thy cc term;
2.141
2.142 @@ -151,7 +163,7 @@
2.143 ],
2.144 scr = EmptyScr};
2.145 fun rewrit thm t =
2.146 - fst (the (rewrite_inst_ Integrate.thy tless_true
2.147 + fst (the (rewrite_inst_ thy tless_true
2.148 conditions_in_integration true subs thm t));
2.149 val t = rewrit call_for_new_c (str2term "x ^^^ 2 / 2"); term2s t;
2.150 val t = (rewrit call_for_new_c t)
2.151 @@ -165,9 +177,9 @@
2.152 --------------------------------------------------------------------*)
2.153
2.154
2.155 -"----------- simplify by ruleset reducing make_ratpoly_in --------";
2.156 -"----------- simplify by ruleset reducing make_ratpoly_in --------";
2.157 -"----------- simplify by ruleset reducing make_ratpoly_in --------";
2.158 +"----------- simplify by ruleset reducing make_ratpoly_in";
2.159 +"----------- simplify by ruleset reducing make_ratpoly_in";
2.160 +"----------- simplify by ruleset reducing make_ratpoly_in";
2.161 val thy = Isac.thy;
2.162 val subs = [(str2term"bdv",str2term"x")];
2.163 val t = str2term "1/EI * (L * q_0 * x / 2 + -1 * q_0 * x^^^2 / 2)";
2.164 @@ -234,17 +246,17 @@
2.165
2.166
2.167
2.168 -"----------- simplify by ruleset extending make_polynomial_in ----";
2.169 -"----------- simplify by ruleset extending make_polynomial_in ----";
2.170 -"----------- simplify by ruleset extending make_polynomial_in ----";
2.171 +"----------- simplify by extending make_polynomial_in ---";
2.172 +"----------- simplify by extending make_polynomial_in ---";
2.173 +"----------- simplify by extending make_polynomial_in ---";
2.174 trace_rewrite:=true;
2.175 trace_rewrite:=false;
2.176 (*postponed: see *)
2.177
2.178
2.179 -"----------- integrate by ruleset --------------------------------";
2.180 -"----------- integrate by ruleset --------------------------------";
2.181 -"----------- integrate by ruleset --------------------------------";
2.182 +"----------- integrate by ruleset -----------------------";
2.183 +"----------- integrate by ruleset -----------------------";
2.184 +"----------- integrate by ruleset -----------------------";
2.185 val rls = "integration_rules";
2.186 val subs = [("bdv","x::real")];
2.187 fun rewrit_sinst subs rls str =
2.188 @@ -294,9 +306,9 @@
2.189 then () else raise error "integrate.sml: diff.behav. in integration #4";
2.190
2.191
2.192 -"----------- rewrite 3rd integration in 7.27 ---------------------";
2.193 -"----------- rewrite 3rd integration in 7.27 ---------------------";
2.194 -"----------- rewrite 3rd integration in 7.27 ---------------------";
2.195 +"----------- rewrite 3rd integration in 7.27 ------------";
2.196 +"----------- rewrite 3rd integration in 7.27 ------------";
2.197 +"----------- rewrite 3rd integration in 7.27 ------------";
2.198 val thy = Isac.thy (*because of Undeclared constant "Biegelinie.EI*);
2.199 val bdv = [(str2term"bdv", str2term"x")];
2.200 val t = str2term
2.201 @@ -311,15 +323,15 @@
2.202 then () else raise error "integrate.sml 3rd integration in 7.27, integration";
2.203
2.204
2.205 -"----------- check probem type -----------------------------------";
2.206 -"----------- check probem type -----------------------------------";
2.207 -"----------- check probem type -----------------------------------";
2.208 +"----------- check probem type --------------------------";
2.209 +"----------- check probem type --------------------------";
2.210 +"----------- check probem type --------------------------";
2.211 val model = {Given =["functionTerm f_f", "integrateBy v_v"],
2.212 Where =[],
2.213 Find =["antiDerivative F_"],
2.214 With =[],
2.215 Relate=[]}:string ppc;
2.216 -val chkmodel = ((map (the o (parse Integrate.thy))) o ppc2list) model;
2.217 +val chkmodel = ((map (the o (parse thy))) o ppc2list) model;
2.218 val t1 = (term_of o hd) chkmodel;
2.219 val t2 = (term_of o hd o tl) chkmodel;
2.220 val t3 = (term_of o hd o tl o tl) chkmodel;
2.221 @@ -331,7 +343,7 @@
2.222 Find =["antiDerivativeName F_"],
2.223 With =[],
2.224 Relate=[]}:string ppc;
2.225 -val chkmodel = ((map (the o (parse Integrate.thy))) o ppc2list) model;
2.226 +val chkmodel = ((map (the o (parse thy))) o ppc2list) model;
2.227 val t1 = (term_of o hd) chkmodel;
2.228 val t2 = (term_of o hd o tl) chkmodel;
2.229 val t3 = (term_of o hd o tl o tl) chkmodel;
2.230 @@ -358,9 +370,9 @@
2.231 | _ => raise error "integrate.sml: Integrate.Integrate ???";
2.232
2.233
2.234 -"----------- check Scripts ---------------------------------------";
2.235 -"----------- check Scripts ---------------------------------------";
2.236 -"----------- check Scripts ---------------------------------------";
2.237 +"----------- check Scripts ------------------------------";
2.238 +"----------- check Scripts ------------------------------";
2.239 +"----------- check Scripts ------------------------------";
2.240 val str =
2.241 "Script IntegrationScript (f_f::real) (v_v::real) = \
2.242 \ (let t_ = Take (Integral f_ D v_v) \
2.243 @@ -377,9 +389,9 @@
2.244 show_mets();
2.245
2.246
2.247 -"----------- me method [diff,integration] ---------------------";
2.248 -"----------- me method [diff,integration] ---------------------";
2.249 -"----------- me method [diff,integration] ---------------------";
2.250 +"----------- me method [diff,integration] ---------------";
2.251 +"----------- me method [diff,integration] ---------------";
2.252 +"----------- me method [diff,integration] ---------------";
2.253 (*exp_CalcInt_No-1.xml*)
2.254 val fmz = ["functionTerm (x^^^2 + 1)",
2.255 "integrateBy x","antiDerivative FF"];
2.256 @@ -402,9 +414,9 @@
2.257 else raise error "integrate.sml: method [diff,integration]";
2.258
2.259
2.260 -"----------- me method [diff,integration,named] ------------------";
2.261 -"----------- me method [diff,integration,named] ------------------";
2.262 -"----------- me method [diff,integration,named] ------------------";
2.263 +"----------- me method [diff,integration,named] ---------";
2.264 +"----------- me method [diff,integration,named] ---------";
2.265 +"----------- me method [diff,integration,named] ---------";
2.266 (*exp_CalcInt_No-2.xml*)
2.267 val fmz = ["functionTerm (x^^^2 + 1)",
2.268 "integrateBy x","antiDerivativeName F"];
2.269 @@ -427,9 +439,9 @@
2.270 else raise error "integrate.sml: method [diff,integration,named]";
2.271
2.272
2.273 -"----------- me method [diff,integration,named] Biegelinie.Q -----";
2.274 -"----------- me method [diff,integration,named] Biegelinie.Q -----";
2.275 -"----------- me method [diff,integration,named] Biegelinie.Q -----";
2.276 +"----------- me met [diff,integration,named] Biegelinie.Q";
2.277 +"----------- me met [diff,integration,named] Biegelinie.Q";
2.278 +"----------- me met [diff,integration,named] Biegelinie.Q";
2.279 (*exp_CalcInt_No-3.xml*)
2.280 val fmz = ["functionTerm (- q_0)",
2.281 "integrateBy x","antiDerivativeName Q"];
2.282 @@ -454,9 +466,9 @@
2.283 else raise error "integrate.sml: method [diff,integration,named] .Q";
2.284
2.285
2.286 -"----------- interSteps [diff,integration] -----------------------";
2.287 -"----------- interSteps [diff,integration] -----------------------";
2.288 -"----------- interSteps [diff,integration] -----------------------";
2.289 +"----------- interSteps [diff,integration] --------------";
2.290 +"----------- interSteps [diff,integration] --------------";
2.291 +"----------- interSteps [diff,integration] --------------";
2.292 states:=[];
2.293 CalcTree
2.294 [(["functionTerm (x^2 + 1)","integrateBy x","antiDerivative FF"],
2.295 @@ -473,11 +485,11 @@
2.296 else raise error "integrate.sml: interSteps on Rewrite_Set_Inst 1";
2.297
2.298
2.299 -"----------- method analog to rls 'integration' ------------------";
2.300 -"----------- method analog to rls 'integration' ------------------";
2.301 -"----------- method analog to rls 'integration' ------------------";
2.302 +"----------- method analog to rls 'integration' ---------";
2.303 +"----------- method analog to rls 'integration' ---------";
2.304 +"----------- method analog to rls 'integration' ---------";
2.305 store_met
2.306 - (prep_met Integrate.thy "met_testint" [] e_metID
2.307 + (prep_met thy "met_testint" [] e_metID
2.308 (["diff","integration","test"],
2.309 [("#Given" ,["functionTerm f_f", "integrateBy v_v"]),
2.310 ("#Find" ,["antiDerivative F_"])
2.311 @@ -521,9 +533,9 @@
2.312 else raise error "integrate.sml: test-script doesnt work";
2.313
2.314
2.315 -"----------- Ambiguous input: Integral ?u + ?v D ?bdv = ..--------";
2.316 -"----------- Ambiguous input: Integral ?u + ?v D ?bdv = ..--------";
2.317 -"----------- Ambiguous input: Integral ?u + ?v D ?bdv = ..--------";
2.318 +"----------- Ambiguous input: Integral ?u + ?v D ?bdv = .";
2.319 +"----------- Ambiguous input: Integral ?u + ?v D ?bdv = .";
2.320 +"----------- Ambiguous input: Integral ?u + ?v D ?bdv = .";
2.321 states:=[];
2.322 CalcTree
2.323 [(["functionTerm (x^2 + 1)","integrateBy x","antiDerivative FF"],
2.324 @@ -556,9 +568,10 @@
2.325 if existpt' ([1,1,5], Res) pt then ()
2.326 else raise error "integrate.sml: interSteps on Rewrite_Set_Inst 2";
2.327
2.328 -"----------- CAS input -------------------------------------------";
2.329 -"----------- CAS input -------------------------------------------";
2.330 -"----------- CAS input -------------------------------------------";
2.331 +
2.332 +"----------- CAS input ----------------------------------";
2.333 +"----------- CAS input ----------------------------------";
2.334 +"----------- CAS input ----------------------------------";
2.335 val t = str2term "Integrate (x^^^2 + x + 1, x)";
2.336 case t of Const ("Integrate.Integrate", _) $ _ => ()
2.337 | _ => raise error "diff.sml behav.changed for Integrate (..., x)";
3.1 --- a/test/Tools/isac/Test_Isac.thy Thu Sep 23 08:54:26 2010 +0200
3.2 +++ b/test/Tools/isac/Test_Isac.thy Thu Sep 23 12:56:51 2010 +0200
3.3 @@ -77,9 +77,20 @@
3.4 use"complex.sml";
3.5 use"diff.sml";
3.6 use"diffapp.sml";
3.7 -(**)
3.8 -use"Knowledge/integrate.sml";
3.9 -(**)
3.10 +*)
3.11 +ML {*print_depth 99*}
3.12 +
3.13 +ML {*
3.14 +fun term2str trm = Print_Mode.setmp (Print_Mode.input ::
3.15 + filter (curry (op =) Symbol.xsymbolsN) (print_mode_value ()))
3.16 + (Syntax.string_of_term @{context}) trm;
3.17 +val trm = str2term "a+b"; term2str trm;
3.18 +val trm = str2term "x ^^^ 2 * c + c_2 = x ^^^ 2 * c + c_2 + c_3"; term2str trm;
3.19 +"=========================================================";
3.20 +*}
3.21 +
3.22 +use "Knowledge/integrate.sml";
3.23 +(*
3.24 use"equation.sml";
3.25 (*use"inssort.sml"; problems with recdef in Isabelle2002*)
3.26 use"logexp.sml";
3.27 @@ -104,6 +115,9 @@
3.28 use"algein.sml";
3.29 cd "../..";
3.30 *)
3.31 +use_thy "../../Pure/Isar/Test_Parse_Term"
3.32 +use_thy "../../Pure/Isar/Test_Parsers"
3.33 +
3.34 ML{* writeln "**** run tests on IsacKnowledge complete ****************" *};
3.35 (*
3.36 val path = "/home/neuper/proto2/testsml2xml/";