move lambda translation option from ATP to Sledgehammer, to avoid accidentally breaking Metis (its reconstruction code can only deal with combinators)

--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Jul 14 16:50:05 2011 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Jul 14 16:50:05 2011 +0200
@@ -369,7 +369,8 @@
     val st' =
       st |> Proof.map_context
                 (change_dir dir
-                 #> (Option.map (Config.put ATP_Translate.lambda_translation)
+                 #> (Option.map (Config.put
+                       Sledgehammer_Provers.atp_lambda_translation)
                        lambda_translation |> the_default I)
                  #> (Option.map (Config.put ATP_Systems.e_weight_method)
                        e_weight_method |> the_default I)

--- a/src/HOL/TPTP/atp_export.ML	Thu Jul 14 16:50:05 2011 +0200
+++ b/src/HOL/TPTP/atp_export.ML	Thu Jul 14 16:50:05 2011 +0200
@@ -159,8 +159,8 @@
     val (atp_problem, _, _, _, _, _, _) =
       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 false
-                             true [] @{prop False}
+      |> prepare_atp_problem ctxt format Axiom Axiom type_enc true true
+                             combinatorsN 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	Thu Jul 14 16:50:05 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Thu Jul 14 16:50:05 2011 +0200
@@ -31,6 +31,11 @@
     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
@@ -63,12 +68,6 @@
   val prefixed_predicator_name : string
   val prefixed_app_op_name : string
   val prefixed_type_tag_name : string
-  val concealed_lambdasN : string
-  val lambda_liftingN : string
-  val combinatorsN : string
-  val lambdasN : string
-  val smartN : string
-  val lambda_translation : string Config.T
   val ascii_of : string -> string
   val unascii_of : string -> string
   val strip_prefix_and_unascii : string -> string -> string option
@@ -82,6 +81,7 @@
   val atp_schematic_consts_of : term -> typ list Symtab.table
   val is_locality_global : locality -> bool
   val type_enc_from_string : string -> type_enc
+  val is_type_enc_higher_order : type_enc -> bool
   val polymorphism_of_type_enc : type_enc -> polymorphism
   val level_of_type_enc : type_enc -> type_level
   val is_type_enc_virtually_sound : type_enc -> bool
@@ -95,7 +95,7 @@
   val factsN : string
   val prepare_atp_problem :
     Proof.context -> format -> formula_kind -> formula_kind -> type_enc -> bool
-    -> bool -> bool -> bool -> term list -> term
+    -> 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
@@ -110,8 +110,13 @@
 
 type name = string * string
 
-(* experimental *)
-val generate_info = false
+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 =
   if generate_info then SOME (ATerm ("[]", [ATerm ("isabelle_" ^ s, [])]))
@@ -166,15 +171,6 @@
 
 val concealed_lambda_prefix = sledgehammer_weak_prefix ^ "lambda_"
 
-val concealed_lambdasN = "concealed_lambdas"
-val lambda_liftingN = "lambda_lifting"
-val combinatorsN = "combinators"
-val lambdasN = "lambdas"
-val smartN = "smart"
-
-val lambda_translation =
-  Attrib.setup_config_string @{binding atp_lambda_translation} (K smartN)
-
 (*Escaping of special characters.
   Alphanumeric characters are left unchanged.
   The character _ goes to __
@@ -613,14 +609,6 @@
   is_type_level_virtually_sound level orelse level = Fin_Nonmono_Types
 val is_type_enc_fairly_sound = is_type_level_fairly_sound o level_of_type_enc
 
-fun effective_lambda_translation ctxt type_enc =
-  Config.get ctxt lambda_translation
-  |> (fn trans =>
-         if trans = smartN then
-           if is_type_enc_higher_order type_enc then lambdasN else combinatorsN
-         else
-           trans)
-
 fun choose_format formats (Simple_Types (order, level)) =
     if member (op =) formats THF then
       (THF, Simple_Types (order, level))
@@ -923,11 +911,12 @@
 
 fun conceal_lambdas Ts (t1 $ t2) = conceal_lambdas Ts t1 $ conceal_lambdas Ts t2
   | 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
 
-fun process_abstractions_in_term ctxt type_enc kind t =
+fun process_abstractions_in_term ctxt lambda_trans kind t =
   let val thy = Proof_Context.theory_of ctxt in
     if Meson.is_fol_term thy t then
       t
@@ -954,24 +943,22 @@
             if not (exists_subterm (fn Abs _ => true | _ => false) t) then
               t
             else
-              let
-                val trans = effective_lambda_translation ctxt type_enc
-                val t = t |> Envir.eta_contract
-              in
-                if trans = concealed_lambdasN then
+              let val t = t |> Envir.eta_contract in
+                if lambda_trans = concealed_lambdasN then
                   t |> conceal_lambdas []
-                else if trans = lambda_liftingN then
+                else if lambda_trans = lambda_liftingN then
                   t (* TODO: implement *)
-                else if trans = combinatorsN then
+                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 trans = lambdasN then
+                else if lambda_trans = lambdasN then
                   t
                 else
-                  error ("Unknown lambda translation: " ^ quote trans ^ ".")
+                  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
@@ -992,7 +979,7 @@
       | aux t = t
   in t |> exists_subterm is_Var t ? aux end
 
-fun preprocess_prop ctxt type_enc presimp_consts kind t =
+fun preprocess_prop ctxt lambda_trans presimp_consts kind t =
   let
     val thy = Proof_Context.theory_of ctxt
     val t = t |> Envir.beta_eta_contract
@@ -1005,7 +992,7 @@
       |> extensionalize_term ctxt
       |> presimplify_term ctxt presimp_consts
       |> perhaps (try (HOLogic.dest_Trueprop))
-      |> process_abstractions_in_term ctxt type_enc kind
+      |> process_abstractions_in_term ctxt lambda_trans kind
   end
 
 (* making fact and conjecture formulas *)
@@ -1018,10 +1005,10 @@
      atomic_types = atomic_types}
   end
 
