--- 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
--- 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
--- 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,
--- 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
--- 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 =
--- 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)
--- 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)
--- 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 =
--- 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
--- 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
--- 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 =