# HG changeset patch # User blanchet # Date 1306767638 -7200 # Node ID b6e61d22fa61d05466d153c1d11c9fe945041a15 # Parent 8f1f80a40498be5e8c3e4d577a321ef79ceb62ed made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly diff -r 8f1f80a40498 -r b6e61d22fa61 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- 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 ()) diff -r 8f1f80a40498 -r b6e61d22fa61 src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML --- 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 diff -r 8f1f80a40498 -r b6e61d22fa61 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- 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" diff -r 8f1f80a40498 -r b6e61d22fa61 src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML --- 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 diff -r 8f1f80a40498 -r b6e61d22fa61 src/HOL/Tools/Sledgehammer/sledgehammer_run.ML --- 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)) diff -r 8f1f80a40498 -r b6e61d22fa61 src/HOL/ex/tptp_export.ML --- 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 []