neuper@41931: (* Title:  tests on DiophantEq.thy
neuper@41931:    Author: Mathias Lehnfeld 2011
neuper@41931:    (c) due to copyright terms
neuper@41931: 12345678901234567890123456789012345678901234567890123456789012345678901234567890
neuper@41931:         10        20        30        40        50        60        70        80
neuper@41931: *)
neuper@41931: "--------------------------------------------------------";
neuper@41931: "table of contents --------------------------------------";
neuper@41931: "--------------------------------------------------------";
neuper@41931: "----------- rewriting for usecase1 ---------------------";
neuper@41931: "----------- mathengine with usecase1 -------------------";
neuper@41936: "----------- rewriting for usecase2 ---------------------";
neuper@41936: "----------- mathengine with usecase2 -------------------";
neuper@41931: "--------------------------------------------------------";
neuper@41931: "--------------------------------------------------------";
neuper@41931: "--------------------------------------------------------";
neuper@41931: 
neuper@41936: (*there seemed to be no way to do these tests within DiophantEq.thy:
neuper@41931: val thy = @{theory};(**** ME_Isa: thy 'DiophantEq' not in system
neuper@41931:   from CalcTreeTest*)
wneuper@59592: (*val thy = @{theory "Isac_Knowledge"};toplevel error from store_met?!?*)
neuper@41931: *)
neuper@41931: val thy = @{theory "DiophantEq"};
neuper@48761: val ctxt = Proof_Context.init_global thy;
neuper@41931: 
neuper@41931: "----------- rewriting for usecase1 ---------------------";
neuper@41931: "----------- rewriting for usecase1 ---------------------";
neuper@41931: "----------- rewriting for usecase1 ---------------------";
bonzai@41951: val subst = case (parseNEW ctxt "bdv::int", parseNEW ctxt "xxx::int") of
bonzai@41951:       (SOME r, SOME s) => [(r,s)]
bonzai@41951:     | _ => error "diophanteq.sml: syntax error in rewriting for usecase1"
bonzai@41949: val t = case parseNEW ctxt "xxx + 111 = abc + (123::int)" of
bonzai@41949:       SOME t' => t'
bonzai@41949:     | NONE => error "diophanteq.sml: syntax error in rewriting for usecase1";
neuper@41931: 
Walther@60509: val SOME (t,_) = rewrite_inst_ ctxt Rewrite_Ord.function_empty Rule_Set.empty true subst 
walther@60337:   @{thm "int_isolate_add"} t; UnparseC.term t;
neuper@41931: 
walther@59686: val SOME (thmID,thm) = adhoc_thm thy (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"TIMES"))) t; 
Walther@60500: val SOME (t,_) = rewrite_ ctxt tless_true tval_rls true thm t; UnparseC.term t;
neuper@41931: 
walther@59686: val SOME (thmID,thm) = adhoc_thm thy (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"PLUS"))) t; 
Walther@60500: val SOME (t,_) = rewrite_ ctxt tless_true tval_rls true thm t; UnparseC.term t;
neuper@41931: 
neuper@41931: "----------- mathengine with usecase1 -------------------";
neuper@41931: "----------- mathengine with usecase1 -------------------";
neuper@41931: "----------- mathengine with usecase1 -------------------";
neuper@41934: val p = e_pos'; val c = [];
neuper@41934: val (fmz, (thy, pbl, met)) = 
neuper@41936:   (["boolTestGiven (xxx + 111 = abc + (123::int))", "intTestGiven xxx", 
neuper@41936:     "intTestFind sss"],
neuper@41934:    (Context.theory_name thy, ["diophantine", "equation"], 
neuper@41934:     ["Test", "solve_diophant"]));
neuper@41934: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (thy, pbl, met))];
neuper@41931: val (p,_,f,nxt,_,pt) = me nxt p c pt; 
neuper@41931: val (p,_,f,nxt,_,pt) = me nxt p c pt; 
neuper@41931: val (p,_,f,nxt,_,pt) = me nxt p c pt; 
neuper@41931: val (p,_,f,nxt,_,pt) = me nxt p c pt; 
wneuper@59238: val (p,_,f,nxt,_,pt) = me nxt p c pt;
wneuper@59238: (* BROKEN WITH 62e72f77e695 excluded "ERROR in creating the environment.." FROM "helpless"
neuper@41931: val (p,_,f,nxt,_,pt) = me nxt p c pt; 
wneuper@59238: val (p,_,f,nxt,_,pt) = me nxt p c pt;
wneuper@59238: *)
neuper@41936: 
neuper@41936: "----------- rewriting for usecase2 ---------------------";
neuper@41936: "----------- rewriting for usecase2 ---------------------";
neuper@41936: val thy = @{theory "Test"};
neuper@41936: "----------- rewriting for usecase2 ---------------------";
neuper@41936: 
walther@60329: val t = case parseNEW ctxt "xxx + abc + - 1 * 111 + (123::int)" of
bonzai@41949:       SOME t' => t'
bonzai@41949:     | NONE => error "diophanteq.sml: syntax error in rewriting for usecase2";
neuper@41936: 
walther@59686: val SOME (thmID,thm) = adhoc_thm thy (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"TIMES"))) t; 
Walther@60500: val SOME (t,_) = rewrite_ ctxt tless_true tval_rls true thm t; UnparseC.term t;
neuper@41936: 
walther@59686: val SOME (thmID,thm) = adhoc_thm thy (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"PLUS"))) t; 
Walther@60500: val SOME (t,_) = rewrite_ ctxt tless_true tval_rls true thm t; UnparseC.term t;
neuper@41936: 
neuper@41936: 
neuper@41936: "----------- mathengine with usecase2 -------------------";
neuper@41936: "----------- mathengine with usecase2 -------------------";
neuper@41936: "----------- mathengine with usecase2 -------------------";
neuper@41936: val p = e_pos'; val c = [];
neuper@41936: val (fmz, (thy, pbl, met)) = 
walther@60329:   (["intTestGiven (xxx + abc + - 1 * 111 + (123::int))", "intTestFind sss"],
walther@59997:    (Context.theory_name thy, ["inttype", "test"], ["Test", "intsimp"]));
neuper@41936: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (thy, pbl, met))];
neuper@41936: (*nxt = ("Model_Problem", ...)*)
neuper@41936: val (p,_,f,nxt,_,pt) = me nxt p c pt; 
walther@60329: (*nxt = ("Add_Given", Add_Given "intTestGiven (xxx + abc + - 1 * 111 + 123)")*)
neuper@41936: val (p,_,f,nxt,_,pt) = me nxt p c pt; 
neuper@41936: (* Add_Find ###########################################*)
neuper@41936: val (p,_,f,nxt,_,pt) = me nxt p c pt; 
neuper@41936: (*nxt = ("Specify_Theory", ...)*)
neuper@41936: val (p,_,f,nxt,_,pt) = me nxt p c pt; 
wneuper@59238: (* BROKEN WITH 62e72f77e695 excluded "ERROR in creating the environment.." FROM "helpless"
neuper@41936: (*nxt = ("Specify_Problem", ...)*)
neuper@41936: val (p,_,f,nxt,_,pt) = me nxt p c pt; 
neuper@41936: (*nxt = ("Specify_Method", ...)*)
neuper@41936: val (p,_,f,nxt,_,pt) = me nxt p c pt; 
neuper@41936: (*nxt = ("Empty_Tac", ...) #############################*)
wneuper@59238: val (p,_,f,nxt,_,pt) = me nxt p c pt;
wneuper@59238: *)
t@42166: