Mercurial Mercurial > wneuper > isa / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
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 {} \; 
     1 (* tests on simplification

     2    author: Walther Neuper

     3    061019

     4    (c) due to copyright terms

     5 

     6 use"../smltest/IsacKnowledge/simplify.sml";

     7 use"simplify.sml";

     8 *)

     9 val thy = Simplify.thy;

    10 

    11 "-----------------------------------------------------------------";

    12 "table of contents -----------------------------------------------";

    13 "-----------------------------------------------------------------";

    14 "----------- CAS-command Simplify --------------------------------";

    15 "----------- append inform with final result ---------------------";

    16 "-----------------------------------------------------------------";

    17 "-----------------------------------------------------------------";

    18 "-----------------------------------------------------------------";

    19 

    20 

    21 

    22 "----------- CAS-command Simplify --------------------------------";

    23 "----------- CAS-command Simplify --------------------------------";

    24 "----------- CAS-command Simplify --------------------------------";

    25 states:=[];

    26 CalcTree [([], ("e_domID", ["e_pblID"], ["e_metID"]))];

    27 Iterator 1;

    28 moveActiveRoot 1;

    29 replaceFormula 1 "Simplify (2*a + 3*a)";

    30 autoCalculate 1 (Step 1);

    31 autoCalculate 1 CompleteCalc;

    32 val ((pt,p),_) = get_calc 1;

    33 val Form res = (#1 o pt_extract) (pt, ([],Res));

    34 show_pt pt;

    35 if p = ([], Res) andalso term2str res = "5 * a" then ()

    36 else raise error "simplify.sml: diff.behav. CAScmd: Simplify (2*a + 3*a)";

    37 

    38 

    39 "----------- append inform with final result ---------------------";

    40 "----------- append inform with final result ---------------------";

    41 "----------- append inform with final result ---------------------";

    42 states:=[];

    43 CalcTree [(["TERM ((14 * x * y) / ( x * y ))", "normalform N"],

    44 	   ("Rational",["rational","simplification"],

    45 	    ["simplification","of_rationals"]))];

    46 Iterator 1;

    47 moveActiveRoot 1;

    48 autoCalculate 1 CompleteCalcHead;

    49 autoCalculate 1 (Step 1);

    50 appendFormula 1 "14";

    51 val ((pt,p),_) = get_calc 1; show_pt pt;

    52 

    53 autoCalculate 1 (Step 1);

    54 val ((pt,p),_) = get_calc 1; show_pt pt;

    55 val Form res = (#1 o pt_extract) (pt, ([],Res));

    56 if p = ([], Res) andalso term2str res = "14" then ()

    57 else raise error "simplify.sml: append inform with final result ?!?";
wneuper/isa