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