test/Tools/isac/Knowledge/simplify.sml
author Walther Neuper <neuper@ist.tugraz.at>
Wed, 08 Sep 2010 16:47:22 +0200
branchisac-update-Isa09-2
changeset 37991 028442673981
parent 37967 bd4f7a35e892
child 38031 460c24a6a6ba
permissions -rw-r--r--
tuned src + test

find . -type f -exec sed -i s/nadd_divide_distrib/add_divide_distrib/g {} \;
find . -type f -exec sed -i s/"\.thy\""/"\""/g {} \;
find . -type f -exec sed -i s/" indexname_ord"/" Term_Ord.indexname_ord"/g {} \;
find . -type f -exec sed -i s/"(string_of_cterm o cterm_of(sign_of thy))"/"(Syntax.string_of_term (thy2ctxt thy))"/g {} \;
find . -type f -exec sed -i s/" L_"/" L_L"/g {} \;
find . -type f -exec sed -i s/" L_:"/" L_L:"/g {} \;
find . -type f -exec sed -i s/"e_;"/"e_e;"/g {} \;
find . -type f -exec sed -i s/"v_)"/"v_v)"/g {} \;
find . -type f -exec sed -i s/"v_:"/"v_v:"/g {} \;
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
val thy = Simplify.thy;
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@37906
    21
neuper@37906
    22
"----------- CAS-command Simplify --------------------------------";
neuper@37906
    23
"----------- CAS-command Simplify --------------------------------";
neuper@37906
    24
"----------- CAS-command Simplify --------------------------------";
neuper@37906
    25
states:=[];
neuper@37906
    26
CalcTree [([], ("e_domID", ["e_pblID"], ["e_metID"]))];
neuper@37906
    27
Iterator 1;
neuper@37906
    28
moveActiveRoot 1;
neuper@37906
    29
replaceFormula 1 "Simplify (2*a + 3*a)";
neuper@37906
    30
autoCalculate 1 (Step 1);
neuper@37906
    31
autoCalculate 1 CompleteCalc;
neuper@37906
    32
val ((pt,p),_) = get_calc 1;
neuper@37906
    33
val Form res = (#1 o pt_extract) (pt, ([],Res));
neuper@37906
    34
show_pt pt;
neuper@37906
    35
if p = ([], Res) andalso term2str res = "5 * a" then ()
neuper@37906
    36
else raise error "simplify.sml: diff.behav. CAScmd: Simplify (2*a + 3*a)";
neuper@37906
    37
neuper@37906
    38
neuper@37906
    39
"----------- append inform with final result ---------------------";
neuper@37906
    40
"----------- append inform with final result ---------------------";
neuper@37906
    41
"----------- append inform with final result ---------------------";
neuper@37906
    42
states:=[];
neuper@37967
    43
CalcTree [(["TERM ((14 * x * y) / ( x * y ))", "normalform N"],
neuper@37991
    44
	   ("Rational",["rational","simplification"],
neuper@37906
    45
	    ["simplification","of_rationals"]))];
neuper@37906
    46
Iterator 1;
neuper@37906
    47
moveActiveRoot 1;
neuper@37906
    48
autoCalculate 1 CompleteCalcHead;
neuper@37906
    49
autoCalculate 1 (Step 1);
neuper@37906
    50
appendFormula 1 "14";
neuper@37906
    51
val ((pt,p),_) = get_calc 1; show_pt pt;
neuper@37906
    52
neuper@37906
    53
autoCalculate 1 (Step 1);
neuper@37906
    54
val ((pt,p),_) = get_calc 1; show_pt pt;
neuper@37906
    55
val Form res = (#1 o pt_extract) (pt, ([],Res));
neuper@37906
    56
if p = ([], Res) andalso term2str res = "14" then ()
neuper@37906
    57
else raise error "simplify.sml: append inform with final result ?!?";