1.1 --- a/doc-src/isac/akargl/ferialprakt.tex Mon Jul 25 11:52:07 2011 +0200
1.2 +++ b/doc-src/isac/akargl/ferialprakt.tex Mon Jul 25 14:19:22 2011 +0200
1.3 @@ -46,6 +46,13 @@
1.4 & Fehlersuche/Debugging Isac-Tests & 7.5 \\ \hline
1.5 19.7.2011
1.6 & Fehlersuche/Debugging Isac-Tests & 7.5 \\ \hline
1.7 +20.7.2011
1.8 + & Fehlersuche/Debugging Isac-Tests & 7.5 \\ \hline
1.9 +21.7.2011
1.10 + & Fehlersuche/Debugging Isac-Tests & 7.5 \\ \hline
1.11 +22.7.2011
1.12 + & Information \"uber Studienrichtungen etc. & 1.0 \\
1.13 + & Fehlersuche/Debugging Isac-Tests & 6.5 \\ \hline
1.14 \end{tabular}
1.15 \end{center}
1.16
2.1 --- a/test/Tools/isac/Interpret/calchead.sml Mon Jul 25 11:52:07 2011 +0200
2.2 +++ b/test/Tools/isac/Interpret/calchead.sml Mon Jul 25 14:19:22 2011 +0200
2.3 @@ -1,4 +1,3 @@
2.4 -
2.5 (* Title: tests on calchead.sml
2.6 Author: Walther Neuper 051013,
2.7 (c) due to copyright terms
2.8 @@ -85,11 +84,10 @@
2.9 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
2.10 (**)
2.11
2.12 -(*========== inhibit exn AK110718 =======================================================
2.13 val nxt = tac2tac_ pt p (Add_Find "valuesFor [(a::real)]");
2.14 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
2.15 (*uncaught exception TYPE 6.5.03*)
2.16 -
2.17 +(*========== inhibit exn AK110718 =======================================================
2.18 if ppc<>(Problem [],
2.19 {Find=[Incompl "maximum",Incompl "valuesFor [a]"],
2.20 Given=[Correct "fixedValues [r = Arbfix]"],
2.21 @@ -98,18 +96,21 @@
2.22 else (); (*different with show_types !!!*)
2.23 ========== inhibit exn AK110718 =======================================================*)
2.24
2.25 +val nxt = tac2tac_ pt p (Add_Given "boundVariable a");
2.26 (*========== inhibit exn AK110718 =======================================================
2.27 -val nxt = tac2tac_ pt p (Add_Given "boundVariable a");
2.28 +(* ERROR: Exception Bind raised *)
2.29 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
2.30 +========== inhibit exn AK110718 =======================================================*)
2.31
2.32 val nxt = tac2tac_ pt p (Add_Given "boundVariable a+");
2.33 +(*========== inhibit exn AK110718 =======================================================
2.34 +(* ERROR: Exception Bind raised *)
2.35 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
2.36 ========== inhibit exn AK110718 =======================================================*)
2.37
2.38 val m = Specify_Problem ["maximum_of","function"];
2.39 val nxt = tac2tac_ pt p m;
2.40 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
2.41 -(**)
2.42 (*========== inhibit exn AK110718 =======================================================
2.43 if ppc<>(Problem ["maximum_of","function"],
2.44 {Find=[Incompl "maximum",Incompl "valuesFor"],
2.45 @@ -124,10 +125,11 @@
2.46 Relate=[Missing "relations rs_"],Where=[],With=[]})
2.47 then error "diffappl.sml: Specify_Problem different behaviour"
2.48 else ();*)
2.49 +========== inhibit exn AK110718 =======================================================*)
2.50
2.51 val nxt = tac2tac_ pt p(Specify_Method ["DiffApp","max_by_calculus"]);
2.52 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
2.53 -(**)
2.54 +(*========== inhibit exn AK110718 =======================================================
2.55
2.56 if ppc<>(Method ["DiffApp","max_by_calculus"],
2.57 {Find=[Incompl "maximum",Incompl "valuesFor"],
2.58 @@ -280,13 +282,13 @@
2.59 (*val nxt = Add_Relation "relations" ---
2.60 --- [b=Arbfix] KANN NICHT VERLANGT WERDEN !!!!*)
2.61
2.62 -(*========== inhibit exn 010830 =======================================================
2.63 +(*========== inhibit exn 010830 =======================================================*)
2.64 (*30.8.01 ... funktioniert nicht mehr nach Einfuehrung env ....
2.65 if nxt<>(Add_Relation "relations []")
2.66 then error "test specify, fmz <> []: nxt <> Add_Relation.."
2.67 else (); (*different with show_types !!!*)
2.68 *)
2.69 -========== inhibit exn 010830 =======================================================*)
2.70 +(*========== inhibit exn 010830 =======================================================*)
2.71
2.72 val nxt = Add_Relation "relations [(A=a+b)]";
2.73 val nxt = tac2tac_ pt p nxt;
2.74 @@ -725,4 +727,3 @@
2.75
2.76 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
2.77 -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
2.78 -
3.1 --- a/test/Tools/isac/Interpret/rewtools.sml Mon Jul 25 11:52:07 2011 +0200
3.2 +++ b/test/Tools/isac/Interpret/rewtools.sml Mon Jul 25 14:19:22 2011 +0200
3.3 @@ -1,4 +1,4 @@
3.4 -(* test for rewtools.sml
3.5 +(* Title: test for rewtools.sml
3.6 authors: Walther Neuper 2000, 2006
3.7 *)
3.8
3.9 @@ -69,11 +69,11 @@
3.10 val ancestors = Theory.ancestors_of @{theory "Complex_Main"};
3.11 val isabthms = (flat o (map Theory.axioms_of)) ancestors;
3.12
3.13 -(*=== inhibit exn ?=============================================================
3.14 val isacrules = (flat o (map (thms_of_rls o #2 o #2))) (! ruleset');
3.15 (*thms from rulesets*)
3.16 +(*=== inhibit exn AK110725 =============================================================
3.17 val isacrlsthms = ((map rep_thm_G') o flat o
3.18 - (map (PureThy.all_thms_of_rls o #2 o #2))) (!ruleset');
3.19 + (map (PureThy.all_thms_of_rls o #2 o #2))) (!ruleset');
3.20 length isacrlsthms;
3.21 (*takes a few seconds...
3.22 val isacrlsthms = gen_distinct eq_thmI isacrlsthms;
3.23 @@ -83,6 +83,7 @@
3.24 "----- theorems used in isac's rulesets -----^^^^^^^^^^^^^^^^^^^^^";
3.25 ...*)
3.26
3.27 +
3.28 (!theory');
3.29 map #2 (!theory');
3.30 map (PureThy.all_thms_of o #2) (!theory');
3.31 @@ -108,7 +109,6 @@
3.32 length (PureThy.all_thms_of (nth 9 ancestors));
3.33 length sec;
3.34 ...*)
3.35 -
3.36 (*takes 1 minute...
3.37 print_depth 99;
3.38 map ((inter eq_thmI) rlsthmsNOTisac o PureThy.all_thms_of) ancestors;
3.39 @@ -120,32 +120,33 @@
3.40 ((#ancestors o rep_theory) first_isac_thy);
3.41 print_depth 99; isab_thm_thy; print_depth 3;
3.42 *)
3.43 +=== inhibit exn AK110725 =============================================================*)
3.44
3.45
3.46 "----------- fun thy_containing_thm ---------------------";
3.47 "----------- fun thy_containing_thm ---------------------";
3.48 "----------- fun thy_containing_thm ---------------------";
3.49 -val (str, (thy', thy)) = ("real_diff_minus",("Root", Root.thy));
3.50 +val (str, (thy', thy)) = ("real_diff_minus",("Root", @{theory Root}));
3.51 if thy_contains_thm str ("XXX",thy) then ()
3.52 -else error "rewtools.sml: NOT thy_contains_thm \
3.53 - \(real_diff_minus,(Root.thy,.";
3.54 + else error "rewtools.sml: NOT thy_contains_thm (real_diff_minus,(Root.thy,.";
3.55 (rev (!theory'));
3.56 -dropuntil (curry op= thy');
3.57 -dropuntil ((curry op= thy') o (#1:theory' * theory -> theory'));
3.58 -val startsearch = dropuntil ((curry op= thy') o
3.59 +dropuntil (curry op = thy');
3.60 +dropuntil ((curry op = thy') o (#1:theory' * theory -> theory'));
3.61 +val startsearch = dropuntil ((curry op = thy') o
3.62 (#1:theory' * theory -> theory'))
3.63 (rev (!theory'));
3.64 +
3.65 if thy_containing_thm thy' str = ("IsacKnowledge", "Root") then ()
3.66 -else error "rewtools.sml: NOT thy_containin_thm \
3.67 - \(real_diff_minus,(Root.thy,.";
3.68 + else error "rewtools.sml: NOT thy_containin_thm (real_diff_minus,(Root.thy,.";
3.69
3.70 "----- search the same theorem somewhere further below in the list";
3.71 -if thy_contains_thm str ("XXX",Poly.thy) then ()
3.72 -else error "rewtools.sml: NOT thy_contains_thm \
3.73 - \(real_diff_minus,(Poly.thy,.";
3.74 +if thy_contains_thm str ("XXX",@{theory Poly}) then ()
3.75 + else error "rewtools.sml: NOT thy_contains_thm (real_diff_minus,(Poly.thy,.";
3.76 +(*=== inhibit exn AK110725 =============================================================
3.77 +(* AK110725 "LineEq" can't be "Poly" - change "LineEq" to "Poly"??? *)
3.78 if thy_containing_thm "LinEq" str = ("IsacKnowledge", "Poly") then ()
3.79 -else error "rewtools.sml: NOT thy_containing_thm \
3.80 - \(real_diff_minus,(Poly.thy,.";
3.81 + else error "rewtools.sml: NOT thy_containing_thm (real_diff_minus,(Poly.thy,.";
3.82 +=== inhibit exn AK110725 =============================================================*)
3.83
3.84 "----- second test -------------------------------";
3.85 show_thes();
3.86 @@ -160,7 +161,6 @@
3.87 else error "rewtools.sml: diff.behav. in \
3.88 \thy_containing_thm Test radd_commute";
3.89
3.90 -
3.91 "----------- fun thy_containing_rls ---------------------";
3.92 "----------- fun thy_containing_rls ---------------------";
3.93 "----------- fun thy_containing_rls ---------------------";
3.94 @@ -191,6 +191,7 @@
3.95 if length (!ruleset') <> length startsearch then ()
3.96 else error "rewtools.sml: diff.behav. in thy_containing_rls 2";
3.97
3.98 +
3.99 val rls' = "norm_Poly";
3.100 case assoc (startsearch, rls') of
3.101 SOME (thy', _) => thyID2theory' thy'
3.102 @@ -218,7 +219,6 @@
3.103 val startsearch = filter_out ((curry ((op mem) o swap) dropthy's) o
3.104 (#1 : calc -> string)) (rev (!calclist'));
3.105 WN100819 =====================================================*)
3.106 -=== inhibit exn ?=============================================================*)
3.107
3.108 "----------- initContext Thy_ Integration-demo ----------";
3.109 "----------- initContext Thy_ Integration-demo ----------";
3.110 @@ -389,12 +389,12 @@
3.111 "----------- fun guh2theID ------------------------------";
3.112 "----------- fun guh2theID ------------------------------";
3.113 "----------- fun guh2theID ------------------------------";
3.114 +
3.115 val guh = "thy_scri_ListG-thm-zip_Nil";
3.116 -(*========== inhibit exn 110718 ================================================
3.117 -
3.118 -take_fromto 1 4 (explode guh);
3.119 -take_fromto 5 9 (explode guh);
3.120 -val rest = takerest (9,(explode guh));
3.121 +print_depth 999;
3.122 +take_fromto 1 4 (Symbol.explode guh);
3.123 +take_fromto 5 9 (Symbol.explode guh);
3.124 +val rest = takerest (9,(Symbol.explode guh));
3.125
3.126 separate "-" rest;
3.127 space_implode "-" rest;
3.128 @@ -408,7 +408,6 @@
3.129
3.130 if guh2theID guh = ["IsacScripts", "ListG", "Theorems", "zip_Nil"] then ()
3.131 else error "rewtools.sml: guh2theID thy_scri_ListG-thm-zip_Nil changed";
3.132 -============ inhibit exn 110718 ==============================================*)
3.133
3.134
3.135 "----------- debugging on Tests/solve_linear_as_rootpbl -";
3.136 @@ -457,18 +456,17 @@
3.137 checkContext 1 ([2,1],Res) "thy_isac_Test-rls-Test_simplify";
3.138 checkContext 1 ([2,2],Res) "thy_isac_Test-rls-Test_simplify";
3.139
3.140 -(*========== inhibit exn 110718 ================================================
3.141 -
3.142 -(* ERROR: constructor real_minus_eq_cancel has not been declared *)
3.143
3.144 "----------- fun string_of_thmI for_[.]_) ---------------";
3.145 "----------- fun string_of_thmI for_[.]_) ---------------";
3.146 "----------- fun string_of_thmI for_[.]_) ---------------";
3.147 "----- these work ?!?";
3.148 +(*========== inhibit exn 110718 ================================================
3.149 +(* ERROR: constructor real_minus_eq_cancel has not been declared *)
3.150 val th = sym_thm real_minus_eq_cancel;
3.151 val Th = sym_Thm (Thm ("real_minus_eq_cancel", real_minus_eq_cancel));
3.152 -val th'= mk_thm (theory "Isac") ((de_quote o string_of_thm) real_minus_eq_cancel);
3.153 -val th'= mk_thm Biegelinie.thy((de_quote o string_of_thm)real_minus_eq_cancel);
3.154 +val th'= mk_thm ( @{theory "Isac"} ) ((de_quote o string_of_thm) real_minus_eq_cancel);
3.155 +val th'= mk_thm Biegelinie.thy((de_quote o string_of_thm) real_minus_eq_cancel);
3.156
3.157 "----- DIFFERENCE TO ABOVE ?!?: this is still ok, when called in next_tac...";
3.158 val ((pt,(p,p_)), _) = get_calc 1; show_pt pt;
3.159 @@ -559,5 +557,3 @@
3.160 val r1 = Calc ("Groups.minus_class.minus", eval_binop "#add_");
3.161 if not (contains_rule r1 Test_simplify) then ()
3.162 else error "rewtools.sml contains_rule Calc";
3.163 -
3.164 -
4.1 --- a/test/Tools/isac/Test_Isac.thy Mon Jul 25 11:52:07 2011 +0200
4.2 +++ b/test/Tools/isac/Test_Isac.thy Mon Jul 25 14:19:22 2011 +0200
4.3 @@ -123,7 +123,7 @@
4.4 use "Interpret/ctree.sml" (*!...!see(25)*)
4.5 use "Interpret/ptyps.sml" (* *)
4.6 (*use "Interpret/generate.sml" new 2011*)
4.7 - use "Interpret/calchead.sml" (*! *)
4.8 + use "Interpret/calchead.sml" (*part.*)
4.9 use "Interpret/appl.sml" (*!complete WEGEN INTERMED TESTCODE*)
4.10 use "Interpret/rewtools.sml" (*! *)
4.11 use "Interpret/script.sml" (*!TODO/part.*)
5.1 --- a/test/Tools/isac/Test_Some.thy Mon Jul 25 11:52:07 2011 +0200
5.2 +++ b/test/Tools/isac/Test_Some.thy Mon Jul 25 14:19:22 2011 +0200
5.3 @@ -7,7 +7,7 @@
5.4
5.5 ML{* writeln "**** run the test ***************************************" *}
5.6
5.7 -use"../../../test/Tools/isac/Interpret/inform.sml"
5.8 +use"../../../test/Tools/isac/Interpret/calchead.sml"
5.9
5.10 ML{*
5.11
5.12 @@ -19,6 +19,10 @@
5.13
5.14
5.15
5.16 +
5.17 +
5.18 +
5.19 +
5.20 *}
5.21 ML{*
5.22 *}