# HG changeset patch # User blanchet # Date 1272043119 -7200 # Node ID 1e8fcaccb3e85c1bf639f79735dcbe6493472866 # Parent 20ef039bccff1f2c06920ae17ed51b6c53015cd6 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 diff -r 20ef039bccff -r 1e8fcaccb3e8 src/HOL/Tools/Nitpick/nitpick.ML --- 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 diff -r 20ef039bccff -r 1e8fcaccb3e8 src/HOL/Tools/Nitpick/nitpick_hol.ML --- 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 diff -r 20ef039bccff -r 1e8fcaccb3e8 src/HOL/Tools/Nitpick/nitpick_isar.ML --- 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 diff -r 20ef039bccff -r 1e8fcaccb3e8 src/HOL/Tools/Nitpick/nitpick_scope.ML --- 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 *) diff -r 20ef039bccff -r 1e8fcaccb3e8 src/HOL/Tools/Nitpick/nitpick_util.ML --- 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;