(* Title:  tests on DiophantEq.thy

   Author: Mathias Lehnfeld 2011

   (c) due to copyright terms

12345678901234567890123456789012345678901234567890123456789012345678901234567890

        10        20        30        40        50        60        70        80

*)

"--------------------------------------------------------";

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

"--------------------------------------------------------";

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

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

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

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

"--------------------------------------------------------";

"--------------------------------------------------------";

"--------------------------------------------------------";

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

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

  from CalcTreeTest*)

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

*)

val thy = @{theory "DiophantEq"};

val ctxt = Proof_Context.init_global thy;

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

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

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

val subst = case (parseNEW ctxt "bdv::int", parseNEW ctxt "xxx::int") of

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

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

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

      SOME t' => t'

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

val SOME (t,_) = rewrite_inst_ thy e_rew_ord Rule_Set.empty true subst 

  (ThmC.numerals_to_Free @{thm "int_isolate_add"}) t; UnparseC.term t;

val SOME (thmID,thm) = adhoc_thm thy (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"TIMES"))) t; 

val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; UnparseC.term t;

val SOME (thmID,thm) = adhoc_thm thy (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"PLUS"))) t; 

val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; UnparseC.term t;

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

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

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

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

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

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

    "intTestFind sss"],

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

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

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

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

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

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

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

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

(* BROKEN WITH 62e72f77e695 excluded "ERROR in creating the environment.." FROM "helpless"

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

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

*)

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

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

val thy = @{theory "Test"};

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

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

      SOME t' => t'

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

val SOME (thmID,thm) = adhoc_thm thy (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"TIMES"))) t; 

val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; UnparseC.term t;

val SOME (thmID,thm) = adhoc_thm thy (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"PLUS"))) t; 

val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; UnparseC.term t;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

(* BROKEN WITH 62e72f77e695 excluded "ERROR in creating the environment.." FROM "helpless"

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

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

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

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

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

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

*)