author | Walther Neuper <neuper@ist.tugraz.at> |
Fri, 21 Jun 2013 08:06:16 +0200 | |
changeset 48889 | 4592ea17edd8 |
parent 48888 | 4eb0d1968d46 |
child 48891 | 882e79a01a4f |
permissions | -rwxr-xr-x |
neuper@41945 | 1 |
(* Title: All tests on isac; observe outcommented |
neuper@41943 | 2 |
Author: Walther Neuper 101001 |
neuper@41943 | 3 |
(c) copyright due to lincense terms. |
neuper@41943 | 4 |
|
neuper@41943 | 5 |
$ cd /usr/local/isabisac/test/Tools/isac |
neuper@48884 | 6 |
$ /usr/local/isabisac/bin/isabelle jedit -l Isac Test_Isac.thy & |
neuper@41943 | 7 |
*) |
neuper@41943 | 8 |
|
neuper@48888 | 9 |
theory Test_Isac imports Isac |
neuper@41980 | 10 |
"ADDTESTS/Ctxt" |
neuper@42048 | 11 |
"ADDTESTS/test-depend/Build_Test" |
neuper@42023 | 12 |
"ADDTESTS/All_Ctxt" |
neuper@42179 | 13 |
"ADDTESTS/course/phst11/T1_Basics" |
neuper@42092 | 14 |
"ADDTESTS/course/phst11/T2_Rewriting" |
neuper@42179 | 15 |
"ADDTESTS/course/phst11/T3_MathEngine" |
neuper@42048 | 16 |
"ADDTESTS/file-depend/Build_Test" |
neuper@42280 | 17 |
"ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform" |
neuper@42048 | 18 |
"../../Pure/Isar/Test_Parsers" |
neuper@42048 | 19 |
(*"../../Pure/Isar/Pure/Isar/Struct_Deriv" update 2009-2-->2011*) |
neuper@42048 | 20 |
"../../Pure/Isar/Test_Parse_Term" |
neuper@42387 | 21 |
|
neuper@41945 | 22 |
uses |
neuper@41945 | 23 |
( "library.sml") |
neuper@41945 | 24 |
( "calcelems.sml") |
neuper@42185 | 25 |
("ProgLang/termC.sml") |
neuper@41945 | 26 |
("ProgLang/calculate.sml") |
neuper@41945 | 27 |
("ProgLang/rewrite.sml") |
neuper@48884 | 28 |
("ProgLang/listC.sml") |
akargl@42176 | 29 |
("ProgLang/scrtools.sml") |
akargl@42176 | 30 |
("ProgLang/tools.sml") |
neuper@41945 | 31 |
|
neuper@41985 | 32 |
("Minisubpbl/000-comments.sml") |
neuper@41985 | 33 |
("Minisubpbl/100-init-rootpbl.sml") |
neuper@41986 | 34 |
("Minisubpbl/150-add-given.sml") |
neuper@41985 | 35 |
("Minisubpbl/200-start-method.sml") |
neuper@41985 | 36 |
("Minisubpbl/300-init-subpbl.sml") |
neuper@41985 | 37 |
("Minisubpbl/400-start-meth-subpbl.sml") |
neuper@42022 | 38 |
("Minisubpbl/490-nxt-Check_Postcond.sml") |
neuper@42022 | 39 |
("Minisubpbl/500-met-sub-to-root.sml") |
neuper@42022 | 40 |
("Minisubpbl/530-error-Check_Elementwise.sml") |
neuper@42022 | 41 |
("Minisubpbl/600-postcond.sml") |
neuper@41985 | 42 |
|
neuper@41945 | 43 |
("Interpret/mstools.sml") |
bonzai@41951 | 44 |
("Interpret/ctree.sml") |
neuper@41945 | 45 |
("Interpret/ptyps.sml") |
akargl@42176 | 46 |
("Interpret/generate.sml") |
neuper@41945 | 47 |
("Interpret/calchead.sml") |
akargl@42176 | 48 |
("Interpret/appl.sml") |
neuper@41945 | 49 |
("Interpret/rewtools.sml") |
akargl@42169 | 50 |
("Interpret/script.sml") |
akargl@42176 | 51 |
("Interpret/solve.sml") |
akargl@42176 | 52 |
("Interpret/inform.sml") |
neuper@41945 | 53 |
("Interpret/mathengine.sml") |
neuper@41945 | 54 |
|
akargl@42176 | 55 |
("xmlsrc/mathml.sml") |
neuper@41945 | 56 |
("xmlsrc/datatypes.sml") |
neuper@41945 | 57 |
("xmlsrc/pbl-met-hierarchy.sml") |
akargl@42176 | 58 |
("xmlsrc/thy-hierarchy.sml") |
neuper@41945 | 59 |
("xmlsrc/interface-xml.sml") |
neuper@41945 | 60 |
|
neuper@41945 | 61 |
("Frontend/messages.sml") |
neuper@41945 | 62 |
("Frontend/states.sml") |
neuper@41945 | 63 |
("Frontend/interface.sml") |
neuper@41945 | 64 |
("print_exn_G.sml") |
neuper@41945 | 65 |
|
neuper@41945 | 66 |
("Knowledge/delete.sml") |
neuper@41945 | 67 |
("Knowledge/descript.sml") |
neuper@41945 | 68 |
("Knowledge/atools.sml") |
neuper@41945 | 69 |
("Knowledge/simplify.sml") |
neuper@41945 | 70 |
("Knowledge/poly.sml") |
neuper@48884 | 71 |
(*THIS WAITS UNTIL Isabelle2013: ("Knowledge/gcd_poly.sml") ("Knowledge/gcd_poly_winkler.sml") |
neuper@48884 | 72 |
IN THIS SEQUENCE: SEE Test_Some2.thy*) |
neuper@41945 | 73 |
("Knowledge/rational.sml") |
neuper@41945 | 74 |
("Knowledge/equation.sml") |
neuper@41945 | 75 |
("Knowledge/root.sml") |
neuper@41945 | 76 |
("Knowledge/lineq.sml") |
neuper@41945 | 77 |
("Knowledge/rooteq.sml") |
neuper@41945 | 78 |
("Knowledge/rateq.sml") |
neuper@41945 | 79 |
("Knowledge/rootrateq.sml") |
neuper@42185 | 80 |
("Knowledge/polyeq.sml") |
neuper@41945 | 81 |
("Knowledge/calculus.sml") |
neuper@41945 | 82 |
("Knowledge/trig.sml") |
neuper@41945 | 83 |
("Knowledge/logexp.sml") |
neuper@41945 | 84 |
("Knowledge/diff.sml") |
neuper@41945 | 85 |
("Knowledge/integrate.sml") |
neuper@41945 | 86 |
("Knowledge/eqsystem.sml") |
neuper@41945 | 87 |
("Knowledge/test.sml") |
neuper@42289 | 88 |
("Knowledge/partial_fractions.sml") |
neuper@41945 | 89 |
("Knowledge/polyminus.sml") |
neuper@41945 | 90 |
("Knowledge/vect.sml") |
neuper@41945 | 91 |
("Knowledge/diffapp.sml") |
neuper@41945 | 92 |
("Knowledge/biegelinie.sml") |
neuper@41945 | 93 |
("Knowledge/algein.sml") |
neuper@41945 | 94 |
("Knowledge/diophanteq.sml") |
neuper@42412 | 95 |
("Knowledge/Inverse_Z_Transform/inverse_z_transform.sml") |
neuper@41945 | 96 |
("Knowledge/isac.sml") |
neuper@42407 | 97 |
("Knowledge/build_thydata.sml") |
neuper@41945 | 98 |
|
neuper@41943 | 99 |
begin |
neuper@41947 | 100 |
|
neuper@42451 | 101 |
ML {*"%%%%%%%%%%%%%%%%% start ProgLang.thy %%%%%%%%%%%%%%%%%%%";*} |
neuper@42179 | 102 |
use "library.sml" |
neuper@42179 | 103 |
use "calcelems.sml" |
akargl@42188 | 104 |
use "ProgLang/termC.sml" |
t@42225 | 105 |
use "ProgLang/calculate.sml" |
t@42227 | 106 |
use "ProgLang/rewrite.sml" |
neuper@42185 | 107 |
(*use "ProgLang/listC.sml" 2002*) |
t@42225 | 108 |
use "ProgLang/scrtools.sml" |
t@42225 | 109 |
use "ProgLang/tools.sml" |
neuper@41943 | 110 |
ML {*"%%%%%%%%%%%%%%%%% end ProgLang.thy %%%%%%%%%%%%%%%%%%%%%";*} |
neuper@41986 | 111 |
ML {*"%%%%%%%%%%%%%%%%% start Minisubpbl %%%%%%%%%%%%%%%%%%%%%";*} |
neuper@41985 | 112 |
use "Minisubpbl/000-comments.sml" |
neuper@41985 | 113 |
use "Minisubpbl/100-init-rootpbl.sml" |
neuper@41986 | 114 |
use "Minisubpbl/150-add-given.sml" |
neuper@41985 | 115 |
use "Minisubpbl/200-start-method.sml" |
neuper@41990 | 116 |
use "Minisubpbl/300-init-subpbl.sml" |
neuper@41997 | 117 |
use "Minisubpbl/400-start-meth-subpbl.sml" |
neuper@42022 | 118 |
use "Minisubpbl/490-nxt-Check_Postcond.sml" |
neuper@41998 | 119 |
use "Minisubpbl/500-met-sub-to-root.sml" |
neuper@42022 | 120 |
use "Minisubpbl/530-error-Check_Elementwise.sml" |
neuper@41998 | 121 |
use "Minisubpbl/600-postcond.sml" |
akargl@42188 | 122 |
ML {*"%%%%%%%%%%%%%%%%% end Minisubpbl.thy %%%%%%%%%%%%%%%%%%%%%%%";*} |
neuper@41943 | 123 |
ML {*"%%%%%%%%%%%%%%%%% start Interpret.thy %%%%%%%%%%%%%%%%%%";*} |
neuper@42185 | 124 |
use "Interpret/mstools.sml" |
neuper@41989 | 125 |
use "Interpret/ctree.sml" (*!...!see(25)*) |
neuper@42390 | 126 |
use "Interpret/ptyps.sml" |
neuper@48889 | 127 |
ML {* check_unsynchronized_ref (); (*==== trick on error: CUT AND PASTE THIS LINE =========*) *} |
neuper@48889 | 128 |
(*get_pbt not found: ["IsacKnowledge","Diff","Theorems","diff_sin_chain"]*) |
neuper@42321 | 129 |
use "Interpret/generate.sml" |
neuper@48889 | 130 |
(*... SAME ERROR HERE ON ISABELLE2012 AS IN ISAC ON ISABELLE2011*) |
akargl@42181 | 131 |
use "Interpret/calchead.sml" (*part.*) |
neuper@41975 | 132 |
use "Interpret/appl.sml" (*!complete WEGEN INTERMED TESTCODE*) |
neuper@42407 | 133 |
use "Interpret/rewtools.sml" (*TODO/part.WN120406*) |
neuper@48889 | 134 |
(*val it = "----------- fun thy_containing_rls ---------------------": string |
neuper@48889 | 135 |
: |
neuper@48889 | 136 |
thy_containing_rls changed 1 ...CONCERNED WITH thehier |
neuper@48889 | 137 |
*) |
akargl@42176 | 138 |
use "Interpret/script.sml" (*!TODO/part.*) |
akargl@42176 | 139 |
use "Interpret/solve.sml" (*part.*) |
akargl@42176 | 140 |
use "Interpret/inform.sml" (*part.*) |
neuper@48889 | 141 |
(*val it = "--------- embed fun check_error_patterns ------------------------": string |
neuper@48889 | 142 |
: |
neuper@48889 | 143 |
val it = "~~~~~ from inform return val:": string |
neuper@48889 | 144 |
check_error_patterns broken ...CONCERNED WITH thehier |
neuper@48889 | 145 |
*) |
neuper@41972 | 146 |
use "Interpret/mathengine.sml" (*!part.*) |
neuper@41943 | 147 |
ML {*"%%%%%%%%%%%%%%%%% end Interpret.thy %%%%%%%%%%%%%%%%%%%%";*} |
neuper@41943 | 148 |
ML {*"%%%%%%%%%%%%%%%%% start xmlsrc.thy %%%%%%%%%%%%%%%%%%%%%";*} |
akargl@42176 | 149 |
use "xmlsrc/mathml.sml" (*part.*) |
akargl@42176 | 150 |
use "xmlsrc/datatypes.sml" (*TODO/part.*) |
neuper@42407 | 151 |
use "xmlsrc/pbl-met-hierarchy.sml" (*TODO after 2009-2/part.*) |
neuper@42407 | 152 |
use "xmlsrc/thy-hierarchy.sml" (*TODO after 2009-2/part.*) |
neuper@48889 | 153 |
(*val it = "----------- ### thes2file ... Exception- Match raised -----------": string |
neuper@48889 | 154 |
: |
neuper@48889 | 155 |
val it = "~~~~~ fun thes2file, args:": string |
neuper@48889 | 156 |
val p = "../../tmp/": path |
neuper@48889 | 157 |
val it = (): unit |
neuper@48889 | 158 |
exception Bind raised (line 359 of "~~/test/Tools/isac/xmlsrc/thy-hierarchy.sml") |
neuper@48889 | 159 |
...CONCERNED WITH thehier |
neuper@48889 | 160 |
*) |
akargl@42176 | 161 |
use "xmlsrc/interface-xml.sml" (*TODO after 2009-2*) |
neuper@41943 | 162 |
ML {*"%%%%%%%%%%%%%%%%% end xmlsrc.thy %%%%%%%%%%%%%%%%%%%%%%%";*} |
neuper@41943 | 163 |
ML {*"%%%%%%%%%%%%%%%%% start Frontend.thy %%%%%%%%%%%%%%%%%%%";*} |
neuper@42321 | 164 |
use "Frontend/messages.sml" |
neuper@42321 | 165 |
use "Frontend/states.sml" |
t@42225 | 166 |
use "Frontend/interface.sml" |
neuper@48889 | 167 |
(*... SAME ERROR HERE ON ISABELLE2012 AS IN ISAC ON ISABELLE2011*) |
neuper@42407 | 168 |
use "print_exn_G.sml" |
neuper@41943 | 169 |
ML {*"%%%%%%%%%%%%%%%%% end Frontend.thy %%%%%%%%%%%%%%%%%%%%%";*} |
neuper@41943 | 170 |
ML {*"%%%%%%%%%%%%%%%%% start Knowledge.thy %%%%%%%%%%%%%%%%%%";*} |
neuper@42321 | 171 |
use "Knowledge/delete.sml" |
neuper@42321 | 172 |
use "Knowledge/descript.sml" |
neuper@42397 | 173 |
use "Knowledge/atools.sml" |
neuper@42396 | 174 |
use "Knowledge/simplify.sml" |
neuper@42395 | 175 |
use "Knowledge/poly.sml" |
neuper@48884 | 176 |
(*THIS WAITS UNTIL Isabelle2013 IN THIS SEQUENCE (SEE Test_Some2.thy):0 |
neuper@48884 | 177 |
use "Knowledge/gcd_poly.sml" (*type error 'nth' etc*) |
neuper@48884 | 178 |
use "Knowledge/gcd_poly_winkler.sml"*) |
neuper@42399 | 179 |
(*use "Knowledge/rational.sml" WN120317.TODO postponed to joint work with dmeindl *) |
neuper@42395 | 180 |
use "Knowledge/equation.sml" |
neuper@42395 | 181 |
use "Knowledge/root.sml" |
neuper@42395 | 182 |
use "Knowledge/lineq.sml" |
neuper@42395 | 183 |
(*use "Knowledge/rooteq.sml" some complicated equations not recovered from 2002 *) |
neuper@42395 | 184 |
use "Knowledge/rateq.sml" (*some complicated equations not recovered from 2002 *) |
neuper@42392 | 185 |
use "Knowledge/rootrat.sml" |
neuper@42397 | 186 |
use "Knowledge/rootrateq.sml"(*ome complicated equations not recovered from 2002 *) |
neuper@42289 | 187 |
use "Knowledge/partial_fractions.sml" |
neuper@42319 | 188 |
use "Knowledge/polyeq.sml" |
neuper@42413 | 189 |
(*use "Knowledge/rlang.sml" much to clean up, not urgent due to similar tests *) |
neuper@42321 | 190 |
use "Knowledge/calculus.sml" |
t@42225 | 191 |
use "Knowledge/trig.sml" |
neuper@42393 | 192 |
(*use "Knowledge/logexp.sml" not included as stuff for presentation of authoring*) |
neuper@42393 | 193 |
use "Knowledge/diff.sml" |
neuper@42393 | 194 |
use "Knowledge/integrate.sml" |
neuper@42391 | 195 |
use "Knowledge/eqsystem.sml" |
t@42225 | 196 |
use "Knowledge/test.sml" |
neuper@42390 | 197 |
use "Knowledge/polyminus.sml" |
t@42225 | 198 |
use "Knowledge/vect.sml" |
neuper@42399 | 199 |
use "Knowledge/diffapp.sml" (* postponed to dev. specification | TP-prog. *) |
neuper@42387 | 200 |
use "Knowledge/biegelinie.sml" |
neuper@42385 | 201 |
use "Knowledge/algein.sml" |
t@42225 | 202 |
use "Knowledge/diophanteq.sml" |
neuper@42412 | 203 |
use "Knowledge/Inverse_Z_Transform/inverse_z_transform.sml" |
neuper@42399 | 204 |
use "Knowledge/isac.sml" |
neuper@42400 | 205 |
use "Knowledge/build_thydata.sml" |
neuper@41943 | 206 |
ML {*"%%%%%%%%%%%%%%%%% end Knowledge.thy %%%%%%%%%%%%%%%%%%%%";*} |
neuper@41945 | 207 |
ML {*"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";*} |
neuper@41945 | 208 |
ML {*"%%%%%%%%%%%%%%%%% all tests successful %%%%%%%%%%%%%%%%%";*} |
neuper@41945 | 209 |
ML {*"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";*} |
neuper@41943 | 210 |
|
neuper@41943 | 211 |
end |
neuper@42067 | 212 |
(*========== inhibit exn 110628 ================================================ |
neuper@42067 | 213 |
============ inhibit exn 110628 ==============================================*) |
neuper@41943 | 214 |
|
neuper@41943 | 215 |
(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-. |
neuper@41943 | 216 |
-.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*) |
neuper@41975 | 217 |