src/HOL/Tools/Nitpick/nitpick_util.ML
author wenzelm
Tue Jun 06 13:13:25 2017 +0200 (2017-06-06)
changeset 66020 a31760eee09d
parent 62519 a564458f94db
child 69593 3dda49e08b9d
permissions -rw-r--r--
discontinued obsolete print mode;
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
  datatype polarity = Pos | Neg | Neut
blanchet@33192
    11
blanchet@33192
    12
  exception ARG of string * string
blanchet@33192
    13
  exception BAD of string * string
blanchet@34124
    14
  exception TOO_SMALL of string * string
blanchet@34124
    15
  exception TOO_LARGE of string * string
blanchet@33192
    16
  exception NOT_SUPPORTED of string
blanchet@33192
    17
  exception SAME of unit
blanchet@33192
    18
blanchet@33192
    19
  val nitpick_prefix : string
blanchet@33192
    20
  val curry3 : ('a * 'b * 'c -> 'd) -> 'a -> 'b -> 'c -> 'd
blanchet@33705
    21
  val pairf : ('a -> 'b) -> ('a -> 'c) -> 'a -> 'b * 'c
blanchet@35385
    22
  val pair_from_fun : (bool -> 'a) -> 'a * 'a
blanchet@35385
    23
  val fun_from_pair : 'a * 'a -> bool -> 'a
blanchet@35385
    24
  val int_from_bool : bool -> int
blanchet@33705
    25
  val nat_minus : int -> int -> int
blanchet@33192
    26
  val reasonable_power : int -> int -> int
blanchet@33192
    27
  val exact_log : int -> int -> int
blanchet@33192
    28
  val exact_root : int -> int -> int
blanchet@33192
    29
  val offset_list : int list -> int list
blanchet@33192
    30
  val index_seq : int -> int -> int list
blanchet@33192
    31
  val filter_indices : int list -> 'a list -> 'a list
blanchet@33192
    32
  val filter_out_indices : int list -> 'a list -> 'a list
blanchet@33192
    33
  val fold1 : ('a -> 'a -> 'a) -> 'a list -> 'a
blanchet@33192
    34
  val replicate_list : int -> 'a list -> 'a list
blanchet@33192
    35
  val n_fold_cartesian_product : 'a list list -> 'a list list
blanchet@33192
    36
  val all_distinct_unordered_pairs_of : ''a list -> (''a * ''a) list
blanchet@33192
    37
  val nth_combination : (int * int) list -> int -> int list
blanchet@33192
    38
  val all_combinations : (int * int) list -> int list list
blanchet@33192
    39
  val all_permutations : 'a list -> 'a list list
blanchet@48323
    40
  val chunk_list : int -> 'a list -> 'a list list
blanchet@33192
    41
  val chunk_list_unevenly : int list -> 'a list -> 'a list list
blanchet@33192
    42
  val double_lookup :
blanchet@33192
    43
    ('a * 'a -> bool) -> ('a option * 'b) list -> 'a -> 'b option
blanchet@33192
    44
  val triple_lookup :
blanchet@33192
    45
    (''a * ''a -> bool) -> (''a option * 'b) list -> ''a -> 'b option
blanchet@33192
    46
  val is_substring_of : string -> string -> bool
blanchet@33192
    47
  val plural_s : int -> string
blanchet@33192
    48
  val plural_s_for_list : 'a list -> string
blanchet@36380
    49
  val serial_commas : string -> string list -> string list
blanchet@38188
    50
  val pretty_serial_commas : string -> Pretty.T list -> Pretty.T list
blanchet@36380
    51
  val parse_bool_option : bool -> string -> string -> bool option
blanchet@54816
    52
  val parse_time : string -> string -> Time.time
blanchet@52031
    53
  val string_of_time : Time.time -> string
blanchet@38652
    54
  val nat_subscript : int -> string
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@55080
    61
  val num_binder_types : typ -> int
blanchet@42697
    62
  val varify_type : Proof.context -> typ -> typ
blanchet@42697
    63
  val instantiate_type : theory -> typ -> typ -> typ -> typ
blanchet@42697
    64
  val varify_and_instantiate_type : Proof.context -> typ -> typ -> typ -> typ
blanchet@53806
    65
  val varify_and_instantiate_type_global : theory -> typ -> typ -> typ -> typ
blanchet@37260
    66
  val is_of_class_const : theory -> string * typ -> bool
blanchet@37260
    67
  val get_class_def : theory -> string -> (string * term) option
blanchet@37260
    68
  val specialize_type : theory -> string * typ -> term -> term
blanchet@38652
    69
  val eta_expand : typ list -> term -> int -> term
blanchet@54816
    70
  val DETERM_TIMEOUT : Time.time -> tactic -> tactic
blanchet@33192
    71
  val indent_size : int
wenzelm@58928
    72
  val pretty_maybe_quote : Keyword.keywords -> Pretty.T -> Pretty.T
blanchet@43827
    73
  val hash_term : term -> int
blanchet@53815
    74
  val spying : bool -> (unit -> Proof.state * int * string) -> unit
blanchet@35866
    75
end;
blanchet@33192
    76
blanchet@33232
    77
structure Nitpick_Util : NITPICK_UTIL =
blanchet@33192
    78
struct
blanchet@33192
    79
blanchet@33192
    80
datatype polarity = Pos | Neg | Neut
blanchet@33192
    81
blanchet@33192
    82
exception ARG of string * string
blanchet@33192
    83
exception BAD of string * string
blanchet@34124
    84
exception TOO_SMALL of string * string
blanchet@34124
    85
exception TOO_LARGE of string * string
blanchet@33192
    86
exception NOT_SUPPORTED of string
blanchet@33192
    87
exception SAME of unit
blanchet@33192
    88
wenzelm@46711
    89
val nitpick_prefix = "Nitpick" ^ Long_Name.separator
blanchet@33192
    90
blanchet@53802
    91
val timestamp = ATP_Util.timestamp
blanchet@53802
    92
blanchet@33192
    93
fun curry3 f = fn x => fn y => fn z => f (x, y, z)
blanchet@33192
    94
blanchet@33705
    95
fun pairf f g x = (f x, g x)
blanchet@33192
    96
blanchet@35385
    97
fun pair_from_fun f = (f false, f true)
blanchet@35385
    98
fun fun_from_pair (f, t) b = if b then t else f
blanchet@35385
    99
blanchet@35385
   100
fun int_from_bool b = if b then 1 else 0
blanchet@33705
   101
fun nat_minus i j = if i > j then i - j else 0
blanchet@33192
   102
blanchet@33192
   103
val max_exponent = 16384
blanchet@33192
   104
blanchet@35280
   105
fun reasonable_power _ 0 = 1
blanchet@33192
   106
  | reasonable_power a 1 = a
blanchet@33192
   107
  | reasonable_power 0 _ = 0
blanchet@33192
   108
  | reasonable_power 1 _ = 1
blanchet@33192
   109
  | reasonable_power a b =
blanchet@34124
   110
    if b < 0 then
blanchet@34124
   111
      raise ARG ("Nitpick_Util.reasonable_power",
blanchet@34124
   112
                 "negative exponent (" ^ signed_string_of_int b ^ ")")
blanchet@34124
   113
    else if b > max_exponent then
blanchet@34124
   114
      raise TOO_LARGE ("Nitpick_Util.reasonable_power",
blanchet@47667
   115
                       "too large exponent (" ^ signed_string_of_int a ^ " ^ " ^
blanchet@47667
   116
                       signed_string_of_int b ^ ")")
blanchet@33192
   117
    else
blanchet@34124
   118
      let val c = reasonable_power a (b div 2) in
blanchet@34124
   119
        c * c * reasonable_power a (b mod 2)
blanchet@34124
   120
      end
blanchet@33192
   121
blanchet@33192
   122
fun exact_log m n =
blanchet@33192
   123
  let
blanchet@33192
   124
    val r = Math.ln (Real.fromInt n) / Math.ln (Real.fromInt m) |> Real.round
blanchet@33192
   125
  in
blanchet@33192
   126
    if reasonable_power m r = n then
blanchet@33192
   127
      r
blanchet@33192
   128
    else
blanchet@33232
   129
      raise ARG ("Nitpick_Util.exact_log",
blanchet@33192
   130
                 commas (map signed_string_of_int [m, n]))
blanchet@33192
   131
  end
blanchet@33192
   132
blanchet@33192
   133
fun exact_root m n =
blanchet@33192
   134
  let val r = Math.pow (Real.fromInt n, 1.0 / (Real.fromInt m)) |> Real.round in
blanchet@33192
   135
    if reasonable_power r m = n then
blanchet@33192
   136
      r
blanchet@33192
   137
    else
blanchet@33232
   138
      raise ARG ("Nitpick_Util.exact_root",
blanchet@33192
   139
                 commas (map signed_string_of_int [m, n]))
blanchet@33192
   140
  end
blanchet@33192
   141
blanchet@33192
   142
fun fold1 f = foldl1 (uncurry f)
blanchet@33192
   143
blanchet@33192
   144
fun replicate_list 0 _ = []
blanchet@33192
   145
  | replicate_list n xs = xs @ replicate_list (n - 1) xs
blanchet@33192
   146
blanchet@33192
   147
fun offset_list ns = rev (tl (fold (fn x => fn xs => (x + hd xs) :: xs) ns [0]))
blanchet@55889
   148
blanchet@33192
   149
fun index_seq j0 n = if j0 < 0 then j0 downto j0 - n + 1 else j0 upto j0 + n - 1
blanchet@33192
   150
blanchet@33192
   151
fun filter_indices js xs =
blanchet@33192
   152
  let
blanchet@33192
   153
    fun aux _ [] _ = []
blanchet@33192
   154
      | aux i (j :: js) (x :: xs) =
blanchet@33192
   155
        if i = j then x :: aux (i + 1) js xs else aux (i + 1) (j :: js) xs
blanchet@33232
   156
      | aux _ _ _ = raise ARG ("Nitpick_Util.filter_indices",
blanchet@33192
   157
                               "indices unordered or out of range")
blanchet@33192
   158
  in aux 0 js xs end
blanchet@55889
   159
blanchet@33192
   160
fun filter_out_indices js xs =
blanchet@33192
   161
  let
blanchet@33192
   162
    fun aux _ [] xs = xs
blanchet@33192
   163
      | aux i (j :: js) (x :: xs) =
blanchet@33192
   164
        if i = j then aux (i + 1) js xs else x :: aux (i + 1) (j :: js) xs
blanchet@33232
   165
      | aux _ _ _ = raise ARG ("Nitpick_Util.filter_out_indices",
blanchet@33192
   166
                               "indices unordered or out of range")
blanchet@33192
   167
  in aux 0 js xs end
blanchet@33192
   168
blanchet@57055
   169
fun cartesian_product [] _ = []
blanchet@57055
   170
  | cartesian_product (x :: xs) yss = map (cons x) yss @ cartesian_product xs yss
blanchet@57055
   171
blanchet@57055
   172
fun n_fold_cartesian_product xss = fold_rev cartesian_product xss [[]]
blanchet@54695
   173
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@49206
   192
(* FIXME: use "Library.chop_groups" *)
blanchet@48323
   193
val chunk_list = ATP_Util.chunk_list
blanchet@33192
   194
blanchet@49206
   195
(* FIXME: use "Library.unflat" *)
blanchet@33192
   196
fun chunk_list_unevenly _ [] = []
blanchet@48323
   197
  | chunk_list_unevenly [] xs = map single xs
blanchet@48323
   198
  | chunk_list_unevenly (k :: ks) xs =
blanchet@48323
   199
    let val (xs1, xs2) = chop k xs in xs1 :: chunk_list_unevenly ks xs2 end
blanchet@33192
   200
blanchet@33192
   201
fun double_lookup eq ps key =
blanchet@33192
   202
  case AList.lookup (fn (SOME x, SOME y) => eq (x, y) | _ => false) ps
blanchet@33192
   203
                    (SOME key) of
blanchet@33192
   204
    SOME z => SOME z
blanchet@33192
   205
  | NONE => ps |> find_first (is_none o fst) |> Option.map snd
blanchet@55889
   206
blanchet@35220
   207
fun triple_lookup _ [(NONE, z)] _ = SOME z
blanchet@35220
   208
  | triple_lookup eq ps key =
blanchet@35220
   209
    case AList.lookup (op =) ps (SOME key) of
blanchet@35220
   210
      SOME z => SOME z
blanchet@35220
   211
    | NONE => double_lookup eq ps key
blanchet@33192
   212
blanchet@33192
   213
fun is_substring_of needle stack =
blanchet@33192
   214
  not (Substring.isEmpty (snd (Substring.position needle
blanchet@33192
   215
                                                  (Substring.full stack))))
blanchet@33192
   216
blanchet@36380
   217
val plural_s = Sledgehammer_Util.plural_s
blanchet@33192
   218
fun plural_s_for_list xs = plural_s (length xs)
blanchet@33192
   219
blanchet@43029
   220
val serial_commas = Try.serial_commas
blanchet@36380
   221
blanchet@38188
   222
fun pretty_serial_commas _ [] = []
blanchet@38188
   223
  | pretty_serial_commas _ [p] = [p]
blanchet@38188
   224
  | pretty_serial_commas conj [p1, p2] =
blanchet@38188
   225
    [p1, Pretty.brk 1, Pretty.str conj, Pretty.brk 1, p2]
blanchet@38188
   226
  | pretty_serial_commas conj [p1, p2, p3] =
blanchet@38188
   227
    [p1, Pretty.str ",", Pretty.brk 1, p2, Pretty.str ",", Pretty.brk 1,
blanchet@38188
   228
     Pretty.str conj, Pretty.brk 1, p3]
blanchet@38188
   229
  | pretty_serial_commas conj (p :: ps) =
blanchet@38188
   230
    p :: Pretty.str "," :: Pretty.brk 1 :: pretty_serial_commas conj ps
blanchet@38188
   231
blanchet@36380
   232
val parse_bool_option = Sledgehammer_Util.parse_bool_option
blanchet@54816
   233
val parse_time = Sledgehammer_Util.parse_time
blanchet@52031
   234
val string_of_time = ATP_Util.string_of_time
blanchet@36380
   235
wenzelm@53021
   236
val subscript = implode o map (prefix "\<^sub>") o Symbol.explode
blanchet@55889
   237
blanchet@38652
   238
fun nat_subscript n =
wenzelm@66020
   239
  n |> signed_string_of_int |> not (print_mode_active Print_Mode.ASCII) ? subscript
blanchet@38652
   240
blanchet@33192
   241
fun flip_polarity Pos = Neg
blanchet@33192
   242
  | flip_polarity Neg = Pos
blanchet@33192
   243
  | flip_polarity Neut = Neut
blanchet@33192
   244
blanchet@33192
   245
val prop_T = @{typ prop}
blanchet@33192
   246
val bool_T = @{typ bool}
blanchet@33192
   247
val nat_T = @{typ nat}
blanchet@33192
   248
val int_T = @{typ int}
blanchet@33192
   249
blanchet@55080
   250
fun simple_string_of_typ (Type (s, _)) = s
blanchet@55080
   251
  | simple_string_of_typ (TFree (s, _)) = s
blanchet@49985
   252
  | simple_string_of_typ (TVar ((s, _), _)) = s
blanchet@49985
   253
blanchet@55080
   254
val num_binder_types = BNF_Util.num_binder_types
blanchet@55080
   255
blanchet@43085
   256
val varify_type = ATP_Util.varify_type
blanchet@43085
   257
val instantiate_type = ATP_Util.instantiate_type
blanchet@43085
   258
val varify_and_instantiate_type = ATP_Util.varify_and_instantiate_type
blanchet@49985
   259
blanchet@53806
   260
fun varify_and_instantiate_type_global thy T1 T1' T2 =
blanchet@53806
   261
  instantiate_type thy (Logic.varifyT_global T1) T1' (Logic.varifyT_global T2)
blanchet@53806
   262
blanchet@49985
   263
fun is_of_class_const thy (s, _) =
blanchet@49985
   264
  member (op =) (map Logic.const_of_class (Sign.all_classes thy)) s
blanchet@49985
   265
blanchet@49985
   266
fun get_class_def thy class =
blanchet@49985
   267
  let val axname = class ^ "_class_def" in
blanchet@49985
   268
    Option.map (pair axname)
blanchet@49985
   269
      (AList.lookup (op =) (Theory.all_axioms_of thy) axname)
blanchet@49985
   270
  end;
blanchet@49985
   271
blanchet@43085
   272
val specialize_type = ATP_Util.specialize_type
blanchet@43085
   273
val eta_expand = ATP_Util.eta_expand
blanchet@33192
   274
blanchet@33192
   275
fun DETERM_TIMEOUT delay tac st =
wenzelm@62519
   276
  Seq.of_list (the_list (Timeout.apply delay (fn () => SINGLE tac st) ()))
blanchet@33192
   277
blanchet@33192
   278
val indent_size = 2
blanchet@33192
   279
blanchet@43085
   280
val maybe_quote = ATP_Util.maybe_quote
blanchet@55889
   281
wenzelm@58928
   282
fun pretty_maybe_quote keywords pretty =
wenzelm@61877
   283
  let val s = Pretty.unformatted_string_of pretty
wenzelm@61877
   284
  in if maybe_quote keywords s = s then pretty else Pretty.quote pretty end
blanchet@33192
   285
blanchet@53802
   286
val hashw = ATP_Util.hashw
blanchet@53802
   287
val hashw_string = ATP_Util.hashw_string
blanchet@53802
   288
blanchet@53802
   289
fun hashw_term (t1 $ t2) = hashw (hashw_term t1, hashw_term t2)
blanchet@53802
   290
  | hashw_term (Const (s, _)) = hashw_string (s, 0w0)
blanchet@53802
   291
  | hashw_term (Free (s, _)) = hashw_string (s, 0w0)
blanchet@53505
   292
  | hashw_term _ = 0w0
blanchet@53505
   293
blanchet@53505
   294
val hash_term = Word.toInt o hashw_term
blanchet@36380
   295
blanchet@53815
   296
val hackish_string_of_term = Sledgehammer_Util.hackish_string_of_term
blanchet@53815
   297
blanchet@53815
   298
val spying_version = "b"
blanchet@53815
   299
blanchet@53815
   300
fun spying false _ = ()
blanchet@53815
   301
  | spying true f =
blanchet@53815
   302
    let
blanchet@53815
   303
      val (state, i, message) = f ()
blanchet@53815
   304
      val ctxt = Proof.context_of state
wenzelm@59582
   305
      val goal = Logic.get_goal (Thm.prop_of (#goal (Proof.goal state))) i
blanchet@53815
   306
      val hash = String.substring (SHA1.rep (SHA1.digest (hackish_string_of_term ctxt goal)), 0, 12)
blanchet@53815
   307
    in
blanchet@53815
   308
      File.append (Path.explode "$ISABELLE_HOME_USER/spy_nitpick")
blanchet@53815
   309
        (spying_version ^ " " ^ timestamp () ^ ": " ^ hash ^ ": " ^ message ^ "\n")
blanchet@53815
   310
    end
blanchet@53815
   311
blanchet@33192
   312
end;