--- a/src/HOL/Tools/Nitpick/kodkod_sat.ML Sun Aug 14 12:26:09 2016 +0200
+++ b/src/HOL/Tools/Nitpick/kodkod_sat.ML Sun Aug 14 12:26:09 2016 +0200
@@ -117,10 +117,10 @@
error (if AList.defined (op =) static_list name then
"The SAT solver " ^ quote name ^ " is not configured. The \
\following solvers are configured:\n" ^
- enum_solvers dyns ^ "."
+ enum_solvers dyns
else
- "Unknown SAT solver " ^ quote name ^ ". The following \
- \solvers are supported:\n" ^ enum_solvers static_list ^ ".")
+ "Unknown SAT solver " ^ quote name ^ "\nThe following \
+ \solvers are supported:\n" ^ enum_solvers static_list)
end
end;
--- a/src/HOL/Tools/Nitpick/nitpick.ML Sun Aug 14 12:26:09 2016 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Sun Aug 14 12:26:09 2016 +0200
@@ -169,19 +169,18 @@
Pretty.indent indent_size (Pretty.chunks
(map2 (fn j => fn t =>
Pretty.block [t |> shorten_names_in_term
- |> Syntax.pretty_term ctxt,
- Pretty.str (if j = 1 then "." else ";")])
+ |> Syntax.pretty_term ctxt])
(length ts downto 1) ts))]
val isabelle_wrong_message =
- "Something appears to be wrong with your Isabelle installation."
+ "something appears to be wrong with your Isabelle installation"
val java_not_found_message =
- "Java could not be launched. " ^ isabelle_wrong_message
+ "Java could not be launched -- " ^ isabelle_wrong_message
val java_too_old_message =
- "The Java version is too old. " ^ isabelle_wrong_message
+ "The Java version is too old -- " ^ isabelle_wrong_message
val kodkodi_not_installed_message =
- "Nitpick requires the external Java program Kodkodi."
-val kodkodi_too_old_message = "The installed Kodkodi version is too old."
+ "Nitpick requires the external Java program Kodkodi"
+val kodkodi_too_old_message = "The installed Kodkodi version is too old"
val max_unsound_delay_ms = 200
val max_unsound_delay_percent = 2
@@ -269,7 +268,7 @@
else
"goal")) [Logic.list_implies (nondef_assm_ts, orig_t)]))
val _ = spying spy (fn () => (state, i, "starting " ^ @{make_string} mode ^ " mode"))
- val _ = print_v (enclose "Timestamp: " "." o Date.fmt "%H:%M:%S"
+ val _ = print_v (prefix "Timestamp: " o Date.fmt "%H:%M:%S"
o Date.fromTimeLocal o Time.now)
val neg_t = if falsify then Logic.mk_implies (orig_t, @{prop False})
else orig_t
@@ -317,7 +316,7 @@
val pseudo_frees = []
val real_frees = fold Term.add_frees conj_ts []
val _ = null (fold Term.add_tvars conj_ts []) orelse
- error "Nitpick cannot handle goals with schematic type variables."
+ error "Nitpick cannot handle goals with schematic type variables"
val (nondef_ts, def_ts, need_ts, got_all_mono_user_axioms,
no_poly_user_axioms, binarize) =
preprocess_formulas hol_ctxt nondef_assm_ts neg_t
@@ -329,11 +328,11 @@
Pretty.text ("The " ^ (if gfp then "co" else "") ^ "inductive predicate") @
[Pretty.brk 1, Pretty.quote (Syntax.pretty_term ctxt (Const x)), Pretty.brk 1] @
Pretty.text (if wf then
- "was proved well-founded. Nitpick can compute it \
- \efficiently."
+ "was proved well-founded; Nitpick can compute it \
+ \efficiently"
else
- "could not be proved well-founded. Nitpick might need to \
- \unroll it.")))
+ "could not be proved well-founded; Nitpick might need to \
+ \unroll it")))
val _ = if verbose then List.app print_wf (!wf_cache) else ()
val das_wort_formula = if falsify then "Negated conjecture" else "Formula"
val _ =
@@ -371,7 +370,7 @@
else
(if length pretties = 1 then "is" else "are") ^
" considered monotonic") ^
- ". " ^ extra))
+ "; " ^ extra))
end
fun is_type_fundamentally_monotonic T =
(is_data_type ctxt T andalso not (is_quot_type ctxt T) andalso
@@ -409,7 +408,7 @@
exists (member (op =) [nat_T, int_T]) all_Ts then
print_v (K "The option \"binary_ints\" will be ignored because of the \
\presence of rationals, reals, \"Suc\", \"gcd\", or \"lcm\" \
- \in the problem.")
+ \in the problem")
else
()
val (mono_Ts, nonmono_Ts) = List.partition is_type_monotonic all_Ts
@@ -419,7 +418,7 @@
[] => ()
| interesting_mono_Ts =>
pprint_v (K (monotonicity_message interesting_mono_Ts
- "Nitpick might be able to skip some scopes."))
+ "Nitpick might be able to skip some scopes"))
else
()
val (deep_dataTs, shallow_dataTs) =
@@ -433,7 +432,7 @@
val _ =
if verbose andalso not (null finitizable_dataTs) then
pprint_v (K (monotonicity_message finitizable_dataTs
- "Nitpick can use a more precise finite encoding."))
+ "Nitpick can use a more precise finite encoding"))
else
()
(*
@@ -450,7 +449,7 @@
not (member (op =) (Kodkod_SAT.configured_sat_solvers true)
sat_solver) then
(print_nt (K ("An incremental SAT solver is required: \"SAT4J\" will \
- \be used instead of " ^ quote sat_solver ^ "."));
+ \be used instead of " ^ quote sat_solver));
"SAT4J")
else
sat_solver
@@ -459,10 +458,10 @@
val _ =
if sat_solver = "smart" then
print_v (fn () =>
- "Using SAT solver " ^ quote actual_sat_solver ^ ". The following" ^
+ "Using SAT solver " ^ quote actual_sat_solver ^ "\nThe following" ^
(if incremental then " incremental " else " ") ^
"solvers are configured: " ^
- commas_quote (Kodkod_SAT.configured_sat_solvers incremental) ^ ".")
+ commas_quote (Kodkod_SAT.configured_sat_solvers incremental))
else
()
@@ -601,15 +600,15 @@
else
(Unsynchronized.change too_big_scopes (cons scope);
print_v (fn () =>
- "Limit reached: " ^ msg ^ ". Skipping " ^
+ "Limit reached: " ^ msg ^ "; skipping " ^
(if unsound then "potential component of " else "") ^
- "scope.");
+ "scope");
NONE)
| TOO_SMALL (_, msg) =>
(print_v (fn () =>
- "Limit reached: " ^ msg ^ ". Skipping " ^
+ "Limit reached: " ^ msg ^ "; skipping " ^
(if unsound then "potential component of " else "") ^
- "scope.");
+ "scope");
NONE)
val das_wort_model = if falsify then "counterexample" else "model"
@@ -624,7 +623,7 @@
List.app (Unsynchronized.change checked_problems o Option.map o cons
o nth problems)
fun show_kodkod_warning "" = ()
- | show_kodkod_warning s = print_nt (fn () => "Kodkod warning: " ^ s ^ ".")
+ | show_kodkod_warning s = print_nt (fn () => "Kodkod warning: " ^ s)
fun print_and_check_model genuine bounds
({free_names, sel_names, nonsel_names, rel_table, scope, ...}
@@ -692,12 +691,12 @@
print ("Try again with " ^
space_implode " " (serial_commas "and" ss) ^
" to confirm that the " ^ das_wort_model ^
- " is genuine.")
+ " is genuine")
end
else
print ("Nitpick is unable to guarantee the authenticity of \
\the " ^ das_wort_model ^ " in the presence of \
- \polymorphic axioms.")
+ \polymorphic axioms")
else
();
NONE)
@@ -811,7 +810,7 @@
(update_checked_problems problems unsat_js; raise Timeout.TIMEOUT Time.zeroTime)
| KK.Error (s, unsat_js) =>
(update_checked_problems problems unsat_js;
- print_v (K ("Kodkod error: " ^ s ^ "."));
+ print_v (K ("Kodkod error: " ^ s));
(found_really_genuine, max_potential, max_genuine, donno + 1))
end
@@ -820,7 +819,7 @@
let
val _ =
if null scopes then
- print_nt (K "The scope specification is inconsistent.")
+ print_nt (K "The scope specification is inconsistent")
else if verbose then
pprint_nt (fn () => Pretty.chunks
[Pretty.blk (0,
@@ -837,8 +836,7 @@
Pretty.block (
(case pretties_for_scope scope true of
[] => [Pretty.str "Empty"]
- | pretties => pretties) @
- [Pretty.str (if j = 1 then "." else ";")]))
+ | pretties => pretties)))
(length scopes downto 1) scopes))])
else
()
@@ -873,11 +871,11 @@
(if falsify then "either trivially holds"
else "is either trivially unsatisfiable") ^
" for the given scopes or lies outside Nitpick's supported \
- \fragment." ^
+ \fragment" ^
(if exists (not o KK.is_problem_trivially_false o fst)
unsound_problems then
- " Only potentially spurious " ^ das_wort_model ^
- "s may be found."
+ "; only potentially spurious " ^ das_wort_model ^
+ "s may be found"
else
""))
else
@@ -913,7 +911,7 @@
" " ^ string_of_int unsat ^ " of " ^ string_of_int total ^ " scope"
^ plural_s total
else
- "") ^ "."
+ "")
end
val (skipped, the_scopes) =
@@ -936,16 +934,16 @@
else if max_genuine = original_max_genuine then
if max_potential = original_max_potential then
(print_t (K "% SZS status GaveUp");
- print_nt (fn () => "Nitpick found no " ^ das_wort_model ^ ".");
+ print_nt (fn () => "Nitpick found no " ^ das_wort_model);
if skipped > 0 then unknownN else noneN)
else
(print_nt (fn () =>
excipit ("could not find a" ^
(if max_genuine = 1 then
- " better " ^ das_wort_model ^ "."
+ " better " ^ das_wort_model
else
- "ny better " ^ das_wort_model ^ "s.") ^
- " It checked"));
+ "ny better " ^ das_wort_model ^ "s") ^
+ "\nIt checked"));
potentialN)
else if found_really_genuine then
genuineN
@@ -964,8 +962,7 @@
(print_nt (fn () => excipit "ran out of time after checking");
if !met_potential > 0 then potentialN else unknownN)
val _ = print_v (fn () =>
- "Total time: " ^ string_of_time (Timer.checkRealTimer timer) ^
- ".")
+ "Total time: " ^ string_of_time (Timer.checkRealTimer timer))
val _ = spying spy (fn () => (state, i, "outcome: " ^ outcome_code))
in (outcome_code, Queue.content (Synchronized.value outcome)) end
@@ -993,20 +990,20 @@
def_assm_ts nondef_assm_ts) orig_t
handle TOO_LARGE (_, details) =>
(print_t "% SZS status GaveUp";
- print_nt ("Limit reached: " ^ details ^ "."); unknown_outcome)
+ print_nt ("Limit reached: " ^ details); unknown_outcome)
| TOO_SMALL (_, details) =>
(print_t "% SZS status GaveUp";
- print_nt ("Limit reached: " ^ details ^ "."); unknown_outcome)
+ print_nt ("Limit reached: " ^ details); unknown_outcome)
| Kodkod.SYNTAX (_, details) =>
(print_t "% SZS status GaveUp";
- print_nt ("Malformed Kodkodi output: " ^ details ^ ".");
+ print_nt ("Malformed Kodkodi output: " ^ details);
unknown_outcome)
| Timeout.TIMEOUT _ =>
(print_t "% SZS status TimedOut";
- print_nt "Nitpick ran out of time."; unknown_outcome)
+ print_nt "Nitpick ran out of time"; unknown_outcome)
in
if expect = "" orelse outcome_code = expect then outcome
- else error ("Unexpected outcome: " ^ quote outcome_code ^ ".")
+ else error ("Unexpected outcome: " ^ quote outcome_code)
end
end
--- a/src/HOL/Tools/Nitpick/nitpick_commands.ML Sun Aug 14 12:26:09 2016 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_commands.ML Sun Aug 14 12:26:09 2016 +0200
@@ -104,7 +104,7 @@
fun check_raw_param (s, _) =
if is_known_raw_param s then ()
- else error ("Unknown parameter: " ^ quote s ^ ".")
+ else error ("Unknown parameter: " ^ quote s)
fun unnegate_param_name name =
case AList.lookup (op =) negated_params name of
@@ -166,7 +166,7 @@
SOME s => (case Int.fromString s of
SOME i => i
| NONE => error ("Parameter " ^ quote name ^
- " must be assigned an integer value."))
+ " must be assigned an integer value"))
| NONE => 0
fun lookup_int name = do_int name (lookup name)
fun lookup_int_option name =
@@ -185,7 +185,7 @@
in if k1 <= k2 then k1 upto k2 else k1 downto k2 end
handle Option.Option =>
error ("Parameter " ^ quote name ^
- " must be assigned a sequence of integers.")
+ " must be assigned a sequence of integers")
fun int_seq_from_string name min_int s =
maps (int_range_from_string name min_int) (space_explode "," s)
fun lookup_int_seq name min_int =
@@ -305,22 +305,22 @@
fun handle_exceptions ctxt f x =
f x
handle ARG (loc, details) =>
- error ("Bad argument(s) to " ^ quote loc ^ ": " ^ details ^ ".")
+ error ("Bad argument(s) to " ^ quote loc ^ ": " ^ details)
| BAD (loc, details) =>
- error ("Internal error (" ^ quote loc ^ "): " ^ details ^ ".")
+ error ("Internal error (" ^ quote loc ^ "): " ^ details)
| NOT_SUPPORTED details =>
- (warning ("Unsupported case: " ^ details ^ "."); x)
+ (warning ("Unsupported case: " ^ details); x)
| NUT (loc, us) =>
error ("Invalid intermediate term" ^ plural_s_for_list us ^
" (" ^ quote loc ^ "): " ^
- commas (map (string_for_nut ctxt) us) ^ ".")
+ commas (map (string_for_nut ctxt) us))
| REP (loc, Rs) =>
error ("Invalid representation" ^ plural_s_for_list Rs ^
- " (" ^ quote loc ^ "): " ^ commas (map string_for_rep Rs) ^ ".")
+ " (" ^ quote loc ^ "): " ^ commas (map string_for_rep Rs))
| TERM (loc, ts) =>
error ("Invalid term" ^ plural_s_for_list ts ^
" (" ^ quote loc ^ "): " ^
- commas (map (Syntax.string_of_term ctxt) ts) ^ ".")
+ commas (map (Syntax.string_of_term ctxt) ts))
| TYPE (loc, Ts, ts) =>
error ("Invalid type" ^ plural_s_for_list Ts ^
(if null ts then
@@ -329,7 +329,7 @@
" for term" ^ plural_s_for_list ts ^ " " ^
commas (map (quote o Syntax.string_of_term ctxt) ts)) ^
" (" ^ quote loc ^ "): " ^
- commas (map (Syntax.string_of_typ ctxt) Ts) ^ ".")
+ commas (map (Syntax.string_of_typ ctxt) Ts))
fun pick_nits override_params mode i step state =
let
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Sun Aug 14 12:26:09 2016 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Sun Aug 14 12:26:09 2016 +0200
@@ -1908,7 +1908,7 @@
| Const (@{const_name Pure.eq}, Type (_, [T, _])) $ t1 $ t2 =>
@{const Trueprop} $ extensional_equal j T t1 t2
| _ => (warning ("Ignoring " ^ quote tag ^ " for non-equation " ^
- quote (Syntax.string_of_term ctxt t) ^ ".");
+ quote (Syntax.string_of_term ctxt t));
raise SAME ()))
|> SOME
end
@@ -2132,7 +2132,7 @@
map (wf_constraint_for_triple rel) triples
|> foldr1 s_conj |> HOLogic.mk_Trueprop
val _ = if debug then
- writeln ("Wellfoundedness goal: " ^ Syntax.string_of_term ctxt prop ^ ".")
+ writeln ("Wellfoundedness goal: " ^ Syntax.string_of_term ctxt prop)
else
()
in
--- a/src/HOL/Tools/Nitpick/nitpick_tests.ML Sun Aug 14 12:26:09 2016 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_tests.ML Sun Aug 14 12:26:09 2016 +0200
@@ -217,7 +217,7 @@
case Kodkod.solve_any_problem debug overlord timeout max_threads max_solutions
(map (problem_for_nut @{context}) tests) of
Kodkod.Normal ([], _, _) => ()
- | _ => error "Tests failed."
+ | _ => error "Tests failed"
end
end;