src/HOL/Tools/Nitpick/nitpick_isar.ML
author blanchet
Fri Mar 19 15:07:44 2010 +0100 (2010-03-19)
changeset 35866 513074557e06
parent 35665 ff2bf50505ab
child 35964 77f2cb359b49
permissions -rw-r--r--
move the Sledgehammer Isar commands together into one file;
this will make easier to add options and reorganize them later
blanchet@33982
     1
(*  Title:      HOL/Tools/Nitpick/nitpick_isar.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@33192
     9
signature NITPICK_ISAR =
blanchet@33192
    10
sig
blanchet@33192
    11
  type params = Nitpick.params
blanchet@33192
    12
blanchet@33561
    13
  val auto: bool Unsynchronized.ref
blanchet@33192
    14
  val default_params : theory -> (string * string) list -> params
blanchet@33561
    15
  val setup : theory -> theory
blanchet@35866
    16
end;
blanchet@33192
    17
blanchet@33232
    18
structure Nitpick_Isar : NITPICK_ISAR =
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@33561
    27
val auto = Unsynchronized.ref false;
blanchet@33561
    28
wenzelm@33601
    29
val _ =
wenzelm@33601
    30
  ProofGeneralPgip.add_preference Preferences.category_tracing
blanchet@34982
    31
      (Preferences.bool_pref auto "auto-nitpick"
blanchet@34982
    32
           "Whether to run Nitpick automatically.")
blanchet@33561
    33
blanchet@33192
    34
type raw_param = string * string list
blanchet@33192
    35
blanchet@33192
    36
val default_default_params =
blanchet@33192
    37
  [("card", ["1\<midarrow>8"]),
blanchet@33192
    38
   ("iter", ["0,1,2,4,8,12,16,24"]),
blanchet@34124
    39
   ("bits", ["1,2,3,4,6,8,10,12"]),
blanchet@33192
    40
   ("bisim_depth", ["7"]),
blanchet@33192
    41
   ("box", ["smart"]),
blanchet@35665
    42
   ("finitize", ["smart"]),
blanchet@33192
    43
   ("mono", ["smart"]),
blanchet@34982
    44
   ("std", ["true"]),
blanchet@33192
    45
   ("wf", ["smart"]),
blanchet@33192
    46
   ("sat_solver", ["smart"]),
blanchet@33192
    47
   ("batch_size", ["smart"]),
blanchet@33192
    48
   ("blocking", ["true"]),
blanchet@33192
    49
   ("falsify", ["true"]),
blanchet@33192
    50
   ("user_axioms", ["smart"]),
blanchet@33192
    51
   ("assms", ["true"]),
blanchet@33556
    52
   ("merge_type_vars", ["false"]),
blanchet@34124
    53
   ("binary_ints", ["smart"]),
blanchet@33192
    54
   ("destroy_constrs", ["true"]),
blanchet@33192
    55
   ("specialize", ["true"]),
blanchet@33192
    56
   ("skolemize", ["true"]),
blanchet@33192
    57
   ("star_linear_preds", ["true"]),
blanchet@33192
    58
   ("uncurry", ["true"]),
blanchet@33192
    59
   ("fast_descrs", ["true"]),
blanchet@33192
    60
   ("peephole_optim", ["true"]),
blanchet@33192
    61
   ("timeout", ["30 s"]),
blanchet@33192
    62
   ("tac_timeout", ["500 ms"]),
blanchet@33192
    63
   ("sym_break", ["20"]),
blanchet@33192
    64
   ("sharing_depth", ["3"]),
blanchet@33192
    65
   ("flatten_props", ["false"]),
blanchet@33192
    66
   ("max_threads", ["0"]),
blanchet@33192
    67
   ("verbose", ["false"]),
blanchet@33192
    68
   ("debug", ["false"]),
blanchet@33197
    69
   ("overlord", ["false"]),
blanchet@33192
    70
   ("show_all", ["false"]),
blanchet@33192
    71
   ("show_skolems", ["true"]),
blanchet@33192
    72
   ("show_datatypes", ["false"]),
blanchet@33192
    73
   ("show_consts", ["false"]),
blanchet@33192
    74
   ("format", ["1"]),
blanchet@33192
    75
   ("max_potential", ["1"]),
blanchet@33192
    76
   ("max_genuine", ["1"]),
blanchet@33192
    77
   ("check_potential", ["false"]),
blanchet@33192
    78
   ("check_genuine", ["false"])]
blanchet@33192
    79
blanchet@33192
    80
val negated_params =
blanchet@33192
    81
  [("dont_box", "box"),
blanchet@35665
    82
   ("dont_finitize", "finitize"),
blanchet@33192
    83
   ("non_mono", "mono"),
blanchet@34982
    84
   ("non_std", "std"),
blanchet@33192
    85
   ("non_wf", "wf"),
blanchet@33192
    86
   ("non_blocking", "blocking"),
blanchet@33192
    87
   ("satisfy", "falsify"),
blanchet@33192
    88
   ("no_user_axioms", "user_axioms"),
blanchet@33192
    89
   ("no_assms", "assms"),
blanchet@33556
    90
   ("dont_merge_type_vars", "merge_type_vars"),
blanchet@34124
    91
   ("unary_ints", "binary_ints"),
blanchet@33192
    92
   ("dont_destroy_constrs", "destroy_constrs"),
blanchet@33192
    93
   ("dont_specialize", "specialize"),
blanchet@33192
    94
   ("dont_skolemize", "skolemize"),
blanchet@33192
    95
   ("dont_star_linear_preds", "star_linear_preds"),
blanchet@33192
    96
   ("dont_uncurry", "uncurry"),
blanchet@33192
    97
   ("full_descrs", "fast_descrs"),
blanchet@33192
    98
   ("no_peephole_optim", "peephole_optim"),
blanchet@33192
    99
   ("dont_flatten_props", "flatten_props"),
blanchet@33192
   100
   ("quiet", "verbose"),
blanchet@33192
   101
   ("no_debug", "debug"),
blanchet@33192
   102
   ("no_overlord", "overlord"),
blanchet@33192
   103
   ("dont_show_all", "show_all"),
blanchet@33192
   104
   ("hide_skolems", "show_skolems"),
blanchet@33192
   105
   ("hide_datatypes", "show_datatypes"),
blanchet@33192
   106
   ("hide_consts", "show_consts"),
blanchet@33192
   107
   ("trust_potential", "check_potential"),
blanchet@33192
   108
   ("trust_genuine", "check_genuine")]
blanchet@33192
   109
blanchet@33192
   110
(* string -> bool *)
blanchet@33192
   111
fun is_known_raw_param s =
blanchet@34936
   112
  AList.defined (op =) default_default_params s orelse
blanchet@34936
   113
  AList.defined (op =) negated_params s orelse
blanchet@34936
   114
  s = "max" orelse s = "eval" orelse s = "expect" orelse
blanchet@34936
   115
  exists (fn p => String.isPrefix (p ^ " ") s)
blanchet@35665
   116
         ["card", "max", "iter", "box", "dont_box", "finitize", "dont_finitize",
blanchet@35665
   117
          "mono", "non_mono", "std", "non_std", "wf", "non_wf", "format"]
blanchet@33192
   118
blanchet@33192
   119
(* string * 'a -> unit *)
blanchet@33192
   120
fun check_raw_param (s, _) =
blanchet@33192
   121
  if is_known_raw_param s then ()
blanchet@33192
   122
  else error ("Unknown parameter " ^ quote s ^ ".")  
blanchet@33192
   123
blanchet@33192
   124
(* string -> string option *)
blanchet@33192
   125
fun unnegate_param_name name =
blanchet@33192
   126
  case AList.lookup (op =) negated_params name of
blanchet@33192
   127
    NONE => if String.isPrefix "dont_" name then SOME (unprefix "dont_" name)
blanchet@33192
   128
            else if String.isPrefix "non_" name then SOME (unprefix "non_" name)
blanchet@33192
   129
            else NONE
blanchet@33192
   130
  | some_name => some_name
blanchet@33192
   131
(* raw_param -> raw_param *)
blanchet@33192
   132
fun unnegate_raw_param (name, value) =
blanchet@33192
   133
  case unnegate_param_name name of
blanchet@33192
   134
    SOME name' => (name', case value of
blanchet@33192
   135
                            ["false"] => ["true"]
blanchet@33192
   136
                          | ["true"] => ["false"]
blanchet@33192
   137
                          | [] => ["false"]
blanchet@33192
   138
                          | _ => value)
blanchet@33192
   139
  | NONE => (name, value)
blanchet@33192
   140
blanchet@33583
   141
structure Data = Theory_Data(
blanchet@33561
   142
  type T = {params: raw_param list}
blanchet@33561
   143
  val empty = {params = rev default_default_params}
blanchet@33192
   144
  val extend = I
wenzelm@33599
   145
  fun merge ({params = ps1}, {params = ps2}) : T =
wenzelm@33699
   146
    {params = AList.merge (op =) (K true) (ps1, ps2)})
blanchet@33192
   147
blanchet@33192
   148
(* raw_param -> theory -> theory *)
blanchet@33192
   149
fun set_default_raw_param param thy =
blanchet@33583
   150
  let val {params} = Data.get thy in
blanchet@33583
   151
    Data.put {params = AList.update (op =) (unnegate_raw_param param) params}
blanchet@33583
   152
             thy
blanchet@33192
   153
  end
blanchet@33192
   154
(* theory -> raw_param list *)
blanchet@33583
   155
val default_raw_params = #params o Data.get
blanchet@33192
   156
blanchet@33192
   157
(* string -> bool *)
blanchet@33192
   158
fun is_punctuation s = (s = "," orelse s = "-" orelse s = "\<midarrow>")
blanchet@33192
   159
blanchet@33192
   160
(* string list -> string *)
blanchet@33192
   161
fun stringify_raw_param_value [] = ""
blanchet@33192
   162
  | stringify_raw_param_value [s] = s
blanchet@33192
   163
  | stringify_raw_param_value (s1 :: s2 :: ss) =
blanchet@33192
   164
    s1 ^ (if is_punctuation s1 orelse is_punctuation s2 then "" else " ") ^
blanchet@33192
   165
    stringify_raw_param_value (s2 :: ss)
blanchet@33192
   166
blanchet@33192
   167
(* bool -> string -> string -> bool option *)
blanchet@33192
   168
fun bool_option_from_string option name s =
blanchet@33192
   169
  (case s of
blanchet@33192
   170
     "smart" => if option then NONE else raise Option
blanchet@33192
   171
   | "false" => SOME false
blanchet@33192
   172
   | "true" => SOME true
blanchet@33192
   173
   | "" => SOME true
blanchet@35280
   174
   | _ => raise Option)
blanchet@33192
   175
  handle Option.Option =>
blanchet@33192
   176
         let val ss = map quote ((option ? cons "smart") ["true", "false"]) in
blanchet@33192
   177
           error ("Parameter " ^ quote name ^ " must be assigned " ^
blanchet@33192
   178
                  space_implode " " (serial_commas "or" ss) ^ ".")
blanchet@33192
   179
         end
blanchet@33192
   180
(* bool -> raw_param list -> bool option -> string -> bool option *)
blanchet@33192
   181
fun general_lookup_bool option raw_params default_value name =
blanchet@33192
   182
  case AList.lookup (op =) raw_params name of
blanchet@33192
   183
    SOME s => s |> stringify_raw_param_value
blanchet@33192
   184
                |> bool_option_from_string option name
blanchet@33192
   185
  | NONE => default_value
blanchet@33192
   186
blanchet@33192
   187
(* int -> string -> int *)
blanchet@33192
   188
fun maxed_int_from_string min_int s = Int.max (min_int, the (Int.fromString s))
blanchet@33192
   189
blanchet@33192
   190
(* Proof.context -> bool -> raw_param list -> raw_param list -> params *)
blanchet@33192
   191
fun extract_params ctxt auto default_params override_params =
blanchet@33192
   192
  let
blanchet@33192
   193
    val override_params = map unnegate_raw_param override_params
blanchet@33192
   194
    val raw_params = rev override_params @ rev default_params
blanchet@33192
   195
    val lookup =
blanchet@33192
   196
      Option.map stringify_raw_param_value o AList.lookup (op =) raw_params
blanchet@33192
   197
    (* string -> string *)
blanchet@33192
   198
    fun lookup_string name = the_default "" (lookup name)
blanchet@33192
   199
    (* string -> bool *)
blanchet@33192
   200
    val lookup_bool = the o general_lookup_bool false raw_params (SOME false)
blanchet@33192
   201
    (* string -> bool option *)
blanchet@33192
   202
    val lookup_bool_option = general_lookup_bool true raw_params NONE
blanchet@33192
   203
    (* string -> string option -> int *)
blanchet@33192
   204
    fun do_int name value =
blanchet@33192
   205
      case value of
blanchet@33192
   206
        SOME s => (case Int.fromString s of
blanchet@33192
   207
                     SOME i => i
blanchet@33192
   208
                   | NONE => error ("Parameter " ^ quote name ^
blanchet@33192
   209
                                    " must be assigned an integer value."))
blanchet@33192
   210
      | NONE => 0
blanchet@33192
   211
    (* string -> int *)
blanchet@33192
   212
    fun lookup_int name = do_int name (lookup name)
blanchet@33192
   213
    (* string -> int option *)
blanchet@33192
   214
    fun lookup_int_option name =
blanchet@33192
   215
      case lookup name of
blanchet@33192
   216
        SOME "smart" => NONE
blanchet@33192
   217
      | value => SOME (do_int name value)
blanchet@33192
   218
    (* string -> int -> string -> int list *)
blanchet@33192
   219
    fun int_range_from_string name min_int s =
blanchet@33192
   220
      let
blanchet@33192
   221
        val (k1, k2) =
blanchet@33192
   222
          (case space_explode "-" s of
blanchet@33192
   223
             [s] => the_default (s, s) (first_field "\<midarrow>" s)
blanchet@33192
   224
           | ["", s2] => ("-" ^ s2, "-" ^ s2)
blanchet@33192
   225
           | [s1, s2] => (s1, s2)
blanchet@33192
   226
           | _ => raise Option)
blanchet@33192
   227
          |> pairself (maxed_int_from_string min_int)
blanchet@33192
   228
      in if k1 <= k2 then k1 upto k2 else k1 downto k2 end
blanchet@33192
   229
      handle Option.Option =>
blanchet@33192
   230
             error ("Parameter " ^ quote name ^
blanchet@33192
   231
                    " must be assigned a sequence of integers.")
blanchet@33192
   232
    (* string -> int -> string -> int list *)
blanchet@33192
   233
    fun int_seq_from_string name min_int s =
blanchet@33192
   234
      maps (int_range_from_string name min_int) (space_explode "," s)
blanchet@33192
   235
    (* string -> int -> int list *)
blanchet@33192
   236
    fun lookup_int_seq name min_int =
blanchet@33192
   237
      case lookup name of
blanchet@33192
   238
        SOME s => (case int_seq_from_string name min_int s of
blanchet@33192
   239
                     [] => [min_int]
blanchet@33192
   240
                   | value => value)
blanchet@33192
   241
      | NONE => [min_int]
blanchet@33192
   242
    (* (string -> 'a) -> int -> string -> ('a option * int list) list *)
blanchet@33192
   243
    fun lookup_ints_assigns read prefix min_int =
blanchet@33192
   244
      (NONE, lookup_int_seq prefix min_int)
blanchet@33192
   245
      :: map (fn (name, value) =>
blanchet@33192
   246
                 (SOME (read (String.extract (name, size prefix + 1, NONE))),
blanchet@33192
   247
                  value |> stringify_raw_param_value
blanchet@33192
   248
                        |> int_seq_from_string name min_int))
blanchet@33192
   249
             (filter (String.isPrefix (prefix ^ " ") o fst) raw_params)
blanchet@34982
   250
    (* (string -> 'a) -> string -> ('a option * bool) list *)
blanchet@34982
   251
    fun lookup_bool_assigns read prefix =
blanchet@34982
   252
      (NONE, lookup_bool prefix)
blanchet@34982
   253
      :: map (fn (name, value) =>
blanchet@34982
   254
                 (SOME (read (String.extract (name, size prefix + 1, NONE))),
blanchet@34982
   255
                  value |> stringify_raw_param_value
blanchet@34982
   256
                        |> bool_option_from_string false name |> the))
blanchet@34982
   257
             (filter (String.isPrefix (prefix ^ " ") o fst) raw_params)
blanchet@33192
   258
    (* (string -> 'a) -> string -> ('a option * bool option) list *)
blanchet@33192
   259
    fun lookup_bool_option_assigns read prefix =
blanchet@33192
   260
      (NONE, lookup_bool_option prefix)
blanchet@33192
   261
      :: map (fn (name, value) =>
blanchet@33192
   262
                 (SOME (read (String.extract (name, size prefix + 1, NONE))),
blanchet@33192
   263
                  value |> stringify_raw_param_value
blanchet@33192
   264
                        |> bool_option_from_string true name))
blanchet@33192
   265
             (filter (String.isPrefix (prefix ^ " ") o fst) raw_params)
blanchet@33192
   266
    (* string -> Time.time option *)
blanchet@33192
   267
    fun lookup_time name =
blanchet@33192
   268
      case lookup name of
blanchet@33192
   269
        NONE => NONE
blanchet@33192
   270
      | SOME "none" => NONE
blanchet@33192
   271
      | SOME s =>
blanchet@33192
   272
        let
blanchet@33192
   273
          val msecs =
blanchet@33192
   274
            case space_explode " " s of
blanchet@33192
   275
              [s1, "min"] => 60000 * the (Int.fromString s1)
blanchet@33192
   276
            | [s1, "s"] => 1000 * the (Int.fromString s1)
blanchet@33192
   277
            | [s1, "ms"] => the (Int.fromString s1)
blanchet@33192
   278
            | _ => 0
blanchet@33192
   279
        in
blanchet@33192
   280
          if msecs <= 0 then
blanchet@33192
   281
            error ("Parameter " ^ quote name ^ " must be assigned a positive \
blanchet@33192
   282
                   \time value (e.g., \"60 s\", \"200 ms\") or \"none\".")
blanchet@33192
   283
          else
blanchet@33192
   284
            SOME (Time.fromMilliseconds msecs)
blanchet@33192
   285
        end
blanchet@33192
   286
    (* string -> term list *)
blanchet@33192
   287
    val lookup_term_list =
blanchet@33192
   288
      AList.lookup (op =) raw_params #> these #> Syntax.read_terms ctxt
blanchet@33192
   289
    val read_type_polymorphic =
blanchet@33192
   290
      Syntax.read_typ ctxt #> Logic.mk_type
blanchet@33192
   291
      #> singleton (Variable.polymorphic ctxt) #> Logic.dest_type
blanchet@33192
   292
    (* string -> term *)
blanchet@33192
   293
    val read_term_polymorphic =
blanchet@33192
   294
      Syntax.read_term ctxt #> singleton (Variable.polymorphic ctxt)
blanchet@33192
   295
    (* string -> styp *)
blanchet@33192
   296
    val read_const_polymorphic = read_term_polymorphic #> dest_Const
blanchet@33192
   297
    val cards_assigns = lookup_ints_assigns read_type_polymorphic "card" 1
blanchet@33192
   298
    val maxes_assigns = lookup_ints_assigns read_const_polymorphic "max" ~1
blanchet@33192
   299
    val iters_assigns = lookup_ints_assigns read_const_polymorphic "iter" 0
blanchet@34124
   300
    val bitss = lookup_int_seq "bits" 1
blanchet@33192
   301
    val bisim_depths = lookup_int_seq "bisim_depth" ~1
blanchet@35665
   302
    val boxes = lookup_bool_option_assigns read_type_polymorphic "box"
blanchet@35665
   303
    val finitizes = lookup_bool_option_assigns read_type_polymorphic "finitize"
blanchet@33192
   304
    val monos = lookup_bool_option_assigns read_type_polymorphic "mono"
blanchet@34982
   305
    val stds = lookup_bool_assigns read_type_polymorphic "std"
blanchet@33192
   306
    val wfs = lookup_bool_option_assigns read_const_polymorphic "wf"
blanchet@33192
   307
    val sat_solver = lookup_string "sat_solver"
blanchet@33192
   308
    val blocking = not auto andalso lookup_bool "blocking"
blanchet@33192
   309
    val falsify = lookup_bool "falsify"
blanchet@33192
   310
    val debug = not auto andalso lookup_bool "debug"
blanchet@33192
   311
    val verbose = debug orelse (not auto andalso lookup_bool "verbose")
blanchet@33192
   312
    val overlord = lookup_bool "overlord"
blanchet@33192
   313
    val user_axioms = lookup_bool_option "user_axioms"
blanchet@33192
   314
    val assms = lookup_bool "assms"
blanchet@33556
   315
    val merge_type_vars = lookup_bool "merge_type_vars"
blanchet@34124
   316
    val binary_ints = lookup_bool_option "binary_ints"
blanchet@33192
   317
    val destroy_constrs = lookup_bool "destroy_constrs"
blanchet@33192
   318
    val specialize = lookup_bool "specialize"
blanchet@33192
   319
    val skolemize = lookup_bool "skolemize"
blanchet@33192
   320
    val star_linear_preds = lookup_bool "star_linear_preds"
blanchet@33192
   321
    val uncurry = lookup_bool "uncurry"
blanchet@33192
   322
    val fast_descrs = lookup_bool "fast_descrs"
blanchet@33192
   323
    val peephole_optim = lookup_bool "peephole_optim"
blanchet@33561
   324
    val timeout = if auto then NONE else lookup_time "timeout"
blanchet@33192
   325
    val tac_timeout = lookup_time "tac_timeout"
blanchet@33192
   326
    val sym_break = Int.max (0, lookup_int "sym_break")
blanchet@33192
   327
    val sharing_depth = Int.max (1, lookup_int "sharing_depth")
blanchet@33192
   328
    val flatten_props = lookup_bool "flatten_props"
blanchet@33192
   329
    val max_threads = Int.max (0, lookup_int "max_threads")
blanchet@33192
   330
    val show_all = debug orelse lookup_bool "show_all"
blanchet@33192
   331
    val show_skolems = show_all orelse lookup_bool "show_skolems"
blanchet@33192
   332
    val show_datatypes = show_all orelse lookup_bool "show_datatypes"
blanchet@33192
   333
    val show_consts = show_all orelse lookup_bool "show_consts"
blanchet@33192
   334
    val formats = lookup_ints_assigns read_term_polymorphic "format" 0
blanchet@33192
   335
    val evals = lookup_term_list "eval"
blanchet@33561
   336
    val max_potential =
blanchet@33561
   337
      if auto then 0 else Int.max (0, lookup_int "max_potential")
blanchet@33192
   338
    val max_genuine = Int.max (0, lookup_int "max_genuine")
blanchet@33192
   339
    val check_potential = lookup_bool "check_potential"
blanchet@33192
   340
    val check_genuine = lookup_bool "check_genuine"
blanchet@33192
   341
    val batch_size = case lookup_int_option "batch_size" of
blanchet@33192
   342
                       SOME n => Int.max (1, n)
blanchet@33192
   343
                     | NONE => if debug then 1 else 64
blanchet@33192
   344
    val expect = lookup_string "expect"
blanchet@33192
   345
  in
blanchet@33192
   346
    {cards_assigns = cards_assigns, maxes_assigns = maxes_assigns,
blanchet@34124
   347
     iters_assigns = iters_assigns, bitss = bitss, bisim_depths = bisim_depths,
blanchet@35665
   348
     boxes = boxes, finitizes = finitizes, monos = monos, stds = stds,
blanchet@35665
   349
     wfs = wfs, sat_solver = sat_solver, blocking = blocking, falsify = falsify,
blanchet@34982
   350
     debug = debug, verbose = verbose, overlord = overlord,
blanchet@34982
   351
     user_axioms = user_axioms, assms = assms,
blanchet@34124
   352
     merge_type_vars = merge_type_vars, binary_ints = binary_ints,
blanchet@34124
   353
     destroy_constrs = destroy_constrs, specialize = specialize,
blanchet@34124
   354
     skolemize = skolemize, star_linear_preds = star_linear_preds,
blanchet@34124
   355
     uncurry = uncurry, fast_descrs = fast_descrs,
blanchet@34124
   356
     peephole_optim = peephole_optim, timeout = timeout,
blanchet@34124
   357
     tac_timeout = tac_timeout, sym_break = sym_break,
blanchet@33192
   358
     sharing_depth = sharing_depth, flatten_props = flatten_props,
blanchet@33192
   359
     max_threads = max_threads, show_skolems = show_skolems,
blanchet@33192
   360
     show_datatypes = show_datatypes, show_consts = show_consts,
blanchet@33192
   361
     formats = formats, evals = evals, max_potential = max_potential,
blanchet@33192
   362
     max_genuine = max_genuine, check_potential = check_potential,
blanchet@33192
   363
     check_genuine = check_genuine, batch_size = batch_size, expect = expect}
blanchet@33192
   364
  end
blanchet@33192
   365
blanchet@33192
   366
(* theory -> (string * string) list -> params *)
blanchet@33192
   367
fun default_params thy =
blanchet@33192
   368
  extract_params (ProofContext.init thy) false (default_raw_params thy)
blanchet@33192
   369
  o map (apsnd single)
blanchet@33192
   370
blanchet@33192
   371
(* OuterParse.token list -> string * OuterParse.token list *)
blanchet@33192
   372
val scan_key = Scan.repeat1 OuterParse.typ_group >> space_implode " "
blanchet@33192
   373
blanchet@33192
   374
(* OuterParse.token list -> string list * OuterParse.token list *)
blanchet@33192
   375
val scan_value =
blanchet@33192
   376
  Scan.repeat1 (OuterParse.minus >> single
blanchet@33192
   377
                || Scan.repeat1 (Scan.unless OuterParse.minus OuterParse.name)
blanchet@33192
   378
                || OuterParse.$$$ "," |-- OuterParse.number >> prefix ","
blanchet@33192
   379
                   >> single) >> flat
blanchet@33192
   380
blanchet@33192
   381
(* OuterParse.token list -> raw_param * OuterParse.token list *)
blanchet@33192
   382
val scan_param =
blanchet@33192
   383
  scan_key -- (Scan.option (OuterParse.$$$ "=" |-- scan_value) >> these)
blanchet@33192
   384
(* OuterParse.token list -> raw_param list option * OuterParse.token list *)
blanchet@33192
   385
val scan_params = Scan.option (OuterParse.$$$ "[" |-- OuterParse.list scan_param
blanchet@33192
   386
                               --| OuterParse.$$$ "]")
blanchet@33192
   387
blanchet@33192
   388
(* Proof.context -> ('a -> 'a) -> 'a -> 'a *)
blanchet@33192
   389
fun handle_exceptions ctxt f x =
blanchet@33192
   390
  f x
blanchet@33192
   391
  handle ARG (loc, details) =>
blanchet@33192
   392
         error ("Bad argument(s) to " ^ quote loc ^ ": " ^ details ^ ".")
blanchet@33192
   393
       | BAD (loc, details) =>
blanchet@33192
   394
         error ("Internal error (" ^ quote loc ^ "): " ^ details ^ ".")
blanchet@33192
   395
       | NOT_SUPPORTED details =>
blanchet@33192
   396
         (warning ("Unsupported case: " ^ details ^ "."); x)
blanchet@33192
   397
       | NUT (loc, us) =>
blanchet@33192
   398
         error ("Invalid intermediate term" ^ plural_s_for_list us ^
blanchet@33192
   399
                " (" ^ quote loc ^ "): " ^
blanchet@33192
   400
                commas (map (string_for_nut ctxt) us) ^ ".")
blanchet@33192
   401
       | REP (loc, Rs) =>
blanchet@33192
   402
         error ("Invalid representation" ^ plural_s_for_list Rs ^
blanchet@33192
   403
                " (" ^ quote loc ^ "): " ^ commas (map string_for_rep Rs) ^ ".")
blanchet@33192
   404
       | TERM (loc, ts) =>
blanchet@33192
   405
         error ("Invalid term" ^ plural_s_for_list ts ^
blanchet@33192
   406
                " (" ^ quote loc ^ "): " ^
blanchet@33192
   407
                commas (map (Syntax.string_of_term ctxt) ts) ^ ".")
blanchet@34124
   408
       | TOO_LARGE (_, details) =>
blanchet@34124
   409
         (warning ("Limit reached: " ^ details ^ "."); x)
blanchet@34124
   410
       | TOO_SMALL (_, details) =>
blanchet@34124
   411
         (warning ("Limit reached: " ^ details ^ "."); x)
blanchet@33192
   412
       | TYPE (loc, Ts, ts) =>
blanchet@33192
   413
         error ("Invalid type" ^ plural_s_for_list Ts ^
blanchet@33192
   414
                (if null ts then
blanchet@33192
   415
                   ""
blanchet@33192
   416
                 else
blanchet@33192
   417
                   " for term" ^ plural_s_for_list ts ^ " " ^
blanchet@33192
   418
                   commas (map (quote o Syntax.string_of_term ctxt) ts)) ^
blanchet@33192
   419
                " (" ^ quote loc ^ "): " ^
blanchet@33192
   420
                commas (map (Syntax.string_of_typ ctxt) Ts) ^ ".")
blanchet@33192
   421
       | Kodkod.SYNTAX (_, details) =>
blanchet@33192
   422
         (warning ("Ill-formed Kodkodi output: " ^ details ^ "."); x)
blanchet@33192
   423
       | Refute.REFUTE (loc, details) =>
blanchet@33192
   424
         error ("Unhandled Refute error (" ^ quote loc ^ "): " ^ details ^ ".")
blanchet@33192
   425
blanchet@34982
   426
blanchet@34982
   427
(* raw_param list -> bool -> int -> int -> Proof.state -> bool * Proof.state *)
blanchet@34982
   428
fun pick_nits override_params auto i step state =
blanchet@33192
   429
  let
blanchet@33192
   430
    val thy = Proof.theory_of state
blanchet@33192
   431
    val ctxt = Proof.context_of state
blanchet@33192
   432
    val _ = List.app check_raw_param override_params
blanchet@33192
   433
    val params as {blocking, debug, ...} =
blanchet@33192
   434
      extract_params ctxt auto (default_raw_params thy) override_params
blanchet@33561
   435
    (* unit -> bool * Proof.state *)
blanchet@33192
   436
    fun go () =
blanchet@33561
   437
      (false, state)
blanchet@33561
   438
      |> (if auto then perhaps o try
blanchet@33561
   439
          else if debug then fn f => fn x => f x
blanchet@33561
   440
          else handle_exceptions ctxt)
blanchet@34982
   441
         (fn (_, state) => pick_nits_in_subgoal state params auto i step
blanchet@34121
   442
                           |>> curry (op =) "genuine")
blanchet@33192
   443
  in
blanchet@33561
   444
    if auto orelse blocking then go ()
wenzelm@33604
   445
    else (Toplevel.thread true (fn () => (go (); ())); (false, state))
blanchet@33192
   446
  end
blanchet@33192
   447
blanchet@34121
   448
(* raw_param list option * int option -> Toplevel.transition
blanchet@34121
   449
   -> Toplevel.transition *)
blanchet@34121
   450
fun nitpick_trans (opt_params, opt_i) =
blanchet@34982
   451
  Toplevel.keep (fn st =>
blanchet@34982
   452
      (pick_nits (these opt_params) false (the_default 1 opt_i)
blanchet@34982
   453
                 (Toplevel.proof_position_of st) (Toplevel.proof_of st); ()))
blanchet@33192
   454
blanchet@33192
   455
(* raw_param -> string *)
blanchet@33192
   456
fun string_for_raw_param (name, value) =
blanchet@33192
   457
  name ^ " = " ^ stringify_raw_param_value value
blanchet@33192
   458
blanchet@34121
   459
(* raw_param list option -> Toplevel.transition -> Toplevel.transition *)
blanchet@33192
   460
fun nitpick_params_trans opt_params =
blanchet@33192
   461
  Toplevel.theory
blanchet@33561
   462
      (fold set_default_raw_param (these opt_params)
blanchet@33561
   463
       #> tap (fn thy => 
blanchet@33561
   464
                  writeln ("Default parameters for Nitpick:\n" ^
blanchet@33561
   465
                           (case rev (default_raw_params thy) of
blanchet@33561
   466
                              [] => "none"
blanchet@33561
   467
                            | params =>
blanchet@33561
   468
                              (map check_raw_param params;
blanchet@33561
   469
                               params |> map string_for_raw_param
blanchet@33561
   470
                                      |> sort_strings |> cat_lines)))))
blanchet@33192
   471
blanchet@33192
   472
(* OuterParse.token list
blanchet@33192
   473
   -> (Toplevel.transition -> Toplevel.transition) * OuterParse.token list *)
blanchet@33561
   474
val scan_nitpick_command =
blanchet@33561
   475
  (scan_params -- Scan.option OuterParse.nat) #>> nitpick_trans
blanchet@33561
   476
val scan_nitpick_params_command = scan_params #>> nitpick_params_trans
blanchet@33192
   477
blanchet@33192
   478
val _ = OuterSyntax.improper_command "nitpick"
blanchet@33192
   479
            "try to find a counterexample for a given subgoal using Kodkod"
blanchet@33192
   480
            OuterKeyword.diag scan_nitpick_command
blanchet@33192
   481
val _ = OuterSyntax.command "nitpick_params"
blanchet@33192
   482
            "set and display the default parameters for Nitpick"
blanchet@33192
   483
            OuterKeyword.thy_decl scan_nitpick_params_command
blanchet@33192
   484
blanchet@33561
   485
(* Proof.state -> bool * Proof.state *)
blanchet@33561
   486
fun auto_nitpick state =
blanchet@34982
   487
  if not (!auto) then (false, state) else pick_nits [] true 1 0 state
blanchet@33561
   488
blanchet@33561
   489
val setup = Auto_Counterexample.register_tool ("nitpick", auto_nitpick)
blanchet@33561
   490
blanchet@33192
   491
end;