diff -r 5e2d381b0695 -r b5e0909cd5ea src/HOL/Tools/Nitpick/nitpick_isar.ML --- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Tue Nov 10 13:17:50 2009 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Tue Nov 10 13:54:00 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,12 +43,11 @@ ("wf", ["smart"]), ("sat_solver", ["smart"]), ("batch_size", ["smart"]), - ("auto", ["false"]), ("blocking", ["true"]), ("falsify", ["true"]), ("user_axioms", ["smart"]), ("assms", ["true"]), - ("coalesce_type_vars", ["false"]), + ("merge_type_vars", ["false"]), ("destroy_constrs", ["true"]), ("specialize", ["true"]), ("skolemize", ["true"]), @@ -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,12 +78,11 @@ [("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_coalesce_type_vars", "coalesce_type_vars"), + ("dont_merge_type_vars", "merge_type_vars"), ("dont_destroy_constrs", "destroy_constrs"), ("dont_specialize", "specialize"), ("dont_skolemize", "skolemize"), @@ -125,30 +132,22 @@ | _ => value) | NONE => (name, value) -structure TheoryData = Theory_Data( - type T = {params: raw_param list, registered_auto: bool} - val empty = {params = rev default_default_params, registered_auto = false} +structure Data = Theory_Data( + 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}) : T = - {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 - TheoryData.put - {params = AList.update (op =) (unnegate_raw_param param) params, - registered_auto = registered_auto} thy + let val {params} = Data.get thy in + Data.put {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 +val default_raw_params = #params o Data.get (* string -> bool *) fun is_punctuation s = (s = "," orelse s = "-" orelse s = "\") @@ -304,7 +303,7 @@ val overlord = lookup_bool "overlord" val user_axioms = lookup_bool_option "user_axioms" val assms = lookup_bool "assms" - val coalesce_type_vars = lookup_bool "coalesce_type_vars" + val merge_type_vars = lookup_bool "merge_type_vars" val destroy_constrs = lookup_bool "destroy_constrs" val specialize = lookup_bool "specialize" val skolemize = lookup_bool "skolemize" @@ -312,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") @@ -325,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" @@ -340,7 +338,7 @@ monos = monos, wfs = wfs, sat_solver = sat_solver, blocking = blocking, falsify = falsify, debug = debug, verbose = verbose, overlord = overlord, user_axioms = user_axioms, assms = assms, - coalesce_type_vars = coalesce_type_vars, destroy_constrs = destroy_constrs, + merge_type_vars = merge_type_vars, destroy_constrs = destroy_constrs, specialize = specialize, skolemize = skolemize, star_linear_preds = star_linear_preds, uncurry = uncurry, fast_descrs = fast_descrs, peephole_optim = peephole_optim, @@ -411,7 +409,7 @@ | 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 @@ -420,70 +418,49 @@ 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" @@ -492,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;