1.1 --- a/test/Tools/isac/Frontend/interface.sml Fri Oct 14 14:34:10 2011 +0200
1.2 +++ b/test/Tools/isac/Frontend/interface.sml Fri Oct 14 16:12:50 2011 +0200
1.3 @@ -1,11 +1,11 @@
1.4 -(* tests the interface of isac's SML-kernel in accordance to
1.5 - java-tests/isac.bridge.
1.6 +(* Title: tests the interface of isac's SML-kernel in accordance to
1.7 + java-tests/isac.bridge.
1.8 + Author: Walther Neuper
1.9 + (c) copyright due to lincense terms.
1.10
1.11 WN050707 ... if true, the test ist marked with a \label referring
1.12 to the same UC in isac-docu.tex as the JUnit testcase.
1.13 -use"../smltest/FE-interface/interface.sml";
1.14 -use"interface.sml";
1.15 - *)
1.16 +*)
1.17
1.18 "--------------------------------------------------------";
1.19 "table of contents --------------------------------------";
2.1 --- a/test/Tools/isac/Frontend/messages.sml Fri Oct 14 14:34:10 2011 +0200
2.2 +++ b/test/Tools/isac/Frontend/messages.sml Fri Oct 14 16:12:50 2011 +0200
2.3 @@ -2,3 +2,12 @@
2.4 Author: Walther Neuper 110320
2.5 (c) copyright due to lincense terms.
2.6 *)
2.7 +
2.8 +"-----------------------------------------------------------------";
2.9 +"table of contents -----------------------------------------------";
2.10 +"-----------------------------------------------------------------";
2.11 +"----------- test TODO -------------------------------------------";
2.12 +"-----------------------------------------------------------------";
2.13 +"-----------------------------------------------------------------";
2.14 +"-----------------------------------------------------------------";
2.15 +
3.1 --- a/test/Tools/isac/Frontend/states.sml Fri Oct 14 14:34:10 2011 +0200
3.2 +++ b/test/Tools/isac/Frontend/states.sml Fri Oct 14 16:12:50 2011 +0200
3.3 @@ -2,3 +2,12 @@
3.4 Author: Walther Neuper 110320
3.5 (c) copyright due to lincense terms.
3.6 *)
3.7 +
3.8 +"-----------------------------------------------------------------";
3.9 +"table of contents -----------------------------------------------";
3.10 +"-----------------------------------------------------------------";
3.11 +"----------- test TODO -------------------------------------------";
3.12 +"-----------------------------------------------------------------";
3.13 +"-----------------------------------------------------------------";
3.14 +"-----------------------------------------------------------------";
3.15 +
4.1 --- a/test/Tools/isac/Interpret/generate.sml Fri Oct 14 14:34:10 2011 +0200
4.2 +++ b/test/Tools/isac/Interpret/generate.sml Fri Oct 14 16:12:50 2011 +0200
4.3 @@ -2,3 +2,12 @@
4.4 Author: Walther Neuper 110320
4.5 (c) copyright due to lincense terms.
4.6 *)
4.7 +
4.8 +"-----------------------------------------------------------------";
4.9 +"table of contents -----------------------------------------------";
4.10 +"-----------------------------------------------------------------";
4.11 +"----------- test TODO -------------------------------------------";
4.12 +"-----------------------------------------------------------------";
4.13 +"-----------------------------------------------------------------";
4.14 +"-----------------------------------------------------------------";
4.15 +
5.1 --- a/test/Tools/isac/Knowledge/calculus.sml Fri Oct 14 14:34:10 2011 +0200
5.2 +++ b/test/Tools/isac/Knowledge/calculus.sml Fri Oct 14 16:12:50 2011 +0200
5.3 @@ -2,3 +2,12 @@
5.4 Author: Walther Neuper 110320
5.5 (c) copyright due to lincense terms.
5.6 *)
5.7 +
5.8 +"-----------------------------------------------------------------";
5.9 +"table of contents -----------------------------------------------";
5.10 +"-----------------------------------------------------------------";
5.11 +"----------- test TODO -------------------------------------------";
5.12 +"-----------------------------------------------------------------";
5.13 +"-----------------------------------------------------------------";
5.14 +"-----------------------------------------------------------------";
5.15 +
6.1 --- a/test/Tools/isac/Knowledge/delete.sml Fri Oct 14 14:34:10 2011 +0200
6.2 +++ b/test/Tools/isac/Knowledge/delete.sml Fri Oct 14 16:12:50 2011 +0200
6.3 @@ -2,3 +2,12 @@
6.4 Author: Walther Neuper 110320
6.5 (c) copyright due to lincense terms.
6.6 *)
6.7 +
6.8 +"-----------------------------------------------------------------";
6.9 +"table of contents -----------------------------------------------";
6.10 +"-----------------------------------------------------------------";
6.11 +"----------- test TODO -------------------------------------------";
6.12 +"-----------------------------------------------------------------";
6.13 +"-----------------------------------------------------------------";
6.14 +"-----------------------------------------------------------------";
6.15 +
7.1 --- a/test/Tools/isac/Knowledge/descript.sml Fri Oct 14 14:34:10 2011 +0200
7.2 +++ b/test/Tools/isac/Knowledge/descript.sml Fri Oct 14 16:12:50 2011 +0200
7.3 @@ -2,3 +2,12 @@
7.4 Author: Walther Neuper 110320
7.5 (c) copyright due to lincense terms.
7.6 *)
7.7 +
7.8 +"-----------------------------------------------------------------";
7.9 +"table of contents -----------------------------------------------";
7.10 +"-----------------------------------------------------------------";
7.11 +"----------- test TODO -------------------------------------------";
7.12 +"-----------------------------------------------------------------";
7.13 +"-----------------------------------------------------------------";
7.14 +"-----------------------------------------------------------------";
7.15 +
8.1 --- a/test/Tools/isac/Knowledge/integrate.sml Fri Oct 14 14:34:10 2011 +0200
8.2 +++ b/test/Tools/isac/Knowledge/integrate.sml Fri Oct 14 16:12:50 2011 +0200
8.3 @@ -45,7 +45,7 @@
8.4 Thm ("not_true",num_str @{thm not_true}),
8.5 Thm ("not_false",num_str @{thm not_false})],
8.6 scr = EmptyScr};
8.7 -val subs = [(str2t "bdv", str2t "x")];
8.8 +val subs = [(str2t "bdv::real", str2t "x::real")];
8.9 fun rewrit thm str =
8.10 fst (the (rewrite_inst_ thy tless_true
8.11 conditions_in_integration_rules
8.12 @@ -70,35 +70,30 @@
8.13 "----------- integrate by rewriting ---------------------";
8.14 "----------- integrate by rewriting ---------------------";
8.15 "----------- integrate by rewriting ---------------------";
8.16 -(*========== inhibit exn 110628 ================================================
8.17 val str = rewrit @{thm "integral_const"} (str2t "Integral 1 D x");
8.18 if term2s str = "1 * x" then () else error "integrate.sml Integral 1 D x";
8.19
8.20 val str = rewrit @{thm "integral_const"} (str2t "Integral M'/EJ D x");
8.21 -term2s str;
8.22 -val str = (rewrit @{thm "integral_const"} (str2t "Integral x D x"))
8.23 - handle OPTION => str2t "no_rewrite";
8.24 +if term2s str = "M' / EJ * x" then ()
8.25 +else error "Integral M'/EJ D x BY integral_const";
8.26
8.27 val str = rewrit @{thm "integral_var"} (str2t "Integral x D x");
8.28 -term2s str;
8.29 -val str = (rewrit @{thm "integral_var"} (str2t "Integral a D x"))
8.30 - handle OPTION => str2t "no_rewrite";
8.31 +if term2s str = "x ^^^ 2 / 2" then ()
8.32 +else error "Integral x D x BY integral_var";
8.33
8.34 val str = rewrit @{thm "integral_add"} (str2t "Integral x + 1 D x");
8.35 -term2s str;
8.36 +if term2s str = "Integral x D x + Integral 1 D x" then ()
8.37 +else error "Integral x + 1 D x BY integral_add";
8.38
8.39 val str = rewrit @{thm "integral_mult"} (str2t "Integral M'/EJ * x^^^3 D x");
8.40 -term2s str;
8.41 -val str = (rewrit @{thm "integral_mult"} (str2t "Integral x * x D x"))
8.42 - handle OPTION => str2t "no_rewrite";
8.43 +if term2s str = "M' / EJ * Integral x ^^^ 3 D x" then ()
8.44 +else error "Integral M'/EJ * x^^^3 D x BY integral_mult";
8.45
8.46 val str = rewrit @{thm "integral_pow"} (str2t "Integral x^^^3 D x");
8.47 if term2s str = "x ^^^ (3 + 1) / (3 + 1)" then ()
8.48 else error "integrate.sml Integral x^^^3 D x";
8.49 -============ inhibit exn 110628 ==============================================*)
8.50
8.51
8.52 -(*=== inhibit exn ?=============================================================
8.53 "----------- test add_new_c, is_f_x ---------------------";
8.54 "----------- test add_new_c, is_f_x ---------------------";
8.55 "----------- test add_new_c, is_f_x ---------------------";
8.56 @@ -205,19 +200,16 @@
8.57
8.58 "===== test 4";
8.59 val rls =
8.60 - (append_rls "separate_bdv"
8.61 - collect_bdv
8.62 - [Thm ("separate_bdv", num_str @{thm separate_bdv}),
8.63 - (*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*)
8.64 - (*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*)
8.65 - Thm ("separate_bdv_n", num_str @{thm separate_bdv_n}),
8.66 - (*"?a * ?bdv ^^^ ?n / ?b = ?a / ?b * ?bdv ^^^ ?n"*)
8.67 + (append_rls "separate_bdv" collect_bdv
8.68 + [Thm ("separate_bdv", num_str @{thm separate_bdv}),
8.69 + (*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*)
8.70 + Thm ("separate_bdv_n", num_str @{thm separate_bdv_n}),
8.71 + (*"?a * ?bdv ^^^ ?n / ?b = ?a / ?b * ?bdv ^^^ ?n"*)
8.72 Thm ("separate_1_bdv", num_str @{thm separate_1_bdv}),
8.73 - (*"?bdv / ?b = (1 / ?b) * ?bdv"*)
8.74 - (*"?bdv / ?b = (1::?'a) / ?b * ?bdv"*)
8.75 + (*"?bdv / ?b = (1 / ?b) * ?bdv"*)
8.76 Thm ("separate_1_bdv_n", num_str @{thm separate_1_bdv_n})
8.77 - (*"?bdv ^^^ ?n / ?b = 1 / ?b * ?bdv ^^^ ?n"*)
8.78 - ]);
8.79 + (*"?bdv ^^^ ?n / ?b = 1 / ?b * ?bdv ^^^ ?n"*)
8.80 + ]);
8.81 (*show_types := true; --- do we need type-constraint in thms? *)
8.82 @{thm separate_bdv}; (*::?'a does NOT rewrite here WITHOUT type constraint*)
8.83 @{thm separate_bdv_n}; (*::real ..because of ^^^, rewrites*)
8.84 @@ -393,7 +385,6 @@
8.85 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
8.86 atomty sc;
8.87 show_mets();
8.88 -===== inhibit exn ?===========================================================*)
8.89
8.90
8.91 "----------- me method [diff,integration] ---------------";
9.1 --- a/test/Tools/isac/Knowledge/logexp.sml Fri Oct 14 14:34:10 2011 +0200
9.2 +++ b/test/Tools/isac/Knowledge/logexp.sml Fri Oct 14 16:12:50 2011 +0200
9.3 @@ -1,7 +1,7 @@
9.4
9.5 -(* testexamples for LogExp, logarithms and exponential functions and terms
9.6 -
9.7 -use"../smltest/IsacKnowledge/logexp.sml";
9.8 +(* Title: test/../logexp.sml
9.9 + Author: Walther Neuper 110320
9.10 + (c) copyright due to lincense terms.
9.11 *)
9.12
9.13 "-----------------------------------------------------------------";
10.1 --- a/test/Tools/isac/Test_Isac.thy Fri Oct 14 14:34:10 2011 +0200
10.2 +++ b/test/Tools/isac/Test_Isac.thy Fri Oct 14 16:12:50 2011 +0200
10.3 @@ -124,7 +124,7 @@
10.4 use "Interpret/mstools.sml"
10.5 use "Interpret/ctree.sml" (*!...!see(25)*)
10.6 use "Interpret/ptyps.sml" (*part.*)
10.7 -(*use "Interpret/generate.sml" new 2011*)
10.8 + use "Interpret/generate.sml"
10.9 use "Interpret/calchead.sml" (*part.*)
10.10 use "Interpret/appl.sml" (*!complete WEGEN INTERMED TESTCODE*)
10.11 use "Interpret/rewtools.sml" (*! *)
10.12 @@ -141,14 +141,14 @@
10.13 use "xmlsrc/interface-xml.sml" (*TODO after 2009-2*)
10.14 ML {*"%%%%%%%%%%%%%%%%% end xmlsrc.thy %%%%%%%%%%%%%%%%%%%%%%%";*}
10.15 ML {*"%%%%%%%%%%%%%%%%% start Frontend.thy %%%%%%%%%%%%%%%%%%%";*}
10.16 - use "Frontend/messages.sml" (*new 2011*)
10.17 - use "Frontend/states.sml" (*new 2011*)
10.18 + use "Frontend/messages.sml"
10.19 + use "Frontend/states.sml"
10.20 use "Frontend/interface.sml"
10.21 - use "print_exn_G.sml" (*new 2011*)
10.22 + use "print_exn_G.sml"
10.23 ML {*"%%%%%%%%%%%%%%%%% end Frontend.thy %%%%%%%%%%%%%%%%%%%%%";*}
10.24 ML {*"%%%%%%%%%%%%%%%%% start Knowledge.thy %%%%%%%%%%%%%%%%%%";*}
10.25 - use "Knowledge/delete.sml" (*new 2011*)
10.26 - use "Knowledge/descript.sml" (*new 2011*)
10.27 + use "Knowledge/delete.sml"
10.28 + use "Knowledge/descript.sml"
10.29 (*use "Knowledge/atools.sml" 2002, added termorder.sml 2011*)
10.30 use "Knowledge/simplify.sml" (*part.*)
10.31 (*use "Knowledge/poly.sml" 2002*)
10.32 @@ -163,9 +163,9 @@
10.33 use "Knowledge/partial_fractions.sml"
10.34 use "Knowledge/polyeq.sml"
10.35 (*use "Knowledge/rlang.sml" 2002???*)
10.36 - use "Knowledge/calculus.sml" (*new 2011*)
10.37 + use "Knowledge/calculus.sml"
10.38 use "Knowledge/trig.sml"
10.39 - use "Knowledge/logexp.sml" (*part.*)
10.40 +(*use "Knowledge/logexp.sml" not included as stuff for presentation of authoring*)
10.41 use "Knowledge/diff.sml" (*part.*)
10.42 use "Knowledge/integrate.sml" (*part. was complete 2009-2
10.43 diff.emacs--jedit*)
11.1 --- a/test/Tools/isac/Test_Some.thy Fri Oct 14 14:34:10 2011 +0200
11.2 +++ b/test/Tools/isac/Test_Some.thy Fri Oct 14 16:12:50 2011 +0200
11.3 @@ -1,9 +1,114 @@
11.4
11.5 theory Test_Some imports Isac begin
11.6
11.7 -use"../../../test/Tools/isac/Knowledge/polyeq.sml"
11.8 +use"../../../test/Tools/isac/Knowledge/integrate.sml"
11.9
11.10 ML {* (*=================*)
11.11 +@{thm separate_1_bdv}
11.12 +*}
11.13 +ML{*
11.14 +val thy = @{theory "Integrate"};
11.15 +val ctxt = thy2ctxt thy;
11.16 +
11.17 +fun str2t str = parseNEW ctxt str |> the;
11.18 +fun term2s t = Print_Mode.setmp [] (Syntax.string_of_term ctxt) t;
11.19 +
11.20 +val conditions_in_integration_rules =
11.21 + Rls {id="conditions_in_integration_rules",
11.22 + preconds = [],
11.23 + rew_ord = ("termlessI",termlessI),
11.24 + erls = Erls,
11.25 + srls = Erls, calc = [],
11.26 + rules = [(*for rewriting conditions in Thm's*)
11.27 + Calc ("Atools.occurs'_in",
11.28 + eval_occurs_in "#occurs_in_"),
11.29 + Thm ("not_true",num_str @{thm not_true}),
11.30 + Thm ("not_false",num_str @{thm not_false})],
11.31 + scr = EmptyScr};
11.32 +val subs = [(str2t "bdv::real", str2t "x::real")];
11.33 +fun rewrit thm str =
11.34 + fst (the (rewrite_inst_ thy tless_true
11.35 + conditions_in_integration_rules
11.36 + true subs thm str));
11.37 +*}
11.38 +ML{* (*==================*)
11.39 +"----------- simplify by ruleset reducing make_ratpoly_in";
11.40 +val thy = @{theory "Isac"};
11.41 +"===== test 1";
11.42 +val subs = [(str2t "bdv", str2t "x")];
11.43 +val t = str2t "1/EI * (L * q_0 * x / 2 + -1 * q_0 * x^^^2 / 2)";
11.44 +
11.45 +"----- stepwise from the rulesets in simplify_Integral and below-----";
11.46 +val rls = norm_Rational_noadd_fractions;
11.47 +case rewrite_set_inst_ thy true subs rls t of
11.48 + SOME _ => error "integrate.sml simplify by ruleset norm_Rational_.#2"
11.49 + | NONE => ();
11.50 +
11.51 +"===== test 2";
11.52 +val rls = order_add_mult_in;
11.53 +val SOME (t,[]) = rewrite_set_ thy true rls t;
11.54 +if term2str t = "1 / EI * (L * (q_0 * x) / 2 + -1 * (q_0 * x ^^^ 2) / 2)" then()
11.55 +else error "integrate.sml simplify by ruleset order_add_mult_in #2";
11.56 +
11.57 +"===== test 3";
11.58 +val rls = discard_parentheses;
11.59 +val SOME (t,[]) = rewrite_set_ thy true rls t;
11.60 +if term2str t = "1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)" then ()
11.61 +else error "integrate.sml simplify by ruleset discard_parenth.. #3";
11.62 +
11.63 +"===== test 4";
11.64 +val rls =
11.65 + (append_rls "separate_bdv" collect_bdv
11.66 + [Thm ("separate_bdv", num_str @{thm separate_bdv}),
11.67 + (*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*)
11.68 + Thm ("separate_bdv_n", num_str @{thm separate_bdv_n}),
11.69 + (*"?a * ?bdv ^^^ ?n / ?b = ?a / ?b * ?bdv ^^^ ?n"*)
11.70 + Thm ("separate_1_bdv", num_str @{thm separate_1_bdv}),
11.71 + (*"?bdv / ?b = (1 / ?b) * ?bdv"*)
11.72 + Thm ("separate_1_bdv_n", num_str @{thm separate_1_bdv_n})
11.73 + (*"?bdv ^^^ ?n / ?b = 1 / ?b * ?bdv ^^^ ?n"*)
11.74 + ]);
11.75 +(*show_types := true; --- do we need type-constraint in thms? *)
11.76 +@{thm separate_bdv}; (*::?'a does NOT rewrite here WITHOUT type constraint*)
11.77 +@{thm separate_bdv_n}; (*::real ..because of ^^^, rewrites*)
11.78 +@{thm separate_1_bdv}; (*::?'a*)
11.79 +val xxx = num_str @{thm separate_1_bdv}; (*::?'a*)
11.80 +@{thm separate_1_bdv_n}; (*::real ..because of ^^^*)
11.81 +(*show_types := false; --- do we need type-constraint in thms? YES ?!?!?!*)
11.82 +
11.83 +*}
11.84 +ML{*
11.85 +atomty t;
11.86 +term2str t;
11.87 +*}
11.88 +ML{*
11.89 +val SOME (t, []) = rewrite_set_inst_ thy true subs rls t;
11.90 +*}
11.91 +ML{*
11.92 +if term2str t = "1 / EI * (L * q_0 / 2 * x + -1 * q_0 / 2 * x ^^^ 2)" then ()
11.93 +else error "integrate.sml simplify by ruleset separate_bdv.. #4";
11.94 +
11.95 +*}
11.96 +ML{*
11.97 +"===== test 5";
11.98 +val t = str2t "1/EI * (L * q_0 * x / 2 + -1 * q_0 * x^^^2 / 2)";
11.99 +*}
11.100 +ML{*
11.101 +val rls = simplify_Integral;
11.102 +*}
11.103 +ML{*
11.104 +val SOME (t,[]) = rewrite_set_inst_ thy true subs rls t;
11.105 +(* given was: "1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x^^^2 / 2)" *)
11.106 +*}
11.107 +ML{*
11.108 +if term2str t = "1 / EI * (L * q_0 / 2 * x + -1 * q_0 / 2 * x ^^^ 2)" then ()
11.109 +else error "integrate.sml, simplify_Integral #99";
11.110 +
11.111 +
11.112 +
11.113 +*}
11.114 +ML{*
11.115 +subs
11.116 *}
11.117 ML{*
11.118 *}
12.1 --- a/test/Tools/isac/print_exn_G.sml Fri Oct 14 14:34:10 2011 +0200
12.2 +++ b/test/Tools/isac/print_exn_G.sml Fri Oct 14 16:12:50 2011 +0200
12.3 @@ -2,3 +2,12 @@
12.4 Author: Walther Neuper 110320
12.5 (c) copyright due to lincense terms.
12.6 *)
12.7 +
12.8 +"-----------------------------------------------------------------";
12.9 +"table of contents -----------------------------------------------";
12.10 +"-----------------------------------------------------------------";
12.11 +"----------- test TODO -------------------------------------------";
12.12 +"-----------------------------------------------------------------";
12.13 +"-----------------------------------------------------------------";
12.14 +"-----------------------------------------------------------------";
12.15 +