# HG changeset patch # User blanchet # Date 1307386566 -7200 # Node ID 4e850b2c1f5c5fd266f61f109fb9af011efeb59b # Parent e1fdd27e0c988d96a53e2ff8a8ff6d66ec22f362 removed old optimization that isn't one anyone diff -r e1fdd27e0c98 -r 4e850b2c1f5c src/HOL/Tools/ATP/atp_translate.ML --- 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 = diff -r e1fdd27e0c98 -r 4e850b2c1f5c src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- 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 diff -r e1fdd27e0c98 -r 4e850b2c1f5c src/HOL/ex/tptp_export.ML --- 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