63 ("max_threads", "0"), |
63 ("max_threads", "0"), |
64 ("debug", "false"), |
64 ("debug", "false"), |
65 ("verbose", "false"), |
65 ("verbose", "false"), |
66 ("overlord", "false"), |
66 ("overlord", "false"), |
67 ("show_all", "false"), |
67 ("show_all", "false"), |
68 ("show_skolems", "true"), |
|
69 ("show_datatypes", "false"), |
68 ("show_datatypes", "false"), |
70 ("show_consts", "false"), |
69 ("show_consts", "false"), |
71 ("format", "1"), |
70 ("format", "1"), |
72 ("max_potential", "1"), |
71 ("max_potential", "1"), |
73 ("max_genuine", "1"), |
72 ("max_genuine", "1"), |
93 ("no_peephole_optim", "peephole_optim"), |
92 ("no_peephole_optim", "peephole_optim"), |
94 ("no_debug", "debug"), |
93 ("no_debug", "debug"), |
95 ("quiet", "verbose"), |
94 ("quiet", "verbose"), |
96 ("no_overlord", "overlord"), |
95 ("no_overlord", "overlord"), |
97 ("dont_show_all", "show_all"), |
96 ("dont_show_all", "show_all"), |
98 ("hide_skolems", "show_skolems"), |
|
99 ("hide_datatypes", "show_datatypes"), |
97 ("hide_datatypes", "show_datatypes"), |
100 ("hide_consts", "show_consts"), |
98 ("hide_consts", "show_consts"), |
101 ("trust_potential", "check_potential"), |
99 ("trust_potential", "check_potential"), |
102 ("trust_genuine", "check_genuine")] |
100 ("trust_genuine", "check_genuine")] |
103 |
101 |
253 val peephole_optim = lookup_bool "peephole_optim" |
251 val peephole_optim = lookup_bool "peephole_optim" |
254 val timeout = if auto then NONE else lookup_time "timeout" |
252 val timeout = if auto then NONE else lookup_time "timeout" |
255 val tac_timeout = lookup_time "tac_timeout" |
253 val tac_timeout = lookup_time "tac_timeout" |
256 val max_threads = Int.max (0, lookup_int "max_threads") |
254 val max_threads = Int.max (0, lookup_int "max_threads") |
257 val show_all = debug orelse lookup_bool "show_all" |
255 val show_all = debug orelse lookup_bool "show_all" |
258 val show_skolems = show_all orelse lookup_bool "show_skolems" |
|
259 val show_datatypes = show_all orelse lookup_bool "show_datatypes" |
256 val show_datatypes = show_all orelse lookup_bool "show_datatypes" |
260 val show_consts = show_all orelse lookup_bool "show_consts" |
257 val show_consts = show_all orelse lookup_bool "show_consts" |
261 val formats = lookup_ints_assigns read_term_polymorphic "format" 0 |
258 val formats = lookup_ints_assigns read_term_polymorphic "format" 0 |
262 val evals = lookup_term_list "eval" |
259 val evals = lookup_term_list "eval" |
263 val max_potential = |
260 val max_potential = |
264 if auto then 0 else Int.max (0, lookup_int "max_potential") |
261 if auto then 0 else Int.max (0, lookup_int "max_potential") |
265 val max_genuine = Int.max (0, lookup_int "max_genuine") |
262 val max_genuine = Int.max (0, lookup_int "max_genuine") |
266 val check_potential = lookup_bool "check_potential" |
263 val check_potential = lookup_bool "check_potential" |
267 val check_genuine = lookup_bool "check_genuine" |
264 val check_genuine = lookup_bool "check_genuine" |
268 val batch_size = case lookup_int_option "batch_size" of |
265 val batch_size = |
269 SOME n => Int.max (1, n) |
266 case lookup_int_option "batch_size" of |
270 | NONE => if debug then 1 else 64 |
267 SOME n => Int.max (1, n) |
|
268 | NONE => if debug then 1 else 64 |
271 val expect = lookup_string "expect" |
269 val expect = lookup_string "expect" |
272 in |
270 in |
273 {cards_assigns = cards_assigns, maxes_assigns = maxes_assigns, |
271 {cards_assigns = cards_assigns, maxes_assigns = maxes_assigns, |
274 iters_assigns = iters_assigns, bitss = bitss, bisim_depths = bisim_depths, |
272 iters_assigns = iters_assigns, bitss = bitss, bisim_depths = bisim_depths, |
275 boxes = boxes, finitizes = finitizes, monos = monos, stds = stds, |
273 boxes = boxes, finitizes = finitizes, monos = monos, stds = stds, |
279 merge_type_vars = merge_type_vars, binary_ints = binary_ints, |
277 merge_type_vars = merge_type_vars, binary_ints = binary_ints, |
280 destroy_constrs = destroy_constrs, specialize = specialize, |
278 destroy_constrs = destroy_constrs, specialize = specialize, |
281 star_linear_preds = star_linear_preds, fast_descrs = fast_descrs, |
279 star_linear_preds = star_linear_preds, fast_descrs = fast_descrs, |
282 peephole_optim = peephole_optim, timeout = timeout, |
280 peephole_optim = peephole_optim, timeout = timeout, |
283 tac_timeout = tac_timeout, max_threads = max_threads, |
281 tac_timeout = tac_timeout, max_threads = max_threads, |
284 show_skolems = show_skolems, show_datatypes = show_datatypes, |
282 show_datatypes = show_datatypes, show_consts = show_consts, |
285 show_consts = show_consts, formats = formats, evals = evals, |
283 formats = formats, evals = evals, max_potential = max_potential, |
286 max_potential = max_potential, max_genuine = max_genuine, |
284 max_genuine = max_genuine, check_potential = check_potential, |
287 check_potential = check_potential, check_genuine = check_genuine, |
285 check_genuine = check_genuine, batch_size = batch_size, expect = expect} |
288 batch_size = batch_size, expect = expect} |
|
289 end |
286 end |
290 |
287 |
291 fun default_params thy = |
288 fun default_params thy = |
292 extract_params (ProofContext.init thy) false (default_raw_params thy) |
289 extract_params (ProofContext.init thy) false (default_raw_params thy) |
293 o map (apsnd single) |
290 o map (apsnd single) |
380 val parse_nitpick_command = |
377 val parse_nitpick_command = |
381 (parse_params -- Scan.optional P.nat 1) #>> nitpick_trans |
378 (parse_params -- Scan.optional P.nat 1) #>> nitpick_trans |
382 val parse_nitpick_params_command = parse_params #>> nitpick_params_trans |
379 val parse_nitpick_params_command = parse_params #>> nitpick_params_trans |
383 |
380 |
384 val _ = OuterSyntax.improper_command "nitpick" |
381 val _ = OuterSyntax.improper_command "nitpick" |
385 "try to find a counterexample for a given subgoal using Kodkod" |
382 "try to find a counterexample for a given subgoal using Nitpick" |
386 K.diag parse_nitpick_command |
383 K.diag parse_nitpick_command |
387 val _ = OuterSyntax.command "nitpick_params" |
384 val _ = OuterSyntax.command "nitpick_params" |
388 "set and display the default parameters for Nitpick" |
385 "set and display the default parameters for Nitpick" |
389 K.thy_decl parse_nitpick_params_command |
386 K.thy_decl parse_nitpick_params_command |
390 |
387 |