1.1 --- a/src/HOL/TPTP/atp_export.ML	Tue Aug 09 09:05:21 2011 +0200
     1.2 +++ b/src/HOL/TPTP/atp_export.ML	Tue Aug 09 09:05:22 2011 +0200
     1.3 @@ -160,8 +160,7 @@
     1.4        facts
     1.5        |> map (fn ((_, loc), th) => ((Thm.get_name_hint th, loc), prop_of th))
     1.6        |> prepare_atp_problem ctxt format Axiom Axiom type_enc true true
     1.7 -                             (rpair [] o map (introduce_combinators ctxt))
     1.8 -                             false true [] @{prop False}
     1.9 +                             combinatorsN false true [] @{prop False}
    1.10      val atp_problem =
    1.11        atp_problem
    1.12        |> map (apsnd (filter_out (is_problem_line_tautology ctxt)))

     2.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Tue Aug 09 09:05:21 2011 +0200
     2.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Tue Aug 09 09:05:22 2011 +0200
     2.3 @@ -31,6 +31,13 @@
     2.4      Guards of polymorphism * type_level * type_heaviness |
     2.5      Tags of polymorphism * type_level * type_heaviness
     2.6  
     2.7 +  val no_lambdasN : string
     2.8 +  val concealedN : string
     2.9 +  val liftingN : string
    2.10 +  val combinatorsN : string
    2.11 +  val hybridN : string
    2.12 +  val lambdasN : string
    2.13 +  val smartN : string
    2.14    val bound_var_prefix : string
    2.15    val schematic_var_prefix : string
    2.16    val fixed_var_prefix : string
    2.17 @@ -88,11 +95,10 @@
    2.18    val unmangled_const_name : string -> string
    2.19    val helper_table : ((string * bool) * thm list) list
    2.20    val factsN : string
    2.21 -  val introduce_combinators : Proof.context -> term -> term
    2.22    val prepare_atp_problem :
    2.23      Proof.context -> format -> formula_kind -> formula_kind -> type_enc -> bool
    2.24 -    -> bool -> (term list -> term list * term list) -> bool -> bool -> term list
    2.25 -    -> term -> ((string * locality) * term) list
    2.26 +    -> bool -> string -> bool -> bool -> term list -> term
    2.27 +    -> ((string * locality) * term) list
    2.28      -> string problem * string Symtab.table * int * int
    2.29         * (string * locality) list vector * int list * int Symtab.table
    2.30    val atp_problem_weights : string problem -> (string * real) list
    2.31 @@ -106,6 +112,14 @@
    2.32  
    2.33  type name = string * string
    2.34  
    2.35 +val no_lambdasN = "no_lambdas"
    2.36 +val concealedN = "concealed"
    2.37 +val liftingN = "lifting"
    2.38 +val combinatorsN = "combinators"
    2.39 +val hybridN = "hybrid"
    2.40 +val lambdasN = "lambdas"
    2.41 +val smartN = "smart"
    2.42 +
    2.43  val generate_info = false (* experimental *)
    2.44  
    2.45  fun isabelle_info s =
    2.46 @@ -606,6 +620,29 @@
    2.47                   | _ => type_enc)
    2.48       | format => (format, type_enc))
    2.49  
    2.50 +fun lift_lambdas ctxt type_enc =
    2.51 +  map (close_form o Envir.eta_contract) #> rpair ctxt
    2.52 +  #-> Lambda_Lifting.lift_lambdas
    2.53 +          (if polymorphism_of_type_enc type_enc = Polymorphic then
    2.54 +             SOME polymorphic_free_prefix
    2.55 +           else
    2.56 +             NONE)
    2.57 +          Lambda_Lifting.is_quantifier
    2.58 +  #> fst
    2.59 +
    2.60 +fun intentionalize_def (Const (@{const_name All}, _) $ Abs (_, _, t)) =
    2.61 +    intentionalize_def t
    2.62 +  | intentionalize_def (Const (@{const_name HOL.eq}, _) $ t $ u) =
    2.63 +    let
    2.64 +      fun lam T t = Abs (Name.uu, T, t)
    2.65 +      val (head, args) = strip_comb t ||> rev
    2.66 +      val head_T = fastype_of head
    2.67 +      val n = length args
    2.68 +      val arg_Ts = head_T |> binder_types |> take n |> rev
    2.69 +      val u = u |> subst_atomic (args ~~ map Bound (0 upto n - 1))
    2.70 +    in HOLogic.eq_const head_T $ head $ fold lam arg_Ts u end
    2.71 +  | intentionalize_def t = t
    2.72 +
    2.73  type translated_formula =
    2.74    {name : string,
    2.75     locality : locality,
    2.76 @@ -1918,9 +1955,36 @@
    2.77  val explicit_apply = NONE (* for experiments *)
    2.78  
    2.79  fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_enc sound
    2.80 -        exporter trans_lambdas readable_names preproc hyp_ts concl_t facts =
    2.81 +        exporter lambda_trans readable_names preproc hyp_ts concl_t facts =
    2.82    let
    2.83      val (format, type_enc) = choose_format [format] type_enc
    2.84 +    val lambda_trans =
    2.85 +      if lambda_trans = smartN then
    2.86 +        if is_type_enc_higher_order type_enc then lambdasN else combinatorsN
    2.87 +      else if lambda_trans = lambdasN andalso
    2.88 +              not (is_type_enc_higher_order type_enc) then
    2.89 +        error ("Lambda translation method incompatible with first-order \
    2.90 +               \encoding.")
    2.91 +      else
    2.92 +        lambda_trans
    2.93 +    val trans_lambdas =
    2.94 +      if lambda_trans = no_lambdasN then
    2.95 +        rpair []
    2.96 +      else if lambda_trans = concealedN then
    2.97 +        lift_lambdas ctxt type_enc ##> K []
    2.98 +      else if lambda_trans = liftingN then
    2.99 +        lift_lambdas ctxt type_enc
   2.100 +      else if lambda_trans = combinatorsN then
   2.101 +        map (introduce_combinators ctxt) #> rpair []
   2.102 +      else if lambda_trans = hybridN then
   2.103 +        lift_lambdas ctxt type_enc
   2.104 +        ##> maps (fn t => [t, introduce_combinators ctxt
   2.105 +                                  (intentionalize_def t)])
   2.106 +      else if lambda_trans = lambdasN then
   2.107 +        map (Envir.eta_contract) #> rpair []
   2.108 +      else
   2.109 +        error ("Unknown lambda translation method: " ^
   2.110 +               quote lambda_trans ^ ".")
   2.111      val (fact_names, (conjs, facts, class_rel_clauses, arity_clauses)) =
   2.112        translate_formulas ctxt format prem_kind type_enc trans_lambdas preproc
   2.113                           hyp_ts concl_t facts

     3.1 --- a/src/HOL/Tools/Metis/metis_translate.ML	Tue Aug 09 09:05:21 2011 +0200
     3.2 +++ b/src/HOL/Tools/Metis/metis_translate.ML	Tue Aug 09 09:05:22 2011 +0200
     3.3 @@ -197,7 +197,7 @@
     3.4      *)
     3.5      val (atp_problem, _, _, _, _, _, sym_tab) =
     3.6        prepare_atp_problem ctxt CNF Hypothesis Axiom type_enc true false
     3.7 -                          (rpair []) false false [] @{prop False} props
     3.8 +                          no_lambdasN false false [] @{prop False} props
     3.9      (*
    3.10      val _ = tracing ("ATP PROBLEM: " ^
    3.11                       cat_lines (tptp_lines_for_atp_problem CNF atp_problem))

     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Aug 09 09:05:21 2011 +0200
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Aug 09 09:05:22 2011 +0200
     4.3 @@ -60,12 +60,6 @@
     4.4    type prover =
     4.5      params -> (string -> minimize_command) -> prover_problem -> prover_result
     4.6  
     4.7 -  val concealedN : string
     4.8 -  val liftingN : string
     4.9 -  val combinatorsN : string
    4.10 -  val hybridN : string
    4.11 -  val lambdasN : string
    4.12 -  val smartN : string
    4.13    val dest_dir : string Config.T
    4.14    val problem_prefix : string Config.T
    4.15    val measure_run_time : bool Config.T
    4.16 @@ -335,13 +329,6 @@
    4.17  
    4.18  (* configuration attributes *)
    4.19  
    4.20 -val concealedN = "concealed"
    4.21 -val liftingN = "lifting"
    4.22 -val combinatorsN = "combinators"
    4.23 -val hybridN = "hybrid"
    4.24 -val lambdasN = "lambdas"
    4.25 -val smartN = "smart"
    4.26 -
    4.27  (* Empty string means create files in Isabelle's temporary files directory. *)
    4.28  val dest_dir =
    4.29    Attrib.setup_config_string @{binding sledgehammer_dest_dir} (K "")
    4.30 @@ -527,56 +514,6 @@
    4.31     | NONE => type_enc_from_string best_type_enc)
    4.32    |> choose_format formats
    4.33  
    4.34 -fun lift_lambdas ctxt type_enc =
    4.35 -  map (close_form o Envir.eta_contract) #> rpair ctxt
    4.36 -  #-> Lambda_Lifting.lift_lambdas
    4.37 -          (if polymorphism_of_type_enc type_enc = Polymorphic then
    4.38 -             SOME polymorphic_free_prefix
    4.39 -           else
    4.40 -             NONE)
    4.41 -          Lambda_Lifting.is_quantifier
    4.42 -  #> fst
    4.43 -
    4.44 -fun intentionalize_def (Const (@{const_name All}, _) $ Abs (_, _, t)) =
    4.45 -    intentionalize_def t
    4.46 -  | intentionalize_def (Const (@{const_name HOL.eq}, _) $ t $ u) =
    4.47 -    let
    4.48 -      fun lam T t = Abs (Name.uu, T, t)
    4.49 -      val (head, args) = strip_comb t ||> rev
    4.50 -      val head_T = fastype_of head
    4.51 -      val n = length args
    4.52 -      val arg_Ts = head_T |> binder_types |> take n |> rev
    4.53 -      val u = u |> subst_atomic (args ~~ map Bound (0 upto n - 1))
    4.54 -    in HOLogic.eq_const head_T $ head $ fold lam arg_Ts u end
    4.55 -  | intentionalize_def t = t
    4.56 -
    4.57 -fun translate_atp_lambdas ctxt type_enc =
    4.58 -  Config.get ctxt atp_lambda_translation
    4.59 -  |> (fn trans =>
    4.60 -         if trans = smartN then
    4.61 -           if is_type_enc_higher_order type_enc then lambdasN else combinatorsN
    4.62 -         else if trans = lambdasN andalso
    4.63 -                 not (is_type_enc_higher_order type_enc) then
    4.64 -           error ("Lambda translation method incompatible with first-order \
    4.65 -                  \encoding.")
    4.66 -         else
    4.67 -           trans)
    4.68 -  |> (fn trans =>
    4.69 -         if trans = concealedN then
    4.70 -           lift_lambdas ctxt type_enc ##> K []
    4.71 -         else if trans = liftingN then
    4.72 -           lift_lambdas ctxt type_enc
    4.73 -         else if trans = combinatorsN then
    4.74 -           map (introduce_combinators ctxt) #> rpair []
    4.75 -         else if trans = hybridN then
    4.76 -           lift_lambdas ctxt type_enc
    4.77 -           ##> maps (fn t => [t, introduce_combinators ctxt
    4.78 -                                     (intentionalize_def t)])
    4.79 -         else if trans = lambdasN then
    4.80 -           map (Envir.eta_contract) #> rpair []
    4.81 -         else
    4.82 -           error ("Unknown lambda translation method: " ^ quote trans ^ "."))
    4.83 -
    4.84  val metis_minimize_max_time = seconds 2.0
    4.85  
    4.86  fun choose_minimize_command minimize_command name preplay =
    4.87 @@ -708,7 +645,8 @@
    4.88                  val (atp_problem, pool, conjecture_offset, facts_offset,
    4.89                       fact_names, typed_helpers, sym_tab) =
    4.90                    prepare_atp_problem ctxt format conj_sym_kind prem_kind
    4.91 -                      type_enc sound false (translate_atp_lambdas ctxt type_enc)
    4.92 +                      type_enc sound false
    4.93 +                      (Config.get ctxt atp_lambda_translation)
    4.94                        (Config.get ctxt atp_readable_names) true hyp_ts concl_t
    4.95                        facts
    4.96                  fun weights () = atp_problem_weights atp_problem