src/HOL/Tools/Nitpick/nitpick_isar.ML
author blanchet
Mon, 21 Feb 2011 17:36:32 +0100
changeset 42674 ef13e3b7cbaf
parent 42672 ed77524f3429
child 42727 7244589c8ccc
permissions -rw-r--r--
more work on "fix_datatype_vals" optimization (renamed "preconstruct")
blanchet@33982
     1
(*  Title:      HOL/Tools/Nitpick/nitpick_isar.ML
blanchet@33192
     2
    Author:     Jasmin Blanchette, TU Muenchen
blanchet@34969
     3
    Copyright   2008, 2009, 2010
blanchet@33192
     4
blanchet@33192
     5
Adds the "nitpick" and "nitpick_params" commands to Isabelle/Isar's outer
blanchet@33192
     6
syntax.
blanchet@33192
     7
*)
blanchet@33192
     8
blanchet@33192
     9
signature NITPICK_ISAR =
blanchet@33192
    10
sig
blanchet@33192
    11
  type params = Nitpick.params
blanchet@33192
    12
blanchet@39562
    13
  val auto : bool Unsynchronized.ref
blanchet@33192
    14
  val default_params : theory -> (string * string) list -> params
blanchet@33552
    15
  val setup : theory -> theory
blanchet@35866
    16
end;
blanchet@33192
    17
blanchet@33224
    18
structure Nitpick_Isar : NITPICK_ISAR =
blanchet@33192
    19
struct
blanchet@33192
    20
blanchet@33224
    21
open Nitpick_Util
blanchet@33224
    22
open Nitpick_HOL
blanchet@33224
    23
open Nitpick_Rep
blanchet@33224
    24
open Nitpick_Nut
blanchet@33192
    25
open Nitpick
blanchet@33192
    26
blanchet@39562
    27
val auto = Unsynchronized.ref false
blanchet@33552
    28
blanchet@39590
    29
(* Maximum number of scopes for Auto Nitpick. Be frugal since it has to share
blanchet@39590
    30
   its time slot with several other automatic tools. *)
blanchet@39590
    31
val max_auto_scopes = 6
blanchet@39590
    32
wenzelm@33601
    33
val _ =
wenzelm@33601
    34
  ProofGeneralPgip.add_preference Preferences.category_tracing
blanchet@34969
    35
      (Preferences.bool_pref auto "auto-nitpick"
blanchet@39574
    36
           "Run Nitpick automatically.")
blanchet@33552
    37
blanchet@33192
    38
type raw_param = string * string list
blanchet@33192
    39
blanchet@33192
    40
val default_default_params =
blanchet@38407
    41
  [("card", "1\<midarrow>10"),
blanchet@38407
    42
   ("iter", "0,1,2,4,8,12,16,20,24,28"),
blanchet@38407
    43
   ("bits", "1,2,3,4,6,8,10,12,14,16"),
blanchet@38407
    44
   ("bisim_depth", "9"),
blanchet@35962
    45
   ("box", "smart"),
blanchet@35962
    46
   ("finitize", "smart"),
blanchet@35962
    47
   ("mono", "smart"),
blanchet@35962
    48
   ("std", "true"),
blanchet@35962
    49
   ("wf", "smart"),
blanchet@35962
    50
   ("sat_solver", "smart"),
blanchet@35962
    51
   ("batch_size", "smart"),
blanchet@35962
    52
   ("blocking", "true"),
blanchet@35962
    53
   ("falsify", "true"),
blanchet@35962
    54
   ("user_axioms", "smart"),
blanchet@35962
    55
   ("assms", "true"),
blanchet@35962
    56
   ("merge_type_vars", "false"),
blanchet@35962
    57
   ("binary_ints", "smart"),
blanchet@35962
    58
   ("destroy_constrs", "true"),
blanchet@35962
    59
   ("specialize", "true"),
blanchet@35962
    60
   ("star_linear_preds", "true"),
blanchet@42674
    61
   ("preconstr", "smart"),
blanchet@35962
    62
   ("peephole_optim", "true"),
blanchet@38373
    63
   ("datatype_sym_break", "5"),
blanchet@38373
    64
   ("kodkod_sym_break", "15"),
blanchet@40582
    65
   ("timeout", "30"),
blanchet@40582
    66
   ("tac_timeout", "0.5"),
blanchet@35962
    67
   ("max_threads", "0"),
blanchet@35962
    68
   ("debug", "false"),
blanchet@35962
    69
   ("verbose", "false"),
blanchet@35962
    70
   ("overlord", "false"),
blanchet@35962
    71
   ("show_datatypes", "false"),
blanchet@35962
    72
   ("show_consts", "false"),
blanchet@35962
    73
   ("format", "1"),
blanchet@35962
    74
   ("max_potential", "1"),
blanchet@35962
    75
   ("max_genuine", "1"),
blanchet@35962
    76
   ("check_potential", "false"),
blanchet@35962
    77
   ("check_genuine", "false")]
