intermed. 'fun parse_patt' fixes types to real (like 'parse')
this was on the way to repair rewrite (prepat in Rrls)
1 (* Title Run_Tests on isac
2 $ cd /usr/local/isabisac/test/Tools/isac
3 $ /usr/local/isabisac/bin/isabelle emacs -l Isac Test_Isac.thy &
5 RESTART emacs after having created a new Isac heap.
6 was sml/RTEST-root.sml in isac-2002
8 12345678901234567890123456789012345678901234567890123456789012345678901234567890
9 10 20 30 40 50 60 70 80
12 theory Test_Isac imports "Knowledge/Isac" begin
14 ML{* writeln "**** run the tests **************************************" *};
15 ML {* Toplevel.debug := true; *}
18 (*+ check kbtest/diffapp.sml for additional items in met-model*)
21 (* use"script_if.sml"; WN03 missing: is_rootequation_in*)
25 use"interface-xml.sml";
26 (* use"testdaten.sml"; no update after dropping 'errorBound'*)
29 ML{* writeln "**** run systests complete ******************************" *};
33 use"../../../test/Tools/isac/ProgLang/termC.sml"; (*part.*)
34 use"../../../test/Tools/isac/ProgLang/calculate.sml"; (*part.*)
36 ML {*print_depth 999;*}
37 use"../../../test/Tools/isac/ProgLang/rewrite.sml"; (*GOON*)
45 use "../../../test/Tools/isac/Interpret/mstools.sml"; (*empty*)
48 use "../../../test/Tools/isac/Interpret/ptyps.sml"; (*TODO*)
49 use "../../../test/Tools/isac/Interpret/calchead.sml" (*part.*)
53 use"solve.sml"; (*detailrls can notyet ackn. 'Rewrite_Set "cancel"' *);
60 use"pbl-met-hierarchy.sml";
61 use"thy-hierarchy.sml";
63 cd"smltest/FE-interface";
67 ML{* writeln "**** run tests on math-engine complete ******************" *};
69 cd"smltest/IsacKnowledge"; ---below the order as in theoryy Isac---
75 val t = str2term "(x^^^2 * x) is_multUnordered";
76 val pat = parse_patt (theory "Isac") "?p is_multUnordered";
79 val subst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
80 Envir.subst_term subst (*pres?*);
82 use"../../../test/Tools/isac/Knowledge/poly.sml"; (*part.*)
87 (*use"inssort.sml"; problems with recdef in Isabelle2002*)
92 use"polyeq.sml"; (*TODO 31.b, n1., 44.a, 1.a~, 1.b (all'expanded')WN
93 ? also check others without check 'diff.behav.'*);
94 use"rlang.sml"; (*WN.12.6.03: for TODOs search 'writeln',
95 for simplification search MG
96 erls: 98a(1) 104a(1) 104a(2) 68a *);
102 use "../../../test/Tools/isac/Knowledge/integrate.sml"; (*part.*)
106 use "../../../test/Tools/isac/Knowledge/polyminus.sml"; (*part.*)
115 use_thy "../../Tools/isac/ADDTESTS/file-depend/Build_Test"
117 *** Could not find theory file "Foo_Language.thy" in "1language", "/usr/local/isabisac/test/Tools/isac", ".", "$ISABELLE_HOME/src/HOL/Library"
118 *** Theory loader: the error(s) above occurred while examining theory "Foo_Language"
120 use_thy "../../Tools/isac/ADDTESTS/trace-rewrite/Build_Test"
122 use_thy "../../../test/Pure/Isar/Test_Parse_Term"
123 use_thy "../../../test/Pure/Isar/Test_Parsers"
125 ML{* writeln "**** run tests on IsacKnowledge complete ****************" *};
127 val path = "/home/neuper/proto3/testsml2xml/";
128 pbl_hierarchy2file (path ^ "pbl/");
129 pbls2file (path ^ "pbl/");
130 met_hierarchy2file (path ^ "met/");
131 mets2file (path ^ "met/");
132 thy_hierarchy2file (path ^ "thy/");
133 thes2file (path ^ "thy/");
136 ML{* writeln "**** tested creation of xmldata *************************" *};
139 writeln "=========================================================";
141 writeln "**** run systests complete ***************** re-organize!";
142 writeln "**** run tests on math-engine complete ******************";
143 writeln "**** run tests on IsacKnowledge complete ****************";
144 writeln "**** build isac kernel + run tests complete *************";
145 writeln "**** tested creation of xmldata *************************";