--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Jul 14 17:14:54 2011 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Jul 14 17:15:24 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,9 @@
val st' =
st |> Proof.map_context
(change_dir dir
+ #> (Option.map (Config.put
+ Sledgehammer_Provers.atp_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 +460,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 +472,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/TPTP/atp_export.ML Thu Jul 14 17:14:54 2011 +0200
+++ b/src/HOL/TPTP/atp_export.ML Thu Jul 14 17:15:24 2011 +0200
@@ -159,8 +159,8 @@
val (atp_problem, _, _, _, _, _, _) =
facts
|> map (fn ((_, loc), th) => ((Thm.get_name_hint th, loc), prop_of th))
- |> prepare_atp_problem ctxt format Axiom Axiom type_enc true true false
- true [] @{prop False}
+ |> prepare_atp_problem ctxt format Axiom Axiom type_enc true true
+ combinatorsN false true [] @{prop False}
val atp_problem =
atp_problem
|> map (apsnd (filter_out (is_problem_line_tautology ctxt)))
--- a/src/HOL/Tools/ATP/atp_problem.ML Thu Jul 14 17:14:54 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML Thu Jul 14 17:15:24 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 17:14:54 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML Thu Jul 14 17:15:24 2011 +0200
@@ -31,6 +31,11 @@
Preds of polymorphism * type_level * type_heaviness |
Tags of polymorphism * type_level * type_heaviness
+ val concealed_lambdasN : string
+ val lambda_liftingN : string
+ val combinatorsN : string
+ val lambdasN : string
+ val smartN : string
val bound_var_prefix : string
val schematic_var_prefix : string
val fixed_var_prefix : string
@@ -76,6 +81,7 @@
val atp_schematic_consts_of : term -> typ list Symtab.table
val is_locality_global : locality -> bool
val type_enc_from_string : string -> type_enc
+ val is_type_enc_higher_order : type_enc -> bool
val polymorphism_of_type_enc : type_enc -> polymorphism
val level_of_type_enc : type_enc -> type_level
val is_type_enc_virtually_sound : type_enc -> bool
@@ -89,7 +95,7 @@
val factsN : string
val prepare_atp_problem :
Proof.context -> format -> formula_kind -> formula_kind -> type_enc -> bool
- -> bool -> bool -> bool -> term list -> term
+ -> bool -> string -> bool -> bool -> term list -> term
-> ((string * locality) * term) list
-> string problem * string Symtab.table * int * int
* (string * locality) list vector * int list * int Symtab.table
@@ -104,8 +110,13 @@
type name = string * string
-(* experimental *)
-val generate_info = false
+val concealed_lambdasN = "concealed_lambdas"
+val lambda_liftingN = "lambda_lifting"
+val combinatorsN = "combinators"
+val lambdasN = "lambdas"
+val smartN = "smart"
+
+val generate_info = false (* experimental *)
fun isabelle_info s =
if generate_info then SOME (ATerm ("[]", [ATerm ("isabelle_" ^ s, [])]))
@@ -158,6 +169,8 @@
(* Freshness almost guaranteed! *)
val sledgehammer_weak_prefix = "Sledgehammer:"
+val concealed_lambda_prefix = sledgehammer_weak_prefix ^ "lambda_"
+
(*Escaping of special characters.
Alphanumeric characters are left unchanged.
The character _ goes to __
@@ -896,7 +909,14 @@
else
t
-fun process_abstractions_in_term ctxt type_enc kind t =
+fun conceal_lambdas Ts (t1 $ t2) = conceal_lambdas Ts t1 $ conceal_lambdas Ts t2
+ | conceal_lambdas Ts (Abs (_, T, t)) =
+ (* slightly unsound because of hash collisions *)
+ 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 lambda_trans kind t =
let val thy = Proof_Context.theory_of ctxt in
if Meson.is_fol_term thy t then
t
@@ -919,17 +939,27 @@
| (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 t = t |> Envir.eta_contract in
+ if lambda_trans = concealed_lambdasN then
+ t |> conceal_lambdas []
+ else if lambda_trans = lambda_liftingN then
+ t (* TODO: implement *)
+ else if lambda_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 lambda_trans = lambdasN then
+ t
+ else
+ error ("Unknown lambda translation method: " ^
+ quote lambda_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 _ =>
@@ -949,7 +979,7 @@
| aux t = t
in t |> exists_subterm is_Var t ? aux end
-fun preprocess_prop ctxt type_enc presimp_consts kind t =
+fun preprocess_prop ctxt lambda_trans presimp_consts kind t =
let
val thy = Proof_Context.theory_of ctxt
val t = t |> Envir.beta_eta_contract
@@ -962,7 +992,7 @@
|> extensionalize_term ctxt
|> presimplify_term ctxt presimp_consts
|> perhaps (try (HOLogic.dest_Trueprop))
- |> process_abstractions_in_term ctxt type_enc kind
+ |> process_abstractions_in_term ctxt lambda_trans kind
end
(* making fact and conjecture formulas *)
@@ -975,10 +1005,10 @@
atomic_types = atomic_types}
end
-fun make_fact ctxt format type_enc eq_as_iff preproc presimp_consts
+fun make_fact ctxt format type_enc lambda_trans eq_as_iff preproc presimp_consts
((name, loc), t) =
let val thy = Proof_Context.theory_of ctxt in
- case t |> preproc ? preprocess_prop ctxt type_enc presimp_consts Axiom
+ case t |> preproc ? preprocess_prop ctxt lambda_trans presimp_consts Axiom
|> make_formula thy type_enc (eq_as_iff andalso format <> CNF) name
loc Axiom of
formula as {combformula = AAtom (CombConst ((s, _), _, _)), ...} =>
@@ -986,7 +1016,8 @@
| formula => SOME formula
end
-fun make_conjecture ctxt format prem_kind type_enc preproc presimp_consts ts =
+fun make_conjecture ctxt format prem_kind type_enc lambda_trans preproc
+ presimp_consts ts =
let
val thy = Proof_Context.theory_of ctxt
val last = length ts - 1
@@ -1002,7 +1033,8 @@
else I)
in
t |> preproc ?
- (preprocess_prop ctxt type_enc presimp_consts kind #> freeze_term)
+ (preprocess_prop ctxt lambda_trans presimp_consts kind
+ #> freeze_term)
|> make_formula thy type_enc (format <> CNF) (string_of_int j)
Local kind
|> maybe_negate
@@ -1349,7 +1381,8 @@
level_of_type_enc type_enc <> No_Types andalso
not (null (Term.hidden_polymorphism t))
-fun helper_facts_for_sym ctxt format type_enc (s, {types, ...} : sym_info) =
+fun helper_facts_for_sym ctxt format type_enc lambda_trans
+ (s, {types, ...} : sym_info) =
case strip_prefix_and_unascii const_prefix s of
SOME mangled_s =>
let
@@ -1371,7 +1404,7 @@
end
|> map (fn (k, t) => (dub needs_fairly_sound j k, t)) o tag_list 1
val make_facts =
- map_filter (make_fact ctxt format type_enc false false [])
+ map_filter (make_fact ctxt format type_enc lambda_trans false false [])
val fairly_sound = is_type_enc_fairly_sound type_enc
in
helper_table
@@ -1385,9 +1418,10 @@
|> make_facts)
end
| NONE => []
-fun helper_facts_for_sym_table ctxt format type_enc sym_tab =
- Symtab.fold_rev (append o helper_facts_for_sym ctxt format type_enc) sym_tab
- []
+fun helper_facts_for_sym_table ctxt format type_enc lambda_trans sym_tab =
+ Symtab.fold_rev (append
+ o helper_facts_for_sym ctxt format type_enc lambda_trans)
+ sym_tab []
(***************************************************************)
(* Type Classes Present in the Axiom or Conjecture Clauses *)
@@ -1427,13 +1461,14 @@
fun type_constrs_of_terms thy ts =
Symtab.keys (fold (add_type_constrs_in_term thy) ts Symtab.empty)
-fun translate_formulas ctxt format prem_kind type_enc preproc hyp_ts concl_t
- facts =
+fun translate_formulas ctxt format prem_kind type_enc lambda_trans preproc
+ hyp_ts concl_t facts =
let
val thy = Proof_Context.theory_of ctxt
val fact_ts = facts |> map snd
val presimp_consts = Meson.presimplified_consts ctxt
- val make_fact = make_fact ctxt format type_enc true preproc presimp_consts
+ val make_fact =
+ make_fact ctxt format type_enc lambda_trans true preproc presimp_consts
val (facts, fact_names) =
facts |> map (fn (name, t) => (name, t) |> make_fact |> rpair name)
|> map_filter (try (apfst the))
@@ -1450,7 +1485,8 @@
val tycons = type_constrs_of_terms thy all_ts
val conjs =
hyp_ts @ [concl_t]
- |> make_conjecture ctxt format prem_kind type_enc preproc presimp_consts
+ |> make_conjecture ctxt format prem_kind type_enc lambda_trans preproc
+ presimp_consts
val (supers', arity_clauses) =
if level_of_type_enc type_enc = No_Types then ([], [])
else make_arity_clauses thy tycons supers
@@ -1864,15 +1900,22 @@
val conjsN = "Conjectures"
val free_typesN = "Type variables"
-val explicit_apply = NONE (* for experimental purposes *)
+val explicit_apply = NONE (* for experiments *)
fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_enc sound
- exporter readable_names preproc hyp_ts concl_t facts =
+ exporter lambda_trans readable_names preproc hyp_ts concl_t facts =
let
val (format, type_enc) = choose_format [format] type_enc
+ val _ =
+ if lambda_trans = lambdasN andalso
+ not (is_type_enc_higher_order type_enc) then
+ error ("Lambda translation method incompatible with \
+ \first-order encoding.")
+ else
+ ()
val (fact_names, (conjs, facts, class_rel_clauses, arity_clauses)) =
- translate_formulas ctxt format prem_kind type_enc preproc hyp_ts concl_t
- facts
+ translate_formulas ctxt format prem_kind type_enc lambda_trans preproc
+ hyp_ts concl_t facts
val sym_tab = conjs @ facts |> sym_table_for_facts ctxt explicit_apply
val nonmono_Ts =
conjs @ facts |> nonmonotonic_types_for_facts ctxt type_enc sound
@@ -1881,8 +1924,9 @@
val repaired_sym_tab =
conjs @ facts |> sym_table_for_facts ctxt (SOME false)
val helpers =
- repaired_sym_tab |> helper_facts_for_sym_table ctxt format type_enc
- |> map repair
+ repaired_sym_tab
+ |> helper_facts_for_sym_table ctxt format type_enc lambda_trans
+ |> map repair
val poly_nonmono_Ts =
if null nonmono_Ts orelse nonmono_Ts = [@{typ bool}] orelse
polymorphism_of_type_enc type_enc <> Polymorphic then
--- a/src/HOL/Tools/ATP/atp_util.ML Thu Jul 14 17:14:54 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_util.ML Thu Jul 14 17:15:24 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/Metis/metis_translate.ML Thu Jul 14 17:14:54 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_translate.ML Thu Jul 14 17:15:24 2011 +0200
@@ -196,8 +196,8 @@
tracing ("PROPS:\n" ^ cat_lines (map (Syntax.string_of_term ctxt) props))
*)
val (atp_problem, _, _, _, _, _, sym_tab) =
- prepare_atp_problem ctxt CNF Hypothesis Axiom type_enc true false false
- false [] @{prop False} props
+ prepare_atp_problem ctxt CNF Hypothesis Axiom type_enc true false
+ combinatorsN false false [] @{prop False} props
(*
val _ = tracing ("ATP PROBLEM: " ^
cat_lines (tptp_lines_for_atp_problem CNF atp_problem))
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Thu Jul 14 17:14:54 2011 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Thu Jul 14 17:15:24 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 17:14:54 2011 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_util.ML Thu Jul 14 17:15:24 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;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Jul 14 17:14:54 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Jul 14 17:15:24 2011 +0200
@@ -63,6 +63,7 @@
val dest_dir : string Config.T
val problem_prefix : string Config.T
val measure_run_time : bool Config.T
+ val atp_lambda_translation : string Config.T
val atp_readable_names : bool Config.T
val smt_triggers : bool Config.T
val smt_weights : bool Config.T
@@ -336,6 +337,9 @@
val measure_run_time =
Attrib.setup_config_bool @{binding sledgehammer_measure_run_time} (K false)
+val atp_lambda_translation =
+ Attrib.setup_config_string @{binding sledgehammer_atp_lambda_translation}
+ (K smartN)
(* In addition to being easier to read, readable names are often much shorter,
especially if types are mangled in names. For these reason, they are enabled
by default. *)
@@ -510,6 +514,14 @@
| NONE => type_enc_from_string best_type_enc)
|> choose_format formats
+fun effective_atp_lambda_translation ctxt type_enc =
+ Config.get ctxt atp_lambda_translation
+ |> (fn trans =>
+ if trans = smartN then
+ if is_type_enc_higher_order type_enc then lambdasN else combinatorsN
+ else
+ trans)
+
val metis_minimize_max_time = seconds 2.0
fun choose_minimize_command minimize_command name preplay =
@@ -641,8 +653,10 @@
val (atp_problem, pool, conjecture_offset, facts_offset,
fact_names, typed_helpers, sym_tab) =
prepare_atp_problem ctxt format conj_sym_kind prem_kind
- type_enc sound false (Config.get ctxt atp_readable_names)
- true hyp_ts concl_t facts
+ type_enc sound false
+ (effective_atp_lambda_translation ctxt type_enc)
+ (Config.get ctxt atp_readable_names) true hyp_ts concl_t
+ facts
fun weights () = atp_problem_weights atp_problem
val full_proof = debug orelse isar_proof
val core =