wneuper/isa: comparison src/HOL/Tools/Nitpick/nitpick

equal deleted inserted replaced

-:b12ab081e5d1
+:ab01b72715ef
 signature NITPICK_ISAR =
 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 =
 struct
 open Nitpick_Util
 open Nitpick_HOL
 open Nitpick_Rep
 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 =
 [("card", ["1\<midarrow>8"]),
 ("box", ["smart"]),
 ("mono", ["smart"]),
 ("wf", ["smart"]),
 ("sat_solver", ["smart"]),
 ("batch_size", ["smart"]),
-("auto", ["false"]),
 ("blocking", ["true"]),
 ("falsify", ["true"]),
 ("user_axioms", ["smart"]),
 ("assms", ["true"]),
 ("merge_type_vars", ["false"]),
 ("star_linear_preds", ["true"]),
 ("uncurry", ["true"]),
 ("fast_descrs", ["true"]),
 ("peephole_optim", ["true"]),
 ("timeout", ["30 s"]),
-("auto_timeout", ["5 s"]),
 ("tac_timeout", ["500 ms"]),
 ("sym_break", ["20"]),
 ("sharing_depth", ["3"]),
 ("flatten_props", ["false"]),
 ("max_threads", ["0"]),
 val negated_params =
 [("dont_box", "box"),
 ("non_mono", "mono"),
 ("non_wf", "wf"),
-("no_auto", "auto"),
 ("non_blocking", "blocking"),
 ("satisfy", "falsify"),
 ("no_user_axioms", "user_axioms"),
 ("no_assms", "assms"),
 ("dont_merge_type_vars", "merge_type_vars"),
 | [] => ["false"]
 | _ => value)
 | NONE => (name, value)
 structure TheoryData = TheoryDataFun(
-type T = {params: raw_param list, registered_auto: bool}
+type T = {params: raw_param list}
-val empty = {params = rev default_default_params, registered_auto = false}
+val empty = {params = rev default_default_params}
 val copy = I
 val extend = I
-fun merge _ ({params = ps1, registered_auto = a1},
+fun merge _ ({params = ps1}, {params = ps2}) =
-{params = ps2, registered_auto = a2}) =
+{params = AList.merge (op =) (op =) (ps1, ps2)})
-{params = AList.merge (op =) (op =) (ps1, ps2),
-registered_auto = a1 orelse a2})
 (* 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,
+{params = AList.update (op =) (unnegate_raw_param param) params} thy
-registered_auto = registered_auto} 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>")
 (* string list -> string *)
 val skolemize = lookup_bool "skolemize"
 val star_linear_preds = lookup_bool "star_linear_preds"
 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"
+val timeout = if auto then NONE else lookup_time "timeout"
-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")
 val flatten_props = lookup_bool "flatten_props"
 val max_threads = Int.max (0, lookup_int "max_threads")
 val show_skolems = show_all orelse lookup_bool "show_skolems"
 val show_datatypes = show_all orelse lookup_bool "show_datatypes"
 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
+val max_potential =
-else Int.max (0, lookup_int "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"
 val batch_size = case lookup_int_option "batch_size" of
 SOME n => Int.max (1, n)
 | Kodkod.SYNTAX (_, details) =>
 (warning ("Ill-formed Kodkodi output: " ^ details ^ "."); x)
 | 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
+(false, state)
-else if debug then fn f => fn x => f x
+|> (if auto then perhaps o try
-else handle_exceptions ctxt)
+else if debug then fn f => fn x => f x
-(fn state => pick_nits_in_subgoal state params auto subgoal |> snd)
+else handle_exceptions ctxt)
-state
+(fn (_, state) => pick_nits_in_subgoal state params auto subgoal
+|>> equal "genuine")
 in
-if auto orelse blocking then
+if auto orelse blocking then go ()
-go ()
+else (SimpleThread.fork true (fn () => (go (); ())); (false, state))
-else
-(SimpleThread.fork true (fn () => (go (); ()));
-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 =>
+(fold set_default_raw_param (these opt_params)
-let val thy = fold set_default_raw_param (these opt_params) thy in
+#> 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
+params |> map string_for_raw_param
-|> cat_lines)));
+|> sort_strings |> cat_lines)))))
-register_auto thy
-end)
 (* OuterParse.token list
 -> (Toplevel.transition -> Toplevel.transition) * OuterParse.token list *)
-fun scan_nitpick_command tokens =
+val scan_nitpick_command =
-(scan_params -- Scan.option OuterParse.nat) tokens |>> nitpick_trans
+(scan_params -- Scan.option OuterParse.nat) #>> nitpick_trans
-fun scan_nitpick_params_command tokens =
+val scan_nitpick_params_command = scan_params #>> nitpick_params_trans
-scan_params tokens |>> nitpick_params_trans
 val _ = OuterSyntax.improper_command "nitpick"
 "try to find a counterexample for a given subgoal using Kodkod"
 OuterKeyword.diag scan_nitpick_command
 val _ = OuterSyntax.command "nitpick_params"
 "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;

changeset 33552	ab01b72715ef
parent 33547	cba22e2999d5
child 33557	1c62ac4ef6d1