blanchet@33192
    78
blanchet@33192
    79
val negated_params =
blanchet@33192
    80
  [("dont_box", "box"),
blanchet@35665
    81
   ("dont_finitize", "finitize"),
blanchet@33192
    82
   ("non_mono", "mono"),
blanchet@34969
    83
   ("non_std", "std"),
blanchet@33192
    84
   ("non_wf", "wf"),
blanchet@33192
    85
   ("non_blocking", "blocking"),
blanchet@33192
    86
   ("satisfy", "falsify"),
blanchet@33192
    87
   ("no_user_axioms", "user_axioms"),
blanchet@33192
    88
   ("no_assms", "assms"),
blanchet@33547
    89
   ("dont_merge_type_vars", "merge_type_vars"),
blanchet@34121
    90
   ("unary_ints", "binary_ints"),
blanchet@33192
    91
   ("dont_destroy_constrs", "destroy_constrs"),
blanchet@33192
    92
   ("dont_specialize", "specialize"),
blanchet@33192
    93
   ("dont_star_linear_preds", "star_linear_preds"),
blanchet@42674
    94
   ("dont_preconstr", "preconstr"),
blanchet@33192
    95
   ("no_peephole_optim", "peephole_optim"),
blanchet@35962
    96
   ("no_debug", "debug"),
blanchet@33192
    97
   ("quiet", "verbose"),
blanchet@33192
    98
   ("no_overlord", "overlord"),
blanchet@33192
    99
   ("hide_datatypes", "show_datatypes"),
blanchet@33192
   100
   ("hide_consts", "show_consts"),
blanchet@33192
   101
   ("trust_potential", "check_potential"),
blanchet@33192
   102
   ("trust_genuine", "check_genuine")]
blanchet@33192
   103
blanchet@33192
   104
fun is_known_raw_param s =
blanchet@34923
   105
  AList.defined (op =) default_default_params s orelse
blanchet@34923
   106
  AList.defined (op =) negated_params s orelse
blanchet@42674
   107
  member (op =) ["max", "show_all", "whack", "eval", "atoms", "expect"] s orelse
blanchet@34923
   108
  exists (fn p => String.isPrefix (p ^ " ") s)
blanchet@35665
   109
         ["card", "max", "iter", "box", "dont_box", "finitize", "dont_finitize",
blanchet@42674
   110
          "mono", "non_mono", "std", "non_std", "wf", "non_wf", "preconstr",
blanchet@42674
   111
          "dont_preconstr", "format", "atoms"]
blanchet@33192
   112
blanchet@33192
   113
fun check_raw_param (s, _) =
blanchet@33192
   114
  if is_known_raw_param s then ()
blanchet@39562
   115
  else error ("Unknown parameter: " ^ quote s ^ ".")
blanchet@33192
   116
blanchet@33192
   117
fun unnegate_param_name name =
blanchet@33192
   118
  case AList.lookup (op =) negated_params name of
blanchet@33192
   119
    NONE => if String.isPrefix "dont_" name then SOME (unprefix "dont_" name)
blanchet@33192
   120
            else if String.isPrefix "non_" name then SOME (unprefix "non_" name)
blanchet@33192
   121
            else NONE
blanchet@33192
   122
  | some_name => some_name
blanchet@37163
   123
