# HG changeset patch # User blanchet # Date 1284193724 -7200 # Node ID ce5c6a8b03599d83e61541b7c2f889e095ec6da6 # Parent 80420a0f21797d917cca3bbe47db1a09504753e1 start renaming "Auto_Counterexample" to "Auto_Tools"; Auto Sledgehammer now uses so the name is clearly wrong diff -r 80420a0f2179 -r ce5c6a8b0359 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Sat Sep 11 10:25:27 2010 +0200 +++ b/src/HOL/IsaMakefile Sat Sep 11 10:28:44 2010 +0200 @@ -122,8 +122,8 @@ $(SRC)/Tools/IsaPlanner/rw_tools.ML \ $(SRC)/Tools/IsaPlanner/zipper.ML \ $(SRC)/Tools/atomize_elim.ML \ - $(SRC)/Tools/auto_counterexample.ML \ $(SRC)/Tools/auto_solve.ML \ + $(SRC)/Tools/auto_tools.ML \ $(SRC)/Tools/coherent.ML \ $(SRC)/Tools/cong_tac.ML \ $(SRC)/Tools/eqsubst.ML \ diff -r 80420a0f2179 -r ce5c6a8b0359 src/Tools/Code_Generator.thy --- a/src/Tools/Code_Generator.thy Sat Sep 11 10:25:27 2010 +0200 +++ b/src/Tools/Code_Generator.thy Sat Sep 11 10:28:44 2010 +0200 @@ -8,8 +8,8 @@ imports Pure uses "~~/src/Tools/cache_io.ML" + "~~/src/Tools/auto_tools.ML" "~~/src/Tools/auto_solve.ML" - "~~/src/Tools/auto_counterexample.ML" "~~/src/Tools/quickcheck.ML" "~~/src/Tools/value.ML" "~~/src/Tools/Code/code_preproc.ML" diff -r 80420a0f2179 -r ce5c6a8b0359 src/Tools/auto_counterexample.ML --- a/src/Tools/auto_counterexample.ML Sat Sep 11 10:25:27 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,59 +0,0 @@ -(* Title: Tools/auto_counterexample.ML - Author: Jasmin Blanchette, TU Muenchen - -Counterexample Search Unit (do not abbreviate!). -*) - -signature AUTO_COUNTEREXAMPLE = -sig - val time_limit: int Unsynchronized.ref - - val register_tool : - string * (Proof.state -> bool * Proof.state) -> theory -> theory -end; - -structure Auto_Counterexample : AUTO_COUNTEREXAMPLE = -struct - -(* preferences *) - -val time_limit = Unsynchronized.ref 2500 - -val _ = - ProofGeneralPgip.add_preference Preferences.category_tracing - (Preferences.nat_pref time_limit - "auto-counterexample-time-limit" - "Time limit for automatic counterexample search (in milliseconds).") - - -(* configuration *) - -structure Data = Theory_Data -( - type T = (string * (Proof.state -> bool * Proof.state)) list - val empty = [] - val extend = I - fun merge data : T = AList.merge (op =) (K true) data -) - -val register_tool = Data.map o AList.update (op =) - - -(* automatic testing *) - -val _ = Context.>> (Specification.add_theorem_hook (fn interact => fn state => - case !time_limit of - 0 => state - | ms => - TimeLimit.timeLimit (Time.fromMilliseconds ms) - (fn () => - if interact andalso not (!Toplevel.quiet) then - fold_rev (fn (_, tool) => fn (true, state) => (true, state) - | (false, state) => tool state) - (Data.get (Proof.theory_of state)) (false, state) |> snd - else - state) () - handle TimeLimit.TimeOut => - (warning "Automatic counterexample search timed out."; state))) - -end; diff -r 80420a0f2179 -r ce5c6a8b0359 src/Tools/auto_tools.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/auto_tools.ML Sat Sep 11 10:28:44 2010 +0200 @@ -0,0 +1,59 @@ +(* Title: Tools/auto_counterexample.ML + Author: Jasmin Blanchette, TU Muenchen + +Counterexample Search Unit (do not abbreviate!). +*) + +signature AUTO_COUNTEREXAMPLE = +sig + val time_limit: int Unsynchronized.ref + + val register_tool : + string * (Proof.state -> bool * Proof.state) -> theory -> theory +end; + +structure Auto_Counterexample : AUTO_COUNTEREXAMPLE = +struct + +(* preferences *) + +val time_limit = Unsynchronized.ref 2500 + +val _ = + ProofGeneralPgip.add_preference Preferences.category_tracing + (Preferences.nat_pref time_limit + "auto-counterexample-time-limit" + "Time limit for automatic counterexample search (in milliseconds).") + + +(* configuration *) + +structure Data = Theory_Data +( + type T = (string * (Proof.state -> bool * Proof.state)) list + val empty = [] + val extend = I + fun merge data : T = AList.merge (op =) (K true) data +) + +val register_tool = Data.map o AList.update (op =) + + +(* automatic testing *) + +val _ = Context.>> (Specification.add_theorem_hook (fn interact => fn state => + case !time_limit of + 0 => state + | ms => + TimeLimit.timeLimit (Time.fromMilliseconds ms) + (fn () => + if interact andalso not (!Toplevel.quiet) then + fold_rev (fn (_, tool) => fn (true, state) => (true, state) + | (false, state) => tool state) + (Data.get (Proof.theory_of state)) (false, state) |> snd + else + state) () + handle TimeLimit.TimeOut => + (warning "Automatic counterexample search timed out."; state))) + +end;