1.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML Fri May 27 10:30:08 2011 +0200
1.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Fri May 27 10:30:08 2011 +0200
1.3 @@ -9,6 +9,9 @@
1.4 sig
1.5 type styp = Nitpick_Util.styp
1.6 type term_postprocessor = Nitpick_Model.term_postprocessor
1.7 +
1.8 + datatype mode = Auto_Try | Try | Normal
1.9 +
1.10 type params =
1.11 {cards_assigns: (typ option * int list) list,
1.12 maxes_assigns: (styp option * int list) list,
1.13 @@ -68,10 +71,10 @@
1.14 typ -> term_postprocessor -> theory -> theory
1.15 val unregister_term_postprocessor : typ -> theory -> theory
1.16 val pick_nits_in_term :
1.17 - Proof.state -> params -> bool -> int -> int -> int -> (term * term) list
1.18 + Proof.state -> params -> mode -> int -> int -> int -> (term * term) list
1.19 -> term list -> term -> string * Proof.state
1.20 val pick_nits_in_subgoal :
1.21 - Proof.state -> params -> bool -> int -> int -> string * Proof.state
1.22 + Proof.state -> params -> mode -> int -> int -> string * Proof.state
1.23 end;
1.24
1.25 structure Nitpick : NITPICK =
1.26 @@ -90,6 +93,8 @@
1.27
1.28 structure KK = Kodkod
1.29
1.30 +datatype mode = Auto_Try | Try | Normal
1.31 +
1.32 type params =
1.33 {cards_assigns: (typ option * int list) list,
1.34 maxes_assigns: (styp option * int list) list,
1.35 @@ -210,7 +215,7 @@
1.36
1.37 fun plazy f = Pretty.blk (0, pstrs (f ()))
1.38
1.39 -fun pick_them_nits_in_term deadline state (params : params) auto i n step
1.40 +fun pick_them_nits_in_term deadline state (params : params) mode i n step
1.41 subst assm_ts orig_t =
1.42 let
1.43 val timer = Timer.startRealTimer ()
1.44 @@ -232,32 +237,32 @@
1.45 max_genuine, check_potential, check_genuine, batch_size, ...} = params
1.46 val state_ref = Unsynchronized.ref state
1.47 val pprint =
1.48 - if auto then
1.49 + if mode = Auto_Try then
1.50 Unsynchronized.change state_ref o Proof.goal_message o K
1.51 o Pretty.chunks o cons (Pretty.str "") o single
1.52 o Pretty.mark Markup.hilite
1.53 else
1.54 (fn s => (Output.urgent_message s; if debug then tracing s else ()))
1.55 o Pretty.string_of
1.56 - fun pprint_m f = () |> not auto ? pprint o f
1.57 + fun pprint_n f = () |> mode = Normal ? pprint o f
1.58 fun pprint_v f = () |> verbose ? pprint o f
1.59 fun pprint_d f = () |> debug ? pprint o f
1.60 val print = pprint o curry Pretty.blk 0 o pstrs
1.61 (*
1.62 val print_g = pprint o Pretty.str
1.63 *)
1.64 - val print_m = pprint_m o K o plazy
1.65 + val print_n = pprint_n o K o plazy
1.66 val print_v = pprint_v o K o plazy
1.67
1.68 fun check_deadline () =
1.69 if passed_deadline deadline then raise TimeLimit.TimeOut else ()
1.70
1.71 - val assm_ts = if assms orelse auto then assm_ts else []
1.72 + val assm_ts = if assms orelse mode <> Normal then assm_ts else []
1.73 val _ =
1.74 if step = 0 then
1.75 - print_m (fn () => "Nitpicking formula...")
1.76 + print_n (fn () => "Nitpicking formula...")
1.77 else
1.78 - pprint_m (fn () => Pretty.chunks (
1.79 + pprint_n (fn () => Pretty.chunks (
1.80 pretties_for_formulas ctxt ("Nitpicking " ^
1.81 (if i <> 1 orelse n <> 1 then
1.82 "subgoal " ^ string_of_int i ^ " of " ^ string_of_int n
1.83 @@ -408,10 +413,10 @@
1.84 else
1.85 ()
1.86 val _ =
1.87 - if not auto andalso
1.88 + if mode = Normal andalso
1.89 exists (fn Type (@{type_name Datatype.node}, _) => true | _ => false)
1.90 all_Ts then
1.91 - print_m (K ("Warning: The problem involves directly or indirectly the \
1.92 + print_n (K ("Warning: The problem involves directly or indirectly the \
1.93 \internal type " ^ quote @{type_name Datatype.node} ^
1.94 ". This type is very Nitpick-unfriendly, and its presence \
1.95 \usually indicates either a failure of abstraction or a \
1.96 @@ -452,7 +457,7 @@
1.97 val likely_in_struct_induct_step =
1.98 exists is_struct_induct_step (Proof_Context.cases_of ctxt)
1.99 val _ = if standard andalso likely_in_struct_induct_step then
1.100 - pprint_m (fn () => Pretty.blk (0,
1.101 + pprint_n (fn () => Pretty.blk (0,
1.102 pstrs "Hint: To check that the induction hypothesis is \
1.103 \general enough, try this command: " @
1.104 [Pretty.mark Markup.sendback (Pretty.blk (0,
1.105 @@ -472,7 +477,7 @@
1.106 if incremental andalso
1.107 not (member (op =) (Kodkod_SAT.configured_sat_solvers true)
1.108 sat_solver) then
1.109 - (print_m (K ("An incremental SAT solver is required: \"SAT4J\" will \
1.110 + (print_n (K ("An incremental SAT solver is required: \"SAT4J\" will \
1.111 \be used instead of " ^ quote sat_solver ^ "."));
1.112 "SAT4J")
1.113 else
1.114 @@ -650,7 +655,7 @@
1.115 List.app (Unsynchronized.change checked_problems o Option.map o cons
1.116 o nth problems)
1.117 fun show_kodkod_warning "" = ()
1.118 - | show_kodkod_warning s = print_m (fn () => "Kodkod warning: " ^ s ^ ".")
1.119 + | show_kodkod_warning s = print_n (fn () => "Kodkod warning: " ^ s ^ ".")
1.120
1.121 fun print_and_check_model genuine bounds
1.122 ({free_names, sel_names, nonsel_names, rel_table, scope, ...}
1.123 @@ -670,7 +675,8 @@
1.124 in
1.125 (pprint (Pretty.chunks
1.126 [Pretty.blk (0,
1.127 - (pstrs ((if auto then "Auto " else "") ^ "Nitpick found a" ^
1.128 + (pstrs ((if mode = Auto_Try then "Auto " else "") ^
1.129 + "Nitpick found a" ^
1.130 (if not genuine then " potentially spurious "
1.131 else if genuine_means_genuine then " "
1.132 else " quasi genuine ") ^ das_wort_model) @
1.133 @@ -781,13 +787,13 @@
1.134 case KK.solve_any_problem debug overlord deadline max_threads
1.135 max_solutions (map fst problems) of
1.136 KK.JavaNotInstalled =>
1.137 - (print_m install_java_message;
1.138 + (print_n install_java_message;
1.139 (found_really_genuine, max_potential, max_genuine, donno + 1))
1.140 | KK.JavaTooOld =>
1.141 - (print_m install_java_message;
1.142 + (print_n install_java_message;
1.143 (found_really_genuine, max_potential, max_genuine, donno + 1))
1.144 | KK.KodkodiNotInstalled =>
1.145 - (print_m install_kodkodi_message;
1.146 + (print_n install_kodkodi_message;
1.147 (found_really_genuine, max_potential, max_genuine, donno + 1))
1.148 | KK.Normal ([], unsat_js, s) =>
1.149 (update_checked_problems problems unsat_js; show_kodkod_warning s;
1.150 @@ -874,7 +880,7 @@
1.151 let
1.152 val _ =
1.153 if null scopes then
1.154 - print_m (K "The scope specification is inconsistent.")
1.155 + print_n (K "The scope specification is inconsistent.")
1.156 else if verbose then
1.157 pprint (Pretty.chunks
1.158 [Pretty.blk (0,
1.159 @@ -922,7 +928,7 @@
1.160 if not (null sound_problems) andalso
1.161 forall (KK.is_problem_trivially_false o fst)
1.162 sound_problems then
1.163 - print_m (fn () =>
1.164 + print_n (fn () =>
1.165 "Warning: The conjecture either trivially holds for the \
1.166 \given scopes or lies outside Nitpick's supported \
1.167 \fragment." ^
1.168 @@ -972,7 +978,7 @@
1.169 bitss bisim_depths mono_Ts nonmono_Ts deep_dataTs
1.170 finitizable_dataTs
1.171 val _ = if skipped > 0 then
1.172 - print_m (fn () => "Too many scopes. Skipping " ^
1.173 + print_n (fn () => "Too many scopes. Skipping " ^
1.174 string_of_int skipped ^ " scope" ^
1.175 plural_s skipped ^
1.176 ". (Consider using \"mono\" or \
1.177 @@ -984,10 +990,10 @@
1.178 fun run_batches _ _ []
1.179 (found_really_genuine, max_potential, max_genuine, donno) =
1.180 if donno > 0 andalso max_genuine > 0 then
1.181 - (print_m (fn () => excipit "checked"); unknownN)
1.182 + (print_n (fn () => excipit "checked"); unknownN)
1.183 else if max_genuine = original_max_genuine then
1.184 if max_potential = original_max_potential then
1.185 - (print_m (fn () =>
1.186 + (print_n (fn () =>
1.187 "Nitpick found no " ^ das_wort_model ^ "." ^
1.188 (if not standard andalso likely_in_struct_induct_step then
1.189 " This suggests that the induction hypothesis might be \
1.190 @@ -995,7 +1001,7 @@
1.191 else
1.192 "")); if skipped > 0 then unknownN else noneN)
1.193 else
1.194 - (print_m (fn () =>
1.195 + (print_n (fn () =>
1.196 excipit ("could not find a" ^
1.197 (if max_genuine = 1 then
1.198 " better " ^ das_wort_model ^ "."
1.199 @@ -1017,7 +1023,7 @@
1.200 run_batches 0 (length batches) batches
1.201 (false, max_potential, max_genuine, 0)
1.202 handle TimeLimit.TimeOut =>
1.203 - (print_m (fn () => excipit "ran out of time after checking");
1.204 + (print_n (fn () => excipit "ran out of time after checking");
1.205 if !met_potential > 0 then potentialN else unknownN)
1.206 val _ = print_v (fn () =>
1.207 "Total time: " ^ string_from_time (Timer.checkRealTimer timer) ^
1.208 @@ -1027,13 +1033,13 @@
1.209 (* Give the inner timeout a chance. *)
1.210 val timeout_bonus = seconds 1.0
1.211
1.212 -fun pick_nits_in_term state (params as {debug, timeout, expect, ...}) auto i n
1.213 +fun pick_nits_in_term state (params as {debug, timeout, expect, ...}) mode i n
1.214 step subst assm_ts orig_t =
1.215 - let val print_m = if auto then K () else Output.urgent_message in
1.216 + let val print_n = if mode = Normal then Output.urgent_message else K () in
1.217 if getenv "KODKODI" = "" then
1.218 (* The "expect" argument is deliberately ignored if Kodkodi is missing so
1.219 that the "Nitpick_Examples" can be processed on any machine. *)
1.220 - (print_m (Pretty.string_of (plazy install_kodkodi_message));
1.221 + (print_n (Pretty.string_of (plazy install_kodkodi_message));
1.222 ("no_kodkodi", state))
1.223 else
1.224 let
1.225 @@ -1042,17 +1048,17 @@
1.226 val outcome as (outcome_code, _) =
1.227 time_limit (if debug orelse is_none timeout then NONE
1.228 else SOME (Time.+ (the timeout, timeout_bonus)))
1.229 - (pick_them_nits_in_term deadline state params auto i n step subst
1.230 + (pick_them_nits_in_term deadline state params mode i n step subst
1.231 assm_ts) orig_t
1.232 handle TOO_LARGE (_, details) =>
1.233 - (print_m ("Limit reached: " ^ details ^ "."); unknown_outcome)
1.234 + (print_n ("Limit reached: " ^ details ^ "."); unknown_outcome)
1.235 | TOO_SMALL (_, details) =>
1.236 - (print_m ("Limit reached: " ^ details ^ "."); unknown_outcome)
1.237 + (print_n ("Limit reached: " ^ details ^ "."); unknown_outcome)
1.238 | Kodkod.SYNTAX (_, details) =>
1.239 - (print_m ("Malformed Kodkodi output: " ^ details ^ ".");
1.240 + (print_n ("Malformed Kodkodi output: " ^ details ^ ".");
1.241 unknown_outcome)
1.242 | TimeLimit.TimeOut =>
1.243 - (print_m "Nitpick ran out of time."; unknown_outcome)
1.244 + (print_n "Nitpick ran out of time."; unknown_outcome)
1.245 in
1.246 if expect = "" orelse outcome_code = expect then outcome
1.247 else error ("Unexpected outcome: " ^ quote outcome_code ^ ".")
1.248 @@ -1070,7 +1076,7 @@
1.249 |>> map Logic.dest_equals
1.250 in (subst, other_assms, subst_atomic subst t) end
1.251
1.252 -fun pick_nits_in_subgoal state params auto i step =
1.253 +fun pick_nits_in_subgoal state params mode i step =
1.254 let
1.255 val ctxt = Proof.context_of state
1.256 val t = state |> Proof.raw_goal |> #goal |> prop_of
1.257 @@ -1082,7 +1088,7 @@
1.258 val t = Logic.goal_params t i |> fst
1.259 val assms = map term_of (Assumption.all_assms_of ctxt)
1.260 val (subst, assms, t) = extract_fixed_frees ctxt (assms, t)
1.261 - in pick_nits_in_term state params auto i n step subst assms t end
1.262 + in pick_nits_in_term state params mode i n step subst assms t end
1.263 end
1.264
1.265 end;
2.1 --- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Fri May 27 10:30:08 2011 +0200
2.2 +++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Fri May 27 10:30:08 2011 +0200
2.3 @@ -33,12 +33,11 @@
2.4
2.5 (* Maximum number of scopes for Auto Nitpick. Be frugal since it has to share
2.6 its time slot with several other automatic tools. *)
2.7 -val max_auto_scopes = 6
2.8 +val auto_try_max_scopes = 6
2.9
2.10 val _ =
2.11 ProofGeneralPgip.add_preference Preferences.category_tracing
2.12 - (Preferences.bool_pref auto "auto-nitpick"
2.13 - "Run Nitpick automatically.")
2.14 + (Preferences.bool_pref auto "auto-nitpick" "Run Nitpick automatically.")
2.15
2.16 type raw_param = string * string list
2.17
2.18 @@ -163,7 +162,7 @@
2.19
2.20 fun maxed_int_from_string min_int s = Int.max (min_int, the (Int.fromString s))
2.21
2.22 -fun extract_params ctxt auto default_params override_params =
2.23 +fun extract_params ctxt mode default_params override_params =
2.24 let
2.25 val override_params = maps normalize_raw_param override_params
2.26 val raw_params = rev override_params @ rev default_params
2.27 @@ -236,23 +235,24 @@
2.28 val lookup_term_list_option_polymorphic =
2.29 AList.lookup (op =) raw_params #> Option.map (map read_term_polymorphic)
2.30 val read_const_polymorphic = read_term_polymorphic #> dest_Const
2.31 - val cards_assigns = lookup_ints_assigns read_type_polymorphic "card" 1
2.32 - |> auto ? map (apsnd (take max_auto_scopes))
2.33 + val cards_assigns =
2.34 + lookup_ints_assigns read_type_polymorphic "card" 1
2.35 + |> mode = Auto_Try ? map (apsnd (take auto_try_max_scopes))
2.36 val maxes_assigns = lookup_ints_assigns read_const_polymorphic "max" ~1
2.37 val iters_assigns = lookup_ints_assigns read_const_polymorphic "iter" 0
2.38 val bitss = lookup_int_seq "bits" 1
2.39 val bisim_depths = lookup_int_seq "bisim_depth" ~1
2.40 val boxes = lookup_bool_option_assigns read_type_polymorphic "box"
2.41 val finitizes = lookup_bool_option_assigns read_type_polymorphic "finitize"
2.42 - val monos = if auto then [(NONE, SOME true)]
2.43 + val monos = if mode = Auto_Try then [(NONE, SOME true)]
2.44 else lookup_bool_option_assigns read_type_polymorphic "mono"
2.45 val stds = lookup_bool_assigns read_type_polymorphic "std"
2.46 val wfs = lookup_bool_option_assigns read_const_polymorphic "wf"
2.47 val sat_solver = lookup_string "sat_solver"
2.48 - val blocking = auto orelse lookup_bool "blocking"
2.49 + val blocking = mode <> Normal orelse lookup_bool "blocking"
2.50 val falsify = lookup_bool "falsify"
2.51 - val debug = not auto andalso lookup_bool "debug"
2.52 - val verbose = debug orelse (not auto andalso lookup_bool "verbose")
2.53 + val debug = (mode <> Auto_Try andalso lookup_bool "debug")
2.54 + val verbose = debug orelse (mode <> Auto_Try andalso lookup_bool "verbose")
2.55 val overlord = lookup_bool "overlord"
2.56 val user_axioms = lookup_bool_option "user_axioms"
2.57 val assms = lookup_bool "assms"
2.58 @@ -267,9 +267,10 @@
2.59 val peephole_optim = lookup_bool "peephole_optim"
2.60 val datatype_sym_break = lookup_int "datatype_sym_break"
2.61 val kodkod_sym_break = lookup_int "kodkod_sym_break"
2.62 - val timeout = if auto then NONE else lookup_time "timeout"
2.63 + val timeout = if mode = Auto_Try then NONE else lookup_time "timeout"
2.64 val tac_timeout = lookup_time "tac_timeout"
2.65 - val max_threads = if auto then 1 else Int.max (0, lookup_int "max_threads")
2.66 + val max_threads =
2.67 + if mode = Normal then Int.max (0, lookup_int "max_threads") else 1
2.68 val show_datatypes = debug orelse lookup_bool "show_datatypes"
2.69 val show_skolems = debug orelse lookup_bool "show_skolems"
2.70 val show_consts = debug orelse lookup_bool "show_consts"
2.71 @@ -277,7 +278,7 @@
2.72 val formats = lookup_ints_assigns read_term_polymorphic "format" 0
2.73 val atomss = lookup_strings_assigns read_type_polymorphic "atoms"
2.74 val max_potential =
2.75 - if auto then 0 else Int.max (0, lookup_int "max_potential")
2.76 + if mode = Auto_Try then Int.max (0, lookup_int "max_potential") else 0
2.77 val max_genuine = Int.max (0, lookup_int "max_genuine")
2.78 val check_potential = lookup_bool "check_potential"
2.79 val check_genuine = lookup_bool "check_genuine"
2.80 @@ -308,7 +309,7 @@
2.81 end
2.82
2.83 fun default_params thy =
2.84 - extract_params (Proof_Context.init_global thy) false (default_raw_params thy)
2.85 + extract_params (Proof_Context.init_global thy) Normal (default_raw_params thy)
2.86 o map (apsnd single)
2.87
2.88 val parse_key = Scan.repeat1 Parse.typ_group >> space_implode " "
2.89 @@ -353,25 +354,25 @@
2.90 | Refute.REFUTE (loc, details) =>
2.91 error ("Unhandled Refute error (" ^ quote loc ^ "): " ^ details ^ ".")
2.92
2.93 -fun pick_nits override_params auto i step state =
2.94 +fun pick_nits override_params mode i step state =
2.95 let
2.96 val thy = Proof.theory_of state
2.97 val ctxt = Proof.context_of state
2.98 val _ = List.app check_raw_param override_params
2.99 val params as {blocking, debug, ...} =
2.100 - extract_params ctxt auto (default_raw_params thy) override_params
2.101 + extract_params ctxt mode (default_raw_params thy) override_params
2.102 fun go () =
2.103 (unknownN, state)
2.104 - |> (if auto then perhaps o try
2.105 + |> (if mode = Auto_Try then perhaps o try
2.106 else if debug then fn f => fn x => f x
2.107 else handle_exceptions ctxt)
2.108 - (fn (_, state) => pick_nits_in_subgoal state params auto i step)
2.109 + (fn (_, state) => pick_nits_in_subgoal state params mode i step)
2.110 in if blocking then go () else Future.fork (tap go) |> K (unknownN, state) end
2.111 |> `(fn (outcome_code, _) => outcome_code = genuineN)
2.112
2.113 fun nitpick_trans (params, i) =
2.114 Toplevel.keep (fn state =>
2.115 - pick_nits params false i (Toplevel.proof_position_of state)
2.116 + pick_nits params Normal i (Toplevel.proof_position_of state)
2.117 (Toplevel.proof_of state) |> K ())
2.118
2.119 fun string_for_raw_param (name, value) =
2.120 @@ -400,7 +401,7 @@
2.121 "set and display the default parameters for Nitpick"
2.122 Keyword.thy_decl parse_nitpick_params_command
2.123
2.124 -fun try_nitpick auto = pick_nits [] auto 1 0
2.125 +fun try_nitpick auto = pick_nits [] (if auto then Auto_Try else Try) 1 0
2.126
2.127 val setup = Try.register_tool (nitpickN, (auto, try_nitpick))
2.128
3.1 --- a/src/HOL/Tools/Nitpick/nitrox.ML Fri May 27 10:30:08 2011 +0200
3.2 +++ b/src/HOL/Tools/Nitpick/nitrox.ML Fri May 27 10:30:08 2011 +0200
3.3 @@ -15,6 +15,8 @@
3.4
3.5 open ATP_Problem
3.6 open ATP_Proof
3.7 +open Nitpick
3.8 +open Nitpick_Isar
3.9
3.10 exception SYNTAX of string
3.11
3.12 @@ -124,16 +126,15 @@
3.13 ("format", "1000"),
3.14 ("max_potential", "0"),
3.15 (* ("timeout", "240 s"), *)
3.16 - ("expect", Nitpick.genuineN)]
3.17 - |> Nitpick_Isar.default_params @{theory}
3.18 - val auto = false
3.19 + ("expect", genuineN)]
3.20 + |> default_params @{theory}
3.21 val i = 1
3.22 val n = 1
3.23 val step = 0
3.24 val subst = []
3.25 in
3.26 - Nitpick.pick_nits_in_term state params auto i n step subst ts
3.27 - @{prop False} |> fst
3.28 + pick_nits_in_term state params Normal i n step subst ts @{prop False}
3.29 + |> fst
3.30 end
3.31
3.32 end;