1.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML Wed Apr 18 22:40:25 2012 +0200
1.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Wed Apr 18 22:40:25 2012 +0200
1.3 @@ -10,7 +10,7 @@
1.4 type styp = Nitpick_Util.styp
1.5 type term_postprocessor = Nitpick_Model.term_postprocessor
1.6
1.7 - datatype mode = Auto_Try | Try | Normal
1.8 + datatype mode = Auto_Try | Try | Normal | TPTP
1.9
1.10 type params =
1.11 {cards_assigns: (typ option * int list) list,
1.12 @@ -93,7 +93,9 @@
1.13
1.14 structure KK = Kodkod
1.15
1.16 -datatype mode = Auto_Try | Try | Normal
1.17 +datatype mode = Auto_Try | Try | Normal | TPTP
1.18 +
1.19 +fun is_mode_nt mode = (mode = Normal orelse mode = TPTP)
1.20
1.21 type params =
1.22 {cards_assigns: (typ option * int list) list,
1.23 @@ -243,14 +245,15 @@
1.24 else
1.25 print o Pretty.string_of
1.26 val pprint_a = pprint Output.urgent_message
1.27 - fun pprint_n f = () |> mode = Normal ? pprint Output.urgent_message o f
1.28 + fun pprint_nt f = () |> is_mode_nt mode ? pprint Output.urgent_message o f
1.29 fun pprint_v f = () |> verbose ? pprint Output.urgent_message o f
1.30 fun pprint_d f = () |> debug ? pprint tracing o f
1.31 val print = pprint Output.urgent_message o curry Pretty.blk 0 o pstrs
1.32 + fun print_t f = () |> mode = TPTP ? print o f
1.33 (*
1.34 val print_g = pprint tracing o Pretty.str
1.35 *)
1.36 - val print_n = pprint_n o K o plazy
1.37 + val print_nt = pprint_nt o K o plazy
1.38 val print_v = pprint_v o K o plazy
1.39
1.40 fun check_deadline () =
1.41 @@ -259,9 +262,9 @@
1.42 val assm_ts = if assms orelse mode <> Normal then assm_ts else []
1.43 val _ =
1.44 if step = 0 then
1.45 - print_n (fn () => "Nitpicking formula...")
1.46 + print_nt (fn () => "Nitpicking formula...")
1.47 else
1.48 - pprint_n (fn () => Pretty.chunks (
1.49 + pprint_nt (fn () => Pretty.chunks (
1.50 pretties_for_formulas ctxt ("Nitpicking " ^
1.51 (if i <> 1 orelse n <> 1 then
1.52 "subgoal " ^ string_of_int i ^ " of " ^ string_of_int n
1.53 @@ -323,7 +326,7 @@
1.54 got_all_mono_user_axioms andalso no_poly_user_axioms
1.55
1.56 fun print_wf (x, (gfp, wf)) =
1.57 - pprint_n (fn () => Pretty.blk (0,
1.58 + pprint_nt (fn () => Pretty.blk (0,
1.59 pstrs ("The " ^ (if gfp then "co" else "") ^ "inductive predicate \"")
1.60 @ Syntax.pretty_term ctxt (Const x) ::
1.61 pstrs (if wf then
1.62 @@ -414,11 +417,11 @@
1.63 if mode = Normal andalso
1.64 exists (fn Type (@{type_name Datatype.node}, _) => true | _ => false)
1.65 all_Ts then
1.66 - print_n (K ("Warning: The problem involves directly or indirectly the \
1.67 - \internal type " ^ quote @{type_name Datatype.node} ^
1.68 - ". This type is very Nitpick-unfriendly, and its presence \
1.69 - \usually indicates either a failure of abstraction or a \
1.70 - \quirk in Nitpick."))
1.71 + print_nt (K ("Warning: The problem involves directly or indirectly the \
1.72 + \internal type " ^ quote @{type_name Datatype.node} ^
1.73 + ". This type is very Nitpick-unfriendly, and its presence \
1.74 + \usually indicates either a failure of abstraction or a \
1.75 + \quirk in Nitpick."))
1.76 else
1.77 ()
1.78 val (mono_Ts, nonmono_Ts) = List.partition is_type_monotonic all_Ts
1.79 @@ -455,7 +458,7 @@
1.80 val likely_in_struct_induct_step =
1.81 exists is_struct_induct_step (Proof_Context.cases_of ctxt)
1.82 val _ = if standard andalso likely_in_struct_induct_step then
1.83 - pprint_n (fn () => Pretty.blk (0,
1.84 + pprint_nt (fn () => Pretty.blk (0,
1.85 pstrs "Hint: To check that the induction hypothesis is \
1.86 \general enough, try this command: " @
1.87 [Pretty.mark Isabelle_Markup.sendback (Pretty.blk (0,
1.88 @@ -475,8 +478,8 @@
1.89 if incremental andalso
1.90 not (member (op =) (Kodkod_SAT.configured_sat_solvers true)
1.91 sat_solver) then
1.92 - (print_n (K ("An incremental SAT solver is required: \"SAT4J\" will \
1.93 - \be used instead of " ^ quote sat_solver ^ "."));
1.94 + (print_nt (K ("An incremental SAT solver is required: \"SAT4J\" will \
1.95 + \be used instead of " ^ quote sat_solver ^ "."));
1.96 "SAT4J")
1.97 else
1.98 sat_solver
1.99 @@ -653,7 +656,7 @@
1.100 List.app (Unsynchronized.change checked_problems o Option.map o cons
1.101 o nth problems)
1.102 fun show_kodkod_warning "" = ()
1.103 - | show_kodkod_warning s = print_n (fn () => "Kodkod warning: " ^ s ^ ".")
1.104 + | show_kodkod_warning s = print_nt (fn () => "Kodkod warning: " ^ s ^ ".")
1.105
1.106 fun print_and_check_model genuine bounds
1.107 ({free_names, sel_names, nonsel_names, rel_table, scope, ...}
1.108 @@ -671,7 +674,14 @@
1.109 codatatypes_ok
1.110 fun assms_prop () = Logic.mk_conjunction_list (neg_t :: assm_ts)
1.111 in
1.112 - (pprint_a (Pretty.chunks
1.113 + (print_t (fn () =>
1.114 + "% SZS status " ^
1.115 + (if genuine then
1.116 + if falsify then "CounterSatisfiable" else "Satisfiable"
1.117 + else
1.118 + "Unknown") ^ "\n" ^
1.119 + "% SZS output start FiniteModel\n");
1.120 + pprint_a (Pretty.chunks
1.121 [Pretty.blk (0,
1.122 (pstrs ((if mode = Auto_Try then "Auto " else "") ^
1.123 "Nitpick found a" ^
1.124 @@ -683,6 +693,7 @@
1.125 | pretties => pstrs " for " @ pretties) @
1.126 [Pretty.str ":\n"])),
1.127 Pretty.indent indent_size reconstructed_model]);
1.128 + print_t (fn () => "% SZS output stop\n");
1.129 if genuine then
1.130 (if check_genuine andalso standard then
1.131 case prove_hol_model scope tac_timeout free_names sel_names
1.132 @@ -785,13 +796,13 @@
1.133 case KK.solve_any_problem debug overlord deadline max_threads
1.134 max_solutions (map fst problems) of
1.135 KK.JavaNotInstalled =>
1.136 - (print_n install_java_message;
1.137 + (print_nt install_java_message;
1.138 (found_really_genuine, max_potential, max_genuine, donno + 1))
1.139 | KK.JavaTooOld =>
1.140 - (print_n install_java_message;
1.141 + (print_nt install_java_message;
1.142 (found_really_genuine, max_potential, max_genuine, donno + 1))
1.143 | KK.KodkodiNotInstalled =>
1.144 - (print_n install_kodkodi_message;
1.145 + (print_nt install_kodkodi_message;
1.146 (found_really_genuine, max_potential, max_genuine, donno + 1))
1.147 | KK.Normal ([], unsat_js, s) =>
1.148 (update_checked_problems problems unsat_js; show_kodkod_warning s;
1.149 @@ -878,9 +889,9 @@
1.150 let
1.151 val _ =
1.152 if null scopes then
1.153 - print_n (K "The scope specification is inconsistent.")
1.154 + print_nt (K "The scope specification is inconsistent.")
1.155 else if verbose then
1.156 - pprint_n (fn () => Pretty.chunks
1.157 + pprint_nt (fn () => Pretty.chunks
1.158 [Pretty.blk (0,
1.159 pstrs ((if n > 1 then
1.160 "Batch " ^ string_of_int (j + 1) ^ " of " ^
1.161 @@ -926,7 +937,7 @@
1.162 if not (null sound_problems) andalso
1.163 forall (KK.is_problem_trivially_false o fst)
1.164 sound_problems then
1.165 - print_n (fn () =>
1.166 + print_nt (fn () =>
1.167 "Warning: The conjecture " ^
1.168 (if falsify then "either trivially holds"
1.169 else "is either trivially unsatisfiable") ^
1.170 @@ -965,6 +976,7 @@
1.171 scope = n
1.172 ? Integer.add 1) (!generated_scopes) 0
1.173 in
1.174 + (if mode = TPTP then "% SZS status Unknown\n" else "") ^
1.175 "Nitpick " ^ did_so_and_so ^
1.176 (if is_some (!checked_problems) andalso total > 0 then
1.177 " " ^ string_of_int unsat ^ " of " ^ string_of_int total ^ " scope"
1.178 @@ -978,11 +990,11 @@
1.179 bitss bisim_depths mono_Ts nonmono_Ts deep_dataTs
1.180 finitizable_dataTs
1.181 val _ = if skipped > 0 then
1.182 - print_n (fn () => "Too many scopes. Skipping " ^
1.183 - string_of_int skipped ^ " scope" ^
1.184 - plural_s skipped ^
1.185 - ". (Consider using \"mono\" or \
1.186 - \\"merge_type_vars\" to prevent this.)")
1.187 + print_nt (fn () => "Too many scopes. Skipping " ^
1.188 + string_of_int skipped ^ " scope" ^
1.189 + plural_s skipped ^
1.190 + ". (Consider using \"mono\" or \
1.191 + \\"merge_type_vars\" to prevent this.)")
1.192 else
1.193 ()
1.194 val _ = scopes := the_scopes
1.195 @@ -990,10 +1002,11 @@
1.196 fun run_batches _ _ []
1.197 (found_really_genuine, max_potential, max_genuine, donno) =
1.198 if donno > 0 andalso max_genuine > 0 then
1.199 - (print_n (fn () => excipit "checked"); unknownN)
1.200 + (print_nt (fn () => excipit "checked"); unknownN)
1.201 else if max_genuine = original_max_genuine then
1.202 if max_potential = original_max_potential then
1.203 - (print_n (fn () =>
1.204 + (print_t (K "% SZS status Unknown\n");
1.205 + print_nt (fn () =>
1.206 "Nitpick found no " ^ das_wort_model ^ "." ^
1.207 (if not standard andalso likely_in_struct_induct_step then
1.208 " This suggests that the induction hypothesis might be \
1.209 @@ -1001,7 +1014,7 @@
1.210 else
1.211 "")); if skipped > 0 then unknownN else noneN)
1.212 else
1.213 - (print_n (fn () =>
1.214 + (print_nt (fn () =>
1.215 excipit ("could not find a" ^
1.216 (if max_genuine = 1 then
1.217 " better " ^ das_wort_model ^ "."
1.218 @@ -1023,7 +1036,7 @@
1.219 run_batches 0 (length batches) batches
1.220 (false, max_potential, max_genuine, 0)
1.221 handle TimeLimit.TimeOut =>
1.222 - (print_n (fn () => excipit "ran out of time after checking");
1.223 + (print_nt (fn () => excipit "ran out of time after checking");
1.224 if !met_potential > 0 then potentialN else unknownN)
1.225 val _ = print_v (fn () =>
1.226 "Total time: " ^ string_from_time (Timer.checkRealTimer timer) ^
1.227 @@ -1035,11 +1048,11 @@
1.228
1.229 fun pick_nits_in_term state (params as {debug, timeout, expect, ...}) mode i n
1.230 step subst assm_ts orig_t =
1.231 - let val print_n = if mode = Normal then Output.urgent_message else K () in
1.232 + let val print_nt = if is_mode_nt mode then Output.urgent_message else K () in
1.233 if getenv "KODKODI" = "" then
1.234 (* The "expect" argument is deliberately ignored if Kodkodi is missing so
1.235 that the "Nitpick_Examples" can be processed on any machine. *)
1.236 - (print_n (Pretty.string_of (plazy install_kodkodi_message));
1.237 + (print_nt (Pretty.string_of (plazy install_kodkodi_message));
1.238 ("no_kodkodi", state))
1.239 else
1.240 let
1.241 @@ -1051,14 +1064,14 @@
1.242 (pick_them_nits_in_term deadline state params mode i n step subst
1.243 assm_ts) orig_t
1.244 handle TOO_LARGE (_, details) =>
1.245 - (print_n ("Limit reached: " ^ details ^ "."); unknown_outcome)
1.246 + (print_nt ("Limit reached: " ^ details ^ "."); unknown_outcome)
1.247 | TOO_SMALL (_, details) =>
1.248 - (print_n ("Limit reached: " ^ details ^ "."); unknown_outcome)
1.249 + (print_nt ("Limit reached: " ^ details ^ "."); unknown_outcome)
1.250 | Kodkod.SYNTAX (_, details) =>
1.251 - (print_n ("Malformed Kodkodi output: " ^ details ^ ".");
1.252 + (print_nt ("Malformed Kodkodi output: " ^ details ^ ".");
1.253 unknown_outcome)
1.254 | TimeLimit.TimeOut =>
1.255 - (print_n "Nitpick ran out of time."; unknown_outcome)
1.256 + (print_nt "Nitpick ran out of time."; unknown_outcome)
1.257 in
1.258 if expect = "" orelse outcome_code = expect then outcome
1.259 else error ("Unexpected outcome: " ^ quote outcome_code ^ ".")