move "prepare_clauses" from "sledgehammer_fact_filter.ML" to "sledgehammer_hol_clause.ML";
authorblanchet
Fri Jun 25 15:01:35 2010 +0200 (2010-06-25 ago)
changeset 375669ca40dff25bd
parent 37553 08fc6b026b01
child 37567 02e4ccd512b6
move "prepare_clauses" from "sledgehammer_fact_filter.ML" to "sledgehammer_hol_clause.ML";
since it has nothing to do with filtering
src/HOL/Tools/Sledgehammer/metis_tactics.ML
src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Fri Jun 25 12:15:49 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Fri Jun 25 15:01:35 2010 +0200
     1.3 @@ -23,7 +23,6 @@
     1.4  open Sledgehammer_Fact_Preprocessor
     1.5  open Sledgehammer_HOL_Clause
     1.6  open Sledgehammer_Proof_Reconstruct
     1.7 -open Sledgehammer_Fact_Filter
     1.8  open Sledgehammer_TPTP_Format
     1.9  
    1.10  exception METIS of string * string
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Fri Jun 25 12:15:49 2010 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Fri Jun 25 15:01:35 2010 +0200
     2.3 @@ -18,18 +18,9 @@
     2.4    val use_natural_form : bool Unsynchronized.ref
     2.5    val name_thms_pair_from_ref :
     2.6      Proof.context -> thm list -> Facts.ref -> string * thm list
     2.7 -  val tvar_classes_of_terms : term list -> string list
     2.8 -  val tfree_classes_of_terms : term list -> string list
     2.9 -  val type_consts_of_terms : theory -> term list -> string list
    2.10 -  val is_quasi_fol_theorem : theory -> thm -> bool
    2.11    val relevant_facts :
    2.12      bool -> bool -> real -> real -> bool -> int -> bool -> relevance_override
    2.13      -> Proof.context * (thm list * 'a) -> thm list -> cnf_thm list
    2.14 -  val prepare_clauses :
    2.15 -    bool -> thm list -> cnf_thm list -> cnf_thm list -> theory
    2.16 -    -> string vector
    2.17 -       * (hol_clause list * hol_clause list * hol_clause list
    2.18 -          * hol_clause list * classrel_clause list * arity_clause list)
    2.19  end;
    2.20  
    2.21  structure Sledgehammer_Fact_Filter : SLEDGEHAMMER_FACT_FILTER =
    2.22 @@ -392,10 +383,6 @@
    2.23  
    2.24  (*** retrieve lemmas and filter them ***)
    2.25  
    2.26 -(*Hashing to detect duplicate and variant clauses, e.g. from the [iff] attribute*)
    2.27 -
    2.28 -fun setinsert (x,s) = Symtab.update (x,()) s;
    2.29 -
    2.30  (*Reject theorems with names like "List.filter.filter_list_def" or
    2.31    "Accessible_Part.acc.defs", as these are definitions arising from packages.*)
    2.32  fun is_package_def a =
    2.33 @@ -406,16 +393,7 @@
    2.34       String.isSuffix "_def" a  orelse  String.isSuffix "_defs" a
    2.35    end;
    2.36  
    2.37 -fun mk_clause_table xs =
    2.38 -  fold (Termtab.update o `(prop_of o fst)) xs Termtab.empty
    2.39 -
    2.40 -fun make_unique xs =
    2.41 -  Termtab.fold (cons o snd) (mk_clause_table xs) []
    2.42 -
    2.43 -(* Remove existing axiom clauses from the conjecture clauses, as this can
    2.44 -   dramatically boost an ATP's performance (for some reason). *)
    2.45 -fun subtract_cls ax_clauses =
    2.46 -  filter_out (Termtab.defined (mk_clause_table ax_clauses) o prop_of)
    2.47 +fun make_unique xs = Termtab.fold (cons o snd) (make_clause_table xs) []
    2.48  
    2.49  val exists_sledgehammer_const =
    2.50    exists_Const (fn (s, _) => String.isPrefix sledgehammer_prefix s) o prop_of
    2.51 @@ -491,48 +469,9 @@
    2.52  
    2.53  
    2.54  (***************************************************************)
    2.55 -(* Type Classes Present in the Axiom or Conjecture Clauses     *)
    2.56 -(***************************************************************)
    2.57 -
    2.58 -fun add_classes (sorts, cset) = List.foldl setinsert cset (flat sorts);
    2.59 -
    2.60 -(*Remove this trivial type class*)
    2.61 -fun delete_type cset = Symtab.delete_safe (the_single @{sort HOL.type}) cset;
    2.62 -
    2.63 -fun tvar_classes_of_terms ts =
    2.64 -  let val sorts_list = map (map #2 o OldTerm.term_tvars) ts
    2.65 -  in  Symtab.keys (delete_type (List.foldl add_classes Symtab.empty sorts_list))  end;
    2.66 -
    2.67 -fun tfree_classes_of_terms ts =
    2.68 -  let val sorts_list = map (map #2 o OldTerm.term_tfrees) ts
    2.69 -  in  Symtab.keys (delete_type (List.foldl add_classes Symtab.empty sorts_list))  end;
    2.70 -
    2.71 -(*fold type constructors*)
    2.72 -fun fold_type_consts f (Type (a, Ts)) x = fold (fold_type_consts f) Ts (f (a,x))
    2.73 -  | fold_type_consts _ _ x = x;
    2.74 -
    2.75 -(*Type constructors used to instantiate overloaded constants are the only ones needed.*)
    2.76 -fun add_type_consts_in_term thy =
    2.77 -  let
    2.78 -    val const_typargs = Sign.const_typargs thy
    2.79 -    fun aux (Const cT) = fold (fold_type_consts setinsert) (const_typargs cT)
    2.80 -      | aux (Abs (_, _, u)) = aux u
    2.81 -      | aux (Const (@{const_name skolem_id}, _) $ _) = I
    2.82 -      | aux (t $ u) = aux t #> aux u
    2.83 -      | aux _ = I
    2.84 -  in aux end
    2.85 -
    2.86 -fun type_consts_of_terms thy ts =
    2.87 -  Symtab.keys (fold (add_type_consts_in_term thy) ts Symtab.empty);
    2.88 -
    2.89 -
    2.90 -(***************************************************************)
    2.91  (* ATP invocation methods setup                                *)
    2.92  (***************************************************************)
    2.93  
    2.94 -fun is_quasi_fol_theorem thy =
    2.95 -  Meson.is_fol_term thy o snd o conceal_skolem_somes ~1 [] o prop_of
    2.96 -
    2.97  (**** Predicates to detect unwanted clauses (prolific or likely to cause
    2.98        unsoundness) ****)
    2.99  
   2.100 @@ -581,8 +520,6 @@
   2.101      (has_typed_var dangerous_types t orelse
   2.102       forall too_general_equality (HOLogic.disjuncts (strip_Trueprop t)))
   2.103  
   2.104 -fun is_fol_goal thy = forall (Meson.is_fol_term thy) o map prop_of
   2.105 -
   2.106  fun relevant_facts full_types respect_no_atp relevance_threshold
   2.107                     relevance_convergence defs_relevant max_new theory_relevant
   2.108                     (relevance_override as {add, del, only})
   2.109 @@ -591,7 +528,7 @@
   2.110      val thy = ProofContext.theory_of ctxt
   2.111      val add_thms = maps (ProofContext.get_fact ctxt) add
   2.112      val has_override = not (null add) orelse not (null del)
   2.113 -    val is_FO = is_fol_goal thy goal_cls
   2.114 +    val is_FO = forall (Meson.is_fol_term thy o prop_of) goal_cls
   2.115      val axioms =
   2.116        checked_name_thm_pairs (respect_no_atp andalso not only) ctxt
   2.117            (map (name_thms_pair_from_ref ctxt chained_ths) add @
   2.118 @@ -611,70 +548,4 @@
   2.119      |> sort (prod_ord string_ord int_ord o pairself (fst o snd))
   2.120    end
   2.121  
   2.122 -(** Helper clauses **)
   2.123 -
   2.124 -fun count_combterm (CombConst ((c, _), _, _)) =
   2.125 -    Symtab.map_entry c (Integer.add 1)
   2.126 -  | count_combterm (CombVar _) = I
   2.127 -  | count_combterm (CombApp (t1, t2)) = count_combterm t1 #> count_combterm t2
   2.128 -fun count_literal (Literal (_, t)) = count_combterm t
   2.129 -fun count_clause (HOLClause {literals, ...}) = fold count_literal literals
   2.130 -
   2.131 -fun raw_cnf_rules_pairs ps = map (fn (name, thm) => (thm, ((name, 0), thm))) ps
   2.132 -fun cnf_helper_thms thy raw =
   2.133 -  map (`Thm.get_name_hint)
   2.134 -  #> (if raw then raw_cnf_rules_pairs else cnf_rules_pairs thy)
   2.135 -
   2.136 -val optional_helpers =
   2.137 -  [(["c_COMBI", "c_COMBK"], (false, @{thms COMBI_def COMBK_def})),
   2.138 -   (["c_COMBB", "c_COMBC"], (false, @{thms COMBB_def COMBC_def})),
   2.139 -   (["c_COMBS"], (false, @{thms COMBS_def}))]
   2.140 -val optional_typed_helpers =
   2.141 -  [(["c_True", "c_False"], (true, @{thms True_or_False})),
   2.142 -   (["c_If"], (true, @{thms if_True if_False True_or_False}))]
   2.143 -val mandatory_helpers = @{thms fequal_imp_equal equal_imp_fequal}
   2.144 -
   2.145 -val init_counters =
   2.146 -  Symtab.make (maps (maps (map (rpair 0) o fst))
   2.147 -                    [optional_helpers, optional_typed_helpers])
   2.148 -
   2.149 -fun get_helper_clauses thy is_FO full_types conjectures axcls =
   2.150 -  let
   2.151 -    val axclauses = map snd (make_axiom_clauses thy axcls)
   2.152 -    val ct = fold (fold count_clause) [conjectures, axclauses] init_counters
   2.153 -    fun is_needed c = the (Symtab.lookup ct c) > 0
   2.154 -    val cnfs =
   2.155 -      (optional_helpers
   2.156 -       |> full_types ? append optional_typed_helpers
   2.157 -       |> maps (fn (ss, (raw, ths)) =>
   2.158 -                   if exists is_needed ss then cnf_helper_thms thy raw ths
   2.159 -                   else []))
   2.160 -      @ (if is_FO then [] else cnf_helper_thms thy false mandatory_helpers)
   2.161 -  in map snd (make_axiom_clauses thy cnfs) end
   2.162 -
   2.163 -(* prepare for passing to writer,
   2.164 -   create additional clauses based on the information from extra_cls *)
   2.165 -fun prepare_clauses full_types goal_cls axcls extra_cls thy =
   2.166 -  let
   2.167 -    val is_FO = is_fol_goal thy goal_cls
   2.168 -    val ccls = subtract_cls extra_cls goal_cls
   2.169 -    val _ = app (fn th => trace_msg (fn _ => Display.string_of_thm_global thy th)) ccls
   2.170 -    val ccltms = map prop_of ccls
   2.171 -    and axtms = map (prop_of o #1) extra_cls
   2.172 -    val subs = tfree_classes_of_terms ccltms
   2.173 -    and supers = tvar_classes_of_terms axtms
   2.174 -    and tycons = type_consts_of_terms thy (ccltms @ axtms)
   2.175 -    (*TFrees in conjecture clauses; TVars in axiom clauses*)
   2.176 -    val conjectures = make_conjecture_clauses thy ccls
   2.177 -    val (_, extra_clauses) = ListPair.unzip (make_axiom_clauses thy extra_cls)
   2.178 -    val (clnames, axiom_clauses) = ListPair.unzip (make_axiom_clauses thy axcls)
   2.179 -    val helper_clauses =
   2.180 -      get_helper_clauses thy is_FO full_types conjectures extra_cls
   2.181 -    val (supers', arity_clauses) = make_arity_clauses thy tycons supers
   2.182 -    val classrel_clauses = make_classrel_clauses thy subs supers'
   2.183 -  in
   2.184 -    (Vector.fromList clnames,
   2.185 -      (conjectures, axiom_clauses, extra_clauses, helper_clauses, classrel_clauses, arity_clauses))
   2.186 -  end
   2.187 -
   2.188  end;
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Fri Jun 25 12:15:49 2010 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Fri Jun 25 15:01:35 2010 +0200
     3.3 @@ -27,15 +27,23 @@
     3.4    datatype hol_clause =
     3.5      HOLClause of {clause_id: int, axiom_name: string, th: thm, kind: kind,
     3.6                    literals: literal list, ctypes_sorts: typ list}
     3.7 +  exception TRIVIAL of unit
     3.8  
     3.9    val type_of_combterm : combterm -> combtyp
    3.10    val strip_combterm_comb : combterm -> combterm * combterm list
    3.11    val literals_of_term : theory -> term -> literal list * typ list
    3.12    val conceal_skolem_somes :
    3.13      int -> (string * term) list -> term -> (string * term) list * term
    3.14 -  exception TRIVIAL of unit
    3.15 -  val make_conjecture_clauses : theory -> thm list -> hol_clause list
    3.16 -  val make_axiom_clauses : theory -> cnf_thm list -> (string * hol_clause) list
    3.17 +  val is_quasi_fol_theorem : theory -> thm -> bool
    3.18 +  val make_clause_table : (thm * 'a) list -> (thm * 'a) Termtab.table
    3.19 +  val tfree_classes_of_terms : term list -> string list
    3.20 +  val tvar_classes_of_terms : term list -> string list
    3.21 +  val type_consts_of_terms : theory -> term list -> string list
    3.22 +  val prepare_clauses :
    3.23 +    bool -> thm list -> cnf_thm list -> cnf_thm list -> theory
    3.24 +    -> string vector
    3.25 +       * (hol_clause list * hol_clause list * hol_clause list * hol_clause list
    3.26 +          * classrel_clause list * arity_clause list)
    3.27  end
    3.28  
    3.29  structure Sledgehammer_HOL_Clause : SLEDGEHAMMER_HOL_CLAUSE =
    3.30 @@ -192,6 +200,9 @@
    3.31    else
    3.32      (skolem_somes, t)
    3.33  
    3.34 +fun is_quasi_fol_theorem thy =
    3.35 +  Meson.is_fol_term thy o snd o conceal_skolem_somes ~1 [] o prop_of
    3.36 +
    3.37  (* Trivial problem, which resolution cannot handle (empty clause) *)
    3.38  exception TRIVIAL of unit
    3.39  
    3.40 @@ -228,4 +239,116 @@
    3.41          in cls :: aux (n + 1) skolem_somes ths end
    3.42    in aux 0 [] end
    3.43  
    3.44 +(** Helper clauses **)
    3.45 +
    3.46 +fun count_combterm (CombConst ((c, _), _, _)) =
    3.47 +    Symtab.map_entry c (Integer.add 1)
    3.48 +  | count_combterm (CombVar _) = I
    3.49 +  | count_combterm (CombApp (t1, t2)) = count_combterm t1 #> count_combterm t2
    3.50 +fun count_literal (Literal (_, t)) = count_combterm t
    3.51 +fun count_clause (HOLClause {literals, ...}) = fold count_literal literals
    3.52 +
    3.53 +fun raw_cnf_rules_pairs ps = map (fn (name, thm) => (thm, ((name, 0), thm))) ps
    3.54 +fun cnf_helper_thms thy raw =
    3.55 +  map (`Thm.get_name_hint)
    3.56 +  #> (if raw then raw_cnf_rules_pairs else cnf_rules_pairs thy)
    3.57 +
    3.58 +val optional_helpers =
    3.59 +  [(["c_COMBI", "c_COMBK"], (false, @{thms COMBI_def COMBK_def})),
    3.60 +   (["c_COMBB", "c_COMBC"], (false, @{thms COMBB_def COMBC_def})),
    3.61 +   (["c_COMBS"], (false, @{thms COMBS_def}))]
    3.62 +val optional_typed_helpers =
    3.63 +  [(["c_True", "c_False"], (true, @{thms True_or_False})),
    3.64 +   (["c_If"], (true, @{thms if_True if_False True_or_False}))]
    3.65 +val mandatory_helpers = @{thms fequal_imp_equal equal_imp_fequal}
    3.66 +
    3.67 +val init_counters =
    3.68 +  Symtab.make (maps (maps (map (rpair 0) o fst))
    3.69 +                    [optional_helpers, optional_typed_helpers])
    3.70 +
    3.71 +fun get_helper_clauses thy is_FO full_types conjectures axcls =
    3.72 +  let
    3.73 +    val axclauses = map snd (make_axiom_clauses thy axcls)
    3.74 +    val ct = fold (fold count_clause) [conjectures, axclauses] init_counters
    3.75 +    fun is_needed c = the (Symtab.lookup ct c) > 0
    3.76 +    val cnfs =
    3.77 +      (optional_helpers
    3.78 +       |> full_types ? append optional_typed_helpers
    3.79 +       |> maps (fn (ss, (raw, ths)) =>
    3.80 +                   if exists is_needed ss then cnf_helper_thms thy raw ths
    3.81 +                   else []))
    3.82 +      @ (if is_FO then [] else cnf_helper_thms thy false mandatory_helpers)
    3.83 +  in map snd (make_axiom_clauses thy cnfs) end
    3.84 +
    3.85 +fun make_clause_table xs =
    3.86 +  fold (Termtab.update o `(prop_of o fst)) xs Termtab.empty
    3.87 +
    3.88 +
    3.89 +(***************************************************************)
    3.90 +(* Type Classes Present in the Axiom or Conjecture Clauses     *)
    3.91 +(***************************************************************)
    3.92 +
    3.93 +fun set_insert (x, s) = Symtab.update (x, ()) s
    3.94 +
    3.95 +fun add_classes (sorts, cset) = List.foldl set_insert cset (flat sorts)
    3.96 +
    3.97 +(*Remove this trivial type class*)
    3.98 +fun delete_type cset = Symtab.delete_safe (the_single @{sort HOL.type}) cset;
    3.99 +
   3.100 +fun tfree_classes_of_terms ts =
   3.101 +  let val sorts_list = map (map #2 o OldTerm.term_tfrees) ts
   3.102 +  in  Symtab.keys (delete_type (List.foldl add_classes Symtab.empty sorts_list))  end;
   3.103 +
   3.104 +fun tvar_classes_of_terms ts =
   3.105 +  let val sorts_list = map (map #2 o OldTerm.term_tvars) ts
   3.106 +  in  Symtab.keys (delete_type (List.foldl add_classes Symtab.empty sorts_list))  end;
   3.107 +
   3.108 +(*fold type constructors*)
   3.109 +fun fold_type_consts f (Type (a, Ts)) x = fold (fold_type_consts f) Ts (f (a,x))
   3.110 +  | fold_type_consts _ _ x = x;
   3.111 +
   3.112 +(*Type constructors used to instantiate overloaded constants are the only ones needed.*)
   3.113 +fun add_type_consts_in_term thy =
   3.114 +  let
   3.115 +    val const_typargs = Sign.const_typargs thy
   3.116 +    fun aux (Const x) = fold (fold_type_consts set_insert) (const_typargs x)
   3.117 +      | aux (Abs (_, _, u)) = aux u
   3.118 +      | aux (Const (@{const_name skolem_id}, _) $ _) = I
   3.119 +      | aux (t $ u) = aux t #> aux u
   3.120 +      | aux _ = I
   3.121 +  in aux end
   3.122 +
   3.123 +fun type_consts_of_terms thy ts =
   3.124 +  Symtab.keys (fold (add_type_consts_in_term thy) ts Symtab.empty);
   3.125 +
   3.126 +(* Remove existing axiom clauses from the conjecture clauses, as this can
   3.127 +   dramatically boost an ATP's performance (for some reason). *)
   3.128 +fun subtract_cls ax_clauses =
   3.129 +  filter_out (Termtab.defined (make_clause_table ax_clauses) o prop_of)
   3.130 +
   3.131 +(* prepare for passing to writer,
   3.132 +   create additional clauses based on the information from extra_cls *)
   3.133 +fun prepare_clauses full_types goal_cls axcls extra_cls thy =
   3.134 +  let
   3.135 +    val is_FO = forall (Meson.is_fol_term thy o prop_of) goal_cls
   3.136 +    val ccls = subtract_cls extra_cls goal_cls
   3.137 +    val _ = app (fn th => trace_msg (fn _ => Display.string_of_thm_global thy th)) ccls
   3.138 +    val ccltms = map prop_of ccls
   3.139 +    and axtms = map (prop_of o #1) extra_cls
   3.140 +    val subs = tfree_classes_of_terms ccltms
   3.141 +    and supers = tvar_classes_of_terms axtms
   3.142 +    and tycons = type_consts_of_terms thy (ccltms @ axtms)
   3.143 +    (*TFrees in conjecture clauses; TVars in axiom clauses*)
   3.144 +    val conjectures = make_conjecture_clauses thy ccls
   3.145 +    val (_, extra_clauses) = ListPair.unzip (make_axiom_clauses thy extra_cls)
   3.146 +    val (clnames, axiom_clauses) = ListPair.unzip (make_axiom_clauses thy axcls)
   3.147 +    val helper_clauses =
   3.148 +      get_helper_clauses thy is_FO full_types conjectures extra_cls
   3.149 +    val (supers', arity_clauses) = make_arity_clauses thy tycons supers
   3.150 +    val classrel_clauses = make_classrel_clauses thy subs supers'
   3.151 +  in
   3.152 +    (Vector.fromList clnames,
   3.153 +      (conjectures, axiom_clauses, extra_clauses, helper_clauses, classrel_clauses, arity_clauses))
   3.154 +  end
   3.155 +
   3.156  end;