# HG changeset patch # User wenzelm # Date 1240691353 -7200 # Node ID e6349035148ab5041b31c0e01898869b0f10eca3 # Parent e54777ab68bdc7da95d3c32546eaf61545d493ef# Parent 7882a1268a48370b88e56a93551119e44d2eb2ad merged diff -r e54777ab68bd -r e6349035148a CONTRIBUTORS --- a/CONTRIBUTORS Sat Apr 25 21:42:05 2009 +0200 +++ b/CONTRIBUTORS Sat Apr 25 22:29:13 2009 +0200 @@ -7,6 +7,10 @@ Contributions to this Isabelle version -------------------------------------- + +Contributions to Isabelle2009 +----------------------------- + * March 2009: Robert Himmelmann, TUM and Amine Chaieb, University of Cambridge Elementary topology in Euclidean space. diff -r e54777ab68bd -r e6349035148a contrib/SystemOnTPTP/remote --- a/contrib/SystemOnTPTP/remote Sat Apr 25 21:42:05 2009 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,120 +0,0 @@ -#!/usr/bin/env perl -# -# Wrapper for custom remote provers on SystemOnTPTP -# Author: Fabian Immler, TU Muenchen -# - -use warnings; -use strict; -use Getopt::Std; -use HTTP::Request::Common; -use LWP; - -my $SystemOnTPTPFormReplyURL = "http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTPFormReply"; - -# default parameters -my %URLParameters = ( - "NoHTML" => 1, - "QuietFlag" => "-q01", - "X2TPTP" => "-S", - "SubmitButton" => "RunSelectedSystems", - "ProblemSource" => "UPLOAD", - ); - -#----Get format and transform options if specified -my %Options; -getopts("hws:t:c:",\%Options); - -#----Usage -sub usage() { - print("Usage: remote [] \n"); - print(" are ...\n"); - print(" -h - print this help\n"); - print(" -w - list available ATP systems\n"); - print(" -s - specified system to use\n"); - print(" -t - CPU time limit for system\n"); - print(" -c - custom command for system\n"); - print(" - TPTP problem file\n"); - exit(0); -} -if (exists($Options{'h'})) { - usage(); -} -#----What systems flag -if (exists($Options{'w'})) { - $URLParameters{"SubmitButton"} = "ListSystems"; - delete($URLParameters{"ProblemSource"}); -} -#----Selected system -my $System; -if (exists($Options{'s'})) { - $System = $Options{'s'}; -} else { - # use Vampire as default - $System = "Vampire---9.0"; -} -$URLParameters{"System___$System"} = $System; - -#----Time limit -if (exists($Options{'t'})) { - $URLParameters{"TimeLimit___$System"} = $Options{'t'}; -} -#----Custom command -if (exists($Options{'c'})) { - $URLParameters{"Command___$System"} = $Options{'c'}; -} - -#----Get single file name -if (exists($URLParameters{"ProblemSource"})) { - if (scalar(@ARGV) >= 1) { - $URLParameters{"UPLOADProblem"} = [shift(@ARGV)]; - } else { - print("Missing problem file\n"); - usage(); - die; - } -} - -# Query Server -my $Agent = LWP::UserAgent->new; -if (exists($Options{'t'})) { - # give server more time to respond - $Agent->timeout($Options{'t'} + 10); -} -my $Request = POST($SystemOnTPTPFormReplyURL, - Content_Type => 'form-data',Content => \%URLParameters); -my $Response = $Agent->request($Request); - -#catch errors / failure -if(! $Response->is_success){ - print "HTTP-Error: " . $Response->message . "\n"; - exit(-1); -} elsif (exists($Options{'w'})) { - print $Response->content; - exit (0); -} elsif ($Response->content =~ /WARNING: (\S*) does not exist/) { - print "Specified System $1 does not exist\n"; - exit(-1); -} elsif ($Response->content =~ /%\s*Result\s*:\s*Unsatisfiable.*\n%\s*Output\s*:\s*(CNF)?Refutation.*\n%/) { - my @lines = split( /\n/, $Response->content); - my $extract = ""; - foreach my $line (@lines){ - #ignore comments - if ($line !~ /^%/ && !($line eq "")) { - $extract .= "$line"; - } - } - # insert newlines after ').' - $extract =~ s/\s//g; - $extract =~ s/\)\.cnf/\)\.\ncnf/g; - - # orientation for res_reconstruct.ML - print "# SZS output start CNFRefutation.\n"; - print "$extract\n"; - print "# SZS output end CNFRefutation.\n"; - exit(0); -} else { - print "Remote-script could not extract proof:\n".$Response->content; - exit(-1); -} - diff -r e54777ab68bd -r e6349035148a lib/scripts/SystemOnTPTP --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/lib/scripts/SystemOnTPTP Sat Apr 25 22:29:13 2009 +0200 @@ -0,0 +1,120 @@ +#!/usr/bin/env perl +# +# Wrapper for custom remote provers on SystemOnTPTP +# Author: Fabian Immler, TU Muenchen +# + +use warnings; +use strict; +use Getopt::Std; +use HTTP::Request::Common; +use LWP; + +my $SystemOnTPTPFormReplyURL = "http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTPFormReply"; + +# default parameters +my %URLParameters = ( + "NoHTML" => 1, + "QuietFlag" => "-q01", + "X2TPTP" => "-S", + "SubmitButton" => "RunSelectedSystems", + "ProblemSource" => "UPLOAD", + ); + +#----Get format and transform options if specified +my %Options; +getopts("hws:t:c:",\%Options); + +#----Usage +sub usage() { + print("Usage: remote [] \n"); + print(" are ...\n"); + print(" -h - print this help\n"); + print(" -w - list available ATP systems\n"); + print(" -s - specified system to use\n"); + print(" -t - CPU time limit for system\n"); + print(" -c - custom command for system\n"); + print(" - TPTP problem file\n"); + exit(0); +} +if (exists($Options{'h'})) { + usage(); +} +#----What systems flag +if (exists($Options{'w'})) { + $URLParameters{"SubmitButton"} = "ListSystems"; + delete($URLParameters{"ProblemSource"}); +} +#----Selected system +my $System; +if (exists($Options{'s'})) { + $System = $Options{'s'}; +} else { + # use Vampire as default + $System = "Vampire---9.0"; +} +$URLParameters{"System___$System"} = $System; + +#----Time limit +if (exists($Options{'t'})) { + $URLParameters{"TimeLimit___$System"} = $Options{'t'}; +} +#----Custom command +if (exists($Options{'c'})) { + $URLParameters{"Command___$System"} = $Options{'c'}; +} + +#----Get single file name +if (exists($URLParameters{"ProblemSource"})) { + if (scalar(@ARGV) >= 1) { + $URLParameters{"UPLOADProblem"} = [shift(@ARGV)]; + } else { + print("Missing problem file\n"); + usage(); + die; + } +} + +# Query Server +my $Agent = LWP::UserAgent->new; +if (exists($Options{'t'})) { + # give server more time to respond + $Agent->timeout($Options{'t'} + 10); +} +my $Request = POST($SystemOnTPTPFormReplyURL, + Content_Type => 'form-data',Content => \%URLParameters); +my $Response = $Agent->request($Request); + +#catch errors / failure +if(! $Response->is_success){ + print "HTTP-Error: " . $Response->message . "\n"; + exit(-1); +} elsif (exists($Options{'w'})) { + print $Response->content; + exit (0); +} elsif ($Response->content =~ /WARNING: (\S*) does not exist/) { + print "Specified System $1 does not exist\n"; + exit(-1); +} elsif ($Response->content =~ /%\s*Result\s*:\s*Unsatisfiable.*\n%\s*Output\s*:\s*(CNF)?Refutation.*\n%/) { + my @lines = split( /\n/, $Response->content); + my $extract = ""; + foreach my $line (@lines){ + #ignore comments + if ($line !~ /^%/ && !($line eq "")) { + $extract .= "$line"; + } + } + # insert newlines after ').' + $extract =~ s/\s//g; + $extract =~ s/\)\.cnf/\)\.\ncnf/g; + + # orientation for res_reconstruct.ML + print "# SZS output start CNFRefutation.\n"; + print "$extract\n"; + print "# SZS output end CNFRefutation.\n"; + exit(0); +} else { + print "Remote-script could not extract proof:\n".$Response->content; + exit(-1); +} + diff -r e54777ab68bd -r e6349035148a src/HOL/HOL.thy --- a/src/HOL/HOL.thy Sat Apr 25 21:42:05 2009 +0200 +++ b/src/HOL/HOL.thy Sat Apr 25 22:29:13 2009 +0200 @@ -8,6 +8,7 @@ imports Pure "~~/src/Tools/Code_Generator" uses ("Tools/hologic.ML") + "~~/src/Tools/auto_solve.ML" "~~/src/Tools/IsaPlanner/zipper.ML" "~~/src/Tools/IsaPlanner/isand.ML" "~~/src/Tools/IsaPlanner/rw_tools.ML" @@ -1921,7 +1922,7 @@ quickcheck_params [size = 5, iterations = 50] -subsection {* Nitpick hooks *} +subsection {* Nitpick setup *} text {* This will be relocated once Nitpick is moved to HOL. *} @@ -1947,10 +1948,14 @@ val description = "introduction rules for (co)inductive predicates as needed by Nitpick" ) *} -setup {* Nitpick_Const_Def_Thms.setup - #> Nitpick_Const_Simp_Thms.setup - #> Nitpick_Const_Psimp_Thms.setup - #> Nitpick_Ind_Intro_Thms.setup *} + +setup {* + Nitpick_Const_Def_Thms.setup + #> Nitpick_Const_Simp_Thms.setup + #> Nitpick_Const_Psimp_Thms.setup + #> Nitpick_Ind_Intro_Thms.setup +*} + subsection {* Legacy tactics and ML bindings *} diff -r e54777ab68bd -r e6349035148a src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Sat Apr 25 21:42:05 2009 +0200 +++ b/src/HOL/IsaMakefile Sat Apr 25 22:29:13 2009 +0200 @@ -89,6 +89,7 @@ $(SRC)/Tools/IsaPlanner/rw_tools.ML \ $(SRC)/Tools/IsaPlanner/zipper.ML \ $(SRC)/Tools/atomize_elim.ML \ + $(SRC)/Tools/auto_solve.ML \ $(SRC)/Tools/code/code_haskell.ML \ $(SRC)/Tools/code/code_ml.ML \ $(SRC)/Tools/code/code_name.ML \ diff -r e54777ab68bd -r e6349035148a src/HOL/Tools/atp_manager.ML --- a/src/HOL/Tools/atp_manager.ML Sat Apr 25 21:42:05 2009 +0200 +++ b/src/HOL/Tools/atp_manager.ML Sat Apr 25 22:29:13 2009 +0200 @@ -51,15 +51,17 @@ fun set_timeout time = CRITICAL (fn () => timeout := time); val _ = - ProofGeneralPgip.add_preference "Proof" + ProofGeneralPgip.add_preference Preferences.category_proof (Preferences.string_pref atps "ATP: provers" "Default automatic provers (separated by whitespace)"); -val _ = ProofGeneralPgip.add_preference "Proof" +val _ = + ProofGeneralPgip.add_preference Preferences.category_proof (Preferences.int_pref max_atps "ATP: maximum number" "How many provers may run in parallel"); -val _ = ProofGeneralPgip.add_preference "Proof" +val _ = + ProofGeneralPgip.add_preference Preferences.category_proof (Preferences.int_pref timeout "ATP: timeout" "ATPs will be interrupted after this time (in seconds)"); diff -r e54777ab68bd -r e6349035148a src/HOL/Tools/atp_wrapper.ML --- a/src/HOL/Tools/atp_wrapper.ML Sat Apr 25 21:42:05 2009 +0200 +++ b/src/HOL/Tools/atp_wrapper.ML Sat Apr 25 22:29:13 2009 +0200 @@ -1,5 +1,4 @@ (* Title: HOL/Tools/atp_wrapper.ML - ID: $Id$ Author: Fabian Immler, TU Muenchen Wrapper functions for external ATPs. @@ -179,7 +178,7 @@ fun remote_prover_opts max_new theory_const args timeout = tptp_prover_opts max_new theory_const - (Path.explode "$ISABELLE_HOME/contrib/SystemOnTPTP/remote", args ^ " -t " ^ string_of_int timeout) + (Path.explode "$ISABELLE_HOME/lib/scripts/SystemOnTPTP", args ^ " -t " ^ string_of_int timeout) timeout; val remote_prover = remote_prover_opts 60 false; diff -r e54777ab68bd -r e6349035148a src/Pure/IsaMakefile --- a/src/Pure/IsaMakefile Sat Apr 25 21:42:05 2009 +0200 +++ b/src/Pure/IsaMakefile Sat Apr 25 22:29:13 2009 +0200 @@ -40,9 +40,8 @@ Pure: $(OUT)/Pure -$(OUT)/Pure: $(BOOTSTRAP_FILES) \ - Concurrent/ROOT.ML Concurrent/future.ML \ - Concurrent/mailbox.ML Concurrent/par_list.ML \ +$(OUT)/Pure: $(BOOTSTRAP_FILES) Concurrent/ROOT.ML \ + Concurrent/future.ML Concurrent/mailbox.ML Concurrent/par_list.ML \ Concurrent/par_list_dummy.ML Concurrent/simple_thread.ML \ Concurrent/synchronized.ML Concurrent/task_queue.ML General/ROOT.ML \ General/alist.ML General/antiquote.ML General/balanced_tree.ML \ @@ -87,7 +86,7 @@ Thy/html.ML Thy/latex.ML Thy/present.ML Thy/term_style.ML \ Thy/thm_deps.ML Thy/thy_header.ML Thy/thy_info.ML Thy/thy_load.ML \ Thy/thy_output.ML Thy/thy_syntax.ML Tools/ROOT.ML \ - Tools/auto_solve.ML Tools/find_consts.ML Tools/find_theorems.ML Tools/named_thms.ML \ + Tools/find_consts.ML Tools/find_theorems.ML Tools/named_thms.ML \ Tools/xml_syntax.ML assumption.ML axclass.ML codegen.ML config.ML \ conjunction.ML consts.ML context.ML context_position.ML conv.ML \ defs.ML display.ML drule.ML envir.ML facts.ML goal.ML \ diff -r e54777ab68bd -r e6349035148a src/Pure/ProofGeneral/ROOT.ML --- a/src/Pure/ProofGeneral/ROOT.ML Sat Apr 25 21:42:05 2009 +0200 +++ b/src/Pure/ProofGeneral/ROOT.ML Sat Apr 25 22:29:13 2009 +0200 @@ -14,11 +14,7 @@ use "pgip_isabelle.ML"; -(use - |> setmp Proofterm.proofs 1 - |> setmp quick_and_dirty true - |> setmp Quickcheck.auto true - |> setmp auto_solve true) "preferences.ML"; +use "preferences.ML"; use "pgip_parser.ML"; diff -r e54777ab68bd -r e6349035148a src/Pure/ProofGeneral/preferences.ML --- a/src/Pure/ProofGeneral/preferences.ML Sat Apr 25 21:42:05 2009 +0200 +++ b/src/Pure/ProofGeneral/preferences.ML Sat Apr 25 22:29:13 2009 +0200 @@ -6,6 +6,10 @@ signature PREFERENCES = sig + val category_display: string + val category_advanced_display: string + val category_tracing: string + val category_proof: string type preference = {name: string, descr: string, @@ -29,6 +33,14 @@ structure Preferences: PREFERENCES = struct +(* categories *) + +val category_display = "Display"; +val category_advanced_display = "Advanced Display"; +val category_tracing = "Tracing"; +val category_proof = "Proof" + + (* preferences and preference tables *) type preference = @@ -66,11 +78,11 @@ (* preferences of Pure *) -val proof_pref = +val proof_pref = setmp Proofterm.proofs 1 (fn () => let fun get () = PgipTypes.bool_to_pgstring (! Proofterm.proofs >= 2); fun set s = Proofterm.proofs := (if PgipTypes.read_pgipbool s then 2 else 1); - in mkpref get set PgipTypes.Pgipbool "full-proofs" "Record full proof objects internally" end; + in mkpref get set PgipTypes.Pgipbool "full-proofs" "Record full proof objects internally" end) (); val thm_depsN = "thm_deps"; val thm_deps_pref = @@ -145,24 +157,13 @@ bool_pref Toplevel.debug "debugging" "Whether to enable debugging.", - bool_pref Quickcheck.auto - "auto-quickcheck" - "Whether to enable quickcheck automatically.", - nat_pref Quickcheck.auto_time_limit - "auto-quickcheck-time-limit" - "Time limit for automatic quickcheck (in milliseconds).", - bool_pref AutoSolve.auto - "auto-solve" - "Try to solve newly declared lemmas with existing theorems.", - nat_pref AutoSolve.auto_time_limit - "auto-solve-time-limit" - "Time limit for seeking automatic solutions (in milliseconds).", thm_deps_pref]; val proof_preferences = - [bool_pref quick_and_dirty - "quick-and-dirty" - "Take a few short cuts", + [setmp quick_and_dirty true (fn () => + bool_pref quick_and_dirty + "quick-and-dirty" + "Take a few short cuts") (), bool_pref Toplevel.skip_proofs "skip-proofs" "Skip over proofs (interactive-only)", @@ -175,10 +176,10 @@ "Check proofs in parallel"]; val pure_preferences = - [("Display", display_preferences), - ("Advanced Display", advanced_display_preferences), - ("Tracing", tracing_preferences), - ("Proof", proof_preferences)]; + [(category_display, display_preferences), + (category_advanced_display, advanced_display_preferences), + (category_tracing, tracing_preferences), + (category_proof, proof_preferences)]; (* table of categories and preferences; names must be unique *) diff -r e54777ab68bd -r e6349035148a src/Pure/Tools/ROOT.ML --- a/src/Pure/Tools/ROOT.ML Sat Apr 25 21:42:05 2009 +0200 +++ b/src/Pure/Tools/ROOT.ML Sat Apr 25 22:29:13 2009 +0200 @@ -1,23 +1,9 @@ -(* Title: Pure/Tools/ROOT.ML - -Miscellaneous tools and packages for Pure Isabelle. -*) +(* Miscellaneous tools and packages for Pure Isabelle *) use "named_thms.ML"; -(*basic XML support*) use "xml_syntax.ML"; use "find_theorems.ML"; use "find_consts.ML"; -use "auto_solve.ML"; - -(*quickcheck stub needed here because of pg preferences*) -structure Quickcheck = -struct - -val auto = ref false; -val auto_time_limit = ref 5000; - -end; diff -r e54777ab68bd -r e6349035148a src/Pure/Tools/auto_solve.ML --- a/src/Pure/Tools/auto_solve.ML Sat Apr 25 21:42:05 2009 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,87 +0,0 @@ -(* Title: Tools/auto_solve.ML - Author: Timothy Bourke and Gerwin Klein, NICTA - -Check whether a newly stated theorem can be solved directly by an -existing theorem. Duplicate lemmas can be detected in this way. - -The implementation is based in part on Berghofer and Haftmann's -quickcheck.ML. It relies critically on the FindTheorems solves -feature. -*) - -signature AUTO_SOLVE = -sig - val auto : bool ref - val auto_time_limit : int ref - val limit : int ref - - val seek_solution : bool -> Proof.state -> Proof.state -end; - -structure AutoSolve : AUTO_SOLVE = -struct - -val auto = ref false; -val auto_time_limit = ref 2500; -val limit = ref 5; - -fun seek_solution int state = - let - val ctxt = Proof.context_of state; - - val crits = [(true, FindTheorems.Solves)]; - fun find g = snd (FindTheorems.find_theorems ctxt (SOME g) (SOME (! limit)) false crits); - - fun prt_result (goal, results) = - let - val msg = - (case goal of - NONE => "The current goal" - | SOME sg => Syntax.string_of_term ctxt (Thm.term_of sg)); - in - Pretty.big_list - (msg ^ " could be solved directly with:") - (map (FindTheorems.pretty_thm ctxt) results) - end; - - fun seek_against_goal () = - (case try Proof.get_goal state of - NONE => NONE - | SOME (_, (_, goal)) => - let - val subgoals = Conjunction.dest_conjunctions (Thm.cprem_of goal 1); - val rs = - if length subgoals = 1 - then [(NONE, find goal)] - else map (fn sg => (SOME sg, find (Goal.init sg))) subgoals; - val results = filter_out (null o snd) rs; - in if null results then NONE else SOME results end); - - fun go () = - let - val res = - TimeLimit.timeLimit (Time.fromMilliseconds (! auto_time_limit)) - (try seek_against_goal) (); - in - (case res of - SOME (SOME results) => - state |> Proof.goal_message - (fn () => Pretty.chunks - [Pretty.str "", - Pretty.markup Markup.hilite - (separate (Pretty.brk 0) (map prt_result results))]) - | _ => state) - end handle TimeLimit.TimeOut => (warning "AutoSolve: timeout."; state); - in - if int andalso ! auto andalso not (! Toplevel.quiet) - then go () - else state - end; - -end; - -val _ = Context.>> (Specification.add_theorem_hook AutoSolve.seek_solution); - -val auto_solve = AutoSolve.auto; -val auto_solve_time_limit = AutoSolve.auto_time_limit; - diff -r e54777ab68bd -r e6349035148a src/Tools/auto_solve.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/auto_solve.ML Sat Apr 25 22:29:13 2009 +0200 @@ -0,0 +1,101 @@ +(* Title: Tools/auto_solve.ML + Author: Timothy Bourke and Gerwin Klein, NICTA + +Check whether a newly stated theorem can be solved directly by an +existing theorem. Duplicate lemmas can be detected in this way. + +The implementation is based in part on Berghofer and Haftmann's +quickcheck.ML. It relies critically on the FindTheorems solves +feature. +*) + +signature AUTO_SOLVE = +sig + val auto : bool ref + val auto_time_limit : int ref + val limit : int ref +end; + +structure AutoSolve : AUTO_SOLVE = +struct + +(* preferences *) + +val auto = ref false; +val auto_time_limit = ref 2500; +val limit = ref 5; + +val _ = + ProofGeneralPgip.add_preference Preferences.category_tracing + (setmp auto true (fn () => + Preferences.bool_pref auto + "auto-solve" + "Try to solve newly declared lemmas with existing theorems.") ()); + +val _ = + ProofGeneralPgip.add_preference Preferences.category_tracing + (Preferences.nat_pref auto_time_limit + "auto-solve-time-limit" + "Time limit for seeking automatic solutions (in milliseconds)."); + + +(* hook *) + +val _ = Context.>> (Specification.add_theorem_hook (fn int => fn state => + let + val ctxt = Proof.context_of state; + + val crits = [(true, FindTheorems.Solves)]; + fun find g = snd (FindTheorems.find_theorems ctxt (SOME g) (SOME (! limit)) false crits); + + fun prt_result (goal, results) = + let + val msg = + (case goal of + NONE => "The current goal" + | SOME sg => Syntax.string_of_term ctxt (Thm.term_of sg)); + in + Pretty.big_list + (msg ^ " could be solved directly with:") + (map (FindTheorems.pretty_thm ctxt) results) + end; + + fun seek_against_goal () = + (case try Proof.get_goal state of + NONE => NONE + | SOME (_, (_, goal)) => + let + val subgoals = Conjunction.dest_conjunctions (Thm.cprem_of goal 1); + val rs = + if length subgoals = 1 + then [(NONE, find goal)] + else map (fn sg => (SOME sg, find (Goal.init sg))) subgoals; + val results = filter_out (null o snd) rs; + in if null results then NONE else SOME results end); + + fun go () = + let + val res = + TimeLimit.timeLimit (Time.fromMilliseconds (! auto_time_limit)) + (try seek_against_goal) (); + in + (case res of + SOME (SOME results) => + state |> Proof.goal_message + (fn () => Pretty.chunks + [Pretty.str "", + Pretty.markup Markup.hilite + (separate (Pretty.brk 0) (map prt_result results))]) + | _ => state) + end handle TimeLimit.TimeOut => (warning "AutoSolve: timeout."; state); + in + if int andalso ! auto andalso not (! Toplevel.quiet) + then go () + else state + end)); + +end; + +val auto_solve = AutoSolve.auto; +val auto_solve_time_limit = AutoSolve.auto_time_limit; + diff -r e54777ab68bd -r e6349035148a src/Tools/quickcheck.ML --- a/src/Tools/quickcheck.ML Sat Apr 25 21:42:05 2009 +0200 +++ b/src/Tools/quickcheck.ML Sat Apr 25 22:29:13 2009 +0200 @@ -6,16 +6,34 @@ signature QUICKCHECK = sig - val test_term: Proof.context -> bool -> string option -> int -> int -> term -> (string * term) list option; - val add_generator: string * (Proof.context -> term -> int -> term list option) -> theory -> theory val auto: bool ref val auto_time_limit: int ref + val test_term: Proof.context -> bool -> string option -> int -> int -> term -> + (string * term) list option + val add_generator: string * (Proof.context -> term -> int -> term list option) -> theory -> theory end; structure Quickcheck : QUICKCHECK = struct -open Quickcheck; (*c.f. Pure/Tools/ROOT.ML*) +(* preferences *) + +val auto = ref false; +val auto_time_limit = ref 2500; + +val _ = + ProofGeneralPgip.add_preference Preferences.category_tracing + (setmp auto true (fn () => + Preferences.bool_pref auto + "auto-quickcheck" + "Whether to enable quickcheck automatically.") ()); + +val _ = + ProofGeneralPgip.add_preference Preferences.category_tracing + (Preferences.nat_pref auto_time_limit + "auto-quickcheck-time-limit" + "Time limit for automatic quickcheck (in milliseconds)."); + (* quickcheck configuration -- default parameters, test generators *) @@ -140,7 +158,7 @@ (* automatic testing *) -fun test_goal_auto int state = +val _ = Context.>> (Specification.add_theorem_hook (fn int => fn state => let val ctxt = Proof.context_of state; val assms = map term_of (Assumption.all_assms_of ctxt); @@ -161,12 +179,10 @@ if int andalso !auto andalso not (!Toplevel.quiet) then test () else state - end; - -val _ = Context.>> (Specification.add_theorem_hook test_goal_auto); + end)); -(* Isar interfaces *) +(* Isar commands *) fun read_nat s = case (Library.read_int o Symbol.explode) s of (k, []) => if k >= 0 then k