|
neuper@37906
|
1 |
(* tests on simplification
|
|
neuper@37906
|
2 |
author: Walther Neuper
|
|
neuper@37906
|
3 |
061019
|
|
neuper@37906
|
4 |
(c) due to copyright terms
|
|
neuper@37906
|
5 |
|
|
neuper@37906
|
6 |
use"../smltest/IsacKnowledge/simplify.sml";
|
|
neuper@37906
|
7 |
use"simplify.sml";
|
|
neuper@37906
|
8 |
*)
|
|
neuper@37906
|
9 |
|
|
neuper@38066
|
10 |
"--------------------------------------------------------";
|
|
neuper@38066
|
11 |
"--------------------------------------------------------";
|
|
neuper@38066
|
12 |
"table of contents --------------------------------------";
|
|
neuper@38066
|
13 |
"--------------------------------------------------------";
|
|
neuper@38066
|
14 |
"----------- CAS-command Simplify -----------------------";
|
|
neuper@38066
|
15 |
"----------- append inform with final result ------------";
|
|
neuper@38066
|
16 |
"--------------------------------------------------------";
|
|
neuper@38066
|
17 |
"--------------------------------------------------------";
|
|
neuper@38066
|
18 |
"--------------------------------------------------------";
|
|
neuper@37906
|
19 |
|
|
neuper@42396
|
20 |
val thy = @{theory "Simplify"};
|
|
neuper@37906
|
21 |
|
|
neuper@38066
|
22 |
"----------- CAS-command Simplify -----------------------";
|
|
neuper@38066
|
23 |
"----------- CAS-command Simplify -----------------------";
|
|
neuper@38066
|
24 |
"----------- CAS-command Simplify -----------------------";
|
|
neuper@42400
|
25 |
(*============ inhibit exn WN120321 ==============================================
|
|
neuper@42400
|
26 |
WN120321.TODO reanimate test/../simplify.sml: CAS-command Simplify
|
|
neuper@42400
|
27 |
|
|
neuper@37906
|
28 |
states:=[];
|
|
neuper@37906
|
29 |
CalcTree [([], ("e_domID", ["e_pblID"], ["e_metID"]))];
|
|
neuper@37906
|
30 |
Iterator 1;
|
|
neuper@37906
|
31 |
moveActiveRoot 1;
|
|
neuper@37906
|
32 |
replaceFormula 1 "Simplify (2*a + 3*a)";
|
|
neuper@37906
|
33 |
autoCalculate 1 (Step 1);
|
|
neuper@37906
|
34 |
autoCalculate 1 CompleteCalc;
|
|
neuper@37906
|
35 |
val ((pt,p),_) = get_calc 1;
|
|
neuper@38066
|
36 |
val Form res = (#1 o pt_extract) (pt, ([],Res)); show_pt pt; term2str res;
|
|
neuper@37906
|
37 |
if p = ([], Res) andalso term2str res = "5 * a" then ()
|
|
neuper@38031
|
38 |
else error "simplify.sml: diff.behav. CAScmd: Simplify (2*a + 3*a)";
|
|
neuper@42400
|
39 |
============ inhibit exn WN120321 ==============================================*)
|
|
neuper@37906
|
40 |
|
|
neuper@37906
|
41 |
|
|
neuper@38066
|
42 |
"----------- append inform with final result ------------";
|
|
neuper@38066
|
43 |
"----------- append inform with final result ------------";
|
|
neuper@38066
|
44 |
"----------- append inform with final result ------------";
|
|
neuper@37906
|
45 |
states:=[];
|
|
neuper@38083
|
46 |
CalcTree [(["Term ((14 * x * y) / ( x * y ))", "normalform N"],
|
|
neuper@52105
|
47 |
("Rational", ["rational","simplification"], ["simplification","of_rationals"]))];
|
|
neuper@37906
|
48 |
Iterator 1;
|
|
neuper@37906
|
49 |
moveActiveRoot 1;
|
|
neuper@37906
|
50 |
autoCalculate 1 CompleteCalcHead;
|
|
neuper@52105
|
51 |
val ((pt,p),_) = get_calc 1; show_pt pt;
|
|
neuper@52105
|
52 |
(*[
|
|
neuper@52105
|
53 |
(([], Frm), Simplify (14 * x * y / (x * y)))] *)
|
|
neuper@52105
|
54 |
pt_extract (pt, p); (*determines SOME (Apply_Method ["simplification", "of_rationals"])*)
|
|
neuper@38065
|
55 |
|
|
neuper@37906
|
56 |
autoCalculate 1 (Step 1);
|
|
neuper@52105
|
57 |
val ((pt,p),_) = get_calc 1; show_pt pt;
|
|
neuper@52105
|
58 |
(*[
|
|
neuper@52105
|
59 |
(([], Frm), Simplify (14 * x * y / (x * y))),
|
|
neuper@52105
|
60 |
(([1], Frm), 14 * x * y / (x * y))] *)
|
|
neuper@38065
|
61 |
|
|
neuper@37906
|
62 |
appendFormula 1 "14";
|
|
neuper@37906
|
63 |
val ((pt,p),_) = get_calc 1; show_pt pt;
|
|
neuper@52105
|
64 |
(*[
|
|
neuper@52105
|
65 |
(([], Frm), Simplify (14 * x * y / (x * y))),
|
|
neuper@52105
|
66 |
(([1], Frm), 14 * x * y / (x * y)),
|
|
neuper@52105
|
67 |
(([1,1], Frm), 14 * x * y / (x * y)),
|
|
neuper@52105
|
68 |
(([1,1], Res), 14 * (x * y) / (x * y)),
|
|
neuper@52105
|
69 |
(([1,2], Res), 14 / 1),
|
|
neuper@52105
|
70 |
(([1,3], Res), 14),
|
|
neuper@52105
|
71 |
(([1], Res), 14)]*)
|
|
neuper@37906
|
72 |
|
|
neuper@37906
|
73 |
autoCalculate 1 (Step 1);
|
|
neuper@37906
|
74 |
val ((pt,p),_) = get_calc 1; show_pt pt;
|
|
neuper@52105
|
75 |
(*[
|
|
neuper@52105
|
76 |
(([], Frm), Simplify (14 * x * y / (x * y))),
|
|
neuper@52105
|
77 |
(([1], Frm), 14 * x * y / (x * y)),
|
|
neuper@52105
|
78 |
(([1,1], Frm), 14 * x * y / (x * y)),
|
|
neuper@52105
|
79 |
(([1,1], Res), 14 * (x * y) / (x * y)),
|
|
neuper@52105
|
80 |
(([1,2], Res), 14 / 1),
|
|
neuper@52105
|
81 |
(([1,3], Res), 14),
|
|
neuper@52105
|
82 |
(([1], Res), 14),
|
|
neuper@52105
|
83 |
(([], Res), 14)] *)
|
|
neuper@37906
|
84 |
val Form res = (#1 o pt_extract) (pt, ([],Res));
|
|
neuper@37906
|
85 |
if p = ([], Res) andalso term2str res = "14" then ()
|
|
neuper@52105
|
86 |
else error "simplify.sml: append inform with final result changed";
|
|
neuper@38065
|
87 |
|