# HG changeset patch
# User blanchet
# Date 1310655005 -7200
# Node ID 62d64709af3b2ceffe37b828dfadf29900399336
# Parent  2b094d17f432011b12fd1f80a65c70cec31fd08b
added option to control which lambda translation to use (for experiments)

diff -r 2b094d17f432 -r 62d64709af3b src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Jul 14 15:14:38 2011 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Jul 14 16:50:05 2011 +0200
@@ -10,6 +10,7 @@
 val keepK = "keep"
 val type_encK = "type_enc"
 val slicingK = "slicing"
+val lambda_translationK = "lambda_translation"
 val e_weight_methodK = "e_weight_method"
 val spass_force_sosK = "spass_force_sos"
 val vampire_force_sosK = "vampire_force_sos"
@@ -353,8 +354,9 @@
   SH_FAIL of int * int |
   SH_ERROR
 
-fun run_sh prover_name prover type_enc max_relevant slicing e_weight_method spass_force_sos
-      vampire_force_sos hard_timeout timeout dir st =
+fun run_sh prover_name prover type_enc max_relevant slicing lambda_translation
+      e_weight_method spass_force_sos vampire_force_sos hard_timeout timeout dir
+      st =
   let
     val {context = ctxt, facts = chained_ths, goal} = Proof.goal st
     val i = 1
@@ -367,6 +369,8 @@
     val st' =
       st |> Proof.map_context
                 (change_dir dir
+                 #> (Option.map (Config.put ATP_Translate.lambda_translation)
+                       lambda_translation |> the_default I)
                  #> (Option.map (Config.put ATP_Systems.e_weight_method)
                        e_weight_method |> the_default I)
                  #> (Option.map (Config.put ATP_Systems.spass_force_sos)
@@ -455,6 +459,7 @@
     val type_enc = AList.lookup (op =) args type_encK |> the_default "smart"
     val max_relevant = AList.lookup (op =) args max_relevantK |> the_default "smart"
     val slicing = AList.lookup (op =) args slicingK |> the_default "true"
+    val lambda_translation = AList.lookup (op =) args lambda_translationK
     val e_weight_method = AList.lookup (op =) args e_weight_methodK
     val spass_force_sos = AList.lookup (op =) args spass_force_sosK
       |> Option.map (curry (op <>) "false")
@@ -466,8 +471,9 @@
        minimizer has a chance to do its magic *)
     val hard_timeout = SOME (2 * timeout)
     val (msg, result) =
-      run_sh prover_name prover type_enc max_relevant slicing e_weight_method spass_force_sos
-        vampire_force_sos hard_timeout timeout dir st
+      run_sh prover_name prover type_enc max_relevant slicing lambda_translation
+        e_weight_method spass_force_sos vampire_force_sos hard_timeout timeout
+        dir st
   in
     case result of
       SH_OK (time_isa, time_prover, names) =>
diff -r 2b094d17f432 -r 62d64709af3b src/HOL/Tools/ATP/atp_problem.ML
--- a/src/HOL/Tools/ATP/atp_problem.ML	Thu Jul 14 15:14:38 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Thu Jul 14 16:50:05 2011 +0200
@@ -480,7 +480,7 @@
       |> (fn s =>
              if size s > max_readable_name_size then
                String.substring (s, 0, max_readable_name_size div 2 - 4) ^
-               Word.toString (hashw_string (full_name, 0w0)) ^
+               string_of_int (hash_string full_name) ^
                String.extract (s, size s - max_readable_name_size div 2 + 4,
                                NONE)
              else
diff -r 2b094d17f432 -r 62d64709af3b src/HOL/Tools/ATP/atp_translate.ML
--- a/src/HOL/Tools/ATP/atp_translate.ML	Thu Jul 14 15:14:38 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Thu Jul 14 16:50:05 2011 +0200
@@ -63,6 +63,12 @@
   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
@@ -158,6 +164,17 @@
 (* Freshness almost guaranteed! *)
 val sledgehammer_weak_prefix = "Sledgehammer:"
 
+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 __
@@ -596,6 +613,14 @@
   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))
@@ -896,6 +921,12 @@
   else
     t
 
+fun conceal_lambdas Ts (t1 $ t2) = conceal_lambdas Ts t1 $ conceal_lambdas Ts t2
+  | conceal_lambdas Ts (Abs (_, T, t)) =
+    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 =
   let val thy = Proof_Context.theory_of ctxt in
     if Meson.is_fol_term thy t then