fun normalize_raw_param (name, value) =
blanchet@33192
   124
  case unnegate_param_name name of
blanchet@37163
   125
    SOME name' => [(name', case value of
blanchet@37163
   126
                             ["false"] => ["true"]
blanchet@37163
   127
                           | ["true"] => ["false"]
blanchet@37163
   128
                           | [] => ["false"]
blanchet@37163
   129
                           | _ => value)]
blanchet@37163
   130
  | NONE => if name = "show_all" then
blanchet@37163
   131
              [("show_datatypes", value), ("show_consts", value)]
blanchet@37163
   132
            else
blanchet@37163
   133
              [(name, value)]
blanchet@33192
   134
wenzelm@41720
   135
structure Data = Theory_Data
wenzelm@41720
   136
(
blanchet@35962
   137
  type T = raw_param list
blanchet@36391
   138
  val empty = map (apsnd single) default_default_params
blanchet@33192
   139
  val extend = I
wenzelm@41720
   140
  fun merge data = AList.merge (op =) (K true) data
wenzelm@41720
   141
)
blanchet@33192
   142
blanchet@37163
   143
val set_default_raw_param =
blanchet@37163
   144
  Data.map o fold (AList.update (op =)) o normalize_raw_param
blanchet@35962
   145
val default_raw_params = Data.get
blanchet@33192
   146
blanchet@33192
   147
fun is_punctuation s = (s = "," orelse s = "-" orelse s = "\<midarrow>")
blanchet@33192
   148
blanchet@33192
   149
fun stringify_raw_param_value [] = ""
blanchet@33192
   150
  | stringify_raw_param_value [s] = s
blanchet@33192
   151
  | stringify_raw_param_value (s1 :: s2 :: ss) =
blanchet@33192
   152
    s1 ^ (if is_punctuation s1 orelse is_punctuation s2 then "" else " ") ^
blanchet@33192
   153
    stringify_raw_param_value (s2 :: ss)
blanchet@33192
   154
blanchet@33192
   155
fun maxed_int_from_string min_int s = Int.max (min_int, the (Int.fromString s))
blanchet@33192
   156
blanchet@33192
   157
fun extract_params ctxt auto default_params override_params =
blanchet@33192
   158
  let
blanchet@37163
   159
    val override_params = maps normalize_raw_param override_params
blanchet@33192
   160
    val raw_params = rev override_params @ rev default_params
blanchet@37259
   161
    val raw_lookup = AList.lookup (op =) raw_params
blanchet@37259
   162
    val lookup = Option.map stringify_raw_param_value o raw_lookup
blanchet@35962
   163
    val lookup_string = the_default "" o lookup
blanchet@35962
   164
    fun general_lookup_bool option default_value name =
blanchet@35962
   165
      case lookup name of
blanchet@36380
   166
        SOME s => parse_bool_option option name s
blanchet@35962
   167
      | NONE => default_value
blanchet@35962
   168
    val lookup_bool = the o general_lookup_bool false (SOME false)
blanchet@35962
   169
    val lookup_bool_option = general_lookup_bool true NONE
blanchet@33192
   170
    fun do_int name value =
blanchet@33192
   171
      case value of
blanchet@33192
   172
        SOME s => (case Int.fromString s of
blanchet@33192
   173
                     SOME i => i
blanchet@33192
   174
                   | NONE => error ("Parameter " ^ quote name ^
blanchet@33192
   175
                                    " must be assigned an integer value."))
blanchet@33192
   176
      | NONE => 0
blanchet@33192
   177
    fun lookup_int name = do_int name (lookup name)
blanchet@33192
   178
    fun lookup_int_option name =
blanchet@33192
   179
      case lookup name of
blanchet@33192
   180
        SOME "smart" => NONE
blanchet@33192
   181
      | value => SOME (do_int name value)
blanchet@33192
   182
    fun int_range_from_string name min_int s =
blanchet@33192
   183
      let
blanchet@33192
   184
        val (k1, k2) =
blanchet@33192
   185
          (case space_explode "-" s of
blanchet@33192
   186
             [s] => the_default (s, s) (first_field "\<midarrow>" s)
blanchet@33192
   187
           | ["", s2] => ("-" ^ s2, "-" ^ s2)
blanchet@33192
   188
           | [s1, s2] => (s1, s2)
blanchet@33192
   189
           | _ => raise Option)
