# HG changeset patch # User blanchet # Date 1307437509 -7200 # Node ID 9d717505595f24b20bb0fe0c4e4799ba23297c9a # Parent 2749c357f865f2a74b687f8f9828956d0b433ad7# Parent dabf6e3112136174a22851b1495249b4d3101b3f merged diff -r dabf6e311213 -r 9d717505595f src/HOL/Tools/ATP/atp_reconstruct.ML --- 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 diff -r dabf6e311213 -r 9d717505595f src/HOL/Tools/Metis/metis_reconstruct.ML --- 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 [] = [] diff -r dabf6e311213 -r 9d717505595f src/HOL/Tools/Metis/metis_translate.ML --- 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)), diff -r dabf6e311213 -r 9d717505595f src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- 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 diff -r dabf6e311213 -r 9d717505595f src/HOL/Tools/Sledgehammer/sledgehammer_run.ML --- 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), diff -r dabf6e311213 -r 9d717505595f src/HOL/Tools/monomorph.ML --- 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)