# HG changeset patch # User blanchet # Date 1284193225 -7200 # Node ID b6c4385ab400682c1f3b31d7b65d9c69ac6662c3 # Parent 27f7b7748425e02e0d3c802d8231b20d5c266d10 change defaults of Auto Nitpick so that it consumes less resources (time and Kodkod threads) diff -r 27f7b7748425 -r b6c4385ab400 src/HOL/Tools/Nitpick/nitpick.ML --- a/src/HOL/Tools/Nitpick/nitpick.ML Sat Sep 11 10:13:51 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Sat Sep 11 10:20:25 2010 +0200 @@ -144,7 +144,7 @@ rel_table: nut NameTable.table, unsound: bool, scope: scope} - + type rich_problem = KK.problem * problem_extension fun pretties_for_formulas _ _ [] = [] diff -r 27f7b7748425 -r b6c4385ab400 src/HOL/Tools/Nitpick/nitpick_isar.ML --- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Sat Sep 11 10:13:51 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Sat Sep 11 10:20:25 2010 +0200 @@ -10,7 +10,7 @@ sig type params = Nitpick.params - val auto: bool Unsynchronized.ref + val auto : bool Unsynchronized.ref val default_params : theory -> (string * string) list -> params val setup : theory -> theory end; @@ -24,7 +24,7 @@ open Nitpick_Nut open Nitpick -val auto = Unsynchronized.ref false; +val auto = Unsynchronized.ref false val _ = ProofGeneralPgip.add_preference Preferences.category_tracing @@ -109,7 +109,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 @@ -212,8 +212,8 @@ lookup_assigns read prefix "" (space_explode " ") fun lookup_time name = case lookup name of - NONE => NONE - | SOME s => parse_time_option name s + SOME s => parse_time_option name s + | NONE => NONE val read_type_polymorphic = Syntax.read_typ ctxt #> Logic.mk_type #> singleton (Variable.polymorphic ctxt) #> Logic.dest_type @@ -229,11 +229,12 @@ val bisim_depths = lookup_int_seq "bisim_depth" ~1 val boxes = lookup_bool_option_assigns read_type_polymorphic "box" val finitizes = lookup_bool_option_assigns read_type_polymorphic "finitize" - val monos = lookup_bool_option_assigns read_type_polymorphic "mono" + val monos = if auto then [(NONE, SOME true)] + else lookup_bool_option_assigns read_type_polymorphic "mono" val stds = lookup_bool_assigns read_type_polymorphic "std" val wfs = lookup_bool_option_assigns read_const_polymorphic "wf" val sat_solver = lookup_string "sat_solver" - val blocking = not auto andalso lookup_bool "blocking" + val blocking = auto orelse lookup_bool "blocking" val falsify = lookup_bool "falsify" val debug = not auto andalso lookup_bool "debug" val verbose = debug orelse (not auto andalso lookup_bool "verbose") @@ -252,7 +253,7 @@ val kodkod_sym_break = lookup_int "kodkod_sym_break" val timeout = if auto then NONE else lookup_time "timeout" val tac_timeout = lookup_time "tac_timeout" - val max_threads = Int.max (0, lookup_int "max_threads") + val max_threads = if auto then 1 else Int.max (0, lookup_int "max_threads") val show_datatypes = debug orelse lookup_bool "show_datatypes" val show_consts = debug orelse lookup_bool "show_consts" val formats = lookup_ints_assigns read_term_polymorphic "format" 0 @@ -346,10 +347,7 @@ else handle_exceptions ctxt) (fn (_, state) => pick_nits_in_subgoal state params auto i step |>> curry (op =) "genuine") - in - if auto orelse blocking then go () - else (Toplevel.thread true (tap go); (false, state)) (* FIXME no threads in user-space *) - end + in if blocking then go () else Future.fork (tap go) |> K (false, state) end fun nitpick_trans (params, i) = Toplevel.keep (fn st => @@ -362,7 +360,7 @@ fun nitpick_params_trans params = Toplevel.theory (fold set_default_raw_param params - #> tap (fn thy => + #> tap (fn thy => writeln ("Default parameters for Nitpick:\n" ^ (case rev (default_raw_params thy) of [] => "none" diff -r 27f7b7748425 -r b6c4385ab400 src/HOL/Tools/Nitpick/nitpick_kodkod.ML --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Sat Sep 11 10:13:51 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Sat Sep 11 10:20:25 2010 +0200 @@ -280,7 +280,7 @@ (map (bound_for_built_in_rel debug ofs univ_card nat_card int_card main_j0) rels, map_filter axiom_for_built_in_rel rels) - end + end fun bound_comment ctxt debug nick T R = short_name nick ^ diff -r 27f7b7748425 -r b6c4385ab400 src/HOL/Tools/Nitpick/nitpick_mono.ML --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Sat Sep 11 10:13:51 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Sat Sep 11 10:20:25 2010 +0200 @@ -660,7 +660,7 @@ |>> curry3 MFun bool_M (S Minus) | @{const_name Pair} => do_pair_constr T accum | @{const_name fst} => do_nth_pair_sel 0 T accum - | @{const_name snd} => do_nth_pair_sel 1 T accum + | @{const_name snd} => do_nth_pair_sel 1 T accum | @{const_name Id} => (MFun (mtype_for (domain_type T), S Minus, bool_M), accum) | @{const_name converse} => @@ -894,7 +894,7 @@ in (MApp (MApp (MRaw (t0, mtype_for (fastype_of t0)), m1), m2), accum) - end + end else do_term t accum | _ => do_term t accum) @@ -1105,7 +1105,7 @@ val (T1, T2) = pairself (curry fastype_of1 new_Ts) (t1, t2) val (t1', T2') = case T1 of - Type (s, [T11, T12]) => + Type (s, [T11, T12]) => (if s = @{type_name fin_fun} then select_nth_constr_arg ctxt stds (fin_fun_constr T11 T12) t1 0 (T11 --> T12)