blanchet@33192
   190
          |> pairself (maxed_int_from_string min_int)
blanchet@33192
   191
      in if k1 <= k2 then k1 upto k2 else k1 downto k2 end
blanchet@33192
   192
      handle Option.Option =>
blanchet@33192
   193
             error ("Parameter " ^ quote name ^
blanchet@33192
   194
                    " must be assigned a sequence of integers.")
blanchet@33192
   195
    fun int_seq_from_string name min_int s =
blanchet@33192
   196
      maps (int_range_from_string name min_int) (space_explode "," s)
blanchet@33192
   197
    fun lookup_int_seq name min_int =
blanchet@33192
   198
      case lookup name of
blanchet@33192
   199
        SOME s => (case int_seq_from_string name min_int s of
blanchet@33192
   200
                     [] => [min_int]
blanchet@33192
   201
                   | value => value)
blanchet@33192
   202
      | NONE => [min_int]
blanchet@37259
   203
    fun lookup_assigns read prefix default convert =
blanchet@37259
   204
      (NONE, convert (the_default default (lookup prefix)))
blanchet@33192
   205
      :: map (fn (name, value) =>
blanchet@33192
   206
                 (SOME (read (String.extract (name, size prefix + 1, NONE))),
blanchet@37259
   207
                  convert (stringify_raw_param_value value)))
blanchet@33192
   208
             (filter (String.isPrefix (prefix ^ " ") o fst) raw_params)
blanchet@37259
   209
    fun lookup_ints_assigns read prefix min_int =
blanchet@37259
   210
      lookup_assigns read prefix (signed_string_of_int min_int)
blanchet@37259
   211
                     (int_seq_from_string prefix min_int)
blanchet@34969
   212
    fun lookup_bool_assigns read prefix =
blanchet@37259
   213
      lookup_assigns read prefix "" (the o parse_bool_option false prefix)
blanchet@33192
   214
    fun lookup_bool_option_assigns read prefix =
blanchet@37259
   215
      lookup_assigns read prefix "" (parse_bool_option true prefix)
blanchet@37259
   216
    fun lookup_strings_assigns read prefix =
blanchet@37259
   217
      lookup_assigns read prefix "" (space_explode " ")
blanchet@33192
   218
    fun lookup_time name =
blanchet@33192
   219
      case lookup name of
blanchet@39562
   220
        SOME s => parse_time_option name s
blanchet@39562
   221
      | NONE => NONE
blanchet@33192
   222
    val read_type_polymorphic =
blanchet@33192
   223
      Syntax.read_typ ctxt #> Logic.mk_type
blanchet@33192
   224
      #> singleton (Variable.polymorphic ctxt) #> Logic.dest_type
blanchet@33192
   225
    val read_term_polymorphic =
blanchet@33192
   226
      Syntax.read_term ctxt #> singleton (Variable.polymorphic ctxt)
blanchet@38436
   227
    val lookup_term_list_polymorphic =
blanchet@38436
   228
      AList.lookup (op =) raw_params #> these #> map read_term_polymorphic
blanchet@33192
   229
    val read_const_polymorphic = read_term_polymorphic #> dest_Const
blanchet@33192
   230
    val cards_assigns = lookup_ints_assigns read_type_polymorphic "card" 1
blanchet@39590
   231
                        |> auto ? map (apsnd (take max_auto_scopes))
blanchet@33192
   232
    val maxes_assigns = lookup_ints_assigns read_const_polymorphic "max" ~1
blanchet@33192
   233
    val iters_assigns = lookup_ints_assigns read_const_polymorphic "iter" 0
blanchet@34121
   234
    val bitss = lookup_int_seq "bits" 1
blanchet@33192
   235
    val bisim_depths = lookup_int_seq "bisim_depth" ~1
blanchet@35665
   236
    val boxes = lookup_bool_option_assigns read_type_polymorphic "box"
blanchet@35665
   237
    val finitizes = lookup_bool_option_assigns read_type_polymorphic "finitize"
