remove some bloat
authorblanchet
Fri Apr 23 19:12:49 2010 +0200 (2010-04-23)
changeset 36378f32c567dbcaa
parent 36377 b3dce4c715d0
child 36379 20ef039bccff
remove some bloat
src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML
src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML	Fri Apr 23 18:11:41 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML	Fri Apr 23 19:12:49 2010 +0200
     1.3 @@ -8,11 +8,10 @@
     1.4  signature SLEDGEHAMMER_FACT_MINIMIZER =
     1.5  sig
     1.6    type params = ATP_Manager.params
     1.7 -  type prover = ATP_Manager.prover
     1.8    type prover_result = ATP_Manager.prover_result
     1.9  
    1.10    val minimize_theorems :
    1.11 -    params -> prover -> string -> int -> Proof.state -> (string * thm list) list
    1.12 +    params -> int -> Proof.state -> (string * thm list) list
    1.13      -> (string * thm list) list option * string
    1.14  end;
    1.15  
    1.16 @@ -68,14 +67,18 @@
    1.17  
    1.18  (* minimalization of thms *)
    1.19  
    1.20 -fun minimize_theorems (params as {debug, minimize_timeout, isar_proof, modulus,
    1.21 -                                  sorts, ...})
    1.22 -                      prover atp_name i state name_thms_pairs =
    1.23 +fun minimize_theorems (params as {debug, atps, minimize_timeout, isar_proof,
    1.24 +                                  modulus, sorts, ...})
    1.25 +                      i state name_thms_pairs =
    1.26    let
    1.27 +    val thy = Proof.theory_of state
    1.28 +    val prover = case atps of
    1.29 +                   [atp_name] => get_prover thy atp_name
    1.30 +                 | _ => error "Expected a single ATP."
    1.31      val msecs = Time.toMilliseconds minimize_timeout
    1.32      val n = length name_thms_pairs
    1.33      val _ =
    1.34 -      priority ("Sledgehammer minimizer: ATP " ^ quote atp_name ^
    1.35 +      priority ("Sledgehammer minimizer: ATP " ^ quote (the_single atps) ^
    1.36                  " with a time limit of " ^ string_of_int msecs ^ " ms.")
    1.37      val test_thms_fun =
    1.38        sledgehammer_test_theorems params prover minimize_timeout i state
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML	Fri Apr 23 18:11:41 2010 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML	Fri Apr 23 19:12:49 2010 +0200
     2.3 @@ -190,11 +190,15 @@
     2.4        tvar_prefix ^ (ascii_of_indexname (trim_type_var x,i));
     2.5  fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (trim_type_var x));
     2.6  
     2.7 -(* HACK because SPASS 3.0 truncates identifiers to 63 characters. (This is
     2.8 -   solved in 3.7 and perhaps in earlier versions too.) *)
     2.9 -(* 32-bit hash, so we expect no collisions. *)
    2.10 +val max_dfg_symbol_length = 63
    2.11 +
    2.12 +(* HACK because SPASS 3.0 truncates identifiers to 63 characters. *)
    2.13  fun controlled_length dfg s =
    2.14 -  if dfg andalso size s > 60 then Word.toString (hashw_string (s, 0w0)) else s;
    2.15 +  if dfg andalso size s > max_dfg_symbol_length then
    2.16 +    String.extract (s, 0, SOME (max_dfg_symbol_length div 2 - 1)) ^ "__" ^
    2.17 +    String.extract (s, size s - max_dfg_symbol_length div 2 + 1, NONE)
    2.18 +  else
    2.19 +    s
    2.20  
    2.21  fun lookup_const dfg c =
    2.22      case Symtab.lookup const_trans_table c of
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Apr 23 18:11:41 2010 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Apr 23 19:12:49 2010 +0200
     3.3 @@ -211,40 +211,16 @@
     3.4                                              proof_state) atps
     3.5      in () end
     3.6  
     3.7 -fun minimize override_params old_style_args i fact_refs state =
     3.8 +fun minimize override_params i fact_refs state =
     3.9    let
    3.10      val thy = Proof.theory_of state
    3.11      val ctxt = Proof.context_of state
    3.12 -    fun theorems_from_refs ctxt =
    3.13 -      map (fn fact_ref =>
    3.14 -              let
    3.15 -                val ths = ProofContext.get_fact ctxt fact_ref
    3.16 -                val name' = Facts.string_of_ref fact_ref
    3.17 -              in (name', ths) end)
    3.18 -    fun get_time_limit_arg s =
    3.19 -      (case Int.fromString s of
    3.20 -        SOME t => Time.fromSeconds t
    3.21 -      | NONE => error ("Invalid time limit: " ^ quote s ^ "."))
    3.22 -    fun get_opt (name, a) (p, t) =
    3.23 -      (case name of
    3.24 -        "time" => (p, get_time_limit_arg a)
    3.25 -      | "atp" => (a, t)
    3.26 -      | n => error ("Invalid argument: " ^ n ^ "."))
    3.27 -    val {atps, minimize_timeout, ...} = get_params thy override_params
    3.28 -    val (atp, timeout) = fold get_opt old_style_args (hd atps, minimize_timeout)
    3.29 -    val params =
    3.30 -      get_params thy
    3.31 -          (override_params @
    3.32 -           [("atps", [atp]),
    3.33 -            ("minimize_timeout",
    3.34 -             [string_of_int (Time.toMilliseconds timeout) ^ " ms"])])
    3.35 -    val prover =
    3.36 -      (case get_prover thy atp of
    3.37 -        SOME prover => prover
    3.38 -      | NONE => error ("Unknown ATP: " ^ quote atp ^ "."))
    3.39 +    val theorems_from_refs =
    3.40 +      map o pairf Facts.string_of_ref o ProofContext.get_fact
    3.41      val name_thms_pairs = theorems_from_refs ctxt fact_refs
    3.42    in
    3.43 -    priority (#2 (minimize_theorems params prover atp i state name_thms_pairs))
    3.44 +    priority (#2 (minimize_theorems (get_params thy override_params) i state
    3.45 +                                    name_thms_pairs))
    3.46    end
    3.47  
    3.48  val sledgehammerN = "sledgehammer"
    3.49 @@ -287,7 +263,7 @@
    3.50              (minimize_command override_params i) state
    3.51        end
    3.52      else if subcommand = minimizeN then
    3.53 -      minimize (map (apfst minimizize_raw_param_name) override_params) []
    3.54 +      minimize (map (apfst minimizize_raw_param_name) override_params)
    3.55                 (the_default 1 opt_i) (#add relevance_override) state
    3.56      else if subcommand = messagesN then
    3.57        messages opt_i
    3.58 @@ -345,33 +321,6 @@
    3.59  val parse_sledgehammer_params_command =
    3.60    parse_params #>> sledgehammer_params_trans
    3.61  
    3.62 -val parse_minimize_args =
    3.63 -  Scan.optional (Args.bracks (P.list (P.short_ident --| P.$$$ "=" -- P.xname)))
    3.64 -                []
    3.65 -val _ =
    3.66 -  OuterSyntax.improper_command "atp_kill" "kill all managed provers" K.diag
    3.67 -    (Scan.succeed (Toplevel.no_timing o Toplevel.imperative kill_atps))
    3.68 -val _ =
    3.69 -  OuterSyntax.improper_command "atp_info"
    3.70 -    "print information about managed provers" K.diag
    3.71 -    (Scan.succeed (Toplevel.no_timing o Toplevel.imperative running_atps))
    3.72 -val _ =
    3.73 -  OuterSyntax.improper_command "atp_messages"
    3.74 -    "print recent messages issued by managed provers" K.diag
    3.75 -    (Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")") >>
    3.76 -      (fn limit => Toplevel.no_timing
    3.77 -                   o Toplevel.imperative (fn () => messages limit)))
    3.78 -val _ =
    3.79 -  OuterSyntax.improper_command "print_atps" "print external provers" K.diag
    3.80 -    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory o
    3.81 -      Toplevel.keep (available_atps o Toplevel.theory_of)))
    3.82 -val _ =
    3.83 -  OuterSyntax.improper_command "atp_minimize"
    3.84 -    "minimize theorem list with external prover" K.diag
    3.85 -    (parse_minimize_args -- parse_fact_refs >> (fn (args, fact_refs) =>
    3.86 -      Toplevel.no_timing o Toplevel.unknown_proof o
    3.87 -        Toplevel.keep (minimize [] args 1 fact_refs o Toplevel.proof_of)))
    3.88 -
    3.89  val _ =
    3.90    OuterSyntax.improper_command sledgehammerN
    3.91      "search for first-order proof using automatic theorem provers" K.diag
     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Fri Apr 23 18:11:41 2010 +0200
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Fri Apr 23 19:12:49 2010 +0200
     4.3 @@ -6,6 +6,7 @@
     4.4  
     4.5  signature SLEDGEHAMMER_UTIL =
     4.6  sig
     4.7 +  val pairf : ('a -> 'b) -> ('a -> 'c) -> 'a -> 'b * 'c
     4.8    val plural_s : int -> string
     4.9    val serial_commas : string -> string list -> string list
    4.10    val replace_all : string -> string -> string -> string
    4.11 @@ -13,14 +14,13 @@
    4.12    val timestamp : unit -> string
    4.13    val parse_bool_option : bool -> string -> string -> bool option
    4.14    val parse_time_option : string -> string -> Time.time option
    4.15 -  val hashw : word * word -> word
    4.16 -  val hashw_char : Char.char * word -> word
    4.17 -  val hashw_string : string * word -> word
    4.18  end;
    4.19   
    4.20  structure Sledgehammer_Util : SLEDGEHAMMER_UTIL =
    4.21  struct
    4.22  
    4.23 +fun pairf f g x = (f x, g x)
    4.24 +
    4.25  fun plural_s n = if n = 1 then "" else "s"
    4.26  
    4.27  fun serial_commas _ [] = ["??"]
    4.28 @@ -73,11 +73,4 @@
    4.29          SOME (Time.fromMilliseconds msecs)
    4.30      end
    4.31  
    4.32 -(* This hash function is recommended in Compilers: Principles, Techniques, and
    4.33 -   Tools, by Aho, Sethi and Ullman. The hashpjw function, which they
    4.34 -   particularly recommend, triggers a bug in versions of Poly/ML up to 4.2.0. *)
    4.35 -fun hashw (u, w) = Word.+ (u, Word.* (0w65599, w))
    4.36 -fun hashw_char (c, w) = hashw (Word.fromInt (Char.ord c), w)
    4.37 -fun hashw_string (s:string, w) = CharVector.foldl hashw_char w s
    4.38 -
    4.39  end;