src/HOL/Tools/Nitpick/nitpick_util.ML
author blanchet
Tue Jun 01 12:20:08 2010 +0200 (2010-06-01)
changeset 37260 dde817e6dfb1
parent 36555 8ff45c2076da
child 37261 8a89fd40ed0b
permissions -rw-r--r--
added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"
blanchet@33982
     1
(*  Title:      HOL/Tools/Nitpick/nitpick_util.ML
blanchet@33192
     2
    Author:     Jasmin Blanchette, TU Muenchen
blanchet@34982
     3
    Copyright   2008, 2009, 2010
blanchet@33192
     4
blanchet@33192
     5
General-purpose functions used by the Nitpick modules.
blanchet@33192
     6
*)
blanchet@33192
     7
blanchet@33705
     8
signature NITPICK_UTIL =
blanchet@33192
     9
sig
blanchet@33192
    10
  type styp = string * typ
blanchet@33192
    11
  datatype polarity = Pos | Neg | Neut
blanchet@33192
    12
blanchet@33192
    13
  exception ARG of string * string
blanchet@33192
    14
  exception BAD of string * string
blanchet@34124
    15
  exception TOO_SMALL of string * string
blanchet@34124
    16
  exception TOO_LARGE of string * string
blanchet@33192
    17
  exception NOT_SUPPORTED of string
blanchet@33192
    18
  exception SAME of unit
blanchet@33192
    19
blanchet@33192
    20
  val nitpick_prefix : string
blanchet@33192
    21
  val curry3 : ('a * 'b * 'c -> 'd) -> 'a -> 'b -> 'c -> 'd
blanchet@33705
    22
  val pairf : ('a -> 'b) -> ('a -> 'c) -> 'a -> 'b * 'c
