1.1 --- a/test/Tools/isac/Test_Isac.thy Sat Jul 20 08:07:39 2013 +0200
1.2 +++ b/test/Tools/isac/Test_Isac.thy Sun Jul 21 15:08:31 2013 +0200
1.3 @@ -1,149 +1,79 @@
1.4 -(* Title: All tests on isac; observe outcommented
1.5 +(* Title: All tests on isac (some outcommented since Isabelle2002-->2009-2)
1.6 Author: Walther Neuper 101001
1.7 (c) copyright due to lincense terms.
1.8
1.9 -$ cd /usr/local/isabisac/test/Tools/isac
1.10 -$ /usr/local/isabisac/bin/isabelle jedit -l Isac Test_Isac.thy &
1.11 + isac tests
1.12 + in ~~/test/Tools/isac are structured according
1.13 + to ~~/src/Tools/isac
1.14 + Additional tests are in
1.15 + ~~/test/Tools/isac/ADDTESTS
1.16 + ~~/test/Tools/isac/Minisubpbl
1.17 +
1.18 +$ cd /usr/local/isabisac/
1.19 +$ ./bin/isabelle jedit -l Isac test/Tools/isac/Test_Isac.thy &
1.20 *)
1.21
1.22 -theory Test_Isac imports "~~/src/Tools/isac/Build_Isac"
1.23 +theory Test_Isac imports Isac
1.24 "ADDTESTS/Ctxt"
1.25 "ADDTESTS/test-depend/Build_Test"
1.26 "ADDTESTS/All_Ctxt"
1.27 "ADDTESTS/course/phst11/T1_Basics"
1.28 "ADDTESTS/course/phst11/T2_Rewriting"
1.29 "ADDTESTS/course/phst11/T3_MathEngine"
1.30 - "ADDTESTS/file-depend/Build_Test"
1.31 + "ADDTESTS/file-depend/BuildC_Test"
1.32 "ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform"
1.33 "../../Pure/Isar/Test_Parsers"
1.34 (*"../../Pure/Isar/Pure/Isar/Struct_Deriv" update 2009-2-->2011*)
1.35 "../../Pure/Isar/Test_Parse_Term"
1.36
1.37 -uses
1.38 - ( "library.sml")
1.39 - ( "calcelems.sml")
1.40 - ("ProgLang/termC.sml")
1.41 - ("ProgLang/calculate.sml")
1.42 - ("ProgLang/rewrite.sml")
1.43 - (*"ProgLang/listC.sml"*)
1.44 - ("ProgLang/scrtools.sml")
1.45 - ("ProgLang/tools.sml")
1.46 -
1.47 - ("Minisubpbl/000-comments.sml")
1.48 - ("Minisubpbl/100-init-rootpbl.sml")
1.49 - ("Minisubpbl/150-add-given.sml")
1.50 - ("Minisubpbl/200-start-method.sml")
1.51 - ("Minisubpbl/300-init-subpbl.sml")
1.52 - ("Minisubpbl/400-start-meth-subpbl.sml")
1.53 - ("Minisubpbl/490-nxt-Check_Postcond.sml")
1.54 - ("Minisubpbl/500-met-sub-to-root.sml")
1.55 - ("Minisubpbl/530-error-Check_Elementwise.sml")
1.56 - ("Minisubpbl/600-postcond.sml")
1.57 -
1.58 - ("Interpret/mstools.sml")
1.59 - ("Interpret/ctree.sml")
1.60 - ("Interpret/ptyps.sml")
1.61 - ("Interpret/generate.sml")
1.62 - ("Interpret/calchead.sml")
1.63 - ("Interpret/appl.sml")
1.64 - ("Interpret/rewtools.sml")
1.65 - ("Interpret/script.sml")
1.66 - ("Interpret/solve.sml")
1.67 - ("Interpret/inform.sml")
1.68 - ("Interpret/mathengine.sml")
1.69 -
1.70 - ("xmlsrc/mathml.sml")
1.71 - ("xmlsrc/datatypes.sml")
1.72 - ("xmlsrc/pbl-met-hierarchy.sml")
1.73 - (*"xmlsrc/thy-hierarchy.sml"*)
1.74 - ("xmlsrc/interface-xml.sml")
1.75 -
1.76 - ("Frontend/messages.sml")
1.77 - ("Frontend/states.sml")
1.78 - ("Frontend/interface.sml")
1.79 - ("print_exn_G.sml")
1.80 -
1.81 - ("Knowledge/delete.sml")
1.82 - ("Knowledge/descript.sml")
1.83 - ("Knowledge/atools.sml")
1.84 - ("Knowledge/simplify.sml")
1.85 - ("Knowledge/poly.sml")
1.86 -(*THIS WAITS UNTIL Isabelle2013: ("Knowledge/gcd_poly.sml") ("Knowledge/gcd_poly_winkler.sml")
1.87 - IN THIS SEQUENCE: SEE Test_Some2.thy*)
1.88 - (*"Knowledge/rational.sml"*)
1.89 - ("Knowledge/equation.sml")
1.90 - ("Knowledge/root.sml")
1.91 - ("Knowledge/lineq.sml")
1.92 - (*"Knowledge/rooteq.sml"*)
1.93 - ("Knowledge/rateq.sml")
1.94 - ("Knowledge/rootrateq.sml")
1.95 - ("Knowledge/polyeq.sml")
1.96 - ("Knowledge/calculus.sml")
1.97 - ("Knowledge/trig.sml")
1.98 - (*"Knowledge/logexp.sml"*)
1.99 - ("Knowledge/diff.sml")
1.100 - ("Knowledge/integrate.sml")
1.101 - ("Knowledge/eqsystem.sml")
1.102 - ("Knowledge/test.sml")
1.103 - ("Knowledge/partial_fractions.sml")
1.104 - ("Knowledge/polyminus.sml")
1.105 - ("Knowledge/vect.sml")
1.106 - ("Knowledge/diffapp.sml")
1.107 - ("Knowledge/biegelinie.sml")
1.108 - ("Knowledge/algein.sml")
1.109 - ("Knowledge/diophanteq.sml")
1.110 - ("Knowledge/Inverse_Z_Transform/inverse_z_transform.sml")
1.111 - ("Knowledge/isac.sml")
1.112 - ("Knowledge/build_thydata.sml")
1.113 -
1.114 begin
1.115 section {* test ML Code of isac *}
1.116 ML {*"%%%%%%%%%%%%%%%%% start ProgLang.thy %%%%%%%%%%%%%%%%%%%";*}
1.117 - use "library.sml"
1.118 - use "calcelems.sml"
1.119 - use "ProgLang/termC.sml"
1.120 - use "ProgLang/calculate.sml"
1.121 - use "ProgLang/rewrite.sml"
1.122 -(*use "ProgLang/listC.sml" 2002*)
1.123 - use "ProgLang/scrtools.sml"
1.124 - use "ProgLang/tools.sml"
1.125 + ML_file "library.sml"
1.126 + ML_file "calcelems.sml"
1.127 + ML_file "ProgLang/termC.sml"
1.128 + ML_file "ProgLang/calculate.sml"
1.129 + ML_file "ProgLang/rewrite.sml"
1.130 +(*ML_file "ProgLang/listC.sml" 2002*)
1.131 + ML_file "ProgLang/scrtools.sml"
1.132 + ML_file "ProgLang/tools.sml"
1.133 ML {*"%%%%%%%%%%%%%%%%% end ProgLang.thy %%%%%%%%%%%%%%%%%%%%%";*}
1.134 ML {*"%%%%%%%%%%%%%%%%% start Minisubpbl %%%%%%%%%%%%%%%%%%%%%";*}
1.135 - use "Minisubpbl/000-comments.sml"
1.136 - use "Minisubpbl/100-init-rootpbl.sml"
1.137 - use "Minisubpbl/150-add-given.sml"
1.138 - use "Minisubpbl/200-start-method.sml"
1.139 - use "Minisubpbl/300-init-subpbl.sml"
1.140 - use "Minisubpbl/400-start-meth-subpbl.sml"
1.141 - use "Minisubpbl/490-nxt-Check_Postcond.sml"
1.142 - use "Minisubpbl/500-met-sub-to-root.sml"
1.143 - use "Minisubpbl/530-error-Check_Elementwise.sml"
1.144 - use "Minisubpbl/600-postcond.sml"
1.145 + ML_file "Minisubpbl/000-comments.sml"
1.146 + ML_file "Minisubpbl/100-init-rootpbl.sml"
1.147 + ML_file "Minisubpbl/150-add-given.sml"
1.148 + ML_file "Minisubpbl/200-start-method.sml"
1.149 + ML_file "Minisubpbl/300-init-subpbl.sml"
1.150 + ML_file "Minisubpbl/400-start-meth-subpbl.sml"
1.151 + ML_file "Minisubpbl/490-nxt-Check_Postcond.sml"
1.152 + ML_file "Minisubpbl/500-met-sub-to-root.sml"
1.153 + ML_file "Minisubpbl/530-error-Check_Elementwise.sml"
1.154 + ML_file "Minisubpbl/600-postcond.sml"
1.155 ML {*"%%%%%%%%%%%%%%%%% end Minisubpbl.thy %%%%%%%%%%%%%%%%%%%%%%%";*}
1.156 ML {*"%%%%%%%%%%%%%%%%% start Interpret.thy %%%%%%%%%%%%%%%%%%";*}
1.157 - use "Interpret/mstools.sml"
1.158 - use "Interpret/ctree.sml" (*!...!see(25)*)
1.159 - use "Interpret/ptyps.sml"
1.160 + ML_file "Interpret/mstools.sml"
1.161 + ML_file "Interpret/ctree.sml" (*!...!see(25)*)
1.162 + ML_file "Interpret/ptyps.sml"
1.163 ML {* (*check_unsynchronized_ref (); ==== trick on error: CUT AND PASTE THIS LINE =========*) *}
1.164 (*TRICK DOESN'T WORK: get_pbt not found: ["IsacKnowledge","Diff","Theorems","diff_sin_chain"]*)
1.165 - use "Interpret/generate.sml"
1.166 + ML_file "Interpret/generate.sml"
1.167 (*WITHOUT inhibit exn WN1130621 Isabelle2012-->13 !thehier! THIS ERROR OCCURS:
1.168 ... SAME ERROR HERE ON ISABELLE2012 AS IN ISAC ON ISABELLE2011*)
1.169 - use "Interpret/calchead.sml"
1.170 - use "Interpret/appl.sml" (*complete "WEGEN INTERMED TESTCODE" *)
1.171 - use "Interpret/rewtools.sml" (*complete, isac's Context broken at 2009-2 --> 2011, thehier!*)
1.172 - use "Interpret/script.sml"
1.173 - use "Interpret/solve.sml"
1.174 - use "Interpret/inform.sml"
1.175 + ML_file "Interpret/calchead.sml"
1.176 + ML_file "Interpret/appl.sml" (*complete "WEGEN INTERMED TESTCODE" *)
1.177 + ML_file "Interpret/rewtools.sml" (*complete, isac's Context broken at 2009-2 --> 2011, thehier!*)
1.178 + ML_file "Interpret/script.sml"
1.179 + ML_file "Interpret/solve.sml"
1.180 + ML_file "Interpret/inform.sml"
1.181 (*WITHOUT inhibit exn WN1130621 Isabelle2012-->13 !thehier! THIS ERROR OCCURS:
1.182 ... SAME ERROR HERE ON ISABELLE2012 AS IN ISAC ON ISABELLE2011*)
1.183 - use "Interpret/mathengine.sml" (*!part.*)
1.184 + ML_file "Interpret/mathengine.sml" (*!part.*)
1.185 ML {*"%%%%%%%%%%%%%%%%% end Interpret.thy %%%%%%%%%%%%%%%%%%%%";*}
1.186 ML {*"%%%%%%%%%%%%%%%%% start xmlsrc.thy %%%%%%%%%%%%%%%%%%%%%";*}
1.187 - use "xmlsrc/mathml.sml" (*part.*)
1.188 - use "xmlsrc/datatypes.sml" (*TODO/part.*)
1.189 - use "xmlsrc/pbl-met-hierarchy.sml"(*TODO after 2009-2/part.*)
1.190 -(*use "xmlsrc/thy-hierarchy.sml" TODO after 2009-2/part | Isabelle2012-->13 !thehier! *)
1.191 + ML_file "xmlsrc/mathml.sml" (*part.*)
1.192 + ML_file "xmlsrc/datatypes.sml" (*TODO/part.*)
1.193 + ML_file "xmlsrc/pbl-met-hierarchy.sml"(*TODO after 2009-2/part.*)
1.194 +(*ML_file "xmlsrc/thy-hierarchy.sml" TODO after 2009-2/part | Isabelle2012-->13 !thehier! *)
1.195 (*WITHOUT inhibit exn WN1130621 Isabelle2012-->13 !thehier! THIS ERROR OCCURS:
1.196 val it = "----------- ### thes2file ... Exception- Match raised -----------": string
1.197 :
1.198 @@ -153,52 +83,52 @@
1.199 exception Bind raised (line 359 of "~~/test/Tools/isac/xmlsrc/thy-hierarchy.sml")
1.200 ...CONCERNED WITH thehier
1.201 *)
1.202 - use "xmlsrc/interface-xml.sml" (*TODO after 2009-2*)
1.203 + ML_file "xmlsrc/interface-xml.sml" (*TODO after 2009-2*)
1.204 ML {*"%%%%%%%%%%%%%%%%% end xmlsrc.thy %%%%%%%%%%%%%%%%%%%%%%%";*}
1.205 ML {*"%%%%%%%%%%%%%%%%% start Frontend.thy %%%%%%%%%%%%%%%%%%%";*}
1.206 - use "Frontend/messages.sml"
1.207 - use "Frontend/states.sml"
1.208 - use "Frontend/interface.sml"
1.209 + ML_file "Frontend/messages.sml"
1.210 + ML_file "Frontend/states.sml"
1.211 + ML_file "Frontend/interface.sml"
1.212 (*WITHOUT inhibit exn WN1130621 Isabelle2012-->13 !thehier! THIS ERROR OCCURS:
1.213 ... SAME ERROR HERE ON ISABELLE2012 AS IN ISAC ON ISABELLE2011*)
1.214 - use "print_exn_G.sml"
1.215 + ML_file "print_exn_G.sml"
1.216 ML {*"%%%%%%%%%%%%%%%%% end Frontend.thy %%%%%%%%%%%%%%%%%%%%%";*}
1.217 ML {*"%%%%%%%%%%%%%%%%% start Knowledge %%%%%%%%%%%%%%%%%%%%%%";*}
1.218 - use "Knowledge/delete.sml"
1.219 - use "Knowledge/descript.sml"
1.220 - use "Knowledge/atools.sml"
1.221 - use "Knowledge/simplify.sml"
1.222 - use "Knowledge/poly.sml"
1.223 + ML_file "Knowledge/delete.sml"
1.224 + ML_file "Knowledge/descript.sml"
1.225 + ML_file "Knowledge/atools.sml"
1.226 + ML_file "Knowledge/simplify.sml"
1.227 + ML_file "Knowledge/poly.sml"
1.228 (*THIS WAITS UNTIL Isabelle2013 IN THIS SEQUENCE (SEE Test_Some2.thy):0
1.229 - use "Knowledge/gcd_poly.sml" (*type error 'nth' etc*)
1.230 - use "Knowledge/gcd_poly_winkler.sml"*)
1.231 -(*use "Knowledge/rational.sml" WN120317.TODO postponed to joint work with dmeindl *)
1.232 - use "Knowledge/equation.sml"
1.233 - use "Knowledge/root.sml"
1.234 - use "Knowledge/lineq.sml"
1.235 -(*use "Knowledge/rooteq.sml" some complicated equations not recovered from 2002 *)
1.236 - use "Knowledge/rateq.sml" (*some complicated equations not recovered from 2002 *)
1.237 - use "Knowledge/rootrat.sml"
1.238 - use "Knowledge/rootrateq.sml"(*ome complicated equations not recovered from 2002 *)
1.239 - use "Knowledge/partial_fractions.sml"
1.240 - use "Knowledge/polyeq.sml"
1.241 -(*use "Knowledge/rlang.sml" much to clean up, not urgent due to similar tests *)
1.242 - use "Knowledge/calculus.sml"
1.243 - use "Knowledge/trig.sml"
1.244 -(*use "Knowledge/logexp.sml" not included as stuff for presentation of authoring*)
1.245 - use "Knowledge/diff.sml"
1.246 - use "Knowledge/integrate.sml"
1.247 - use "Knowledge/eqsystem.sml"
1.248 - use "Knowledge/test.sml"
1.249 - use "Knowledge/polyminus.sml"
1.250 - use "Knowledge/vect.sml"
1.251 - use "Knowledge/diffapp.sml" (* postponed to dev. specification | TP-prog. *)
1.252 - use "Knowledge/biegelinie.sml"
1.253 - use "Knowledge/algein.sml"
1.254 - use "Knowledge/diophanteq.sml"
1.255 - use "Knowledge/Inverse_Z_Transform/inverse_z_transform.sml"
1.256 - use "Knowledge/isac.sml"
1.257 - use "Knowledge/build_thydata.sml"
1.258 + ML_file "Knowledge/gcd_poly.sml" (*type error 'nth' etc*)
1.259 + ML_file "Knowledge/gcd_poly_winkler.sml"*)
1.260 +(*ML_file "Knowledge/rational.sml" WN120317.TODO postponed to joint work with dmeindl *)
1.261 + ML_file "Knowledge/equation.sml"
1.262 + ML_file "Knowledge/root.sml"
1.263 + ML_file "Knowledge/lineq.sml"
1.264 +(*ML_file "Knowledge/rooteq.sml" some complicated equations not recovered from 2002 *)
1.265 + ML_file "Knowledge/rateq.sml" (*some complicated equations not recovered from 2002 *)
1.266 + ML_file "Knowledge/rootrat.sml"
1.267 + ML_file "Knowledge/rootrateq.sml"(*ome complicated equations not recovered from 2002 *)
1.268 + ML_file "Knowledge/partial_fractions.sml"
1.269 + ML_file "Knowledge/polyeq.sml"
1.270 +(*ML_file "Knowledge/rlang.sml" much to clean up, not urgent due to similar tests *)
1.271 + ML_file "Knowledge/calculus.sml"
1.272 + ML_file "Knowledge/trig.sml"
1.273 +(*ML_file "Knowledge/logexp.sml" not included as stuff for presentation of authoring*)
1.274 + ML_file "Knowledge/diff.sml"
1.275 + ML_file "Knowledge/integrate.sml"
1.276 + ML_file "Knowledge/eqsystem.sml"
1.277 + ML_file "Knowledge/test.sml"
1.278 + ML_file "Knowledge/polyminus.sml"
1.279 + ML_file "Knowledge/vect.sml"
1.280 + ML_file "Knowledge/diffapp.sml" (* postponed to dev. specification | TP-prog. *)
1.281 + ML_file "Knowledge/biegelinie.sml"
1.282 + ML_file "Knowledge/algein.sml"
1.283 + ML_file "Knowledge/diophanteq.sml"
1.284 + ML_file "Knowledge/Inverse_Z_Transform/inverse_z_transform.sml"
1.285 + ML_file "Knowledge/isac.sml"
1.286 + ML_file "Knowledge/build_thydata.sml"
1.287 ML {*"%%%%%%%%%%%%%%%%% end Knowledge %%%%%%%%%%%%%%%%%%%%%%%%";*}
1.288 ML {*"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";*}
1.289 ML {*"%%%%%%%%%%%%%%%%% all tests successful %%%%%%%%%%%%%%%%%";*}
1.290 @@ -385,10 +315,9 @@
1.291 *}
1.292
1.293 end
1.294 -(*========== inhibit exn 110628 ================================================
1.295 -============ inhibit exn 110628 ==============================================*)
1.296 +(*========== inhibit exn 130719 Isabelle2013 ===================================
1.297 +============ inhibit exn 130719 Isabelle2013 =================================*)
1.298
1.299 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
1.300 -Pending source file dependencies: "Knowledge/algein.sml"
1.301 -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
1.302