Boyer_Moore/definitions.ml

   1 (******************************************************************************)
   2 (* FILE          : definitions.ml                                             *)
   3 (* DESCRIPTION   : Using definitions.                                         *)
   4 (*                                                                            *)
   5 (* READS FILES   : <none>                                                     *)
   6 (* WRITES FILES  : <none>                                                     *)
   7 (*                                                                            *)
   8 (* AUTHOR        : R.J.Boulton                                                *)
   9 (* DATE          : 6th June 1991                                              *)
  10 (*                                                                            *)
  11 (* LAST MODIFIED : R.J.Boulton                                                *)
  12 (* DATE          : 3rd August 1992                                            *)
  13 (*                                                                            *)
  14 (* LAST MODIFIED : P. Papapanagiotou (University of Edinburgh)                *)
  15 (* DATE          : 2008                                                       *)
  16 (******************************************************************************)
  17
  18 (*----------------------------------------------------------------------------*)
  19 (* recursive_calls : string -> term -> term list                              *)
  20 (*                                                                            *)
  21 (* Function to compute the occurrences of applications of a constant in a     *)
  22 (* term. The first argument is the name of the constant. The second argument  *)
  23 (* is the term to be examined. If there are no occurrences, an empty list is  *)
  24 (* returned. The function assumes that the term does not contain              *)
  25 (* abstractions.                                                              *)
  26 (*----------------------------------------------------------------------------*)
  27
  28 let rec recursive_calls name tm =
  29  try (let (f,args) = strip_comb tm
  30   in  if (try(fst (dest_const f) = name) with Failure _ -> false)
  31       then [tm]
  32       else itlist List.append (map (recursive_calls name) args) [])
  33  with Failure _ -> [];;
  34
  35 (*----------------------------------------------------------------------------*)
  36 (* is_subterm : term -> term -> bool                                          *)
  37 (*                                                                            *)
  38 (* Function to compute whether one term is a subterm of another.              *)
  39 (*----------------------------------------------------------------------------*)
  40
  41 let rec is_subterm subterm tm =
  42 try(   if (tm = subterm)
  43    then true
  44    else ((is_subterm subterm (rator tm)) or (is_subterm subterm (rand tm)))
  45   )with Failure _ -> false;;
  46
  47 (*----------------------------------------------------------------------------*)
  48 (* no_new_terms : term -> term -> bool                                        *)
  49 (*                                                                            *)
  50 (* Function to determine whether all of the arguments of an application       *)
  51 (* "f x1 ... xn" are subterms of a term.                                      *)
  52 (*----------------------------------------------------------------------------*)
  53
  54 let no_new_terms app tm =
  55 try
  56  (let args = snd (strip_comb app)
  57   in  itlist (fun x y -> x & y) (map (fun arg -> is_subterm arg tm) args) true
  58  ) with Failure _ -> failwith "no_new_terms";;
  59
  60 (*----------------------------------------------------------------------------*)
  61 (* hide_fun_call : term -> term -> term                                       *)
  62 (*                                                                            *)
  63 (* Function to replace occurrences of a particular function call in a term    *)
  64 (* with a genvar, so that `no_new_terms' can be used to look for arguments in *)
  65 (* a term less the original call.                                             *)
  66 (*----------------------------------------------------------------------------*)
  67
  68 let hide_fun_call app tm =
  69    let var = genvar (type_of app)
  70    in  subst [(var,app)] tm;;
  71
  72 (*----------------------------------------------------------------------------*)
  73 (* is_explicit_value : term -> bool                                           *)
  74 (*                                                                            *)
  75 (* Function to compute whether a term is an explicit value. An explicit value *)
  76 (* is either T or F or an application of a shell constructor to explicit      *)
  77 (* values. A `bottom object' corresponds to an application to no arguments.   *)
  78 (* I have also made numeric constants explicit values, since they are         *)
  79 (* equivalent to some number of applications of SUC to 0.                     *)
  80 (*----------------------------------------------------------------------------*)
  81
  82 let is_explicit_value tm =
  83    let rec is_explicit_value' constructors tm =
  84       (is_T tm) or (is_F tm) or ((is_const tm) & (type_of tm = `:num`)) or
  85       (let (f,args) = strip_comb tm
  86        in  (try(mem (fst (dest_const f)) constructors) with Failure _ -> false) &
  87            (forall (is_explicit_value' constructors) args))
  88    in  is_explicit_value' (all_constructors ()) tm;;
  89
  90 (*----------------------------------------------------------------------------*)
  91 (* more_explicit_values : term -> term -> bool                                *)
  92 (*                                                                            *)
  93 (* Returns true if and only if a new function call (second argument) has more *)
  94 (* arguments that are explicit values than the old function call (first       *)
  95 (* argument).                                                                 *)
  96 (*----------------------------------------------------------------------------*)
  97
  98 let more_explicit_values old_call new_call =
  99 try
 100  (let (f1,args1) = strip_comb old_call
 101   and (f2,args2) = strip_comb new_call
 102   in  if (f1 = f2)
 103       then let n1 = length (filter is_explicit_value args1)
 104            and n2 = length (filter is_explicit_value args2)
 105            in  n2 > n1
 106       else failwith "" ) with Failure _ -> failwith "more_explicit_values";;
 107
 108 (*----------------------------------------------------------------------------*)
 109 (* good_properties : term list -> term -> term -> term -> bool                *)
 110 (*                                                                            *)
 111 (* Function to determine whether the recursive calls in the expansion of a    *)
 112 (* function call have good properties. The first argument is a list of        *)
 113 (* assumptions currently being made. The second argument is the original      *)
 114 (* call. The third argument is the (simplified) expansion of the call, and    *)
 115 (* the fourth argument is the term currently being processed and which        *)
 116 (* contains the function call.                                                *)
 117 (*----------------------------------------------------------------------------*)
 118
 119 (*< Boyer and Moore's heuristic
 120 let good_properties assumps call body_of_call tm =
 121  let rec in_assumps tm assumps =
 122     if (assumps = [])
 123     then false
 124     else if (is_subterm tm (hd assumps))
 125          then true
 126          else in_assumps tm (tl assumps)
 127  in
 128  (let name = fst (dest_const (fst (strip_comb call)))
 129   and body_less_call = hide_fun_call call tm
 130   in  let rec_calls = recursive_calls name body_of_call
 131   in  let bools = map (fun rc -> (no_new_terms rc body_less_call) or
 132                             (in_assumps rc assumps) or
 133                             (more_explicit_values call rc)) rec_calls
 134   in  itlist (fun x y -> x & y) bools true
 135  ) with Failure _ -> failwith "good_properties";;
 136 >*)
 137
 138 (* For HOL implementation, the restricted form of definitions allows all      *)
 139 (* recursive calls to be considered to have good properties.                  *)
 140
 141 let good_properties assumps call body_of_call tm = true;;