1.1 --- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Mon Feb 01 14:12:12 2010 +0100
1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Tue Feb 02 11:38:38 2010 +0100
1.3 @@ -1,6 +1,6 @@
1.4 (* Title: HOL/Tools/Nitpick/nitpick_isar.ML
1.5 Author: Jasmin Blanchette, TU Muenchen
1.6 - Copyright 2008, 2009
1.7 + Copyright 2008, 2009, 2010
1.8
1.9 Adds the "nitpick" and "nitpick_params" commands to Isabelle/Isar's outer
1.10 syntax.
1.11 @@ -28,9 +28,8 @@
1.12
1.13 val _ =
1.14 ProofGeneralPgip.add_preference Preferences.category_tracing
1.15 - (Preferences.bool_pref auto
1.16 - "auto-nitpick"
1.17 - "Whether to run Nitpick automatically.")
1.18 + (Preferences.bool_pref auto "auto-nitpick"
1.19 + "Whether to run Nitpick automatically.")
1.20
1.21 type raw_param = string * string list
1.22
1.23 @@ -41,6 +40,7 @@
1.24 ("bisim_depth", ["7"]),
1.25 ("box", ["smart"]),
1.26 ("mono", ["smart"]),
1.27 + ("std", ["true"]),
1.28 ("wf", ["smart"]),
1.29 ("sat_solver", ["smart"]),
1.30 ("batch_size", ["smart"]),
1.31 @@ -79,6 +79,7 @@
1.32 val negated_params =
1.33 [("dont_box", "box"),
1.34 ("non_mono", "mono"),
1.35 + ("non_std", "std"),
1.36 ("non_wf", "wf"),
1.37 ("non_blocking", "blocking"),
1.38 ("satisfy", "falsify"),
1.39 @@ -110,8 +111,8 @@
1.40 AList.defined (op =) negated_params s orelse
1.41 s = "max" orelse s = "eval" orelse s = "expect" orelse
1.42 exists (fn p => String.isPrefix (p ^ " ") s)
1.43 - ["card", "max", "iter", "box", "dont_box", "mono", "non_mono", "wf",
1.44 - "non_wf", "format"]
1.45 + ["card", "max", "iter", "box", "dont_box", "mono", "non_mono", "std",
1.46 + "non_std", "wf", "non_wf", "format"]
1.47
1.48 (* string * 'a -> unit *)
1.49 fun check_raw_param (s, _) =
1.50 @@ -244,6 +245,14 @@
1.51 value |> stringify_raw_param_value
1.52 |> int_seq_from_string name min_int))
1.53 (filter (String.isPrefix (prefix ^ " ") o fst) raw_params)
1.54 + (* (string -> 'a) -> string -> ('a option * bool) list *)
1.55 + fun lookup_bool_assigns read prefix =
1.56 + (NONE, lookup_bool prefix)
1.57 + :: map (fn (name, value) =>
1.58 + (SOME (read (String.extract (name, size prefix + 1, NONE))),
1.59 + value |> stringify_raw_param_value
1.60 + |> bool_option_from_string false name |> the))
1.61 + (filter (String.isPrefix (prefix ^ " ") o fst) raw_params)
1.62 (* (string -> 'a) -> string -> ('a option * bool option) list *)
1.63 fun lookup_bool_option_assigns read prefix =
1.64 (NONE, lookup_bool_option prefix)
1.65 @@ -297,6 +306,7 @@
1.66 NONE
1.67 | (NONE, _) => NONE) cards_assigns
1.68 val monos = lookup_bool_option_assigns read_type_polymorphic "mono"
1.69 + val stds = lookup_bool_assigns read_type_polymorphic "std"
1.70 val wfs = lookup_bool_option_assigns read_const_polymorphic "wf"
1.71 val sat_solver = lookup_string "sat_solver"
1.72 val blocking = not auto andalso lookup_bool "blocking"
1.73 @@ -339,9 +349,10 @@
1.74 in
1.75 {cards_assigns = cards_assigns, maxes_assigns = maxes_assigns,
1.76 iters_assigns = iters_assigns, bitss = bitss, bisim_depths = bisim_depths,
1.77 - boxes = boxes, monos = monos, wfs = wfs, sat_solver = sat_solver,
1.78 - blocking = blocking, falsify = falsify, debug = debug, verbose = verbose,
1.79 - overlord = overlord, user_axioms = user_axioms, assms = assms,
1.80 + boxes = boxes, monos = monos, stds = stds, wfs = wfs,
1.81 + sat_solver = sat_solver, blocking = blocking, falsify = falsify,
1.82 + debug = debug, verbose = verbose, overlord = overlord,
1.83 + user_axioms = user_axioms, assms = assms,
1.84 merge_type_vars = merge_type_vars, binary_ints = binary_ints,
1.85 destroy_constrs = destroy_constrs, specialize = specialize,
1.86 skolemize = skolemize, star_linear_preds = star_linear_preds,
1.87 @@ -416,8 +427,9 @@
1.88 | Refute.REFUTE (loc, details) =>
1.89 error ("Unhandled Refute error (" ^ quote loc ^ "): " ^ details ^ ".")
1.90
1.91 -(* raw_param list -> bool -> int -> Proof.state -> bool * Proof.state *)
1.92 -fun pick_nits override_params auto i state =
1.93 +
1.94 +(* raw_param list -> bool -> int -> int -> Proof.state -> bool * Proof.state *)
1.95 +fun pick_nits override_params auto i step state =
1.96 let
1.97 val thy = Proof.theory_of state
1.98 val ctxt = Proof.context_of state
1.99 @@ -431,7 +443,7 @@
1.100 |> (if auto then perhaps o try
1.101 else if debug then fn f => fn x => f x
1.102 else handle_exceptions ctxt)
1.103 - (fn (_, state) => pick_nits_in_subgoal state params auto i
1.104 + (fn (_, state) => pick_nits_in_subgoal state params auto i step
1.105 |>> curry (op =) "genuine")
1.106 in
1.107 if auto orelse blocking then go ()
1.108 @@ -441,9 +453,9 @@
1.109 (* raw_param list option * int option -> Toplevel.transition
1.110 -> Toplevel.transition *)
1.111 fun nitpick_trans (opt_params, opt_i) =
1.112 - Toplevel.keep (K ()
1.113 - o snd o pick_nits (these opt_params) false (the_default 1 opt_i)
1.114 - o Toplevel.proof_of)
1.115 + Toplevel.keep (fn st =>
1.116 + (pick_nits (these opt_params) false (the_default 1 opt_i)
1.117 + (Toplevel.proof_position_of st) (Toplevel.proof_of st); ()))
1.118
1.119 (* raw_param -> string *)
1.120 fun string_for_raw_param (name, value) =
1.121 @@ -477,7 +489,7 @@
1.122
1.123 (* Proof.state -> bool * Proof.state *)
1.124 fun auto_nitpick state =
1.125 - if not (!auto) then (false, state) else pick_nits [] true 1 state
1.126 + if not (!auto) then (false, state) else pick_nits [] true 1 0 state
1.127
1.128 val setup = Auto_Counterexample.register_tool ("nitpick", auto_nitpick)
1.129