Boyer_Moore/counterexample.ml

   1 (******************************************************************************)
   2 (* FILE          : counterexample.ml                                          *)
   3 (* DESCRIPTION   : Simple counterexample checker                              *)
   4 (*                 Based on ideas and suggestions from S. Wilson              *)
   5 (*                                                                            *)
   6 (* READS FILES   : <none>                                                     *)
   7 (* WRITES FILES  : <none>                                                     *)
   8 (*                                                                            *)
   9 (* AUTHOR        : P. Papapanagiotou (University of Edinburgh)                *)
  10 (* DATE          : July 2009                                                  *)
  11 (******************************************************************************)
  12
  13 (*----------------------------------------------------------------------------*)
  14 (* Reference of how many examples will be tried on each check.                *)
  15 (* Set to 0 to turn off counterexample checker.                               *)
  16 (*----------------------------------------------------------------------------*)
  17
  18 let counter_check_num = ref 5;;
  19
  20 let counter_checks t =
  21   counter_check_num := t;;
  22
  23
  24 (*----------------------------------------------------------------------------*)
  25 (* Reference to count how many counterexamples were found during a proof.     *)
  26 (*----------------------------------------------------------------------------*)
  27
  28 let counterexamples = ref 0;;
  29
  30 let inc_counterexamples () = counterexamples := !counterexamples + 1 ; ();;
  31
  32
  33 (*----------------------------------------------------------------------------*)
  34 (* inst_type                                                                  *)
  35 (*----------------------------------------------------------------------------*)
  36 (* Hacky function to instantiate types.                                       *)
  37 (* I'm surprised there is no such function in HOL Light (or perhaps I just    *)
  38 (* haven't found it yet?).                                                    *)
  39 (*----------------------------------------------------------------------------*)
  40 (* Creates a variable of the given type. Instantiates the term using "inst"   *)
  41 (* then returns the type of the resulting term.                               *)
  42 (*----------------------------------------------------------------------------*)
  43
  44 let inst_type : (hol_type * hol_type) list -> hol_type -> hol_type =
  45   fun ins ty ->
  46     let tm = mk_var ("x",ty) in
  47     let itm = inst ins tm in
  48     type_of itm;;
  49
  50
  51 (*----------------------------------------------------------------------------*)
  52 (* shell_type_match                                                           *)
  53 (*----------------------------------------------------------------------------*)
  54 (* Does a deep search to check if a type can be properly grounded to a        *)
  55 (* combination of types defined in the shell.                                 *)
  56 (* Returns the type instantiation pairs to make it happen.                    *)
  57 (* Variable types are instantiated by `:num`.                                 *)
  58 (*----------------------------------------------------------------------------*)
  59 (* If the type is an instance of a type constructor (is_type) then it is      *)
  60 (* split. The name of the constructor is looked up in the system shells list. *)
  61 (* The arguments are checked recursively.                                     *)
  62 (* If it's not an instance of a  type constructor, we try to replace it by    *)
  63 (* `:num`.                                                                    *)
  64 (*----------------------------------------------------------------------------*)
  65
  66 let rec shell_type_match : hol_type -> (hol_type * hol_type) list =
  67   fun ty ->
  68     if (is_type ty) then
  69       let tys,tyargs = dest_type ty in
  70       let info = try sys_shell_info tys
  71           with Failure _ -> failwith ("No shell defined for type '" ^
  72                                     (string_of_type ty) ^ "'") in
  73       itlist union (map shell_type_match tyargs) []
  74     else
  75        try type_match ty `:num` []
  76         with Failure _ -> failwith ("Unknown type '" ^
  77                                     (string_of_type ty) ^ "' that doesn't match 'num'!");;
  78
  79
  80 (*----------------------------------------------------------------------------*)
  81 (* HL_rewrite_ground_term : term -> term                                      *)
  82 (*                                                                            *)
  83 (* Uses HOL Light's REWRITE_CONV to rewrite a ground term.                    *)
  84 (* The function and accessor definitions are used as rewrite rules.           *)
  85 (* This reduces valid expressions to `T`.                                     *)
  86 (*----------------------------------------------------------------------------*)
  87
  88 let HL_rewrite_ground_term tm =
  89 (* ((proof_print_newline) o (proof_print_term) o (proof_print_string "Checking:")) tm ;*)
  90   if (frees tm = []) then
  91 (*    let rules = (union ((flat o defs) ()) (all_accessor_thms ())) *)
  92 (* let rules = (union (rewrite_rules ()) (all_accessor_thms ())) *)
  93     let numred = try (rhs o concl o NUM_REDUCE_CONV) tm with Failure _ -> tm in
  94     if (is_T numred) then numred else
  95     let rew = REWRITE_CONV (union (rewrite_rules ()) (all_accessor_thms ()))
  96     in (rhs o concl o rew) tm
  97   else failwith ("rewrite_ground_term: free vars in term: " ^ (string_of_term tm));;
  98
  99
 100
 101 let HL_rewrite_ground_term' tm =
 102   if (frees tm = []) then
 103 (*    let rules = (union ((flat o defs) ()) (all_accessor_thms ())) *)
 104     let rules = (union ((flat o defs) ()) (all_accessor_thms ())) in
 105     let arith_rules = [PRE;ADD;MULT;EXP;EVEN;ODD;LE;LT;GE;GT;SUB] in
 106 (* Need to apply preprocessing similar to add_def in environment.ml *)
 107     let rew = REWRITE_CONV (ARITH :: (subtract rules arith_rules))
 108     in (rhs o concl o rew) tm
 109   else failwith ("rewrite_ground_term: free vars in term: " ^ (string_of_term tm));;
 110
 111 (*----------------------------------------------------------------------------*)
 112 (* random_example : int -> hol_type -> term                                   *)
 113 (*----------------------------------------------------------------------------*)
 114 (* Creates a random example of a given type.                                  *)
 115 (* The first argument is a maximum depth so as to control the size of the     *)
 116 (* example.                                                                   *)
 117 (*----------------------------------------------------------------------------*)
 118 (* Uses "shell_type_match" in order to ground the type to a combination of    *)
 119 (* types defined as shells. Therefore, all variable types are instantiated to *)
 120 (* `:num`.                                                                    *)
 121 (* Instantiates the arg_types of the shell for each constructor, then uses    *)
 122 (* mk_cons_type to create proper types for the constructors. Having those and *)
 123 (* by using mk_mconst creates the constructors as terms.                      *)
 124 (* random_example is called recursively for every constructor argument, while *)
 125 (* decreasing the maxdepth to ensure termination.                             *)
 126 (* If maxdepth is reached, we just pick randomly one of the base              *)
 127 (* constructors.                                                              *)
 128 (*----------------------------------------------------------------------------*)
 129 (* NOTE: The current version can still afford  a few optimisations.           *)
 130 (* eg. The preprocessing so as to ground the given type should only happen    *)
 131 (* once.                                                                      *)
 132 (* NOTE: We could optimise this function further by accommodating the         *)
 133 (* constructors as terms (rather than or in addition to strings) within the   *)
 134 (* shell.                                                                     *)
 135 (*----------------------------------------------------------------------------*)
 136
 137 let random_example : int -> hol_type -> term =
 138   let rec random_example': int->int->hol_type->term =
 139     fun origdepth maxdepth ty ->
 140       let tyi = shell_type_match ty in
 141       let ty' = inst_type tyi ty in
 142       let tystr,typarams = dest_type ty' in
 143       let sinfo = sys_shell_info tystr in
 144       let ocons = shell_constructors sinfo in
 145       let sh_arg_types = shell_arg_types sinfo in
 146
 147       let arg_type_pairs = zip sh_arg_types typarams in
 148       let arg_types_matches = try
 149         itlist (fun (x,y) l -> type_match x y l) arg_type_pairs tyi
 150       with Failure _ -> failwith "Shell argument types cannot be matched." in
 151
 152       let mk_cons_type = fun arglist ->
 153         List.fold_left (fun ty i -> mk_type ("fun",[i;ty])) ty' (rev arglist) in
 154       let inst_cons = map (fun x,y,_ -> x,map (inst_type arg_types_matches) y) ocons in
 155       let mk_cons = fun x,y ->
 156         try let n = num_of_string x in (mk_numeral n),y
 157         with Failure _ ->  mk_mconst(x,(mk_cons_type y)),y in
 158       let cons = map mk_cons inst_cons in
 159
 160       let terminal_filter = fun (_,l) -> (l=[]) in
 161       let tcons,ntcons = partition terminal_filter cons in
 162
 163       if (maxdepth > 1) then
 164         let prob = 200/((maxdepth-1)*3) in
 165 (*      let newdepth = origdepth / (length cons) in*)
 166         let newdepth = maxdepth - 1 in
 167         let selcons = if ((Random.int 100) <= prob) then tcons else ntcons in
 168         let cconstm,cconsargs = List.nth selcons (Random.int (length selcons)) in
 169         let args = (map (random_example' origdepth newdepth) cconsargs) in
 170         List.fold_left (fun x y ->  mk_comb (x,y)) cconstm args
 171       else
 172         (fst o hd) tcons
 173   in fun maxdepth ty -> random_example' maxdepth maxdepth ty;;
 174
 175 (*      print_string "*" ; print_term cconstm ; print_string "*" ; print_type (type_of cconstm); print_newline (); *)
 176 (*      map (fun x -> print_term x ; print_string ":" ; print_type (type_of x); print_newline()) args ; *)
 177 (*      print_newline (); *)
 178
 179
 180 let random_grounding maxdepth tm =
 181   let vars = frees tm in
 182   let types = map type_of vars in
 183   let examples = map (random_example maxdepth) types in
 184   let pairs = zip vars examples in
 185   let insts = map (fun v,e -> term_match [] v e) pairs in
 186   itlist instantiate insts tm;;
 187
 188
 189 let counter_check_once maxdepth tm =
 190   let tm' = random_grounding maxdepth tm in
 191   let tm'' = HL_rewrite_ground_term tm' in
 192   if (is_T(tm'')) then true else let junk =
 193   warn (!proof_printing) ("Found counterexample for " ^ string_of_term(tm) ^ " : " ^ string_of_term(tm')) in
 194   inc_counterexamples() ; false;;
 195
 196 let rec counter_check_n maxdepth n tm =
 197   if (n<=0) then true
 198   else if (counter_check_once maxdepth tm) then counter_check_n maxdepth (n-1) tm
 199   else false;;
 200
 201 let counter_check maxdepth tm =
 202   counter_check_n maxdepth !counter_check_num tm;;