tuned ML file name
authorblanchet
Fri Jan 31 10:23:32 2014 +0100 (2014-01-31)
changeset 55199ba93ef2c0d27
parent 55198 7a538e58b64e
child 55200 777328c9f1ea
tuned ML file name
src/HOL/Mutabelle/mutabelle_extra.ML
src/HOL/Nitpick.thy
src/HOL/Nitpick_Examples/minipick.ML
src/HOL/TPTP/atp_problem_import.ML
src/HOL/Tools/Nitpick/nitpick_commands.ML
src/HOL/Tools/Nitpick/nitpick_isar.ML
src/HOL/Tools/Nitpick/nitpick_tests.ML
     1.1 --- a/src/HOL/Mutabelle/mutabelle_extra.ML	Fri Jan 31 10:23:32 2014 +0100
     1.2 +++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Fri Jan 31 10:23:32 2014 +0100
     1.3 @@ -189,7 +189,7 @@
     1.4      val ctxt = Proof_Context.init_global thy
     1.5      val state = Proof.init ctxt
     1.6      val (res, _) = Nitpick.pick_nits_in_term state
     1.7 -      (Nitpick_Isar.default_params thy []) Nitpick.Normal 1 1 1 [] [] [] t
     1.8 +      (Nitpick_Commands.default_params thy []) Nitpick.Normal 1 1 1 [] [] [] t
     1.9      val _ = Output.urgent_message ("Nitpick: " ^ res)
    1.10    in
    1.11      (rpair []) (case res of
     2.1 --- a/src/HOL/Nitpick.thy	Fri Jan 31 10:23:32 2014 +0100
     2.2 +++ b/src/HOL/Nitpick.thy	Fri Jan 31 10:23:32 2014 +0100
     2.3 @@ -219,7 +219,7 @@
     2.4  ML_file "Tools/Nitpick/nitpick_kodkod.ML"
     2.5  ML_file "Tools/Nitpick/nitpick_model.ML"
     2.6  ML_file "Tools/Nitpick/nitpick.ML"
     2.7 -ML_file "Tools/Nitpick/nitpick_isar.ML"
     2.8 +ML_file "Tools/Nitpick/nitpick_commands.ML"
     2.9  ML_file "Tools/Nitpick/nitpick_tests.ML"
    2.10  
    2.11  setup {*
     3.1 --- a/src/HOL/Nitpick_Examples/minipick.ML	Fri Jan 31 10:23:32 2014 +0100
     3.2 +++ b/src/HOL/Nitpick_Examples/minipick.ML	Fri Jan 31 10:23:32 2014 +0100
     3.3 @@ -429,7 +429,7 @@
     3.4  
     3.5  fun solve_any_kodkod_problem thy problems =
     3.6    let
     3.7 -    val {debug, overlord, timeout, ...} = Nitpick_Isar.default_params thy []
     3.8 +    val {debug, overlord, timeout, ...} = Nitpick_Commands.default_params thy []
     3.9      val max_threads = 1
    3.10      val max_solutions = 1
    3.11    in
    3.12 @@ -450,13 +450,13 @@
    3.13  fun minipick ctxt n t =
    3.14    let
    3.15      val thy = Proof_Context.theory_of ctxt
    3.16 -    val {total_consts, ...} = Nitpick_Isar.default_params thy []
    3.17 +    val {total_consts, ...} = Nitpick_Commands.default_params thy []
    3.18      val totals =
    3.19        total_consts |> Option.map single |> the_default [true, false]
    3.20      fun problem_for (total, k) =
    3.21        kodkod_problem_from_term ctxt total (K k) default_raw_infinite t
    3.22    in
    3.23 -    (totals, 1 upto n)
    3.24 +    (totalsNitpick_Commands, 1 upto n)
    3.25      |-> map_product pair
    3.26      |> map problem_for
    3.27      |> solve_any_kodkod_problem (Proof_Context.theory_of ctxt)
     4.1 --- a/src/HOL/TPTP/atp_problem_import.ML	Fri Jan 31 10:23:32 2014 +0100
     4.2 +++ b/src/HOL/TPTP/atp_problem_import.ML	Fri Jan 31 10:23:32 2014 +0100
     4.3 @@ -1,4 +1,4 @@
     4.4 -(*  Title:      HOL/TPTP/atp_problem_import.ML
     4.5 +Nitpick_Commands(*  Title:      HOL/TPTP/atp_problem_import.ML
     4.6      Author:     Jasmin Blanchette, TU Muenchen
     4.7      Copyright   2012
     4.8  
     4.9 @@ -93,7 +93,7 @@
    4.10         ("max_potential", "0"),
    4.11         ("timeout", string_of_int timeout),
    4.12         ("tac_timeout", string_of_int ((timeout + 49) div 50))]
    4.13 -      |> Nitpick_Isar.default_params thy
    4.14 +      |> Nitpick_Commands.default_params thy
    4.15      val i = 1
    4.16      val n = 1
    4.17      val step = 0
    4.18 @@ -168,7 +168,7 @@
    4.19             ("overlord", if overlord then "true" else "false"),
    4.20             ("max_potential", "0"),
    4.21             ("timeout", string_of_int timeout)]
    4.22 -          |> Nitpick_Isar.default_params thy
    4.23 +          |> Nitpick_Commands.default_params thy
    4.24          val i = 1
    4.25          val n = 1
    4.26          val step = 0
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/Tools/Nitpick/nitpick_commands.ML	Fri Jan 31 10:23:32 2014 +0100
     5.3 @@ -0,0 +1,401 @@
     5.4 +(*  Title:      HOL/Tools/Nitpick/nitpick_commands.ML
     5.5 +    Author:     Jasmin Blanchette, TU Muenchen
     5.6 +    Copyright   2008, 2009, 2010
     5.7 +
     5.8 +Adds the "nitpick" and "nitpick_params" commands to Isabelle/Isar's outer
     5.9 +syntax.
    5.10 +*)
    5.11 +
    5.12 +signature NITPICK_COMMANDS =
    5.13 +sig
    5.14 +  type params = Nitpick.params
    5.15 +
    5.16 +  val nitpickN : string
    5.17 +  val nitpick_paramsN : string
    5.18 +  val default_params : theory -> (string * string) list -> params
    5.19 +end;
    5.20 +
    5.21 +structure Nitpick_Commands : NITPICK_Commands =
    5.22 +struct
    5.23 +
    5.24 +open Nitpick_Util
    5.25 +open Nitpick_HOL
    5.26 +open Nitpick_Rep
    5.27 +open Nitpick_Nut
    5.28 +open Nitpick
    5.29 +
    5.30 +val nitpickN = "nitpick"
    5.31 +val nitpick_paramsN = "nitpick_params"
    5.32 +
    5.33 +(* Maximum number of scopes for Auto Nitpick. Be frugal since it has to share
    5.34 +   its time slot with several other automatic tools. *)
    5.35 +val auto_try_max_scopes = 6
    5.36 +
    5.37 +val _ =
    5.38 +  ProofGeneral.preference_option ProofGeneral.category_tracing
    5.39 +    NONE
    5.40 +    @{option auto_nitpick}
    5.41 +    "auto-nitpick"
    5.42 +    "Run Nitpick automatically"
    5.43 +
    5.44 +type raw_param = string * string list
    5.45 +
    5.46 +val default_default_params =
    5.47 +  [("card", "1\<emdash>10"),
    5.48 +   ("iter", "0,1,2,4,8,12,16,20,24,28"),
    5.49 +   ("bits", "1\<emdash>10"),
    5.50 +   ("bisim_depth", "9"),
    5.51 +   ("box", "smart"),
    5.52 +   ("finitize", "smart"),
    5.53 +   ("mono", "smart"),
    5.54 +   ("std", "true"),
    5.55 +   ("wf", "smart"),
    5.56 +   ("sat_solver", "smart"),
    5.57 +   ("batch_size", "smart"),
    5.58 +   ("blocking", "true"),
    5.59 +   ("falsify", "true"),
    5.60 +   ("user_axioms", "smart"),
    5.61 +   ("assms", "true"),
    5.62 +   ("merge_type_vars", "false"),
    5.63 +   ("binary_ints", "smart"),
    5.64 +   ("destroy_constrs", "true"),
    5.65 +   ("specialize", "true"),
    5.66 +   ("star_linear_preds", "true"),
    5.67 +   ("total_consts", "smart"),
    5.68 +   ("peephole_optim", "true"),
    5.69 +   ("datatype_sym_break", "5"),
    5.70 +   ("kodkod_sym_break", "15"),
    5.71 +   ("timeout", "30"),
    5.72 +   ("tac_timeout", "0.5"),
    5.73 +   ("max_threads", "0"),
    5.74 +   ("debug", "false"),
    5.75 +   ("verbose", "false"),
    5.76 +   ("overlord", "false"),
    5.77 +   ("spy", "false"),
    5.78 +   ("show_datatypes", "false"),
    5.79 +   ("show_skolems", "true"),
    5.80 +   ("show_consts", "false"),
    5.81 +   ("format", "1"),
    5.82 +   ("max_potential", "1"),
    5.83 +   ("max_genuine", "1"),
    5.84 +   ("check_potential", "false"),
    5.85 +   ("check_genuine", "false")]
    5.86 +
    5.87 +val negated_params =
    5.88 +  [("dont_box", "box"),
    5.89 +   ("dont_finitize", "finitize"),
    5.90 +   ("non_mono", "mono"),
    5.91 +   ("non_std", "std"),
    5.92 +   ("non_wf", "wf"),
    5.93 +   ("non_blocking", "blocking"),
    5.94 +   ("satisfy", "falsify"),
    5.95 +   ("no_user_axioms", "user_axioms"),
    5.96 +   ("no_assms", "assms"),
    5.97 +   ("dont_merge_type_vars", "merge_type_vars"),
    5.98 +   ("unary_ints", "binary_ints"),
    5.99 +   ("dont_destroy_constrs", "destroy_constrs"),
   5.100 +   ("dont_specialize", "specialize"),
   5.101 +   ("dont_star_linear_preds", "star_linear_preds"),
   5.102 +   ("partial_consts", "total_consts"),
   5.103 +   ("no_peephole_optim", "peephole_optim"),
   5.104 +   ("no_debug", "debug"),
   5.105 +   ("quiet", "verbose"),
   5.106 +   ("no_overlord", "overlord"),
   5.107 +   ("dont_spy", "spy"),
   5.108 +   ("hide_datatypes", "show_datatypes"),
   5.109 +   ("hide_skolems", "show_skolems"),
   5.110 +   ("hide_consts", "show_consts"),
   5.111 +   ("trust_potential", "check_potential"),
   5.112 +   ("trust_genuine", "check_genuine")]
   5.113 +
   5.114 +fun is_known_raw_param s =
   5.115 +  AList.defined (op =) default_default_params s orelse
   5.116 +  AList.defined (op =) negated_params s orelse
   5.117 +  member (op =) ["max", "show_all", "whack", "eval", "need", "atoms",
   5.118 +                 "expect"] s orelse
   5.119 +  exists (fn p => String.isPrefix (p ^ " ") s)
   5.120 +         ["card", "max", "iter", "box", "dont_box", "finitize", "dont_finitize",
   5.121 +          "mono", "non_mono", "std", "non_std", "wf", "non_wf", "format",
   5.122 +          "atoms"]
   5.123 +
   5.124 +fun check_raw_param (s, _) =
   5.125 +  if is_known_raw_param s then ()
   5.126 +  else error ("Unknown parameter: " ^ quote s ^ ".")
   5.127 +
   5.128 +fun unnegate_param_name name =
   5.129 +  case AList.lookup (op =) negated_params name of
   5.130 +    NONE => if String.isPrefix "dont_" name then SOME (unprefix "dont_" name)
   5.131 +            else if String.isPrefix "non_" name then SOME (unprefix "non_" name)
   5.132 +            else NONE
   5.133 +  | some_name => some_name
   5.134 +fun normalize_raw_param (name, value) =
   5.135 +  case unnegate_param_name name of
   5.136 +    SOME name' => [(name', case value of
   5.137 +                             ["false"] => ["true"]
   5.138 +                           | ["true"] => ["false"]
   5.139 +                           | [] => ["false"]
   5.140 +                           | _ => value)]
   5.141 +  | NONE => if name = "show_all" then
   5.142 +              [("show_datatypes", value), ("show_skolems", value),
   5.143 +               ("show_consts", value)]
   5.144 +            else
   5.145 +              [(name, value)]
   5.146 +
   5.147 +structure Data = Theory_Data
   5.148 +(
   5.149 +  type T = raw_param list
   5.150 +  val empty = default_default_params |> map (apsnd single)
   5.151 +  val extend = I
   5.152 +  fun merge data = AList.merge (op =) (K true) data
   5.153 +)
   5.154 +
   5.155 +val set_default_raw_param =
   5.156 +  Data.map o fold (AList.update (op =)) o normalize_raw_param
   5.157 +val default_raw_params = Data.get
   5.158 +
   5.159 +fun is_punctuation s = (s = "," orelse s = "-" orelse s = "\<emdash>")
   5.160 +
   5.161 +fun stringify_raw_param_value [] = ""
   5.162 +  | stringify_raw_param_value [s] = s
   5.163 +  | stringify_raw_param_value (s1 :: s2 :: ss) =
   5.164 +    s1 ^ (if is_punctuation s1 orelse is_punctuation s2 then "" else " ") ^
   5.165 +    stringify_raw_param_value (s2 :: ss)
   5.166 +
   5.167 +fun maxed_int_from_string min_int s = Int.max (min_int, the (Int.fromString s))
   5.168 +
   5.169 +fun extract_params ctxt mode default_params override_params =
   5.170 +  let
   5.171 +    val override_params = maps normalize_raw_param override_params
   5.172 +    val raw_params = rev override_params @ rev default_params
   5.173 +    val raw_lookup = AList.lookup (op =) raw_params
   5.174 +    val lookup = Option.map stringify_raw_param_value o raw_lookup
   5.175 +    val lookup_string = the_default "" o lookup
   5.176 +    fun general_lookup_bool option default_value name =
   5.177 +      case lookup name of
   5.178 +        SOME s => parse_bool_option option name s
   5.179 +      | NONE => default_value
   5.180 +    val lookup_bool = the o general_lookup_bool false (SOME false)
   5.181 +    val lookup_bool_option = general_lookup_bool true NONE
   5.182 +    fun do_int name value =
   5.183 +      case value of
   5.184 +        SOME s => (case Int.fromString s of
   5.185 +                     SOME i => i
   5.186 +                   | NONE => error ("Parameter " ^ quote name ^
   5.187 +                                    " must be assigned an integer value."))
   5.188 +      | NONE => 0
   5.189 +    fun lookup_int name = do_int name (lookup name)
   5.190 +    fun lookup_int_option name =
   5.191 +      case lookup name of
   5.192 +        SOME "smart" => NONE
   5.193 +      | value => SOME (do_int name value)
   5.194 +    fun int_range_from_string name min_int s =
   5.195 +      let
   5.196 +        val (k1, k2) =
   5.197 +          (case space_explode "-" s of
   5.198 +             [s] => the_default (s, s) (first_field "\<emdash>" s)
   5.199 +           | ["", s2] => ("-" ^ s2, "-" ^ s2)
   5.200 +           | [s1, s2] => (s1, s2)
   5.201 +           | _ => raise Option.Option)
   5.202 +          |> pairself (maxed_int_from_string min_int)
   5.203 +      in if k1 <= k2 then k1 upto k2 else k1 downto k2 end
   5.204 +      handle Option.Option =>
   5.205 +             error ("Parameter " ^ quote name ^
   5.206 +                    " must be assigned a sequence of integers.")
   5.207 +    fun int_seq_from_string name min_int s =
   5.208 +      maps (int_range_from_string name min_int) (space_explode "," s)
   5.209 +    fun lookup_int_seq name min_int =
   5.210 +      case lookup name of
   5.211 +        SOME s => (case int_seq_from_string name min_int s of
   5.212 +                     [] => [min_int]
   5.213 +                   | value => value)
   5.214 +      | NONE => [min_int]
   5.215 +    fun lookup_assigns read prefix default convert =
   5.216 +      (NONE, convert (the_default default (lookup prefix)))
   5.217 +      :: map (fn (name, value) =>
   5.218 +                 (SOME (read (String.extract (name, size prefix + 1, NONE))),
   5.219 +                  convert (stringify_raw_param_value value)))
   5.220 +             (filter (String.isPrefix (prefix ^ " ") o fst) raw_params)
   5.221 +    fun lookup_ints_assigns read prefix min_int =
   5.222 +      lookup_assigns read prefix (signed_string_of_int min_int)
   5.223 +                     (int_seq_from_string prefix min_int)
   5.224 +    fun lookup_bool_assigns read prefix =
   5.225 +      lookup_assigns read prefix "" (the o parse_bool_option false prefix)
   5.226 +    fun lookup_bool_option_assigns read prefix =
   5.227 +      lookup_assigns read prefix "" (parse_bool_option true prefix)
   5.228 +    fun lookup_strings_assigns read prefix =
   5.229 +      lookup_assigns read prefix "" (space_explode " ")
   5.230 +    fun lookup_time name =
   5.231 +      case lookup name of
   5.232 +        SOME s => parse_time name s
   5.233 +      | NONE => Time.zeroTime
   5.234 +    val read_type_polymorphic =
   5.235 +      Syntax.read_typ ctxt #> Logic.mk_type
   5.236 +      #> singleton (Variable.polymorphic ctxt) #> Logic.dest_type
   5.237 +    val read_term_polymorphic =
   5.238 +      Syntax.read_term ctxt #> singleton (Variable.polymorphic ctxt)
   5.239 +    val lookup_term_list_option_polymorphic =
   5.240 +      AList.lookup (op =) raw_params #> Option.map (map read_term_polymorphic)
   5.241 +    val read_const_polymorphic = read_term_polymorphic #> dest_Const
   5.242 +    val cards_assigns =
   5.243 +      lookup_ints_assigns read_type_polymorphic "card" 1
   5.244 +      |> mode = Auto_Try ? map (apsnd (take auto_try_max_scopes))
   5.245 +    val maxes_assigns = lookup_ints_assigns read_const_polymorphic "max" ~1
   5.246 +    val iters_assigns = lookup_ints_assigns read_const_polymorphic "iter" 0
   5.247 +    val bitss = lookup_int_seq "bits" 1
   5.248 +    val bisim_depths = lookup_int_seq "bisim_depth" ~1
   5.249 +    val boxes = lookup_bool_option_assigns read_type_polymorphic "box"
   5.250 +    val finitizes = lookup_bool_option_assigns read_type_polymorphic "finitize"
   5.251 +    val monos = if mode = Auto_Try then [(NONE, SOME true)]
   5.252 +                else lookup_bool_option_assigns read_type_polymorphic "mono"
   5.253 +    val stds = lookup_bool_assigns read_type_polymorphic "std"
   5.254 +    val wfs = lookup_bool_option_assigns read_const_polymorphic "wf"
   5.255 +    val sat_solver = lookup_string "sat_solver"
   5.256 +    val blocking = mode <> Normal orelse lookup_bool "blocking"
   5.257 +    val falsify = lookup_bool "falsify"
   5.258 +    val debug = (mode <> Auto_Try andalso lookup_bool "debug")
   5.259 +    val verbose = debug orelse (mode <> Auto_Try andalso lookup_bool "verbose")
   5.260 +    val overlord = lookup_bool "overlord"
   5.261 +    val spy = getenv "NITPICK_SPY" = "yes" orelse lookup_bool "spy"
   5.262 +    val user_axioms = lookup_bool_option "user_axioms"
   5.263 +    val assms = lookup_bool "assms"
   5.264 +    val whacks = lookup_term_list_option_polymorphic "whack" |> these
   5.265 +    val merge_type_vars = lookup_bool "merge_type_vars"
   5.266 +    val binary_ints = lookup_bool_option "binary_ints"
   5.267 +    val destroy_constrs = lookup_bool "destroy_constrs"
   5.268 +    val specialize = lookup_bool "specialize"
   5.269 +    val star_linear_preds = lookup_bool "star_linear_preds"
   5.270 +    val total_consts = lookup_bool_option "total_consts"
   5.271 +    val needs = lookup_term_list_option_polymorphic "need"
   5.272 +    val peephole_optim = lookup_bool "peephole_optim"
   5.273 +    val datatype_sym_break = lookup_int "datatype_sym_break"
   5.274 +    val kodkod_sym_break = lookup_int "kodkod_sym_break"
   5.275 +    val timeout = lookup_time "timeout"
   5.276 +    val tac_timeout = lookup_time "tac_timeout"
   5.277 +    val max_threads =
   5.278 +      if mode = Normal then Int.max (0, lookup_int "max_threads") else 1
   5.279 +    val show_datatypes = debug orelse lookup_bool "show_datatypes"
   5.280 +    val show_skolems = debug orelse lookup_bool "show_skolems"
   5.281 +    val show_consts = debug orelse lookup_bool "show_consts"
   5.282 +    val evals = lookup_term_list_option_polymorphic "eval" |> these
   5.283 +    val formats = lookup_ints_assigns read_term_polymorphic "format" 0
   5.284 +    val atomss = lookup_strings_assigns read_type_polymorphic "atoms"
   5.285 +    val max_potential =
   5.286 +      if mode = Normal then Int.max (0, lookup_int "max_potential") else 0
   5.287 +    val max_genuine = Int.max (0, lookup_int "max_genuine")
   5.288 +    val check_potential = lookup_bool "check_potential"
   5.289 +    val check_genuine = lookup_bool "check_genuine"
   5.290 +    val batch_size =
   5.291 +      case lookup_int_option "batch_size" of
   5.292 +        SOME n => Int.max (1, n)
   5.293 +      | NONE => if debug then 1 else 50
   5.294 +    val expect = lookup_string "expect"
   5.295 +  in
   5.296 +    {cards_assigns = cards_assigns, maxes_assigns = maxes_assigns, iters_assigns = iters_assigns,
   5.297 +     bitss = bitss, bisim_depths = bisim_depths, boxes = boxes, finitizes = finitizes,
   5.298 +     monos = monos, stds = stds, wfs = wfs, sat_solver = sat_solver, blocking = blocking,
   5.299 +     falsify = falsify, debug = debug, verbose = verbose, overlord = overlord, spy = spy,
   5.300 +     user_axioms = user_axioms, assms = assms, whacks = whacks, merge_type_vars = merge_type_vars,
   5.301 +     binary_ints = binary_ints, destroy_constrs = destroy_constrs, specialize = specialize,
   5.302 +     star_linear_preds = star_linear_preds, total_consts = total_consts, needs = needs,
   5.303 +     peephole_optim = peephole_optim, datatype_sym_break = datatype_sym_break,
   5.304 +     kodkod_sym_break = kodkod_sym_break, timeout = timeout, tac_timeout = tac_timeout,
   5.305 +     max_threads = max_threads, show_datatypes = show_datatypes, show_skolems = show_skolems,
   5.306 +     show_consts = show_consts, evals = evals, formats = formats, atomss = atomss,
   5.307 +     max_potential = max_potential, max_genuine = max_genuine, check_potential = check_potential,
   5.308 +     check_genuine = check_genuine, batch_size = batch_size, expect = expect}
   5.309 +  end
   5.310 +
   5.311 +fun default_params thy =
   5.312 +  extract_params (Proof_Context.init_global thy) Normal (default_raw_params thy)
   5.313 +  o map (apsnd single)
   5.314 +
   5.315 +val parse_key = Scan.repeat1 Parse.typ_group >> space_implode " "
   5.316 +val parse_value =
   5.317 +  Scan.repeat1 (Parse.minus >> single
   5.318 +                || Scan.repeat1 (Scan.unless Parse.minus
   5.319 +                                             (Parse.name || Parse.float_number))
   5.320 +                || @{keyword ","} |-- Parse.number >> prefix "," >> single)
   5.321 +  >> flat
   5.322 +val parse_param = parse_key -- Scan.optional (@{keyword "="} |-- parse_value) []
   5.323 +val parse_params =
   5.324 +  Scan.optional (@{keyword "["} |-- Parse.list parse_param --| @{keyword "]"}) []
   5.325 +
   5.326 +fun handle_exceptions ctxt f x =
   5.327 +  f x
   5.328 +  handle ARG (loc, details) =>
   5.329 +         error ("Bad argument(s) to " ^ quote loc ^ ": " ^ details ^ ".")
   5.330 +       | BAD (loc, details) =>
   5.331 +         error ("Internal error (" ^ quote loc ^ "): " ^ details ^ ".")
   5.332 +       | NOT_SUPPORTED details =>
   5.333 +         (warning ("Unsupported case: " ^ details ^ "."); x)
   5.334 +       | NUT (loc, us) =>
   5.335 +         error ("Invalid intermediate term" ^ plural_s_for_list us ^
   5.336 +                " (" ^ quote loc ^ "): " ^
   5.337 +                commas (map (string_for_nut ctxt) us) ^ ".")
   5.338 +       | REP (loc, Rs) =>
   5.339 +         error ("Invalid representation" ^ plural_s_for_list Rs ^
   5.340 +                " (" ^ quote loc ^ "): " ^ commas (map string_for_rep Rs) ^ ".")
   5.341 +       | TERM (loc, ts) =>
   5.342 +         error ("Invalid term" ^ plural_s_for_list ts ^
   5.343 +                " (" ^ quote loc ^ "): " ^
   5.344 +                commas (map (Syntax.string_of_term ctxt) ts) ^ ".")
   5.345 +       | TYPE (loc, Ts, ts) =>
   5.346 +         error ("Invalid type" ^ plural_s_for_list Ts ^
   5.347 +                (if null ts then
   5.348 +                   ""
   5.349 +                 else
   5.350 +                   " for term" ^ plural_s_for_list ts ^ " " ^
   5.351 +                   commas (map (quote o Syntax.string_of_term ctxt) ts)) ^
   5.352 +                " (" ^ quote loc ^ "): " ^
   5.353 +                commas (map (Syntax.string_of_typ ctxt) Ts) ^ ".")
   5.354 +
   5.355 +fun pick_nits override_params mode i step state =
   5.356 +  let
   5.357 +    val thy = Proof.theory_of state
   5.358 +    val ctxt = Proof.context_of state
   5.359 +    val _ = List.app check_raw_param override_params
   5.360 +    val params as {blocking, debug, ...} =
   5.361 +      extract_params ctxt mode (default_raw_params thy) override_params
   5.362 +    fun go () =
   5.363 +      (unknownN, state)
   5.364 +      |> (if mode = Auto_Try then perhaps o try
   5.365 +          else if debug then fn f => fn x => f x
   5.366 +          else handle_exceptions ctxt)
   5.367 +         (fn (_, state) => pick_nits_in_subgoal state params mode i step)
   5.368 +  in if blocking then go () else Future.fork (tap go) |> K (unknownN, state) end
   5.369 +  |> `(fn (outcome_code, _) => outcome_code = genuineN)
   5.370 +
   5.371 +fun string_for_raw_param (name, value) =
   5.372 +  name ^ " = " ^ stringify_raw_param_value value
   5.373 +
   5.374 +fun nitpick_params_trans params =
   5.375 +  Toplevel.theory
   5.376 +      (fold set_default_raw_param params
   5.377 +       #> tap (fn thy =>
   5.378 +                  writeln ("Default parameters for Nitpick:\n" ^
   5.379 +                           (case rev (default_raw_params thy) of
   5.380 +                              [] => "none"
   5.381 +                            | params =>
   5.382 +                              (map check_raw_param params;
   5.383 +                               params |> map string_for_raw_param
   5.384 +                                      |> sort_strings |> cat_lines)))))
   5.385 +
   5.386 +val _ =
   5.387 +  Outer_Syntax.improper_command @{command_spec "nitpick"}
   5.388 +    "try to find a counterexample for a given subgoal using Nitpick"
   5.389 +    (parse_params -- Scan.optional Parse.nat 1 >> (fn (params, i) =>
   5.390 +      Toplevel.unknown_proof o
   5.391 +      Toplevel.keep (fn state =>
   5.392 +        ignore (pick_nits params Normal i (Toplevel.proof_position_of state)
   5.393 +          (Toplevel.proof_of state)))))
   5.394 +
   5.395 +val _ =
   5.396 +  Outer_Syntax.command @{command_spec "nitpick_params"}
   5.397 +    "set and display the default parameters for Nitpick"
   5.398 +    (parse_params #>> nitpick_params_trans)
   5.399 +
   5.400 +fun try_nitpick auto = pick_nits [] (if auto then Auto_Try else Try) 1 0
   5.401 +
   5.402 +val _ = Try.tool_setup (nitpickN, (50, @{option auto_nitpick}, try_nitpick))
   5.403 +
   5.404 +end;
     6.1 --- a/src/HOL/Tools/Nitpick/nitpick_isar.ML	Fri Jan 31 10:23:32 2014 +0100
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,401 +0,0 @@
     6.4 -(*  Title:      HOL/Tools/Nitpick/nitpick_isar.ML
     6.5 -    Author:     Jasmin Blanchette, TU Muenchen
     6.6 -    Copyright   2008, 2009, 2010
     6.7 -
     6.8 -Adds the "nitpick" and "nitpick_params" commands to Isabelle/Isar's outer
     6.9 -syntax.
    6.10 -*)
    6.11 -
    6.12 -signature NITPICK_ISAR =
    6.13 -sig
    6.14 -  type params = Nitpick.params
    6.15 -
    6.16 -  val nitpickN : string
    6.17 -  val nitpick_paramsN : string
    6.18 -  val default_params : theory -> (string * string) list -> params
    6.19 -end;
    6.20 -
    6.21 -structure Nitpick_Isar : NITPICK_ISAR =
    6.22 -struct
    6.23 -
    6.24 -open Nitpick_Util
    6.25 -open Nitpick_HOL
    6.26 -open Nitpick_Rep
    6.27 -open Nitpick_Nut
    6.28 -open Nitpick
    6.29 -
    6.30 -val nitpickN = "nitpick"
    6.31 -val nitpick_paramsN = "nitpick_params"
    6.32 -
    6.33 -(* Maximum number of scopes for Auto Nitpick. Be frugal since it has to share
    6.34 -   its time slot with several other automatic tools. *)
    6.35 -val auto_try_max_scopes = 6
    6.36 -
    6.37 -val _ =
    6.38 -  ProofGeneral.preference_option ProofGeneral.category_tracing
    6.39 -    NONE
    6.40 -    @{option auto_nitpick}
    6.41 -    "auto-nitpick"
    6.42 -    "Run Nitpick automatically"
    6.43 -
    6.44 -type raw_param = string * string list
    6.45 -
    6.46 -val default_default_params =
    6.47 -  [("card", "1\<emdash>10"),
    6.48 -   ("iter", "0,1,2,4,8,12,16,20,24,28"),
    6.49 -   ("bits", "1\<emdash>10"),
    6.50 -   ("bisim_depth", "9"),
    6.51 -   ("box", "smart"),
    6.52 -   ("finitize", "smart"),
    6.53 -   ("mono", "smart"),
    6.54 -   ("std", "true"),
    6.55 -   ("wf", "smart"),
    6.56 -   ("sat_solver", "smart"),
    6.57 -   ("batch_size", "smart"),
    6.58 -   ("blocking", "true"),
    6.59 -   ("falsify", "true"),
    6.60 -   ("user_axioms", "smart"),
    6.61 -   ("assms", "true"),
    6.62 -   ("merge_type_vars", "false"),
    6.63 -   ("binary_ints", "smart"),
    6.64 -   ("destroy_constrs", "true"),
    6.65 -   ("specialize", "true"),
    6.66 -   ("star_linear_preds", "true"),
    6.67 -   ("total_consts", "smart"),
    6.68 -   ("peephole_optim", "true"),
    6.69 -   ("datatype_sym_break", "5"),
    6.70 -   ("kodkod_sym_break", "15"),
    6.71 -   ("timeout", "30"),
    6.72 -   ("tac_timeout", "0.5"),
    6.73 -   ("max_threads", "0"),
    6.74 -   ("debug", "false"),
    6.75 -   ("verbose", "false"),
    6.76 -   ("overlord", "false"),
    6.77 -   ("spy", "false"),
    6.78 -   ("show_datatypes", "false"),
    6.79 -   ("show_skolems", "true"),
    6.80 -   ("show_consts", "false"),
    6.81 -   ("format", "1"),
    6.82 -   ("max_potential", "1"),
    6.83 -   ("max_genuine", "1"),
    6.84 -   ("check_potential", "false"),
    6.85 -   ("check_genuine", "false")]
    6.86 -
    6.87 -val negated_params =
    6.88 -  [("dont_box", "box"),
    6.89 -   ("dont_finitize", "finitize"),
    6.90 -   ("non_mono", "mono"),
    6.91 -   ("non_std", "std"),
    6.92 -   ("non_wf", "wf"),
    6.93 -   ("non_blocking", "blocking"),
    6.94 -   ("satisfy", "falsify"),
    6.95 -   ("no_user_axioms", "user_axioms"),
    6.96 -   ("no_assms", "assms"),
    6.97 -   ("dont_merge_type_vars", "merge_type_vars"),
    6.98 -   ("unary_ints", "binary_ints"),
    6.99 -   ("dont_destroy_constrs", "destroy_constrs"),
   6.100 -   ("dont_specialize", "specialize"),
   6.101 -   ("dont_star_linear_preds", "star_linear_preds"),
   6.102 -   ("partial_consts", "total_consts"),
   6.103 -   ("no_peephole_optim", "peephole_optim"),
   6.104 -   ("no_debug", "debug"),
   6.105 -   ("quiet", "verbose"),
   6.106 -   ("no_overlord", "overlord"),
   6.107 -   ("dont_spy", "spy"),
   6.108 -   ("hide_datatypes", "show_datatypes"),
   6.109 -   ("hide_skolems", "show_skolems"),
   6.110 -   ("hide_consts", "show_consts"),
   6.111 -   ("trust_potential", "check_potential"),
   6.112 -   ("trust_genuine", "check_genuine")]
   6.113 -
   6.114 -fun is_known_raw_param s =
   6.115 -  AList.defined (op =) default_default_params s orelse
   6.116 -  AList.defined (op =) negated_params s orelse
   6.117 -  member (op =) ["max", "show_all", "whack", "eval", "need", "atoms",
   6.118 -                 "expect"] s orelse
   6.119 -  exists (fn p => String.isPrefix (p ^ " ") s)
   6.120 -         ["card", "max", "iter", "box", "dont_box", "finitize", "dont_finitize",
   6.121 -          "mono", "non_mono", "std", "non_std", "wf", "non_wf", "format",
   6.122 -          "atoms"]
   6.123 -
   6.124 -fun check_raw_param (s, _) =
   6.125 -  if is_known_raw_param s then ()
   6.126 -  else error ("Unknown parameter: " ^ quote s ^ ".")
   6.127 -
   6.128 -fun unnegate_param_name name =
   6.129 -  case AList.lookup (op =) negated_params name of
   6.130 -    NONE => if String.isPrefix "dont_" name then SOME (unprefix "dont_" name)
   6.131 -            else if String.isPrefix "non_" name then SOME (unprefix "non_" name)
   6.132 -            else NONE
   6.133 -  | some_name => some_name
   6.134 -fun normalize_raw_param (name, value) =
   6.135 -  case unnegate_param_name name of
   6.136 -    SOME name' => [(name', case value of
   6.137 -                             ["false"] => ["true"]
   6.138 -                           | ["true"] => ["false"]
   6.139 -                           | [] => ["false"]
   6.140 -                           | _ => value)]
   6.141 -  | NONE => if name = "show_all" then
   6.142 -              [("show_datatypes", value), ("show_skolems", value),
   6.143 -               ("show_consts", value)]
   6.144 -            else
   6.145 -              [(name, value)]
   6.146 -
   6.147 -structure Data = Theory_Data
   6.148 -(
   6.149 -  type T = raw_param list
   6.150 -  val empty = default_default_params |> map (apsnd single)
   6.151 -  val extend = I
   6.152 -  fun merge data = AList.merge (op =) (K true) data
   6.153 -)
   6.154 -
   6.155 -val set_default_raw_param =
   6.156 -  Data.map o fold (AList.update (op =)) o normalize_raw_param
   6.157 -val default_raw_params = Data.get
   6.158 -
   6.159 -fun is_punctuation s = (s = "," orelse s = "-" orelse s = "\<emdash>")
   6.160 -
   6.161 -fun stringify_raw_param_value [] = ""
   6.162 -  | stringify_raw_param_value [s] = s
   6.163 -  | stringify_raw_param_value (s1 :: s2 :: ss) =
   6.164 -    s1 ^ (if is_punctuation s1 orelse is_punctuation s2 then "" else " ") ^
   6.165 -    stringify_raw_param_value (s2 :: ss)
   6.166 -
   6.167 -fun maxed_int_from_string min_int s = Int.max (min_int, the (Int.fromString s))
   6.168 -
   6.169 -fun extract_params ctxt mode default_params override_params =
   6.170 -  let
   6.171 -    val override_params = maps normalize_raw_param override_params
   6.172 -    val raw_params = rev override_params @ rev default_params
   6.173 -    val raw_lookup = AList.lookup (op =) raw_params
   6.174 -    val lookup = Option.map stringify_raw_param_value o raw_lookup
   6.175 -    val lookup_string = the_default "" o lookup
   6.176 -    fun general_lookup_bool option default_value name =
   6.177 -      case lookup name of
   6.178 -        SOME s => parse_bool_option option name s
   6.179 -      | NONE => default_value
   6.180 -    val lookup_bool = the o general_lookup_bool false (SOME false)
   6.181 -    val lookup_bool_option = general_lookup_bool true NONE
   6.182 -    fun do_int name value =
   6.183 -      case value of
   6.184 -        SOME s => (case Int.fromString s of
   6.185 -                     SOME i => i
   6.186 -                   | NONE => error ("Parameter " ^ quote name ^
   6.187 -                                    " must be assigned an integer value."))
   6.188 -      | NONE => 0
   6.189 -    fun lookup_int name = do_int name (lookup name)
   6.190 -    fun lookup_int_option name =
   6.191 -      case lookup name of
   6.192 -        SOME "smart" => NONE
   6.193 -      | value => SOME (do_int name value)
   6.194 -    fun int_range_from_string name min_int s =
   6.195 -      let
   6.196 -        val (k1, k2) =
   6.197 -          (case space_explode "-" s of
   6.198 -             [s] => the_default (s, s) (first_field "\<emdash>" s)
   6.199 -           | ["", s2] => ("-" ^ s2, "-" ^ s2)
   6.200 -           | [s1, s2] => (s1, s2)
   6.201 -           | _ => raise Option.Option)
   6.202 -          |> pairself (maxed_int_from_string min_int)
   6.203 -      in if k1 <= k2 then k1 upto k2 else k1 downto k2 end
   6.204 -      handle Option.Option =>
   6.205 -             error ("Parameter " ^ quote name ^
   6.206 -                    " must be assigned a sequence of integers.")
   6.207 -    fun int_seq_from_string name min_int s =
   6.208 -      maps (int_range_from_string name min_int) (space_explode "," s)
   6.209 -    fun lookup_int_seq name min_int =
   6.210 -      case lookup name of
   6.211 -        SOME s => (case int_seq_from_string name min_int s of
   6.212 -                     [] => [min_int]
   6.213 -                   | value => value)
   6.214 -      | NONE => [min_int]
   6.215 -    fun lookup_assigns read prefix default convert =
   6.216 -      (NONE, convert (the_default default (lookup prefix)))
   6.217 -      :: map (fn (name, value) =>
   6.218 -                 (SOME (read (String.extract (name, size prefix + 1, NONE))),
   6.219 -                  convert (stringify_raw_param_value value)))
   6.220 -             (filter (String.isPrefix (prefix ^ " ") o fst) raw_params)
   6.221 -    fun lookup_ints_assigns read prefix min_int =
   6.222 -      lookup_assigns read prefix (signed_string_of_int min_int)
   6.223 -                     (int_seq_from_string prefix min_int)
   6.224 -    fun lookup_bool_assigns read prefix =
   6.225 -      lookup_assigns read prefix "" (the o parse_bool_option false prefix)
   6.226 -    fun lookup_bool_option_assigns read prefix =
   6.227 -      lookup_assigns read prefix "" (parse_bool_option true prefix)
   6.228 -    fun lookup_strings_assigns read prefix =
   6.229 -      lookup_assigns read prefix "" (space_explode " ")
   6.230 -    fun lookup_time name =
   6.231 -      case lookup name of
   6.232 -        SOME s => parse_time name s
   6.233 -      | NONE => Time.zeroTime
   6.234 -    val read_type_polymorphic =
   6.235 -      Syntax.read_typ ctxt #> Logic.mk_type
   6.236 -      #> singleton (Variable.polymorphic ctxt) #> Logic.dest_type
   6.237 -    val read_term_polymorphic =
   6.238 -      Syntax.read_term ctxt #> singleton (Variable.polymorphic ctxt)
   6.239 -    val lookup_term_list_option_polymorphic =
   6.240 -      AList.lookup (op =) raw_params #> Option.map (map read_term_polymorphic)
   6.241 -    val read_const_polymorphic = read_term_polymorphic #> dest_Const
   6.242 -    val cards_assigns =
   6.243 -      lookup_ints_assigns read_type_polymorphic "card" 1
   6.244 -      |> mode = Auto_Try ? map (apsnd (take auto_try_max_scopes))
   6.245 -    val maxes_assigns = lookup_ints_assigns read_const_polymorphic "max" ~1
   6.246 -    val iters_assigns = lookup_ints_assigns read_const_polymorphic "iter" 0
   6.247 -    val bitss = lookup_int_seq "bits" 1
   6.248 -    val bisim_depths = lookup_int_seq "bisim_depth" ~1
   6.249 -    val boxes = lookup_bool_option_assigns read_type_polymorphic "box"
   6.250 -    val finitizes = lookup_bool_option_assigns read_type_polymorphic "finitize"
   6.251 -    val monos = if mode = Auto_Try then [(NONE, SOME true)]
   6.252 -                else lookup_bool_option_assigns read_type_polymorphic "mono"
   6.253 -    val stds = lookup_bool_assigns read_type_polymorphic "std"
   6.254 -    val wfs = lookup_bool_option_assigns read_const_polymorphic "wf"
   6.255 -    val sat_solver = lookup_string "sat_solver"
   6.256 -    val blocking = mode <> Normal orelse lookup_bool "blocking"
   6.257 -    val falsify = lookup_bool "falsify"
   6.258 -    val debug = (mode <> Auto_Try andalso lookup_bool "debug")
   6.259 -    val verbose = debug orelse (mode <> Auto_Try andalso lookup_bool "verbose")
   6.260 -    val overlord = lookup_bool "overlord"
   6.261 -    val spy = getenv "NITPICK_SPY" = "yes" orelse lookup_bool "spy"
   6.262 -    val user_axioms = lookup_bool_option "user_axioms"
   6.263 -    val assms = lookup_bool "assms"
   6.264 -    val whacks = lookup_term_list_option_polymorphic "whack" |> these
   6.265 -    val merge_type_vars = lookup_bool "merge_type_vars"
   6.266 -    val binary_ints = lookup_bool_option "binary_ints"
   6.267 -    val destroy_constrs = lookup_bool "destroy_constrs"
   6.268 -    val specialize = lookup_bool "specialize"
   6.269 -    val star_linear_preds = lookup_bool "star_linear_preds"
   6.270 -    val total_consts = lookup_bool_option "total_consts"
   6.271 -    val needs = lookup_term_list_option_polymorphic "need"
   6.272 -    val peephole_optim = lookup_bool "peephole_optim"
   6.273 -    val datatype_sym_break = lookup_int "datatype_sym_break"
   6.274 -    val kodkod_sym_break = lookup_int "kodkod_sym_break"
   6.275 -    val timeout = lookup_time "timeout"
   6.276 -    val tac_timeout = lookup_time "tac_timeout"
   6.277 -    val max_threads =
   6.278 -      if mode = Normal then Int.max (0, lookup_int "max_threads") else 1
   6.279 -    val show_datatypes = debug orelse lookup_bool "show_datatypes"
   6.280 -    val show_skolems = debug orelse lookup_bool "show_skolems"
   6.281 -    val show_consts = debug orelse lookup_bool "show_consts"
   6.282 -    val evals = lookup_term_list_option_polymorphic "eval" |> these
   6.283 -    val formats = lookup_ints_assigns read_term_polymorphic "format" 0
   6.284 -    val atomss = lookup_strings_assigns read_type_polymorphic "atoms"
   6.285 -    val max_potential =
   6.286 -      if mode = Normal then Int.max (0, lookup_int "max_potential") else 0
   6.287 -    val max_genuine = Int.max (0, lookup_int "max_genuine")
   6.288 -    val check_potential = lookup_bool "check_potential"
   6.289 -    val check_genuine = lookup_bool "check_genuine"
   6.290 -    val batch_size =
   6.291 -      case lookup_int_option "batch_size" of
   6.292 -        SOME n => Int.max (1, n)
   6.293 -      | NONE => if debug then 1 else 50
   6.294 -    val expect = lookup_string "expect"
   6.295 -  in
   6.296 -    {cards_assigns = cards_assigns, maxes_assigns = maxes_assigns, iters_assigns = iters_assigns,
   6.297 -     bitss = bitss, bisim_depths = bisim_depths, boxes = boxes, finitizes = finitizes,
   6.298 -     monos = monos, stds = stds, wfs = wfs, sat_solver = sat_solver, blocking = blocking,
   6.299 -     falsify = falsify, debug = debug, verbose = verbose, overlord = overlord, spy = spy,
   6.300 -     user_axioms = user_axioms, assms = assms, whacks = whacks, merge_type_vars = merge_type_vars,
   6.301 -     binary_ints = binary_ints, destroy_constrs = destroy_constrs, specialize = specialize,
   6.302 -     star_linear_preds = star_linear_preds, total_consts = total_consts, needs = needs,
   6.303 -     peephole_optim = peephole_optim, datatype_sym_break = datatype_sym_break,
   6.304 -     kodkod_sym_break = kodkod_sym_break, timeout = timeout, tac_timeout = tac_timeout,
   6.305 -     max_threads = max_threads, show_datatypes = show_datatypes, show_skolems = show_skolems,
   6.306 -     show_consts = show_consts, evals = evals, formats = formats, atomss = atomss,
   6.307 -     max_potential = max_potential, max_genuine = max_genuine, check_potential = check_potential,
   6.308 -     check_genuine = check_genuine, batch_size = batch_size, expect = expect}
   6.309 -  end
   6.310 -
   6.311 -fun default_params thy =
   6.312 -  extract_params (Proof_Context.init_global thy) Normal (default_raw_params thy)
   6.313 -  o map (apsnd single)
   6.314 -
   6.315 -val parse_key = Scan.repeat1 Parse.typ_group >> space_implode " "
   6.316 -val parse_value =
   6.317 -  Scan.repeat1 (Parse.minus >> single
   6.318 -                || Scan.repeat1 (Scan.unless Parse.minus
   6.319 -                                             (Parse.name || Parse.float_number))
   6.320 -                || @{keyword ","} |-- Parse.number >> prefix "," >> single)
   6.321 -  >> flat
   6.322 -val parse_param = parse_key -- Scan.optional (@{keyword "="} |-- parse_value) []
   6.323 -val parse_params =
   6.324 -  Scan.optional (@{keyword "["} |-- Parse.list parse_param --| @{keyword "]"}) []
   6.325 -
   6.326 -fun handle_exceptions ctxt f x =
   6.327 -  f x
   6.328 -  handle ARG (loc, details) =>
   6.329 -         error ("Bad argument(s) to " ^ quote loc ^ ": " ^ details ^ ".")
   6.330 -       | BAD (loc, details) =>
   6.331 -         error ("Internal error (" ^ quote loc ^ "): " ^ details ^ ".")
   6.332 -       | NOT_SUPPORTED details =>
   6.333 -         (warning ("Unsupported case: " ^ details ^ "."); x)
   6.334 -       | NUT (loc, us) =>
   6.335 -         error ("Invalid intermediate term" ^ plural_s_for_list us ^
   6.336 -                " (" ^ quote loc ^ "): " ^
   6.337 -                commas (map (string_for_nut ctxt) us) ^ ".")
   6.338 -       | REP (loc, Rs) =>
   6.339 -         error ("Invalid representation" ^ plural_s_for_list Rs ^
   6.340 -                " (" ^ quote loc ^ "): " ^ commas (map string_for_rep Rs) ^ ".")
   6.341 -       | TERM (loc, ts) =>
   6.342 -         error ("Invalid term" ^ plural_s_for_list ts ^
   6.343 -                " (" ^ quote loc ^ "): " ^
   6.344 -                commas (map (Syntax.string_of_term ctxt) ts) ^ ".")
   6.345 -       | TYPE (loc, Ts, ts) =>
   6.346 -         error ("Invalid type" ^ plural_s_for_list Ts ^
   6.347 -                (if null ts then
   6.348 -                   ""
   6.349 -                 else
   6.350 -                   " for term" ^ plural_s_for_list ts ^ " " ^
   6.351 -                   commas (map (quote o Syntax.string_of_term ctxt) ts)) ^
   6.352 -                " (" ^ quote loc ^ "): " ^
   6.353 -                commas (map (Syntax.string_of_typ ctxt) Ts) ^ ".")
   6.354 -
   6.355 -fun pick_nits override_params mode i step state =
   6.356 -  let
   6.357 -    val thy = Proof.theory_of state
   6.358 -    val ctxt = Proof.context_of state
   6.359 -    val _ = List.app check_raw_param override_params
   6.360 -    val params as {blocking, debug, ...} =
   6.361 -      extract_params ctxt mode (default_raw_params thy) override_params
   6.362 -    fun go () =
   6.363 -      (unknownN, state)
   6.364 -      |> (if mode = Auto_Try then perhaps o try
   6.365 -          else if debug then fn f => fn x => f x
   6.366 -          else handle_exceptions ctxt)
   6.367 -         (fn (_, state) => pick_nits_in_subgoal state params mode i step)
   6.368 -  in if blocking then go () else Future.fork (tap go) |> K (unknownN, state) end
   6.369 -  |> `(fn (outcome_code, _) => outcome_code = genuineN)
   6.370 -
   6.371 -fun string_for_raw_param (name, value) =
   6.372 -  name ^ " = " ^ stringify_raw_param_value value
   6.373 -
   6.374 -fun nitpick_params_trans params =
   6.375 -  Toplevel.theory
   6.376 -      (fold set_default_raw_param params
   6.377 -       #> tap (fn thy =>
   6.378 -                  writeln ("Default parameters for Nitpick:\n" ^
   6.379 -                           (case rev (default_raw_params thy) of
   6.380 -                              [] => "none"
   6.381 -                            | params =>
   6.382 -                              (map check_raw_param params;
   6.383 -                               params |> map string_for_raw_param
   6.384 -                                      |> sort_strings |> cat_lines)))))
   6.385 -
   6.386 -val _ =
   6.387 -  Outer_Syntax.improper_command @{command_spec "nitpick"}
   6.388 -    "try to find a counterexample for a given subgoal using Nitpick"
   6.389 -    (parse_params -- Scan.optional Parse.nat 1 >> (fn (params, i) =>
   6.390 -      Toplevel.unknown_proof o
   6.391 -      Toplevel.keep (fn state =>
   6.392 -        ignore (pick_nits params Normal i (Toplevel.proof_position_of state)
   6.393 -          (Toplevel.proof_of state)))))
   6.394 -
   6.395 -val _ =
   6.396 -  Outer_Syntax.command @{command_spec "nitpick_params"}
   6.397 -    "set and display the default parameters for Nitpick"
   6.398 -    (parse_params #>> nitpick_params_trans)
   6.399 -
   6.400 -fun try_nitpick auto = pick_nits [] (if auto then Auto_Try else Try) 1 0
   6.401 -
   6.402 -val _ = Try.tool_setup (nitpickN, (50, @{option auto_nitpick}, try_nitpick))
   6.403 -
   6.404 -end;
     7.1 --- a/src/HOL/Tools/Nitpick/nitpick_tests.ML	Fri Jan 31 10:23:32 2014 +0100
     7.2 +++ b/src/HOL/Tools/Nitpick/nitpick_tests.ML	Fri Jan 31 10:23:32 2014 +0100
     7.3 @@ -1,4 +1,4 @@
     7.4 -(*  Title:      HOL/Tools/Nitpick/nitpick_tests.ML
     7.5 +Nitpick_Commands(*  Title:      HOL/Tools/Nitpick/nitpick_tests.ML
     7.6      Author:     Jasmin Blanchette, TU Muenchen
     7.7      Copyright   2008, 2009, 2010
     7.8  
     7.9 @@ -211,7 +211,7 @@
    7.10  
    7.11  fun run_all_tests () =
    7.12    let
    7.13 -    val {debug, overlord, timeout, ...} = Nitpick_Isar.default_params @{theory} []
    7.14 +    val {debug, overlord, timeout, ...} = Nitpick_Commands.default_params @{theory} []
    7.15      val max_threads = 1
    7.16      val max_solutions = 1
    7.17    in