stop referring to Sledgehammer_Util stuff all over Nitpick code; instead, redeclare any needed function in Nitpick_Util as synonym for the Sledgehammer_Util function of the same name
--- a/src/HOL/Tools/Nitpick/nitpick.ML Fri Apr 23 19:16:52 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Fri Apr 23 19:18:39 2010 +0200
@@ -348,7 +348,7 @@
fun monotonicity_message Ts extra =
let val ss = map (quote o string_for_type ctxt) Ts in
"The type" ^ plural_s_for_list ss ^ " " ^
- space_implode " " (Sledgehammer_Util.serial_commas "and" ss) ^ " " ^
+ space_implode " " (serial_commas "and" ss) ^ " " ^
(if none_true monos then
"passed the monotonicity test"
else
@@ -686,8 +686,7 @@
options
in
print ("Try again with " ^
- space_implode " "
- (Sledgehammer_Util.serial_commas "and" ss) ^
+ space_implode " " (serial_commas "and" ss) ^
" to confirm that the " ^ das_wort_model ^
" is genuine.")
end
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Fri Apr 23 19:16:52 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Fri Apr 23 19:18:39 2010 +0200
@@ -217,7 +217,6 @@
structure Nitpick_HOL : NITPICK_HOL =
struct
-open Sledgehammer_Util
open Nitpick_Util
type const_table = term list Symtab.table
--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Fri Apr 23 19:16:52 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Fri Apr 23 19:18:39 2010 +0200
@@ -176,7 +176,7 @@
(* bool -> bool option -> string -> bool option *)
fun general_lookup_bool option default_value name =
case lookup name of
- SOME s => Sledgehammer_Util.parse_bool_option option name s
+ SOME s => parse_bool_option option name s
| NONE => default_value
(* string -> bool *)
val lookup_bool = the o general_lookup_bool false (SOME false)
@@ -235,8 +235,7 @@
:: map (fn (name, value) =>
(SOME (read (String.extract (name, size prefix + 1, NONE))),
value |> stringify_raw_param_value
- |> Sledgehammer_Util.parse_bool_option false name
- |> the))
+ |> parse_bool_option false name |> the))
(filter (String.isPrefix (prefix ^ " ") o fst) raw_params)
(* (string -> 'a) -> string -> ('a option * bool option) list *)
fun lookup_bool_option_assigns read prefix =
@@ -244,13 +243,13 @@
:: map (fn (name, value) =>
(SOME (read (String.extract (name, size prefix + 1, NONE))),
value |> stringify_raw_param_value
- |> Sledgehammer_Util.parse_bool_option true name))
+ |> parse_bool_option true name))
(filter (String.isPrefix (prefix ^ " ") o fst) raw_params)
(* string -> Time.time option *)
fun lookup_time name =
case lookup name of
NONE => NONE
- | SOME s => Sledgehammer_Util.parse_time_option name s
+ | SOME s => parse_time_option name s
(* string -> term list *)
val lookup_term_list =
AList.lookup (op =) raw_params #> these #> Syntax.read_terms ctxt
--- a/src/HOL/Tools/Nitpick/nitpick_scope.ML Fri Apr 23 19:16:52 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML Fri Apr 23 19:18:39 2010 +0200
@@ -194,11 +194,8 @@
else
[])
in
- if null ss then
- []
- else
- Sledgehammer_Util.serial_commas "and" ss
- |> map Pretty.str |> Pretty.breaks
+ if null ss then []
+ else serial_commas "and" ss |> map Pretty.str |> Pretty.breaks
end
(* scope -> string *)
--- a/src/HOL/Tools/Nitpick/nitpick_util.ML Fri Apr 23 19:16:52 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_util.ML Fri Apr 23 19:18:39 2010 +0200
@@ -48,6 +48,10 @@
val is_substring_of : string -> string -> bool
val plural_s : int -> string
val plural_s_for_list : 'a list -> string
+ val serial_commas : string -> string list -> string list
+ val timestamp : unit -> string
+ val parse_bool_option : bool -> string -> string -> bool option
+ val parse_time_option : string -> string -> Time.time option
val flip_polarity : polarity -> polarity
val prop_T : typ
val bool_T : typ
@@ -61,6 +65,8 @@
val pstrs : string -> Pretty.T list
val unyxml : string -> string
val maybe_quote : string -> string
+ val hashw : word * word -> word
+ val hashw_string : string * word -> word
end;
structure Nitpick_Util : NITPICK_UTIL =
@@ -82,7 +88,6 @@
(* ('a * 'b * 'c -> 'd) -> 'a -> 'b -> 'c -> 'd *)
fun curry3 f = fn x => fn y => fn z => f (x, y, z)
-(* ('a -> 'b) -> ('a -> 'c) -> 'a -> 'b * 'c *)
fun pairf f g x = (f x, g x)
(* (bool -> 'a) -> 'a * 'a *)
@@ -233,10 +238,20 @@
(Substring.full stack))))
(* int -> string *)
-fun plural_s n = if n = 1 then "" else "s"
+val plural_s = Sledgehammer_Util.plural_s
(* 'a list -> string *)
fun plural_s_for_list xs = plural_s (length xs)
+(* string -> string list -> string list *)
+val serial_commas = Sledgehammer_Util.serial_commas
+
+(* unit -> string *)
+val timestamp = Sledgehammer_Util.timestamp
+(* bool -> string -> string -> bool option *)
+val parse_bool_option = Sledgehammer_Util.parse_bool_option
+(* string -> string -> Time.time option *)
+val parse_time_option = Sledgehammer_Util.parse_time_option
+
(* polarity -> polarity *)
fun flip_polarity Pos = Neg
| flip_polarity Neg = Pos
@@ -290,4 +305,14 @@
OuterKeyword.is_keyword s) ? quote
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. *)
+(* word * word -> word *)
+fun hashw (u, w) = Word.+ (u, Word.* (0w65599, w))
+(* Char.char * word -> word *)
+fun hashw_char (c, w) = hashw (Word.fromInt (Char.ord c), w)
+(* string * word -> word *)
+fun hashw_string (s:string, w) = CharVector.foldl hashw_char w s
+
end;