--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Wed Oct 28 11:55:48 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Wed Oct 28 17:43:43 2009 +0100
@@ -10,7 +10,9 @@
sig
type params = Nitpick.params
+ val auto: bool Unsynchronized.ref
val default_params : theory -> (string * string) list -> params
+ val setup : theory -> theory
end
structure Nitpick_Isar : NITPICK_ISAR =
@@ -22,6 +24,14 @@
open Nitpick_Nut
open Nitpick
+val auto = Unsynchronized.ref false;
+
+val _ = ProofGeneralPgip.add_preference Preferences.category_tracing
+ (setmp_CRITICAL auto false
+ (fn () => Preferences.bool_pref auto
+ "auto-nitpick"
+ "Whether to run Nitpick automatically.") ())
+
type raw_param = string * string list
val default_default_params =
@@ -33,7 +43,6 @@
("wf", ["smart"]),
("sat_solver", ["smart"]),
("batch_size", ["smart"]),
- ("auto", ["false"]),
("blocking", ["true"]),
("falsify", ["true"]),
("user_axioms", ["smart"]),
@@ -47,7 +56,6 @@
("fast_descrs", ["true"]),
("peephole_optim", ["true"]),
("timeout", ["30 s"]),
- ("auto_timeout", ["5 s"]),
("tac_timeout", ["500 ms"]),
("sym_break", ["20"]),
("sharing_depth", ["3"]),
@@ -70,7 +78,6 @@
[("dont_box", "box"),
("non_mono", "mono"),
("non_wf", "wf"),
- ("no_auto", "auto"),
("non_blocking", "blocking"),
("satisfy", "falsify"),
("no_user_axioms", "user_axioms"),
@@ -126,31 +133,22 @@
| NONE => (name, value)
structure TheoryData = TheoryDataFun(
- type T = {params: raw_param list, registered_auto: bool}
- val empty = {params = rev default_default_params, registered_auto = false}
+ type T = {params: raw_param list}
+ val empty = {params = rev default_default_params}
val copy = I
val extend = I
- fun merge _ ({params = ps1, registered_auto = a1},
- {params = ps2, registered_auto = a2}) =
- {params = AList.merge (op =) (op =) (ps1, ps2),
- registered_auto = a1 orelse a2})
+ fun merge _ ({params = ps1}, {params = ps2}) =
+ {params = AList.merge (op =) (op =) (ps1, ps2)})
(* raw_param -> theory -> theory *)
fun set_default_raw_param param thy =
- let val {params, registered_auto} = TheoryData.get thy in
+ let val {params} = TheoryData.get thy in
TheoryData.put
- {params = AList.update (op =) (unnegate_raw_param param) params,
- registered_auto = registered_auto} thy
+ {params = AList.update (op =) (unnegate_raw_param param) params} thy
end
(* theory -> raw_param list *)
val default_raw_params = #params o TheoryData.get
-(* theory -> theory *)
-fun set_registered_auto thy =
- TheoryData.put {params = default_raw_params thy, registered_auto = true} thy
-(* theory -> bool *)
-val is_registered_auto = #registered_auto o TheoryData.get
-
(* string -> bool *)
fun is_punctuation s = (s = "," orelse s = "-" orelse s = "\<midarrow>")
@@ -313,8 +311,7 @@
val uncurry = lookup_bool "uncurry"
val fast_descrs = lookup_bool "fast_descrs"
val peephole_optim = lookup_bool "peephole_optim"
- val timeout = if auto then lookup_time "auto_timeout"
- else lookup_time "timeout"
+ val timeout = if auto then NONE else lookup_time "timeout"
val tac_timeout = lookup_time "tac_timeout"
val sym_break = Int.max (0, lookup_int "sym_break")
val sharing_depth = Int.max (1, lookup_int "sharing_depth")
@@ -326,8 +323,8 @@
val show_consts = show_all orelse lookup_bool "show_consts"
val formats = lookup_ints_assigns read_term_polymorphic "format" 0
val evals = lookup_term_list "eval"
- val max_potential = if auto then 0
- else Int.max (0, lookup_int "max_potential")
+ val max_potential =
+ if auto then 0 else Int.max (0, lookup_int "max_potential")
val max_genuine = Int.max (0, lookup_int "max_genuine")
val check_potential = lookup_bool "check_potential"
val check_genuine = lookup_bool "check_genuine"
@@ -412,79 +409,58 @@
| Refute.REFUTE (loc, details) =>
error ("Unhandled Refute error (" ^ quote loc ^ "): " ^ details ^ ".")
-(* raw_param list -> bool -> int -> Proof.state -> Proof.state *)
+(* raw_param list -> bool -> int -> Proof.state -> bool * Proof.state *)
fun pick_nits override_params auto subgoal state =
let
val thy = Proof.theory_of state
val ctxt = Proof.context_of state
- val thm = snd (snd (Proof.get_goal state))
+ val thm = state |> Proof.get_goal |> snd |> snd
val _ = List.app check_raw_param override_params
val params as {blocking, debug, ...} =
extract_params ctxt auto (default_raw_params thy) override_params
- (* unit -> Proof.state *)
+ (* unit -> bool * Proof.state *)
fun go () =
- (if auto then perhaps o try
- else if debug then fn f => fn x => f x
- else handle_exceptions ctxt)
- (fn state => pick_nits_in_subgoal state params auto subgoal |> snd)
- state
+ (false, state)
+ |> (if auto then perhaps o try
+ else if debug then fn f => fn x => f x
+ else handle_exceptions ctxt)
+ (fn (_, state) => pick_nits_in_subgoal state params auto subgoal
+ |>> equal "genuine")
in
- if auto orelse blocking then
- go ()
- else
- (SimpleThread.fork true (fn () => (go (); ()));
- state)
+ if auto orelse blocking then go ()
+ else (SimpleThread.fork true (fn () => (go (); ())); (false, state))
end
(* (TableFun().key * string list) list option * int option
-> Toplevel.transition -> Toplevel.transition *)
fun nitpick_trans (opt_params, opt_subgoal) =
Toplevel.keep (K ()
- o pick_nits (these opt_params) false (the_default 1 opt_subgoal)
+ o snd o pick_nits (these opt_params) false (the_default 1 opt_subgoal)
o Toplevel.proof_of)
(* raw_param -> string *)
fun string_for_raw_param (name, value) =
name ^ " = " ^ stringify_raw_param_value value
-(* bool -> Proof.state -> Proof.state *)
-fun pick_nits_auto interactive state =
- let val thy = Proof.theory_of state in
- ((interactive andalso not (!Toplevel.quiet)
- andalso the (general_lookup_bool false (default_raw_params thy)
- (SOME false) "auto"))
- ? pick_nits [] true 0) state
- end
-
-(* theory -> theory *)
-fun register_auto thy =
- (not (is_registered_auto thy)
- ? (set_registered_auto
- #> Context.theory_map (Specification.add_theorem_hook pick_nits_auto)))
- thy
-
(* (TableFun().key * string) list option -> Toplevel.transition
-> Toplevel.transition *)
fun nitpick_params_trans opt_params =
Toplevel.theory
- (fn thy =>
- let val thy = fold set_default_raw_param (these opt_params) thy in
- writeln ("Default parameters for Nitpick:\n" ^
- (case rev (default_raw_params thy) of
- [] => "none"
- | params =>
- (map check_raw_param params;
- params |> map string_for_raw_param |> sort_strings
- |> cat_lines)));
- register_auto thy
- end)
+ (fold set_default_raw_param (these opt_params)
+ #> tap (fn thy =>
+ writeln ("Default parameters for Nitpick:\n" ^
+ (case rev (default_raw_params thy) of
+ [] => "none"
+ | params =>
+ (map check_raw_param params;
+ params |> map string_for_raw_param
+ |> sort_strings |> cat_lines)))))
(* OuterParse.token list
-> (Toplevel.transition -> Toplevel.transition) * OuterParse.token list *)
-fun scan_nitpick_command tokens =
- (scan_params -- Scan.option OuterParse.nat) tokens |>> nitpick_trans
-fun scan_nitpick_params_command tokens =
- scan_params tokens |>> nitpick_params_trans
+val scan_nitpick_command =
+ (scan_params -- Scan.option OuterParse.nat) #>> nitpick_trans
+val scan_nitpick_params_command = scan_params #>> nitpick_params_trans
val _ = OuterSyntax.improper_command "nitpick"
"try to find a counterexample for a given subgoal using Kodkod"
@@ -493,4 +469,10 @@
"set and display the default parameters for Nitpick"
OuterKeyword.thy_decl scan_nitpick_params_command
+(* Proof.state -> bool * Proof.state *)
+fun auto_nitpick state =
+ if not (!auto) then (false, state) else pick_nits [] true 1 state
+
+val setup = Auto_Counterexample.register_tool ("nitpick", auto_nitpick)
+
end;