src/HOL/Tools/Nitpick/nitpick.ML
changeset 47560 e30323bfc93c
parent 47559 366838a5e235
child 47562 a72239723ae8
     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 ^ ".")