--- a/src/HOL/Tools/Nitpick/nitpick.ML Tue Mar 09 09:25:23 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Tue Mar 09 14:18:21 2010 +0100
@@ -326,8 +326,6 @@
val sound_finitizes =
none_true (filter_out (fn (SOME (Type (@{type_name fun}, _)), _) => true
| _ => false) finitizes)
- val genuine_means_genuine =
- got_all_user_axioms andalso none_true wfs andalso sound_finitizes
val standard = forall snd stds
(*
val _ = List.app (priority o string_for_nut ctxt) (nondef_us @ def_us)
@@ -603,7 +601,7 @@
fun show_kodkod_warning "" = ()
| show_kodkod_warning s = print_m (fn () => "Kodkod warning: " ^ s ^ ".")
- (* bool -> KK.raw_bound list -> problem_extension -> bool option *)
+ (* bool -> KK.raw_bound list -> problem_extension -> bool * bool option *)
fun print_and_check_model genuine bounds
({free_names, sel_names, nonsel_names, rel_table, scope, ...}
: problem_extension) =
@@ -614,119 +612,126 @@
show_consts = show_consts}
scope formats frees free_names sel_names nonsel_names rel_table
bounds
- val genuine_means_genuine = genuine_means_genuine andalso codatatypes_ok
+ val genuine_means_genuine =
+ got_all_user_axioms andalso none_true wfs andalso
+ sound_finitizes andalso codatatypes_ok
in
- pprint (Pretty.chunks
- [Pretty.blk (0,
- (pstrs ("Nitpick found a" ^
- (if not genuine then " potential "
- else if genuine_means_genuine then " "
- else " likely genuine ") ^ das_wort_model) @
- (case pretties_for_scope scope verbose of
- [] => []
- | pretties => pstrs " for " @ pretties) @
- [Pretty.str ":\n"])),
- Pretty.indent indent_size reconstructed_model]);
- if genuine then
- (if check_genuine andalso standard then
- (case prove_hol_model scope tac_timeout free_names sel_names
+ (pprint (Pretty.chunks
+ [Pretty.blk (0,
+ (pstrs ("Nitpick found a" ^
+ (if not genuine then " potential "
+ else if genuine_means_genuine then " "
+ else " quasi genuine ") ^ das_wort_model) @
+ (case pretties_for_scope scope verbose of
+ [] => []
+ | pretties => pstrs " for " @ pretties) @
+ [Pretty.str ":\n"])),
+ Pretty.indent indent_size reconstructed_model]);
+ if genuine then
+ (if check_genuine andalso standard then
+ case prove_hol_model scope tac_timeout free_names sel_names
rel_table bounds assms_t of
- SOME true => print ("Confirmation by \"auto\": The above " ^
- das_wort_model ^ " is really genuine.")
+ SOME true =>
+ print ("Confirmation by \"auto\": The above " ^
+ das_wort_model ^ " is really genuine.")
| SOME false =>
if genuine_means_genuine then
error ("A supposedly genuine " ^ das_wort_model ^ " was \
\shown to be spurious by \"auto\".\nThis should never \
\happen.\nPlease send a bug report to blanchet\
\te@in.tum.de.")
- else
- print ("Refutation by \"auto\": The above " ^ das_wort_model ^
- " is spurious.")
- | NONE => print "No confirmation by \"auto\".")
- else
- ();
- if not standard andalso likely_in_struct_induct_step then
- print "The existence of a nonstandard model suggests that the \
- \induction hypothesis is not general enough or perhaps even \
- \wrong. See the \"Inductive Properties\" section of the \
- \Nitpick manual for details (\"isabelle doc nitpick\")."
- else
- ();
- if has_syntactic_sorts orig_t then
- print "Hint: Maybe you forgot a type constraint?"
+ else
+ print ("Refutation by \"auto\": The above " ^
+ das_wort_model ^ " is spurious.")
+ | NONE => print "No confirmation by \"auto\"."
+ else
+ ();
+ if not standard andalso likely_in_struct_induct_step then
+ print "The existence of a nonstandard model suggests that the \
+ \induction hypothesis is not general enough or perhaps \
+ \even wrong. See the \"Inductive Properties\" section of \
+ \the Nitpick manual for details (\"isabelle doc nitpick\")."
+ else
+ ();
+ if has_syntactic_sorts orig_t then
+ print "Hint: Maybe you forgot a type constraint?"
+ else
+ ();
+ if not genuine_means_genuine then
+ if no_poly_user_axioms then
+ let
+ val options =
+ [] |> not got_all_mono_user_axioms
+ ? cons ("user_axioms", "\"true\"")
+ |> not (none_true wfs)
+ ? cons ("wf", "\"smart\" or \"false\"")
+ |> not sound_finitizes
+ ? cons ("finitize", "\"smart\" or \"false\"")
+ |> not codatatypes_ok
+ ? cons ("bisim_depth", "a nonnegative value")
+ val ss =
+ map (fn (name, value) => quote name ^ " set to " ^ value)
+ options
+ in
+ print ("Try again with " ^
+ space_implode " " (serial_commas "and" ss) ^
+ " to confirm that the " ^ das_wort_model ^
+ " is genuine.")
+ end
+ else
+ print ("Nitpick is unable to guarantee the authenticity of \
+ \the " ^ das_wort_model ^ " in the presence of \
+ \polymorphic axioms.")
+ else
+ ();
+ NONE)
+ else
+ if not genuine then
+ (Unsynchronized.inc met_potential;
+ if check_potential then
+ let
+ val status = prove_hol_model scope tac_timeout free_names
+ sel_names rel_table bounds assms_t
+ in
+ (case status of
+ SOME true => print ("Confirmation by \"auto\": The \
+ \above " ^ das_wort_model ^
+ " is genuine.")
+ | SOME false => print ("Refutation by \"auto\": The above " ^
+ das_wort_model ^ " is spurious.")
+ | NONE => print "No confirmation by \"auto\".");
+ status
+ end
+ else
+ NONE)
else
- ();
- if not genuine_means_genuine then
- if no_poly_user_axioms then
- let
- val options =
- [] |> not got_all_mono_user_axioms
- ? cons ("user_axioms", "\"true\"")
- |> not (none_true wfs)
- ? cons ("wf", "\"smart\" or \"false\"")
- |> not sound_finitizes
- ? cons ("finitize", "\"smart\" or \"false\"")
- |> not codatatypes_ok
- ? cons ("bisim_depth", "a nonnegative value")
- val ss =
- map (fn (name, value) => quote name ^ " set to " ^ value)
- options
- in
- print ("Try again with " ^
- space_implode " " (serial_commas "and" ss) ^
- " to confirm that the " ^ das_wort_model ^
- " is genuine.")
- end
- else
- print ("Nitpick is unable to guarantee the authenticity of \
- \the " ^ das_wort_model ^ " in the presence of \
- \polymorphic axioms.")
- else
- ();
- NONE)
- else
- if not genuine then
- (Unsynchronized.inc met_potential;
- if check_potential then
- let
- val status = prove_hol_model scope tac_timeout free_names
- sel_names rel_table bounds assms_t
- in
- (case status of
- SOME true => print ("Confirmation by \"auto\": The above " ^
- das_wort_model ^ " is genuine.")
- | SOME false => print ("Refutation by \"auto\": The above " ^
- das_wort_model ^ " is spurious.")
- | NONE => print "No confirmation by \"auto\".");
- status
- end
- else
- NONE)
- else
- NONE
+ NONE)
+ |> pair genuine_means_genuine
end
- (* int -> int -> int -> bool -> rich_problem list -> int * int * int *)
- fun solve_any_problem max_potential max_genuine donno first_time problems =
+ (* bool * int * int * int -> bool -> rich_problem list
+ -> bool * int * int * int *)
+ fun solve_any_problem (found_really_genuine, max_potential, max_genuine,
+ donno) first_time problems =
let
val max_potential = Int.max (0, max_potential)
val max_genuine = Int.max (0, max_genuine)
- (* bool -> int * KK.raw_bound list -> bool option *)
+ (* bool -> int * KK.raw_bound list -> bool * bool option *)
fun print_and_check genuine (j, bounds) =
print_and_check_model genuine bounds (snd (nth problems j))
val max_solutions = max_potential + max_genuine
|> not need_incremental ? curry Int.min 1
in
if max_solutions <= 0 then
- (0, 0, donno)
+ (found_really_genuine, 0, 0, donno)
else
case KK.solve_any_problem overlord deadline max_threads max_solutions
(map fst problems) of
KK.NotInstalled =>
(print_m install_kodkodi_message;
- (max_potential, max_genuine, donno + 1))
+ (found_really_genuine, max_potential, max_genuine, donno + 1))
| KK.Normal ([], unsat_js, s) =>
(update_checked_problems problems unsat_js; show_kodkod_warning s;
- (max_potential, max_genuine, donno))
+ (found_really_genuine, max_potential, max_genuine, donno))
| KK.Normal (sat_ps, unsat_js, s) =>
let
val (lib_ps, con_ps) =
@@ -736,16 +741,19 @@
show_kodkod_warning s;
if null con_ps then
let
- val num_genuine = take max_potential lib_ps
- |> map (print_and_check false)
- |> filter (curry (op =) (SOME true))
- |> length
+ val genuine_codes =
+ lib_ps |> take max_potential
+ |> map (print_and_check false)
+ |> filter (curry (op =) (SOME true) o snd)
+ val found_really_genuine =
+ found_really_genuine orelse exists fst genuine_codes
+ val num_genuine = length genuine_codes
val max_genuine = max_genuine - num_genuine
val max_potential = max_potential
- (length lib_ps - num_genuine)
in
if max_genuine <= 0 then
- (0, 0, donno)
+ (found_really_genuine, 0, 0, donno)
else
let
(* "co_js" is the list of sound problems whose unsound
@@ -765,18 +773,21 @@
|> max_potential <= 0
? filter_out (#unsound o snd)
in
- solve_any_problem max_potential max_genuine donno false
- problems
+ solve_any_problem (found_really_genuine, max_potential,
+ max_genuine, donno) false problems
end
end
else
let
- val _ = take max_genuine con_ps
- |> List.app (ignore o print_and_check true)
- val max_genuine = max_genuine - length con_ps
+ val genuine_codes =
+ con_ps |> take max_genuine
+ |> map (print_and_check true)
+ val max_genuine = max_genuine - length genuine_codes
+ val found_really_genuine =
+ found_really_genuine orelse exists fst genuine_codes
in
if max_genuine <= 0 orelse not first_time then
- (0, max_genuine, donno)
+ (found_really_genuine, 0, max_genuine, donno)
else
let
val bye_js = sort_distinct int_ord
@@ -784,7 +795,10 @@
val problems =
problems |> filter_out_indices bye_js
|> filter_out (#unsound o snd)
- in solve_any_problem 0 max_genuine donno false problems end
+ in
+ solve_any_problem (found_really_genuine, 0, max_genuine,
+ donno) false problems
+ end
end
end
| KK.TimedOut unsat_js =>
@@ -795,11 +809,13 @@
| KK.Error (s, unsat_js) =>
(update_checked_problems problems unsat_js;
print_v (K ("Kodkod error: " ^ s ^ "."));
- (max_potential, max_genuine, donno + 1))
+ (found_really_genuine, max_potential, max_genuine, donno + 1))
end
- (* int -> int -> scope list -> int * int * int -> int * int * int *)
- fun run_batch j n scopes (max_potential, max_genuine, donno) =
+ (* int -> int -> scope list -> bool * int * int * int
+ -> bool * int * int * int *)
+ fun run_batch j n scopes (found_really_genuine, max_potential, max_genuine,
+ donno) =
let
val _ =
if null scopes then
@@ -869,7 +885,8 @@
else
()
in
- solve_any_problem max_potential max_genuine donno true (rev problems)
+ solve_any_problem (found_really_genuine, max_potential, max_genuine,
+ donno) true (rev problems)
end
(* rich_problem list -> scope -> int *)
@@ -901,8 +918,9 @@
"") ^ "."
end
- (* int -> int -> scope list -> int * int * int -> KK.outcome *)
- fun run_batches _ _ [] (max_potential, max_genuine, donno) =
+ (* int -> int -> scope list -> bool * int * int * int -> KK.outcome *)
+ fun run_batches _ _ []
+ (found_really_genuine, max_potential, max_genuine, donno) =
if donno > 0 andalso max_genuine > 0 then
(print_m (fn () => excipit "ran out of some resource"); "unknown")
else if max_genuine = original_max_genuine then
@@ -919,10 +937,12 @@
"Nitpick could not find a" ^
(if max_genuine = 1 then " better " ^ das_wort_model ^ "."
else "ny better " ^ das_wort_model ^ "s.")); "potential")
+ else if found_really_genuine then
+ "genuine"
else
- if genuine_means_genuine then "genuine" else "likely_genuine"
+ "quasi_genuine"
| run_batches j n (batch :: batches) z =
- let val (z as (_, max_genuine, _)) = run_batch j n batch z in
+ let val (z as (_, _, max_genuine, _)) = run_batch j n batch z in
run_batches (j + 1) n (if max_genuine > 0 then batches else []) z
end
@@ -942,7 +962,8 @@
val batches = batch_list batch_size (!scopes)
val outcome_code =
- (run_batches 0 (length batches) batches (max_potential, max_genuine, 0)
+ (run_batches 0 (length batches) batches
+ (false, max_potential, max_genuine, 0)
handle Exn.Interrupt => do_interrupted ())
handle TimeLimit.TimeOut =>
(print_m (fn () => excipit "ran out of time");