--- a/src/HOL/TPTP/atp_export.ML Sun Jul 17 14:11:35 2011 +0200
+++ b/src/HOL/TPTP/atp_export.ML Sun Jul 17 14:11:35 2011 +0200
@@ -160,8 +160,8 @@
facts
|> map (fn ((_, loc), th) => ((Thm.get_name_hint th, loc), prop_of th))
|> prepare_atp_problem ctxt format Axiom Axiom type_enc true true
- (map (introduce_combinators ctxt)) false true []
- @{prop False}
+ (map (introduce_combinators ctxt o snd)) false true
+ [] @{prop False}
val atp_problem =
atp_problem
|> map (apsnd (filter_out (is_problem_line_tautology ctxt)))
--- a/src/HOL/Tools/ATP/atp_translate.ML Sun Jul 17 14:11:35 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML Sun Jul 17 14:11:35 2011 +0200
@@ -92,8 +92,8 @@
val introduce_combinators : Proof.context -> term -> term
val prepare_atp_problem :
Proof.context -> format -> formula_kind -> formula_kind -> type_enc -> bool
- -> bool -> (term list -> term list) -> bool -> bool -> term list -> term
- -> ((string * locality) * term) list
+ -> bool -> ((formula_kind * term) list -> term list) -> bool -> bool
+ -> term list -> term -> ((string * locality) * term) list
-> string problem * string Symtab.table * int * int
* (string * locality) list vector * int list * int Symtab.table
val atp_problem_weights : string problem -> (string * real) list
@@ -900,7 +900,7 @@
else
t
-fun generic_translate_lambdas do_lambdas ctxt t =
+fun simple_translate_lambdas do_lambdas ctxt t =
let
fun aux Ts t =
case t of
@@ -932,29 +932,25 @@
Free (concealed_lambda_prefix ^ string_of_int (hash_term t),
T --> fastype_of1 (Ts, t))
| do_conceal_lambdas _ t = t
-val conceal_lambdas = generic_translate_lambdas (K do_conceal_lambdas)
-
-fun do_introduce_combinators ctxt Ts =
- let val thy = Proof_Context.theory_of ctxt in
- conceal_bounds Ts
- #> cterm_of thy
- #> Meson_Clausify.introduce_combinators_in_cterm
- #> prop_of #> Logic.dest_equals #> snd
- #> reveal_bounds Ts
- end
-val introduce_combinators = generic_translate_lambdas do_introduce_combinators
+val conceal_lambdas = simple_translate_lambdas (K do_conceal_lambdas)
-fun process_abstractions_in_term ctxt trans_lambdas kind t =
+fun do_introduce_combinators ctxt Ts t =
let val thy = Proof_Context.theory_of ctxt in
- if Meson.is_fol_term thy t then
- t
- else
- t |> singleton trans_lambdas
- handle THM _ =>
- (* A type variable of sort "{}" will make abstraction fail. *)
- if kind = Conjecture then HOLogic.false_const
- else HOLogic.true_const
+ t |> conceal_bounds Ts
+ |> cterm_of thy
+ |> Meson_Clausify.introduce_combinators_in_cterm
+ |> prop_of |> Logic.dest_equals |> snd
+ |> reveal_bounds Ts
end
+ (* A type variable of sort "{}" will make abstraction fail. *)
+ handle THM _ => do_conceal_lambdas Ts t
+val introduce_combinators = simple_translate_lambdas do_introduce_combinators
+
+fun process_abstractions_in_terms ctxt trans_lambdas ps =
+ let
+ val thy = Proof_Context.theory_of ctxt
+ val (fo_ps, ho_ps) = ps |> List.partition (Meson.is_fol_term thy o snd)
+ in map snd fo_ps @ trans_lambdas ho_ps end
(* Metis's use of "resolve_tac" freezes the schematic variables. We simulate the
same in Sledgehammer to prevent the discovery of unreplayable proofs. *)
@@ -967,7 +963,7 @@
| aux t = t
in t |> exists_subterm is_Var t ? aux end
-fun preprocess_prop ctxt trans_lambdas presimp_consts kind t =
+fun preprocess_prop ctxt presimp_consts t =
let
val thy = Proof_Context.theory_of ctxt
val t = t |> Envir.beta_eta_contract
@@ -980,7 +976,6 @@
|> extensionalize_term ctxt
|> presimplify_term ctxt presimp_consts
|> perhaps (try (HOLogic.dest_Trueprop))
- |> process_abstractions_in_term ctxt trans_lambdas kind
end
(* making fact and conjecture formulas *)
@@ -1431,7 +1426,11 @@
let
val thy = Proof_Context.theory_of ctxt
val presimp_consts = Meson.presimplified_consts ctxt
- val preprocess = preprocess_prop ctxt trans_lambdas presimp_consts
+ fun preprocess kind =
+ preprocess_prop ctxt presimp_consts
+ #> pair kind #> single
+ #> process_abstractions_in_terms ctxt trans_lambdas
+ #> the_single
val fact_ts = facts |> map snd
(* Remove existing facts from the conjecture, as this can dramatically
boost an ATP's performance (for some reason). *)
--- a/src/HOL/Tools/Metis/metis_translate.ML Sun Jul 17 14:11:35 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_translate.ML Sun Jul 17 14:11:35 2011 +0200
@@ -197,8 +197,8 @@
*)
val (atp_problem, _, _, _, _, _, sym_tab) =
prepare_atp_problem ctxt CNF Hypothesis Axiom type_enc true false
- (map (introduce_combinators ctxt)) false false []
- @{prop False} props
+ (map (introduce_combinators ctxt o snd)) false false
+ [] @{prop False} props
(*
val _ = tracing ("ATP PROBLEM: " ^
cat_lines (tptp_lines_for_atp_problem CNF atp_problem))
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Sun Jul 17 14:11:35 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Sun Jul 17 14:11:35 2011 +0200
@@ -525,10 +525,14 @@
| NONE => type_enc_from_string best_type_enc)
|> choose_format formats
-fun lift_lambdas ctxt ts =
- case SMT_Translate.lift_lambdas ctxt false ts |> snd of
- (defs, [t]) => [foldr1 HOLogic.mk_conj (t :: defs)] (* FIXME: hack *)
- | (defs, ts) => ts @ defs
+fun lift_lambdas ctxt ps =
+ let
+ val ts = map snd ps (*###*)
+ in
+ case SMT_Translate.lift_lambdas ctxt false ts |> snd of
+ (defs, [t]) => [foldr1 HOLogic.mk_conj (t :: defs)] (* FIXME: hack *)
+ | (defs, ts) => ts @ defs
+ end
fun translate_atp_lambdas ctxt type_enc =
Config.get ctxt atp_lambda_translation
@@ -542,11 +546,16 @@
else
trans)
|> (fn trans =>
- if trans = concealed_lambdasN then map (conceal_lambdas ctxt)
- else if trans = lambda_liftingN then lift_lambdas ctxt
- else if trans = combinatorsN then map (introduce_combinators ctxt)
- else if trans = lambdasN then map Envir.eta_contract
- else error ("Unknown lambda translation method: " ^ quote trans ^ "."))
+ if trans = concealed_lambdasN then
+ map (conceal_lambdas ctxt o snd)
+ else if trans = lambda_liftingN then
+ lift_lambdas ctxt
+ else if trans = combinatorsN then
+ map (introduce_combinators ctxt o snd)
+ else if trans = lambdasN then
+ map (Envir.eta_contract o snd)
+ else
+ error ("Unknown lambda translation method: " ^ quote trans ^ "."))
val metis_minimize_max_time = seconds 2.0