# HG changeset patch # User blanchet # Date 1312873522 -7200 # Node ID 3693baa6befb61073a58f26796474d2cf31debe6 # Parent 8e491cb8841cc62c481e9222bdaf48b254cd5572 move lambda-lifting code to ATP encoding, so it can be used by Metis diff -r 8e491cb8841c -r 3693baa6befb src/HOL/TPTP/atp_export.ML --- 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))) diff -r 8e491cb8841c -r 3693baa6befb src/HOL/Tools/ATP/atp_translate.ML --- 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 diff -r 8e491cb8841c -r 3693baa6befb src/HOL/Tools/Metis/metis_translate.ML --- 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)) diff -r 8e491cb8841c -r 3693baa6befb src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- 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