Boyer_Moore/make.ml

   1 (* ========================================================================= *)
   2 (* Load in Petros Papapanagiotou's Boyer-Moore code and try examples.        *)
   3 (* ========================================================================= *)
   4
   5 loads "Boyer_Moore/boyer-moore.ml";;
   6
   7 (* ------------------------------------------------------------------------- *)
   8 (* Slight variant of Petros's eval.ml file.                                  *)
   9 (* ------------------------------------------------------------------------- *)
  10
  11 (* ========================================================================= *)
  12
  13 (* ------------------------------------------------------------------------- *)
  14 (* Shortcuts for the various evaluation versions:                            *)
  15 (* ------------------------------------------------------------------------- *)
  16
  17 let BM = BOYER_MOORE;; (* Pure re-implementation of R.Boulton's work. *)
  18 let BME = BOYER_MOORE_EXT;; (* Extended with early termination heuristics and HOL Light features. *)
  19 let BMG = BOYER_MOORE_GEN;; (* Further extended with M.Aderhold's generalization techniques. *)
  20
  21 let RBM = new_rewrite_rule o BOYER_MOORE;;
  22 let RBME = new_rewrite_rule o BOYER_MOORE_EXT;;
  23 let RBMG = new_rewrite_rule o BOYER_MOORE_GEN;;
  24
  25 (* ------------------------------------------------------------------------- *)
  26 (* Add a theorem as a new function definition and rewrite rule.              *)
  27 (* Adding it as a rewrite rule should no longer be necessary after the       *)
  28 (* latest (July 2009) bugfixes but it doesn't do any harm either.            *)
  29 (* ------------------------------------------------------------------------- *)
  30
  31 let new_stuff x = (new_def x ; new_rewrite_rule x);;
  32
  33 (* ------------------------------------------------------------------------- *)
  34 (* Test sets extracted from the proven theorems in HOL Light's arith.ml and  *)
  35 (* list.ml.                                                                  *)
  36 (* ------------------------------------------------------------------------- *)
  37
  38 loads "Boyer_Moore/testset/arith.ml";; (* Arithmetic test set *)
  39 loads "Boyer_Moore/testset/list.ml";; (* List test set *)
  40
  41 (* ------------------------------------------------------------------------- *)
  42 (* Reloads all the necessary definitions and rules for the evaluation of the *)
  43 (* test sets above.                                                          *)
  44 (* ------------------------------------------------------------------------- *)
  45
  46 let bm_reset () =
  47
  48 system_defs := [];
  49 system_rewrites := [];
  50
  51 new_stuff ADD;
  52 new_stuff MULT;
  53 new_stuff SUB;
  54 new_stuff LE;
  55 new_stuff LT;
  56 new_stuff GE;
  57 new_stuff GT;
  58 new_rewrite_rule (ARITH_RULE `1=SUC(0)`);
  59 new_stuff EXP;
  60 new_stuff FACT;
  61 new_stuff ODD;
  62 new_stuff EVEN;
  63
  64 new_rewrite_rule NOT_SUC;
  65 new_rewrite_rule SUC_INJ;
  66 new_rewrite_rule PRE;
  67
  68 new_stuff HD;
  69 new_stuff TL;
  70 new_stuff APPEND;
  71 new_stuff REVERSE;
  72 new_stuff LENGTH;
  73 new_stuff MAP;
  74 new_stuff LAST;
  75 new_stuff REPLICATE;
  76 new_stuff NULL;
  77 new_stuff ALL;
  78 new_stuff EX;
  79 new_stuff ITLIST;
  80 new_stuff MEM;
  81 new_stuff ALL2_DEF;
  82 new_rewrite_rule ALL2;
  83 new_stuff MAP2_DEF;
  84 new_rewrite_rule MAP2;
  85 new_stuff EL;
  86 new_stuff FILTER;
  87 new_stuff ASSOC;
  88 new_stuff ITLIST2_DEF;
  89 new_rewrite_rule ITLIST2;
  90 new_stuff ZIP_DEF;
  91 new_rewrite_rule ZIP;
  92
  93 new_rewrite_rule NOT_CONS_NIL;
  94 new_rewrite_rule CONS_11 ;;
  95
  96 bm_reset();;
  97
  98 (* ------------------------------------------------------------------------- *)
  99 (* Test functions. They use the Unix library to measure time.                *)
 100 (* Unfortunately this means that they do not load properly in Cygwin.        *)
 101 (* ------------------------------------------------------------------------- *)
 102
 103 #load "unix.cma";;
 104 open Unix;;
 105 open Printf;;
 106
 107
 108 (* ------------------------------------------------------------------------- *)
 109 (* Reference of the remaining theory to be proven. Load a list of theorems   *)
 110 (* that you want the evaluation to run through.                              *)
 111 (* eg. remaining_theory := !mytheory;;                                       *)
 112 (* Then use nexttm (see below) to evaluate one of the BOYER_MOORE_*          *)
 113 (* procedures over the list.                                                 *)
 114 (* ------------------------------------------------------------------------- *)
 115
 116 let remaining_theory = ref ([]:term list);;
 117
 118 let currenttm = ref `p`;;
 119
 120 (* ------------------------------------------------------------------------- *)
 121 (* Tries a theorem-proving procedure f on arg.                               *)
 122 (* Returns a truth value of whether the procedure succeeded in finding a     *)
 123 (* proof and a pair of timestamps taken from the start and the end of the    *)
 124 (* procedure.                                                                *)
 125 (* ------------------------------------------------------------------------- *)
 126
 127 let bm_time f arg =
 128     let t1=Unix.times () in
 129        let resu = try (if (can dest_thm (f arg)) then true else false) with Failure _ -> false in
 130        let t2=Unix.times () in (resu,(t1,t2));;
 131         (*  printf "User time: %f - system time: %f\n%!" (t2.tms_utime -. t1.tms_utime) (t2.tms_stime -. t1.tms_stime);; *)
 132
 133
 134 (* ------------------------------------------------------------------------- *)
 135 (* Uses bm_time to try a Boyer-Moore theorem-proving procedure f on tm.      *)
 136 (* Prints out all the evaluation information that is collected and returns   *)
 137 (* the list of generalizations made during the proof.                        *)
 138 (* ------------------------------------------------------------------------- *)
 139
 140 let bm_test f tm =
 141     let pfpt = (print_term tm ; print_newline() ; proof_printer false) in
 142     let (resu,(t1,t2)) = bm_time f tm in
 143     let pfpt = proof_printer pfpt in
 144     printf "Proven: %b - Time: %f - Steps: %d - Inductions: %d - Gen terms: %d - Over gens: %d \\\\\n" resu
 145 (t2.tms_utime -. t1.tms_utime) (fst !bm_steps) (snd !bm_steps) (length !my_gen_terms) (!counterexamples) ;
 146     !my_gen_terms;;
 147
 148 (* ------------------------------------------------------------------------- *)
 149 (* Another version of bm_test but with a more compact printout.              *)
 150 (* Returns unit ().                                                          *)
 151 (* ------------------------------------------------------------------------- *)
 152
 153 let bm_test2 f tm =
 154     let pfpt = (print_term tm ; print_newline() ; proof_printer false) in
 155     let (resu,(t1,t2)) = bm_time f tm in
 156     let pfpt = proof_printer pfpt in
 157     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) ;
 158     ();;
 159
 160 (* ------------------------------------------------------------------------- *)
 161 (* Convenient function for evaluation.                                       *)
 162 (* Uses f to try and prove the next term in !remaining_theory by bm_test2    *)
 163 (* ------------------------------------------------------------------------- *)
 164
 165 let nexttm f =
 166     if (!remaining_theory = []) then failwith "No more"
 167     else currenttm := hd !remaining_theory ; remaining_theory := tl !remaining_theory ;
 168     bm_test2 f !currenttm;;
 169
 170 (* ------------------------------------------------------------------------- *)
 171 (* Reruns evaluation on the same term that was last loaded with nexttm.      *)
 172 (* ------------------------------------------------------------------------- *)
 173
 174 let sametm f = bm_test2 f !currenttm;;
 175
 176
 177 (* ========================================================================= *)
 178
 179
 180 (* ------------------------------------------------------------------------- *)
 181 (* Just one example.                                                         *)
 182 (* ------------------------------------------------------------------------- *)
 183
 184 bm_test BME `m + n:num = n + m`;;
 185
 186 (* ------------------------------------------------------------------------- *)
 187 (* Note that these don't all terminate, so need more delicacy really.        *)
 188 (* Should carefully reconstruct the cases in Petros's thesis, also maybe     *)
 189 (* using a timeout.                                                          *)
 190 (* ------------------------------------------------------------------------- *)
 191
 192 (****
 193 do_list (bm_test BME) (!mytheory);;
 194
 195 do_list (bm_test BME) (!mytheory2);;
 196  ****)