made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Mon May 30 17:00:38 2011 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Mon May 30 17:00:38 2011 +0200
@@ -505,14 +505,14 @@
AList.lookup (op =) args minimize_timeoutK
|> Option.map (fst o read_int o raw_explode) (* FIXME Symbol.explode (?) *)
|> the_default 5
- val params as {explicit_apply, ...} = Sledgehammer_Isar.default_params ctxt
+ val params = Sledgehammer_Isar.default_params ctxt
[("provers", prover_name),
("verbose", "true"),
("type_sys", type_sys),
("timeout", string_of_int timeout)]
val minimize =
Sledgehammer_Minimize.minimize_facts prover_name params
- (SOME explicit_apply) true 1 (Sledgehammer_Util.subgoal_count st)
+ true 1 (Sledgehammer_Util.subgoal_count st)
val _ = log separator
val (used_facts, (preplay, message)) = minimize st (these (!named_thms))
val msg = message (preplay ())
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Mon May 30 17:00:38 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Mon May 30 17:00:38 2011 +0200
@@ -46,7 +46,7 @@
-> translated_formula option * ((string * locality) * thm)
val prepare_atp_problem :
Proof.context -> format -> formula_kind -> formula_kind -> type_system
- -> bool -> term list -> term
+ -> bool option -> term list -> term
-> (translated_formula option * ((string * 'a) * thm)) list
-> string problem * string Symtab.table * int * int
* (string * 'a) list vector * int list * int Symtab.table
@@ -199,6 +199,13 @@
fun fact_lift f ({combformula, ...} : translated_formula) = f combformula
+val type_instance = Sign.typ_instance o Proof_Context.theory_of
+
+fun insert_type ctxt get_T x xs =
+ let val T = get_T x in
+ if exists (curry (type_instance ctxt) T o get_T) xs then xs
+ else x :: filter_out (curry (type_instance ctxt o swap) T o get_T) xs
+ end
(* The Booleans indicate whether all type arguments should be kept. *)
datatype type_arg_policy =
@@ -519,8 +526,6 @@
| deep_freeze_atyp T = T
val deep_freeze_type = map_atyps deep_freeze_atyp
-val type_instance = Sign.typ_instance o Proof_Context.theory_of
-
(* Finite types such as "unit", "bool", "bool * bool", and "bool => bool" are
dangerous because their "exhaust" properties can easily lead to unsound ATP
proofs. On the other hand, all HOL infinite types can be given the same
@@ -567,46 +572,91 @@
(** "hBOOL" and "hAPP" **)
type sym_info =
- {pred_sym : bool, min_ary : int, max_ary : int, typ : typ option}
+ {pred_sym : bool, min_ary : int, max_ary : int, types : typ list}
-fun add_combterm_syms_to_table explicit_apply =
+fun add_combterm_syms_to_table ctxt explicit_apply =
let
- fun aux top_level tm =
+ fun consider_var_arity const_T var_T max_ary =
+ let
+ fun iter ary T =
+ if ary = max_ary orelse type_instance ctxt (var_T, T) then ary
+ else iter (ary + 1) (range_type T)
+ in iter 0 const_T end
+ fun add top_level tm (accum as (ho_var_Ts, sym_tab)) =
let val (head, args) = strip_combterm_comb tm in
(case head of
CombConst ((s, _), T, _) =>
if String.isPrefix bound_var_prefix s then
- I
+ if explicit_apply = NONE andalso can dest_funT T then
+ let
+ fun repair_min_arity {pred_sym, min_ary, max_ary, types} =
+ {pred_sym = pred_sym,
+ min_ary =
+ fold (fn T' => consider_var_arity T' T) types min_ary,
+ max_ary = max_ary, types = types}
+ val ho_var_Ts' = ho_var_Ts |> insert_type ctxt I T
+ in
+ if pointer_eq (ho_var_Ts', ho_var_Ts) then accum
+ else (ho_var_Ts', Symtab.map (K repair_min_arity) sym_tab)
+ end
+ else
+ accum
else
- let val ary = length args in
- Symtab.map_default
- (s, {pred_sym = true,
- min_ary = if explicit_apply then 0 else ary,
- max_ary = 0, typ = SOME T})
- (fn {pred_sym, min_ary, max_ary, typ} =>
- {pred_sym = pred_sym andalso top_level,
- min_ary = Int.min (ary, min_ary),
- max_ary = Int.max (ary, max_ary),
- typ = if typ = SOME T then typ else NONE})
- end
- | _ => I)
- #> fold (aux false) args
+ let
+ val ary = length args
+ in
+ (ho_var_Ts,
+ case Symtab.lookup sym_tab s of
+ SOME {pred_sym, min_ary, max_ary, types} =>
+ let
+ val types' = types |> insert_type ctxt I T
+ val min_ary =
+ if is_some explicit_apply orelse
+ pointer_eq (types', types) then
+ min_ary
+ else
+ fold (consider_var_arity T) ho_var_Ts min_ary
+ in
+ Symtab.update (s, {pred_sym = pred_sym andalso top_level,
+ min_ary = Int.min (ary, min_ary),
+ max_ary = Int.max (ary, max_ary),
+ types = types'})
+ sym_tab
+ end
+ | NONE =>
+ let
+ val min_ary =
+ case explicit_apply of
+ SOME true => 0
+ | SOME false => ary
+ | NONE => fold (consider_var_arity T) ho_var_Ts ary
+ in
+ Symtab.update_new (s, {pred_sym = top_level,
+ min_ary = min_ary, max_ary = ary,
+ types = [T]})
+ sym_tab
+ end)
+ end
+ | _ => accum)
+ |> fold (add false) args
end
- in aux true end
-fun add_fact_syms_to_table explicit_apply =
- fact_lift (formula_fold NONE (K (add_combterm_syms_to_table explicit_apply)))
+ in add true end
+fun add_fact_syms_to_table ctxt explicit_apply =
+ fact_lift (formula_fold NONE
+ (K (add_combterm_syms_to_table ctxt explicit_apply)))
val default_sym_table_entries : (string * sym_info) list =
- [(tptp_equal, {pred_sym = true, min_ary = 2, max_ary = 2, typ = NONE}),
- (tptp_old_equal, {pred_sym = true, min_ary = 2, max_ary = 2, typ = NONE}),
+ [(tptp_equal, {pred_sym = true, min_ary = 2, max_ary = 2, types = []}),
+ (tptp_old_equal, {pred_sym = true, min_ary = 2, max_ary = 2, types = []}),
(make_fixed_const predicator_name,
- {pred_sym = true, min_ary = 1, max_ary = 1, typ = NONE})] @
+ {pred_sym = true, min_ary = 1, max_ary = 1, types = []})] @
([tptp_false, tptp_true]
- |> map (rpair {pred_sym = true, min_ary = 0, max_ary = 0, typ = NONE}))
+ |> map (rpair {pred_sym = true, min_ary = 0, max_ary = 0, types = []}))
-fun sym_table_for_facts explicit_apply facts =
- Symtab.empty |> fold Symtab.default default_sym_table_entries
- |> fold (add_fact_syms_to_table explicit_apply) facts
+fun sym_table_for_facts ctxt explicit_apply facts =
+ Symtab.empty
+ |> fold Symtab.default default_sym_table_entries
+ |> pair [] |> fold (add_fact_syms_to_table ctxt explicit_apply) facts |> snd
fun min_arity_of sym_tab s =
case Symtab.lookup sym_tab s of
@@ -759,7 +809,7 @@
|> close_formula_universally, simp_info, NONE)
end
-fun helper_facts_for_sym ctxt format type_sys (s, {typ, ...} : sym_info) =
+fun helper_facts_for_sym ctxt format type_sys (s, {types, ...} : sym_info) =
case strip_prefix_and_unascii const_prefix s of
SOME mangled_s =>
let
@@ -775,9 +825,9 @@
Mangled_Type_Args _ => true
| _ => false) andalso
not (null (Term.hidden_polymorphism t)))
- ? (case typ of
- SOME T => specialize_type thy (invert_const unmangled_s, T)
- | NONE => I)
+ ? (case types of
+ [T] => specialize_type thy (invert_const unmangled_s, T)
+ | _ => I)
end)
fun make_facts eq_as_iff =
map_filter (make_fact ctxt format type_sys false eq_as_iff false)
@@ -990,12 +1040,6 @@
(** Symbol declarations **)
-fun insert_type ctxt get_T x xs =
- let val T = get_T x in
- if exists (curry (type_instance ctxt) T o get_T) xs then xs
- else x :: filter_out (curry (type_instance ctxt o swap) T o get_T) xs
- end
-
fun should_declare_sym type_sys pred_sym s =
is_tptp_user_symbol s andalso not (String.isPrefix bound_var_prefix s) andalso
(case type_sys of
@@ -1223,11 +1267,12 @@
let
val (fact_names, (conjs, facts, class_rel_clauses, arity_clauses)) =
translate_formulas ctxt format prem_kind type_sys hyp_ts concl_t facts
- val sym_tab = conjs @ facts |> sym_table_for_facts explicit_apply
+ val sym_tab = conjs @ facts |> sym_table_for_facts ctxt explicit_apply
val nonmono_Ts = conjs @ facts |> nonmonotonic_types_for_facts ctxt type_sys
val repair = repair_fact ctxt format nonmono_Ts type_sys sym_tab
val (conjs, facts) = (conjs, facts) |> pairself (map repair)
- val repaired_sym_tab = conjs @ facts |> sym_table_for_facts false
+ 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_sys
|> map repair
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon May 30 17:00:38 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon May 30 17:00:38 2011 +0200
@@ -96,7 +96,7 @@
("max_relevant", "smart"),
("max_mono_iters", "3"),
("max_new_mono_instances", "400"),
- ("explicit_apply", "false"),
+ ("explicit_apply", "smart"),
("isar_proof", "false"),
("isar_shrink_factor", "1"),
("slicing", "true"),
@@ -118,8 +118,8 @@
val params_for_minimize =
["debug", "verbose", "overlord", "type_sys", "full_types", "max_mono_iters",
- "max_new_mono_instances", "isar_proof", "isar_shrink_factor", "timeout",
- "preplay_timeout"]
+ "max_new_mono_instances", "explicit_apply", "isar_proof",
+ "isar_shrink_factor", "timeout", "preplay_timeout"]
val property_dependent_params = ["provers", "full_types", "timeout"]
@@ -262,10 +262,10 @@
| _ => error ("Parameter " ^ quote name ^
"must be assigned a pair of floating-point \
\values (e.g., \"0.6 0.95\")")
- fun lookup_int_option name =
+ fun lookup_option lookup' name =
case lookup name of
SOME "smart" => NONE
- | _ => SOME (lookup_int name)
+ | _ => SOME (lookup' name)
val debug = mode <> Auto_Try andalso lookup_bool "debug"
val verbose = debug orelse (mode <> Auto_Try andalso lookup_bool "verbose")
val overlord = lookup_bool "overlord"
@@ -281,10 +281,10 @@
"smart" => Smart_Type_Sys (mode = Try orelse lookup_bool "full_types")
| s => Dumb_Type_Sys (type_sys_from_string s)
val relevance_thresholds = lookup_real_pair "relevance_thresholds"
- val max_relevant = lookup_int_option "max_relevant"
+ val max_relevant = lookup_option lookup_int "max_relevant"
val max_mono_iters = lookup_int "max_mono_iters"
val max_new_mono_instances = lookup_int "max_new_mono_instances"
- val explicit_apply = lookup_bool "explicit_apply"
+ val explicit_apply = lookup_option lookup_bool "explicit_apply"
val isar_proof = lookup_bool "isar_proof"
val isar_shrink_factor = Int.max (1, lookup_int "isar_shrink_factor")
val slicing = mode <> Auto_Try andalso lookup_bool "slicing"
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Mon May 30 17:00:38 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Mon May 30 17:00:38 2011 +0200
@@ -13,7 +13,7 @@
val binary_min_facts : int Config.T
val minimize_facts :
- string -> params -> bool option -> bool -> int -> int -> Proof.state
+ string -> params -> bool -> int -> int -> Proof.state
-> ((string * locality) * thm list) list
-> ((string * locality) * thm list) list option
* ((unit -> play) * (play -> string))
@@ -45,26 +45,16 @@
fun print silent f = if silent then () else Output.urgent_message (f ())
fun test_facts ({debug, verbose, overlord, provers, max_mono_iters,
- max_new_mono_instances, type_sys, isar_proof,
+ max_new_mono_instances, type_sys, explicit_apply, isar_proof,
isar_shrink_factor, preplay_timeout, ...} : params)
- explicit_apply_opt silent (prover : prover) timeout i n state facts =
+ silent (prover : prover) timeout i n state facts =
let
- val ctxt = Proof.context_of state
- val thy = Proof.theory_of state
val _ =
print silent (fn () =>
"Testing " ^ n_facts (map fst facts) ^
(if verbose then " (timeout: " ^ string_from_time timeout ^ ")"
else "") ^ "...")
val {goal, ...} = Proof.goal state
- val explicit_apply =
- case explicit_apply_opt of
- SOME explicit_apply => explicit_apply
- | NONE =>
- let val (_, hyp_ts, concl_t) = strip_subgoal ctxt goal i in
- not (forall (Meson.is_fol_term thy)
- (concl_t :: hyp_ts @ maps (map prop_of o snd) facts))
- end
val params =
{debug = debug, verbose = verbose, overlord = overlord, blocking = true,
provers = provers, type_sys = type_sys, explicit_apply = explicit_apply,
@@ -154,16 +144,15 @@
part of the timeout. *)
val slack_msecs = 200
-fun minimize_facts prover_name (params as {timeout, ...}) explicit_apply_opt
- silent i n state facts =
+fun minimize_facts prover_name (params as {timeout, ...}) silent i n state
+ facts =
let
val ctxt = Proof.context_of state
val prover = get_prover ctxt Minimize prover_name
val msecs = Time.toMilliseconds timeout
val _ = print silent (fn () => "Sledgehammer minimizer: " ^
quote prover_name ^ ".")
- fun do_test timeout =
- test_facts params explicit_apply_opt silent prover timeout i n state
+ fun do_test timeout = test_facts params silent prover timeout i n state
val timer = Timer.startRealTimer ()
in
(case do_test timeout facts of
@@ -212,7 +201,7 @@
[] => error "No prover is set."
| prover :: _ =>
(kill_provers ();
- minimize_facts prover params NONE false i n state facts
+ minimize_facts prover params false i n state facts
|> (fn (_, (preplay, message)) =>
Output.urgent_message (message (preplay ()))))
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Mon May 30 17:00:38 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Mon May 30 17:00:38 2011 +0200
@@ -73,7 +73,7 @@
(K 5.0)
fun get_minimizing_prover ctxt mode name
- (params as {debug, verbose, explicit_apply, ...}) minimize_command
+ (params as {debug, verbose, ...}) minimize_command
(problem as {state, subgoal, subgoal_count, facts, ...}) =
get_prover ctxt mode name params minimize_command problem
|> (fn result as {outcome, used_facts, run_time_in_msecs, preplay, message} =>
@@ -105,7 +105,7 @@
((false, name), preplay)
val (used_facts, (preplay, message)) =
if minimize then
- minimize_facts minimize_name params (SOME explicit_apply)
+ minimize_facts minimize_name params
(not verbose) subgoal subgoal_count state
(filter_used_facts used_facts
(map (apsnd single o untranslated_fact) facts))
--- a/src/HOL/ex/tptp_export.ML Mon May 30 17:00:38 2011 +0200
+++ b/src/HOL/ex/tptp_export.ML Mon May 30 17:00:38 2011 +0200
@@ -103,7 +103,7 @@
facts0 |> map_filter (try (fn ((_, loc), (_, th)) =>
Sledgehammer_ATP_Translate.translate_atp_fact ctxt format
type_sys true ((Thm.get_name_hint th, loc), th)))
- val explicit_apply = false
+ val explicit_apply = NONE
val (atp_problem, _, _, _, _, _, _) =
Sledgehammer_ATP_Translate.prepare_atp_problem ctxt format
ATP_Problem.Axiom ATP_Problem.Axiom type_sys explicit_apply []