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/diophanteq.sml
author Mathias Lehnfeld <bonzai@inode.at>
Mon, 04 Apr 2011 11:05:07 +0200
branchdecompose-isar
changeset 41949 c1859b72ae8d
parent 41936 c12d6f2a11aa
child 41951 50bc995aa45b
permissions -rw-r--r--
intermed. context integration appl_add does not work 
     1 (* Title:  tests on DiophantEq.thy

     2    Author: Mathias Lehnfeld 2011

     3    (c) due to copyright terms

     4 12345678901234567890123456789012345678901234567890123456789012345678901234567890

     5         10        20        30        40        50        60        70        80

     6 *)

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

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

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

    10 "----------- rewriting for usecase1 ---------------------";

    11 "----------- mathengine with usecase1 -------------------";

    12 "----------- rewriting for usecase2 ---------------------";

    13 "----------- mathengine with usecase2 -------------------";

    14 "--------------------------------------------------------";

    15 "--------------------------------------------------------";

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

    17 

    18 (*there seemed to be no way to do these tests within DiophantEq.thy:

    19 val thy = @{theory};(**** ME_Isa: thy 'DiophantEq' not in system

    20   from CalcTreeTest*)

    21 (*val thy = @{theory "Isac"};toplevel error from store_met?!?*)

    22 *)

    23 val thy = @{theory "DiophantEq"};

    24 val ctxt = ProofContext.init_global thy;

    25 

    26 "----------- rewriting for usecase1 ---------------------";

    27 "----------- rewriting for usecase1 ---------------------";

    28 "----------- rewriting for usecase1 ---------------------";

    29 val subst = let

    30       val pair = (parseNEW ctxt "bdv::int", parseNEW ctxt "xxx::int");

    31     in case pair of

    32         (SOME r, SOME s) => [(r,s)]

    33       | _ => error "diophanteq.sml: syntax error in rewriting for usecase1"

    34     end;

    35 val t = case parseNEW ctxt "xxx + 111 = abc + (123::int)" of

    36       SOME t' => t'

    37     | NONE => error "diophanteq.sml: syntax error in rewriting for usecase1";

    38 

    39 val SOME (t,_) = rewrite_inst_ thy e_rew_ord e_rls true subst 

    40   (num_str @{thm "int_isolate_add"}) t; term2str t;

    41 

    42 val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"TIMES"))) t; 

    43 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; term2str t;

    44 

    45 val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"PLUS"))) t; 

    46 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; term2str t;

    47 

    48 "----------- mathengine with usecase1 -------------------";

    49 "----------- mathengine with usecase1 -------------------";

    50 "----------- mathengine with usecase1 -------------------";

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

    52 val (fmz, (thy, pbl, met)) = 

    53   (["boolTestGiven (xxx + 111 = abc + (123::int))", "intTestGiven xxx", 

    54     "intTestFind sss"],

    55    (Context.theory_name thy, ["diophantine", "equation"], 

    56     ["Test", "solve_diophant"]));

    57 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (thy, pbl, met))];

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

    59 (*========== inhibit exn WN110318 ==============================================

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

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

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

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

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

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

    66 ============ inhibit exn WN110318 ============================================*)

    67 

    68 "----------- rewriting for usecase2 ---------------------";

    69 "----------- rewriting for usecase2 ---------------------";

    70 val thy = @{theory "Test"};

    71 "----------- rewriting for usecase2 ---------------------";

    72 

    73 val t = case parseNEW ctxt "xxx + abc + -1 * 111 + (123::int)" of

    74       SOME t' => t'

    75     | NONE => error "diophanteq.sml: syntax error in rewriting for usecase2";

    76 

    77 val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"TIMES"))) t; 

    78 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; term2str t;

    79 

    80 val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"PLUS"))) t; 

    81 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; term2str t;

    82 

    83 

    84 "----------- mathengine with usecase2 -------------------";

    85 "----------- mathengine with usecase2 -------------------";

    86 "----------- mathengine with usecase2 -------------------";

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

    88 val (fmz, (thy, pbl, met)) = 

    89   (["intTestGiven (xxx + abc + -1 * 111 + (123::int))", "intTestFind sss"],

    90    (Context.theory_name thy, ["inttype","test"], ["Test","intsimp"]));

    91 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (thy, pbl, met))];

    92 (*nxt = ("Model_Problem", ...)*)

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

    94 (*nxt = ("Add_Given", Add_Given "intTestGiven (xxx + abc + -1 * 111 + 123)")*)

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

    96 (* Add_Find ###########################################*)

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

    98 (*nxt = ("Specify_Theory", ...)*)

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

   100 (*nxt = ("Specify_Problem", ...)*)

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

   102 (*nxt = ("Specify_Method", ...)*)

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

   104 (*nxt = ("Empty_Tac", ...) #############################*)

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

   106 (*========== inhibit exn WN110318 ==============================================

   107 ============ inhibit exn WN110318 ============================================*)
wneuper/isa