# HG changeset patch # User blanchet # Date 1292408788 -3600 # Node ID eb80538166b6c6c02482decdb48f57a78e5875c1 # Parent 8b634031b2a546d392855d2cdd2bbeab06266d07 implemented partially-typed "tags" type encoding diff -r 8b634031b2a5 -r eb80538166b6 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Dec 15 11:26:28 2010 +0100 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Dec 15 11:26:28 2010 +0100 @@ -351,7 +351,7 @@ st |> Proof.map_context (change_dir dir #> Config.put Sledgehammer_Provers.measure_run_time true) - val params as {full_types, relevance_thresholds, max_relevant, ...} = + val params as {type_sys, relevance_thresholds, max_relevant, ...} = Sledgehammer_Isar.default_params ctxt [("verbose", "true"), ("timeout", Int.toString timeout)] @@ -363,8 +363,11 @@ Sledgehammer_Provers.relevance_fudge_for_prover ctxt prover_name val relevance_override = {add = [], del = [], only = false} val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal i + val no_dangerous_types = + Sledgehammer_ATP_Translate.types_dangerous_types type_sys val facts = - Sledgehammer_Filter.relevant_facts ctxt full_types relevance_thresholds + Sledgehammer_Filter.relevant_facts ctxt no_dangerous_types + relevance_thresholds (the_default default_max_relevant max_relevant) is_built_in_const relevance_fudge relevance_override chained_ths hyp_ts concl_t val problem = diff -r 8b634031b2a5 -r eb80538166b6 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Wed Dec 15 11:26:28 2010 +0100 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Wed Dec 15 11:26:28 2010 +0100 @@ -116,12 +116,14 @@ extract_relevance_fudge args (Sledgehammer_Provers.relevance_fudge_for_prover ctxt prover) val relevance_override = {add = [], del = [], only = false} - val {relevance_thresholds, full_types, max_relevant, ...} = + val {relevance_thresholds, type_sys, max_relevant, ...} = Sledgehammer_Isar.default_params ctxt args val subgoal = 1 val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal subgoal + val no_dangerous_types = + Sledgehammer_ATP_Translate.types_dangerous_types type_sys val facts = - Sledgehammer_Filter.relevant_facts ctxt full_types + Sledgehammer_Filter.relevant_facts ctxt no_dangerous_types relevance_thresholds (the_default default_max_relevant max_relevant) is_built_in_const relevance_fudge relevance_override facts hyp_ts concl_t diff -r 8b634031b2a5 -r eb80538166b6 src/HOL/Mirabelle/Tools/sledgehammer_tactic.ML --- a/src/HOL/Mirabelle/Tools/sledgehammer_tactic.ML Wed Dec 15 11:26:28 2010 +0100 +++ b/src/HOL/Mirabelle/Tools/sledgehammer_tactic.ML Wed Dec 15 11:26:28 2010 +0100 @@ -17,7 +17,7 @@ fun run_atp force_full_types timeout i n ctxt goal name = let val chained_ths = [] (* a tactic has no chained ths *) - val params as {full_types, relevance_thresholds, max_relevant, ...} = + val params as {type_sys, relevance_thresholds, max_relevant, ...} = ((if force_full_types then [("full_types", "true")] else []) @ [("timeout", Int.toString (Time.toSeconds timeout))]) @ [("overlord", "true")] @@ -31,8 +31,11 @@ Sledgehammer_Provers.relevance_fudge_for_prover ctxt name val relevance_override = {add = [], del = [], only = false} val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal i + val no_dangerous_types = + Sledgehammer_ATP_Translate.types_dangerous_types type_sys val facts = - Sledgehammer_Filter.relevant_facts ctxt full_types relevance_thresholds + Sledgehammer_Filter.relevant_facts ctxt no_dangerous_types + relevance_thresholds (the_default default_max_relevant max_relevant) is_built_in_const relevance_fudge relevance_override chained_ths hyp_ts concl_t (* Check for constants other than the built-in HOL constants. If none of diff -r 8b634031b2a5 -r eb80538166b6 src/HOL/Tools/Metis/metis_translate.ML --- a/src/HOL/Tools/Metis/metis_translate.ML Wed Dec 15 11:26:28 2010 +0100 +++ b/src/HOL/Tools/Metis/metis_translate.ML Wed Dec 15 11:26:28 2010 +0100 @@ -36,7 +36,7 @@ tfrees: type_literal list, old_skolems: (string * term) list} - val type_wrapper_name : string + val type_tag_name : string val bound_var_prefix : string val schematic_var_prefix: string val fixed_var_prefix: string @@ -82,7 +82,7 @@ structure Metis_Translate : METIS_TRANSLATE = struct -val type_wrapper_name = "ti" +val type_tag_name = "ty" val bound_var_prefix = "B_" val schematic_var_prefix = "V_" @@ -580,15 +580,16 @@ Metis_Term.Fn (".", map hol_term_to_fol_HO [tm1, tm2]); (*The fully-typed translation, to avoid type errors*) -fun wrap_type (tm, ty) = - Metis_Term.Fn (type_wrapper_name, [tm, metis_term_from_combtyp ty]) +fun tag_with_type tm ty = + Metis_Term.Fn (type_tag_name, [tm, metis_term_from_combtyp ty]) -fun hol_term_to_fol_FT (CombVar ((s, _), ty)) = wrap_type (Metis_Term.Var s, ty) - | hol_term_to_fol_FT (CombConst((a, _), ty, _)) = - wrap_type (Metis_Term.Fn(fn_isa_to_met_sublevel a, []), ty) - | hol_term_to_fol_FT (tm as CombApp(tm1,tm2)) = - wrap_type (Metis_Term.Fn(".", map hol_term_to_fol_FT [tm1,tm2]), - combtyp_of tm) +fun hol_term_to_fol_FT (CombVar ((s, _), ty)) = + tag_with_type (Metis_Term.Var s) ty + | hol_term_to_fol_FT (CombConst ((a, _), ty, _)) = + tag_with_type (Metis_Term.Fn (fn_isa_to_met_sublevel a, [])) ty + | hol_term_to_fol_FT (tm as CombApp (tm1,tm2)) = + tag_with_type (Metis_Term.Fn (".", map hol_term_to_fol_FT [tm1, tm2])) + (combtyp_of tm) fun hol_literal_to_fol FO (FOLLiteral (pos, tm)) = let val (CombConst((p, _), _, tys), tms) = strip_combterm_comb tm diff -r 8b634031b2a5 -r eb80538166b6 src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Wed Dec 15 11:26:28 2010 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Wed Dec 15 11:26:28 2010 +0100 @@ -311,7 +311,7 @@ ATerm ("hBOOL", [u1]) => aux (SOME @{typ bool}) [] u1 | ATerm ("hAPP", [u1, u2]) => aux opt_T (u2 :: extra_us) u1 | ATerm (a, us) => - if a = type_wrapper_name then + if a = type_tag_name then case us of [typ_u, term_u] => aux (SOME (type_from_fo_term tfrees typ_u)) extra_us term_u diff -r 8b634031b2a5 -r eb80538166b6 src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Wed Dec 15 11:26:28 2010 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Wed Dec 15 11:26:28 2010 +0100 @@ -15,12 +15,13 @@ Tags of bool | Preds of bool | Const_Args | - Overload_Args | No_Types + val precise_overloaded_args : bool Unsynchronized.ref val fact_prefix : string val conjecture_prefix : string val is_fully_typed : type_system -> bool + val types_dangerous_types : type_system -> bool val num_atp_type_args : theory -> type_system -> string -> int val translate_atp_fact : Proof.context -> (string * 'a) * thm @@ -31,13 +32,17 @@ -> string problem * string Symtab.table * int * (string * 'a) list vector end; -structure Sledgehammer_ATP_Translate : SLEDGEHAMMER_ATP_TRANSLATE = +structure Sledgehammer_ATP_Translate (*### : SLEDGEHAMMER_ATP_TRANSLATE *) = struct open ATP_Problem open Metis_Translate open Sledgehammer_Util +(* FIXME: Remove references once appropriate defaults have been determined + empirically. *) +val precise_overloaded_args = Unsynchronized.ref false + val fact_prefix = "fact_" val conjecture_prefix = "conj_" val helper_prefix = "help_" @@ -58,26 +63,29 @@ Tags of bool | Preds of bool | Const_Args | - Overload_Args | No_Types fun is_fully_typed (Tags full_types) = full_types | is_fully_typed (Preds full_types) = full_types | is_fully_typed _ = false +fun types_dangerous_types (Tags _) = true + | types_dangerous_types (Preds _) = true + | types_dangerous_types _ = false + (* This is an approximation. If it returns "true" for a constant that isn't overloaded (i.e., that has one uniform definition), needless clutter is generated; if it returns "false" for an overloaded constant, the ATP gets a license to do unsound reasoning if the type system is "overloaded_args". *) fun is_overloaded thy s = + not (!precise_overloaded_args) orelse length (Defs.specifications_of (Theory.defs_of thy) s) > 1 fun needs_type_args thy type_sys s = case type_sys of - Tags full_types => not full_types - | Preds full_types => not full_types - | Const_Args => true - | Overload_Args => is_overloaded thy s + Tags full_types => not full_types andalso is_overloaded thy s + | Preds full_types => is_overloaded thy s (* FIXME: could be more precise *) + | Const_Args => is_overloaded thy s | No_Types => false fun num_atp_type_args thy type_sys s = @@ -319,7 +327,7 @@ (conjectures, facts, helper_facts, class_rel_clauses, arity_clauses)) end -fun wrap_type ty t = ATerm ((type_wrapper_name, type_wrapper_name), [ty, t]) +fun tag_with_type ty t = ATerm (`I type_tag_name, [ty, t]) fun fo_term_for_combtyp (CombTVar name) = ATerm (name, []) | fo_term_for_combtyp (CombTFree name) = ATerm (name, []) @@ -333,8 +341,44 @@ fun formula_for_fo_literal (pos, t) = AAtom t |> not pos ? mk_anot -fun fo_term_for_combterm thy type_sys = +(* Finite types such as "unit", "bool", "bool * bool", and "bool => bool" are + considered dangerous because their "exhaust" properties can easily lead to + unsound ATP proofs. The checks below are an (unsound) approximation of + finiteness. *) + +fun is_dtyp_dangerous _ (Datatype_Aux.DtTFree _) = true + | is_dtyp_dangerous ctxt (Datatype_Aux.DtType (s, Us)) = + is_type_constr_dangerous ctxt s andalso forall (is_dtyp_dangerous ctxt) Us + | is_dtyp_dangerous _ (Datatype_Aux.DtRec _) = false +and is_type_dangerous ctxt (Type (s, Ts)) = + is_type_constr_dangerous ctxt s andalso forall (is_type_dangerous ctxt) Ts + | is_type_dangerous ctxt _ = false +and is_type_constr_dangerous ctxt s = + let val thy = ProofContext.theory_of ctxt in + case Datatype_Data.get_info thy s of + SOME {descr, ...} => + forall (fn (_, (_, _, constrs)) => + forall (forall (is_dtyp_dangerous ctxt) o snd) constrs) descr + | NONE => + case Typedef.get_info ctxt s of + ({rep_type, ...}, _) :: _ => is_type_dangerous ctxt rep_type + | [] => true + end + +fun is_combtyp_dangerous ctxt (CombType ((s, _), tys)) = + (case strip_prefix_and_unascii type_const_prefix s of + SOME s' => forall (is_combtyp_dangerous ctxt) tys andalso + is_type_constr_dangerous ctxt (invert_const s') + | NONE => false) + | is_combtyp_dangerous _ _ = false + +fun should_tag_with_type ctxt (Tags full_types) ty = + full_types orelse is_combtyp_dangerous ctxt ty + | should_tag_with_type _ _ _ = false + +fun fo_term_for_combterm ctxt type_sys = let + val thy = ProofContext.theory_of ctxt fun aux top_level u = let val (head, args) = strip_combterm_comb u @@ -364,31 +408,32 @@ end) | CombVar (name, _) => (name, []) | CombApp _ => raise Fail "impossible \"CombApp\"" - val t = ATerm (x, map fo_term_for_combtyp ty_args @ - map (aux false) args) + val t = + ATerm (x, map fo_term_for_combtyp ty_args @ map (aux false) args) + val ty = combtyp_of u in - t |> (if type_sys = Tags true then - wrap_type (fo_term_for_combtyp (combtyp_of u)) + t |> (if should_tag_with_type ctxt type_sys ty then + tag_with_type (fo_term_for_combtyp ty) else I) end in aux true end -fun formula_for_combformula thy type_sys = +fun formula_for_combformula ctxt type_sys = let fun aux (AQuant (q, xs, phi)) = AQuant (q, xs, aux phi) | aux (AConn (c, phis)) = AConn (c, map aux phis) - | aux (AAtom tm) = AAtom (fo_term_for_combterm thy type_sys tm) + | aux (AAtom tm) = AAtom (fo_term_for_combterm ctxt type_sys tm) in aux end -fun formula_for_fact thy type_sys +fun formula_for_fact ctxt type_sys ({combformula, ctypes_sorts, ...} : translated_formula) = mk_ahorn (map (formula_for_fo_literal o fo_literal_for_type_literal) (atp_type_literals_for_types type_sys ctypes_sorts)) - (formula_for_combformula thy type_sys combformula) + (formula_for_combformula ctxt type_sys combformula) -fun problem_line_for_fact thy prefix type_sys (formula as {name, kind, ...}) = - Fof (prefix ^ ascii_of name, kind, formula_for_fact thy type_sys formula) +fun problem_line_for_fact ctxt prefix type_sys (formula as {name, kind, ...}) = + Fof (prefix ^ ascii_of name, kind, formula_for_fact ctxt type_sys formula) fun problem_line_for_class_rel_clause (ClassRelClause {name, subclass, superclass, ...}) = @@ -411,10 +456,10 @@ (formula_for_fo_literal (fo_literal_for_arity_literal conclLit))) -fun problem_line_for_conjecture thy type_sys +fun problem_line_for_conjecture ctxt type_sys ({name, kind, combformula, ...} : translated_formula) = Fof (conjecture_prefix ^ name, kind, - formula_for_combformula thy type_sys combformula) + formula_for_combformula ctxt type_sys combformula) fun free_type_literals_for_conjecture type_sys ({ctypes_sorts, ...} : translated_formula) = @@ -445,7 +490,7 @@ max_arity = Int.max (n, max_arity), sub_level = sub_level orelse not top_level}) end) - #> fold (consider_term (top_level andalso s = type_wrapper_name)) ts + #> fold (consider_term (top_level andalso s = type_tag_name)) ts fun consider_formula (AQuant (_, _, phi)) = consider_formula phi | consider_formula (AConn (_, phis)) = fold consider_formula phis | consider_formula (AAtom tm) = consider_term true tm @@ -458,7 +503,7 @@ else SOME (Symtab.empty |> consider_problem problem) fun min_arity_of thy type_sys NONE s = - (if s = "equal" orelse s = type_wrapper_name orelse + (if s = "equal" orelse s = type_tag_name orelse String.isPrefix type_const_prefix s orelse String.isPrefix class_prefix s then 16383 (* large number *) @@ -471,25 +516,29 @@ | NONE => 0 fun full_type_of (ATerm ((s, _), [ty, _])) = - if s = type_wrapper_name then ty else raise Fail "expected type wrapper" - | full_type_of _ = raise Fail "expected type wrapper" + if s = type_tag_name then SOME ty else NONE + | full_type_of _ = NONE fun list_hAPP_rev _ t1 [] = t1 | list_hAPP_rev NONE t1 (t2 :: ts2) = ATerm (`I "hAPP", [list_hAPP_rev NONE t1 ts2, t2]) | list_hAPP_rev (SOME ty) t1 (t2 :: ts2) = - let val ty' = ATerm (`make_fixed_type_const @{type_name fun}, - [full_type_of t2, ty]) in - ATerm (`I "hAPP", [wrap_type ty' (list_hAPP_rev (SOME ty') t1 ts2), t2]) - end + case full_type_of t2 of + SOME ty2 => + let val ty' = ATerm (`make_fixed_type_const @{type_name fun}, + [ty2, ty]) in + ATerm (`I "hAPP", + [tag_with_type ty' (list_hAPP_rev (SOME ty') t1 ts2), t2]) + end + | NONE => list_hAPP_rev NONE t1 (t2 :: ts2) fun repair_applications_in_term thy type_sys const_tab = let fun aux opt_ty (ATerm (name as (s, _), ts)) = - if s = type_wrapper_name then + if s = type_tag_name then case ts of [t1, t2] => ATerm (name, [aux NONE t1, aux (SOME t1) t2]) - | _ => raise Fail "malformed type wrapper" + | _ => raise Fail "malformed type tag" else let val ts = map (aux NONE) ts @@ -513,11 +562,11 @@ | NONE => false fun repair_predicates_in_term const_tab (t as ATerm ((s, _), ts)) = - if s = type_wrapper_name then + if s = type_tag_name then case ts of [_, t' as ATerm ((s', _), _)] => if is_predicate const_tab s' then t' else boolify t - | _ => raise Fail "malformed type wrapper" + | _ => raise Fail "malformed type tag" else t |> not (is_predicate const_tab s) ? boolify @@ -561,11 +610,11 @@ val (fact_names, (conjectures, facts, helper_facts, class_rel_clauses, arity_clauses)) = translate_formulas ctxt type_sys hyp_ts concl_t facts - val fact_lines = map (problem_line_for_fact thy fact_prefix type_sys) facts + val fact_lines = map (problem_line_for_fact ctxt fact_prefix type_sys) facts val helper_lines = - map (problem_line_for_fact thy helper_prefix type_sys) helper_facts + map (problem_line_for_fact ctxt helper_prefix type_sys) helper_facts val conjecture_lines = - map (problem_line_for_conjecture thy type_sys) conjectures + map (problem_line_for_conjecture ctxt type_sys) conjectures val tfree_lines = problem_lines_for_free_types type_sys conjectures val class_rel_lines = map problem_line_for_class_rel_clause class_rel_clauses diff -r 8b634031b2a5 -r eb80538166b6 src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Wed Dec 15 11:26:28 2010 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Wed Dec 15 11:26:28 2010 +0100 @@ -661,19 +661,19 @@ (* Facts containing variables of type "unit" or "bool" or of the form "ALL x. x = A | x = B | x = C" are likely to lead to unsound proofs if types are omitted. *) -fun is_dangerous_term full_types t = - not full_types andalso +fun is_dangerous_term no_dangerous_types t = + not no_dangerous_types andalso let val t = transform_elim_term t in has_bound_or_var_of_type dangerous_types t orelse is_exhaustive_finite t end -fun is_theorem_bad_for_atps full_types thm = +fun is_theorem_bad_for_atps no_dangerous_types thm = let val t = prop_of thm in is_formula_too_complex t orelse exists_type type_has_top_sort t orelse - is_dangerous_term full_types t orelse exists_sledgehammer_const t orelse - exists_low_level_class_const t orelse is_metastrange_theorem thm orelse - is_that_fact thm + is_dangerous_term no_dangerous_types t orelse + exists_sledgehammer_const t orelse exists_low_level_class_const t orelse + is_metastrange_theorem thm orelse is_that_fact thm end fun clasimpset_rules_of ctxt = @@ -704,7 +704,7 @@ (Term.add_vars t [] |> sort_wrt (fst o fst)) |> fst -fun all_facts ctxt reserved full_types +fun all_facts ctxt reserved no_dangerous_types ({intro_bonus, elim_bonus, simp_bonus, ...} : relevance_fudge) add_ths chained_ths = let @@ -754,7 +754,7 @@ pair 1 #> fold (fn th => fn (j, rest) => (j + 1, - if is_theorem_bad_for_atps full_types th andalso + if is_theorem_bad_for_atps no_dangerous_types th andalso not (member Thm.eq_thm add_ths th) then rest else @@ -799,9 +799,9 @@ (* ATP invocation methods setup *) (***************************************************************) -fun relevant_facts ctxt full_types (threshold0, threshold1) max_relevant - is_built_in_const fudge (override as {add, only, ...}) - chained_ths hyp_ts concl_t = +fun relevant_facts ctxt no_dangerous_types (threshold0, threshold1) + max_relevant is_built_in_const fudge + (override as {add, only, ...}) chained_ths hyp_ts concl_t = let val decay = Math.pow ((1.0 - threshold1) / (1.0 - threshold0), 1.0 / Real.fromInt (max_relevant + 1)) @@ -812,7 +812,7 @@ maps (map (fn ((name, loc), th) => ((K name, loc), (true, th))) o fact_from_ref ctxt reserved chained_ths) add else - all_facts ctxt reserved full_types fudge add_ths chained_ths) + all_facts ctxt reserved no_dangerous_types fudge add_ths chained_ths) |> rearrange_facts ctxt (respect_no_atp andalso not only) |> uniquify in diff -r 8b634031b2a5 -r eb80538166b6 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Dec 15 11:26:28 2010 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Dec 15 11:26:28 2010 +0100 @@ -21,6 +21,7 @@ open ATP_Systems open Sledgehammer_Util +open Sledgehammer_ATP_Translate open Sledgehammer_Provers open Sledgehammer_Minimize open Sledgehammer_Run @@ -221,8 +222,15 @@ val overlord = lookup_bool "overlord" val provers = lookup_string "provers" |> space_explode " " |> auto ? single o hd - val type_sys = lookup_string "type_sys" - val full_types = lookup_bool "full_types" + val type_sys = + case (lookup_string "type_sys", lookup_bool "full_types") of + ("tags", full_types) => Tags full_types + | ("preds", full_types) => Preds full_types + | ("const_args", _) => Const_Args + | ("none", _) => No_Types + | ("smart", true) => Tags true + | ("smart", false) => Const_Args + | (type_sys, _) => error ("Unknown type system: " ^ quote type_sys ^ ".") val explicit_apply = lookup_bool "explicit_apply" val relevance_thresholds = lookup_real_pair "relevance_thresholds" val max_relevant = lookup_int_option "max_relevant" @@ -232,8 +240,7 @@ val expect = lookup_string "expect" in {blocking = blocking, debug = debug, verbose = verbose, overlord = overlord, - provers = provers, type_sys = type_sys, full_types = full_types, - explicit_apply = explicit_apply, + provers = provers, type_sys = type_sys, explicit_apply = explicit_apply, relevance_thresholds = relevance_thresholds, max_relevant = max_relevant, isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor, timeout = timeout, expect = expect} diff -r 8b634031b2a5 -r eb80538166b6 src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Wed Dec 15 11:26:28 2010 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Wed Dec 15 11:26:28 2010 +0100 @@ -48,17 +48,17 @@ fun print silent f = if silent then () else Output.urgent_message (f ()) -fun test_facts ({debug, overlord, provers, full_types, type_sys, isar_proof, +fun test_facts ({debug, overlord, provers, type_sys, isar_proof, isar_shrink_factor, ...} : params) silent (prover : prover) explicit_apply timeout i n state facts = let val _ = print silent (fn () => "Testing " ^ n_facts (map fst facts) ^ "...") val params = {blocking = true, debug = debug, verbose = false, overlord = overlord, - provers = provers, full_types = full_types, type_sys = type_sys, - explicit_apply = explicit_apply, relevance_thresholds = (1.01, 1.01), - max_relevant = NONE, isar_proof = isar_proof, - isar_shrink_factor = isar_shrink_factor, timeout = timeout, expect = ""} + provers = provers, type_sys = type_sys, explicit_apply = explicit_apply, + relevance_thresholds = (1.01, 1.01), max_relevant = NONE, + isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor, + timeout = timeout, expect = ""} val facts = facts |> maps (fn (n, ths) => ths |> map (Untranslated_Fact o pair n)) val {goal, ...} = Proof.goal state diff -r 8b634031b2a5 -r eb80538166b6 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Wed Dec 15 11:26:28 2010 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Wed Dec 15 11:26:28 2010 +0100 @@ -12,6 +12,7 @@ type locality = Sledgehammer_Filter.locality type relevance_fudge = Sledgehammer_Filter.relevance_fudge type translated_formula = Sledgehammer_ATP_Translate.translated_formula + type type_system = Sledgehammer_ATP_Translate.type_system type minimize_command = Sledgehammer_ATP_Reconstruct.minimize_command type params = @@ -20,8 +21,7 @@ verbose: bool, overlord: bool, provers: string list, - type_sys: string, - full_types: bool, + type_sys: type_system, explicit_apply: bool, relevance_thresholds: real * real, max_relevant: int option, @@ -204,8 +204,7 @@ verbose: bool, overlord: bool, provers: string list, - type_sys: string, - full_types: bool, + type_sys: type_system, explicit_apply: bool, relevance_thresholds: real * real, max_relevant: int option, @@ -270,22 +269,13 @@ fun run_atp auto atp_name ({exec, required_execs, arguments, has_incomplete_mode, proof_delims, - known_failures, explicit_forall, use_conjecture_for_hypotheses, ...} : atp_config) - ({debug, verbose, overlord, type_sys, full_types, explicit_apply, - isar_proof, isar_shrink_factor, timeout, ...} : params) + known_failures, explicit_forall, use_conjecture_for_hypotheses, ...} + : atp_config) + ({debug, verbose, overlord, type_sys, explicit_apply, isar_proof, + isar_shrink_factor, timeout, ...} : params) minimize_command ({state, goal, subgoal, facts, ...} : prover_problem) = let val ctxt = Proof.context_of state - val type_sys = - case (type_sys, full_types) of - ("tags", _) => Tags full_types - | ("preds", _) => Preds full_types - | ("const_args", _) => Const_Args - | ("overload_args", _) => Overload_Args - | ("none", _) => No_Types - | _ => (if type_sys = "smart" then () - else warning ("Unknown type system: " ^ quote type_sys ^ "."); - if full_types then Tags true else Const_Args) val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal val facts = facts |> map (atp_translated_fact ctxt) val dest_dir = if overlord then getenv "ISABELLE_HOME_USER" diff -r 8b634031b2a5 -r eb80538166b6 src/HOL/Tools/Sledgehammer/sledgehammer_run.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Wed Dec 15 11:26:28 2010 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Wed Dec 15 11:26:28 2010 +0100 @@ -114,7 +114,7 @@ (* FUDGE *) val auto_max_relevant_divisor = 2 -fun run_sledgehammer (params as {blocking, debug, provers, full_types, +fun run_sledgehammer (params as {blocking, debug, provers, type_sys, relevance_thresholds, max_relevant, ...}) auto i (relevance_override as {only, ...}) minimize_command state = @@ -128,14 +128,15 @@ val ctxt = Proof.context_of state val {facts = chained_ths, goal, ...} = Proof.goal state val (_, hyp_ts, concl_t) = strip_subgoal goal i + val no_dangerous_types = types_dangerous_types type_sys val _ = () |> not blocking ? kill_provers val _ = case find_first (not o is_prover_available ctxt) provers of SOME name => error ("No such prover: " ^ name ^ ".") | NONE => () val _ = if auto then () else Output.urgent_message "Sledgehammering..." val (smts, atps) = provers |> List.partition (is_smt_prover ctxt) - fun run_provers label full_types relevance_fudge maybe_translate provers - (res as (success, state)) = + fun run_provers label no_dangerous_types relevance_fudge maybe_translate + provers (res as (success, state)) = if success orelse null provers then res else @@ -150,7 +151,7 @@ val is_built_in_const = is_built_in_const_for_prover ctxt (hd provers) val facts = - relevant_facts ctxt full_types relevance_thresholds + relevant_facts ctxt no_dangerous_types relevance_thresholds max_max_relevant is_built_in_const relevance_fudge relevance_override chained_ths hyp_ts concl_t |> map maybe_translate @@ -180,7 +181,7 @@ |> exists fst |> rpair state end val run_atps = - run_provers "ATP" full_types atp_relevance_fudge + run_provers "ATP" no_dangerous_types atp_relevance_fudge (ATP_Translated_Fact o translate_atp_fact ctxt) atps val run_smts = run_provers "SMT solver" true smt_relevance_fudge Untranslated_Fact smts