(* 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"};toplevel error from store_met?!?*)

*)

val thy = @{theory "DiophantEq"};

val ctxt = ProofContext.init_global thy;

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

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

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

val subst = let

      val pair = (parseNEW ctxt "bdv::int", parseNEW ctxt "xxx::int");

    in case pair of

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

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

    end;

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 e_rls true subst 

  (num_str @{thm "int_isolate_add"}) t; term2str t;

val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"TIMES"))) t; 

val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; term2str t;

val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"PLUS"))) t; 

val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; term2str 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; 

(*========== inhibit exn WN110318 ==============================================

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; 

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

============ inhibit exn WN110318 ============================================*)

"----------- 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) = get_calculation_ thy (the(assoc(calclist,"TIMES"))) t; 

val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; term2str t;

val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"PLUS"))) t; 

val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; term2str 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; 

(*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; 

(*========== inhibit exn WN110318 ==============================================

============ inhibit exn WN110318 ============================================*)