change defaults of Auto Nitpick so that it consumes less resources (time and Kodkod threads)
authorblanchet
Sat Sep 11 10:20:25 2010 +0200 (2010-09-11)
changeset 39316b6c4385ab400
parent 39315 27f7b7748425
child 39317 6ec8d4683699
change defaults of Auto Nitpick so that it consumes less resources (time and Kodkod threads)
src/HOL/Tools/Nitpick/nitpick.ML
src/HOL/Tools/Nitpick/nitpick_isar.ML
src/HOL/Tools/Nitpick/nitpick_kodkod.ML
src/HOL/Tools/Nitpick/nitpick_mono.ML
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Sat Sep 11 10:13:51 2010 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Sat Sep 11 10:20:25 2010 +0200
     1.3 @@ -144,7 +144,7 @@
     1.4     rel_table: nut NameTable.table,
     1.5     unsound: bool,
     1.6     scope: scope}
     1.7 - 
     1.8 +
     1.9  type rich_problem = KK.problem * problem_extension
    1.10  
    1.11  fun pretties_for_formulas _ _ [] = []
     2.1 --- a/src/HOL/Tools/Nitpick/nitpick_isar.ML	Sat Sep 11 10:13:51 2010 +0200
     2.2 +++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML	Sat Sep 11 10:20:25 2010 +0200
     2.3 @@ -10,7 +10,7 @@
     2.4  sig
     2.5    type params = Nitpick.params
     2.6  
     2.7 -  val auto: bool Unsynchronized.ref
     2.8 +  val auto : bool Unsynchronized.ref
     2.9    val default_params : theory -> (string * string) list -> params
    2.10    val setup : theory -> theory
    2.11  end;
    2.12 @@ -24,7 +24,7 @@
    2.13  open Nitpick_Nut
    2.14  open Nitpick
    2.15  
    2.16 -val auto = Unsynchronized.ref false;
    2.17 +val auto = Unsynchronized.ref false
    2.18  
    2.19  val _ =
    2.20    ProofGeneralPgip.add_preference Preferences.category_tracing
    2.21 @@ -109,7 +109,7 @@
    2.22  
    2.23  fun check_raw_param (s, _) =
    2.24    if is_known_raw_param s then ()
    2.25 -  else error ("Unknown parameter: " ^ quote s ^ ".")  
    2.26 +  else error ("Unknown parameter: " ^ quote s ^ ".")
    2.27  
    2.28  fun unnegate_param_name name =
    2.29    case AList.lookup (op =) negated_params name of
    2.30 @@ -212,8 +212,8 @@
    2.31        lookup_assigns read prefix "" (space_explode " ")
    2.32      fun lookup_time name =
    2.33        case lookup name of
    2.34 -        NONE => NONE
    2.35 -      | SOME s => parse_time_option name s
    2.36 +        SOME s => parse_time_option name s
    2.37 +      | NONE => NONE
    2.38      val read_type_polymorphic =
    2.39        Syntax.read_typ ctxt #> Logic.mk_type
    2.40        #> singleton (Variable.polymorphic ctxt) #> Logic.dest_type
    2.41 @@ -229,11 +229,12 @@
    2.42      val bisim_depths = lookup_int_seq "bisim_depth" ~1
    2.43      val boxes = lookup_bool_option_assigns read_type_polymorphic "box"
    2.44      val finitizes = lookup_bool_option_assigns read_type_polymorphic "finitize"
    2.45 -    val monos = lookup_bool_option_assigns read_type_polymorphic "mono"
    2.46 +    val monos = if auto then [(NONE, SOME true)]
    2.47 +                else lookup_bool_option_assigns read_type_polymorphic "mono"
    2.48      val stds = lookup_bool_assigns read_type_polymorphic "std"
    2.49      val wfs = lookup_bool_option_assigns read_const_polymorphic "wf"
    2.50      val sat_solver = lookup_string "sat_solver"
    2.51 -    val blocking = not auto andalso lookup_bool "blocking"
    2.52 +    val blocking = auto orelse lookup_bool "blocking"
    2.53      val falsify = lookup_bool "falsify"
    2.54      val debug = not auto andalso lookup_bool "debug"
    2.55      val verbose = debug orelse (not auto andalso lookup_bool "verbose")
    2.56 @@ -252,7 +253,7 @@
    2.57      val kodkod_sym_break = lookup_int "kodkod_sym_break"
    2.58      val timeout = if auto then NONE else lookup_time "timeout"
    2.59      val tac_timeout = lookup_time "tac_timeout"
    2.60 -    val max_threads = Int.max (0, lookup_int "max_threads")
    2.61 +    val max_threads = if auto then 1 else Int.max (0, lookup_int "max_threads")
    2.62      val show_datatypes = debug orelse lookup_bool "show_datatypes"
    2.63      val show_consts = debug orelse lookup_bool "show_consts"
    2.64      val formats = lookup_ints_assigns read_term_polymorphic "format" 0
    2.65 @@ -346,10 +347,7 @@
    2.66            else handle_exceptions ctxt)
    2.67           (fn (_, state) => pick_nits_in_subgoal state params auto i step
    2.68                             |>> curry (op =) "genuine")
    2.69 -  in
    2.70 -    if auto orelse blocking then go ()
    2.71 -    else (Toplevel.thread true (tap go); (false, state))  (* FIXME no threads in user-space *)
    2.72 -  end
    2.73 +  in if blocking then go () else Future.fork (tap go) |> K (false, state) end
    2.74  
    2.75  fun nitpick_trans (params, i) =
    2.76    Toplevel.keep (fn st =>
    2.77 @@ -362,7 +360,7 @@
    2.78  fun nitpick_params_trans params =
    2.79    Toplevel.theory
    2.80        (fold set_default_raw_param params
    2.81 -       #> tap (fn thy => 
    2.82 +       #> tap (fn thy =>
    2.83                    writeln ("Default parameters for Nitpick:\n" ^
    2.84                             (case rev (default_raw_params thy) of
    2.85                                [] => "none"
     3.1 --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Sat Sep 11 10:13:51 2010 +0200
     3.2 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Sat Sep 11 10:20:25 2010 +0200
     3.3 @@ -280,7 +280,7 @@
     3.4      (map (bound_for_built_in_rel debug ofs univ_card nat_card int_card main_j0)
     3.5           rels,
     3.6       map_filter axiom_for_built_in_rel rels)
     3.7 -  end 
     3.8 +  end
     3.9  
    3.10  fun bound_comment ctxt debug nick T R =
    3.11    short_name nick ^
     4.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Sat Sep 11 10:13:51 2010 +0200
     4.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Sat Sep 11 10:20:25 2010 +0200
     4.3 @@ -660,7 +660,7 @@
     4.4                  |>> curry3 MFun bool_M (S Minus)
     4.5                | @{const_name Pair} => do_pair_constr T accum
     4.6                | @{const_name fst} => do_nth_pair_sel 0 T accum
     4.7 -              | @{const_name snd} => do_nth_pair_sel 1 T accum 
     4.8 +              | @{const_name snd} => do_nth_pair_sel 1 T accum
     4.9                | @{const_name Id} =>
    4.10                  (MFun (mtype_for (domain_type T), S Minus, bool_M), accum)
    4.11                | @{const_name converse} =>
    4.12 @@ -894,7 +894,7 @@
    4.13                 in
    4.14                   (MApp (MApp (MRaw (t0, mtype_for (fastype_of t0)), m1), m2),
    4.15                    accum)
    4.16 -               end 
    4.17 +               end
    4.18               else
    4.19                 do_term t accum
    4.20             | _ => do_term t accum)
    4.21 @@ -1105,7 +1105,7 @@
    4.22                val (T1, T2) = pairself (curry fastype_of1 new_Ts) (t1, t2)
    4.23                val (t1', T2') =
    4.24                  case T1 of
    4.25 -                  Type (s, [T11, T12]) => 
    4.26 +                  Type (s, [T11, T12]) =>
    4.27                    (if s = @{type_name fin_fun} then
    4.28                       select_nth_constr_arg ctxt stds (fin_fun_constr T11 T12) t1
    4.29                                             0 (T11 --> T12)