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