# HG changeset patch # User blanchet # Date 1304267845 -7200 # Node ID 2552c09b1a72ec1c4e148f057c612de082ef962e # Parent 1eaf4d437d4c02adc67bd4a6641db7cf4d1cbcb5 implement the new ATP type system in Sledgehammer diff -r 1eaf4d437d4c -r 2552c09b1a72 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Sun May 01 18:37:25 2011 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Sun May 01 18:37:25 2011 +0200 @@ -377,8 +377,7 @@ 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.type_system_types_dangerous_types type_sys + val half_sound = Sledgehammer_Provers.is_rich_type_sys_half_sound type_sys val time_limit = (case hard_timeout of NONE => I @@ -388,7 +387,7 @@ time_isa) = time_limit (Mirabelle.cpu_time (fn () => let val facts = - Sledgehammer_Filter.relevant_facts ctxt no_dangerous_types + Sledgehammer_Filter.relevant_facts ctxt half_sound relevance_thresholds (the_default default_max_relevant max_relevant) is_built_in_const relevance_fudge relevance_override chained_ths hyp_ts concl_t diff -r 1eaf4d437d4c -r 2552c09b1a72 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Sun May 01 18:37:25 2011 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Sun May 01 18:37:25 2011 +0200 @@ -125,10 +125,10 @@ val relevance_override = {add = [], del = [], only = false} val subgoal = 1 val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal subgoal - val no_dangerous_types = - Sledgehammer_ATP_Translate.type_system_types_dangerous_types type_sys + val half_sound = + Sledgehammer_Provers.is_rich_type_sys_half_sound type_sys val facts = - Sledgehammer_Filter.relevant_facts ctxt no_dangerous_types + Sledgehammer_Filter.relevant_facts ctxt half_sound relevance_thresholds (the_default default_max_relevant max_relevant) is_built_in_const relevance_fudge relevance_override facts hyp_ts concl_t diff -r 1eaf4d437d4c -r 2552c09b1a72 src/HOL/Tools/ATP/atp_systems.ML --- a/src/HOL/Tools/ATP/atp_systems.ML Sun May 01 18:37:25 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_systems.ML Sun May 01 18:37:25 2011 +0200 @@ -11,12 +11,13 @@ type formula_kind = ATP_Problem.formula_kind type failure = ATP_Proof.failure - datatype type_level = Level_All | Level_Some | Level_None + datatype type_level = Sound | Half_Sound | Unsound datatype type_system = Many_Typed | Mangled of type_level | Args of bool * type_level | - Tags of bool * type_level + Tags of bool * type_level | + No_Types type atp_config = {exec : string * string, @@ -32,6 +33,7 @@ datatype e_weight_method = E_Slices | E_Auto | E_Fun_Weight | E_Sym_Offset_Weight + val level_of_type_sys : type_system -> type_level (* for experimentation purposes -- do not use in production code *) val e_weight_method : e_weight_method Unsynchronized.ref val e_default_fun_weight : real Unsynchronized.ref @@ -40,7 +42,7 @@ val e_default_sym_offs_weight : real Unsynchronized.ref val e_sym_offs_weight_base : real Unsynchronized.ref val e_sym_offs_weight_span : real Unsynchronized.ref - + (* end *) val eN : string val spassN : string val vampireN : string @@ -69,12 +71,19 @@ (* ATP configuration *) -datatype type_level = Level_All | Level_Some | Level_None +datatype type_level = Sound | Half_Sound | Unsound datatype type_system = Many_Typed | Mangled of type_level | Args of bool * type_level | - Tags of bool * type_level + Tags of bool * type_level | + No_Types + +fun level_of_type_sys Many_Typed = Sound + | level_of_type_sys (Mangled level) = level + | level_of_type_sys (Args (_, level)) = level + | level_of_type_sys (Tags (_, level)) = level + | level_of_type_sys No_Types = Unsound type atp_config = {exec : string * string, diff -r 1eaf4d437d4c -r 2552c09b1a72 src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Sun May 01 18:37:25 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Sun May 01 18:37:25 2011 +0200 @@ -45,6 +45,7 @@ open ATP_Problem open ATP_Proof +open ATP_Systems open Metis_Translate open Sledgehammer_Util open Sledgehammer_Filter @@ -193,7 +194,7 @@ | using_labels ls = "using " ^ space_implode " " (map string_for_label ls) ^ " " fun metis_name type_sys = - if type_system_types_dangerous_types type_sys then "metisFT" else "metis" + if level_of_type_sys type_sys = Unsound then "metis" else "metisFT" fun metis_call type_sys ss = command_call (metis_name type_sys) ss fun metis_command type_sys i n (ls, ss) = using_labels ls ^ apply_on_subgoal "" i n ^ metis_call type_sys ss diff -r 1eaf4d437d4c -r 2552c09b1a72 src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Sun May 01 18:37:25 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Sun May 01 18:37:25 2011 +0200 @@ -10,15 +10,9 @@ sig type 'a fo_term = 'a ATP_Problem.fo_term type 'a problem = 'a ATP_Problem.problem + type type_system = ATP_Systems.type_system type translated_formula - datatype type_system = - Many_Typed | - Mangled of bool | - Args of bool | - Tags of bool | - No_Types - val readable_names : bool Unsynchronized.ref val fact_prefix : string val conjecture_prefix : string @@ -26,8 +20,6 @@ val explicit_app_base : string val type_pred_base : string val tff_type_prefix : string - val is_type_system_sound : type_system -> bool - val type_system_types_dangerous_types : type_system -> bool val num_atp_type_args : theory -> type_system -> string -> int val unmangled_const : string -> string * string fo_term list val translate_atp_fact : @@ -45,6 +37,7 @@ struct open ATP_Problem +open ATP_Systems open Metis_Translate open Sledgehammer_Util @@ -98,29 +91,10 @@ fun fact_lift f ({combformula, ...} : translated_formula) = f combformula -datatype type_system = - Many_Typed | - Mangled of bool | - Args of bool | - Tags of bool | - No_Types - -fun is_type_system_sound Many_Typed = true - | is_type_system_sound (Mangled full_types) = full_types - | is_type_system_sound (Args full_types) = full_types - | is_type_system_sound (Tags full_types) = full_types - | is_type_system_sound No_Types = false - -fun type_system_types_dangerous_types (Tags _) = true - | type_system_types_dangerous_types type_sys = is_type_system_sound type_sys - -fun type_system_introduces_type_preds (Mangled true) = true - | type_system_introduces_type_preds (Args true) = true - | type_system_introduces_type_preds _ = false - -fun type_system_declares_sym_types Many_Typed = true - | type_system_declares_sym_types type_sys = - type_system_introduces_type_preds type_sys +fun type_sys_declares_sym_types Many_Typed = true + | type_sys_declares_sym_types (Mangled level) = level <> Unsound + | type_sys_declares_sym_types (Args (_, level)) = level <> Unsound + | type_sys_declares_sym_types _ = false val boring_consts = [explicit_app_base, @{const_name Metis.fequal}] @@ -130,14 +104,15 @@ case type_sys of Many_Typed => false | Mangled _ => false + | Tags (_, Sound) => true | No_Types => true - | Tags true => true | _ => member (op =) boring_consts s) datatype type_arg_policy = No_Type_Args | Mangled_Types | Explicit_Type_Args fun general_type_arg_policy Many_Typed = Mangled_Types | general_type_arg_policy (Mangled _) = Mangled_Types + | general_type_arg_policy No_Types = No_Type_Args | general_type_arg_policy _ = Explicit_Type_Args fun type_arg_policy type_sys s = @@ -542,8 +517,8 @@ let val thy = Proof_Context.theory_of ctxt val unmangled_s = mangled_s |> unmangled_const_name - fun dub_and_inst c needs_full_types (th, j) = - ((c ^ "_" ^ string_of_int j ^ (if needs_full_types then "ft" else ""), + fun dub_and_inst c needs_some_types (th, j) = + ((c ^ "_" ^ string_of_int j ^ (if needs_some_types then "T" else ""), false), let val t = th |> prop_of in t |> (general_type_arg_policy type_sys = Mangled_Types andalso @@ -556,15 +531,15 @@ map_filter (make_fact ctxt false eq_as_iff false) in metis_helpers - |> maps (fn (metis_s, (needs_full_types, ths)) => + |> maps (fn (metis_s, (needs_some_types, ths)) => if metis_s <> unmangled_s orelse - (needs_full_types andalso - not (type_system_types_dangerous_types type_sys)) then + (needs_some_types andalso + level_of_type_sys type_sys = Unsound) then [] else ths ~~ (1 upto length ths) - |> map (dub_and_inst mangled_s needs_full_types) - |> make_facts (not needs_full_types)) + |> map (dub_and_inst mangled_s needs_some_types) + |> make_facts (not needs_some_types)) end | NONE => [] fun helper_facts_for_sym_table ctxt type_sys sym_tab = @@ -632,10 +607,20 @@ | [] => true end -fun should_tag_with_type ctxt (Tags full_types) T = - full_types orelse is_type_dangerous ctxt T +fun should_encode_type _ Sound _ = true + | should_encode_type ctxt Half_Sound T = is_type_dangerous ctxt T + | should_encode_type _ Unsound _ = false + +fun should_tag_with_type ctxt (Tags (_, level)) T = + should_encode_type ctxt level T | should_tag_with_type _ _ _ = false +fun should_predicate_on_type ctxt (Mangled level) T = + should_encode_type ctxt level T + | should_predicate_on_type ctxt (Args (_, level)) T = + should_encode_type ctxt level T + | should_predicate_on_type _ _ _ = false + fun type_pred_combatom type_sys T tm = CombApp (CombConst (`make_fixed_const type_pred_base, T --> @{typ bool}, [T]), tm) @@ -664,7 +649,7 @@ val do_bound_type = if type_sys = Many_Typed then SOME o mangled_type_name else K NONE fun do_out_of_bound_type (s, T) = - if type_system_introduces_type_preds type_sys then + if should_predicate_on_type ctxt type_sys T then type_pred_combatom type_sys T (CombVar (s, T)) |> do_formula |> SOME else @@ -749,8 +734,13 @@ fun add_combterm_syms_to_decl_table type_sys repaired_sym_tab = let fun declare_sym (decl as (_, _, T, _, _)) decls = - if exists (curry Type.raw_instance T o #3) decls then decls - else decl :: filter_out ((fn T' => Type.raw_instance (T', T)) o #3) decls + case type_sys of + Tags (false, Sound) => + if exists (curry Type.raw_instance T o #3) decls then + decls + else + decl :: filter_out ((fn T' => Type.raw_instance (T', T)) o #3) decls + | _ => insert (op =) decl decls fun do_term tm = let val (head, args) = strip_combterm_comb tm in (case head of @@ -770,7 +760,7 @@ fact_lift (formula_fold (add_combterm_syms_to_decl_table type_sys repaired_sym_tab)) fun sym_decl_table_for_facts type_sys repaired_sym_tab facts = - Symtab.empty |> type_system_declares_sym_types type_sys + Symtab.empty |> type_sys_declares_sym_types type_sys ? fold (add_fact_syms_to_decl_table type_sys repaired_sym_tab) facts @@ -779,47 +769,59 @@ n_ary_strip_type (n - 1) ran_T |>> cons dom_T | n_ary_strip_type _ _ = raise Fail "unexpected non-function" -fun problem_line_for_sym_decl ctxt type_sys need_bound_types s j - (s', T_args, T, pred_sym, ary) = +fun result_type_of_decl (_, _, T, _, ary) = n_ary_strip_type ary T |> snd + +fun decl_line_for_sym_decl s (s', _, T, pred_sym, ary) = + let val (arg_Ts, res_T) = n_ary_strip_type ary T in + Decl (sym_decl_prefix ^ ascii_of s, (s, s'), + map mangled_type_name arg_Ts, + if pred_sym then `I tptp_tff_bool_type else mangled_type_name res_T) + end + +fun formula_line_for_sym_decl ctxt type_sys n s j (s', T_args, T, _, ary) = + let + val (arg_Ts, res_T) = n_ary_strip_type ary T + val bound_names = + 1 upto length arg_Ts |> map (`I o make_bound_var o string_of_int) + val bound_tms = + bound_names ~~ arg_Ts |> map (fn (name, T) => CombConst (name, T, [])) + val bound_Ts = + arg_Ts |> map (if n > 1 then SOME else K NONE) + val freshener = + case type_sys of Args _ => string_of_int j ^ "_" | _ => "" + in + Formula (sym_decl_prefix ^ freshener ^ "_" ^ ascii_of s, Axiom, + CombConst ((s, s'), T, T_args) + |> fold (curry (CombApp o swap)) bound_tms + |> type_pred_combatom type_sys res_T + |> mk_aquant AForall (bound_names ~~ bound_Ts) + |> formula_from_combformula ctxt type_sys, + NONE, NONE) + end + +fun problem_lines_for_sym_decls ctxt type_sys (s, decls) = if type_sys = Many_Typed then - let val (arg_Ts, res_T) = n_ary_strip_type ary T in - Decl (sym_decl_prefix ^ ascii_of s, (s, s'), - map mangled_type_name arg_Ts, - if pred_sym then `I tptp_tff_bool_type else mangled_type_name res_T) - end + map (decl_line_for_sym_decl s) decls else let - val (arg_Ts, res_T) = n_ary_strip_type ary T - val bound_names = - 1 upto length arg_Ts |> map (`I o make_bound_var o string_of_int) - val bound_tms = - bound_names ~~ arg_Ts |> map (fn (name, T) => CombConst (name, T, [])) - val bound_Ts = arg_Ts |> map (if need_bound_types then SOME else K NONE) - val freshener = - case type_sys of Args _ => string_of_int j ^ "_" | _ => "" + val decls = + case decls of + decl :: (decls' as _ :: _) => + if forall (curry (op =) (result_type_of_decl decl) + o result_type_of_decl) decls' then + [decl] + else + decls + | _ => decls + val n = length decls + val decls = + decls |> filter (should_predicate_on_type ctxt type_sys + o result_type_of_decl) in - Formula (sym_decl_prefix ^ freshener ^ "_" ^ ascii_of s, Axiom, - CombConst ((s, s'), T, T_args) - |> fold (curry (CombApp o swap)) bound_tms - |> type_pred_combatom type_sys res_T - |> mk_aquant AForall (bound_names ~~ bound_Ts) - |> formula_from_combformula ctxt type_sys, - NONE, NONE) + map2 (formula_line_for_sym_decl ctxt type_sys n s) + (0 upto length decls - 1) decls end -fun problem_lines_for_sym_decls ctxt type_sys (s, decls) = - let - val n = length decls - fun result_type_of_decl (_, _, T, _, ary) = n_ary_strip_type ary T |> snd - val need_bound_types = - case decls of - decl :: (decls as _ :: _) => - exists (curry (op <>) (result_type_of_decl decl) - o result_type_of_decl) decls - | _ => false - in - map2 (problem_line_for_sym_decl ctxt type_sys need_bound_types s) - (0 upto n - 1) decls - end + fun problem_lines_for_sym_decl_table ctxt type_sys sym_decl_tab = Symtab.fold_rev (append o problem_lines_for_sym_decls ctxt type_sys) sym_decl_tab [] @@ -880,8 +882,9 @@ (aritiesN, map formula_line_for_arity_clause arity_clauses), (helpersN, map (formula_line_for_fact ctxt helper_prefix type_sys) (0 upto length helpers - 1 ~~ helpers) - |> (if type_sys = Tags false then cons (ti_ti_helper_fact ()) - else I)), + |> (case type_sys of + Tags (_, Half_Sound) => cons (ti_ti_helper_fact ()) + | _ => I)), (conjsN, map (formula_line_for_conjecture ctxt type_sys) conjs), (free_typesN, formula_lines_for_free_types type_sys (facts @ conjs))] val problem = diff -r 1eaf4d437d4c -r 2552c09b1a72 src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Sun May 01 18:37:25 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Sun May 01 18:37:25 2011 +0200 @@ -777,19 +777,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 no_dangerous_types t = - not no_dangerous_types andalso +fun is_dangerous_term half_sound t = + not half_sound 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 no_dangerous_types thm = +fun is_theorem_bad_for_atps half_sound 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 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 + is_dangerous_term half_sound 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 = @@ -800,7 +800,7 @@ val simps = ctxt |> simpset_of |> dest_ss |> #simps |> map snd in (mk_fact_table I intros, mk_fact_table I elims, mk_fact_table I simps) end -fun all_facts ctxt reserved really_all no_dangerous_types +fun all_facts ctxt reserved really_all half_sound ({intro_bonus, elim_bonus, simp_bonus, ...} : relevance_fudge) add_ths chained_ths = let @@ -846,7 +846,7 @@ pair 1 #> fold (fn th => fn (j, rest) => (j + 1, - if is_theorem_bad_for_atps no_dangerous_types th andalso + if is_theorem_bad_for_atps half_sound th andalso not (member Thm.eq_thm add_ths th) then rest else @@ -890,9 +890,9 @@ fun external_frees t = [] |> Term.add_frees t |> filter_out (can Name.dest_internal o fst) -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 = +fun relevant_facts ctxt half_sound (threshold0, threshold1) max_relevant + is_built_in_const fudge (override as {add, only, ...}) + chained_ths hyp_ts concl_t = let val thy = Proof_Context.theory_of ctxt val decay = Math.pow ((1.0 - threshold1) / (1.0 - threshold0), @@ -908,8 +908,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 false no_dangerous_types fudge add_ths - chained_ths) + all_facts ctxt reserved false half_sound fudge add_ths chained_ths) |> instantiate_inducts ? maps (instantiate_if_induct_rule ctxt ind_stmt ind_stmt_xs) |> rearrange_facts ctxt (respect_no_atp andalso not only) diff -r 1eaf4d437d4c -r 2552c09b1a72 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Sun May 01 18:37:25 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Sun May 01 18:37:25 2011 +0200 @@ -82,7 +82,6 @@ ("type_sys", "smart"), ("relevance_thresholds", "0.45 0.85"), ("max_relevant", "smart"), - ("monomorphize", "false"), ("monomorphize_limit", "4"), ("explicit_apply", "false"), ("isar_proof", "false"), @@ -98,7 +97,6 @@ ("quiet", "verbose"), ("no_overlord", "overlord"), ("non_blocking", "blocking"), - ("dont_monomorphize", "monomorphize"), ("partial_types", "full_types"), ("implicit_apply", "explicit_apply"), ("no_isar_proof", "isar_proof"), @@ -235,21 +233,28 @@ val blocking = auto orelse debug orelse lookup_bool "blocking" val provers = lookup_string "provers" |> space_explode " " |> auto ? single o hd + val type_sys = lookup_string "type_sys" val type_sys = - case (lookup_string "type_sys", lookup_bool "full_types") of - ("many_typed", _) => Many_Typed - | ("mangled", full_types) => Mangled full_types - | ("args", full_types) => Args full_types - | ("tags", full_types) => Tags full_types - | ("none", false) => No_Types - | (type_sys, full_types) => - if member (op =) ["none", "smart"] type_sys then - if full_types then Tags true else Args false - else - error ("Unknown type system: " ^ quote type_sys ^ ".") + (case try (unprefix "mono_") type_sys of + SOME s => (true, s) + | NONE => (false, type_sys)) + ||> (fn s => case try (unsuffix " **") s of + SOME s => (Unsound, s) + | NONE => case try (unsuffix " *") s of + SOME s => (Half_Sound, s) + | NONE => (Sound, s)) + |> (fn (mono, (level, core)) => + case (core, (mono, level)) of + ("many_typed", (false, Sound)) => Dumb_Type_Sys Many_Typed + | ("mangled", (false, level)) => Dumb_Type_Sys (Mangled level) + | ("args", extra) => Dumb_Type_Sys (Args extra) + | ("tags", extra) => Dumb_Type_Sys (Tags extra) + | ("none", (false, Sound)) => Dumb_Type_Sys No_Types + | ("smart", (false, Sound)) => + Smart_Type_Sys (lookup_bool "full_types") + | _ => error ("Unknown type system: " ^ quote type_sys ^ ".")) val relevance_thresholds = lookup_real_pair "relevance_thresholds" val max_relevant = lookup_int_option "max_relevant" - val monomorphize = lookup_bool "monomorphize" val monomorphize_limit = lookup_int "monomorphize_limit" val explicit_apply = lookup_bool "explicit_apply" val isar_proof = lookup_bool "isar_proof" @@ -260,11 +265,10 @@ in {debug = debug, verbose = verbose, overlord = overlord, blocking = blocking, provers = provers, relevance_thresholds = relevance_thresholds, - max_relevant = max_relevant, monomorphize = monomorphize, - monomorphize_limit = monomorphize_limit, type_sys = type_sys, - explicit_apply = explicit_apply, isar_proof = isar_proof, - isar_shrink_factor = isar_shrink_factor, slicing = slicing, - timeout = timeout, expect = expect} + max_relevant = max_relevant, monomorphize_limit = monomorphize_limit, + type_sys = type_sys, explicit_apply = explicit_apply, + isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor, + slicing = slicing, timeout = timeout, expect = expect} end fun get_params auto ctxt = extract_params auto (default_raw_params ctxt) diff -r 1eaf4d437d4c -r 2552c09b1a72 src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Sun May 01 18:37:25 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Sun May 01 18:37:25 2011 +0200 @@ -65,9 +65,9 @@ {debug = debug, verbose = verbose, overlord = overlord, blocking = true, provers = provers, type_sys = type_sys, explicit_apply = explicit_apply, relevance_thresholds = (1.01, 1.01), max_relevant = NONE, - monomorphize = false, monomorphize_limit = monomorphize_limit, - isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor, - slicing = false, timeout = timeout, expect = ""} + monomorphize_limit = monomorphize_limit, isar_proof = isar_proof, + isar_shrink_factor = isar_shrink_factor, slicing = false, + timeout = timeout, expect = ""} val facts = facts |> maps (fn (n, ths) => ths |> map (Untranslated_Fact o pair n)) val problem = diff -r 1eaf4d437d4c -r 2552c09b1a72 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Sun May 01 18:37:25 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Sun May 01 18:37:25 2011 +0200 @@ -15,16 +15,19 @@ type type_system = Sledgehammer_ATP_Translate.type_system type minimize_command = Sledgehammer_ATP_Reconstruct.minimize_command + datatype rich_type_system = + Dumb_Type_Sys of type_system | + Smart_Type_Sys of bool + type params = {debug: bool, verbose: bool, overlord: bool, blocking: bool, provers: string list, - type_sys: type_system, + type_sys: rich_type_system, relevance_thresholds: real * real, max_relevant: int option, - monomorphize: bool, monomorphize_limit: int, explicit_apply: bool, isar_proof: bool, @@ -35,8 +38,6 @@ datatype prover_fact = Untranslated_Fact of (string * locality) * thm | - ATP_Translated_Fact of - translated_formula option * ((string * locality) * thm) | SMT_Weighted_Fact of (string * locality) * (int option * thm) type prover_problem = @@ -85,6 +86,7 @@ val weight_smt_fact : theory -> int -> ((string * locality) * thm) * int -> (string * locality) * (int option * thm) + val is_rich_type_sys_half_sound : rich_type_system -> bool val untranslated_fact : prover_fact -> (string * locality) * thm val smt_weighted_fact : theory -> int -> prover_fact * int @@ -227,16 +229,19 @@ (** problems, results, ATPs, etc. **) +datatype rich_type_system = + Dumb_Type_Sys of type_system | + Smart_Type_Sys of bool + type params = {debug: bool, verbose: bool, overlord: bool, blocking: bool, provers: string list, - type_sys: type_system, + type_sys: rich_type_system, relevance_thresholds: real * real, max_relevant: int option, - monomorphize: bool, monomorphize_limit: int, explicit_apply: bool, isar_proof: bool, @@ -247,8 +252,6 @@ datatype prover_fact = Untranslated_Fact of (string * locality) * thm | - ATP_Translated_Fact of - translated_formula option * ((string * locality) * thm) | SMT_Weighted_Fact of (string * locality) * (int option * thm) type prover_problem = @@ -310,11 +313,13 @@ fun weight_smt_fact thy num_facts ((info, th), j) = (info, (smt_fact_weight j num_facts, th |> Thm.transfer thy)) +fun is_rich_type_sys_half_sound (Dumb_Type_Sys type_sys) = + level_of_type_sys type_sys <> Unsound + | is_rich_type_sys_half_sound (Smart_Type_Sys full_types) = full_types + fun untranslated_fact (Untranslated_Fact p) = p - | untranslated_fact (ATP_Translated_Fact (_, p)) = p | untranslated_fact (SMT_Weighted_Fact (info, (_, th))) = (info, th) -fun atp_translated_fact _ (ATP_Translated_Fact p) = p - | atp_translated_fact ctxt fact = +fun atp_translated_fact ctxt fact = translate_atp_fact ctxt false (untranslated_fact fact) fun smt_weighted_fact _ _ (SMT_Weighted_Fact p, _) = p | smt_weighted_fact thy num_facts (fact, j) = @@ -334,21 +339,41 @@ them each time. *) val atp_important_message_keep_factor = 0.1 -fun must_monomorphize Many_Typed = true - | must_monomorphize (Mangled _) = true - | must_monomorphize _ = false +fun type_sys_monomorphizes Many_Typed = true + | type_sys_monomorphizes (Mangled _) = true + | type_sys_monomorphizes (Args (mono, _)) = mono + | type_sys_monomorphizes (Tags (mono, _)) = mono + | type_sys_monomorphizes No_Types = false + +val fallback_best_type_systems = [Many_Typed, Args (false, Unsound)] + +fun adjust_dumb_type_sys formats Many_Typed = + if member (op =) formats Tff then (Tff, Many_Typed) + else (Fof, Mangled Sound) + | adjust_dumb_type_sys formats type_sys = + if member (op =) formats Fof then (Fof, type_sys) + else (Tff, Many_Typed) +fun determine_format_and_type_sys _ formats (Dumb_Type_Sys type_sys) = + adjust_dumb_type_sys formats type_sys + | determine_format_and_type_sys best_type_systems formats + (Smart_Type_Sys full_types) = + best_type_systems @ fallback_best_type_systems + |> filter (fn type_sys => (level_of_type_sys type_sys = Sound) = full_types) + |> hd |> adjust_dumb_type_sys formats fun run_atp auto name ({exec, required_execs, arguments, proof_delims, known_failures, - hypothesis_kind, best_slices, ...} : atp_config) - ({debug, verbose, overlord, type_sys, max_relevant, monomorphize, - monomorphize_limit, explicit_apply, isar_proof, isar_shrink_factor, - slicing, timeout, ...} : params) + hypothesis_kind, formats, best_slices, best_type_systems, ...} + : atp_config) + ({debug, verbose, overlord, type_sys, max_relevant, monomorphize_limit, + explicit_apply, isar_proof, isar_shrink_factor, slicing, timeout, ...} + : params) minimize_command ({state, goal, subgoal, facts, ...} : prover_problem) = let val thy = Proof.theory_of state val ctxt = Proof.context_of state - val format = if type_sys = Many_Typed then Tff else Fof + val (format, type_sys) = + determine_format_and_type_sys best_type_systems formats type_sys val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal val (dest_dir, problem_prefix) = if overlord then overlord_file_location_for_prover name @@ -418,8 +443,7 @@ |> not (null blacklist) ? filter_out (member (op =) blacklist o fst o untranslated_fact) - |> (monomorphize orelse must_monomorphize type_sys) - ? monomorphize_facts + |> type_sys_monomorphizes type_sys ? monomorphize_facts |> map (atp_translated_fact ctxt) val real_ms = Real.fromInt o Time.toMilliseconds val slice_timeout = @@ -479,7 +503,7 @@ (conjecture_shape, fact_names) (* don't bother repairing *) val outcome = case outcome of - NONE => if not (is_type_system_sound type_sys) andalso + NONE => if level_of_type_sys type_sys <> Sound andalso is_unsound_proof conjecture_shape facts_offset fact_names atp_proof then SOME UnsoundProof diff -r 1eaf4d437d4c -r 2552c09b1a72 src/HOL/Tools/Sledgehammer/sledgehammer_run.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Sun May 01 18:37:25 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Sun May 01 18:37:25 2011 +0200 @@ -23,6 +23,7 @@ structure Sledgehammer_Run : SLEDGEHAMMER_RUN = struct +open ATP_Systems open Sledgehammer_Util open Sledgehammer_Filter open Sledgehammer_ATP_Translate @@ -162,12 +163,11 @@ fun dest_SMT_Weighted_Fact (SMT_Weighted_Fact p) = p | dest_SMT_Weighted_Fact _ = raise Fail "dest_SMT_Weighted_Fact" -(* FUDGE *) -val auto_max_relevant_divisor = 2 +val auto_max_relevant_divisor = 2 (* FUDGE *) -fun run_sledgehammer (params as {debug, blocking, provers, monomorphize, - type_sys, relevance_thresholds, max_relevant, - slicing, timeout, ...}) +fun run_sledgehammer (params as {debug, blocking, provers, type_sys, + relevance_thresholds, max_relevant, slicing, + timeout, ...}) auto i (relevance_override as {only, ...}) minimize_command state = if null provers then error "No prover is set." @@ -183,7 +183,7 @@ val thy = Proof_Context.theory_of ctxt val {facts = chained_ths, goal, ...} = Proof.goal state val (_, hyp_ts, concl_t) = strip_subgoal goal i - val no_dangerous_types = type_system_types_dangerous_types type_sys + val half_sound = is_rich_type_sys_half_sound type_sys val _ = () |> not blocking ? kill_provers val _ = case find_first (not o is_prover_supported ctxt) provers of SOME name => error ("No such prover: " ^ name ^ ".") @@ -212,7 +212,7 @@ |> (if blocking then smart_par_list_map else map) (launch problem) |> exists fst |> rpair state end - fun get_facts label no_dangerous_types relevance_fudge provers = + fun get_facts label half_sound relevance_fudge provers = let val max_max_relevant = case max_relevant of @@ -225,9 +225,9 @@ val is_built_in_const = is_built_in_const_for_prover ctxt (hd provers) in - 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 + relevant_facts ctxt half_sound relevance_thresholds max_max_relevant + is_built_in_const relevance_fudge relevance_override + chained_ths hyp_ts concl_t |> tap (fn facts => if debug then label ^ plural_s (length provers) ^ ": " ^ @@ -246,12 +246,8 @@ accum else launch_provers state - (get_facts "ATP" no_dangerous_types atp_relevance_fudge o K atps) - (if monomorphize then - K (Untranslated_Fact o fst) - else - ATP_Translated_Fact oo K (translate_atp_fact ctxt false o fst)) - (K (K NONE)) atps + (get_facts "ATP" half_sound atp_relevance_fudge o K atps) + (K (Untranslated_Fact o fst)) (K (K NONE)) atps fun launch_smts accum = if null smts then accum diff -r 1eaf4d437d4c -r 2552c09b1a72 src/HOL/ex/sledgehammer_tactics.ML --- a/src/HOL/ex/sledgehammer_tactics.ML Sun May 01 18:37:25 2011 +0200 +++ b/src/HOL/ex/sledgehammer_tactics.ML Sun May 01 18:37:25 2011 +0200 @@ -32,11 +32,9 @@ 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.type_system_types_dangerous_types type_sys + val half_sound = Sledgehammer_Provers.is_rich_type_sys_half_sound type_sys val facts = - Sledgehammer_Filter.relevant_facts ctxt no_dangerous_types - relevance_thresholds + Sledgehammer_Filter.relevant_facts ctxt half_sound 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 =