blanchet@35385
    23
  val pair_from_fun : (bool -> 'a) -> 'a * 'a
blanchet@35385
    24
  val fun_from_pair : 'a * 'a -> bool -> 'a
blanchet@35385
    25
  val int_from_bool : bool -> int
blanchet@33705
    26
  val nat_minus : int -> int -> int
blanchet@33192
    27
  val reasonable_power : int -> int -> int
blanchet@33192
    28
  val exact_log : int -> int -> int
blanchet@33192
    29
  val exact_root : int -> int -> int
blanchet@33192
    30
  val offset_list : int list -> int list
blanchet@33192
    31
  val index_seq : int -> int -> int list
blanchet@33192
    32
  val filter_indices : int list -> 'a list -> 'a list
blanchet@33192
    33
  val filter_out_indices : int list -> 'a list -> 'a list
blanchet@33192
    34
  val fold1 : ('a -> 'a -> 'a) -> 'a list -> 'a
blanchet@33192
    35
  val replicate_list : int -> 'a list -> 'a list
blanchet@33192
    36
  val n_fold_cartesian_product : 'a list list -> 'a list list
blanchet@33192
    37
  val all_distinct_unordered_pairs_of : ''a list -> (''a * ''a) list
blanchet@33192
    38
  val nth_combination : (int * int) list -> int -> int list
blanchet@33192
    39
  val all_combinations : (int * int) list -> int list list
blanchet@33192
    40
  val all_permutations : 'a list -> 'a list list
blanchet@33192
    41
  val batch_list : int -> 'a list -> 'a list list
blanchet@33192
    42
  val chunk_list_unevenly : int list -> 'a list -> 'a list list
blanchet@33192
    43
  val map3 : ('a -> 'b -> 'c -> 'd) -> 'a list -> 'b list -> 'c list -> 'd list
blanchet@33192
    44
  val double_lookup :
blanchet@33192
    45
    ('a * 'a -> bool) -> ('a option * 'b) list -> 'a -> 'b option
blanchet@33192
    46
  val triple_lookup :
blanchet@33192
    47
    (''a * ''a -> bool) -> (''a option * 'b) list -> ''a -> 'b option
blanchet@33192
    48
  val is_substring_of : string -> string -> bool
blanchet@33192
    49
  val plural_s : int -> string
blanchet@33192
    50
  val plural_s_for_list : 'a list -> string
blanchet@36380
    51
  val serial_commas : string -> string list -> string list
blanchet@36380
    52
  val timestamp : unit -> string
blanchet@36380
    53
  val parse_bool_option : bool -> string -> string -> bool option
blanchet@36380
    54
  val parse_time_option : string -> string -> Time.time option
blanchet@33192
    55
  val flip_polarity : polarity -> polarity
blanchet@33192
    56
  val prop_T : typ
blanchet@33192
    57
  val bool_T : typ
blanchet@33192
    58
  val nat_T : typ
blanchet@33192
    59
  val int_T : typ
blanchet@37260
    60
  val simple_string_of_typ : typ -> string
blanchet@37260
    61
  val is_real_constr : theory -> string * typ -> bool
blanchet@37260
    62
  val typ_of_dtyp :
blanchet@37260
    63
    Datatype_Aux.descr -> (Datatype_Aux.dtyp * typ) list -> Datatype_Aux.dtyp
blanchet@37260
    64
    -> typ
blanchet@37260
    65
  val is_of_class_const : theory -> string * typ -> bool
blanchet@37260
    66
  val get_class_def : theory -> string -> (string * term) option
blanchet@36555
    67
  val monomorphic_term : Type.tyenv -> term -> term
blanchet@37260
    68
  val specialize_type : theory -> string * typ -> term -> term
blanchet@33192
    69
  val nat_subscript : int -> string
blanchet@33192
    70
  val time_limit : Time.time option -> ('a -> 'b) -> 'a -> 'b
blanchet@33192
    71
  val DETERM_TIMEOUT : Time.time option -> tactic -> tactic
blanchet@33192
    72
  val setmp_show_all_types : ('a -> 'b) -> 'a -> 'b
blanchet@33192
    73
  val indent_size : int
blanchet@33192
    74
  val pstrs : string -> Pretty.T list
blanchet@34982
    75
  val unyxml : string -> string
blanchet@33192
    76
  val maybe_quote : string -> string
blanchet@36380
    77
  val hashw : word * word -> word
blanchet@36380
    78
  val hashw_string : string * word -> word
blanchet@35866
    79
end;
blanchet@33192
    80
blanchet@33232
    81
structure Nitpick_Util : NITPICK_UTIL =
blanchet@33192
    82
struct
blanchet@33192
    83
blanchet@33192
    84
type styp = string * typ
blanchet@33192
    85
blanchet@33192
    86
datatype polarity = Pos | Neg | Neut
blanchet@33192
    87
blanchet@33192
    88
exception ARG of string * string
blanchet@33192
    89
exception BAD of string * string
blanchet@34124
    90
exception TOO_SMALL of string * string
blanchet@34124
    91
exception TOO_LARGE of string * string
blanchet@33192
    92
exception NOT_SUPPORTED of string
blanchet@33192
    93
exception SAME of unit
blanchet@33192
    94
blanchet@33192
    95
val nitpick_prefix = "Nitpick."
blanchet@33192
    96
blanchet@33192
    97
fun curry3 f = fn x => fn y => fn z => f (x, y, z)
blanchet@33192
    98
blanchet@33705
    99
fun pairf f g x = (f x, g x)
blanchet@33192
   100
blanchet@35385
   101
fun pair_from_fun f = (f false, f true)
blanchet@35385
   102
fun fun_from_pair (f, t) b = if b then t else f
blanchet@35385
   103
blanchet@35385
   104
fun int_from_bool b = if b then 1 else 0
blanchet@33705
   105
fun nat_minus i j = if i > j then i - j else 0
blanchet@33192
   106
blanchet@33192
   107
val max_exponent = 16384
blanchet@33192
   108
blanchet@35280
   109
fun reasonable_power _ 0 = 1
blanchet@33192
   110
  | reasonable_power a 1 = a
blanchet@33192
   111
  | reasonable_power 0 _ = 0
blanchet@33192
   112
  | reasonable_power 1 _ = 1
blanchet@33192
   113
  | reasonable_power a b =
blanchet@34124
   114
    if b < 0 then
blanchet@34124
   115
      raise ARG ("Nitpick_Util.reasonable_power",
blanchet@34124
   116
                 "negative exponent (" ^ signed_string_of_int b ^ ")")
blanchet@34124
   117
    else if b > max_exponent then
blanchet@34124
   118
      raise TOO_LARGE ("Nitpick_Util.reasonable_power",
blanchet@34124
   119
                       "too large exponent (" ^ signed_string_of_int b ^ ")")
blanchet@33192
   120
    else
blanchet@34124
   121
      let val c = reasonable_power a (b div 2) in
blanchet@34124
   122
        c * c * reasonable_power a (b mod 2)
blanchet@34124
   123
      end
blanchet@33192
   124
blanchet@33192
   125
fun exact_log m n =
blanchet@33192
   126
  let
blanchet@33192
   127
    val r = Math.ln (Real.fromInt n) / Math.ln (Real.fromInt m) |> Real.round
blanchet@33192
   128
  in
blanchet@33192
   129
    if reasonable_power m r = n then
blanchet@33192
   130
      r
blanchet@33192
   131
    else
blanchet@33232
   132
      raise ARG ("Nitpick_Util.exact_log",
blanchet@33192
   133
                 commas (map signed_string_of_int [m, n]))
blanchet@33192
   134
  end
blanchet@33192
   135
blanchet@33192
   136
fun exact_root m n =
blanchet@33192
   137
  let val r = Math.pow (Real.fromInt n, 1.0 / (Real.fromInt m)) |> Real.round in
blanchet@33192
   138
    if reasonable_power r m = n then
blanchet@33192
   139
      r
blanchet@33192
   140
    else
blanchet@33232
   141
      raise ARG ("Nitpick_Util.exact_root",
blanchet@33192
   142
                 commas (map signed_string_of_int [m, n]))
blanchet@33192
   143
  end
blanchet@33192
   144
blanchet@33192
   145
fun fold1 f = foldl1 (uncurry f)
blanchet@33192
   146
blanchet@33192
   147
fun replicate_list 0 _ = []
blanchet@33192
   148
  | replicate_list n xs = xs @ replicate_list (n - 1) xs
blanchet@33192
   149
blanchet@33192
   150
fun offset_list ns = rev (tl (fold (fn x => fn xs => (x + hd xs) :: xs) ns [0]))
blanchet@33192
   151
fun index_seq j0 n = if j0 < 0 then j0 downto j0 - n + 1 else j0 upto j0 + n - 1
blanchet@33192
   152
blanchet@33192
   153
fun filter_indices js xs =
blanchet@33192
   154
  let
blanchet@33192
   155
    fun aux _ [] _ = []
blanchet@33192
   156
      | aux i (j :: js) (x :: xs) =
blanchet@33192
   157
        if i = j then x :: aux (i + 1) js xs else aux (i + 1) (j :: js) xs
blanchet@33232
   158
      | aux _ _ _ = raise ARG ("Nitpick_Util.filter_indices",
blanchet@33192
   159
                               "indices unordered or out of range")
blanchet@33192
   160
  in aux 0 js xs end
blanchet@33192
   161
fun filter_out_indices js xs =
blanchet@33192
   162
  let
blanchet@33192
   163
    fun aux _ [] xs = xs
blanchet@33192
   164
      | aux i (j :: js) (x :: xs) =
blanchet@33192
   165
        if i = j then aux (i + 1) js xs else x :: aux (i + 1) (j :: js) xs
blanchet@33232
   166
      | aux _ _ _ = raise ARG ("Nitpick_Util.filter_out_indices",
blanchet@33192
   167
                               "indices unordered or out of range")
blanchet@33192
   168
  in aux 0 js xs end
blanchet@33192
   169
blanchet@33192
   170
fun cartesian_product [] _ = []
blanchet@33192
   171
  | cartesian_product (x :: xs) yss =
blanchet@33192
   172
    map (cons x) yss @ cartesian_product xs yss
blanchet@33192
   173
fun n_fold_cartesian_product xss = fold_rev cartesian_product xss [[]]
blanchet@33192
   174
fun all_distinct_unordered_pairs_of [] = []
blanchet@33192
   175
  | all_distinct_unordered_pairs_of (x :: xs) =
blanchet@33192
   176
    map (pair x) xs @ all_distinct_unordered_pairs_of xs
blanchet@33192
   177
blanchet@33192
   178
val nth_combination =
blanchet@33192
   179
  let
blanchet@33192
   180
    fun aux [] n = ([], n)
blanchet@33192
   181
      | aux ((k, j0) :: xs) n =
blanchet@33192
   182
        let val (js, n) = aux xs n in ((n mod k) + j0 :: js, n div k) end
blanchet@33192
   183
  in fst oo aux end
blanchet@33192
   184
blanchet@33192
   185
val all_combinations = n_fold_cartesian_product o map (uncurry index_seq o swap)
blanchet@33192
   186
blanchet@33192
   187
fun all_permutations [] = [[]]
blanchet@33192
   188
  | all_permutations xs =
blanchet@33192
   189
    maps (fn j => map (cons (nth xs j)) (all_permutations (nth_drop j xs)))
blanchet@33192
   190
         (index_seq 0 (length xs))
blanchet@33192
   191
blanchet@33192
   192
fun batch_list _ [] = []
blanchet@33192
   193
  | batch_list k xs =
blanchet@33192
   194
    if length xs <= k then [xs]
blanchet@33192
   195
    else List.take (xs, k) :: batch_list k (List.drop (xs, k))
blanchet@33192
   196
blanchet@33192
   197
fun chunk_list_unevenly _ [] = []
blanchet@33192
   198
  | chunk_list_unevenly [] ys = map single ys
blanchet@33192
   199
  | chunk_list_unevenly (k :: ks) ys =
blanchet@33192
   200
    let val (ys1, ys2) = chop k ys in ys1 :: chunk_list_unevenly ks ys2 end
blanchet@33192
   201
blanchet@33192
   202
fun map3 _ [] [] [] = []
blanchet@33192
   203
  | map3 f (x :: xs) (y :: ys) (z :: zs) = f x y z :: map3 f xs ys zs
blanchet@33192
   204
  | map3 _ _ _ _ = raise UnequalLengths
blanchet@33192
   205
blanchet@33192
   206
fun double_lookup eq ps key =
blanchet@33192
   207
  case AList.lookup (fn (SOME x, SOME y) => eq (x, y) | _ => false) ps
blanchet@33192
   208
                    (SOME key) of
blanchet@33192
   209
    SOME z => SOME z
blanchet@33192
   210
  | NONE => ps |> find_first (is_none o fst) |> Option.map snd
blanchet@35220
   211
fun triple_lookup _ [(NONE, z)] _ = SOME z
blanchet@35220
   212
  | triple_lookup eq ps key =
blanchet@35220
   213
    case AList.lookup (op =) ps (SOME key) of
blanchet@35220
   214
      SOME z => SOME z
blanchet@35220
   215
    | NONE => double_lookup eq ps key
blanchet@33192
   216
blanchet@33192
   217
fun is_substring_of needle stack =
blanchet@33192
   218
  not (Substring.isEmpty (snd (Substring.position needle
blanchet@33192
   219
                                                  (Substring.full stack))))
blanchet@33192
   220
blanchet@36380
   221
val plural_s = Sledgehammer_Util.plural_s
blanchet@33192
   222
fun plural_s_for_list xs = plural_s (length xs)
blanchet@33192
   223
blanchet@36380
   224
val serial_commas = Sledgehammer_Util.serial_commas
blanchet@36380
   225
blanchet@36380
   226
val timestamp = Sledgehammer_Util.timestamp
blanchet@36380
   227
val parse_bool_option = Sledgehammer_Util.parse_bool_option
blanchet@36380
   228
val parse_time_option = Sledgehammer_Util.parse_time_option
blanchet@36380
   229
blanchet@33192
   230
fun flip_polarity Pos = Neg
blanchet@33192
   231
  | flip_polarity Neg = Pos
blanchet@33192
   232
  | flip_polarity Neut = Neut
blanchet@33192
   233
blanchet@33192
   234
val prop_T = @{typ prop}
blanchet@33192
   235
val bool_T = @{typ bool}
blanchet@33192
   236
val nat_T = @{typ nat}
blanchet@33192
   237
val int_T = @{typ int}
blanchet@33192
   238
blanchet@37260
   239
val simple_string_of_typ = Refute.string_of_typ
blanchet@37260
   240
val is_real_constr = Refute.is_IDT_constructor
blanchet@37260
   241
val typ_of_dtyp = Refute.typ_of_dtyp
blanchet@37260
   242
val is_of_class_const = Refute.is_const_of_class
blanchet@37260
   243
val get_class_def = Refute.get_classdef
blanchet@36555
   244
val monomorphic_term = Sledgehammer_Util.monomorphic_term
blanchet@36555
   245
val specialize_type = Sledgehammer_Util.specialize_type
blanchet@36555
   246
blanchet@33192
   247
val subscript = implode o map (prefix "\<^isub>") o explode
blanchet@34124
   248
fun nat_subscript n =
blanchet@34124
   249
  (* cheap trick to ensure proper alphanumeric ordering for one- and two-digit
blanchet@34124
   250
     numbers *)
blanchet@34124
   251
  if n <= 9 then "\<^bsub>" ^ signed_string_of_int n ^ "\<^esub>"
blanchet@34124
   252
  else subscript (string_of_int n)
blanchet@33192
   253
blanchet@34039
   254
fun time_limit NONE = I
blanchet@34039
   255
  | time_limit (SOME delay) = TimeLimit.timeLimit delay
blanchet@33192
   256
blanchet@33192
   257
fun DETERM_TIMEOUT delay tac st =
blanchet@33192
   258
  Seq.of_list (the_list (time_limit delay (fn () => SINGLE tac st) ()))
blanchet@33192
   259
blanchet@33192
   260
fun setmp_show_all_types f =
blanchet@33192
   261
  setmp_CRITICAL show_all_types
blanchet@33192
   262
                 (! show_types orelse ! show_sorts orelse ! show_all_types) f
blanchet@33192
   263
blanchet@33192
   264
val indent_size = 2
blanchet@33192
   265
blanchet@33192
   266
val pstrs = Pretty.breaks o map Pretty.str o space_explode " "
blanchet@33192
   267
blanchet@36483
   268
val unyxml = Sledgehammer_Util.unyxml
blanchet@36483
   269
val maybe_quote = Sledgehammer_Util.maybe_quote
blanchet@33192
   270
blanchet@36380
   271
(* This hash function is recommended in Compilers: Principles, Techniques, and
blanchet@36483
   272
   Tools, by Aho, Sethi, and Ullman. The "hashpjw" function, which they
blanchet@36380
   273
   particularly recommend, triggers a bug in versions of Poly/ML up to 4.2.0. *)
blanchet@36380
   274
fun hashw (u, w) = Word.+ (u, Word.* (0w65599, w))
blanchet@36380
   275
fun hashw_char (c, w) = hashw (Word.fromInt (Char.ord c), w)
blanchet@36380
   276
fun hashw_string (s:string, w) = CharVector.foldl hashw_char w s
blanchet@36380
   277
blanchet@33192
   278
end;