1 (* Title: All tests on isac; observe outcommented
2 Author: Walther Neuper 101001
3 (c) copyright due to lincense terms.
5 $ cd /usr/local/isabisac/test/Tools/isac
6 $ /usr/local/Isabelle/bin/isabelle jedit -l Isac Test_Isac.thy &
7 1234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890
8 10 20 30 40 50 60 70 80 90 100
11 theory Test_Isac imports
13 "Knowledge/Rational_Test"
15 "ADDTESTS/test-depend/Build_Test"
17 (*"ADDTESTS/course/T2_Rewriting" theory has not been declared*)
18 (*"ADDTESTS/course/T1_Basics.thy" could not find ^^^*)
19 (*"ADDTESTS/course/T3_MathEngine" could not find ^^^*)
20 "ADDTESTS/file-depend/Build_Test"
21 "../../Pure/Isar/Test_Parsers"
22 (*"../../Pure/Isar/Pure/Isar/Struct_Deriv" update 2009-2-->2011*)
23 "../../Pure/Isar/Test_Parse_Term"
28 ("ProgLang/termC.sml")
29 ("ProgLang/calculate.sml")
30 ("ProgLang/rewrite.sml")
31 (*("ProgLang/listg.sml") ("ProgLang/scrtools.sml") ("ProgLang/tools.sml") *)
33 ("Minisubpbl/000-comments.sml")
34 ("Minisubpbl/100-init-rootpbl.sml")
35 ("Minisubpbl/150-add-given.sml")
36 ("Minisubpbl/200-start-method.sml")
37 ("Minisubpbl/300-init-subpbl.sml")
38 ("Minisubpbl/400-start-meth-subpbl.sml")
39 ("Minisubpbl/490-nxt-Check_Postcond.sml")
40 ("Minisubpbl/500-met-sub-to-root.sml")
41 ("Minisubpbl/530-error-Check_Elementwise.sml")
42 ("Minisubpbl/600-postcond.sml")
44 ("Interpret/mstools.sml")
45 ("Interpret/ctree.sml")
46 ("Interpret/ptyps.sml")
47 (*("Interpret/generate.sml")*)
48 ("Interpret/calchead.sml")
49 (*("Interpret/appl.sml")*)
50 ("Interpret/rewtools.sml")
51 (*("Interpret/script.sml")
52 ("Interpret/solve.sml")
53 ("Interpret/inform.sml")*)
54 ("Interpret/mathengine.sml")
56 (*("xmlsrc/mathml.sml")
57 ("xmlsrc/datatypes.sml")
58 ("xmlsrc/pbl-met-hierarchy.sml")
59 ("xmlsrc/thy-hierarchy.sml")*)
60 ("xmlsrc/interface-xml.sml")
62 ("Frontend/messages.sml")
63 ("Frontend/states.sml")
64 ("Frontend/interface.sml")
67 ("Knowledge/delete.sml")
68 ("Knowledge/descript.sml")
69 ("Knowledge/atools.sml")
70 ("Knowledge/simplify.sml")
71 ("Knowledge/poly.sml")
72 ("Knowledge/rational.sml")
73 ("Knowledge/equation.sml")
74 ("Knowledge/root.sml")
75 ("Knowledge/lineq.sml")
76 ("Knowledge/rooteq.sml")
77 ("Knowledge/rateq.sml")
78 ("Knowledge/rootrateq.sml")
79 (*("Knowledge/polyeq.sml")*)
80 ("Knowledge/calculus.sml")
81 ("Knowledge/trig.sml")
82 ("Knowledge/logexp.sml")
83 ("Knowledge/diff.sml")
84 ("Knowledge/integrate.sml")
85 ("Knowledge/eqsystem.sml")
86 ("Knowledge/test.sml")
87 ("Knowledge/polyminus.sml")
88 ("Knowledge/vect.sml")
89 ("Knowledge/diffapp.sml")
90 ("Knowledge/biegelinie.sml")
91 ("Knowledge/algein.sml")
92 ("Knowledge/diophanteq.sml")
93 ("Knowledge/isac.sml")
97 ML {*"%%%%%%%%%%%%%%%%% start ProgLang.thy %%%%%%%%%%%%%%%%%%%";*}
98 use "library.sml" (*new 2011*)
99 use "calcelems.sml" (*complete*)
100 use "ProgLang/termC.sml" (*part.*)
101 use "ProgLang/calculate.sml" (*part.*)
102 use "ProgLang/rewrite.sml" (*part.*)
103 (*use "ProgLang/listg.sml" 2002*)
104 (*use "ProgLang/scrtools.sml" 2002*)
105 (*use "ProgLang/tools.sml" 2002*)
106 ML {*"%%%%%%%%%%%%%%%%% end ProgLang.thy %%%%%%%%%%%%%%%%%%%%%";*}
107 ML {*"%%%%%%%%%%%%%%%%% start Minisubpbl %%%%%%%%%%%%%%%%%%%%%";*}
108 use "Minisubpbl/000-comments.sml"
109 use "Minisubpbl/100-init-rootpbl.sml"
110 use "Minisubpbl/150-add-given.sml"
111 use "Minisubpbl/200-start-method.sml"
112 use "Minisubpbl/300-init-subpbl.sml"
113 use "Minisubpbl/400-start-meth-subpbl.sml"
114 use "Minisubpbl/490-nxt-Check_Postcond.sml"
115 use "Minisubpbl/500-met-sub-to-root.sml"
116 use "Minisubpbl/530-error-Check_Elementwise.sml"
117 use "Minisubpbl/600-postcond.sml"
118 ML {*"%%%%%%%%%%%%%%%%% end Minisubpbl %%%%%%%%%%%%%%%%%%%%%%%";*}
119 ML {*"%%%%%%%%%%%%%%%%% start Interpret.thy %%%%%%%%%%%%%%%%%%";*}
120 use "Interpret/mstools.sml" (*new 2010*)
121 use "Interpret/ctree.sml" (*!...!see(25)*)
122 use "Interpret/ptyps.sml" (* *)
123 (*use "Interpret/generate.sml" new 2011*)
124 use "Interpret/calchead.sml" (*! *)
125 use "Interpret/appl.sml" (*!complete WEGEN INTERMED TESTCODE*)
126 use "Interpret/rewtools.sml" (*! *)
127 use "Interpret/script.sml" (*!TODO*)
128 (*use "Interpret/solve.sml" !TODO*)
129 (*use "Interpret/inform.sml" !TODO*)
130 use "Interpret/mathengine.sml" (*!part.*)
131 ML {*"%%%%%%%%%%%%%%%%% end Interpret.thy %%%%%%%%%%%%%%%%%%%%";*}
132 ML {*"%%%%%%%%%%%%%%%%% start xmlsrc.thy %%%%%%%%%%%%%%%%%%%%%";*}
133 (*use "xmlsrc/mathml.sml" TODO*)
134 (*use "xmlsrc/datatypes.sml" TODO*)
135 (*use "xmlsrc/pbl-met-hierarchy.sml" TODO*)
136 (*use "xmlsrc/thy-hierarchy.sml" TODO after 2009-2*)
137 use "xmlsrc/interface-xml.sml" (*TODO after 2009-2*)
138 ML {*"%%%%%%%%%%%%%%%%% end xmlsrc.thy %%%%%%%%%%%%%%%%%%%%%%%";*}
139 ML {*"%%%%%%%%%%%%%%%%% start Frontend.thy %%%%%%%%%%%%%%%%%%%";*}
140 use "Frontend/messages.sml" (*new 2011*)
141 use "Frontend/states.sml" (*new 2011*)
142 use "Frontend/interface.sml" (*part.*)
159 use "print_exn_G.sml" (*new 2011*)
160 ML {*"%%%%%%%%%%%%%%%%% end Frontend.thy %%%%%%%%%%%%%%%%%%%%%";*}
161 ML {*"%%%%%%%%%%%%%%%%% start Knowledge.thy %%%%%%%%%%%%%%%%%%";*}
162 use "Knowledge/delete.sml" (*new 2011*)
163 use "Knowledge/descript.sml" (*new 2011*)
164 (*use "Knowledge/atools.sml" 2002, added termorder.sml 2011*)
165 use "Knowledge/simplify.sml" (*part.*)
166 (*use "Knowledge/poly.sml" 2002*)
167 (*use "Knowledge/rational.sml" part.; diff.emacs--jedit*)
168 (*use "Knowledge/equation.sml" 2002*)
169 (*use "Knowledge/root.sml" 2002*)
170 use "Knowledge/lineq.sml" (*new 2011*)
171 (*use "Knowledge/rooteq.sml" 2002*)
172 (*use "Knowledge/rateq.sml" 2002*)
173 (*use "Knowledge/rootrat.sml" 2002*)
174 (*use "Knowledge/rootrateq.sml" 2002*)
175 (*use "Knowledge/polyeq.sml" 2002*)
176 (*use "Knowledge/rlang.sml" 2002???*)
177 use "Knowledge/calculus.sml" (*new 2011*)
178 (*use "Knowledge/trig.sml" 2002*)
179 (*use "Knowledge/logexp.sml" 2002*)
180 use "Knowledge/diff.sml" (*part.*)
181 (*use "Knowledge/integrate.sml" part. was complete 2009-2
183 (*use "Knowledge/eqsystem.sml" 2002*)
184 use "Knowledge/test.sml" (*new 2011*)
185 use "Knowledge/polyminus.sml" (*part.*)
186 (*use "Knowledge/vect.sml" 2002*)
187 (*use "Knowledge/diffapp.sml" 2002*)
188 (*use "Knowledge/biegelinie.sml" 2002*)
189 (*use "Knowledge/algein.sml" 2002*)
190 use "Knowledge/diophanteq.sml" (*complete*)
191 use "Knowledge/isac.sml" (*part.*)
192 ML {*"%%%%%%%%%%%%%%%%% end Knowledge.thy %%%%%%%%%%%%%%%%%%%%";*}
193 ML {*"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";*}
194 ML {*"%%%%%%%%%%%%%%%%% all tests successful %%%%%%%%%%%%%%%%%";*}
195 ML {*"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";*}
198 "--------- mini-subpbl AUTO CompleteCalcHead ------------";
200 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
201 ("Test", ["sqroot-test","univariate","equation","test"],
202 ["Test","squ-equ-test-subpbl1"]))];
205 (* doesn't terminate !!!*)
206 autoCalculate 1 CompleteCalcHead;
207 val (ModSpec (x1,x2,x3,x4,x5,x6), tac, asms) = pt_extract (pt, p);
215 ML {*"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";*}
219 (*=== inhibit exn ?=============================================================
220 ===== inhibit exn ?===========================================================*)
222 (*========== inhibit exn 110620 ================================================
224 "########### testcode inserted vvv ###########################################";
225 "########### testcode inserted ^^^ ###########################################";
227 ============ inhibit exn 110620 ==============================================*)
229 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
230 -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)