#use "topfind";;
#require "unix";;
open Unix;;
open Printf;;

let remaining_theory = ref ([]:term list);;
let currenttm = ref `p`;;

let bm_time f arg =
    let t1=Unix.times () in
       let resu = try (if (can dest_thm (f arg)) then true else false) with Failure _ -> false in
       let t2=Unix.times () in (resu,(t1,t2));;
        (*  printf "User time: %f - system time: %f\n%!" (t2.tms_utime -. t1.tms_utime) (t2.tms_stime -. t1.tms_stime);; *)

let bm_test f tm =
    let pfpt = (print_term tm ; print_newline() ; proof_printer false) in
    let (resu,(t1,t2)) = bm_time f tm in
    let pfpt = proof_printer pfpt in
    printf "Proven: %b - Time: %f - Steps: %d - Inductions: %d - Gen terms: %d \\\\\n" resu (t2.tms_utime -. t1.tms_utime) (fst !bm_steps) (snd !bm_steps) (length !my_gen_terms) ; !my_gen_terms;;

let bm_test3 f tm =
    let pfpt = (print_term tm ; print_newline() ; proof_printer false) in
    let (resu,(t1,t2)) = bm_time f tm in
    let voi = if (resu) then new_rewrite_rule( f tm ) else () in
    let pfpt = proof_printer pfpt in
    printf "& %b & %f & %d & %d & %d \\\\\n" 
resu (t2.tms_utime -. t1.tms_utime) (fst !bm_steps) (snd !bm_steps) (length !my_gen_terms) ; !my_gen_terms;;

let bm_test2 f tm =
    let pfpt = (print_term tm ; print_newline() ; proof_printer false) in
    let (resu,(t1,t2)) = bm_time f tm in
    let pfpt = proof_printer pfpt in
    printf "& %b & %f & %d & %d & %d & %d \\\\\n" resu (t2.tms_utime -. t1.tms_utime) (fst !bm_steps) (snd !bm_steps) (length !my_gen_terms) (!counterexamples) ; 
(*!my_gen_terms;;*)
    ();;

let nexttm f =
    if (!remaining_theory = []) then failwith "No more"
    else currenttm := hd !remaining_theory ; remaining_theory := tl !remaining_theory ;
    bm_test2 f !currenttm;;
    

let sametm f = bm_test2 f !currenttm;;

let nexttm2 f =
    if (!remaining_theory = []) then failwith "No more"
    else currenttm := hd !remaining_theory ; remaining_theory := tl !remaining_theory ;
    bm_test3 f !currenttm;;
    

let sametm2 f = bm_test3 f !currenttm;;
    

let BM = BOYER_MOORE;;
let BME = BOYER_MOORE_EXT;;
let BMG = BOYER_MOORE_GEN;;

let RBM = new_rewrite_rule o BOYER_MOORE;;
let RBME = new_rewrite_rule o BOYER_MOORE_EXT;;
let RBMG = new_rewrite_rule o BOYER_MOORE_GEN;;

let new_stuff x = (new_def x ; new_rewrite_rule x);;

#use "boulton/arith.ml";;
#use "boulton/list.ml";;

let bm_reset () =

system_defs := [];
system_rewrites := [];

new_stuff ADD;
new_stuff MULT;
new_stuff SUB;
new_stuff LE;
new_stuff LT;
new_stuff GE;
new_stuff GT;
new_rewrite_rule (ARITH_RULE `1=SUC(0)`);
new_stuff EXP;
new_stuff FACT;
new_stuff ODD;
new_stuff EVEN;

new_rewrite_rule NOT_SUC;
new_rewrite_rule SUC_INJ;
new_rewrite_rule PRE;

new_stuff HD;
new_stuff TL;
new_stuff APPEND;
new_stuff REVERSE;
new_stuff LENGTH;
new_stuff MAP;
new_stuff LAST;
new_stuff REPLICATE;
new_stuff NULL;
new_stuff ALL;
new_stuff EX;
new_stuff ITLIST;
new_stuff MEM;
new_stuff ALL2_DEF;
new_rewrite_rule ALL2;
new_stuff MAP2_DEF;
new_rewrite_rule MAP2;
new_stuff EL;
new_stuff FILTER;
new_stuff ASSOC;
new_stuff ITLIST2_DEF;
new_rewrite_rule ITLIST2;
new_stuff ZIP_DEF;
new_rewrite_rule ZIP;

new_rewrite_rule NOT_CONS_NIL;
new_rewrite_rule CONS_11 ;;

bm_reset();;
