1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/Tools/isac/Test_Isac.thy Mon Sep 27 13:35:06 2010 +0200
1.3 @@ -0,0 +1,148 @@
1.4 +(* Title Run_Tests on isac
1.5 +$ cd /usr/local/isabisac/test/Tools/isac
1.6 +$ /usr/local/isabisac/bin/isabelle emacs -l Isac Test_Isac.thy &
1.7 +
1.8 +RESTART emacs after having created a new Isac heap.
1.9 +was sml/RTEST-root.sml in isac-2002
1.10 +
1.11 +12345678901234567890123456789012345678901234567890123456789012345678901234567890
1.12 + 10 20 30 40 50 60 70 80
1.13 +*)
1.14 +
1.15 +theory Test_Isac imports Isac begin
1.16 +
1.17 +ML{* writeln "**** run the tests **************************************" *};
1.18 +ML {* Toplevel.debug := true; *}
1.19 +(*
1.20 +cd "systest";
1.21 +(*+ check kbtest/diffapp.sml for additional items in met-model*)
1.22 + use"root-equ.sml";
1.23 + use"script.sml";
1.24 + (* use"script_if.sml"; WN03 missing: is_rootequation_in*)
1.25 + use"scriptnew.sml";
1.26 + use"subp-rooteq.sml";
1.27 + use"tacis.sml";
1.28 + use"interface-xml.sml";
1.29 + (* use"testdaten.sml"; no update after dropping 'errorBound'*)
1.30 + cd "../..";
1.31 +*)
1.32 +ML{* writeln "**** run systests complete ******************************" *};
1.33 +
1.34 +ML {*
1.35 +val t1 = @{term "1+2::real"};
1.36 +val t2 = @{term "abc"};
1.37 +term2str t2 = "abc";
1.38 +fun terms2str ts = (strs2str o (map term2str )) ts;
1.39 +terms2str [t1,t2] = "[\"1 + 2\",\"abc\"]";
1.40 +fun terms2str' ts = (strs2str' o (map term2str )) ts;
1.41 +terms2str' [t1,t2] = "[1 + 2,abc]";
1.42 +fun terms2strs ts = (map term2str) ts;
1.43 +terms2strs [t1,t2] = ["1 + 2", "abc"];
1.44 +*}
1.45 +
1.46 +(*
1.47 +cd"smltest/Scripts";
1.48 + use"calculate-float.sml";
1.49 +*)
1.50 +use"ProgLang/calculate.sml"; (*part.*)
1.51 +(*
1.52 + use"listg.sml";
1.53 +*)
1.54 +use"ProgLang/rewrite.sml"; (*part.*)
1.55 +(*
1.56 + use"scrtools.sml";
1.57 + use"term.sml";
1.58 + use"tools.sml";
1.59 + cd "../..";
1.60 +cd"smltest/ME";
1.61 + use"ctree.sml";
1.62 +*)
1.63 +use "Interpret/calchead.sml" (*part.*)
1.64 +(*
1.65 + use"calchead.sml";
1.66 + use"rewtools.sml";
1.67 + use"solve.sml"; (*detailrls can notyet ackn. 'Rewrite_Set "cancel"' *);
1.68 + use"inform.sml";
1.69 + use"me.sml";
1.70 + use"ptyps.sml";
1.71 + cd "../..";
1.72 +cd"smltest/xmlsrc";
1.73 + use"datatypes.sml";
1.74 + use"pbl-met-hierarchy.sml";
1.75 + use"thy-hierarchy.sml";
1.76 + cd "../..";
1.77 +cd"smltest/FE-interface";
1.78 + use"interface.sml";
1.79 + cd "../..";
1.80 +*)
1.81 +ML{* writeln "**** run tests on math-engine complete ******************" *};
1.82 +(*
1.83 +cd"smltest/IsacKnowledge";
1.84 + use"atools.sml";
1.85 + use"complex.sml";
1.86 + use"diff.sml";
1.87 + use"diffapp.sml";
1.88 +(**)
1.89 +use "Knowledge/integrate.sml"; (*part.*)
1.90 +
1.91 + use"equation.sml";
1.92 + (*use"inssort.sml"; problems with recdef in Isabelle2002*)
1.93 + use"logexp.sml";
1.94 +*)
1.95 +use"Knowledge/poly.sml"; (*part.*)
1.96 +(*
1.97 + use"polyminus.sml";
1.98 + use"polyeq.sml"; (*TODO 31.b, n1., 44.a, 1.a~, 1.b (all'expanded')WN
1.99 + ? also check others without check 'diff.behav.'*);
1.100 + use"rateq.sml";
1.101 + use"rational.sml" (*TODO add_fractions_p throws overflow-exn WN*);
1.102 + use"rlang.sml"; (*WN.12.6.03: for TODOs search 'writeln',
1.103 + for simplification search MG
1.104 + erls: 98a(1) 104a(1) 104a(2) 68a *);
1.105 + use"root.sml";
1.106 + use"rooteq.sml";
1.107 + use"rootrateq.sml";
1.108 + use"termorder.sml";
1.109 + use"trig.sml";
1.110 + use"vect.sml";
1.111 + use"wn.sml";
1.112 + use"eqsystem.sml";
1.113 + use"biegelinie.sml";
1.114 + use"algein.sml";
1.115 + cd "../..";
1.116 +*)
1.117 +(* TODO
1.118 +use_thy "../../Tools/isac/ADDTESTS/file-depend/Build_Test"
1.119 +
1.120 +*** Could not find theory file "Foo_Language.thy" in "1language", "/usr/local/isabisac/test/Tools/isac", ".", "$ISABELLE_HOME/src/HOL/Library"
1.121 +*** Theory loader: the error(s) above occurred while examining theory "Foo_Language"
1.122 +
1.123 +use_thy "../../Tools/isac/ADDTESTS/trace-rewrite/Build_Test"
1.124 +*)
1.125 +use_thy "../../Pure/Isar/Test_Parse_Term"
1.126 +use_thy "../../Pure/Isar/Test_Parsers"
1.127 +
1.128 +ML{* writeln "**** run tests on IsacKnowledge complete ****************" *};
1.129 +(*
1.130 +val path = "/home/neuper/proto2/testsml2xml/";
1.131 +pbl_hierarchy2file (path ^ "pbl/");
1.132 +pbls2file (path ^ "pbl/");
1.133 +met_hierarchy2file (path ^ "met/");
1.134 +mets2file (path ^ "met/");
1.135 +thy_hierarchy2file (path ^ "thy/");
1.136 +thes2file (path ^ "thy/");
1.137 +cd"sml";
1.138 +*)
1.139 +ML{* writeln "**** tested creation of xmldata *************************" *};
1.140 +
1.141 +ML{*states:=[];
1.142 + writeln "=========================================================";
1.143 +
1.144 + writeln "**** run systests complete ***************** re-organize!";
1.145 + writeln "**** run tests on math-engine complete ******************";
1.146 + writeln "**** run tests on IsacKnowledge complete ****************";
1.147 + writeln "**** build isac kernel + run tests complete *************";
1.148 + writeln "**** tested creation of xmldata *************************";
1.149 +*}
1.150 +
1.151 +end