1.1 --- a/src/Tools/isac/Interpret/appl.sml Thu Mar 17 10:11:18 2011 +0100
1.2 +++ b/src/Tools/isac/Interpret/appl.sml Thu Mar 17 10:46:02 2011 +0100
1.3 @@ -745,6 +745,7 @@
1.4 val pp = par_pblobj pt p;
1.5 val thy' = (get_obj g_domID pt pp):theory';
1.6 val thy = assoc_thy thy';
1.7 + val _ = tracing ("fun applicable_in Tac: p_ = " ^ pos_2str p_);
1.8 val f = case p_ of
1.9 Frm => get_obj g_form pt p
1.10 | Res => (fst o (get_obj g_result pt)) p;
2.1 --- a/src/Tools/isac/Test_Isac.thy Thu Mar 17 10:11:18 2011 +0100
2.2 +++ b/src/Tools/isac/Test_Isac.thy Thu Mar 17 10:46:02 2011 +0100
2.3 @@ -11,6 +11,8 @@
2.4
2.5 12345678901234567890123456789012345678901234567890123456789012345678901234567890
2.6 10 20 30 40 50 60 70 80
2.7 +Keep this width during test; otherwise \n would be inserted into string-
2.8 +representation of terms and thus break some tests.
2.9 *)
2.10
2.11 theory Test_Isac imports "Knowledge/Isac" begin
3.1 --- a/src/Tools/isac/Test_Some.thy Thu Mar 17 10:11:18 2011 +0100
3.2 +++ b/src/Tools/isac/Test_Some.thy Thu Mar 17 10:46:02 2011 +0100
3.3 @@ -17,6 +17,8 @@
3.4 (*..............................................########......................*)
3.5 *}
3.6
3.7 +ML {*pos_2str*}
3.8 +
3.9 use"../../../test/Tools/isac/Knowledge/diophanteq.sml";
3.10
3.11 end
4.1 --- a/test/Tools/isac/Knowledge/diophanteq.sml Thu Mar 17 10:11:18 2011 +0100
4.2 +++ b/test/Tools/isac/Knowledge/diophanteq.sml Thu Mar 17 10:46:02 2011 +0100
4.3 @@ -16,7 +16,7 @@
4.4 (*apparently no way to do these tests within DiophantEq.thy:
4.5 val thy = @{theory};(**** ME_Isa: thy 'DiophantEq' not in system
4.6 from CalcTreeTest*)
4.7 -(*(*val thy = @{theory "Isac"};toplevel error from store_met?!?*)*)
4.8 +(*val thy = @{theory "Isac"};toplevel error from store_met?!?*)
4.9 *)
4.10 val thy = @{theory "DiophantEq"};
4.11 val ctxt = ProofContext.init_global thy;
4.12 @@ -36,7 +36,6 @@
4.13 val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"PLUS"))) t;
4.14 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; term2str t;
4.15
4.16 -(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
4.17 "----------- mathengine with usecase1 -------------------";
4.18 "----------- mathengine with usecase1 -------------------";
4.19 "----------- mathengine with usecase1 -------------------";
4.20 @@ -49,6 +48,7 @@
4.21 "----- step 1: returns nxt = Add_Given \"functionTerm (x ^^^ 2 + 1)\" ---";
4.22 val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.23 val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.24 +(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
4.25 val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.26 val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.27 val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.1 --- a/test/Tools/isac/Knowledge/integrate.sml Thu Mar 17 10:11:18 2011 +0100
5.2 +++ b/test/Tools/isac/Knowledge/integrate.sml Thu Mar 17 10:46:02 2011 +0100
5.3 @@ -246,16 +246,14 @@
5.4 val rls = simplify_Integral;
5.5 val SOME (t,[]) = rewrite_set_inst_ thy true subs rls t;
5.6 if term2str t =
5.7 - "Integral 1 / EI *\n (L * q_0 / 4 * x ^^^ 2 +\n -1 * q_0 / 6 * x ^^^ 3) D x"
5.8 - (*"Integral 1 / EI * (L * q_0 / 4 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3) D x"*)
5.9 + "Integral 1 / EI * (L * q_0 / 4 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3) D x"
5.10 then () else raise error "integrate.sml, simplify_Integral #198";
5.11
5.12 val rls = integration_rules;
5.13 val SOME (t,[]) = rewrite_set_ thy true rls t;
5.14 term2str t;
5.15 if term2str t =
5.16 - "1 / EI *\n(L * q_0 / 4 * (x ^^^ 3 / 3) +\n -1 * q_0 / 6 * (x ^^^ 4 / 4))"
5.17 - (*"1 / EI * (L * q_0 / 4 * (x ^^^ 3 / 3) + -1 * q_0 / 6 * (x ^^^ 4 / 4))"*)
5.18 + "1 / EI * (L * q_0 / 4 * (x ^^^ 3 / 3) + -1 * q_0 / 6 * (x ^^^ 4 / 4))"
5.19 then () else error "integrate.sml, simplify_Integral #199";
5.20
5.21
5.22 @@ -301,19 +299,16 @@
5.23 val str = rewrit_sinst subs rls
5.24 "Integral 1 / EI * (L * q_0 / 2 * x + -1 * q_0 / 2 * x ^^^ 2) D x";
5.25 if str =
5.26 - "c +\n1 / EI * (L * q_0 / 4 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)"
5.27 - (*"c + 1 / EI * (L * q_0 / 4 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)"*)
5.28 + "c + 1 / EI * (L * q_0 / 4 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)"
5.29 then () else error "integrate.sml: diff.behav. in integration #3";
5.30
5.31 val str = "Integral "^str^" D x";
5.32 val str = rewrit_sinst subs rls str;
5.33 if str =
5.34 - "c_2 + c * x +\n1 / EI *\n(L * q_0 / 12 * x ^^^ 3 + -1 * q_0 / 24 * x ^^^ 4)"
5.35 -(*"c_2 + c * x + 1 / EI * (L * q_0 / 12 * x ^^^ 3 + -1 * q_0 / 24 * x ^^^ 4)"*)
5.36 + "c_2 + c * x + 1 / EI * (L * q_0 / 12 * x ^^^ 3 + -1 * q_0 / 24 * x ^^^ 4)"
5.37 then () else error "integrate.sml: diff.behav. in integration #4";
5.38
5.39
5.40 -
5.41 "----------- rewrite 3rd integration in 7.27 ------------";
5.42 "----------- rewrite 3rd integration in 7.27 ------------";
5.43 "----------- rewrite 3rd integration in 7.27 ------------";
5.44 @@ -322,17 +317,14 @@
5.45 val t = str2term
5.46 "Integral 1 / EI * ((L * q_0 * x + -1 * q_0 * x ^^^ 2) / 2) D x";
5.47 val SOME(t,_)= rewrite_set_inst_ thy true bdv simplify_Integral t;
5.48 -term2str t;
5.49 if term2str t =
5.50 - "Integral 1 / EI *\n (L * q_0 / 2 * x + -1 * q_0 / 2 * x ^^^ 2) D x"
5.51 -(*"Integral 1 / EI * (L * q_0 / 2 * x + -1 * q_0 / 2 * x ^^^ 2) D x" *)
5.52 + "Integral 1 / EI * (L * q_0 / 2 * x + -1 * q_0 / 2 * x ^^^ 2) D x"
5.53 then () else error "integrate.sml 3rd integration in 7.27, simplify_Integral";
5.54
5.55 val SOME(t,_)= rewrite_set_inst_ thy true bdv integration t;
5.56 term2str t;
5.57 if term2str t =
5.58 - "c +\n1 / EI * (L * q_0 / 4 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)"
5.59 -(*"c + 1 / EI * (L * q_0 / 4 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)"*)
5.60 + "c + 1 / EI * (L * q_0 / 4 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)"
5.61 then () else error "integrate.sml 3rd integration in 7.27, integration";
5.62
5.63
6.1 --- a/test/Tools/isac/Knowledge/rational.sml Thu Mar 17 10:11:18 2011 +0100
6.2 +++ b/test/Tools/isac/Knowledge/rational.sml Thu Mar 17 10:46:02 2011 +0100
6.3 @@ -1343,8 +1343,11 @@
6.4 "----- S.K. corrected non-termination 060904";
6.5 val t = str2term "(3*a - 4*b) * (3*a+4*b)/((4*c+3*e)*(9*a^^^2 - 16*b^^^2))";
6.6 val SOME (t',_) = rewrite_set_ thy false make_polynomial t;
6.7 -if term2str t' = "(9 * a ^^^ 2 + -16 * b ^^^ 2) /\n(36 * a ^^^ 2 * c + 27 * a ^^^ 2 * e + -64 * b ^^^ 2 * c +\n -48 * b ^^^ 2 * e)" then ()
6.8 -else error "rational.sml: S.K.8..corrected 060904-6";
6.9 +term2str t';
6.10 +if term2str t' =
6.11 + "(9 * a ^^^ 2 + -16 * b ^^^ 2) /\n(36 * a ^^^ 2 * c + 27 * a ^^^ 2 * e + -64 * b ^^^ 2 * c + -48 * b ^^^ 2 * e)"
6.12 +(*"(9 * a ^^^ 2 + -16 * b ^^^ 2) / (36 * a ^^^ 2 * c + 27 * a ^^^ 2 * e + -64 * b ^^^ 2 * c + -48 * b ^^^ 2 * e)"*)
6.13 +then () else error "rational.sml: S.K.8..corrected 060904-6";
6.14
6.15 "----- S.K. corrected non-termination of cancel_p_";
6.16 val t'' = str2term ("(9 * a ^^^ 2 + -16 * b ^^^ 2) /" ^
6.17 @@ -1420,7 +1423,7 @@
6.18 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
6.19 term2str t;
6.20 if (term2str t) =
6.21 -"(36 * b ^^^ 3 + 3 * a ^^^ 2 * b ^^^ 2 +\n 16 * a ^^^ 4 * b) /\n(9 * a ^^^ 4)"
6.22 + "(36 * b ^^^ 3 + 3 * a ^^^ 2 * b ^^^ 2 + 16 * a ^^^ 4 * b) / (9 * a ^^^ 4)"
6.23 then () else error "rational.sml: diff.behav. in norm_Rational_mg 28";
6.24
6.25 (*SRAM Schalk I, p.69 Nr. 442b *)
6.26 @@ -1531,10 +1534,8 @@
6.27 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
6.28 term2str t;
6.29 if (term2str t) =
6.30 -(*"8 * a ^^^ 2 + -6 * a * b + -12 * a ^^^ 2 * b + 9 * a * b ^^^ 2"*)
6.31 -"8 * a ^^^ 2 + -6 * a * b + -12 * a ^^^ 2 * b +\n9 * a * b ^^^ 2"
6.32 -then ()
6.33 -else error "rational.sml: diff.behav. in norm_Rational_mg 39";
6.34 + "8 * a ^^^ 2 + -6 * a * b + -12 * a ^^^ 2 * b + 9 * a * b ^^^ 2"
6.35 +then () else error "rational.sml: diff.behav. in norm_Rational_mg 39";
6.36
6.37 "----- Schalk I, p.69 Nr. 458b works since 0707";
6.38 val t = str2term
6.39 @@ -2077,3 +2078,5 @@
6.40 " Try (Rewrite_Set discard_parentheses False)) " ^
6.41 " t_t)"
6.42 );
6.43 +(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
6.44 +-.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)