@@ -919,17 +950,29 @@
           | (t0 as Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])))
               $ t1 $ t2 =>
             t0 $ aux Ts t1 $ aux Ts t2
-          | _ => if not (exists_subterm (fn Abs _ => true | _ => false) t) then
-                   t
-                 else if is_type_enc_higher_order type_enc then
-                   t |> Envir.eta_contract
-                 else
-                   t |> conceal_bounds Ts
-                     |> Envir.eta_contract
-                     |> cterm_of thy
-                     |> Meson_Clausify.introduce_combinators_in_cterm
-                     |> prop_of |> Logic.dest_equals |> snd
-                     |> reveal_bounds Ts
+          | _ =>
+            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
+                  t |> conceal_lambdas []
+                else if trans = lambda_liftingN then
+                  t (* TODO: implement *)
+                else if 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
+                  t
+                else
+                  error ("Unknown lambda translation: " ^ quote trans ^ ".")
+              end
         val (t, ctxt') = Variable.import_terms true [t] ctxt |>> the_single
       in t |> aux [] |> singleton (Variable.export_terms ctxt' ctxt) end
       handle THM _ =>
diff -r 2b094d17f432 -r 62d64709af3b src/HOL/Tools/ATP/atp_util.ML
--- a/src/HOL/Tools/ATP/atp_util.ML	Thu Jul 14 15:14:38 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_util.ML	Thu Jul 14 16:50:05 2011 +0200
@@ -7,8 +7,8 @@
 signature ATP_UTIL =
 sig
   val timestamp : unit -> string
-  val hashw : word * word -> word
-  val hashw_string : string * word -> word
+  val hash_string : string -> int
+  val hash_term : term -> int
   val strip_spaces : bool -> (char -> bool) -> string -> string
   val nat_subscript : int -> string
   val unyxml : string -> string
@@ -42,6 +42,13 @@
 fun hashw (u, w) = Word.+ (u, Word.* (0w65599, w))
 fun hashw_char (c, w) = hashw (Word.fromInt (Char.ord c), w)
 fun hashw_string (s : string, w) = CharVector.foldl hashw_char w s
+fun hashw_term (t1 $ t2) = hashw (hashw_term t1, hashw_term t2)
+  | hashw_term (Const (s, _)) = hashw_string (s, 0w0)
+  | hashw_term (Free (s, _)) = hashw_string (s, 0w0)
+  | hashw_term _ = 0w0
+
+fun hash_string s = Word.toInt (hashw_string (s, 0w0))
+val hash_term = Word.toInt o hashw_term
 
 fun strip_c_style_comment _ [] = []
   | strip_c_style_comment is_evil (#"*" :: #"/" :: cs) =
diff -r 2b094d17f432 -r 62d64709af3b src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Thu Jul 14 15:14:38 2011 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Thu Jul 14 16:50:05 2011 +0200
@@ -1229,11 +1229,6 @@
   | is_ground_term (Const _) = true
   | is_ground_term _ = false
 
-fun hashw_term (t1 $ t2) = hashw (hashw_term t1, hashw_term t2)
-  | hashw_term (Const (s, _)) = hashw_string (s, 0w0)
-  | hashw_term _ = 0w0
-val hash_term = Word.toInt o hashw_term
-
 fun special_bounds ts =
   fold Term.add_vars ts [] |> sort (Term_Ord.fast_indexname_ord o pairself fst)
 
diff -r 2b094d17f432 -r 62d64709af3b src/HOL/Tools/Nitpick/nitpick_util.ML
--- a/src/HOL/Tools/Nitpick/nitpick_util.ML	Thu Jul 14 15:14:38 2011 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_util.ML	Thu Jul 14 16:50:05 2011 +0200
@@ -79,8 +79,7 @@
   val pstrs : string -> Pretty.T list
   val unyxml : string -> string
   val pretty_maybe_quote : Pretty.T -> Pretty.T
-  val hashw : word * word -> word
-  val hashw_string : string * word -> word
+  val hash_term : term -> int
 end;
 
 structure Nitpick_Util : NITPICK_UTIL =
@@ -298,7 +297,6 @@
     if maybe_quote s = s then pretty else Pretty.enum "" "\"" "\"" [pretty]
   end
 
-val hashw = ATP_Util.hashw
-val hashw_string = ATP_Util.hashw_string
+val hash_term = ATP_Util.hash_term
 
 end;