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