--- a/src/HOL/TPTP/atp_export.ML Tue Aug 09 09:05:21 2011 +0200
+++ b/src/HOL/TPTP/atp_export.ML Tue Aug 09 09:05:22 2011 +0200
@@ -160,8 +160,7 @@
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
- (rpair [] o map (introduce_combinators ctxt))
- false true [] @{prop False}
+ combinatorsN 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 Tue Aug 09 09:05:21 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML Tue Aug 09 09:05:22 2011 +0200
@@ -31,6 +31,13 @@
Guards of polymorphism * type_level * type_heaviness |
Tags of polymorphism * type_level * type_heaviness
+ val no_lambdasN : string
+ val concealedN : string
+ val liftingN : string
+ val combinatorsN : string
+ val hybridN : string
+ val lambdasN : string
+ val smartN : string
val bound_var_prefix : string
val schematic_var_prefix : string
val fixed_var_prefix : string
@@ -88,11 +95,10 @@
val unmangled_const_name : string -> string
val helper_table : ((string * bool) * thm list) list
val factsN : string
- 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 * term list) -> bool -> bool -> term list
- -> term -> ((string * locality) * term) list
+ -> bool -> string -> 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
@@ -106,6 +112,14 @@
type name = string * string
+val no_lambdasN = "no_lambdas"
+val concealedN = "concealed"
+val liftingN = "lifting"
+val combinatorsN = "combinators"
+val hybridN = "hybrid"
+val lambdasN = "lambdas"
+val smartN = "smart"
+
val generate_info = false (* experimental *)
fun isabelle_info s =
@@ -606,6 +620,29 @@
| _ => type_enc)
| format => (format, type_enc))
+fun lift_lambdas ctxt type_enc =
+ map (close_form o Envir.eta_contract) #> rpair ctxt
+ #-> Lambda_Lifting.lift_lambdas
+ (if polymorphism_of_type_enc type_enc = Polymorphic then
+ SOME polymorphic_free_prefix
+ else
+ NONE)
+ Lambda_Lifting.is_quantifier
+ #> fst
+
+fun intentionalize_def (Const (@{const_name All}, _) $ Abs (_, _, t)) =
+ intentionalize_def t
+ | intentionalize_def (Const (@{const_name HOL.eq}, _) $ t $ u) =
+ let
+ fun lam T t = Abs (Name.uu, T, t)
+ val (head, args) = strip_comb t ||> rev
+ val head_T = fastype_of head
+ val n = length args
+ val arg_Ts = head_T |> binder_types |> take n |> rev
+ val u = u |> subst_atomic (args ~~ map Bound (0 upto n - 1))
+ in HOLogic.eq_const head_T $ head $ fold lam arg_Ts u end
+ | intentionalize_def t = t
+
type translated_formula =
{name : string,
locality : locality,
@@ -1918,9 +1955,36 @@
val explicit_apply = NONE (* for experiments *)
fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_enc sound
- exporter trans_lambdas readable_names preproc hyp_ts concl_t facts =
+ exporter lambda_trans readable_names preproc hyp_ts concl_t facts =
let
val (format, type_enc) = choose_format [format] type_enc
+ val lambda_trans =
+ if lambda_trans = smartN then
+ if is_type_enc_higher_order type_enc then lambdasN else combinatorsN
+ else if lambda_trans = lambdasN andalso
+ not (is_type_enc_higher_order type_enc) then
+ error ("Lambda translation method incompatible with first-order \
+ \encoding.")
+ else
+ lambda_trans
+ val trans_lambdas =
+ if lambda_trans = no_lambdasN then
+ rpair []
+ else if lambda_trans = concealedN then
+ lift_lambdas ctxt type_enc ##> K []
+ else if lambda_trans = liftingN then
+ lift_lambdas ctxt type_enc
+ else if lambda_trans = combinatorsN then
+ map (introduce_combinators ctxt) #> rpair []
+ else if lambda_trans = hybridN then
+ lift_lambdas ctxt type_enc
+ ##> maps (fn t => [t, introduce_combinators ctxt
+ (intentionalize_def t)])
+ else if lambda_trans = lambdasN then
+ map (Envir.eta_contract) #> rpair []
+ else
+ error ("Unknown lambda translation method: " ^
+ quote lambda_trans ^ ".")
val (fact_names, (conjs, facts, class_rel_clauses, arity_clauses)) =
translate_formulas ctxt format prem_kind type_enc trans_lambdas preproc
hyp_ts concl_t facts
--- a/src/HOL/Tools/Metis/metis_translate.ML Tue Aug 09 09:05:21 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_translate.ML Tue Aug 09 09:05:22 2011 +0200
@@ -197,7 +197,7 @@
*)
val (atp_problem, _, _, _, _, _, sym_tab) =
prepare_atp_problem ctxt CNF Hypothesis Axiom type_enc true false
- (rpair []) false false [] @{prop False} props
+ no_lambdasN 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 Tue Aug 09 09:05:21 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Aug 09 09:05:22 2011 +0200
@@ -60,12 +60,6 @@
type prover =
params -> (string -> minimize_command) -> prover_problem -> prover_result
- val concealedN : string
- val liftingN : string
- val combinatorsN : string
- val hybridN : string
- val lambdasN : string
- val smartN : string
val dest_dir : string Config.T
val problem_prefix : string Config.T
val measure_run_time : bool Config.T
@@ -335,13 +329,6 @@
(* configuration attributes *)
-val concealedN = "concealed"
-val liftingN = "lifting"
-val combinatorsN = "combinators"
-val hybridN = "hybrid"
-val lambdasN = "lambdas"
-val smartN = "smart"
-
(* Empty string means create files in Isabelle's temporary files directory. *)
val dest_dir =
Attrib.setup_config_string @{binding sledgehammer_dest_dir} (K "")
@@ -527,56 +514,6 @@
| NONE => type_enc_from_string best_type_enc)
|> choose_format formats
-fun lift_lambdas ctxt type_enc =
- map (close_form o Envir.eta_contract) #> rpair ctxt
- #-> Lambda_Lifting.lift_lambdas
- (if polymorphism_of_type_enc type_enc = Polymorphic then
- SOME polymorphic_free_prefix
- else
- NONE)
- Lambda_Lifting.is_quantifier
- #> fst
-
-fun intentionalize_def (Const (@{const_name All}, _) $ Abs (_, _, t)) =
- intentionalize_def t
- | intentionalize_def (Const (@{const_name HOL.eq}, _) $ t $ u) =
- let
- fun lam T t = Abs (Name.uu, T, t)
- val (head, args) = strip_comb t ||> rev
- val head_T = fastype_of head
- val n = length args
- val arg_Ts = head_T |> binder_types |> take n |> rev
- val u = u |> subst_atomic (args ~~ map Bound (0 upto n - 1))
- in HOLogic.eq_const head_T $ head $ fold lam arg_Ts u end
- | intentionalize_def t = t
-
-fun translate_atp_lambdas ctxt type_enc =
- Config.get ctxt atp_lambda_translation
- |> (fn trans =>
- if trans = smartN then
- if is_type_enc_higher_order type_enc then lambdasN else combinatorsN
- else if trans = lambdasN andalso
- not (is_type_enc_higher_order type_enc) then
- error ("Lambda translation method incompatible with first-order \
- \encoding.")
- else
- trans)
- |> (fn trans =>
- if trans = concealedN then
- lift_lambdas ctxt type_enc ##> K []
- else if trans = liftingN then
- lift_lambdas ctxt type_enc
- else if trans = combinatorsN then
- map (introduce_combinators ctxt) #> rpair []
- else if trans = hybridN then
- lift_lambdas ctxt type_enc
- ##> maps (fn t => [t, introduce_combinators ctxt
- (intentionalize_def t)])
- else if trans = lambdasN then
- map (Envir.eta_contract) #> rpair []
- else
- error ("Unknown lambda translation method: " ^ quote trans ^ "."))
-
val metis_minimize_max_time = seconds 2.0
fun choose_minimize_command minimize_command name preplay =
@@ -708,7 +645,8 @@
val (atp_problem, pool, conjecture_offset, facts_offset,
fact_names, typed_helpers, sym_tab) =
prepare_atp_problem ctxt format conj_sym_kind prem_kind
- type_enc sound false (translate_atp_lambdas ctxt type_enc)
+ type_enc sound false
+ (Config.get ctxt atp_lambda_translation)
(Config.get ctxt atp_readable_names) true hyp_ts concl_t
facts
fun weights () = atp_problem_weights atp_problem