1 (* Title: tests on DiophantEq.thy
2 Author: Mathias Lehnfeld 2011
3 (c) due to copyright terms
5 "--------------------------------------------------------";
6 "table of contents --------------------------------------";
7 "--------------------------------------------------------";
8 "----------- rewriting for usecase1 ---------------------";
9 "----------- mathengine with usecase1 -------------------";
10 "----------- rewriting for usecase2 ---------------------";
11 "----------- mathengine with usecase2 -------------------";
12 "--------------------------------------------------------";
13 "--------------------------------------------------------";
14 "--------------------------------------------------------";
16 (*there seemed to be no way to do these tests within DiophantEq.thy:
17 val thy = @{theory};(** ME_Isa: thy 'DiophantEq' not in system
18 from Test_Code.init_calc*)
19 (*val thy = @{theory "Isac_Knowledge"};toplevel error from store_met?!?*)
21 val thy = @{theory "DiophantEq"};
22 val ctxt = Proof_Context.init_global thy;
24 "----------- rewriting for usecase1 ---------------------";
25 "----------- rewriting for usecase1 ---------------------";
26 "----------- rewriting for usecase1 ---------------------";
27 val subst = case (ParseC.term_opt ctxt "bdv::int", ParseC.term_opt ctxt "xxx::int") of
28 (SOME r, SOME s) => [(r,s)]
29 | _ => error "diophanteq.sml: syntax error in rewriting for usecase1"
30 val t = case ParseC.term_opt ctxt "xxx + 111 = abc + (123::int)" of
32 | NONE => error "diophanteq.sml: syntax error in rewriting for usecase1";
34 val SOME (t,_) = rewrite_inst_ ctxt Rewrite_Ord.function_empty Rule_Set.empty true subst
35 @{thm "int_isolate_add"} t; UnparseC.term @{context} t;
37 val SOME (thmID,thm) = adhoc_thm ctxt (the(LibraryC.assoc(Know_Store.get_calcs @{theory},"TIMES"))) t;
38 val SOME (t,_) = rewrite_ ctxt tless_true tval_rls true thm t; UnparseC.term @{context} t;
40 val SOME (thmID,thm) = adhoc_thm ctxt (the(LibraryC.assoc(Know_Store.get_calcs @{theory},"PLUS"))) t;
41 val SOME (t,_) = rewrite_ ctxt tless_true tval_rls true thm t; UnparseC.term @{context} t;
43 "----------- mathengine with usecase1 -------------------";
44 "----------- mathengine with usecase1 -------------------";
45 "----------- mathengine with usecase1 -------------------";
46 "----------- Take as 1st stac in program -------------------------------------------------------";
47 (*/--------- valueless test with experimental Problem and MethodC -----------------------------\* )
48 val p = e_pos'; val c = [];
49 val (fmz, (thy, pbl, met)) =
50 (["boolTestGiven (xxx + 111 = abc + (123::int))", "intTestGiven xxx",
52 (Context.theory_name thy, ["diophantine", "equation"],
53 ["Test", "solve_diophant"]));
54 val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (thy, pbl, met))];
55 val (p,_,f,nxt,_,pt) = me nxt p c pt;
56 val (p,_,f,nxt,_,pt) = me nxt p c pt;
57 val (p,_,f,nxt,_,pt) = me nxt p c pt;
58 val (p,_,f,nxt,_,pt) = me nxt p c pt;
59 val (p,_,f,nxt,_,pt) = me nxt p c pt;
60 (* BROKEN WITH 62e72f77e695 excluded "ERROR in creating the environment.." FROM "helpless"
61 val (p,_,f,nxt,_,pt) = me nxt p c pt;
62 val (p,_,f,nxt,_,pt) = me nxt p c pt;
64 ( *\--------- valueless test with experimental Problem and MethodC -----------------------------/*)
66 "----------- rewriting for usecase2 ---------------------";
67 "----------- rewriting for usecase2 ---------------------";
68 val thy = @{theory "Test"};
69 "----------- rewriting for usecase2 ---------------------";
71 val t = case ParseC.term_opt ctxt "xxx + abc + - 1 * 111 + (123::int)" of
73 | NONE => error "diophanteq.sml: syntax error in rewriting for usecase2";
75 val SOME (thmID,thm) = adhoc_thm ctxt (the(LibraryC.assoc(Know_Store.get_calcs @{theory},"TIMES"))) t;
76 val SOME (t,_) = rewrite_ ctxt tless_true tval_rls true thm t; UnparseC.term @{context} t;
78 val SOME (thmID,thm) = adhoc_thm ctxt (the(LibraryC.assoc(Know_Store.get_calcs @{theory},"PLUS"))) t;
79 val SOME (t,_) = rewrite_ ctxt tless_true tval_rls true thm t; UnparseC.term @{context} t;
82 "----------- mathengine with usecase2 -------------------";
83 "----------- mathengine with usecase2 -------------------";
84 "----------- mathengine with usecase2 -------------------";
85 (*/--------- valueless test with experimenta Problem and MethodC ------------------------------\* )
86 val p = e_pos'; val c = [];
87 val (fmz, (thy, pbl, met)) =
88 (["intTestGiven (xxx + abc + - 1 * 111 + (123::int))", "intTestFind sss"],
89 (Context.theory_name thy, ["inttype", "test"], ["Test", "intsimp"]));
90 val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (thy, pbl, met))];
91 (*nxt = ("Model_Problem", ...)*)
92 val (p,_,f,nxt,_,pt) = me nxt p c pt;
93 (*nxt = ("Add_Given", Add_Given "intTestGiven (xxx + abc + - 1 * 111 + 123)")*)
94 val (p,_,f,nxt,_,pt) = me nxt p c pt;
95 (* Add_Find ###########################################*)
96 val (p,_,f,nxt,_,pt) = me nxt p c pt;
97 (*nxt = ("Specify_Theory", ...)*)
98 val (p,_,f,nxt,_,pt) = me nxt p c pt;
99 (* BROKEN WITH 62e72f77e695 excluded "ERROR in creating the environment.." FROM "helpless"
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;
107 ( *\--------- valueless test with experimental Problem and MethodC -----------------------------/*)