# HG changeset patch # User blanchet # Date 1310904695 -7200 # Node ID a14fdb8c0497f79c54b27a2116cb9985f0ccce77 # Parent a08c591bdcdf7b823c4574777ec9cea5abe6fb7a pass kind to lambda-translation function diff -r a08c591bdcdf -r a14fdb8c0497 src/HOL/TPTP/atp_export.ML --- 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))) diff -r a08c591bdcdf -r a14fdb8c0497 src/HOL/Tools/ATP/atp_translate.ML --- 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). *) diff -r a08c591bdcdf -r a14fdb8c0497 src/HOL/Tools/Metis/metis_translate.ML --- 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)) diff -r a08c591bdcdf -r a14fdb8c0497 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- 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