test/Tools/isac/Test_Isac.thy
author Walther Neuper <neuper@ist.tugraz.at>
Tue, 18 Jun 2013 17:56:09 +0200
changeset 48885 75b869e7b009
parent 48884 b933b88a268a
child 48888 4eb0d1968d46
permissions -rwxr-xr-x
tuned
     1 (* Title:  All tests on isac; observe outcommented
     2    Author: Walther Neuper 101001
     3    (c) copyright due to lincense terms.
     4 
     5 $ cd /usr/local/isabisac/test/Tools/isac
     6 $ /usr/local/isabisac/bin/isabelle jedit -l Isac Test_Isac.thy &
     7 *)
     8 
     9 theory Test_Isac imports
    10   "~~/src/Tools/isac/Frontend/Isac"
    11 (*Isac
    12 OUTCOMMENT THE ABOVE AND SET <Prover Session> <Isac> (INSTEAD OF 'HOL')*)
    13 (*"Knowledge/Rational_Test" ...THIS FILE HAS DISAPPEARED*)
    14   "ADDTESTS/Ctxt"
    15   "ADDTESTS/test-depend/Build_Test"
    16   "ADDTESTS/All_Ctxt"
    17   "ADDTESTS/course/phst11/T1_Basics"
    18   "ADDTESTS/course/phst11/T2_Rewriting"
    19   "ADDTESTS/course/phst11/T3_MathEngine"
    20   "ADDTESTS/file-depend/Build_Test"
    21   "ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform"
    22   "../../Pure/Isar/Test_Parsers"
    23 (*"../../Pure/Isar/Pure/Isar/Struct_Deriv" update 2009-2-->2011*)
    24   "../../Pure/Isar/Test_Parse_Term"
    25 
    26 uses 
    27   (         "library.sml")
    28   (         "calcelems.sml")
    29   ("ProgLang/termC.sml")      
    30   ("ProgLang/calculate.sml")
    31   ("ProgLang/rewrite.sml")
    32   ("ProgLang/listC.sml")
    33   ("ProgLang/scrtools.sml")
    34   ("ProgLang/tools.sml")
    35 
    36   ("Minisubpbl/000-comments.sml")
    37   ("Minisubpbl/100-init-rootpbl.sml")
    38   ("Minisubpbl/150-add-given.sml")
    39   ("Minisubpbl/200-start-method.sml")
    40   ("Minisubpbl/300-init-subpbl.sml")
    41   ("Minisubpbl/400-start-meth-subpbl.sml")
    42   ("Minisubpbl/490-nxt-Check_Postcond.sml")
    43   ("Minisubpbl/500-met-sub-to-root.sml")
    44   ("Minisubpbl/530-error-Check_Elementwise.sml")
    45   ("Minisubpbl/600-postcond.sml")
    46 
    47   ("Interpret/mstools.sml") 
    48   ("Interpret/ctree.sml")
    49   ("Interpret/ptyps.sml") 
    50   ("Interpret/generate.sml")
    51   ("Interpret/calchead.sml") 
    52   ("Interpret/appl.sml")
    53   ("Interpret/rewtools.sml") 
    54   ("Interpret/script.sml")
    55   ("Interpret/solve.sml") 
    56   ("Interpret/inform.sml")
    57   ("Interpret/mathengine.sml")
    58 
    59   ("xmlsrc/mathml.sml")
    60   ("xmlsrc/datatypes.sml")
    61   ("xmlsrc/pbl-met-hierarchy.sml")
    62   ("xmlsrc/thy-hierarchy.sml")
    63   ("xmlsrc/interface-xml.sml")
    64 
    65   ("Frontend/messages.sml")
    66   ("Frontend/states.sml")
    67   ("Frontend/interface.sml")
    68   ("print_exn_G.sml")
    69 
    70   ("Knowledge/delete.sml")
    71   ("Knowledge/descript.sml")
    72   ("Knowledge/atools.sml")
    73   ("Knowledge/simplify.sml")
    74   ("Knowledge/poly.sml")
    75 (*THIS WAITS UNTIL Isabelle2013: ("Knowledge/gcd_poly.sml") ("Knowledge/gcd_poly_winkler.sml")
    76   IN THIS SEQUENCE: SEE Test_Some2.thy*)
    77   ("Knowledge/rational.sml")
    78   ("Knowledge/equation.sml")
    79   ("Knowledge/root.sml")
    80   ("Knowledge/lineq.sml")
    81   ("Knowledge/rooteq.sml")
    82   ("Knowledge/rateq.sml")
    83   ("Knowledge/rootrateq.sml")
    84   ("Knowledge/polyeq.sml")
    85   ("Knowledge/calculus.sml")
    86   ("Knowledge/trig.sml")
    87   ("Knowledge/logexp.sml")
    88   ("Knowledge/diff.sml")
    89   ("Knowledge/integrate.sml")
    90   ("Knowledge/eqsystem.sml")
    91   ("Knowledge/test.sml")
    92   ("Knowledge/partial_fractions.sml")
    93   ("Knowledge/polyminus.sml")
    94   ("Knowledge/vect.sml")
    95   ("Knowledge/diffapp.sml")
    96   ("Knowledge/biegelinie.sml")
    97   ("Knowledge/algein.sml")
    98   ("Knowledge/diophanteq.sml")
    99   ("Knowledge/Inverse_Z_Transform/inverse_z_transform.sml")
   100   ("Knowledge/isac.sml")
   101   ("Knowledge/build_thydata.sml")
   102 
   103 begin
   104 
   105   ML {*"%%%%%%%%%%%%%%%%% start ProgLang.thy %%%%%%%%%%%%%%%%%%%";*}  
   106   use          "library.sml"
   107   use          "calcelems.sml"
   108   use "ProgLang/termC.sml"
   109   use "ProgLang/calculate.sml"
   110   use "ProgLang/rewrite.sml"
   111 (*use "ProgLang/listC.sml"            2002*)
   112   use "ProgLang/scrtools.sml"
   113   use "ProgLang/tools.sml"
   114   ML {*"%%%%%%%%%%%%%%%%% end ProgLang.thy %%%%%%%%%%%%%%%%%%%%%";*}
   115   ML {*"%%%%%%%%%%%%%%%%% start Minisubpbl %%%%%%%%%%%%%%%%%%%%%";*}
   116   use "Minisubpbl/000-comments.sml"
   117   use "Minisubpbl/100-init-rootpbl.sml"
   118   use "Minisubpbl/150-add-given.sml"
   119   use "Minisubpbl/200-start-method.sml"
   120   use "Minisubpbl/300-init-subpbl.sml"
   121   use "Minisubpbl/400-start-meth-subpbl.sml"
   122   use "Minisubpbl/490-nxt-Check_Postcond.sml"
   123   use "Minisubpbl/500-met-sub-to-root.sml"
   124   use "Minisubpbl/530-error-Check_Elementwise.sml"
   125   use "Minisubpbl/600-postcond.sml"
   126   ML {*"%%%%%%%%%%%%%%%%% end Minisubpbl.thy %%%%%%%%%%%%%%%%%%%%%%%";*}
   127   ML {*"%%%%%%%%%%%%%%%%% start Interpret.thy %%%%%%%%%%%%%%%%%%";*}
   128   use "Interpret/mstools.sml"
   129   use "Interpret/ctree.sml"         (*!...!see(25)*)
   130   use "Interpret/ptyps.sml"
   131   ML {* check_unsynchronized_ref (); (*========= on error: CUT AND PASTE THIS LINE =========*) *}
   132   use "Interpret/generate.sml"
   133   use "Interpret/calchead.sml"      (*part.*)
   134   use "Interpret/appl.sml"          (*!complete WEGEN INTERMED TESTCODE*)
   135   use "Interpret/rewtools.sml"      (*TODO/part.WN120406*)
   136   use "Interpret/script.sml"        (*!TODO/part.*)
   137   use "Interpret/solve.sml"         (*part.*)
   138   use "Interpret/inform.sml"        (*part.*)
   139   use "Interpret/mathengine.sml"    (*!part.*)
   140   ML {*"%%%%%%%%%%%%%%%%% end Interpret.thy %%%%%%%%%%%%%%%%%%%%";*}
   141   ML {*"%%%%%%%%%%%%%%%%% start xmlsrc.thy %%%%%%%%%%%%%%%%%%%%%";*}
   142   use "xmlsrc/mathml.sml"            (*part.*)
   143   use "xmlsrc/datatypes.sml"         (*TODO/part.*)
   144   use "xmlsrc/pbl-met-hierarchy.sml" (*TODO after 2009-2/part.*)
   145   use "xmlsrc/thy-hierarchy.sml"     (*TODO after 2009-2/part.*)
   146   use "xmlsrc/interface-xml.sml"     (*TODO after 2009-2*)
   147   ML {*"%%%%%%%%%%%%%%%%% end xmlsrc.thy %%%%%%%%%%%%%%%%%%%%%%%";*}
   148   ML {*"%%%%%%%%%%%%%%%%% start Frontend.thy %%%%%%%%%%%%%%%%%%%";*}
   149   use "Frontend/messages.sml"
   150   use "Frontend/states.sml"
   151   use "Frontend/interface.sml"
   152   use          "print_exn_G.sml"
   153   ML {*"%%%%%%%%%%%%%%%%% end Frontend.thy %%%%%%%%%%%%%%%%%%%%%";*}
   154   ML {*"%%%%%%%%%%%%%%%%% start Knowledge.thy %%%%%%%%%%%%%%%%%%";*}
   155   use "Knowledge/delete.sml"
   156   use "Knowledge/descript.sml"
   157   use "Knowledge/atools.sml"
   158   use "Knowledge/simplify.sml"
   159   use "Knowledge/poly.sml"
   160 (*THIS WAITS UNTIL Isabelle2013 IN THIS SEQUENCE (SEE Test_Some2.thy):0
   161   use "Knowledge/gcd_poly.sml" (*type error 'nth' etc*)
   162   use "Knowledge/gcd_poly_winkler.sml"*)
   163 (*use "Knowledge/rational.sml"  WN120317.TODO postponed to joint work with dmeindl *)
   164   use "Knowledge/equation.sml"
   165   use "Knowledge/root.sml"
   166   use "Knowledge/lineq.sml"
   167 (*use "Knowledge/rooteq.sml"    some complicated equations not recovered from 2002 *)
   168   use "Knowledge/rateq.sml"   (*some complicated equations not recovered from 2002 *)
   169   use "Knowledge/rootrat.sml"
   170   use "Knowledge/rootrateq.sml"(*ome complicated equations not recovered from 2002 *)
   171   use "Knowledge/partial_fractions.sml"
   172   use "Knowledge/polyeq.sml"
   173 (*use "Knowledge/rlang.sml"     much to clean up, not urgent due to similar tests  *)
   174   use "Knowledge/calculus.sml"
   175   use "Knowledge/trig.sml"
   176 (*use "Knowledge/logexp.sml"    not included as stuff for presentation of authoring*) 
   177   use "Knowledge/diff.sml"
   178   use "Knowledge/integrate.sml"
   179   use "Knowledge/eqsystem.sml"
   180   use "Knowledge/test.sml"
   181   use "Knowledge/polyminus.sml"
   182   use "Knowledge/vect.sml"
   183   use "Knowledge/diffapp.sml"        (* postponed to dev. specification | TP-prog. *)
   184   use "Knowledge/biegelinie.sml"
   185   use "Knowledge/algein.sml"
   186   use "Knowledge/diophanteq.sml"
   187   use "Knowledge/Inverse_Z_Transform/inverse_z_transform.sml"
   188   use "Knowledge/isac.sml"
   189   use "Knowledge/build_thydata.sml"
   190   ML {*"%%%%%%%%%%%%%%%%% end Knowledge.thy %%%%%%%%%%%%%%%%%%%%";*}
   191   ML {*"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";*}
   192   ML {*"%%%%%%%%%%%%%%%%% all tests successful %%%%%%%%%%%%%%%%%";*}
   193   ML {*"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";*}
   194 
   195 end
   196 (*========== inhibit exn 110628 ================================================
   197 ============ inhibit exn 110628 ==============================================*)
   198 
   199 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
   200 -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
   201