intermed: uncommented tests decompose-isar
authorAlexander Kargl <akargl@brgkepler.net>
Wed, 27 Jul 2011 08:43:58 +0200
branchdecompose-isar
changeset 42209a12b724f1d37
parent 42202 3ef5679743fb
child 42210 87ff4d96da1d
intermed: uncommented tests
doc-src/isac/akargl/ferialprakt.tex
test/Tools/isac/Interpret/inform.sml
test/Tools/isac/Interpret/solve.sml
test/Tools/isac/Test_Some.thy
     1.1 --- a/doc-src/isac/akargl/ferialprakt.tex	Tue Jul 26 15:52:07 2011 +0200
     1.2 +++ b/doc-src/isac/akargl/ferialprakt.tex	Wed Jul 27 08:43:58 2011 +0200
     1.3 @@ -54,6 +54,8 @@
     1.4   & Information \"uber Studienrichtungen etc. & 1.0 \\
     1.5   & Fehlersuche/Debugging Isac-Tests & 6.5 \\ \hline \hline
     1.6  25.7.2011
     1.7 + & Fehlersuche/Debugging Isac-Tests & 7.5 \\ \hline
     1.8 +26.7.2011
     1.9   & Fehlersuche/Debugging Isac-Tests & 7.5 \\ \hline 
    1.10  \end{tabular}
    1.11  \end{center}
     2.1 --- a/test/Tools/isac/Interpret/inform.sml	Tue Jul 26 15:52:07 2011 +0200
     2.2 +++ b/test/Tools/isac/Interpret/inform.sml	Wed Jul 27 08:43:58 2011 +0200
     2.3 @@ -63,13 +63,13 @@
     2.4   val str = pr_ptree pr_short pt;
     2.5  
     2.6   writeln str;
     2.7 -(*============ inhibit exn AK110725 ==============================================
     2.8 +(*============ inhibit exn AK110726 ==============================================
     2.9  (* 2nd string should be the same as 1st one *)
    2.10  ".    ----- pblobj -----\n1.   x + 1 = 2\n2.   x + 1 + -1 * 2 = 0\n2.1.   x + 1 + -1 * 2 = 0\n2.2.   1 + x + -1 * 2 = 0\n2.3.   1 + (x + -1 * 2) = 0\n2.4.   1 + (x + -2) = 0\n2.5.   1 + (x + -2 * 1) = 0\n2.6.   1 + x + -2 * 1 = 0\n";
    2.11  ".    ----- pblobj -----\n1.   x + 1 = 2\n2.   x + 1 + -1 * 2 = 0\n2.1.   x + 1 + -1 * 2 = 0\n2.2.   -1 * 2 + (x + 1) = 0\n2.3.   -1 * 2 + (1 + x) = 0\n2.4.   1 + (-1 * 2 + x) = 0\n2.5.   1 + (-2 + x) = 0\n2.6.   1 + (-2 * 1 + x) = 0\n";
    2.12   if str = ".    ----- pblobj -----\n1.   x + 1 = 2\n2.   x + 1 + -1 * 2 = 0\n2.1.   x + 1 + -1 * 2 = 0\n2.2.   -1 * 2 + (x + 1) = 0\n2.3.   -1 * 2 + (1 + x) = 0\n2.4.   1 + (-1 * 2 + x) = 0\n2.5.   1 + (-2 + x) = 0\n2.6.   1 + (-2 * 1 + x) = 0\n" then ()
    2.13 - else error "inform.sml: diff.behav.appendFormula: on Res + equ 1";
    2.14 -============ inhibit exn AK110725 ==============================================*)
    2.15 +   else error "inform.sml: diff.behav.appendFormula: on Res + equ 1";
    2.16 +============ inhibit exn AK110726 ==============================================*)
    2.17  
    2.18   moveDown 1 ([ ],Pbl); refFormula 1 ([1],Frm); (*x + 1 = 2*)
    2.19   moveDown 1 ([1],Frm); refFormula 1 ([1],Res); (*x + 1 + -1 * 2 = 0*)
    2.20 @@ -87,12 +87,14 @@
    2.21   else error "inform.sml: diff.behav.appendFormula: on Res + equ 2";
    2.22  
    2.23   fetchProposedTactic 1; (*takes Iterator 1 _1_*)
    2.24 +
    2.25  (*============ inhibit exn AK110725 ==============================================
    2.26  (* ERROR: exception Bind raised *)
    2.27   val (_,(tac,_,_)::_) = get_calc 1;
    2.28   if tac = Rewrite_Set "Test_simplify" then ()
    2.29   else error "inform.sml: diff.behav.appendFormula: on Res + equ 3";
    2.30  ============ inhibit exn AK110725 ==============================================*)
    2.31 +
    2.32   autoCalculate 1 CompleteCalc;
    2.33   val ((pt,_),_) = get_calc 1;
    2.34   if "[x = 1]" = term2str (fst (get_obj g_result pt [])) then ()
    2.35 @@ -529,8 +531,10 @@
    2.36  spec;
    2.37  writeln (itms2str_ ctxt probl);
    2.38  writeln (itms2str_ ctxt meth);
    2.39 +
    2.40  (*============ inhibit exn AK110725 ==============================================
    2.41 -(* ERROR: Argument: istate : istate * Proof.context Reason: Can't unify istate to istate * Proof.context *)
    2.42 +(* ERROR: Argument: istate : istate * Proof.context Reason: 
    2.43 +        Can't unify istate to istate * Proof.context *)
    2.44  writeln (istate2str istate);
    2.45  ============ inhibit exn AK110725 ==============================================*)
    2.46  
     3.1 --- a/test/Tools/isac/Interpret/solve.sml	Tue Jul 26 15:52:07 2011 +0200
     3.2 +++ b/test/Tools/isac/Interpret/solve.sml	Wed Jul 27 08:43:58 2011 +0200
     3.3 @@ -8,8 +8,6 @@
     3.4  which in turn
     3.5  uses from Poly.ML: Rls make_polynomial, Rls expand_binom 
     3.6  
     3.7 -use"../smltest/ME/solve.sml";
     3.8 -use"solve.sml";
     3.9  *)
    3.10  
    3.11  "-----------------------------------------------------------------";
    3.12 @@ -256,8 +254,9 @@
    3.13  (---------------WN060614?!?---*)
    3.14  
    3.15   val t = str2term "(3 + x) * (3 + -1 * x)";
    3.16 -(*========== inhibit exn AK110725 ================================================
    3.17 -(* ERROR: Argument: thy : domID * rls Reason: Can't unify theory to domID * rls *)
    3.18 +(*============ inhibit exn AK110725 ==============================================
    3.19 +(* ERROR: error is only visible in Test_Isac.sml -
    3.20 +   can't unify theory to domID * rls *)
    3.21   val SOME (t,_) = rewrite_set_ thy false expand_poly t; term2str t;
    3.22   "3 * 3 + 3 * (-1 * x) + (x * 3 + x * (-1 * x))";
    3.23   val SOME (t,_) = rewrite_set_ thy false order_add_mult t; term2str t;
    3.24 @@ -268,9 +267,9 @@
    3.25   "9 + (0 * x + -1 * x ^^^ 2)";
    3.26   val SOME (t,_) = rewrite_set_ thy false reduce_012 t; term2str t;
    3.27   "9 + - (x ^^^ 2)"; 
    3.28 +============ inhibit exn AK110725 ==============================================*)
    3.29 +
    3.30   (*14.3.03*)
    3.31 -========== inhibit exn AK110725 ================================================*)
    3.32 -
    3.33  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    3.34  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    3.35  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
     4.1 --- a/test/Tools/isac/Test_Some.thy	Tue Jul 26 15:52:07 2011 +0200
     4.2 +++ b/test/Tools/isac/Test_Some.thy	Wed Jul 27 08:43:58 2011 +0200
     4.3 @@ -7,7 +7,7 @@
     4.4  
     4.5  ML{* writeln "**** run the test ***************************************" *}
     4.6  
     4.7 -use"../../../test/Tools/isac/Interpret/appl.sml" 
     4.8 +use"../../../test/Tools/isac/Interpret/solve.sml" 
     4.9  
    4.10  ML {*
    4.11