1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Thu Jul 14 15:14:38 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Thu Jul 14 16:50:05 2011 +0200
     1.3 @@ -63,6 +63,12 @@
     1.4    val prefixed_predicator_name : string
     1.5    val prefixed_app_op_name : string
     1.6    val prefixed_type_tag_name : string
     1.7 +  val concealed_lambdasN : string
     1.8 +  val lambda_liftingN : string
     1.9 +  val combinatorsN : string
    1.10 +  val lambdasN : string
    1.11 +  val smartN : string
    1.12 +  val lambda_translation : string Config.T
    1.13    val ascii_of : string -> string
    1.14    val unascii_of : string -> string
    1.15    val strip_prefix_and_unascii : string -> string -> string option
    1.16 @@ -158,6 +164,17 @@
    1.17  (* Freshness almost guaranteed! *)
    1.18  val sledgehammer_weak_prefix = "Sledgehammer:"
    1.19  
    1.20 +val concealed_lambda_prefix = sledgehammer_weak_prefix ^ "lambda_"
    1.21 +
    1.22 +val concealed_lambdasN = "concealed_lambdas"
    1.23 +val lambda_liftingN = "lambda_lifting"
    1.24 +val combinatorsN = "combinators"
    1.25 +val lambdasN = "lambdas"
    1.26 +val smartN = "smart"
    1.27 +
    1.28 +val lambda_translation =
    1.29 +  Attrib.setup_config_string @{binding atp_lambda_translation} (K smartN)
    1.30 +
    1.31  (*Escaping of special characters.
    1.32    Alphanumeric characters are left unchanged.
    1.33    The character _ goes to __
    1.34 @@ -596,6 +613,14 @@
    1.35    is_type_level_virtually_sound level orelse level = Fin_Nonmono_Types
    1.36  val is_type_enc_fairly_sound = is_type_level_fairly_sound o level_of_type_enc
    1.37  
    1.38 +fun effective_lambda_translation ctxt type_enc =
    1.39 +  Config.get ctxt lambda_translation
    1.40 +  |> (fn trans =>
    1.41 +         if trans = smartN then
    1.42 +           if is_type_enc_higher_order type_enc then lambdasN else combinatorsN
    1.43 +         else
    1.44 +           trans)
    1.45 +
    1.46  fun choose_format formats (Simple_Types (order, level)) =
    1.47      if member (op =) formats THF then
    1.48        (THF, Simple_Types (order, level))
    1.49 @@ -896,6 +921,12 @@
    1.50    else
    1.51      t
    1.52  
    1.53 +fun conceal_lambdas Ts (t1 $ t2) = conceal_lambdas Ts t1 $ conceal_lambdas Ts t2
    1.54 +  | conceal_lambdas Ts (Abs (_, T, t)) =
    1.55 +    Free (concealed_lambda_prefix ^ string_of_int (hash_term t),
    1.56 +          T --> fastype_of1 (Ts, t))
    1.57 +  | conceal_lambdas _ t = t
    1.58 +
    1.59  fun process_abstractions_in_term ctxt type_enc kind t =
    1.60    let val thy = Proof_Context.theory_of ctxt in
    1.61      if Meson.is_fol_term thy t then
    1.62 @@ -919,17 +950,29 @@
    1.63            | (t0 as Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])))
    1.64                $ t1 $ t2 =>
    1.65              t0 $ aux Ts t1 $ aux Ts t2
    1.66 -          | _ => if not (exists_subterm (fn Abs _ => true | _ => false) t) then
    1.67 -                   t
    1.68 -                 else if is_type_enc_higher_order type_enc then
    1.69 -                   t |> Envir.eta_contract
    1.70 -                 else
    1.71 -                   t |> conceal_bounds Ts
    1.72 -                     |> Envir.eta_contract
    1.73 -                     |> cterm_of thy
    1.74 -                     |> Meson_Clausify.introduce_combinators_in_cterm
    1.75 -                     |> prop_of |> Logic.dest_equals |> snd
    1.76 -                     |> reveal_bounds Ts
    1.77 +          | _ =>
    1.78 +            if not (exists_subterm (fn Abs _ => true | _ => false) t) then
    1.79 +              t
    1.80 +            else
    1.81 +              let
    1.82 +                val trans = effective_lambda_translation ctxt type_enc
    1.83 +                val t = t |> Envir.eta_contract
    1.84 +              in
    1.85 +                if trans = concealed_lambdasN then
    1.86 +                  t |> conceal_lambdas []
    1.87 +                else if trans = lambda_liftingN then
    1.88 +                  t (* TODO: implement *)
    1.89 +                else if trans = combinatorsN then
    1.90 +                  t |> conceal_bounds Ts
    1.91 +                    |> cterm_of thy
    1.92 +                    |> Meson_Clausify.introduce_combinators_in_cterm
    1.93 +                    |> prop_of |> Logic.dest_equals |> snd
    1.94 +                    |> reveal_bounds Ts
    1.95 +                else if trans = lambdasN then
    1.96 +                  t
    1.97 +                else
    1.98 +                  error ("Unknown lambda translation: " ^ quote trans ^ ".")
    1.99 +              end
   1.100          val (t, ctxt') = Variable.import_terms true [t] ctxt |>> the_single
   1.101        in t |> aux [] |> singleton (Variable.export_terms ctxt' ctxt) end
   1.102        handle THM _ =>