# HG changeset patch # User blanchet # Date 1306852716 -7200 # Node ID f181d66046d4123864b08d959a5797a63a05a6dc # Parent ccf1c09dea8230a637ac6de0928e3b6a377acd5f don't preprocess twice diff -r ccf1c09dea82 -r f181d66046d4 src/HOL/Tools/ATP/atp_translate.ML --- a/src/HOL/Tools/ATP/atp_translate.ML Tue May 31 16:38:36 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_translate.ML Tue May 31 16:38:36 2011 +0200 @@ -114,7 +114,7 @@ val type_consts_of_terms : theory -> term list -> string list val prepare_atp_problem : Proof.context -> format -> formula_kind -> formula_kind -> type_system - -> bool option -> bool -> term list -> term + -> bool option -> bool -> bool -> term list -> term -> (translated_formula option * ((string * 'a) * thm)) list -> string problem * string Symtab.table * int * int * (string * 'a) list vector * int list * int Symtab.table @@ -796,7 +796,8 @@ #>> uncurry (mk_aconn c) and do_formula bs t = case t of - @{const Not} $ t1 => do_formula bs t1 #>> mk_anot + @{const Trueprop} $ t1 => do_formula bs t1 + | @{const Not} $ t1 => do_formula bs t1 #>> mk_anot | Const (@{const_name All}, _) $ Abs (s, T, t') => do_quant bs AForall s T t' | Const (@{const_name Ex}, _) $ Abs (s, T, t') => @@ -879,22 +880,25 @@ | aux t = t in t |> exists_subterm is_Var t ? aux end -(* making fact and conjecture formulas *) -fun make_formula ctxt format type_sys eq_as_iff presimp name loc kind t = +fun preprocess_prop ctxt presimp kind t = let val thy = Proof_Context.theory_of ctxt val t = t |> Envir.beta_eta_contract |> transform_elim_prop |> Object_Logic.atomize_term thy val need_trueprop = (fastype_of t = @{typ bool}) - val t = t |> need_trueprop ? HOLogic.mk_Trueprop - |> Raw_Simplifier.rewrite_term thy - (Meson.unfold_set_const_simps ctxt) [] - |> extensionalize_term ctxt - |> presimp ? presimplify_term ctxt - |> perhaps (try (HOLogic.dest_Trueprop)) - |> introduce_combinators_in_term ctxt kind - |> kind <> Axiom ? freeze_term + in + t |> need_trueprop ? HOLogic.mk_Trueprop + |> Raw_Simplifier.rewrite_term thy (Meson.unfold_set_const_simps ctxt) [] + |> extensionalize_term ctxt + |> presimp ? presimplify_term ctxt + |> introduce_combinators_in_term ctxt kind + |> kind <> Axiom ? freeze_term + end + +(* making fact and conjecture formulas *) +fun make_formula thy format type_sys eq_as_iff name loc kind t = + let val (combformula, atomic_types) = combformula_from_prop thy format type_sys eq_as_iff t [] in @@ -902,16 +906,23 @@ atomic_types = atomic_types} end -fun make_fact ctxt format type_sys keep_trivial eq_as_iff presimp +fun make_fact ctxt format type_sys keep_trivial eq_as_iff preproc presimp ((name, loc), t) = - case (keep_trivial, - make_formula ctxt format type_sys eq_as_iff presimp name loc Axiom t) of - (false, formula as {combformula = AAtom (CombConst ((s, _), _, _)), ...}) => - if s = tptp_true then NONE else SOME formula - | (_, formula) => SOME formula + let val thy = Proof_Context.theory_of ctxt in + case (keep_trivial, + t |> preproc ? preprocess_prop ctxt presimp Axiom + |> make_formula thy format type_sys eq_as_iff name loc Axiom) of + (false, + formula as {combformula = AAtom (CombConst ((s, _), _, _)), ...}) => + if s = tptp_true then NONE else SOME formula + | (_, formula) => SOME formula + end -fun make_conjecture ctxt format prem_kind type_sys ts = - let val last = length ts - 1 in +fun make_conjecture ctxt format prem_kind type_sys preproc ts = + let + val thy = Proof_Context.theory_of ctxt + val last = length ts - 1 + in map2 (fn j => fn t => let val (kind, maybe_negate) = @@ -922,8 +933,9 @@ if prem_kind = Conjecture then update_combformula mk_anot else I) in - t |> make_formula ctxt format type_sys true true - (string_of_int j) General kind + t |> preproc ? preprocess_prop ctxt true kind + |> make_formula thy format type_sys true (string_of_int j) + General kind |> maybe_negate end) (0 upto last) ts @@ -1273,7 +1285,7 @@ | _ => I) end) fun make_facts eq_as_iff = - map_filter (make_fact ctxt format type_sys false eq_as_iff false) + map_filter (make_fact ctxt format type_sys true false eq_as_iff false) val fairly_sound = is_type_sys_fairly_sound type_sys in helper_table @@ -1292,7 +1304,7 @@ [] fun translate_atp_fact ctxt format type_sys keep_trivial = - `(make_fact ctxt format type_sys keep_trivial true true o apsnd prop_of) + `(make_fact ctxt format type_sys keep_trivial true true true o apsnd prop_of) (***************************************************************) (* Type Classes Present in the Axiom or Conjecture Clauses *) @@ -1331,8 +1343,7 @@ fun type_consts_of_terms thy ts = Symtab.keys (fold (add_type_consts_in_term thy) ts Symtab.empty) - -fun translate_formulas ctxt format prem_kind type_sys hyp_ts concl_t +fun translate_formulas ctxt format prem_kind type_sys preproc hyp_ts concl_t rich_facts = let val thy = Proof_Context.theory_of ctxt @@ -1351,7 +1362,8 @@ val supers = tvar_classes_of_terms all_ts val tycons = type_consts_of_terms thy all_ts val conjs = - hyp_ts @ [concl_t] |> make_conjecture ctxt format prem_kind type_sys + hyp_ts @ [concl_t] + |> make_conjecture ctxt format prem_kind type_sys preproc val (supers', arity_clauses) = if level_of_type_sys type_sys = No_Types then ([], []) else make_arity_clauses thy tycons supers @@ -1745,10 +1757,12 @@ val free_typesN = "Type variables" fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_sys - explicit_apply readable_names hyp_ts concl_t facts = + explicit_apply readable_names preproc hyp_ts concl_t + facts = let val (fact_names, (conjs, facts, class_rel_clauses, arity_clauses)) = - translate_formulas ctxt format prem_kind type_sys hyp_ts concl_t facts + translate_formulas ctxt format prem_kind type_sys preproc hyp_ts concl_t + facts val sym_tab = conjs @ facts |> sym_table_for_facts ctxt explicit_apply val nonmono_Ts = conjs @ facts |> nonmonotonic_types_for_facts ctxt type_sys val repair = repair_fact ctxt format nonmono_Ts type_sys sym_tab diff -r ccf1c09dea82 -r f181d66046d4 src/HOL/Tools/Metis/metis_translate.ML --- a/src/HOL/Tools/Metis/metis_translate.ML Tue May 31 16:38:36 2011 +0200 +++ b/src/HOL/Tools/Metis/metis_translate.ML Tue May 31 16:38:36 2011 +0200 @@ -44,8 +44,8 @@ val metis_name_table = [((tptp_equal, 2), metis_equal), ((tptp_old_equal, 2), metis_equal), - ((predicator_name, 1), metis_predicator), - ((app_op_name, 2), metis_app_op)] + ((const_prefix ^ predicator_name, 1), metis_predicator), + ((const_prefix ^ app_op_name, 2), metis_app_op)] fun predicate_of thy ((@{const Not} $ P), pos) = predicate_of thy (P, not pos) | predicate_of thy (t, pos) = @@ -314,9 +314,8 @@ val clauses = conj_clauses @ fact_clauses val (atp_problem, _, _, _, _, _, sym_tab) = prepare_atp_problem ctxt CNF Hypothesis Axiom type_sys - explicit_apply false (map prop_of clauses) + explicit_apply false false (map prop_of clauses) @{prop False} [] - (* val _ = tracing (PolyML.makestring atp_problem) FIXME ### *) val axioms = atp_problem |> maps (map_filter (try (metis_axiom_from_atp clauses)) o snd) diff -r ccf1c09dea82 -r f181d66046d4 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue May 31 16:38:36 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue May 31 16:38:36 2011 +0200 @@ -667,7 +667,8 @@ fact_names, typed_helpers, sym_tab) = prepare_atp_problem ctxt format conj_sym_kind prem_kind type_sys explicit_apply - (Config.get ctxt atp_readable_names) hyp_ts concl_t facts + (Config.get ctxt atp_readable_names) true hyp_ts concl_t + facts fun weights () = atp_problem_weights atp_problem val core = File.shell_path command ^ " " ^