finished renaming "Auto_Counterexample" to "Auto_Tools"
authorblanchet
Sat Sep 11 10:35:00 2010 +0200 (2010-09-11)
changeset 3932405452dd66b2b
parent 39323 ce5c6a8b0359
child 39325 5208954d906c
finished renaming "Auto_Counterexample" to "Auto_Tools"
src/HOL/Mutabelle/MutabelleExtra.thy
src/HOL/Mutabelle/mutabelle_extra.ML
src/HOL/Tools/Nitpick/nitpick_isar.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
src/Tools/auto_tools.ML
src/Tools/quickcheck.ML
     1.1 --- a/src/HOL/Mutabelle/MutabelleExtra.thy	Sat Sep 11 10:28:44 2010 +0200
     1.2 +++ b/src/HOL/Mutabelle/MutabelleExtra.thy	Sat Sep 11 10:35:00 2010 +0200
     1.3 @@ -29,7 +29,7 @@
     1.4  nitpick_params [timeout = 5 s, sat_solver = MiniSat, no_overlord, verbose, card = 1-5, iter = 1,2,4,8,12]
     1.5  refute_params [maxtime = 10, minsize = 1, maxsize = 5, satsolver = jerusat]
     1.6  *)
     1.7 -ML {* Auto_Counterexample.time_limit := 10 *}
     1.8 +ML {* Auto_Tools.time_limit := 10 *}
     1.9  
    1.10  
    1.11  text {* Uncomment the following ML code to check the counterexample generation with all theorems of Complex_Main. *}
    1.12 @@ -53,4 +53,4 @@
    1.13  ML {* Output.priority_fn := old_pr *}
    1.14  ML {* Output.warning_fn := old_wa *}
    1.15  
    1.16 -end
    1.17 \ No newline at end of file
    1.18 +end
     2.1 --- a/src/HOL/Mutabelle/mutabelle_extra.ML	Sat Sep 11 10:28:44 2010 +0200
     2.2 +++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Sat Sep 11 10:35:00 2010 +0200
     2.3 @@ -94,13 +94,13 @@
     2.4   (map_types (inst_type insts) (Mutabelle.freeze t));
     2.5  
     2.6  fun invoke_quickcheck quickcheck_generator thy t =
     2.7 -  TimeLimit.timeLimit (Time.fromSeconds (! Auto_Counterexample.time_limit))
     2.8 +  TimeLimit.timeLimit (Time.fromSeconds (!Auto_Tools.time_limit))
     2.9        (fn _ =>
    2.10            case Quickcheck.gen_test_term (ProofContext.init_global thy) true (SOME quickcheck_generator)
    2.11                                      size iterations (preprocess thy [] t) of
    2.12              (NONE, (time_report, report)) => (NoCex, (time_report, report))
    2.13            | (SOME _, (time_report, report)) => (GenuineCex, (time_report, report))) ()
    2.14 -  handle TimeLimit.TimeOut => (Timeout, ([("timelimit", !Auto_Counterexample.time_limit)], NONE))
    2.15 +  handle TimeLimit.TimeOut => (Timeout, ([("timelimit", !Auto_Tools.time_limit)], NONE))
    2.16  
    2.17  fun quickcheck_mtd quickcheck_generator =
    2.18    ("quickcheck_" ^ quickcheck_generator, invoke_quickcheck quickcheck_generator)
     3.1 --- a/src/HOL/Tools/Nitpick/nitpick_isar.ML	Sat Sep 11 10:28:44 2010 +0200
     3.2 +++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML	Sat Sep 11 10:35:00 2010 +0200
     3.3 @@ -383,6 +383,6 @@
     3.4  fun auto_nitpick state =
     3.5    if not (!auto) then (false, state) else pick_nits [] true 1 0 state
     3.6  
     3.7 -val setup = Auto_Counterexample.register_tool ("nitpick", auto_nitpick)
     3.8 +val setup = Auto_Tools.register_tool ("nitpick", auto_nitpick)
     3.9  
    3.10  end;
     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Sat Sep 11 10:28:44 2010 +0200
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Sat Sep 11 10:35:00 2010 +0200
     4.3 @@ -313,7 +313,6 @@
     4.4                         (minimize_command [] 1) state
     4.5      end
     4.6  
     4.7 -val setup =
     4.8 -  Auto_Counterexample.register_tool ("sledgehammer", auto_sledgehammer)
     4.9 +val setup = Auto_Tools.register_tool ("sledgehammer", auto_sledgehammer)
    4.10  
    4.11  end;
     5.1 --- a/src/Tools/auto_tools.ML	Sat Sep 11 10:28:44 2010 +0200
     5.2 +++ b/src/Tools/auto_tools.ML	Sat Sep 11 10:35:00 2010 +0200
     5.3 @@ -1,10 +1,10 @@
     5.4 -(*  Title:      Tools/auto_counterexample.ML
     5.5 +(*  Title:      Tools/auto_tools.ML
     5.6      Author:     Jasmin Blanchette, TU Muenchen
     5.7  
     5.8 -Counterexample Search Unit (do not abbreviate!).
     5.9 +Manager for tools that should be run automatically on newly entered conjectures.
    5.10  *)
    5.11  
    5.12 -signature AUTO_COUNTEREXAMPLE =
    5.13 +signature AUTO_TOOLS =
    5.14  sig
    5.15    val time_limit: int Unsynchronized.ref
    5.16  
    5.17 @@ -12,7 +12,7 @@
    5.18      string * (Proof.state -> bool * Proof.state) -> theory -> theory
    5.19  end;
    5.20  
    5.21 -structure Auto_Counterexample : AUTO_COUNTEREXAMPLE =
    5.22 +structure Auto_Tools : AUTO_TOOLS =
    5.23  struct
    5.24  
    5.25  (* preferences *)
    5.26 @@ -22,8 +22,8 @@
    5.27  val _ =
    5.28    ProofGeneralPgip.add_preference Preferences.category_tracing
    5.29      (Preferences.nat_pref time_limit
    5.30 -      "auto-counterexample-time-limit"
    5.31 -      "Time limit for automatic counterexample search (in milliseconds).")
    5.32 +      "auto-tools-time-limit"
    5.33 +      "Time limit for automatic tools (in milliseconds).")
    5.34  
    5.35  
    5.36  (* configuration *)
    5.37 @@ -53,7 +53,6 @@
    5.38                     (Data.get (Proof.theory_of state)) (false, state) |> snd
    5.39              else
    5.40                state) ()
    5.41 -    handle TimeLimit.TimeOut =>
    5.42 -           (warning "Automatic counterexample search timed out."; state)))
    5.43 +    handle TimeLimit.TimeOut => state))
    5.44  
    5.45  end;
     6.1 --- a/src/Tools/quickcheck.ML	Sat Sep 11 10:28:44 2010 +0200
     6.2 +++ b/src/Tools/quickcheck.ML	Sat Sep 11 10:35:00 2010 +0200
     6.3 @@ -320,7 +320,7 @@
     6.4            Pretty.mark Markup.hilite (pretty_counterex ctxt cex)])) state)
     6.5      end
     6.6  
     6.7 -val setup = Auto_Counterexample.register_tool ("quickcheck", auto_quickcheck)
     6.8 +val setup = Auto_Tools.register_tool ("quickcheck", auto_quickcheck)
     6.9  
    6.10  
    6.11  (* Isar commands *)