neuper@38024
|
1 |
(* Title Run_Tests on isac
|
neuper@38024
|
2 |
$ cd /usr/local/isabisac/test/Tools/isac
|
neuper@38024
|
3 |
$ /usr/local/isabisac/bin/isabelle emacs -l Isac Test_Isac.thy &
|
neuper@38024
|
4 |
|
neuper@38024
|
5 |
RESTART emacs after having created a new Isac heap.
|
neuper@38024
|
6 |
was sml/RTEST-root.sml in isac-2002
|
neuper@38024
|
7 |
|
neuper@38024
|
8 |
12345678901234567890123456789012345678901234567890123456789012345678901234567890
|
neuper@38024
|
9 |
10 20 30 40 50 60 70 80
|
neuper@38024
|
10 |
*)
|
neuper@38024
|
11 |
|
neuper@38036
|
12 |
theory Test_Isac imports "Knowledge/Isac" begin
|
neuper@38024
|
13 |
|
neuper@38024
|
14 |
ML{* writeln "**** run the tests **************************************" *};
|
neuper@38024
|
15 |
ML {* Toplevel.debug := true; *}
|
neuper@38024
|
16 |
(*
|
neuper@38024
|
17 |
cd "systest";
|
neuper@38024
|
18 |
(*+ check kbtest/diffapp.sml for additional items in met-model*)
|
neuper@38024
|
19 |
use"root-equ.sml";
|
neuper@38024
|
20 |
use"script.sml";
|
neuper@38024
|
21 |
(* use"script_if.sml"; WN03 missing: is_rootequation_in*)
|
neuper@38024
|
22 |
use"scriptnew.sml";
|
neuper@38024
|
23 |
use"subp-rooteq.sml";
|
neuper@38024
|
24 |
use"tacis.sml";
|
neuper@38024
|
25 |
use"interface-xml.sml";
|
neuper@38024
|
26 |
(* use"testdaten.sml"; no update after dropping 'errorBound'*)
|
neuper@38024
|
27 |
cd "../..";
|
neuper@38024
|
28 |
*)
|
neuper@38024
|
29 |
ML{* writeln "**** run systests complete ******************************" *};
|
neuper@38024
|
30 |
(*
|
neuper@38024
|
31 |
cd"smltest/Scripts";
|
neuper@38024
|
32 |
*)
|
neuper@38025
|
33 |
use"../../../test/Tools/isac/ProgLang/termC.sml"; (*part.*)
|
neuper@38025
|
34 |
use"../../../test/Tools/isac/ProgLang/calculate.sml"; (*part.*)
|
neuper@38032
|
35 |
|
neuper@38036
|
36 |
ML {*print_depth 999;*}
|
neuper@38036
|
37 |
use"../../../test/Tools/isac/ProgLang/rewrite.sml"; (*GOON*)
|
neuper@38024
|
38 |
(*
|
neuper@38024
|
39 |
use"listg.sml";
|
neuper@38024
|
40 |
use"scrtools.sml";
|
neuper@38024
|
41 |
use"tools.sml";
|
neuper@38024
|
42 |
cd "../..";
|
neuper@38024
|
43 |
cd"smltest/ME";
|
neuper@38024
|
44 |
*)
|
neuper@38036
|
45 |
use "../../../test/Tools/isac/Interpret/mstools.sml"; (*empty*)
|
neuper@38036
|
46 |
(* use"ctree.sml";
|
neuper@38036
|
47 |
*)
|
neuper@38036
|
48 |
use "../../../test/Tools/isac/Interpret/ptyps.sml"; (*TODO*)
|
neuper@38025
|
49 |
use "../../../test/Tools/isac/Interpret/calchead.sml" (*part.*)
|
neuper@38024
|
50 |
(*
|
neuper@38024
|
51 |
use"calchead.sml";
|
neuper@38024
|
52 |
use"rewtools.sml";
|
neuper@38024
|
53 |
use"solve.sml"; (*detailrls can notyet ackn. 'Rewrite_Set "cancel"' *);
|
neuper@38024
|
54 |
use"inform.sml";
|
neuper@38024
|
55 |
use"me.sml";
|
neuper@38024
|
56 |
use"ptyps.sml";
|
neuper@38024
|
57 |
cd "../..";
|
neuper@38024
|
58 |
cd"smltest/xmlsrc";
|
neuper@38024
|
59 |
use"datatypes.sml";
|
neuper@38024
|
60 |
use"pbl-met-hierarchy.sml";
|
neuper@38024
|
61 |
use"thy-hierarchy.sml";
|
neuper@38024
|
62 |
cd "../..";
|
neuper@38024
|
63 |
cd"smltest/FE-interface";
|
neuper@38024
|
64 |
use"interface.sml";
|
neuper@38024
|
65 |
cd "../..";
|
neuper@38024
|
66 |
*)
|
neuper@38024
|
67 |
ML{* writeln "**** run tests on math-engine complete ******************" *};
|
neuper@38024
|
68 |
(*
|
neuper@38036
|
69 |
cd"smltest/IsacKnowledge"; ---below the order as in theoryy Isac---
|
neuper@38024
|
70 |
use"atools.sml";
|
neuper@38036
|
71 |
use"termorder.sml";
|
neuper@38036
|
72 |
*)
|
neuper@38036
|
73 |
|
neuper@38036
|
74 |
ML {*
|
neuper@38036
|
75 |
val t = str2term "(x^^^2 * x) is_multUnordered";
|
neuper@38036
|
76 |
val pat = parse_patt (theory "Isac") "?p is_multUnordered";
|
neuper@38036
|
77 |
*}
|
neuper@38036
|
78 |
ML {*
|
neuper@38036
|
79 |
val subst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
|
neuper@38036
|
80 |
Envir.subst_term subst (*pres?*);
|
neuper@38036
|
81 |
*}
|
neuper@38036
|
82 |
use"../../../test/Tools/isac/Knowledge/poly.sml"; (*part.*)
|
neuper@38036
|
83 |
(*
|
neuper@38036
|
84 |
use"rational.sml"
|
neuper@38036
|
85 |
use"equation.sml";
|
neuper@38036
|
86 |
use"root.sml";
|
neuper@38036
|
87 |
(*use"inssort.sml"; problems with recdef in Isabelle2002*)
|
neuper@38036
|
88 |
use"rooteq.sml";
|
neuper@38036
|
89 |
use"rateq.sml";
|
neuper@38036
|
90 |
use"rootrateq.sml";
|
neuper@38036
|
91 |
|
neuper@38036
|
92 |
use"polyeq.sml"; (*TODO 31.b, n1., 44.a, 1.a~, 1.b (all'expanded')WN
|
neuper@38036
|
93 |
? also check others without check 'diff.behav.'*);
|
neuper@38036
|
94 |
use"rlang.sml"; (*WN.12.6.03: for TODOs search 'writeln',
|
neuper@38036
|
95 |
for simplification search MG
|
neuper@38036
|
96 |
erls: 98a(1) 104a(1) 104a(2) 68a *);
|
neuper@38036
|
97 |
use"wn.sml";
|
neuper@38036
|
98 |
use"trig.sml";
|
neuper@38036
|
99 |
use"logexp.sml";
|
neuper@38024
|
100 |
use"diff.sml";
|
neuper@38030
|
101 |
*)
|
neuper@38030
|
102 |
use "../../../test/Tools/isac/Knowledge/integrate.sml"; (*part.*)
|
neuper@38030
|
103 |
(*
|
neuper@38036
|
104 |
use"eqsystem.sml";
|
neuper@38024
|
105 |
use"polyminus.sml";
|
neuper@38024
|
106 |
use"vect.sml";
|
neuper@38036
|
107 |
use"diffapp.sml";
|
neuper@38024
|
108 |
use"biegelinie.sml";
|
neuper@38024
|
109 |
use"algein.sml";
|
neuper@38024
|
110 |
cd "../..";
|
neuper@38024
|
111 |
*)
|
neuper@38024
|
112 |
(* TODO
|
neuper@38024
|
113 |
use_thy "../../Tools/isac/ADDTESTS/file-depend/Build_Test"
|
neuper@38024
|
114 |
|
neuper@38024
|
115 |
*** Could not find theory file "Foo_Language.thy" in "1language", "/usr/local/isabisac/test/Tools/isac", ".", "$ISABELLE_HOME/src/HOL/Library"
|
neuper@38024
|
116 |
*** Theory loader: the error(s) above occurred while examining theory "Foo_Language"
|
neuper@38024
|
117 |
|
neuper@38024
|
118 |
use_thy "../../Tools/isac/ADDTESTS/trace-rewrite/Build_Test"
|
neuper@38024
|
119 |
*)
|
neuper@38025
|
120 |
use_thy "../../../test/Pure/Isar/Test_Parse_Term"
|
neuper@38025
|
121 |
use_thy "../../../test/Pure/Isar/Test_Parsers"
|
neuper@38024
|
122 |
|
neuper@38024
|
123 |
ML{* writeln "**** run tests on IsacKnowledge complete ****************" *};
|
neuper@38024
|
124 |
(*
|
neuper@38025
|
125 |
val path = "/home/neuper/proto3/testsml2xml/";
|
neuper@38024
|
126 |
pbl_hierarchy2file (path ^ "pbl/");
|
neuper@38024
|
127 |
pbls2file (path ^ "pbl/");
|
neuper@38024
|
128 |
met_hierarchy2file (path ^ "met/");
|
neuper@38024
|
129 |
mets2file (path ^ "met/");
|
neuper@38024
|
130 |
thy_hierarchy2file (path ^ "thy/");
|
neuper@38024
|
131 |
thes2file (path ^ "thy/");
|
neuper@38024
|
132 |
cd"sml";
|
neuper@38024
|
133 |
*)
|
neuper@38024
|
134 |
ML{* writeln "**** tested creation of xmldata *************************" *};
|
neuper@38024
|
135 |
|
neuper@38024
|
136 |
ML{*states:=[];
|
neuper@38024
|
137 |
writeln "=========================================================";
|
neuper@38024
|
138 |
|
neuper@38024
|
139 |
writeln "**** run systests complete ***************** re-organize!";
|
neuper@38024
|
140 |
writeln "**** run tests on math-engine complete ******************";
|
neuper@38024
|
141 |
writeln "**** run tests on IsacKnowledge complete ****************";
|
neuper@38024
|
142 |
writeln "**** build isac kernel + run tests complete *************";
|
neuper@38024
|
143 |
writeln "**** tested creation of xmldata *************************";
|
neuper@38024
|
144 |
*}
|
neuper@38024
|
145 |
|
neuper@38024
|
146 |
end
|