blanchet@39562
   238
    val monos = if auto then [(NONE, SOME true)]
blanchet@39562
   239
                else lookup_bool_option_assigns read_type_polymorphic "mono"
blanchet@34969
   240
    val stds = lookup_bool_assigns read_type_polymorphic "std"
blanchet@33192
   241
    val wfs = lookup_bool_option_assigns read_const_polymorphic "wf"
blanchet@33192
   242
    val sat_solver = lookup_string "sat_solver"
blanchet@39562
   243
    val blocking = auto orelse lookup_bool "blocking"
blanchet@33192
   244
    val falsify = lookup_bool "falsify"
blanchet@33192
   245
    val debug = not auto andalso lookup_bool "debug"
blanchet@33192
   246
    val verbose = debug orelse (not auto andalso lookup_bool "verbose")
blanchet@33192
   247
    val overlord = lookup_bool "overlord"
blanchet@33192
   248
    val user_axioms = lookup_bool_option "user_axioms"
blanchet@33192
   249
    val assms = lookup_bool "assms"
blanchet@38436
   250
    val whacks = lookup_term_list_polymorphic "whack"
blanchet@33547
   251
    val merge_type_vars = lookup_bool "merge_type_vars"
blanchet@34121
   252
    val binary_ints = lookup_bool_option "binary_ints"
blanchet@33192
   253
    val destroy_constrs = lookup_bool "destroy_constrs"
blanchet@33192
   254
    val specialize = lookup_bool "specialize"
blanchet@33192
   255
    val star_linear_preds = lookup_bool "star_linear_preds"
blanchet@42674
   256
    val preconstrs =
blanchet@42674
   257
      lookup_bool_option_assigns read_term_polymorphic "preconstr"
blanchet@33192
   258
    val peephole_optim = lookup_bool "peephole_optim"
blanchet@38370
   259
    val datatype_sym_break = lookup_int "datatype_sym_break"
blanchet@38370
   260
    val kodkod_sym_break = lookup_int "kodkod_sym_break"
blanchet@33552
   261
    val timeout = if auto then NONE else lookup_time "timeout"
blanchet@33192
   262
    val tac_timeout = lookup_time "tac_timeout"
blanchet@39562
   263
    val max_threads = if auto then 1 else Int.max (0, lookup_int "max_threads")
blanchet@37163
   264
    val show_datatypes = debug orelse lookup_bool "show_datatypes"
blanchet@37163
   265
    val show_consts = debug orelse lookup_bool "show_consts"
blanchet@42674
   266
    val evals = lookup_term_list_polymorphic "eval"
blanchet@33192
   267
    val formats = lookup_ints_assigns read_term_polymorphic "format" 0
blanchet@37259
   268
    val atomss = lookup_strings_assigns read_type_polymorphic "atoms"
blanchet@33552
   269
    val max_potential =
blanchet@33552
   270
      if auto then 0 else Int.max (0, lookup_int "max_potential")
blanchet@33192
   271
    val max_genuine = Int.max (0, lookup_int "max_genuine")
blanchet@33192
   272
    val check_potential = lookup_bool "check_potential"
blanchet@33192
   273
    val check_genuine = lookup_bool "check_genuine"
blanchet@36390
   274
    val batch_size =
blanchet@36390
   275
      case lookup_int_option "batch_size" of
blanchet@36390
   276
        SOME n => Int.max (1, n)
blanchet@38407
   277
      | NONE => if debug then 1 else 50
blanchet@33192
   278
    val expect = lookup_string "expect"
blanchet@33192
   279
  in
