src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
changeset 36169 27b1cc58715e
parent 36142 f5e15e9aae10
child 36170 0cdb76723c88
equal deleted inserted replaced
36168:0a6ed065683d 36169:27b1cc58715e
     6 
     6 
     7 signature SLEDGEHAMMER_UTIL =
     7 signature SLEDGEHAMMER_UTIL =
     8 sig
     8 sig
     9   val plural_s : int -> string
     9   val plural_s : int -> string
    10   val serial_commas : string -> string list -> string list
    10   val serial_commas : string -> string list -> string list
       
    11   val replace_all : string -> string -> string -> string
       
    12   val remove_all : string -> string -> string
    11   val parse_bool_option : bool -> string -> string -> bool option
    13   val parse_bool_option : bool -> string -> string -> bool option
    12   val parse_time_option : string -> string -> Time.time option
    14   val parse_time_option : string -> string -> Time.time option
    13   val hashw : word * word -> word
    15   val hashw : word * word -> word
    14   val hashw_char : Char.char * word -> word
    16   val hashw_char : Char.char * word -> word
    15   val hashw_string : string * word -> word
    17   val hashw_string : string * word -> word
    23 fun serial_commas _ [] = ["??"]
    25 fun serial_commas _ [] = ["??"]
    24   | serial_commas _ [s] = [s]
    26   | serial_commas _ [s] = [s]
    25   | serial_commas conj [s1, s2] = [s1, conj, s2]
    27   | serial_commas conj [s1, s2] = [s1, conj, s2]
    26   | serial_commas conj [s1, s2, s3] = [s1 ^ ",", s2 ^ ",", conj, s3]
    28   | serial_commas conj [s1, s2, s3] = [s1 ^ ",", s2 ^ ",", conj, s3]
    27   | serial_commas conj (s :: ss) = s ^ "," :: serial_commas conj ss
    29   | serial_commas conj (s :: ss) = s ^ "," :: serial_commas conj ss
       
    30 
       
    31 fun replace_all bef aft =
       
    32   let
       
    33     fun aux seen "" = String.implode (rev seen)
       
    34       | aux seen s =
       
    35       if String.isPrefix bef s then
       
    36           aux seen "" ^ aft ^ aux [] (unprefix bef s)
       
    37         else
       
    38           aux (String.sub (s, 0) :: seen) (String.extract (s, 1, NONE))
       
    39   in aux [] end
       
    40 
       
    41 fun remove_all bef = replace_all bef ""
    28 
    42 
    29 fun parse_bool_option option name s =
    43 fun parse_bool_option option name s =
    30   (case s of
    44   (case s of
    31      "smart" => if option then NONE else raise Option
    45      "smart" => if option then NONE else raise Option
    32    | "false" => SOME false
    46    | "false" => SOME false