Boyer_Moore/environment.ml

   1 (******************************************************************************)
   2 (* FILE          : environment.ml                                             *)
   3 (* DESCRIPTION   : Environment of definitions and pre-proved theorems for use *)
   4 (*                 in automation.                                             *)
   5 (*                                                                            *)
   6 (* READS FILES   : <none>                                                     *)
   7 (* WRITES FILES  : <none>                                                     *)
   8 (*                                                                            *)
   9 (* AUTHOR        : R.J.Boulton                                                *)
  10 (* DATE          : 8th May 1991                                               *)
  11 (*                                                                            *)
  12 (* LAST MODIFIED : R.J.Boulton                                                *)
  13 (* DATE          : 12th October 1992                                          *)
  14 (*                                                                            *)
  15 (* LAST MODIFIED : P. Papapanagiotou (University of Edinburgh)                *)
  16 (* DATE          : July 2009                                                  *)
  17 (******************************************************************************)
  18
  19 let my_gen_terms = ref ([]:term list);;
  20 let bm_steps = ref (0,0);;
  21
  22
  23 let rec GSPEC th =
  24   let wl,w = dest_thm th in
  25   if is_forall w then
  26       GSPEC (SPEC (genvar (type_of (fst (dest_forall w)))) th)
  27   else th;;
  28
  29 let LIST_CONJ = end_itlist CONJ ;;
  30
  31 let rec CONJ_LIST n th =
  32   try if n=1 then [th] else (CONJUNCT1 th)::(CONJ_LIST (n-1) (CONJUNCT2 th))
  33   with Failure _ -> failwith "CONJ_LIST";;
  34
  35 (*----------------------------------------------------------------------------*)
  36 (* Reference variable to hold the defining theorems for operators currently   *)
  37 (* defined within the system. Each definition is stored as a triple. The      *)
  38 (* first component is the name of the operator. The second is the number of   *)
  39 (* the recursive argument. If the operator is not defined recursively, this   *)
  40 (* number is zero. The third component is a list of pairs of type constructor *)
  41 (* names and the theorems that define the behaviour of the operator for each  *)
  42 (* constructor. If the operator is not recursive, the constructor names are   *)
  43 (* empty (null) strings.                                                      *)
  44 (*----------------------------------------------------------------------------*)
  45
  46 let system_defs = ref ([] : (string * (int * (string * thm) list)) list);;
  47
  48 (*----------------------------------------------------------------------------*)
  49 (* new_def : thm -> void                                                      *)
  50 (*                                                                            *)
  51 (* Make a new definition available. Checks that theorem has no hypotheses,    *)
  52 (* then splits it into conjuncts. The variables for each conjunct are         *)
  53 (* specialised and then the conjuncts are made into equations.                *)
  54 (*                                                                            *)
  55 (* For each equation, a triple is obtained, consisting of the name of the     *)
  56 (* function on the LHS, the number of the recursive argument, and the name of *)
  57 (* the constructor used in that argument. This process fails if the LHS is    *)
  58 (* not an application of a constant (possibly to zero arguments), or if more  *)
  59 (* than one of the arguments is anything other than a variable. The argument  *)
  60 (* that is not a variable must be an application of a constructor. If the     *)
  61 (* function is not recursive, the argument number returned is zero.           *)
  62 (*                                                                            *)
  63 (* Having obtained a triple for each equation, a check is made that the first *)
  64 (* two components are the same for each equation. Then, the equations are     *)
  65 (* saved together with constructor names for each, and the name of the        *)
  66 (* operator being defined, and the number of the recursive argument.          *)
  67 (*----------------------------------------------------------------------------*)
  68
  69 let new_def th =
  70 try
  71  (let make_into_eqn th =
  72      let tm = concl th
  73      in  if (is_eq tm) then th
  74          else if (is_neg tm) then EQF_INTRO th
  75          else EQT_INTRO th
  76   and get_constructor th =
  77      let tm = lhs (concl th)
  78      in  let (f,args) = strip_comb tm
  79      in  let name = fst (dest_const f)
  80      in  let bools = number_list (map is_var args)
  81      in  let i = itlist (fun (b,i) n -> if ((not b) & (n = 0)) then i
  82                                    else if b then n else failwith "") bools 0
  83      in  if (i = 0)
  84          then ((name,i),"")
  85          else ((name,i),fst (dest_const (fst (strip_comb (el (i-1) args)))))
  86   in  let ([],tm) = dest_thm th
  87   in  let ths = CONJ_LIST (length (conj_list tm)) th
  88   in  let ths' = map SPEC_ALL ths
  89   in  let eqs = map make_into_eqn ths'
  90   in  let constructs = map get_constructor eqs
  91   in  let (xl,yl) = hashI setify (List.split constructs)
  92   in  let (name,i) = if (length xl = 1) then (hd xl) else failwith ""
  93   in  system_defs := (name,(i,List.combine yl eqs))::(!system_defs)
  94  ) with Failure _ -> failwith "new_def";;
  95
  96 (*----------------------------------------------------------------------------*)
  97 (* defs : void -> thm list list                                               *)
  98 (*                                                                            *)
  99 (* Returns a list of lists of theorems currently being used as definitions.   *)
 100 (* Each list in the list is for one operator.                                 *)
 101 (*----------------------------------------------------------------------------*)
 102
 103 let defs () = map ((map snd) o snd o snd) (!system_defs);;
 104 let defs_names () = map fst (!system_defs);;
 105
 106 (*----------------------------------------------------------------------------*)
 107 (* get_def : string -> (string # int # (string # thm) list)                   *)
 108 (*                                                                            *)
 109 (* Function to obtain the definition information of a named operator.         *)
 110 (*----------------------------------------------------------------------------*)
 111
 112 let get_def name = try ( assoc name (!system_defs) ) with Failure _ -> failwith "get_def";;
 113
 114 (*----------------------------------------------------------------------------*)
 115 (* Reference variable for a list of theorems currently proved in the system.  *)
 116 (* These theorems are available to the automatic proof procedures for use as  *)
 117 (* rewrite rules. The elements of the list are actually pairs of theorems.    *)
 118 (* The first theorem is that specified by the user. The second is an          *)
 119 (* equivalent theorem in a standard form.                                     *)
 120 (*----------------------------------------------------------------------------*)
 121
 122 let system_rewrites = ref ([] : (thm * thm) list);;
 123
 124 (*----------------------------------------------------------------------------*)
 125 (* CONJ_IMP_IMP_IMP = |- x /\ y ==> z = x ==> y ==> z                         *)
 126 (*----------------------------------------------------------------------------*)
 127
 128 let CONJ_IMP_IMP_IMP =
 129  prove
 130   (`((x /\ y) ==> z) = (x ==> (y ==> z))`,
 131    BOOL_CASES_TAC `x:bool` THEN
 132    BOOL_CASES_TAC `y:bool` THEN
 133    BOOL_CASES_TAC `z:bool` THEN
 134    REWRITE_TAC []);;
 135
 136 (*----------------------------------------------------------------------------*)
 137 (* CONJ_UNDISCH : thm -> thm                                                  *)
 138 (*                                                                            *)
 139 (* Undischarges the conjuncts of the antecedant of an implication.            *)
 140 (* e.g. |- x /\ (y /\ z) /\ w ==> x  --->  x, y /\ z, w |- x                  *)
 141 (*                                                                            *)
 142 (* Has to check for negations, because UNDISCH processes them when we don't   *)
 143 (* want it to.                                                                *)
 144 (*----------------------------------------------------------------------------*)
 145
 146 let rec CONJ_UNDISCH th =
 147 try
 148  (let th' = CONV_RULE (REWR_CONV CONJ_IMP_IMP_IMP) th
 149   in  let th'' = UNDISCH th'
 150   in  CONJ_UNDISCH th'')
 151  with Failure _ -> try (if not (is_neg (concl th)) then UNDISCH th else failwith "")
 152  with Failure _ -> failwith "CONJ_UNDISCH";;
 153
 154 (*----------------------------------------------------------------------------*)
 155 (* new_rewrite_rule : thm -> void                                             *)
 156 (*                                                                            *)
 157 (* Make a new rewrite rule available. Checks that theorem has no hypotheses.  *)
 158 (* The theorem is saved together with an equivalent theorem in a standard     *)
 159 (* form. Theorems are fully generalized, then specialized with unique         *)
 160 (* variable names (genvars), and then standardized as follows:                *)
 161 (*                                                                            *)
 162 (*    |- (h1 /\ ... /\ hn) ==> (l = r)  --->  h1, ..., hn |- l = r            *)
 163 (*    |- (h1 /\ ... /\ hn) ==> ~b       --->  h1, ..., hn |- b = F            *)
 164 (*    |- (h1 /\ ... /\ hn) ==> b        --->  h1, ..., hn |- b = T            *)
 165 (*    |- l = r                          --->  |- l = r                        *)
 166 (*    |- ~b                             --->  |- b = F                        *)
 167 (*    |- b                              --->  |- b = T                        *)
 168 (*                                                                            *)
 169 (* A conjunction of rules may be given. The function will treat each conjunct *)
 170 (* in the theorem as a separate rule.                                         *)
 171 (*----------------------------------------------------------------------------*)
 172
 173 let rec new_rewrite_rule th =
 174 try (if (is_conj (concl th))
 175   then (map new_rewrite_rule (CONJUNCTS th); ())
 176   else let ([],tm) = dest_thm th
 177   in  let th' = GSPEC (GEN_ALL th)
 178   in  let th'' = try (CONJ_UNDISCH th') with Failure _ -> th'
 179   in  let tm'' = concl th''
 180   in  let th''' =
 181          (if (is_eq tm'') then th''
 182          else if (is_neg tm'') then EQF_INTRO th''
 183          else EQT_INTRO th'')
 184   in system_rewrites := (th,th''')::(!system_rewrites)
 185  ) with Failure _ -> failwith "new_rewrite_rule";;
 186
 187 (*----------------------------------------------------------------------------*)
 188 (* rewrite_rules : void -> thm list                                           *)
 189 (*                                                                            *)
 190 (* Returns the list of theorems currently being used as rewrites, in the form *)
 191 (* they were originally given by the user.                                    *)
 192 (*----------------------------------------------------------------------------*)
 193
 194 let rewrite_rules () = map fst (!system_rewrites);;
 195
 196 (*----------------------------------------------------------------------------*)
 197 (* Reference variable to hold the generalisation lemmas currently known to    *)
 198 (* the system.                                                                *)
 199 (*----------------------------------------------------------------------------*)
 200
 201 let system_gen_lemmas = ref ([] : thm list);;
 202
 203 (*----------------------------------------------------------------------------*)
 204 (* new_gen_lemma : thm -> void                                                *)
 205 (*                                                                            *)
 206 (* Make a new generalisation lemma available.                                 *)
 207 (* Checks that the theorem has no hypotheses.                                 *)
 208 (*----------------------------------------------------------------------------*)
 209
 210 let new_gen_lemma th =
 211    if ((hyp th) = [])
 212    then system_gen_lemmas := th::(!system_gen_lemmas)
 213    else failwith "new_gen_lemma";;
 214
 215 (*----------------------------------------------------------------------------*)
 216 (* gen_lemmas : void -> thm list                                              *)
 217 (*                                                                            *)
 218 (* Returns the list of theorems currently being used as                       *)
 219 (* generalisation lemmas.                                                     *)
 220 (*----------------------------------------------------------------------------*)
 221
 222 let gen_lemmas () = !system_gen_lemmas;;
 223
 224
 225
 226 (*----------------------------------------------------------------------------*)
 227 (* max_var_depth : term -> int                                                *)
 228 (*                                                                            *)
 229 (* Returns the maximum depth of any variable in a term.                       *)
 230 (* eg. max_var_depth  `PRE (a + SUC c)` = 4                                   *)
 231 (*     max_var_depth  `a` = 1                                                 *)
 232 (*     max_var_depth  `PRE (5 + SUC 2)` = 0                                   *)
 233 (*     max_var_depth  `PRE (a + SUC 2)` = 3                                   *)
 234 (*----------------------------------------------------------------------------*)
 235 (* This is primarily used to limit non-termination. If max_var_depth exceeds  *)
 236 (* a limit the system will fail.                                              *)
 237 (* The algorithm is simple:                                                   *)
 238 (* if constant,numeral,etc then 0                                             *)
 239 (* else if variable then 1                                                    *)
 240 (* else if definition,constructor,accessor then                               *)
 241 (*         if (max_var_depth of arguments) > 0 then result + 1                *)
 242 (*         else 0                                                             *)
 243 (* else if any other combination then max_var_depth of arguments              *)
 244 (*----------------------------------------------------------------------------*)
 245
 246
 247 let rec max_var_depth tm =
 248   if (is_var tm) then 1
 249   else if ((is_numeral tm)
 250              or (is_const tm)
 251              or (is_T tm) or (is_F tm)) then 0
 252   else try
 253     let (f,args) = strip_comb tm in
 254     let fn = (fst o dest_const) f in
 255     let l = flat [defs_names();all_constructors();all_accessors()] in
 256     if (mem fn l) then
 257       let x = itlist max (map max_var_depth args) 0 in
 258       if (x>0) then x+1 else 0
 259     else itlist max (map max_var_depth args) 0
 260   with Failure _ -> 0;;