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*)
neuper@41932: (*val thy = @{theory "Isac"};toplevel error from store_met?!?*)
neuper@41931: *)
neuper@41931: val thy = @{theory "DiophantEq"};
neuper@41931: val ctxt = ProofContext.init_global thy;
neuper@41931: 
neuper@41931: "----------- rewriting for usecase1 ---------------------";
neuper@41931: "----------- rewriting for usecase1 ---------------------";
neuper@41931: "----------- rewriting for usecase1 ---------------------";
bonzai@41949: val subst = let
bonzai@41949:       val pair = (parseNEW ctxt "bdv::int", parseNEW ctxt "xxx::int");
bonzai@41949:     in case pair of
bonzai@41949:         (SOME r, SOME s) => [(r,s)]
bonzai@41949:       | _ => error "diophanteq.sml: syntax error in rewriting for usecase1"
bonzai@41949:     end;
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: 
neuper@41931: val SOME (t,_) = rewrite_inst_ thy e_rew_ord e_rls true subst 
neuper@41931:   (num_str @{thm "int_isolate_add"}) t; term2str t;
neuper@41931: 
neuper@41931: val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"TIMES"))) t; 
neuper@41931: val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; term2str t;
neuper@41931: 
neuper@41931: val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"PLUS"))) t; 
neuper@41931: val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; term2str 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@41936: (*========== inhibit exn WN110318 ==============================================
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; 
neuper@41931: val (p,_,f,nxt,_,pt) = me nxt p c pt; 
neuper@41933: val (p,_,f,nxt,_,pt) = me nxt p c pt; 
neuper@41936: ============ inhibit exn WN110318 ============================================*)
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: 
bonzai@41949: 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: 
neuper@41936: val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"TIMES"))) t; 
neuper@41936: val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; term2str t;
neuper@41936: 
neuper@41936: val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"PLUS"))) t; 
neuper@41936: val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; term2str 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)) = 
neuper@41936:   (["intTestGiven (xxx + abc + -1 * 111 + (123::int))", "intTestFind sss"],
neuper@41936:    (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; 
neuper@41936: (*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; 
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", ...) #############################*)
neuper@41936: val (p,_,f,nxt,_,pt) = me nxt p c pt; 
neuper@41936: (*========== inhibit exn WN110318 ==============================================
neuper@41936: ============ inhibit exn WN110318 ============================================*)