-fun make_fact ctxt format type_enc eq_as_iff preproc presimp_consts
+fun make_fact ctxt format type_enc lambda_trans eq_as_iff preproc presimp_consts
               ((name, loc), t) =
   let val thy = Proof_Context.theory_of ctxt in
-    case t |> preproc ? preprocess_prop ctxt type_enc presimp_consts Axiom
+    case t |> preproc ? preprocess_prop ctxt lambda_trans presimp_consts Axiom
            |> make_formula thy type_enc (eq_as_iff andalso format <> CNF) name
                            loc Axiom of
       formula as {combformula = AAtom (CombConst ((s, _), _, _)), ...} =>
@@ -1029,7 +1016,8 @@
     | formula => SOME formula
   end
 
-fun make_conjecture ctxt format prem_kind type_enc preproc presimp_consts ts =
+fun make_conjecture ctxt format prem_kind type_enc lambda_trans preproc
+                    presimp_consts ts =
   let
     val thy = Proof_Context.theory_of ctxt
     val last = length ts - 1
@@ -1045,7 +1033,8 @@
                     else I)
               in
                 t |> preproc ?
-                     (preprocess_prop ctxt type_enc presimp_consts kind #> freeze_term)
+                     (preprocess_prop ctxt lambda_trans presimp_consts kind
+                      #> freeze_term)
                   |> make_formula thy type_enc (format <> CNF) (string_of_int j)
                                   Local kind
                   |> maybe_negate
@@ -1392,7 +1381,8 @@
   level_of_type_enc type_enc <> No_Types andalso
   not (null (Term.hidden_polymorphism t))
 
-fun helper_facts_for_sym ctxt format type_enc (s, {types, ...} : sym_info) =
+fun helper_facts_for_sym ctxt format type_enc lambda_trans
+                         (s, {types, ...} : sym_info) =
   case strip_prefix_and_unascii const_prefix s of
     SOME mangled_s =>
     let
@@ -1414,7 +1404,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 false false [])
+        map_filter (make_fact ctxt format type_enc lambda_trans false false [])
       val fairly_sound = is_type_enc_fairly_sound type_enc
     in
       helper_table
@@ -1428,9 +1418,10 @@
                     |> make_facts)
     end
   | NONE => []
-fun helper_facts_for_sym_table ctxt format type_enc sym_tab =
-  Symtab.fold_rev (append o helper_facts_for_sym ctxt format type_enc) sym_tab
-                  []
+fun helper_facts_for_sym_table ctxt format type_enc lambda_trans sym_tab =
+  Symtab.fold_rev (append
+                   o helper_facts_for_sym ctxt format type_enc lambda_trans)
+                  sym_tab []
 
 (***************************************************************)
 (* Type Classes Present in the Axiom or Conjecture Clauses     *)
@@ -1470,13 +1461,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 preproc hyp_ts concl_t
-                       facts =
+fun translate_formulas ctxt format prem_kind type_enc lambda_trans 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 true preproc presimp_consts
+    val make_fact =
+      make_fact ctxt format type_enc lambda_trans true preproc presimp_consts
     val (facts, fact_names) =
       facts |> map (fn (name, t) => (name, t) |> make_fact |> rpair name)
             |> map_filter (try (apfst the))
