--- 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) =>
--- 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
--- 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 _ =>
--- 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) =
--- 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)
--- 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;