blanchet@33192
   280
    {cards_assigns = cards_assigns, maxes_assigns = maxes_assigns,
blanchet@34121
   281
     iters_assigns = iters_assigns, bitss = bitss, bisim_depths = bisim_depths,
blanchet@35665
   282
     boxes = boxes, finitizes = finitizes, monos = monos, stds = stds,
blanchet@35665
   283
     wfs = wfs, sat_solver = sat_solver, blocking = blocking, falsify = falsify,
blanchet@34969
   284
     debug = debug, verbose = verbose, overlord = overlord,
blanchet@38436
   285
     user_axioms = user_axioms, assms = assms, whacks = whacks,
blanchet@34121
   286
     merge_type_vars = merge_type_vars, binary_ints = binary_ints,
blanchet@34121
   287
     destroy_constrs = destroy_constrs, specialize = specialize,
blanchet@42674
   288
     star_linear_preds = star_linear_preds, preconstrs = preconstrs,
blanchet@42674
   289
     peephole_optim = peephole_optim, datatype_sym_break = datatype_sym_break,
blanchet@38370
   290
     kodkod_sym_break = kodkod_sym_break, timeout = timeout,
blanchet@36389
   291
     tac_timeout = tac_timeout, max_threads = max_threads,
blanchet@36390
   292
     show_datatypes = show_datatypes, show_consts = show_consts,
blanchet@42674
   293
     evals = evals, formats = formats, atomss = atomss,
blanchet@37259
   294
     max_potential = max_potential, max_genuine = max_genuine,
blanchet@37259
   295
     check_potential = check_potential, check_genuine = check_genuine,
blanchet@37259
   296
     batch_size = batch_size, expect = expect}
blanchet@33192
   297
  end
blanchet@33192
   298
blanchet@33192
   299
fun default_params thy =
wenzelm@36633
   300
  extract_params (ProofContext.init_global thy) false (default_raw_params thy)
blanchet@33192
   301
  o map (apsnd single)
blanchet@33192
   302
wenzelm@36970
   303
val parse_key = Scan.repeat1 Parse.typ_group >> space_implode " "
blanchet@35962
   304
val parse_value =
wenzelm@36970
   305
  Scan.repeat1 (Parse.minus >> single
blanchet@40582
   306
                || Scan.repeat1 (Scan.unless Parse.minus
blanchet@40582
   307
                                             (Parse.name || Parse.float_number))
blanchet@40582
   308
                || Parse.$$$ "," |-- Parse.number >> prefix "," >> single)
blanchet@40582
   309
  >> flat
wenzelm@36970
   310
val parse_param = parse_key -- Scan.optional (Parse.$$$ "=" |-- parse_value) []
blanchet@35966
   311
val parse_params =
wenzelm@36970
   312
  Scan.optional (Parse.$$$ "[" |-- Parse.list parse_param --| Parse.$$$ "]") []
blanchet@33192
   313
blanchet@33192
   314
fun handle_exceptions ctxt f x =
blanchet@33192
   315
  f x
blanchet@33192
   316
  handle ARG (loc, details) =>
blanchet@33192
   317
         error ("Bad argument(s) to " ^ quote loc ^ ": " ^ details ^ ".")
blanchet@33192
   318
       | BAD (loc, details) =>
blanchet@33192
   319
         error ("Internal error (" ^ quote loc ^ "): " ^ details ^ ".")
blanchet@33192
   320
       | NOT_SUPPORTED details =>
blanchet@33192
   321
         (warning ("Unsupported case: " ^ details ^ "."); x)
blanchet@33192
   322
       | NUT (loc, us) =>
blanchet@33192
   323
         error ("Invalid intermediate term" ^ plural_s_for_list us ^
blanchet@33192
   324
                " (" ^ quote loc ^ "): " ^
blanchet@33192
   325
                commas (map (string_for_nut ctxt) us) ^ ".")
blanchet@33192
   326
       | REP (loc, Rs) =>
blanchet@33192
   327
         error ("Invalid representation" ^ plural_s_for_list Rs ^
blanchet@33192
   328
                " (" ^ quote loc ^ "): " ^ commas (map string_for_rep Rs) ^ ".")
blanchet@33192
   329
       | TERM (loc, ts) =>
blanchet@33192
   330
         error ("Invalid term" ^ plural_s_for_list ts ^
blanchet@33192
   331
                " (" ^ quote loc ^ "): " ^
blanchet@33192
   332
                commas (map (Syntax.string_of_term ctxt) ts) ^ ".")
blanchet@33192
   333
       | TYPE (loc, Ts, ts) =>
