1.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Jul 14 15:14:38 2011 +0200
     1.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Jul 14 16:50:05 2011 +0200
     1.3 @@ -10,6 +10,7 @@
     1.4  val keepK = "keep"
     1.5  val type_encK = "type_enc"
     1.6  val slicingK = "slicing"
     1.7 +val lambda_translationK = "lambda_translation"
     1.8  val e_weight_methodK = "e_weight_method"
     1.9  val spass_force_sosK = "spass_force_sos"
    1.10  val vampire_force_sosK = "vampire_force_sos"
    1.11 @@ -353,8 +354,9 @@
    1.12    SH_FAIL of int * int |
    1.13    SH_ERROR
    1.14  
    1.15 -fun run_sh prover_name prover type_enc max_relevant slicing e_weight_method spass_force_sos
    1.16 -      vampire_force_sos hard_timeout timeout dir st =
    1.17 +fun run_sh prover_name prover type_enc max_relevant slicing lambda_translation
    1.18 +      e_weight_method spass_force_sos vampire_force_sos hard_timeout timeout dir
    1.19 +      st =
    1.20    let
    1.21      val {context = ctxt, facts = chained_ths, goal} = Proof.goal st
    1.22      val i = 1
    1.23 @@ -367,6 +369,8 @@
    1.24      val st' =
    1.25        st |> Proof.map_context
    1.26                  (change_dir dir
    1.27 +                 #> (Option.map (Config.put ATP_Translate.lambda_translation)
    1.28 +                       lambda_translation |> the_default I)
    1.29                   #> (Option.map (Config.put ATP_Systems.e_weight_method)
    1.30                         e_weight_method |> the_default I)
    1.31                   #> (Option.map (Config.put ATP_Systems.spass_force_sos)
    1.32 @@ -455,6 +459,7 @@
    1.33      val type_enc = AList.lookup (op =) args type_encK |> the_default "smart"
    1.34      val max_relevant = AList.lookup (op =) args max_relevantK |> the_default "smart"
    1.35      val slicing = AList.lookup (op =) args slicingK |> the_default "true"
    1.36 +    val lambda_translation = AList.lookup (op =) args lambda_translationK
    1.37      val e_weight_method = AList.lookup (op =) args e_weight_methodK
    1.38      val spass_force_sos = AList.lookup (op =) args spass_force_sosK
    1.39        |> Option.map (curry (op <>) "false")
    1.40 @@ -466,8 +471,9 @@
    1.41         minimizer has a chance to do its magic *)
    1.42      val hard_timeout = SOME (2 * timeout)
    1.43      val (msg, result) =
    1.44 -      run_sh prover_name prover type_enc max_relevant slicing e_weight_method spass_force_sos
    1.45 -        vampire_force_sos hard_timeout timeout dir st
    1.46 +      run_sh prover_name prover type_enc max_relevant slicing lambda_translation
    1.47 +        e_weight_method spass_force_sos vampire_force_sos hard_timeout timeout
    1.48 +        dir st
    1.49    in
    1.50      case result of
    1.51        SH_OK (time_isa, time_prover, names) =>

     2.1 --- a/src/HOL/Tools/ATP/atp_problem.ML	Thu Jul 14 15:14:38 2011 +0200
     2.2 +++ b/src/HOL/Tools/ATP/atp_problem.ML	Thu Jul 14 16:50:05 2011 +0200
     2.3 @@ -480,7 +480,7 @@
     2.4        |> (fn s =>
     2.5               if size s > max_readable_name_size then
     2.6                 String.substring (s, 0, max_readable_name_size div 2 - 4) ^
     2.7 -               Word.toString (hashw_string (full_name, 0w0)) ^
     2.8 +               string_of_int (hash_string full_name) ^
     2.9                 String.extract (s, size s - max_readable_name_size div 2 + 4,
    2.10                                 NONE)
    2.11               else

     3.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Thu Jul 14 15:14:38 2011 +0200
     3.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Thu Jul 14 16:50:05 2011 +0200
     3.3 @@ -63,6 +63,12 @@
     3.4    val prefixed_predicator_name : string
     3.5    val prefixed_app_op_name : string
     3.6    val prefixed_type_tag_name : string
     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 lambda_translation : string Config.T
    3.13    val ascii_of : string -> string
    3.14    val unascii_of : string -> string
    3.15    val strip_prefix_and_unascii : string -> string -> string option
    3.16 @@ -158,6 +164,17 @@
    3.17  (* Freshness almost guaranteed! *)
    3.18  val sledgehammer_weak_prefix = "Sledgehammer:"
    3.19  
    3.20 +val concealed_lambda_prefix = sledgehammer_weak_prefix ^ "lambda_"
    3.21 +
    3.22 +val concealed_lambdasN = "concealed_lambdas"
    3.23 +val lambda_liftingN = "lambda_lifting"
    3.24 +val combinatorsN = "combinators"
    3.25 +val lambdasN = "lambdas"
    3.26 +val smartN = "smart"
    3.27 +
    3.28 +val lambda_translation =
    3.29 +  Attrib.setup_config_string @{binding atp_lambda_translation} (K smartN)
    3.30 +
    3.31  (*Escaping of special characters.
    3.32    Alphanumeric characters are left unchanged.
    3.33    The character _ goes to __
    3.34 @@ -596,6 +613,14 @@
    3.35    is_type_level_virtually_sound level orelse level = Fin_Nonmono_Types
    3.36  val is_type_enc_fairly_sound = is_type_level_fairly_sound o level_of_type_enc
    3.37  
    3.38 +fun effective_lambda_translation ctxt type_enc =
    3.39 +  Config.get ctxt lambda_translation
    3.40 +  |> (fn trans =>
    3.41 +         if trans = smartN then
    3.42 +           if is_type_enc_higher_order type_enc then lambdasN else combinatorsN
    3.43 +         else
    3.44 +           trans)
    3.45 +
    3.46  fun choose_format formats (Simple_Types (order, level)) =
    3.47      if member (op =) formats THF then
    3.48        (THF, Simple_Types (order, level))
    3.49 @@ -896,6 +921,12 @@
    3.50    else
    3.51      t
    3.52  
    3.53 +fun conceal_lambdas Ts (t1 $ t2) = conceal_lambdas Ts t1 $ conceal_lambdas Ts t2
    3.54 +  | conceal_lambdas Ts (Abs (_, T, t)) =
    3.55 +    Free (concealed_lambda_prefix ^ string_of_int (hash_term t),
    3.56 +          T --> fastype_of1 (Ts, t))
    3.57 +  | conceal_lambdas _ t = t
    3.58 +
    3.59  fun process_abstractions_in_term ctxt type_enc kind t =
    3.60    let val thy = Proof_Context.theory_of ctxt in
    3.61      if Meson.is_fol_term thy t then
    3.62 @@ -919,17 +950,29 @@
    3.63            | (t0 as Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])))
    3.64                $ t1 $ t2 =>
    3.65              t0 $ aux Ts t1 $ aux Ts t2
    3.66 -          | _ => if not (exists_subterm (fn Abs _ => true | _ => false) t) then
    3.67 -                   t
    3.68 -                 else if is_type_enc_higher_order type_enc then
    3.69 -                   t |> Envir.eta_contract
    3.70 -                 else
    3.71 -                   t |> conceal_bounds Ts
    3.72 -                     |> Envir.eta_contract
    3.73 -                     |> cterm_of thy
    3.74 -                     |> Meson_Clausify.introduce_combinators_in_cterm
    3.75 -                     |> prop_of |> Logic.dest_equals |> snd
    3.76 -                     |> reveal_bounds Ts
    3.77 +          | _ =>
    3.78 +            if not (exists_subterm (fn Abs _ => true | _ => false) t) then
    3.79 +              t
    3.80 +            else
    3.81 +              let
    3.82 +                val trans = effective_lambda_translation ctxt type_enc
    3.83 +                val t = t |> Envir.eta_contract
    3.84 +              in
    3.85 +                if trans = concealed_lambdasN then
    3.86 +                  t |> conceal_lambdas []
    3.87 +                else if trans = lambda_liftingN then
    3.88 +                  t (* TODO: implement *)
    3.89 +                else if trans = combinatorsN then
    3.90 +                  t |> conceal_bounds Ts
    3.91 +                    |> cterm_of thy
    3.92 +                    |> Meson_Clausify.introduce_combinators_in_cterm
    3.93 +                    |> prop_of |> Logic.dest_equals |> snd
    3.94 +                    |> reveal_bounds Ts
    3.95 +                else if trans = lambdasN then
    3.96 +                  t
    3.97 +                else
    3.98 +                  error ("Unknown lambda translation: " ^ quote trans ^ ".")
    3.99 +              end
   3.100          val (t, ctxt') = Variable.import_terms true [t] ctxt |>> the_single
   3.101        in t |> aux [] |> singleton (Variable.export_terms ctxt' ctxt) end
   3.102        handle THM _ =>

     4.1 --- a/src/HOL/Tools/ATP/atp_util.ML	Thu Jul 14 15:14:38 2011 +0200
     4.2 +++ b/src/HOL/Tools/ATP/atp_util.ML	Thu Jul 14 16:50:05 2011 +0200
     4.3 @@ -7,8 +7,8 @@
     4.4  signature ATP_UTIL =
     4.5  sig
     4.6    val timestamp : unit -> string
     4.7 -  val hashw : word * word -> word
     4.8 -  val hashw_string : string * word -> word
     4.9 +  val hash_string : string -> int
    4.10 +  val hash_term : term -> int
    4.11    val strip_spaces : bool -> (char -> bool) -> string -> string
    4.12    val nat_subscript : int -> string
    4.13    val unyxml : string -> string
    4.14 @@ -42,6 +42,13 @@
    4.15  fun hashw (u, w) = Word.+ (u, Word.* (0w65599, w))
    4.16  fun hashw_char (c, w) = hashw (Word.fromInt (Char.ord c), w)
    4.17  fun hashw_string (s : string, w) = CharVector.foldl hashw_char w s
    4.18 +fun hashw_term (t1 $ t2) = hashw (hashw_term t1, hashw_term t2)
    4.19 +  | hashw_term (Const (s, _)) = hashw_string (s, 0w0)
    4.20 +  | hashw_term (Free (s, _)) = hashw_string (s, 0w0)
    4.21 +  | hashw_term _ = 0w0
    4.22 +
    4.23 +fun hash_string s = Word.toInt (hashw_string (s, 0w0))
    4.24 +val hash_term = Word.toInt o hashw_term
    4.25  
    4.26  fun strip_c_style_comment _ [] = []
    4.27    | strip_c_style_comment is_evil (#"*" :: #"/" :: cs) =

     5.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Thu Jul 14 15:14:38 2011 +0200
     5.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Thu Jul 14 16:50:05 2011 +0200
     5.3 @@ -1229,11 +1229,6 @@
     5.4    | is_ground_term (Const _) = true
     5.5    | is_ground_term _ = false
     5.6  
     5.7 -fun hashw_term (t1 $ t2) = hashw (hashw_term t1, hashw_term t2)
     5.8 -  | hashw_term (Const (s, _)) = hashw_string (s, 0w0)
     5.9 -  | hashw_term _ = 0w0
    5.10 -val hash_term = Word.toInt o hashw_term
    5.11 -
    5.12  fun special_bounds ts =
    5.13    fold Term.add_vars ts [] |> sort (Term_Ord.fast_indexname_ord o pairself fst)
    5.14  

     6.1 --- a/src/HOL/Tools/Nitpick/nitpick_util.ML	Thu Jul 14 15:14:38 2011 +0200
     6.2 +++ b/src/HOL/Tools/Nitpick/nitpick_util.ML	Thu Jul 14 16:50:05 2011 +0200
     6.3 @@ -79,8 +79,7 @@
     6.4    val pstrs : string -> Pretty.T list
     6.5    val unyxml : string -> string
     6.6    val pretty_maybe_quote : Pretty.T -> Pretty.T
     6.7 -  val hashw : word * word -> word
     6.8 -  val hashw_string : string * word -> word
     6.9 +  val hash_term : term -> int
    6.10  end;
    6.11  
    6.12  structure Nitpick_Util : NITPICK_UTIL =
    6.13 @@ -298,7 +297,6 @@
    6.14      if maybe_quote s = s then pretty else Pretty.enum "" "\"" "\"" [pretty]
    6.15    end
    6.16  
    6.17 -val hashw = ATP_Util.hashw
    6.18 -val hashw_string = ATP_Util.hashw_string
    6.19 +val hash_term = ATP_Util.hash_term
    6.20  
    6.21  end;