--- a/src/HOL/Tools/Nitpick/nitpick.ML Fri May 27 10:30:08 2011 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Fri May 27 10:30:08 2011 +0200
@@ -9,6 +9,9 @@
sig
type styp = Nitpick_Util.styp
type term_postprocessor = Nitpick_Model.term_postprocessor
+
+ datatype mode = Auto_Try | Try | Normal
+
type params =
{cards_assigns: (typ option * int list) list,
maxes_assigns: (styp option * int list) list,
@@ -68,10 +71,10 @@
typ -> term_postprocessor -> theory -> theory
val unregister_term_postprocessor : typ -> theory -> theory
val pick_nits_in_term :
- Proof.state -> params -> bool -> int -> int -> int -> (term * term) list
+ Proof.state -> params -> mode -> int -> int -> int -> (term * term) list
-> term list -> term -> string * Proof.state
val pick_nits_in_subgoal :
- Proof.state -> params -> bool -> int -> int -> string * Proof.state
+ Proof.state -> params -> mode -> int -> int -> string * Proof.state
end;
structure Nitpick : NITPICK =
@@ -90,6 +93,8 @@
structure KK = Kodkod
+datatype mode = Auto_Try | Try | Normal
+
type params =
{cards_assigns: (typ option * int list) list,
maxes_assigns: (styp option * int list) list,
@@ -210,7 +215,7 @@
fun plazy f = Pretty.blk (0, pstrs (f ()))
-fun pick_them_nits_in_term deadline state (params : params) auto i n step
+fun pick_them_nits_in_term deadline state (params : params) mode i n step
subst assm_ts orig_t =
let
val timer = Timer.startRealTimer ()
@@ -232,32 +237,32 @@
max_genuine, check_potential, check_genuine, batch_size, ...} = params
val state_ref = Unsynchronized.ref state
val pprint =
- if auto then
+ if mode = Auto_Try then
Unsynchronized.change state_ref o Proof.goal_message o K
o Pretty.chunks o cons (Pretty.str "") o single
o Pretty.mark Markup.hilite
else
(fn s => (Output.urgent_message s; if debug then tracing s else ()))
o Pretty.string_of
- fun pprint_m f = () |> not auto ? pprint o f
+ fun pprint_n f = () |> mode = Normal ? pprint o f
fun pprint_v f = () |> verbose ? pprint o f
fun pprint_d f = () |> debug ? pprint o f
val print = pprint o curry Pretty.blk 0 o pstrs
(*
val print_g = pprint o Pretty.str
*)
- val print_m = pprint_m o K o plazy
+ val print_n = pprint_n o K o plazy
val print_v = pprint_v o K o plazy
fun check_deadline () =
if passed_deadline deadline then raise TimeLimit.TimeOut else ()
- val assm_ts = if assms orelse auto then assm_ts else []
+ val assm_ts = if assms orelse mode <> Normal then assm_ts else []
val _ =
if step = 0 then
- print_m (fn () => "Nitpicking formula...")
+ print_n (fn () => "Nitpicking formula...")
else
- pprint_m (fn () => Pretty.chunks (
+ pprint_n (fn () => Pretty.chunks (
pretties_for_formulas ctxt ("Nitpicking " ^
(if i <> 1 orelse n <> 1 then
"subgoal " ^ string_of_int i ^ " of " ^ string_of_int n
@@ -408,10 +413,10 @@
else
()
val _ =
- if not auto andalso
+ if mode = Normal andalso
exists (fn Type (@{type_name Datatype.node}, _) => true | _ => false)
all_Ts then
- print_m (K ("Warning: The problem involves directly or indirectly the \
+ print_n (K ("Warning: The problem involves directly or indirectly the \
\internal type " ^ quote @{type_name Datatype.node} ^
". This type is very Nitpick-unfriendly, and its presence \
\usually indicates either a failure of abstraction or a \
@@ -452,7 +457,7 @@
val likely_in_struct_induct_step =
exists is_struct_induct_step (Proof_Context.cases_of ctxt)
val _ = if standard andalso likely_in_struct_induct_step then
- pprint_m (fn () => Pretty.blk (0,
+ pprint_n (fn () => Pretty.blk (0,
pstrs "Hint: To check that the induction hypothesis is \
\general enough, try this command: " @
[Pretty.mark Markup.sendback (Pretty.blk (0,
@@ -472,7 +477,7 @@
if incremental andalso
not (member (op =) (Kodkod_SAT.configured_sat_solvers true)
sat_solver) then
- (print_m (K ("An incremental SAT solver is required: \"SAT4J\" will \
+ (print_n (K ("An incremental SAT solver is required: \"SAT4J\" will \
\be used instead of " ^ quote sat_solver ^ "."));
"SAT4J")
else
@@ -650,7 +655,7 @@
List.app (Unsynchronized.change checked_problems o Option.map o cons
o nth problems)
fun show_kodkod_warning "" = ()
- | show_kodkod_warning s = print_m (fn () => "Kodkod warning: " ^ s ^ ".")
+ | show_kodkod_warning s = print_n (fn () => "Kodkod warning: " ^ s ^ ".")
fun print_and_check_model genuine bounds
({free_names, sel_names, nonsel_names, rel_table, scope, ...}
@@ -670,7 +675,8 @@
in
(pprint (Pretty.chunks
[Pretty.blk (0,
- (pstrs ((if auto then "Auto " else "") ^ "Nitpick found a" ^
+ (pstrs ((if mode = Auto_Try then "Auto " else "") ^
+ "Nitpick found a" ^
(if not genuine then " potentially spurious "
else if genuine_means_genuine then " "
else " quasi genuine ") ^ das_wort_model) @
@@ -781,13 +787,13 @@
case KK.solve_any_problem debug overlord deadline max_threads
max_solutions (map fst problems) of
KK.JavaNotInstalled =>
- (print_m install_java_message;
+ (print_n install_java_message;
(found_really_genuine, max_potential, max_genuine, donno + 1))
| KK.JavaTooOld =>
- (print_m install_java_message;
+ (print_n install_java_message;
(found_really_genuine, max_potential, max_genuine, donno + 1))
| KK.KodkodiNotInstalled =>
- (print_m install_kodkodi_message;
+ (print_n install_kodkodi_message;
(found_really_genuine, max_potential, max_genuine, donno + 1))
| KK.Normal ([], unsat_js, s) =>
(update_checked_problems problems unsat_js; show_kodkod_warning s;
@@ -874,7 +880,7 @@
let
val _ =
if null scopes then
- print_m (K "The scope specification is inconsistent.")
+ print_n (K "The scope specification is inconsistent.")
else if verbose then
pprint (Pretty.chunks
[Pretty.blk (0,
@@ -922,7 +928,7 @@
if not (null sound_problems) andalso
forall (KK.is_problem_trivially_false o fst)
sound_problems then
- print_m (fn () =>
+ print_n (fn () =>
"Warning: The conjecture either trivially holds for the \
\given scopes or lies outside Nitpick's supported \
\fragment." ^
@@ -972,7 +978,7 @@
bitss bisim_depths mono_Ts nonmono_Ts deep_dataTs
finitizable_dataTs
val _ = if skipped > 0 then
- print_m (fn () => "Too many scopes. Skipping " ^
+ print_n (fn () => "Too many scopes. Skipping " ^
string_of_int skipped ^ " scope" ^
plural_s skipped ^
". (Consider using \"mono\" or \
@@ -984,10 +990,10 @@
fun run_batches _ _ []
(found_really_genuine, max_potential, max_genuine, donno) =
if donno > 0 andalso max_genuine > 0 then
- (print_m (fn () => excipit "checked"); unknownN)
+ (print_n (fn () => excipit "checked"); unknownN)
else if max_genuine = original_max_genuine then
if max_potential = original_max_potential then
- (print_m (fn () =>
+ (print_n (fn () =>
"Nitpick found no " ^ das_wort_model ^ "." ^
(if not standard andalso likely_in_struct_induct_step then
" This suggests that the induction hypothesis might be \
@@ -995,7 +1001,7 @@
else
"")); if skipped > 0 then unknownN else noneN)
else
- (print_m (fn () =>
+ (print_n (fn () =>
excipit ("could not find a" ^
(if max_genuine = 1 then
" better " ^ das_wort_model ^ "."
@@ -1017,7 +1023,7 @@
run_batches 0 (length batches) batches
(false, max_potential, max_genuine, 0)
handle TimeLimit.TimeOut =>
- (print_m (fn () => excipit "ran out of time after checking");
+ (print_n (fn () => excipit "ran out of time after checking");
if !met_potential > 0 then potentialN else unknownN)
val _ = print_v (fn () =>
"Total time: " ^ string_from_time (Timer.checkRealTimer timer) ^
@@ -1027,13 +1033,13 @@
(* Give the inner timeout a chance. *)
val timeout_bonus = seconds 1.0
-fun pick_nits_in_term state (params as {debug, timeout, expect, ...}) auto i n
+fun pick_nits_in_term state (params as {debug, timeout, expect, ...}) mode i n
step subst assm_ts orig_t =
- let val print_m = if auto then K () else Output.urgent_message in
+ let val print_n = if mode = Normal then Output.urgent_message else K () in
if getenv "KODKODI" = "" then
(* The "expect" argument is deliberately ignored if Kodkodi is missing so
that the "Nitpick_Examples" can be processed on any machine. *)
- (print_m (Pretty.string_of (plazy install_kodkodi_message));
+ (print_n (Pretty.string_of (plazy install_kodkodi_message));
("no_kodkodi", state))
else
let
@@ -1042,17 +1048,17 @@
val outcome as (outcome_code, _) =
time_limit (if debug orelse is_none timeout then NONE
else SOME (Time.+ (the timeout, timeout_bonus)))
- (pick_them_nits_in_term deadline state params auto i n step subst
+ (pick_them_nits_in_term deadline state params mode i n step subst
assm_ts) orig_t
handle TOO_LARGE (_, details) =>
- (print_m ("Limit reached: " ^ details ^ "."); unknown_outcome)
+ (print_n ("Limit reached: " ^ details ^ "."); unknown_outcome)
| TOO_SMALL (_, details) =>
- (print_m ("Limit reached: " ^ details ^ "."); unknown_outcome)
+ (print_n ("Limit reached: " ^ details ^ "."); unknown_outcome)
| Kodkod.SYNTAX (_, details) =>
- (print_m ("Malformed Kodkodi output: " ^ details ^ ".");
+ (print_n ("Malformed Kodkodi output: " ^ details ^ ".");
unknown_outcome)
| TimeLimit.TimeOut =>
- (print_m "Nitpick ran out of time."; unknown_outcome)
+ (print_n "Nitpick ran out of time."; unknown_outcome)
in
if expect = "" orelse outcome_code = expect then outcome
else error ("Unexpected outcome: " ^ quote outcome_code ^ ".")
@@ -1070,7 +1076,7 @@
|>> map Logic.dest_equals
in (subst, other_assms, subst_atomic subst t) end
-fun pick_nits_in_subgoal state params auto i step =
+fun pick_nits_in_subgoal state params mode i step =
let
val ctxt = Proof.context_of state
val t = state |> Proof.raw_goal |> #goal |> prop_of
@@ -1082,7 +1088,7 @@
val t = Logic.goal_params t i |> fst
val assms = map term_of (Assumption.all_assms_of ctxt)
val (subst, assms, t) = extract_fixed_frees ctxt (assms, t)
- in pick_nits_in_term state params auto i n step subst assms t end
+ in pick_nits_in_term state params mode i n step subst assms t end
end
end;
--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Fri May 27 10:30:08 2011 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Fri May 27 10:30:08 2011 +0200
@@ -33,12 +33,11 @@
(* Maximum number of scopes for Auto Nitpick. Be frugal since it has to share
its time slot with several other automatic tools. *)
-val max_auto_scopes = 6
+val auto_try_max_scopes = 6
val _ =
ProofGeneralPgip.add_preference Preferences.category_tracing
- (Preferences.bool_pref auto "auto-nitpick"
- "Run Nitpick automatically.")
+ (Preferences.bool_pref auto "auto-nitpick" "Run Nitpick automatically.")
type raw_param = string * string list
@@ -163,7 +162,7 @@
fun maxed_int_from_string min_int s = Int.max (min_int, the (Int.fromString s))
-fun extract_params ctxt auto default_params override_params =
+fun extract_params ctxt mode default_params override_params =
let
val override_params = maps normalize_raw_param override_params
val raw_params = rev override_params @ rev default_params
@@ -236,23 +235,24 @@
val lookup_term_list_option_polymorphic =
AList.lookup (op =) raw_params #> Option.map (map read_term_polymorphic)
val read_const_polymorphic = read_term_polymorphic #> dest_Const
- val cards_assigns = lookup_ints_assigns read_type_polymorphic "card" 1
- |> auto ? map (apsnd (take max_auto_scopes))
+ val cards_assigns =
+ lookup_ints_assigns read_type_polymorphic "card" 1
+ |> mode = Auto_Try ? map (apsnd (take auto_try_max_scopes))
val maxes_assigns = lookup_ints_assigns read_const_polymorphic "max" ~1
val iters_assigns = lookup_ints_assigns read_const_polymorphic "iter" 0
val bitss = lookup_int_seq "bits" 1
val bisim_depths = lookup_int_seq "bisim_depth" ~1
val boxes = lookup_bool_option_assigns read_type_polymorphic "box"
val finitizes = lookup_bool_option_assigns read_type_polymorphic "finitize"
- val monos = if auto then [(NONE, SOME true)]
+ val monos = if mode = Auto_Try then [(NONE, SOME true)]
else lookup_bool_option_assigns read_type_polymorphic "mono"
val stds = lookup_bool_assigns read_type_polymorphic "std"
val wfs = lookup_bool_option_assigns read_const_polymorphic "wf"
val sat_solver = lookup_string "sat_solver"
- val blocking = auto orelse lookup_bool "blocking"
+ val blocking = mode <> Normal orelse lookup_bool "blocking"
val falsify = lookup_bool "falsify"
- val debug = not auto andalso lookup_bool "debug"
- val verbose = debug orelse (not auto andalso lookup_bool "verbose")
+ val debug = (mode <> Auto_Try andalso lookup_bool "debug")
+ val verbose = debug orelse (mode <> Auto_Try andalso lookup_bool "verbose")
val overlord = lookup_bool "overlord"
val user_axioms = lookup_bool_option "user_axioms"
val assms = lookup_bool "assms"
@@ -267,9 +267,10 @@
val peephole_optim = lookup_bool "peephole_optim"
val datatype_sym_break = lookup_int "datatype_sym_break"
val kodkod_sym_break = lookup_int "kodkod_sym_break"
- val timeout = if auto then NONE else lookup_time "timeout"
+ val timeout = if mode = Auto_Try then NONE else lookup_time "timeout"
val tac_timeout = lookup_time "tac_timeout"
- val max_threads = if auto then 1 else Int.max (0, lookup_int "max_threads")
+ val max_threads =
+ if mode = Normal then Int.max (0, lookup_int "max_threads") else 1
val show_datatypes = debug orelse lookup_bool "show_datatypes"
val show_skolems = debug orelse lookup_bool "show_skolems"
val show_consts = debug orelse lookup_bool "show_consts"
@@ -277,7 +278,7 @@
val formats = lookup_ints_assigns read_term_polymorphic "format" 0
val atomss = lookup_strings_assigns read_type_polymorphic "atoms"
val max_potential =
- if auto then 0 else Int.max (0, lookup_int "max_potential")
+ if mode = Auto_Try then Int.max (0, lookup_int "max_potential") else 0
val max_genuine = Int.max (0, lookup_int "max_genuine")
val check_potential = lookup_bool "check_potential"
val check_genuine = lookup_bool "check_genuine"
@@ -308,7 +309,7 @@
end
fun default_params thy =
- extract_params (Proof_Context.init_global thy) false (default_raw_params thy)
+ extract_params (Proof_Context.init_global thy) Normal (default_raw_params thy)
o map (apsnd single)
val parse_key = Scan.repeat1 Parse.typ_group >> space_implode " "
@@ -353,25 +354,25 @@
| Refute.REFUTE (loc, details) =>
error ("Unhandled Refute error (" ^ quote loc ^ "): " ^ details ^ ".")
-fun pick_nits override_params auto i step state =
+fun pick_nits override_params mode i step state =
let
val thy = Proof.theory_of state
val ctxt = Proof.context_of state
val _ = List.app check_raw_param override_params
val params as {blocking, debug, ...} =
- extract_params ctxt auto (default_raw_params thy) override_params
+ extract_params ctxt mode (default_raw_params thy) override_params
fun go () =
(unknownN, state)
- |> (if auto then perhaps o try
+ |> (if mode = Auto_Try 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 i step)
+ (fn (_, state) => pick_nits_in_subgoal state params mode i step)
in if blocking then go () else Future.fork (tap go) |> K (unknownN, state) end
|> `(fn (outcome_code, _) => outcome_code = genuineN)
fun nitpick_trans (params, i) =
Toplevel.keep (fn state =>
- pick_nits params false i (Toplevel.proof_position_of state)
+ pick_nits params Normal i (Toplevel.proof_position_of state)
(Toplevel.proof_of state) |> K ())
fun string_for_raw_param (name, value) =
@@ -400,7 +401,7 @@
"set and display the default parameters for Nitpick"
Keyword.thy_decl parse_nitpick_params_command
-fun try_nitpick auto = pick_nits [] auto 1 0
+fun try_nitpick auto = pick_nits [] (if auto then Auto_Try else Try) 1 0
val setup = Try.register_tool (nitpickN, (auto, try_nitpick))
--- a/src/HOL/Tools/Nitpick/nitrox.ML Fri May 27 10:30:08 2011 +0200
+++ b/src/HOL/Tools/Nitpick/nitrox.ML Fri May 27 10:30:08 2011 +0200
@@ -15,6 +15,8 @@
open ATP_Problem
open ATP_Proof
+open Nitpick
+open Nitpick_Isar
exception SYNTAX of string
@@ -124,16 +126,15 @@
("format", "1000"),
("max_potential", "0"),
(* ("timeout", "240 s"), *)
- ("expect", Nitpick.genuineN)]
- |> Nitpick_Isar.default_params @{theory}
- val auto = false
+ ("expect", genuineN)]
+ |> default_params @{theory}
val i = 1
val n = 1
val step = 0
val subst = []
in
- Nitpick.pick_nits_in_term state params auto i n step subst ts
- @{prop False} |> fst
+ pick_nits_in_term state params Normal i n step subst ts @{prop False}
+ |> fst
end
end;