--- a/src/HOL/Tools/ATP/atp_reconstruct.ML Tue Jun 07 10:24:16 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_reconstruct.ML Tue Jun 07 11:05:09 2011 +0200
@@ -42,7 +42,6 @@
Proof.context -> type_sys -> int list list -> int
-> (string * locality) list vector -> 'a proof -> string list option
val uses_typed_helpers : int list -> 'a proof -> bool
- val reconstructor_name : reconstructor -> string
val one_line_proof_text : one_line_params -> string
val make_tvar : string -> typ
val make_tfree : Proof.context -> string -> typ
@@ -254,10 +253,10 @@
(** Soft-core proof reconstruction: Metis one-liner **)
(* unfortunate leaking abstraction *)
-fun reconstructor_name Metis = "metis"
- | reconstructor_name Metis_Full_Types = "metis (full_types)"
- | reconstructor_name Metis_No_Types = "metis (no_types)"
- | reconstructor_name (SMT _) = "smt"
+fun name_of_reconstructor Metis = "metis"
+ | name_of_reconstructor Metis_Full_Types = "metis (full_types)"
+ | name_of_reconstructor Metis_No_Types = "metis (no_types)"
+ | name_of_reconstructor (SMT _) = "smt"
fun reconstructor_settings (SMT settings) = settings
| reconstructor_settings _ = ""
@@ -283,7 +282,7 @@
fun reconstructor_command reconstructor i n (ls, ss) =
using_labels ls ^
apply_on_subgoal (reconstructor_settings reconstructor) i n ^
- command_call (reconstructor_name reconstructor) ss
+ command_call (name_of_reconstructor reconstructor) ss
fun minimize_line _ [] = ""
| minimize_line minimize_command ss =
case minimize_command ss of
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML Tue Jun 07 10:24:16 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Tue Jun 07 11:05:09 2011 +0200
@@ -11,10 +11,6 @@
sig
exception METIS of string * string
- val trace : bool Config.T
- val trace_msg : Proof.context -> (unit -> string) -> unit
- val verbose : bool Config.T
- val verbose_warning : Proof.context -> string -> unit
val hol_clause_from_metis :
Proof.context -> int Symtab.table -> (string * term) list -> Metis_Thm.thm
-> term
@@ -38,13 +34,6 @@
exception METIS of string * string
-val trace = Attrib.setup_config_bool @{binding metis_trace} (K false)
-val verbose = Attrib.setup_config_bool @{binding metis_verbose} (K true)
-
-fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ()
-fun verbose_warning ctxt msg =
- if Config.get ctxt verbose then warning ("Metis: " ^ msg) else ()
-
datatype term_or_type = SomeTerm of term | SomeType of typ
fun terms_of [] = []
--- a/src/HOL/Tools/Metis/metis_translate.ML Tue Jun 07 10:24:16 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_translate.ML Tue Jun 07 11:05:09 2011 +0200
@@ -20,6 +20,10 @@
val metis_app_op : string
val metis_type_tag : string
val metis_generated_var_prefix : string
+ val trace : bool Config.T
+ val verbose : bool Config.T
+ val trace_msg : Proof.context -> (unit -> string) -> unit
+ val verbose_warning : Proof.context -> string -> unit
val metis_name_table : ((string * int) * (string * bool)) list
val reveal_old_skolem_terms : (string * term) list -> term -> term
val prepare_metis_problem :
@@ -39,6 +43,13 @@
val metis_type_tag = ":"
val metis_generated_var_prefix = "_"
+val trace = Attrib.setup_config_bool @{binding metis_trace} (K false)
+val verbose = Attrib.setup_config_bool @{binding metis_verbose} (K true)
+
+fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ()
+fun verbose_warning ctxt msg =
+ if Config.get ctxt verbose then warning ("Metis: " ^ msg) else ()
+
val metis_name_table =
[((tptp_equal, 2), (metis_equal, false)),
((tptp_old_equal, 2), (metis_equal, false)),
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Jun 07 10:24:16 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Jun 07 11:05:09 2011 +0200
@@ -10,10 +10,11 @@
sig
type failure = ATP_Proof.failure
type locality = ATP_Translate.locality
- type relevance_fudge = Sledgehammer_Filter.relevance_fudge
type type_sys = ATP_Translate.type_sys
+ type reconstructor = ATP_Reconstruct.reconstructor
type play = ATP_Reconstruct.play
type minimize_command = ATP_Reconstruct.minimize_command
+ type relevance_fudge = Sledgehammer_Filter.relevance_fudge
datatype mode = Auto_Try | Try | Normal | Minimize
@@ -79,6 +80,7 @@
val smt_slice_min_secs : int Config.T
val das_tool : string
val select_smt_solver : string -> Proof.context -> Proof.context
+ val prover_name_for_reconstructor : reconstructor -> string option
val is_metis_prover : string -> bool
val is_atp : theory -> string -> bool
val is_smt_prover : Proof.context -> string -> bool
@@ -137,13 +139,15 @@
(metis_full_typesN, Metis_Full_Types),
(metis_no_typesN, Metis_No_Types)]
+val prover_name_for_reconstructor =
+ AList.find (op =) metis_prover_infos #> try hd
+
val metis_reconstructors = map snd metis_prover_infos
val is_metis_prover = AList.defined (op =) metis_prover_infos
val is_atp = member (op =) o supported_atps
-val select_smt_solver =
- Context.proof_map o SMT_Config.select_solver
+val select_smt_solver = Context.proof_map o SMT_Config.select_solver
fun is_smt_prover ctxt name =
member (op =) (SMT_Solver.available_solvers_of ctxt) name
@@ -531,22 +535,19 @@
(case preplay of
Played (reconstructor, time) =>
if Time.<= (time, metis_minimize_max_time) then
- case AList.find (op =) metis_prover_infos reconstructor of
- metis_name :: _ => metis_name
- | [] => name
+ prover_name_for_reconstructor reconstructor |> the_default name
else
name
| _ => name)
|> minimize_command
-fun repair_monomorph_context debug max_iters max_new_instances =
- Config.put Monomorph.verbose debug
- #> Config.put Monomorph.max_rounds max_iters
+fun repair_monomorph_context max_iters max_new_instances =
+ Config.put Monomorph.max_rounds max_iters
#> Config.put Monomorph.max_new_instances max_new_instances
#> Config.put Monomorph.keep_partial_instances false
fun repair_smt_monomorph_context debug max_mono_iters max_mono_instances =
- Config.put SMT_Config.verbose debug
+ (not debug ? Config.put SMT_Config.verbose false)
#> Config.put SMT_Config.monomorph_limit max_mono_iters
#> Config.put SMT_Config.monomorph_instances max_mono_instances
#> Config.put SMT_Config.monomorph_full false
@@ -603,7 +604,7 @@
fun monomorphize_facts facts =
let
val ctxt =
- ctxt |> repair_monomorph_context debug max_mono_iters
+ ctxt |> repair_monomorph_context max_mono_iters
max_new_mono_instances
(* pseudo-theorem involving the same constants as the subgoal *)
val subgoal_th =
@@ -876,14 +877,14 @@
let
val max_slices = if slicing then Config.get ctxt smt_max_slices else 1
val repair_context =
- select_smt_solver name
- #> (if overlord then
- Config.put SMT_Config.debug_files
- (overlord_file_location_for_prover name
- |> (fn (path, name) => path ^ "/" ^ name))
- else
- I)
- #> Config.put SMT_Config.infer_triggers (Config.get ctxt smt_triggers)
+ select_smt_solver name
+ #> (if overlord then
+ Config.put SMT_Config.debug_files
+ (overlord_file_location_for_prover name
+ |> (fn (path, name) => path ^ "/" ^ name))
+ else
+ I)
+ #> Config.put SMT_Config.infer_triggers (Config.get ctxt smt_triggers)
val state = state |> Proof.map_context repair_context
fun do_slice timeout slice outcome0 time_so_far facts =
let
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Tue Jun 07 10:24:16 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Tue Jun 07 11:05:09 2011 +0200
@@ -102,7 +102,8 @@
(case preplay of
Played (reconstructor, timeout) =>
if can_min_fast_enough (Time.toMilliseconds timeout) then
- (true, reconstructor_name reconstructor)
+ (true, prover_name_for_reconstructor reconstructor
+ |> the_default name)
else
(prover_fast_enough, name)
| _ => (prover_fast_enough, name),
--- a/src/HOL/Tools/monomorph.ML Tue Jun 07 10:24:16 2011 +0200
+++ b/src/HOL/Tools/monomorph.ML Tue Jun 07 11:05:09 2011 +0200
@@ -35,7 +35,6 @@
typ list Symtab.table
(* configuration options *)
- val verbose: bool Config.T
val max_rounds: int Config.T
val max_new_instances: int Config.T
val keep_partial_instances: bool Config.T
@@ -64,7 +63,6 @@
(* configuration options *)
-val verbose = Attrib.setup_config_bool @{binding monomorph_verbose} (K true)
val max_rounds = Attrib.setup_config_int @{binding monomorph_max_rounds} (K 5)
val max_new_instances =
Attrib.setup_config_int @{binding monomorph_max_new_instances} (K 300)