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/logexp.sml
author Walther Neuper <neuper@ist.tugraz.at>
Wed, 08 Sep 2010 16:47:22 +0200
branchisac-update-Isa09-2
changeset 37991 028442673981
parent 37960 ec20007095f2
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 (* testexamples for LogExp, logarithms and exponential functions and terms

     2 

     3 use"../smltest/IsacKnowledge/logexp.sml";

     4 *)

     5 

     6 val thy = LogExp.thy;

     7 "-----------------------------------------------------------------";

     8 "table of contents -----------------------------------------------";

     9 "-----------------------------------------------------------------";

    10 "----------- setup presentation innsbruck ------------------------";

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

    12 "-----------------------------------------------------------------";

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

    14 

    15 

    16 "----------- setup presentation innsbruck ------------------------";

    17 "----------- setup presentation innsbruck ------------------------";

    18 "----------- setup presentation innsbruck ------------------------";

    19 (*

    20 NOT INCLUDED IN ROOT.ML and RTEST-root.sml, since the pbl and met

    21 defined in IsacKnowledge/Test.ML are out-commented

    22 in order to allow for demonstration of authoring !

    23 

    24 equality_power;

    25 exp_invers_log;

    26 (* WN071203 ???... wrong thy ?!? because parsing with Isac.thy works ?

    27 refine ["equality ((2 log x) = 3)","solveFor x", "solutions L"] 

    28        ["equation","test"];

    29 *)

    30 

    31 val t = str2term "(2 log x)";

    32 val t = str2term "(2 log x) = 3";

    33 val t = str2term "matches ((?a log x) = ?b) ((2 log x) = 3)";

    34 atomty t;

    35 

    36 

    37 val fmz = ["equality ((2 log x) = 3)","solveFor x", "solutions L"];

    38 val (dI',pI',mI') =

    39   ("Isac",["logarithmic","univariate","equation","test"],

    40    ["Test","solve_log"]);

    41 val p = e_pos'; val c = []; 

    42 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

    43 val (p,_,f,nxt,_,pt) = me nxt p c pt;

    44 val (p,_,f,nxt,_,pt) = me nxt p c pt;

    45 val (p,_,f,nxt,_,pt) = me nxt p c pt;

    46 val (p,_,f,nxt,_,pt) = me nxt p c pt;

    47 val (p,_,f,nxt,_,pt) = me nxt p c pt;

    48 val (p,_,f,nxt,_,pt) = me nxt p c pt;

    49 val (p,_,f,nxt,_,pt) = me nxt p c pt;

    50 case nxt of ("Apply_Method",_) => ()

    51 	  | _ => raise error "logexp.sml setup innsbruck";

    52 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;

    53 

    54 

    55 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;

    56 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;

    57 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;

    58 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;

    59 show_pt pt;

    60 

    61 *-------------------------------------------------------------------*)
wneuper/isa