blanchet@33192
   334
         error ("Invalid type" ^ plural_s_for_list Ts ^
blanchet@33192
   335
                (if null ts then
blanchet@33192
   336
                   ""
blanchet@33192
   337
                 else
blanchet@33192
   338
                   " for term" ^ plural_s_for_list ts ^ " " ^
blanchet@33192
   339
                   commas (map (quote o Syntax.string_of_term ctxt) ts)) ^
blanchet@33192
   340
                " (" ^ quote loc ^ "): " ^
blanchet@33192
   341
                commas (map (Syntax.string_of_typ ctxt) Ts) ^ ".")
blanchet@33192
   342
       | Refute.REFUTE (loc, details) =>
blanchet@33192
   343
         error ("Unhandled Refute error (" ^ quote loc ^ "): " ^ details ^ ".")
blanchet@33192
   344
blanchet@34969
   345
fun pick_nits override_params auto i step state =
blanchet@33192
   346
  let
blanchet@33192
   347
    val thy = Proof.theory_of state
blanchet@33192
   348
    val ctxt = Proof.context_of state
blanchet@33192
   349
    val _ = List.app check_raw_param override_params
blanchet@33192
   350
    val params as {blocking, debug, ...} =
blanchet@33192
   351
      extract_params ctxt auto (default_raw_params thy) override_params
blanchet@33192
   352
    fun go () =
blanchet@33552
   353
      (false, state)
blanchet@33552
   354
      |> (if auto then perhaps o try
blanchet@33552
   355
          else if debug then fn f => fn x => f x
blanchet@33552
   356
          else handle_exceptions ctxt)
blanchet@34969
   357
         (fn (_, state) => pick_nits_in_subgoal state params auto i step
blanchet@34118
   358
                           |>> curry (op =) "genuine")
blanchet@39562
   359
  in if blocking then go () else Future.fork (tap go) |> K (false, state) end
blanchet@33192
   360
blanchet@35966
   361
fun nitpick_trans (params, i) =
blanchet@34969
   362
  Toplevel.keep (fn st =>
blanchet@35966
   363
      (pick_nits params false i (Toplevel.proof_position_of st)
blanchet@35966
   364
                 (Toplevel.proof_of st); ()))
blanchet@33192
   365
blanchet@33192
   366
fun string_for_raw_param (name, value) =
blanchet@33192
   367
  name ^ " = " ^ stringify_raw_param_value value
blanchet@33192
   368
blanchet@35966
   369
fun nitpick_params_trans params =
blanchet@33192
   370
  Toplevel.theory
blanchet@35966
   371
      (fold set_default_raw_param params
blanchet@39562
   372
       #> tap (fn thy =>
blanchet@33552
   373
                  writeln ("Default parameters for Nitpick:\n" ^
blanchet@33552
   374
                           (case rev (default_raw_params thy) of
blanchet@33552
   375
                              [] => "none"
blanchet@33552
   376
                            | params =>
blanchet@33552
   377
                              (map check_raw_param params;
blanchet@33552
   378
                               params |> map string_for_raw_param
blanchet@33552
   379
                                      |> sort_strings |> cat_lines)))))
blanchet@33192
   380
blanchet@35962
   381
val parse_nitpick_command =
wenzelm@36970
   382
  (parse_params -- Scan.optional Parse.nat 1) #>> nitpick_trans
blanchet@35962
   383
val parse_nitpick_params_command = parse_params #>> nitpick_params_trans
blanchet@33192
   384
wenzelm@36970
   385
val _ = Outer_Syntax.improper_command "nitpick"
blanchet@36390
   386
            "try to find a counterexample for a given subgoal using Nitpick"
wenzelm@36970
   387
            Keyword.diag parse_nitpick_command
wenzelm@36970
   388
val _ = Outer_Syntax.command "nitpick_params"
blanchet@33192
   389
            "set and display the default parameters for Nitpick"
wenzelm@36970
   390
            Keyword.thy_decl parse_nitpick_params_command
blanchet@33192
   391
blanchet@41175
   392
val auto_nitpick = pick_nits [] true 1 0
blanchet@33552
   393
blanchet@41175
   394
val setup = Auto_Tools.register_tool (auto, auto_nitpick)
blanchet@33552
   395
blanchet@33192
   396
end;