static defaults for configuration options;
authorwenzelm
Sun Mar 28 16:59:06 2010 +0200 (2010-03-28)
changeset 36001992839c4be90
parent 36000 5560b2437789
child 36002 f4f343500249
static defaults for configuration options;
src/HOL/Mirabelle/Tools/mirabelle.ML
src/HOL/SMT/Tools/smt_normalize.ML
src/HOL/SMT/Tools/smt_solver.ML
src/HOL/SMT/Tools/z3_proof_rules.ML
src/HOL/SMT/Tools/z3_solver.ML
src/HOL/Tools/ATP_Manager/atp_wrapper.ML
src/HOL/Tools/Sledgehammer/metis_tactics.ML
src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
src/HOL/Tools/inductive_codegen.ML
src/HOL/Tools/lin_arith.ML
src/HOL/Tools/meson.ML
src/Provers/blast.ML
src/Pure/meta_simplifier.ML
src/Pure/unify.ML
     1.1 --- a/src/HOL/Mirabelle/Tools/mirabelle.ML	Sun Mar 28 16:13:29 2010 +0200
     1.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle.ML	Sun Mar 28 16:59:06 2010 +0200
     1.3 @@ -43,10 +43,10 @@
     1.4  
     1.5  (* Mirabelle configuration *)
     1.6  
     1.7 -val (logfile, setup1) = Attrib.config_string "mirabelle_logfile" ""
     1.8 -val (timeout, setup2) = Attrib.config_int "mirabelle_timeout" 30
     1.9 -val (start_line, setup3) = Attrib.config_int "mirabelle_start_line" 0
    1.10 -val (end_line, setup4) = Attrib.config_int "mirabelle_end_line" ~1
    1.11 +val (logfile, setup1) = Attrib.config_string "mirabelle_logfile" (K "")
    1.12 +val (timeout, setup2) = Attrib.config_int "mirabelle_timeout" (K 30)
    1.13 +val (start_line, setup3) = Attrib.config_int "mirabelle_start_line" (K 0)
    1.14 +val (end_line, setup4) = Attrib.config_int "mirabelle_end_line" (K ~1)
    1.15  
    1.16  val setup = setup1 #> setup2 #> setup3 #> setup4
    1.17  
     2.1 --- a/src/HOL/SMT/Tools/smt_normalize.ML	Sun Mar 28 16:13:29 2010 +0200
     2.2 +++ b/src/HOL/SMT/Tools/smt_normalize.ML	Sun Mar 28 16:59:06 2010 +0200
     2.3 @@ -290,7 +290,7 @@
     2.4  (* include additional rules *)
     2.5  
     2.6  val (unfold_defs, unfold_defs_setup) =
     2.7 -  Attrib.config_bool "smt_unfold_defs" true
     2.8 +  Attrib.config_bool "smt_unfold_defs" (K true)
     2.9  
    2.10  local
    2.11    val pair_rules = [@{thm fst_conv}, @{thm snd_conv}, @{thm pair_collapse}]
     3.1 --- a/src/HOL/SMT/Tools/smt_solver.ML	Sun Mar 28 16:13:29 2010 +0200
     3.2 +++ b/src/HOL/SMT/Tools/smt_solver.ML	Sun Mar 28 16:59:06 2010 +0200
     3.3 @@ -79,13 +79,13 @@
     3.4  
     3.5  (* SMT options *)
     3.6  
     3.7 -val (timeout, setup_timeout) = Attrib.config_int "smt_timeout" 30
     3.8 +val (timeout, setup_timeout) = Attrib.config_int "smt_timeout" (K 30)
     3.9  
    3.10  fun with_timeout ctxt f x =
    3.11    TimeLimit.timeLimit (Time.fromSeconds (Config.get ctxt timeout)) f x
    3.12    handle TimeLimit.TimeOut => raise SMT "timeout"
    3.13  
    3.14 -val (trace, setup_trace) = Attrib.config_bool "smt_trace" false
    3.15 +val (trace, setup_trace) = Attrib.config_bool "smt_trace" (K false)
    3.16  
    3.17  fun trace_msg ctxt f x =
    3.18    if Config.get ctxt trace then tracing (f x) else ()
    3.19 @@ -93,7 +93,7 @@
    3.20  
    3.21  (* SMT certificates *)
    3.22  
    3.23 -val (record, setup_record) = Attrib.config_bool "smt_record" true
    3.24 +val (record, setup_record) = Attrib.config_bool "smt_record" (K true)
    3.25  
    3.26  structure Certificates = Generic_Data
    3.27  (
     4.1 --- a/src/HOL/SMT/Tools/z3_proof_rules.ML	Sun Mar 28 16:13:29 2010 +0200
     4.2 +++ b/src/HOL/SMT/Tools/z3_proof_rules.ML	Sun Mar 28 16:59:06 2010 +0200
     4.3 @@ -476,7 +476,7 @@
     4.4  val true_false = @{lemma "True == ~ False" by simp}
     4.5  
     4.6  val (trace_assms, trace_assms_setup) =
     4.7 -  Attrib.config_bool "z3_trace_assms" false
     4.8 +  Attrib.config_bool "z3_trace_assms" (K false)
     4.9  
    4.10  local
    4.11    val TT_eq = @{lemma "(P = (~False)) == P" by simp}
     5.1 --- a/src/HOL/SMT/Tools/z3_solver.ML	Sun Mar 28 16:13:29 2010 +0200
     5.2 +++ b/src/HOL/SMT/Tools/z3_solver.ML	Sun Mar 28 16:59:06 2010 +0200
     5.3 @@ -17,8 +17,8 @@
     5.4  val solver_name = "z3"
     5.5  val env_var = "Z3_SOLVER"
     5.6  
     5.7 -val (proofs, proofs_setup) = Attrib.config_bool "z3_proofs" false
     5.8 -val (options, options_setup) = Attrib.config_string "z3_options" ""
     5.9 +val (proofs, proofs_setup) = Attrib.config_bool "z3_proofs" (K false)
    5.10 +val (options, options_setup) = Attrib.config_string "z3_options" (K "")
    5.11  
    5.12  fun add xs ys = ys @ xs
    5.13  
     6.1 --- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Sun Mar 28 16:13:29 2010 +0200
     6.2 +++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Sun Mar 28 16:59:06 2010 +0200
     6.3 @@ -30,14 +30,14 @@
     6.4  
     6.5  (* external problem files *)
     6.6  
     6.7 -val (destdir, destdir_setup) = Attrib.config_string "atp_destdir" "";
     6.8 +val (destdir, destdir_setup) = Attrib.config_string "atp_destdir" (K "");
     6.9    (*Empty string means create files in Isabelle's temporary files directory.*)
    6.10  
    6.11  val (problem_prefix, problem_prefix_setup) =
    6.12 -  Attrib.config_string "atp_problem_prefix" "prob";
    6.13 +  Attrib.config_string "atp_problem_prefix" (K "prob");
    6.14  
    6.15  val (measure_runtime, measure_runtime_setup) =
    6.16 -  Attrib.config_bool "atp_measure_runtime" false;
    6.17 +  Attrib.config_bool "atp_measure_runtime" (K false);
    6.18  
    6.19  
    6.20  (* prover configuration *)
     7.1 --- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Sun Mar 28 16:13:29 2010 +0200
     7.2 +++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Sun Mar 28 16:59:06 2010 +0200
     7.3 @@ -27,7 +27,7 @@
     7.4  val trace = Unsynchronized.ref false;
     7.5  fun trace_msg msg = if !trace then tracing (msg ()) else ();
     7.6  
     7.7 -val (type_lits, type_lits_setup) = Attrib.config_bool "metis_type_lits" true;
     7.8 +val (type_lits, type_lits_setup) = Attrib.config_bool "metis_type_lits" (K true);
     7.9  
    7.10  datatype mode = FO | HO | FT  (* first-order, higher-order, fully-typed *)
    7.11  
     8.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Sun Mar 28 16:13:29 2010 +0200
     8.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Sun Mar 28 16:59:06 2010 +0200
     8.3 @@ -34,10 +34,10 @@
     8.4  fun string_of_thm ctxt = PrintMode.setmp [] (Display.string_of_thm ctxt);
     8.5  
     8.6  (*For generating structured proofs: keep every nth proof line*)
     8.7 -val (modulus, modulus_setup) = Attrib.config_int "sledgehammer_modulus" 1;
     8.8 +val (modulus, modulus_setup) = Attrib.config_int "sledgehammer_modulus" (K 1);
     8.9  
    8.10  (*Indicates whether to include sort information in generated proofs*)
    8.11 -val (recon_sorts, recon_sorts_setup) = Attrib.config_bool "sledgehammer_sorts" true;
    8.12 +val (recon_sorts, recon_sorts_setup) = Attrib.config_bool "sledgehammer_sorts" (K true);
    8.13  
    8.14  val setup = modulus_setup #> recon_sorts_setup;
    8.15  
     9.1 --- a/src/HOL/Tools/inductive_codegen.ML	Sun Mar 28 16:13:29 2010 +0200
     9.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Sun Mar 28 16:59:06 2010 +0200
     9.3 @@ -794,10 +794,10 @@
     9.4        NONE => deepen bound f (i + 1)
     9.5      | SOME x => SOME x);
     9.6  
     9.7 -val (depth_bound, setup_depth_bound) = Attrib.config_int "ind_quickcheck_depth" 10;
     9.8 -val (depth_start, setup_depth_start) = Attrib.config_int "ind_quickcheck_depth_start" 1;
     9.9 -val (random_values, setup_random_values) = Attrib.config_int "ind_quickcheck_random" 5;
    9.10 -val (size_offset, setup_size_offset) = Attrib.config_int "ind_quickcheck_size_offset" 0;
    9.11 +val (depth_bound, setup_depth_bound) = Attrib.config_int "ind_quickcheck_depth" (K 10);
    9.12 +val (depth_start, setup_depth_start) = Attrib.config_int "ind_quickcheck_depth_start" (K 1);
    9.13 +val (random_values, setup_random_values) = Attrib.config_int "ind_quickcheck_random" (K 5);
    9.14 +val (size_offset, setup_size_offset) = Attrib.config_int "ind_quickcheck_size_offset" (K 0);
    9.15  
    9.16  fun test_term ctxt report t =
    9.17    let
    10.1 --- a/src/HOL/Tools/lin_arith.ML	Sun Mar 28 16:13:29 2010 +0200
    10.2 +++ b/src/HOL/Tools/lin_arith.ML	Sun Mar 28 16:59:06 2010 +0200
    10.3 @@ -100,8 +100,8 @@
    10.4    {splits = splits, inj_consts = update (op =) c inj_consts,
    10.5     discrete = discrete});
    10.6  
    10.7 -val (split_limit, setup_split_limit) = Attrib.config_int "linarith_split_limit" 9;
    10.8 -val (neq_limit, setup_neq_limit) = Attrib.config_int "linarith_neq_limit" 9;
    10.9 +val (split_limit, setup_split_limit) = Attrib.config_int "linarith_split_limit" (K 9);
   10.10 +val (neq_limit, setup_neq_limit) = Attrib.config_int "linarith_neq_limit" (K 9);
   10.11  
   10.12  
   10.13  structure LA_Data =
    11.1 --- a/src/HOL/Tools/meson.ML	Sun Mar 28 16:13:29 2010 +0200
    11.2 +++ b/src/HOL/Tools/meson.ML	Sun Mar 28 16:59:06 2010 +0200
    11.3 @@ -48,7 +48,7 @@
    11.4  fun trace_msg msg = if ! trace then tracing (msg ()) else ();
    11.5  
    11.6  val max_clauses_default = 60;
    11.7 -val (max_clauses, setup) = Attrib.config_int "max_clauses" max_clauses_default;
    11.8 +val (max_clauses, setup) = Attrib.config_int "max_clauses" (K max_clauses_default);
    11.9  
   11.10  val disj_forward = @{thm disj_forward};
   11.11  val disj_forward2 = @{thm disj_forward2};
    12.1 --- a/src/Provers/blast.ML	Sun Mar 28 16:13:29 2010 +0200
    12.2 +++ b/src/Provers/blast.ML	Sun Mar 28 16:59:06 2010 +0200
    12.3 @@ -1275,7 +1275,7 @@
    12.4  (*Public version with fixed depth*)
    12.5  fun depth_tac cs lim i st = timing_depth_tac (start_timing ()) cs lim i st;
    12.6  
    12.7 -val (depth_limit, setup_depth_limit) = Attrib.config_int_global "blast_depth_limit" 20;
    12.8 +val (depth_limit, setup_depth_limit) = Attrib.config_int_global "blast_depth_limit" (K 20);
    12.9  
   12.10  fun blast_tac cs i st =
   12.11      ((DEEPEN (1, Config.get_thy (Thm.theory_of_thm st) depth_limit)
    13.1 --- a/src/Pure/meta_simplifier.ML	Sun Mar 28 16:13:29 2010 +0200
    13.2 +++ b/src/Pure/meta_simplifier.ML	Sun Mar 28 16:59:06 2010 +0200
    13.3 @@ -251,7 +251,7 @@
    13.4  
    13.5  (* simp depth *)
    13.6  
    13.7 -val simp_depth_limit_value = Config.declare false "simp_depth_limit" (Config.Int 100);
    13.8 +val simp_depth_limit_value = Config.declare false "simp_depth_limit" (K (Config.Int 100));
    13.9  val simp_depth_limit = Config.int simp_depth_limit_value;
   13.10  
   13.11  val trace_simp_depth_limit = Unsynchronized.ref 1;
   13.12 @@ -274,10 +274,10 @@
   13.13  
   13.14  exception SIMPLIFIER of string * thm;
   13.15  
   13.16 -val debug_simp_value = Config.declare false "debug_simp" (Config.Bool false);
   13.17 +val debug_simp_value = Config.declare false "debug_simp" (K (Config.Bool false));
   13.18  val debug_simp = Config.bool debug_simp_value;
   13.19  
   13.20 -val trace_simp_value = Config.declare false "trace_simp" (Config.Bool false);
   13.21 +val trace_simp_value = Config.declare false "trace_simp" (K (Config.Bool false));
   13.22  val trace_simp = Config.bool trace_simp_value;
   13.23  val trace_simp_ref = Unsynchronized.ref false;
   13.24  
    14.1 --- a/src/Pure/unify.ML	Sun Mar 28 16:13:29 2010 +0200
    14.2 +++ b/src/Pure/unify.ML	Sun Mar 28 16:59:06 2010 +0200
    14.3 @@ -32,19 +32,19 @@
    14.4  (*Unification options*)
    14.5  
    14.6  (*tracing starts above this depth, 0 for full*)
    14.7 -val trace_bound_value = Config.declare true "unify_trace_bound" (Config.Int 50);
    14.8 +val trace_bound_value = Config.declare true "unify_trace_bound" (K (Config.Int 50));
    14.9  val trace_bound = Config.int trace_bound_value;
   14.10  
   14.11  (*unification quits above this depth*)
   14.12 -val search_bound_value = Config.declare true "unify_search_bound" (Config.Int 60);
   14.13 +val search_bound_value = Config.declare true "unify_search_bound" (K (Config.Int 60));
   14.14  val search_bound = Config.int search_bound_value;
   14.15  
   14.16  (*print dpairs before calling SIMPL*)
   14.17 -val trace_simp_value = Config.declare true "unify_trace_simp" (Config.Bool false);
   14.18 +val trace_simp_value = Config.declare true "unify_trace_simp" (K (Config.Bool false));
   14.19  val trace_simp = Config.bool trace_simp_value;
   14.20  
   14.21  (*announce potential incompleteness of type unification*)
   14.22 -val trace_types_value = Config.declare true "unify_trace_types" (Config.Bool false);
   14.23 +val trace_types_value = Config.declare true "unify_trace_types" (K (Config.Bool false));
   14.24  val trace_types = Config.bool trace_types_value;
   14.25  
   14.26