# HG changeset patch # User blanchet # Date 1310904695 -7200 # Node ID a875729380a4dd26091e0b0d521f554f0b57e987 # Parent d636b053d4ff644bc045d3e0f1fe2454595a3c80 added lambda-lifting to Sledgehammer (rough) diff -r d636b053d4ff -r a875729380a4 src/HOL/Tools/ATP/atp_translate.ML --- a/src/HOL/Tools/ATP/atp_translate.ML Sun Jul 17 14:11:34 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_translate.ML Sun Jul 17 14:11:35 2011 +0200 @@ -993,8 +993,8 @@ atomic_types = atomic_types} end -fun make_fact ctxt format type_enc trans_lambdas eq_as_iff preproc presimp_consts - ((name, loc), t) = +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 trans_lambdas presimp_consts Axiom |> make_formula thy type_enc (eq_as_iff andalso format <> CNF) name diff -r d636b053d4ff -r a875729380a4 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Sun Jul 17 14:11:34 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Sun Jul 17 14:11:35 2011 +0200 @@ -525,6 +525,11 @@ | 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 translate_atp_lambdas ctxt type_enc = Config.get ctxt atp_lambda_translation |> (fn trans => @@ -537,16 +542,11 @@ 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 ^ ".")) + 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 ^ ".")) val metis_minimize_max_time = seconds 2.0