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

     2.1 --- a/src/HOL/TPTP/atp_export.ML	Thu Jul 14 16:50:05 2011 +0200
     2.2 +++ b/src/HOL/TPTP/atp_export.ML	Thu Jul 14 16:50:05 2011 +0200
     2.3 @@ -159,8 +159,8 @@
     2.4      val (atp_problem, _, _, _, _, _, _) =
     2.5        facts
     2.6        |> map (fn ((_, loc), th) => ((Thm.get_name_hint th, loc), prop_of th))
     2.7 -      |> prepare_atp_problem ctxt format Axiom Axiom type_enc true true false
     2.8 -                             true [] @{prop False}
     2.9 +      |> prepare_atp_problem ctxt format Axiom Axiom type_enc true true
    2.10 +                             combinatorsN false true [] @{prop False}
    2.11      val atp_problem =
    2.12        atp_problem
    2.13        |> map (apsnd (filter_out (is_problem_line_tautology ctxt)))

     3.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Thu Jul 14 16:50:05 2011 +0200
     3.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Thu Jul 14 16:50:05 2011 +0200
     3.3 @@ -31,6 +31,11 @@
     3.4      Preds of polymorphism * type_level * type_heaviness |
     3.5      Tags of polymorphism * type_level * type_heaviness
     3.6  
     3.7 +  val concealed_lambdasN : string
     3.8 +  val lambda_liftingN : string
     3.9 +  val combinatorsN : string
    3.10 +  val lambdasN : string
    3.11 +  val smartN : string
    3.12    val bound_var_prefix : string
    3.13    val schematic_var_prefix : string
    3.14    val fixed_var_prefix : string
    3.15 @@ -63,12 +68,6 @@
    3.16    val prefixed_predicator_name : string
    3.17    val prefixed_app_op_name : string
    3.18    val prefixed_type_tag_name : string
    3.19 -  val concealed_lambdasN : string
    3.20 -  val lambda_liftingN : string
    3.21 -  val combinatorsN : string
    3.22 -  val lambdasN : string
    3.23 -  val smartN : string
    3.24 -  val lambda_translation : string Config.T
    3.25    val ascii_of : string -> string
    3.26    val unascii_of : string -> string
    3.27    val strip_prefix_and_unascii : string -> string -> string option
    3.28 @@ -82,6 +81,7 @@
    3.29    val atp_schematic_consts_of : term -> typ list Symtab.table
    3.30    val is_locality_global : locality -> bool
    3.31    val type_enc_from_string : string -> type_enc
    3.32 +  val is_type_enc_higher_order : type_enc -> bool
    3.33    val polymorphism_of_type_enc : type_enc -> polymorphism
    3.34    val level_of_type_enc : type_enc -> type_level
    3.35    val is_type_enc_virtually_sound : type_enc -> bool
    3.36 @@ -95,7 +95,7 @@
    3.37    val factsN : string
    3.38    val prepare_atp_problem :
    3.39      Proof.context -> format -> formula_kind -> formula_kind -> type_enc -> bool
    3.40 -    -> bool -> bool -> bool -> term list -> term
    3.41 +    -> bool -> string -> bool -> bool -> term list -> term
    3.42      -> ((string * locality) * term) list
    3.43      -> string problem * string Symtab.table * int * int
    3.44         * (string * locality) list vector * int list * int Symtab.table
    3.45 @@ -110,8 +110,13 @@
    3.46  
    3.47  type name = string * string
    3.48  
    3.49 -(* experimental *)
    3.50 -val generate_info = false
    3.51 +val concealed_lambdasN = "concealed_lambdas"
    3.52 +val lambda_liftingN = "lambda_lifting"
    3.53 +val combinatorsN = "combinators"
    3.54 +val lambdasN = "lambdas"
    3.55 +val smartN = "smart"
    3.56 +
    3.57 +val generate_info = false (* experimental *)
    3.58  
    3.59  fun isabelle_info s =
    3.60    if generate_info then SOME (ATerm ("[]", [ATerm ("isabelle_" ^ s, [])]))
    3.61 @@ -166,15 +171,6 @@
    3.62  
    3.63  val concealed_lambda_prefix = sledgehammer_weak_prefix ^ "lambda_"
    3.64  
    3.65 -val concealed_lambdasN = "concealed_lambdas"
    3.66 -val lambda_liftingN = "lambda_lifting"
    3.67 -val combinatorsN = "combinators"
    3.68 -val lambdasN = "lambdas"
    3.69 -val smartN = "smart"
    3.70 -
    3.71 -val lambda_translation =
    3.72 -  Attrib.setup_config_string @{binding atp_lambda_translation} (K smartN)
    3.73 -
    3.74  (*Escaping of special characters.
    3.75    Alphanumeric characters are left unchanged.
    3.76    The character _ goes to __
    3.77 @@ -613,14 +609,6 @@
    3.78    is_type_level_virtually_sound level orelse level = Fin_Nonmono_Types
    3.79  val is_type_enc_fairly_sound = is_type_level_fairly_sound o level_of_type_enc
    3.80  
    3.81 -fun effective_lambda_translation ctxt type_enc =
    3.82 -  Config.get ctxt lambda_translation
    3.83 -  |> (fn trans =>
    3.84 -         if trans = smartN then
    3.85 -           if is_type_enc_higher_order type_enc then lambdasN else combinatorsN
    3.86 -         else
    3.87 -           trans)
    3.88 -
    3.89  fun choose_format formats (Simple_Types (order, level)) =
    3.90      if member (op =) formats THF then
    3.91        (THF, Simple_Types (order, level))
    3.92 @@ -923,11 +911,12 @@
    3.93  
    3.94  fun conceal_lambdas Ts (t1 $ t2) = conceal_lambdas Ts t1 $ conceal_lambdas Ts t2
    3.95    | conceal_lambdas Ts (Abs (_, T, t)) =
    3.96 +    (* slightly unsound because of hash collisions *)
    3.97      Free (concealed_lambda_prefix ^ string_of_int (hash_term t),
    3.98            T --> fastype_of1 (Ts, t))
    3.99    | conceal_lambdas _ t = t
   3.100  
   3.101 -fun process_abstractions_in_term ctxt type_enc kind t =
   3.102 +fun process_abstractions_in_term ctxt lambda_trans kind t =
   3.103    let val thy = Proof_Context.theory_of ctxt in
   3.104      if Meson.is_fol_term thy t then
   3.105        t
   3.106 @@ -954,24 +943,22 @@
   3.107              if not (exists_subterm (fn Abs _ => true | _ => false) t) then
   3.108                t
   3.109              else
   3.110 -              let
   3.111 -                val trans = effective_lambda_translation ctxt type_enc
   3.112 -                val t = t |> Envir.eta_contract
   3.113 -              in
   3.114 -                if trans = concealed_lambdasN then
   3.115 +              let val t = t |> Envir.eta_contract in
   3.116 +                if lambda_trans = concealed_lambdasN then
   3.117                    t |> conceal_lambdas []
   3.118 -                else if trans = lambda_liftingN then
   3.119 +                else if lambda_trans = lambda_liftingN then
   3.120                    t (* TODO: implement *)
   3.121 -                else if trans = combinatorsN then
   3.122 +                else if lambda_trans = combinatorsN then
   3.123                    t |> conceal_bounds Ts
   3.124                      |> cterm_of thy
   3.125                      |> Meson_Clausify.introduce_combinators_in_cterm
   3.126                      |> prop_of |> Logic.dest_equals |> snd
   3.127                      |> reveal_bounds Ts
   3.128 -                else if trans = lambdasN then
   3.129 +                else if lambda_trans = lambdasN then
   3.130                    t
   3.131                  else
   3.132 -                  error ("Unknown lambda translation: " ^ quote trans ^ ".")
   3.133 +                  error ("Unknown lambda translation method: " ^
   3.134 +                         quote lambda_trans ^ ".")
   3.135                end
   3.136          val (t, ctxt') = Variable.import_terms true [t] ctxt |>> the_single
   3.137        in t |> aux [] |> singleton (Variable.export_terms ctxt' ctxt) end
   3.138 @@ -992,7 +979,7 @@
   3.139        | aux t = t
   3.140    in t |> exists_subterm is_Var t ? aux end
   3.141  
   3.142 -fun preprocess_prop ctxt type_enc presimp_consts kind t =
   3.143 +fun preprocess_prop ctxt lambda_trans presimp_consts kind t =
   3.144    let
   3.145      val thy = Proof_Context.theory_of ctxt
   3.146      val t = t |> Envir.beta_eta_contract
   3.147 @@ -1005,7 +992,7 @@
   3.148        |> extensionalize_term ctxt
   3.149        |> presimplify_term ctxt presimp_consts
   3.150        |> perhaps (try (HOLogic.dest_Trueprop))
   3.151 -      |> process_abstractions_in_term ctxt type_enc kind
   3.152 +      |> process_abstractions_in_term ctxt lambda_trans kind
   3.153    end
   3.154  
   3.155  (* making fact and conjecture formulas *)
   3.156 @@ -1018,10 +1005,10 @@
   3.157       atomic_types = atomic_types}
   3.158    end
   3.159  
   3.160 -fun make_fact ctxt format type_enc eq_as_iff preproc presimp_consts
   3.161 +fun make_fact ctxt format type_enc lambda_trans eq_as_iff preproc presimp_consts
   3.162                ((name, loc), t) =
   3.163    let val thy = Proof_Context.theory_of ctxt in
   3.164 -    case t |> preproc ? preprocess_prop ctxt type_enc presimp_consts Axiom
   3.165 +    case t |> preproc ? preprocess_prop ctxt lambda_trans presimp_consts Axiom
   3.166             |> make_formula thy type_enc (eq_as_iff andalso format <> CNF) name
   3.167                             loc Axiom of
   3.168        formula as {combformula = AAtom (CombConst ((s, _), _, _)), ...} =>
   3.169 @@ -1029,7 +1016,8 @@
   3.170      | formula => SOME formula
   3.171    end
   3.172  
   3.173 -fun make_conjecture ctxt format prem_kind type_enc preproc presimp_consts ts =
   3.174 +fun make_conjecture ctxt format prem_kind type_enc lambda_trans preproc
   3.175 +                    presimp_consts ts =
   3.176    let
   3.177      val thy = Proof_Context.theory_of ctxt
   3.178      val last = length ts - 1
   3.179 @@ -1045,7 +1033,8 @@
   3.180                      else I)
   3.181                in
   3.182                  t |> preproc ?
   3.183 -                     (preprocess_prop ctxt type_enc presimp_consts kind #> freeze_term)
   3.184 +                     (preprocess_prop ctxt lambda_trans presimp_consts kind
   3.185 +                      #> freeze_term)
   3.186                    |> make_formula thy type_enc (format <> CNF) (string_of_int j)
   3.187                                    Local kind
   3.188                    |> maybe_negate
   3.189 @@ -1392,7 +1381,8 @@
   3.190    level_of_type_enc type_enc <> No_Types andalso
   3.191    not (null (Term.hidden_polymorphism t))
   3.192  
   3.193 -fun helper_facts_for_sym ctxt format type_enc (s, {types, ...} : sym_info) =
   3.194 +fun helper_facts_for_sym ctxt format type_enc lambda_trans
   3.195 +                         (s, {types, ...} : sym_info) =
   3.196    case strip_prefix_and_unascii const_prefix s of
   3.197      SOME mangled_s =>
   3.198      let
   3.199 @@ -1414,7 +1404,7 @@
   3.200          end
   3.201          |> map (fn (k, t) => (dub needs_fairly_sound j k, t)) o tag_list 1
   3.202        val make_facts =
   3.203 -        map_filter (make_fact ctxt format type_enc false false [])
   3.204 +        map_filter (make_fact ctxt format type_enc lambda_trans false false [])
   3.205        val fairly_sound = is_type_enc_fairly_sound type_enc
   3.206      in
   3.207        helper_table
   3.208 @@ -1428,9 +1418,10 @@
   3.209                      |> make_facts)
   3.210      end
   3.211    | NONE => []
   3.212 -fun helper_facts_for_sym_table ctxt format type_enc sym_tab =
   3.213 -  Symtab.fold_rev (append o helper_facts_for_sym ctxt format type_enc) sym_tab
   3.214 -                  []
   3.215 +fun helper_facts_for_sym_table ctxt format type_enc lambda_trans sym_tab =
   3.216 +  Symtab.fold_rev (append
   3.217 +                   o helper_facts_for_sym ctxt format type_enc lambda_trans)
   3.218 +                  sym_tab []
   3.219  
   3.220  (***************************************************************)
   3.221  (* Type Classes Present in the Axiom or Conjecture Clauses     *)
   3.222 @@ -1470,13 +1461,14 @@
   3.223  fun type_constrs_of_terms thy ts =
   3.224    Symtab.keys (fold (add_type_constrs_in_term thy) ts Symtab.empty)
   3.225  
   3.226 -fun translate_formulas ctxt format prem_kind type_enc preproc hyp_ts concl_t
   3.227 -                       facts =
   3.228 +fun translate_formulas ctxt format prem_kind type_enc lambda_trans preproc
   3.229 +                       hyp_ts concl_t facts =
   3.230    let
   3.231      val thy = Proof_Context.theory_of ctxt
   3.232      val fact_ts = facts |> map snd
   3.233      val presimp_consts = Meson.presimplified_consts ctxt
   3.234 -    val make_fact = make_fact ctxt format type_enc true preproc presimp_consts
   3.235 +    val make_fact =
   3.236 +      make_fact ctxt format type_enc lambda_trans true preproc presimp_consts
   3.237      val (facts, fact_names) =
   3.238        facts |> map (fn (name, t) => (name, t) |> make_fact |> rpair name)
   3.239              |> map_filter (try (apfst the))
   3.240 @@ -1493,7 +1485,8 @@
   3.241      val tycons = type_constrs_of_terms thy all_ts
   3.242      val conjs =
   3.243        hyp_ts @ [concl_t]
   3.244 -      |> make_conjecture ctxt format prem_kind type_enc preproc presimp_consts
   3.245 +      |> make_conjecture ctxt format prem_kind type_enc lambda_trans preproc
   3.246 +                         presimp_consts
   3.247      val (supers', arity_clauses) =
   3.248        if level_of_type_enc type_enc = No_Types then ([], [])
   3.249        else make_arity_clauses thy tycons supers
   3.250 @@ -1907,15 +1900,22 @@
   3.251  val conjsN = "Conjectures"
   3.252  val free_typesN = "Type variables"
   3.253  
   3.254 -val explicit_apply = NONE (* for experimental purposes *)
   3.255 +val explicit_apply = NONE (* for experiments *)
   3.256  
   3.257  fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_enc sound
   3.258 -        exporter readable_names preproc hyp_ts concl_t facts =
   3.259 +        exporter lambda_trans readable_names preproc hyp_ts concl_t facts =
   3.260    let
   3.261      val (format, type_enc) = choose_format [format] type_enc
   3.262 +    val _ =
   3.263 +      if lambda_trans = lambdasN andalso
   3.264 +         not (is_type_enc_higher_order type_enc) then
   3.265 +        error ("Lambda translation method incompatible with \
   3.266 +               \first-order encoding.")
   3.267 +      else
   3.268 +        ()
   3.269      val (fact_names, (conjs, facts, class_rel_clauses, arity_clauses)) =
   3.270 -      translate_formulas ctxt format prem_kind type_enc preproc hyp_ts concl_t
   3.271 -                         facts
   3.272 +      translate_formulas ctxt format prem_kind type_enc lambda_trans preproc
   3.273 +                         hyp_ts concl_t facts
   3.274      val sym_tab = conjs @ facts |> sym_table_for_facts ctxt explicit_apply
   3.275      val nonmono_Ts =
   3.276        conjs @ facts |> nonmonotonic_types_for_facts ctxt type_enc sound
   3.277 @@ -1924,8 +1924,9 @@
   3.278      val repaired_sym_tab =
   3.279        conjs @ facts |> sym_table_for_facts ctxt (SOME false)
   3.280      val helpers =
   3.281 -      repaired_sym_tab |> helper_facts_for_sym_table ctxt format type_enc
   3.282 -                       |> map repair
   3.283 +      repaired_sym_tab
   3.284 +      |> helper_facts_for_sym_table ctxt format type_enc lambda_trans
   3.285 +      |> map repair
   3.286      val poly_nonmono_Ts =
   3.287        if null nonmono_Ts orelse nonmono_Ts = [@{typ bool}] orelse
   3.288           polymorphism_of_type_enc type_enc <> Polymorphic then

     4.1 --- a/src/HOL/Tools/Metis/metis_translate.ML	Thu Jul 14 16:50:05 2011 +0200
     4.2 +++ b/src/HOL/Tools/Metis/metis_translate.ML	Thu Jul 14 16:50:05 2011 +0200
     4.3 @@ -196,8 +196,8 @@
     4.4        tracing ("PROPS:\n" ^ cat_lines (map (Syntax.string_of_term ctxt) props))
     4.5      *)
     4.6      val (atp_problem, _, _, _, _, _, sym_tab) =
     4.7 -      prepare_atp_problem ctxt CNF Hypothesis Axiom type_enc true false false
     4.8 -                          false [] @{prop False} props
     4.9 +      prepare_atp_problem ctxt CNF Hypothesis Axiom type_enc true false
    4.10 +                          combinatorsN false false [] @{prop False} props
    4.11      (*
    4.12      val _ = tracing ("ATP PROBLEM: " ^
    4.13                       cat_lines (tptp_lines_for_atp_problem CNF atp_problem))

     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Jul 14 16:50:05 2011 +0200
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Jul 14 16:50:05 2011 +0200
     5.3 @@ -63,6 +63,7 @@
     5.4    val dest_dir : string Config.T
     5.5    val problem_prefix : string Config.T
     5.6    val measure_run_time : bool Config.T
     5.7 +  val atp_lambda_translation : string Config.T
     5.8    val atp_readable_names : bool Config.T
     5.9    val smt_triggers : bool Config.T
    5.10    val smt_weights : bool Config.T
    5.11 @@ -336,6 +337,9 @@
    5.12  val measure_run_time =
    5.13    Attrib.setup_config_bool @{binding sledgehammer_measure_run_time} (K false)
    5.14  
    5.15 +val atp_lambda_translation =
    5.16 +  Attrib.setup_config_string @{binding sledgehammer_atp_lambda_translation}
    5.17 +                             (K smartN)
    5.18  (* In addition to being easier to read, readable names are often much shorter,
    5.19     especially if types are mangled in names. For these reason, they are enabled
    5.20     by default. *)
    5.21 @@ -510,6 +514,14 @@
    5.22     | NONE => type_enc_from_string best_type_enc)
    5.23    |> choose_format formats
    5.24  
    5.25 +fun effective_atp_lambda_translation ctxt type_enc =
    5.26 +  Config.get ctxt atp_lambda_translation
    5.27 +  |> (fn trans =>
    5.28 +         if trans = smartN then
    5.29 +           if is_type_enc_higher_order type_enc then lambdasN else combinatorsN
    5.30 +         else
    5.31 +           trans)
    5.32 +
    5.33  val metis_minimize_max_time = seconds 2.0
    5.34  
    5.35  fun choose_minimize_command minimize_command name preplay =
    5.36 @@ -641,8 +653,10 @@
    5.37                  val (atp_problem, pool, conjecture_offset, facts_offset,
    5.38                       fact_names, typed_helpers, sym_tab) =
    5.39                    prepare_atp_problem ctxt format conj_sym_kind prem_kind
    5.40 -                      type_enc sound false (Config.get ctxt atp_readable_names)
    5.41 -                      true hyp_ts concl_t facts
    5.42 +                      type_enc sound false
    5.43 +                      (effective_atp_lambda_translation ctxt type_enc)
    5.44 +                      (Config.get ctxt atp_readable_names) true hyp_ts concl_t
    5.45 +                      facts
    5.46                  fun weights () = atp_problem_weights atp_problem
    5.47                  val full_proof = debug orelse isar_proof
    5.48                  val core =