7 |
7 |
8 12345678901234567890123456789012345678901234567890123456789012345678901234567890 |
8 12345678901234567890123456789012345678901234567890123456789012345678901234567890 |
9 10 20 30 40 50 60 70 80 |
9 10 20 30 40 50 60 70 80 |
10 *) |
10 *) |
11 |
11 |
12 theory Test_Isac imports Isac begin |
12 theory Test_Isac imports "Knowledge/Isac" begin |
13 |
13 |
14 ML{* writeln "**** run the tests **************************************" *}; |
14 ML{* writeln "**** run the tests **************************************" *}; |
15 ML {* Toplevel.debug := true; *} |
15 ML {* Toplevel.debug := true; *} |
16 (* |
16 (* |
17 cd "systest"; |
17 cd "systest"; |
29 ML{* writeln "**** run systests complete ******************************" *}; |
29 ML{* writeln "**** run systests complete ******************************" *}; |
30 (* |
30 (* |
31 cd"smltest/Scripts"; |
31 cd"smltest/Scripts"; |
32 *) |
32 *) |
33 use"../../../test/Tools/isac/ProgLang/termC.sml"; (*part.*) |
33 use"../../../test/Tools/isac/ProgLang/termC.sml"; (*part.*) |
34 |
|
35 use"../../../test/Tools/isac/ProgLang/calculate.sml"; (*part.*) |
34 use"../../../test/Tools/isac/ProgLang/calculate.sml"; (*part.*) |
36 |
35 |
37 use"../../../test/Tools/isac/ProgLang/rewrite.sml"; (*part.*) |
36 ML {*print_depth 999;*} |
|
37 use"../../../test/Tools/isac/ProgLang/rewrite.sml"; (*GOON*) |
38 (* |
38 (* |
39 use"listg.sml"; |
39 use"listg.sml"; |
40 use"scrtools.sml"; |
40 use"scrtools.sml"; |
41 use"tools.sml"; |
41 use"tools.sml"; |
42 cd "../.."; |
42 cd "../.."; |
43 cd"smltest/ME"; |
43 cd"smltest/ME"; |
44 use"ctree.sml"; |
|
45 *) |
44 *) |
|
45 use "../../../test/Tools/isac/Interpret/mstools.sml"; (*empty*) |
|
46 (* use"ctree.sml"; |
|
47 *) |
|
48 use "../../../test/Tools/isac/Interpret/ptyps.sml"; (*TODO*) |
46 use "../../../test/Tools/isac/Interpret/calchead.sml" (*part.*) |
49 use "../../../test/Tools/isac/Interpret/calchead.sml" (*part.*) |
47 (* |
50 (* |
48 use"calchead.sml"; |
51 use"calchead.sml"; |
49 use"rewtools.sml"; |
52 use"rewtools.sml"; |
50 use"solve.sml"; (*detailrls can notyet ackn. 'Rewrite_Set "cancel"' *); |
53 use"solve.sml"; (*detailrls can notyet ackn. 'Rewrite_Set "cancel"' *); |
61 use"interface.sml"; |
64 use"interface.sml"; |
62 cd "../.."; |
65 cd "../.."; |
63 *) |
66 *) |
64 ML{* writeln "**** run tests on math-engine complete ******************" *}; |
67 ML{* writeln "**** run tests on math-engine complete ******************" *}; |
65 (* |
68 (* |
66 cd"smltest/IsacKnowledge"; |
69 cd"smltest/IsacKnowledge"; ---below the order as in theoryy Isac--- |
67 use"atools.sml"; |
70 use"atools.sml"; |
68 use"complex.sml"; |
71 use"termorder.sml"; |
|
72 *) |
|
73 |
|
74 ML {* |
|
75 val t = str2term "(x^^^2 * x) is_multUnordered"; |
|
76 val pat = parse_patt (theory "Isac") "?p is_multUnordered"; |
|
77 *} |
|
78 ML {* |
|
79 val subst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty); |
|
80 Envir.subst_term subst (*pres?*); |
|
81 *} |
|
82 use"../../../test/Tools/isac/Knowledge/poly.sml"; (*part.*) |
|
83 (* |
|
84 use"rational.sml" |
|
85 use"equation.sml"; |
|
86 use"root.sml"; |
|
87 (*use"inssort.sml"; problems with recdef in Isabelle2002*) |
|
88 use"rooteq.sml"; |
|
89 use"rateq.sml"; |
|
90 use"rootrateq.sml"; |
|
91 |
|
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 *); |
|
97 use"wn.sml"; |
|
98 use"trig.sml"; |
|
99 use"logexp.sml"; |
69 use"diff.sml"; |
100 use"diff.sml"; |
70 use"diffapp.sml"; |
|
71 *) |
101 *) |
72 use "../../../test/Tools/isac/Knowledge/integrate.sml"; (*part.*) |
102 use "../../../test/Tools/isac/Knowledge/integrate.sml"; (*part.*) |
73 (* |
103 (* |
74 use"equation.sml"; |
104 use"eqsystem.sml"; |
75 (*use"inssort.sml"; problems with recdef in Isabelle2002*) |
|
76 use"logexp.sml"; |
|
77 *) |
|
78 use"../../../test/Tools/isac/Knowledge/poly.sml"; (*part.*) |
|
79 (* |
|
80 use"polyminus.sml"; |
105 use"polyminus.sml"; |
81 use"polyeq.sml"; (*TODO 31.b, n1., 44.a, 1.a~, 1.b (all'expanded')WN |
|
82 ? also check others without check 'diff.behav.'*); |
|
83 use"rateq.sml"; |
|
84 use"rational.sml" (*TODO add_fractions_p throws overflow-exn WN*); |
|
85 use"rlang.sml"; (*WN.12.6.03: for TODOs search 'writeln', |
|
86 for simplification search MG |
|
87 erls: 98a(1) 104a(1) 104a(2) 68a *); |
|
88 use"root.sml"; |
|
89 use"rooteq.sml"; |
|
90 use"rootrateq.sml"; |
|
91 use"termorder.sml"; |
|
92 use"trig.sml"; |
|
93 use"vect.sml"; |
106 use"vect.sml"; |
94 use"wn.sml"; |
107 use"diffapp.sml"; |
95 use"eqsystem.sml"; |
|
96 use"biegelinie.sml"; |
108 use"biegelinie.sml"; |
97 use"algein.sml"; |
109 use"algein.sml"; |
98 cd "../.."; |
110 cd "../.."; |
99 *) |
111 *) |
100 (* TODO |
112 (* TODO |