# HG changeset patch # User blanchet # Date 1272042769 -7200 # Node ID f32c567dbcaa1b06c0aa7e868dd44865f7173bc5 # Parent b3dce4c715d0c804a8d65d1964d8f2400bd2a1b3 remove some bloat diff -r b3dce4c715d0 -r f32c567dbcaa src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML Fri Apr 23 18:11:41 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML Fri Apr 23 19:12:49 2010 +0200 @@ -8,11 +8,10 @@ signature SLEDGEHAMMER_FACT_MINIMIZER = sig type params = ATP_Manager.params - type prover = ATP_Manager.prover type prover_result = ATP_Manager.prover_result val minimize_theorems : - params -> prover -> string -> int -> Proof.state -> (string * thm list) list + params -> int -> Proof.state -> (string * thm list) list -> (string * thm list) list option * string end; @@ -68,14 +67,18 @@ (* minimalization of thms *) -fun minimize_theorems (params as {debug, minimize_timeout, isar_proof, modulus, - sorts, ...}) - prover atp_name i state name_thms_pairs = +fun minimize_theorems (params as {debug, atps, minimize_timeout, isar_proof, + modulus, sorts, ...}) + i state name_thms_pairs = let + val thy = Proof.theory_of state + val prover = case atps of + [atp_name] => get_prover thy atp_name + | _ => error "Expected a single ATP." val msecs = Time.toMilliseconds minimize_timeout val n = length name_thms_pairs val _ = - priority ("Sledgehammer minimizer: ATP " ^ quote atp_name ^ + priority ("Sledgehammer minimizer: ATP " ^ quote (the_single atps) ^ " with a time limit of " ^ string_of_int msecs ^ " ms.") val test_thms_fun = sledgehammer_test_theorems params prover minimize_timeout i state diff -r b3dce4c715d0 -r f32c567dbcaa src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML Fri Apr 23 18:11:41 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML Fri Apr 23 19:12:49 2010 +0200 @@ -190,11 +190,15 @@ tvar_prefix ^ (ascii_of_indexname (trim_type_var x,i)); fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (trim_type_var x)); -(* HACK because SPASS 3.0 truncates identifiers to 63 characters. (This is - solved in 3.7 and perhaps in earlier versions too.) *) -(* 32-bit hash, so we expect no collisions. *) +val max_dfg_symbol_length = 63 + +(* HACK because SPASS 3.0 truncates identifiers to 63 characters. *) fun controlled_length dfg s = - if dfg andalso size s > 60 then Word.toString (hashw_string (s, 0w0)) else s; + if dfg andalso size s > max_dfg_symbol_length then + String.extract (s, 0, SOME (max_dfg_symbol_length div 2 - 1)) ^ "__" ^ + String.extract (s, size s - max_dfg_symbol_length div 2 + 1, NONE) + else + s fun lookup_const dfg c = case Symtab.lookup const_trans_table c of diff -r b3dce4c715d0 -r f32c567dbcaa src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Apr 23 18:11:41 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Apr 23 19:12:49 2010 +0200 @@ -211,40 +211,16 @@ proof_state) atps in () end -fun minimize override_params old_style_args i fact_refs state = +fun minimize override_params i fact_refs state = let val thy = Proof.theory_of state val ctxt = Proof.context_of state - fun theorems_from_refs ctxt = - map (fn fact_ref => - let - val ths = ProofContext.get_fact ctxt fact_ref - val name' = Facts.string_of_ref fact_ref - in (name', ths) end) - fun get_time_limit_arg s = - (case Int.fromString s of - SOME t => Time.fromSeconds t - | NONE => error ("Invalid time limit: " ^ quote s ^ ".")) - fun get_opt (name, a) (p, t) = - (case name of - "time" => (p, get_time_limit_arg a) - | "atp" => (a, t) - | n => error ("Invalid argument: " ^ n ^ ".")) - val {atps, minimize_timeout, ...} = get_params thy override_params - val (atp, timeout) = fold get_opt old_style_args (hd atps, minimize_timeout) - val params = - get_params thy - (override_params @ - [("atps", [atp]), - ("minimize_timeout", - [string_of_int (Time.toMilliseconds timeout) ^ " ms"])]) - val prover = - (case get_prover thy atp of - SOME prover => prover - | NONE => error ("Unknown ATP: " ^ quote atp ^ ".")) + val theorems_from_refs = + map o pairf Facts.string_of_ref o ProofContext.get_fact val name_thms_pairs = theorems_from_refs ctxt fact_refs in - priority (#2 (minimize_theorems params prover atp i state name_thms_pairs)) + priority (#2 (minimize_theorems (get_params thy override_params) i state + name_thms_pairs)) end val sledgehammerN = "sledgehammer" @@ -287,7 +263,7 @@ (minimize_command override_params i) state end else if subcommand = minimizeN then - minimize (map (apfst minimizize_raw_param_name) override_params) [] + minimize (map (apfst minimizize_raw_param_name) override_params) (the_default 1 opt_i) (#add relevance_override) state else if subcommand = messagesN then messages opt_i @@ -345,33 +321,6 @@ val parse_sledgehammer_params_command = parse_params #>> sledgehammer_params_trans -val parse_minimize_args = - Scan.optional (Args.bracks (P.list (P.short_ident --| P.$$$ "=" -- P.xname))) - [] -val _ = - OuterSyntax.improper_command "atp_kill" "kill all managed provers" K.diag - (Scan.succeed (Toplevel.no_timing o Toplevel.imperative kill_atps)) -val _ = - OuterSyntax.improper_command "atp_info" - "print information about managed provers" K.diag - (Scan.succeed (Toplevel.no_timing o Toplevel.imperative running_atps)) -val _ = - OuterSyntax.improper_command "atp_messages" - "print recent messages issued by managed provers" K.diag - (Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")") >> - (fn limit => Toplevel.no_timing - o Toplevel.imperative (fn () => messages limit))) -val _ = - OuterSyntax.improper_command "print_atps" "print external provers" K.diag - (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory o - Toplevel.keep (available_atps o Toplevel.theory_of))) -val _ = - OuterSyntax.improper_command "atp_minimize" - "minimize theorem list with external prover" K.diag - (parse_minimize_args -- parse_fact_refs >> (fn (args, fact_refs) => - Toplevel.no_timing o Toplevel.unknown_proof o - Toplevel.keep (minimize [] args 1 fact_refs o Toplevel.proof_of))) - val _ = OuterSyntax.improper_command sledgehammerN "search for first-order proof using automatic theorem provers" K.diag diff -r b3dce4c715d0 -r f32c567dbcaa src/HOL/Tools/Sledgehammer/sledgehammer_util.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri Apr 23 18:11:41 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri Apr 23 19:12:49 2010 +0200 @@ -6,6 +6,7 @@ signature SLEDGEHAMMER_UTIL = sig + val pairf : ('a -> 'b) -> ('a -> 'c) -> 'a -> 'b * 'c val plural_s : int -> string val serial_commas : string -> string list -> string list val replace_all : string -> string -> string -> string @@ -13,14 +14,13 @@ val timestamp : unit -> string val parse_bool_option : bool -> string -> string -> bool option val parse_time_option : string -> string -> Time.time option - val hashw : word * word -> word - val hashw_char : Char.char * word -> word - val hashw_string : string * word -> word end; structure Sledgehammer_Util : SLEDGEHAMMER_UTIL = struct +fun pairf f g x = (f x, g x) + fun plural_s n = if n = 1 then "" else "s" fun serial_commas _ [] = ["??"] @@ -73,11 +73,4 @@ SOME (Time.fromMilliseconds msecs) end -(* This hash function is recommended in Compilers: Principles, Techniques, and - Tools, by Aho, Sethi and Ullman. The hashpjw function, which they - particularly recommend, triggers a bug in versions of Poly/ML up to 4.2.0. *) -fun hashw (u, w) = Word.+ (u, Word.* (0w65599, w)) -fun hashw_char (c, w) = hashw (Word.fromInt (Char.ord c), w) -fun hashw_string (s:string, w) = CharVector.foldl hashw_char w s - end;