--- 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 =
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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}
--- 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
--- 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"
--- 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