src/HOL/Tools/Nitpick/nitpick_util.ML
changeset 38188 7f12a03c513c
parent 38026 bdd19b641062
child 38200 2f531f620cb8
equal deleted inserted replaced
38187:fd28328daf73 38188:7f12a03c513c
    47     (''a * ''a -> bool) -> (''a option * 'b) list -> ''a -> 'b option
    47     (''a * ''a -> bool) -> (''a option * 'b) list -> ''a -> 'b option
    48   val is_substring_of : string -> string -> bool
    48   val is_substring_of : string -> string -> bool
    49   val plural_s : int -> string
    49   val plural_s : int -> string
    50   val plural_s_for_list : 'a list -> string
    50   val plural_s_for_list : 'a list -> string
    51   val serial_commas : string -> string list -> string list
    51   val serial_commas : string -> string list -> string list
       
    52   val pretty_serial_commas : string -> Pretty.T list -> Pretty.T list
    52   val parse_bool_option : bool -> string -> string -> bool option
    53   val parse_bool_option : bool -> string -> string -> bool option
    53   val parse_time_option : string -> string -> Time.time option
    54   val parse_time_option : string -> string -> Time.time option
    54   val flip_polarity : polarity -> polarity
    55   val flip_polarity : polarity -> polarity
    55   val prop_T : typ
    56   val prop_T : typ
    56   val bool_T : typ
    57   val bool_T : typ
    70   val DETERM_TIMEOUT : Time.time option -> tactic -> tactic
    71   val DETERM_TIMEOUT : Time.time option -> tactic -> tactic
    71   val setmp_show_all_types : ('a -> 'b) -> 'a -> 'b
    72   val setmp_show_all_types : ('a -> 'b) -> 'a -> 'b
    72   val indent_size : int
    73   val indent_size : int
    73   val pstrs : string -> Pretty.T list
    74   val pstrs : string -> Pretty.T list
    74   val unyxml : string -> string
    75   val unyxml : string -> string
    75   val maybe_quote : string -> string
    76   val pretty_maybe_quote : Pretty.T -> Pretty.T
    76   val hashw : word * word -> word
    77   val hashw : word * word -> word
    77   val hashw_string : string * word -> word
    78   val hashw_string : string * word -> word
    78 end;
    79 end;
    79 
    80 
    80 structure Nitpick_Util : NITPICK_UTIL =
    81 structure Nitpick_Util : NITPICK_UTIL =
   220 val plural_s = Sledgehammer_Util.plural_s
   221 val plural_s = Sledgehammer_Util.plural_s
   221 fun plural_s_for_list xs = plural_s (length xs)
   222 fun plural_s_for_list xs = plural_s (length xs)
   222 
   223 
   223 val serial_commas = Sledgehammer_Util.serial_commas
   224 val serial_commas = Sledgehammer_Util.serial_commas
   224 
   225 
       
   226 fun pretty_serial_commas _ [] = []
       
   227   | pretty_serial_commas _ [p] = [p]
       
   228   | pretty_serial_commas conj [p1, p2] =
       
   229     [p1, Pretty.brk 1, Pretty.str conj, Pretty.brk 1, p2]
       
   230   | pretty_serial_commas conj [p1, p2, p3] =
       
   231     [p1, Pretty.str ",", Pretty.brk 1, p2, Pretty.str ",", Pretty.brk 1,
       
   232      Pretty.str conj, Pretty.brk 1, p3]
       
   233   | pretty_serial_commas conj (p :: ps) =
       
   234     p :: Pretty.str "," :: Pretty.brk 1 :: pretty_serial_commas conj ps
       
   235 
   225 val parse_bool_option = Sledgehammer_Util.parse_bool_option
   236 val parse_bool_option = Sledgehammer_Util.parse_bool_option
   226 val parse_time_option = Sledgehammer_Util.parse_time_option
   237 val parse_time_option = Sledgehammer_Util.parse_time_option
   227 
   238 
   228 fun flip_polarity Pos = Neg
   239 fun flip_polarity Pos = Neg
   229   | flip_polarity Neg = Pos
   240   | flip_polarity Neg = Pos
   260 fun DETERM_TIMEOUT delay tac st =
   271 fun DETERM_TIMEOUT delay tac st =
   261   Seq.of_list (the_list (time_limit delay (fn () => SINGLE tac st) ()))
   272   Seq.of_list (the_list (time_limit delay (fn () => SINGLE tac st) ()))
   262 
   273 
   263 fun setmp_show_all_types f =
   274 fun setmp_show_all_types f =
   264   setmp_CRITICAL show_all_types
   275   setmp_CRITICAL show_all_types
   265                  (! show_types orelse ! show_sorts orelse ! show_all_types) f
   276                  (!show_types orelse !show_sorts orelse !show_all_types) f
   266 
   277 
   267 val indent_size = 2
   278 val indent_size = 2
   268 
   279 
   269 val pstrs = Pretty.breaks o map Pretty.str o space_explode " "
   280 val pstrs = Pretty.breaks o map Pretty.str o space_explode " "
   270 
   281 
   271 val unyxml = Sledgehammer_Util.unyxml
   282 val unyxml = Sledgehammer_Util.unyxml
       
   283 
   272 val maybe_quote = Sledgehammer_Util.maybe_quote
   284 val maybe_quote = Sledgehammer_Util.maybe_quote
       
   285 fun pretty_maybe_quote pretty =
       
   286   let val s = Pretty.str_of pretty in
       
   287     if maybe_quote s = s then pretty else Pretty.enum "" "\"" "\"" [pretty]
       
   288   end
   273 
   289 
   274 (* This hash function is recommended in Compilers: Principles, Techniques, and
   290 (* This hash function is recommended in Compilers: Principles, Techniques, and
   275    Tools, by Aho, Sethi, and Ullman. The "hashpjw" function, which they
   291    Tools, by Aho, Sethi, and Ullman. The "hashpjw" function, which they
   276    particularly recommend, triggers a bug in versions of Poly/ML up to 4.2.0. *)
   292    particularly recommend, triggers a bug in versions of Poly/ML up to 4.2.0. *)
   277 fun hashw (u, w) = Word.+ (u, Word.* (0w65599, w))
   293 fun hashw (u, w) = Word.+ (u, Word.* (0w65599, w))