move more lambda-handling logic to Sledgehammer, from ATP module, for formal dependency reasons
--- a/src/HOL/TPTP/atp_export.ML Sun Jul 17 08:45:06 2011 +0200
+++ b/src/HOL/TPTP/atp_export.ML Sun Jul 17 14:11:34 2011 +0200
@@ -160,7 +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
- combinatorsN false true [] @{prop False}
+ (map (introduce_combinators ctxt)) 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 08:45:06 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML Sun Jul 17 14:11:34 2011 +0200
@@ -31,11 +31,6 @@
Preds of polymorphism * type_level * type_heaviness |
Tags of polymorphism * type_level * type_heaviness
- val concealed_lambdasN : string
- val lambda_liftingN : string
- val combinatorsN : string
- val lambdasN : string
- val smartN : string
val bound_var_prefix : string
val schematic_var_prefix : string
val fixed_var_prefix : string
@@ -93,9 +88,11 @@
val unmangled_const_name : string -> string
val helper_table : ((string * bool) * thm list) list
val factsN : string
+ val conceal_lambdas : Proof.context -> term -> term
+ val introduce_combinators : Proof.context -> term -> term
val prepare_atp_problem :
Proof.context -> format -> formula_kind -> formula_kind -> type_enc -> bool
- -> bool -> string -> bool -> bool -> term list -> term
+ -> bool -> (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
@@ -110,12 +107,6 @@
type name = string * string
-val concealed_lambdasN = "concealed_lambdas"
-val lambda_liftingN = "lambda_lifting"
-val combinatorsN = "combinators"
-val lambdasN = "lambdas"
-val smartN = "smart"
-
val generate_info = false (* experimental *)
fun isabelle_info s =
@@ -909,59 +900,56 @@
else
t
-fun conceal_lambdas Ts (t1 $ t2) = conceal_lambdas Ts t1 $ conceal_lambdas Ts t2
- | conceal_lambdas Ts (Abs (_, T, t)) =
+fun generic_translate_lambdas do_lambdas ctxt t =
+ let
+ fun aux Ts t =
+ case t of
+ @{const Not} $ t1 => @{const Not} $ aux Ts t1
+ | (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') =>
+ t0 $ Abs (s, T, aux (T :: Ts) t')
+ | (t0 as Const (@{const_name All}, _)) $ t1 =>
+ aux Ts (t0 $ eta_expand Ts t1 1)
+ | (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') =>
+ t0 $ Abs (s, T, aux (T :: Ts) t')
+ | (t0 as Const (@{const_name Ex}, _)) $ t1 =>
+ aux Ts (t0 $ eta_expand Ts t1 1)
+ | (t0 as @{const HOL.conj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
+ | (t0 as @{const HOL.disj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
+ | (t0 as @{const HOL.implies}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
+ | (t0 as Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])))
+ $ t1 $ t2 =>
+ t0 $ aux Ts t1 $ aux Ts t2
+ | _ =>
+ if not (exists_subterm (fn Abs _ => true | _ => false) t) then t
+ else t |> Envir.eta_contract |> do_lambdas ctxt Ts
+ val (t, ctxt') = Variable.import_terms true [t] ctxt |>> the_single
+ in t |> aux [] |> singleton (Variable.export_terms ctxt' ctxt) end
+
+fun do_conceal_lambdas Ts (t1 $ t2) =
+ do_conceal_lambdas Ts t1 $ do_conceal_lambdas Ts t2
+ | do_conceal_lambdas Ts (Abs (_, T, t)) =
(* slightly unsound because of hash collisions *)
Free (concealed_lambda_prefix ^ string_of_int (hash_term t),
T --> fastype_of1 (Ts, t))
- | conceal_lambdas _ t = t
+ | do_conceal_lambdas _ t = t
+val conceal_lambdas = generic_translate_lambdas (K do_conceal_lambdas)
-fun process_abstractions_in_term ctxt lambda_trans kind t =
+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
+
+fun process_abstractions_in_term ctxt trans_lambdas kind t =
let val thy = Proof_Context.theory_of ctxt in
if Meson.is_fol_term thy t then
t
else
- let
- fun aux Ts t =
- case t of
- @{const Not} $ t1 => @{const Not} $ aux Ts t1
- | (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') =>
- t0 $ Abs (s, T, aux (T :: Ts) t')
- | (t0 as Const (@{const_name All}, _)) $ t1 =>
- aux Ts (t0 $ eta_expand Ts t1 1)
- | (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') =>
- t0 $ Abs (s, T, aux (T :: Ts) t')
- | (t0 as Const (@{const_name Ex}, _)) $ t1 =>
- aux Ts (t0 $ eta_expand Ts t1 1)
- | (t0 as @{const HOL.conj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
- | (t0 as @{const HOL.disj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
- | (t0 as @{const HOL.implies}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
- | (t0 as Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])))
- $ t1 $ t2 =>
- t0 $ aux Ts t1 $ aux Ts t2
- | _ =>
- if not (exists_subterm (fn Abs _ => true | _ => false) t) then
- t
- else
- let val t = t |> Envir.eta_contract in
- if lambda_trans = concealed_lambdasN then
- t |> conceal_lambdas []
- else if lambda_trans = lambda_liftingN then
- t (* TODO: implement *)
- else if lambda_trans = combinatorsN then
- t |> conceal_bounds Ts
- |> cterm_of thy
- |> Meson_Clausify.introduce_combinators_in_cterm
- |> prop_of |> Logic.dest_equals |> snd
- |> reveal_bounds Ts
- else if lambda_trans = lambdasN then
- t
- else
- error ("Unknown lambda translation method: " ^
- quote lambda_trans ^ ".")
- end
- val (t, ctxt') = Variable.import_terms true [t] ctxt |>> the_single
- in t |> aux [] |> singleton (Variable.export_terms ctxt' ctxt) end
+ t |> singleton trans_lambdas
handle THM _ =>
(* A type variable of sort "{}" will make abstraction fail. *)
if kind = Conjecture then HOLogic.false_const
@@ -979,7 +967,7 @@
| aux t = t
in t |> exists_subterm is_Var t ? aux end
-fun preprocess_prop ctxt lambda_trans presimp_consts kind t =
+fun preprocess_prop ctxt trans_lambdas presimp_consts kind t =
let
val thy = Proof_Context.theory_of ctxt
val t = t |> Envir.beta_eta_contract
@@ -992,7 +980,7 @@
|> extensionalize_term ctxt
|> presimplify_term ctxt presimp_consts
|> perhaps (try (HOLogic.dest_Trueprop))
- |> process_abstractions_in_term ctxt lambda_trans kind
+ |> process_abstractions_in_term ctxt trans_lambdas kind
end
(* making fact and conjecture formulas *)
@@ -1005,10 +993,10 @@
atomic_types = atomic_types}
end
-fun make_fact ctxt format type_enc lambda_trans eq_as_iff preproc presimp_consts
+fun make_fact ctxt format type_enc trans_lambdas eq_as_iff preproc presimp_consts
((name, loc), t) =
let val thy = Proof_Context.theory_of ctxt in
- case t |> preproc ? preprocess_prop ctxt lambda_trans presimp_consts Axiom
+ case t |> preproc ? preprocess_prop ctxt trans_lambdas presimp_consts Axiom
|> make_formula thy type_enc (eq_as_iff andalso format <> CNF) name
loc Axiom of
formula as {combformula = AAtom (CombConst ((s, _), _, _)), ...} =>
@@ -1016,7 +1004,7 @@
| formula => SOME formula
end
-fun make_conjecture ctxt format prem_kind type_enc lambda_trans preproc
+fun make_conjecture ctxt format prem_kind type_enc trans_lambdas preproc
presimp_consts ts =
let
val thy = Proof_Context.theory_of ctxt
@@ -1033,7 +1021,7 @@
else I)
in
t |> preproc ?
- (preprocess_prop ctxt lambda_trans presimp_consts kind
+ (preprocess_prop ctxt trans_lambdas presimp_consts kind
#> freeze_term)
|> make_formula thy type_enc (format <> CNF) (string_of_int j)
Local kind
@@ -1381,7 +1369,7 @@
level_of_type_enc type_enc <> No_Types andalso
not (null (Term.hidden_polymorphism t))
-fun helper_facts_for_sym ctxt format type_enc lambda_trans
+fun helper_facts_for_sym ctxt format type_enc trans_lambdas
(s, {types, ...} : sym_info) =
case strip_prefix_and_unascii const_prefix s of
SOME mangled_s =>
@@ -1404,7 +1392,7 @@
end
|> map (fn (k, t) => (dub needs_fairly_sound j k, t)) o tag_list 1
val make_facts =
- map_filter (make_fact ctxt format type_enc lambda_trans false false [])
+ map_filter (make_fact ctxt format type_enc trans_lambdas false false [])
val fairly_sound = is_type_enc_fairly_sound type_enc
in
helper_table
@@ -1418,9 +1406,9 @@
|> make_facts)
end
| NONE => []
-fun helper_facts_for_sym_table ctxt format type_enc lambda_trans sym_tab =
+fun helper_facts_for_sym_table ctxt format type_enc trans_lambdas sym_tab =
Symtab.fold_rev (append
- o helper_facts_for_sym ctxt format type_enc lambda_trans)
+ o helper_facts_for_sym ctxt format type_enc trans_lambdas)
sym_tab []
(***************************************************************)
@@ -1461,14 +1449,14 @@
fun type_constrs_of_terms thy ts =
Symtab.keys (fold (add_type_constrs_in_term thy) ts Symtab.empty)
-fun translate_formulas ctxt format prem_kind type_enc lambda_trans preproc
+fun translate_formulas ctxt format prem_kind type_enc trans_lambdas preproc
hyp_ts concl_t facts =
let
val thy = Proof_Context.theory_of ctxt
val fact_ts = facts |> map snd
val presimp_consts = Meson.presimplified_consts ctxt
val make_fact =
- make_fact ctxt format type_enc lambda_trans true preproc presimp_consts
+ make_fact ctxt format type_enc trans_lambdas true preproc presimp_consts
val (facts, fact_names) =
facts |> map (fn (name, t) => (name, t) |> make_fact |> rpair name)
|> map_filter (try (apfst the))
@@ -1485,7 +1473,7 @@
val tycons = type_constrs_of_terms thy all_ts
val conjs =
hyp_ts @ [concl_t]
- |> make_conjecture ctxt format prem_kind type_enc lambda_trans preproc
+ |> make_conjecture ctxt format prem_kind type_enc trans_lambdas preproc
presimp_consts
val (supers', arity_clauses) =
if level_of_type_enc type_enc = No_Types then ([], [])
@@ -1903,11 +1891,11 @@
val explicit_apply = NONE (* for experiments *)
fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_enc sound
- exporter lambda_trans readable_names preproc hyp_ts concl_t facts =
+ exporter trans_lambdas readable_names preproc hyp_ts concl_t facts =
let
val (format, type_enc) = choose_format [format] type_enc
val (fact_names, (conjs, facts, class_rel_clauses, arity_clauses)) =
- translate_formulas ctxt format prem_kind type_enc lambda_trans preproc
+ translate_formulas ctxt format prem_kind type_enc trans_lambdas preproc
hyp_ts concl_t facts
val sym_tab = conjs @ facts |> sym_table_for_facts ctxt explicit_apply
val nonmono_Ts =
@@ -1918,7 +1906,7 @@
conjs @ facts |> sym_table_for_facts ctxt (SOME false)
val helpers =
repaired_sym_tab
- |> helper_facts_for_sym_table ctxt format type_enc lambda_trans
+ |> helper_facts_for_sym_table ctxt format type_enc trans_lambdas
|> map repair
val poly_nonmono_Ts =
if null nonmono_Ts orelse nonmono_Ts = [@{typ bool}] orelse
--- a/src/HOL/Tools/Metis/metis_translate.ML Sun Jul 17 08:45:06 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_translate.ML Sun Jul 17 14:11:34 2011 +0200
@@ -197,7 +197,8 @@
*)
val (atp_problem, _, _, _, _, _, sym_tab) =
prepare_atp_problem ctxt CNF Hypothesis Axiom type_enc true false
- combinatorsN false false [] @{prop False} props
+ (map (introduce_combinators ctxt)) 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 08:45:06 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Sun Jul 17 14:11:34 2011 +0200
@@ -60,6 +60,11 @@
type prover =
params -> (string -> minimize_command) -> prover_problem -> prover_result
+ val concealed_lambdasN : string
+ val lambda_liftingN : string
+ val combinatorsN : 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
@@ -329,6 +334,12 @@
(* configuration attributes *)
+val concealed_lambdasN = "concealed_lambdas"
+val lambda_liftingN = "lambda_lifting"
+val combinatorsN = "combinators"
+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 "")
@@ -514,7 +525,7 @@
| NONE => type_enc_from_string best_type_enc)
|> choose_format formats
-fun effective_atp_lambda_translation ctxt type_enc =
+fun translate_atp_lambdas ctxt type_enc =
Config.get ctxt atp_lambda_translation
|> (fn trans =>
if trans = smartN then
@@ -525,6 +536,17 @@
\first-order encoding.")
else
trans)
+ |> (fn trans =>
+ if trans = concealed_lambdasN then
+ map (conceal_lambdas ctxt)
+ else if trans = lambda_liftingN then
+ I (* TODO: implement *)
+ 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 ^ "."))
val metis_minimize_max_time = seconds 2.0
@@ -657,8 +679,7 @@
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
- (effective_atp_lambda_translation ctxt type_enc)
+ type_enc sound false (translate_atp_lambdas ctxt type_enc)
(Config.get ctxt atp_readable_names) true hyp_ts concl_t
facts
fun weights () = atp_problem_weights atp_problem