neuper@41931
|
1 |
(* Title: tests on DiophantEq.thy
|
neuper@41931
|
2 |
Author: Mathias Lehnfeld 2011
|
neuper@41931
|
3 |
(c) due to copyright terms
|
neuper@41931
|
4 |
12345678901234567890123456789012345678901234567890123456789012345678901234567890
|
neuper@41931
|
5 |
10 20 30 40 50 60 70 80
|
neuper@41931
|
6 |
*)
|
neuper@41931
|
7 |
"--------------------------------------------------------";
|
neuper@41931
|
8 |
"table of contents --------------------------------------";
|
neuper@41931
|
9 |
"--------------------------------------------------------";
|
neuper@41931
|
10 |
"----------- rewriting for usecase1 ---------------------";
|
neuper@41931
|
11 |
"----------- mathengine with usecase1 -------------------";
|
neuper@41936
|
12 |
"----------- rewriting for usecase2 ---------------------";
|
neuper@41936
|
13 |
"----------- mathengine with usecase2 -------------------";
|
neuper@41931
|
14 |
"--------------------------------------------------------";
|
neuper@41931
|
15 |
"--------------------------------------------------------";
|
neuper@41931
|
16 |
"--------------------------------------------------------";
|
neuper@41931
|
17 |
|
neuper@41936
|
18 |
(*there seemed to be no way to do these tests within DiophantEq.thy:
|
neuper@41931
|
19 |
val thy = @{theory};(**** ME_Isa: thy 'DiophantEq' not in system
|
neuper@41931
|
20 |
from CalcTreeTest*)
|
wneuper@59592
|
21 |
(*val thy = @{theory "Isac_Knowledge"};toplevel error from store_met?!?*)
|
neuper@41931
|
22 |
*)
|
neuper@41931
|
23 |
val thy = @{theory "DiophantEq"};
|
neuper@48761
|
24 |
val ctxt = Proof_Context.init_global thy;
|
neuper@41931
|
25 |
|
neuper@41931
|
26 |
"----------- rewriting for usecase1 ---------------------";
|
neuper@41931
|
27 |
"----------- rewriting for usecase1 ---------------------";
|
neuper@41931
|
28 |
"----------- rewriting for usecase1 ---------------------";
|
bonzai@41951
|
29 |
val subst = case (parseNEW ctxt "bdv::int", parseNEW ctxt "xxx::int") of
|
bonzai@41951
|
30 |
(SOME r, SOME s) => [(r,s)]
|
bonzai@41951
|
31 |
| _ => error "diophanteq.sml: syntax error in rewriting for usecase1"
|
bonzai@41949
|
32 |
val t = case parseNEW ctxt "xxx + 111 = abc + (123::int)" of
|
bonzai@41949
|
33 |
SOME t' => t'
|
bonzai@41949
|
34 |
| NONE => error "diophanteq.sml: syntax error in rewriting for usecase1";
|
neuper@41931
|
35 |
|
Walther@60500
|
36 |
val SOME (t,_) = rewrite_inst_ ctxt e_rew_ord Rule_Set.empty true subst
|
walther@60337
|
37 |
@{thm "int_isolate_add"} t; UnparseC.term t;
|
neuper@41931
|
38 |
|
walther@59686
|
39 |
val SOME (thmID,thm) = adhoc_thm thy (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"TIMES"))) t;
|
Walther@60500
|
40 |
val SOME (t,_) = rewrite_ ctxt tless_true tval_rls true thm t; UnparseC.term t;
|
neuper@41931
|
41 |
|
walther@59686
|
42 |
val SOME (thmID,thm) = adhoc_thm thy (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"PLUS"))) t;
|
Walther@60500
|
43 |
val SOME (t,_) = rewrite_ ctxt tless_true tval_rls true thm t; UnparseC.term t;
|
neuper@41931
|
44 |
|
neuper@41931
|
45 |
"----------- mathengine with usecase1 -------------------";
|
neuper@41931
|
46 |
"----------- mathengine with usecase1 -------------------";
|
neuper@41931
|
47 |
"----------- mathengine with usecase1 -------------------";
|
neuper@41934
|
48 |
val p = e_pos'; val c = [];
|
neuper@41934
|
49 |
val (fmz, (thy, pbl, met)) =
|
neuper@41936
|
50 |
(["boolTestGiven (xxx + 111 = abc + (123::int))", "intTestGiven xxx",
|
neuper@41936
|
51 |
"intTestFind sss"],
|
neuper@41934
|
52 |
(Context.theory_name thy, ["diophantine", "equation"],
|
neuper@41934
|
53 |
["Test", "solve_diophant"]));
|
neuper@41934
|
54 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (thy, pbl, met))];
|
neuper@41931
|
55 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@41931
|
56 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@41931
|
57 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@41931
|
58 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
wneuper@59238
|
59 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
wneuper@59238
|
60 |
(* BROKEN WITH 62e72f77e695 excluded "ERROR in creating the environment.." FROM "helpless"
|
neuper@41931
|
61 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
wneuper@59238
|
62 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
wneuper@59238
|
63 |
*)
|
neuper@41936
|
64 |
|
neuper@41936
|
65 |
"----------- rewriting for usecase2 ---------------------";
|
neuper@41936
|
66 |
"----------- rewriting for usecase2 ---------------------";
|
neuper@41936
|
67 |
val thy = @{theory "Test"};
|
neuper@41936
|
68 |
"----------- rewriting for usecase2 ---------------------";
|
neuper@41936
|
69 |
|
walther@60329
|
70 |
val t = case parseNEW ctxt "xxx + abc + - 1 * 111 + (123::int)" of
|
bonzai@41949
|
71 |
SOME t' => t'
|
bonzai@41949
|
72 |
| NONE => error "diophanteq.sml: syntax error in rewriting for usecase2";
|
neuper@41936
|
73 |
|
walther@59686
|
74 |
val SOME (thmID,thm) = adhoc_thm thy (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"TIMES"))) t;
|
Walther@60500
|
75 |
val SOME (t,_) = rewrite_ ctxt tless_true tval_rls true thm t; UnparseC.term t;
|
neuper@41936
|
76 |
|
walther@59686
|
77 |
val SOME (thmID,thm) = adhoc_thm thy (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"PLUS"))) t;
|
Walther@60500
|
78 |
val SOME (t,_) = rewrite_ ctxt tless_true tval_rls true thm t; UnparseC.term t;
|
neuper@41936
|
79 |
|
neuper@41936
|
80 |
|
neuper@41936
|
81 |
"----------- mathengine with usecase2 -------------------";
|
neuper@41936
|
82 |
"----------- mathengine with usecase2 -------------------";
|
neuper@41936
|
83 |
"----------- mathengine with usecase2 -------------------";
|
neuper@41936
|
84 |
val p = e_pos'; val c = [];
|
neuper@41936
|
85 |
val (fmz, (thy, pbl, met)) =
|
walther@60329
|
86 |
(["intTestGiven (xxx + abc + - 1 * 111 + (123::int))", "intTestFind sss"],
|
walther@59997
|
87 |
(Context.theory_name thy, ["inttype", "test"], ["Test", "intsimp"]));
|
neuper@41936
|
88 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (thy, pbl, met))];
|
neuper@41936
|
89 |
(*nxt = ("Model_Problem", ...)*)
|
neuper@41936
|
90 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
walther@60329
|
91 |
(*nxt = ("Add_Given", Add_Given "intTestGiven (xxx + abc + - 1 * 111 + 123)")*)
|
neuper@41936
|
92 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@41936
|
93 |
(* Add_Find ###########################################*)
|
neuper@41936
|
94 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@41936
|
95 |
(*nxt = ("Specify_Theory", ...)*)
|
neuper@41936
|
96 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
wneuper@59238
|
97 |
(* BROKEN WITH 62e72f77e695 excluded "ERROR in creating the environment.." FROM "helpless"
|
neuper@41936
|
98 |
(*nxt = ("Specify_Problem", ...)*)
|
neuper@41936
|
99 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@41936
|
100 |
(*nxt = ("Specify_Method", ...)*)
|
neuper@41936
|
101 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@41936
|
102 |
(*nxt = ("Empty_Tac", ...) #############################*)
|
wneuper@59238
|
103 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
wneuper@59238
|
104 |
*)
|
t@42166
|
105 |
|