|
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@38065
|
9 |
val thy = theory "Simplify";
|
|
neuper@37906
|
10 |
|
|
neuper@37906
|
11 |
"-----------------------------------------------------------------";
|
|
neuper@37906
|
12 |
"table of contents -----------------------------------------------";
|
|
neuper@37906
|
13 |
"-----------------------------------------------------------------";
|
|
neuper@37906
|
14 |
"----------- CAS-command Simplify --------------------------------";
|
|
neuper@37906
|
15 |
"----------- append inform with final result ---------------------";
|
|
neuper@37906
|
16 |
"-----------------------------------------------------------------";
|
|
neuper@37906
|
17 |
"-----------------------------------------------------------------";
|
|
neuper@37906
|
18 |
"-----------------------------------------------------------------";
|
|
neuper@37906
|
19 |
|
|
neuper@37906
|
20 |
|
|
neuper@38065
|
21 |
(*=== inhibit exn ?=============================================================
|
|
neuper@37906
|
22 |
|
|
neuper@37906
|
23 |
"----------- CAS-command Simplify --------------------------------";
|
|
neuper@37906
|
24 |
"----------- CAS-command Simplify --------------------------------";
|
|
neuper@37906
|
25 |
"----------- CAS-command Simplify --------------------------------";
|
|
neuper@37906
|
26 |
states:=[];
|
|
neuper@37906
|
27 |
CalcTree [([], ("e_domID", ["e_pblID"], ["e_metID"]))];
|
|
neuper@37906
|
28 |
Iterator 1;
|
|
neuper@37906
|
29 |
moveActiveRoot 1;
|
|
neuper@37906
|
30 |
replaceFormula 1 "Simplify (2*a + 3*a)";
|
|
neuper@37906
|
31 |
autoCalculate 1 (Step 1);
|
|
neuper@37906
|
32 |
autoCalculate 1 CompleteCalc;
|
|
neuper@37906
|
33 |
val ((pt,p),_) = get_calc 1;
|
|
neuper@37906
|
34 |
val Form res = (#1 o pt_extract) (pt, ([],Res));
|
|
neuper@37906
|
35 |
show_pt pt;
|
|
neuper@37906
|
36 |
if p = ([], Res) andalso term2str res = "5 * a" then ()
|
|
neuper@38031
|
37 |
else error "simplify.sml: diff.behav. CAScmd: Simplify (2*a + 3*a)";
|
|
neuper@38065
|
38 |
===== inhibit exn ?===========================================================*)
|
|
neuper@37906
|
39 |
|
|
neuper@37906
|
40 |
|
|
neuper@37906
|
41 |
"----------- append inform with final result ---------------------";
|
|
neuper@37906
|
42 |
"----------- append inform with final result ---------------------";
|
|
neuper@37906
|
43 |
"----------- append inform with final result ---------------------";
|
|
neuper@37906
|
44 |
states:=[];
|
|
neuper@37967
|
45 |
CalcTree [(["TERM ((14 * x * y) / ( x * y ))", "normalform N"],
|
|
neuper@37991
|
46 |
("Rational",["rational","simplification"],
|
|
neuper@37906
|
47 |
["simplification","of_rationals"]))];
|
|
neuper@37906
|
48 |
Iterator 1;
|
|
neuper@37906
|
49 |
moveActiveRoot 1;
|
|
neuper@37906
|
50 |
autoCalculate 1 CompleteCalcHead;
|
|
neuper@38065
|
51 |
|
|
neuper@38065
|
52 |
val ((pt,_),_) = get_calc 1;
|
|
neuper@38065
|
53 |
pt_extract (pt, p);
|
|
neuper@38065
|
54 |
|
|
neuper@38065
|
55 |
(*========== inhibit exn =======================================================
|
|
neuper@37906
|
56 |
autoCalculate 1 (Step 1);
|
|
neuper@38065
|
57 |
|
|
neuper@37906
|
58 |
appendFormula 1 "14";
|
|
neuper@37906
|
59 |
val ((pt,p),_) = get_calc 1; show_pt pt;
|
|
neuper@37906
|
60 |
|
|
neuper@37906
|
61 |
autoCalculate 1 (Step 1);
|
|
neuper@37906
|
62 |
val ((pt,p),_) = get_calc 1; show_pt pt;
|
|
neuper@37906
|
63 |
val Form res = (#1 o pt_extract) (pt, ([],Res));
|
|
neuper@37906
|
64 |
if p = ([], Res) andalso term2str res = "14" then ()
|
|
neuper@38031
|
65 |
else error "simplify.sml: append inform with final result ?!?";
|
|
neuper@38065
|
66 |
|
|
neuper@38065
|
67 |
============ inhibit exn =====================================================*)
|
|
neuper@38065
|
68 |
|