--- a/src/HOL/Tools/ATP/atp_translate.ML Mon Jun 06 20:56:06 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML Mon Jun 06 20:56:06 2011 +0200
@@ -52,8 +52,6 @@
Preds of polymorphism * type_level * type_heaviness |
Tags of polymorphism * type_level * type_heaviness
- type translated_formula
-
val bound_var_prefix : string
val schematic_var_prefix: string
val fixed_var_prefix: string
@@ -124,9 +122,6 @@
connective -> ('a, 'b, 'c) formula list -> ('a, 'b, 'c) formula
val unmangled_const_name : string -> string
val unmangled_const : string -> string * string fo_term list
- val translate_atp_fact :
- Proof.context -> format -> type_sys -> bool -> (string * locality) * thm
- -> translated_formula option * ((string * locality) * thm)
val helper_table : ((string * bool) * thm list) list
val should_specialize_helper : type_sys -> term -> bool
val tfree_classes_of_terms : term list -> string list
@@ -135,9 +130,9 @@
val prepare_atp_problem :
Proof.context -> format -> formula_kind -> formula_kind -> type_sys
-> bool option -> bool -> bool -> term list -> term
- -> (translated_formula option * ((string * 'a) * thm)) list
+ -> ((string * locality) * thm) list
-> string problem * string Symtab.table * int * int
- * (string * 'a) list vector * int list * int Symtab.table
+ * (string * locality) list vector * int list * int Symtab.table
val atp_problem_weights : string problem -> (string * real) list
end;
@@ -1348,9 +1343,6 @@
Symtab.fold_rev (append o helper_facts_for_sym ctxt format type_sys) sym_tab
[]
-fun translate_atp_fact ctxt format type_sys keep_trivial =
- `(make_fact ctxt format type_sys keep_trivial true true true o apsnd prop_of)
-
(***************************************************************)
(* Type Classes Present in the Axiom or Conjecture Clauses *)
(***************************************************************)
@@ -1391,15 +1383,17 @@
Symtab.keys (fold (add_type_constrs_in_term thy) ts Symtab.empty)
fun translate_formulas ctxt format prem_kind type_sys preproc hyp_ts concl_t
- rich_facts =
+ facts =
let
val thy = Proof_Context.theory_of ctxt
- val fact_ts = map (prop_of o snd o snd) rich_facts
+ val fact_ts = facts |> map (prop_of o snd)
val (facts, fact_names) =
- rich_facts
- |> map_filter (fn (NONE, _) => NONE
- | (SOME fact, (name, _)) => SOME (fact, name))
- |> ListPair.unzip
+ facts |> map (fn (name, th) =>
+ (name, prop_of th)
+ |> make_fact ctxt format type_sys false true true true
+ |> rpair name)
+ |> map_filter (try (apfst the))
+ |> ListPair.unzip
(* Remove existing facts from the conjecture, as this can dramatically
boost an ATP's performance (for some reason). *)
val hyp_ts =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Mon Jun 06 20:56:06 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Mon Jun 06 20:56:06 2011 +0200
@@ -11,7 +11,6 @@
type failure = ATP_Proof.failure
type locality = ATP_Translate.locality
type relevance_fudge = Sledgehammer_Filter.relevance_fudge
- type translated_formula = ATP_Translate.translated_formula
type type_sys = ATP_Translate.type_sys
type play = ATP_Reconstruct.play
type minimize_command = ATP_Reconstruct.minimize_command
@@ -388,8 +387,6 @@
fun untranslated_fact (Untranslated_Fact p) = p
| untranslated_fact (SMT_Weighted_Fact (info, (_, th))) = (info, th)
-fun atp_translated_fact ctxt format type_sys fact =
- translate_atp_fact ctxt format type_sys false (untranslated_fact fact)
fun smt_weighted_fact _ _ (SMT_Weighted_Fact p, _) = p
| smt_weighted_fact ctxt num_facts (fact, j) =
(untranslated_fact fact, j) |> weight_smt_fact ctxt num_facts
@@ -593,7 +590,6 @@
val num_actual_slices = length actual_slices
fun monomorphize_facts facts =
let
- val facts = facts |> map untranslated_fact
(* pseudo-theorem involving the same constants as the subgoal *)
val subgoal_th =
Logic.list_implies (hyp_ts, concl_t)
@@ -607,7 +603,7 @@
|> SMT_Monomorph.monomorph indexed_facts
|> fst |> sort (int_ord o pairself fst)
|> filter_out (curry (op =) ~1 o fst)
- |> map (Untranslated_Fact o apfst (fst o nth facts))
+ |> map (apfst (fst o nth facts))
end
fun run_slice blacklist (slice, (time_frac, (complete,
(best_max_relevant, best_type_systems))))
@@ -620,16 +616,14 @@
choose_format_and_type_sys best_type_systems formats type_sys
val fairly_sound = is_type_sys_fairly_sound type_sys
val facts =
- facts |> not fairly_sound
- ? filter_out (is_dangerous_prop ctxt o prop_of o snd
- o untranslated_fact)
+ facts |> map untranslated_fact
+ |> not fairly_sound
+ ? filter_out (is_dangerous_prop ctxt o prop_of o snd)
|> take num_facts
|> not (null blacklist)
- ? filter_out (member (op =) blacklist o fst
- o untranslated_fact)
+ ? filter_out (member (op =) blacklist o fst)
|> polymorphism_of_type_sys type_sys <> Polymorphic
? monomorphize_facts
- |> map (atp_translated_fact ctxt format type_sys)
val real_ms = Real.fromInt o Time.toMilliseconds
val slice_timeout =
((real_ms time_left
--- a/src/HOL/ex/tptp_export.ML Mon Jun 06 20:56:06 2011 +0200
+++ b/src/HOL/ex/tptp_export.ML Mon Jun 06 20:56:06 2011 +0200
@@ -100,9 +100,8 @@
val _ = File.write path ""
val facts0 = facts_of thy
val facts =
- facts0 |> map_filter (try (fn ((_, loc), (_, th)) =>
- ATP_Translate.translate_atp_fact ctxt format
- type_sys true ((Thm.get_name_hint th, loc), th)))
+ facts0 |> map (fn ((_, loc), (_, th)) =>
+ ((Thm.get_name_hint th, loc), th))
val explicit_apply = NONE
val (atp_problem, _, _, _, _, _, _) =
ATP_Translate.prepare_atp_problem ctxt format