handle non-auto try case gracefully in Nitpick
authorblanchet
Fri May 27 10:30:08 2011 +0200 (2011-05-27 ago)
changeset 430227d3ce43d9464
parent 43021 5910dd009d0e
child 43023 cb8d4c2af639
handle non-auto try case gracefully in Nitpick
src/HOL/Tools/Nitpick/nitpick.ML
src/HOL/Tools/Nitpick/nitpick_isar.ML
src/HOL/Tools/Nitpick/nitrox.ML
     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;