@@ -1493,7 +1485,8 @@
     val tycons = type_constrs_of_terms thy all_ts
     val conjs =
       hyp_ts @ [concl_t]
-      |> make_conjecture ctxt format prem_kind type_enc preproc presimp_consts
+      |> make_conjecture ctxt format prem_kind type_enc lambda_trans preproc
+                         presimp_consts
     val (supers', arity_clauses) =
       if level_of_type_enc type_enc = No_Types then ([], [])
       else make_arity_clauses thy tycons supers
@@ -1907,15 +1900,22 @@
 val conjsN = "Conjectures"
 val free_typesN = "Type variables"
 
-val explicit_apply = NONE (* for experimental purposes *)
+val explicit_apply = NONE (* for experiments *)
 
 fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_enc sound
-        exporter 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 _ =
+      if lambda_trans = lambdasN andalso
+         not (is_type_enc_higher_order type_enc) then
+        error ("Lambda translation method incompatible with \
+               \first-order encoding.")
+      else
+        ()
     val (fact_names, (conjs, facts, class_rel_clauses, arity_clauses)) =
-      translate_formulas ctxt format prem_kind type_enc preproc hyp_ts concl_t
-                         facts
+      translate_formulas ctxt format prem_kind type_enc lambda_trans preproc
+                         hyp_ts concl_t facts
     val sym_tab = conjs @ facts |> sym_table_for_facts ctxt explicit_apply
     val nonmono_Ts =
       conjs @ facts |> nonmonotonic_types_for_facts ctxt type_enc sound
@@ -1924,8 +1924,9 @@
     val repaired_sym_tab =
       conjs @ facts |> sym_table_for_facts ctxt (SOME false)
     val helpers =
-      repaired_sym_tab |> helper_facts_for_sym_table ctxt format type_enc
-                       |> map repair
+      repaired_sym_tab
+      |> helper_facts_for_sym_table ctxt format type_enc lambda_trans
+      |> map repair
     val poly_nonmono_Ts =
       if null nonmono_Ts orelse nonmono_Ts = [@{typ bool}] orelse
          polymorphism_of_type_enc type_enc <> Polymorphic then

--- a/src/HOL/Tools/Metis/metis_translate.ML	Thu Jul 14 16:50:05 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_translate.ML	Thu Jul 14 16:50:05 2011 +0200
@@ -196,8 +196,8 @@
       tracing ("PROPS:\n" ^ cat_lines (map (Syntax.string_of_term ctxt) props))
     *)
     val (atp_problem, _, _, _, _, _, sym_tab) =
-      prepare_atp_problem ctxt CNF Hypothesis Axiom type_enc true false false
-                          false [] @{prop False} props
+      prepare_atp_problem ctxt CNF Hypothesis Axiom type_enc true false
+                          combinatorsN 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	Thu Jul 14 16:50:05 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Jul 14 16:50:05 2011 +0200
@@ -63,6 +63,7 @@
   val dest_dir : string Config.T
   val problem_prefix : string Config.T
   val measure_run_time : bool Config.T
+  val atp_lambda_translation : string Config.T
   val atp_readable_names : bool Config.T
   val smt_triggers : bool Config.T
   val smt_weights : bool Config.T
@@ -336,6 +337,9 @@
 val measure_run_time =
   Attrib.setup_config_bool @{binding sledgehammer_measure_run_time} (K false)
 
+val atp_lambda_translation =
+  Attrib.setup_config_string @{binding sledgehammer_atp_lambda_translation}
+                             (K smartN)
 (* In addition to being easier to read, readable names are often much shorter,
    especially if types are mangled in names. For these reason, they are enabled
    by default. *)
@@ -510,6 +514,14 @@
    | NONE => type_enc_from_string best_type_enc)
   |> choose_format formats
 
+fun effective_atp_lambda_translation 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
+           trans)
+
 val metis_minimize_max_time = seconds 2.0
 
 fun choose_minimize_command minimize_command name preplay =
@@ -641,8 +653,10 @@
                 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 (Config.get ctxt atp_readable_names)
-                      true hyp_ts concl_t facts
+                      type_enc sound false
+                      (effective_atp_lambda_translation ctxt type_enc)
+                      (Config.get ctxt atp_readable_names) true hyp_ts concl_t
+                      facts
                 fun weights () = atp_problem_weights atp_problem
                 val full_proof = debug orelse isar_proof
                 val core =