src/HOL/Tools/Nitpick/nitpick_util.ML
author blanchet
Fri Mar 19 15:07:44 2010 +0100 (2010-03-19)
changeset 35866 513074557e06
parent 35807 e4d1b5cbd429
child 35964 77f2cb359b49
permissions -rw-r--r--
move the Sledgehammer Isar commands together into one file;
this will make easier to add options and reorganize them later
     1 (*  Title:      HOL/Tools/Nitpick/nitpick_util.ML
     2     Author:     Jasmin Blanchette, TU Muenchen
     3     Copyright   2008, 2009, 2010
     4 
     5 General-purpose functions used by the Nitpick modules.
     6 *)
     7 
     8 signature NITPICK_UTIL =
     9 sig
    10   type styp = string * typ
    11   datatype polarity = Pos | Neg | Neut
    12 
    13   exception ARG of string * string
    14   exception BAD of string * string
    15   exception TOO_SMALL of string * string
    16   exception TOO_LARGE of string * string
    17   exception NOT_SUPPORTED of string
    18   exception SAME of unit
    19 
    20   val nitpick_prefix : string
    21   val curry3 : ('a * 'b * 'c -> 'd) -> 'a -> 'b -> 'c -> 'd
    22   val pairf : ('a -> 'b) -> ('a -> 'c) -> 'a -> 'b * 'c
    23   val pair_from_fun : (bool -> 'a) -> 'a * 'a
    24   val fun_from_pair : 'a * 'a -> bool -> 'a
    25   val int_from_bool : bool -> int
    26   val nat_minus : int -> int -> int
    27   val reasonable_power : int -> int -> int
    28   val exact_log : int -> int -> int
    29   val exact_root : int -> int -> int
    30   val offset_list : int list -> int list
    31   val index_seq : int -> int -> int list
    32   val filter_indices : int list -> 'a list -> 'a list
    33   val filter_out_indices : int list -> 'a list -> 'a list
    34   val fold1 : ('a -> 'a -> 'a) -> 'a list -> 'a
    35   val replicate_list : int -> 'a list -> 'a list
    36   val n_fold_cartesian_product : 'a list list -> 'a list list
    37   val all_distinct_unordered_pairs_of : ''a list -> (''a * ''a) list
    38   val nth_combination : (int * int) list -> int -> int list
    39   val all_combinations : (int * int) list -> int list list
    40   val all_permutations : 'a list -> 'a list list
    41   val batch_list : int -> 'a list -> 'a list list
    42   val chunk_list_unevenly : int list -> 'a list -> 'a list list
    43   val map3 : ('a -> 'b -> 'c -> 'd) -> 'a list -> 'b list -> 'c list -> 'd list
    44   val double_lookup :
    45     ('a * 'a -> bool) -> ('a option * 'b) list -> 'a -> 'b option
    46   val triple_lookup :
    47     (''a * ''a -> bool) -> (''a option * 'b) list -> ''a -> 'b option
    48   val is_substring_of : string -> string -> bool
    49   val serial_commas : string -> string list -> string list
    50   val plural_s : int -> string
    51   val plural_s_for_list : 'a list -> string
    52   val flip_polarity : polarity -> polarity
    53   val prop_T : typ
    54   val bool_T : typ
    55   val nat_T : typ
    56   val int_T : typ
    57   val nat_subscript : int -> string
    58   val time_limit : Time.time option -> ('a -> 'b) -> 'a -> 'b
    59   val DETERM_TIMEOUT : Time.time option -> tactic -> tactic
    60   val setmp_show_all_types : ('a -> 'b) -> 'a -> 'b
    61   val indent_size : int
    62   val pstrs : string -> Pretty.T list
    63   val unyxml : string -> string
    64   val maybe_quote : string -> string
    65 end;
    66 
    67 structure Nitpick_Util : NITPICK_UTIL =
    68 struct
    69 
    70 type styp = string * typ
    71 
    72 datatype polarity = Pos | Neg | Neut
    73 
    74 exception ARG of string * string
    75 exception BAD of string * string
    76 exception TOO_SMALL of string * string
    77 exception TOO_LARGE of string * string
    78 exception NOT_SUPPORTED of string
    79 exception SAME of unit
    80 
    81 val nitpick_prefix = "Nitpick."
    82 
    83 (* ('a * 'b * 'c -> 'd) -> 'a -> 'b -> 'c -> 'd *)
    84 fun curry3 f = fn x => fn y => fn z => f (x, y, z)
    85 
    86 (* ('a -> 'b) -> ('a -> 'c) -> 'a -> 'b * 'c *)
    87 fun pairf f g x = (f x, g x)
    88 
    89 (* (bool -> 'a) -> 'a * 'a *)
    90 fun pair_from_fun f = (f false, f true)
    91 (* 'a * 'a -> bool -> 'a *)
    92 fun fun_from_pair (f, t) b = if b then t else f
    93 
    94 (* bool -> int *)
    95 fun int_from_bool b = if b then 1 else 0
    96 (* int -> int -> int *)
    97 fun nat_minus i j = if i > j then i - j else 0
    98 
    99 val max_exponent = 16384
   100 
   101 (* int -> int -> int *)
   102 fun reasonable_power _ 0 = 1
   103   | reasonable_power a 1 = a
   104   | reasonable_power 0 _ = 0
   105   | reasonable_power 1 _ = 1
   106   | reasonable_power a b =
   107     if b < 0 then
   108       raise ARG ("Nitpick_Util.reasonable_power",
   109                  "negative exponent (" ^ signed_string_of_int b ^ ")")
   110     else if b > max_exponent then
   111       raise TOO_LARGE ("Nitpick_Util.reasonable_power",
   112                        "too large exponent (" ^ signed_string_of_int b ^ ")")
   113     else
   114       let val c = reasonable_power a (b div 2) in
   115         c * c * reasonable_power a (b mod 2)
   116       end
   117 
   118 (* int -> int -> int *)
   119 fun exact_log m n =
   120   let
   121     val r = Math.ln (Real.fromInt n) / Math.ln (Real.fromInt m) |> Real.round
   122   in
   123     if reasonable_power m r = n then
   124       r
   125     else
   126       raise ARG ("Nitpick_Util.exact_log",
   127                  commas (map signed_string_of_int [m, n]))
   128   end
   129 
   130 (* int -> int -> int *)
   131 fun exact_root m n =
   132   let val r = Math.pow (Real.fromInt n, 1.0 / (Real.fromInt m)) |> Real.round in
   133     if reasonable_power r m = n then
   134       r
   135     else
   136       raise ARG ("Nitpick_Util.exact_root",
   137                  commas (map signed_string_of_int [m, n]))
   138   end
   139 
   140 (* ('a -> 'a -> 'a) -> 'a list -> 'a *)
   141 fun fold1 f = foldl1 (uncurry f)
   142 
   143 (* int -> 'a list -> 'a list *)
   144 fun replicate_list 0 _ = []
   145   | replicate_list n xs = xs @ replicate_list (n - 1) xs
   146 
   147 (* int list -> int list *)
   148 fun offset_list ns = rev (tl (fold (fn x => fn xs => (x + hd xs) :: xs) ns [0]))
   149 (* int -> int -> int list *)
   150 fun index_seq j0 n = if j0 < 0 then j0 downto j0 - n + 1 else j0 upto j0 + n - 1
   151 
   152 (* int list -> 'a list -> 'a list *)
   153 fun filter_indices js xs =
   154   let
   155     (* int -> int list -> 'a list -> 'a list *)
   156     fun aux _ [] _ = []
   157       | aux i (j :: js) (x :: xs) =
   158         if i = j then x :: aux (i + 1) js xs else aux (i + 1) (j :: js) xs
   159       | aux _ _ _ = raise ARG ("Nitpick_Util.filter_indices",
   160                                "indices unordered or out of range")
   161   in aux 0 js xs end
   162 fun filter_out_indices js xs =
   163   let
   164     (* int -> int list -> 'a list -> 'a list *)
   165     fun aux _ [] xs = xs
   166       | aux i (j :: js) (x :: xs) =
   167         if i = j then aux (i + 1) js xs else x :: aux (i + 1) (j :: js) xs
   168       | aux _ _ _ = raise ARG ("Nitpick_Util.filter_out_indices",
   169                                "indices unordered or out of range")
   170   in aux 0 js xs end
   171 
   172 (* 'a list -> 'a list list -> 'a list list *)
   173 fun cartesian_product [] _ = []
   174   | cartesian_product (x :: xs) yss =
   175     map (cons x) yss @ cartesian_product xs yss
   176 (* 'a list list -> 'a list list *)
   177 fun n_fold_cartesian_product xss = fold_rev cartesian_product xss [[]]
   178 (* ''a list -> (''a * ''a) list *)
   179 fun all_distinct_unordered_pairs_of [] = []
   180   | all_distinct_unordered_pairs_of (x :: xs) =
   181     map (pair x) xs @ all_distinct_unordered_pairs_of xs
   182 
   183 (* (int * int) list -> int -> int list *)
   184 val nth_combination =
   185   let
   186     (* (int * int) list -> int -> int list * int *)
   187     fun aux [] n = ([], n)
   188       | aux ((k, j0) :: xs) n =
   189         let val (js, n) = aux xs n in ((n mod k) + j0 :: js, n div k) end
   190   in fst oo aux end
   191 
   192 (* (int * int) list -> int list list *)
   193 val all_combinations = n_fold_cartesian_product o map (uncurry index_seq o swap)
   194 
   195 (* 'a list -> 'a list list *)
   196 fun all_permutations [] = [[]]
   197   | all_permutations xs =
   198     maps (fn j => map (cons (nth xs j)) (all_permutations (nth_drop j xs)))
   199          (index_seq 0 (length xs))
   200 
   201 (* int -> 'a list -> 'a list list *)
   202 fun batch_list _ [] = []
   203   | batch_list k xs =
   204     if length xs <= k then [xs]
   205     else List.take (xs, k) :: batch_list k (List.drop (xs, k))
   206 
   207 (* int list -> 'a list -> 'a list list *)
   208 fun chunk_list_unevenly _ [] = []
   209   | chunk_list_unevenly [] ys = map single ys
   210   | chunk_list_unevenly (k :: ks) ys =
   211     let val (ys1, ys2) = chop k ys in ys1 :: chunk_list_unevenly ks ys2 end
   212 
   213 (* ('a -> 'b -> 'c -> 'd) -> 'a list -> 'b list -> 'c list -> 'd list *)
   214 fun map3 _ [] [] [] = []
   215   | map3 f (x :: xs) (y :: ys) (z :: zs) = f x y z :: map3 f xs ys zs
   216   | map3 _ _ _ _ = raise UnequalLengths
   217 
   218 (* ('a * 'a -> bool) -> ('a option * 'b) list -> 'a -> 'b option *)
   219 fun double_lookup eq ps key =
   220   case AList.lookup (fn (SOME x, SOME y) => eq (x, y) | _ => false) ps
   221                     (SOME key) of
   222     SOME z => SOME z
   223   | NONE => ps |> find_first (is_none o fst) |> Option.map snd
   224 (* (''a * ''a -> bool) -> (''a option * 'b) list -> ''a -> 'b option *)
   225 fun triple_lookup _ [(NONE, z)] _ = SOME z
   226   | triple_lookup eq ps key =
   227     case AList.lookup (op =) ps (SOME key) of
   228       SOME z => SOME z
   229     | NONE => double_lookup eq ps key
   230 
   231 (* string -> string -> bool *)
   232 fun is_substring_of needle stack =
   233   not (Substring.isEmpty (snd (Substring.position needle
   234                                                   (Substring.full stack))))
   235 
   236 (* string -> string list -> string list *)
   237 fun serial_commas _ [] = ["??"]
   238   | serial_commas _ [s] = [s]
   239   | serial_commas conj [s1, s2] = [s1, conj, s2]
   240   | serial_commas conj [s1, s2, s3] = [s1 ^ ",", s2 ^ ",", conj, s3]
   241   | serial_commas conj (s :: ss) = s ^ "," :: serial_commas conj ss
   242 
   243 (* int -> string *)
   244 fun plural_s n = if n = 1 then "" else "s"
   245 (* 'a list -> string *)
   246 fun plural_s_for_list xs = plural_s (length xs)
   247 
   248 (* polarity -> polarity *)
   249 fun flip_polarity Pos = Neg
   250   | flip_polarity Neg = Pos
   251   | flip_polarity Neut = Neut
   252 
   253 val prop_T = @{typ prop}
   254 val bool_T = @{typ bool}
   255 val nat_T = @{typ nat}
   256 val int_T = @{typ int}
   257 
   258 (* string -> string *)
   259 val subscript = implode o map (prefix "\<^isub>") o explode
   260 (* int -> string *)
   261 fun nat_subscript n =
   262   (* cheap trick to ensure proper alphanumeric ordering for one- and two-digit
   263      numbers *)
   264   if n <= 9 then "\<^bsub>" ^ signed_string_of_int n ^ "\<^esub>"
   265   else subscript (string_of_int n)
   266 
   267 (* Time.time option -> ('a -> 'b) -> 'a -> 'b *)
   268 fun time_limit NONE = I
   269   | time_limit (SOME delay) = TimeLimit.timeLimit delay
   270 
   271 (* Time.time option -> tactic -> tactic *)
   272 fun DETERM_TIMEOUT delay tac st =
   273   Seq.of_list (the_list (time_limit delay (fn () => SINGLE tac st) ()))
   274 
   275 (* ('a -> 'b) -> 'a -> 'b *)
   276 fun setmp_show_all_types f =
   277   setmp_CRITICAL show_all_types
   278                  (! show_types orelse ! show_sorts orelse ! show_all_types) f
   279 
   280 val indent_size = 2
   281 
   282 (* string -> Pretty.T list *)
   283 val pstrs = Pretty.breaks o map Pretty.str o space_explode " "
   284 
   285 (* XML.tree -> string *)
   286 fun plain_string_from_xml_tree t =
   287   Buffer.empty |> XML.add_content t |> Buffer.content
   288 (* string -> string *)
   289 val unyxml = plain_string_from_xml_tree o YXML.parse
   290 
   291 (* string -> bool *)
   292 val is_long_identifier = forall Syntax.is_identifier o space_explode "."
   293 (* string -> string *)
   294 fun maybe_quote y =
   295   let val s = unyxml y in
   296     y |> ((not (is_long_identifier (perhaps (try (unprefix "'")) s)) andalso
   297            not (is_long_identifier (perhaps (try (unprefix "?")) s))) orelse
   298            OuterKeyword.is_keyword s) ? quote
   299   end
   300 
   301 end;